apply
plain-language theorem explainer
apply defines the evaluation of an affine map on an integer argument. Researchers working on unit conversions in Recognition Science would reference it when composing projections from δ-subgroups with real-valued scalings. The definition directly implements the linear expression using the map's slope and offset components.
Claim. For an affine map given by slope $s$ and offset $o$, the image of integer $n$ is $s n + o$.
background
The UnitMapping module treats the subgroup generated by δ as an abstract placeholder realized via integers for mapping purposes only. AffineMapZ is the structure with fields slope and offset that encodes maps of the form $n ↦ s·n + o$. Upstream, toZ from LedgerUnits projects a DeltaSub δ element to an integer, while the sibling toZ in this module is the identity on that integer; similar AffineMapZ structures appear in RecogSpec.Scales and Measurement for scale and observation mappings.
proof idea
Direct definition that casts n to reals, multiplies by the slope field, and adds the offset field. No lemmas or tactics are invoked.
why it matters
The definition supplies the concrete action of affine maps inside the unit-mapping layer, enabling composition with integer projections from δ-subgroups. It supports sibling operations such as mapDelta and chargeMap within the same module and aligns with the affine scale maps used in RecogSpec.Scales for the phi-ladder and discrete-to-continuous transitions in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.