CalibratedAgainstGraph
plain-language theorem explainer
A deficit angle functional D is calibrated against a weighted ledger graph G when its Regge sum on the conformal edge-length field at scale a equals the conversion constant times the Laplacian action of G, for every log potential. Workers proving the simplicial field-curvature identity cite this definition to state the required matching hypothesis cleanly. The definition consists of a direct universal equality between the two sides.
Claim. A deficit angle functional $D$ is calibrated against a weighted ledger graph $G$ (with scale $a>0$, hinge list, and graph $G$) when, for every log potential $ε$, the Regge sum of $D$ on the conformal edge-length field at scale $a$ equals $κ$ times the Laplacian action of $G$ on $ε$, where $κ$ is the J-cost to Regge conversion factor.
background
This definition sits in the Simplicial Deficit Discharge module, Phase C5 of the program to prove the paper's Theorem 5.1 (field-curvature identity) as a Lean theorem. The module composes Phases C1–C4 by supplying a general simplicial discharge of the ReggeDeficitLinearizationHypothesis. A deficit functional is calibrated against a ledger graph if its Regge sum matches $κ · laplacian_action$ on the conformal $ε$-field; Phase A supplies the cubic case explicitly while Phase C4's linear_regge_vanishes supplies the general case.
proof idea
This is a definition whose body is the single equality ∀ ε : LogPotential n, regge_sum D (conformal_edge_length_field a ha ε) hinges = jcost_to_regge_factor * laplacian_action G ε. No lemmas are applied; the declaration simply names the calibration property that downstream theorems assume via the hypothesis hCal.
why it matters
The definition is invoked by field_curvature_identity_simplicial and field_curvature_identity_simplicial_einstein (which conclude the J-cost Dirichlet energy equals (1/κ) times the Regge action) and by the master certificate SimplicialFieldCurvatureCert. It also feeds refinement_discharge_inherits and cubic_calibrated_against_graph. It clarifies that the matching is a property of the functional itself, directly supporting the paper's Theorem 5.1 upgrade of the algebraic-form argument to piecewise-flat Regge calculus. It touches the T5–T8 forcing chain landmarks via the underlying J-uniqueness and eight-tick structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.