mapDelta_step
The lemma shows that the difference between mapDelta applied to consecutive elements of the δ-generated subgroup equals the slope of the affine map f. Researchers deriving incremental changes in time or action units within Recognition Science cite this result. The proof is a calc block that unfolds the definition via toZ_fromZ, applies ring to cancel the offset, and finishes with algebraic simplification using mul_add and commutativity lemmas.
claimLet $δ ∈ ℤ$ with $δ ≠ 0$, let $f$ be the affine map $m ↦ s·m + b$ from $ℤ$ to $ℝ$, and let $n ∈ ℤ$. Then mapDelta(δ, f, fromZ(δ, n+1)) − mapDelta(δ, f, fromZ(δ, n)) = s.
background
AffineMapZ is the structure with fields slope and offset that encodes the map m ↦ slope·m + offset. The function fromZ embeds an integer n into the subgroup generated by δ via the element n·δ. The lemma toZ_fromZ states that toZ recovers the original integer n from fromZ(δ, n).
proof idea
The proof opens a calc block. The first step applies simp with the definitions of mapDelta and toZ_fromZ to obtain the explicit difference (slope·(n+1) + offset) − (slope·n + offset). Ring cancels the offset. Simpa handles the integer-to-real cast. The final simp uses mul_add together with sub_eq_add_neg, add_comm and add_assoc to reduce the expression to the slope.
why it matters in Recognition Science
mapDelta_step is invoked directly by mapDeltaTime_step and mapDeltaAction_step, which establish that consecutive increments equal the base time unit tau0 and the action unit hbar. It supplies the discrete stepping rule inside the UnitMapping module that translates ledger subgroups into physical quantities. The result sits downstream of the arithmetic lemmas add_assoc, add_comm and mul_add.
scope and limits
- Does not apply when δ = 0.
- Does not extend beyond affine maps.
- Does not treat continuous or real-valued subgroups.
- Does not establish uniqueness of the embedding.
Lean usage
simpa [mapDeltaAction, actionMap] using (mapDelta_step (δ:=δ) (hδ:=hδ) (f:=actionMap hbar) (n:=n))formal statement (Lean)
80lemma mapDelta_step (δ : ℤ) (hδ : δ ≠ 0) (f : AffineMapZ) (n : ℤ) :
81 mapDelta δ hδ f (LedgerUnits.fromZ δ (n+1)) - mapDelta δ hδ f (LedgerUnits.fromZ δ n) = f.slope := by
proof body
Tactic-mode proof.
82 classical
83 calc
84 mapDelta δ hδ f (LedgerUnits.fromZ δ (n+1))
85 - mapDelta δ hδ f (LedgerUnits.fromZ δ n)
86 = (f.slope * ((n+1 : ℤ) : ℝ) + f.offset)
87 - (f.slope * (n : ℝ) + f.offset) := by
88 simp [mapDelta, LedgerUnits.toZ_fromZ]
89 _ = f.slope * ((n+1 : ℤ) : ℝ) - f.slope * (n : ℝ) := by
90 ring
91 _ = f.slope * ((n : ℝ) + 1) - f.slope * (n : ℝ) := by
92 simpa [Int.cast_add, Int.cast_one]
93 _ = f.slope := by
94 simp [mul_add, sub_eq_add_neg, add_comm, add_left_comm, add_assoc]
95