planckMass
plain-language theorem explainer
The declaration supplies the Planck mass m_P as sqrt(hbar c / G) in RS-native units. Researchers deriving black-hole thermodynamics or Planck-scale cutoffs from the Recognition functional equation would cite it to set the mass ladder rung. The definition is a direct one-line algebraic wrapper on the imported constants hbar, c and G.
Claim. $m_P = sqrt( ħ c / G )$ where ħ and G are the RS-native reduced Planck constant and gravitational constant.
background
The module derives black-hole thermodynamics from Recognition Science, targeting Bekenstein-Hawking entropy S_BH = k_B A / (4 l_P²) and Hawking temperature. Planck mass supplies the fundamental mass scale that converts horizon area into entropy and sets the temperature via E_P = m_P c². Upstream, hbar is defined as cLagLock · tau0 (equal to phi^{-5} in native units) and G as (lambda_rec² c³) / (pi hbar), both obtained from the forcing chain T0-T8 and the Recognition Composition Law.
proof idea
One-line definition that directly applies the imported constants hbar, c and G to the classical Planck-mass expression; no lemmas or tactics are invoked beyond the Real.sqrt abbreviation.
why it matters
It supplies the mass scale required by the downstream definitions of planckEnergy and planckTemperature, which in turn feed the Bekenstein-Hawking entropy and horizon-area results. The declaration therefore closes the first step of the QG-001 target in the module doc-comment, linking the Recognition functional equation to the holographic bound. No open scaffolding remains at this node.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.