Exact block decomposition for the residual R-324 collapse

For a nested inside-to-outside interval chain, the collapse blocks are:

• the innermost interval trace;
• the closed shell between every two successive traces;
• the exterior of the outermost trace.

If the chain is empty, the whole residual carrier is the sole block. This file proves that these blocks cover the residual carrier exactly and that every block is fully paired by the combined contraction pairing. It is the finite-carrier decomposition used before applying the primitive analytic estimate successively in paper §4.2 Step 3.

def Anderson4D.nestedResidualShells {n : ℕ} (active : Finset (Fin n)) (previous : Fin n × Fin n) : List (Fin n × Fin n) → List (Finset (Fin n))

Shells after a current inner trace, ending with the exterior of the last outer trace.

Equations

• Anderson4D.nestedResidualShells active previous [] = [Anderson4D.residualIntervalExterior active previous]
• Anderson4D.nestedResidualShells active previous (next :: rest) = Anderson4D.residualIntervalShell active previous next :: Anderson4D.nestedResidualShells active next rest

def Anderson4D.residualCollapseBlocks {n : ℕ} (active : Finset (Fin n)) : List (Fin n × Fin n) → List (Finset (Fin n))

Complete block list associated with an inside-to-outside chain.

Equations

• Anderson4D.residualCollapseBlocks active [] = [active]
• Anderson4D.residualCollapseBlocks active (next :: rest) = Anderson4D.residualIntervalTrace active next :: Anderson4D.nestedResidualShells active next rest

def Anderson4D.finsetUnionList {α : Type u_1} [DecidableEq α] : List (Finset α) → Finset α

Union of a finite list of finite carriers.

Equations

• Anderson4D.finsetUnionList [] = ∅
• Anderson4D.finsetUnionList (s :: ss) = s ∪ Anderson4D.finsetUnionList ss

def Anderson4D.IsRelPrimitiveOn {n : ℕ} (κ : PartialPairing (Fin n)) (active : Finset (Fin n)) : Prop

Relative primitivity on a sparse carrier: every relative fully paired interval is the whole carrier. After order-preserving renaming this is exactly paper Definition 2.3.

Equations

• Anderson4D.IsRelPrimitiveOn κ active = ∀ (a b : Fin n), Anderson4D.IsRelFullyPaired κ active a b → Anderson4D.relIcc active a b = active

theorem Anderson4D.relIcc_residualIntervalTrace {n : ℕ} {active : Finset (Fin n)} {p : Fin n × Fin n} {a b : Fin n} (ha : a ∈ residualIntervalTrace active p) (hb : b ∈ residualIntervalTrace active p) : relIcc (residualIntervalTrace active p) a b = relIcc active a b

Restricting twice to nested endpoint bounds does not change a relative interval whose endpoints already belong to the outer trace.

