apply_timeMap
The lemma shows that the time map derived from RS units U applied to integer tick count n returns exactly n times the fundamental tick duration tau0. Modelers of discrete time evolution in Recognition Science cite it when converting lattice steps to continuous time in scale derivations. The proof is a direct simplification that unfolds the apply operator and timeMap definition.
claimLet $U$ be an RS unit system with fundamental tick duration $τ_0$. For any integer $n$, the time map applied to $n$ satisfies $apply(timeMap(U), n) = τ_0 · n$.
background
The module develops binary scales and φ-exponential wrappers for Recognition Science quantities. RSUnits is the structure holding the fundamental constants tau0 (tick duration), ell0 (voxel length), and c (speed of light) with the relation c · tau0 = ell0. Upstream results define tau0 as the base time unit, set to 1 tick in the RS-native gauge where c = 1 and ell0 = 1 voxel.
proof idea
The proof is a one-line wrapper that applies simp using the definitions of apply and timeMap.
why it matters in Recognition Science
The lemma supplies the concrete scaling rule for time in the binary scales framework, anchoring it to the fundamental tick duration tau0 from Constants. It supports consistent conversion between integer steps and real time in scale-based derivations, consistent with the eight-tick octave structure in the forcing chain. No direct downstream uses appear in the current graph.
formal statement (Lean)
161@[simp] lemma apply_timeMap (U : Constants.RSUnits) (n : ℤ) :
162 apply (timeMap U) n = U.tau0 * (n : ℝ) := by simp [apply, timeMap]
proof body
Term-mode proof.
163
164-- (no actionMap in minimal RSUnits)
165
166/-- Specialization of `mapDelta` to δ = 1 using the canonical projection. -/