CalibrationCert
CalibrationCert bundles one measured scalar τ₀ in seconds with a protocol equality check and a positivity guarantee. Researchers converting RS-native tick/voxel measurements to SI units cite it as the minimal input that produces a full ExternalCalibration without extra fit parameters. The declaration is a direct structure definition whose three fields enforce the single-anchor protocol and the positivity of τ₀.
claimA structure consisting of a measurement record τ₀ of type Measurement ℝ, a proof that its protocol equals the canonical single-anchor protocol, and a proof that the value of τ₀ is strictly positive.
background
In the RS-native framework all quantities live in tick/voxel/coh/act units with c = 1. The module supplies a concrete single-anchor protocol that lets users report SI values by supplying only one empirical scalar: seconds per tick (τ₀). Everything else (meters per voxel from the SI definition of c, joules per coherence from the SI definition of ħ) is derived or definitional. The upstream ExternalCalibration structure records seconds_per_tick, meters_per_voxel and joules_per_coh; the various tau0_pos lemmas establish that the fundamental tick duration is positive.
proof idea
Structure definition with three fields. The first field is a Measurement record, the second is the literal equality cert.tau0_seconds.protocol = tau0_seconds_protocol, and the third is the positivity assertion 0 < tau0_seconds.value. No lemmas or tactics are invoked beyond the record constructor.
why it matters in Recognition Science
CalibrationCert is the canonical input object for the single-anchor calibration path. It is consumed by the calibration function that builds ExternalCalibration and by the downstream theorems c_reports_exact and one_act_reports_hbar, which recover the SI values of c and ħ respectively. The construction therefore closes the seam between the RS forcing chain (T0–T8) and experimental reporting while keeping every quantity beyond τ₀ fixed by SI definitions.
scope and limits
- Does not prescribe any numerical value for τ₀.
- Does not derive τ₀ from the RS forcing chain or Recognition Composition Law.
- Does not support multi-anchor or parameter-fitting calibrations.
- Does not propagate measurement uncertainty beyond the positivity check.
Lean usage
def exampleCert : CalibrationCert := mkCert 1.0 (by norm_num)formal statement (Lean)
121structure CalibrationCert where
122 /-- The single empirical scalar: τ₀ in seconds (seconds per tick). -/
123 tau0_seconds : Measurement ℝ
124 /-- Protocol is the canonical single-anchor protocol. -/
125 protocol_ok : tau0_seconds.protocol = tau0_seconds_protocol
126 /-- Positivity: τ₀ must be positive. -/
127 tau0_pos : 0 < tau0_seconds.value
128
129/-- The derived `ExternalCalibration` associated to a certificate. -/