Canonical ambient tails of an R-322 extraction fibre

ExtractionComplementFiberAt is naturally a pairing on the complement subtype. That representation is ideal for a single block split, but awkward for iteration because the next reduction step is formulated on the original ordered ambient carrier. This file gives the exact missing bridge:

• the complementary coordinate is equivalent to an ambient extraction-fibre member whose current block has been reset to the reference primitive coordinate;
• every extraction-fibre member has the fixed tail extraction after deleting the selected block;
• the one-step block equivalence can therefore return an ambient canonical tail, ready for the next active carrier.

No quotient and no multiplicity factor is introduced.

Tail extraction on the original ambient carrier

theorem Anderson4D.extractionFiber_tail_extractAux_eq {m : ℕ} (κ : PartialPairing (Fin m)) (fuel : ℕ) (active : Finset (Fin m)) (h : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired κ active a b) (τ : ExtractionFiberAt κ fuel active) : extractAux (↑τ) fuel (active \ selectedExtractionBlock κ active h) = extractAux κ fuel (active \ selectedExtractionBlock κ active h)

Equality of the complete nonempty extraction lists implies equality of their tails on the carrier left after the common first block is removed.

Canonical ambient representatives of complementary coordinates

@[reducible, inline]

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

Ambient members of the current extraction fibre whose exposed first primitive coordinate is the reference coordinate. Their remaining pairing is precisely the recursive tail data.

Equations

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

def Anderson4D.extractionComplementFiberEquivCanonicalTail {m : ℕ} (κ : PartialPairing (Fin m)) (fuel : ℕ) (active : Finset (Fin m)) (h : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired κ active a b) : ExtractionComplementFiberAt κ fuel active h ≃ CanonicalExtractionTailAt κ fuel active h

The complement-subtype coordinate is exactly a canonical ambient tail. This is the complement-to-tail bridge needed to iterate the one-block factorization without changing the ambient ordered carrier.

Equations

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

theorem Anderson4D.CanonicalExtractionTailAt.tail_extractAux_eq {m : ℕ} (κ : PartialPairing (Fin m)) (fuel : ℕ) (active : Finset (Fin m)) (h : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired κ active a b) (τ : CanonicalExtractionTailAt κ fuel active h) : extractAux (↑↑τ) fuel (active \ selectedExtractionBlock κ active h) = extractAux κ fuel (active \ selectedExtractionBlock κ active h)

Every canonical ambient tail has the correct next extraction on the shrunk active carrier.

First block followed by an ambient recursive tail

def Anderson4D.extractionFiberEquivBlockCanonicalTail {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))) × CanonicalExtractionTailAt κ fuel active h

Exact one-step extraction-fibre equivalence whose second coordinate stays on the original ambient carrier and is ready for the next active set.

Equations

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

theorem Anderson4D.sum_extractionFiber_eq_sum_block_canonicalTail {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))), ∑ tail : CanonicalExtractionTailAt κ fuel active h, F ((extractionFiberEquivBlockCanonicalTail κ fuel active h).symm (κB, tail))

Finite-sum form of extractionFiberEquivBlockCanonicalTail; it exposes one complete primitive coordinate and an ambient recursive tail with no cardinality loss.