16.1. Introduction🔗

A Conway polynomial C(p, n) is the canonical irreducible degree-n polynomial over the prime field 𝔽_p used to give a standard, compatible presentation of the finite field 𝔽_{pⁿ}. The full treatment of Conway polynomials has three tiers: a Tier 1 lookup of committed table entries, Tier 2 proofs that those entries satisfy the Conway compatibility conditions across the subfield lattice, and Tier 3 search for entries beyond the committed table. HexConway is the executable Tier 1 library: it exposes the imported Lübeck Conway table as a lookup, keeping the baseline lookup separate from the later compatibility and search work.

HexConway is Mathlib-free. It depends only on HexBerlekamp (for the Rabin irreducibility checker that certifies each committed entry) and the prime-field polynomial library it reaches through it. Each supported (p, n) pair commits a named polynomial literal, a machine-checked irreducibility proof, and a Hex.Conway.SupportedEntry witness packaging the lookup together with its proof. See Cross-references.