hex

16.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 (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

The committed C(2, 3) entry is irreducible.

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.