continuumFieldCurvatureCert
plain-language theorem explainer
continuumFieldCurvatureCert supplies the bundled certificate for the field-curvature identity at the Einstein coupling. Researchers deriving gravity from the Recognition Science functional equation cite this when applying the linearized Regge action to the J-cost Dirichlet energy on the cubic lattice. The term-mode proof assembles six pre-proved components: the cubic discharge lemma, the Einstein-scaled identity, flat vacuum baselines, and the explicit kappa equality plus positivity results.
Claim. The Continuum Field Curvature Certificate holds: for any natural number $n$, positive real $a$, and weighted ledger graph $G$, the Regge deficit linearization hypothesis is discharged for the cubic deficit functional; the J-cost Dirichlet energy equals $(1/κ_{Einstein})$ times the Regge sum on the conformal edge-length field generated by a log potential; the flat-vacuum J-cost and Regge sum vanish; and $κ_{Einstein}=8φ^5>0$.
background
This module completes Phase D toward an unconditional Lean version of the paper's Theorem 5.1. It composes the cubic linearization discharge (Phase A), which discharges the ReggeDeficitLinearizationHypothesis on the cubic lattice, with the bridge normalization to the Einstein coupling (Phase B). Upstream results include the quadratic remainder bound from the Gravity/CubicReggeProof module and the definition $G=λ_{rec}^2 c^3/(π ℏ)$ in Constants, together with the lemmas $κ_{Einstein}=8φ^5$ and $0<κ_{Einstein}$.
proof idea
The proof is a term-mode structure constructor for ContinuumFieldCurvatureCert. It supplies the discharge field by direct application of cubic_linearization_discharge, the identity field by field_curvature_identity_einstein, the flat J-cost baseline by laplacian_action_flat, the flat Regge baseline by flat_regge_sum_zero, and the coupling fields by the equality and positivity lemmas from Constants.
why it matters
This certificate is the single citable artifact for the field-curvature identity in the Recognition framework, as stated in the module documentation. It realizes the composition of the cubic deficit discharge and the jcost-to-regge factor at $κ_{Einstein}=8φ^5$, feeding directly into the paper's Theorem 5.1. The result ties to the forcing chain through J-uniqueness (T5) and the phi fixed point (T6), with the eight-tick octave (T7) and $D=3$ (T8) implicit in the simplicial ledger setup.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.