Position bookkeeping for the fixed-class inner estimate

This file isolates the part of paper (5.87) which depends on the position of the distinguished (minimal parent-scale) leaf in the permutation.

There are two independent issues.

• Cutting the chain at the distinguished position produces a left run and a right run. Pairing consecutive positions in either parity leaves at most two singletons on each run, hence at most four altogether. Choosing at most three rough pair blocks then creates at most 2 * 4 + 4 * 3 = 20 scalar losses.
• A rough block is not literally the common target in (5.87). The exact comparison loses sqrt Y and, for a skipped incoming edge, Xi⁻¹. Both atoms are bounded by the total multiplicity. The resulting polynomial m^20 is bounded here by the explicit exponential (2^20)^m.

The last section records the orientation issue on the left of the cut. Its gain is the forward gain of the reversed class pair, and the concrete retained-edge interface preserves that orientation. The exact reindexing to the bidirectional sequence product is proved in SingleScaleAnchorGlue; no pointwise forward/reverse comparison is assumed here.

The two scalar losses in a rough local target

noncomputable def Anderson4D.XYCluster.paperDyadicXiInv {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (a : NXClass) (skipped : Bool) : ℝ

The inverse of the paper factor Xi. We keep it as a separate atom so that the 20-loss ledger counts sqrt Y and Xi⁻¹ separately.

Equations

• Anderson4D.XYCluster.paperDyadicXiInv Nm mu a skipped = if skipped = true then √(↑a.2 * Anderson4D.XYCluster.paperDyadicY Nm mu a) else 1

noncomputable def Anderson4D.XYCluster.paperDyadicRoughScaleGain (R : ℝ) (a : NXClass) (skipped : Bool) : ℝ

The explicit (N/R)² supplied by a rough estimate when the incoming edge is skipped.

Equations

• Anderson4D.XYCluster.paperDyadicRoughScaleGain R a skipped = if skipped = true then (↑a.1 / R) ^ 2 else 1

theorem Anderson4D.XYCluster.paperDyadicXiInv_nonneg {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (a : NXClass) (skipped : Bool) : 0 ≤ paperDyadicXiInv Nm mu a skipped

theorem Anderson4D.XYCluster.paperDyadicRoughScaleGain_nonneg (R : ℝ) (a : NXClass) (skipped : Bool) : 0 ≤ paperDyadicRoughScaleGain R a skipped

theorem Anderson4D.XYCluster.paperDyadicSkipXi_mul_XiInv {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) {a : NXClass} (ha : a ∈ nxCarrier Nm mu) (skipped : Bool) : paperDyadicSkipXi Nm mu a skipped * paperDyadicXiInv Nm mu a skipped = 1

On an active class, Xi * Xi⁻¹ = 1.

theorem Anderson4D.XYCluster.paperDyadicSingleRoughTarget_eq_common_mul_losses {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (R : ℝ) (hR : 0 < R) {a : NXClass} (ha : a ∈ nxCarrier Nm mu) (skipped : Bool) : paperDyadicSingleRoughTarget Nm mu R a skipped = paperDyadicLocalTarget Nm mu a skipped * √(paperDyadicY Nm mu a) * paperDyadicXiInv Nm mu a skipped * paperDyadicRoughScaleGain R a skipped

Exact comparison of a one-variable rough target with the common local factor of (5.87). No Y or Xi loss is hidden in a constant.

theorem Anderson4D.XYCluster.paperDyadicPairRoughTarget_eq_common_mul_losses {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (R : ℝ) (hR : 0 < R) {a b : NXClass} (ha : a ∈ nxCarrier Nm mu) (hb : b ∈ nxCarrier Nm mu) (skipA skipB : Bool) : paperDyadicPairRoughTarget Nm mu R a b skipA skipB = paperDyadicLocalTarget Nm mu a skipA * paperDyadicLocalTarget Nm mu b skipB * (√(paperDyadicY Nm mu a) * paperDyadicXiInv Nm mu a skipA) * (√(paperDyadicY Nm mu b) * paperDyadicXiInv Nm mu b skipB) * (paperDyadicRoughScaleGain R a skipA * paperDyadicRoughScaleGain R b skipB)

Exact rough-pair conversion. It exposes four possible scalar loss atoms (sqrt Y and Xi⁻¹ for each endpoint) and the two scale gains.

Every scalar loss is at most the total multiplicity

theorem Anderson4D.XYCluster.paperDyadicY_le_totalMultiplicity {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) {a : NXClass} (ha : a ∈ nxCarrier Nm mu) : paperDyadicY Nm mu a ≤ ↑(totalMultiplicity mu)

theorem Anderson4D.XYCluster.paperDyadicXY_le_totalMultiplicity {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) {a : NXClass} (ha : a ∈ nxCarrier Nm mu) : a.2 * (singleScaleSigma2 Nm mu a).2 ≤ totalMultiplicity mu

theorem Anderson4D.XYCluster.paperDyadicSqrtY_le_totalMultiplicity {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) {a : NXClass} (ha : a ∈ nxCarrier Nm mu) : √(paperDyadicY Nm mu a) ≤ ↑(totalMultiplicity mu)

theorem Anderson4D.XYCluster.paperDyadicXiInv_le_totalMultiplicity {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) {a : NXClass} (ha : a ∈ nxCarrier Nm mu) (skipped : Bool) : paperDyadicXiInv Nm mu a skipped ≤ ↑(totalMultiplicity mu)

The explicit m^20 <= C^m absorption

def Anderson4D.XYCluster.positionLossBase : ℕ

The concrete universal base used to absorb the twenty polynomial losses.

Equations

• Anderson4D.XYCluster.positionLossBase = 2 ^ 20

theorem Anderson4D.XYCluster.pow_twenty_le_positionLossBase_pow (m : ℕ) : m ^ 20 ≤ positionLossBase ^ m

theorem Anderson4D.XYCluster.prod_lossAtoms_le_positionLossBase_pow {ι : Type u_1} (s : Finset ι) (loss : ι → ℝ) (m : ℕ) (hcard : s.card ≤ 20) (hnonneg : ∀ i ∈ s, 0 ≤ loss i) (hle : ∀ i ∈ s, loss i ≤ ↑m) : ∏ i ∈ s, loss i ≤ ↑positionLossBase ^ m

A product of at most twenty nonnegative atoms, each at most m, is absorbed by the same universal exponential.

Pairing the two runs cut at the distinguished position

inductive Anderson4D.XYCluster.PositionBlock (α : Type u_1) : Type u_1

A purely positional single or consecutive-pair block.

• single {α : Type u_1} (x : α) : PositionBlock α
• pair {α : Type u_1} (x y : α) : PositionBlock α

def Anderson4D.XYCluster.instDecidableEqPositionBlock.decEq {α✝ : Type u_1} [DecidableEq α✝] (x✝ x✝¹ : PositionBlock α✝) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Anderson4D.XYCluster.instDecidableEqPositionBlock.decEq (Anderson4D.XYCluster.PositionBlock.single x_2) (Anderson4D.XYCluster.PositionBlock.pair x_3 y) = isFalse ⋯
• Anderson4D.XYCluster.instDecidableEqPositionBlock.decEq (Anderson4D.XYCluster.PositionBlock.pair x_2 y) (Anderson4D.XYCluster.PositionBlock.single x_3) = isFalse ⋯

@[implicit_reducible]

instance Anderson4D.XYCluster.instDecidableEqPositionBlock {α✝ : Type u_1} [DecidableEq α✝] : DecidableEq (PositionBlock α✝)

Equations

• Anderson4D.XYCluster.instDecidableEqPositionBlock = Anderson4D.XYCluster.instDecidableEqPositionBlock.decEq

def Anderson4D.XYCluster.pairPositionRun {α : Type u_1} : Bool → List α → List (PositionBlock α)

Pair consecutive entries of a run. In the shifted phase the first entry is left single before ordinary pairing starts.

Equations

• Anderson4D.XYCluster.pairPositionRun false [] = []
• Anderson4D.XYCluster.pairPositionRun false [x_2] = [Anderson4D.XYCluster.PositionBlock.single x_2]
• Anderson4D.XYCluster.pairPositionRun false (x_2 :: y :: xs) = Anderson4D.XYCluster.PositionBlock.pair x_2 y :: Anderson4D.XYCluster.pairPositionRun false xs
• Anderson4D.XYCluster.pairPositionRun true [] = []
• Anderson4D.XYCluster.pairPositionRun true (x_2 :: xs) = Anderson4D.XYCluster.PositionBlock.single x_2 :: Anderson4D.XYCluster.pairPositionRun false xs

def Anderson4D.XYCluster.PositionBlock.entries {α : Type u_1} : PositionBlock α → List α

Positions contained in a block, in traversal order.

Equations

• (Anderson4D.XYCluster.PositionBlock.single x_1).entries = [x_1]
• (Anderson4D.XYCluster.PositionBlock.pair x_1 y).entries = [x_1, y]

def Anderson4D.XYCluster.PositionBlock.map {α : Type u_1} {β : Type u_2} (f : α → β) : PositionBlock α → PositionBlock β

Equations

• Anderson4D.XYCluster.PositionBlock.map f (Anderson4D.XYCluster.PositionBlock.single x_1) = Anderson4D.XYCluster.PositionBlock.single (f x_1)
• Anderson4D.XYCluster.PositionBlock.map f (Anderson4D.XYCluster.PositionBlock.pair x_1 y) = Anderson4D.XYCluster.PositionBlock.pair (f x_1) (f y)

@[simp]

theorem Anderson4D.XYCluster.pairPositionRun_map {α : Type u_1} {β : Type u_2} (phase : Bool) (f : α → β) (xs : List α) : List.map (PositionBlock.map f) (pairPositionRun phase xs) = pairPositionRun phase (List.map f xs)

@[simp]

theorem Anderson4D.XYCluster.flatten_pairPositionRun {α : Type u_1} (phase : Bool) (xs : List α) : List.flatMap PositionBlock.entries (pairPositionRun phase xs) = xs

theorem Anderson4D.XYCluster.pairPositionRun_pair_endpoints_mem {α : Type u_1} (phase : Bool) (xs : List α) (x y : α) (h : PositionBlock.pair x y ∈ pairPositionRun phase xs) : x ∈ xs ∧ y ∈ xs

Both endpoints of a pair block really occur in the run it was built from. This small interface avoids reopening the recursive pairing definition in later geometric arguments.

def Anderson4D.XYCluster.positionSingleCount {α : Type u_1} (bs : List (PositionBlock α)) : ℕ

Number of one-variable estimates in a schedule.

Equations

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

@[simp]

theorem Anderson4D.XYCluster.positionSingleCount_single_cons {α : Type u_1} (x : α) (bs : List (PositionBlock α)) : positionSingleCount (PositionBlock.single x :: bs) = positionSingleCount bs + 1

@[simp]

theorem Anderson4D.XYCluster.positionSingleCount_pair_cons {α : Type u_1} (x y : α) (bs : List (PositionBlock α)) : positionSingleCount (PositionBlock.pair x y :: bs) = positionSingleCount bs

theorem Anderson4D.XYCluster.positionSingleCount_pairPositionRun_le_two {α : Type u_1} (phase : Bool) (xs : List α) : positionSingleCount (pairPositionRun phase xs) ≤ 2

theorem Anderson4D.XYCluster.positionSingleCount_pairPositionRun_le_two.falseLeOne {α : Type u_1} (ys : List α) : positionSingleCount (pairPositionRun false ys) ≤ 1

theorem Anderson4D.XYCluster.positionSingleCount_append {α : Type u_1} (xs ys : List (PositionBlock α)) : positionSingleCount (xs ++ ys) = positionSingleCount xs + positionSingleCount ys

def Anderson4D.XYCluster.anchorPositionSchedule {α : Type u_1} (phase : Bool) (left right : List α) : List (PositionBlock α)

Pair both sides of a cut. The lists are ordered away from the anchor; the left list is therefore the mirrored traversal.

Equations

• Anderson4D.XYCluster.anchorPositionSchedule phase left right = Anderson4D.XYCluster.pairPositionRun phase left ++ Anderson4D.XYCluster.pairPositionRun phase right

def Anderson4D.XYCluster.anchorPositionScheduleWithPhases {α : Type u_1} (leftPhase rightPhase : Bool) (left right : List α) : List (PositionBlock α)

Independent phases are required after reversing the left run.

Equations

• Anderson4D.XYCluster.anchorPositionScheduleWithPhases leftPhase rightPhase left right = Anderson4D.XYCluster.pairPositionRun leftPhase left ++ Anderson4D.XYCluster.pairPositionRun rightPhase right

theorem Anderson4D.XYCluster.anchorPositionSchedule_singleCount_le_four {α : Type u_1} (phase : Bool) (left right : List α) : positionSingleCount (anchorPositionSchedule phase left right) ≤ 4

The promised at-most-four one-variable blocks.

theorem Anderson4D.XYCluster.anchorPositionScheduleWithPhases_singleCount_le_four {α : Type u_1} (leftPhase rightPhase : Bool) (left right : List α) : positionSingleCount (anchorPositionScheduleWithPhases leftPhase rightPhase left right) ≤ 4

@[simp]

theorem Anderson4D.XYCluster.flatten_anchorPositionSchedule {α : Type u_1} (phase : Bool) (left right : List α) : List.flatMap PositionBlock.entries (anchorPositionSchedule phase left right) = left ++ right

@[simp]

theorem Anderson4D.XYCluster.flatten_anchorPositionScheduleWithPhases {α : Type u_1} (leftPhase rightPhase : Bool) (left right : List α) : List.flatMap PositionBlock.entries (anchorPositionScheduleWithPhases leftPhase rightPhase left right) = left ++ right

def Anderson4D.XYCluster.positionBlockToNXParityBlock {α : Type u_1} {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (cls : α → ActiveNXClass Nm mu) (incomingSkipped : α → Bool) : PositionBlock α → NXParityBlock Nm mu

A schedule whose blocks remember the active (N,X) class at every position.

Equations

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

def Anderson4D.XYCluster.nxParitySingleCount {t : PlaneTree} {Nm : t.HeppMarking} {mu : t.Multiplicities} (bs : List (NXParityBlock Nm mu)) : ℕ

Number of one-variable blocks after classes have been attached.

Equations

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

def Anderson4D.XYCluster.nxParityRoughPairCount {t : PlaneTree} {Nm : t.HeppMarking} {mu : t.Multiplicities} (bs : List (NXParityBlock Nm mu)) : ℕ

Number of pair blocks deliberately assigned the rough estimate (5.90).

Equations

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

@[simp]

theorem Anderson4D.XYCluster.nxParitySingleCount_single_cons {t : PlaneTree} {Nm : t.HeppMarking} {mu : t.Multiplicities} (a : ActiveNXClass Nm mu) (skipped : Bool) (bs : List (NXParityBlock Nm mu)) : nxParitySingleCount (NXParityBlock.single a skipped :: bs) = nxParitySingleCount bs + 1

@[simp]

theorem Anderson4D.XYCluster.nxParitySingleCount_pair_cons {t : PlaneTree} {Nm : t.HeppMarking} {mu : t.Multiplicities} (p : NXPairBlock Nm mu) (bs : List (NXParityBlock Nm mu)) : nxParitySingleCount (NXParityBlock.pair p :: bs) = nxParitySingleCount bs

@[simp]

theorem Anderson4D.XYCluster.nxParitySingleCount_roughPair_cons {t : PlaneTree} {Nm : t.HeppMarking} {mu : t.Multiplicities} (p : NXPairBlock Nm mu) (bs : List (NXParityBlock Nm mu)) : nxParitySingleCount (NXParityBlock.roughPair p :: bs) = nxParitySingleCount bs

@[simp]

theorem Anderson4D.XYCluster.nxParityRoughPairCount_single_cons {t : PlaneTree} {Nm : t.HeppMarking} {mu : t.Multiplicities} (a : ActiveNXClass Nm mu) (skipped : Bool) (bs : List (NXParityBlock Nm mu)) : nxParityRoughPairCount (NXParityBlock.single a skipped :: bs) = nxParityRoughPairCount bs

@[simp]

theorem Anderson4D.XYCluster.nxParityRoughPairCount_pair_cons {t : PlaneTree} {Nm : t.HeppMarking} {mu : t.Multiplicities} (p : NXPairBlock Nm mu) (bs : List (NXParityBlock Nm mu)) : nxParityRoughPairCount (NXParityBlock.pair p :: bs) = nxParityRoughPairCount bs

@[simp]

theorem Anderson4D.XYCluster.nxParityRoughPairCount_roughPair_cons {t : PlaneTree} {Nm : t.HeppMarking} {mu : t.Multiplicities} (p : NXPairBlock Nm mu) (bs : List (NXParityBlock Nm mu)) : nxParityRoughPairCount (NXParityBlock.roughPair p :: bs) = nxParityRoughPairCount bs + 1

theorem Anderson4D.XYCluster.nxParitySingleCount_append {t : PlaneTree} {Nm : t.HeppMarking} {mu : t.Multiplicities} (xs ys : List (NXParityBlock Nm mu)) : nxParitySingleCount (xs ++ ys) = nxParitySingleCount xs + nxParitySingleCount ys

theorem Anderson4D.XYCluster.nxParityRoughPairCount_append {t : PlaneTree} {Nm : t.HeppMarking} {mu : t.Multiplicities} (xs ys : List (NXParityBlock Nm mu)) : nxParityRoughPairCount (xs ++ ys) = nxParityRoughPairCount xs + nxParityRoughPairCount ys

theorem Anderson4D.XYCluster.nxParitySingleCount_map_positionBlockToNXParityBlock {α : Type u_1} {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (cls : α → ActiveNXClass Nm mu) (incomingSkipped : α → Bool) (bs : List (PositionBlock α)) : nxParitySingleCount (List.map (positionBlockToNXParityBlock Nm mu cls incomingSkipped) bs) = positionSingleCount bs

theorem Anderson4D.XYCluster.nxParityRoughPairCount_map_positionBlockToNXParityBlock {α : Type u_1} {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (cls : α → ActiveNXClass Nm mu) (incomingSkipped : α → Bool) (bs : List (PositionBlock α)) : nxParityRoughPairCount (List.map (positionBlockToNXParityBlock Nm mu cls incomingSkipped) bs) = 0

def Anderson4D.XYCluster.nxPairBlockTouchesSkip {t : PlaneTree} {Nm : t.HeppMarking} {mu : t.Multiplicities} (p : NXPairBlock Nm mu) : Bool

Whether a refined pair touches a skipped edge and is therefore eligible for one of the paper's at-most-three rough estimates.

Equations

• Anderson4D.XYCluster.nxPairBlockTouchesSkip p = (p.skipLeft || p.skipRight)

def Anderson4D.XYCluster.markFirstSkippedPairsRough {t : PlaneTree} {Nm : t.HeppMarking} {mu : t.Multiplicities} : ℕ → List (NXParityBlock Nm mu) → List (NXParityBlock Nm mu)

Mark the first fuel eligible refined pairs as rough. This is the literal "choose three (or all if fewer)" operation following (5.92).

Equations

• One or more equations did not get rendered due to their size.
• Anderson4D.XYCluster.markFirstSkippedPairsRough x✝ [] = []
• Anderson4D.XYCluster.markFirstSkippedPairsRough 0 x✝ = x✝

@[simp]

theorem Anderson4D.XYCluster.length_markFirstSkippedPairsRough {t : PlaneTree} {Nm : t.HeppMarking} {mu : t.Multiplicities} (fuel : ℕ) (bs : List (NXParityBlock Nm mu)) : (markFirstSkippedPairsRough fuel bs).length = bs.length

theorem Anderson4D.XYCluster.nxParitySingleCount_markFirstSkippedPairsRough {t : PlaneTree} {Nm : t.HeppMarking} {mu : t.Multiplicities} (fuel : ℕ) (bs : List (NXParityBlock Nm mu)) : nxParitySingleCount (markFirstSkippedPairsRough fuel bs) = nxParitySingleCount bs

theorem Anderson4D.XYCluster.nxParityRoughPairCount_markFirstSkippedPairsRough_le {t : PlaneTree} {Nm : t.HeppMarking} {mu : t.Multiplicities} (fuel : ℕ) (bs : List (NXParityBlock Nm mu)) : nxParityRoughPairCount (markFirstSkippedPairsRough fuel bs) ≤ nxParityRoughPairCount bs + fuel

Rough marking creates at most fuel new rough pairs.

def Anderson4D.XYCluster.positionLossAtomBudget (singleBlocks roughPairs : ℕ) : ℕ

The scalar-loss ledger has two atoms for each single block and four for each rough pair.

Equations

• Anderson4D.XYCluster.positionLossAtomBudget singleBlocks roughPairs = 2 * singleBlocks + 4 * roughPairs

theorem Anderson4D.XYCluster.positionLossAtomBudget_le_twenty {singleBlocks roughPairs : ℕ} (hsingle : singleBlocks ≤ 4) (hrough : roughPairs ≤ 3) : positionLossAtomBudget singleBlocks roughPairs ≤ 20

The concrete cut of Fin m at an anchor

def Anderson4D.XYCluster.leftAnchorPositions {m : ℕ} (anchor : Fin m) : List (Fin m)

Positions strictly to the left of the anchor, ordered away from the anchor. Thus this list is decreasing in the original word order.

Equations

• Anderson4D.XYCluster.leftAnchorPositions anchor = List.map (fun (i : Fin ↑anchor) => ⟨↑i, ⋯⟩) (List.finRange ↑anchor).reverse

def Anderson4D.XYCluster.rightAnchorPositions {m : ℕ} (anchor : Fin m) : List (Fin m)

Positions strictly to the right of the anchor, ordered away from the anchor (increasing in the original word order).

Equations

• Anderson4D.XYCluster.rightAnchorPositions anchor = List.map (fun (i : Fin (m - (↑anchor + 1))) => ⟨↑anchor + 1 + ↑i, ⋯⟩) (List.finRange (m - (↑anchor + 1)))

def Anderson4D.XYCluster.anchorPositionOutwardOffset {m : ℕ} (anchor i : Fin m) : ℕ

Zero-based position inside the outward run on the position's side.

Equations

• Anderson4D.XYCluster.anchorPositionOutwardOffset anchor i = if ↑i < ↑anchor then ↑anchor - 1 - ↑i else ↑i - (↑anchor + 1)

@[simp]

theorem Anderson4D.XYCluster.length_leftAnchorPositions {m : ℕ} (anchor : Fin m) : (leftAnchorPositions anchor).length = ↑anchor

@[simp]

theorem Anderson4D.XYCluster.length_rightAnchorPositions {m : ℕ} (anchor : Fin m) : (rightAnchorPositions anchor).length = m - (↑anchor + 1)

theorem Anderson4D.XYCluster.leftAnchorPositions_nodup {m : ℕ} (anchor : Fin m) : (leftAnchorPositions anchor).Nodup

theorem Anderson4D.XYCluster.rightAnchorPositions_nodup {m : ℕ} (anchor : Fin m) : (rightAnchorPositions anchor).Nodup

theorem Anderson4D.XYCluster.map_anchorPositionOutwardOffset_left {m : ℕ} (anchor : Fin m) : List.map (anchorPositionOutwardOffset anchor) (leftAnchorPositions anchor) = List.range ↑anchor

theorem Anderson4D.XYCluster.map_anchorPositionOutwardOffset_right {m : ℕ} (anchor : Fin m) : List.map (anchorPositionOutwardOffset anchor) (rightAnchorPositions anchor) = List.range (m - (↑anchor + 1))

theorem Anderson4D.XYCluster.mem_leftAnchorPositions_iff {m : ℕ} (anchor i : Fin m) : i ∈ leftAnchorPositions anchor ↔ ↑i < ↑anchor

theorem Anderson4D.XYCluster.mem_rightAnchorPositions_iff {m : ℕ} (anchor i : Fin m) : i ∈ rightAnchorPositions anchor ↔ ↑anchor < ↑i

theorem Anderson4D.XYCluster.mem_left_or_right_anchor_iff {m : ℕ} (anchor i : Fin m) : i ∈ leftAnchorPositions anchor ∨ i ∈ rightAnchorPositions anchor ↔ i ≠ anchor

The two concrete runs contain every position except the anchor, exactly as a set.

theorem Anderson4D.XYCluster.leftAnchorPositions_disjoint_right {m : ℕ} (anchor : Fin m) : (leftAnchorPositions anchor).Disjoint (rightAnchorPositions anchor)

theorem Anderson4D.XYCluster.left_append_rightAnchorPositions_nodup {m : ℕ} (anchor : Fin m) : (leftAnchorPositions anchor ++ rightAnchorPositions anchor).Nodup

def Anderson4D.XYCluster.finAnchorPositionSchedule {m : ℕ} (phase : Bool) (anchor : Fin m) : List (PositionBlock (Fin m))

The concrete schedule obtained by cutting Fin m at anchor.

Equations

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

def Anderson4D.XYCluster.finAnchorPositionScheduleWithPhases {m : ℕ} (leftPhase rightPhase : Bool) (anchor : Fin m) : List (PositionBlock (Fin m))

Concrete anchor schedule with the independently selectable phases used on the reversed left and forward right runs.

Equations

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

theorem Anderson4D.XYCluster.finAnchorPositionSchedule_singleCount_le_four {m : ℕ} (phase : Bool) (anchor : Fin m) : positionSingleCount (finAnchorPositionSchedule phase anchor) ≤ 4

theorem Anderson4D.XYCluster.finAnchorPositionScheduleWithPhases_singleCount_le_four {m : ℕ} (leftPhase rightPhase : Bool) (anchor : Fin m) : positionSingleCount (finAnchorPositionScheduleWithPhases leftPhase rightPhase anchor) ≤ 4

theorem Anderson4D.XYCluster.length_flatten_finAnchorPositionSchedule {m : ℕ} (phase : Bool) (anchor : Fin m) : (List.flatMap PositionBlock.entries (finAnchorPositionSchedule phase anchor)).length = m - 1

Counting entries after the cut gives exactly m-1; the anchor is the single omitted position.

theorem Anderson4D.XYCluster.flatten_finAnchorPositionScheduleWithPhases {m : ℕ} (leftPhase rightPhase : Bool) (anchor : Fin m) : List.flatMap PositionBlock.entries (finAnchorPositionScheduleWithPhases leftPhase rightPhase anchor) = leftAnchorPositions anchor ++ rightAnchorPositions anchor

theorem Anderson4D.XYCluster.mem_flatten_finAnchorPositionScheduleWithPhases_iff {m : ℕ} (leftPhase rightPhase : Bool) (anchor i : Fin m) : i ∈ List.flatMap PositionBlock.entries (finAnchorPositionScheduleWithPhases leftPhase rightPhase anchor) ↔ i ≠ anchor

theorem Anderson4D.XYCluster.length_flatten_finAnchorPositionScheduleWithPhases {m : ℕ} (leftPhase rightPhase : Bool) (anchor : Fin m) : (List.flatMap PositionBlock.entries (finAnchorPositionScheduleWithPhases leftPhase rightPhase anchor)).length = m - 1

theorem Anderson4D.XYCluster.nodup_flatten_finAnchorPositionScheduleWithPhases {m : ℕ} (leftPhase rightPhase : Bool) (anchor : Fin m) : (List.flatMap PositionBlock.entries (finAnchorPositionScheduleWithPhases leftPhase rightPhase anchor)).Nodup

inductive Anderson4D.XYCluster.PositionDirection : Type

Direction of traversal away from the anchor.

• forward : PositionDirection
• reverse : PositionDirection

@[implicit_reducible]

instance Anderson4D.XYCluster.instDecidableEqPositionDirection : DecidableEq PositionDirection

Equations

• Anderson4D.XYCluster.instDecidableEqPositionDirection x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Anderson4D.XYCluster.forwardIncomingEdge {m : ℕ} (i : Fin m) : Option (AdjacentIndex m)

Incoming adjacency in the original left-to-right orientation.

Equations

• Anderson4D.XYCluster.forwardIncomingEdge i = if h : 0 < ↑i then some ⟨⟨↑i - 1, ⋯⟩, ⋯⟩ else none

def Anderson4D.XYCluster.reverseIncomingEdge {m : ℕ} (i : Fin m) : Option (AdjacentIndex m)

Incoming adjacency when traversing the word from right to left.

Equations

• Anderson4D.XYCluster.reverseIncomingEdge i = if h : ↑i + 1 < m then some ⟨i, h⟩ else none

def Anderson4D.XYCluster.positionIncomingSkipped {m : ℕ} (O : Finset (AdjacentIndex m)) (dir : PositionDirection) (i : Fin m) : Bool

Whether the edge entering a position in the chosen traversal direction belongs to the skipped set O.

Equations

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

Position-preserving exceptional-gain ledger

def Anderson4D.XYCluster.positionIncidentEdges {m : ℕ} (i : Fin m) : Finset (AdjacentIndex m)

The original chain edges incident to a position. These are the only ratio gains whose local argument can use that position.

Equations

• Anderson4D.XYCluster.positionIncidentEdges i = (Anderson4D.XYCluster.forwardIncomingEdge i).toFinset ∪ (Anderson4D.XYCluster.reverseIncomingEdge i).toFinset

def Anderson4D.XYCluster.PositionBlock.affectedEdges {m : ℕ} : PositionBlock (Fin m) → Finset (AdjacentIndex m)

The original ratio-gain edges touched by a one- or two-variable local operation. This definition is geometric: an edge is recorded only when one of its endpoints is actually eliminated by the block.

Equations

• (Anderson4D.XYCluster.PositionBlock.single i).affectedEdges = Anderson4D.XYCluster.positionIncidentEdges i
• (Anderson4D.XYCluster.PositionBlock.pair i j).affectedEdges = Anderson4D.XYCluster.positionIncidentEdges i ∪ Anderson4D.XYCluster.positionIncidentEdges j

The genuine even/odd carrier in original edge coordinates

def Anderson4D.XYCluster.anchorEdgeOutwardDistance {m : ℕ} (anchor : Fin m) (j : AdjacentIndex m) : ℕ

Distance of an original adjacency edge from the anchor, measured outward on its own side. Both boundary edges adjacent to the anchor have distance zero.

Equations

• Anderson4D.XYCluster.anchorEdgeOutwardDistance anchor j = if ↑↑j < ↑anchor then ↑anchor - 1 - ↑↑j else ↑↑j - ↑anchor

def Anderson4D.XYCluster.anchorEdgeSelectedPhase {m : ℕ} (leftPhase rightPhase : Bool) (anchor : Fin m) (j : AdjacentIndex m) : Bool

The phase selected on the side containing an original adjacency edge.

Equations

• Anderson4D.XYCluster.anchorEdgeSelectedPhase leftPhase rightPhase anchor j = if ↑↑j < ↑anchor then leftPhase else rightPhase

@[simp]

theorem Anderson4D.XYCluster.anchorEdgeSelectedPhase_flip {m : ℕ} (leftPhase rightPhase : Bool) (anchor : Fin m) (j : AdjacentIndex m) : anchorEdgeSelectedPhase (!leftPhase) (!rightPhase) anchor j = !anchorEdgeSelectedPhase leftPhase rightPhase anchor j

def Anderson4D.XYCluster.finAnchorPositionPhaseCarrierWithPhases {m : ℕ} (leftPhase rightPhase : Bool) (anchor : Fin m) : Finset (AdjacentIndex m)

The original edges matched by one parity schedule. Shifted phase true selects even outward distances (including the anchor boundary), while ordinary phase false selects odd outward distances.

Equations

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

@[simp]

theorem Anderson4D.XYCluster.mem_finAnchorPositionPhaseCarrierWithPhases {m : ℕ} (leftPhase rightPhase : Bool) (anchor : Fin m) (j : AdjacentIndex m) : j ∈ finAnchorPositionPhaseCarrierWithPhases leftPhase rightPhase anchor ↔ decide (anchorEdgeOutwardDistance anchor j % 2 = 0) = anchorEdgeSelectedPhase leftPhase rightPhase anchor j

theorem Anderson4D.XYCluster.finAnchorPositionPhaseCarrier_union_flip {m : ℕ} (leftPhase rightPhase : Bool) (anchor : Fin m) : finAnchorPositionPhaseCarrierWithPhases leftPhase rightPhase anchor ∪ finAnchorPositionPhaseCarrierWithPhases (!leftPhase) (!rightPhase) anchor = Finset.univ

Flipping both independently chosen side phases gives the complementary carrier of original edges.

theorem Anderson4D.XYCluster.finAnchorPositionPhaseCarrier_disjoint_flip {m : ℕ} (leftPhase rightPhase : Bool) (anchor : Fin m) : Disjoint (finAnchorPositionPhaseCarrierWithPhases leftPhase rightPhase anchor) (finAnchorPositionPhaseCarrierWithPhases (!leftPhase) (!rightPhase) anchor)

theorem Anderson4D.XYCluster.finAnchorPositionPhaseCarrier_pair_or_single {m : ℕ} (leftPhase rightPhase : Bool) (anchor : Fin m) (edge : AdjacentIndex m) (hedge : edge ∈ finAnchorPositionPhaseCarrierWithPhases leftPhase rightPhase anchor) : (∃ (i : Fin m), PositionBlock.single i ∈ finAnchorPositionScheduleWithPhases leftPhase rightPhase anchor ∧ edge ∈ (PositionBlock.single i).affectedEdges) ∨ ∃ (i : Fin m) (j : Fin m), PositionBlock.pair i j ∈ finAnchorPositionScheduleWithPhases leftPhase rightPhase anchor ∧ (↑edge = i ∧ ↑i + 1 = ↑j ∨ ↑edge = j ∧ ↑j + 1 = ↑i)

Every edge selected by a phase schedule is accounted for by a concrete block: either it is incident to a singleton, or it is the internal edge of a pair. This is the converse coverage statement missing from the earlier pair-to-carrier interface.

theorem Anderson4D.XYCluster.finAnchorPositionSchedule_pair_internalEdge_mem_phaseCarrier {m : ℕ} (leftPhase rightPhase : Bool) (anchor i j : Fin m) (hpair : PositionBlock.pair i j ∈ finAnchorPositionScheduleWithPhases leftPhase rightPhase anchor) : ∃ edge ∈ finAnchorPositionPhaseCarrierWithPhases leftPhase rightPhase anchor, ↑edge = i ∧ ↑i + 1 = ↑j ∨ ↑edge = j ∧ ↑j + 1 = ↑i

Every concrete pair block contributes its internal original-word edge to the phase carrier selected for that side of the anchor. The disjunction records the reversal of the left run: right-run pairs are (i,i+1), while left-run pairs are (i,i-1) in traversal order.

theorem Anderson4D.XYCluster.card_positionIncidentEdges_le_two {m : ℕ} (i : Fin m) : (positionIncidentEdges i).card ≤ 2

theorem Anderson4D.XYCluster.PositionBlock.card_affectedEdges_le {m : ℕ} (b : PositionBlock (Fin m)) : b.affectedEdges.card ≤ match b with | single x => 2 | pair x y => 4

theorem Anderson4D.XYCluster.PositionBlock.card_affectedEdges_pair_le_three_of_adjacent {m : ℕ} (i j : Fin m) (hij : ↑i + 1 = ↑j ∨ ↑j + 1 = ↑i) : (pair i j).affectedEdges.card ≤ 3

Consecutive positions share their connecting edge, so their incident edge union has cardinality at most three.

inductive Anderson4D.XYCluster.LocatedNXParityBlock {t : PlaneTree} {m : ℕ} (Nm : t.HeppMarking) (mu : t.Multiplicities) : Type

An analytic parity block together with the exact original positions it eliminates. Unlike NXParityBlock, this type retains enough information to state which gain indices are discarded. The constructors enforce matching one- and two-variable arity.

• single {t : PlaneTree} {m : ℕ} {Nm : t.HeppMarking} {mu : t.Multiplicities} (position : Fin m) (a : ActiveNXClass Nm mu) (skipped : Bool) : LocatedNXParityBlock Nm mu
• pair {t : PlaneTree} {m : ℕ} {Nm : t.HeppMarking} {mu : t.Multiplicities} (leftPosition rightPosition : Fin m) (p : NXPairBlock Nm mu) : LocatedNXParityBlock Nm mu
• roughPair {t : PlaneTree} {m : ℕ} {Nm : t.HeppMarking} {mu : t.Multiplicities} (leftPosition rightPosition : Fin m) (p : NXPairBlock Nm mu) : LocatedNXParityBlock Nm mu

def Anderson4D.XYCluster.LocatedNXParityBlock.positionBlock {t : PlaneTree} {m : ℕ} {Nm : t.HeppMarking} {mu : t.Multiplicities} : LocatedNXParityBlock Nm mu → PositionBlock (Fin m)

Equations

• (Anderson4D.XYCluster.LocatedNXParityBlock.single i a skipped).positionBlock = Anderson4D.XYCluster.PositionBlock.single i
• (Anderson4D.XYCluster.LocatedNXParityBlock.pair i j p).positionBlock = Anderson4D.XYCluster.PositionBlock.pair i j
• (Anderson4D.XYCluster.LocatedNXParityBlock.roughPair i j p).positionBlock = Anderson4D.XYCluster.PositionBlock.pair i j

def Anderson4D.XYCluster.LocatedNXParityBlock.analyticBlock {t : PlaneTree} {m : ℕ} {Nm : t.HeppMarking} {mu : t.Multiplicities} : LocatedNXParityBlock Nm mu → NXParityBlock Nm mu

Equations

• (Anderson4D.XYCluster.LocatedNXParityBlock.single i a skipped).analyticBlock = Anderson4D.XYCluster.NXParityBlock.single a skipped
• (Anderson4D.XYCluster.LocatedNXParityBlock.pair i j p).analyticBlock = Anderson4D.XYCluster.NXParityBlock.pair p
• (Anderson4D.XYCluster.LocatedNXParityBlock.roughPair i j p).analyticBlock = Anderson4D.XYCluster.NXParityBlock.roughPair p

def Anderson4D.XYCluster.locatePositionBlock {t : PlaneTree} {m : ℕ} (Nm : t.HeppMarking) (mu : t.Multiplicities) (cls : Fin m → ActiveNXClass Nm mu) (incomingSkipped : Fin m → Bool) : PositionBlock (Fin m) → LocatedNXParityBlock Nm mu

Equations

• One or more equations did not get rendered due to their size.
• Anderson4D.XYCluster.locatePositionBlock Nm mu cls incomingSkipped (Anderson4D.XYCluster.PositionBlock.single i) = Anderson4D.XYCluster.LocatedNXParityBlock.single i (cls i) (incomingSkipped i)

@[simp]

theorem Anderson4D.XYCluster.analyticBlock_locatePositionBlock {t : PlaneTree} {m : ℕ} (Nm : t.HeppMarking) (mu : t.Multiplicities) (cls : Fin m → ActiveNXClass Nm mu) (incomingSkipped : Fin m → Bool) (b : PositionBlock (Fin m)) : (locatePositionBlock Nm mu cls incomingSkipped b).analyticBlock = positionBlockToNXParityBlock Nm mu cls incomingSkipped b

@[simp]

theorem Anderson4D.XYCluster.positionBlock_locatePositionBlock {t : PlaneTree} {m : ℕ} (Nm : t.HeppMarking) (mu : t.Multiplicities) (cls : Fin m → ActiveNXClass Nm mu) (incomingSkipped : Fin m → Bool) (b : PositionBlock (Fin m)) : (locatePositionBlock Nm mu cls incomingSkipped b).positionBlock = b

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

Position-preserving version of markFirstSkippedPairsRough.

Equations

• One or more equations did not get rendered due to their size.
• Anderson4D.XYCluster.markFirstSkippedLocatedPairsRough x✝ [] = []
• Anderson4D.XYCluster.markFirstSkippedLocatedPairsRough 0 x✝ = x✝

@[simp]

theorem Anderson4D.XYCluster.map_analyticBlock_markFirstSkippedLocatedPairsRough {t : PlaneTree} {m : ℕ} {Nm : t.HeppMarking} {mu : t.Multiplicities} (fuel : ℕ) (bs : List (LocatedNXParityBlock Nm mu)) : List.map LocatedNXParityBlock.analyticBlock (markFirstSkippedLocatedPairsRough fuel bs) = markFirstSkippedPairsRough fuel (List.map LocatedNXParityBlock.analyticBlock bs)

@[simp]

theorem Anderson4D.XYCluster.map_positionBlock_markFirstSkippedLocatedPairsRough {t : PlaneTree} {m : ℕ} {Nm : t.HeppMarking} {mu : t.Multiplicities} (fuel : ℕ) (bs : List (LocatedNXParityBlock Nm mu)) : List.map LocatedNXParityBlock.positionBlock (markFirstSkippedLocatedPairsRough fuel bs) = List.map LocatedNXParityBlock.positionBlock bs

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

Union of the actual original chain edges affected by single and rough blocks. Precise pair blocks do not discard any gain.

Equations

• One or more equations did not get rendered due to their size.
• Anderson4D.XYCluster.locatedExceptionalEdges [] = ∅
• Anderson4D.XYCluster.locatedExceptionalEdges (Anderson4D.XYCluster.LocatedNXParityBlock.pair leftPosition rightPosition p :: bs) = Anderson4D.XYCluster.locatedExceptionalEdges bs

theorem Anderson4D.XYCluster.card_locatedExceptionalEdges_le_lossAtomBudget {t : PlaneTree} {m : ℕ} {Nm : t.HeppMarking} {mu : t.Multiplicities} (bs : List (LocatedNXParityBlock Nm mu)) : (locatedExceptionalEdges bs).card ≤ positionLossAtomBudget (nxParitySingleCount (List.map LocatedNXParityBlock.analyticBlock bs)) (nxParityRoughPairCount (List.map LocatedNXParityBlock.analyticBlock bs))

The explicit edge union is bounded by exactly the same 2·single + 4·rough budget used for the scalar losses. The proof does not infer an exception count from prose: every recorded edge is incident to a concrete position in an exceptional block.

Erasing the analytic class payload from the exception ledger

inductive Anderson4D.XYCluster.PositionExceptionControlBlock (m : ℕ) : Type

The positional and skipped-edge data which alone controls rough marking.

• single {m : ℕ} (position : Fin m) (skipped : Bool) : PositionExceptionControlBlock m
• pair {m : ℕ} (leftPosition rightPosition : Fin m) (skipLeft skipRight : Bool) : PositionExceptionControlBlock m
• roughPair {m : ℕ} (leftPosition rightPosition : Fin m) (skipLeft skipRight : Bool) : PositionExceptionControlBlock m

def Anderson4D.XYCluster.instDecidableEqPositionExceptionControlBlock.decEq {m✝ : ℕ} (x✝ x✝¹ : PositionExceptionControlBlock m✝) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Anderson4D.XYCluster.instDecidableEqPositionExceptionControlBlock {m✝ : ℕ} : DecidableEq (PositionExceptionControlBlock m✝)

Equations

• Anderson4D.XYCluster.instDecidableEqPositionExceptionControlBlock = Anderson4D.XYCluster.instDecidableEqPositionExceptionControlBlock.decEq

def Anderson4D.XYCluster.positionBlockToExceptionControl {m : ℕ} (incomingSkipped : Fin m → Bool) : PositionBlock (Fin m) → PositionExceptionControlBlock m

Equations

• One or more equations did not get rendered due to their size.
• Anderson4D.XYCluster.positionBlockToExceptionControl incomingSkipped (Anderson4D.XYCluster.PositionBlock.single i) = Anderson4D.XYCluster.PositionExceptionControlBlock.single i (incomingSkipped i)

def Anderson4D.XYCluster.LocatedNXParityBlock.exceptionControl {t : PlaneTree} {m : ℕ} {Nm : t.HeppMarking} {mu : t.Multiplicities} : LocatedNXParityBlock Nm mu → PositionExceptionControlBlock m

Equations

• (Anderson4D.XYCluster.LocatedNXParityBlock.single i a skipped).exceptionControl = Anderson4D.XYCluster.PositionExceptionControlBlock.single i skipped
• (Anderson4D.XYCluster.LocatedNXParityBlock.pair i j p).exceptionControl = Anderson4D.XYCluster.PositionExceptionControlBlock.pair i j p.skipLeft p.skipRight
• (Anderson4D.XYCluster.LocatedNXParityBlock.roughPair i j p).exceptionControl = Anderson4D.XYCluster.PositionExceptionControlBlock.roughPair i j p.skipLeft p.skipRight

@[simp]

theorem Anderson4D.XYCluster.exceptionControl_locatePositionBlock {t : PlaneTree} {m : ℕ} (Nm : t.HeppMarking) (mu : t.Multiplicities) (cls : Fin m → ActiveNXClass Nm mu) (incomingSkipped : Fin m → Bool) (b : PositionBlock (Fin m)) : (locatePositionBlock Nm mu cls incomingSkipped b).exceptionControl = positionBlockToExceptionControl incomingSkipped b

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

Pure positional copy of “mark the first three eligible pairs rough”.

Equations

• One or more equations did not get rendered due to their size.
• Anderson4D.XYCluster.markFirstSkippedPositionExceptionRough x✝ [] = []
• Anderson4D.XYCluster.markFirstSkippedPositionExceptionRough 0 x✝ = x✝

@[simp]

theorem Anderson4D.XYCluster.map_exceptionControl_markFirstSkippedLocatedPairsRough {t : PlaneTree} {m : ℕ} {Nm : t.HeppMarking} {mu : t.Multiplicities} (fuel : ℕ) (bs : List (LocatedNXParityBlock Nm mu)) : List.map LocatedNXParityBlock.exceptionControl (markFirstSkippedLocatedPairsRough fuel bs) = markFirstSkippedPositionExceptionRough fuel (List.map LocatedNXParityBlock.exceptionControl bs)

def Anderson4D.XYCluster.positionExceptionControlEdges {m : ℕ} : List (PositionExceptionControlBlock m) → Finset (AdjacentIndex m)

Exceptional original edges computed with no analytic class payload.

Equations

• One or more equations did not get rendered due to their size.
• Anderson4D.XYCluster.positionExceptionControlEdges [] = ∅

theorem Anderson4D.XYCluster.positionExceptionControlEdges_map_exceptionControl {t : PlaneTree} {m : ℕ} {Nm : t.HeppMarking} {mu : t.Multiplicities} (bs : List (LocatedNXParityBlock Nm mu)) : positionExceptionControlEdges (List.map LocatedNXParityBlock.exceptionControl bs) = locatedExceptionalEdges bs

structure Anderson4D.XYCluster.AnchoredNXParityRuns {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) : Type

The two analytic runs must remain separate: concatenating them and feeding the result to conditionedNXParityChainSum would invent an edge between the two outer endpoints.

• left : List (NXParityBlock Nm mu)
• right : List (NXParityBlock Nm mu)

def Anderson4D.XYCluster.AnchoredNXParityRuns.ledger {t : PlaneTree} {Nm : t.HeppMarking} {mu : t.Multiplicities} (runs : AnchoredNXParityRuns Nm mu) : List (NXParityBlock Nm mu)

Flatten the two runs only for block counting. This list is a ledger, not an analytic chain.

Equations

• runs.ledger = runs.left ++ runs.right

def Anderson4D.XYCluster.finAnchorNXParityRunsWithPhases {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)) : AnchoredNXParityRuns Nm mu

The paper class runs on the two sides of an anchored word. The left run uses the reverse incoming edge; the right run uses the ordinary incoming edge.

Equations

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

def Anderson4D.XYCluster.finAnchorNXParityRuns {t : PlaneTree} {m : ℕ} (Nm : t.HeppMarking) (mu : t.Multiplicities) (phase : Bool) (anchor : Fin m) (cls : Fin m → ActiveNXClass Nm mu) (O : Finset (AdjacentIndex m)) : AnchoredNXParityRuns Nm mu

Equal-phase convenience wrapper. The paper-facing parity constructor below may instead use finAnchorNXParityRunsWithPhases, since reversal can change the phase on the left run.

Equations

• Anderson4D.XYCluster.finAnchorNXParityRuns Nm mu phase anchor cls O = Anderson4D.XYCluster.finAnchorNXParityRunsWithPhases Nm mu phase phase anchor cls O

def Anderson4D.XYCluster.finAnchorNXParityLedgerWithPhases {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)) : List (NXParityBlock Nm mu)

Flattened raw-run ledger, used only for the finite block counts.

Equations

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

def Anderson4D.XYCluster.finAnchorNXParityLedger {t : PlaneTree} {m : ℕ} (Nm : t.HeppMarking) (mu : t.Multiplicities) (phase : Bool) (anchor : Fin m) (cls : Fin m → ActiveNXClass Nm mu) (O : Finset (AdjacentIndex m)) : List (NXParityBlock Nm mu)

Equations

• Anderson4D.XYCluster.finAnchorNXParityLedger Nm mu phase anchor cls O = (Anderson4D.XYCluster.finAnchorNXParityRuns Nm mu phase anchor cls O).ledger

def Anderson4D.XYCluster.finAnchorNXLocatedParityLedgerWithPhases {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)) : List (LocatedNXParityBlock Nm mu)

Raw parity ledger which retains the concrete original positions. The two directions use their respective incoming edges before the lists are flattened for counting.

Equations

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

theorem Anderson4D.XYCluster.map_analyticBlock_finAnchorNXLocatedParityLedgerWithPhases {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)) : List.map LocatedNXParityBlock.analyticBlock (finAnchorNXLocatedParityLedgerWithPhases Nm mu leftPhase rightPhase anchor cls O) = finAnchorNXParityLedgerWithPhases Nm mu leftPhase rightPhase anchor cls O

theorem Anderson4D.XYCluster.map_positionBlock_finAnchorNXLocatedParityLedgerWithPhases {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)) : List.map LocatedNXParityBlock.positionBlock (finAnchorNXLocatedParityLedgerWithPhases Nm mu leftPhase rightPhase anchor cls O) = finAnchorPositionScheduleWithPhases leftPhase rightPhase anchor

def Anderson4D.XYCluster.finAnchorPositionExceptionControlLedgerWithPhases {m : ℕ} (leftPhase rightPhase : Bool) (anchor : Fin m) (O : Finset (AdjacentIndex m)) : List (PositionExceptionControlBlock m)

The raw anchor ledger after erasing every analytic (N,X) class.

Equations

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

theorem Anderson4D.XYCluster.map_exceptionControl_finAnchorNXLocatedParityLedgerWithPhases {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)) : List.map LocatedNXParityBlock.exceptionControl (finAnchorNXLocatedParityLedgerWithPhases Nm mu leftPhase rightPhase anchor cls O) = finAnchorPositionExceptionControlLedgerWithPhases leftPhase rightPhase anchor O

def Anderson4D.XYCluster.finAnchorPositionExceptionControlCoarseLedgerWithPhases {m : ℕ} (leftPhase rightPhase : Bool) (anchor : Fin m) (O : Finset (AdjacentIndex m)) : List (PositionExceptionControlBlock m)

Pure positional coarse ledger, including the global first-three rule.

Equations

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

def Anderson4D.XYCluster.finAnchorPureRawExceptionalEdgesWithPhases {m : ℕ} (leftPhase rightPhase : Bool) (anchor : Fin m) (O : Finset (AdjacentIndex m)) : Finset (AdjacentIndex m)

Raw exceptional edges before restricting them to the selected phase.

Equations

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

theorem Anderson4D.XYCluster.finAnchorNXParityLedgerWithPhases_singleCount_le_four {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)) : nxParitySingleCount (finAnchorNXParityLedgerWithPhases Nm mu leftPhase rightPhase anchor cls O) ≤ 4

