QuadraticKernelSeparation.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Disjoint prime supports of the two endpoint kernel populations

theorem OAI.Ostmann.kernel_prime_not_dvd_denominator line 14

Source documentation

A prime divisor of a kernel cannot divide the reduced denominator.

theorem kernel_prime_not_dvd_denominator (m : ℕ) (h x u t : ℤ)
    (hred : h.natAbs.Coprime m) (heq : u * t ^ 2 = (m : ℤ) * x - h)
    {p : ℕ} (hp : p.Prime) (hpu : p ∣ u.natAbs) : ¬p ∣ m := by
…

theorem OAI.Ostmann.quadratic_kernels_coprime line 31

Source documentation

The sumset primality condition forces opposite-side kernels to have disjoint prime factors. This is valid for signed kernels and endpoints.

theorem quadratic_kernels_coprime (m : ℕ) (h x y u v s t : ℤ)
    (hu0 : u ≠ 0)
    (hred : h.natAbs.Coprime m)
    (hx : u * s ^ 2 = (m : ℤ) * x - h)
    (hy : v * t ^ 2 = (m : ℤ) * y - h)
    (hprime : (x - y).natAbs.Prime)
    (hsmall : u.natAbs < (x - y).natAbs) :
    u.natAbs.Coprime v.natAbs := by
…