tau0_seconds_protocol
plain-language theorem explainer
Defines the single-anchor SI calibration protocol by supplying only τ₀ in seconds per RS tick as the empirical input. Researchers reporting RS-native predictions in SI units cite this definition to fix the reporting scale without introducing fit parameters or tuning dimensionless quantities. The definition directly constructs a Protocol record with name, summary, hypothesis status, two assumptions on measurement stability, and two falsifiers for consistency checks.
Claim. The single-anchor SI calibration protocol is the Protocol record that accepts one empirical scalar τ₀ (seconds per RS tick) and derives meters_per_voxel from the SI definition of c = 299792458 m/s together with joules_per_coh from the SI definition of h (hence ħ = h/(2π)) and the RS identity 1 act = 1 coh × 1 tick.
background
RS-native theory runs in tick/voxel/coh/act units with c = 1 and no SI numerals. The module supplies a concrete single-anchor calibration seam: the sole empirical scalar is τ₀ (seconds per tick). Meters per voxel follows from the exact SI definition of c; joules per coh follows from the exact SI h together with the RS identity act = coh · tick. Upstream, the fundamental tick is defined as 1 in RS-native units (Constants.tick) and ħ is set to φ^{-5} in those units (Constants.hbar). The protocol is marked hypothesis because τ₀ is treated as measured input rather than derived.
proof idea
The definition constructs the Protocol record inline. It sets the name field to the calibration identifier, the summary to the single-anchor derivation description, status to hypothesis, assumptions to the two listed conditions on τ₀ stability and SI definitional constants, and falsifiers to the two consistency checks on independent anchors and speed consistency.
why it matters
This definition supplies the protocol used by CalibrationCert and mkCert to bundle a measured τ₀ with the derived ExternalCalibration. It implements the explicit seam described in the module documentation, ensuring no dimensionless RS predictions receive fit freedom. It connects to the RS-native constants where tick and ħ are defined and supports the overall measurement framework for SI reporting. The parent structure CalibrationCert depends on it directly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.