mapDelta
plain-language theorem explainer
The mapDelta definition composes an affine map with the integer projection toZ to send elements of the δ-generated subgroup to reals. Researchers constructing charge, time, or action scales in Recognition Science cite it as the shared implementation for unit mappings. The definition is a direct one-line functional composition of slope times the extracted coefficient plus offset.
Claim. For nonzero integer δ and affine map f with slope s and offset o, mapDelta(δ, h_δ, f) sends each p in the subgroup Δ_δ to s · toZ(δ, p) + o, where toZ recovers the integer multiplier k such that p = k · δ.
background
DeltaSub δ denotes the subgroup of ℤ generated by δ, realized concretely in LedgerUnits as {x : ℤ // ∃ n : ℤ, x = n * δ} and abstracted to ℤ in this module for mapping purposes. AffineMapZ is the structure carrying slope and offset so that the map acts as n ↦ slope · n + offset. The projection toZ extracts the coefficient via Classical.choose on the subgroup membership proof.
proof idea
One-line wrapper that applies the affine map directly: multiply slope by the integer from LedgerUnits.toZ δ p and add the offset.
why it matters
This definition supplies the common implementation for mapDeltaCharge, mapDeltaAction, and timeMap specializations in the same module, which are then used by apply_timeMap and mapDelta in RecogSpec.Scales. It realizes the abstract δ-subgroup to real mapping needed for the context constructors of charge, time, and action scales.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.