pith. machine review for the scientific record. sign in
theorem proved term proof

flat_zero_cost

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 269theorem flat_zero_cost : Jcost 1 = 0 := Jcost_unit0

proof body

Term-mode proof.

 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. -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (18)

Lean names referenced from this declaration's body.