Poset matrices and quasi-full rooted trees

DefinitionPoset matrix#✓fully proved

An \(n \times n\) Boolean matrix \(M\), with rows and columns indexed by \(\{0, \dots, n-1\}\), is an upper-triangular \((0, 1)\)-poset matrix when its entries strictly below the main diagonal are false (\(M_{ij}\) is false whenever \(j < i\)), its diagonal entries \(M_{ii}\) are true, and its true entries are transitive: if \(M_{ij}\) and \(M_{jk}\) are true, then \(M_{ik}\) is true.

def IsPosetMatrix (n : ℕ) (M : Matrix (Fin n) (Fin n) Bool) : Prop :=
  (∀ i j : Fin n, (j : ℕ) < (i : ℕ) → M i j = false) ∧
    (∀ i : Fin n, M i i = true) ∧
    (∀ i j k : Fin n, M i j = true → M j k = true → M i k = true)

Sources

• JIS mohammad3.tex, lines 171–176.

Used by 9

Used byBlock properties decide connectedness of the represented poset · Diagonal entries of a poset matrix · Direct and ordinal sums of poset matrices represent sums of posets · Block decomposition of a poset matrix · Direct sum criterion for relabeling inequivalence · The relation of a poset matrix is reflexive · The relation of a poset matrix is transitive · Transitivity of the true entries of a poset matrix · Poset matrices are upper triangular

DefinitionRelation represented by a Boolean matrix#✓fully proved

Let \(M\) be an \(n \times n\) Boolean matrix with rows and columns indexed by \(\{0, \dots, n-1\}\). The relation represented by \(M\) relates index \(i\) to index \(j\) exactly when the entry \(M_{ij}\) is true.

The matrix \(M\) is arbitrary; it need not be a poset matrix.

def IsPosetMatrix.Rel {n : ℕ} (M : Matrix (Fin n) (Fin n) Bool)
    (i j : Fin n) : Prop :=
  M i j = true

Used by 2

Used byThe relation of a poset matrix is reflexive · The relation of a poset matrix is transitive

TheoremPoset matrices are upper triangular#✓fully proved

If \(M\) is an \(n \times n\) poset matrix, then \(M_{ij}\) is false for all indices \(i, j < n\) with \(j < i\).

theorem IsPosetMatrix.upper {n : ℕ} {M : Matrix (Fin n) (Fin n) Bool}
    (h : IsPosetMatrix n M) :
    ∀ i j : Fin n, (j : ℕ) < (i : ℕ) → M i j = false

Uses 1

Statement usesPoset matrix

TheoremDiagonal entries of a poset matrix#✓fully proved

If \(M\) is an \(n \times n\) poset matrix, then \(M_{ii}\) is true for every index \(i < n\).

theorem IsPosetMatrix.diagonal {n : ℕ} {M : Matrix (Fin n) (Fin n) Bool}
    (h : IsPosetMatrix n M) : ∀ i : Fin n, M i i = true

Uses 1

Statement usesPoset matrix

TheoremTransitivity of the true entries of a poset matrix#✓fully proved

If \(M\) is an \(n \times n\) poset matrix, then for all indices \(i, j, k < n\), if \(M_{ij}\) and \(M_{jk}\) are true, then \(M_{ik}\) is true.

theorem IsPosetMatrix.transitive {n : ℕ}
    {M : Matrix (Fin n) (Fin n) Bool} (h : IsPosetMatrix n M) :
    ∀ i j k : Fin n, M i j = true → M j k = true → M i k = true

Uses 1

Statement usesPoset matrix

TheoremThe relation of a poset matrix is reflexive#✓fully proved

If \(M\) is an \(n \times n\) poset matrix, then the relation represented by \(M\) relates every index \(i < n\) to itself.

theorem IsPosetMatrix.rel_refl {n : ℕ} {M : Matrix (Fin n) (Fin n) Bool}
    (h : IsPosetMatrix n M) (i : Fin n) :
    IsPosetMatrix.Rel M i i

