def
definition
actionMap
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.UnitMapping on GitHub at line 61.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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 }
62
63/-- Existence of affine δ→charge mapping (no numerics). -/
64noncomputable def mapDeltaCharge (δ : ℤ) (hδ : δ ≠ 0) (qe : ℝ) : DeltaSub δ → ℝ :=
65 mapDelta δ hδ (chargeMap qe)
66
67/-- Existence of affine δ→time mapping via τ0. -/
68noncomputable def mapDeltaTime (δ : ℤ) (hδ : δ ≠ 0) (U : Constants.RSUnits) : DeltaSub δ → ℝ :=
69 mapDelta δ hδ (timeMap U)
70
71/-- Existence of affine δ→action mapping via an explicit ħ parameter. -/
72noncomputable def mapDeltaAction (δ : ℤ) (hδ : δ ≠ 0) (hbar : ℝ) : DeltaSub δ → ℝ :=
73 mapDelta δ hδ (actionMap hbar)
74
75@[simp] lemma mapDelta_fromZ (δ : ℤ) (hδ : δ ≠ 0) (f : AffineMapZ) (n : ℤ) :
76 mapDelta δ hδ f (LedgerUnits.fromZ δ n) = f.slope * (n : ℝ) + f.offset := by
77 classical
78 simp [mapDelta, LedgerUnits.toZ_fromZ δ hδ]
79
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
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