The canonical nested cross-residual state for R-324

After both signed within-half schedules have been removed, paper §4.2 Step 3 does not use an arbitrary block order. Every remaining fully paired proper interval crosses the central cut, and the literal reduction order is the inside-to-outside chain

[a₁,b₁] ⊂ ... ⊂ [aₜ,bₜ].

This module turns the already-proved trace/shell/exterior decomposition into a proof-relevant cross-block schedule. Every nonempty scheduled block contains a left and a right coordinate, so it has a canonical central gap. That gap is the location of the numerator in (4.20); after one inserted collapse the gap moves to the next outer shell.

Cross-cut carriers and their canonical gap

def Anderson4D.R324CrossCutCarrier (m : ℕ) (B : Finset (Fin (2 * m))) : Prop

A sparse doubled carrier genuinely crosses the cut between the two copies.

Equations

• Anderson4D.R324CrossCutCarrier m B = ∃ left ∈ B, ∃ right ∈ B, ↑left < m ∧ m ≤ ↑right

def Anderson4D.r324CrossLeftPart (m : ℕ) (B : Finset (Fin (2 * m))) : Finset (Fin (2 * m))

The left component of a doubled sparse carrier.

Equations

• Anderson4D.r324CrossLeftPart m B = {i ∈ B | ↑i < m}

def Anderson4D.r324CrossRightPart (m : ℕ) (B : Finset (Fin (2 * m))) : Finset (Fin (2 * m))

The right component of a doubled sparse carrier.

Equations

• Anderson4D.r324CrossRightPart m B = {i ∈ B | m ≤ ↑i}

theorem Anderson4D.r324CrossCutCarrier_iff_parts_nonempty {m : ℕ} {B : Finset (Fin (2 * m))} : R324CrossCutCarrier m B ↔ (r324CrossLeftPart m B).Nonempty ∧ (r324CrossRightPart m B).Nonempty

def Anderson4D.r324CrossGapLeft {m : ℕ} (B : Finset (Fin (2 * m))) (hcross : R324CrossCutCarrier m B) : Fin (2 * m)

The last surviving coordinate on the left side of a cross carrier.

Equations

• Anderson4D.r324CrossGapLeft B hcross = (Anderson4D.r324CrossLeftPart m B).max' ⋯

def Anderson4D.r324CrossGapRight {m : ℕ} (B : Finset (Fin (2 * m))) (hcross : R324CrossCutCarrier m B) : Fin (2 * m)

The first surviving coordinate on the right side of a cross carrier.

Equations

• Anderson4D.r324CrossGapRight B hcross = (Anderson4D.r324CrossRightPart m B).min' ⋯

theorem Anderson4D.r324CrossGapLeft_mem {m : ℕ} (B : Finset (Fin (2 * m))) (hcross : R324CrossCutCarrier m B) : r324CrossGapLeft B hcross ∈ B

theorem Anderson4D.r324CrossGapRight_mem {m : ℕ} (B : Finset (Fin (2 * m))) (hcross : R324CrossCutCarrier m B) : r324CrossGapRight B hcross ∈ B

theorem Anderson4D.r324CrossGapLeft_lt_cut {m : ℕ} (B : Finset (Fin (2 * m))) (hcross : R324CrossCutCarrier m B) : ↑(r324CrossGapLeft B hcross) < m

theorem Anderson4D.r324CrossGapRight_ge_cut {m : ℕ} (B : Finset (Fin (2 * m))) (hcross : R324CrossCutCarrier m B) : m ≤ ↑(r324CrossGapRight B hcross)

theorem Anderson4D.r324CrossGapLeft_lt_right {m : ℕ} (B : Finset (Fin (2 * m))) (hcross : R324CrossCutCarrier m B) : r324CrossGapLeft B hcross < r324CrossGapRight B hcross

A generic min/max interval on a closed sparse carrier

theorem Anderson4D.isRelFullyPaired_min'_max' {n : ℕ} {κ : PartialPairing (Fin n)} {B : Finset (Fin n)} (hne : B.Nonempty) (hfull : IsFullyPairedOn κ B) : IsRelFullyPaired κ B (B.min' hne) (B.max' hne)

On a nonempty closed sparse carrier, its minimum and maximum expose the whole carrier as one relative fully paired interval.

Every literal residual block crosses the cut

theorem Anderson4D.momentResidualCollapseBlocks_forall_crossCut_of_nonempty {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) : List.Forall (fun (B : Finset (Fin (2 * m))) => B.Nonempty → R324CrossCutCarrier m B) (momentResidualCollapseBlocks κp κm π)

Every nonempty member of the literal trace/shell/exterior schedule crosses the central cut.

