timeMap
The definition supplying the affine map from integers to real time sets its slope to the fundamental tick duration τ₀ taken from an RS unit system and its offset to zero. Researchers constructing discrete-to-continuous conversions in Recognition Science would cite this construction when assembling delta-time mappings. It proceeds by direct record construction of the affine-map structure.
claimGiven an RS unit system $U$, the time-mapping function returns the affine map sending each integer $n$ to $U.τ_0 · n$ from $ℤ$ to $ℝ$.
background
UnitMapping realizes mappings for time, charge and action as affine functions on the integer subgroup generated by a step δ. The structure AffineMapZ holds the slope and offset of such a map. An RSUnits record bundles τ₀ (tick duration), ℓ₀ (voxel length) and c (speed of light) together with the relation c τ₀ = ℓ₀. The component τ₀ is defined in Constants as the fundamental tick duration and instantiated to 1 in the RS-native gauge. Upstream, τ₀ appears as a placeholder in Compat.Constants and is derived from codata constants in Constants.Derivation.
proof idea
This is a direct definition that constructs the AffineMapZ record by setting its slope field to the τ₀ component of the input RSUnits record and its offset field to zero.
why it matters in Recognition Science
The construction is used to define mapDeltaTime in the same module and is applied in lemmas such as apply_timeMap and mapDeltaTime_fromZ_one in RecogSpec.Scales. It supplies the time component required for unit-consistent conversion of recognition steps into physical time intervals in the Recognition Science framework.
scope and limits
- Does not assign a concrete numerical value to the tick duration τ₀.
- Does not define a corresponding map for action, which would require an explicit Planck constant.
- Does not extend the domain beyond integer steps.
- Does not incorporate the speed-of-light consistency relation from the RSUnits record.
Lean usage
lemma example (U : Constants.RSUnits) (n : ℤ) : apply (timeMap U) n = U.tau0 * (n : ℝ) := by simp [apply, timeMap]formal statement (Lean)
58def timeMap (U : Constants.RSUnits) : AffineMapZ := { slope := U.tau0, offset := 0 }
proof body
Definition body.
59
60/-- WIP: action mapping requires Planck-like constant. Pass it explicitly. -/