theorem Anderson4D.XYCluster.finAnchorNXParityLedger_singleCount_le_four {t : PlaneTree} {m : ℕ} (Nm : t.HeppMarking) (mu : t.Multiplicities) (phase : Bool) (anchor : Fin m) (cls : Fin m → ActiveNXClass Nm mu) (O : Finset (AdjacentIndex m)) : nxParitySingleCount (finAnchorNXParityLedger Nm mu phase anchor cls O) ≤ 4

theorem Anderson4D.XYCluster.finAnchorNXParityLedgerWithPhases_roughPairCount_eq_zero {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)) : nxParityRoughPairCount (finAnchorNXParityLedgerWithPhases Nm mu leftPhase rightPhase anchor cls O) = 0

theorem Anderson4D.XYCluster.finAnchorNXParityLedger_roughPairCount_eq_zero {t : PlaneTree} {m : ℕ} (Nm : t.HeppMarking) (mu : t.Multiplicities) (phase : Bool) (anchor : Fin m) (cls : Fin m → ActiveNXClass Nm mu) (O : Finset (AdjacentIndex m)) : nxParityRoughPairCount (finAnchorNXParityLedger Nm mu phase anchor cls O) = 0

def Anderson4D.XYCluster.finAnchorNXCoarseLedgerWithPhases {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)) : List (NXParityBlock Nm mu)

