planckTemperature
The declaration defines the Planck temperature as the Planck mass times c squared divided by Boltzmann's constant. Researchers working on black hole thermodynamics or Planck-scale derivations in Recognition Science cite this constant when linking energy scales to temperature. The definition is a direct algebraic combination of the upstream Planck mass and the imported constants c and k_B.
claimThe Planck temperature is defined by $T_P = m_P c^2 / k_B$, where $m_P$ is the Planck mass, $c$ the speed of light, and $k_B$ Boltzmann's constant.
background
This definition appears in the Bekenstein-Hawking module whose module doc targets QG-001 and QG-002, deriving black hole thermodynamics from Recognition Science by treating horizon area as ledger information capacity and temperature as arising from the τ₀-scale. The Planck mass is supplied by the sibling definition planckMass := Real.sqrt (hbar * c / G). Boltzmann's constant k_B is fixed at 1.380649e-23 in the same module and in the upstream ComputationLimitsStructure, where it enters the Landauer energy bound k_B T ln(2).
proof idea
The definition is a direct one-line combination that multiplies the sibling planckMass by c squared and divides by the module-local k_B. No lemmas or tactics are applied beyond the algebraic expression itself.
why it matters in Recognition Science
It supplies the Planck temperature value required by the downstream planckTemperature declaration in the PlanckScale module. The definition advances the module's goal of obtaining Hawking temperature from Recognition Science information capacity, connecting to the framework's D = 3 and phi-ladder constants at the Planck scale. It leaves open the reconciliation of RS-native units with the numerical Planck temperature.
scope and limits
- Does not derive the Planck mass from the forcing chain T0-T8.
- Does not include quantum corrections to the temperature.
- Does not extend to rotating or charged black holes.
- Does not compute a numerical value in SI units.
formal statement (Lean)
56noncomputable def planckTemperature : ℝ := planckMass * c^2 / k_B
proof body
Definition body.
57
58/-! ## Black Hole Properties -/
59
60/-- A Schwarzschild black hole with mass M. -/