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)
64theorem bhEntropy_pos {M : ℝ} (hM : 0 < M) : 0 < bhEntropy M := by
proof body
Term-mode proof.
65 rw [bhEntropy_eq]
66 exact mul_pos (mul_pos (by linarith) Real.pi_pos) (sq_pos_of_pos hM)
67
68/-! ## §2. Horizon Bandwidth -/
69
70/-- Recognition bandwidth at the horizon: total holographic bits / (k_R · 8τ₀). -/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.
depends on (9)
Lean names referenced from this declaration's body.
-
k_R
in IndisputableMonolith.Constants.BoltzmannConstant
decl_use
-
k_R
in IndisputableMonolith.Gravity.UltramassiveBH
decl_use
-
total
in IndisputableMonolith.NavierStokes.DiscreteVorticity
decl_use
-
total
in IndisputableMonolith.NumberTheory.RiemannHypothesis.ErrorBudget
decl_use
-
M
in IndisputableMonolith.Recognition
decl_use
-
M
in IndisputableMonolith.Recognition.Cycle3
decl_use
-
bhEntropy
in IndisputableMonolith.Unification.BlackHoleBandwidth
decl_use
-
bhEntropy_eq
in IndisputableMonolith.Unification.BlackHoleBandwidth
decl_use
-
bandwidth
in IndisputableMonolith.Unification.RecognitionBandwidth
decl_use