diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index cfd37c4..56f537e 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -49,7 +49,7 @@ jobs:
         run: lake exe cache get
 
       - name: Run validation wrapper
-        run: ./scripts/validate.sh
+        run: ./scripts/validate.sh --axioms
 
       - name: Save Lean cache
         if: success() && steps.lake-cache.outputs.cache-hit != 'true'
diff --git a/AGENTS.md b/AGENTS.md
index 3bac8b2..fbd0068 100644
--- a/AGENTS.md
+++ b/AGENTS.md
@@ -186,6 +186,10 @@ lake exe cache get && lake build
 
 After adding new `.lean` files: `./scripts/update-lib.sh`.
 For routine local validation: `./scripts/validate.sh`.
+For anything that must stay axiom-clean, run `./scripts/validate.sh --axioms`.
+PolyFun has a zero-debt baseline: do not add `sorry` or non-standard axioms to it.
+`lake exe axiomsweep --update-baseline` only rewrites the empty baseline after all
+taint has been removed; it refuses to record tainted declarations.
 
 Environment linters and the test library have Lake drivers:
 
diff --git a/docs/wiki/quickstart.md b/docs/wiki/quickstart.md
index 3922481..899ccd2 100644
--- a/docs/wiki/quickstart.md
+++ b/docs/wiki/quickstart.md
@@ -56,8 +56,14 @@ untracked `PolyFun/**/*.lean` files are present.
 
 `--lint` adds `lake lint` (Batteries' environment linters: `docBlame`,
 `simpNF`, `checkUnivs`, …) to the convenience wrapper. `--test` adds
-`lake test` (builds the `PolyFunTest` library). The main CI `build` job runs
-`validate.sh` without these flags, but separate `lint` and `test` CI jobs run
+`lake test` (builds the `PolyFunTest` library). `--axioms` adds
+the executable fixture matrix and `lake exe axiomsweep --check`. The check scans
+every imported `PolyFun.*` declaration and fails on any `sorryAx` or non-standard
+axiom dependency. The committed `scripts/axiom_baseline.json` is a zero-debt
+policy, not an allowlist: both arrays must remain empty. Update mode refuses to
+record taint and is only useful for resetting a stale baseline after all debt is
+removed. The main CI `build` job runs `validate.sh --axioms`, so a taint finding
+fails CI. Separate `lint` and `test` CI jobs run
 `lake lint` / `lake test`, and the `linting.yml` workflow runs the text style
 lint, so treat all three as required for merge. Text style (copyright headers,
 line length, module docstrings) is additionally enforced at build time by the
diff --git a/lakefile.toml b/lakefile.toml
index 97fe35b..acdac31 100644
--- a/lakefile.toml
+++ b/lakefile.toml
@@ -49,3 +49,18 @@ name = "PolyFun"
 name = "PolyFunTest"
 globs = ["PolyFunTest.+"]
 leanOptions = { weak.linter.style.header = false }