Uses 2

Statement usesPoset matrix · Relation represented by a Boolean matrix

TheoremThe relation of a poset matrix is transitive#✓fully proved

If \(M\) is an \(n \times n\) poset matrix and \(i, j, k < n\) are indices such that the relation represented by \(M\) relates \(i\) to \(j\) and \(j\) to \(k\), then it relates \(i\) to \(k\).

theorem IsPosetMatrix.rel_trans {n : ℕ} {M : Matrix (Fin n) (Fin n) Bool}
    (h : IsPosetMatrix n M) (i j k : Fin n)
    (hij : IsPosetMatrix.Rel M i j)
    (hjk : IsPosetMatrix.Rel M j k) :
    IsPosetMatrix.Rel M i k

Uses 2

Statement usesPoset matrix · Relation represented by a Boolean matrix

TheoremBlock decomposition of a poset matrix#●ready to prove

Let \(m, k \ge 1\) and let \(M\) be a poset matrix of order \(m + k\), a Boolean matrix with rows and columns indexed by \(0, \dots, m + k - 1\). Then \(M_{ij}\) is false for all \(i < m \le j\) if and only if there are poset matrices \(A\) of order \(m\) and \(B\) of order \(k\) such that \(M\) is their direct sum: \(M_{ij} = A_{ij}\) for \(i, j < m\), \(M_{m+i, m+j} = B_{ij}\) for \(i, j < k\), and every other entry of \(M\) is false. Likewise \(M_{ij}\) is true for all \(i < m \le j\) if and only if there are poset matrices \(A\) of order \(m\) and \(B\) of order \(k\) such that \(M\) is their ordinal sum: the same diagonal blocks, \(M_{ij}\) true for all \(i < m \le j\), and \(M_{ij}\) false for all \(j < m \le i\).

Only one block length is stated; the version with several lengths \(n_1 < \dots < n_r\) follows by iterating it.

public theorem_wanted isPosetMatrix_block_iff_directSum_ordinalSum (m k : ℕ) (hm : 1 ≤ m)
    (hk : 1 ≤ k) (M : Matrix (Fin (m + k)) (Fin (m + k)) Bool) (hM : IsPosetMatrix (m + k) M) :
    ((∀ i j : Fin (m + k), (i : ℕ) < m → m ≤ (j : ℕ) → M i j = false) ↔
      ∃ A : Matrix (Fin m) (Fin m) Bool, ∃ B : Matrix (Fin k) (Fin k) Bool,
        IsPosetMatrix m A ∧ IsPosetMatrix k B ∧
          M = reindex finSumFinEquiv finSumFinEquiv
            (fromBlocks A (Matrix.of fun _ _ => false) (Matrix.of fun _ _ => false) B)) ∧
    ((∀ i j : Fin (m + k), (i : ℕ) < m → m ≤ (j : ℕ) → M i j = true) ↔
      ∃ A : Matrix (Fin m) (Fin m) Bool, ∃ B : Matrix (Fin k) (Fin k) Bool,
        IsPosetMatrix m A ∧ IsPosetMatrix k B ∧
          M = reindex finSumFinEquiv finSumFinEquiv
            (fromBlocks A (Matrix.of fun _ _ => true) (Matrix.of fun _ _ => false) B))

Sources

• Salah Uddin Mohammad, Md. Shah Noor, and Md. Rashed Talukder, Recognition and Enumeration of the Quasi-Full Rooted Trees, Journal of Integer Sequences 28 (2025), Article 25.6.3, Theorem 3 (jis-2025-25.6.3-thm-3).

Uses 1

Statement usesPoset matrix

TheoremDirect and ordinal sums of poset matrices represent sums of posets#●ready to prove

