apply
Defines the evaluation of an affine map from integers to reals by scaling the input and adding an offset. Researchers composing unit mappings from delta-subgroups in Recognition Science cite this when turning integer projections into real values. The definition is a direct algebraic expression using the slope and offset fields of the map structure.
claimLet $f$ be an affine map from integers to reals given by slope $m$ and offset $b$. Then $f(n) = m n + b$ for any integer $n$.
background
AffineMapZ is the structure with real slope and real offset representing the map $n mapsto$ slope times $n$ plus offset. The module treats the subgroup generated by delta as an abstract placeholder using integers solely for mapping purposes. Upstream, toZ projects a DeltaSub element to an integer while Measurement.Map provides the general scaffold for measurement maps.
proof idea
One-line definition that casts the integer input to reals, multiplies by the slope field, and adds the offset field.
why it matters in Recognition Science
This supplies the concrete evaluation step for affine maps inside the UnitMapping module. It allows integer projections from delta-subgroups to be scaled to real units, supporting the mapping layer that sits between ledger units and measurement structures in the Recognition framework. No downstream theorems are recorded yet.
scope and limits
- Does not define the AffineMapZ structure or its fields.
- Does not handle non-integer inputs or continuous domains.
- Does not incorporate measurement uncertainty or window data.
- Does not reference phi-ladder, J-cost, or Recognition constants.
formal statement (Lean)
28@[simp] def apply (f : AffineMapZ) (n : ℤ) : ℝ := f.slope * (n : ℝ) + f.offset
proof body
Definition body.
29
30/-- Map δ-subgroup to ℝ by composing the (stubbed) projection `toZ` with an affine map. -/