timeMap
plain-language theorem explainer
timeMap constructs the affine map from ℤ to ℝ with slope equal to the fundamental tick duration τ₀ taken from an RSUnits record and with zero offset. Workers on discrete-to-continuous mappings in Recognition Science cite it when converting integer recognition steps into physical time intervals. The definition is a direct record literal with no computation or lemmas.
Claim. For RS units $U$, the time map is the affine map $nmapsto U.τ_0·n$ from $ℤ$ to $ℝ$ (offset zero).
background
AffineMapZ is the structure whose fields are slope : ℝ and offset : ℝ, so that the map sends $n$ to slope·$n$ + offset. RSUnits bundles the minimal constants τ₀, ℓ₀, c together with the relation $c·τ_0=ℓ_0$. The module supplies abstract integer-to-real maps for the subgroup generated by a fixed δ, using these units as coefficients. Upstream, tau0 is defined as the duration of one tick in RS-native units (where τ₀ = 1).
proof idea
Direct definition that builds the AffineMapZ record with slope := U.tau0 and offset := 0. No tactics or lemmas are invoked.
why it matters
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 anchors the time scaling used in the Recognition Composition Law and the eight-tick octave. The definition remains open on the numerical value of τ₀ and on the inclusion of an action (ħ) map.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.