hex

16.6. 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 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.

  • The Tier 2 compatibility proofs (Conway conditions across the subfield lattice) and Tier 3 search live in separate libraries above this one. This chapter documents only the Tier 1 committed lookup.

  • 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.