3.8. Cross-references🔗

• HexArith supplies the Mathlib-free prime predicate, modular exponentiation, gcd, and exact trial-division foundation.

• HexBasic supplies the explicit reproducible random state used by every bounded randomized search.

• HexIntFactor reuses primality certificates and the factor-search primitives to certify complete natural-number factorizations.