Statement summands on a fixed (N,X) fiber

This file connects the frozen single-scale summand to the canonical anchor/phase edge kernel. It is deliberately upstream of the analytic finite-Fubini estimate: the only input here is the pointwise statement-kernel comparison.

theorem Anderson4D.XYCluster.finAnchorNXArrangementEdgeKernel_nonneg {t : PlaneTree} {m : ℕ} (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 : ℝ) (O : Finset (AdjacentIndex m)) (leftPhase rightPhase : Bool) (anchor : Fin m) (x : Fin m → ActiveNXClass Nm mu) (σ : Fin m → HeppLabeledCopy mu) (edge : AdjacentIndex m) : 0 ≤ finAnchorNXArrangementEdgeKernel ht hroot Nm mu z hz R O leftPhase rightPhase anchor x σ edge

Every canonical anchor/phase edge kernel is nonnegative.

theorem Anderson4D.XYCluster.finAnchorNXArrangementEdgeKernelProduct_nonneg {t : PlaneTree} {m : ℕ} (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 : ℝ) (O : Finset (AdjacentIndex m)) (leftPhase rightPhase : Bool) (anchor : Fin m) (x : Fin m → ActiveNXClass Nm mu) (σ : Fin m → HeppLabeledCopy mu) : 0 ≤ ∏ edge : AdjacentIndex m, finAnchorNXArrangementEdgeKernel ht hroot Nm mu z hz R O leftPhase rightPhase anchor x σ edge

The product used by either canonical phase choice is nonnegative.

theorem Anderson4D.XYCluster.sum_arrangementsAtNXWord_finAnchorNXEdgeKernel_nonneg {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 : ℝ) (O : Finset (AdjacentIndex (totalMultiplicity mu))) (leftPhase rightPhase : Bool) (anchor : Fin (totalMultiplicity mu)) (x : Fin (totalMultiplicity mu) → ActiveNXClass Nm mu) : 0 ≤ ∑ σ ∈ arrangementsAtNXWord Nm mu x, ∏ edge : AdjacentIndex (totalMultiplicity mu), finAnchorNXArrangementEdgeKernel ht hroot Nm mu z hz R O leftPhase rightPhase anchor x (⇑σ) edge

The whole canonical edge-kernel fiber sum is nonnegative.

theorem Anderson4D.XYCluster.singleScaleChainWeight_induced_le_finAnchorNXEdgeKernelProduct {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 : R ≠ 0) (O : Finset (AdjacentIndex (totalMultiplicity mu))) (leftPhase rightPhase : Bool) (anchor : Fin (totalMultiplicity mu)) (x : Fin (totalMultiplicity mu) → ActiveNXClass Nm mu) (σ : HeppArrangement mu) (hσ : σ ∈ arrangementsAtNXWord Nm mu x) : singleScaleChainWeight z O (inducedWord (leafMultiplicity mu) σ) ≤ R ^ (2 * O.card) * ∏ edge : AdjacentIndex (totalMultiplicity mu), finAnchorNXArrangementEdgeKernel ht hroot Nm mu z hz R O leftPhase rightPhase anchor x (⇑σ) edge

Pointwise frozen-summand comparison for two independently selectable canonical phases.

theorem Anderson4D.XYCluster.sum_arrangementsAtNXWord_singleScaleChainWeight_le_edgeKernelWithPhases {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 : R ≠ 0) (O : Finset (AdjacentIndex (totalMultiplicity mu))) (leftPhase rightPhase : Bool) (anchor : Fin (totalMultiplicity mu)) (x : Fin (totalMultiplicity mu) → ActiveNXClass Nm mu) : ∑ σ ∈ arrangementsAtNXWord Nm mu x, singleScaleChainWeight z O (inducedWord (leafMultiplicity mu) σ) ≤ R ^ (2 * O.card) * ∑ σ ∈ arrangementsAtNXWord Nm mu x, ∏ edge : AdjacentIndex (totalMultiplicity mu), finAnchorNXArrangementEdgeKernel ht hroot Nm mu z hz R O leftPhase rightPhase anchor x (⇑σ) edge

Fixed (N,X)-word fiber bridge, generalized to independent phases on the left and right runs. No validity hypothesis on x is needed for this stronger local statement.

theorem Anderson4D.XYCluster.sum_arrangementsAtNXWord_singleScaleChainWeight_le_edgeKernel {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))) (phase : Bool) (anchor : Fin (totalMultiplicity mu)) (x : Fin (totalMultiplicity mu) → ActiveNXClass Nm mu) (_hx : x ∈ validWords (activeNXMultiplicity Nm mu)) : ∑ σ ∈ arrangementsAtNXWord Nm mu x, singleScaleChainWeight z O (inducedWord (leafMultiplicity mu) σ) ≤ ↑R ^ (2 * O.card) * ∑ σ ∈ arrangementsAtNXWord Nm mu x, ∏ edge : AdjacentIndex (totalMultiplicity mu), finAnchorNXArrangementEdgeKernel ht hroot Nm mu z hz (↑R) O phase phase anchor x (⇑σ) edge

Frozen-data specialization: the scale is a positive natural number, the class word is valid, and both outward runs use the same phase.