Actual primitive certificates for production R-322

Edge certificates control kernels only away from the identity. This file keeps that distinction exact: the raw primitive kernel is replaced at one point only inside the collapse integral, where the diagonal is null.

theorem Anderson4D.ae_fst_ne_snd_paperMeasure : ∀ᵐ (p : T4 × T4) ∂paperMeasure.prod paperMeasure, p.1 ≠ p.2

The diagonal in the two-endpoint paper product is null.

theorem Anderson4D.r322CollapseIntegrand_offDiagonalRepresentative_ae_eq (Gp J Gr : T4 → ℝ) (u : T4) : r322CollapseIntegrand Gp (offDiagonalRepresentative J) Gr u =ᵐ[paperMeasure.prod paperMeasure] r322CollapseIntegrand Gp J Gr u

Zeroing the primitive input at the identity changes the collapse integrand only on the null endpoint diagonal.

theorem Anderson4D.r322Collapse_offDiagonalRepresentative (Gp J Gr : T4 → ℝ) (u : T4) : r322Collapse Gp (offDiagonalRepresentative J) Gr u = r322Collapse Gp J Gr u

theorem Anderson4D.measurable_offDiagonalRepresentative {J : T4 → ℝ} (hJ : Measurable J) : Measurable (offDiagonalRepresentative J)

theorem Anderson4D.exists_r322Collapse_le_scaled_middle_offDiagonal {supportConstant : ℝ} (hsupport : 0 < supportConstant) : ∃ (K : ℝ), 0 < K ∧ ∀ (C lam ε A Jscale : ℝ) (n : ℕ) (Gp J : T4 → ℝ) (x : T4), 0 ≤ C → 0 ≤ lam → 0 ≤ A → 0 < Jscale → 0 < ε → ε ≤ 1 → 1 ≤ |Real.log ε| → x ≠ 0 → Measurable J → MemEClassT4 J → (∀ (u : T4), u ≠ 0 → |J u| ≤ Jscale * primitiveKernelMajorant C lam ε supportConstant n u) → (∀ (z : T4), z ≠ 0 → |Gp z| ≤ A * invSqKer z) → MeasureTheory.Integrable (r322CollapseIntegrand Gp J greenFn x) (paperMeasure.prod paperMeasure) → |r322Collapse Gp J greenFn x| ≤ A * Jscale * (C * lam) ^ (2 * n) * K * invSqKer x

Scaled one-block closure from an off-diagonal primitive bound. Raw integrability remains an explicit premise and is transported by a.e. equality; it is not inferred from the pointwise majorant.

theorem Anderson4D.primitiveKernelDiff_le_prod_edgeScales_mul_majorant_offDiagonal (ρ : SmoothCutoff) {lam ε supportConstant primitiveConstant : ℝ} {n : ℕ} (hn : 1 ≤ n) (G : Fin (2 * n - 1) → T4 → ℝ) (Cedge : Fin (2 * n - 1) → ℝ) (hCedge : ∀ (j : Fin (2 * n - 1)), 0 < Cedge j) (hmem : ∀ (j : Fin (2 * n - 1)), MemEClassT4 (G j)) (hbound : ∀ (j : Fin (2 * n - 1)) (z : T4), z ≠ 0 → |G j z| ≤ Cedge j * invSqKer z) (hprop : ∀ (H : Fin (2 * n - 1) → T4 → ℝ), IsAdmissiblePrimitiveInput n H → MemEClassT4 (primitiveKernelDiff ρ lam ε n hn H) ∧ MemEClassT4 (primitiveKernelInsertedDiff ρ lam ε n hn H) ∧ PrimitiveKernelBounds ρ lam ε n hn H supportConstant primitiveConstant) (z : T4) (hz : z ≠ 0) : |primitiveKernelDiff ρ lam ε n hn G z| ≤ (∏ j : Fin (2 * n - 1), Cedge j) * primitiveKernelMajorant primitiveConstant lam ε supportConstant n z

