apply
plain-language theorem explainer
The declaration defines the evaluation of an affine map from integers to reals by the formula slope times n plus offset. It supplies the concrete operation for mapping δ-subgroup integers in the UnitMapping module. Researchers composing projections to real scales in Recognition Science would cite this when building measurement maps. The definition is a direct field extraction and arithmetic expression with the simp attribute.
Claim. Let $f$ be an affine map from integers to reals given by slope $s$ and offset $o$. Then the evaluation at integer $n$ is $s n + o$.
background
The UnitMapping module treats the subgroup generated by δ as an abstract placeholder represented by integers solely for mapping purposes. The AffineMapZ structure encodes an affine transformation from ℤ to ℝ via its two fields: slope and offset. Upstream results include the toZ projection that extracts an integer from a DeltaSub element, together with analogous AffineMapZ structures in Measurement and RecogSpec.Scales that enforce the same slope-offset convention across the framework.
proof idea
The declaration is a direct definition that projects the slope and offset fields from the AffineMapZ structure and performs the linear combination after casting the integer argument to ℝ. No lemmas are applied; it is the primitive implementation of the affine evaluation.
why it matters
This definition completes the basic toolkit for applying affine maps to integer projections inside the unit-mapping layer. It supports the composition of δ-subgroup projections with real-valued transformations required for consistent scaling. Although no downstream uses are recorded yet, the definition aligns with the abstract mapping scaffold needed for the phi-ladder and mass formulas in Recognition Science.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.