feat(scripts): kernel-level axiom sweep with committed regression baseline

.github/workflows/lean_action_ci.yml

@@ -200,6 +200,8 @@ jobs:
         run: |
           bash scripts/build_timing_report.sh run test_path "$BUILD_TIMING_RESULTS" -- \
             bash -eo pipefail -c 'lake test'
+      - name: Axiom sweep
+        run: lake exe axiomsweep --check
       - name: Fail on build warnings
         continue-on-error: true
         run: lake build --wfail

AGENTS.md

@@ -16,6 +16,10 @@ Human contributors should usually start with [`README.md`](README.md),
    `./scripts/update-lib.sh` and then `./scripts/check-imports.sh`.
 4. Use `./scripts/lint-style.sh` when touching Lean style-sensitive files.
 5. If you touch repo docs or links, run `python3 ./scripts/check-docs-integrity.py`.
+6. When filling or adding a `sorry` (or anything that must stay axiom-clean), run
+   `lake exe axiomsweep --check`; refresh `scripts/axiom_baseline.json` with
+   `lake exe axiomsweep --update-baseline` and commit the diff if the change is
+   intentional. Native-compiler trust is never baselineable.
 
 ## Where To Work
 

docs/wiki/generated-files.md

@@ -9,6 +9,7 @@ This page records which paths are source of truth and which are derived outputs.
 | `CompPoly.lean` | Generated and committed | Regenerate with `./scripts/update-lib.sh` after adding, renaming, or deleting `CompPoly/**/*.lean` files. Emitted in module form: `module`, blank line, one `public import` per file. |
 | `CompPoly/Fields/*/Ext*/`*`CertData.lean` | Generated and committed | Rabin irreducibility certificate data for non-binomial extension moduli. Regenerate with `scripts/gen_rabin_certificate.py --p <p> --f <coeffs> --lean <path> --namespace <NS>`; the exact command is recorded in each file's docstring. Do not hand-edit. Nothing in them is trusted — the kernel re-checks every step through `CompPoly.RabinCert.runChain`. |
 | `bench/report-*.md`, `bench/results-*.jsonl`, `bench/evaluation-bench-*` | Generated, not source | Produced by `lake exe CompPolyBench`; keep reports as local or CI artifacts. All three patterns are ignored — the first two by `bench/.gitignore`, `evaluation-bench-*` by the root `.gitignore` — so a benchmark run leaves the working tree clean. |
+| `scripts/axiom_baseline.json` | Generated and committed | Kernel-level axiom/`sorry` regression baseline. Regenerate with `lake exe axiomsweep --update-baseline` after a built `lake build`; commit the diff in the same PR that intentionally adds or removes baselineable taint. Checked by the enforcing axiom-sweep CI step; native-compiler trust cannot be baselined. |
 | `CLAUDE.md` | Compatibility symlink | Must remain a symlink to `AGENTS.md`; do not replace it with a separate copy. |
 | `.lake/` | Derived, not source | Local dependency cache and build output produced by Lake. Do not edit files here by hand. |
 | `.lake/build/` | Derived, not source | Build artifacts from `lake build` and `lake test`. Safe to delete and regenerate. |

docs/wiki/quickstart.md

@@ -37,6 +37,29 @@ lake build
 lake test
 ```
 
+### Filling a `sorry`, or work that must stay axiom-clean
+
+```bash
+lake build
+lake exe axiomsweep --check
+```
+
+`axiomsweep` is kernel-level axiom/`sorry` accounting for every reportable
+`CompPoly.*` declaration, diffed against the committed baseline
+`scripts/axiom_baseline.json`. It sweeps the `CompPoly` library as imported by the
+umbrella (`tests/` and `bench/` are outside it), and inherits the blind spots of any
+environment walk (structure-field defaults and `example`s never enter the
+environment) — see the module docstring in `scripts/AxiomSweep.lean`. It fails only on *new*
+`sorryAx` or non-standard-axiom taint, so pre-existing gaps stay allowed. After
+intentionally adding or closing a `sorry`, refresh and commit the baseline:
+
+```bash
+lake exe axiomsweep --update-baseline
+```
+
+CI runs the same check as an enforcing gate (see `lean_action_ci.yml`). Native-compiler
+trust is never baselineable.
+
 ### Added, renamed, or deleted files under `CompPoly/`
 
 ```bash
@@ -82,8 +105,10 @@ to be covered there. See [`../../bench/README.md`](../../bench/README.md).
 
 - [`../../.github/workflows/lean_action_ci.yml`](../../.github/workflows/lean_action_ci.yml)
   runs a **warm** (incremental) `lake build` by default — reusing cached Lake
-  oleans so only dirty modules rebuild — then `lake test`, and posts a
-  build-timing report. It also builds and runs `CompPolyBench --medium` over the curated
+  oleans so only dirty modules rebuild — then `lake test`, then the axiom sweep
+  as an enforcing gate, and posts a build-timing report. It also builds and runs
+  `CompPolyBench --medium` over the curated
+  `BENCH_CI_GROUPS` selection, then uploads benchmark reports as CI artifacts.
   `BENCH_CI_GROUPS` selection, then uploads benchmark reports as CI artifacts.
   A full cold rebuild (`rm -rf .lake/build && lake build`) runs automatically
   when `lean-toolchain` or `lake-manifest.json` differs from the comparison base
@@ -129,6 +154,7 @@ Use the direct scripts when debugging a specific failure:
 python3 ./scripts/check-docs-integrity.py
 lake test
 lake build CompPolyBench
+lake exe axiomsweep --check
 ```
 
 For more detail on the helper scripts, see

lakefile.lean

@@ -41,3 +41,11 @@ lean_lib CompPolyBenchLib where
 
 lean_exe CompPolyBench where
   srcDir := "bench"
+
+/-- Kernel-level axiom / `sorry` accounting with a committed regression baseline
+(`scripts/axiom_baseline.json`). Runtime-imports the built CompPoly oleans, so run it
+after `lake build`. See `scripts/AxiomSweep.lean`. -/
+lean_exe axiomsweep where
+  srcDir := "scripts"
+  root := `AxiomSweep
+  supportInterpreter := true