timeMap
plain-language theorem explainer
Recognition Science equips each RSUnits record with a canonical affine map that converts integer tick counts n into real time via multiplication by the native tick duration τ₀. Workers on discrete-to-continuous mappings in the framework cite this definition when building delta-time and step lemmas. The implementation is a direct record constructor that sets slope to U.tau0 and offset to zero, inheriting simp rules from AffineMapZ.
Claim. For RS units $U$, the time map is the affine map $nmapsto tau_0(U)cdot n$ from $mathbb{Z}$ to $mathbb{R}$, where $tau_0(U)$ is the fundamental tick duration supplied by $U$.
background
The RecogSpec.Scales module supplies binary-scale and φ-exponential wrappers for Recognition Science. AffineMapZ is the structure whose fields are a real slope and a real offset, so that the map sends each integer n to slope·n + offset. RSUnits is the minimal record containing tau0, ell0 and c together with the relation c·tau0 = ell0; its tau0 field is the fundamental tick duration in native units. Upstream, tau0 is defined as the duration of one tick (both in Compat.Constants and in the main Constants module), while hbar is derived from it as φ^{-5} in RS-native units.
proof idea
Direct definition that constructs the AffineMapZ record literal with slope := U.tau0 and offset := 0. No lemmas or tactics are invoked; the declaration is the canonical constructor for the time affine map.
why it matters
timeMap supplies the time component required by the UnitMapping module's mapDeltaTime family and by the specializations apply_timeMap and mapDeltaTime_fromZ_one inside RecogSpec.Scales. It realizes the fundamental time scaling of the T7 eight-tick octave inside RS-native units (c = 1) without invoking action or hbar, which are omitted from the minimal RSUnits structure. The definition therefore closes the time half of the affine-mapping interface used throughout the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.