`mapDeltaOne_step`

proved

show as: view math explainer →

module: IndisputableMonolith.RecogSpec.Scales
domain: RecogSpec
line: 177 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.RecogSpec.Scales on GitHub at line 177.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

 174    = f.slope * (n : ℝ) + f.offset := by
 175  simp [mapDeltaOne, LedgerUnits.toZ_one, LedgerUnits.fromZ_one]
 176
 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
 180  simp [mapDeltaOne, add_comm, add_left_comm, add_assoc, sub_eq_add_neg, mul_add]
 181
 182@[simp] lemma mapDeltaTime_fromZ_one
 183  (U : Constants.RSUnits) (n : ℤ) :
 184  mapDeltaOne LedgerUnits.toZ_one (timeMap U) (LedgerUnits.fromZ_one n)
 185    = U.tau0 * (n : ℝ) := by
 186  simp [mapDeltaOne, timeMap, add_comm]
 187
 188-- (no actionMap in minimal RSUnits)
 189
 190end Scales
 191
 192end RecogSpec
 193end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.