balance_at_lambda_0

formal source

  58  norm_num
  59
  60/-- The balance residual vanishes at lambda_0. -/
  61theorem balance_at_lambda_0 : balanceResidual lambda_0 = 0 := by
  62  unfold balanceResidual J_curv J_bit_normalized
  63  rw [lambda_0_sq]
  64  ring
  65
  66/-- lambda_0 is the unique positive root of the balance residual. -/
  67theorem balance_unique_positive_root (lambda : ℝ) (hlambda : lambda > 0) :
  68    balanceResidual lambda = 0 ↔ lambda = lambda_0 := by
  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. -/