20.6. Regenerating the table🔗

The committed table is ordinary Lean code that the kernel checks like any other definition, and it is long: coefficient literals, monicity and degree lemmas, a Rabin certificate, and an irreducibility proof for every entry. Changing which slice of Lübeck's data is committed is therefore not a hand edit. The offline generator scripts/conway/generate.py reads the exact pair list in scripts/conway/scope.json and the pinned source rows in scripts/conway/candidates.json. With the pinned SymPy version installed, run it to regenerate coefficients, Rabin certificates, factorizations, primality certificates, primitivity and compatibility proofs, supported-entry witnesses, Mathlib generator-order and subfield-embedding specializations, and the runtime replay driver. Its --check mode verifies that committed outputs match the inputs.

Only scripts/conway/import_source.py fetches Lübeck's source. The source URL, digest, coefficient convention, and unavailable requested pairs are recorded alongside the imported rows. The separate shared Lübeck cache used by the factorization benchmark corpus is unchanged by this pipeline. The Lean commands rebuild_luebeckConwayPolynomial? and #conway_entry_source remain available for inspecting individual entries. Ordinary builds perform no network requests or certificate searches.

The scope must preserve existing support and contain every positive divisor of each supported degree. Selection is measured against a 300-second clean rebuild ceiling for all Conway code and proofs with dependencies already built. The selected scope must pass three controlled runs. Additional Mathlib bridge compilation is measured separately. See reports/hex-conway-performance.md for the machine, exact scopes, costs, and unavailable or expensive candidates.