test: add the BZMathlib conformance module and proof-track probe suite - #9504
Open
kim-em wants to merge 2 commits into
Open
test: add the BZMathlib conformance module and proof-track probe suite#9504kim-em wants to merge 2 commits into
kim-em wants to merge 2 commits into
Conversation
…actic surface HexBerlekampZassenhausMathlib owns an executable runtime (the factor_poly/irreducibility elaborators and their kernel-decide bang fallbacks), so per SPEC/testing.md it takes the ordinary Phase-3 criteria rather than the correspondence-only exemption. Add conformance/HexBerlekampZassenhausMathlib/Conformance.lean exercising all four tactic entry points on committed Polynomial ℤ and Hex.ZPoly fixtures across the certificate languages (single-prime witness, Eisenstein handover, multi-prime degree obstruction, kernel fallback), pinning hand-derived factor lists and counts, the decline diagnostics on reducible/zero/unit/over-budget inputs, and the emitted proofs' axiom cones; wire it into the HexConformance globs and record the runtime-contract conformance section in the library SPEC. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
This adds the Phase-4 proof-track evidence code for the HexBerlekampZassenhausMathlib tactic surface: build-only fresh modules under bench/HexBerlekampZassenhausMathlib/ProofProbe/ exercising factor_poly on distinct-quadratic products over ℤ at degrees 4/8/12 (with a degree-8 multiplicity-attribution pair), irreducibility on the Eisenstein binomials X^n - 2 at degrees 4/8/16, and the kernel-decide fallback irreducibility! on the Swinnerton-Dyer minimal polynomials at degrees 4/8, each with the matched import-all baseline; the HexBerlekampZassenhausMathlibProofProbe (CI) and HexBerlekampZassenhausMathlibProofProbeScientific (release) lean_libs; the external sweep runner scripts/bench/bz_mathlib_sweep.py with manifest tests; the libraries.yml proof_probes declaration (done_through unchanged; measurements are serialized externally); and the SPEC 'Phase-4 proof evidence' section. Progress notes in progress/2026-08-24T02-57-08Z.md. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
kim-em
enabled auto-merge (squash)
August 24, 2026 03:02
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This PR add the Phase-3 and Phase-4 evidence code for HexBerlekampZassenhausMathlib, which owns an executable tactic/checker surface and therefore falls outside the correspondence-only conformance exemption. The new
conformance/HexBerlekampZassenhausMathlib/Conformance.lean(Oracle: none — the surface is proof-emitting and kernel-certified, with the untrusted compiled search python-flint-checked in the computational sibling; Mode: always) coversirreducibility,factor_poly, and both budgeted!variants across typical, edge, and adversarial cases including the A4 multi-prime certificate, the cyclotomicX^6 - 1factor pinning, multiplicity attribution, the over-budget dense-size error path, and genuine kernel-fallback replays on Swinnerton-Dyer inputs, with five axiom pins at the clean triple. The Phase-4 proof track lands as ten matched-import build-only probes (Baseline, three factor ladders plus a repeated-factor partner, three irreducibility rungs, two kernel-replay rungs) split into a CI probe lib and a scientific arm, withscripts/bench/bz_mathlib_sweep.pyand its unit test mirroring the freshest sweep-runner model, the structuralproof_probes:registration the Mathlib-free bench lint requires, and new## Conformanceand## Phase-4 proof evidenceSPEC sections. The scaffolding token's flagged gaps are confirmed stale: #2200's associates ambiguity is resolved by sign-normalized multiset uniqueness in FactorSoundness.lean and #2201's Mignotte wiring is live in FactorBound.lean, both proven and axiom-pinned. Timed measurements and thedone_throughbumps follow in the serialized measurement PR.🤖 Prepared with Claude Code