Primitive-block replacement preserves endpoint extraction

The fixed-signature collapse in paper §4.2 requires a converse to the already proved extraction facts. Once the selector has exposed a primitive fully paired block, the pairing inside that block may be replaced by any other primitive full pairing without changing the selected endpoint or the remainder of the extraction.

This file proves that statement directly from the smallest-then-leftmost selector. The key order fact is that a fully paired relative interval meeting a primitive closed relative block must contain the whole block.

theorem Anderson4D.isRelFullyPaired_iff_of_eq_on_active {m : ℕ} {κ κ' : PartialPairing (Fin m)} {active : Finset (Fin m)} (hagree : ∀ i ∈ active, κ i = κ' i) (a b : Fin m) : IsRelFullyPaired κ active a b ↔ IsRelFullyPaired κ' active a b

Agreement of two pairings on the active carrier preserves every relative fully-paired predicate on that carrier.

theorem Anderson4D.selectRel_eq_of_candidates_iff {m : ℕ} {κ κ' : PartialPairing (Fin m)} {active : Finset (Fin m)} (hcand : ∀ (a b : Fin m), IsRelFullyPaired κ active a b ↔ IsRelFullyPaired κ' active a b) (h : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired κ active a b) (h' : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired κ' active a b) : selectRel κ active h = selectRel κ' active h'

If the relative candidate predicates agree, the deterministic smallest-then-leftmost selectors agree as well.

theorem Anderson4D.extractAux_eq_of_eq_on_active {m : ℕ} {κ κ' : PartialPairing (Fin m)} (fuel : ℕ) (active : Finset (Fin m)) (hagree : ∀ i ∈ active, κ i = κ' i) : extractAux κ fuel active = extractAux κ' fuel active

Pairings agreeing on the active carrier have identical extraction recursions from that carrier.

theorem Anderson4D.extractionBlocksAux_eq_of_eq_on_active {m : ℕ} {κ κ' : PartialPairing (Fin m)} (fuel : ℕ) (active : Finset (Fin m)) (hagree : ∀ i ∈ active, κ i = κ' i) : extractionBlocksAux κ fuel active = extractionBlocksAux κ' fuel active

Agreement on the active carrier also preserves the concrete list of traces recorded alongside endpoint extraction.

theorem Anderson4D.relIcc_inter_relIcc {m : ℕ} (active : Finset (Fin m)) (a b c d : Fin m) : relIcc active a b ∩ relIcc active c d = relIcc active (max a c) (min b d)

The intersection of two relative intervals on the same active carrier is the relative interval with the maximum left and minimum right endpoint.

theorem Anderson4D.isFullyPairedOn_of_disjoint_of_eq_outside {m : ℕ} {κ κ' : PartialPairing (Fin m)} {B R : Finset (Fin m)} (hdisjoint : Disjoint B R) (hagree : ∀ i ∉ B, κ i = κ' i) (hR : IsFullyPairedOn κ R) : IsFullyPairedOn κ' R

A fully paired set disjoint from the replacement block remains fully paired when the pairings agree outside that block.

theorem Anderson4D.relPrimitiveBlock_subset_of_not_disjoint {m : ℕ} {κ : PartialPairing (Fin m)} {active : Finset (Fin m)} {p q a b : Fin m} (hB : IsRelFullyPaired κ active p q) (hprim : IsRelPrimitiveOn κ (relIcc active p q)) (hR : IsRelFullyPaired κ active a b) (hinter : ¬Disjoint (relIcc active p q) (relIcc active a b)) : relIcc active p q ⊆ relIcc active a b

Any fully paired relative interval meeting a primitive fully paired relative block contains that entire block. This is the laminarity fact which makes primitive-block replacement invisible to the selector.

theorem Anderson4D.isRelFullyPaired_of_card_le_primitiveBlockReplacement {m : ℕ} {κ κ' : PartialPairing (Fin m)} {active : Finset (Fin m)} {p q a b : Fin m} (hB : IsRelFullyPaired κ active p q) (hB' : IsRelFullyPaired κ' active p q) (hprim' : IsRelPrimitiveOn κ' (relIcc active p q)) (hagree : ∀ i ∉ relIcc active p q, κ i = κ' i) (hR' : IsRelFullyPaired κ' active a b) (hcard : (relIcc active a b).card ≤ (relIcc active p q).card) : IsRelFullyPaired κ active a b

