bridge_chain_complete
plain-language theorem explainer
The theorem asserts that on any weighted ledger graph the linearized Regge deficit equals the J-cost Dirichlet energy scaled by the Einstein coupling, with exact identity and flat-vacuum vanishing. Recognition Science derivations of general relativity and discrete gravity models cite it as the unconditional bridge from the functional equation to the continuum Einstein equations. The proof is a term-mode composition of the cubic linearization discharge lemma with the field-curvature identity and the pre-proved coupling constants.
Claim. Let $n$ be a natural number, $a>0$ a real, and $G$ a weighted ledger graph on $n$ sites. The Regge deficit linearization hypothesis holds for the cubic deficit functional at scale $a$ with the cubic hinges of $G$. For every log-potential $ε$, the Laplacian action of $G$ on $ε$ equals $(1/κ_E)$ times the Regge sum of the cubic deficit evaluated on the conformal edge-length field generated by $a$ and $ε$. Both sides are zero when $ε$ is identically zero. The Einstein coupling satisfies $κ_E=8φ^5>0$.
background
The module completes Phase D of the program to render the paper's Theorem 5.1 (field-curvature identity) as an unconditional Lean theorem. It composes the cubic linearization discharge (Phase A) with the identification of the bridge normalization to the Einstein coupling $κ_E=8φ^5$ (Phase B) and the upstream quadratic-remainder bound $J_log_quadratic_approx$. The Laplacian action is the Dirichlet energy built from the J-cost functional; the Regge sum is the linearized deficit on the conformal edge-length field. The constants module supplies $κ_E=8φ^5$ via the RS-native derivation $G=λ_rec^2 c^3/(π ħ)$ with $ħ=φ^{-5}$.
proof idea
The proof is a term-mode one-line wrapper. It applies cubic_linearization_discharge to discharge the linearization hypothesis, then invokes field_curvature_identity_einstein for the exact scaling identity, and pairs laplacian_action_flat with flat_regge_sum_zero for the vacuum case. The two constant lemmas kappa_einstein_eq and kappa_einstein_pos are inserted directly.
why it matters
This declaration supplies the single artifact (ContinuumFieldCurvatureCert) that downstream work cites when invoking the field-curvature identity with the derived Einstein coupling. It closes the chain from the Recognition Composition Law through J-uniqueness and the forced value of φ to the continuum limit of the Regge action. The result is unconditional and contains no new axioms or hidden hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.