Every cross-cut primitive block carries a cross pair

Paper: R-324 — §4.2 Step 3, the nested blocks straddle the cut

Paper §4.2 Step 3(b) proves that every surviving fully paired subinterval of κ₀ contains {p, p+1}, i.e. straddles the cut between the two copies. The blocks of the nested cross schedule therefore all satisfy R324CrossCutCarrier.

This module records the elementary consequence that the schedule needs: a block which straddles the cut, is fully paired, and is relatively primitive must actually pair some site below the cut to a site above it. Without that, the part below the cut would be a proper fully paired relative subinterval, which relative primitivity forbids.

theorem Anderson4D.exists_cross_pair_of_crossCut_primitive {m : ℕ} (κ : PartialPairing (Fin (2 * m))) (B : Finset (Fin (2 * m))) (hfull : IsFullyPairedOn κ B) (hprim : IsRelPrimitiveOn κ B) {l r : Fin (2 * m)} (hl : l ∈ B) (hr : r ∈ B) (hlm : ↑l < m) (hrm : m ≤ ↑r) : ∃ i ∈ B, ↑i < m ∧ m ≤ ↑(κ i)

A cross-cut, fully paired, relatively primitive block pairs across the cut.

The part of B below the cut is a relative interval — it is relIcc B a b for a the least element of B and b the greatest element below the cut — so if it were closed under the pairing it would be a proper fully paired relative subinterval of B, contradicting IsRelPrimitiveOn.

theorem Anderson4D.exists_leftSingle_of_cross_pair {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) {i : Fin (2 * m)} (him : ↑i < m) (hcross : m ≤ ↑((momentCombinedPairing κp κm π) i)) : ∃ (j : Fin m) (_ : j ∈ κp.singles), leftMomentIndex j = i

A site below the cut whose partner is above it is the left copy of a single of the left half: within-copy pairs stay below the cut.

theorem Anderson4D.exists_selected_markedBlock_eq {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) {B : Finset (Fin (2 * m))} (hmem : B ∈ nonemptyMomentResidualCollapseBlocks κp κm π) (hfull : IsFullyPairedOn (momentCombinedPairing κp κm π) B) (hprim : IsRelPrimitiveOn (momentCombinedPairing κp κm π) B) {l r : Fin (2 * m)} (hl : l ∈ B) (hr : r ∈ B) (hlm : ↑l < m) (hrm : m ≤ ↑r) : ∃ (selected : R324ResidualCovarianceSlot κp), r324MarkedResidualBlock κp κm π selected = B

Every block of the nested cross schedule is the marked block of some residual covariance slot.

Combining the two previous lemmas with the uniqueness in existsUnique_residualBlock_mem_of_marked: a cross-cut, fully paired, relatively primitive block contains a cross pair, hence the left copy of a single of the left half, and that single's marked block is the block itself.