tau0_seconds_protocol_hygienic
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not supply numerical values for any calibration constants.
- Does not address multi-anchor or data-fitting calibrations.
- Does not verify physical accuracy of the derived SI units.
formal statement (Lean)
93theorem tau0_seconds_protocol_hygienic : Protocol.hygienic tau0_seconds_protocol := by
proof body
Term-mode proof.
94 simp [Protocol.hygienic, tau0_seconds_protocol]
95
96/-! ## Derive the full `ExternalCalibration` from one scalar -/
97
98/-- Build a full `ExternalCalibration` from one scalar: τ₀ in seconds. -/