mapDeltaOne_step
The lemma establishes that the difference between the delta-one mapped value of an affine map at n+1 and at n equals the map's slope. Researchers verifying incremental linearity in binary scale constructions within Recognition Science would cite it when building phi-exponential wrappers. The proof reduces directly as a simplification tactic that unfolds the map definition and applies arithmetic identities.
claimLet $f$ be an affine map from integers to reals with slope $m$. Then the difference between the delta-one mapped value of $f$ at consecutive integer $n+1$ and at $n$ equals $m$.
background
The module develops binary scales and φ-exponential wrappers. AffineMapZ is the structure of maps sending each integer $n$ to slope times $n$ plus offset. The functions fromZ_one and toZ_one embed integers into and project from the δ=1 subgroup of ledger units. Upstream arithmetic results supply associativity and commutativity of addition together with distributivity of multiplication over addition, all derived from the foundational logic layer.
proof idea
The proof is a one-line wrapper that applies simp to the definition of mapDeltaOne together with add_comm, add_left_comm, add_assoc, sub_eq_add_neg, and mul_add.
why it matters in Recognition Science
This lemma verifies the constant-increment property required for affine maps inside the delta-one embedding, supporting scale constructions that feed into Recognition Science derivations of constants and mass ladders. It aligns with the framework's T5 J-uniqueness and T6 self-similar fixed point by ensuring linear steps remain consistent under the Recognition Composition Law. No downstream uses appear in the current graph, indicating it functions as an internal consistency check for the scales module.
scope and limits
- Does not address maps outside the affine class.
- Does not extend the increment property to delta values other than 1.
- Does not compute or constrain the offset component of the map.
- Does not connect directly to the J-cost function or phi-ladder rungs.
formal statement (Lean)
177lemma mapDeltaOne_step (f : AffineMapZ) (n : ℤ) :
178 mapDeltaOne LedgerUnits.toZ_one f (LedgerUnits.fromZ_one (n+1))
179 - mapDeltaOne LedgerUnits.toZ_one f (LedgerUnits.fromZ_one n) = f.slope := by
proof body
One-line wrapper that applies simp.
180 simp [mapDeltaOne, add_comm, add_left_comm, add_assoc, sub_eq_add_neg, mul_add]
181