theorem Oppermann.oppermann_conjecture (n : ℕ) : 2 ≤ n → HasOppermannPrimes n

Oppermann's conjecture: for each n >= 2, there is a prime in each of (n(n-1), n^2) and (n^2, n(n+1)).

theorem Oppermann.legendre_form_of_oppermann_conjecture (n : ℕ) : 1 ≤ n → HasPrimeBetweenSquares n

Legendre-style consequence obtained by shifting the Oppermann index.

theorem Oppermann.two_primes_between_squares_todo : True

TODO: Show Oppermann implies at least two primes between consecutive squares.

theorem Oppermann.asymptotic_consequences_todo : True

TODO: Add asymptotic and density-style consequences as formal targets.