calibrated_iff_hypothesis
plain-language theorem explainer
The equivalence identifies the calibration condition on a deficit functional D against ledger graph G with the Regge deficit linearization hypothesis. Researchers deriving the simplicial field-curvature identity cite it to treat the per-hinge matching as interchangeable with the hypothesis from EdgeLengthFromPsi. The proof is a single reflexivity step because the two predicates are definitionally identical.
Claim. Let $D$ be a deficit angle functional, $a>0$, hinges a list of hinge data, and $G$ a weighted ledger graph. Then $D$ is calibrated against $G$ (its Regge sum on the conformal edge length field equals the scaled Laplacian action on the log potential) if and only if the Regge deficit linearization hypothesis holds for these data.
background
Phase C5 of the Recognition Science program composes Phases C1–C4 to discharge the linearization hypothesis for general simplicial complexes in the proof of paper Theorem 5.1. CalibratedAgainstGraph requires that for every log potential ε the regge_sum of D on the conformal edge length field equals jcost_to_regge_factor times laplacian_action of G on ε. This matches the ReggeDeficitLinearizationHypothesis by construction, with the cubic case supplied explicitly in CubicDeficitDischarge and the general case via linear_regge_vanishes from Phase C4.
proof idea
The proof is a one-line term that applies Iff.rfl. It exploits the definitional identity between CalibratedAgainstGraph and ReggeDeficitLinearizationHypothesis stated in the module doc-comment.
why it matters
This equivalence feeds directly into simplicial_linearization_discharge, which converts a calibration assumption into the required hypothesis for the simplicial bridge identity. It supplies the structural rename needed for Phase C5 to handle arbitrary deficit functionals while preserving the J-cost Dirichlet energy matching. The declaration closes the gap between explicit cubic construction and the general simplicial case that relies on the Schläfli identity to kill the linear term.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.