mapDelta_fromZ
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.
claimLet $δ ∈ ℤ$ 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 in Recognition Science
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.
scope and limits
- Does not apply when δ = 0.
- Does not compute explicit numerical values of slope or offset.
- Does not extend the result to non-integer indices.
- Does not address group structures other than DeltaSub δ.
Lean usage
have h := mapDelta_fromZ δ hδ f nformal statement (Lean)
75@[simp] lemma mapDelta_fromZ (δ : ℤ) (hδ : δ ≠ 0) (f : AffineMapZ) (n : ℤ) :
76 mapDelta δ hδ f (LedgerUnits.fromZ δ n) = f.slope * (n : ℝ) + f.offset := by
proof body
Term-mode proof.
77 classical
78 simp [mapDelta, LedgerUnits.toZ_fromZ δ hδ]
79