SICalibrationCert
plain-language theorem explainer
This structure packages a certificate confirming that the SI Planck length and time are positive and satisfy approximate consistency with the exact SI speed of light. Cosmologists converting RS-native predictions to observables such as the SH0ES Hubble constant would cite it to validate the calibration seam. The definition simply assembles four fields: two positivity statements and two numerical inequalities checked via unfolding and norm_num.
Claim. A structure whose fields assert that the SI Planck length satisfies $0 < 1.616255e-35$, the SI Planck time satisfies $0 < 5.391247e-44$, and the derived quantities obey $1.616255e-35 / 299792458 < 5.391247e-44 * 1.01$ together with $5.391247e-44 * 0.99 < 1.616255e-35 / 299792458$.
background
The module supplies SI anchor constants that convert RS-native units (where $c = 1$) into meters, seconds, and km/s/Mpc for comparison with observations. planck_length_SI is the CODATA 2018 value $1.616255e-35$ m; planck_time_SI is the corresponding $5.391247e-44$ s; c_SI is the exact 2019 SI value 299792458 m/s. These are external experimental anchors, not RS predictions; the theoretical content lies in the ratios that use them. Upstream results from Constants.ExternalAnchors and local siblings provide the exact numerical definitions and positivity lemmas.
proof idea
The declaration is a structure definition that collects four fields. Downstream theorem si_calibration_cert populates the structure by supplying planck_length_SI_pos and planck_time_SI_pos for the positivity fields and applying norm_num after unfolding the three constants for the two consistency inequalities.
why it matters
The certificate is consumed by si_calibration_cert to certify the SI calibration seam that lets RS predictions be expressed in human units. It supports the module's goal of bridging native units to late-universe observables such as the SH0ES H0 value 73.04 km/s/Mpc while keeping the theoretical ratios inside RS. The construction touches the framework's use of external anchors for empirical comparison without claiming to derive the SI numbers from the phi-ladder or RCL.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.