to_seconds
The definition converts a discrete Tick to seconds via direct multiplication by the seconds_per_tick factor from an ExternalCalibration record. Researchers converting RS-native simulation outputs to SI units cite this adapter to keep core theory free of CODATA values. The implementation is a one-line scalar multiplication after coercing the tick to a real number.
claimGiven an external calibration record supplying a factor $s$ (seconds per tick) and a tick $t$, the map yields $t · s$ where $t$ is interpreted as a real number.
background
The module supplies explicit adapters that report RS-native quantities in SI units while keeping the core theory independent of external constants. An ExternalCalibration record is a structure holding conversion factors, with the seconds_per_tick field defined as the scaling from the atomic tick to seconds. The Tick type is the atomic discrete time unit: time advances only in ledger ticks with no background continuous manifold. Upstream results establish the ExternalCalibration structure and the Tick definition as the ledger step.
proof idea
The definition is a one-line wrapper that coerces the input tick to a real number and multiplies it by the seconds_per_tick field of the supplied calibration record.
why it matters in Recognition Science
This definition supplies the primitive conversion used by the downstream measure_to_seconds to lift the map onto Measurement types. It implements the explicit seam required by the module for RS-native to SI reporting and supports the calibration pipeline without embedding numerical constants in the foundation. It aligns with the framework rule that SI conversion occurs only through an externally supplied record.
scope and limits
- Does not prescribe any numerical value for seconds per tick.
- Does not propagate uncertainty or scale factors itself.
- Does not apply to continuous-time or manifold-based models.
- Does not embed CODATA or external constants into the core theory.
Lean usage
measure_to_seconds cal mformal statement (Lean)
25@[simp] noncomputable def to_seconds (cal : ExternalCalibration) (t : Tick) : ℝ :=
proof body
Definition body.
26 (t : ℝ) * cal.seconds_per_tick
27