The rough-scale payoff in the one-parity ledger

This file records, with multiplicity, the skipped incoming edges whose rough estimates contribute the explicit (N / R)² factors in (5.90)--(5.92). It also isolates the two estimates needed to collapse those local factors to the root scale:

• marking the first fuel eligible pairs retains at least the first min skipped fuel skipped occurrences;
• every active N-class lies below the root Hepp scale.

The occurrence list below is deliberately a List, rather than a Finset: when both incoming edges of one rough pair are skipped, both copies of the scale gain occur in the analytic target.

Pure positional counting

def Anderson4D.XYCluster.positionExceptionSkippedCountBlock {m : ℕ} : PositionExceptionControlBlock m → ℕ

Number of skipped incoming edges carried by one positional block.

Equations

• One or more equations did not get rendered due to their size.
• Anderson4D.XYCluster.positionExceptionSkippedCountBlock (Anderson4D.XYCluster.PositionExceptionControlBlock.single position skipped) = if skipped = true then 1 else 0

def Anderson4D.XYCluster.positionExceptionSkippedCount {m : ℕ} : List (PositionExceptionControlBlock m) → ℕ

Number of skipped incoming-edge occurrences in a positional ledger.

Equations

• Anderson4D.XYCluster.positionExceptionSkippedCount [] = 0
• Anderson4D.XYCluster.positionExceptionSkippedCount (b :: bs) = Anderson4D.XYCluster.positionExceptionSkippedCountBlock b + Anderson4D.XYCluster.positionExceptionSkippedCount bs

def Anderson4D.XYCluster.positionExceptionRoughFactorCountBlock {m : ℕ} : PositionExceptionControlBlock m → ℕ

Number of rough scale factors retained by one positional block. Singles are intrinsically rough; unmarked pairs contribute none.

Equations

• One or more equations did not get rendered due to their size.
• Anderson4D.XYCluster.positionExceptionRoughFactorCountBlock (Anderson4D.XYCluster.PositionExceptionControlBlock.single position skipped) = if skipped = true then 1 else 0
• Anderson4D.XYCluster.positionExceptionRoughFactorCountBlock (Anderson4D.XYCluster.PositionExceptionControlBlock.pair leftPosition rightPosition skipLeft skipRight) = 0

def Anderson4D.XYCluster.positionExceptionRoughFactorCount {m : ℕ} : List (PositionExceptionControlBlock m) → ℕ

Number of explicit (N/R)² occurrences retained by a ledger.

Equations

• Anderson4D.XYCluster.positionExceptionRoughFactorCount [] = 0
• Anderson4D.XYCluster.positionExceptionRoughFactorCount (b :: bs) = Anderson4D.XYCluster.positionExceptionRoughFactorCountBlock b + Anderson4D.XYCluster.positionExceptionRoughFactorCount bs

@[simp]

theorem Anderson4D.XYCluster.positionExceptionSkippedCount_append {m : ℕ} (bs cs : List (PositionExceptionControlBlock m)) : positionExceptionSkippedCount (bs ++ cs) = positionExceptionSkippedCount bs + positionExceptionSkippedCount cs

theorem Anderson4D.XYCluster.positionExceptionSkippedCount_finAnchor_raw_eq_positionSums {m : ℕ} (leftPhase rightPhase : Bool) (anchor : Fin m) (O : Finset (AdjacentIndex m)) : positionExceptionSkippedCount (finAnchorPositionExceptionControlLedgerWithPhases leftPhase rightPhase anchor O) = (List.map (fun (i : Fin m) => if positionIncomingSkipped O PositionDirection.reverse i = true then 1 else 0) (leftAnchorPositions anchor)).sum + (List.map (fun (i : Fin m) => if positionIncomingSkipped O PositionDirection.forward i = true then 1 else 0) (rightAnchorPositions anchor)).sum

The raw skip count is the sum of the incoming-edge indicators on the two outward position runs, independently of the pairing phases.

theorem Anderson4D.XYCluster.positionExceptionSkippedCount_finAnchor_raw {n : ℕ} (leftPhase rightPhase : Bool) (anchor : Fin (n + 1)) (O : Finset (AdjacentIndex (n + 1))) : positionExceptionSkippedCount (finAnchorPositionExceptionControlLedgerWithPhases leftPhase rightPhase anchor O) = O.card