+
+# Kernel-level axiom / sorry accounting; see scripts/AxiomSweep.lean.
+# Runtime-imports the built PolyFun oleans, so run it after `lake build`.
+[[lean_exe]]
+name = "axiomsweep"
+srcDir = "scripts"
+root = "AxiomSweep"
+supportInterpreter = true
+
+# Isolated executable fixtures for the axiom-sweep mutation matrix. This library is not
+# a default target and deliberately contains synthetic kernel taint.
+[[lean_lib]]
+name = "AxiomSweepTestFixtures"
+srcDir = "scripts"
+globs = ["AxiomSweepTestFixtures.+"]
diff --git a/scripts/AxiomSweep.lean b/scripts/AxiomSweep.lean
new file mode 100644
index 0000000..cd8980e
--- /dev/null
+++ b/scripts/AxiomSweep.lean
@@ -0,0 +1,340 @@
+/-
+Copyright (c) 2026 PolyFun Contributors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Alexander Hicks
+-/
+import Lean
+
+/-!
+# Axiom sweep: whole-library kernel-level axiom and `sorry` accounting
+
+Walks the compiled environment (the same data the kernel checked) and computes, for every
+declaration in `PolyFun.*` modules, the set of axioms its statement and proof ultimately
+depend on — the same information as `#print axioms`, for the whole library at once.
+
+Because this reads elaborated `.olean` data rather than source text, it sees exactly what
+the kernel accepted: private declarations and instances are reported, compiler-generated
+auxiliaries are traversed (their taint surfaces on the parent declaration), and no
+source-level heuristics are involved. The sweep covers what the root modules transitively
+import — pair it with the repo's import-completeness gate so every
+source file is actually in scope; an unimported file is invisible to any kernel-level
+census.
+
+Known blind spots, shared with `#print axioms` (all environment-walking tools):
+* structure-field **default values** and autoparams (`:= by sorry`) are re-elaborated at
+  each use site and attach to no swept constant of the defining module;
+* `example`s never enter the environment;
+* files not transitively imported by the swept roots are invisible (pair with the repo's
+  import-completeness gate).
+A source-level `sorry` grep is the complementary check for the first two.
+
+Modes (run after `lake build`):
+
+```
+lake exe axiomsweep                     # summary only
+lake exe axiomsweep --out report.json   # also write the full per-declaration report
+lake exe axiomsweep --check             # gate against scripts/axiom_baseline.json
+lake exe axiomsweep --update-baseline   # reset the baseline after all taint is removed
+```
+
+The committed baseline (`scripts/axiom_baseline.json`) is an explicit, machine-checked
+zero-debt policy: both arrays must remain empty. `--check` fails on every declaration
+that depends on `sorryAx` or a non-standard axiom (anything beyond `propext`,
+`Classical.choice`, and `Quot.sound`). Native trust axioms surface here too:
+`native_decide`-style tactics mint per-declaration
+`…._native.<tactic>.ax_<number>_<number>` axioms, recorded under their owning
+declaration. `--update-baseline` can clear stale debt after the build becomes clean, but
+refuses to write a nonempty baseline. It cannot pre-authorize future taint.
+-/
+
+open Lean
+
+namespace AxiomSweep
+
+/-- Root modules swept when no `--root` is given. -/
+def defaultRoots : Array Name := #[`PolyFun]
+
+/-- Axioms that carry no extra trust assumptions beyond Lean's standard foundation. -/
+def standardAxioms : List Name := [``propext, ``Classical.choice, ``Quot.sound]
+
+/-- Phase 1: DFS. Compute, for every constant reachable from the work list, an
+under-approximation of the set of axioms it transitively depends on, memoised across
+roots via `memo`. Also records the finalisation order — a topological order of the
+dependency graph except inside mutual-inductive cycles.
+
+`gray` marks constants whose dependencies are still being expanded. Back-edges (cycles,
+which the kernel only permits inside mutual inductive families) contribute nothing in
+this phase; `repair` below propagates to the true fixpoint. An axiom contributes itself
+plus anything reachable through its *type* (matching Lean's own `CollectAxioms`). -/
+partial def collect (env : Environment) (stack : List Name) (gray : Std.HashSet Name)
+    (memo : Std.HashMap Name (Array Name)) (order : Array Name) :
+    Std.HashMap Name (Array Name) × Array Name :=
+  match stack with
+  | [] => (memo, order)
+  | n :: rest =>
+    if memo.contains n then
+      collect env rest gray memo order
+    else match env.find? n with
+      | none => collect env rest gray (memo.insert n #[]) order
+      | some ci =>
+        let deps := ci.getUsedConstantsAsSet.toList
+        if gray.contains n then
+          let seed : Array Name := if ci matches .axiomInfo _ then #[n] else #[]
+          let axs := deps.foldl (init := seed) fun acc d =>
+            match memo[d]? with
+            | some as => as.foldl (init := acc) fun acc a =>
+                if acc.contains a then acc else acc.push a
+            | none => acc
+          collect env rest gray (memo.insert n axs) (order.push n)
+        else
+          let pending := deps.filter fun d => !memo.contains d && !gray.contains d
+          collect env (pending ++ stack) (gray.insert n) memo order
+
+/-- Phase 2: propagate to fixpoint. The DFS under-approximates inside mutual-inductive
+cycles (a member's taint may not reach its siblings), and — because `memo` persists
+across roots — anything finalised after reading such a member inherits the error.
+Re-deriving every set in finalisation order until nothing changes computes the least
+fixpoint of the closure equations: the true kernel-level axiom dependency set. This is
+strictly more accurate than `#print axioms`, whose `CollectAxioms` has the same
+mutual-family blind spot this phase repairs. Sets grow monotonically and are bounded,
+so termination is immediate; in practice one or two passes suffice. -/
+partial def repair (env : Environment) (order : Array Name)
+    (memo : Std.HashMap Name (Array Name)) : Std.HashMap Name (Array Name) :=
+  let (memo', changed) := order.foldl (init := (memo, false)) fun (memo, changed) n =>
+    match env.find? n with
+    | none => (memo, changed)
+    | some ci =>
+      let deps := ci.getUsedConstantsAsSet.toList
+      let seed : Array Name := if ci matches .axiomInfo _ then #[n] else #[]
+      let axs := deps.foldl (init := seed) fun acc d =>
+        match memo[d]? with
+        | some as => as.foldl (init := acc) fun acc a =>
+            if acc.contains a then acc else acc.push a
+        | none => acc
+      let old := (memo[n]?.getD #[]).size
+      if axs.size == old then (memo, changed)
+      else (memo.insert n axs, true)
+  if changed then repair env order memo' else memo'
+
+/-- One row of the per-declaration report. -/
+structure Entry where
+  name : String
+  module : String
+  kind : String
+  line : Option Nat
+  axioms : Array String
+  deriving ToJson
+
+/-- A declaration depending on axioms beyond the standard foundation (and `sorryAx`,
+which is tracked separately). -/
+structure NonstandardEntry where
+  name : String
+  axioms : Array String
+  deriving FromJson, ToJson
+
+/-- The committed regression baseline. -/
+structure Baseline where
+  «sorry» : Array String
+  nonstandard : Array NonstandardEntry
+  deriving FromJson, ToJson
+
+/-- Whether `s` is a nonempty string of ASCII decimal digits. -/
+def isDecimal (s : String) : Bool :=
+  !s.isEmpty && s.toList.all fun c => '0' ≤ c && c ≤ '9'
+
+/-- Collapse exactly the generated counter suffix of native trust axioms
+(`Foo._native.native_decide.ax_1_1` → `Foo._native.native_decide`). Names that merely
+contain `._native.` or resemble a generated suffix are preserved. -/
+def normalizeAxiomName (s : String) : String :=
+  match s.splitOn "._native." with
+  | [owner, tail] =>
+    match tail.splitOn "." with
+    | [tactic, counter] =>
+      match counter.splitOn "_" with
+      | ["ax", major, minor] =>
+        if !owner.isEmpty && !tactic.isEmpty && isDecimal major && isDecimal minor then
+          owner ++ "._native." ++ tactic
+        else
+          s
+      | _ => s
+    | _ => s
+  | _ => s
+
+/-- Sort and deduplicate (normalisation can identify adjacent names). -/
+def dedupSort (a : Array String) : Array String :=
+  (a.qsort (· < ·)).foldl (init := #[]) fun acc x =>
+    if acc.back? == some x then acc else acc.push x
+
+def kindOf : ConstantInfo → String
+  | .axiomInfo _ => "axiom"
+  | .defnInfo _ => "def"
+  | .thmInfo _ => "theorem"
+  | .opaqueInfo _ => "opaque"
+  | .quotInfo _ => "quot"
+  | .inductInfo _ => "inductive"
+  | .ctorInfo _ => "constructor"
+  | .recInfo _ => "recursor"
+
+/-- Whether to report a constant: skip compiler-internal auxiliaries (`_proof_*`,
+`match_*`, numbered equation lemmas, …), whose axiom footprint is inherited by their
+parent declaration, but keep `private` declarations (checked under their user-facing
+name, since the `_private` mangling would otherwise look internal). On-demand aux
+lemmas with symbolic names (`.eq_def`, `.congr_simp`) are reported. -/
+def isReportable (n : Name) : Bool :=
+  !n.hasMacroScopes && !((privateToUserName? n).getD n).isInternalDetail
+
+/-- Enumerate the reportable declarations of every module under one of `roots` and
+compute their axiom closures. -/
+def buildEntries (roots : Array Name) : CoreM (Array Entry × Nat) := do
+  let env ← getEnv
+  let mut targets : Array (Name × Name) := #[]
+  let mut seen : Std.HashSet Name := {}
+  let mut moduleCount := 0
+  for (mname, mdata) in env.header.moduleNames.zip env.header.moduleData do
+    if roots.any (·.isPrefixOf mname) then
+      moduleCount := moduleCount + 1
+      for c in mdata.constNames do
+        -- A realised constant (e.g. `.congr_simp`) can appear in several modules'
+        -- `constNames`; report it once, under the first module that carries it.
+        if isReportable c && !seen.contains c then
+          seen := seen.insert c
+          targets := targets.push (c, mname)
+  let (memo0, order) :=
+    targets.foldl (init := (({} : Std.HashMap Name (Array Name)), (#[] : Array Name)))
+      fun (memo, order) (c, _) => collect env [c] {} memo order
+  let memo := repair env order memo0
+  let mut entries : Array Entry := #[]
+  for (c, mname) in targets do
+    let some ci := env.find? c | continue
+    let line := (← findDeclarationRanges? c).map (·.range.pos.line)
+    entries := entries.push {
+      name := c.toString
+      module := mname.toString
+      kind := kindOf ci
+      line := line
+      axioms := dedupSort ((memo[c]?.getD #[]).map (normalizeAxiomName ·.toString)) }
+  return (entries.qsort (fun a b => a.name < b.name), moduleCount)
+
+def isStandard (a : String) : Bool :=
+  standardAxioms.any (toString · == a)
+
+def sorryAxName : String := "sorryAx"
+
+/-- Non-standard axioms of an entry: everything beyond the standard foundation, with
+`sorryAx` tracked separately. -/
+def nonstandardOf (e : Entry) : Array String :=
+  e.axioms.filter fun a => !isStandard a && a != sorryAxName
+
+/-- Project the current build's taint sets into baseline form (deterministically
+sorted, since `entries` is sorted by name). -/
+def currentBaseline (entries : Array Entry) : Baseline where
+  «sorry» := (entries.filter (·.axioms.contains sorryAxName)).map (·.name)
+  nonstandard := entries.filterMap fun e =>
+    let bad := nonstandardOf e
+    if bad.isEmpty then none else some { name := e.name, axioms := bad }
+
+/-- Read and validate the committed zero-debt baseline. A nonempty baseline is a policy
+error rather than an allowlist: PolyFun does not carry accepted axiom or `sorry` debt. -/
+def readZeroBaseline (basePath : String) : IO (Except UInt32 Baseline) := do
+  if !(← System.FilePath.pathExists basePath) then
+    IO.eprintln s!"axiomsweep: baseline {basePath} not found"
+    return .error 2
+  let base ← match Json.parse (← IO.FS.readFile basePath) >>= fromJson? (α := Baseline) with
+    | .ok b => pure b
+    | .error e =>
+      IO.eprintln s!"axiomsweep: cannot parse baseline {basePath}: {e}"
+      return .error 2
+  if !base.«sorry».isEmpty || !base.nonstandard.isEmpty then
+    IO.eprintln s!"axiomsweep: baseline {basePath} is nonempty; PolyFun's zero-debt \
+      policy forbids allowlisting axiom or sorry taint"
+    return .error 2
+  return .ok base
+
+/-- Check the current taint sets against PolyFun's zero-debt policy. Returns exit code
+`1` for a taint finding and `2` for a missing, malformed, or nonempty baseline. -/
+def runCheck (cur : Baseline) (basePath : String) : IO UInt32 := do
+  if let .error code ← readZeroBaseline basePath then return code
+  if !cur.«sorry».isEmpty then
+    IO.eprintln s!"axiomsweep: {cur.«sorry».size} declaration(s) depend on sorryAx:"
+    for n in cur.«sorry» do IO.eprintln s!"  {n}"
+  if !cur.nonstandard.isEmpty then
+    IO.eprintln s!"axiomsweep: {cur.nonstandard.size} declaration(s) depend on \
+      non-standard axioms:"
+    for e in cur.nonstandard do IO.eprintln s!"  {e.name} : {e.axioms}"
+  if !cur.«sorry».isEmpty || !cur.nonstandard.isEmpty then
+    IO.eprintln "axiomsweep: check failed; remove all axiom and sorry taint"
+    return 1
+  IO.println "axiomsweep: check passed (zero axiom/sorry taint)."
+  return 0
+
+/-- Write the canonical empty baseline, but only after the current sweep is clean. -/
+def runUpdate (cur : Baseline) (basePath : String) : IO UInt32 := do
+  if !cur.«sorry».isEmpty || !cur.nonstandard.isEmpty then
+    IO.eprintln "axiomsweep: refusing to update the baseline while axiom or sorry taint exists"
+    return 1
+  IO.FS.writeFile basePath ((toJson cur).pretty ++ "\n")
+  IO.println s!"axiomsweep: wrote zero-debt baseline to {basePath}"
+  return 0
+
+structure Config where
+  roots : Array Name := #[]
+  out? : Option String := none
+  check : Bool := false
+  update : Bool := false
+  baseline : String := "scripts/axiom_baseline.json"
+
+def parseArgs : List String → Config → Except String Config
+  | [], cfg => .ok cfg
+  | "--check" :: rest, cfg => parseArgs rest { cfg with check := true }
+  | "--update-baseline" :: rest, cfg => parseArgs rest { cfg with update := true }
+  | "--out" :: path :: rest, cfg => parseArgs rest { cfg with out? := some path }
+  | "--baseline" :: path :: rest, cfg => parseArgs rest { cfg with baseline := path }
+  | "--root" :: mod :: rest, cfg =>
+    parseArgs rest { cfg with roots := cfg.roots.push mod.toName }
+  | arg :: _, _ => .error s!"axiomsweep: unknown or incomplete argument: {arg}\n\
+      usage: lake exe axiomsweep [--out FILE] [--check] [--update-baseline] \
+      [--baseline FILE] [--root MOD]*\n      (--check and --update-baseline are mutually exclusive)"
+
+end AxiomSweep
+
+open AxiomSweep in
+unsafe def main (args : List String) : IO UInt32 := do
+  let cfg ← match parseArgs args {} with
+    | .ok cfg => pure cfg
+    | .error e => IO.eprintln e; return 2
+  if cfg.check && cfg.update then
+    IO.eprintln "axiomsweep: --check and --update-baseline are mutually exclusive"
+    return 2
+  let roots := if cfg.roots.isEmpty then defaultRoots else cfg.roots
+  initSearchPath (← findSysroot)
+  enableInitializersExecution
+  let env ← try
+      importModules (roots.map ({ module := · })) {} (trustLevel := 1024)
+        (loadExts := true)
+    catch e =>
+      IO.eprintln s!"axiomsweep: cannot import root modules {roots}: {e.toString}\n\
+        (roots must be importable modules — glob-based libs without an umbrella \
+        module cannot be swept by library name)"
+      return (2 : UInt32)
+  let ((entries, moduleCount), _) ← (buildEntries roots).toIO
+    { fileName := "<axiomsweep>", fileMap := default } { env }
+  let cur := currentBaseline entries
+  let distinctNonstd := cur.nonstandard.foldl (init := (#[] : Array String)) fun acc e =>
+    e.axioms.foldl (init := acc) fun acc a => if acc.contains a then acc else acc.push a
+  IO.println s!"axiomsweep: {entries.size} declarations across {moduleCount} modules \
+    under {roots}"
+  IO.println s!"  sorryAx-tainted: {cur.«sorry».size}"
+  IO.println s!"  non-standard-axiom-tainted: {cur.nonstandard.size} \
+    (axioms: {distinctNonstd})"
+  if let some out := cfg.out? then
+    let report := Json.mkObj [
+      ("roots", toJson (roots.map (·.toString))),
+      ("declarationCount", toJson entries.size),
+      ("declarations", toJson entries)]
+    IO.FS.writeFile out (report.pretty ++ "\n")
+    IO.println s!"axiomsweep: wrote report to {out}"
+  if cfg.update then
+    return (← runUpdate cur cfg.baseline)
+  if cfg.check then
+    return (← runCheck cur cfg.baseline)
+  return 0
diff --git a/scripts/AxiomSweepTestFixtures/Clean.lean b/scripts/AxiomSweepTestFixtures/Clean.lean
new file mode 100644
index 0000000..72e76a8
--- /dev/null
+++ b/scripts/AxiomSweepTestFixtures/Clean.lean
@@ -0,0 +1,18 @@
+/-
+Copyright (c) 2026 PolyFun Contributors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Quang Dao
+-/
+module
+
+/-! # Clean executable fixture for axiomsweep -/
+
+public section
+
+namespace AxiomSweepTestFixtures.Clean
+
+def base : Nat := 7
+
+def transitive : Nat := base + 1
+
+end AxiomSweepTestFixtures.Clean
diff --git a/scripts/AxiomSweepTestFixtures/Tainted.lean b/scripts/AxiomSweepTestFixtures/Tainted.lean
new file mode 100644
index 0000000..00c7407
--- /dev/null
+++ b/scripts/AxiomSweepTestFixtures/Tainted.lean
@@ -0,0 +1,13 @@
+/-
+Copyright (c) 2026 PolyFun Contributors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Quang Dao
+-/
+module
+
+import AxiomSweepTestFixtures.Tainted.AxiomInType
+import AxiomSweepTestFixtures.Tainted.DirectSorry
+import AxiomSweepTestFixtures.Tainted.Mutual
+import AxiomSweepTestFixtures.Tainted.NativeNames
+
+/-! # Imported taint fixture root for axiomsweep -/
diff --git a/scripts/AxiomSweepTestFixtures/Tainted/AxiomInType.lean b/scripts/AxiomSweepTestFixtures/Tainted/AxiomInType.lean
new file mode 100644
index 0000000..3ff0bbb
--- /dev/null
+++ b/scripts/AxiomSweepTestFixtures/Tainted/AxiomInType.lean
@@ -0,0 +1,18 @@
+/-
+Copyright (c) 2026 PolyFun Contributors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Quang Dao
+-/
+module
+
+/-! # Axiom-in-type fixture for axiomsweep -/
+
+public section
+
+namespace AxiomSweepTestFixtures.Tainted
+
+axiom typeIndex : Nat
+
+axiom axiomInType : Fin (typeIndex + 1)
+
+end AxiomSweepTestFixtures.Tainted
diff --git a/scripts/AxiomSweepTestFixtures/Tainted/DirectSorry.lean b/scripts/AxiomSweepTestFixtures/Tainted/DirectSorry.lean
new file mode 100644
index 0000000..5859b6d
--- /dev/null
+++ b/scripts/AxiomSweepTestFixtures/Tainted/DirectSorry.lean
@@ -0,0 +1,18 @@
+/-
+Copyright (c) 2026 PolyFun Contributors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Quang Dao
+-/
+module
+
+/-! # Direct and transitive `sorryAx` fixtures for axiomsweep -/
+
+public section
+
+namespace AxiomSweepTestFixtures.Tainted
+
+opaque directSorry : Nat := sorryAx Nat true
+
+def transitiveSorry : Nat := directSorry
+
+end AxiomSweepTestFixtures.Tainted
diff --git a/scripts/AxiomSweepTestFixtures/Tainted/Mutual.lean b/scripts/AxiomSweepTestFixtures/Tainted/Mutual.lean
new file mode 100644
index 0000000..f449ded
--- /dev/null
+++ b/scripts/AxiomSweepTestFixtures/Tainted/Mutual.lean
@@ -0,0 +1,25 @@
+/-
+Copyright (c) 2026 PolyFun Contributors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Quang Dao
+-/
+module
+
+/-! # Mutual-inductive fixpoint fixture for axiomsweep -/
+
+public section
+
+namespace AxiomSweepTestFixtures.Tainted
+
+axiom mutualAxiom : True
+
+mutual
+  inductive MutualLeft : Type where
+    | fromRight : MutualRight → MutualLeft
+    | tainted : True.intro = mutualAxiom → MutualLeft
+
+  inductive MutualRight : Type where
+    | fromLeft : MutualLeft → MutualRight
+end
+
+end AxiomSweepTestFixtures.Tainted
diff --git a/scripts/AxiomSweepTestFixtures/Tainted/NativeNames.lean b/scripts/AxiomSweepTestFixtures/Tainted/NativeNames.lean
new file mode 100644
index 0000000..681b7b2
--- /dev/null
+++ b/scripts/AxiomSweepTestFixtures/Tainted/NativeNames.lean
@@ -0,0 +1,42 @@
+/-
+Copyright (c) 2026 PolyFun Contributors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Quang Dao
+-/
+module
+
+/-! # Native-axiom name-normalization fixtures for axiomsweep -/
+
+public section
+
+namespace AxiomSweepTestFixtures.Tainted.Generated._native.native_decide
+
+axiom ax_12_34 : True
+
+end AxiomSweepTestFixtures.Tainted.Generated._native.native_decide
+
+namespace AxiomSweepTestFixtures.Tainted.Collision._native.native_decide
+
+axiom ax_12_extra : True
+axiom ax_x_34 : True
+
+namespace ax_12_34
+
+axiom extra : True
+
+end ax_12_34
+
+end AxiomSweepTestFixtures.Tainted.Collision._native.native_decide
+
+namespace AxiomSweepTestFixtures.Tainted
+
+theorem generatedNativeUser : True := Generated._native.native_decide.ax_12_34
+
+theorem collisionUser : True := Collision._native.native_decide.ax_12_extra
+
+theorem collisionNondecimalUser : True := Collision._native.native_decide.ax_x_34
+
+theorem collisionExtraSegmentUser : True :=
+  Collision._native.native_decide.ax_12_34.extra
+
+end AxiomSweepTestFixtures.Tainted
diff --git a/scripts/AxiomSweepTestFixtures/Unimported.lean b/scripts/AxiomSweepTestFixtures/Unimported.lean
new file mode 100644
index 0000000..602a573
--- /dev/null
+++ b/scripts/AxiomSweepTestFixtures/Unimported.lean
@@ -0,0 +1,16 @@
+/-
+Copyright (c) 2026 PolyFun Contributors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Quang Dao
+-/
+module
+
+/-! # Deliberately unimported `sorryAx` fixture for axiomsweep -/
+
+public section
+
+namespace AxiomSweepTestFixtures.Unimported
+
+opaque hiddenSorry : Nat := sorryAx Nat true
+
+end AxiomSweepTestFixtures.Unimported
diff --git a/scripts/axiom_baseline.json b/scripts/axiom_baseline.json
new file mode 100644
index 0000000..ffa44b2
--- /dev/null
+++ b/scripts/axiom_baseline.json
@@ -0,0 +1 @@
+{"sorry": [], "nonstandard": []}
diff --git a/scripts/test-axiomsweep.sh b/scripts/test-axiomsweep.sh
new file mode 100755
index 0000000..a9a39a5
--- /dev/null
+++ b/scripts/test-axiomsweep.sh
@@ -0,0 +1,134 @@
+#!/usr/bin/env bash
+
+# Execute falsifiable fixtures for the kernel-level axiom sweep.
+
+set -euo pipefail
+
+REPO_ROOT="$(git rev-parse --show-toplevel)"
+cd "$REPO_ROOT"
+
+FIXTURE_TMP="$(mktemp -d "${TMPDIR:-/tmp}/polyfun-axiomsweep.XXXXXX")"
+trap 'rm -rf -- "$FIXTURE_TMP"' EXIT
+
+expect_status() {
+  local expected="$1"
+  local label="$2"
+  shift 2
+  local log="$FIXTURE_TMP/${label}.log"
+  local actual=0
+  "$@" >"$log" 2>&1 || actual=$?
+  if [[ "$actual" -ne "$expected" ]]; then
+    echo "ERROR: $label returned $actual; expected $expected" >&2
+    sed -n '1,160p' "$log" >&2
+    return 1
+  fi
+}
+
+EMPTY_BASELINE="$FIXTURE_TMP/empty.json"
+NONEMPTY_BASELINE="$FIXTURE_TMP/nonempty.json"
+INVALID_BASELINE="$FIXTURE_TMP/invalid.json"
+MISSING_BASELINE="$FIXTURE_TMP/missing.json"
+CLEAN_REPORT="$FIXTURE_TMP/clean.json"
+TAINTED_REPORT="$FIXTURE_TMP/tainted.json"
+TAINTED_REPORT_2="$FIXTURE_TMP/tainted-2.json"
+UNIMPORTED_REPORT="$FIXTURE_TMP/unimported.json"
+
+printf '{"sorry": [], "nonstandard": []}\n' >"$EMPTY_BASELINE"
+printf '{"sorry": ["preauthorized.future"], "nonstandard": []}\n' >"$NONEMPTY_BASELINE"
+printf '{not-json}\n' >"$INVALID_BASELINE"
+
+lake build AxiomSweepTestFixtures
+lake exe axiomsweep --root AxiomSweepTestFixtures.Clean --out "$CLEAN_REPORT"
+lake exe axiomsweep --root AxiomSweepTestFixtures.Tainted --out "$TAINTED_REPORT"
+lake exe axiomsweep --root AxiomSweepTestFixtures.Tainted --out "$TAINTED_REPORT_2"
+lake exe axiomsweep --root AxiomSweepTestFixtures.Unimported --out "$UNIMPORTED_REPORT"
+
+cmp "$TAINTED_REPORT" "$TAINTED_REPORT_2"
+
+python3 - "$CLEAN_REPORT" "$TAINTED_REPORT" "$UNIMPORTED_REPORT" <<'PY'
+import json
+import sys
+
+clean_path, tainted_path, unimported_path = sys.argv[1:]
+
+with open(clean_path, encoding="utf-8") as stream:
+    clean = json.load(stream)
+with open(tainted_path, encoding="utf-8") as stream:
+    tainted = json.load(stream)
+with open(unimported_path, encoding="utf-8") as stream:
+    unimported = json.load(stream)
+
+clean_entries = {entry["name"]: entry for entry in clean["declarations"]}
+tainted_entries = {entry["name"]: entry for entry in tainted["declarations"]}
+unimported_entries = {entry["name"]: entry for entry in unimported["declarations"]}
+
+assert clean_entries
+assert all(not entry["axioms"] for entry in clean_entries.values())
+
+prefix = "AxiomSweepTestFixtures.Tainted."
+direct = tainted_entries[prefix + "directSorry"]["axioms"]
+transitive = tainted_entries[prefix + "transitiveSorry"]["axioms"]
+assert "sorryAx" in direct
+assert "sorryAx" in transitive
+
+axiom_in_type = tainted_entries[prefix + "axiomInType"]["axioms"]
+assert prefix + "typeIndex" in axiom_in_type
+
+mutual_right = tainted_entries[prefix + "MutualRight"]["axioms"]
+assert prefix + "mutualAxiom" in mutual_right
+
+all_axioms = {
+    axiom
+    for entry in tainted_entries.values()
+    for axiom in entry["axioms"]
+}
+generated = prefix + "Generated._native.native_decide"
+generated_raw = generated + ".ax_12_34"
+assert generated in all_axioms
+assert generated_raw not in all_axioms
+assert prefix + "Collision._native.native_decide.ax_12_extra" in all_axioms
+assert prefix + "Collision._native.native_decide.ax_x_34" in all_axioms
+assert prefix + "Collision._native.native_decide.ax_12_34.extra" in all_axioms
+
+hidden = "AxiomSweepTestFixtures.Unimported.hiddenSorry"
+assert hidden not in tainted_entries
+assert hidden in unimported_entries
+assert "sorryAx" in unimported_entries[hidden]["axioms"]
+PY
+
+expect_status 0 clean-check \
+  lake exe axiomsweep --root AxiomSweepTestFixtures.Clean \
+    --check --baseline "$EMPTY_BASELINE"
+expect_status 1 tainted-check \
+  lake exe axiomsweep --root AxiomSweepTestFixtures.Tainted \
+    --check --baseline "$EMPTY_BASELINE"
+expect_status 2 preauthorized-taint \
+  lake exe axiomsweep --root AxiomSweepTestFixtures.Tainted \
+    --check --baseline "$NONEMPTY_BASELINE"
+expect_status 2 stale-debt \
+  lake exe axiomsweep --root AxiomSweepTestFixtures.Clean \
+    --check --baseline "$NONEMPTY_BASELINE"
+expect_status 2 missing-baseline \
+  lake exe axiomsweep --root AxiomSweepTestFixtures.Clean \
+    --check --baseline "$MISSING_BASELINE"
+expect_status 2 invalid-baseline \
+  lake exe axiomsweep --root AxiomSweepTestFixtures.Clean \
+    --check --baseline "$INVALID_BASELINE"
+expect_status 2 conflicting-flags \
+  lake exe axiomsweep --root AxiomSweepTestFixtures.Clean \
+    --check --update-baseline --baseline "$EMPTY_BASELINE"
+
+cp "$NONEMPTY_BASELINE" "$FIXTURE_TMP/shrink.json"
+expect_status 0 shrink-baseline \
+  lake exe axiomsweep --root AxiomSweepTestFixtures.Clean \
+    --update-baseline --baseline "$FIXTURE_TMP/shrink.json"
+cmp "$EMPTY_BASELINE" "$FIXTURE_TMP/shrink.json"
+
+cp "$EMPTY_BASELINE" "$FIXTURE_TMP/growth.json"
+cp "$FIXTURE_TMP/growth.json" "$FIXTURE_TMP/growth-before.json"
+expect_status 1 reject-baseline-growth \
+  lake exe axiomsweep --root AxiomSweepTestFixtures.Tainted \
+    --update-baseline --baseline "$FIXTURE_TMP/growth.json"
+cmp "$FIXTURE_TMP/growth-before.json" "$FIXTURE_TMP/growth.json"
+
+echo "✓ Axiom sweep executable fixture matrix passed."
diff --git a/scripts/validate.sh b/scripts/validate.sh
index 46efcd0..d1368a2 100755
--- a/scripts/validate.sh
+++ b/scripts/validate.sh
@@ -9,10 +9,11 @@ cd "$REPO_ROOT"
 
 run_lint=0
 run_test=0
+run_axioms=0
 
 usage() {
   cat <<'EOF'
-Usage: ./scripts/validate.sh [--lint] [--test]
+Usage: ./scripts/validate.sh [--lint] [--test] [--axioms]
 
 Default checks:
   - lake build
@@ -21,8 +22,9 @@ Default checks:
   - python3 ./scripts/check-docs-integrity.py
 
 Optional checks:
-  --lint   Run `lake lint` (Batteries environment linters)
-  --test   Run `lake test` (builds the PolyFunTest library)
+  --lint    Run `lake lint` (Batteries environment linters)
+  --test    Run `lake test` (builds the PolyFunTest library)
+  --axioms  Test axiomsweep, then enforce the zero axiom/sorry-debt gate
 EOF
 }
 
@@ -34,6 +36,9 @@ for arg in "$@"; do
     --test)
       run_test=1
       ;;
+    --axioms)
+      run_axioms=1
+      ;;
     -h|--help)
       usage
       exit 0
@@ -73,5 +78,15 @@ if (( run_test )); then
   lake test
 fi
 
+if (( run_axioms )); then
+  echo ""
+  echo "# Testing the axiom sweep tool"
+  ./scripts/test-axiomsweep.sh
+
+  echo ""
+  echo "# Enforcing zero axiom/sorry debt"
+  lake exe axiomsweep --check
+fi
+
 echo ""
 echo "All requested validation checks passed."