mapDeltaTime_fromZ
The lemma establishes that the time component of the delta map applied to the integer-generated ledger unit fromZ δ n equals U.tau0 multiplied by the integer n. Researchers handling unit conversions in Recognition Science models would cite this when reducing time intervals on the integer subgroup to native tick units. The proof is a direct one-line wrapper invoking the general mapDelta_fromZ lemma on the timeMap function and simplifying via the definitions of mapDeltaTime and timeMap.
claimLet $δ ∈ ℤ$ with $δ ≠ 0$, let $U$ be an RS-units structure, and let $n ∈ ℤ$. Then the time-delta mapping satisfies mapDeltaTime(δ, U, fromZ(δ, n)) = U.τ₀ ⋅ n.
background
RSUnits is the structure holding the three base quantities τ₀ (tick duration), ℓ₀ (voxel length), and c (speed) together with the relation c ⋅ τ₀ = ℓ₀. The constant τ₀ itself is defined as the fundamental tick in RS-native units. LedgerUnits.fromZ δ n constructs the abstract ledger element generated by the integer subgroup of δ. mapDeltaTime is the time projection of the general delta-mapping operator that acts on these ledger elements. The module treats the subgroup generated by δ as an abstract placeholder realized via integers solely for mapping purposes.
proof idea
The proof is a term-mode one-liner. It obtains an instance of the general mapDelta_fromZ lemma by instantiating the function argument with timeMap U, then applies simpa using the definitions of mapDeltaTime, timeMap, and add_comm to reach the target equality.
why it matters in Recognition Science
The result supplies an explicit evaluation rule inside the UnitMapping layer that converts abstract integer ledger units into physical time intervals measured in RS-native ticks. It sits downstream of the RSUnits and tau0 definitions and supports the larger unit-conversion infrastructure required by the Recognition Science forcing chain. No immediate parent theorems are recorded among the used-by edges, leaving the lemma as a self-contained computational closure for time mappings.
scope and limits
- Does not apply when δ = 0.
- Does not treat non-integer ledger elements.
- Does not compute spatial or charge components of the same delta.
- Does not insert numerical values for τ₀ or φ.
formal statement (Lean)
96@[simp] lemma mapDeltaTime_fromZ (δ : ℤ) (hδ : δ ≠ 0)
97 (U : Constants.RSUnits) (n : ℤ) :
98 mapDeltaTime δ hδ U (LedgerUnits.fromZ δ n) = U.tau0 * (n : ℝ) := by
proof body
Term-mode proof.
99 classical
100 have h := mapDelta_fromZ (δ:=δ) (hδ:=hδ) (f:=timeMap U) (n:=n)
101 simpa [mapDeltaTime, timeMap, add_comm] using h
102