Every original adjacency is the incoming edge of exactly one non-anchor position. Hence the raw Boolean ledger counts O with no loss and no duplication.

theorem Anderson4D.XYCluster.min_positionExceptionSkippedCount_le_roughFactorCount_mark {m : ℕ} (fuel : ℕ) (bs : List (PositionExceptionControlBlock m)) : min (positionExceptionSkippedCount bs) fuel ≤ positionExceptionRoughFactorCount (markFirstSkippedPositionExceptionRough fuel bs)

Exact selection-count inequality for the first-skipped-pair algorithm.

The left side counts skipped incoming edges, not merely eligible blocks. Consequently, a marked pair whose two incoming edges are both skipped contributes two rough factors, exactly as its analytic target does.

Occurrence-level analytic ledger

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

The active dyadic scales whose explicit square factors occur in one located block. Both skipped sides of a rough pair are retained.

Equations

• One or more equations did not get rendered due to their size.
• Anderson4D.XYCluster.locatedBlockRoughScaleOccurrences (Anderson4D.XYCluster.LocatedNXParityBlock.single position a skipped) = if skipped = true then [a] else []
• Anderson4D.XYCluster.locatedBlockRoughScaleOccurrences (Anderson4D.XYCluster.LocatedNXParityBlock.pair leftPosition rightPosition p) = []

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

All rough square-factor scales, retaining their multiplicities.

Equations

• Anderson4D.XYCluster.locatedLedgerRoughScaleOccurrences bs = List.flatMap Anderson4D.XYCluster.locatedBlockRoughScaleOccurrences bs

@[simp]

theorem Anderson4D.XYCluster.length_locatedBlockRoughScaleOccurrences {t : PlaneTree} {m : ℕ} {Nm : t.HeppMarking} {mu : t.Multiplicities} (b : LocatedNXParityBlock Nm mu) : (locatedBlockRoughScaleOccurrences b).length = positionExceptionRoughFactorCountBlock b.exceptionControl

theorem Anderson4D.XYCluster.length_locatedLedgerRoughScaleOccurrences {t : PlaneTree} {m : ℕ} {Nm : t.HeppMarking} {mu : t.Multiplicities} (bs : List (LocatedNXParityBlock Nm mu)) : (locatedLedgerRoughScaleOccurrences bs).length = positionExceptionRoughFactorCount (List.map LocatedNXParityBlock.exceptionControl bs)

theorem Anderson4D.XYCluster.locatedLedgerRoughScaleProduct_eq_occurrences {t : PlaneTree} {m : ℕ} {Nm : t.HeppMarking} {mu : t.Multiplicities} (R : ℝ) (bs : List (LocatedNXParityBlock Nm mu)) : locatedLedgerRoughScaleProduct R bs = (List.map (fun (a : ActiveNXClass Nm mu) => (↑(↑a).1 / R) ^ 2) (locatedLedgerRoughScaleOccurrences bs)).prod

The rough-scale product is exactly the product over its occurrence list.

theorem Anderson4D.XYCluster.finAnchorNXLocatedCoarse_roughScaleOccurrences_count_from_raw {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)) : min (positionExceptionSkippedCount (finAnchorPositionExceptionControlLedgerWithPhases leftPhase rightPhase anchor O)) 3 ≤ (locatedLedgerRoughScaleOccurrences (finAnchorNXLocatedCoarseLedgerWithPhases Nm mu leftPhase rightPhase anchor cls O)).length

Concrete first-three selection theorem. Its left side is computed from the raw, pre-marking flags, so it does not assume an abstract supply of eligible blocks.

theorem Anderson4D.XYCluster.finAnchorNXLocatedCoarse_roughScaleOccurrences_count {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))) : min O.card 3 ≤ (locatedLedgerRoughScaleOccurrences (finAnchorNXLocatedCoarseLedgerWithPhases Nm mu leftPhase rightPhase anchor cls O)).length

Concrete paper count: the selected schedule contains at least min |O| 3 explicit square factors.

Moving local scales to the root

