field_curvature_identity_simplicial
plain-language theorem explainer
The simplicial field-curvature identity equates the J-cost Dirichlet energy (Laplacian action) on a weighted ledger graph to one over the J-cost-to-Regge conversion factor times the Regge sum of a calibrated deficit-angle functional evaluated on the conformal edge-length field. Researchers deriving discrete gravity or Regge calculus from recognition principles cite this as the general simplicial bridge to the continuum identity. The proof is a one-line term wrapper that composes the general linearization identity with the calibration discharge.
Claim. Let $D$ be a deficit-angle functional calibrated against weighted ledger graph $G$ (i.e., its Regge sum on the conformal edge-length field equals the conversion factor times the Laplacian action of $G$ for every log-potential). Then for scale $a>0$ and any log-potential $ε$, the Laplacian action of $G$ on $ε$ equals one over the conversion factor times the Regge sum of $D$ on the conformal field generated by $a$ and $ε$.
background
This declaration sits in the Simplicial Deficit Discharge module (Phase C5), whose MODULE_DOC states it composes Phases C1–C4 to prove the paper's Theorem 5.1 as a Lean theorem for general simplicial complexes. CalibratedAgainstGraph is the key sibling definition: it asserts that for all log-potentials $ε$ the Regge sum of $D$ on the conformal edge-length field equals jcost_to_regge_factor times laplacian_action of $G$. The module DOC further notes that this calibration is the cleanest way to state the general result without re-plumbing the entire simplicial-graph correspondence, and that Phase A's cubic case is recovered when $D$ is the cubic deficit functional.
proof idea
The proof is a one-line term-mode wrapper: it feeds the calibration hypothesis hCal into simplicial_linearization_discharge to obtain the ReggeDeficitLinearizationHypothesis, then applies the upstream field_curvature_identity_under_linearization (from EdgeLengthFromPsi) to that discharged hypothesis and the given $ε$. No additional tactics or reductions are required.
why it matters
It supplies the general simplicial form of the field-curvature identity and is the direct parent of the Einstein-coupled specialization field_curvature_identity_simplicial_einstein. The MODULE_DOC explicitly ties it to paper Theorem 5.1 (field-curvature identity) and the upgrade of the algebraic-form argument to piecewise-flat Regge calculus. In the Recognition framework it realizes the bridge from J-cost Dirichlet energy (T5 J-uniqueness) through the eight-tick octave to the discrete Einstein equations via the Regge action and the conversion factor that equals kappa_einstein.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.