mapDeltaOne_fromZ_one
plain-language theorem explainer
The lemma shows that the δ=1 specialization of an affine map recovers the direct slope-times-n-plus-offset evaluation when applied to the canonical integer embedding. Workers on binary scales and integer projections in Recognition Science cite it to simplify expressions involving DeltaSub 1. The proof is a one-line simp wrapper that unfolds mapDeltaOne together with the toZ_one and fromZ_one projections.
Claim. Let $f$ be an affine map from integers to reals with slope $s$ and offset $o$. For any integer $n$, mapDeltaOne applied with the canonical projection toZ_1 to $f$ on the embedded value fromZ_1($n$) equals $s n + o$, where fromZ_1 embeds ℤ into the δ=1 subgroup and toZ_1 projects back to ℤ.
background
The module develops binary scales and φ-exponential wrappers. AffineMapZ is the structure of maps ℤ → ℝ given by n ↦ slope·n + offset. Upstream, fromZ_one embeds an integer n into DeltaSub 1 by the pair ⟨n, proof that n·1 = n⟩ while toZ_one extracts the integer value. mapDeltaOne is the specialization of the general mapDelta to the δ=1 case that composes with the projection toZ.
proof idea
The proof is a one-line simp wrapper. It applies the simp tactic to the definitions of mapDeltaOne, LedgerUnits.toZ_one, and LedgerUnits.fromZ_one, which immediately reduce the left-hand side to the affine expression slope·n + offset.
why it matters
The result ensures that affine maps on the canonical δ=1 subgroup behave exactly as their direct real-valued counterparts, supporting consistent scale constructions in the RecogSpec module. It fills a basic compatibility step for integer embeddings used in binary scales and φ-exponential wrappers. No downstream theorems are listed, but the lemma aligns with the framework's reliance on integer ladders and projections.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.