Integrated primitive-iteration boundary for R-324

Paper Section 4.2 does not bound a pointwise physical density. Step 2 successively removes the within-half primitive intervals while the physical integrand is signed; Step 3 then integrates the endpoints in the uniform branch and continues with the relative cross-cut primitive blocks. Accordingly, the correct cancellation-preserving output of the complete block iteration is a scalar bound for each residual-refined fibre.

This file supplies the cancellation-preserving downstream API and proves all finite regrouping steps. Its analytic input is the successive primitive-block collapse for one residual-refined fibre; no pointwise domination of momentSignaturePhysicalDensity appears.

The actual integrated refined fibres

noncomputable def Anderson4D.momentRefinedDeterministicTermSum (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (α β : Z4) (s r : Finset (Fin (2 * m)) × Finset (Fin (2 * m))) : ℂ

The already-integrated deterministic contribution of one complete residual-refined contraction fibre.

Equations

• Anderson4D.momentRefinedDeterministicTermSum ρ ε m α β s r = ∑ e ∈ Anderson4D.momentRefinedContractionFiber m s r, Anderson4D.deterministicMomentContractionTerm ρ ε m α β e

theorem Anderson4D.sum_momentRefinedDeterministicTermSum (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (α β : Z4) (s : Finset (Fin (2 * m)) × Finset (Fin (2 * m))) : ∑ r ∈ momentResidualChainSignaturesAt m s, momentRefinedDeterministicTermSum ρ ε m α β s r = ∑ e ∈ momentContractionFiber m s, deterministicMomentContractionTerm ρ ε m α β e

Exact regrouping of one fixed-signature deterministic contribution by the realized residual schedules.

structure Anderson4D.MomentRefinedIntegratedReductionData (ρ : SmoothCutoff) (lam ε : ℝ) (m : ℕ) (α β : Z4) (primitiveConstant supportConstant : ℝ) : Prop

Correct analytic output of the successive block iteration: after the external integrations, one complete residual-refined fibre is bounded by the integral of the inserted Proposition 4.1 majorant.

• refined_bound (s : Finset (Fin (2 * m)) × Finset (Fin (2 * m))) : s ∈ momentContractionSignatures m → ∀ r ∈ momentResidualChainSignaturesAt m s, |lamEps lam ε| ^ (2 * m) * ‖momentRefinedDeterministicTermSum ρ ε m α β s r‖ ≤ ∫ (z : T4), primitiveInsertedMajorant primitiveConstant lam ε supportConstant m z ∂paperMeasure

structure Anderson4D.MomentIntegratedFiberReductionData (ρ : SmoothCutoff) (lam ε : ℝ) (m : ℕ) (α β : Z4) (primitiveConstant supportConstant : ℝ) : Prop

Per-signature integrated output after summing the residual schedules. This scalar statement matches the integration order in paper Section 4.2 Step 3.

• fiber_bound (s : Finset (Fin (2 * m)) × Finset (Fin (2 * m))) : s ∈ momentContractionSignatures m → |lamEps lam ε| ^ (2 * m) * ‖∑ e ∈ momentContractionFiber m s, deterministicMomentContractionTerm ρ ε m α β e‖ ≤ ∫ (z : T4), primitiveInsertedMajorant primitiveConstant lam ε supportConstant m z ∂paperMeasure

theorem Anderson4D.primitiveInsertedMajorant_mul_constant (a C lam ε supportConstant : ℝ) (m : ℕ) (z : T4) : primitiveInsertedMajorant (a * C) lam ε supportConstant m z = a ^ (2 * m) * primitiveInsertedMajorant C lam ε supportConstant m z

Scaling the primitive constant by a scales either majorant by a^(2m).

theorem Anderson4D.MomentRefinedIntegratedReductionData.toIntegratedFiberReductionData {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {α β : Z4} {primitiveConstant supportConstant : ℝ} (hC : 0 ≤ primitiveConstant) (hlam : 0 ≤ lam) (d : MomentRefinedIntegratedReductionData ρ lam ε m α β primitiveConstant supportConstant) : MomentIntegratedFiberReductionData ρ lam ε m α β (4 * primitiveConstant) supportConstant

Sum the independent residual-refined estimates. The exact 4^(2m) schedule count is absorbed by C ↦ 4C; no factorial loss is introduced.

def Anderson4D.MomentIntegratedFiberReductionOutputAt (ρ : SmoothCutoff) (lam ε : ℝ) (m : ℕ) (α β : Z4) (primitiveConstant supportConstant : ℝ) : Prop

Existence wrapper for the corrected fixed-signature output.

Equations

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

def Anderson4D.MomentRefinedIntegratedReductionOutputAt (ρ : SmoothCutoff) (lam ε : ℝ) (m : ℕ) (α β : Z4) (primitiveConstant supportConstant : ℝ) : Prop

Existence wrapper for the corrected residual-refined output.

Equations

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

theorem Anderson4D.MomentRefinedIntegratedReductionOutputAt.toIntegratedFiberReductionOutputAt {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {α β : Z4} {primitiveConstant supportConstant : ℝ} (hC : 0 ≤ primitiveConstant) (hlam : 0 ≤ lam) (h : MomentRefinedIntegratedReductionOutputAt ρ lam ε m α β primitiveConstant supportConstant) : MomentIntegratedFiberReductionOutputAt ρ lam ε m α β (4 * primitiveConstant) supportConstant

Direct uniform bound without the false pointwise density

theorem Anderson4D.deterministicMomentPairingSum_le_integral_insertedMajorant_of_integrated {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {α β : Z4} {primitiveConstant supportConstant : ℝ} (hC : 0 ≤ primitiveConstant) (hlam : 0 ≤ lam) (hred : MomentIntegratedFiberReductionOutputAt ρ lam ε m α β primitiveConstant supportConstant) : ‖deterministicMomentPairingSum ρ lam ε m α β‖ ≤ ∫ (z : T4), primitiveInsertedMajorant (4 * primitiveConstant) lam ε supportConstant m z ∂paperMeasure

Summing the fixed-signature scalar estimates costs the second exact 4^(2m) factor, absorbed once more into the named primitive constant.

theorem Anderson4D.deterministicMomentPairingSum_le_integral_insertedMajorant_of_refined {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {α β : Z4} {primitiveConstant supportConstant : ℝ} (hC : 0 ≤ primitiveConstant) (hlam : 0 ≤ lam) (hred : MomentRefinedIntegratedReductionOutputAt ρ lam ε m α β primitiveConstant supportConstant) : ‖deterministicMomentPairingSum ρ lam ε m α β‖ ≤ ∫ (z : T4), primitiveInsertedMajorant (16 * primitiveConstant) lam ε supportConstant m z ∂paperMeasure

Direct composition from residual-refined scalar collapse to the global uniform deterministic moment bound. The two exponential schedule counts are visible as C ↦ 16C.