69 unfold balanceResidual J_curv J_bit_normalized lambda_0 70 constructor 71 · intro h 72 have hsq : lambda ^ 2 = 1 / 2 := by linarith 73 have hlam_sqrt : lambda = Real.sqrt (1 / 2) := by 74 rw [← Real.sqrt_sq (le_of_lt hlambda), hsq] 75 rw [hlam_sqrt, Real.sqrt_div (by norm_num : (0:ℝ) ≤ 1), Real.sqrt_one] 76 · intro h 77 rw [h, div_pow, Real.sq_sqrt (by norm_num : (0:ℝ) ≤ 2)] 78 ring 79 80/-! ## The Curvature Functional K (for backward compatibility) 81 82The functional K(λ) := λ²/λ_rec² - 1 is an algebraic restatement 83of the balance condition. Since G is *defined* from λ_rec, the 84identity K(λ_rec) = 0 is a consequence of definitions, not an 85independent derivation. The physical content is in the balance 86condition above. -/ 87 88/-- Curvature functional (algebraic restatement of balance condition). 89 K(λ) = 0 iff λ = λ_rec. This is tautological given the definition 90 of G, but is retained for backward compatibility with the 91 verification infrastructure. -/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.