cubic_calibrated_against_graph
plain-language theorem explainer
The theorem establishes that the cubic deficit functional is calibrated against any weighted ledger graph, so its Regge sum on conformal edge-length fields equals the scaled Laplacian action on the graph. Researchers working on discrete Regge calculus or simplicial models of gravity would cite it when discharging the linearization hypothesis for cubic lattices in the field-curvature identity. The proof is a direct one-line application of the cubic linearization discharge lemma.
Claim. For any natural number $n$, positive real $a$, and weighted ledger graph $G$, the cubic deficit functional satisfies regge_sum $D$ (conformal_edge_length_field $a$ $ha$ $ε$) hinges = jcost_to_regge_factor · laplacian_action $G$ $ε$ for every log-potential $ε$, where the hinges are those of the cubic lattice associated to $G$.
background
The module SimplicialDeficitDischarge forms Phase C5 of the program to prove the paper's Theorem 5.1 (field-curvature identity) as a Lean theorem. It composes earlier phases into a general simplicial discharge of the ReggeDeficitLinearizationHypothesis. CalibratedAgainstGraph is the property that a deficit functional $D$ satisfies regge_sum $D$ on the conformal edge-length field equals the scaled Laplacian action on the ledger graph $G$; the cubic case is supplied explicitly by Phase A while the general case uses Phase C4's linear_regge_vanishes. Upstream results include the RS-native gravitational constant $G = λ_rec² c³ / (π ℏ)$ and the cost functions induced by multiplicative recognizers and observer forcing events, which supply the J-cost Dirichlet energy appearing in the ledger graph.
proof idea
The proof is a one-line wrapper that applies the cubic_linearization_discharge lemma directly to the parameters $a$, $ha$, and $G$.
why it matters
This declaration is invoked inside simplicialFieldCurvatureCert to supply the cubic_calibrated component of the assembled SimplicialFieldCurvatureCert record. It fills the cubic special case of the paper's Theorem 5.1 on the field-curvature identity, extending the linearization result from EdgeLengthFromPsi.lean. In the Recognition Science framework it supports the simplicial discretization in which J-cost Dirichlet energy matches the Regge action, consistent with the eight-tick octave and the derivation of three spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.