def
definition
chargeMap
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.RecogSpec.Scales on GitHub at line 154.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
151 fun p => f.slope * ((toZ p) : ℝ) + f.offset
152
153/-- Context constructors: charge (quantum `qe`), time (τ0), and action (ħ). -/
154@[simp] def chargeMap (qe : ℝ) : AffineMapZ := { slope := qe, offset := 0 }
155@[simp] def timeMap (U : Constants.RSUnits) : AffineMapZ := { slope := U.tau0, offset := 0 }
156-- actionMap omitted in minimal RSUnits (no `hbar` field)
157
158@[simp] lemma apply_chargeMap (qe : ℝ) (n : ℤ) :
159 apply (chargeMap qe) n = qe * (n : ℝ) := by simp [apply, chargeMap]
160
161@[simp] lemma apply_timeMap (U : Constants.RSUnits) (n : ℤ) :
162 apply (timeMap U) n = U.tau0 * (n : ℝ) := by simp [apply, timeMap]
163
164-- (no actionMap in minimal RSUnits)
165
166/-- Specialization of `mapDelta` to δ = 1 using the canonical projection. -/
167noncomputable def mapDeltaOne
168 (toZ : LedgerUnits.DeltaSub 1 → ℤ) (f : AffineMapZ) : LedgerUnits.DeltaSub 1 → ℝ :=
169 fun p => f.slope * ((toZ p) : ℝ) + f.offset
170
171@[simp] lemma mapDeltaOne_fromZ_one
172 (f : AffineMapZ) (n : ℤ) :
173 mapDeltaOne LedgerUnits.toZ_one f (LedgerUnits.fromZ_one n)
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)