fromNat

formal source

  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]