Cross-cut interval geometry for the doubled moment reduction

After the within-half intervals have been removed in paper §4.2 Step 2, every proper fully paired interval of the residual doubled pairing straddles the central cut. This file isolates the order-theoretic part of Step 3: laminar intervals which straddle one cut cannot be disjoint, and the extraction order therefore lists them from inside to outside.

def Anderson4D.IntervalStraddlesCut {n : ℕ} (cut : ℕ) (p : Fin n × Fin n) : Prop

An interval on Fin n straddles the cut immediately before cut when its left endpoint lies below cut and its right endpoint does not.

Equations

• Anderson4D.IntervalStraddlesCut cut p = (↑p.1 < cut ∧ cut ≤ ↑p.2)

def Anderson4D.LaterCrossCutIntervalContains {n : ℕ} (p q : Fin n × Fin n) : Prop

For two cross-cut intervals, the second one strictly contains the first. This is the direction forced by the paper's extraction order.

Equations

• Anderson4D.LaterCrossCutIntervalContains p q = (q.1 < p.1 ∧ p.2 < q.2)

Geometry of the doubled residual carrier

@[simp]

theorem Anderson4D.leftMomentIndex_mem_momentResidualActive_iff {m : ℕ} (κp κm : PartialPairing (Fin m)) (i : Fin m) : leftMomentIndex i ∈ momentResidualActive κp κm ↔ i ∈ finalActive κp

@[simp]

theorem Anderson4D.rightMomentIndex_mem_momentResidualActive_iff {m : ℕ} (κp κm : PartialPairing (Fin m)) (j : Fin m) : rightMomentIndex j ∈ momentResidualActive κp κm ↔ j ∈ finalActive κm

theorem Anderson4D.exists_leftMomentIndex_of_mem_momentResidualActive {m : ℕ} {κp κm : PartialPairing (Fin m)} {x : Fin (2 * m)} (hx : x ∈ momentResidualActive κp κm) (hxLeft : ↑x < m) : ∃ i ∈ finalActive κp, x = leftMomentIndex i

A residual index below the central cut comes uniquely from the left copy.

theorem Anderson4D.exists_rightMomentIndex_of_mem_momentResidualActive {m : ℕ} {κp κm : PartialPairing (Fin m)} {x : Fin (2 * m)} (hx : x ∈ momentResidualActive κp κm) (hxRight : m ≤ ↑x) : ∃ j ∈ finalActive κm, x = rightMomentIndex j

A residual index at or above the central cut comes uniquely from the right copy.

theorem Anderson4D.relIcc_momentResidualActive_left {m : ℕ} (κp κm : PartialPairing (Fin m)) (a b : Fin m) : relIcc (momentResidualActive κp κm) (leftMomentIndex a) (leftMomentIndex b) = relIcc (Finset.image leftMomentIndex (finalActive κp)) (leftMomentIndex a) (leftMomentIndex b)

If both endpoints lie below the cut, the relative interval in the doubled residual carrier is exactly the corresponding left-image relative interval.

theorem Anderson4D.relIcc_momentResidualActive_right {m : ℕ} (κp κm : PartialPairing (Fin m)) (a b : Fin m) : relIcc (momentResidualActive κp κm) (rightMomentIndex a) (rightMomentIndex b) = relIcc (Finset.image rightMomentIndex (finalActive κm)) (rightMomentIndex a) (rightMomentIndex b)

Right-copy counterpart of relIcc_momentResidualActive_left.

Every residual fully paired interval crosses the cut

