mkCert
plain-language theorem explainer
mkCert assembles a CalibrationCert record from a user-supplied positive real number τ₀ that represents seconds per RS tick. Workers converting RS-native quantities to SI units invoke it to supply the single empirical anchor required by the single-anchor protocol. The definition is a direct structure constructor that fixes the protocol field to the canonical single-anchor protocol and copies the positivity hypothesis into the certificate.
Claim. Given a positive real number τ₀ (seconds per tick), the function returns a calibration certificate whose τ₀-seconds component is the measurement record carrying value τ₀ under the single-anchor protocol, together with a reflexivity proof that the protocol matches and the supplied witness that τ₀ > 0.
background
RS-native theory runs in tick/voxel/coh/act units with c = 1 and no SI numerals. To obtain SI reporting, a calibration seam is introduced that supplies only one empirical scalar, τ₀ (seconds per tick). Meters per voxel then follow from the SI definition of c and joules per coherence from the SI value of ħ together with the identity 1 act = 1 coh × 1 tick. The CalibrationCert structure bundles the empirical τ₀ measurement, a proof that its protocol equals the canonical single-anchor protocol, and a positivity proof. Upstream lemmas establish positivity of the fundamental tick in RS units and define the tick itself as the duration of one RS time quantum.
proof idea
The definition is a direct structure constructor. It initializes the tau0_seconds field as a Measurement record whose value is the input real and whose protocol is the fixed single-anchor protocol, sets the protocol_ok field to reflexivity, and assigns the tau0_pos field to the input positivity hypothesis.
why it matters
This definition supplies the single empirical anchor required for SI reporting of RS-native results under the single-anchor protocol. It implements the calibration seam that lets downstream code derive the full ExternalCalibration from one measured scalar. The construction aligns with the Recognition Science framework by providing the interface between RS-native constants (tick duration, ħ = ϕ^{-5}) and SI units without introducing fit parameters. No parent theorem is yet recorded among the used-by edges.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.