Skip to content

Frobenius pseudoprimes

11 fully proved

Polynomial

DefinitionGreatest common monic divisor#✓fully proved

Let \(R\) be a commutative ring and let \(h, g_1, g_2 \in R[x]\). Then \(h\) is a greatest common monic divisor of \(g_1\) and \(g_2\) when \(h\), \(g_1\) and \(g_2\) are monic and the ideal generated by \(g_1\) and \(g_2\) equals the principal ideal generated by \(h\).

Such an \(h\) need not exist.

public def IsGreatestCommonMonicDivisor {R : Type*} [CommRing R]
    (h g₁ g₂ : _root_.Polynomial R) : Prop :=
  h.Monic ∧ g₁.Monic ∧ g₂.Monic ∧
    Ideal.span ({g₁, g₂} : Set (_root_.Polynomial R)) =
      Ideal.span ({h} : Set (_root_.Polynomial R))
Sources
  • pseudo1.tex lines 617-624.
Used by 6
Used byFrobenius probable prime · Frobenius probable primes use monic polynomials · Frobenius probable primes are odd · Frobenius probable primes exceed one · Unfolding the greatest common monic divisor · Characterization of Frobenius probable primes

TheoremUnfolding the greatest common monic divisor#✓fully proved

For polynomials \(h\), \(g_1\) and \(g_2\) over a commutative ring \(R\), \(h\) is a greatest common monic divisor of \(g_1\) and \(g_2\) if and only if \(h\), \(g_1\) and \(g_2\) are monic and the ideal of \(R[X]\) generated by \(g_1\) and \(g_2\) equals the principal ideal generated by \(h\).

public theorem IsGreatestCommonMonicDivisor.unfold {R : Type*} [CommRing R]
    (h g₁ g₂ : _root_.Polynomial R) :
    IsGreatestCommonMonicDivisor h g₁ g₂ ↔
      (h.Monic ∧ g₁.Monic ∧ g₂.Monic ∧
        Ideal.span ({g₁, g₂} : Set (_root_.Polynomial R)) =
          Ideal.span ({h} : Set (_root_.Polynomial R)))
Uses 1
Statement usesGreatest common monic divisor

Frobenius probable primes and pseudoprimes

DefinitionFrobenius probable prime#✓fully proved

Let \(f \in \mathbb{Z}[x]\) be a polynomial of degree \(d\) with discriminant \(\Delta\), and let \(n\) be a natural number. Then \(n\) is a Frobenius probable prime with respect to \(f\) when \(f\) is monic, \(n\) is odd, \(n > 1\), \(n\) is coprime to \(|f(0)\Delta|\), and there exist polynomials \(F_i, f_i \in (\mathbb{Z}/n\mathbb{Z})[x]\) and natural numbers \(q_i\), indexed by \(i \in \mathbb{N}\), such that: - \(f_0\) is the reduction of \(f\) modulo \(n\), and \(f_d = 1\); - for each \(i\) with \(1 \le i \le d\), \(F_i\) is a greatest common monic divisor of \(x^{n^i} - x\) and \(f_{i-1}\), and \(f_{i-1} = F_i f_i\); - (Frobenius step) for each \(i\) with \(2 \le i \le d\), \(F_i(x)\) divides \(F_i(x^n)\); - for each even \(i\) with \(1 \le i \le d\), \(\deg F_i = i q_i\); - (Jacobi step) \((-1)^S = \left(\frac{\Delta}{n}\right)\), the Jacobi symbol, where \(S\) is the sum of \(q_i\) over the even \(i\) with \(1 \le i \le d\).

