A cross-cut shell is contiguous in each half

Paper: R-324 — §4.2 Step 3, the shells of the nested chain

The blocks of the nested schedule are the shells between consecutive intervals of paper Step 3(b)'s nested chain [a_t,b_t] ⊂ … ⊂ [a_1,b_1]:

residualIntervalShell active p q = relIcc active q.1 q.2 \ relIcc active p.1 p.2

with p the inner interval and q the outer one. Both straddle the cut (Step 3(b)), so on the left of the cut i ≤ p.2 and i ≤ q.2 hold automatically, and the shell's left part collapses to the relative half-open interval

{ i ∈ active | q.1 ≤ i < p.1 }

— contiguous in the active order by construction, which is what makes "the chain edges interior to the shell" a well-defined complement. The right part is the mirror image.

theorem Anderson4D.residualIntervalShell_filter_lt {n m : ℕ} (active : Finset (Fin n)) (p q : Fin n × Fin n) (hp1 : ↑p.1 < m) (hmp2 : m ≤ ↑p.2) (hmq2 : m ≤ ↑q.2) : {i ∈ residualIntervalShell active p q | ↑i < m} = {i ∈ active | q.1 ≤ i ∧ i < p.1}

The part of a cross-cut shell below the cut is a relative half-open interval.

Both bounding intervals straddle the cut, so below it the constraints i ≤ p.2 and i ≤ q.2 are vacuous and only q.1 ≤ i < p.1 survives.

theorem Anderson4D.residualIntervalShell_filter_ge {n m : ℕ} (active : Finset (Fin n)) (p q : Fin n × Fin n) (hp2 : m ≤ ↑p.2) (hq1 : ↑q.1 < m) (hp1 : ↑p.1 < m) : {i ∈ residualIntervalShell active p q | m ≤ ↑i} = {i ∈ active | p.2 < i ∧ i ≤ q.2}

The part of a cross-cut shell above the cut is a relative half-open interval. Mirror image of the previous lemma.