planck_length_SI
plain-language theorem explainer
planck_length_SI supplies the CODATA 2018 numerical value of the Planck length in meters. Cosmologists and Recognition Science workers cite it when mapping native-unit predictions onto SI observables. The definition is a direct constant assignment drawn from external data rather than derived inside the theory.
Claim. The Planck length in SI units is defined by the constant assignment $ℓ_P := 1.616255 × 10^{-35}$ meters.
background
The module establishes the SI calibration seam required once Recognition Science works entirely in native units where $c = ℓ_0 = τ_0 = 1$. The Planck scale supplies the single external anchor: $ℓ_P = √(ℏG/c³)$ in SI meters and $t_P = ℓ_P/c$ in seconds. These numerical values are imported from CODATA 2018; the theoretical content of the framework resides in the ratios of observables to these anchors, not in the anchors themselves.
proof idea
Direct constant definition that assigns the published CODATA figure with no further computation or lemma application.
why it matters
The definition supplies the calibration anchor used by planck_to_meters, planck_length_SI_pos, and si_calibration_cert. It closes the reporting seam described in the module documentation, allowing RS-native results (such as the phi-ladder mass formula or the eight-tick octave) to be expressed in meters and seconds while keeping the SI numbers external to the theory.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.