theorem TwinPrime.isTwinPrimePair_iff {p q : ℕ} : IsTwinPrimePair p q ↔ IsTwinPrimeAt p ∧ q = p + 2

theorem TwinPrime.isTwinPrimeAt_three : IsTwinPrimeAt 3

theorem TwinPrime.isTwinPrimeAt_five : IsTwinPrimeAt 5

theorem TwinPrime.isTwinPrimeAt_eleven : IsTwinPrimeAt 11

theorem TwinPrime.hasTwinPrimeFrom_zero : HasTwinPrimeFrom 0

theorem TwinPrime.hasTwinPrimeFrom_three : HasTwinPrimeFrom 3

theorem TwinPrime.hasTwinPrimeFrom_ten : HasTwinPrimeFrom 10

theorem TwinPrime.IsTwinPrimeAt.left_prime {p : ℕ} (h : IsTwinPrimeAt p) : Nat.Prime p

theorem TwinPrime.IsTwinPrimeAt.right_prime {p : ℕ} (h : IsTwinPrimeAt p) : Nat.Prime (p + 2)

theorem TwinPrime.odd_of_isTwinPrimeAt_of_two_lt {p : ℕ} (hp2 : 2 < p) (h : IsTwinPrimeAt p) : Odd p

TODO: Show all nontrivial twin-prime starters are odd.

theorem TwinPrime.mod_six_of_large_twin_prime {p : ℕ} (hp3 : 3 < p) (h : IsTwinPrimeAt p) : p % 6 = 5

TODO: Show any sufficiently large twin-prime starter is 5 mod 6.

theorem TwinPrime.finite_exclusion_criterion_todo : True

TODO: Develop sieve-style exclusions for candidate starters.