Factorial ledger for the collapse coordinates

The inverse ((s+1)!)⁻¹ in (5.45) comes only from the normalization of paperSum. Collapsing all inside blocks to one marker introduces a marker of multiplicity k = s+1 in the contracted alphabet. Consequently, the product of the inside and contracted factorial ledgers is exactly k! times the original ledger.

No fiber cardinality is used here.

def Anderson4D.sumMultiplicity {A : Type u_1} {B : Type u_2} (a : A → ℕ) (b : B → ℕ) : A ⊕ B → ℕ

Multiplicity on a split alphabet.

Equations

• Anderson4D.sumMultiplicity a b (Sum.inl x_1) = a x_1
• Anderson4D.sumMultiplicity a b (Sum.inr y) = b y

def Anderson4D.markerMultiplicity {B : Type u_1} (k : ℕ) (b : B → ℕ) : Unit ⊕ B → ℕ

Multiplicity on the contracted alphabet: one marker with multiplicity k, and all outside multiplicities unchanged.

Equations

• Anderson4D.markerMultiplicity k b (Sum.inl val) = k
• Anderson4D.markerMultiplicity k b (Sum.inr y) = b y

theorem Anderson4D.factorialLedger_sum {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] (a : A → ℕ) (b : B → ℕ) : ∏ x : A ⊕ B, ↑(sumMultiplicity a b x).factorial = (∏ x : A, ↑(a x).factorial) * ∏ y : B, ↑(b y).factorial

A factorial product over a sum type splits exactly.

theorem Anderson4D.factorialLedger_marker {B : Type u_1} [Fintype B] (k : ℕ) (b : B → ℕ) : ∏ x : Unit ⊕ B, ↑(markerMultiplicity k b x).factorial = ↑k.factorial * ∏ y : B, ↑(b y).factorial

The contracted ledger is the marker factorial times the outside ledger.

theorem Anderson4D.collapse_factorialLedger {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] (a : A → ℕ) (b : B → ℕ) (k : ℕ) : (∏ x : A, ↑(a x).factorial) * ∏ x : Unit ⊕ B, ↑(markerMultiplicity k b x).factorial = ↑k.factorial * ∏ x : A ⊕ B, ↑(sumMultiplicity a b x).factorial

Collapse factorial ledger. Inside ledger times contracted ledger equals the new marker factorial times the original ledger.

theorem Anderson4D.factorialLedger_sum_eq_inv_marker_mul {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] (a : A → ℕ) (b : B → ℕ) (k : ℕ) : ∏ x : A ⊕ B, ↑(sumMultiplicity a b x).factorial = (↑k.factorial)⁻¹ * ((∏ x : A, ↑(a x).factorial) * ∏ x : Unit ⊕ B, ↑(markerMultiplicity k b x).factorial)

Division form used in (5.44)--(5.45). This is the unique source of (k!)⁻¹; the word-collapse map itself remains an honest equivalence.