L0 combinatorics: iterated extraction of fully paired subintervals

Endpoint-extraction layer for Def 3.1 of Deng–Shen (arXiv:2607.10105), node D-RI (DESIGN §5.7bis): the renormalization iteratively removes the smallest-then-leftmost fully paired subinterval, where after removals a "subinterval" is contiguous in the remaining index order.

Design

• We never change the index type: the remaining indices are a shrinking active : Finset (Fin m). The trace of [a, b] on active is relIcc; IsRelFullyPaired κ active a b is the relative variant of IsFullyPairedOn κ (Finset.Icc a b).
• The Def 3.1(2) selector on the relative structure, selectRel, picks the candidate (a, b) minimizing the lexicographic triple ((relIcc active a b).card, a, b), encoded into ℕ by the mixed-radix key candKey active a b = card * ((m+1) * (m+1)) + (a * (m+1) + b) and selected via Finset.min' on the key image (minCandKey) plus Finset.choose (the key is injective, candKey_inj).
• The extraction recursion extractAux runs on fuel; each step removes the selected trace from active, which shrinks active by at least 2 (IsRelFullyPaired.two_le_card), so fuel m always reaches the no-candidate state (extract_fuel_sufficient, via the stateful variant extractAuxS).

Relative intervals

def Anderson4D.relIcc {m : ℕ} (active : Finset (Fin m)) (a b : Fin m) : Finset (Fin m)

The trace of the interval [a, b] on the set active of remaining indices: for the Def 3.1 iteration, "subinterval" means contiguous in the remaining index order, i.e. a set of this form.

Equations

• Anderson4D.relIcc active a b = {i ∈ active | a ≤ i ∧ i ≤ b}

@[simp]

theorem Anderson4D.mem_relIcc {m : ℕ} {active : Finset (Fin m)} {a b i : Fin m} : i ∈ relIcc active a b ↔ i ∈ active ∧ a ≤ i ∧ i ≤ b

theorem Anderson4D.relIcc_subset_active {m : ℕ} (active : Finset (Fin m)) (a b : Fin m) : relIcc active a b ⊆ active

theorem Anderson4D.relIcc_mono {m : ℕ} {active active' : Finset (Fin m)} (h : active ⊆ active') (a b : Fin m) : relIcc active a b ⊆ relIcc active' a b

Monotonicity of the trace in the active set.

def Anderson4D.IsRelFullyPaired {m : ℕ} (κ : PartialPairing (Fin m)) (active : Finset (Fin m)) (a b : Fin m) : Prop

Relative form of paper Def 2.3 / Def 3.1(2). The trace of [a, b] on active is a fully paired subinterval of the remaining index order: both endpoints are still active, a ≤ b, and the trace is fully paired.

Equations

• Anderson4D.IsRelFullyPaired κ active a b = (a ∈ active ∧ b ∈ active ∧ a ≤ b ∧ Anderson4D.IsFullyPairedOn κ (Anderson4D.relIcc active a b))

@[implicit_reducible]

instance Anderson4D.instDecidableIsRelFullyPaired {m : ℕ} (κ : PartialPairing (Fin m)) (active : Finset (Fin m)) (a b : Fin m) : Decidable (IsRelFullyPaired κ active a b)

Equations

• Anderson4D.instDecidableIsRelFullyPaired κ active a b = decidable_of_iff (a ∈ active ∧ b ∈ active ∧ a ≤ b ∧ Anderson4D.IsFullyPairedOn κ (Anderson4D.relIcc active a b)) ⋯

theorem Anderson4D.IsRelFullyPaired.left_mem {m : ℕ} {κ : PartialPairing (Fin m)} {active : Finset (Fin m)} {a b : Fin m} (h : IsRelFullyPaired κ active a b) : a ∈ active

theorem Anderson4D.IsRelFullyPaired.right_mem {m : ℕ} {κ : PartialPairing (Fin m)} {active : Finset (Fin m)} {a b : Fin m} (h : IsRelFullyPaired κ active a b) : b ∈ active

theorem Anderson4D.IsRelFullyPaired.le {m : ℕ} {κ : PartialPairing (Fin m)} {active : Finset (Fin m)} {a b : Fin m} (h : IsRelFullyPaired κ active a b) : a ≤ b

