Rigidity of the smallest-leftmost extraction order

The endpoint signature initially determines the interval family only up to List.Perm. For the exact R-324 fibre factorization we also need the concrete recursive order, because each step removes a sparse relative trace.

The key observation is that every interval selected later in the recursion was already fully paired in the earlier active carrier. A disjoint earlier trace does not change it, while a nested earlier trace is itself a closed fully-paired component of the larger interval. Therefore two extraction lists which are permutations have the same smallest-key head; recursion then forces equality of the lists and of their concrete trace blocks.

theorem Anderson4D.IsRelFullyPaired.lift_before_compatible_removal {m : ℕ} {κ : PartialPairing (Fin m)} {active : Finset (Fin m)} {p q : Fin m × Fin m} (hp : IsRelFullyPaired κ active p.1 p.2) (hq : IsRelFullyPaired κ (active \ relIcc active p.1 p.2) q.1 q.2) (hcompat : EarlierReductionIntervalCompatible p q) : IsRelFullyPaired κ active q.1 q.2

A later relative candidate remains a candidate before an earlier, compatible fully-paired trace is removed.

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

Every endpoint pair appearing later in an extraction recursion was already a fully-paired relative interval in the initial active carrier.

theorem Anderson4D.selectRel_eq_of_extractAux_perm {m fuel : ℕ} {κ κ' : PartialPairing (Fin m)} {active : Finset (Fin m)} (h : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired κ active a b) (h' : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired κ' active a b) (hperm : (extractAux κ (fuel + 1) active).Perm (extractAux κ' (fuel + 1) active)) : selectRel κ active h = selectRel κ' active h'

Permutation of two nonempty extraction recursions forces equality of their smallest-key selectors.

theorem Anderson4D.extractAux_eq_of_perm {m : ℕ} (κ κ' : PartialPairing (Fin m)) (fuel : ℕ) (active : Finset (Fin m)) : (extractAux κ fuel active).Perm (extractAux κ' fuel active) → extractAux κ fuel active = extractAux κ' fuel active

The deterministic smallest-leftmost recursion is rigid: if two output lists are permutations, then they are equal in their actual recursion order.

theorem Anderson4D.extract_eq_of_reductionEndpointSignature_eq {m : ℕ} (κ κ' : PartialPairing (Fin m)) (hsignature : reductionEndpointSignature κ = reductionEndpointSignature κ') : extract κ = extract κ'

Endpoint signatures determine the actual extraction list, not merely its unordered interval family.

