mapDelta_fromZ
plain-language theorem explainer
The lemma shows that composing the fromZ construction with mapDelta recovers the affine evaluation on the integer index n. Researchers formalizing unit conversions for charge, time, and action in Recognition Science cite it when reducing lattice expressions. The proof is a one-line term simplification that unfolds mapDelta and substitutes the retraction toZ_fromZ.
Claim. Let $δ ∈ ℤ$ with $δ ≠ 0$, let $f$ be an affine map $ℤ → ℝ$ given by $f(k) = s·k + o$, and let $n ∈ ℤ$. Then mapDelta_δ(f)(fromZ_δ(n)) = s·n + o.
background
The UnitMapping module treats the subgroup generated by a fixed nonzero integer δ, with n serving as an abstract integer index for mapping purposes. AffineMapZ is the structure carrying a real slope and offset, so that the map sends n to slope·n + offset. The constructor fromZ δ n produces the corresponding element of DeltaSub δ, while mapDelta δ hδ f applies the affine map after projecting the subgroup element back to its integer coefficient via toZ.
proof idea
The proof is a one-line term-mode wrapper. It invokes classical, then simp with the definitions of mapDelta and the upstream lemma toZ_fromZ δ hδ, which replaces the projection with n and yields the slope-offset expression.
why it matters
The lemma is invoked directly by the downstream results mapDeltaTime_fromZ and mapDeltaAction_fromZ, which specialize it to the time and action affine maps. It ensures consistent affine scaling across δ-subgroups, supporting the Recognition Science unit conversions that relate τ0, ħ, and the phi-ladder constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.