def
definition
mapDelta
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.UnitMapping on GitHub at line 31.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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 }
59
60/-- WIP: action mapping requires Planck-like constant. Pass it explicitly. -/
61def actionMap (hbar : ℝ) : AffineMapZ := { slope := hbar, offset := 0 }