Flattened coarse ledger: select the first three eligible pair blocks (or all of them if fewer). As above, this is not itself an analytic chain.

Equations

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

def Anderson4D.XYCluster.finAnchorNXCoarseLedger {t : PlaneTree} {m : ℕ} (Nm : t.HeppMarking) (mu : t.Multiplicities) (phase : Bool) (anchor : Fin m) (cls : Fin m → ActiveNXClass Nm mu) (O : Finset (AdjacentIndex m)) : List (NXParityBlock Nm mu)

Equations

• Anderson4D.XYCluster.finAnchorNXCoarseLedger Nm mu phase anchor cls O = Anderson4D.XYCluster.finAnchorNXCoarseLedgerWithPhases Nm mu phase phase anchor cls O

def Anderson4D.XYCluster.finAnchorNXLocatedCoarseLedgerWithPhases {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)) : List (LocatedNXParityBlock Nm mu)

Mark the first three eligible concrete pair blocks while retaining their positions.

Equations

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

theorem Anderson4D.XYCluster.map_analyticBlock_finAnchorNXLocatedCoarseLedgerWithPhases {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)) : List.map LocatedNXParityBlock.analyticBlock (finAnchorNXLocatedCoarseLedgerWithPhases Nm mu leftPhase rightPhase anchor cls O) = finAnchorNXCoarseLedgerWithPhases Nm mu leftPhase rightPhase anchor cls O