theorem Anderson4D.IsRelFullyPaired.isFullyPairedOn {m : ℕ} {κ : PartialPairing (Fin m)} {active : Finset (Fin m)} {a b : Fin m} (h : IsRelFullyPaired κ active a b) : IsFullyPairedOn κ (relIcc active a b)

theorem Anderson4D.IsRelFullyPaired.left_mem_relIcc {m : ℕ} {κ : PartialPairing (Fin m)} {active : Finset (Fin m)} {a b : Fin m} (h : IsRelFullyPaired κ active a b) : a ∈ relIcc active a b

theorem Anderson4D.IsRelFullyPaired.right_mem_relIcc {m : ℕ} {κ : PartialPairing (Fin m)} {active : Finset (Fin m)} {a b : Fin m} (h : IsRelFullyPaired κ active a b) : b ∈ relIcc active a b

theorem Anderson4D.IsRelFullyPaired.two_le_card {m : ℕ} {κ : PartialPairing (Fin m)} {active : Finset (Fin m)} {a b : Fin m} (h : IsRelFullyPaired κ active a b) : 2 ≤ (relIcc active a b).card

A relative fully paired interval contains at least one whole pair: its trace has at least two elements. This is the engine of the fuel bound for the extraction recursion.

The relative selector

Among all (a, b) with IsRelFullyPaired κ active a b, select the one with lexicographically minimal ((relIcc active a b).card, a, b), via the mixed-radix embedding candKey into ℕ and Finset.min'.

theorem Anderson4D.radix_le_left {N c₁ c₂ r₁ r₂ : ℕ} (hr₂ : r₂ < N) (h : c₁ * N + r₁ ≤ c₂ * N + r₂) : c₁ ≤ c₂

Mixed-radix comparison, leading digit: if r₁, r₂ < N then c₁ * N + r₁ ≤ c₂ * N + r₂ forces c₁ ≤ c₂.

theorem Anderson4D.radix_eq {N c₁ c₂ r₁ r₂ : ℕ} (hr₁ : r₁ < N) (hr₂ : r₂ < N) (h : c₁ * N + r₁ = c₂ * N + r₂) : c₁ = c₂ ∧ r₁ = r₂

Mixed-radix decomposition is unique: equal keys with in-range remainders have equal digits.

def Anderson4D.candKey {m : ℕ} (active : Finset (Fin m)) (a b : Fin m) : ℕ

The mixed-radix selection key of a candidate (a, b): (relIcc active a b).card * ((m+1) * (m+1)) + (a * (m+1) + b), i.e. the lexicographic triple (card, a, b) in base m + 1.

Equations

• Anderson4D.candKey active a b = (Anderson4D.relIcc active a b).card * ((m + 1) * (m + 1)) + (↑a * (m + 1) + ↑b)

theorem Anderson4D.candKey_inner_lt {m : ℕ} (a b : Fin m) : ↑a * (m + 1) + ↑b < (m + 1) * (m + 1)

The inner two digits of candKey stay below the outer radix.

theorem Anderson4D.candKey_inj {m : ℕ} {active : Finset (Fin m)} {a₁ b₁ a₂ b₂ : Fin m} (h : candKey active a₁ b₁ = candKey active a₂ b₂) : a₁ = a₂ ∧ b₁ = b₂

The key determines the candidate.

def Anderson4D.relCands {m : ℕ} (κ : PartialPairing (Fin m)) (active : Finset (Fin m)) : Finset (Fin m × Fin m)

The candidates of the relative selector: endpoint pairs of relative fully paired intervals of active.

Equations

• Anderson4D.relCands κ active = {p : Fin m × Fin m | Anderson4D.IsRelFullyPaired κ active p.1 p.2}

@[simp]

theorem Anderson4D.mem_relCands {m : ℕ} {κ : PartialPairing (Fin m)} {active : Finset (Fin m)} {p : Fin m × Fin m} : p ∈ relCands κ active ↔ IsRelFullyPaired κ active p.1 p.2

theorem Anderson4D.relCands_nonempty_iff {m : ℕ} {κ : PartialPairing (Fin m)} {active : Finset (Fin m)} : (relCands κ active).Nonempty ↔ ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired κ active a b

def Anderson4D.minCandKey {m : ℕ} (κ : PartialPairing (Fin m)) (active : Finset (Fin m)) (h : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired κ active a b) : ℕ

The minimal selection key over all candidates.

Equations