theorem Anderson4D.crossCut_of_mem_nonemptyMomentResidualCollapseBlocks {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (B : Finset (Fin (2 * m))) (hB : B ∈ nonemptyMomentResidualCollapseBlocks κp κm π) : R324CrossCutCarrier m B

The proof-relevant canonical nested schedule

structure Anderson4D.R324NestedCrossBlock {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) : Type

One actual nonempty cross-residual block, with its literal schedule membership and canonical central gap certificate.

• carrier : Finset (Fin (2 * m))
• mem_schedule : self.carrier ∈ nonemptyMomentResidualCollapseBlocks κp κm π
• crossCut : R324CrossCutCarrier m self.carrier

def Anderson4D.R324NestedCrossBlock.leftGap {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (block : R324NestedCrossBlock κp κm π) : Fin (2 * m)

Equations

• block.leftGap = Anderson4D.r324CrossGapLeft block.carrier ⋯

def Anderson4D.R324NestedCrossBlock.rightGap {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (block : R324NestedCrossBlock κp κm π) : Fin (2 * m)

Equations

• block.rightGap = Anderson4D.r324CrossGapRight block.carrier ⋯

theorem Anderson4D.R324NestedCrossBlock.leftGap_mem {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (block : R324NestedCrossBlock κp κm π) : block.leftGap ∈ block.carrier

theorem Anderson4D.R324NestedCrossBlock.rightGap_mem {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (block : R324NestedCrossBlock κp κm π) : block.rightGap ∈ block.carrier

theorem Anderson4D.R324NestedCrossBlock.leftGap_lt_rightGap {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (block : R324NestedCrossBlock κp κm π) : block.leftGap < block.rightGap

theorem Anderson4D.R324NestedCrossBlock.one_le_order {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (block : R324NestedCrossBlock κp κm π) : 1 ≤ residualBlockOrder block.carrier

def Anderson4D.r324NestedCrossSchedule {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) : List (R324NestedCrossBlock κp κm π)

The literal inside-to-outside nonempty residual schedule, enriched by its canonical central gap at every block.

Equations

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

@[simp]

theorem Anderson4D.r324NestedCrossSchedule_carriers {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) : List.map R324NestedCrossBlock.carrier (r324NestedCrossSchedule κp κm π) = nonemptyMomentResidualCollapseBlocks κp κm π

theorem Anderson4D.r324NestedCrossSchedule_sum_orders {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) : (List.map (fun (block : R324NestedCrossBlock κp κm π) => residualBlockOrder block.carrier) (r324NestedCrossSchedule κp κm π)).sum = (List.map residualBlockOrder (nonemptyMomentResidualCollapseBlocks κp κm π)).sum

Enriching the residual schedule does not alter its exact perturbative order ledger.

theorem Anderson4D.r324NestedCrossSchedule_pairwise_disjoint {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) : List.Pairwise (fun (left right : R324NestedCrossBlock κp κm π) => Disjoint left.carrier right.carrier) (r324NestedCrossSchedule κp κm π)

Genuine prefixes of the nested schedule

structure Anderson4D.R324NestedCrossResidualPrefix {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) : Type

A processed prefix and literal remaining suffix of the canonical inside-to-outside cross schedule.

• processed : List (R324NestedCrossBlock κp κm π)
• remaining : List (R324NestedCrossBlock κp κm π)
• schedule_eq : r324NestedCrossSchedule κp κm π = self.processed ++ self.remaining

def Anderson4D.R324NestedCrossResidualPrefix.initial {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) : R324NestedCrossResidualPrefix κp κm π

The cross state before the innermost residual block is removed.

Equations

• Anderson4D.R324NestedCrossResidualPrefix.initial κp κm π = { processed := [], remaining := Anderson4D.r324NestedCrossSchedule κp κm π, schedule_eq := ⋯ }

def Anderson4D.R324NestedCrossResidualPrefix.activeCarrier {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (res : R324NestedCrossResidualPrefix κp κm π) : Finset (Fin (2 * m))

The union of all variables not yet removed.

Equations

• res.activeCarrier = Anderson4D.finsetUnionList (List.map Anderson4D.R324NestedCrossBlock.carrier res.remaining)

def Anderson4D.R324NestedCrossResidualPrefix.processedOrder {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (res : R324NestedCrossResidualPrefix κp κm π) : ℕ

Total perturbative order already removed.

Equations

• res.processedOrder = (List.map (fun (block : Anderson4D.R324NestedCrossBlock κp κm π) => Anderson4D.residualBlockOrder block.carrier) res.processed).sum

def Anderson4D.R324NestedCrossResidualPrefix.remainingOrder {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (res : R324NestedCrossResidualPrefix κp κm π) : ℕ

Total perturbative order still carried by the cross suffix.

Equations

• res.remainingOrder = (List.map (fun (block : Anderson4D.R324NestedCrossBlock κp κm π) => Anderson4D.residualBlockOrder block.carrier) res.remaining).sum

theorem Anderson4D.R324NestedCrossResidualPrefix.processedOrder_add_remainingOrder {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (res : R324NestedCrossResidualPrefix κp κm π) : res.processedOrder + res.remainingOrder = (List.map residualBlockOrder (nonemptyMomentResidualCollapseBlocks κp κm π)).sum

def Anderson4D.R324NestedCrossResidualPrefix.afterHead {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (res : R324NestedCrossResidualPrefix κp κm π) (head : R324NestedCrossBlock κp κm π) (tail : List (R324NestedCrossBlock κp κm π)) (hremaining : res.remaining = head :: tail) : R324NestedCrossResidualPrefix κp κm π

Delete the literal innermost remaining block and expose the next outer shell (or final exterior).

Equations

• res.afterHead head tail hremaining = { processed := res.processed ++ [head], remaining := tail, schedule_eq := ⋯ }

@[simp]

theorem Anderson4D.R324NestedCrossResidualPrefix.afterHead_remaining {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (res : R324NestedCrossResidualPrefix κp κm π) (head : R324NestedCrossBlock κp κm π) (tail : List (R324NestedCrossBlock κp κm π)) (hremaining : res.remaining = head :: tail) : (res.afterHead head tail hremaining).remaining = tail

theorem Anderson4D.R324NestedCrossResidualPrefix.activeCarrier_head {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (res : R324NestedCrossResidualPrefix κp κm π) (head : R324NestedCrossBlock κp κm π) (tail : List (R324NestedCrossBlock κp κm π)) (hremaining : res.remaining = head :: tail) : res.activeCarrier = head.carrier ∪ (res.afterHead head tail hremaining).activeCarrier

theorem Anderson4D.R324NestedCrossResidualPrefix.head_disjoint_afterHead_activeCarrier {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (res : R324NestedCrossResidualPrefix κp κm π) (head : R324NestedCrossBlock κp κm π) (tail : List (R324NestedCrossBlock κp κm π)) (hremaining : res.remaining = head :: tail) : Disjoint head.carrier (res.afterHead head tail hremaining).activeCarrier

The block removed at one step is disjoint from the whole later cross-residual carrier.

theorem Anderson4D.R324NestedCrossResidualPrefix.remainingOrder_head {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (res : R324NestedCrossResidualPrefix κp κm π) (head : R324NestedCrossBlock κp κm π) (tail : List (R324NestedCrossBlock κp κm π)) (hremaining : res.remaining = head :: tail) : res.remainingOrder = residualBlockOrder head.carrier + (res.afterHead head tail hremaining).remainingOrder

The moving (4.20) numerator

noncomputable def Anderson4D.R324NestedCrossBlock.centralGapNumerator {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (block : R324NestedCrossBlock κp κm π) (v : Fin (2 * m) → T4) : ℝ

The central numerator attached to the current cross block.

Equations

• block.centralGapNumerator v = Anderson4D.torusDistSq (v block.leftGap - v block.rightGap)

theorem Anderson4D.R324NestedCrossBlock.centralGapNumerator_nonneg {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (block : R324NestedCrossBlock κp κm π) (v : Fin (2 * m) → T4) : 0 ≤ block.centralGapNumerator v

theorem Anderson4D.R324NestedCrossBlock.centralGapCancellation_le_one {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (block : R324NestedCrossBlock κp κm π) (v : Fin (2 * m) → T4) : block.centralGapNumerator v * invSqKer (v block.leftGap - v block.rightGap) ≤ 1

The paper's central gap cancellation is pointwise bounded by one. Equality is intentionally not asserted at the totalized diagonal.

theorem Anderson4D.R324NestedCrossBlock.centralGapCancellation_eq_one_of_ne {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (block : R324NestedCrossBlock κp κm π) (v : Fin (2 * m) → T4) (hne : v block.leftGap ≠ v block.rightGap) : block.centralGapNumerator v * invSqKer (v block.leftGap - v block.rightGap) = 1

Off the null diagonal, the central inverse-square factor and the (4.20) numerator cancel exactly.

theorem Anderson4D.R324NestedCrossBlock.ae_centralGapCancellation_eq_one {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (block : R324NestedCrossBlock κp κm π) : ∀ᵐ (v : Fin (2 * m) → T4) ∂MeasureTheory.Measure.pi fun (x : Fin (2 * m)) => paperMeasure, block.centralGapNumerator v * invSqKer (v block.leftGap - v block.rightGap) = 1

Under the genuine product measure, the paper's moving central gap cancels exactly almost everywhere.