mapDeltaTime_step
plain-language theorem explainer
The lemma shows that advancing one step along the integer subgroup generated by nonzero δ under the time mapping produces a difference of exactly the fundamental tick duration τ₀ from the RSUnits structure. Researchers verifying consistency of time increments in Recognition Science unit mappings would cite it. The proof is a one-line wrapper that instantiates the general mapDelta_step lemma at the timeMap function.
Claim. Let δ be a nonzero integer, U an RSUnits structure, and n an integer. Then the difference between the time-mapped values at the (n+1)th and nth points of the δ-generated subgroup equals the fundamental tick duration τ₀ of U: mapDeltaTime(δ, U, fromZ(δ, n+1)) − mapDeltaTime(δ, U, fromZ(δ, n)) = U.τ₀.
background
The module treats mappings over the abstract subgroup generated by a fixed nonzero integer δ, with integers serving as placeholders. RSUnits is the structure holding the base units τ₀ (tick duration), ℓ₀ (voxel length), and c (speed of light) satisfying the relation c τ₀ = ℓ₀. The time mapping mapDeltaTime is obtained by composing timeMap with the fromZ embedding of integers into the subgroup. Upstream results supply the definition of τ₀ as the duration of one tick and the RSNativeUnits gauge in which τ₀ = 1.
proof idea
One-line wrapper that applies mapDelta_step (δ:=δ) (hδ:=hδ) (f:=timeMap U) (n:=n) and simplifies using the definitions of mapDeltaTime and timeMap.
why it matters
The result confirms that time increments remain uniform and equal to the base tick τ₀ under the δ-subgroup mapping, supporting the overall construction of affine maps in the UnitMapping module. It aligns with the Recognition Science requirement that time advances occur in discrete ticks consistent with the eight-tick octave and the RS-native constants. No downstream uses are recorded, indicating it functions as an internal consistency check rather than a terminal theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.