Constructive closure of Proposition 3.5(b)

This file removes the qualitative interfaces from the proof of paper (3.24). Joint spatial integrability is supplied by the increasing-tree proof in R324DetIntegrability, while the exact noise contraction law is the concrete mollified Wick theorem.

Two genuinely quantitative parts of paper §4.2 remain explicit in the final theorem:

• pointwise domination of each constructed fixed-signature physical density by the Proposition 4.1 inserted majorant;
• construction of the finite routed frequency decomposition from Step 4.

They are stated directly, rather than hidden in a new output structure.

Qualitative R-324 and Wick closure

theorem Anderson4D.integrable_r324Flatten_pairingMomentDeterministicFactor (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (m : ℕ) (α β : Z4) (κp κm : PartialPairing (Fin m)) : MeasureTheory.Integrable (r324Flatten (pairingMomentDeterministicFactor ρ ε m α β κp κm)) (r324PhysicalMeasure m)

The four unit-modulus Fourier characters do not affect joint integrability of the bare doubled deterministic profile.

theorem Anderson4D.pmCoeffMomentFubiniOutput_of_r324 (M : NoiseModel) (ρ : SmoothCutoff) (lam : ℝ) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (m : ℕ) (α β : Z4) : PmCoeffMomentFubiniOutput M ρ lam ε m α β

The complete Fubini output for one order and mode pair follows from the constructed R-324 integrability theorems; no analytic output predicate is assumed.

theorem Anderson4D.integral_norm_sq_pmCoeff_eq_deterministicMomentPairingSum_of_r324 (M : NoiseModel) (ρ : SmoothCutoff) (lam : ℝ) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (m : ℕ) (α β : Z4) : ↑(∫ (ω : M.Ω), ‖pmCoeff M ρ lam ε m α β ω‖ ^ 2) = deterministicMomentPairingSum ρ lam ε m α β

Exact second-moment identity with both the Fubini and Wick inputs instantiated by their concrete constructions.

theorem Anderson4D.memLp_pmCoeff_of_r324 (M : NoiseModel) (ρ : SmoothCutoff) (lam : ℝ) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (m : ℕ) (α β : Z4) : MeasureTheory.MemLp (pmCoeff M ρ lam ε m α β) 2 MeasureTheory.volume

Concrete qualitative half of P-3.5(b): every coefficient belongs to L², without assuming a Fubini or random-integrability interface.

Quantitative P-3.5(b) closure

theorem Anderson4D.exists_parametrix_coeff_bound_of_physical_r324_and_routing {blockConstant supportConstant : ℝ} (hblock : 0 < blockConstant) (hsupport : 0 < supportConstant) : ∃ (outerConstant : ℝ), 0 < outerConstant ∧ ∀ (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (m : ℕ) (α β : Z4), 0 ≤ lam → 0 < ε → ε ≤ 1 / 4 → 1 ≤ |Real.log ε| → 1 ≤ m → (∀ s ∈ momentContractionSignatures m, ∀ (x : T4), |lamEps lam ε| ^ (2 * m) * momentSignaturePhysicalDensity ρ ε m α β s x ≤ primitiveInsertedMajorant blockConstant lam ε supportConstant m x) → RoutedMomentReductionOutput ρ lam ε m α β (lamEps lam ε ^ 2 * outerConstant * (4 * blockConstant * lam) ^ (2 * m - 2)) → MeasureTheory.MemLp (pmCoeff M ρ lam ε m α β) 2 MeasureTheory.volume ∧ ∫ (ω : M.Ω), ‖pmCoeff M ρ lam ε m α β ω‖ ^ 2 ≤ deterministicMomentRHS outerConstant (4 * blockConstant) lam ε m α β

P-3.5(b) with every qualitative premise discharged and only the two literal missing estimates from §4.2 left as hypotheses.

The first hypothesis is exactly the pointwise block-collapse estimate needed by MomentPhysicalFiberReductionData.toMomentFiberReductionData. The second is the concrete finite frequency-routing output of Step 4. No bound on pmCoeff or on deterministicMomentPairingSum is assumed.