mapDeltaTime
plain-language theorem explainer
This definition constructs an affine map from the subgroup generated by a nonzero integer δ to the reals, scaled via the time component of the RS units structure U. Researchers converting discrete ledger steps to continuous time intervals in Recognition Science calculations would cite it for unit translations. It is realized as a direct composition of the general delta mapping with the time scaling function.
Claim. Let $Δ_δ$ be the subgroup generated by the nonzero integer $δ$. The map $Δ_δ → ℝ$ is obtained by composing the general $δ$-mapping operator with the time scaling function induced by the RS units structure $U = (τ_0, ℓ_0, c)$.
background
DeltaSub δ is defined simply as the integers ℤ and serves as an abstract placeholder for the subgroup generated by δ, used only for mapping purposes. The RSUnits structure consists of the base quantities tau0 (time tick), ell0 (length voxel), and c (speed) satisfying the relation c ⋅ tau0 = ell0. This definition lives in the UnitMapping module, which translates discrete integer steps into physical quantities using Recognition Science constants and draws on upstream definitions of RSUnits together with the general mapDelta construction.
proof idea
The definition is a one-line wrapper that applies the general mapDelta function instantiated with the timeMap derived from the supplied RS units U.
why it matters
This supplies the time-specific instance of the delta mapping and is invoked directly by the lemmas mapDeltaTime_fromZ and mapDeltaTime_step, which establish that the map sends the generator n to n ⋅ τ₀ and that consecutive steps differ by exactly τ₀. It completes the affine time component of the unit system in Recognition Science, consistent with the native tick τ₀ = 1. No open questions are resolved here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.