AffineMapZ
plain-language theorem explainer
AffineMapZ encodes an affine map from the integers to the reals of the form n maps to slope times n plus offset. It is cited in Recognition Science unit mappings when constructing projections for charge, time, and action from the delta subgroup. The structure declaration introduces the two real parameters directly with no computational body or proof steps required.
Claim. An affine map $f: ℤ → ℝ$ given by $f(n) = s · n + o$ where slope $s ∈ ℝ$ and offset $o ∈ ℝ$.
background
The module treats the subgroup generated by δ as an abstract placeholder using integers for mapping only. AffineMapZ supplies the linear transformation applied to these integer representatives. The upstream result in RecogSpec.Scales repeats the identical structure definition for use in scaling specifications.
proof idea
The declaration is a structure definition introducing fields slope and offset. No lemmas or tactics are invoked; it serves as the primitive type for affine maps in this context.
why it matters
This structure supports downstream constructions such as apply, chargeMap, mapDelta, and timeMap in RecogSpec.Scales. It provides the affine component for mapping the delta-subgroup to real quantities including quantum charge and time scales in the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.