Product-scale Proposition 4.1 estimate valid away from the external diagonal at every order, including order one.

structure Anderson4D.R322AnalyticPrimitiveCertificate {q : ℕ} {hq : 1 ≤ q} (ctx : R322AnalyticProperStepContext q hq) (scale : Fin (2 * q - 1) → ℝ) (ρ : SmoothCutoff) (C lam ε supportConstant : ℝ) : Prop

The actual primitive kernel data consumed by a production proper step. Integrability is intentionally a field, not a derived claim.

• measurable : Measurable (primitiveKernelDiff ρ lam ε (residualBlockOrder ctx.step.2) ⋯ ctx.internalEdges)
• memE : MemEClassT4 (primitiveKernelDiff ρ lam ε (residualBlockOrder ctx.step.2) ⋯ ctx.internalEdges)
• bound (u : T4) : u ≠ 0 → |primitiveKernelDiff ρ lam ε (residualBlockOrder ctx.step.2) ⋯ ctx.internalEdges u| ≤ r322AnalyticInternalEdgeScaleProduct ctx scale * primitiveKernelMajorant C lam ε supportConstant (residualBlockOrder ctx.step.2) u
• integrable (x : T4) : x ≠ 0 → MeasureTheory.Integrable (r322CollapseIntegrand (ctx.state.edges ctx.predecessorEdge) (primitiveKernelDiff ρ lam ε (residualBlockOrder ctx.step.2) ⋯ ctx.internalEdges) greenFn x) (paperMeasure.prod paperMeasure)

theorem Anderson4D.R322AnalyticEdgeCertificate.primitiveCertificate {q : ℕ} {hq : 1 ≤ q} {ctx : R322AnalyticProperStepContext q hq} {scale : Fin (2 * q - 1) → ℝ} (hcert : R322AnalyticEdgeCertificate ctx.state scale) (ρ : SmoothCutoff) (C lam ε supportConstant : ℝ) (hmeas : Measurable (primitiveKernelDiff ρ lam ε (residualBlockOrder ctx.step.2) ⋯ ctx.internalEdges)) (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) (hint : ∀ (x : T4), x ≠ 0 → MeasureTheory.Integrable (r322CollapseIntegrand (ctx.state.edges ctx.predecessorEdge) (primitiveKernelDiff ρ lam ε (residualBlockOrder ctx.step.2) ⋯ ctx.internalEdges) greenFn x) (paperMeasure.prod paperMeasure)) : R322AnalyticPrimitiveCertificate ctx scale ρ C lam ε supportConstant

Proposition 4.1 plus explicit raw measurability and integrability premises produce the actual primitive certificate.

theorem Anderson4D.exists_r322AnalyticEdgeCertificate_updateProper_internalProduct_offDiagonal {supportConstant : ℝ} (hsupport : 0 < supportConstant) : ∃ (K : ℝ), 0 < K ∧ ∀ (ρ : SmoothCutoff) (C lam ε : ℝ) (q : ℕ) (hq : 1 ≤ q) (κ : PartialPairing (Fin (2 * q))) (hκ : κ ∈ nonSplitPairings q) (ctx : R322AnalyticProperStepContext q hq), R322AnalyticAbsorbedState ρ lam ε hq κ hκ ctx.state → ctx.pairing = κ → ∀ (scale : Fin (2 * q - 1) → ℝ), R322AnalyticEdgeCertificate ctx.state scale → R322AnalyticPrimitiveCertificate ctx scale ρ C lam ε supportConstant → 0 < C → 0 < lam → 0 < ε → ε ≤ 1 → 1 ≤ |Real.log ε| → R322AnalyticEdgeCertificate (ctx.nextState ρ lam ε) (r322AnalyticUpdatedEdgeScale ctx scale (r322AnalyticInternalEdgeScaleProduct ctx scale) C lam K)

One-step production closure driven by an actual off-diagonal primitive certificate.