A candidate for the replaced pairing whose trace is no larger than the primitive replacement block was already a candidate for the original pairing. It is either disjoint from the block or equal to the block.

theorem Anderson4D.selectRel_eq_of_primitive_selectedBlockReplacement {m : ℕ} {κ κ' : 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) (hB' : IsFullyPairedOn κ' (relIcc active (selectRel κ active h).1 (selectRel κ active h).2)) (hprim' : IsRelPrimitiveOn κ' (relIcc active (selectRel κ active h).1 (selectRel κ active h).2)) (hagree : ∀ i ∉ relIcc active (selectRel κ active h).1 (selectRel κ active h).2, κ i = κ' i) : selectRel κ active h = selectRel κ' active h'

Replacing the pairing inside the currently selected trace by an arbitrary primitive full pairing leaves the deterministic selector unchanged.

theorem Anderson4D.extractAux_eq_of_primitive_selectedBlockReplacement {m : ℕ} {κ κ' : PartialPairing (Fin m)} (fuel : ℕ) (active : Finset (Fin m)) (h : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired κ active a b) (hB' : IsFullyPairedOn κ' (relIcc active (selectRel κ active h).1 (selectRel κ active h).2)) (hprim' : IsRelPrimitiveOn κ' (relIcc active (selectRel κ active h).1 (selectRel κ active h).2)) (hagree : ∀ i ∉ relIcc active (selectRel κ active h).1 (selectRel κ active h).2, κ i = κ' i) : extractAux κ (fuel + 1) active = extractAux κ' (fuel + 1) active

One primitive replacement step preserves the complete endpoint extraction recursion: the selected block is unchanged, and after removing it the pairings agree on the remaining active carrier.

theorem Anderson4D.extractionBlocksAux_eq_of_primitive_selectedBlockReplacement {m : ℕ} {κ κ' : PartialPairing (Fin m)} (fuel : ℕ) (active : Finset (Fin m)) (h : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired κ active a b) (hB' : IsFullyPairedOn κ' (relIcc active (selectRel κ active h).1 (selectRel κ active h).2)) (hprim' : IsRelPrimitiveOn κ' (relIcc active (selectRel κ active h).1 (selectRel κ active h).2)) (hagree : ∀ i ∉ relIcc active (selectRel κ active h).1 (selectRel κ active h).2, κ i = κ' i) : extractionBlocksAux κ (fuel + 1) active = extractionBlocksAux κ' (fuel + 1) active

Concrete-trace counterpart of extractAux_eq_of_primitive_selectedBlockReplacement.

Concrete replacement by a standard primitive pairing

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

The trace selected at the current extraction state.

Equations

• Anderson4D.selectedExtractionBlock κ active h = Anderson4D.relIcc active (Anderson4D.selectRel κ active h).1 (Anderson4D.selectRel κ active h).2

def Anderson4D.selectedPrimitiveClosedOnReplacement {m : ℕ} (κ : PartialPairing (Fin m)) (active : Finset (Fin m)) (h : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired κ active a b) (κB : ↥(primitiveFullPairings (residualBlockOrder (selectedExtractionBlock κ active h)))) : PrimitiveClosedOn (residualBlockOrder (selectedExtractionBlock κ active h)) (selectedExtractionBlock κ active h) (residualPrimitiveBlockOrderIso κ (selectedExtractionBlock κ active h) ⋯)

Replace the currently selected block by one standard primitive pairing, retaining the original pairing on the complementary carrier. The exact block/complement equivalence makes this a multiplicity-free operation.

Equations

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

def Anderson4D.selectedPrimitiveReplacement {m : ℕ} (κ : PartialPairing (Fin m)) (active : Finset (Fin m)) (h : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired κ active a b) (κB : ↥(primitiveFullPairings (residualBlockOrder (selectedExtractionBlock κ active h)))) : PartialPairing (Fin m)

Ambient pairing obtained from selectedPrimitiveClosedOnReplacement.

Equations

• Anderson4D.selectedPrimitiveReplacement κ active h κB = ↑↑(Anderson4D.selectedPrimitiveClosedOnReplacement κ active h κB)

