planck_to_meters
plain-language theorem explainer
planck_to_meters supplies the linear scaling that turns a distance expressed in Planck lengths into meters by multiplying by the CODATA Planck length. Cosmologists comparing RS-native predictions for cosmic scales against meter-based observations would apply it to any length ratio. The definition is a direct multiplication by the imported constant planck_length_SI.
Claim. The map sending a distance $r$ measured in Planck lengths to its value in meters is $rmapsto rcdotell_P$, where $ell_P=1.616255times10^{-35}$ m is the fixed Planck length in SI units.
background
Recognition Science derives physics in native units with $c=ell_0=tau_0=1$. The SIConversion module supplies the external calibration seam that lets RS ratios be reported in meters and seconds; the Planck length serves as the single anchor because its SI value is taken from CODATA rather than derived inside the theory. The upstream definition planck_length_SI fixes this numerical value at 1.616255e-35 m with its stated uncertainty. The theorem from PrimitiveDistinction records the passage from seven independent axioms to four structural conditions plus three definitional facts that underwrite the cosmology layer.
proof idea
One-line definition that multiplies the input real by the constant planck_length_SI.
why it matters
It supplies the concrete bridge that lets any RS length ratio (for example those generated on the phi-ladder or inside the eight-tick octave) be expressed in laboratory meters. The module documentation stresses that the theoretical content resides in the ratios, not in the SI numbers themselves; this definition therefore closes the reporting seam for cosmological observables without introducing new axioms. No downstream theorems are yet recorded, leaving the conversion available for later use in age or distance calculations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.