theorem TwinPrime.twin_prime_conjecture (N : ℕ) : HasTwinPrimeFrom N

Twin prime conjecture: for every threshold N, there is a twin-prime starter p >= N.

theorem TwinPrime.twin_prime_unbounded_iff_infinite : (∀ (N : ℕ), HasTwinPrimeFrom N) ↔ {p : ℕ | IsTwinPrimeAt p}.Infinite

TODO: Prove equivalence between unbounded and infinite-set formulations.

theorem TwinPrime.infinitely_many_twin_primes : {p : ℕ | IsTwinPrimeAt p}.Infinite

theorem TwinPrime.twin_prime_counting_lower_bound_todo : True

TODO: Add quantitative consequences and asymptotic comparison statements.