planck_length_rs
plain-language theorem explainer
The definition sets the Planck length in RS-native units to the square root of (ℏ_rs times G_rs over c_rs cubed). Researchers deriving physical constants from the Recognition Science foundation cite it to establish unit consistency when all scales reduce to the fundamental length. The expression is obtained by direct substitution of the RS values for each constant into the classical formula.
Claim. The Planck length in RS-native units is defined by ℓ_P := √(ℏ_rs G_rs / c_rs³), where c_rs = 1, ℏ_rs = φ^{-5}, and G_rs = φ^5.
background
The module derives fundamental constants from the RS foundation via the Composition Law, J-uniqueness, and the self-similar fixed point φ. The speed of light c_rs is the ratio of fundamental length to time and equals 1 in native units. The gravitational constant G_rs is the curvature extremum in recognition geometry and equals φ^5 in the local native units (with mass scale 1/φ^5). Upstream results establish the same constants algebraically in φ, with one variant including a factor of 1/π that is absorbed here.
proof idea
The definition is a direct transcription of the standard Planck length formula using the already-derived RS-native constants c_rs, G_rs, and the implied ℏ_rs = φ^{-5}. No tactics or reductions occur; the body is a single expression.
why it matters
This definition supplies the Planck length term required by the downstream theorem all_constants_from_phi and enables the equality proof in planck_length_eq_one. It completes the Level 4 step in the module's derivation chain, where constants become ratios of RS-native quantities algebraic in φ, consistent with the T0-T8 forcing chain that fixes D = 3 and the eight-tick octave. It touches the open mapping from these algebraic identities to observed physics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.