IndisputableMonolith.UnitMapping

   1import Mathlib
   2import IndisputableMonolith.Constants
   3
   4namespace IndisputableMonolith
   5namespace UnitMapping
   6
   7-- Minimal δ-ledger subgroup interface for decoupled mapping
   8namespace LedgerUnits
   9
  10/-- Subgroup generated by δ (abstract placeholder using integers for mapping only). -/
  11def DeltaSub (δ : ℤ) := ℤ
  12
  13@[simp] def fromZ (δ : ℤ) (n : ℤ) : DeltaSub δ := n
  14@[simp] def toZ   (δ : ℤ) (p : DeltaSub δ) : ℤ := p
  15
  16@[simp] lemma toZ_fromZ (δ : ℤ) (hδ : δ ≠ 0) (n : ℤ) :
  17  toZ δ (fromZ δ n) = n := rfl
  18
  19end LedgerUnits
  20
  21open LedgerUnits
  22
  23/-- Affine map from ℤ to ℝ: n ↦ slope·n + offset. -/
  24structure AffineMapZ where
  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 }
  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
  92              simpa [Int.cast_add, Int.cast_one]
  93    _   = f.slope := by
  94              simp [mul_add, sub_eq_add_neg, add_comm, add_left_comm, add_assoc]
  95
  96@[simp] lemma mapDeltaTime_fromZ (δ : ℤ) (hδ : δ ≠ 0)
  97  (U : Constants.RSUnits) (n : ℤ) :
  98  mapDeltaTime δ hδ U (LedgerUnits.fromZ δ n) = U.tau0 * (n : ℝ) := by
  99  classical
 100  have h := mapDelta_fromZ (δ:=δ) (hδ:=hδ) (f:=timeMap U) (n:=n)
 101  simpa [mapDeltaTime, timeMap, add_comm] using h
 102
 103lemma mapDeltaTime_step (δ : ℤ) (hδ : δ ≠ 0)
 104  (U : Constants.RSUnits) (n : ℤ) :
 105  mapDeltaTime δ hδ U (LedgerUnits.fromZ δ (n+1)) - mapDeltaTime δ hδ U (LedgerUnits.fromZ δ n) = U.tau0 := by
 106  simpa [mapDeltaTime, timeMap] using
 107    (mapDelta_step (δ:=δ) (hδ:=hδ) (f:=timeMap U) (n:=n))
 108
 109@[simp] lemma mapDeltaAction_fromZ (δ : ℤ) (hδ : δ ≠ 0)
 110  (hbar : ℝ) (n : ℤ) :
 111  mapDeltaAction δ hδ hbar (LedgerUnits.fromZ δ n) = hbar * (n : ℝ) := by
 112  classical
 113  have h := mapDelta_fromZ (δ:=δ) (hδ:=hδ) (f:=actionMap hbar) (n:=n)
 114  simpa [mapDeltaAction, actionMap, add_comm] using h
 115
 116lemma mapDeltaAction_step (δ : ℤ) (hδ : δ ≠ 0)
 117  (hbar : ℝ) (n : ℤ) :
 118  mapDeltaAction δ hδ hbar (LedgerUnits.fromZ δ (n+1)) - mapDeltaAction δ hδ hbar (LedgerUnits.fromZ δ n)
 119    = hbar := by
 120  simpa [mapDeltaAction, actionMap] using
 121    (mapDelta_step (δ:=δ) (hδ:=hδ) (f:=actionMap hbar) (n:=n))
 122
 123lemma mapDelta_diff_toZ (δ : ℤ) (hδ : δ ≠ 0) (f : AffineMapZ)
 124  (p q : DeltaSub δ) :
 125  mapDelta δ hδ f p - mapDelta δ hδ f q
 126    = f.slope * ((LedgerUnits.toZ δ p - LedgerUnits.toZ δ q : ℤ) : ℝ) := by
 127  classical
 128  simpa using (mapDelta_diff (δ:=δ) (hδ:=hδ) (f:=f) (p:=p) (q:=q))
 129
 130end UnitMapping
 131end IndisputableMonolith
 132