simplicial_linearization_discharge

formal source

 107    simplicial case supplies it via Phase C4's
 108    `linear_regge_vanishes` (using the Schläfli identity to kill the
 109    first-order term and the Phase A pattern for the quadratic term). -/
 110theorem simplicial_linearization_discharge {n : ℕ}
 111    (D : DeficitAngleFunctional n) (a : ℝ) (ha : 0 < a)
 112    (hinges : List (HingeDatum n)) (G : WeightedLedgerGraph n)
 113    (hCal : CalibratedAgainstGraph D a ha hinges G) :
 114    ReggeDeficitLinearizationHypothesis D a ha hinges G :=
 115  (calibrated_iff_hypothesis D a ha hinges G).mp hCal
 116
 117/-- The cubic lattice is calibrated against every weighted ledger graph,
 118    by Phase A. -/
 119theorem cubic_calibrated_against_graph {n : ℕ} (a : ℝ) (ha : 0 < a)
 120    (G : WeightedLedgerGraph n) :
 121    CalibratedAgainstGraph (cubicDeficitFunctional n) a ha (cubicHinges G) G :=
 122  cubic_linearization_discharge a ha G
 123
 124/-! ## §3. Field-curvature identity (simplicial form) -/
 125
 126/-- **THE FIELD-CURVATURE IDENTITY (general simplicial form).**
 127
 128    For any calibrated simplicial `DeficitAngleFunctional`, the J-cost
 129    Dirichlet energy equals `(1/κ)` times the Regge action on the
 130    conformal edge-length field. Directly extends
 131    `field_curvature_identity_under_linearization` from
 132    `EdgeLengthFromPsi.lean`. -/
 133theorem field_curvature_identity_simplicial {n : ℕ}
 134    (D : DeficitAngleFunctional n) (a : ℝ) (ha : 0 < a)
 135    (hinges : List (HingeDatum n)) (G : WeightedLedgerGraph n)
 136    (hCal : CalibratedAgainstGraph D a ha hinges G)
 137    (ε : LogPotential n) :
 138    laplacian_action G ε
 139    = (1 / jcost_to_regge_factor) *
 140        regge_sum D (conformal_edge_length_field a ha ε) hinges :=