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)
105theorem c_positive : c > 0 := by
proof body
Term-mode proof.
106 rw [c_eq_one]
107 norm_num
108
109/-! ## Section C-006: Boltzmann Analog k_R -/
110
111/-- **CALCULATED**: RS-native Boltzmann constant k_R = ln(φ). -/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.
depends on (4)
Lean names referenced from this declaration's body.
-
k_R
in IndisputableMonolith.Constants.BoltzmannConstant
decl_use
-
k_R
in IndisputableMonolith.Gravity.UltramassiveBH
decl_use
-
constant
in IndisputableMonolith.Relativity.Fields.Scalar
decl_use
-
c_eq_one
in IndisputableMonolith.Unification.ConstantsPredictionsProved
decl_use