feat(conway): verify 594 entries within the five-minute rebuild budget

[kim-em]

Expands the committed, fully verified Conway table from 38 to 594 entries, covering every prime characteristic below 1000. Every entry has irreducibility and primitivity proofs (including GF(2)), and all 522 supported proper-divisor pairs have compatibility proofs.

Coverage is divisor-closed, with no holes: degrees 1–16 at characteristic 2; 1–8 at 3, 5 and 7; 1–6 at 11 and 13; 1–4 at other primes below 300; and 1–3 at primes between 300 and 1000. The next larger 627-entry scope failed one of three runs even after simplifying replay; it is retained as a rejected candidate. Binary degrees 32 and 64 are expensive rejected candidates; degree 128 is explicitly unavailable in the pinned source.

The offline generator now emits both certificate tiers, shared Pocklington prime proofs, supported-entry witnesses, field instances, generator-order theorems, and subfield embeddings. Structural binary powers, direct exponents and bounded concurrent proof modules reduce replay costs. Ordinary builds fetch no data and search for no certificates or factorizations. The shared factorization-corpus coefficient cache is unchanged. The SPEC, READMEs, manual, conformance checks, release pins, and single-job CI are updated together.

On chungus2 (AMD EPYC 9455, Lean 4.34.0-rc2, LEAN_NUM_THREADS=8), three clean Conway rebuilds with dependencies retained take 244.786, 217.620 and 211.232 seconds. Complete additional HexGFq/HexGFqMathlib rebuilds take 20.525, 21.533 and 21.027 seconds. The report records exact scopes, source hashes, per-module times, peak memory, artifact sizes, failed candidates and reproduction commands.

Hosted CI evidence is committed too: a clean Conway rebuild takes 392.196 seconds, and the companion 27.161 seconds, on a four-thread Xeon 8573C runner. CI warms external imports, measures each initial clean build once with explicit resource limits, and reuses those outputs for subsequent targets. Source provenance checks include meta imports and the shared factorization cache.

Locally verified:

• Both complete libraries, Conway/field/primality conformance, HexPrimalityMathlib, and the manual chapter.
• Deterministic regeneration and 1,188 source-table comparisons, including the optional package adapter.
• Five complete compiled replay passes under the operation budgets; all 14 LeanBench verification registrations.
• The full five-trial lookup benchmark (2,970 observations) fits degree + 2; every fixed scientific check passes its hash and operation ceiling with a single runtime thread and CPU affinity.
• Dependency, release, trust-surface, source and documentation checks.

See the performance report for evidence and limitations. The imported polynomial choice comes from Lübeck; the proofs do not establish lexicographic minimality.

Closes #10093.