lambda_0_sq

formal source

  50  exact Real.sqrt_pos.mpr (by norm_num : (0 : ℝ) < 2)
  51
  52/-- lambda_0² = 1/2. -/
  53lemma lambda_0_sq : lambda_0 ^ 2 = 1 / 2 := by
  54  unfold lambda_0
  55  rw [div_pow]
  56  have h2 : (0 : ℝ) ≤ 2 := by norm_num
  57  rw [Real.sq_sqrt h2]
  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