AffineMapZ
plain-language theorem explainer
AffineMapZ encodes an affine map from ℤ to ℝ via a slope and offset. Developers of discrete-to-continuous projections in Recognition Science cite it when building chargeMap, timeMap, and mapDelta. The declaration is a bare structure definition with two real fields and no proof obligations.
Claim. An affine map from ℤ to ℝ is given by n ↦ s·n + o where s, o ∈ ℝ are the slope and offset.
background
The module RecogSpec.Scales develops binary scales and φ-exponential wrappers. AffineMapZ supplies the primitive structure for attaching real values to integer indices. It is imported from UnitMapping, where the identical structure is defined with the same two fields for unit mappings.
proof idea
The declaration is a structure definition that introduces the fields slope and offset of type ℝ. No lemmas or tactics are applied.
why it matters
AffineMapZ underpins apply, chargeMap, mapDelta, mapDeltaOne and related constructions in the same module. These feed into δ-subgroup projections and context constructors for charge, time, and action. It supports the binary scale framework by providing a uniform discrete-to-real attachment used across the scales layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.