planck_mass
The definition computes the Planck mass in SI units from the CODATA values of the reduced Planck constant, speed of light, and gravitational constant. Researchers deriving mass scales or positivity results in the Recognition Science constants module cite it when bridging empirical values to the phi-ladder. It is implemented as a direct one-line definition applying the standard square root formula to the imported codata constants.
claimThe Planck mass is the real number defined by $m_P := sqrt( (hbar * c) / G )$, where hbar, c, and G are the CODATA numerical values 1.054571817e-34, 299792458, and 6.67430e-11 respectively.
background
This declaration sits inside the module that derives physical constants from Recognition Science primitives. The module first records the CODATA reference values as sibling definitions: c_codata equals 299792458, hbar_codata equals 1.054571817e-34, and G_codata equals 6.67430e-11. These three constants supply the numerical inputs for the Planck mass expression. The local theoretical setting is the extraction of standard constants for later comparison with Recognition Science native units such as c = 1 and hbar = phi^{-5}.
proof idea
The declaration is a one-line definition that directly evaluates the square root of the product of hbar_codata and c_codata divided by G_codata. No lemmas beyond built-in real arithmetic are invoked.
why it matters in Recognition Science
It supplies the concrete value required by the downstream lemma planck_mass_pos that proves positivity. Within the Recognition Science framework the definition anchors the constants module, permitting later arguments that relate the Planck scale to the mass formula yardstick * phi^(rung - 8 + gap(Z)) and the eight-tick octave. The module doc-comment frames the entire block as derivation from primitives, so this supplies the empirical bridge.
scope and limits
- Does not derive the Planck mass from the J-uniqueness or forcing chain T0 to T8.
- Does not relate the result to the Recognition Composition Law or phi-ladder.
- Does not incorporate measurement uncertainty from CODATA.
- Does not connect to the Berry creation threshold or Z_cf = phi^5.
Lean usage
example : 0 < planck_mass := planck_mass_posformal statement (Lean)
152def planck_mass : ℝ := sqrt (hbar_codata * c_codata / G_codata)
proof body
Definition body.
153