mkCert
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.
claimGiven 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 in Recognition Science
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.
scope and limits
- Does not compute τ₀ from first principles or from other RS constants.
- Does not support multi-anchor or multi-parameter calibration protocols.
- Does not propagate measurement uncertainty beyond the supplied scalar value.
- Does not verify numerical consistency with other SI constants such as G or α.
formal statement (Lean)
164def mkCert (tau0_s : ℝ) (htau : 0 < tau0_s) : CalibrationCert :=
proof body
Definition body.
165 { tau0_seconds :=
166 { value := tau0_s
167 protocol := tau0_seconds_protocol
168 notes := ["Units: SI seconds per RS tick (single-anchor calibration seam)."] }
169 protocol_ok := rfl
170 tau0_pos := htau
171 }
172
173end
174
175end SingleAnchor
176end Calibration
177end RSNative
178end Measurement
179end IndisputableMonolith