20.7. Cross-references🔗

HexConway is near the top of the finite-field portion of the DAG:

• HexBerlekamp is the direct dependency. Its Rabin irreducibility test and the soundness theorem Hex.Berlekamp.rabinTest_imp_irreducible (lifting a passing certificate to Hex.FpPoly.Irreducible) certify every committed entry in the correctness section. The prime-field polynomial type Hex.FpPoly and its arithmetic are reached transitively through it.

• Tier 2 primitivity and divisor compatibility are implemented in this library. Generator-order and subfield-embedding bridges live in HexGFqMathlib. Tier 3 search is unimplemented. Every supported entry has an irreducibility proof and a primitivity certificate, including C(2, 1) with its trivial multiplicative group. Every supported proper-divisor pair has a compatibility theorem. The lexicographically minimal choice is imported from Lübeck and checked against the pinned source by the conformance oracle; minimality itself is not proved in Lean.

• HexPrimality supplies Mathlib-free Pocklington certificates for large factors of p^n - 1, avoiding unbounded trial division during builds.

• HexConway is consumed by HexGFq, which turns a Hex.Conway.SupportedEntry into the canonical field GFq p n by handing the committed modulus to the quotient construction in HexGFqField. The table is what makes that field canonical rather than merely a field of order pⁿ: every caller naming GFq 3 4 gets the same modulus, so elements computed in one place are comparable with elements computed in another.

• HexConway is Mathlib-free and never depends on Mathlib. The Mathlib correspondence proofs for the finite-field theory it draws on live in the higher layers' *Mathlib counterparts, not in this library.