Nat.IsFrobeniusProbablePrime · 18 lines 
public def IsFrobeniusProbablePrime (n : ℕ) (f : _root_.Polynomial ℤ) : Prop :=
  f.Monic ∧ Odd n ∧ 1 < n ∧
    _root_.Nat.Coprime n (Int.natAbs (f.eval 0 * f.discr)) ∧
    ∃ F fs : ℕ → _root_.Polynomial (ZMod n),
      ∃ q : ℕ → ℕ,
        fs 0 = f.map (Int.castRingHom (ZMod n)) ∧
        fs f.natDegree = 1 ∧
        (∀ i ∈ Finset.Icc 1 f.natDegree,
          Polynomial.IsGreatestCommonMonicDivisor (F i)
            (Polynomial.X ^ (n ^ i) - Polynomial.X : _root_.Polynomial (ZMod n))
            (fs (i - 1)) ∧ fs (i - 1) = F i * fs i) ∧
        (∀ i ∈ Finset.Icc 2 f.natDegree,
          F i ∣ (F i).comp (Polynomial.X ^ n : _root_.Polynomial (ZMod n))) ∧
        (∀ i ∈ Finset.Icc 1 f.natDegree, Even i → (F i).natDegree = i * q i) ∧
        (-1 : ℤ) ^
            Finset.sum (Finset.Icc 1 f.natDegree)
              (fun i => if i % 2 = 0 then q i else 0) =
          jacobiSym f.discr n
Sources
  • pseudo1.tex lines 713-741.
Uses 1 · Used by 8
Statement usesGreatest common monic divisor
Used byFrobenius pseudoprimes are not prime · Frobenius pseudoprime · Frobenius probable primes use monic polynomials · Frobenius probable primes are odd · Frobenius probable primes exceed one · Frobenius pseudoprimes are Frobenius probable primes · Characterization of Frobenius probable primes · Characterization of Frobenius pseudoprimes

DefinitionFrobenius pseudoprime#✓fully proved

A natural number \(n\) is a Frobenius pseudoprime with respect to a polynomial \(f \in \mathbb{Z}[x]\) when \(n\) is not prime and \(n\) is a Frobenius probable prime with respect to \(f\).

Since a Frobenius probable prime exceeds \(1\), such an \(n\) is composite.

public def IsFrobeniusPseudoprime (n : ℕ) (f : _root_.Polynomial ℤ) : Prop :=
  ¬ n.Prime ∧ IsFrobeniusProbablePrime n f
Sources
  • pseudo1.tex lines 763-768.
Uses 1 · Used by 3
Statement usesFrobenius probable prime
Used byFrobenius pseudoprimes are not prime · Frobenius pseudoprimes are Frobenius probable primes · Characterization of Frobenius pseudoprimes

TheoremCharacterization of Frobenius probable primes#✓fully proved

Let \(f \in \mathbb{Z}[x]\) be a polynomial of degree \(d\) with discriminant \(\Delta\), and let \(n\) be a natural number. Then \(n\) is a Frobenius probable prime with respect to \(f\) if and only if \(f\) is monic, \(n\) is odd, \(n > 1\), \(n\) is coprime to \(|f(0)\Delta|\), and there exist polynomials \(F_i, f_i \in (\mathbb{Z}/n\mathbb{Z})[x]\) and natural numbers \(q_i\), indexed by \(i \in \mathbb{N}\), such that: - \(f_0\) is the reduction of \(f\) modulo \(n\), and \(f_d = 1\); - for each \(i\) with \(1 \le i \le d\), \(F_i\) is a greatest common monic divisor of \(x^{n^i} - x\) and \(f_{i-1}\), and \(f_{i-1} = F_i f_i\); - for each \(i\) with \(2 \le i \le d\), \(F_i(x)\) divides \(F_i(x^n)\); - for each even \(i\) with \(1 \le i \le d\), \(\deg F_i = i q_i\); - \((-1)^S = \left(\frac{\Delta}{n}\right)\), the Jacobi symbol, where \(S\) is the sum of \(q_i\) over the even \(i\) with \(1 \le i \le d\).