theorem Anderson4D.XYCluster.map_positionBlock_finAnchorNXLocatedCoarseLedgerWithPhases {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)) : List.map LocatedNXParityBlock.positionBlock (finAnchorNXLocatedCoarseLedgerWithPhases Nm mu leftPhase rightPhase anchor cls O) = finAnchorPositionScheduleWithPhases leftPhase rightPhase anchor

theorem Anderson4D.XYCluster.map_exceptionControl_finAnchorNXLocatedCoarseLedgerWithPhases {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)) : List.map LocatedNXParityBlock.exceptionControl (finAnchorNXLocatedCoarseLedgerWithPhases Nm mu leftPhase rightPhase anchor cls O) = finAnchorPositionExceptionControlCoarseLedgerWithPhases leftPhase rightPhase anchor O

theorem Anderson4D.XYCluster.locatedExceptionalEdges_finAnchorNXCoarse_eq_pure {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)) : locatedExceptionalEdges (finAnchorNXLocatedCoarseLedgerWithPhases Nm mu leftPhase rightPhase anchor cls O) = finAnchorPureRawExceptionalEdgesWithPhases leftPhase rightPhase anchor O

theorem Anderson4D.XYCluster.mem_flatten_positionBlocks_finAnchorNXLocatedCoarseLedger_iff {t : PlaneTree} {m : ℕ} (Nm : t.HeppMarking) (mu : t.Multiplicities) (leftPhase rightPhase : Bool) (anchor i : Fin m) (cls : Fin m → ActiveNXClass Nm mu) (O : Finset (AdjacentIndex m)) : i ∈ List.flatMap PositionBlock.entries (List.map LocatedNXParityBlock.positionBlock (finAnchorNXLocatedCoarseLedgerWithPhases Nm mu leftPhase rightPhase anchor cls O)) ↔ i ≠ anchor

