Occurrence-level target ledger for the one-parity estimate

The mixed eliminator produces one target for every scheduled block. This file expands those targets without turning repeated scalar losses into a set: the loss ledger is a List, so every occurrence is retained.

For each located block the target is split into four factors:

• the common local factors of (5.87);
• the scalar losses sqrt Y and Xi⁻¹;
• the explicit rough (N/R)² factors;
• the precise-pair dyadic gain.

The resulting identity is exact. In particular, no gain is attached to a single or rough-pair block, and no scalar loss is attached to a precise pair.

noncomputable def Anderson4D.XYCluster.locatedBlockCommonTarget {t : PlaneTree} {m : ℕ} (Nm : t.HeppMarking) (mu : t.Multiplicities) : LocatedNXParityBlock Nm mu → ℝ

Common (5.87) local factors contributed by one located block.

Equations

• One or more equations did not get rendered due to their size.
• Anderson4D.XYCluster.locatedBlockCommonTarget Nm mu (Anderson4D.XYCluster.LocatedNXParityBlock.single position a skipped) = Anderson4D.XYCluster.paperDyadicLocalTarget Nm mu (↑a) skipped

noncomputable def Anderson4D.XYCluster.locatedBlockLossAtoms {t : PlaneTree} {m : ℕ} (Nm : t.HeppMarking) (mu : t.Multiplicities) : LocatedNXParityBlock Nm mu → List ℝ

Occurrence ledger of scalar losses. A singleton contributes two entries and a rough pair contributes four; a precise pair contributes none.

Equations

• One or more equations did not get rendered due to their size.
• Anderson4D.XYCluster.locatedBlockLossAtoms Nm mu (Anderson4D.XYCluster.LocatedNXParityBlock.pair leftPosition rightPosition p) = []

noncomputable def Anderson4D.XYCluster.locatedBlockRoughScale {t : PlaneTree} {m : ℕ} {Nm : t.HeppMarking} {mu : t.Multiplicities} (R : ℝ) : LocatedNXParityBlock Nm mu → ℝ

Explicit rough scale payoff contributed by one block.

Equations

• One or more equations did not get rendered due to their size.
• Anderson4D.XYCluster.locatedBlockRoughScale R (Anderson4D.XYCluster.LocatedNXParityBlock.single position a skipped) = Anderson4D.XYCluster.paperDyadicRoughScaleGain R (↑a) skipped
• Anderson4D.XYCluster.locatedBlockRoughScale R (Anderson4D.XYCluster.LocatedNXParityBlock.pair leftPosition rightPosition p) = 1

noncomputable def Anderson4D.XYCluster.locatedBlockPreciseGain {t : PlaneTree} {m : ℕ} (Nm : t.HeppMarking) (mu : t.Multiplicities) : LocatedNXParityBlock Nm mu → ℝ

The precise-pair gain; exceptional blocks deliberately contribute 1.

Equations

• One or more equations did not get rendered due to their size.
• Anderson4D.XYCluster.locatedBlockPreciseGain Nm mu (Anderson4D.XYCluster.LocatedNXParityBlock.single position a skipped) = 1
• Anderson4D.XYCluster.locatedBlockPreciseGain Nm mu (Anderson4D.XYCluster.LocatedNXParityBlock.roughPair leftPosition rightPosition p) = 1

theorem Anderson4D.XYCluster.locatedBlockCommonTarget_nonneg {t : PlaneTree} {m : ℕ} (Nm : t.HeppMarking) (mu : t.Multiplicities) (b : LocatedNXParityBlock Nm mu) : 0 ≤ locatedBlockCommonTarget Nm mu b

theorem Anderson4D.XYCluster.locatedBlockRoughScale_nonneg {t : PlaneTree} {m : ℕ} {Nm : t.HeppMarking} {mu : t.Multiplicities} (R : ℝ) (b : LocatedNXParityBlock Nm mu) : 0 ≤ locatedBlockRoughScale R b

theorem Anderson4D.XYCluster.locatedBlockPreciseGain_nonneg {t : PlaneTree} {m : ℕ} (Nm : t.HeppMarking) (mu : t.Multiplicities) (b : LocatedNXParityBlock Nm mu) : 0 ≤ locatedBlockPreciseGain Nm mu b

theorem Anderson4D.XYCluster.nxParityBlockTarget_analyticBlock_eq_ledgers {t : PlaneTree} {m : ℕ} (Nm : t.HeppMarking) (mu : t.Multiplicities) (R : ℝ) (hR : 0 < R) (b : LocatedNXParityBlock Nm mu) : nxParityBlockTarget Nm mu R b.analyticBlock = locatedBlockCommonTarget Nm mu b * (locatedBlockLossAtoms Nm mu b).prod * locatedBlockRoughScale R b * locatedBlockPreciseGain Nm mu b

Exact target split for a single scheduled occurrence.

noncomputable def Anderson4D.XYCluster.locatedLedgerLossAtoms {t : PlaneTree} {m : ℕ} (Nm : t.HeppMarking) (mu : t.Multiplicities) (bs : List (LocatedNXParityBlock Nm mu)) : List ℝ

All scalar-loss occurrences in a located schedule.

Equations

• Anderson4D.XYCluster.locatedLedgerLossAtoms Nm mu bs = List.flatMap (Anderson4D.XYCluster.locatedBlockLossAtoms Nm mu) bs

noncomputable def Anderson4D.XYCluster.locatedLedgerCommonProduct {t : PlaneTree} {m : ℕ} (Nm : t.HeppMarking) (mu : t.Multiplicities) (bs : List (LocatedNXParityBlock Nm mu)) : ℝ

Product of all common local factors in a located schedule.

Equations

