in
plain-language theorem explainer
The field-curvature identity equates the J-cost Dirichlet energy laplacian_action on a weighted ledger graph G with conformal spacing a to the Regge sum scaled by the inverse Einstein coupling. Researchers deriving classical gravity from discrete recognition structures cite it when they require the precise coupling value 8 φ^5. The result assembles the cubic deficit discharge, the jcost-to-regge normalization, and the upstream quadratic remainder bound into an unconditional statement.
Claim. For any weighted ledger graph $G$, conformal spacing $a > 0$, and log-potential field $ε$, the J-cost Dirichlet energy satisfies laplacian_action$(G, ε) = (1/κ_Einstein) · regge_sum$, where $κ_Einstein = 8 φ^5$ is the Einstein gravitational coupling in RS-native units ($c=1$).
background
This module forms Phase D of the program to turn the paper's Theorem 5.1 into an unconditional Lean theorem. It composes the exact discharge of ReggeDeficitLinearizationHypothesis on the cubic lattice, the identification of bridge normalization with κ_Einstein from the jcost-to-regge factor, and the quadratic-remainder bound J_log_quadratic_approx proved upstream in Gravity/CubicReggeProof. The local setting is the simplicial ledger where the J-cost functional supplies the Dirichlet energy whose continuum limit recovers the Einstein equations with the derived coupling. Upstream results include the packing of models into CPMBridge structures for traceability and the first-principles derivation of Newton's constant $G = λ_rec^2 c^3 / (π ħ)$.
proof idea
The proof is a direct composition of three prior results: cubic_linearization_discharge supplies the exact linearized Regge sum on the conformal edge lengths, jcost_to_regge_factor_eq_kappa_einstein identifies the normalization factor with κ_Einstein = 8 φ^5, and the quadratic remainder bound closes the approximation error. No new tactics appear; the declaration assembles the upstream lemmas without additional steps.
why it matters
This supplies the exact linearized identity with the physical Einstein coupling and forms the core of the unified certificate ContinuumFieldCurvatureCert that downstream papers cite. It implements the paper's Theorem 5.1 together with Theorem 6.1 on bridge normalization. Within the Recognition framework it links the J-uniqueness fixed point and phi-ladder to the emergence of three spatial dimensions and the gravitational constant $G = φ^5 / π$. It leaves open the quantitative O(a²) convergence for the full nonlinear Regge action, deferred to Phase C.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.