Rough marking changes estimates but neither loses nor duplicates a position: the concrete coarse ledger contains exactly all non-anchor positions.

def Anderson4D.XYCluster.finAnchorNXCoarseRunsWithPhases {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)) : AnchoredNXParityRuns Nm mu

Split the marked ledger back into two analytic runs at the original left run length. length_markFirstSkippedPairsRough guarantees that no block is lost; in particular the two runs are never concatenated analytically.

Equations

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

def Anderson4D.XYCluster.finAnchorNXCoarseRuns {t : PlaneTree} {m : ℕ} (Nm : t.HeppMarking) (mu : t.Multiplicities) (phase : Bool) (anchor : Fin m) (cls : Fin m → ActiveNXClass Nm mu) (O : Finset (AdjacentIndex m)) : AnchoredNXParityRuns Nm mu

Equations

• Anderson4D.XYCluster.finAnchorNXCoarseRuns Nm mu phase anchor cls O = Anderson4D.XYCluster.finAnchorNXCoarseRunsWithPhases Nm mu phase phase anchor cls O

theorem Anderson4D.XYCluster.finAnchorNXCoarseRunsWithPhases_ledger {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)) : (finAnchorNXCoarseRunsWithPhases Nm mu leftPhase rightPhase anchor cls O).ledger = finAnchorNXCoarseLedgerWithPhases Nm mu leftPhase rightPhase anchor cls O

