theorem proved tactic proof

`extremum_unique`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 163theorem extremum_unique (lam : ℝ) (hlam : lam > 0) (h_eq : J_curv lam = J_bit_val) :
 164    lam = lambda_rec_from_Jbit := by

proof body

Tactic-mode proof.

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

depends on (5)

Lean names referenced from this declaration's body.

J_curv in IndisputableMonolith.Constants.LambdaRecDerivation decl_use
J_bit_val in IndisputableMonolith.Constants.PlanckScaleMatching decl_use
J_curv in IndisputableMonolith.Constants.PlanckScaleMatching decl_use
lambda_rec_from_Jbit in IndisputableMonolith.Constants.PlanckScaleMatching decl_use
and in IndisputableMonolith.NumberTheory.CirclePhaseLift decl_use