mapDeltaTime_step
plain-language theorem explainer
The lemma shows that the time component of the delta map increases by exactly the fundamental tick duration τ₀ on each integer step within the subgroup generated by nonzero δ. Modelers of discrete time evolution in RS-native units cite it when verifying uniform tick spacing. The proof is a one-line wrapper that instantiates the general mapDelta_step lemma at the timeMap function after unfolding the relevant definitions.
Claim. Let δ be a nonzero integer, U an RS unit structure containing fundamental time τ₀, and n an integer. Then the difference between the mapped time at the image of n+1 and the image of n under the integer-to-ledger embedding equals τ₀.
background
RSUnits is the minimal structure holding the three base quantities τ₀ (tick duration), ℓ₀ (voxel length), and c together with the relation c τ₀ = ℓ₀. The integer-to-ledger map fromZ embeds multiples of δ into an abstract subgroup used only for bookkeeping. timeMap extracts the time coordinate from a general delta map. tau0 is defined as the placeholder tick duration in both the core constants and the RS-native gauge where it equals one tick.
proof idea
The term proof applies simpa to the definitions of mapDeltaTime and timeMap, then directly invokes the general mapDelta_step lemma with the timeMap function as the target map.
why it matters
The result supplies the uniform time increment required by any consistent delta mapping in the UnitMapping module. It supports the eight-tick octave construction by guaranteeing that each integer step advances time by one fundamental tick. No downstream theorems are recorded, indicating it functions as an internal consistency check rather than a terminal proposition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.