theorem Anderson4D.XYCluster.finAnchorNXCoarseRuns_ledger {t : PlaneTree} {m : ℕ} (Nm : t.HeppMarking) (mu : t.Multiplicities) (phase : Bool) (anchor : Fin m) (cls : Fin m → ActiveNXClass Nm mu) (O : Finset (AdjacentIndex m)) : (finAnchorNXCoarseRuns Nm mu phase anchor cls O).ledger = finAnchorNXCoarseLedger Nm mu phase anchor cls O

theorem Anderson4D.XYCluster.finAnchorNXCoarseLedgerWithPhases_singleCount_le_four {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)) : nxParitySingleCount (finAnchorNXCoarseLedgerWithPhases Nm mu leftPhase rightPhase anchor cls O) ≤ 4

theorem Anderson4D.XYCluster.finAnchorNXCoarseLedger_singleCount_le_four {t : PlaneTree} {m : ℕ} (Nm : t.HeppMarking) (mu : t.Multiplicities) (phase : Bool) (anchor : Fin m) (cls : Fin m → ActiveNXClass Nm mu) (O : Finset (AdjacentIndex m)) : nxParitySingleCount (finAnchorNXCoarseLedger Nm mu phase anchor cls O) ≤ 4

theorem Anderson4D.XYCluster.finAnchorNXCoarseLedgerWithPhases_roughPairCount_le_three {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)) : nxParityRoughPairCount (finAnchorNXCoarseLedgerWithPhases Nm mu leftPhase rightPhase anchor cls O) ≤ 3

theorem Anderson4D.XYCluster.finAnchorNXCoarseLedger_roughPairCount_le_three {t : PlaneTree} {m : ℕ} (Nm : t.HeppMarking) (mu : t.Multiplicities) (phase : Bool) (anchor : Fin m) (cls : Fin m → ActiveNXClass Nm mu) (O : Finset (AdjacentIndex m)) : nxParityRoughPairCount (finAnchorNXCoarseLedger Nm mu phase anchor cls O) ≤ 3

theorem Anderson4D.XYCluster.finAnchorNXCoarseLedgerWithPhases_lossAtomBudget_le_twenty {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)) : positionLossAtomBudget (nxParitySingleCount (finAnchorNXCoarseLedgerWithPhases Nm mu leftPhase rightPhase anchor cls O)) (nxParityRoughPairCount (finAnchorNXCoarseLedgerWithPhases Nm mu leftPhase rightPhase anchor cls O)) ≤ 20

theorem Anderson4D.XYCluster.finAnchorNXCoarseLedger_lossAtomBudget_le_twenty {t : PlaneTree} {m : ℕ} (Nm : t.HeppMarking) (mu : t.Multiplicities) (phase : Bool) (anchor : Fin m) (cls : Fin m → ActiveNXClass Nm mu) (O : Finset (AdjacentIndex m)) : positionLossAtomBudget (nxParitySingleCount (finAnchorNXCoarseLedger Nm mu phase anchor cls O)) (nxParityRoughPairCount (finAnchorNXCoarseLedger Nm mu phase anchor cls O)) ≤ 20

def Anderson4D.XYCluster.finAnchorPureExceptionalEdgesWithPhases {m : ℕ} (leftPhase rightPhase : Bool) (anchor : Fin m) (O : Finset (AdjacentIndex m)) : Finset (AdjacentIndex m)

The phase-matched exceptional set, defined solely from positions, phases, and O. Intersecting with the genuine carrier is essential: a local block may be incident to an edge belonging to the opposite parity.

Equations

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

def Anderson4D.XYCluster.finAnchorNXExceptionalEdgesWithPhases {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)) : Finset (AdjacentIndex m)

Compatibility wrapper for analytic schedules. The class word is deliberately ignored, so the exception set can be moved outside its sum.

Equations

• Anderson4D.XYCluster.finAnchorNXExceptionalEdgesWithPhases _Nm _mu leftPhase rightPhase anchor _cls O = Anderson4D.XYCluster.finAnchorPureExceptionalEdgesWithPhases leftPhase rightPhase anchor O

theorem Anderson4D.XYCluster.positionPhase_exceptionalEdges_independent_cls {t : PlaneTree} {m : ℕ} (Nm : t.HeppMarking) (mu : t.Multiplicities) (leftPhase rightPhase : Bool) (anchor : Fin m) (cls₁ cls₂ : Fin m → ActiveNXClass Nm mu) (O : Finset (AdjacentIndex m)) : finAnchorNXExceptionalEdgesWithPhases Nm mu leftPhase rightPhase anchor cls₁ O = finAnchorNXExceptionalEdgesWithPhases Nm mu leftPhase rightPhase anchor cls₂ O

