mapDelta
plain-language theorem explainer
Defines the function sending each element of the δ-generated subgroup of integers to a real number by first recovering its integer coefficient via the toZ projection and then applying a supplied affine map. Researchers constructing explicit charge, time, or action maps in the Recognition Science unit layer would cite this definition. It is realized by a direct one-line functional composition with no auxiliary lemmas.
Claim. Let $D_δ$ denote the subgroup of $ℤ$ generated by a nonzero integer $δ$. For an affine map $f:ℤ→ℝ$ given by $f(n)=s·n+o$ with $s,o∈ℝ$, the map $D_δ→ℝ$ is $p↦s·proj(p)+o$, where $proj$ recovers the coefficient $n$ such that the representative equals $n·δ$.
background
In UnitMapping, DeltaSub δ is introduced as the abstract placeholder ℤ standing for the subgroup generated by δ. AffineMapZ is the structure carrying a real slope and offset that together define the map $n↦$slope·$n+$offset. The projection toZ, drawn from LedgerUnits, returns the integer coefficient for any element of the subgroup by classical choice of the witnessing multiplier.
proof idea
One-line definition that composes the affine map with the toZ projection: the body is exactly fun p => f.slope * ((LedgerUnits.toZ δ p) : ℝ) + f.offset.
why it matters
Supplies the shared implementation used by mapDeltaCharge, mapDeltaAction, mapDelta_diff and the corresponding time map. It is invoked inside RecogSpec.Scales.mapDelta and apply_timeMap. The definition therefore sits at the interface that converts abstract δ-steps into the concrete units (qe, τ0, ħ) required for the Recognition framework's context constructors.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.