• Anderson4D.minCandKey κ active h = (Finset.image (fun (p : Fin m × Fin m) => Anderson4D.candKey active p.1 p.2) (Anderson4D.relCands κ active)).min' ⋯

theorem Anderson4D.exists_unique_minKey_cand {m : ℕ} (κ : PartialPairing (Fin m)) (active : Finset (Fin m)) (h : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired κ active a b) : ∃! p : Fin m × Fin m, p ∈ relCands κ active ∧ candKey active p.1 p.2 = minCandKey κ active h

def Anderson4D.selectRel {m : ℕ} (κ : PartialPairing (Fin m)) (active : Finset (Fin m)) (h : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired κ active a b) : Fin m × Fin m

Relative Def 3.1(2) selector. The candidate (a, b) with lexicographically minimal ((relIcc active a b).card, a, b).

Equations

• Anderson4D.selectRel κ active h = Finset.choose (fun (a : Fin m × Fin m) => Anderson4D.candKey active a.1 a.2 = Anderson4D.minCandKey κ active h) (Anderson4D.relCands κ active) ⋯

theorem Anderson4D.selectRel_mem_relCands {m : ℕ} (κ : PartialPairing (Fin m)) (active : Finset (Fin m)) (h : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired κ active a b) : selectRel κ active h ∈ relCands κ active

theorem Anderson4D.selectRel_isRelFullyPaired {m : ℕ} (κ : PartialPairing (Fin m)) (active : Finset (Fin m)) (h : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired κ active a b) : IsRelFullyPaired κ active (selectRel κ active h).1 (selectRel κ active h).2

The selected pair is a genuine candidate.

theorem Anderson4D.candKey_selectRel {m : ℕ} (κ : PartialPairing (Fin m)) (active : Finset (Fin m)) (h : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired κ active a b) : candKey active (selectRel κ active h).1 (selectRel κ active h).2 = minCandKey κ active h

theorem Anderson4D.candKey_selectRel_le {m : ℕ} {κ : PartialPairing (Fin m)} {active : Finset (Fin m)} (h : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired κ active a b) {a b : Fin m} (hab : IsRelFullyPaired κ active a b) : candKey active (selectRel κ active h).1 (selectRel κ active h).2 ≤ candKey active a b

Key minimality of the selected pair over all candidates.

theorem Anderson4D.selectRel_card_le {m : ℕ} {κ : PartialPairing (Fin m)} {active : Finset (Fin m)} (h : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired κ active a b) {a b : Fin m} (hab : IsRelFullyPaired κ active a b) : (relIcc active (selectRel κ active h).1 (selectRel κ active h).2).card ≤ (relIcc active a b).card

Selector spec, first component of the lexicographic order: the selected trace has minimal cardinality among all candidates.

theorem Anderson4D.selectRel_fst_le {m : ℕ} {κ : PartialPairing (Fin m)} {active : Finset (Fin m)} (h : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired κ active a b) {a b : Fin m} (hab : IsRelFullyPaired κ active a b) (hcard : (relIcc active (selectRel κ active h).1 (selectRel κ active h).2).card = (relIcc active a b).card) : (selectRel κ active h).1 ≤ a

Selector spec, second component: among candidates of the minimal trace cardinality, the selected left endpoint is leftmost.

theorem Anderson4D.selectRel_snd_le {m : ℕ} {κ : PartialPairing (Fin m)} {active : Finset (Fin m)} (h : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired κ active a b) {a b : Fin m} (hab : IsRelFullyPaired κ active a b) (hcard : (relIcc active (selectRel κ active h).1 (selectRel κ active h).2).card = (relIcc active a b).card) (hfst : (selectRel κ active h).1 = a) : (selectRel κ active h).2 ≤ b

Selector spec, third component: among candidates of minimal trace cardinality and minimal left endpoint, the selected right endpoint is minimal.

The extraction recursion (paper Def 3.1, node D-RI)

def Anderson4D.extractAux {m : ℕ} (κ : PartialPairing (Fin m)) : ℕ → Finset (Fin m) → List (Fin m × Fin m)

Fuel recursion implementing the Def 3.1 iteration: while a relative fully paired interval exists in active, extract the selected endpoint pair and remove its trace from active.

Equations

• One or more equations did not get rendered due to their size.
• Anderson4D.extractAux κ 0 x✝ = []

