si_calibration_cert
plain-language theorem explainer
The certificate verifies positivity of the SI Planck length and time while confirming their ratio is consistent with the exact speed of light to within one percent. Cosmologists converting native-unit predictions to meter and second scales would cite this result to anchor the calibration. The proof is a direct structure construction that invokes the positivity lemmas and applies numerical normalization to the consistency conditions.
Claim. Let $0 < l_{P,SI}$ and $0 < t_{P,SI}$ hold for the CODATA Planck length and time in SI units, with $c_{SI}$ the exact speed of light. The certificate asserts the two positivity statements together with the bounds $l_{P,SI}/c_{SI} < t_{P,SI}·1.01$ and $t_{P,SI}·0.99 < l_{P,SI}/c_{SI}$.
background
RS derives all physics in native units where $c=ℓ_0=τ_0=1$. The module supplies external SI anchors for the Planck scale so that native predictions can be expressed in meters, seconds, and km/s/Mpc. The structure packages four fields: strict positivity of the Planck length in meters, strict positivity of the Planck time in seconds, and two numerical inequalities that enforce the defining relation $l_P = c·t_P$ to within a 1 percent tolerance window.
proof idea
The proof constructs the structure by direct field assignment. It supplies the already-proved positivity theorems for the SI Planck length and time. The two consistency fields are discharged by unfolding the three definitions and applying norm_num to confirm the numerical inequalities hold.
why it matters
This declaration closes the SI calibration seam required for any cosmological observable expressed in human units. It certifies that the external CODATA anchors remain positive and internally consistent with the exact speed of light, thereby licensing downstream conversion routines. The result touches no open question and carries zero sorry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.