tau0_seconds_protocol_hygienic
plain-language theorem explainer
The theorem verifies that the single-anchor SI calibration protocol satisfies the hygiene predicate. Researchers establishing RS-native to SI reporting seams cite this result to confirm protocol validity without extra parameters. The proof is a direct simplification that unfolds the protocol definition and the hygiene predicate.
Claim. The single-anchor protocol with name ``calibration.single_anchor.tau0_seconds'' satisfies the hygiene predicate: its name is nonempty and its status does not trigger the requirement for nonempty assumptions or falsifiers.
background
The module supplies a single-anchor calibration that takes only one empirical scalar, seconds per tick, and derives meters per voxel from the SI definition of c together with joules per coherence from the SI definition of h using the RS identity that one action equals one coherence times one tick. ExternalCalibration packages these three mappings as a structure. The hygiene predicate requires a nonempty name and, for hypothesis or scaffold status, nonempty assumptions and falsifiers.
proof idea
The proof is a one-line wrapper that applies simp to the definitions of hygienic and tau0_seconds_protocol.
why it matters
This theorem feeds the downstream result calibration_protocol_hygienic, which lifts the hygiene check to a full CalibrationCert. It closes the hygiene requirement for the single-anchor protocol described in the module documentation, keeping the calibration a pure reporting seam aligned with the RS framework's single-scalar anchor design.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.