extremum_condition

formal source

 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
 166  unfold lambda_rec_from_Jbit
 167  have h1 : lam^2 = J_bit_val / 2 := by linarith
 168  have h2 : lam = sqrt (lam^2) := (sqrt_sq (le_of_lt hlam)).symm
 169  rw [h1] at h2
 170  exact h2
 171
 172/-! ## Part 4: Face-Averaging and the π Factor -/
 173
 174/-- The solid angle per octant = π/2 steradians. -/
 175noncomputable def solid_angle_per_octant : ℝ := Real.pi / 2
 176
 177/-- There are 8 octants in 3D space. -/
 178def num_octants : ℕ := 8
 179
 180/-- The total solid angle of a sphere = 4π. -/
 181noncomputable def total_solid_angle : ℝ := 4 * Real.pi
 182
 183/-- Verification: 8 × (π/2) = 4π. -/
 184theorem octants_cover_sphere :
 185    (num_octants : ℝ) * solid_angle_per_octant = total_solid_angle := by
 186  simp [num_octants, solid_angle_per_octant, total_solid_angle]