Statement-boundary reduction to fixed class-word kernel sums #
This file combines the exact finite Fubini decomposition with the
pointwise kernel comparison. It is the first genuinely weighted bridge
from the frozen left side of Proposition 5.10 to the fixed (P,NX) fibers
used by the outer and inner arguments.
theorem
Anderson4D.XYCluster.arrangementNXWord_class_eq
{t : PlaneTree}
(Nm : t.HeppMarking)
(mu : t.Multiplicities)
(x : Fin (totalMultiplicity mu) → ActiveNXClass Nm mu)
(σ : HeppArrangement mu)
(hσ : σ ∈ arrangementsAtNXWord Nm mu x)
(i : Fin (totalMultiplicity mu))
:
theorem
Anderson4D.XYCluster.paperSum_singleScaleChainWeight_le_kernelFubini
{t : PlaneTree}
(ht : t.isValid = true)
(hroot : t.rootV ∈ t.BranchNodes)
(Nm : t.HeppMarking)
(mu : t.Multiplicities)
(z : HeppLeaf t → Fin 4 → ℤ)
(hz : IsSeparatedEmbedding Nm z)
(R : ℕ)
(hR : 0 < R)
(O : Finset (AdjacentIndex (totalMultiplicity mu)))
(strongEdges : (Fin (totalMultiplicity mu) → ActiveNXClass Nm mu) → Finset (AdjacentIndex (totalMultiplicity mu)))
:
paperSum (leafMultiplicity mu) (singleScaleChainWeight z O) ≤ ∑ y ∈ validWords (activePMultiplicity Nm mu),
∑ x ∈ validRefinements (activeNXMultiplicity Nm mu) (activeNXToP Nm mu) y,
∑ σ ∈ arrangementsAtNXWord Nm mu x,
↑R ^ (2 * O.card) * ∏ j : AdjacentIndex (totalMultiplicity mu),
nxClassEdgeKernel ht hroot Nm mu z hz (↑R) O (strongEdges x) x (inducedWord (leafMultiplicity mu) σ) j
For any choice of strong-edge schedule depending on the fixed (N,X)
word, the full paper sum is bounded by the corresponding finite Fubini sum
of kernel products. The skipped-edge factor R^(2|O|) is explicit in
every arrangement summand.