Stable residual carriers for the signed R-324 fibre

The first-block factorization of a within-half endpoint fibre is dependent: after exposing the primitive block pairing κB, both the reconstructed ambient pairing and the type of the cross-single equivalence mention κB. Analytically, however, a primitive full block has no singles. Consequently, for a fixed complementary coordinate, changing κB cannot change the ambient single set.

This file records that rigidity before any absolute value is taken. It is the type-level bridge needed to put the complete primitive sum innermost in the signed phase-A Fubini argument while keeping the residual cross-single carrier fixed.

Singles are carried entirely by the complementary coordinate

theorem Anderson4D.primitiveClosedOnEquiv_symm_singles_eq {n q : ℕ} (B : Finset (Fin n)) (e : Fin (2 * q) ≃o ↥B) (κB κB' : ↥(primitiveFullPairings q)) (κC : PartialPairing { i : Fin n // i ∉ B }) : (↑↑((primitiveClosedOnEquiv q B e).symm (κB, κC))).singles = (↑↑((primitiveClosedOnEquiv q B e).symm (κB', κC))).singles

Reassembling two primitive full block coordinates over the same complement produces ambient pairings with exactly the same single set.

The first endpoint-fibre coordinate has a stable residual carrier

theorem Anderson4D.reductionEndpointFiberEquivBlockComplement_symm_singles_eq {m : ℕ} (κ : PartialPairing (Fin m)) (h : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired κ Finset.univ a b) (κB κB' : ↥(primitiveFullPairings (residualBlockOrder (selectedExtractionBlock κ Finset.univ h)))) (κC : ExtractionComplementFiberAt κ (m - 1) Finset.univ h) : (↑((reductionEndpointFiberEquivBlockComplement κ h).symm (κB, κC))).singles = (↑((reductionEndpointFiberEquivBlockComplement κ h).symm (κB', κC))).singles

In the public first-block endpoint-fibre equivalence, the reconstructed pairing's singles depend only on the complementary coordinate, not on the primitive full pairing installed on the selected block.

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

The canonical reconstructed endpoint-fibre member obtained by keeping the complement κC and reinstalling the reference first-block pairing.

Equations

• Anderson4D.firstBlockReferenceEndpointFiber κ h κC = (Anderson4D.reductionEndpointFiberEquivBlockComplement κ h).symm (Anderson4D.selectedExtractionPrimitivePairing κ Finset.univ h, κC)

def Anderson4D.firstBlockCrossEquivStabilization {m : ℕ} (κ : PartialPairing (Fin m)) (h : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired κ Finset.univ a b) (κB : ↥(primitiveFullPairings (residualBlockOrder (selectedExtractionBlock κ Finset.univ h)))) (κC : ExtractionComplementFiberAt κ (m - 1) Finset.univ h) (κother : PartialPairing (Fin m)) : ↥(↑((reductionEndpointFiberEquivBlockComplement κ h).symm (κB, κC))).singles ≃ ↥κother.singles ≃ (↥(↑(firstBlockReferenceEndpointFiber κ h κC)).singles ≃ ↥κother.singles)

Canonical transport of a cross-single equivalence to the κB-independent single carrier furnished by the reference block coordinate.

Equations

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

@[simp]

theorem Anderson4D.firstBlockCrossEquivStabilization_symm_apply {m : ℕ} (κ : PartialPairing (Fin m)) (h : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired κ Finset.univ a b) (κB : ↥(primitiveFullPairings (residualBlockOrder (selectedExtractionBlock κ Finset.univ h)))) (κC : ExtractionComplementFiberAt κ (m - 1) Finset.univ h) (κother : PartialPairing (Fin m)) (π : ↥(↑(firstBlockReferenceEndpointFiber κ h κC)).singles ≃ ↥κother.singles) : (firstBlockCrossEquivStabilization κ h κB κC κother).symm π = (finsetSubtypeEquivOfEq ⋯).trans π

Signed first-left reindex with the primitive sum innermost

theorem Anderson4D.sum_momentSignatureFiber_eq_firstLeftBlock_stable {m : ℕ} (e₀ : MomentContraction m) (hleft : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired e₀.fst Finset.univ a b) {A : Type u_1} [AddCommMonoid A] (F : MomentSignatureFiberAt e₀ → A) : ∑ e : MomentSignatureFiberAt e₀, F e = ∑ κC : ExtractionComplementFiberAt e₀.fst (m - 1) Finset.univ hleft, ∑ κm : ReductionEndpointFiberAt e₀.snd.fst, ∑ π : ↥(↑(firstBlockReferenceEndpointFiber e₀.fst hleft κC)).singles ≃ ↥(↑κm).singles, ∑ κB : ↥(primitiveFullPairings (residualBlockOrder (selectedExtractionBlock e₀.fst Finset.univ hleft))), F ((momentSignatureFiberEquivCoordinates e₀).symm ⟨(reductionEndpointFiberEquivBlockComplement e₀.fst hleft).symm (κB, κC), ⟨κm, (firstBlockCrossEquivStabilization e₀.fst hleft κB κC ↑κm).symm π⟩⟩)

Exact first-left reindexing in the order required by phase A: the complementary left coordinate, right endpoint-fibre member, and cross-single equivalence are fixed before the complete primitive block coordinate is summed. The cross-single type is independent of κB, so the innermost finite sum can be identified with the signed primitive kernel before any norm is taken.