apply
plain-language theorem explainer
apply evaluates an AffineMapZ at an integer by the linear formula slope times n plus offset. Scale modelers in Recognition Science cite it when converting discrete rung indices on binary or phi-ladders into real measurement values. The definition is realized by direct field access and arithmetic on the structure components.
Claim. For an affine map $f$ with real slope and offset, apply$(f,n) = f$.slope $· n + f$.offset for $n ∈ ℤ$.
background
The RecogSpec.Scales module develops binary scales and φ-exponential wrappers that convert discrete indices into continuous reals. AffineMapZ is the structure holding a real slope and real offset that defines the map $n ↦$ slope·$n +$ offset from ℤ to ℝ. Upstream Measurement.Map supplies the minimal scaffold with a positive time parameter T and a meas function from real-valued states to observations, while the RSNative.Core.map preserves measurement metadata under transformations.
proof idea
One-line definition that directly computes the affine transformation by multiplying the slope field by the cast integer and adding the offset field.
why it matters
This supplies the concrete evaluation operation for affine maps inside the binary scales and φ-exponential wrappers of the module. It enables projection of integer rungs onto real values, supporting later composition with phi-powers and the overall Recognition Science treatment of scales. No downstream theorems are recorded, indicating it functions as a primitive building block.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.