[codex] Add Mersenne31 regression tests for PR 257

[adrienlacombe]

Summary

Adds a small regression-test layer on top of Verified-zkEVM#257's Mersenne31 implementation.

Changes

• Adds CompPolyTests.Fields.Mersenne31.
• Checks the canonical Mersenne31.Basic prime, field, and NonBinaryField instances.
• Checks the Mersenne31.Fast field surface and representative/canonical conversion behavior for a few arithmetic paths.
• Imports the test module from CompPolyTests.

Validation

• lake build CompPolyTests.Fields.Mersenne31
• lake build CompPolyTests
• ./scripts/lint-style.py tests/CompPolyTests/Fields/Mersenne31.lean
• ./scripts/lint-style.sh
• ./scripts/check-imports.sh
• lake test

[github-actions]

Build Timing Report

• Commit: 1e6fb3b
• Message: Merge 8fda131 into 5068d4c
• Ref: feat/pr257-mersenne31-tests
• Measured on ubuntu-latest with /usr/bin/time -p.
• Commands: library build (warm) lake build; test path lake test.
• Clean build was skipped (warm/incremental CI; no toolchain or lake-manifest change). Runs automatically when lean-toolchain or lake-manifest.json changes, or via Actions → Lean Action CI → Run workflow with clean_build.

Measurement	Wall (s)	Status
Library build (warm)	345.14	ok
Test path	42.77	ok

Incremental Rebuild Signal

• Warm-only run: default CI reuses cached oleans and rebuilds dirty modules only. No same-job clean:warm ratio.

Slowest Current Build Files (warm library build)

Showing 20 slowest of 277 repo targets parsed from the current warm library build log.

Wall (s)	Path
45.00	CompPoly/Fields/Montgomery/Native64x8Inv.lean
24.00	CompPoly/Bivariate/Deriv.lean
22.00	CompPoly/Bivariate/ToPoly.lean
16.00	CompPoly/Univariate/Raw/Proofs.lean
15.00	CompPoly/Univariate/NTTFast/Correctness/Radix4DIT.lean
14.00	CompPoly/Univariate/NTTFast/Correctness/Radix4DIF.lean
14.00	CompPoly/Fields/Binary/Tower/Support/Preliminaries.lean
13.00	CompPoly/Fields/Binary/AdditiveNTT/Intermediate.lean
13.00	CompPoly/Fields/Binary/BF128Ghash/XPowTwoPowModCertificate.lean
12.00	CompPoly/Bivariate/Factor.lean
12.00	CompPoly/Bivariate/GuruswamiSudan/Root/Alekhnovich/Correctness.lean
11.00	CompPoly/Fields/Binary/AdditiveNTT/Domain.lean
10.00	CompPoly/Data/Nat/Bitwise.lean
10.00	CompPoly/Fields/Montgomery/Native32Field.lean
10.00	CompPoly/Fields/Binary/AdditiveNTT/NovelPolynomialBasis.lean
10.00	CompPoly/Fields/Montgomery/Native64x8.lean
10.00	CompPoly/Univariate/NTT/Forward.lean
10.00	CompPoly/Univariate/DivisionCorrectness.lean
10.00	CompPoly/Univariate/NTTFast/Correctness/DIF.lean
10.00	CompPoly/Multilinear/Basic.lean