One genuine first-left routing step for the physical R-324 core

This module starts from the original deterministicMomentIntegrand, not from a packaged post-collapse object. It reindexes one realized within-half signature fibre, puts the selected spatial block inside all complementary coordinates, and forms the complete primitive covariance sum there before any norm is taken.

This is the exact representation-order step preceding an analytic block collapse. The selected-Green factorization through the heterogeneous detJWith input of integral_completePrimitiveAtEndpoints_eq_replacementEdge, together with the iteration over the other within-half blocks, forms the residual bridge.

Bochner-valued signature routing

theorem Anderson4D.integral_sum_momentSignatureFiber_eq_firstLeft_selected_bochner {m : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (e₀ : MomentContraction m) (hleft : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired e₀.fst Finset.univ a b) (Φ : MomentSignatureFiberAt e₀ → (Fin (2 * m) → T4) → E) (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

Bochner-valued form of the exact first-left signature Fubini step. The selected primitive pairing coordinate is summed inside its selected spatial integral, while all dependent discrete data and complementary spatial coordinates remain outside.

The original physical deterministic fibre

theorem Anderson4D.integral_sum_deterministicMomentIntegrand_eq_firstLeft_primitive {m : ℕ} (ρ : SmoothCutoff) (ε : ℝ) (α β : Z4) (e₀ : MomentContraction m) (hleft : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired e₀.fst Finset.univ a b) (x y z w : T4) (hint : ∀ (e : MomentSignatureFiberAt e₀), MeasureTheory.Integrable (fun (v : Fin (2 * m) → T4) => deterministicMomentIntegrand ρ ε m α β (↑e).fst (↑e).snd.fst (↑e).snd.snd x y z w v) (MeasureTheory.Measure.pi fun (x : Fin (2 * m)) => paperMeasure)) : (∫ (v : Fin (2 * m) → T4), ∑ e : MomentSignatureFiberAt e₀, deterministicMomentIntegrand ρ ε m α β (↑e).fst (↑e).snd.fst (↑e).snd.snd x y z w 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), have v := (MeasurableEquiv.piEquivPiSubtypeProd (fun (x : Fin (2 * m)) => T4) (r324FirstLeftSelected e₀ hleft)).symm (vB, vC); r324FirstLeftOuterFactor ρ ε α β e₀ hleft ω x y z w v * ∑ κB : R324FirstLeftBlockCoordinate e₀ hleft, ↑(primitiveCovarianceProduct ρ ε (residualBlockOrder (selectedExtractionBlock e₀.fst Finset.univ hleft)) ↑κB fun (i : Fin (2 * residualBlockOrder (selectedExtractionBlock e₀.fst Finset.univ hleft))) => v (leftMomentIndex ↑((residualPrimitiveBlockOrderIso e₀.fst (selectedExtractionBlock e₀.fst Finset.univ hleft) ⋯) i))) ∂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

One actual signed phase-A representation-order step.

For one realized first-left block, the original deterministic contraction fibre is routed through the exact selected-coordinate product measure. Inside that integral the selected pairing coordinate is the complete primitive covariance sum, multiplied by the genuine complementary factor from the original integrand. No covariance is Fourier-expanded and no absolute value is introduced.

The section-integrability hypothesis is the precise Fubini premise. It is available for almost every endpoint quadruple from the already proved joint physical integrability; upgrading it to the endpoint-integrated global iteration is left to the next bridge.