CalibrationCert
plain-language theorem explainer
CalibrationCert bundles one measured scalar τ₀ in seconds with a protocol equality check and a positivity guarantee. Researchers converting RS-native tick/voxel measurements to SI units cite it as the minimal input that produces a full ExternalCalibration without extra fit parameters. The declaration is a direct structure definition whose three fields enforce the single-anchor protocol and the positivity of τ₀.
Claim. A structure consisting of a measurement record τ₀ of type Measurement ℝ, a proof that its protocol equals the canonical single-anchor protocol, and a proof that the value of τ₀ is strictly positive.
background
In the RS-native framework all quantities live in tick/voxel/coh/act units with c = 1. The module supplies a concrete single-anchor protocol that lets users report SI values by supplying only one empirical scalar: seconds per tick (τ₀). Everything else (meters per voxel from the SI definition of c, joules per coherence from the SI definition of ħ) is derived or definitional. The upstream ExternalCalibration structure records seconds_per_tick, meters_per_voxel and joules_per_coh; the various tau0_pos lemmas establish that the fundamental tick duration is positive.
proof idea
Structure definition with three fields. The first field is a Measurement record, the second is the literal equality cert.tau0_seconds.protocol = tau0_seconds_protocol, and the third is the positivity assertion 0 < tau0_seconds.value. No lemmas or tactics are invoked beyond the record constructor.
why it matters
CalibrationCert is the canonical input object for the single-anchor calibration path. It is consumed by the calibration function that builds ExternalCalibration and by the downstream theorems c_reports_exact and one_act_reports_hbar, which recover the SI values of c and ħ respectively. The construction therefore closes the seam between the RS forcing chain (T0–T8) and experimental reporting while keeping every quantity beyond τ₀ fixed by SI definitions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.