mapDeltaTime_fromZ_one
plain-language theorem explainer
The lemma shows that mapping an integer ledger step fromZ_one n through timeMap U yields a real duration exactly tau0 times n. Researchers verifying time increments on binary scales in Recognition Science cite this when confirming linear scaling from ledger units to physical time. The proof is a one-line simp that unfolds mapDeltaOne and timeMap then invokes add_comm.
Claim. Let $U$ be an RS unit structure with fundamental tick duration $τ_0$. For any integer $n$, the mapped time delta obtained by applying timeMap $U$ to the one-step ledger unit fromZ_one $n$ equals $τ_0 · n$.
background
The module RecogSpec.Scales develops binary scales and φ-exponential wrappers. RSUnits is the minimal structure bundling $τ_0$ (tick duration), $ℓ_0$, and $c$ subject to $c · τ_0 = ℓ_0$. fromZ_one converts an integer to a ledger unit; timeMap supplies the corresponding time scaling for a given RS unit. Upstream, tau0 is defined as the duration of one tick in RS-native units (Constants.tau0 and Compat.Constants.tau0), while Constants.RSUnits.U supplies the gauge with $τ_0 = 1$ tick.
proof idea
The proof is a one-line simp wrapper that unfolds mapDeltaOne and timeMap, then applies add_comm to finish the algebraic reduction.
why it matters
This lemma supplies a basic consistency check for time scaling inside the binary-scales machinery of Recognition Science. It aligns with the eight-tick octave and the linear step on the phi-ladder in the T0-T8 forcing chain. No downstream theorems are recorded yet, so its role in higher mass or constant derivations remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.