The residual interval chain in the doubled moment reduction

This file packages the fully paired proper subintervals which remain after the two within-half extraction loops in paper §4.2 Step 2. CrossCutIntervals.lean proves that distinct residual intervals are strictly nested. Here they are collected into a finite set and a canonical inside-to-outside list, preparing the successive collapse in Step 3.

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

All relative fully paired intervals of the doubled residual carrier.

Equations

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

@[simp]

theorem Anderson4D.mem_momentResidualFullyPairedIntervals {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} {p : Fin (2 * m) × Fin (2 * m)} : p ∈ momentResidualFullyPairedIntervals κp κm π ↔ IsRelFullyPaired (momentCombinedPairing κp κm π) (momentResidualActive κp κm) p.1 p.2

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

The proper residual intervals reduced before the final primitive block. Properness is relative to the sparse active carrier, before the paper renames its elements consecutively.

Equations

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

@[simp]

theorem Anderson4D.mem_momentResidualProperIntervals {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} {p : Fin (2 * m) × Fin (2 * m)} : p ∈ momentResidualProperIntervals κp κm π ↔ IsRelFullyPaired (momentCombinedPairing κp κm π) (momentResidualActive κp κm) p.1 p.2 ∧ relIcc (momentResidualActive κp κm) p.1 p.2 ≠ momentResidualActive κp κm

theorem Anderson4D.momentResidualProperInterval_straddlesCut {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} {p : Fin (2 * m) × Fin (2 * m)} (hp : p ∈ momentResidualProperIntervals κp κm π) : IntervalStraddlesCut m p

Every proper residual interval straddles the central cut.

theorem Anderson4D.momentResidualProperIntervals_strictlyNested {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} {p q : Fin (2 * m) × Fin (2 * m)} (hp : p ∈ momentResidualProperIntervals κp κm π) (hq : q ∈ momentResidualProperIntervals κp κm π) (hpq : p ≠ q) : p.1 < q.1 ∧ q.2 < p.2 ∨ q.1 < p.1 ∧ p.2 < q.2

Distinct proper residual intervals are strictly nested at both endpoints.

def Anderson4D.momentResidualIntervalChain {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) : List (Fin (2 * m) × Fin (2 * m))

Canonical inside-to-outside ordering. The ordinary lexicographic sort lists the strictly nested intervals outside-to-inside because left endpoints increase inward, so the list is reversed.

Equations

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

@[simp]

theorem Anderson4D.mem_momentResidualIntervalChain {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} {p : Fin (2 * m) × Fin (2 * m)} : p ∈ momentResidualIntervalChain κp κm π ↔ p ∈ momentResidualProperIntervals κp κm π

theorem Anderson4D.momentResidualIntervalChain_nodup {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) : (momentResidualIntervalChain κp κm π).Nodup

theorem Anderson4D.momentResidualIntervalChain_pairwise_laterContains {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) : List.Pairwise LaterCrossCutIntervalContains (momentResidualIntervalChain κp κm π)

The canonical chain is ordered exactly as the successive Step 3 collapses: every later interval strictly contains every earlier one.

Closed shells between successive residual intervals

def Anderson4D.residualIntervalTrace {n : ℕ} (active : Finset (Fin n)) (p : Fin n × Fin n) : Finset (Fin n)

The active trace of an endpoint interval.

Equations

• Anderson4D.residualIntervalTrace active p = Anderson4D.relIcc active p.1 p.2

theorem Anderson4D.residualIntervalTrace_subset {n : ℕ} {active : Finset (Fin n)} {p q : Fin n × Fin n} (h : LaterCrossCutIntervalContains p q) : residualIntervalTrace active p ⊆ residualIntervalTrace active q

def Anderson4D.residualIntervalShell {n : ℕ} (active : Finset (Fin n)) (p q : Fin n × Fin n) : Finset (Fin n)

The new closed shell exposed when the collapse expands from an inner interval p to the next outer interval q.

Equations

• Anderson4D.residualIntervalShell active p q = Anderson4D.residualIntervalTrace active q \ Anderson4D.residualIntervalTrace active p

theorem Anderson4D.residualIntervalShell_isFullyPairedOn {n : ℕ} {κ : PartialPairing (Fin n)} {active : Finset (Fin n)} {p q : Fin n × Fin n} (hp : IsRelFullyPaired κ active p.1 p.2) (hq : IsRelFullyPaired κ active q.1 q.2) : IsFullyPairedOn κ (residualIntervalShell active p q)

A shell between two fully paired intervals is again fully paired.

theorem Anderson4D.residualIntervalShell_nonempty {n : ℕ} {κ : PartialPairing (Fin n)} {active : Finset (Fin n)} {p q : Fin n × Fin n} (_hp : IsRelFullyPaired κ active p.1 p.2) (hq : IsRelFullyPaired κ active q.1 q.2) (h : LaterCrossCutIntervalContains p q) : (residualIntervalShell active p q).Nonempty

Strict containment makes every successive shell nonempty.

theorem Anderson4D.residualIntervalTrace_union_shell {n : ℕ} {active : Finset (Fin n)} {p q : Fin n × Fin n} (h : LaterCrossCutIntervalContains p q) : residualIntervalTrace active p ∪ residualIntervalShell active p q = residualIntervalTrace active q

An inner trace together with its next shell is exactly the outer trace.

def Anderson4D.residualIntervalExterior {n : ℕ} (active : Finset (Fin n)) (p : Fin n × Fin n) : Finset (Fin n)

The exterior remaining after the outermost proper interval.

Equations

• Anderson4D.residualIntervalExterior active p = active \ Anderson4D.residualIntervalTrace active p

theorem Anderson4D.momentResidualIntervalExterior_isFullyPairedOn {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} {p : Fin (2 * m) × Fin (2 * m)} (hp : IsRelFullyPaired (momentCombinedPairing κp κm π) (momentResidualActive κp κm) p.1 p.2) : IsFullyPairedOn (momentCombinedPairing κp κm π) (residualIntervalExterior (momentResidualActive κp κm) p)

The exterior of a fully paired residual interval is closed and has no singles because the whole residual carrier is fully paired.

theorem Anderson4D.residualIntervalTrace_union_exterior {n : ℕ} (active : Finset (Fin n)) (p : Fin n × Fin n) : residualIntervalTrace active p ∪ residualIntervalExterior active p = active

An interval trace and its exterior exactly partition the residual carrier.