mapDelta_diff
plain-language theorem explainer
The lemma proves that the difference of two images under mapDelta equals the affine slope times the integer difference of their toZ projections. Unit-mapping constructions in Recognition Science cite it when converting discrete subgroup elements to real quantities while preserving differences. The proof expands the mapDelta definition, cancels offsets, and reduces via ring and cast lemmas.
Claim. Let $δ ∈ ℤ$ with $δ ≠ 0$, let $f$ be an affine map $ℤ → ℝ$ given by slope $m$ and offset $b$, and let $p, q$ belong to the subgroup generated by $δ$. Then mapDelta$(δ, hδ, f, p)$ − mapDelta$(δ, hδ, f, q)$ = $m · ((toZ(δ, p) − toZ(δ, q) : ℤ) : ℝ)$.
background
Module UnitMapping supplies affine maps from abstract δ-subgroups to real numbers for unit conversion. DeltaSub δ is defined locally as ℤ (abstract placeholder for the subgroup generated by δ). AffineMapZ is the structure with fields slope : ℝ and offset : ℝ. Upstream LedgerUnits.DeltaSub is the actual subgroup {x : ℤ // ∃ n, x = n·δ} and toZ extracts the integer coefficient via Classical.choose.
proof idea
The tactic proof uses a calc block. First simp [mapDelta] expands both sides to slope·toZ(p) + offset minus the same for q. Ring cancels the offsets. mul_sub factors the slope. The final cast equality is discharged by Int.cast_sub inside simpa.
why it matters
The result is invoked by the sibling lemma mapDelta_diff_toZ via simpa, which specializes the difference to the LedgerUnits.toZ projection. It supplies the algebraic difference property required for consistent unit mappings inside the Recognition framework, supporting later composition of scales with affine transformations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.