Fixed-endpoint integrability for production R-322 collapses

This file closes the raw Bochner-integrability field in the production primitive certificate. The proof is pointwise at every nonzero external endpoint; it does not promote the almost-everywhere section supplied by Fubini.

theorem Anderson4D.integrable_r322CollapseIntegrand_of_invSq_add_one {Gp J : T4 → ℝ} {A B Cgreen : ℝ} {x : T4} (hGpMeas : Measurable Gp) (hJMeas : Measurable J) (hA : 0 ≤ A) (hB : 0 ≤ B) (hCgreen : 0 ≤ Cgreen) (hGp : ∀ (z : T4), z ≠ 0 → |Gp z| ≤ A * invSqKer z) (hJ : ∀ (z : T4), z ≠ 0 → |J z| ≤ B * (invSqKer z + 1)) (hgreen : ∀ (z : T4), z ≠ 0 → |greenFn z| ≤ Cgreen * invSqKer z) (hx : x ≠ 0) : MeasureTheory.Integrable (r322CollapseIntegrand Gp J greenFn x) (paperMeasure.prod paperMeasure)

A fixed nonzero endpoint makes the raw proper-block collapse absolutely integrable as soon as its predecessor and middle kernels have the paper's inverse-square bounds. This is a pointwise statement, not an a.e.-section consequence of joint Fubini.

theorem Anderson4D.exists_primitiveKernelMajorant_le_invSq_add_one (C lam ε supportConstant : ℝ) (n : ℕ) (hε : 0 < ε) (hlog : 0 < |Real.log ε|) : ∃ (B : ℝ), 0 ≤ B ∧ ∀ (z : T4), primitiveKernelMajorant C lam ε supportConstant n z ≤ B * (invSqKer z + 1)

At a fixed positive mollification scale, the Proposition 4.1 majorant is bounded by one nonnegative constant times invSqKer + 1. The constant may depend on the scale; only raw integrability is asserted here.

theorem Anderson4D.R322AnalyticAbsorbedState.integrable_stepCollapseIntegrand_offDiagonal {ρ : SmoothCutoff} {C lam ε supportConstant : ℝ} {q : ℕ} {hq : 1 ≤ q} {κ : PartialPairing (Fin (2 * q))} {hκ : κ ∈ nonSplitPairings q} {scale : Fin (2 * q - 1) → ℝ} (ctx : R322AnalyticProperStepContext q hq) (hstate : R322AnalyticAbsorbedState ρ lam ε hq κ hκ ctx.state) (hcert : R322AnalyticEdgeCertificate ctx.state scale) (hε : 0 < ε) (hlog : 0 < |Real.log ε|) (hprop : ∀ (H : Fin (2 * residualBlockOrder ctx.step.2 - 1) → T4 → ℝ), IsAdmissiblePrimitiveInput (residualBlockOrder ctx.step.2) H → MemEClassT4 (primitiveKernelDiff ρ lam ε (residualBlockOrder ctx.step.2) ⋯ H) ∧ MemEClassT4 (primitiveKernelInsertedDiff ρ lam ε (residualBlockOrder ctx.step.2) ⋯ H) ∧ PrimitiveKernelBounds ρ lam ε (residualBlockOrder ctx.step.2) ⋯ H supportConstant C) (x : T4) (hx : x ≠ 0) : MeasureTheory.Integrable (r322CollapseIntegrand (ctx.state.edges ctx.predecessorEdge) (primitiveKernelDiff ρ lam ε (residualBlockOrder ctx.step.2) ⋯ ctx.internalEdges) greenFn x) (paperMeasure.prod paperMeasure)

Reachability, the current edge certificate, and the Proposition 4.1 primitive bound prove raw collapse integrability at every nonzero endpoint. No a.e.-section theorem is used.

theorem Anderson4D.R322AnalyticEdgeCertificate.primitiveCertificate_of_reachable {ρ : SmoothCutoff} {C lam ε supportConstant : ℝ} {q : ℕ} {hq : 1 ≤ q} {κ : PartialPairing (Fin (2 * q))} {hκ : κ ∈ nonSplitPairings q} {ctx : R322AnalyticProperStepContext q hq} {scale : Fin (2 * q - 1) → ℝ} (hstate : R322AnalyticAbsorbedState ρ lam ε hq κ hκ ctx.state) (hcert : R322AnalyticEdgeCertificate ctx.state scale) (hε : 0 < ε) (hlog : 0 < |Real.log ε|) (hprop : ∀ (H : Fin (2 * residualBlockOrder ctx.step.2 - 1) → T4 → ℝ), IsAdmissiblePrimitiveInput (residualBlockOrder ctx.step.2) H → MemEClassT4 (primitiveKernelDiff ρ lam ε (residualBlockOrder ctx.step.2) ⋯ H) ∧ MemEClassT4 (primitiveKernelInsertedDiff ρ lam ε (residualBlockOrder ctx.step.2) ⋯ H) ∧ PrimitiveKernelBounds ρ lam ε (residualBlockOrder ctx.step.2) ⋯ H supportConstant C) : R322AnalyticPrimitiveCertificate ctx scale ρ C lam ε supportConstant

Production constructor for the actual primitive certificate, with its raw integrability field discharged from reachability and Proposition 4.1.