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

kappa_normalized_eq_one

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)

 172theorem kappa_normalized_eq_one : kappa_normalized = 1 := by

proof body

Term-mode proof.

 173  unfold kappa_normalized
 174  rw [total_curvature_gauss_bonnet]
 175  simp [euler_S2]; ring
 176
 177/-- J_curv = 2λ² is the curvature cost per recognition token.
 178    Derivation: |κ_normalized| × (4πλ²) / (2π × χ(S²))
 179    = 1 × (4πλ²) / (2π × 2) = 2λ² / 2 ... wait, let's be precise:
 180    J_curv = (|κ|/(2χ)) × (A/(2π)) where |κ| = 4, χ = 2, A = 4πλ²
 181    = (4/4) × (4πλ²/(2π)) = 1 × 2λ² = 2λ². -/

depends on (14)

Lean names referenced from this declaration's body.