hex

 Hex🔗

The hex project

hex is executable, verified computer algebra for Lean 4: finite fields, polynomial factorization, and lattice reduction. The computational core is Mathlib-free; each chapter documents one library and, where there is one, its correspondence with Mathlib.

Contents

  1. 1. HexMatrix: dense matrices and arithmetic
  2. 2. HexRowReduce: Gauss-Jordan reduction, span, and nullspace
  3. 3. HexDeterminant: the Leibniz determinant and cofactor theory
  4. 4. HexBareiss: the fraction-free integer determinant
  5. 5. HexGramSchmidt: Gram-Schmidt orthogonalization
  6. 6. HexLLL: lattice basis reduction
  7. 7. HexArith: low-level arithmetic foundations
  8. 8. HexModArith: machine-word modular arithmetic
  9. 9. HexPoly: normalized dense polynomials
  10. 10. HexPolyZ: integer dense polynomials
  11. 11. HexPolyFp: prime-field dense polynomials
  12. 12. HexGF2: packed GF(2) polynomials and GF(2ⁿ) fields
  13. 13. HexHensel: executable Hensel lifting
  14. 14. HexGFqRing: executable Fₚ quotient ring
  15. 15. HexGFqField: executable GF(pⁿ)
  16. 16. HexConway: Tier 1 Conway-polynomial lookup
  17. 17. HexGFq: canonical finite-field constructors