planck_length_eq_one
plain-language theorem explainer
Planck length equals 1 in RS-native units. Researchers normalizing length scales inside the constant-derivation chain from the Recognition Composition Law cite this normalization. The proof is a short algebraic reduction that unfolds the square-root definition, substitutes the prior result c = 1, commutes the G ℏ product, and reduces the radicand to unity.
Claim. The Planck length defined by $ℓ_P := √(ℏ_{rs} G_{rs} / c_{rs}^3)$ equals 1 in the native units of Recognition Science.
background
This module derives the fundamental constants from the RS foundation. The Composition Law produces the J-cost J(x) = ½(x + x^{-1}) − 1 whose fixed point is the golden ratio φ; the eight-tick octave then forces D = 3 and the causal speed c = 1. The Planck length is introduced as the square root of the product ℏ G divided by c cubed, with all quantities expressed in RS-native units where lengths and times are scaled to the fundamental tick and coherence length.
proof idea
The proof unfolds the definition of planck_length_rs, rewrites c_rs to 1 via c_rs_eq_one, simplifies the resulting powers and division, commutes the G ℏ product via G_ℏ_product, and concludes with the fact that the square root of one is one.
why it matters
This result is invoked by all_constants_from_phi, which assembles the full set c = 1, ℏ = φ^{-5}, G = φ^5. It supplies the length normalization step in the derivation chain that begins with the Composition Law and proceeds through the forcing sequence to the physical constants. The step closes the unit choice that makes every constant algebraic in φ.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.
papers checked against this theorem (showing 1 of 1)
-
Higgs–dilaton inflation in Weyl geometry hits a unitarity wall
"Dilaton ⟨φ_0⟩ generates M_P via spontaneous breaking of scale symmetry: M_P² = (1/6)(ξ_0 - λ_1 ξ_1/(2λ_2))⟨φ_0²⟩"