kappa_normalized

formal source

 166  simp [Q3_vertices, euler_S2, angular_deficit_value]; ring
 167
 168/-- The normalized curvature magnitude |κ| per vertex-sphere. -/
 169noncomputable def kappa_normalized : ℝ := Q3_vertices * angular_deficit_per_vertex / (4 * Real.pi)
 170
 171/-- |κ_normalized| = 1 (from Gauss-Bonnet). -/
 172theorem kappa_normalized_eq_one : kappa_normalized = 1 := by
 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λ². -/
 182theorem J_curv_derivation (lambda : ℝ) :
 183    J_curv lambda = 2 * lambda ^ 2 := rfl
 184
 185/-- The balance condition J_bit = J_curv uniquely determines lambda. -/
 186theorem balance_determines_lambda :
 187    ∃! lambda : ℝ, lambda > 0 ∧ J_curv lambda = J_bit_normalized :=
 188  balance_unique_pos_root
 189  where
 190    balance_unique_pos_root : ∃! lambda : ℝ, lambda > 0 ∧ J_curv lambda = J_bit_normalized := by
 191      use lambda_0
 192      refine ⟨⟨lambda_0_pos, ?_⟩, ?_⟩
 193      · unfold J_curv J_bit_normalized; rw [lambda_0_sq]; ring
 194      · intro y ⟨hy_pos, hy_eq⟩
 195        have : balanceResidual y = 0 := by unfold balanceResidual; linarith
 196        exact (balance_unique_positive_root y hy_pos).mp this
 197
 198/-- Complete derivation chain certificate: from Q3 geometry to kappa = 8phi^5.
 199