No prose has been written for this declaration yet. The Lean source and graph data below render
without it.
generate prose now
formal statement (Lean)
156theorem extremum_condition : J_curv lambda_rec_from_Jbit = J_bit_val := by
proof body
Term-mode proof.
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. -/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.
depends on (13)
Lean names referenced from this declaration's body.
-
J_bit_pos
in IndisputableMonolith.Astrophysics.StellarAssembly
decl_use
-
J_curv
in IndisputableMonolith.Constants.LambdaRecDerivation
decl_use
-
J_bit_pos
in IndisputableMonolith.Constants.PlanckScaleMatching
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
-
J_bit_pos
in IndisputableMonolith.Foundation.ConstantDerivations
decl_use
-
is
in IndisputableMonolith.Foundation.OptionAEmpiricalProgram
decl_use
-
J_bit_pos
in IndisputableMonolith.Foundation.PhiForcing
decl_use
-
is
in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi
decl_use
-
for
in IndisputableMonolith.Foundation.UniversalForcingSelfReference
decl_use
-
is
in IndisputableMonolith.GameTheory.MechanismDesignFromSigma
decl_use
-
is
in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom
decl_use