One-phase assembly for the single-scale estimate

This file combines the two outward target products into the single located ledger and then applies the scalar-loss, rough-scale, and precise-gain ledgers in their safe inequality directions. It also identifies the oriented dyadic gain with the original-edge active-P gain used by the outer sequence estimate.

theorem Anderson4D.XYCluster.locatedLedgerCommonProduct_nonneg {t : PlaneTree} {m : ℕ} (Nm : t.HeppMarking) (mu : t.Multiplicities) (bs : List (LocatedNXParityBlock Nm mu)) : 0 ≤ locatedLedgerCommonProduct Nm mu bs

theorem Anderson4D.XYCluster.locatedLedgerLossAtoms_prod_nonneg {t : PlaneTree} {m : ℕ} (Nm : t.HeppMarking) (mu : t.Multiplicities) (bs : List (LocatedNXParityBlock Nm mu)) : 0 ≤ (locatedLedgerLossAtoms Nm mu bs).prod

theorem Anderson4D.XYCluster.locatedLedgerRoughScaleProduct_nonneg {t : PlaneTree} {m : ℕ} {Nm : t.HeppMarking} {mu : t.Multiplicities} (R : ℝ) (bs : List (LocatedNXParityBlock Nm mu)) : 0 ≤ locatedLedgerRoughScaleProduct R bs

theorem Anderson4D.XYCluster.locatedLedgerPreciseGainProduct_nonneg {t : PlaneTree} {m : ℕ} (Nm : t.HeppMarking) (mu : t.Multiplicities) (bs : List (LocatedNXParityBlock Nm mu)) : 0 ≤ locatedLedgerPreciseGainProduct Nm mu bs

theorem Anderson4D.XYCluster.finAnchorOrientedDyadicEdgeGain_nonneg {t : PlaneTree} {m : ℕ} (Nm : t.HeppMarking) (mu : t.Multiplicities) (anchor : Fin m) (cls : Fin m → ActiveNXClass Nm mu) (edge : AdjacentIndex m) : 0 ≤ finAnchorOrientedDyadicEdgeGain Nm mu anchor cls edge

theorem Anderson4D.XYCluster.finAnchorNXCoarseRuns_targetProducts_eq_ledger {t : PlaneTree} {m : ℕ} (Nm : t.HeppMarking) (mu : t.Multiplicities) (R : ℝ) (leftPhase rightPhase : Bool) (anchor : Fin m) (cls : Fin m → ActiveNXClass Nm mu) (O : Finset (AdjacentIndex m)) : (List.map (fun (p : NXParityBlock Nm mu) => nxParityBlockTarget Nm mu R p) (finAnchorNXCoarseRunsWithPhases Nm mu leftPhase rightPhase anchor cls O).left).prod * (List.map (fun (p : NXParityBlock Nm mu) => nxParityBlockTarget Nm mu R p) (finAnchorNXCoarseRunsWithPhases Nm mu leftPhase rightPhase anchor cls O).right).prod = (List.map (fun (p : NXParityBlock Nm mu) => nxParityBlockTarget Nm mu R p) (finAnchorNXCoarseLedgerWithPhases Nm mu leftPhase rightPhase anchor cls O)).prod

The two analytic runs remain separate as chains, but their target products may be concatenated algebraically into the located ledger.

theorem Anderson4D.XYCluster.length_positionBlocks_le_flatten_entries {α : Type u_1} (bs : List (PositionBlock α)) : bs.length ≤ (List.flatMap PositionBlock.entries bs).length

Every position block contains at least one position.

theorem Anderson4D.XYCluster.length_finAnchorNXCoarseLedgerWithPhases_le {t : PlaneTree} {m : ℕ} (Nm : t.HeppMarking) (mu : t.Multiplicities) (leftPhase rightPhase : Bool) (anchor : Fin m) (cls : Fin m → ActiveNXClass Nm mu) (O : Finset (AdjacentIndex m)) : (finAnchorNXCoarseLedgerWithPhases Nm mu leftPhase rightPhase anchor cls O).length ≤ m

There is at most one analytic block per paper position.

theorem Anderson4D.XYCluster.finAnchorNXCoarseRuns_constantPower_le {t : PlaneTree} {m : ℕ} (Nm : t.HeppMarking) (mu : t.Multiplicities) (C : ℝ) (hC : 1 ≤ C) (leftPhase rightPhase : Bool) (anchor : Fin m) (cls : Fin m → ActiveNXClass Nm mu) (O : Finset (AdjacentIndex m)) : C ^ ((finAnchorNXCoarseRunsWithPhases Nm mu leftPhase rightPhase anchor cls O).left.length + (finAnchorNXCoarseRunsWithPhases Nm mu leftPhase rightPhase anchor cls O).right.length) ≤ C ^ m

The power of the universal local constant costs at most one factor per paper position.