theorem Anderson4D.XYCluster.finAnchorNXExceptionalEdgesWithPhases_subset_carrier {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)) : finAnchorNXExceptionalEdgesWithPhases Nm mu leftPhase rightPhase anchor cls O ⊆ finAnchorPositionPhaseCarrierWithPhases leftPhase rightPhase anchor

theorem Anderson4D.XYCluster.finAnchorNX_retained_phaseCarrier_mem_precisePair {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)) (edge : AdjacentIndex m) (hcarrier : edge ∈ finAnchorPositionPhaseCarrierWithPhases leftPhase rightPhase anchor) (hnotExceptional : edge ∉ finAnchorNXExceptionalEdgesWithPhases Nm mu leftPhase rightPhase anchor cls O) : ∃ (i : Fin m) (j : Fin m) (p : NXPairBlock Nm mu), LocatedNXParityBlock.pair i j p ∈ finAnchorNXLocatedCoarseLedgerWithPhases Nm mu leftPhase rightPhase anchor cls O ∧ p.left = cls i ∧ p.right = cls j ∧ (i ∈ leftAnchorPositions anchor ∧ j ∈ leftAnchorPositions anchor ∧ ↑edge = j ∧ ↑j + 1 = ↑i ∧ p.skipRight = decide (edge ∈ O) ∨ i ∈ rightAnchorPositions anchor ∧ j ∈ rightAnchorPositions anchor ∧ ↑edge = i ∧ ↑i + 1 = ↑j ∧ p.skipRight = decide (edge ∈ O))

Hard retained-edge interface for the position layer. Every carrier edge which is not charged to the explicit exceptional set is the internal edge of a concrete precise coarse-ledger pair. The conclusion also restores the exact endpoint classes, the outward side and orientation, and the incoming skip bit used by the local pair estimate.

Existence with full metadata is the interface needed by the analytic glue. Uniqueness is deliberately not asserted here; it can be derived separately from the no-duplication schedule invariant if a later consumer needs it.

theorem Anderson4D.XYCluster.card_finAnchorNXExceptionalEdgesWithPhases_le_twenty {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)) : (finAnchorNXExceptionalEdgesWithPhases Nm mu leftPhase rightPhase anchor cls O).card ≤ 20

Fully concrete version of the paper's “at most 20 skipped gains” audit. Each member of the finset is an original adjacency incident to a single or rough pair block; the cardinality bound follows from 4 single blocks and 3 rough pair blocks, with costs 2 and 4 respectively.

Reindexing the concrete exceptions into the anchored sequence bound

def Anderson4D.XYCluster.adjacentIndexSuccEquiv (n : ℕ) : AdjacentIndex (n + 1) ≃ Fin n

The zero-based paper adjacency indices of a word of length n+1 are canonically Fin n.

Equations

• Anderson4D.XYCluster.adjacentIndexSuccEquiv n = { toFun := fun (j : Anderson4D.AdjacentIndex (n + 1)) => ⟨↑↑j, ⋯⟩, invFun := fun (j : Fin n) => ⟨⟨↑j, ⋯⟩, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

def Anderson4D.XYCluster.reindexAdjacentExceptions {n : ℕ} (E : Finset (AdjacentIndex (n + 1))) : Finset (Fin n)

Reindex an original adjacency exception set for the sequence lemmas.

Equations

• Anderson4D.XYCluster.reindexAdjacentExceptions E = Finset.map (Anderson4D.XYCluster.adjacentIndexSuccEquiv n).toEmbedding E

@[simp]

theorem Anderson4D.XYCluster.card_reindexAdjacentExceptions {n : ℕ} (E : Finset (AdjacentIndex (n + 1))) : (reindexAdjacentExceptions E).card = E.card

def Anderson4D.XYCluster.finAnchorPositionPhaseFinCarrierWithPhases {n : ℕ} (leftPhase rightPhase : Bool) (anchor : Fin (n + 1)) : Finset (Fin n)

The phase carrier in the Fin n coordinates used by sequence bounds.

Equations

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

theorem Anderson4D.XYCluster.finAnchorPositionPhaseFinCarrier_union_flip {n : ℕ} (leftPhase rightPhase : Bool) (anchor : Fin (n + 1)) : finAnchorPositionPhaseFinCarrierWithPhases leftPhase rightPhase anchor ∪ finAnchorPositionPhaseFinCarrierWithPhases (!leftPhase) (!rightPhase) anchor = Finset.univ

theorem Anderson4D.XYCluster.finAnchorPositionPhaseFinCarrier_disjoint_flip {n : ℕ} (leftPhase rightPhase : Bool) (anchor : Fin (n + 1)) : Disjoint (finAnchorPositionPhaseFinCarrierWithPhases leftPhase rightPhase anchor) (finAnchorPositionPhaseFinCarrierWithPhases (!leftPhase) (!rightPhase) anchor)

theorem Anderson4D.XYCluster.anchoredBidirectional_code_sum_le_varyingExceptions (θ : ℝ) (hθ : 0 < θ) (B : ℕ) : ∃ (C : ℝ), 1 ≤ C ∧ ∀ (n ν : ℕ) (e : Fin ν → ℤ), ν ≤ n + 1 → Function.Injective e → ∀ (E : Fin (n + 1) → Finset (Fin n)), (∀ (anchor : Fin (n + 1)), (E anchor).card ≤ B) → ∑ anchor : Fin (n + 1), ∑ w : Fin (n + 1) → Fin ν, anchoredBidirectionalCodeWeight θ e (E anchor) anchor w ≤ C ^ (n + 1)

The anchored sequence estimate remains uniform when the exceptional set depends on the anchor position. This is the form required here because the one-variable boundary blocks move with the minimal-scale position.

def Anderson4D.XYCluster.finAnchorPureExceptionalFinEdgesWithPhases {n : ℕ} (leftPhase rightPhase : Bool) (anchor : Fin (n + 1)) (O : Finset (AdjacentIndex (n + 1))) : Finset (Fin n)

Pure positional exception set in the sequence theorem's coordinates.

Equations

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

def Anderson4D.XYCluster.finAnchorNXExceptionalFinEdgesWithPhases {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))) : Finset (Fin n)

Compatibility wrapper for the analytic class schedule.

Equations

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

theorem Anderson4D.XYCluster.positionPhase_exceptionalFinEdges_independent_cls {t : PlaneTree} {n : ℕ} (Nm : t.HeppMarking) (mu : t.Multiplicities) (leftPhase rightPhase : Bool) (anchor : Fin (n + 1)) (cls₁ cls₂ : Fin (n + 1) → ActiveNXClass Nm mu) (O : Finset (AdjacentIndex (n + 1))) : finAnchorNXExceptionalFinEdgesWithPhases Nm mu leftPhase rightPhase anchor cls₁ O = finAnchorNXExceptionalFinEdgesWithPhases Nm mu leftPhase rightPhase anchor cls₂ O

theorem Anderson4D.XYCluster.finAnchorNXExceptionalFinEdgesWithPhases_subset_carrier {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))) : finAnchorNXExceptionalFinEdgesWithPhases Nm mu leftPhase rightPhase anchor cls O ⊆ finAnchorPositionPhaseFinCarrierWithPhases leftPhase rightPhase anchor

theorem Anderson4D.XYCluster.card_finAnchorNXExceptionalFinEdgesWithPhases_le_twenty {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))) : (finAnchorNXExceptionalFinEdgesWithPhases Nm mu leftPhase rightPhase anchor cls O).card ≤ 20

def Anderson4D.XYCluster.finAnchorNXInterpolatedExceptionalFinEdges {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))) : Finset (Fin n)

Union of a phase's exceptions with those of its genuine flipped phase.

Equations

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

theorem Anderson4D.XYCluster.positionPhase_interpolatedExceptionalFinEdges_independent_cls {t : PlaneTree} {n : ℕ} (Nm : t.HeppMarking) (mu : t.Multiplicities) (leftPhase rightPhase : Bool) (anchor : Fin (n + 1)) (cls₁ cls₂ : Fin (n + 1) → ActiveNXClass Nm mu) (O : Finset (AdjacentIndex (n + 1))) : finAnchorNXInterpolatedExceptionalFinEdges Nm mu leftPhase rightPhase anchor cls₁ O = finAnchorNXInterpolatedExceptionalFinEdges Nm mu leftPhase rightPhase anchor cls₂ O

theorem Anderson4D.XYCluster.card_finAnchorNXInterpolatedExceptionalFinEdges_le_forty {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))) : (finAnchorNXInterpolatedExceptionalFinEdges Nm mu leftPhase rightPhase anchor cls O).card ≤ 40

theorem Anderson4D.XYCluster.finAnchorNX_sqrt_phase_gain_eq_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) : √((∏ j ∈ finAnchorPositionPhaseFinCarrierWithPhases leftPhase rightPhase anchor \ finAnchorNXExceptionalFinEdgesWithPhases Nm mu leftPhase rightPhase anchor cls O, ratioGain (1 / 8) (ratio j)) * ∏ j ∈ finAnchorPositionPhaseFinCarrierWithPhases (!leftPhase) (!rightPhase) anchor \ finAnchorNXExceptionalFinEdgesWithPhases Nm mu (!leftPhase) (!rightPhase) anchor cls O, ratioGain (1 / 8) (ratio j)) = ∏ j ∈ Finset.univ \ finAnchorNXInterpolatedExceptionalFinEdges Nm mu leftPhase rightPhase anchor cls O, ratioGain (1 / 16) (ratio j)

Exact interpolation of the two complementary phase carriers. This is the concrete instantiation of sqrt_even_mul_odd_gain_eq_sixteenth; neither the partition nor exception containment is left as an assumption.

theorem Anderson4D.XYCluster.finAnchorNX_two_phase_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) (x : ℝ) (hx : 0 ≤ x) (hphase : x ≤ ∏ j ∈ finAnchorPositionPhaseFinCarrierWithPhases leftPhase rightPhase anchor \ finAnchorNXExceptionalFinEdgesWithPhases Nm mu leftPhase rightPhase anchor cls O, ratioGain (1 / 8) (ratio j)) (hflip : x ≤ ∏ j ∈ finAnchorPositionPhaseFinCarrierWithPhases (!leftPhase) (!rightPhase) anchor \ finAnchorNXExceptionalFinEdgesWithPhases Nm mu (!leftPhase) (!rightPhase) anchor cls O, ratioGain (1 / 8) (ratio j)) : x ≤ ∏ j ∈ Finset.univ \ finAnchorNXInterpolatedExceptionalFinEdges Nm mu leftPhase rightPhase anchor cls O, ratioGain (1 / 16) (ratio j)