theorem Anderson4D.selectedPrimitiveReplacement_eq_outside {m : ℕ} (κ : PartialPairing (Fin m)) (active : Finset (Fin m)) (h : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired κ active a b) (κB : ↥(primitiveFullPairings (residualBlockOrder (selectedExtractionBlock κ active h)))) (i : Fin m) (hi : i ∉ selectedExtractionBlock κ active h) : (selectedPrimitiveReplacement κ active h κB) i = κ i

theorem Anderson4D.extractAux_selectedPrimitiveReplacement {m : ℕ} (κ : PartialPairing (Fin m)) (fuel : ℕ) (active : Finset (Fin m)) (h : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired κ active a b) (κB : ↥(primitiveFullPairings (residualBlockOrder (selectedExtractionBlock κ active h)))) : extractAux κ (fuel + 1) active = extractAux (selectedPrimitiveReplacement κ active h κB) (fuel + 1) active

The concrete standard-pairing replacement preserves the endpoint extraction recursion from the current active state.

theorem Anderson4D.extractionBlocksAux_selectedPrimitiveReplacement {m : ℕ} (κ : PartialPairing (Fin m)) (fuel : ℕ) (active : Finset (Fin m)) (h : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired κ active a b) (κB : ↥(primitiveFullPairings (residualBlockOrder (selectedExtractionBlock κ active h)))) : extractionBlocksAux κ (fuel + 1) active = extractionBlocksAux (selectedPrimitiveReplacement κ active h κB) (fuel + 1) active

Concrete-trace counterpart of extractAux_selectedPrimitiveReplacement.

theorem Anderson4D.extract_selectedPrimitiveReplacement {m : ℕ} (κ : PartialPairing (Fin m)) (h : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired κ Finset.univ a b) (κB : ↥(primitiveFullPairings (residualBlockOrder (selectedExtractionBlock κ Finset.univ h)))) : extract κ = extract (selectedPrimitiveReplacement κ Finset.univ h κB)

At the public initial state, replacing the first primitive block preserves the complete endpoint extraction list.

theorem Anderson4D.extractionBlocks_selectedPrimitiveReplacement {m : ℕ} (κ : PartialPairing (Fin m)) (h : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired κ Finset.univ a b) (κB : ↥(primitiveFullPairings (residualBlockOrder (selectedExtractionBlock κ Finset.univ h)))) : extractionBlocks κ = extractionBlocks (selectedPrimitiveReplacement κ Finset.univ h κB)

Public concrete-trace list is likewise unchanged.

theorem Anderson4D.reductionEndpointSignature_selectedPrimitiveReplacement {m : ℕ} (κ : PartialPairing (Fin m)) (h : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired κ Finset.univ a b) (κB : ↥(primitiveFullPairings (residualBlockOrder (selectedExtractionBlock κ Finset.univ h)))) : reductionEndpointSignature κ = reductionEndpointSignature (selectedPrimitiveReplacement κ Finset.univ h κB)

In particular, first-block replacement stays in the same endpoint signature fiber used by both R-322 and the within-half part of R-324.

Block-coordinate form of replacement invariance

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

Equality with a nonempty extraction step forces existence of a candidate on the other pairing.

theorem Anderson4D.selectRel_eq_of_extractAux_eq {m : ℕ} {κ κ' : PartialPairing (Fin m)} (fuel : ℕ) (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) (hextract : extractAux κ' (fuel + 1) active = extractAux κ (fuel + 1) active) : selectRel κ' active h' = selectRel κ active h

Equality of two nonempty extraction recursions identifies their first selected endpoints.

theorem Anderson4D.selectedExtractionBlock_eq_of_extractAux_eq {m : ℕ} {κ κ' : PartialPairing (Fin m)} (fuel : ℕ) (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) (hextract : extractAux κ' (fuel + 1) active = extractAux κ (fuel + 1) active) : selectedExtractionBlock κ' active h' = selectedExtractionBlock κ active h

Hence equal nonempty extraction recursions have the same concrete first trace.

theorem Anderson4D.PrimitiveClosedOn.eq_outside_of_complement_eq {m q : ℕ} {B : Finset (Fin m)} {e : Fin (2 * q) ≃o ↥B} (κ κ' : PrimitiveClosedOn q B e) (hcomp : ((primitiveClosedOnEquiv q B e) κ).2 = ((primitiveClosedOnEquiv q B e) κ').2) (i : Fin m) (hi : i ∉ B) : ↑↑κ i = ↑↑κ' i

