PrimalityCorrectness.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

def OAI.ExactQuantumFactoring.Primality.PerfectPower line 14
Source documentation
The actual first rejection test in the appendix.
```
def PerfectPower (m : ℕ) : Prop := ∃ b e : ℕ, 2 ≤ b ∧ 2 ≤ e ∧ b^e = m
```
lemma OAI.ExactQuantumFactoring.Primality.other_prime_divisor line 16
lemma OAI.ExactQuantumFactoring.Primality.sqrt_exponent_lt line 33
lemma OAI.ExactQuantumFactoring.Primality.upper_lt_lower line 46

lemma OAI.ExactQuantumFactoring.Primality.root_count_contradiction line 61

Source documentation

This is the appendix's entire root-count contradiction, over an arbitrary characteristic-p extension with a primitive s-th root.

lemma root_count_contradiction {F : Type*} [Field F] {n m s p q : ℕ}
    [Fact s.Prime] [Fact p.Prime] [CharP F p]
    (hn : 3 ≤ n) (hm : 2 ≤ m) (hmb : m < 2^n)
    (hms : (m : ZMod s) ≠ 0) (hps : (p : ZMod s) ≠ 0)
    (hpbig : 8*s < p) (hpm : p ∣ m) (hq : q.Prime) (hqm : q ∣ m) (hpq : p ≠ q)
    (horder : n^2 < orderOf (m : ZMod s))
    {w : F} (hw : IsPrimitiveRoot w s)
    (htest : ∀ a : ℕ, 1 ≤ a → a ≤ 8*s → Introspective s m (X+C (a : F))) : False := by
…

Mentions: OAI.ExactQuantumFactoring.Primality.Introspective

def OAI.ExactQuantumFactoring.Primality.CongruenceTest line 111
Source documentation
The source congruence test, represented without an assumed polynomial identity or an assumed primality oracle.
```
def CongruenceTest (m s a : ℕ) : Prop :=
…
```
lemma OAI.ExactQuantumFactoring.Primality.congruenceTest_to_introspective line 114

theorem OAI.ExactQuantumFactoring.Primality.large_branch_prime line 123

Source documentation

Soundness of the accepting, large-input branch of the exact appendix test. The small branch is literal trial division.

theorem large_branch_prime {n m s : ℕ} (hn : 128 ≤ n) (hm : 2 ≤ m) (hmb : m < 2^n)
    (hs : s.Prime) (hcop : s.Coprime m) (horder : n^2 < orderOf (m : ZMod s))
    (hpow : ¬ PerfectPower m)
    (hsmall : ∀ d : ℕ, 2 ≤ d → d ≤ 8*s → ¬ d ∣ m)
    (htest : ∀ a : ℕ, 1 ≤ a → a ≤ 8*s → CongruenceTest m s a) : m.Prime := by
…

Mentions: OAI.ExactQuantumFactoring.Primality.PerfectPower, OAI.ExactQuantumFactoring.Primality.CongruenceTest