Exponential bounds for multiplicity and relabelling choices

This file isolates the two elementary exponential counts used between paper equations (5.8) and (5.9). A positive tuple with prescribed total is a composition after the index order is fixed. Consequently the number of such tuples is at most 2 ^ total.

Using labelled slots here is deliberate: it bounds both the initial multiplicity choice and the later χ assignment without introducing a factorial for permuting leaves.

def Anderson4D.PositiveTuple (r total : ℕ) : Type

Positive r-tuples with sum total. Values use a bounded carrier so the type is finite without any classical finite-set truncation.

Equations

• Anderson4D.PositiveTuple r total = { f : Fin r → Fin (total + 1) // (∀ (i : Fin r), 0 < ↑(f i)) ∧ ∑ i : Fin r, ↑(f i) = total }

@[implicit_reducible]

instance Anderson4D.PositiveTuple.instFintype (r total : ℕ) : Fintype (PositiveTuple r total)

Equations

• Anderson4D.PositiveTuple.instFintype r total = { elems := Anderson4D.PositiveTuple.instFintype._aux_1 r total, complete := ⋯ }

def Anderson4D.PositiveTuple.toComposition {r total : ℕ} (f : PositiveTuple r total) : Composition total

Forget the fixed length of a positive tuple and regard it as an integer composition.

Equations

• f.toComposition = { blocks := List.ofFn fun (i : Fin r) => ↑(↑f i), blocks_pos := ⋯, blocks_sum := ⋯ }

theorem Anderson4D.PositiveTuple.toComposition_injective {r total : ℕ} : Function.Injective toComposition

The ordered list of blocks remembers the original tuple.

theorem Anderson4D.PositiveTuple.card_le_two_pow (r total : ℕ) : Fintype.card (PositiveTuple r total) ≤ 2 ^ total

The number of positive ordered tuples of any fixed length and total total is exponentially bounded. This is the count used for both the (m_l) and χ choices in paper (5.8)--(5.9).

def Anderson4D.PositiveAssignment (ι : Type u_1) [Fintype ι] (total : ℕ) : Type u_1

Positive assignments on an arbitrary finite labelled carrier with prescribed total. This is the form used for leaf multiplicities and for the χ assignment to an enumeration of the realized set.

Equations

• Anderson4D.PositiveAssignment ι total = { f : ι → Fin (total + 1) // (∀ (i : ι), 0 < ↑(f i)) ∧ ∑ i : ι, ↑(f i) = total }

@[implicit_reducible]

noncomputable instance Anderson4D.PositiveAssignment.instFintype {ι : Type u_1} [Fintype ι] (total : ℕ) : Fintype (PositiveAssignment ι total)

Equations

• Anderson4D.PositiveAssignment.instFintype total = { elems := Anderson4D.PositiveAssignment.instFintype._aux_1 total, complete := ⋯ }

noncomputable def Anderson4D.PositiveAssignment.toComposition {ι : Type u_1} [Fintype ι] {total : ℕ} (f : PositiveAssignment ι total) : Composition total

Canonically order a finite labelled carrier and read an assignment as a composition.

Equations

• f.toComposition = { blocks := List.ofFn fun (i : Fin (Fintype.card ι)) => ↑(↑f ((Fintype.equivFin ι).symm i)), blocks_pos := ⋯, blocks_sum := ⋯ }

theorem Anderson4D.PositiveAssignment.toComposition_injective {ι : Type u_1} [Fintype ι] {total : ℕ} : Function.Injective toComposition

theorem Anderson4D.PositiveAssignment.card_le_two_pow {ι : Type u_1} [Fintype ι] (total : ℕ) : Fintype.card (PositiveAssignment ι total) ≤ 2 ^ total

Paper (5.8)--(5.9): assignments to any finite labelled carrier have no factorial loss.