Equality of the complementary coordinate in primitiveClosedOnEquiv is exactly equality of the ambient pairings away from the block.

theorem Anderson4D.extractAux_eq_of_primitiveClosedOn_sameComplement {m q : ℕ} {B : Finset (Fin m)} {e : Fin (2 * q) ≃o ↥B} (κ κ' : PrimitiveClosedOn q B e) (fuel : ℕ) (active : Finset (Fin m)) (h : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired (↑↑κ) active a b) (hB : B = selectedExtractionBlock (↑↑κ) active h) (hcomp : ((primitiveClosedOnEquiv q B e) κ).2 = ((primitiveClosedOnEquiv q B e) κ').2) : extractAux (↑↑κ) (fuel + 1) active = extractAux (↑↑κ') (fuel + 1) active

Two ambient pairings which differ only in the primitive coordinate of the currently selected block have identical endpoint extraction.

theorem Anderson4D.extractionBlocksAux_eq_of_primitiveClosedOn_sameComplement {m q : ℕ} {B : Finset (Fin m)} {e : Fin (2 * q) ≃o ↥B} (κ κ' : PrimitiveClosedOn q B e) (fuel : ℕ) (active : Finset (Fin m)) (h : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired (↑↑κ) active a b) (hB : B = selectedExtractionBlock (↑↑κ) active h) (hcomp : ((primitiveClosedOnEquiv q B e) κ).2 = ((primitiveClosedOnEquiv q B e) κ').2) : extractionBlocksAux (↑↑κ) (fuel + 1) active = extractionBlocksAux (↑↑κ') (fuel + 1) active

Concrete-trace counterpart of extractAux_eq_of_primitiveClosedOn_sameComplement.

Exact fiber factorization at one extraction step

@[reducible, inline]

abbrev Anderson4D.ExtractionFiberAt {m : ℕ} (κ : PartialPairing (Fin m)) (fuel : ℕ) (active : Finset (Fin m)) : Type

Pairings with exactly the same remaining endpoint extraction as a fixed reference pairing.

Equations

• Anderson4D.ExtractionFiberAt κ fuel active = { τ : Anderson4D.PartialPairing (Fin m) // Anderson4D.extractAux τ (fuel + 1) active = Anderson4D.extractAux κ (fuel + 1) active }

def Anderson4D.extractionFiberPrimitiveClosedOn {m : ℕ} (κ : PartialPairing (Fin m)) (fuel : ℕ) (active : Finset (Fin m)) (h : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired κ active a b) (τ : ExtractionFiberAt κ fuel active) : PrimitiveClosedOn (residualBlockOrder (selectedExtractionBlock κ active h)) (selectedExtractionBlock κ active h) (residualPrimitiveBlockOrderIso κ (selectedExtractionBlock κ active h) ⋯)

Every member of a nonempty extraction fiber carries the fixed first trace as a primitive closed block.

Equations

• Anderson4D.extractionFiberPrimitiveClosedOn κ fuel active h τ = ⟨⟨↑τ, ⋯⟩, ⋯⟩

def Anderson4D.extractionFiberEquivPrimitiveClosedOn {m : ℕ} (κ : PartialPairing (Fin m)) (fuel : ℕ) (active : Finset (Fin m)) (h : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired κ active a b) : ExtractionFiberAt κ fuel active ≃ { τ : PrimitiveClosedOn (residualBlockOrder (selectedExtractionBlock κ active h)) (selectedExtractionBlock κ active h) (residualPrimitiveBlockOrderIso κ (selectedExtractionBlock κ active h) ⋯) // extractAux (↑↑τ) (fuel + 1) active = extractAux κ (fuel + 1) active }

Forgetting the primitive-block certificate recovers the original extraction-fiber member.

Equations

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

def Anderson4D.selectedExtractionPrimitivePairing {m : ℕ} (κ : PartialPairing (Fin m)) (active : Finset (Fin m)) (h : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired κ active a b) : ↥(primitiveFullPairings (residualBlockOrder (selectedExtractionBlock κ active h)))

The reference pairing's standard primitive first-block coordinate.

Equations

• Anderson4D.selectedExtractionPrimitivePairing κ active h = ⟨Anderson4D.residualPrimitiveBlockPairing κ (Anderson4D.selectedExtractionBlock κ active h) ⋯, ⋯⟩

def Anderson4D.IsInPrimitiveExtractionFiber {m : ℕ} (κ : PartialPairing (Fin m)) (fuel : ℕ) (active : Finset (Fin m)) (h : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired κ active a b) (τ : PrimitiveClosedOn (residualBlockOrder (selectedExtractionBlock κ active h)) (selectedExtractionBlock κ active h) (residualPrimitiveBlockOrderIso κ (selectedExtractionBlock κ active h) ⋯)) : Prop

The extraction-fiber predicate on a primitive closed block.

Equations

• Anderson4D.IsInPrimitiveExtractionFiber κ fuel active h τ = (Anderson4D.extractAux (↑↑τ) (fuel + 1) active = Anderson4D.extractAux κ (fuel + 1) active)

@[implicit_reducible]

instance Anderson4D.instDecidableIsInPrimitiveExtractionFiber {m : ℕ} (κ : PartialPairing (Fin m)) (fuel : ℕ) (active : Finset (Fin m)) (h : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired κ active a b) (τ : PrimitiveClosedOn (residualBlockOrder (selectedExtractionBlock κ active h)) (selectedExtractionBlock κ active h) (residualPrimitiveBlockOrderIso κ (selectedExtractionBlock κ active h) ⋯)) : Decidable (IsInPrimitiveExtractionFiber κ fuel active h τ)

Equations

• Anderson4D.instDecidableIsInPrimitiveExtractionFiber κ fuel active h τ = id inferInstance

theorem Anderson4D.isInPrimitiveExtractionFiber_invariant {m : ℕ} (κ : PartialPairing (Fin m)) (fuel : ℕ) (active : Finset (Fin m)) (h : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired κ active a b) (κB κB' : ↥(primitiveFullPairings (residualBlockOrder (selectedExtractionBlock κ active h)))) (κC : PartialPairing { i : Fin m // i ∉ selectedExtractionBlock κ active h }) : IsInPrimitiveExtractionFiber κ fuel active h ((primitiveClosedOnEquiv (residualBlockOrder (selectedExtractionBlock κ active h)) (selectedExtractionBlock κ active h) (residualPrimitiveBlockOrderIso κ (selectedExtractionBlock κ active h) ⋯)).symm (κB, κC)) ↔ IsInPrimitiveExtractionFiber κ fuel active h ((primitiveClosedOnEquiv (residualBlockOrder (selectedExtractionBlock κ active h)) (selectedExtractionBlock κ active h) (residualPrimitiveBlockOrderIso κ (selectedExtractionBlock κ active h) ⋯)).symm (κB', κC))

Membership in the fixed extraction fiber is independent of the primitive first-block coordinate once the complement is fixed.

@[reducible, inline]

abbrev Anderson4D.ExtractionComplementFiberAt {m : ℕ} (κ : PartialPairing (Fin m)) (fuel : ℕ) (active : Finset (Fin m)) (h : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired κ active a b) : Type

Complementary-coordinate fiber left after the complete primitive sum on the current first block has been exposed.

Equations

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

def Anderson4D.extractionFiberEquivBlockComplement {m : ℕ} (κ : PartialPairing (Fin m)) (fuel : ℕ) (active : Finset (Fin m)) (h : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired κ active a b) : ExtractionFiberAt κ fuel active ≃ ↥(primitiveFullPairings (residualBlockOrder (selectedExtractionBlock κ active h))) × ExtractionComplementFiberAt κ fuel active h

One exact recursive step of fixed-signature factorization: a pairing fiber is a complete primitive-pairing coordinate on the current block times one complementary extraction fiber.

Equations

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

theorem Anderson4D.sum_extractionFiber_eq_sum_block_complement {m : ℕ} (κ : PartialPairing (Fin m)) (fuel : ℕ) (active : Finset (Fin m)) (h : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired κ active a b) {M : Type u_1} [AddCommMonoid M] (F : ExtractionFiberAt κ fuel active → M) : ∑ τ : ExtractionFiberAt κ fuel active, F τ = ∑ κB : ↥(primitiveFullPairings (residualBlockOrder (selectedExtractionBlock κ active h))), ∑ κC : ExtractionComplementFiberAt κ fuel active h, F ((extractionFiberEquivBlockComplement κ fuel active h).symm (κB, κC))

Exact finite-sum form of extractionFiberEquivBlockComplement; no block cardinality or factorial factor is introduced.