exact_flat_agrees_with_linearized

formal source

 235/-- **WEAK-FIELD LIMIT.** When every log-potential difference is
 236    zero, `exactJCostAction = laplacian_action = 0`. This is the
 237    flat vacuum limit. -/
 238theorem exact_flat_agrees_with_linearized {n : ℕ}
 239    (G : WeightedLedgerGraph n) :
 240    exactJCostAction G (fun _ => (0 : ℝ))
 241      = laplacian_action G (fun _ => (0 : ℝ)) := by
 242  rw [exact_decomposition, laplacian_action_flat G]
 243  unfold quarticRemainder coshRemainder
 244  simp
 245
 246/-! ## §5. The non-linear J ↔ Regge hypothesis
 247
 248In the weak-field regime, `CubicDeficitDischarge.cubic_linearization_discharge`
 249makes the J ↔ Regge identity a theorem. Beyond that regime, one needs
 250the corresponding non-linear statement, which is what Cayley-Menger
 251calculations on a simplicial mesh produce in the limit.
 252
 253We package that as an explicit hypothesis, NOT an axiom. -/
 254
 255/-- A *non-linear deficit-angle functional*: an extension of the
 256    linear functional to strong-field configurations. Concretely
 257    it is a `DeficitAngleFunctional` that additionally satisfies
 258    the non-linear matching identity below. -/
 259structure NonlinearDeficitFunctional (n : ℕ) where
 260  functional : DeficitAngleFunctional n
 261
 262/-- The **non-linear Regge ↔ J-cost matching hypothesis.** Under
 263    this hypothesis, the Regge sum on the non-linear deficit
 264    functional equals `κ · exactJCostAction`, not merely
 265    `κ · laplacian_action`. -/
 266def NonlinearReggeJCostIdentity
 267    {n : ℕ} (D : NonlinearDeficitFunctional n) (a : ℝ) (ha : 0 < a)
 268    (hinges : List (HingeDatum n)) (G : WeightedLedgerGraph n) : Prop :=