mapDelta
plain-language theorem explainer
The mapDelta definition sends elements of the δ-multiples subgroup of ℤ to ℝ by composing a supplied projection to ℤ with an affine map of given slope and offset. Researchers constructing charge, time, and action scales in Recognition Science cite it when building unit mappings from integer deltas. The implementation is a direct functional composition that multiplies the projected integer by the slope and adds the offset.
Claim. Let $δ ∈ ℤ ∖ {0}$, let $π : {x ∈ ℤ | ∃ n ∈ ℤ, x = nδ} → ℤ$ be a projection, and let $f$ be the affine map $n ↦ s·n + o$ with $s, o ∈ ℝ$. Then the map sending each subgroup element $p$ to $s · π(p) + o$ is the function produced by mapDelta $δ$ $π$ $f$.
background
The RecogSpec.Scales module treats binary scales and φ-exponential wrappers. AffineMapZ is the structure with fields slope : ℝ and offset : ℝ, so that the associated map is n ↦ slope·n + offset. The δ-subgroup is the set of all integer multiples of a fixed nonzero δ. This definition generalizes the mapDelta appearing in UnitMapping, which hard-codes the projection via LedgerUnits.toZ.
proof idea
One-line wrapper that applies the supplied toZ projection, multiplies the resulting integer by the slope of the affine map, and adds the offset.
why it matters
It supplies the general mechanism for turning δ-subgroups into real-valued physical quantities (time via τ0, charge via qe, action via ħ) inside the Recognition Science unit system. It is invoked by apply_timeMap and supports the specialized constructors mapDeltaAction, mapDeltaCharge, and mapDelta_diff in UnitMapping. The construction sits inside the binary-scales layer that precedes the φ-ladder mass formula and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.