Sharp postprocessing of a fixed (N,X) fiber

The fixed-fiber estimate stops after the occurrence bound. It retains the full word base-scale factor and the square of the anchor scale. The outer leaf payoff is not inserted here.

A separate scalar lemma below consumes one explicit copy of the global outer payoff and only then applies anchor completion and reverse-power conversion to the paper-facing simple/compound and branch ledgers.

noncomputable def Anderson4D.XYCluster.finAnchorNXFiberSharpBase (C : ℝ) : ℝ

Uniform base accumulated before the reverse-power step.

Equations

• Anderson4D.XYCluster.finAnchorNXFiberSharpBase C = C * ↑Anderson4D.XYCluster.positionLossBase * (2 * Real.exp 1)

theorem Anderson4D.XYCluster.finAnchorNXFiberSharpBase_nonneg (C : ℝ) (hC : 0 ≤ C) : 0 ≤ finAnchorNXFiberSharpBase C

theorem Anderson4D.XYCluster.finAnchorNXFiberChainCommonPrefactor_le_sharpOccurrence {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (C : ℝ) (hC : 0 ≤ C) (R s : ℕ) (hR : 0 < R) (O : Finset (AdjacentIndex (totalMultiplicity mu))) (hs : O.card = s) (anchor : Fin (totalMultiplicity mu)) (x : Fin (totalMultiplicity mu) → ActiveNXClass Nm mu) (hx : x ∈ validWords (activeNXMultiplicity Nm mu)) : finAnchorNXFiberChainCommonPrefactor Nm mu C R anchor x O ≤ (finAnchorNXFiberSharpBase C ^ totalMultiplicity mu * sqrtFactorial (totalMultiplicity mu - s) * ∏ l : HeppLeaf t, sqrtFactorial (leafMultiplicity mu l)) * nxWordBaseScaleFactor x * ↑(↑(x anchor)).1 ^ 2 * ↑R ^ (2 * s) * (↑(scaleN Nm t.rootV) / ↑R) ^ min (2 * s) 3

Sharp coefficient bound for one valid fixed fiber. Notice that nxWordBaseScaleFactor x, the anchor-scale square, and the leaf square-root factorial product are all still present.

theorem Anderson4D.XYCluster.finAnchorNXInterpolatedFiberGain_eq_orientedActivePWeight {t : PlaneTree} {n : ℕ} (Nm : t.HeppMarking) (mu : t.Multiplicities) (leftPhase rightPhase : Bool) (anchor : Fin (n + 1)) (x : Fin (n + 1) → ActiveNXClass Nm mu) (O : Finset (AdjacentIndex (n + 1))) : finAnchorNXInterpolatedFiberGain Nm mu leftPhase rightPhase (n + 1) anchor x O = anchoredOrientedActivePWeight (1 / 16) (finAnchorPositionalInterpolatedExceptionalFinEdges leftPhase rightPhase anchor O) anchor fun (i : Fin (n + 1)) => activeNXToP Nm mu (x i)

At successor length, the successor-free interpolated gain is exactly the oriented active-P weight.

noncomputable def Anderson4D.XYCluster.finAnchorNXOrientedActivePWeight {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 oriented active-P weight. Its zero branch is uninhabited for the same reason as the interpolated fiber gain.

Equations

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

theorem Anderson4D.XYCluster.finAnchorNXInterpolatedFiberGain_eq_orientedActivePWeight_of_pos {t : PlaneTree} {m : ℕ} (Nm : t.HeppMarking) (mu : t.Multiplicities) (hm : 0 < m) (leftPhase rightPhase : Bool) (anchor : Fin m) (x : Fin m → ActiveNXClass Nm mu) (O : Finset (AdjacentIndex m)) : finAnchorNXInterpolatedFiberGain Nm mu leftPhase rightPhase m anchor x O = finAnchorNXOrientedActivePWeight Nm mu leftPhase rightPhase m anchor x O

At every positive length the successor-free interpolated gain and the successor-free oriented active-P weight coincide. The proof exposes the successor presentation only locally.

theorem Anderson4D.XYCluster.finAnchorNXInterpolatedFiberGain_eq_orientedActivePWeight_total {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (leftPhase rightPhase : Bool) (anchor : Fin (totalMultiplicity mu)) (x : Fin (totalMultiplicity mu) → ActiveNXClass Nm mu) (O : Finset (AdjacentIndex (totalMultiplicity mu))) : finAnchorNXInterpolatedFiberGain Nm mu leftPhase rightPhase (totalMultiplicity mu) anchor x O = finAnchorNXOrientedActivePWeight Nm mu leftPhase rightPhase (totalMultiplicity mu) anchor x O

Total-multiplicity-domain wrapper. The dependent paper carriers are generalized together before the zero/successor split.

theorem Anderson4D.XYCluster.finAnchorNXOrientedActivePWeight_nonneg {t : PlaneTree} {m : ℕ} (Nm : t.HeppMarking) (mu : t.Multiplicities) (hm : 0 < m) (leftPhase rightPhase : Bool) (anchor : Fin m) (x : Fin m → ActiveNXClass Nm mu) (O : Finset (AdjacentIndex m)) : 0 ≤ finAnchorNXOrientedActivePWeight Nm mu leftPhase rightPhase m anchor x O

The successor-free oriented active-P weight is nonnegative.

theorem Anderson4D.XYCluster.fixedFiber_singleScaleChainWeight_le_sharpOccurrence : ∃ (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 → ∀ (s : ℕ) (O : Finset (AdjacentIndex (totalMultiplicity mu))), O.card = s → ∀ x ∈ validWords (activeNXMultiplicity Nm mu), have anchor := totalMultiplicityNXScaleAnchor Nm mu x; ∑ σ ∈ arrangementsAtNXWord Nm mu x, singleScaleChainWeight z O (inducedWord (leafMultiplicity mu) σ) ≤ (finAnchorNXFiberSharpBase C ^ totalMultiplicity mu * sqrtFactorial (totalMultiplicity mu - s) * ∏ l : HeppLeaf t, sqrtFactorial (leafMultiplicity mu l)) * nxWordBaseScaleFactor x * ↑(↑(x anchor)).1 ^ 2 * ↑R ^ (2 * s) * (↑(scaleN Nm t.rootV) / ↑R) ^ min (2 * s) 3 * finAnchorNXOrientedActivePWeight Nm mu false false (totalMultiplicity mu) anchor x O

Pre-outer fixed-fiber theorem at the deterministic minimal-scale anchor. It is the sharp stopping point: no outer payoff, compound factorial, or reverse-power estimate has been used.

theorem Anderson4D.XYCluster.completedNXWordScalar_mul_outerPayoff_le_branchRatioLedger {t : PlaneTree} (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) (anchor : Fin (totalMultiplicity mu)) (x : Fin (totalMultiplicity mu) → ActiveNXClass Nm mu) (hx : x ∈ validWords (activeNXMultiplicity Nm mu)) (hscale : SatisfiesSingleScaleCondition Nm mu) : (∏ l : HeppLeaf t, sqrtFactorial (leafMultiplicity mu l)) * nxWordBaseScaleFactor x * ↑(↑(x anchor)).1 ^ 2 * ∏ l : HeppLeaf t, originalOuterLeafPayoff Nm mu compound l ≤ ((∏ l ∈ simpleLeaves t compound, sqrtFactorial (mu.m l)) * ∏ l ∈ compoundLeaves t compound, factorialThreeQuarters (mu.m l)) * (8 * Real.exp 4) ^ (5 * totalMultiplicity mu) * singleScaleBranchPower Nm mu compound * ∏ v ∈ nonrootBranches t, parentScaleRatio Nm v ^ 3

One explicit copy of the global outer payoff completes the retained base coefficient. This lemma is intentionally independent of the fiber bound: the caller must supply that payoff exactly once.

theorem Anderson4D.XYCluster.global_refinement_orientedWeight_total_le_originalPayoff : ∃ (C : ℝ), 1 ≤ C ∧ ∀ {t : PlaneTree}, t.isValid = true → t.rootV ∈ t.BranchNodes → ∀ (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) (chooseAnchor : (Fin (totalMultiplicity mu) → ActiveNXClass Nm mu) → Fin (totalMultiplicity mu)) (O : Finset (AdjacentIndex (totalMultiplicity mu))), ∑ y ∈ validWords (activePMultiplicity Nm mu), ∑ x ∈ validRefinements (activeNXMultiplicity Nm mu) (activeNXToP Nm mu) y, finAnchorNXOrientedActivePWeight Nm mu false false (totalMultiplicity mu) (chooseAnchor x) x O ≤ C ^ totalMultiplicity mu * ∏ l : HeppLeaf t, originalOuterLeafPayoff Nm mu compound l

Total-multiplicity-domain wrapper for the existing global outer estimate. It consumes the outer payoff once and exposes the successor-free oriented weight used by the sharp fixed-fiber theorem.