mapDeltaOne
The definition specializes the general delta-to-real mapping to the generator δ=1 by composing the canonical integer projection with an affine map. Researchers handling unit conversions and binary scales in Recognition Science cite it when reducing to the δ=1 case for time or length mappings. The implementation is a direct one-line functional application of slope times the projected integer plus offset.
claimLet $Δ_1$ be the subgroup of $ℤ$ generated by 1. Given a projection $π: Δ_1 → ℤ$ and an affine map $f(n) = s·n + o$ with $s,o ∈ ℝ$, the function sends each $p ∈ Δ_1$ to $s·π(p) + o$.
background
The RecogSpec.Scales module addresses binary scales and φ-exponential wrappers. DeltaSub δ is the subgroup of ℤ generated by δ, here specialized to δ=1 to obtain a clean order isomorphism with ℤ. AffineMapZ is the structure carrying a slope and offset that defines the map n ↦ slope·n + offset from ℤ to ℝ. Upstream, toZ extracts the integer coefficient from any element of DeltaSub δ.
proof idea
One-line definition that multiplies the slope by the integer extracted via toZ and adds the offset.
why it matters in Recognition Science
It supplies the concrete δ=1 case required by the lemmas mapDeltaOne_fromZ_one, mapDeltaOne_step, and mapDeltaTime_fromZ_one. These lemmas in turn support integer-based unit mappings that feed the binary-scale constructions in the Recognition framework.
scope and limits
- Does not define the general mapDelta for arbitrary δ.
- Does not prove any algebraic properties of the resulting function.
- Does not incorporate φ-exponentials or Recognition constants.
- Does not extend to non-subgroup or non-integer domains.
Lean usage
mapDeltaOne LedgerUnits.toZ_one f pformal statement (Lean)
167noncomputable def mapDeltaOne
168 (toZ : LedgerUnits.DeltaSub 1 → ℤ) (f : AffineMapZ) : LedgerUnits.DeltaSub 1 → ℝ :=
proof body
Definition body.
169 fun p => f.slope * ((toZ p) : ℝ) + f.offset
170