mapDelta_diff

formal source

  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 }
  62
  63/-- Existence of affine δ→charge mapping (no numerics). -/
  64noncomputable def mapDeltaCharge (δ : ℤ) (hδ : δ ≠ 0) (qe : ℝ) : DeltaSub δ → ℝ :=