rep_unique
Multiplication by a nonzero integer δ is cancellative in ℤ. Constructions of quantized subgroups cite this result to guarantee unique coefficients for each group element. The tactic proof rewrites the equality to obtain a product equal to zero, invokes the no-zero-divisors theorem mul_eq_zero, and discards the δ = 0 case to conclude n equals m.
claimFor integers $δ, n, m$ with $δ ≠ 0$, if $n δ = m δ$ then $n = m$.
background
The module LedgerUnits studies the subgroup of integers generated by a fixed nonzero δ, denoted DeltaSub δ, whose elements are precisely the multiples kδ for k in ℤ. The module documentation notes that this subgroup specializes to a clean order isomorphism when δ equals 1. The lemma depends on mul_eq_zero from IntegersFromLogic, which asserts that the logic integers have no zero divisors because of their isomorphism to the standard integers.
proof idea
The proof first uses sub_mul to show that (n - m) δ equals zero. It then applies mul_eq_zero to deduce that n - m equals zero or δ equals zero. The second alternative is ruled out by the assumption δ ≠ 0, and sub_eq_zero finishes the argument that n equals m.
why it matters in Recognition Science
The result provides the uniqueness half of the bijection between ℤ and the δ-subgroup. It is used in the quantization theorem, which states that every element of DeltaSub δ has a unique integer coefficient, and in the lemma toZ_fromZ to verify that the maps are inverses. Within the Recognition framework this step supports the construction of ledger units from the integer logic, feeding into the forcing chain toward physical constants.
scope and limits
- Does not prove existence of representations for subgroup elements.
- Does not extend cancellation to non-integral domains.
- Does not handle the zero divisor case when δ vanishes.
- Does not supply explicit bounds on coefficient sizes.
Lean usage
lemma example (δ n m : ℤ) (hδ : δ ≠ 0) (h : n * δ = m * δ) : n = m := rep_unique hδ hformal statement (Lean)
40lemma rep_unique {δ n m : ℤ} (hδ : δ ≠ 0) (h : n * δ = m * δ) : n = m := by
proof body
Tactic-mode proof.
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