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

[alexanderlhicks]

What

Adds lake exe axiomsweep: kernel-level axiom / sorry accounting for the whole library, with a committed regression baseline.

The tool loads the built .olean environment (the same data the kernel checked) and computes, for every declaration under the swept root modules, the set of axioms it transitively depends on — i.e. the #print axioms information, library-wide, in one pass. Because it reads elaborated data rather than source text, it sees exactly what the kernel accepted: private declarations, macro-generated declarations, and instances included; no regex heuristics.

Why

PolyFun feeds VCV-io and ArkLib, and its kernel-level state turns out to be pristine — 0 sorryAx, 0 non-standard axioms across all 8,006 declarations. This PR proves that and adds the regression gate that keeps it true, mirroring the same tool on the sibling repos. Reviews of downstream repos have repeatedly found theorems that silently inherit sorryAx through framework stubs; this makes that class of defect mechanical to catch.

How

• scripts/AxiomSweep.lean (+ lean_exe axiomsweep in the lakefile): memoised traversal of the compiled environment; only imports core Lean, runtime-imports the built oleans, so it needs a completed lake build and adds no dependencies. Runs in seconds.
• scripts/axiom_baseline.json: the currently-known sorryAx-tainted declarations (and any non-standard-axiom dependents). --check fails iff a declaration is tainted that the baseline does not list; closing gaps stays green and prints a nudge to shrink the baseline via --update-baseline.
• CI: one report-only step after the build (::warning on regression). Flip to enforcing by deleting the || echo once the baseline has soaked for a few PRs.
• Docs updated in the same PR.

Modes

lake exe axiomsweep                     # summary
lake exe axiomsweep --out report.json   # full per-declaration report (name, module, kind, line, axioms)
lake exe axiomsweep --check             # regression gate against scripts/axiom_baseline.json
lake exe axiomsweep --update-baseline   # refresh the baseline; commit the diff
lake exe axiomsweep --root Foo          # override the swept root modules (repeatable)

Baseline at this commit

• 8,006 declarations across 224 PolyFun.* modules.
• 0 sorryAx-tainted, 0 non-standard-axiom-tainted — fully kernel-clean.
• Spot-checked against #print axioms (PFunctor.Display.responderCoalgebraEquiv_postcondition → [Quot.sound]); ./scripts/validate.sh --axioms verified green end-to-end.

Notes

• Same tool as ArkLib's alh/axiom-sweep branch (multi-root variant); the copies are intentionally self-contained per repo, mirroring how other scripts are shared across the org. If it proves its keep everywhere, extracting a shared home is a possible follow-up.
• lean4export was considered and deliberately not used: it targets external kernel checking, has no source positions, and would add a per-toolchain pinned dependency; walking the environment yields the same information with line numbers and zero new deps.
• The per-declaration report is not committed anywhere; only the baseline is tracked.

Adversarial review

Five independent adversarial reviewers (one per repo deployment) attacked the tool, wiring, and baselines before this PR was opened. Everything they confirmed is fixed in the follow-up commit on this branch:

• Collector defect (HIGH, confirmed in 4 repos): the one-pass DFS finalized self-referencing constants (every inductive/ctor pair) prematurely, producing per-declaration rows that diverged from #print axioms in both directions, with constructible shapes where a new sorry passed --check. Fixed with a fixpoint-repair phase computing the true kernel closure (now strictly more accurate than #print axioms, whose own CollectAxioms wobbles inside mutual families). Post-fix rows spot-verified against ground truth; sorry-sets unchanged everywhere.
• Axiom types now traversed (CollectAxioms parity); duplicate constNames rows deduped; native_decide axiom names normalized to their owning declaration (the ax_N_M counters are Elab.async/toolchain-volatile); --check/--update-baseline mutually exclusive; bare Lean.ofReduceBool/Lean.trustCompiler are never baselinable (floor).
• CI steps now distinguish taint findings (report-only during soak) from infrastructure failures (always fail).
• Known blind spots documented: structure-field defaults and examples never enter any environment walk (#print axioms included); unimported files are invisible — paired with each repo's import-completeness gate.

What survived attack unchanged: baseline determinism (byte-identical regeneration), all headline numbers, spot-checks vs #print axioms, gate exit-code semantics, and the CI/step placement.

🤖 Generated with Claude Code