PrimalityAuxiliaryPrime.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.ExactQuantumFactoring.Primality.primorial_gt_cutoff line 13
Source documentation
A quantitative bound at the manuscript's unchanged cutoff n^8. We reuse Mathlib's proved Chebyshev bound instead of repeating its binomial argument.
```
lemma primorial_gt_cutoff {n : ℕ} (hn : 128 ≤ n) :
    2^(n^6) < primorial (n^8) := by
…
```
def OAI.ExactQuantumFactoring.Primality.badProduct line 58
Source documentation
The finite integer excluded by the auxiliary-prime search.
```
def badProduct (n m : ℕ) : ℕ := m * ∏ j ∈ Finset.Icc 1 (n^2), (m^j-1)
```
lemma OAI.ExactQuantumFactoring.Primality.badProduct_pos line 60
lemma OAI.ExactQuantumFactoring.Primality.badProduct_lt_cutoff line 69
theorem OAI.ExactQuantumFactoring.Primality.auxiliary_prime_exists line 98
Source documentation
The auxiliary prime searched for by the source algorithm exists within n^8; no number-theoretic existence oracle is included in the algorithm.
```
theorem auxiliary_prime_exists {n m : ℕ} (hn : 128 ≤ n) (hm : 2 ≤ m) (hmb : m < 2^n) :
    ∃ s : ℕ, s.Prime ∧ s ≤ n^8 ∧ s.Coprime m ∧ n^2 < orderOf (m : ZMod s) := by
…
```