J_curv_zero

formal source

 132noncomputable def J_curv (lam : ℝ) : ℝ := 2 * lam^2
 133
 134/-- J_curv(0) = 0. -/
 135theorem J_curv_zero : J_curv 0 = 0 := by simp [J_curv]
 136
 137/-- J_curv is non-negative. -/
 138theorem J_curv_nonneg (lam : ℝ) : J_curv lam ≥ 0 := by
 139  unfold J_curv
 140  have h : lam^2 ≥ 0 := sq_nonneg lam
 141  linarith
 142
 143/-! ## Part 3: Curvature Extremum Condition -/
 144
 145/-- **THE EXTREMUM EQUATION**: J_bit = J_curv(λ).
 146
 147Solving for λ: J_bit = 2λ² ⟹ λ = √(J_bit/2). -/
 148noncomputable def lambda_rec_from_Jbit : ℝ := sqrt (J_bit_val / 2)
 149
 150/-- λ_rec_from_Jbit > 0 since J_bit > 0. -/
 151theorem lambda_rec_from_Jbit_pos : lambda_rec_from_Jbit > 0 := by
 152  unfold lambda_rec_from_Jbit
 153  exact sqrt_pos.mpr (div_pos J_bit_pos (by norm_num : (2 : ℝ) > 0))
 154
 155/-- At λ_rec_from_Jbit, the extremum condition holds. -/
 156theorem extremum_condition : J_curv lambda_rec_from_Jbit = J_bit_val := by
 157  unfold J_curv lambda_rec_from_Jbit
 158  have h : J_bit_val / 2 ≥ 0 := le_of_lt (div_pos J_bit_pos (by norm_num))
 159  rw [sq_sqrt h]
 160  ring
 161
 162/-- The extremum is unique: if J_curv(λ) = J_bit for λ > 0, then λ = λ_rec_from_Jbit. -/
 163theorem extremum_unique (lam : ℝ) (hlam : lam > 0) (h_eq : J_curv lam = J_bit_val) :
 164    lam = lambda_rec_from_Jbit := by
 165  unfold J_curv at h_eq