pith. machine review for the scientific record. sign in
theorem proved term proof high

field_curvature_identity_simplicial

show as:
view Lean formalization →

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.

claimLet $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 in Recognition Science

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.

scope and limits

formal statement (Lean)

 133theorem field_curvature_identity_simplicial {n : ℕ}
 134    (D : DeficitAngleFunctional n) (a : ℝ) (ha : 0 < a)
 135    (hinges : List (HingeDatum n)) (G : WeightedLedgerGraph n)
 136    (hCal : CalibratedAgainstGraph D a ha hinges G)
 137    (ε : LogPotential n) :
 138    laplacian_action G ε
 139    = (1 / jcost_to_regge_factor) *
 140        regge_sum D (conformal_edge_length_field a ha ε) hinges :=

proof body

Term-mode proof.

 141  field_curvature_identity_under_linearization D a ha hinges G
 142    (simplicial_linearization_discharge D a ha hinges G hCal) ε
 143
 144/-- **THE FIELD-CURVATURE IDENTITY (Einstein-coupling, simplicial).**
 145    Same as above but with the coupling written as
 146    `Constants.kappa_einstein = 8 φ⁵`, per Phase B's
 147    `jcost_to_regge_factor_eq_kappa_einstein`. -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (21)

Lean names referenced from this declaration's body.