CalibratedAgainstGraph

formal source

  77    Phase A constructs such a calibration explicitly for the cubic
  78    lattice; for general simplicial complexes this calibration is
  79    supplied by Phase C4's `linear_regge_vanishes`. -/
  80def CalibratedAgainstGraph {n : ℕ}
  81    (D : DeficitAngleFunctional n) (a : ℝ) (ha : 0 < a)
  82    (hinges : List (HingeDatum n)) (G : WeightedLedgerGraph n) : Prop :=
  83  ∀ ε : LogPotential n,
  84    regge_sum D (conformal_edge_length_field a ha ε) hinges
  85      = jcost_to_regge_factor * laplacian_action G ε
  86
  87/-- Trivial observation: `CalibratedAgainstGraph` and
  88    `ReggeDeficitLinearizationHypothesis` are definitionally the same
  89    statement. The rename clarifies that the matching is a *property*
  90    of the functional, not a result of the linearization per se. -/
  91theorem calibrated_iff_hypothesis {n : ℕ}
  92    (D : DeficitAngleFunctional n) (a : ℝ) (ha : 0 < a)
  93    (hinges : List (HingeDatum n)) (G : WeightedLedgerGraph n) :
  94    CalibratedAgainstGraph D a ha hinges G ↔
  95    ReggeDeficitLinearizationHypothesis D a ha hinges G :=
  96  Iff.rfl
  97
  98/-! ## §2. The direct discharge -/
  99
 100/-- **SIMPLICIAL LINEARIZATION DISCHARGE.**
 101
 102    For any deficit functional `D` calibrated against a ledger graph `G`,
 103    the `ReggeDeficitLinearizationHypothesis` from `EdgeLengthFromPsi`
 104    holds. This is the general-simplicial analog of
 105    `CubicDeficitDischarge.cubic_linearization_discharge`; the cubic case
 106    supplies the calibration by explicit construction, whereas a general
 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 : ℕ}