theorem Anderson4D.XYCluster.activeNXClass_scale_le_root {t : PlaneTree} (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (Nm : t.HeppMarking) (mu : t.Multiplicities) (a : ActiveNXClass Nm mu) : (↑a).1 ≤ scaleN Nm t.rootV

Every active N-class scale is bounded by the root Hepp scale.

theorem Anderson4D.XYCluster.scaleN_root_le_accumulatedScale_root {t : PlaneTree} (hroot : t.rootV ∈ t.BranchNodes) (Nm : t.HeppMarking) (mu : t.Multiplicities) : scaleN Nm t.rootV ≤ accumulatedScale Nm mu t.rootV

The root dyadic scale is one summand of its accumulated scale.

theorem Anderson4D.XYCluster.roughScaleOccurrence_le_root {t : PlaneTree} (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (Nm : t.HeppMarking) (mu : t.Multiplicities) (R : ℕ) (a : ActiveNXClass Nm mu) : (↑(↑a).1 / ↑R) ^ 2 ≤ (↑(scaleN Nm t.rootV) / ↑R) ^ 2

One selected local square factor is no larger than its root-scale copy.

theorem Anderson4D.XYCluster.roughScaleOccurrences_product_le_root_pow {t : PlaneTree} (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (Nm : t.HeppMarking) (mu : t.Multiplicities) (R : ℕ) (as : List (ActiveNXClass Nm mu)) : (List.map (fun (a : ActiveNXClass Nm mu) => (↑(↑a).1 / ↑R) ^ 2) as).prod ≤ (↑(scaleN Nm t.rootV) / ↑R) ^ (2 * as.length)

The product of k selected local square gains is bounded by the 2k-th power of the root ratio.

theorem Anderson4D.XYCluster.rootScaleRatio_mem_unitInterval {t : PlaneTree} (hroot : t.rootV ∈ t.BranchNodes) (Nm : t.HeppMarking) (mu : t.Multiplicities) (R : ℕ) (hR : accumulatedScale Nm mu t.rootV ≤ R) : 0 ≤ ↑(scaleN Nm t.rootV) / ↑R ∧ ↑(scaleN Nm t.rootV) / ↑R ≤ 1

Under the paper's root accumulated-scale hypothesis, the root ratio lies in the unit interval.

theorem Anderson4D.XYCluster.roughScaleOccurrences_product_le_paperRootGain {t : PlaneTree} (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (Nm : t.HeppMarking) (mu : t.Multiplicities) (R s : ℕ) (hR : accumulatedScale Nm mu t.rootV ≤ R) (as : List (ActiveNXClass Nm mu)) (hcount : min s 3 ≤ as.length) : (List.map (fun (a : ActiveNXClass Nm mu) => (↑(↑a).1 / ↑R) ^ 2) as).prod ≤ (↑(scaleN Nm t.rootV) / ↑R) ^ min (2 * s) 3

The numerical collapse used after (5.92). Counting min s 3 selected square occurrences is enough for the (slightly weaker) paper exponent min (2s) 3.

theorem Anderson4D.XYCluster.locatedLedgerRoughScaleProduct_le_paperRootGain {t : PlaneTree} {m : ℕ} (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (Nm : t.HeppMarking) (mu : t.Multiplicities) (R s : ℕ) (hR : accumulatedScale Nm mu t.rootV ≤ R) (bs : List (LocatedNXParityBlock Nm mu)) (hcount : min s 3 ≤ (locatedLedgerRoughScaleOccurrences bs).length) : locatedLedgerRoughScaleProduct (↑R) bs ≤ (↑(scaleN Nm t.rootV) / ↑R) ^ min (2 * s) 3

Ledger-facing collapse: only the exact selected-occurrence lower bound is needed. The following concrete section proves that lower bound from O.

theorem Anderson4D.XYCluster.finAnchorNXLocatedCoarse_roughScaleProduct_le {t : PlaneTree} {n : ℕ} (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (Nm : t.HeppMarking) (mu : t.Multiplicities) (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))) : locatedLedgerRoughScaleProduct (↑R) (finAnchorNXLocatedCoarseLedgerWithPhases Nm mu leftPhase rightPhase anchor cls O) ≤ (↑(scaleN Nm t.rootV) / ↑R) ^ min (2 * O.card) 3

Final concrete rough-scale ledger bound for one anchored parity schedule. This is the explicit (N_root/R)^(min (2|O|) 3) payoff used after (5.90)--(5.92).