theorem Anderson4D.not_isRelFullyPaired_momentResidualActive_left {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (a b : Fin m) : ¬IsRelFullyPaired (momentCombinedPairing κp κm π) (momentResidualActive κp κm) (leftMomentIndex a) (leftMomentIndex b)

No relative fully paired interval of the doubled residual carrier can have both endpoints in the left copy: reflection would contradict terminality of finalActive κp.

theorem Anderson4D.not_isRelFullyPaired_momentResidualActive_right {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (a b : Fin m) : ¬IsRelFullyPaired (momentCombinedPairing κp κm π) (momentResidualActive κp κm) (rightMomentIndex a) (rightMomentIndex b)

Right-copy counterpart of not_isRelFullyPaired_momentResidualActive_left.

theorem Anderson4D.IsRelFullyPaired.momentResidualActive_straddlesCut {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} {a b : Fin (2 * m)} (h : IsRelFullyPaired (momentCombinedPairing κp κm π) (momentResidualActive κp κm) a b) : IntervalStraddlesCut m (a, b)

Every relative fully paired interval of the residual doubled carrier straddles its central cut. This is the precise combinatorial assertion at the start of paper §4.2 Step 3.

Nesting of residual fully paired intervals

theorem Anderson4D.exists_left_fullyPairedInterval_of_crossing {n : ℕ} {κ : PartialPairing (Fin n)} {active : Finset (Fin n)} {a b c d : Fin n} (hI : IsRelFullyPaired κ active a b) (hJ : IsRelFullyPaired κ active c d) (hac : a < c) (_hcb : c ≤ b) (hbd : b ≤ d) : ∃ (e : Fin n), IsRelFullyPaired κ active a e ∧ e < c

When two fully paired relative intervals cross as a < c ≤ b < d, their left difference is a nonempty fully paired relative interval ending strictly before c.

def Anderson4D.ResidualIntervalsWeaklyNested {n : ℕ} (p q : Fin n × Fin n) : Prop

Weak nesting relation, allowing equality of one endpoint.

Equations

• Anderson4D.ResidualIntervalsWeaklyNested p q = (p.1 ≤ q.1 ∧ q.2 ≤ p.2 ∨ q.1 ≤ p.1 ∧ p.2 ≤ q.2)

theorem Anderson4D.IsRelFullyPaired.momentResidualActive_weaklyNested {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} {a b c d : Fin (2 * m)} (hI : IsRelFullyPaired (momentCombinedPairing κp κm π) (momentResidualActive κp κm) a b) (hJ : IsRelFullyPaired (momentCombinedPairing κp κm π) (momentResidualActive κp κm) c d) : ResidualIntervalsWeaklyNested (a, b) (c, d)

Any two fully paired intervals of the doubled residual carrier are weakly nested. A crossing would produce, by set difference, a fully paired interval wholly to the left of the central cut.

theorem Anderson4D.exists_right_fullyPairedInterval_of_same_left {n : ℕ} {κ : PartialPairing (Fin n)} {active : Finset (Fin n)} {a b d : Fin n} (hI : IsRelFullyPaired κ active a b) (hJ : IsRelFullyPaired κ active a d) (hbd : b < d) : ∃ (e : Fin n), IsRelFullyPaired κ active e d ∧ b < e

If two fully paired relative intervals share their left endpoint and the second extends farther right, their right difference is a nonempty fully paired relative interval starting strictly after the first one.

theorem Anderson4D.IsRelFullyPaired.momentResidualActive_strictlyNested {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} {a b c d : Fin (2 * m)} (hI : IsRelFullyPaired (momentCombinedPairing κp κm π) (momentResidualActive κp κm) a b) (hJ : IsRelFullyPaired (momentCombinedPairing κp κm π) (momentResidualActive κp κm) c d) (hne : (a, b) ≠ (c, d)) : a < c ∧ d < b ∨ c < a ∧ b < d

Distinct fully paired intervals of the doubled residual carrier are strictly nested at both endpoints, exactly the chain aₜ < ⋯ < a₁ ≤ cut < b₁ < ⋯ < bₜ in paper §4.2 Step 3.

theorem Anderson4D.ReductionIntervalsLaminar.nested_of_straddlesCut {n cut : ℕ} {p q : Fin n × Fin n} (hlam : ReductionIntervalsLaminar p q) (hp : IntervalStraddlesCut cut p) (hq : IntervalStraddlesCut cut q) : p.1 < q.1 ∧ q.2 < p.2 ∨ q.1 < p.1 ∧ p.2 < q.2

Two laminar intervals which straddle the same cut are nested.

theorem Anderson4D.EarlierReductionIntervalCompatible.laterContains_of_straddlesCut {n cut : ℕ} {p q : Fin n × Fin n} (hcompat : EarlierReductionIntervalCompatible p q) (hp : IntervalStraddlesCut cut p) (hq : IntervalStraddlesCut cut q) : LaterCrossCutIntervalContains p q

Directional extraction compatibility becomes strict containment once both intervals straddle the same cut.

theorem Anderson4D.List.Pairwise.laterCrossCutIntervalContains {n cut : ℕ} {l : List (Fin n × Fin n)} (hcompat : List.Pairwise EarlierReductionIntervalCompatible l) (hcut : ∀ p ∈ l, IntervalStraddlesCut cut p) : List.Pairwise LaterCrossCutIntervalContains l

A list whose intervals are compatible in extraction order and all straddle one cut is ordered by strict containment from inside to outside.

theorem Anderson4D.extract_pairwise_laterCrossCutIntervalContains {n cut : ℕ} (κ : PartialPairing (Fin n)) (hcut : ∀ p ∈ extract κ, IntervalStraddlesCut cut p) : List.Pairwise LaterCrossCutIntervalContains (extract κ)

If all intervals selected from a pairing straddle a fixed cut, then the actual Definition 3.1 extraction order is strictly inside-to-outside. This is the order pattern a₁ > ⋯ > aₙ and b₁ < ⋯ < bₙ used in paper §4.2 Step 3.