Selector and Fubini routing for R-322

This file turns the deterministic smallest-leftmost selector into the analytic inside-to-outside route used in paper Section 4.1. The first task is to separate the final primitive block from all proper blocks: for a non-splitting full pairing, an extracted interval can meet a global endpoint only when it is the whole interval.

The unique extracted interval meeting the global left endpoint

theorem Anderson4D.extract_mem_isRelFullyPaired_univ {m : ℕ} (κ : PartialPairing (Fin m)) (p : Fin m × Fin m) (hp : p ∈ extract κ) : IsRelFullyPaired κ Finset.univ p.1 p.2

Every pair in the public extraction list was already a fully paired relative interval in the initial full carrier.

theorem Anderson4D.relIcc_univ {m : ℕ} (a b : Fin m) : relIcc Finset.univ a b = Finset.Icc a b

In the initial carrier, a relative interval is the ordinary interval.

theorem Anderson4D.extracted_right_eq_last_of_isNonSplit_of_left_eq_zero {q : ℕ} {κ : PartialPairing (Fin (2 * q))} (hq : 1 ≤ q) (hκ : IsNonSplit κ) (p : Fin (2 * q) × Fin (2 * q)) (hp : p ∈ extract κ) (hleft : p.1 = ⟨0, ⋯⟩) : p.2 = ⟨2 * q - 1, ⋯⟩

For a non-splitting full pairing, an extracted interval whose left endpoint is the global first index must be the whole interval.

theorem Anderson4D.extracted_left_eq_zero_of_isNonSplit_of_right_eq_last {q : ℕ} {κ : PartialPairing (Fin (2 * q))} (hq : 1 ≤ q) (hκ : IsNonSplit κ) (p : Fin (2 * q) × Fin (2 * q)) (hp : p ∈ extract κ) (hright : p.2 = ⟨2 * q - 1, ⋯⟩) : p.1 = ⟨0, ⋯⟩

Dually, an extracted interval whose right endpoint is the global last index must also begin at the global first index. The proof uses fullness: the complement of a fully paired suffix is a fully paired proper prefix, which is forbidden by IsNonSplit.

theorem Anderson4D.extracted_meets_global_endpoint_iff_whole {q : ℕ} {κ : PartialPairing (Fin (2 * q))} (hq : 1 ≤ q) (hκ : IsNonSplit κ) (p : Fin (2 * q) × Fin (2 * q)) (hp : p ∈ extract κ) : p.1 = ⟨0, ⋯⟩ ∨ p.2 = ⟨2 * q - 1, ⋯⟩ ↔ p = (⟨0, ⋯⟩, ⟨2 * q - 1, ⋯⟩)

In a non-splitting extraction, meeting either global endpoint is equivalent to being the unique whole-interval endpoint pair.

The endpoint list and concrete block list are aligned

def Anderson4D.ExtractionPairBlockAligned {m : ℕ} (p : Fin m × Fin m) (B : Finset (Fin m)) : Prop

The endpoint pair selected at one step is the pair of order bounds of the concrete relative trace removed at that step.

Equations

• Anderson4D.ExtractionPairBlockAligned p B = (p.1 ∈ B ∧ p.2 ∈ B ∧ ∀ i ∈ B, p.1 ≤ i ∧ i ≤ p.2)

theorem Anderson4D.extractAux_extractionBlocksAux_aligned {m : ℕ} (κ : PartialPairing (Fin m)) (fuel : ℕ) (active : Finset (Fin m)) : List.Forall₂ ExtractionPairBlockAligned (extractAux κ fuel active) (extractionBlocksAux κ fuel active)

The endpoint and concrete-trace recursions are pointwise aligned, not merely equal in length.

theorem Anderson4D.exists_extractedPair_aligned_of_mem_extractionBlocks {m : ℕ} (κ : PartialPairing (Fin m)) {B : Finset (Fin m)} (hB : B ∈ extractionBlocks κ) : ∃ p ∈ extract κ, ExtractionPairBlockAligned p B

Public endpoint/block alignment.

The whole endpoint pair exists and is terminal

theorem Anderson4D.whole_pair_mem_extract_of_isNonSplit {q : ℕ} {κ : PartialPairing (Fin (2 * q))} (hq : 1 ≤ q) (hκ : IsNonSplit κ) : (⟨0, ⋯⟩, ⟨2 * q - 1, ⋯⟩) ∈ extract κ

A full non-splitting pairing has a whole-interval extraction pair.

theorem Anderson4D.whole_pair_not_earlierCompatible {q : ℕ} (hq : 1 ≤ q) (p : Fin (2 * q) × Fin (2 * q)) : ¬EarlierReductionIntervalCompatible (⟨0, ⋯⟩, ⟨2 * q - 1, ⋯⟩) p

The whole interval cannot precede another extracted interval.

theorem Anderson4D.extract_eq_prefix_append_whole_of_isNonSplit {q : ℕ} {κ : PartialPairing (Fin (2 * q))} (hq : 1 ≤ q) (hκ : IsNonSplit κ) : ∃ (proper : List (Fin (2 * q) × Fin (2 * q))), extract κ = proper ++ [(⟨0, ⋯⟩, ⟨2 * q - 1, ⋯⟩)]

The deterministic selector removes every proper block first and the whole block last.