Tree-facing exact reindexing for the Proposition 5.9 collapse

This file packages the word-collapse equivalence in the precise form used by the induction. The original primitive separated paper sum becomes a sum over raw collapse data, with the marker inverse factorial inserted by the factorial ledger. No fiber cardinality is introduced.

Finite and list chain weights

theorem Anderson4D.alphabetChainWeight_eq_listChainProduct {α : Type u_3} {m : ℕ} (z : α → Fin 4 → ℤ) (w : Fin m → α) : alphabetChainWeight z w = listChainProduct (fun (x y : α) => latticeEdgeWeight (z x) (z y)) (List.ofFn w)

The alphabet-valued chain weight is the corresponding consecutive-edge product on the underlying list.

The inverse collapse word

@[simp]

theorem Anderson4D.ofFn_finWordRawCollapseEquiv_symm {A : Type u_1} {B : Type u_2} [DecidableEq A] [DecidableEq B] {n : ℕ} (d : FixedRawCollapseData A B n) : List.ofFn ((finWordRawCollapseEquiv A B n).symm d) = (↑d).expandWord

Re-expanding inverse finite collapse coordinates recovers their stored expanded list exactly.

noncomputable def Anderson4D.rawPrimitiveSeparatedChainWeight {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] [DecidableEq A] [DecidableEq B] (z : A ⊕ B → Fin 4 → ℤ) (d : RawCollapseData A B) : ℝ

Primitive separated chain statistic written directly on raw collapse coordinates.

Equations

• One or more equations did not get rendered due to their size.

theorem Anderson4D.primitiveSeparatedAlphabetChainWeight_collapse_symm {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] [DecidableEq A] [DecidableEq B] {n : ℕ} (z : A ⊕ B → Fin 4 → ℤ) (d : FixedRawCollapseData A B n) : primitiveSeparatedAlphabetChainWeight z ((finWordRawCollapseEquiv A B n).symm d) = rawPrimitiveSeparatedChainWeight z ↑d

Pointwise compatibility of the raw statistic with the inverse finite collapse equivalence.

Exact tree-facing sum formula

theorem Anderson4D.paperSum_primitiveSeparated_eq_sum_collapseData {t : PlaneTree} {m : ℕ} (mu : t.Multiplicities) (r : t.VPos) (z : HeppLeaf t → Fin 4 → ℤ) : paperSum (leafMultiplicity mu) (primitiveSeparatedChainWeight z) = ∑ d : FixedRawCollapseData (InsideLeaf r) (OutsideLeaf r) m, if CollapseMultiplicitySpec (splitLeafMultiplicity mu r) ↑d then (↑(↑d).blocks.length.factorial)⁻¹ * ((∏ a : InsideLeaf r, ↑(insideMultiplicity (splitLeafMultiplicity mu r) a).factorial) * ∏ x : Unit ⊕ OutsideLeaf r, ↑(collapsedMultiplicity (splitLeafMultiplicity mu r) (↑d) x).factorial) * rawPrimitiveSeparatedChainWeight (splitLeafPosition r z) ↑d else 0

Exact collapse reindexing of the left side of Proposition 5.9.

The factor (blocks.length !)⁻¹ is the marker factorial ledger. The theorem is an equality, so later estimates may work pointwise on a raw collapse datum without assuming uniqueness or introducing a quotient argument.