calibration_protocol_hygienic
plain-language theorem explainer
The theorem establishes that any CalibrationCert built from the canonical single-anchor protocol satisfies the hygienic property on its embedded protocol. Researchers performing RS-native to SI unit conversion cite it to confirm that no extraneous parameters enter the reporting chain. The proof is a one-line wrapper that rewrites via the certificate's protocol_ok field and invokes the base hygienic theorem for tau0_seconds_protocol.
Claim. Let cert be a calibration certificate containing a single empirical scalar τ₀ in seconds together with the canonical single-anchor protocol. Then the protocol associated with cert.τ₀ is hygienic.
background
The module supplies a concrete single-anchor calibration protocol that converts RS-native measurements (tick/voxel/coh) into SI units while introducing only one empirical scalar. RS theory runs with c=1; the anchor τ₀ (seconds per tick) determines meters_per_voxel via the exact SI value of c and joules_per_coh via the exact SI value of h together with the identity 1 act = 1 coh × 1 tick. The structure CalibrationCert bundles τ₀, asserts that its protocol equals the canonical tau0_seconds_protocol, and records positivity of τ₀.
proof idea
The proof is a one-line wrapper. It applies the protocol_ok field of the certificate to rewrite the protocol to the canonical tau0_seconds_protocol, then invokes the base theorem tau0_seconds_protocol_hygienic via simpa.
why it matters
This result closes the hygienic verification step for the single-anchor calibration path, ensuring SI reporting derived from one measured τ₀ introduces no additional parameters. It supports the module claim that all quantities beyond τ₀ are either definitional or fixed by the SI definitions of c and h. The declaration sits inside the consistency-check section that follows the main calibration construction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.