ContinuumFieldCurvatureCert
plain-language theorem explainer
The ContinuumFieldCurvatureCert structure bundles the discharge of the Regge linearization hypothesis on cubic deficits, the exact identity equating the J-cost Laplacian action to the Einstein-scaled Regge sum, flat-vacuum consistency checks, and the explicit coupling value kappa_Einstein = 8 phi^5. Researchers invoking the continuum field-curvature identity from Recognition Science would cite this certificate when referencing paper Theorem 5.1. It is assembled by direct packaging of upstream discharge and bridge-normalization lemmas with no in
Claim. A structure certifying that for every natural number $n$, positive real $a$, and weighted ledger graph $G$, the Regge deficit linearization hypothesis holds for the cubic deficit functional; the Laplacian action of $G$ on any log-potential equals $(1/κ_E)$ times the Regge sum evaluated on the conformal edge-length field generated by that potential; both the Laplacian and Regge sum vanish for the zero potential; and $κ_E = 8φ^5 > 0$.
background
This module completes Phase D toward making the paper's Theorem 5.1 (field-curvature identity) an unconditional Lean theorem. It composes the cubic linearization discharge from CubicDeficitDischarge.cubic_linearization_discharge with the bridge normalization from EdgeLengthFromPsi.jcost_to_regge_factor_eq_kappa_einstein. WeightedLedgerGraph is a finite simplicial graph equipped with positive edge weights; LogPotential n is a real-valued function on its vertices; laplacian_action G ε is the J-cost Dirichlet energy; regge_sum computes the linearized Regge deficit; conformal_edge_length_field a ha ε produces the edge lengths from the potential.
proof idea
This is a structure definition with an empty proof body. The downstream theorem continuumFieldCurvatureCert constructs an instance by supplying cubic_linearization_discharge for the discharge field, field_curvature_identity_einstein for the identity field, laplacian_action_flat for flat_jcost, flat_regge_sum_zero for flat_regge, and Constants.kappa_einstein_eq together with positivity for the coupling fields.
why it matters
This declaration supplies the single citable artifact for the field-curvature identity at the Einstein coupling. It is the parent of the theorem continuumFieldCurvatureCert and realizes paper Theorem 5.1 by identifying the J-cost bridge factor with κ_Einstein = 8φ^5. The construction links directly to the Recognition Composition Law and the T5 J-uniqueness fixed point while closing the Phase D scaffolding for the continuum limit with zero new axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.