Accounting for the deterministic interval-reduction loop

This file supplies the combinatorial bookkeeping used in paper §4.1 (R-322). The endpoint extraction in PairingExtract.lean already implements Definition 3.1 on a shrinking active set. Here we prove:

• removing a fully paired subset preserves fullness of the remainder;
• the final active set remains fully paired whenever the initial set is;
• each extraction consumes at least two active indices, giving the sharp division-free budget 2 * numberOfReductions + finalCard ≤ initialCard;
• for a full pairing the terminal active set is empty.

These are the termination and power-counting facts needed when each primitive reduction contributes one factor controlled by Proposition 4.1.

Fullness under removal

theorem Anderson4D.IsFullyPairedOn.sdiff {m : ℕ} {κ : PartialPairing (Fin m)} {A B : Finset (Fin m)} (hA : IsFullyPairedOn κ A) (hB : IsFullyPairedOn κ B) : IsFullyPairedOn κ (A \ B)

Removing a κ-closed fully paired set from another fully paired set leaves a fully paired set.

theorem Anderson4D.extractAuxS_final_fullyPaired {m : ℕ} (κ : PartialPairing (Fin m)) (fuel : ℕ) (active : Finset (Fin m)) : IsFullyPairedOn κ active → IsFullyPairedOn κ (extractAuxS κ fuel active).2

At every fuel depth, a fully paired active carrier yields a fully paired terminal carrier.

Closure and singles under removal

theorem Anderson4D.extractAuxS_final_apply_mem {m : ℕ} (κ : PartialPairing (Fin m)) (fuel : ℕ) (active : Finset (Fin m)) : (∀ i ∈ active, κ i ∈ active) → ∀ i ∈ (extractAuxS κ fuel active).2, κ i ∈ (extractAuxS κ fuel active).2

The extraction loop preserves closure under the pairing map, without requiring the active carrier to contain no singles.

theorem Anderson4D.mem_extractAuxS_final_of_mem_singles {m : ℕ} (κ : PartialPairing (Fin m)) (fuel : ℕ) (active : Finset (Fin m)) (i : Fin m) : i ∈ active → i ∈ κ.singles → i ∈ (extractAuxS κ fuel active).2

A fixed point cannot lie in a fully paired block, so any single which is initially active survives every extraction step.

theorem Anderson4D.finalActive_apply_mem {m : ℕ} (κ : PartialPairing (Fin m)) {i : Fin m} (hi : i ∈ finalActive κ) : κ i ∈ finalActive κ

The terminal active carrier is closed under every nontrivial pair (and also under fixed points).

theorem Anderson4D.singles_subset_finalActive {m : ℕ} (κ : PartialPairing (Fin m)) : κ.singles ⊆ finalActive κ

Every single survives the Definition 3.1 extraction loop.

Exact reduction budget

theorem Anderson4D.extractAuxS_reduction_budget {m : ℕ} (κ : PartialPairing (Fin m)) (fuel : ℕ) (active : Finset (Fin m)) : 2 * (extractAuxS κ fuel active).1.length + (extractAuxS κ fuel active).2.card ≤ active.card

Every extraction removes at least two active indices. The final-card term is retained, making this an induction invariant rather than merely a terminal estimate.

theorem Anderson4D.extract_reduction_budget {m : ℕ} (κ : PartialPairing (Fin m)) : 2 * (extract κ).length + (finalActive κ).card ≤ m

Public budget for Definition 3.1 extraction: 2 * |extract κ| + |finalActive κ| ≤ m.

theorem Anderson4D.extract_length_le_half {m : ℕ} (κ : PartialPairing (Fin m)) : (extract κ).length ≤ m / 2

In particular the number of primitive interval reductions is at most half the perturbative order.

Full pairings leave no residual active indices

theorem Anderson4D.finalActive_eq_empty_of_full {m : ℕ} {κ : PartialPairing (Fin m)} (hκ : κ.IsFull) : finalActive κ = ∅

A full pairing is exhausted completely by the relative interval extraction loop.

theorem Anderson4D.two_mul_extract_length_le_of_full {m : ℕ} {κ : PartialPairing (Fin m)} (hκ : κ.IsFull) : 2 * (extract κ).length ≤ m

For a full pairing, the accounting identity has no terminal residue.