A poset matrix \(M\) of order \(n\), a Boolean matrix with rows and columns indexed by \(0, \dots, n - 1\), represents a partial order \(P\) when there is a bijection \(e\) from \(\{0, \dots, n - 1\}\) to \(P\) such that \(e(i) \le e(j)\) if and only if \(M_{ij}\) is true. Let \(A\) and \(B\) be poset matrices of orders \(m\) and \(k\) representing partial orders \(P\) and \(Q\). Let \(A \oplus B\) and \(A \boxplus B\) be the matrices \(N\) of order \(m + k\) with \(N_{ij} = A_{ij}\) for \(i, j < m\), \(N_{m+i, m+j} = B_{ij}\) for \(i, j < k\), and \(N_{ij}\) false for all \(j < m \le i\), where \(N_{ij}\) for \(i < m \le j\) is false in \(A \oplus B\) and true in \(A \boxplus B\). Then \(A \oplus B\) is a poset matrix representing the disjoint sum \(P + Q\), in which no element of \(P\) is comparable with an element of \(Q\), and \(A \boxplus B\) is a poset matrix representing the ordinal sum \(P \oplus Q\), in which every element of \(P\) lies below every element of \(Q\).

Only sums of two terms are stated; sums of \(r\) terms follow by iterating.

MetaMathlibExt.directSum_ordinalSum_represents · 16 lines

public theorem_wanted directSum_ordinalSum_represents {P Q : Type*} [PartialOrder P]
    [PartialOrder Q] (m k : ℕ) (A : Matrix (Fin m) (Fin m) Bool) (B : Matrix (Fin k) (Fin k) Bool)
    (hA : IsPosetMatrix m A) (hB : IsPosetMatrix k B) (eA : Fin m ≃ P)
    (heA : ∀ i j, eA i ≤ eA j ↔ A i j = true) (eB : Fin k ≃ Q)
    (heB : ∀ i j, eB i ≤ eB j ↔ B i j = true) :
    (IsPosetMatrix (m + k) (reindex finSumFinEquiv finSumFinEquiv
        (fromBlocks A (Matrix.of fun _ _ => false) (Matrix.of fun _ _ => false) B)) ∧
      ∃ e : Fin (m + k) ≃ P ⊕ Q, ∀ i j, e i ≤ e j ↔
        reindex finSumFinEquiv finSumFinEquiv
          (fromBlocks A (Matrix.of fun _ _ => false) (Matrix.of fun _ _ => false) B) i j =
            true) ∧
    (IsPosetMatrix (m + k) (reindex finSumFinEquiv finSumFinEquiv
        (fromBlocks A (Matrix.of fun _ _ => true) (Matrix.of fun _ _ => false) B)) ∧
      ∃ e : Fin (m + k) ≃ P ⊕ₗ Q, ∀ i j, e i ≤ e j ↔
        reindex finSumFinEquiv finSumFinEquiv
          (fromBlocks A (Matrix.of fun _ _ => true) (Matrix.of fun _ _ => false) B) i j = true)

Sources

• Salah Uddin Mohammad, Md. Shah Noor, and Md. Rashed Talukder, Recognition and Enumeration of the Quasi-Full Rooted Trees, Journal of Integer Sequences 28 (2025), Article 25.6.3, Theorem 4 (jis-2025-25.6.3-thm-4).

Uses 1

Statement usesPoset matrix

TheoremBlock properties decide connectedness of the represented poset#●ready to prove

Let \(M\) be a poset matrix of order \(n\), a Boolean matrix with rows and columns indexed by \(0, \dots, n - 1\), that represents a partial order \(P\): there is a bijection \(e\) from \(\{0, \dots, n - 1\}\) to \(P\) such that \(e(i) \le e(j)\) if and only if \(M_{ij}\) is true. Let \(1 \le r < n\). If \(M_{ij}\) is true for all \(i < r \le j\) (the block of \(1\)s property of length \(r\)), then \(P\) is connected: every subset \(S\) of \(P\) such that \(x \in S \iff y \in S\) whenever \(x \le y\) is empty or all of \(P\). If \(M_{ij}\) is false for all \(i < r \le j\) (the block of \(0\)s property of length \(r\)), then \(P\) is disconnected: some nonempty subset \(S\) of \(P\) with nonempty complement satisfies \(x \in S \iff y \in S\) whenever \(x \le y\).

