Exact full/full factorization of a refined R-324 fibre

If one representative of a residual-refined contraction fibre has full pairings in both halves, endpoint-signature rigidity makes every pairing in the two corresponding endpoint fibres full. The residual carrier is then empty, so the residual signature filter removes nothing. Consequently the entire refined fibre is exactly the product of the two endpoint-signature fibres; the cross-single equivalence is the unique equivalence between two empty single sets.

After this finite reindexing, the already established factorization of one frozen full/full contraction turns the complete refined sum into the product of the two complete half-fibre sums. The only analytic assumptions are termwise integrability of the left and right half integrands. No grouped residual is replaced by a fixed detIntegrand, and no coupling factor is introduced.

Empty residual signatures

theorem Anderson4D.momentResidualChainSignature_eq_empty_of_isFull {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (hp : κp.IsFull) (hm : κm.IsFull) : momentResidualChainSignature κp κm π = (∅, ∅)

Both full within-half pairings have the empty residual-chain signature, independently of the (necessarily empty) cross-single equivalence.

theorem Anderson4D.momentResidualChainSignature_eq_of_full_reference {m : ℕ} (e₀ : MomentContraction m) (hp : e₀.fst.IsFull) (hm : e₀.snd.fst.IsFull) (e : MomentSignatureFiberAt e₀) : momentResidualChainSignature (↑e).fst (↑e).snd.fst (↑e).snd.snd = momentResidualChainSignature e₀.fst e₀.snd.fst e₀.snd.snd

In a moment-signature fibre over a full/full reference, the residual signature is automatically the reference residual signature.

Exact finite fibre equivalence

def Anderson4D.fullPairingSinglesEquiv {m : ℕ} (κp κm : PartialPairing (Fin m)) (hp : κp.IsFull) (hm : κm.IsFull) : ↥κp.singles ≃ ↥κm.singles

The unique cross-single equivalence between two full pairings.

Equations

• Anderson4D.fullPairingSinglesEquiv κp κm hp hm = Equiv.equivOfIsEmpty ↥κp.singles ↥κm.singles

def Anderson4D.momentRefinedFullFullFiberEquivMomentSignatureFiber {m : ℕ} {s r : Finset (Fin (2 * m)) × Finset (Fin (2 * m))} (e₀ : MomentContraction m) (he₀ : e₀ ∈ momentRefinedContractionFiber m s r) (hp : e₀.fst.IsFull) (hm : e₀.snd.fst.IsFull) : MomentRefinedContractionFiberAt m s r ≃ MomentSignatureFiberAt e₀

For a full/full representative, its refined fibre is exactly its whole moment-signature fibre: the residual signature condition is automatic.

Equations

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

def Anderson4D.momentFullFullSignatureCoordinatesEquivEndpointFibers {m : ℕ} (e₀ : MomentContraction m) (hp : e₀.fst.IsFull) (hm : e₀.snd.fst.IsFull) : MomentSignatureCoordinates e₀ ≃ ReductionEndpointFiberAt e₀.fst × ReductionEndpointFiberAt e₀.snd.fst

In full/full moment coordinates, the cross-single equivalence is uniquely determined, leaving just the two independent endpoint fibres.

Equations

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

def Anderson4D.momentRefinedFullFullFiberEquivEndpointFibers {m : ℕ} {s r : Finset (Fin (2 * m)) × Finset (Fin (2 * m))} (e₀ : MomentContraction m) (he₀ : e₀ ∈ momentRefinedContractionFiber m s r) (hp : e₀.fst.IsFull) (hm : e₀.snd.fst.IsFull) : MomentRefinedContractionFiberAt m s r ≃ ReductionEndpointFiberAt e₀.fst × ReductionEndpointFiberAt e₀.snd.fst

Exact product coordinates for an entire full/full residual-refined fibre. This equivalence is the no-multiplicity statement: every contraction occurs once and only once.

Equations

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

Analytic half terms and full-fibre factorization

noncomputable def Anderson4D.deterministicFullHalfIntegral (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (α β : Z4) (κ : PartialPairing (Fin m)) : ℂ

One signed half integral, with the two endpoint modes kept explicit.

Equations

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

def Anderson4D.DeterministicFullHalfIntegrable (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (α β : Z4) (κ : PartialPairing (Fin m)) : Prop

The exact termwise analytic seam needed before applying the frozen full/full contraction factorization.

Equations

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

theorem Anderson4D.sum_momentRefinedContractionFiber_deterministicMomentContractionTerm_eq_fullHalfFiber_mul (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (α β : Z4) {s r : Finset (Fin (2 * m)) × Finset (Fin (2 * m))} (e₀ : MomentContraction m) (he₀ : e₀ ∈ momentRefinedContractionFiber m s r) (hp : e₀.fst.IsFull) (hm : e₀.snd.fst.IsFull) (hleft : ∀ (κp : ReductionEndpointFiberAt e₀.fst), DeterministicFullHalfIntegrable ρ ε m α β ↑κp) (hright : ∀ (κm : ReductionEndpointFiberAt e₀.snd.fst), DeterministicFullHalfIntegrable ρ ε m (-α) (-β) ↑κm) : ∑ e ∈ momentRefinedContractionFiber m s r, deterministicMomentContractionTerm ρ ε m α β e = (∑ κp : ReductionEndpointFiberAt e₀.fst, deterministicFullHalfIntegral ρ ε m α β ↑κp) * ∑ κm : ReductionEndpointFiberAt e₀.snd.fst, deterministicFullHalfIntegral ρ ε m (-α) (-β) ↑κm

Full/full refined-fibre factorization.

The complete frozen contraction sum over a residual-refined fibre is the product of the complete left and right endpoint-signature fibre sums. The right modes are exactly -α,-β; no lamEps factor belongs to the frozen contraction term.