timeMap
plain-language theorem explainer
timeMap constructs the affine map from integers to reals whose slope is the fundamental tick duration τ₀ drawn from an RSUnits bundle and whose offset is zero. Researchers building discrete-to-continuous time conversions in the Recognition Science unit system cite this definition when they need the canonical time scaling for δ-steps. It is a direct record construction that packages the tau0 field into AffineMapZ.
Claim. For an RS-units structure $U$, the time map is the affine function $nmapsto U.tau_0cdot n$ from $mathbb{Z}$ to $mathbb{R}$.
background
The module treats subgroups generated by an integer δ as abstract placeholders for mapping only. AffineMapZ is the structure whose fields are a real slope and real offset, representing the map $n mapsto text{slope}cdot n + text{offset}$. RSUnits is the minimal bundle containing tau0 (tick duration), ell0, and c together with the relation $ccdot tau_0=ell_0$. Upstream, tau0 is supplied as the fundamental tick duration in RS-native units (see Constants.tau0 and RSNativeUnits.U).
proof idea
One-line definition that directly constructs the AffineMapZ record by setting slope to the tau0 field of the supplied RSUnits value and offset to zero.
why it matters
The definition supplies the time component required by mapDeltaTime, mapDeltaTime_fromZ and mapDeltaTime_step inside UnitMapping, and by apply_timeMap and mapDeltaTime_fromZ_one inside RecogSpec.Scales. It therefore implements the time scaling step that converts integer recognition increments into real time intervals within the Recognition framework's unit system.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.