Since a relabeling of \(M\) represents the same poset, this also covers matrices that satisfy a block property after relabeling.

public theorem_wanted connected_or_disconnected_of_block_property {P : Type*} [PartialOrder P]
    (n : ℕ) (M : Matrix (Fin n) (Fin n) Bool) (hM : IsPosetMatrix n M) (e : Fin n ≃ P)
    (he : ∀ i j, e i ≤ e j ↔ M i j = true) (r : ℕ) (hr₁ : 1 ≤ r) (hr₂ : r < n) :
    ((∀ i j : Fin n, (i : ℕ) < r → r ≤ (j : ℕ) → M i j = true) →
      ∀ S : Set P, (∀ x y : P, x ≤ y → (x ∈ S ↔ y ∈ S)) → S = ∅ ∨ S = Set.univ) ∧
    ((∀ i j : Fin n, (i : ℕ) < r → r ≤ (j : ℕ) → M i j = false) →
      ∃ S : Set P, S.Nonempty ∧ Sᶜ.Nonempty ∧ ∀ x y : P, x ≤ y → (x ∈ S ↔ y ∈ S))

Sources

• Salah Uddin Mohammad, Md. Shah Noor, and Md. Rashed Talukder, Recognition and Enumeration of the Quasi-Full Rooted Trees, Journal of Integer Sequences 28 (2025), Article 25.6.3, Theorem 5 (jis-2025-25.6.3-thm-5).

Uses 1

Statement usesPoset matrix

TheoremArity of quasi-full rooted trees#●ready to prove

Let \(P\) be a finite partial order with \(n \ge 3\) elements that is a rooted tree: \(P\) has a least element and, for every \(x \in P\), the elements below \(x\) form a chain. For a natural number \(t\), call \(P\) quasi-full \(t\)-ary when every \(x \in P\) is covered by exactly \(\min(|U_x| - 1, t)\) elements of \(P\), where \(U_x = \{y \in P : x \le y\}\). Then (i) if \(P\) is quasi-full \((n - 1)\)-ary, it is quasi-full \(t\)-ary for every \(t \ge n\); and (ii) if \(P\) is quasi-full \(t\)-ary for some \(t \le n - 2\), it is not quasi-full \(t'\)-ary for any \(t' \ge n\).

The source states this for poset matrices representing quasi-full \(t\)-ary rooted trees; both parts depend only on the represented poset.

