Geometry of a nested residual suffix

Once an interval trace has been processed, all later shells together with the final exterior cover exactly the exterior of that trace. This is the moving-carrier identity behind the inside-to-outside Step 3 induction.

theorem Anderson4D.residualIntervalShell_union_exterior {n : ℕ} (active : Finset (Fin n)) (previous next : Fin n × Fin n) (hcontains : LaterCrossCutIntervalContains previous next) : residualIntervalShell active previous next ∪ residualIntervalExterior active next = residualIntervalExterior active previous

One shell followed by the exterior of its outer interval is exactly the exterior of the inner interval.

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

Nested suffix carrier identity. Starting immediately outside previous, the union of all later shells and the final exterior is exactly the exterior of previous.

theorem Anderson4D.finsetUnionList_nestedResidualShells_momentResidual_eq_exterior {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) : finsetUnionList (nestedResidualShells (momentResidualActive κp κm) previous rest) = residualIntervalExterior (momentResidualActive κp κm) previous

Canonical-chain specialization for any literal suffix beginning at previous. This avoids exposing the later attach/filter enrichment of the proof-relevant block schedule.

Half-carrier formulas and contiguity

theorem Anderson4D.finsetUnionList_nestedResidualShells_filter_lt {n cut : ℕ} (active : Finset (Fin n)) (previous : Fin n × Fin n) (rest : List (Fin n × Fin n)) (hpair : List.Pairwise LaterCrossCutIntervalContains (previous :: rest)) (hp1 : ↑previous.1 < cut) (hcutp2 : cut ≤ ↑previous.2) : {i ∈ finsetUnionList (nestedResidualShells active previous rest) | ↑i < cut} = {i ∈ active | i < previous.1}

The left half of a genuine nested suffix is the active initial interval strictly before the previous left endpoint.

theorem Anderson4D.finsetUnionList_nestedResidualShells_filter_ge {n cut : ℕ} (active : Finset (Fin n)) (previous : Fin n × Fin n) (rest : List (Fin n × Fin n)) (hpair : List.Pairwise LaterCrossCutIntervalContains (previous :: rest)) (hp1 : ↑previous.1 < cut) (hcutp2 : cut ≤ ↑previous.2) : {i ∈ finsetUnionList (nestedResidualShells active previous rest) | cut ≤ ↑i} = {i ∈ active | previous.2 < i}

The right half is the active terminal interval strictly after the previous right endpoint.

theorem Anderson4D.finsetUnionList_nestedResidualShells_filter_lt_ordConnectedWithin {n cut : ℕ} (active : Finset (Fin n)) (previous : Fin n × Fin n) (rest : List (Fin n × Fin n)) (hpair : List.Pairwise LaterCrossCutIntervalContains (previous :: rest)) (hp1 : ↑previous.1 < cut) (hcutp2 : cut ≤ ↑previous.2) : FinsetOrdConnectedWithin active ({i ∈ finsetUnionList (nestedResidualShells active previous rest) | ↑i < cut})

The left half of the nested suffix is order-connected relative to the original active carrier.

theorem Anderson4D.finsetUnionList_nestedResidualShells_filter_ge_ordConnectedWithin {n cut : ℕ} (active : Finset (Fin n)) (previous : Fin n × Fin n) (rest : List (Fin n × Fin n)) (hpair : List.Pairwise LaterCrossCutIntervalContains (previous :: rest)) (hp1 : ↑previous.1 < cut) (hcutp2 : cut ≤ ↑previous.2) : FinsetOrdConnectedWithin active ({i ∈ finsetUnionList (nestedResidualShells active previous rest) | cut ≤ ↑i})

Right-half relative order-connectedness.