Endpoint geometry of the R-322 extraction loop

This file formalizes the structural assertion used in paper §4.1, Step 1: the endpoint intervals selected by Definition 3.1 are pairwise disjoint or nested. In extraction order a later interval can only lie strictly to the left, strictly to the right, or strictly contain the earlier interval; it cannot cross it or lie inside the trace that has already been removed.

def Anderson4D.EarlierReductionIntervalCompatible {m : ℕ} (p q : Fin m × Fin m) : Prop

Directional laminarity for an earlier extracted interval p and a later extracted interval q.

Equations

• Anderson4D.EarlierReductionIntervalCompatible p q = (p.2 < q.1 ∨ q.2 < p.1 ∨ q.1 < p.1 ∧ p.2 < q.2)

def Anderson4D.ReductionIntervalsLaminar {m : ℕ} (p q : Fin m × Fin m) : Prop

Symmetric disjoint-or-nested relation used by the Dyck-word bookkeeping.

Equations

• Anderson4D.ReductionIntervalsLaminar p q = (p.2 < q.1 ∨ q.2 < p.1 ∨ p.1 < q.1 ∧ q.2 < p.2 ∨ q.1 < p.1 ∧ p.2 < q.2)

theorem Anderson4D.EarlierReductionIntervalCompatible.laminar {m : ℕ} {p q : Fin m × Fin m} (h : EarlierReductionIntervalCompatible p q) : ReductionIntervalsLaminar p q

theorem Anderson4D.ReductionIntervalsLaminar.symm {m : ℕ} {p q : Fin m × Fin m} (h : ReductionIntervalsLaminar p q) : ReductionIntervalsLaminar q p

Every selected interval has two distinct endpoints

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

theorem Anderson4D.extract_mem_fst_lt_snd {m : ℕ} (κ : PartialPairing (Fin m)) (p : Fin m × Fin m) (hp : p ∈ extract κ) : p.1 < p.2

Pairwise laminarity

theorem Anderson4D.extractAux_pairwise_earlierCompatible {m : ℕ} (κ : PartialPairing (Fin m)) (fuel : ℕ) (active : Finset (Fin m)) : List.Pairwise EarlierReductionIntervalCompatible (extractAux κ fuel active)

theorem Anderson4D.extract_pairwise_laminar {m : ℕ} (κ : PartialPairing (Fin m)) : List.Pairwise ReductionIntervalsLaminar (extract κ)

The extracted endpoint intervals are pairwise disjoint or nested, exactly the structural fact behind the paper's Dyck-word encoding.

Endpoint disjointness and counting

theorem Anderson4D.ReductionIntervalsLaminar.fst_ne_snd {m : ℕ} {p q : Fin m × Fin m} (hlam : ReductionIntervalsLaminar p q) (hp : p.1 < p.2) (hq : q.1 < q.2) : p.1 ≠ q.2

theorem Anderson4D.disjoint_leftEndpoints_rightEndpoints {m : ℕ} (κ : PartialPairing (Fin m)) : Disjoint (leftEndpoints κ) (rightEndpoints κ)

No index is simultaneously a left and a right endpoint of two extracted intervals.

theorem Anderson4D.card_union_reductionEndpoints {m : ℕ} (κ : PartialPairing (Fin m)) : (leftEndpoints κ ∪ rightEndpoints κ).card = 2 * (extract κ).length

The union of all selected endpoints contains exactly two positions per extracted interval.

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

The endpoint-role signature used to group the R-322 sum before the analytic interval reductions.

Equations

• Anderson4D.reductionEndpointSignature κ = (Anderson4D.leftEndpoints κ, Anderson4D.rightEndpoints κ)

def Anderson4D.nonSplitReductionEndpointSignatures (q : ℕ) : Finset (Finset (Fin (2 * q)) × Finset (Fin (2 * q)))

All signatures realized by the non-splitting pairings at order 2q.

Equations

• Anderson4D.nonSplitReductionEndpointSignatures q = Finset.image Anderson4D.reductionEndpointSignature (Anderson4D.nonSplitPairings q)

theorem Anderson4D.card_nonSplitReductionEndpointSignatures_le (q : ℕ) : (nonSplitReductionEndpointSignatures q).card ≤ 4 ^ (2 * q)

The endpoint and bracket-role choices in paper §4.1, Step 1 cost at most 4^(2q). This is the same coarse exponential factor obtained there from choosing the endpoint union and then a Dyck word.

Exact regrouping by endpoint signature

theorem Anderson4D.sum_nonSplitPairings_by_endpointSignature {M : Type u_1} [AddCommMonoid M] (q : ℕ) (F : PartialPairing (Fin (2 * q)) → M) : ∑ s ∈ nonSplitReductionEndpointSignatures q, ∑ κ ∈ nonSplitPairings q with reductionEndpointSignature κ = s, F κ = ∑ κ ∈ nonSplitPairings q, F κ

Regrouping the non-splitting pairing sum by its extraction-endpoint signature loses no terms and introduces no multiplicity. This is the finite-sum identity used before estimating each signature fiber in paper §4.1, Step 1.

theorem Anderson4D.sum_nonSplitPairings_le_of_endpointSignature_fibers (q : ℕ) (F : PartialPairing (Fin (2 * q)) → ℝ) (B : ℝ) (hB : 0 ≤ B) (hfiber : ∀ s ∈ nonSplitReductionEndpointSignatures q, ∑ κ ∈ nonSplitPairings q with reductionEndpointSignature κ = s, F κ ≤ B) : ∑ κ ∈ nonSplitPairings q, F κ ≤ 4 ^ (2 * q) * B

If every endpoint-signature fiber costs at most B, the whole non-splitting pairing sum costs at most 4^(2q) B.