to_seconds
plain-language theorem explainer
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.
Claim. Given 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.