planck_length
plain-language theorem explainer
The declaration embeds the standard Planck length formula using the CODATA values for the reduced Planck constant, gravitational constant, and speed of light that are stored as constants in the derivation module. Researchers converting between Recognition Science native units and laboratory units would cite it when discussing Planck-scale physics. The definition is a direct algebraic expression that requires no additional lemmas beyond the positivity result that immediately follows it.
Claim. The Planck length is defined by $l_P = sqrt( ħ_{codata} G_{codata} / c_{codata}^3 )$, where the subscripted quantities are the CODATA reference values $c = 299792458$, $ħ = 1.054571817 × 10^{-34}$, and $G = 6.67430 × 10^{-11}$.
background
This definition appears in the Constants.Derivation module, which records CODATA reference values for c, ħ, and G while deriving other constants from Recognition Science primitives. The module first states the exact SI values and then introduces G_derived(τ, ħ, c) := π c^5 τ² / ħ together with the theorem that G_derived(τ₀, ħ_codata, c_codata) equals the CODATA G. The Planck units section begins right after the consistency theorems for these relations.
proof idea
This is a direct definition with no proof body. It assembles the square root of the product of the embedded ħ_codata and G_codata divided by c_codata cubed.
why it matters
The definition supplies the conventional Planck length expression inside the Recognition Science constants framework, enabling the immediate positivity lemma planck_length_pos that follows it. It sits in the Planck Units subsection after the G_relation_satisfied theorem that verifies consistency of the derived G with CODATA. Within the broader framework it supports conversion between the phi-ladder mass formulas and SI units, though it does not itself invoke the J-function or the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.