theorem Anderson4D.extractionBlocksAux_eq_of_extractAux_eq {m : ℕ} (κ κ' : PartialPairing (Fin m)) (fuel : ℕ) (active : Finset (Fin m)) : extractAux κ fuel active = extractAux κ' fuel active → extractionBlocksAux κ fuel active = extractionBlocksAux κ' fuel active

Equality of endpoint extraction recursions determines the concrete sparse traces removed at every step.

theorem Anderson4D.extractionBlocks_eq_of_reductionEndpointSignature_eq {m : ℕ} (κ κ' : PartialPairing (Fin m)) (hsignature : reductionEndpointSignature κ = reductionEndpointSignature κ') : extractionBlocks κ = extractionBlocks κ'

Endpoint signatures determine the concrete primitive trace blocks in their actual extraction order.

Consequences for fixed R-324 moment signatures

theorem Anderson4D.momentExtractionBlocks_eq_of_momentContractionSignature_eq {m : ℕ} (e e' : MomentContraction m) (hsignature : momentContractionSignature e = momentContractionSignature e') : momentLeftExtractionBlocks e.fst = momentLeftExtractionBlocks e'.fst ∧ momentRightExtractionBlocks e.snd.fst = momentRightExtractionBlocks e'.snd.fst

Equality of doubled moment signatures fixes both concrete within-half block lists, including their recursive order and sparse traces.

theorem Anderson4D.finalActive_eq_sdiff_extractionBlocks {m : ℕ} (κ : PartialPairing (Fin m)) : finalActive κ = Finset.univ \ finsetUnionList (extractionBlocks κ)

The terminal active carrier is the complement of the union of the concrete extraction blocks.

theorem Anderson4D.finalActive_eq_of_reductionEndpointSignature_eq {m : ℕ} (κ κ' : PartialPairing (Fin m)) (hsignature : reductionEndpointSignature κ = reductionEndpointSignature κ') : finalActive κ = finalActive κ'

An endpoint signature therefore fixes the terminal active carrier.

theorem Anderson4D.momentFinalActive_eq_of_momentContractionSignature_eq {m : ℕ} (e e' : MomentContraction m) (hsignature : momentContractionSignature e = momentContractionSignature e') : finalActive e.fst = finalActive e'.fst ∧ finalActive e.snd.fst = finalActive e'.snd.fst

A doubled moment signature fixes the left and right residual carriers on which the cross-copy contraction is subsequently collapsed.

Exact first-block factorization of an endpoint-signature fibre

@[reducible, inline]

abbrev Anderson4D.ReductionEndpointFiberAt {m : ℕ} (κ : PartialPairing (Fin m)) : Type

The finite fibre of partial pairings with the same complete reduction endpoint signature as κ.

Equations

• Anderson4D.ReductionEndpointFiberAt κ = { τ : Anderson4D.PartialPairing (Fin m) // Anderson4D.reductionEndpointSignature τ = Anderson4D.reductionEndpointSignature κ }

theorem Anderson4D.reductionEndpointSignature_eq_of_extract_eq {m : ℕ} (κ κ' : PartialPairing (Fin m)) (hextract : extract κ = extract κ') : reductionEndpointSignature κ = reductionEndpointSignature κ'

Equality of the ordered extraction lists immediately implies equality of endpoint-role signatures.

theorem Anderson4D.pred_add_one_eq_of_exists_relFullyPaired {m : ℕ} {κ : PartialPairing (Fin m)} {active : Finset (Fin m)} (h : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired κ active a b) : m - 1 + 1 = m

A nonempty candidate set implies that public fuel m is a successor, so it can be used by the one-step ExtractionFiberAt interface.

def Anderson4D.reductionEndpointFiberEquivExtractionFiber {m : ℕ} (κ : PartialPairing (Fin m)) (h : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired κ Finset.univ a b) : ReductionEndpointFiberAt κ ≃ ExtractionFiberAt κ (m - 1) Finset.univ

The endpoint-signature fibre is exactly the fixed ordered-extraction fibre used by the primitive replacement engine.

Equations

• One or more equations did not get rendered due to their size.

def Anderson4D.reductionEndpointFiberEquivBlockComplement {m : ℕ} (κ : PartialPairing (Fin m)) (h : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired κ Finset.univ a b) : ReductionEndpointFiberAt κ ≃ ↥(primitiveFullPairings (residualBlockOrder (selectedExtractionBlock κ Finset.univ h))) × ExtractionComplementFiberAt κ (m - 1) Finset.univ h

Exact first recursive coordinate of a nonempty endpoint-signature fibre: a complete primitive pairing on the selected block, times the remaining complementary extraction fibre.

Equations

• One or more equations did not get rendered due to their size.

theorem Anderson4D.sum_reductionEndpointFiber_eq_sum_block_complement {m : ℕ} (κ : PartialPairing (Fin m)) (h : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired κ Finset.univ a b) {M : Type u_1} [AddCommMonoid M] (F : ReductionEndpointFiberAt κ → M) : ∑ τ : ReductionEndpointFiberAt κ, F τ = ∑ κB : ↥(primitiveFullPairings (residualBlockOrder (selectedExtractionBlock κ Finset.univ h))), ∑ κC : ExtractionComplementFiberAt κ (m - 1) Finset.univ h, F ((reductionEndpointFiberEquivBlockComplement κ h).symm (κB, κC))

Finite-sum form of the exact first-block endpoint-fibre factorization. In particular, no cardinality factor is introduced.