mapDelta_diff_toZ
plain-language theorem explainer
The lemma shows that the difference of mapDelta applications on a δ-subgroup equals the affine slope times the integer difference of the toZ projections. Researchers aligning ledger units with recognition scales cite it to confirm difference preservation under unit maps. The proof is a one-line wrapper that reduces via simpa to the general mapDelta_diff after classical choice.
Claim. Let $δ ∈ ℤ$ with $δ ≠ 0$, let $f$ be an affine map $n ↦ m·n + b$ with slope $m$, and let $p, q$ lie in the subgroup generated by $δ$. Then $map_δ(f,p) - map_δ(f,q) = m · (toZ_δ(p) - toZ_δ(q))$, where $toZ_δ$ extracts the integer coefficient of the generator.
background
DeltaSub δ is the subgroup of ℤ generated by δ, realized as the set of integer multiples of δ. AffineMapZ is the structure of maps from ℤ to ℝ given by slope and offset. mapDelta applies such an affine map after projecting a subgroup element to its integer coefficient via toZ.
proof idea
The proof invokes classical choice to handle the noncomputable projection, then applies simpa to reduce directly to the sibling lemma mapDelta_diff.
why it matters
The result guarantees that affine differences are preserved under the unit-mapping projection, ensuring linear consistency when transporting scales between LedgerUnits and RecogSpec.Scales. It supports the abstract placeholder layer in UnitMapping for later alignment of physical constants. No downstream uses are recorded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.