SimplicialFieldCurvatureCert
plain-language theorem explainer
The SimplicialFieldCurvatureCert structure assembles the discharge of the Regge linearization hypothesis, the field-curvature identity, cubic calibration, Schläfli vanishing, and the explicit value of kappa_einstein for any calibrated simplicial ledger graph. A researcher proving the discrete Einstein equations from the J-cost functional would cite this certificate when extending the cubic lattice result to general simplicial complexes. The definition packages four universal properties plus the kappa value by direct enumeration of the required
Claim. A structure whose fields assert: (i) if a deficit functional $D$ is calibrated against a weighted ledger graph $G$ then the Regge deficit linearization hypothesis holds for $D$; (ii) the Laplacian action on $G$ equals $(1/κ)$ times the Regge sum of $D$ applied to the conformal edge-length field; (iii) the cubic deficit functional is calibrated against any $G$; (iv) the sum of area times linearized deficit vanishes for any well-shaped data and edge perturbation; (v) $κ = 8φ^5$.
background
Phase C5 composes Phases C1–C4 to prove the field-curvature identity on simplicial complexes. The central auxiliary notion is CalibratedAgainstGraph, which requires that the Regge sum of the deficit functional on the conformal field equals jcost_to_regge_factor times the Laplacian action on the ledger graph. This matching condition is the cleanest way to state the general simplicial result without re-plumbing the entire simplicial-graph correspondence.
proof idea
The structure is introduced by enumerating its five fields, each a universal quantification over deficit functionals, graphs, and perturbations. No tactics are used; the definition directly records the statements that will be instantiated by the cubic and linear cases from sibling declarations such as cubic_calibrated_against_graph and simplicial_linearization_discharge.
why it matters
This certificate is the master object for Phase C, directly feeding the theorem simplicialFieldCurvatureCert which constructs an instance using simplicial_linearization_discharge and field_curvature_identity_simplicial_einstein. It fills the simplicial case of the paper's Theorem 5.1 on the field-curvature identity. In the framework it closes the bridge from the J-cost Dirichlet energy on graphs to the Regge action on piecewise-flat manifolds, with kappa_einstein = 8 phi^5 matching the RS-native Einstein coupling.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.