to_seconds
This definition converts a time value expressed in RS-native ticks to seconds by scaling with the seconds_per_tick factor from an external calibration structure. Researchers mapping Recognition Science ledger times to laboratory data would cite it when bridging abstract units to SI measurements. The implementation is a direct one-line scalar multiplication.
claimLet $cal$ be an external calibration structure containing the factor $s$ (seconds per tick) and let $t$ be a real number representing time in ticks. The converted time in seconds is $t · s$.
background
The RS-native measurement system takes the tick as its base time unit, defined as one discrete ledger posting interval. Time is formalized as an abbreviation for the reals, so any real number can stand for a count of ticks. ExternalCalibration is the structure that supplies the explicit conversion constants, including seconds_per_tick, meters_per_voxel, and joules_per_coh, together with positivity proofs for each factor.
proof idea
One-line definition that multiplies the input tick count by the seconds_per_tick field of the supplied calibration structure.
why it matters in Recognition Science
The definition supplies the concrete time conversion used by measure_to_seconds in the SI calibration module, allowing RS-native measurements to be expressed in laboratory seconds. It realizes the optional SI anchoring described in the module documentation while preserving the native c = 1 and phi-ladder conventions of the framework.
scope and limits
- Does not assign a numerical value to seconds_per_tick.
- Does not propagate measurement uncertainties.
- Does not enforce the positivity constraint (that is recorded in the calibration structure itself).
formal statement (Lean)
307@[simp] noncomputable def to_seconds (cal : ExternalCalibration) (t : Time) : ℝ :=
proof body
Definition body.
308 t * cal.seconds_per_tick
309
310/-- Convert length (in voxels) to meters. -/