hex

17.6. Key correctness: Lean-checked irreducibility🔗

A finite field exists only when its modulus is irreducible, so every constructor in this library ultimately rests on an irreducibility proof. For the generic constructors that proof is the HexConway entry's; for the packed constructors it is a separate certificate over the HexGF2 GF2Poly.Irreducible predicate, discharged by decide on a checkable certificate, never by native_decide. The degree-one case is small enough to prove by exhausting the two monic linear polynomials over 𝔽₂:

🔗theorem
Hex.Conway.packedGF2Entry_2_1_irreducible :
  (Hex.GF2Poly.ofUInt64Monic 1 1).Irreducible
Hex.Conway.packedGF2Entry_2_1_irreducible :
  (Hex.GF2Poly.ofUInt64Monic 1
      1).Irreducible

The packed modulus corresponding to the committed Conway entry C(2, 1) = X + 1.

Higher-degree committed entries are certified the same way through the HexGF2 certificate checker. Because the check runs at elaboration time, a corrupted packed modulus would fail to typecheck rather than silently producing a non-field, so the irreducible-modulus guarantee is checked when the library compiles, not a runtime assertion.