PrimalityArithmetic.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.ExactQuantumFactoring.Primality.orbit_order_le line 12
lemma OAI.ExactQuantumFactoring.Primality.orbit_card_le line 25

lemma OAI.ExactQuantumFactoring.Primality.orbit_collision line 43

Source documentation

Pigeonhole collision in the square of side floor(sqrt |H|)+1.

lemma orbit_collision (s m p : ℕ) [NeZero s] :
    ∃ u v u' v' : ℕ,
      u ≤ Nat.sqrt (Nat.card (residueOrbit s m p)) ∧
      v ≤ Nat.sqrt (Nat.card (residueOrbit s m p)) ∧
      u' ≤ Nat.sqrt (Nat.card (residueOrbit s m p)) ∧
      v' ≤ Nat.sqrt (Nat.card (residueOrbit s m p)) ∧
      (u,v) ≠ (u',v') ∧
      ((m^u*p^v : ℕ) : ZMod s) = ((m^u'*p^v' : ℕ) : ZMod s) := by
…

Mentions: OAI.ExactQuantumFactoring.Primality.residueOrbit

lemma OAI.ExactQuantumFactoring.Primality.prime_factorization_positive line 72
lemma OAI.ExactQuantumFactoring.Primality.exponent_pair_injective line 78
Source documentation
Distinct exponent pairs represent distinct natural numbers, using the other prime divisor of m. This is where the perfect-power test is essential.
```
lemma exponent_pair_injective {m p q : ℕ} (hm : m ≠ 0)
    (hp : p.Prime) (hq : q.Prime) (hqm : q ∣ m) (hpq : p ≠ q) :
    Function.Injective (fun uv : ℕ × ℕ => m^uv.1*p^uv.2) := by
…
```
lemma OAI.ExactQuantumFactoring.Primality.exponent_bound line 97
lemma OAI.ExactQuantumFactoring.Primality.power_le_choose_mul line 106
Source documentation
Elementary combinatorial bound used in the appendix. Pair the descending factors M-i with c*(t-i), so no real logarithms or asymptotics are assumed.
```
lemma power_le_choose_mul {c s t : ℕ} (ht : t ≤ s) :
    c^t ≤ (c*s).choose t := by
…
```