Copy-permutation bridge for the single-scale class words

The factorial ledger converts the paper sum to labeled arrangements. The outer dyadic argument instead counts (N,X) words refining a fixed P word. This file proves that the actual arrangement carrier maps canonically into those class-word carriers:

• every labeled arrangement induces a valid active (N,X) word;
• its image is a valid active P word;
• the (N,X) word belongs to validRefinements above that P word.

Consequently the conditional count in paper (5.79) applies directly to an actual copy permutation, rather than only to an abstract compatible word.

A generic composition-of-fibers lemma

def Anderson4D.composedWordFiberEquiv {δ : Type u_1} {ι : Type u_2} {κ : Type u_3} (g : ι → κ) (w : δ → ι) (b : κ) : { j : δ // g (w j) = b } ≃ (a : { i : ι // g i = b }) × { j : δ // w j = ↑a }

The fiber of a composite word g ∘ w is the sigma of the fibers of w over all fine letters mapping to the prescribed coarse letter.

Equations

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

theorem Anderson4D.card_comp_word_fiber {δ : Type u_1} {ι : Type u_2} {κ : Type u_3} [Fintype δ] [Fintype ι] [DecidableEq δ] [DecidableEq ι] [DecidableEq κ] (g : ι → κ) (w : δ → ι) (b : κ) : {j : δ | g (w j) = b}.card = ∑ a : { i : ι // g i = b }, {j : δ | w j = ↑a}.card

Cardinality form of composedWordFiberEquiv.

theorem Anderson4D.map_mem_validWords_of_fiber_sum {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] [DecidableEq ι] [DecidableEq κ] {M : ℕ} (fineMult : ι → ℕ) (coarseMult : κ → ℕ) (g : ι → κ) (w : Fin M → ι) (hw : w ∈ validWords fineMult) (hmass : ∀ (b : κ), ∑ a : { i : ι // g i = b }, fineMult ↑a = coarseMult b) : (fun (j : Fin M) => g (w j)) ∈ validWords coarseMult

Mapping a valid fine word through g gives a valid coarse word whenever the coarse multiplicity is the sum of the fine multiplicities in each fiber.

The actual arrangement-induced class words

@[reducible, inline]

abbrev Anderson4D.HeppArrangement {t : PlaneTree} (mu : t.Multiplicities) : Type

The labeled-copy arrangements appearing in the statement-boundary factorial ledger.

Equations

• Anderson4D.HeppArrangement mu = (Fin (Anderson4D.totalMultiplicity mu) ≃ (l : Anderson4D.HeppLeaf t) × Fin (Anderson4D.leafMultiplicity mu l))

def Anderson4D.leafActiveNX {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (l : HeppLeaf t) : ActiveNXClass Nm mu

Send a leaf to its active (N,X) class.

Equations

• Anderson4D.leafActiveNX Nm mu l = ⟨Anderson4D.singleScaleSigma1 Nm mu l, ⋯⟩

def Anderson4D.arrangementNXWord {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (σ : HeppArrangement mu) : Fin (totalMultiplicity mu) → ActiveNXClass Nm mu

The (N,X) class word induced by an actual labeled arrangement.

Equations

• Anderson4D.arrangementNXWord Nm mu σ j = Anderson4D.leafActiveNX Nm mu (Anderson4D.inducedWord (Anderson4D.leafMultiplicity mu) σ j)

def Anderson4D.arrangementPWord {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (σ : HeppArrangement mu) : Fin (totalMultiplicity mu) → ActivePClass Nm mu

The coarse P word induced by the same labeled arrangement.

Equations

• Anderson4D.arrangementPWord Nm mu σ j = Anderson4D.activeNXToP Nm mu (Anderson4D.arrangementNXWord Nm mu σ j)

def Anderson4D.leafActiveNXFiberEquiv {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (a : ActiveNXClass Nm mu) : { l : HeppLeaf t // leafActiveNX Nm mu l = a } ≃ ↥(leavesAtNX Nm mu ↑a)

A fiber of leafActiveNX is exactly the corresponding leavesAtNX finset, expressed as an equivalence of subtypes.

Equations

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

theorem Anderson4D.sum_leafMultiplicity_leafActiveNX_fiber {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (a : ActiveNXClass Nm mu) : ∑ l : { l : HeppLeaf t // leafActiveNX Nm mu l = a }, leafMultiplicity mu ↑l = activeNXMultiplicity Nm mu a

The leaf multiplicities above an active (N,X) letter sum to the paper mass m_{N,X}.

theorem Anderson4D.arrangementNXWord_mem_validWords {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (σ : HeppArrangement mu) : arrangementNXWord Nm mu σ ∈ validWords (activeNXMultiplicity Nm mu)

Every actual copy permutation induces a valid (N,X) class word.

theorem Anderson4D.arrangementPWord_mem_validWords {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (σ : HeppArrangement mu) : arrangementPWord Nm mu σ ∈ validWords (activePMultiplicity Nm mu)

The coarse P word of every arrangement has the exact m_P multiplicities.

theorem Anderson4D.arrangementNXWord_mem_validRefinements {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (σ : HeppArrangement mu) : arrangementNXWord Nm mu σ ∈ validRefinements (activeNXMultiplicity Nm mu) (activeNXToP Nm mu) (arrangementPWord Nm mu σ)

The actual (N,X) word belongs to the exact refinement fiber above its actual P word.

theorem Anderson4D.paper579_arrangement_classWord_count {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (σ : HeppArrangement mu) : (validRefinements (activeNXMultiplicity Nm mu) (activeNXToP Nm mu) (arrangementPWord Nm mu σ)).card = ∏ P ∈ pCarrier Nm mu, Nat.multinomial (nxAtP Nm mu P) (multiplicityNX Nm mu)

Arrangement-facing specialization of the conditional class-word count (5.79). Its left side is the refinement fiber containing the class word induced by the given copy permutation; it is not the number of labeled arrangements having that P word, which additionally carries the internal factorial ledger.