@[simp]

theorem Anderson4D.extractAux_zero {m : ℕ} (κ : PartialPairing (Fin m)) (active : Finset (Fin m)) : extractAux κ 0 active = []

theorem Anderson4D.extractAux_succ {m : ℕ} (κ : PartialPairing (Fin m)) (fuel : ℕ) (active : Finset (Fin m)) : extractAux κ (fuel + 1) active = if h : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired κ active a b then selectRel κ active h :: extractAux κ fuel (active \ relIcc active (selectRel κ active h).1 (selectRel κ active h).2) else []

Raw recursion equation at successor fuel.

@[simp]

theorem Anderson4D.extractAux_succ_pos {m : ℕ} {κ : PartialPairing (Fin m)} {active : Finset (Fin m)} (fuel : ℕ) (h : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired κ active a b) : extractAux κ (fuel + 1) active = selectRel κ active h :: extractAux κ fuel (active \ relIcc active (selectRel κ active h).1 (selectRel κ active h).2)

Recursion equation, candidate case.

@[simp]

theorem Anderson4D.extractAux_succ_neg {m : ℕ} {κ : PartialPairing (Fin m)} {active : Finset (Fin m)} (fuel : ℕ) (h : ¬∃ (a : Fin m) (b : Fin m), IsRelFullyPaired κ active a b) : extractAux κ (fuel + 1) active = []

Recursion equation, no-candidate case.

theorem Anderson4D.extractAux_nil_of_no_candidate {m : ℕ} {κ : PartialPairing (Fin m)} {active : Finset (Fin m)} (fuel : ℕ) (h : ¬∃ (a : Fin m) (b : Fin m), IsRelFullyPaired κ active a b) : extractAux κ fuel active = []

def Anderson4D.extract {m : ℕ} (κ : PartialPairing (Fin m)) : List (Fin m × Fin m)

Paper Def 3.1 (node D-RI). The list of endpoint pairs of the successively removed fully paired subintervals, starting from all of Fin m; fuel m always suffices (extract_fuel_sufficient).

Equations

• Anderson4D.extract κ = Anderson4D.extractAux κ m Finset.univ

theorem Anderson4D.extractAux_mem {m : ℕ} (κ : PartialPairing (Fin m)) (fuel : ℕ) (active : Finset (Fin m)) (p : Fin m × Fin m) : p ∈ extractAux κ fuel active → p.1 ∈ active ∧ p.2 ∈ active ∧ p.1 ≤ p.2

Step invariant: every extracted pair has both endpoints in the active set of its step (hence in the initial one), and is ordered.

theorem Anderson4D.extract_spec {m : ℕ} (κ : PartialPairing (Fin m)) (p : Fin m × Fin m) : p ∈ extract κ → p.1 ≤ p.2

Weak extraction spec: every extracted pair is ordered.

theorem Anderson4D.card_sdiff_relIcc_add_two_le {m : ℕ} {κ : PartialPairing (Fin m)} {active : Finset (Fin m)} {a b : Fin m} (h : IsRelFullyPaired κ active a b) : (active \ relIcc active a b).card + 2 ≤ active.card

Each extraction step shrinks the active set by at least two elements.

The stateful recursion and fuel adequacy

def Anderson4D.extractAuxS {m : ℕ} (κ : PartialPairing (Fin m)) : ℕ → Finset (Fin m) → List (Fin m × Fin m) × Finset (Fin m)

Stateful variant of extractAux, additionally returning the final active set; used to state fuel adequacy (extract_fuel_sufficient).

Equations

• One or more equations did not get rendered due to their size.
• Anderson4D.extractAuxS κ 0 x✝ = ([], x✝)

@[simp]

theorem Anderson4D.extractAuxS_zero {m : ℕ} (κ : PartialPairing (Fin m)) (active : Finset (Fin m)) : extractAuxS κ 0 active = ([], active)

@[simp]

theorem Anderson4D.extractAuxS_succ_pos {m : ℕ} {κ : PartialPairing (Fin m)} {active : Finset (Fin m)} (fuel : ℕ) (h : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired κ active a b) : extractAuxS κ (fuel + 1) active = (selectRel κ active h :: (extractAuxS κ fuel (active \ relIcc active (selectRel κ active h).1 (selectRel κ active h).2)).1, (extractAuxS κ fuel (active \ relIcc active (selectRel κ active h).1 (selectRel κ active h).2)).2)

