Perfect compositions

TheoremPerfect compositions are permuted perfect partitions#✓fully proved

Call a list \(L\) of positive integers perfect for \(n\) if for every integer \(m\) with \(0 < m < n\) there is exactly one list of integers that is a sublist of \(L\) (its entries taken in order, not necessarily contiguous) and has sum \(m\). A symbolic part \((a, u)\) with \(a, u > 0\) stands for a run of \(u\) copies of \(a\), and the expansion of a list of symbolic parts is the concatenation of their runs. Let \(n\) be a natural number and let \(C\) be a list of symbolic parts, any two adjacent ones having different values \(a\), whose expansion has sum \(n\). Then the expansion of \(C\) is perfect for \(n\) if and only if \(C\) is a permutation of a list \(P\) of symbolic parts \((a, u)\) with \(a, u > 0\) and strictly increasing values \(a\) whose expansion has sum \(n\) and is perfect for \(n\).

MetaMathlibExt.perfect_composition_iff_symbolic_parts_perm_perfect_partition_general · 18 lines 
theorem perfect_composition_iff_symbolic_parts_perm_perfect_partition_general
    (n : ℕ)
    (C : List (ℕ × ℕ))
    (hCpos : ∀ p ∈ C, 0 < p.1 ∧ 0 < p.2)
    (hCadj : (C.map Prod.fst).IsChain (· ≠ ·))
    (hCsum : (C.flatMap fun p => List.replicate p.2 p.1).foldr (· + ·) 0 = n) :
    let expand : List (ℕ × ℕ) → List ℕ :=
      fun S => S.flatMap fun p => List.replicate p.2 p.1
    let IsPerfect : List (ℕ × ℕ) → ℕ → Prop :=
      fun S k =>
        ∀ m : ℕ, 0 < m → m < k →
          ∃! D : List ℕ, D.Sublist (expand S) ∧ D.foldr (· + ·) 0 = m
    IsPerfect C n ↔
      ∃ P : List (ℕ × ℕ),
        (∀ p ∈ P, 0 < p.1 ∧ 0 < p.2) ∧
        (P.map Prod.fst).Pairwise (· < ·) ∧
        (expand P).foldr (· + ·) 0 = n ∧
        IsPerfect P n ∧ C.Perm P
Used by 1
Used byMunagi's theorem on perfect compositions

TheoremMunagi's theorem on perfect compositions#✓fully proved

Call a list \(L\) of positive integers perfect for \(n\) if for every integer \(m\) with \(0 < m < n\) there is exactly one list of integers that is a sublist of \(L\) (its entries taken in order, not necessarily contiguous) and has sum \(m\). A symbolic part \((a, u)\) with \(a, u > 0\) stands for a run of \(u\) copies of \(a\), and the expansion of a list of symbolic parts is the concatenation of their runs. Let \(n > 0\) and let \(C\) be a list of symbolic parts, any two adjacent ones having different values \(a\), whose expansion has sum \(n\). Then the expansion of \(C\) is perfect for \(n\) if and only if \(C\) is a permutation of a list \(P\) of symbolic parts \((a, u)\) with \(a, u > 0\) and strictly increasing values \(a\) whose expansion has sum \(n\) and is perfect for \(n\).

MetaMathlibExt.perfect_composition_iff_symbolic_parts_perm_perfect_partition · 20 lines 
@[nolint unusedArguments]
theorem perfect_composition_iff_symbolic_parts_perm_perfect_partition
    (n : ℕ)
    (hn : 0 < n)
    (C : List (ℕ × ℕ))
    (hCpos : ∀ p ∈ C, 0 < p.1 ∧ 0 < p.2)
    (hCadj : (C.map Prod.fst).IsChain (· ≠ ·))
    (hCsum : (C.flatMap fun p => List.replicate p.2 p.1).foldr (· + ·) 0 = n) :
    let expand : List (ℕ × ℕ) → List ℕ :=
      fun S => S.flatMap fun p => List.replicate p.2 p.1
    let IsPerfect : List (ℕ × ℕ) → ℕ → Prop :=
      fun S k =>
        ∀ m : ℕ, 0 < m → m < k →
          ∃! D : List ℕ, D.Sublist (expand S) ∧ D.foldr (· + ·) 0 = m
    IsPerfect C n ↔
      ∃ P : List (ℕ × ℕ),
        (∀ p ∈ P, 0 < p.1 ∧ 0 < p.2) ∧
        (P.map Prod.fst).Pairwise (· < ·) ∧
        (expand P).foldr (· + ·) 0 = n ∧
        IsPerfect P n ∧ C.Perm P
Sources
Uses 1
Proof usesPerfect compositions are permuted perfect partitions
2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.