Nat.IsFrobeniusProbablePrime.unfold · 19 lines 
public theorem IsFrobeniusProbablePrime.unfold (n : ℕ) (f : _root_.Polynomial ℤ) :
    IsFrobeniusProbablePrime n f ↔
      (f.Monic ∧ Odd n ∧ 1 < n ∧
        _root_.Nat.Coprime n (Int.natAbs (f.eval 0 * f.discr)) ∧
        ∃ F fs : ℕ → _root_.Polynomial (ZMod n),
          ∃ q : ℕ → ℕ,
            fs 0 = f.map (Int.castRingHom (ZMod n)) ∧
            fs f.natDegree = 1 ∧
            (∀ i ∈ Finset.Icc 1 f.natDegree,
              Polynomial.IsGreatestCommonMonicDivisor (F i)
                (Polynomial.X ^ (n ^ i) - Polynomial.X : _root_.Polynomial (ZMod n))
                (fs (i - 1)) ∧ fs (i - 1) = F i * fs i) ∧
            (∀ i ∈ Finset.Icc 2 f.natDegree,
              F i ∣ (F i).comp (Polynomial.X ^ n : _root_.Polynomial (ZMod n))) ∧
            (∀ i ∈ Finset.Icc 1 f.natDegree, Even i → (F i).natDegree = i * q i) ∧
            (-1 : ℤ) ^
                Finset.sum (Finset.Icc 1 f.natDegree)
                  (fun i => if i % 2 = 0 then q i else 0) =
              jacobiSym f.discr n)
Uses 2
Statement usesFrobenius probable prime · Greatest common monic divisor

TheoremFrobenius probable primes use monic polynomials#✓fully proved

If \(n\) is a Frobenius probable prime with respect to a polynomial \(f \in \mathbb{Z}[x]\), then \(f\) is monic.

public theorem IsFrobeniusProbablePrime.monic {n : ℕ} {f : _root_.Polynomial ℤ}
    (h : IsFrobeniusProbablePrime n f) : f.Monic
Uses 2
Statement usesFrobenius probable prime
Proof usesGreatest common monic divisor

TheoremFrobenius probable primes are odd#✓fully proved

If \(n\) is a Frobenius probable prime with respect to a polynomial \(f \in \mathbb{Z}[x]\), then \(n\) is odd.

public theorem IsFrobeniusProbablePrime.odd {n : ℕ} {f : _root_.Polynomial ℤ}
    (h : IsFrobeniusProbablePrime n f) : Odd n
Uses 2
Statement usesFrobenius probable prime
Proof usesGreatest common monic divisor

TheoremFrobenius probable primes exceed one#✓fully proved

If \(n\) is a Frobenius probable prime with respect to a polynomial \(f \in \mathbb{Z}[x]\), then \(n > 1\).

public theorem IsFrobeniusProbablePrime.one_lt {n : ℕ} {f : _root_.Polynomial ℤ}
    (h : IsFrobeniusProbablePrime n f) : 1 < n
Uses 2
Statement usesFrobenius probable prime
Proof usesGreatest common monic divisor

TheoremCharacterization of Frobenius pseudoprimes#✓fully proved

For every natural number \(n\) and every polynomial \(f \in \mathbb{Z}[x]\), \(n\) is a Frobenius pseudoprime with respect to \(f\) if and only if \(n\) is not prime and \(n\) is a Frobenius probable prime with respect to \(f\).

public theorem IsFrobeniusPseudoprime.unfold (n : ℕ) (f : _root_.Polynomial ℤ) :
    IsFrobeniusPseudoprime n f ↔
      (¬ n.Prime ∧ IsFrobeniusProbablePrime n f)
Uses 2
Statement usesFrobenius probable prime · Frobenius pseudoprime

TheoremFrobenius pseudoprimes are not prime#✓fully proved

If \(n\) is a Frobenius pseudoprime with respect to a polynomial \(f \in \mathbb{Z}[x]\), then \(n\) is not prime.

public theorem IsFrobeniusPseudoprime.composite {n : ℕ} {f : _root_.Polynomial ℤ}
    (h : IsFrobeniusPseudoprime n f) : ¬ n.Prime
Uses 2
Statement usesFrobenius pseudoprime
Proof usesFrobenius probable prime

TheoremFrobenius pseudoprimes are Frobenius probable primes#✓fully proved

If \(n\) is a Frobenius pseudoprime with respect to a polynomial \(f \in \mathbb{Z}[x]\), then \(n\) is a Frobenius probable prime with respect to \(f\).

public theorem IsFrobeniusPseudoprime.probablePrime {n : ℕ} {f : _root_.Polynomial ℤ}
    (h : IsFrobeniusPseudoprime n f) : IsFrobeniusProbablePrime n f
Uses 2
Statement usesFrobenius probable prime · Frobenius pseudoprime

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.