Documentation

LeanPool.SingularModuli.QuadraticOrder.RootCounting

Layer 3: Root Counting for Quadratic Congruences #

This file counts solutions to x² ≡ c (mod p^n) for prime powers p^n. These are the "analytic inputs" for the ideal-counting theorems (Layer 4).

Definition #

source
def QuadraticOrder.cardSqrts (n : ℕ) [NeZero n] (c : ZMod n) :
ℕ

The number of elements x in ZMod n satisfying x ^ 2 = c.

Equations
Instances For

    Base case: odd prime p #

    source
    theorem QuadraticOrder.cardSqrts_prime (p : ℕ) [hp : Fact (Nat.Prime p)] (hp2 : p ≠ 2) (c : ℤ) :
    ↑(cardSqrts p ↑c) = legendreSym p c + 1

    For an odd prime p, the number of solutions to x² = c in ZMod p equals legendreSym p c + 1.

    Odd prime powers #

    source
    theorem QuadraticOrder.cardSqrts_prime_pow_coprime (p : ℕ) [hp : Fact (Nat.Prime p)] (hp2 : p ≠ 2) (n : ℕ) (hn : 0 < n) (c : ℤ) (hc : ¬↑p ∣ c) :
    cardSqrts (p ^ n) ↑c = if legendreSym p c = 1 then 2 else 0

    For odd prime p and p ∤ c, each of the 0 or 2 roots mod p lifts uniquely through all ZMod (p^n) by Hensel's lemma.

    source
    theorem QuadraticOrder.cardSqrts_odd_val_eq_zero (p : ℕ) [hp : Fact (Nat.Prime p)] (n r : ℕ) (u : ℤ) (hr : 2 * r + 1 < n) (hu : ¬↑p ∣ u) :
    cardSqrts (p ^ n) ↑(↑p ^ (2 * r + 1) * u) = 0

    If the p-adic valuation of c is odd and less than n, then x² ≡ c (mod p^n) has no solutions.

    source
    theorem QuadraticOrder.cardSqrts_prime_pow_even_val (p : ℕ) [hp : Fact (Nat.Prime p)] (hp2 : p ≠ 2) (n r : ℕ) (u : ℤ) (hr : 2 * r < n) (hu : ¬↑p ∣ u) :
    cardSqrts (p ^ n) ↑(↑p ^ (2 * r) * u) = if legendreSym p u = 1 then 2 * p ^ r else 0

    When c = p^{2r} · u with p ∤ u and 2r < n, the substitution x = p^r · y reduces the problem to solving y² ≡ u (mod p^{n-2r}).

    source
    theorem QuadraticOrder.cardSqrts_zero (p : ℕ) [hp : Fact (Nat.Prime p)] (n : ℕ) (hn : 0 < n) :
    cardSqrts (p ^ n) 0 = p ^ (n / 2)

    When c ≡ 0 (mod p^n), every multiple of p^⌈n/2⌉ is a solution, giving p^⌊n/2⌋ solutions total.

    Powers of 2 #

    source
    theorem QuadraticOrder.cardSqrts_two (u : ZMod 2) :
    cardSqrts 2 u = 1

    In ZMod 2, squaring is the identity.

    source
    theorem QuadraticOrder.cardSqrts_four_odd (u : ZMod 4) (hu : u = 1 ∨ u = 3) :
    cardSqrts 4 u = if u = 1 then 2 else 0

    In ZMod 4, for odd u, there are 2 roots or none.

    source
    theorem QuadraticOrder.cardSqrts_eight (u : ZMod 8) (hu : u = 1 ∨ u = 3 ∨ u = 5 ∨ u = 7) :
    cardSqrts 8 u = if u = 1 then 4 else 0

    In ZMod 8, for odd u, there are 4 roots or none.