Signed within-half collapse for R-324

Paper Section 4.2 first fixes only the two within-half endpoint signatures. The primitive pairing on a selected within-half block is then summed and its spatial variables are integrated before an absolute value is taken. The residual cross-single equivalence, the other half, and every complementary spatial coordinate remain outside this operation.

This file packages that exact phase-A order. It deliberately does not fix a residual-chain signature and does not use the nonnegative enlarged primitive-partition fibre.

Stable first-left coordinates

@[reducible, inline]

abbrev Anderson4D.R324FirstLeftBlockCoordinate {m : ℕ} (e₀ : MomentContraction m) (hleft : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired e₀.fst Finset.univ a b) : Type

The complete primitive pairing coordinate on the first selected left block.

Equations

• Anderson4D.R324FirstLeftBlockCoordinate e₀ hleft = ↥(Anderson4D.primitiveFullPairings (Anderson4D.residualBlockOrder (Anderson4D.selectedExtractionBlock e₀.fst Finset.univ hleft)))

@[reducible, inline]

abbrev Anderson4D.R324FirstLeftOuterCoordinate {m : ℕ} (e₀ : MomentContraction m) (hleft : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired e₀.fst Finset.univ a b) : Type

All discrete coordinates which remain outside the first-left primitive sum. The single carrier is stabilized at the reference block coordinate, so this type does not mention the varying primitive coordinate.

Equations

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

def Anderson4D.r324FirstLeftReconstruct {m : ℕ} (e₀ : MomentContraction m) (hleft : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired e₀.fst Finset.univ a b) (ω : R324FirstLeftOuterCoordinate e₀ hleft) (κB : R324FirstLeftBlockCoordinate e₀ hleft) : MomentSignatureFiberAt e₀

Reassemble one member of the original within-half signature fibre from the stable outer coordinates and one complete primitive left-block coordinate.

Equations

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

theorem Anderson4D.sum_momentSignatureFiber_eq_firstLeftOuter_block {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 = ∑ ω : R324FirstLeftOuterCoordinate e₀ hleft, ∑ κB : R324FirstLeftBlockCoordinate e₀ hleft, F (r324FirstLeftReconstruct e₀ hleft ω κB)

The signed within-half fibre sum is exactly an outer sum over the residual data followed by the complete primitive coordinate sum.

Exact selected-coordinate Fubini routing

def Anderson4D.r324FirstLeftSelected {m : ℕ} (e₀ : MomentContraction m) (hleft : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired e₀.fst Finset.univ a b) (i : Fin (2 * m)) : Prop

Predicate selecting the doubled spatial coordinates belonging to the first left primitive block.

Equations

• Anderson4D.r324FirstLeftSelected e₀ hleft i = (i ∈ Finset.image Anderson4D.leftMomentIndex (Anderson4D.selectedExtractionBlock e₀.fst Finset.univ hleft))

@[implicit_reducible]

instance Anderson4D.instDecidablePredR324FirstLeftSelected {m : ℕ} (e₀ : MomentContraction m) (hleft : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired e₀.fst Finset.univ a b) : DecidablePred (r324FirstLeftSelected e₀ hleft)

Equations

• Anderson4D.instDecidablePredR324FirstLeftSelected e₀ hleft i = id inferInstance

theorem Anderson4D.integral_sum_momentSignatureFiber_eq_firstLeft_selected {m : ℕ} (e₀ : MomentContraction m) (hleft : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired e₀.fst Finset.univ a b) (Φ : MomentSignatureFiberAt e₀ → (Fin (2 * m) → T4) → ℝ) (hΦ : ∀ (e : MomentSignatureFiberAt e₀), MeasureTheory.Integrable (Φ e) (MeasureTheory.Measure.pi fun (x : Fin (2 * m)) => paperMeasure)) : (∫ (v : Fin (2 * m) → T4), ∑ e : MomentSignatureFiberAt e₀, Φ e v ∂MeasureTheory.Measure.pi fun (x : Fin (2 * m)) => paperMeasure) = ∑ ω : R324FirstLeftOuterCoordinate e₀ hleft, ∫ (vC : { i : Fin (2 * m) // ¬r324FirstLeftSelected e₀ hleft i } → T4), ∫ (vB : { i : Fin (2 * m) // r324FirstLeftSelected e₀ hleft i } → T4), ∑ κB : R324FirstLeftBlockCoordinate e₀ hleft, Φ (r324FirstLeftReconstruct e₀ hleft ω κB) ((MeasurableEquiv.piEquivPiSubtypeProd (fun (x : Fin (2 * m)) => T4) (r324FirstLeftSelected e₀ hleft)).symm (vB, vC)) ∂MeasureTheory.Measure.pi fun (x : { i : Fin (2 * m) // r324FirstLeftSelected e₀ hleft i }) => paperMeasure ∂MeasureTheory.Measure.pi fun (x : { i : Fin (2 * m) // ¬r324FirstLeftSelected e₀ hleft i }) => paperMeasure

Exact signed first-left phase-A Fubini identity.

The complete primitive pairing sum stays inside the selected-coordinate integral. All complementary spatial coordinates and all dependent discrete data stay outside. No norm, triangle inequality, or residual signature grouping occurs in this identity.