Exact scales of rational numbers
Scale.ofRat q is the prime factorization of a positive rational q in the
formal-product representation: every prime of the numerator with exponent 1
and every prime of the denominator with exponent -1. Its exponent at a prime
p is the p-adic valuation of q, so multiplication of rationals is addition
of exponent maps — which is what lets every registry identity be checked exactly.
def Scale.ofPrimes : (l : List ℕ) → (∀ p ∈ l, p.Prime) → ℚ → Scale
Each prime in the list, with exponent e.
def Scale.ofNat (n : ℕ) (e : ℚ) : Scale
The prime factorization of n, each prime with exponent e.
@[simp] theorem Scale.exp_ofRat_prime (q : ℚ) (p : Nat.Primes) :
Scale.exp (Scale.ofRat q) (.prime p) = (padicValRat p.1 q : ℚ)
The exponent of a prime in ofRat q is the p-adic valuation of q.
theorem Scale.real_ofRat (q : ℚ) (hq : 0 < q) : Scale.real (Scale.ofRat q) = (q : ℝ)
ofRat q denotes q.
theorem Scale.exp_ofRat_mul (q r : ℚ) (hq : q ≠ 0) (hr : r ≠ 0) :
Scale.exp (Scale.ofRat (q * r)) = Scale.exp (Scale.ofRat q ++ Scale.ofRat r)
Multiplying rationals adds their exact scales.
theorem Scale.exp_ofRat_inj (q r : ℚ) (hq : 0 < q) (hr : 0 < r) :
Scale.exp (Scale.ofRat q) = Scale.exp (Scale.ofRat r) ↔ q = r
Two positive rationals have the same exact scale iff they are equal.