mapDeltaTime_step
The lemma establishes that advancing one integer step along the subgroup generated by nonzero δ increases the mapped time coordinate by exactly the fundamental tick duration τ₀ of the given RSUnits. Researchers verifying discrete time evolution or unit consistency in Recognition Science would cite it when checking that time increments remain uniform under the integer embedding. The proof is a one-line term wrapper that reduces the claim to the general mapDelta_step lemma applied to the timeMap function.
claimLet δ be a nonzero integer, U an RSUnits structure, and n an integer. Then the time delta map applied to the embedded point fromZ(δ, n+1) minus the time delta map applied to fromZ(δ, n) equals τ₀(U).
background
The UnitMapping module treats the subgroup generated by a fixed nonzero integer δ as an abstract placeholder, with ℤ serving only for indexing. RSUnits is the structure bundling τ₀ (tick duration), ℓ₀ (voxel length), and c with the relation c τ₀ = ℓ₀. mapDeltaTime is obtained by composing the timeMap function with the integer embedding fromZ(δ, ·). Upstream, tau0 is introduced as the fundamental tick duration in Constants (both native and derived forms), while RSNativeUnits.U supplies the gauge where τ₀ = 1.
proof idea
The proof is a one-line term-mode wrapper. It applies simpa to unfold the definitions of mapDeltaTime and timeMap, then directly invokes the general mapDelta_step lemma instantiated at f := timeMap U.
why it matters in Recognition Science
The result supplies the uniform time increment needed for any δ-generated discrete evolution in the unit translation layer. It aligns with the eight-tick octave structure (T7) of the forcing chain by guaranteeing that each integer step corresponds to one fundamental tick. With no downstream uses recorded, it functions as a local consistency lemma supporting later time-evolution theorems.
scope and limits
- Does not treat the case δ = 0.
- Does not extend the mapping to non-integer indices.
- Does not derive τ₀ from the Recognition functional equation.
- Does not address continuous limits of the subgroup.
formal statement (Lean)
103lemma mapDeltaTime_step (δ : ℤ) (hδ : δ ≠ 0)
104 (U : Constants.RSUnits) (n : ℤ) :
105 mapDeltaTime δ hδ U (LedgerUnits.fromZ δ (n+1)) - mapDeltaTime δ hδ U (LedgerUnits.fromZ δ n) = U.tau0 := by
proof body
Term-mode proof.
106 simpa [mapDeltaTime, timeMap] using
107 (mapDelta_step (δ:=δ) (hδ:=hδ) (f:=timeMap U) (n:=n))
108