def
definition
apply
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.UnitMapping on GitHub at line 28.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
25 slope : ℝ
26 offset : ℝ
27
28@[simp] def apply (f : AffineMapZ) (n : ℤ) : ℝ := f.slope * (n : ℝ) + f.offset
29
30/-- Map δ-subgroup to ℝ by composing the (stubbed) projection `toZ` with an affine map. -/
31noncomputable def mapDelta (δ : ℤ) (hδ : δ ≠ 0) (f : AffineMapZ) : DeltaSub δ → ℝ :=
32 fun p => f.slope * ((LedgerUnits.toZ δ p) : ℝ) + f.offset
33
34lemma mapDelta_diff (δ : ℤ) (hδ : δ ≠ 0) (f : AffineMapZ)
35 (p q : DeltaSub δ) :
36 mapDelta δ hδ f p - mapDelta δ hδ f q
37 = f.slope * ((LedgerUnits.toZ δ p - LedgerUnits.toZ δ q : ℤ) : ℝ) := by
38 classical
39 calc
40 mapDelta δ hδ f p - mapDelta δ hδ f q
41 = (f.slope * (LedgerUnits.toZ δ p : ℝ) + f.offset)
42 - (f.slope * (LedgerUnits.toZ δ q : ℝ) + f.offset) := by
43 simp [mapDelta]
44 _ = f.slope * (LedgerUnits.toZ δ p : ℝ)
45 - f.slope * (LedgerUnits.toZ δ q : ℝ) := by
46 ring
47 _ = f.slope * ((LedgerUnits.toZ δ p : ℝ)
48 - (LedgerUnits.toZ δ q : ℝ)) := by
49 simpa [mul_sub]
50 _ = f.slope * ((LedgerUnits.toZ δ p - LedgerUnits.toZ δ q : ℤ) : ℝ) := by
51 have hcast : ((LedgerUnits.toZ δ p - LedgerUnits.toZ δ q : ℤ) : ℝ)
52 = (LedgerUnits.toZ δ p : ℝ) - (LedgerUnits.toZ δ q : ℝ) := by
53 simpa using (Int.cast_sub (LedgerUnits.toZ δ p) (LedgerUnits.toZ δ q))
54 simpa [hcast]
55
56/-- Context constructors: charge (quantum `qe`) and time (τ0). -/
57def chargeMap (qe : ℝ) : AffineMapZ := { slope := qe, offset := 0 }
58def timeMap (U : Constants.RSUnits) : AffineMapZ := { slope := U.tau0, offset := 0 }