theorem proved term proof

`boltzmann_analog_positive`

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

Last generation error: Invalid control character at: line 3 column 53 (char 416)

formal statement (Lean)

 116theorem boltzmann_analog_positive : Real.log phi > 0 := by

Term-mode proof.

 117  apply Real.log_pos
 118  exact one_lt_phi
 119
 120/-- **CALCULATED**: k_R < 0.5 since φ < 1.62 < e^0.5 ≈ 1.6487. -/

From the project-wide theorem graph. These declarations reference this one in their body.

boltzmann_analog_bounds in IndisputableMonolith.Unification.ConstantsPredictionsProved decl_use
constants_predictions_cert_exists in IndisputableMonolith.Unification.ConstantsPredictionsProved decl_use

Lean names referenced from this declaration's body.