Exact pointwise normalization of one refined R-324 root

Before taking a norm or integrating any endpoint, the exact primitive coordinate fibre splits into the two Definition 3.1 within-half factors and the remaining cross-cut factors. This module rewrites the two within-half products as the certified initial R-322 residual traces.

The two embedded within-half list products

theorem Anderson4D.r324LeftPrimitiveBlockProduct_eq_r322 {m : ℕ} (ρ : SmoothCutoff) (ε : ℝ) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (v : Fin (2 * m) → T4) : (List.map (fun (B : Finset (Fin (2 * m))) => r324PrimitivePartitionBlockSum ρ ε κp κm π B v) (momentLeftExtractionBlocks κp)).prod = ∏ B : ExtractionBlockIndex κp, r322ExtractionBlockPrimitiveSum ρ ε κp B fun (i : Fin m) => v (leftMomentIndex i)

The left family in the unified doubled partition is exactly the complete R-322 primitive product of the first contraction.

theorem Anderson4D.r324RightPrimitiveBlockProduct_eq_r322 {m : ℕ} (ρ : SmoothCutoff) (ε : ℝ) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (v : Fin (2 * m) → T4) : (List.map (fun (B : Finset (Fin (2 * m))) => r324PrimitivePartitionBlockSum ρ ε κp κm π B v) (momentRightExtractionBlocks κm)).prod = ∏ B : ExtractionBlockIndex κm, r322ExtractionBlockPrimitiveSum ρ ε κm B fun (i : Fin m) => v (rightMomentIndex i)

The right family in the unified doubled partition is exactly the complete R-322 primitive product of the second contraction.

The exact refined root

noncomputable def Anderson4D.r324ResidualPrimitiveSumProduct {m : ℕ} (ρ : SmoothCutoff) (ε : ℝ) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (v : Fin (2 * m) → T4) : ℝ

Product of the complete primitive sums on the remaining nonempty cross-cut blocks.

Equations

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

theorem Anderson4D.sum_refinedCovariance_eq_twoHalfProducts_mul_residual (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) {s r : Finset (Fin (2 * m)) × Finset (Fin (2 * m))} (e₀ : MomentContraction m) (he₀ : e₀ ∈ momentRefinedContractionFiber m s r) (v : Fin (2 * m) → T4) : ∑ e ∈ momentRefinedContractionFiber m s r, primitiveCovarianceProduct ρ ε m (momentCombinedPairing e.fst e.snd.fst e.snd.snd) v = ((∏ B : ExtractionBlockIndex e₀.fst, r322ExtractionBlockPrimitiveSum ρ ε e₀.fst B fun (i : Fin m) => v (leftMomentIndex i)) * ∏ B : ExtractionBlockIndex e₀.snd.fst, r322ExtractionBlockPrimitiveSum ρ ε e₀.snd.fst B fun (i : Fin m) => v (rightMomentIndex i)) * r324ResidualPrimitiveSumProduct ρ ε e₀.fst e₀.snd.fst e₀.snd.snd v

The exact real covariance sum in one residual-refined fibre is the product of the two complete within-half R-322 factors and the remaining cross-cut factors.

theorem Anderson4D.momentRefinedPhysicalIntegrand_eq_twoInitialResiduals_mul_cross (ρ : SmoothCutoff) (lam ε : ℝ) (m : ℕ) (α β : Z4) (s r : Finset (Fin (2 * m)) × Finset (Fin (2 * m))) (e₀ : MomentContraction m) (he₀ : e₀ ∈ momentRefinedContractionFiber m s r) (x y z w : T4) (v : Fin (2 * m) → T4) : momentRefinedPhysicalIntegrand ρ ε m α β s r x y z w v = momentFourierPhase α β x y z w * ↑((R324WithinHalfResidualPrefix.initial ρ lam ε e₀.fst).residualIntegrand ρ ε x y fun (i : Fin m) => v (leftMomentIndex i)) * ↑((R324WithinHalfResidualPrefix.initial ρ lam ε e₀.snd.fst).residualIntegrand ρ ε z w fun (i : Fin m) => v (rightMomentIndex i)) * ↑(r324ResidualPrimitiveSumProduct ρ ε e₀.fst e₀.snd.fst e₀.snd.snd v)

Pointwise signed normal form of one exact refined root. The two within-half factors are the genuine initial R-322 residual integrands; the cross-cut primitive sums remain outside for the subsequent §4.2 routing.

Schedule form for the next routing stage

theorem Anderson4D.r324ResidualPrimitiveSumProduct_eq_nestedSchedule {m : ℕ} (ρ : SmoothCutoff) (ε : ℝ) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (v : Fin (2 * m) → T4) : r324ResidualPrimitiveSumProduct ρ ε κp κm π v = (List.map (fun (block : R324NestedCrossBlock κp κm π) => r324PrimitivePartitionBlockSum ρ ε κp κm π block.carrier v) (r324NestedCrossSchedule κp κm π)).prod

The residual product can be read directly along the canonical nested cross schedule.