• Anderson4D.XYCluster.locatedLedgerCommonProduct Nm mu bs = (List.map (Anderson4D.XYCluster.locatedBlockCommonTarget Nm mu) bs).prod

noncomputable def Anderson4D.XYCluster.locatedLedgerRoughScaleProduct {t : PlaneTree} {m : ℕ} {Nm : t.HeppMarking} {mu : t.Multiplicities} (R : ℝ) (bs : List (LocatedNXParityBlock Nm mu)) : ℝ

Product of all explicit rough scale factors in a located schedule.

Equations

• Anderson4D.XYCluster.locatedLedgerRoughScaleProduct R bs = (List.map (Anderson4D.XYCluster.locatedBlockRoughScale R) bs).prod

noncomputable def Anderson4D.XYCluster.locatedLedgerPreciseGainProduct {t : PlaneTree} {m : ℕ} (Nm : t.HeppMarking) (mu : t.Multiplicities) (bs : List (LocatedNXParityBlock Nm mu)) : ℝ

Product of all retained precise-pair gains in a located schedule.

Equations

• Anderson4D.XYCluster.locatedLedgerPreciseGainProduct Nm mu bs = (List.map (Anderson4D.XYCluster.locatedBlockPreciseGain Nm mu) bs).prod

theorem Anderson4D.XYCluster.nxParityBlockTarget_product_eq_ledgers {t : PlaneTree} {m : ℕ} (Nm : t.HeppMarking) (mu : t.Multiplicities) (R : ℝ) (hR : 0 < R) (bs : List (LocatedNXParityBlock Nm mu)) : (List.map (fun (b : LocatedNXParityBlock Nm mu) => nxParityBlockTarget Nm mu R b.analyticBlock) bs).prod = locatedLedgerCommonProduct Nm mu bs * (locatedLedgerLossAtoms Nm mu bs).prod * locatedLedgerRoughScaleProduct R bs * locatedLedgerPreciseGainProduct Nm mu bs

Exact product normal form, retaining multiplicities of scalar losses.

theorem Anderson4D.XYCluster.length_locatedLedgerLossAtoms {t : PlaneTree} {m : ℕ} (Nm : t.HeppMarking) (mu : t.Multiplicities) (bs : List (LocatedNXParityBlock Nm mu)) : (locatedLedgerLossAtoms Nm mu bs).length = positionLossAtomBudget (nxParitySingleCount (List.map LocatedNXParityBlock.analyticBlock bs)) (nxParityRoughPairCount (List.map LocatedNXParityBlock.analyticBlock bs))

The length of the occurrence ledger is exactly 2·single + 4·rough.

theorem Anderson4D.XYCluster.mem_locatedLedgerLossAtoms_nonneg {t : PlaneTree} {m : ℕ} (Nm : t.HeppMarking) (mu : t.Multiplicities) (bs : List (LocatedNXParityBlock Nm mu)) {x : ℝ} (hx : x ∈ locatedLedgerLossAtoms Nm mu bs) : 0 ≤ x

theorem Anderson4D.XYCluster.mem_locatedLedgerLossAtoms_le_totalMultiplicity {t : PlaneTree} {m : ℕ} (Nm : t.HeppMarking) (mu : t.Multiplicities) (bs : List (LocatedNXParityBlock Nm mu)) {x : ℝ} (hx : x ∈ locatedLedgerLossAtoms Nm mu bs) : x ≤ ↑(totalMultiplicity mu)

theorem Anderson4D.XYCluster.locatedLedgerLossAtoms_prod_le_positionLossBase_pow {t : PlaneTree} {m : ℕ} (Nm : t.HeppMarking) (mu : t.Multiplicities) (bs : List (LocatedNXParityBlock Nm mu)) (hcard : (locatedLedgerLossAtoms Nm mu bs).length ≤ 20) : (locatedLedgerLossAtoms Nm mu bs).prod ≤ ↑positionLossBase ^ totalMultiplicity mu

At most twenty scalar-loss occurrences are absorbed by the explicit universal exponential. This is a list theorem, so repeated equal atoms are counted with their true multiplicity.

theorem Anderson4D.XYCluster.finAnchorNXCoarse_lossAtoms_prod_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)) : (locatedLedgerLossAtoms Nm mu (finAnchorNXLocatedCoarseLedgerWithPhases Nm mu leftPhase rightPhase anchor cls O)).prod ≤ ↑positionLossBase ^ totalMultiplicity mu

Concrete loss absorption for the marked anchored schedule.

theorem Anderson4D.XYCluster.finAnchorNXCoarse_targetProduct_eq_ledgers {t : PlaneTree} {m : ℕ} (Nm : t.HeppMarking) (mu : t.Multiplicities) (R : ℝ) (hR : 0 < R) (leftPhase rightPhase : Bool) (anchor : Fin m) (cls : Fin m → ActiveNXClass Nm mu) (O : Finset (AdjacentIndex m)) : (List.map (fun (b : NXParityBlock Nm mu) => nxParityBlockTarget Nm mu R b) (finAnchorNXCoarseLedgerWithPhases Nm mu leftPhase rightPhase anchor cls O)).prod = locatedLedgerCommonProduct Nm mu (finAnchorNXLocatedCoarseLedgerWithPhases Nm mu leftPhase rightPhase anchor cls O) * (locatedLedgerLossAtoms Nm mu (finAnchorNXLocatedCoarseLedgerWithPhases Nm mu leftPhase rightPhase anchor cls O)).prod * locatedLedgerRoughScaleProduct R (finAnchorNXLocatedCoarseLedgerWithPhases Nm mu leftPhase rightPhase anchor cls O) * locatedLedgerPreciseGainProduct Nm mu (finAnchorNXLocatedCoarseLedgerWithPhases Nm mu leftPhase rightPhase anchor cls O)

Exact normal form for the concrete marked anchored schedule.