CalibratedAgainstGraph
plain-language theorem explainer
A deficit angle functional D is calibrated against a weighted ledger graph G when the Regge sum of D on the conformal edge-length field equals the jcost-to-Regge factor times the Laplacian action of G for every log-potential ε. Researchers proving the simplicial form of the field-curvature identity cite this equational condition as the general discharge hypothesis. The definition is a direct renaming of the linearization hypothesis with no proof obligations.
Claim. Let $D$ be a deficit angle functional, $a>0$ a scale, hinges a list of hinge data, and $G$ a weighted ledger graph. Then $D$ is calibrated against $G$ when, for every log-potential $ε$, the Regge sum of $D$ evaluated on the conformal edge-length field at scale $a$ equals $κ$ times the Laplacian action of $G$ on $ε$, where $κ$ denotes the jcost-to-Regge conversion factor.
background
This definition sits in the SimplicialDeficitDischarge module, Phase C5 of the program to realize Theorem 5.1 (field-curvature identity) as a Lean theorem. It composes Phases C1–C4 by requiring that any pre-calibrated DeficitAngleFunctional matches the J-cost Dirichlet energy on the ledger graph via the per-hinge identity $A_h · δ_h = (κ/2) · G.weight · (ε_i − ε_j)^2$ under the conformal identification of hinges and edges.
proof idea
The definition is a direct equational statement. It serves as a one-line wrapper that renames ReggeDeficitLinearizationHypothesis for clarity in the simplicial setting, with the body simply asserting the forall equality between regge_sum and the scaled laplacian_action.
why it matters
CalibratedAgainstGraph supplies the hypothesis for the parent theorems field_curvature_identity_simplicial and field_curvature_identity_simplicial_einstein, which state that the J-cost energy equals (1/κ) times the Regge action on the conformal field. It fills the general simplicial case of paper Theorem 5.1, extending the cubic lattice result from Phase A and the linear_regge_vanishes guarantee from Phase C4. It touches the open question of explicit calibration constructions for arbitrary simplicial complexes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.