def
definition
chargeMap
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.UnitMapping on GitHub at line 57.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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 }
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