A norm_num extension for Jacobi and Legendre symbols

We extend the norm_num tactic so that it can be used to provably compute the value of the Jacobi symbol J(a | b) or the Legendre symbol legendreSym p a when the arguments are numerals.

Implementation notes

We use the Law of Quadratic Reciprocity for the Jacobi symbol to compute the value of J(a | b) efficiently, roughly comparable in effort with the euclidean algorithm for the computation of the gcd of a and b. More precisely, the computation is done in the following steps.

• Use J(a | 0) = 1 (an artifact of the definition) and J(a | 1) = 1 to deal with corner cases.

• Use J(a | b) = J(a % b | b) to reduce to the case that a is a natural number. We define a version of the Jacobi symbol restricted to natural numbers for use in the following steps; see NormNum.jacobiSymNat. (But we'll continue to write J(a | b) in this description.)

• Remove powers of two from b. This is done via J(2a | 2b) = 0 and J(2a+1 | 2b) = J(2a+1 | b) (another artifact of the definition).

• Now 0 ≤ a < b and b is odd. If b = 1, then the value is 1. If a = 0 (and b > 1), then the value is 0. Otherwise, we remove powers of two from a via J(4a | b) = J(a | b) and J(2a | b) = ±J(a | b), where the sign is determined by the residue class of b mod 8, to reduce to a odd.

• Once a is odd, we use Quadratic Reciprocity (QR) in the form J(a | b) = ±J(b % a | a), where the sign is determined by the residue classes of a and b mod 4. We are then back in the previous case.

We provide customized versions of these results for the various reduction steps, where we encode the residue classes mod 2, mod 4, or mod 8 by using hypotheses like a % n = b. In this way, the only divisions we have to compute and prove are the ones occurring in the use of QR above.

def Mathlib.Meta.NormNum.jacobiSymNat (a : ℕ) (b : ℕ) : ℤ

The Jacobi symbol restricted to natural numbers in both arguments.

Equations

• Mathlib.Meta.NormNum.jacobiSymNat a b = jacobiSym (↑a) b

API Lemmas

We repeat part of the API for jacobiSym with NormNum.jacobiSymNat and without implicit arguments, in a form that is suitable for constructing proofs in norm_num.

theorem Mathlib.Meta.NormNum.jacobiSymNat.zero_right (a : ℕ) : Mathlib.Meta.NormNum.jacobiSymNat a 0 = 1

Base cases: b = 0, b = 1, a = 0, a = 1.

theorem Mathlib.Meta.NormNum.jacobiSymNat.one_right (a : ℕ) : Mathlib.Meta.NormNum.jacobiSymNat a 1 = 1

theorem Mathlib.Meta.NormNum.jacobiSymNat.zero_left (b : ℕ) (hb : Nat.beq (b / 2) 0 = false) : Mathlib.Meta.NormNum.jacobiSymNat 0 b = 0

theorem Mathlib.Meta.NormNum.jacobiSymNat.one_left (b : ℕ) : Mathlib.Meta.NormNum.jacobiSymNat 1 b = 1

theorem Mathlib.Meta.NormNum.LegendreSym.to_jacobiSym (p : ℕ) (pp : Fact (Nat.Prime p)) (a : ℤ) (r : ℤ) (hr : Mathlib.Meta.NormNum.IsInt (jacobiSym a p) r) : Mathlib.Meta.NormNum.IsInt (legendreSym p a) r

Turn a Legendre symbol into a Jacobi symbol.

theorem Mathlib.Meta.NormNum.JacobiSym.mod_left (a : ℤ) (b : ℕ) (ab' : ℕ) (ab : ℤ) (r : ℤ) (b' : ℤ) (hb' : ↑b = b') (hab : a % b' = ab) (h : ↑ab' = ab) (hr : Mathlib.Meta.NormNum.jacobiSymNat ab' b = r) : jacobiSym a b = r

The value depends only on the residue class of a mod b.

theorem Mathlib.Meta.NormNum.jacobiSymNat.mod_left (a : ℕ) (b : ℕ) (ab : ℕ) (r : ℤ) (hab : a % b = ab) (hr : Mathlib.Meta.NormNum.jacobiSymNat ab b = r) : Mathlib.Meta.NormNum.jacobiSymNat a b = r

theorem Mathlib.Meta.NormNum.jacobiSymNat.even_even (a : ℕ) (b : ℕ) (hb₀ : Nat.beq (b / 2) 0 = false) (ha : a % 2 = 0) (hb₁ : b % 2 = 0) : Mathlib.Meta.NormNum.jacobiSymNat a b = 0

The symbol vanishes when both entries are even (and b / 2 ≠ 0).

theorem Mathlib.Meta.NormNum.jacobiSymNat.odd_even (a : ℕ) (b : ℕ) (c : ℕ) (r : ℤ) (ha : a % 2 = 1) (hb : b % 2 = 0) (hc : b / 2 = c) (hr : Mathlib.Meta.NormNum.jacobiSymNat a c = r) : Mathlib.Meta.NormNum.jacobiSymNat a b = r

When a is odd and b is even, we can replace b by b / 2.

theorem Mathlib.Meta.NormNum.jacobiSymNat.double_even (a : ℕ) (b : ℕ) (c : ℕ) (r : ℤ) (ha : a % 4 = 0) (hb : b % 2 = 1) (hc : a / 4 = c) (hr : Mathlib.Meta.NormNum.jacobiSymNat c b = r) : Mathlib.Meta.NormNum.jacobiSymNat a b = r

If a is divisible by 4 and b is odd, then we can remove the factor 4 from a.

theorem Mathlib.Meta.NormNum.jacobiSymNat.even_odd₁ (a : ℕ) (b : ℕ) (c : ℕ) (r : ℤ) (ha : a % 2 = 0) (hb : b % 8 = 1) (hc : a / 2 = c) (hr : Mathlib.Meta.NormNum.jacobiSymNat c b = r) : Mathlib.Meta.NormNum.jacobiSymNat a b = r

If a is even and b is odd, then we can remove a factor 2 from a, but we may have to change the sign, depending on b % 8. We give one version for each of the four odd residue classes mod 8.

theorem Mathlib.Meta.NormNum.jacobiSymNat.even_odd₇ (a : ℕ) (b : ℕ) (c : ℕ) (r : ℤ) (ha : a % 2 = 0) (hb : b % 8 = 7) (hc : a / 2 = c) (hr : Mathlib.Meta.NormNum.jacobiSymNat c b = r) : Mathlib.Meta.NormNum.jacobiSymNat a b = r

theorem Mathlib.Meta.NormNum.jacobiSymNat.even_odd₃ (a : ℕ) (b : ℕ) (c : ℕ) (r : ℤ) (ha : a % 2 = 0) (hb : b % 8 = 3) (hc : a / 2 = c) (hr : Mathlib.Meta.NormNum.jacobiSymNat c b = r) : Mathlib.Meta.NormNum.jacobiSymNat a b = -r

theorem Mathlib.Meta.NormNum.jacobiSymNat.even_odd₅ (a : ℕ) (b : ℕ) (c : ℕ) (r : ℤ) (ha : a % 2 = 0) (hb : b % 8 = 5) (hc : a / 2 = c) (hr : Mathlib.Meta.NormNum.jacobiSymNat c b = r) : Mathlib.Meta.NormNum.jacobiSymNat a b = -r

theorem Mathlib.Meta.NormNum.jacobiSymNat.qr₁ (a : ℕ) (b : ℕ) (r : ℤ) (ha : a % 4 = 1) (hb : b % 2 = 1) (hr : Mathlib.Meta.NormNum.jacobiSymNat b a = r) : Mathlib.Meta.NormNum.jacobiSymNat a b = r

Use quadratic reciproity to reduce to smaller b.

theorem Mathlib.Meta.NormNum.jacobiSymNat.qr₁_mod (a : ℕ) (b : ℕ) (ab : ℕ) (r : ℤ) (ha : a % 4 = 1) (hb : b % 2 = 1) (hab : b % a = ab) (hr : Mathlib.Meta.NormNum.jacobiSymNat ab a = r) : Mathlib.Meta.NormNum.jacobiSymNat a b = r

theorem Mathlib.Meta.NormNum.jacobiSymNat.qr₁' (a : ℕ) (b : ℕ) (r : ℤ) (ha : a % 2 = 1) (hb : b % 4 = 1) (hr : Mathlib.Meta.NormNum.jacobiSymNat b a = r) : Mathlib.Meta.NormNum.jacobiSymNat a b = r

theorem Mathlib.Meta.NormNum.jacobiSymNat.qr₁'_mod (a : ℕ) (b : ℕ) (ab : ℕ) (r : ℤ) (ha : a % 2 = 1) (hb : b % 4 = 1) (hab : b % a = ab) (hr : Mathlib.Meta.NormNum.jacobiSymNat ab a = r) : Mathlib.Meta.NormNum.jacobiSymNat a b = r

theorem Mathlib.Meta.NormNum.jacobiSymNat.qr₃ (a : ℕ) (b : ℕ) (r : ℤ) (ha : a % 4 = 3) (hb : b % 4 = 3) (hr : Mathlib.Meta.NormNum.jacobiSymNat b a = r) : Mathlib.Meta.NormNum.jacobiSymNat a b = -r

theorem Mathlib.Meta.NormNum.jacobiSymNat.qr₃_mod (a : ℕ) (b : ℕ) (ab : ℕ) (r : ℤ) (ha : a % 4 = 3) (hb : b % 4 = 3) (hab : b % a = ab) (hr : Mathlib.Meta.NormNum.jacobiSymNat ab a = r) : Mathlib.Meta.NormNum.jacobiSymNat a b = -r

theorem Mathlib.Meta.NormNum.isInt_jacobiSym {a : ℤ} {na : ℤ} {b : ℕ} {nb : ℕ} {r : ℤ} : Mathlib.Meta.NormNum.IsInt a na → Mathlib.Meta.NormNum.IsNat b nb → jacobiSym na nb = r → Mathlib.Meta.NormNum.IsInt (jacobiSym a b) r

theorem Mathlib.Meta.NormNum.isInt_jacobiSymNat {a : ℕ} {na : ℕ} {b : ℕ} {nb : ℕ} {r : ℤ} : Mathlib.Meta.NormNum.IsNat a na → Mathlib.Meta.NormNum.IsNat b nb → Mathlib.Meta.NormNum.jacobiSymNat na nb = r → Mathlib.Meta.NormNum.IsInt (Mathlib.Meta.NormNum.jacobiSymNat a b) r

Certified evaluation of the Jacobi symbol

The following functions recursively evaluate a Jacobi symbol and construct the corresponding proof term.

The norm_num plug-in

def Tactic.NormNum.evalJacobiSym : Mathlib.Meta.NormNum.NormNumExt

This is the norm_num plug-in that evaluates Jacobi symbols.

Equations

• One or more equations did not get rendered due to their size.

def Tactic.NormNum.evalJacobiSymNat : Mathlib.Meta.NormNum.NormNumExt

This is the norm_num plug-in that evaluates Jacobi symbols on natural numbers.

Equations

• One or more equations did not get rendered due to their size.

def Tactic.NormNum.evalLegendreSym : Mathlib.Meta.NormNum.NormNumExt

This is the norm_num plug-in that evaluates Legendre symbols.

Equations

• One or more equations did not get rendered due to their size.