Concrete geometric-mean bridge for the two complementary local estimates. Once the same nonnegative quantity is bounded by each retained 1/8 phase product, it is bounded by the common 1/16 target with the union of their positional exceptions.

theorem Anderson4D.XYCluster.finAnchorNX_sixteenth_positionGain_sum_le : ∃ (C : ℝ), 1 ≤ C ∧ ∀ (n ν : ℕ) (e : Fin ν → ℤ), ν ≤ n + 1 → Function.Injective e → ∀ {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (leftPhase rightPhase : Fin (n + 1) → Bool) (cls : Fin (n + 1) → ActiveNXClass Nm mu) (O : Finset (AdjacentIndex (n + 1))), ∑ anchor : Fin (n + 1), ∑ w : Fin (n + 1) → Fin ν, anchoredBidirectionalCodeWeight (1 / 16) e (finAnchorNXInterpolatedExceptionalFinEdges Nm mu (leftPhase anchor) (rightPhase anchor) anchor cls O) anchor w ≤ C ^ (n + 1)

Paper-facing 1/16 gain bound after even/odd interpolation. The exception set is the union of the two concrete one-parity sets and therefore has budget 40. This exponent is unrelated to the Step-3 outer exponent 1/20.

Shared anchor and used-copy state

def Anderson4D.XYCluster.arrangementAnchorUsedCopies {t : PlaneTree} {mu : t.Multiplicities} {M : ℕ} (σ : Fin M ≃ HeppLabeledCopy mu) (anchor : Fin M) : Finset (HeppLabeledCopy mu)

The used set at the moment the two sides start: it contains the single distinguished labeled copy. Both side eliminations must extend this same set, rather than using two independent copies of the anchor.

Equations

• Anderson4D.XYCluster.arrangementAnchorUsedCopies σ anchor = Anderson4D.XYCluster.arrangementUsedCopies σ {anchor}

@[simp]

theorem Anderson4D.XYCluster.arrangementAnchorUsedCopies_eq_singleton {t : PlaneTree} {mu : t.Multiplicities} {M : ℕ} (σ : Fin M ≃ HeppLabeledCopy mu) (anchor : Fin M) : arrangementAnchorUsedCopies σ anchor = {σ anchor}

theorem Anderson4D.XYCluster.arrangement_nonanchor_mem_conditionedNX {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) {M : ℕ} (σ : Fin M ≃ HeppLabeledCopy mu) (anchor j : Fin M) (hj : j ≠ anchor) (a : NXClass) (ha : singleScaleSigma1 Nm mu (σ j).fst = a) : σ j ∈ conditionedCopiesAtNX Nm mu (arrangementAnchorUsedCopies σ anchor) a

Every non-anchor position is an honest conditioned choice when the shared used set initially contains the anchor.

theorem Anderson4D.XYCluster.arrangement_crossSide_pair_mem_conditionedNX {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) {M : ℕ} (σ : Fin M ≃ HeppLabeledCopy mu) (anchor j k : Fin M) (hj : j ≠ anchor) (hk : k ≠ anchor) (hjk : j ≠ k) (a b : NXClass) (ha : singleScaleSigma1 Nm mu (σ j).fst = a) (hb : singleScaleSigma1 Nm mu (σ k).fst = b) : σ j ∈ conditionedCopiesAtNX Nm mu (arrangementAnchorUsedCopies σ anchor) a ∧ σ k ∈ conditionedCopiesAtNX Nm mu (insert (σ j) (arrangementAnchorUsedCopies σ anchor)) b

Choices on opposite sides of the cut remain distinct after the first one is inserted into the common used set. This is the anchor/cross-side bookkeeping required by the global finite-Fubini step.

theorem Anderson4D.XYCluster.finAnchorNXCoarseRunsWithPhases_sharedAnchor_le_targetProducts : ∃ (C : ℝ), 256 ≤ C ∧ ∀ {t : PlaneTree} {m : ℕ} (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 : ℕ), accumulatedScale Nm mu t.rootV ≤ R → ∀ (leftPhase rightPhase : Bool) (anchor : Fin m) (cls : Fin m → ActiveNXClass Nm mu) (O : Finset (AdjacentIndex m)) (σ : Fin m ≃ HeppLabeledCopy mu), conditionedNXParityChainSum ht hroot Nm mu z hz (↑R) (finAnchorNXCoarseRunsWithPhases Nm mu leftPhase rightPhase anchor cls O).left (arrangementAnchorUsedCopies σ anchor) (labeledCopyPoint z (σ anchor)) ≤ (List.map (fun (p : NXParityBlock Nm mu) => C * nxParityBlockTarget Nm mu (↑R) p) (finAnchorNXCoarseRunsWithPhases Nm mu leftPhase rightPhase anchor cls O).left).prod ∧ conditionedNXParityChainSum ht hroot Nm mu z hz (↑R) (finAnchorNXCoarseRunsWithPhases Nm mu leftPhase rightPhase anchor cls O).right (arrangementAnchorUsedCopies σ anchor) (labeledCopyPoint z (σ anchor)) ≤ (List.map (fun (p : NXParityBlock Nm mu) => C * nxParityBlockTarget Nm mu (↑R) p) (finAnchorNXCoarseRunsWithPhases Nm mu leftPhase rightPhase anchor cls O).right).prod

Both outward analytic runs may be fed to the mixed one-parity local estimate with the same anchored used-copy state and anchored lattice point. The theorem gives separate bounds; their product is obtained through the arrangement/Fubini lemma without duplicating the anchor or introducing an edge between the outer endpoints.

Bidirectional gain interface

noncomputable def Anderson4D.XYCluster.positionCodeGain {ν : ℕ} (e : Fin ν → ℤ) (a b : Fin ν) : ℝ

One dyadic gain on an enumerated class family.

Equations

• Anderson4D.XYCluster.positionCodeGain e a b = min 1 ((2 ^ e b / 2 ^ e a) ^ (1 / 8))

theorem Anderson4D.XYCluster.positionCodeGain_nonneg {ν : ℕ} (e : Fin ν → ℤ) (a b : Fin ν) : 0 ≤ positionCodeGain e a b

def Anderson4D.XYCluster.anchoredSideCodeWord {ν k : ℕ} (anchor : Fin ν) (x : Fin k → Fin ν) : Fin (k + 1) → Fin ν

Gain product on one side, with the side word ordered away from the anchor. For the left side this is the reverse of original word order; for the right side it is the original order.

Equations

• Anderson4D.XYCluster.anchoredSideCodeWord anchor x = Fin.cons anchor x

noncomputable def Anderson4D.XYCluster.anchoredSideCodeGain {ν k : ℕ} (e : Fin ν → ℤ) (anchor : Fin ν) (x : Fin k → Fin ν) : ℝ

Equations

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

theorem Anderson4D.XYCluster.anchoredSideCodeGain_nonneg {ν k : ℕ} (e : Fin ν → ℤ) (anchor : Fin ν) (x : Fin k → Fin ν) : 0 ≤ anchoredSideCodeGain e anchor x

noncomputable def Anderson4D.XYCluster.anchoredSideCodeSum {ν : ℕ} (e : Fin ν → ℤ) (k : ℕ) (anchor : Fin ν) : ℝ

Sum over all class words on one side of a fixed anchor class.

Equations

• Anderson4D.XYCluster.anchoredSideCodeSum e k anchor = ∑ x : Fin k → Fin ν, Anderson4D.XYCluster.anchoredSideCodeGain e anchor x

theorem Anderson4D.XYCluster.anchoredSideCodeSum_nonneg {ν : ℕ} (e : Fin ν → ℤ) (k : ℕ) (anchor : Fin ν) : 0 ≤ anchoredSideCodeSum e k anchor

noncomputable def Anderson4D.XYCluster.anchoredBidirectionalCodeSum {ν : ℕ} (e : Fin ν → ℤ) (leftLength rightLength : ℕ) : ℝ

The gain sum prescribed by the paper's "going left and right separately": both words are ordered away from the common anchor. Thus the left product uses original-order reverse gains and the right product uses original-order forward gains.

Equations

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

theorem Anderson4D.XYCluster.anchoredBidirectionalCodeSum_le_of_side_bounds {ν : ℕ} (e : Fin ν → ℤ) (leftLength rightLength M : ℕ) (hν : ν ≤ M) (C : ℝ) (hC : 0 ≤ C) (hleft : ∀ (anchor : Fin ν), anchoredSideCodeSum e leftLength anchor ≤ C ^ M) (hright : ∀ (anchor : Fin ν), anchoredSideCodeSum e rightLength anchor ≤ C ^ M) : anchoredBidirectionalCodeSum e leftLength rightLength ≤ (2 * C ^ 2) ^ M

Once the two padded one-sided applications of Lemma 5.13 are available, the sum over the at-most-M anchor classes costs only another 2^M. This is the global replacement for the invalid pointwise comparison between forward and reverse gains.

Exact cross-module boundary

This file now closes the position layer itself:

• independent left/right phases, the concrete cut at every anchor, and exact coverage of all non-anchor positions;
• position-preserving rough marking, at most four single blocks and three rough pairs, and the exact original adjacency edges affected by them;
• at most 20 exceptional gains per parity and at most 40 after even/odd interpolation;
• exact conversion of heterogeneous rough targets to the common (5.87) baseline, with all sqrt Y and Xi⁻¹ atoms exposed and the resulting polynomial loss absorbed exponentially;
• the shared anchored used-copy state and separate local target-product bounds for the two outward analytic runs;
• the padded bidirectional sequence estimate, specialized to the concrete anchor-dependent exception sets at exponent 1/8, and to their even/odd union at exponent 1/16.

SingleScaleAnchorGlue and the final P-5.10 assembly use these positional facts to:

• identify (or nonnegatively dominate) the fixed-anchor arrangement fiber by the two outward conditioned eliminations while threading one genuinely shared used set through both sides;
• reindex the products of nxParityBlockTarget into the final common (5.87) product, combine the even/odd estimates by geometric mean, and connect the active P word to the code-word sequence sum;
• combine the explicit rough scale gains with R^(2s) and (N_root/R)^(min(2s,3)), then reinsert the finite-Fubini and factorial ledgers at the frozen proposition boundary.

The statement-weight-to-local-kernel inequalities in the first item live in SingleScaleWeightBridge. No pointwise comparison between original forward and traversal-forward gains is valid or assumed; the left run is handled globally by reversal, as in SingleScaleAnchoredSequence.