planck_length_SI_pos
plain-language theorem explainer
The theorem asserts that the Planck length in SI meters is strictly positive. Cosmologists converting RS-native predictions to observable units would cite it to confirm the calibration anchor is well-defined. The proof is a one-line wrapper that unfolds the definition and normalizes the numerical constant.
Claim. $0 < 1.616255e-35$, where the right-hand side is the CODATA 2018 value of the Planck length in meters.
background
The SI Conversion module supplies external calibration anchors so that RS predictions, derived in native units with $c = 1$, can be expressed in meters and seconds. The Planck length in SI is defined as the fixed experimental number $1.616255e-35$, serving as the bridge for cosmological observables; the module documentation states that these SI values are not RS predictions but the seam through which ratios are reported.
proof idea
The proof is a one-line wrapper that unfolds the definition of planck_length_SI and applies norm_num to confirm the hardcoded positive constant satisfies the inequality.
why it matters
It supplies the planck_length_positive field required by the si_calibration_cert theorem, which certifies consistency of the SI calibration seam. In the Recognition Science framework this anchors the conversion from native units to SI units for cosmological comparisons, as described in the module's reporting-seam section; the SI values remain external facts rather than derivations from the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.