hex

20.5. Key correctness theorem🔗

The point of committing a table rather than computing on demand is that each entry carries a machine-checked irreducibility proof. For every supported pair the library proves luebeckConwayPolynomial_p_n_irreducible : FpPoly.Irreducible luebeckConwayPolynomial_p_n, discharged by running the Berlekamp Rabin irreducibility certificate checker, whose soundness is Hex.Berlekamp.rabinTest_imp_irreducible, on a committed certificate. The representative statement for C(2, 3):

🔗theorem
Hex.Conway.luebeckConwayPolynomial_2_3_irreducible :
  Hex.Conway.luebeckConwayPolynomial_2_3.Irreducible
Hex.Conway.luebeckConwayPolynomial_2_3_irreducible :
  Hex.Conway.luebeckConwayPolynomial_2_3.Irreducible

Irreducibility of the imported C(2, 3).

Because the certificate is checked at elaboration time, the irreducible factor structure of the committed table is part of the library's guarantee, not a runtime assertion: a corrupted entry would fail to typecheck rather than silently return a reducible polynomial.