20.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 implements Tiers 1 and 2: it exposes the imported Lübeck Conway table as a lookup with irreducibility, primitivity, and divisor compatibility proofs. Tier 3 search is unimplemented. The imported choice comes from Lübeck; these proofs do not establish lexicographic minimality.

HexConway is Mathlib-free. It depends on HexBerlekamp for Rabin irreducibility certificates and HexPrimality for certificates of the prime factors of multiplicative orders, together with the prime-field polynomial and quotient libraries. 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.