def definition def or abbrev

`informationContent`

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

formal statement (Lean)

 106noncomputable def informationContent (bh : BlackHole) : ℝ :=

proof body

Definition body.

 107  entropyInBits bh
 108
 109/-! ## Hawking Temperature -/
 110
 111/-- The Hawking temperature T_H = ℏ c³ / (8π G M k_B).
 112
 113    A black hole radiates as a black body at this temperature.
 114    Smaller black holes are HOTTER (T ∝ 1/M). -/

depends on (20)

Lean names referenced from this declaration's body.

G in IndisputableMonolith.Constants decl_use
G in IndisputableMonolith.Constants.Codata decl_use
G in IndisputableMonolith.Cost.FunctionalEquation decl_use
T in IndisputableMonolith.Foundation.Breath1024 decl_use
A in IndisputableMonolith.Foundation.IntegrationGap decl_use
as in IndisputableMonolith.Foundation.SimplicialLedger.ContinuumBridge decl_use
T in IndisputableMonolith.Gap45.SyncMinimization decl_use
G in IndisputableMonolith.Gravity.JCostInflaton decl_use
k_B in IndisputableMonolith.Information.ComputationLimitsStructure decl_use
A in IndisputableMonolith.Masses.Anchor decl_use
A in IndisputableMonolith.Modal.Actualization decl_use
BlackHole in IndisputableMonolith.Quantum.BekensteinHawking decl_use
entropyInBits in IndisputableMonolith.Quantum.BekensteinHawking decl_use
k_B in IndisputableMonolith.Quantum.BekensteinHawking decl_use
BlackHole in IndisputableMonolith.Quantum.BlackHoleInformation decl_use
k_B in IndisputableMonolith.Quantum.PageCurve decl_use
M in IndisputableMonolith.Recognition decl_use
M in IndisputableMonolith.Recognition.Cycle3 decl_use
temperature in IndisputableMonolith.Thermodynamics.BoltzmannDistribution decl_use
k_B in IndisputableMonolith.Thermodynamics.PartitionFunction decl_use