theorem Anderson4D.XYCluster.finAnchorNXCoarse_targetProduct_le_onePhaseLedger {t : PlaneTree} {n : ℕ} (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (Nm : t.HeppMarking) (mu : t.Multiplicities) (R : ℕ) (hRpos : 0 < R) (hR : accumulatedScale Nm mu t.rootV ≤ R) (leftPhase rightPhase : Bool) (anchor : Fin (n + 1)) (cls : Fin (n + 1) → ActiveNXClass Nm mu) (O : Finset (AdjacentIndex (n + 1))) : (List.map (fun (p : NXParityBlock Nm mu) => nxParityBlockTarget Nm mu (↑R) p) (finAnchorNXCoarseLedgerWithPhases Nm mu leftPhase rightPhase anchor cls O)).prod ≤ locatedLedgerCommonProduct Nm mu (finAnchorNXLocatedCoarseLedgerWithPhases Nm mu leftPhase rightPhase anchor cls O) * ↑positionLossBase ^ totalMultiplicity mu * (↑(scaleN Nm t.rootV) / ↑R) ^ min (2 * O.card) 3 * ∏ edge ∈ finAnchorPositionPhaseCarrierWithPhases leftPhase rightPhase anchor \ finAnchorNXExceptionalEdgesWithPhases Nm mu leftPhase rightPhase anchor cls O, finAnchorOrientedDyadicEdgeGain Nm mu anchor cls edge

One-phase target-ledger bound. All three lossy replacements are applied with explicit nonnegativity; the retained gain is the carrier-minus- exception product in original-edge orientation.

Original-edge reindexing and scaled phase interpolation

theorem Anderson4D.XYCluster.finAnchorOrientedDyadicEdgeGain_eq_activeP {t : PlaneTree} {n : ℕ} (Nm : t.HeppMarking) (mu : t.Multiplicities) (anchor : Fin (n + 1)) (cls : Fin (n + 1) → ActiveNXClass Nm mu) (edge : AdjacentIndex (n + 1)) : finAnchorOrientedDyadicEdgeGain Nm mu anchor cls edge = anchoredOrientedActivePEdgeGain (1 / 8) anchor (fun (i : Fin (n + 1)) => activeNXToP Nm mu (cls i)) ((adjacentIndexSuccEquiv n) edge)

The precise ledger's outward dyadic gain is definitionally the active-P original-edge gain after the canonical adjacency reindexing.

theorem Anderson4D.XYCluster.prod_finAnchorOrientedDyadicEdgeGain_eq_activeP {t : PlaneTree} {n : ℕ} (Nm : t.HeppMarking) (mu : t.Multiplicities) (anchor : Fin (n + 1)) (cls : Fin (n + 1) → ActiveNXClass Nm mu) (edges : Finset (AdjacentIndex (n + 1))) : ∏ edge ∈ edges, finAnchorOrientedDyadicEdgeGain Nm mu anchor cls edge = ∏ j ∈ reindexAdjacentExceptions edges, anchoredOrientedActivePEdgeGain (1 / 8) anchor (fun (i : Fin (n + 1)) => activeNXToP Nm mu (cls i)) j

Product form of the same reindexing on an arbitrary edge carrier.

theorem Anderson4D.XYCluster.finAnchor_phaseOrientedDyadicProduct_eq_activeP {t : PlaneTree} {n : ℕ} (Nm : t.HeppMarking) (mu : t.Multiplicities) (leftPhase rightPhase : Bool) (anchor : Fin (n + 1)) (cls : Fin (n + 1) → ActiveNXClass Nm mu) (O : Finset (AdjacentIndex (n + 1))) : ∏ edge ∈ finAnchorPositionPhaseCarrierWithPhases leftPhase rightPhase anchor \ finAnchorNXExceptionalEdgesWithPhases Nm mu leftPhase rightPhase anchor cls O, finAnchorOrientedDyadicEdgeGain Nm mu anchor cls edge = ∏ j ∈ finAnchorPositionPhaseFinCarrierWithPhases leftPhase rightPhase anchor \ finAnchorNXExceptionalFinEdgesWithPhases Nm mu leftPhase rightPhase anchor cls O, anchoredOrientedActivePEdgeGain (1 / 8) anchor (fun (i : Fin (n + 1)) => activeNXToP Nm mu (cls i)) j

The retained one-phase product in original adjacency coordinates is exactly the retained active-P product in Fin n coordinates.

theorem Anderson4D.XYCluster.le_mul_geometricMean_of_le_both {x A a b g : ℝ} (hx : 0 ≤ x) (hA : 0 ≤ A) (ha : 0 ≤ a) (hb : 0 ≤ b) (hxa : x ≤ A * a) (hxb : x ≤ A * b) (hg : √(a * b) = g) : x ≤ A * g

Geometric-mean interpolation remains valid with a common nonnegative prefactor. This is the form required at a fixed arrangement fiber.

theorem Anderson4D.XYCluster.finAnchorNX_two_phase_scaled_gain_bounds_le_sixteenth {t : PlaneTree} {n : ℕ} (Nm : t.HeppMarking) (mu : t.Multiplicities) (leftPhase rightPhase : Bool) (anchor : Fin (n + 1)) (cls : Fin (n + 1) → ActiveNXClass Nm mu) (O : Finset (AdjacentIndex (n + 1))) (ratio : Fin n → ℝ) (hratio : ∀ (j : Fin n), 0 ≤ ratio j) (A x : ℝ) (hA : 0 ≤ A) (hx : 0 ≤ x) (hphase : x ≤ A * ∏ j ∈ finAnchorPositionPhaseFinCarrierWithPhases leftPhase rightPhase anchor \ finAnchorNXExceptionalFinEdgesWithPhases Nm mu leftPhase rightPhase anchor cls O, ratioGain (1 / 8) (ratio j)) (hflip : x ≤ A * ∏ j ∈ finAnchorPositionPhaseFinCarrierWithPhases (!leftPhase) (!rightPhase) anchor \ finAnchorNXExceptionalFinEdgesWithPhases Nm mu (!leftPhase) (!rightPhase) anchor cls O, ratioGain (1 / 8) (ratio j)) : x ≤ A * ∏ j ∈ Finset.univ \ finAnchorNXInterpolatedExceptionalFinEdges Nm mu leftPhase rightPhase anchor cls O, ratioGain (1 / 16) (ratio j)

Concrete complementary-phase interpolation with a common prefactor. The exception union and exponent 1/16 are exactly those of the position ledger.