Fixed-fiber assembly

This file combines the canonical pointwise kernel schedule with the finite Fubini/CPS bridge. It then bounds the exposed anchor-copy sum and records the resulting phase-independent prefactor before complementary-phase interpolation.

theorem Anderson4D.XYCluster.sum_arrangementsAtNXWord_edgeKernel_le_conditionedRuns {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) : have runs := finAnchorNXCoarseRunsWithPhases Nm mu leftPhase rightPhase anchor x O; ∑ σ ∈ arrangementsAtNXWord Nm mu x, ∏ edge : AdjacentIndex (totalMultiplicity mu), finAnchorNXArrangementEdgeKernel ht hroot Nm mu z hz R O leftPhase rightPhase anchor x (⇑σ) edge ≤ ∑ b ∈ conditionedCopiesAtNX Nm mu ∅ ↑(x anchor), conditionedNXAnchoredRunsSum ht hroot Nm mu z hz R runs.left runs.right {b} (labeledCopyPoint z b)

The canonical pointwise kernel comparison sums exactly through the finite-Fubini/CPS bridge. No factorial or independent right-run choice is introduced.

One-phase fixed-fiber bound

noncomputable def Anderson4D.XYCluster.finAnchorNXFiberCommonPrefactor {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (C : ℝ) (R : ℕ) (anchor : Fin (totalMultiplicity mu)) (x : Fin (totalMultiplicity mu) → ActiveNXClass Nm mu) (O : Finset (AdjacentIndex (totalMultiplicity mu))) : ℝ

A phase-independent reference for the common scalar ledger. Choosing the unshifted schedule is only a normalization: the exact occurrence/scale/skip factorization shows that every phase choice has the same value.

Equations

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

theorem Anderson4D.XYCluster.locatedLedgerCommonProduct_finAnchor_eq_reference {t : PlaneTree} {m : ℕ} (Nm : t.HeppMarking) (mu : t.Multiplicities) (leftPhase rightPhase : Bool) (anchor : Fin m) (x : Fin m → ActiveNXClass Nm mu) (O : Finset (AdjacentIndex m)) : locatedLedgerCommonProduct Nm mu (finAnchorNXLocatedCoarseLedgerWithPhases Nm mu leftPhase rightPhase anchor x O) = locatedLedgerCommonProduct Nm mu (finAnchorNXLocatedCoarseLedgerWithPhases Nm mu false false anchor x O)

The common scalar ledger is independent of both pairing phases.

theorem Anderson4D.XYCluster.finAnchorNXFiberCommonPrefactor_nonneg {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (C : ℝ) (hC : 0 ≤ C) (R : ℕ) (hR : 0 < R) (anchor : Fin (totalMultiplicity mu)) (x : Fin (totalMultiplicity mu) → ActiveNXClass Nm mu) (O : Finset (AdjacentIndex (totalMultiplicity mu))) : 0 ≤ finAnchorNXFiberCommonPrefactor Nm mu C R anchor x O

The named common prefactor is nonnegative at a positive cutoff.

theorem Anderson4D.XYCluster.fixedFiber_onePhase_edgeKernel_le_commonPrefactor : ∃ (C : ℝ), 256 ≤ C ∧ ∀ {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 : ℕ), 0 < R → accumulatedScale Nm mu t.rootV ≤ R → ∀ (O : Finset (AdjacentIndex (totalMultiplicity mu))) (leftPhase rightPhase : Bool) (anchor : Fin (totalMultiplicity mu)) (x : Fin (totalMultiplicity mu) → ActiveNXClass Nm mu), ∑ σ ∈ arrangementsAtNXWord Nm mu x, ∏ edge : AdjacentIndex (totalMultiplicity mu), finAnchorNXArrangementEdgeKernel ht hroot Nm mu z hz (↑R) O leftPhase rightPhase anchor x (⇑σ) edge ≤ finAnchorNXFiberCommonPrefactor Nm mu C R anchor x O * ∏ edge ∈ finAnchorPositionPhaseCarrierWithPhases leftPhase rightPhase anchor \ finAnchorNXExceptionalEdgesWithPhases Nm mu leftPhase rightPhase anchor x O, finAnchorOrientedDyadicEdgeGain Nm mu anchor x edge

One fixed (N,X) word fiber, one anchor, and one phase choice are bounded by a phase-independent common prefactor times the retained oriented gain. The anchor-copy cardinal and the number of elimination blocks have both been absorbed into the single exponential constant.

Complementary-phase interpolation

noncomputable def Anderson4D.XYCluster.finAnchorNXInterpolatedFiberGain {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (leftPhase rightPhase : Bool) (m : ℕ) : Fin m → (Fin m → ActiveNXClass Nm mu) → Finset (AdjacentIndex m) → ℝ

Successor-free packaging of the interpolated 1/16 gain. At positive length it is exactly the active-P ratio product on the m - 1 original adjacencies; the zero branch is uninhabited because it requires an anchor.

Equations

• One or more equations did not get rendered due to their size.
• Anderson4D.XYCluster.finAnchorNXInterpolatedFiberGain Nm mu leftPhase rightPhase 0 anchor _cls _O = anchor.elim0

noncomputable def Anderson4D.XYCluster.finAnchorNXFiberChainCommonPrefactor {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (C : ℝ) (R : ℕ) (anchor : Fin (totalMultiplicity mu)) (x : Fin (totalMultiplicity mu) → ActiveNXClass Nm mu) (O : Finset (AdjacentIndex (totalMultiplicity mu))) : ℝ

The common prefactor for the frozen chain-weight fiber includes the statement-to-edge-kernel scale factor. It is still independent of both pairing phases.

Equations

• Anderson4D.XYCluster.finAnchorNXFiberChainCommonPrefactor Nm mu C R anchor x O = ↑R ^ (2 * O.card) * Anderson4D.XYCluster.finAnchorNXFiberCommonPrefactor Nm mu C R anchor x O

theorem Anderson4D.XYCluster.finAnchorNXFiberChainCommonPrefactor_nonneg {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (C : ℝ) (hC : 0 ≤ C) (R : ℕ) (hR : 0 < R) (anchor : Fin (totalMultiplicity mu)) (x : Fin (totalMultiplicity mu) → ActiveNXClass Nm mu) (O : Finset (AdjacentIndex (totalMultiplicity mu))) : 0 ≤ finAnchorNXFiberChainCommonPrefactor Nm mu C R anchor x O

The scaled common prefactor is nonnegative.

theorem Anderson4D.XYCluster.fixedFiber_twoPhase_singleScaleChainWeight_le_sixteenth : ∃ (C : ℝ), 256 ≤ C ∧ ∀ {t : PlaneTree}, t.isValid = true → t.rootV ∈ t.BranchNodes → ∀ (Nm : t.HeppMarking) (mu : t.Multiplicities) (z : HeppLeaf t → Fin 4 → ℤ), IsSeparatedEmbedding Nm z → ∀ (R : ℕ), 0 < R → accumulatedScale Nm mu t.rootV ≤ R → ∀ (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) σ) ≤ finAnchorNXFiberChainCommonPrefactor Nm mu C R anchor x O * finAnchorNXInterpolatedFiberGain Nm mu leftPhase rightPhase (totalMultiplicity mu) anchor x O

Complementary phase choices give the fixed-fiber 1/16 estimate for the frozen chain weight. The same universal constant and the same common prefactor are used in both one-phase bounds before interpolation.