mapDelta_diff_toZ
plain-language theorem explainer
The lemma shows that the difference of two mapDelta applications equals the slope times the integer difference of their toZ projections. Researchers formalizing affine mappings between integer subgroups and reals in Recognition Science would cite it for difference preservation. The proof is a one-line wrapper applying mapDelta_diff after classical reasoning and simplification.
Claim. Let $δ ∈ ℤ$ be nonzero, let $f$ be an affine map $ℤ → ℝ$ with slope $m$, and let $p, q$ belong to the subgroup generated by $δ$. Then mapDelta(δ, f, p) − mapDelta(δ, f, q) = $m · (toZ(δ, p) − toZ(δ, q))$, where toZ projects each subgroup element to its integer coefficient.
background
In UnitMapping, DeltaSub δ is defined simply as ℤ, serving as an abstract placeholder for the subgroup generated by δ. AffineMapZ is the structure with fields slope : ℝ and offset : ℝ, encoding maps of the form n ↦ slope·n + offset. The mapDelta operation composes such an affine map with a projection to ℤ, producing a map into ℝ.
proof idea
The proof is a one-line wrapper that applies the mapDelta_diff lemma after classical reasoning and simpa simplification.
why it matters
This lemma ensures difference preservation under affine maps in the unit-mapping layer, supporting consistent translation between discrete δ-subgroups and real values. It builds on the DeltaSub and toZ definitions from LedgerUnits and the mapDelta construction from RecogSpec.Scales, aligning with the abstract integer mappings used throughout the Recognition framework for scale handling.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.