IndisputableMonolith.LedgerUnits

   1import Mathlib
   2
   3namespace IndisputableMonolith
   4namespace LedgerUnits
   5
   6/-- The subgroup of ℤ generated by δ. We specialize to δ = 1 for a clean order isomorphism. -/
   7def DeltaSub (δ : ℤ) := {x : ℤ // ∃ n : ℤ, x = n * δ}
   8
   9/-- Embed ℤ into the δ=1 subgroup. -/
  10def fromZ_one (n : ℤ) : DeltaSub 1 := ⟨n, by exact ⟨n, by simpa using (Int.mul_one n)⟩⟩
  11
  12/-- Project from the δ=1 subgroup back to ℤ by taking its value. -/
  13def toZ_one (p : DeltaSub 1) : ℤ := p.val
  14
  15@[simp] lemma toZ_fromZ_one (n : ℤ) : toZ_one (fromZ_one n) = n := rfl
  16
  17@[simp] lemma fromZ_toZ_one (p : DeltaSub 1) : fromZ_one (toZ_one p) = p := by
  18  cases p with
  19  | mk x hx =>
  20    apply Subtype.ext
  21    rfl
  22
  23/-- Explicit equivalence between the δ=1 subgroup and ℤ (mapping n·1 ↦ n). -/
  24def equiv_delta_one : DeltaSub 1 ≃ ℤ :=
  25{ toFun := toZ_one
  26, invFun := fromZ_one
  27, left_inv := fromZ_toZ_one
  28, right_inv := toZ_fromZ_one }
  29
  30/-! ### General δ ≠ 0: non-canonical equivalence n•δ ↦ n -/
  31
  32noncomputable def fromZ (δ : ℤ) (n : ℤ) : DeltaSub δ := ⟨n * δ, ⟨n, rfl⟩⟩
  33
  34noncomputable def toZ (δ : ℤ) (p : DeltaSub δ) : ℤ :=
  35  Classical.choose p.property
  36
  37lemma toZ_spec (δ : ℤ) (p : DeltaSub δ) : p.val = toZ δ p * δ :=
  38  Classical.choose_spec p.property
  39
  40lemma rep_unique {δ n m : ℤ} (hδ : δ ≠ 0) (h : n * δ = m * δ) : n = m := by
  41  have h' : (n - m) * δ = 0 := by
  42    calc
  43      (n - m) * δ = n * δ - m * δ := by simpa using sub_mul n m δ
  44      _ = 0 := by simpa [h]
  45  have hnm : n - m = 0 := by
  46    have : n - m = 0 ∨ δ = 0 := by
  47      simpa using (mul_eq_zero.mp h')
  48    cases this with
  49    | inl h0 => exact h0
  50    | inr h0 => exact (hδ h0).elim
  51  exact sub_eq_zero.mp hnm
  52
  53@[simp] lemma toZ_fromZ (δ : ℤ) (hδ : δ ≠ 0) (n : ℤ) : toZ δ (fromZ δ n) = n := by
  54  have hval : (fromZ δ n).val = n * δ := rfl
  55  let k := toZ δ (fromZ δ n)
  56  have hk : (fromZ δ n).val = k * δ := toZ_spec δ (fromZ δ n)
  57  have h_eq : n = k := rep_unique (δ:=δ) hδ (by simpa [hval] using hk)
  58  simpa [k, h_eq.symm]
  59
  60@[simp] lemma fromZ_toZ (δ : ℤ) (p : DeltaSub δ) : fromZ δ (toZ δ p) = p := by
  61  apply Subtype.ext
  62  simpa [fromZ, toZ_spec δ p]
  63
  64/-- One δ-step corresponds to adding 1 on coefficients via `toZ`. -/
  65@[simp] lemma toZ_succ (δ : ℤ) (hδ : δ ≠ 0) (n : ℤ) :
  66  toZ δ (fromZ δ (n + 1)) = toZ δ (fromZ δ n) + 1 := by
  67  simp [toZ_fromZ δ hδ]
  68
  69/-- Package rung index as the `toZ` coefficient of a δ‑element. -/
  70noncomputable def rungOf (δ : ℤ) (p : DeltaSub δ) : ℤ := toZ δ p
  71
  72@[simp] lemma rungOf_fromZ (δ : ℤ) (hδ : δ ≠ 0) (n : ℤ) :
  73  rungOf δ (fromZ δ n) = n := by
  74  simpa [rungOf, toZ_fromZ δ hδ]
  75
  76lemma rungOf_step (δ : ℤ) (hδ : δ ≠ 0) (n : ℤ) :
  77  rungOf δ (fromZ δ (n + 1)) = rungOf δ (fromZ δ n) + 1 := by
  78  simpa [rungOf] using (toZ_succ (δ:=δ) (hδ:=hδ) (n:=n))
  79
  80/-- For any nonzero δ, the subgroup of ℤ generated by δ is (non‑canonically) equivalent to ℤ via n·δ ↦ n. -/
  81noncomputable def equiv_delta (δ : ℤ) (hδ : δ ≠ 0) : DeltaSub δ ≃ ℤ :=
  82{ toFun := toZ δ
  83, invFun := fromZ δ
  84, left_inv := fromZ_toZ δ
  85, right_inv := toZ_fromZ δ hδ }
  86
  87/-- Embed `Nat` into the δ‑subgroup via ℤ. -/
  88noncomputable def fromNat (δ : ℤ) (m : Nat) : DeltaSub δ := fromZ δ (Int.ofNat m)
  89
  90/-- Extract a nonnegative "k‑index" from a δ‑element as `Int.toNat (toZ ...)`. -/
  91noncomputable def kOf (δ : ℤ) (p : DeltaSub δ) : Nat := Int.toNat (toZ δ p)
  92
  93@[simp] lemma kOf_fromZ (δ : ℤ) (hδ : δ ≠ 0) (n : ℤ) :
  94  kOf δ (fromZ δ n) = Int.toNat n := by
  95  simp [kOf, toZ_fromZ δ hδ]
  96
  97@[simp] lemma kOf_fromNat (δ : ℤ) (hδ : δ ≠ 0) (m : Nat) :
  98  kOf δ (fromNat δ m) = m := by
  99  simp [kOf, fromNat, toZ_fromZ δ hδ, Int.toNat_natCast]
 100
 101lemma kOf_step_succ (δ : ℤ) (hδ : δ ≠ 0) (m : Nat) :
 102  kOf δ (fromNat δ (m+1)) = kOf δ (fromNat δ m) + 1 := by
 103  simp only [kOf, fromNat, toZ_fromZ δ hδ, Int.natCast_add, Int.natCast_one]
 104  rfl
 105
 106/-- Quantization: every element of the δ-subgroup has a unique integer coefficient. -/
 107theorem quantization {δ : ℤ} (hδ : δ ≠ 0) (x : DeltaSub δ) :
 108  ∃! (n : ℤ), x.val = n * δ :=
 109by
 110  classical
 111  -- Existence from `toZ_spec`
 112  refine ⟨toZ δ x, ?eq, ?uniq⟩
 113  · simpa [toZ_spec δ x]
 114  · intro m hm
 115    -- Uniqueness from `rep_unique`
 116    have h1 : x.val = toZ δ x * δ := toZ_spec δ x
 117    have h2 : x.val = m * δ := hm
 118    have : m * δ = toZ δ x * δ := by rw [← h2, h1]
 119    exact rep_unique (δ:=δ) hδ this
 120
 121end LedgerUnits
 122end IndisputableMonolith
 123