mapDelta_diff
plain-language theorem explainer
mapDelta_diff establishes that for nonzero integer δ, affine map f, and p, q in the δ-subgroup, the difference of their mapDelta images equals f.slope times the integer difference of their toZ projections. Researchers constructing unit maps for charge and time scales in Recognition Science cite it to confirm difference preservation under affine scaling. The proof expands the mapDelta definition in a calc chain then simplifies via ring and integer cast lemmas.
Claim. Let $δ ∈ ℤ$ with $δ ≠ 0$, let $f$ be an affine map $ℤ → ℝ$ with slope $m$ and offset $b$, and let $p, q$ belong to the subgroup generated by $δ$. Then mapDelta$(δ, f, p)$ − mapDelta$(δ, f, q)$ = $m ⋅ ($toZ$_δ(p) − $toZ$_δ(q))$, where toZ$_δ$ recovers the integer coefficient $n$ such that the subgroup element equals $n ⋅ δ$.
background
DeltaSub δ is the subgroup of ℤ consisting of all integer multiples of δ, used as an abstract placeholder for discrete units. AffineMapZ is the structure carrying a real slope and offset that defines the map n ↦ slope ⋅ n + offset. mapDelta composes this affine map with the toZ projection that extracts the generating integer from a subgroup element.
proof idea
The tactic proof opens a calc block that substitutes the definition of mapDelta to obtain (slope ⋅ toZ(p) + offset) − (slope ⋅ toZ(q) + offset). Ring cancels the offsets and factors the slope; simpa together with Int.cast_sub then equates the cast of the integer difference to the real subtraction.
why it matters
The lemma is invoked by the downstream mapDelta_diff_toZ to specialize the projection via LedgerUnits.toZ. It guarantees that differences in mapped values depend only on slope and discrete separation, independent of offset. This algebraic control supports consistent construction of charge (qe) and time (τ0) maps inside the Recognition Science unit-mapping layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.