Recursion equation for extractAuxS, candidate case.

@[simp]

theorem Anderson4D.extractAuxS_succ_neg {m : ℕ} {κ : PartialPairing (Fin m)} {active : Finset (Fin m)} (fuel : ℕ) (h : ¬∃ (a : Fin m) (b : Fin m), IsRelFullyPaired κ active a b) : extractAuxS κ (fuel + 1) active = ([], active)

Recursion equation for extractAuxS, no-candidate case.

theorem Anderson4D.extractAuxS_fst {m : ℕ} (κ : PartialPairing (Fin m)) (fuel : ℕ) (active : Finset (Fin m)) : (extractAuxS κ fuel active).1 = extractAux κ fuel active

The extracted list of the stateful recursion is extractAux.

theorem Anderson4D.extractAuxS_no_candidate {m : ℕ} (κ : PartialPairing (Fin m)) (fuel : ℕ) (active : Finset (Fin m)) : active.card ≤ 2 * fuel + 1 → ¬∃ (a : Fin m) (b : Fin m), IsRelFullyPaired κ (extractAuxS κ fuel active).2 a b

Fuel adequacy, general form: if active.card ≤ 2 * fuel + 1 then the recursion reaches the no-candidate state (each step removes at least two elements, card_sdiff_relIcc_add_two_le).

def Anderson4D.finalActive {m : ℕ} (κ : PartialPairing (Fin m)) : Finset (Fin m)

The active set remaining after the extraction loop (fuel m, initial state Finset.univ).

Equations

• Anderson4D.finalActive κ = (Anderson4D.extractAuxS κ m Finset.univ).2

theorem Anderson4D.extract_eq_extractAuxS_fst {m : ℕ} (κ : PartialPairing (Fin m)) : extract κ = (extractAuxS κ m Finset.univ).1

theorem Anderson4D.extract_fuel_sufficient {m : ℕ} (κ : PartialPairing (Fin m)) : ¬∃ (a : Fin m) (b : Fin m), IsRelFullyPaired κ (finalActive κ) a b

Fuel adequacy. Fuel m reaches the terminal state of the Def 3.1 iteration: no relative fully paired interval survives in finalActive.

Endpoint sets for the closed formulas

theorem Anderson4D.extractAux_map_snd_nodup {m : ℕ} (κ : PartialPairing (Fin m)) (fuel : ℕ) (active : Finset (Fin m)) : (List.map Prod.snd (extractAux κ fuel active)).Nodup

The selected right endpoint lies in the removed trace, so it never reappears: the extracted right endpoints are pairwise distinct.

theorem Anderson4D.extractAux_map_fst_nodup {m : ℕ} (κ : PartialPairing (Fin m)) (fuel : ℕ) (active : Finset (Fin m)) : (List.map Prod.fst (extractAux κ fuel active)).Nodup

Left analogue: the extracted left endpoints are pairwise distinct.

theorem Anderson4D.extract_map_snd_nodup {m : ℕ} (κ : PartialPairing (Fin m)) : (List.map Prod.snd (extract κ)).Nodup

theorem Anderson4D.extract_map_fst_nodup {m : ℕ} (κ : PartialPairing (Fin m)) : (List.map Prod.fst (extract κ)).Nodup

def Anderson4D.rightEndpoints {m : ℕ} (κ : PartialPairing (Fin m)) : Finset (Fin m)

The right endpoints b_i of the extracted intervals (input to the closed formulas of §4.1).

Equations

• Anderson4D.rightEndpoints κ = (List.map Prod.snd (Anderson4D.extract κ)).toFinset

def Anderson4D.leftEndpoints {m : ℕ} (κ : PartialPairing (Fin m)) : Finset (Fin m)

The left endpoints a_i of the extracted intervals.

Equations

• Anderson4D.leftEndpoints κ = (List.map Prod.fst (Anderson4D.extract κ)).toFinset

theorem Anderson4D.rightEndpoints_card_eq_length {m : ℕ} (κ : PartialPairing (Fin m)) : (rightEndpoints κ).card = (extract κ).length

theorem Anderson4D.leftEndpoints_card_eq_length {m : ℕ} (κ : PartialPairing (Fin m)) : (leftEndpoints κ).card = (extract κ).length

Sanity checks on small cases