lambda_rec_from_Jbit

formal source

 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
 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