Quantitative certificates for production R-322 edge states

The primitive kernel is built from the current heterogeneous internal edges. Its complete product scale is therefore charged to the predecessor edge at every proper collapse.

structure Anderson4D.R322AnalyticEdgeCertificate {q : ℕ} {hq : 1 ≤ q} (state : R322AnalyticEdgeState q hq) (scale : Fin (2 * q - 1) → ℝ) : Prop

• scale_pos (edge : Fin (2 * q - 1)) : 0 < scale edge
• memE (edge : Fin (2 * q - 1)) : MemEClassT4 (state.edges edge)
• bound (edge : Fin (2 * q - 1)) (z : T4) : z ≠ 0 → |state.edges edge z| ≤ scale edge * invSqKer z

@[simp]

theorem Anderson4D.r322CollapseIntegrand_const_mul_middle (c : ℝ) (Gp J Gr : T4 → ℝ) (u : T4) (p : T4 × T4) : r322CollapseIntegrand Gp (fun (z : T4) => c * J z) Gr u p = c * r322CollapseIntegrand Gp J Gr u p

theorem Anderson4D.r322Collapse_const_mul_middle (c : ℝ) (Gp J Gr : T4 → ℝ) (u : T4) : r322Collapse Gp (fun (z : T4) => c * J z) Gr u = c * r322Collapse Gp J Gr u

The collapse is linear in its middle (primitive-kernel) input.

theorem Anderson4D.exists_r322Collapse_le_scaled_middle {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), |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

Scale-covariant form of the one-block estimate. Only the raw integrability hypothesis is needed: integrability after normalization follows by multiplication by Jscale⁻¹.

def Anderson4D.r322AnalyticInternalEdgeScaleProduct {q : ℕ} {hq : 1 ≤ q} (ctx : R322AnalyticProperStepContext q hq) (scale : Fin (2 * q - 1) → ℝ) : ℝ

At a proper step, the raw primitive scale is the product of all current internal heterogeneous edge scales.

Equations

• Anderson4D.r322AnalyticInternalEdgeScaleProduct ctx scale = ∏ j : Fin (2 * Anderson4D.residualBlockOrder ctx.step.2 - 1), scale (ctx.internalEdge j)

theorem Anderson4D.R322AnalyticEdgeCertificate.internalEdgeScaleProduct_pos {q : ℕ} {hq : 1 ≤ q} {ctx : R322AnalyticProperStepContext q hq} {scale : Fin (2 * q - 1) → ℝ} (hcert : R322AnalyticEdgeCertificate ctx.state scale) : 0 < r322AnalyticInternalEdgeScaleProduct ctx scale

def Anderson4D.r322AnalyticUpdatedEdgeScale {q : ℕ} {hq : 1 ≤ q} (ctx : R322AnalyticProperStepContext q hq) (scale : Fin (2 * q - 1) → ℝ) (Jscale C lam K : ℝ) : Fin (2 * q - 1) → ℝ

Exact ledger update: predecessor scale, raw internal-edge product, block order power, and universal collapse constant are each charged once.

Equations

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

@[simp]

theorem Anderson4D.r322AnalyticUpdatedEdgeScale_predecessor {q : ℕ} {hq : 1 ≤ q} (ctx : R322AnalyticProperStepContext q hq) (scale : Fin (2 * q - 1) → ℝ) (Jscale C lam K : ℝ) : r322AnalyticUpdatedEdgeScale ctx scale Jscale C lam K ctx.predecessorEdge = scale ctx.predecessorEdge * Jscale * (C * lam) ^ (2 * residualBlockOrder ctx.step.2) * K

theorem Anderson4D.r322AnalyticUpdatedEdgeScale_of_ne {q : ℕ} {hq : 1 ≤ q} (ctx : R322AnalyticProperStepContext q hq) (scale : Fin (2 * q - 1) → ℝ) (Jscale C lam K : ℝ) (edge : Fin (2 * q - 1)) (hne : edge ≠ ctx.predecessorEdge) : r322AnalyticUpdatedEdgeScale ctx scale Jscale C lam K edge = scale edge

theorem Anderson4D.R322AnalyticProperStepContext.nextState_edges_eq_of_ne {q : ℕ} {hq : 1 ≤ q} (ctx : R322AnalyticProperStepContext q hq) (ρ : SmoothCutoff) (lam ε : ℝ) (edge : Fin (2 * q - 1)) (hne : edge ≠ ctx.predecessorEdge) : (ctx.nextState ρ lam ε).edges edge = ctx.state.edges edge

theorem Anderson4D.exists_r322InitialAnalyticEdgeCertificate (q : ℕ) (hq : 1 ≤ q) : ∃ (A : ℝ), 0 < A ∧ R322AnalyticEdgeCertificate (r322InitialAnalyticEdgeState q hq) fun (x : Fin (2 * q - 1)) => A

theorem Anderson4D.exists_r322AnalyticEdgeCertificate_updateProper {supportConstant : ℝ} (hsupport : 0 < supportConstant) : ∃ (K : ℝ), 0 < K ∧ ∀ (ρ : SmoothCutoff) (C lam ε Jscale : ℝ) (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 → 0 < C → 0 < lam → 0 < Jscale → 0 < ε → ε ≤ 1 → 1 ≤ |Real.log ε| → Measurable (primitiveKernelDiff ρ lam ε (residualBlockOrder ctx.step.2) ⋯ ctx.internalEdges) → MemEClassT4 (primitiveKernelDiff ρ lam ε (residualBlockOrder ctx.step.2) ⋯ ctx.internalEdges) → (∀ (u : T4), |primitiveKernelDiff ρ lam ε (residualBlockOrder ctx.step.2) ⋯ ctx.internalEdges u| ≤ Jscale * primitiveKernelMajorant C lam ε supportConstant (residualBlockOrder ctx.step.2) u) → (∀ (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)) → R322AnalyticEdgeCertificate (ctx.nextState ρ lam ε) (r322AnalyticUpdatedEdgeScale ctx scale Jscale C lam K)

One proper production update preserves the full slotwise certificate. Unlike the normalized one-block theorem, this production interface explicitly charges the raw primitive scale Jscale.

theorem Anderson4D.exists_r322AnalyticEdgeCertificate_updateProper_internalProduct {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 → 0 < C → 0 < lam → 0 < ε → ε ≤ 1 → 1 ≤ |Real.log ε| → Measurable (primitiveKernelDiff ρ lam ε (residualBlockOrder ctx.step.2) ⋯ ctx.internalEdges) → MemEClassT4 (primitiveKernelDiff ρ lam ε (residualBlockOrder ctx.step.2) ⋯ ctx.internalEdges) → (∀ (u : T4), |primitiveKernelDiff ρ lam ε (residualBlockOrder ctx.step.2) ⋯ ctx.internalEdges u| ≤ r322AnalyticInternalEdgeScaleProduct ctx scale * primitiveKernelMajorant C lam ε supportConstant (residualBlockOrder ctx.step.2) u) → (∀ (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)) → R322AnalyticEdgeCertificate (ctx.nextState ρ lam ε) (r322AnalyticUpdatedEdgeScale ctx scale (r322AnalyticInternalEdgeScaleProduct ctx scale) C lam K)

Production specialization: Jscale is the product of the actual current internal edge scales, rather than an unrelated external normalization.