Exact finite Fubini decomposition for the single-scale proof

This file groups the labeled arrangements from the factorial ledger first by their active P word and then by the refining active (N,X) word. It is the finite statement-boundary decomposition used before applying the outer class-word count and the conditioned inner estimates.

def Anderson4D.arrangementsAtNXWord {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (x : Fin (totalMultiplicity mu) → ActiveNXClass Nm mu) : Finset (HeppArrangement mu)

Arrangements inducing a prescribed active (N,X) word.

Equations

• Anderson4D.arrangementsAtNXWord Nm mu x = {σ : Anderson4D.HeppArrangement mu | Anderson4D.arrangementNXWord Nm mu σ = x}

theorem Anderson4D.sum_arrangements_eq_sum_NXWords {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (F : HeppArrangement mu → ℝ) : ∑ σ : HeppArrangement mu, F σ = ∑ x ∈ validWords (activeNXMultiplicity Nm mu), ∑ σ ∈ arrangementsAtNXWord Nm mu x, F σ

Exact grouping of all labeled arrangements by their (N,X) word.

def Anderson4D.nxWordToPWord {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (x : Fin (totalMultiplicity mu) → ActiveNXClass Nm mu) : Fin (totalMultiplicity mu) → ActivePClass Nm mu

The coarse word obtained from an abstract active (N,X) word.

Equations

• Anderson4D.nxWordToPWord Nm mu x j = Anderson4D.activeNXToP Nm mu (x j)

theorem Anderson4D.nxWordToPWord_mem_validWords {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) {x : Fin (totalMultiplicity mu) → ActiveNXClass Nm mu} (hx : x ∈ validWords (activeNXMultiplicity Nm mu)) : nxWordToPWord Nm mu x ∈ validWords (activePMultiplicity Nm mu)

theorem Anderson4D.nxWordToPWord_eq_arrangementPWord {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (σ : HeppArrangement mu) : nxWordToPWord Nm mu (arrangementNXWord Nm mu σ) = arrangementPWord Nm mu σ

theorem Anderson4D.validNXWords_fiber_eq_validRefinements {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (y : Fin (totalMultiplicity mu) → ActivePClass Nm mu) : {x ∈ validWords (activeNXMultiplicity Nm mu) | nxWordToPWord Nm mu x = y} = validRefinements (activeNXMultiplicity Nm mu) (activeNXToP Nm mu) y

The fiber of nxWordToPWord inside valid (N,X) words is exactly the project's validRefinements carrier.

theorem Anderson4D.sum_validNXWords_eq_sum_PWords_refinements {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (G : (Fin (totalMultiplicity mu) → ActiveNXClass Nm mu) → ℝ) : ∑ x ∈ validWords (activeNXMultiplicity Nm mu), G x = ∑ y ∈ validWords (activePMultiplicity Nm mu), ∑ x ∈ validRefinements (activeNXMultiplicity Nm mu) (activeNXToP Nm mu) y, G x

Exact two-level grouping of an arbitrary statistic on valid (N,X) words: first fix the P word, then sum over its valid refinements.

theorem Anderson4D.sum_arrangements_eq_sum_PWords_NXWords {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (F : HeppArrangement mu → ℝ) : ∑ σ : HeppArrangement mu, F σ = ∑ y ∈ validWords (activePMultiplicity Nm mu), ∑ x ∈ validRefinements (activeNXMultiplicity Nm mu) (activeNXToP Nm mu) y, ∑ σ ∈ arrangementsAtNXWord Nm mu x, F σ

The complete finite Fubini decomposition of the labeled-arrangement sum. No positivity or analytic estimate is used: this is an exact identity.

theorem Anderson4D.paperSum_eq_sum_PWords_NXWords_arrangements {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (F : (Fin (totalMultiplicity mu) → HeppLeaf t) → ℝ) : paperSum (leafMultiplicity mu) F = ∑ y ∈ validWords (activePMultiplicity Nm mu), ∑ x ∈ validRefinements (activeNXMultiplicity Nm mu) (activeNXToP Nm mu) y, ∑ σ ∈ arrangementsAtNXWord Nm mu x, F (inducedWord (leafMultiplicity mu) σ)

Paper-sum statement-boundary form of the same decomposition. The analytic summand remains a function of the induced leaf word, exactly as in SingleScaleEstimate.