theorem Anderson4D.momentResidualActive_isRelPrimitiveOn_of_chain_eq_nil {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (hchain : momentResidualIntervalChain κp κm π = []) : IsRelPrimitiveOn (momentCombinedPairing κp κm π) (momentResidualActive κp κm)

If the canonical residual chain is empty, the whole residual carrier is already primitive.

theorem Anderson4D.residualIntervalTrace_head_isRelPrimitiveOn {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (first : Fin (2 * m) × Fin (2 * m)) (rest : List (Fin (2 * m) × Fin (2 * m))) (hchain : momentResidualIntervalChain κp κm π = first :: rest) : IsRelPrimitiveOn (momentCombinedPairing κp κm π) (residualIntervalTrace (momentResidualActive κp κm) first)

The first trace of the canonical inside-to-outside residual chain is primitive. Any proper subinterval would itself occur in the chain before the head, contradicting the chosen order.

theorem Anderson4D.mem_residualIntervalShell_iff {n : ℕ} {active : Finset (Fin n)} {p q : Fin n × Fin n} (_h : LaterCrossCutIntervalContains p q) {x : Fin n} : x ∈ residualIntervalShell active p q ↔ x ∈ active ∧ q.1 ≤ x ∧ x ≤ q.2 ∧ (x < p.1 ∨ p.2 < x)

Membership in the shell between two nested traces, expressed as the two open side pieces around the inner trace.

theorem Anderson4D.relIcc_residualIntervalShell_eq_active_of_left {n : ℕ} {active : Finset (Fin n)} {p q : Fin n × Fin n} {a b : Fin n} (h : LaterCrossCutIntervalContains p q) (ha : a ∈ residualIntervalShell active p q) (hb : b ∈ residualIntervalShell active p q) (hbLeft : b < p.1) : relIcc (residualIntervalShell active p q) a b = relIcc active a b

On the left component of a shell, its relative intervals are the same as relative intervals of the full active carrier.

theorem Anderson4D.relIcc_residualIntervalShell_eq_active_of_right {n : ℕ} {active : Finset (Fin n)} {p q : Fin n × Fin n} {a b : Fin n} (h : LaterCrossCutIntervalContains p q) (ha : a ∈ residualIntervalShell active p q) (hb : b ∈ residualIntervalShell active p q) (haRight : p.2 < a) : relIcc (residualIntervalShell active p q) a b = relIcc active a b

Right-component counterpart of relIcc_residualIntervalShell_eq_active_of_left.

theorem Anderson4D.IsRelFullyPaired.momentResidualShell_straddlesInner {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} {p q : Fin (2 * m) × Fin (2 * m)} (hp : IsRelFullyPaired (momentCombinedPairing κp κm π) (momentResidualActive κp κm) p.1 p.2) (hpq : LaterCrossCutIntervalContains p q) {a b : Fin (2 * m)} (hab : IsRelFullyPaired (momentCombinedPairing κp κm π) (residualIntervalShell (momentResidualActive κp κm) p q) a b) : a < p.1 ∧ p.2 < b

A fully paired interval inside a residual shell must meet both side components of that shell. Otherwise it would lift to a residual fully-paired interval lying wholly on one side of the central cut.

theorem Anderson4D.residualIntervalTrace_union_relIcc_shell {n : ℕ} {active : Finset (Fin n)} {p q : Fin n × Fin n} {a b : Fin n} (hpq : LaterCrossCutIntervalContains p q) (ha : a ∈ residualIntervalShell active p q) (hb : b ∈ residualIntervalShell active p q) (haLeft : a < p.1) (hbRight : p.2 < b) : residualIntervalTrace active p ∪ relIcc (residualIntervalShell active p q) a b = relIcc active a b

A shell interval which crosses its inner trace lifts to the union of that inner trace and the shell interval on the original carrier.

theorem Anderson4D.first_residualIntervalShell_isRelPrimitiveOn {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (first next : Fin (2 * m) × Fin (2 * m)) (rest : List (Fin (2 * m) × Fin (2 * m))) (hchain : momentResidualIntervalChain κp κm π = first :: next :: rest) : IsRelPrimitiveOn (momentCombinedPairing κp κm π) (residualIntervalShell (momentResidualActive κp κm) first next)

The first shell of a canonical residual chain is primitive. A proper shell interval would lift to an extra residual interval strictly between the first two adjacent chain entries.

theorem Anderson4D.adjacent_residualIntervalShell_isRelPrimitiveOn {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (pre : List (Fin (2 * m) × Fin (2 * m))) (first next : Fin (2 * m) × Fin (2 * m)) (rest : List (Fin (2 * m) × Fin (2 * m))) (hchain : momentResidualIntervalChain κp κm π = pre ++ first :: next :: rest) : IsRelPrimitiveOn (momentCombinedPairing κp κm π) (residualIntervalShell (momentResidualActive κp κm) first next)

Every shell between adjacent entries of the canonical residual chain is primitive, including shells after a nonempty prefix.

theorem Anderson4D.mem_residualIntervalExterior_iff {n : ℕ} {active : Finset (Fin n)} {p : Fin n × Fin n} {x : Fin n} : x ∈ residualIntervalExterior active p ↔ x ∈ active ∧ (x < p.1 ∨ p.2 < x)

Membership in the exterior of a residual trace, expressed as the two open side pieces outside the trace.

theorem Anderson4D.relIcc_residualIntervalExterior_eq_active_of_left {n : ℕ} {active : Finset (Fin n)} {p : Fin n × Fin n} {a b : Fin n} (_ha : a ∈ residualIntervalExterior active p) (_hb : b ∈ residualIntervalExterior active p) (hbLeft : b < p.1) : relIcc (residualIntervalExterior active p) a b = relIcc active a b

On the left component of an exterior, its relative intervals are the same as relative intervals of the full active carrier.

theorem Anderson4D.relIcc_residualIntervalExterior_eq_active_of_right {n : ℕ} {active : Finset (Fin n)} {p : Fin n × Fin n} {a b : Fin n} (_ha : a ∈ residualIntervalExterior active p) (_hb : b ∈ residualIntervalExterior active p) (haRight : p.2 < a) : relIcc (residualIntervalExterior active p) a b = relIcc active a b

Right-component counterpart of relIcc_residualIntervalExterior_eq_active_of_left.

theorem Anderson4D.IsRelFullyPaired.momentResidualExterior_straddlesInner {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) {a b : Fin (2 * m)} (hab : IsRelFullyPaired (momentCombinedPairing κp κm π) (residualIntervalExterior (momentResidualActive κp κm) p) a b) : a < p.1 ∧ p.2 < b

A fully paired interval inside the final exterior must meet both side components. A one-sided interval would contradict residual cross-cut geometry.

theorem Anderson4D.residualIntervalTrace_union_relIcc_exterior {n : ℕ} {active : Finset (Fin n)} {p : Fin n × Fin n} {a b : Fin n} (_ha : a ∈ residualIntervalExterior active p) (_hb : b ∈ residualIntervalExterior active p) (haLeft : a < p.1) (hbRight : p.2 < b) : residualIntervalTrace active p ∪ relIcc (residualIntervalExterior active p) a b = relIcc active a b

An exterior interval which crosses its inner trace lifts to the union of that trace and the exterior interval on the original carrier.

theorem Anderson4D.last_residualIntervalExterior_isRelPrimitiveOn {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (pre : List (Fin (2 * m) × Fin (2 * m))) (last : Fin (2 * m) × Fin (2 * m)) (hchain : momentResidualIntervalChain κp κm π = pre ++ [last]) : IsRelPrimitiveOn (momentCombinedPairing κp κm π) (residualIntervalExterior (momentResidualActive κp κm) last)

The exterior after the outermost residual interval is primitive. Any proper exterior interval would lift to a residual interval outside the last entry of the canonical chain.

theorem Anderson4D.nestedResidualShells_forall_isRelPrimitiveOn {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (pre : List (Fin (2 * m) × Fin (2 * m))) (previous : Fin (2 * m) × Fin (2 * m)) (rest : List (Fin (2 * m) × Fin (2 * m))) (hchain : momentResidualIntervalChain κp κm π = pre ++ previous :: rest) : List.Forall (IsRelPrimitiveOn (momentCombinedPairing κp κm π)) (nestedResidualShells (momentResidualActive κp κm) previous rest)

All successive shells and the final exterior after a given chain entry are primitive.

theorem Anderson4D.residualIntervalTrace_union_nestedResidualShells {n : ℕ} (active : Finset (Fin n)) (previous : Fin n × Fin n) (rest : List (Fin n × Fin n)) (hpair : List.Pairwise LaterCrossCutIntervalContains (previous :: rest)) : residualIntervalTrace active previous ∪ finsetUnionList (nestedResidualShells active previous rest) = active

Starting from any trace in a nested chain, its later shells and final exterior complete it to the whole active carrier.

theorem Anderson4D.finsetUnionList_residualCollapseBlocks {n : ℕ} (active : Finset (Fin n)) (chain : List (Fin n × Fin n)) (hpair : List.Pairwise LaterCrossCutIntervalContains chain) : finsetUnionList (residualCollapseBlocks active chain) = active

The block list of any nested chain covers the active carrier exactly.

theorem Anderson4D.nestedResidualShells_forall_isFullyPairedOn {n : ℕ} {κ : PartialPairing (Fin n)} {active : Finset (Fin n)} (hactive : IsFullyPairedOn κ active) (previous : Fin n × Fin n) (hprevious : IsRelFullyPaired κ active previous.1 previous.2) (rest : List (Fin n × Fin n)) (hrest : ∀ p ∈ rest, IsRelFullyPaired κ active p.1 p.2) : List.Forall (IsFullyPairedOn κ) (nestedResidualShells active previous rest)

Every later shell and the final exterior are fully paired, provided the active carrier and all interval traces are fully paired.

theorem Anderson4D.residualCollapseBlocks_forall_isFullyPairedOn {n : ℕ} {κ : PartialPairing (Fin n)} {active : Finset (Fin n)} (hactive : IsFullyPairedOn κ active) (chain : List (Fin n × Fin n)) (hchain : ∀ p ∈ chain, IsRelFullyPaired κ active p.1 p.2) : List.Forall (IsFullyPairedOn κ) (residualCollapseBlocks active chain)

Every block in a collapse decomposition is fully paired.

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

Concrete collapse blocks for one R-324 contraction entity.

Equations

• Anderson4D.momentResidualCollapseBlocks κp κm π = Anderson4D.residualCollapseBlocks (Anderson4D.momentResidualActive κp κm) (Anderson4D.momentResidualIntervalChain κp κm π)

theorem Anderson4D.finsetUnionList_momentResidualCollapseBlocks {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) : finsetUnionList (momentResidualCollapseBlocks κp κm π) = momentResidualActive κp κm

The concrete R-324 collapse blocks cover the doubled residual carrier exactly.

theorem Anderson4D.momentResidualCollapseBlocks_forall_isFullyPairedOn {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) : List.Forall (IsFullyPairedOn (momentCombinedPairing κp κm π)) (momentResidualCollapseBlocks κp κm π)

Every concrete R-324 collapse block is closed and contains no single of the combined pairing.

theorem Anderson4D.momentResidualCollapseBlocks_forall_isRelPrimitiveOn {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) : List.Forall (IsRelPrimitiveOn (momentCombinedPairing κp κm π)) (momentResidualCollapseBlocks κp κm π)

Every concrete block used by the successive R-324 residual collapse is primitive on its sparse carrier.