planckMass
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not derive numerical values beyond substitution of the RS constants.
- Does not prove invariance under changes to the Recognition forcing chain.
- Does not incorporate quantum corrections or loop effects.
- Does not address the relation to voxel length or lengthHierarchy beyond the sibling definitions.
Lean usage
noncomputable def planckEnergy : ℝ := planckMass * c^2formal statement (Lean)
41noncomputable def planckMass : ℝ := sqrt (hbar * c / G)
proof body
Definition body.
42
43/-- The Planck time t_P = √(ℏG/c⁵) ≈ 5.391 × 10⁻⁴⁴ s. -/