flat_zero_cost

formal source

 266  exact Finset.sum_const_zero
 267
 268/-- Flat spacetime has zero J-cost. -/
 269theorem flat_zero_cost : Jcost 1 = 0 := Jcost_unit0
 270
 271/-! ## The Deficit Angle – J-Cost Correspondence
 272
 273The deepest structural result: the deficit angle at a hinge in
 274Regge calculus corresponds to J-cost imbalance at a face.
 275
 276For a face shared by simplices σ₁ and σ₂ with potentials ψ₁, ψ₂:
 277  δ_face = J(ψ₁/ψ₂)^(1/2) ∝ |ε₁ − ε₂|
 278
 279The deficit angle IS the square root of the J-cost mismatch.
 280This is not a coincidence — it follows from the quadratic structure:
 281  J(e^δε) ≈ (δε)²/2 and δ_Regge ≈ δε in the linearized regime.
 282
 283The full nonlinear correspondence uses cosh:
 284  J(e^δε) = cosh(δε) − 1
 285
 286For the Regge action, the deficit angle satisfies:
 287  cos(δ) = 1 − δ²/2 + ... so 1 − cos(δ) = δ²/2 + ...
 288
 289Both are quadratic at leading order with coefficient 1/2,
 290confirming the identification. -/
 291
 292/-- The leading-order identification:
 293    J-cost mismatch = (deficit angle)² / 2 at leading order. -/
 294theorem deficit_jcost_correspondence (δε : ℝ) (_hsmall : |δε| < 1) :
 295    J_log_quadratic δε - δε ^ 2 / 2 = 0 := by
 296  unfold J_log_quadratic
 297  ring
 298
 299/-! ## Certificate -/