public theorem_wanted quasiFullTree_arity {P : Type*} [PartialOrder P] [Fintype P]
    (hn : 3 ≤ Fintype.card P) (hroot : ∃ ρ : P, ∀ x, ρ ≤ x)
    (hchain : ∀ x : P, IsChain (· ≤ ·) (Set.Iic x)) :
    ((∀ x : P, Nat.card {y : P // x ⋖ y} =
        min (Nat.card (Set.Ici x) - 1) (Fintype.card P - 1)) →
      ∀ t, Fintype.card P ≤ t →
        ∀ x : P, Nat.card {y : P // x ⋖ y} = min (Nat.card (Set.Ici x) - 1) t) ∧
    (∀ t, t ≤ Fintype.card P - 2 →
      (∀ x : P, Nat.card {y : P // x ⋖ y} = min (Nat.card (Set.Ici x) - 1) t) →
        ∀ t', Fintype.card P ≤ t' →
          ¬ ∀ x : P, Nat.card {y : P // x ⋖ y} = min (Nat.card (Set.Ici x) - 1) t')

Sources

• Salah Uddin Mohammad, Md. Shah Noor, and Md. Rashed Talukder, Recognition and Enumeration of the Quasi-Full Rooted Trees, Journal of Integer Sequences 28 (2025), Article 25.6.3, Theorem 10 (jis-2025-25.6.3-thm-10).

TheoremDirect sum criterion for relabeling inequivalence#●ready to prove

Let \(n, t \ge 2\) and let \(M\) and \(M'\) be poset matrices of order \(n\), Boolean matrices with rows and columns indexed by \(0, \dots, n - 1\). Let \(0 = l_0 < l_1 < \dots < l_t = n\) be such that the gaps \(l_{k+1} - l_k\) are nondecreasing in \(k\). Suppose that for every \(k \le t\), \(M_{ij}\) is false for all \(i < l_k \le j\), and that for every \(k < t\) there is \(s \ge 1\) with \(l_k + s < l_{k+1}\) such that \(M_{ij}\) is true for all \(i, j\) with \(l_k \le i < l_k + s \le j < l_{k+1}\). Suppose the same of \(M'\) with a sequence \(0 = l'_0 < l'_1 < \dots < l'_t = n\) whose gaps are nondecreasing. If \(l_k \ne l'_k\) for some \(k\), then \(M\) and \(M'\) are not relabeling equivalent: there is no permutation \(\sigma\) of \(\{0, \dots, n - 1\}\) with \(M'_{ij} = M_{\sigma(i) \sigma(j)}\) for all \(i, j\).

The source assumes in addition that \(M\) and \(M'\) represent quasi-full \(t\)-ary rooted forests; the statement holds without that assumption.

MetaMathlibExt.not_relabel_equiv_of_blockLengths_ne · 18 lines

public theorem_wanted not_relabel_equiv_of_blockLengths_ne (n t : ℕ) (hn : 2 ≤ n) (ht : 2 ≤ t)
    (M M' : Matrix (Fin n) (Fin n) Bool) (hM : IsPosetMatrix n M) (hM' : IsPosetMatrix n M')
    (l l' : Fin (t + 1) → ℕ)
    (hl : l 0 = 0 ∧ l (Fin.last t) = n ∧ StrictMono l ∧
      Monotone fun k : Fin t => l k.succ - l k.castSucc)
    (hl' : l' 0 = 0 ∧ l' (Fin.last t) = n ∧ StrictMono l' ∧
      Monotone fun k : Fin t => l' k.succ - l' k.castSucc)
    (hzero : ∀ k : Fin (t + 1), ∀ i j : Fin n, (i : ℕ) < l k → l k ≤ (j : ℕ) → M i j = false)
    (hzero' : ∀ k : Fin (t + 1), ∀ i j : Fin n, (i : ℕ) < l' k → l' k ≤ (j : ℕ) →
      M' i j = false)
    (hone : ∀ k : Fin t, ∃ s, 1 ≤ s ∧ l k.castSucc + s < l k.succ ∧
      ∀ i j : Fin n, l k.castSucc ≤ (i : ℕ) → (i : ℕ) < l k.castSucc + s →
        l k.castSucc + s ≤ (j : ℕ) → (j : ℕ) < l k.succ → M i j = true)
    (hone' : ∀ k : Fin t, ∃ s, 1 ≤ s ∧ l' k.castSucc + s < l' k.succ ∧
      ∀ i j : Fin n, l' k.castSucc ≤ (i : ℕ) → (i : ℕ) < l' k.castSucc + s →
        l' k.castSucc + s ≤ (j : ℕ) → (j : ℕ) < l' k.succ → M' i j = true)
    (hne : l ≠ l') :
    ¬ ∃ σ : Equiv.Perm (Fin n), M' = M.submatrix σ σ

Sources

• Salah Uddin Mohammad, Md. Shah Noor, and Md. Rashed Talukder, Recognition and Enumeration of the Quasi-Full Rooted Trees, Journal of Integer Sequences 28 (2025), Article 25.6.3, Theorem 11 (jis-2025-25.6.3-thm-11).

Uses 1

Statement usesPoset matrix

7 fully proved5 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.