simplicialFieldCurvatureCert
plain-language theorem explainer
The simplicialFieldCurvatureCert theorem supplies the master certificate that any deficit-angle functional calibrated to a weighted ledger graph satisfies the Regge deficit linearization hypothesis. Researchers deriving the Einstein equations from Recognition Science via simplicial Regge calculus cite it as the Phase C5 composition step. Its term-mode proof is a direct wrapper that populates the five structure fields from four sibling results.
Claim. Let $D$ be a deficit-angle functional on $n$ vertices, $a>0$, hinges a list of hinge data, and $G$ a weighted ledger graph. If the per-hinge calibration $A_h·δ_h = (κ/2)·G_{ij}·(ε_i−ε_j)^2$ holds, then the Regge action on the linearized deficit equals $κ$ times the Laplacian action on the conformal ε-field. The certificate also supplies the cubic calibration, the vanishing of the linear Regge term by the Schläfli identity, and the Einstein value $κ=8φ^5$.
background
This declaration lives in the SimplicialDeficitDischarge module, Phase C5 of the program to prove the paper's Theorem 5.1 (field-curvature identity). It composes Phases C1–C4 into a general simplicial discharge of ReggeDeficitLinearizationHypothesis. The local setting is piecewise-flat Regge calculus on a simplicial complex whose hinges are identified one-to-one with edges of a weighted ledger graph; the matching condition equates area-deficit products with J-cost Dirichlet energies per edge.
proof idea
The proof is a term-mode construction that directly supplies the five fields of SimplicialFieldCurvatureCert. Discharge is obtained by applying simplicial_linearization_discharge. The identity field is supplied by field_curvature_identity_simplicial_einstein. Cubic calibration invokes cubic_calibrated_against_graph. The Schläfli linearization vanishing uses linear_regge_vanishes. The kappa value is taken from Constants.kappa_einstein_eq.
why it matters
The theorem completes Phase C by delivering the master certificate for the simplicial field-curvature identity. It directly supports the paper's Theorem 5.1 in Gravity from Recognition §5, upgrading the algebraic-form argument to a theorem about actual piecewise-flat Regge calculus. In the Recognition Science framework it realizes the bridge between J-cost Dirichlet energy on the ledger graph and Regge action, with κ fixed by the phi-ladder at 8φ^5; zero open questions remain in the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.