planckMass
plain-language theorem explainer
The declaration defines the Planck mass in Recognition Science as the square root of ħc over G. Researchers deriving black-hole thermodynamics or quantum-gravity scales from the Recognition functional equation cite this when converting between RS-native units and standard Planck quantities. The definition is a direct substitution of the RS expressions for ħ = φ^{-5} and G = λ_rec² c³ / (π ħ) into the classical formula.
Claim. The Planck mass is given by $m_P = √(ℏ c / G)$, where ℏ is the reduced Planck constant in RS-native units (φ^{-5}) and G is the gravitational constant derived from the Recognition Composition Law.
background
Module PlanckScale targets QG-009 and QG-010: derivation of Planck length, mass and time from RS principles. The Planck scale marks the intersection of quantum mechanics and gravity, expressed in RS as l_P = c τ₀ φ^{-n} for appropriate n. Upstream, Constants.hbar supplies ħ = cLagLock · τ₀ = φ^{-5} and Constants.G supplies G = λ_rec² c³ / (π ħ), both obtained from the forcing chain T5–T8 and the J-cost functional equation.
proof idea
One-line definition that substitutes the RS-native constants ħ and G directly into the classical Planck-mass expression. No lemmas are applied beyond the constant declarations imported from Constants and PhiForcing.
why it matters
This supplies the Planck mass used by BekensteinHawking.planckMass, planckTemperature and PlanckScale.planckEnergy. It completes the QG-009 target of expressing Planck quantities via the φ-ladder and the eight-tick octave. The definition anchors the connection between the Recognition Composition Law and the standard Planck units that appear in black-hole entropy formulas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.