Unrestricted depth-three lower bound: irreducible polynomial

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Computability/DepthThree/IrreduciblePolynomial.lean

Imports, namespaces, module visibility, documentation, and formatting are adapted for complexitylib. The source theorem statements and mathematical proofs are retained.

theorem Complexity.DepthThreeLowerBound.exists_monic_irreducible_natDegree_two (r : ℕ) (hr : 0 < r) : ∃ (P : Polynomial (ZMod 2)), P.Monic ∧ Irreducible P ∧ P.natDegree = r

theorem Complexity.DepthThreeLowerBound.exists_monic_irreducible_degree_two (r : ℕ) (hr : 0 < r) : ∃ (P : Polynomial (ZMod 2)), P.Monic ∧ Irreducible P ∧ P.degree = ↑r