simplicial_linearization_discharge
plain-language theorem explainer
Any deficit angle functional D calibrated against a weighted ledger graph G satisfies the Regge deficit linearization hypothesis. Workers proving the field-curvature identity for general simplicial Regge calculus cite this result as the discharge step. The proof is a one-line wrapper that invokes the definitional equivalence between the calibration predicate and the linearization hypothesis.
Claim. Let $D$ be a deficit angle functional on an $n$-simplex, let $a>0$ be a real scale, let hinges be a list of hinge data, and let $G$ be a weighted ledger graph. If the Regge sum of $D$ on the conformal edge-length field equals $jcost_to_regge_factor$ times the Laplacian action of $G$ on every log-potential field, then the Regge deficit linearization hypothesis holds for these data.
background
The module carries out Phase C5 of the program to obtain Theorem 5.1 (field-curvature identity) as a Lean theorem. It composes the cubic calibration of Phase A with the linear-regge-vanishes result of Phase C4 to obtain a general simplicial discharge. CalibratedAgainstGraph is the predicate that the Regge sum of $D$ on the conformal edge-length field equals the scaled Laplacian action of $G$ on every log-potential; the referenced definition states that this predicate is definitionally identical to ReggeDeficitLinearizationHypothesis. WeightedLedgerGraph supplies the discrete Laplacian action that appears in the matching condition.
proof idea
The proof is a one-line wrapper that applies the equivalence calibrated_iff_hypothesis. The tactic simply uses the left-to-right direction of that equivalence on the supplied calibration hypothesis hCal.
why it matters
The declaration supplies the general-simplicial discharge that feeds field_curvature_identity_simplicial and simplicialFieldCurvatureCert. It fills the Phase C5 slot in the paper's Theorem 5.1 argument, extending the cubic case by replacing explicit construction with the Schläfli-based linear_regge_vanishes identity. The result closes the structural composition between the J-cost Dirichlet energy and the Regge action on conformal fields.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.