mapDelta_diff_toZ
mapDelta_diff_toZ establishes that the difference of two mapDelta images equals the affine slope times the integer difference of their toZ projections. Researchers handling unit conversions between abstract delta subgroups and real charges or times would cite it to preserve linearity under projection. The proof is a one-line wrapper that reduces via simpa to the general mapDelta_diff identity after invoking classical.
claimLet $δ ∈ ℤ$ with $δ ≠ 0$, let $f$ be an affine map $ℤ → ℝ$ with slope $s$, and let $p, q$ belong to the $δ$-subgroup. Then mapDelta$(δ, f, p) - $mapDelta$(δ, f, q) = s · (toZ$(δ, p) - $toZ$(δ, q))$, where mapDelta composes the affine map with the integer projection toZ.
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 : ℝ. mapDelta applies the affine map after extracting the integer coefficient via toZ. The module treats these as abstract mappings for unit conversions prior to physical specialization. Upstream, LedgerUnits.DeltaSub defines the precise subgroup as {x : ℤ // ∃ n : ℤ, x = n * δ} and toZ extracts the multiplier by classical choice. RecogSpec.Scales.mapDelta supplies the general difference identity that this lemma specializes.
proof idea
The proof invokes classical to accommodate the noncomputable choice inside toZ, then applies simpa to reduce the claim directly to mapDelta_diff (δ:=δ) (hδ:=hδ) (f:=f) (p:=p) (q:=q).
why it matters in Recognition Science
The lemma guarantees that differences remain linear under the affine projection, which is required for the siblings chargeMap, timeMap and actionMap to produce consistent real-valued quantities. It closes a compatibility step between the abstract DeltaSub layer and the real affine maps used in the Recognition framework's unit conversions. No downstream theorems are recorded yet, but the result supports the overall mapping pipeline that feeds into the phi-ladder and constant derivations.
scope and limits
- Does not apply when δ = 0.
- Does not compute numerical values for specific physical units.
- Does not extend beyond integer subgroups.
- Does not address nonlinear or non-affine maps.
formal statement (Lean)
123lemma mapDelta_diff_toZ (δ : ℤ) (hδ : δ ≠ 0) (f : AffineMapZ)
124 (p q : DeltaSub δ) :
125 mapDelta δ hδ f p - mapDelta δ hδ f q
126 = f.slope * ((LedgerUnits.toZ δ p - LedgerUnits.toZ δ q : ℤ) : ℝ) := by
proof body
Term-mode proof.
127 classical
128 simpa using (mapDelta_diff (δ:=δ) (hδ:=hδ) (f:=f) (p:=p) (q:=q))
129
130end UnitMapping
131end IndisputableMonolith