field_curvature_identity_simplicial_einstein
plain-language theorem explainer
The simplicial Einstein field-curvature identity equates the discrete Laplacian action on a log-potential to the Regge sum over a calibrated deficit functional, scaled by the inverse Einstein coupling 8 phi^5. Discrete gravity and Regge calculus researchers cite it when discharging the linearization hypothesis in simplicial settings. The proof is a one-line wrapper that substitutes the Phase B coupling identity and invokes the general simplicial curvature identity.
Claim. Let $D$ be a deficit angle functional calibrated to a weighted ledger graph $G$ by the condition that its Regge sum equals the factor times the Laplacian action on the conformal field. For any log-potential $ε$, the discrete Laplacian satisfies $Δ_G ε = (1/κ) · regge_sum D(ℓ(ε))$, where $κ = κ_{Einstein} = 8φ^5$ and edge lengths are conformal to $ε$.
background
The Simplicial Deficit Discharge module (Phase C5) composes prior phases to discharge the ReggeDeficitLinearizationHypothesis as a Lean theorem. CalibratedAgainstGraph requires that for every log-potential the Regge sum of area times deficit on the conformal edge lengths equals jcost_to_regge_factor times laplacian_action on the graph. laplacian_action is the quadratic J-cost Dirichlet energy: half the sum over edges of weight times squared potential difference. Upstream, kappa_einstein is defined as 8φ^5 from the RS-native G = φ^5/π and the functional equation for J.
proof idea
The proof is a one-line wrapper. It rewrites the scaling factor via jcost_to_regge_factor_eq_kappa_einstein to align with the general form, then applies field_curvature_identity_simplicial exactly.
why it matters
This supplies the Einstein-coupled version of the curvature identity and is invoked directly by simplicialFieldCurvatureCert, the master certificate for Phase C. It fills the algebraic core of Theorem 5.1 in the draft paper Gravity from Recognition. The result connects the J-cost functional equation (T5) to piecewise-flat Regge calculus while fixing the coupling at 8φ^5 from the eight-tick octave and D=3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.