diff --git a/verification/HARNESS.sha256 b/verification/HARNESS.sha256
index 4cf362f..0b87ac1 100644
--- a/verification/HARNESS.sha256
+++ b/verification/HARNESS.sha256
@@ -1,6 +1,6 @@
 6c821b8e465d3b394cb3cbb4bb3757791ace064b6d1b273ba9a41402dac74e24  AUDIT-MANIFEST.txt
 d505e4dd9283673e78fb34e25780c94334e03de4ad20400f8289d594ab004daf  check-scalar.sh
-785b290842e43f053eaaf977b190c208ed3f96a146b20783ad3c3565d9d62c01  check.sh
+0c0ee439fd5c907719478b08c73f8fc62fc5147b90c87baadf53f1301da2037e  check.sh
 71244d824847311bcb3ba8ad1f1905c4b24fe8f015e3230969914019cb628b61  extract.sh
 c9672a28825cd1d4055fb9efbb4a1d94c921c7b5c79e4cd5d0626ba061e554c1  GEN-MODEL.sha256
 e6f31b4303f5a344781d353f1dddefc185876df470e27b285c81556621e65c05  inventory-allowlist-scalar.txt
@@ -10,8 +10,8 @@ e6f31b4303f5a344781d353f1dddefc185876df470e27b285c81556621e65c05  inventory-allo
 fde2e987a9f69cb9f39b18ab8b405d73db4d9abee9f714f8be993a40ef617c03  model-correspondence.py
 ceebf2872eac57ebe2d61d00258ea3d367d263b6c6ebfaae1eede92ef3d478a2  MODEL-CORRESPONDENCE.txt
 772ca6dd22443c83dc35d5428598c8d17a01c69db5be008474d06476fa66f7f8  Proofs/Audit.lean
-84bc670991fd7456d8c8569ff7b7c32410513a63d3cb7fe8877bb19a82d36a7d  Proofs/InventoryCore.lean
-4b1d7f5249a80375b4ef849a760ae8e4bbcecf103c3f8b9e8d0a5d5a9ae377fc  Proofs/Inventory.lean
+859dcb7fcef13e8b49a8b36a496f46e9fc56448410d3bde16c78361215f4bc19  Proofs/InventoryCore.lean
+660d35343f5673d4bc854787b6a34063c956567bd7e2eb62955a92e3c55bfa6b  Proofs/Inventory.lean
 6fbeb50d3951c7c5ac593f6dec91096fc798123ed0c500fdfa39fb20b118ea78  Proofs/InventoryScalar.lean
 bf71e8d4eb312ebc687bf7e218d90b910543cd92e782078174868d012aca7250  selftest-auditonly.sh
 eb81df6d154b413b243ad282e3b1bfec92fde158a215f89993c08586a121f171  selftest-axgate.sh
diff --git a/verification/Proofs/Inventory.lean b/verification/Proofs/Inventory.lean
index 1d71ca4..67e87ed 100644
--- a/verification/Proofs/Inventory.lean
+++ b/verification/Proofs/Inventory.lean
@@ -10,6 +10,7 @@
    a split is needed was determined by compiling a probe, per repo.
    ────────────────────────────────────────────────────────────────────────── -/
 import Proofs.InventoryCore
+import Proofs.Audit
 import Proofs.Denote
 import Proofs.P25519
 import Proofs.ReduceSpec
@@ -67,4 +68,11 @@ def corpus : Array Name :=
    `Proofs.SigApexSpec, `Proofs.PointLiftSpec, `Proofs.PointEqSpec,
    `Proofs.DecompressSpec, `Proofs.FromBytesSpec, `Proofs.DecompressMain]
 
+-- The instruments. `Proofs.Audit` is the statement-binding driver: a member of
+-- check.sh's compile manifest that was enumerated by NOTHING until 2026-07-31.
+-- This module has no index while it is being elaborated, so `emitDrivers` picks
+-- its own declarations up as the ones with no originating module.
+def drivers : Array Name := #[`Proofs.InventoryCore, `Proofs.Audit]
+
 #eval show MetaM Unit from emitInventory corpus
+#eval show MetaM Unit from emitDrivers drivers
diff --git a/verification/Proofs/InventoryCore.lean b/verification/Proofs/InventoryCore.lean
index e872017..0d8b2ee 100644
--- a/verification/Proofs/InventoryCore.lean
+++ b/verification/Proofs/InventoryCore.lean
@@ -107,4 +107,64 @@ def emitInventory (corpus : Array Name) : MetaM Unit := do
   -- received, in both directions.
   IO.println s!"INV-COUNT|{sorted.size}"
 
+/-- THE INSTRUMENTS' OWN SURFACE.
+
+    `emitInventory` walks the CORPUS. It says nothing about the modules that
+    perform the audit, and until 2026-07-31 nothing else enumerated them either:
+    the kernel counted 3058 declarations across this button's 43 modules while
+    the inventory accounted for 3022, and the 36-declaration difference — the
+    drivers' own machinery — was covered by no allowlist row.
+
+    That difference was never a soundness hole. The drivers ARE members of
+    check.sh's compile manifest, so Phase 2b's kernel-side gate reads their
+    `.olean`s and an axiom in one is rejected whatever its indentation. What was
+    missing is the weaker but still real property: that an instrument declares
+    nothing but inert machinery, and that every declaration the kernel sees is
+    ACCOUNTED FOR by exactly one of the two walks.
+
+    The policy is not "declare nothing" — these files legitimately declare their
+    own functions. It is that an instrument may not declare an AXIOM (which
+    would widen the trusted base outside every cone) nor a standalone CLAIM
+    (which no certificate covers and no allowlist pins). A theorem whose name
+    extends a constant declared alongside it is an artefact the elaborator
+    generated for a definition — well-founded recursion emits these — and is
+    allowed; a theorem whose parent is not a declared constant is not. -/
+def emitDrivers (drivers : Array Name) : MetaM Unit := do
+  let env ← getEnv
+  let mut idxs : Array Nat := #[]
+  for m in drivers do
+    match env.getModuleIdx? m with
+    | some i => idxs := idxs.push i
+    | none   => throwError "DRIVER SURFACE ERROR: driver module {m} is not imported"
+  -- Two passes: collect the names first, so the artefact test can ask whether a
+  -- theorem's parent is itself declared by an instrument.
+  let mut names : Std.HashSet Name := {}
+  let mut here : Array (Name × ConstantInfo) := #[]
+  for (n, ci) in env.constants.toList do
+    let mine : Bool :=
+      match env.getModuleIdxFor? n with
+      | some i => idxs.contains i
+      | none   => true   -- declared by the module being elaborated: this driver
+    if mine then
+      names := names.insert n
+      here := here.push (n, ci)
+  let mut lines : Array String := #[]
+  for (n, ci) in here do
+    let k := kindOf ci
+    if k == "axiom" then
+      throwError "DRIVER SURFACE VIOLATION: {n} is an axiom declared by the audit \
+                  infrastructure. An instrument may not widen the trusted base."
+    if k == "theorem" && !names.contains n.getPrefix then
+      throwError "DRIVER SURFACE VIOLATION: {n} is a standalone theorem declared by \
+                  the audit infrastructure. An instrument may declare definitions \
+                  and whatever the elaborator generates for them — never a claim \
+                  of its own."
+    lines := lines.push s!"DRV|{n}|{k}"
+  let sorted := lines.qsort (· < ·)
+  for l in sorted do
+    IO.println l
+  IO.println s!"DRV-COUNT|{sorted.size}"
+
+
+
 end Ed25519Inventory
diff --git a/verification/check.sh b/verification/check.sh
index 62955c6..ef3ac87 100755
--- a/verification/check.sh
+++ b/verification/check.sh
@@ -589,6 +589,7 @@ run_cmd do
   let mut errs : Array String := #[]
   let mut nMod := 0
   let mut nConst := 0
+  let mut seen : Std.HashSet Name := {}
   for name in expected do
     let p := dir / name
     -- FAIL CLOSED ON ABSENCE: a manifest module whose artifact is missing makes
@@ -599,6 +600,7 @@ run_cmd do
     let (mod, _) ← readModuleData p
     for ci in mod.constants do
       nConst := nConst + 1
+      seen := seen.insert ci.name
       if ci matches .axiomInfo _ then
         errs := errs.push s!"  {name}: {ci.name}"
   unless errs.isEmpty do
@@ -607,6 +609,7 @@ run_cmd do
   -- a code path. A deleted .olean would make the scan above vacuous; an extra
   -- one is orphan litter with no shipped source.
   logInfo s!"  kernel confirms: {nConst} declarations across {nMod} compiled modules (this button's manifest, by membership), none is an axiom"
+  for n in seen do IO.println s!"KERNEL-NAME|{n}"
 LEANGATE
 } > "$GATE"
 cd "$AENEAS_LEAN"
@@ -614,12 +617,13 @@ cd "$AENEAS_LEAN"
 # `set -e` a bare `rm` after the call never runs when the gate goes red, which
 # is exactly how this repo accumulated 101 orphan .olean files (fixed today).
 GATE_RC=0
+KERNLOG=$(mktemp /tmp/check-kernel-XXXX.log)
 lake env bash -c "
   set -euo pipefail
   cd '$HERE/gen' && export LEAN_PATH=\"\$LEAN_PATH:\$PWD:$HERE\"
   cd '$HERE'
   LEAN_TIMEOUT=$TIMEOUT LEAN_MAX_CORES=$CORES '$HERE/lean-guard' '$GATE'
-" || GATE_RC=$?
+" 2>&1 | tee "$KERNLOG" || GATE_RC=${PIPESTATUS[0]}
 rm -f "$GATE" "${GATE%.lean}.olean"
 if [ "$GATE_RC" -ne 0 ]; then
   echo "AXIOM SMUGGLING GATE FAILED (kernel-side) — see the error above."
@@ -686,7 +690,64 @@ OBS=$(mktemp /tmp/check-inv-obs-XXXX.log)
 grep '^INV|' "$INVLOG" > "$OBS"
 echo "INV-COUNT|${SUM:-0}" >> "$OBS"
 "$HERE/inventory_gate.sh" "$OBS" "$HERE/inventory-allowlist.txt" || INVFAIL=1
-rm -f "$INVLOG" "$OBS"
+# ── THE ACCOUNTING IDENTITY ───────────────────────────────────────────────
+# Every declaration the kernel saw must be accounted for by exactly one walk:
+# the corpus inventory, or the instruments' own surface. Until 2026-07-31 the
+# two numbers were never compared — the kernel reported 3058 across this
+# button's manifest, the inventory accounted for 3022, and the 36-declaration
+# difference was the audit drivers' own machinery, covered by no allowlist row
+# and by no other check. It was not a soundness hole (the drivers ARE in the
+# manifest, so Phase 2b's kernel gate rejects an axiom in one whatever its
+# indentation) but it was an unexamined remainder, and an unexamined remainder
+# is where the next defect hides.
+#
+# COUNT DISTINCT CONSTANTS, NOT PHYSICAL DECLARATIONS. The two sides of this
+# identity were, at first, counting different things, and the gap was papered
+# over with a `+ N_DRIVERS` term justified as a "self-observation blind spot".
+# That explanation was WRONG. It fitted dalek and anza (2 drivers, residual 2)
+# and broke on risc0 and betrusted (1 driver, residual 2) — the residual is 2
+# everywhere and has nothing to do with drivers.
+#
+# The measured cause: Lean materialises equation lemmas LAZILY, when something
+# forces an unfold, and each module that forces one gets its own copy in its
+# object file. On every fork, `CurveFieldProofs.denote.eq_1` sits in both
+# `SubNegSpec.olean` and `ConstSpecs.olean`, and `CurveFieldProofs.limbsVal.eq_1`
+# in both `ReduceSpec.olean` and `ConstSpecs.olean`. The kernel gate reads each
+# object file separately and counts both copies; the environment holds one
+# constant per name and the inventory sees it once. Hence exactly 2.
+#
+# So the gate now reports DISTINCT names and the fudge term is gone. This still
+# fails closed: a declaration missing from both walks leaves the sum short, and
+# one counted twice leaves it long. A future mismatch must be explained — as
+# this one finally was — never absorbed into a constant.
+N_DRV=$(grep -c '^DRV|' "$INVLOG" || true)
+DRV_TRAILERS=$(grep -c '^DRV-COUNT|' "$INVLOG" || true)
+DRV_SUM=$(grep '^DRV-COUNT|' "$INVLOG" | cut -d'|' -f2 | paste -sd+ - | bc)
+KERN_NAMES=$(mktemp /tmp/check-kernnames-XXXX.txt)
+ACCT_NAMES=$(mktemp /tmp/check-acctnames-XXXX.txt)
+LC_ALL=C grep '^KERNEL-NAME|' "$KERNLOG" | cut -d'|' -f2 | LC_ALL=C sort -u > "$KERN_NAMES"
+{ LC_ALL=C awk -F'|' '/^INV\|/{print $3}' "$HERE/inventory-allowlist.txt"
+  LC_ALL=C grep '^DRV|' "$INVLOG" | cut -d'|' -f2
+} | LC_ALL=C sort -u > "$ACCT_NAMES"
+UNACCOUNTED=$(LC_ALL=C comm -23 "$KERN_NAMES" "$ACCT_NAMES")
+if [ "$DRV_TRAILERS" -ne "$N_DRIVERS" ]; then
+  echo "  DRIVER SURFACE INCOMPLETE: expected a trailer from each of the $N_DRIVERS driver(s), saw $DRV_TRAILERS"
+  INVFAIL=1
+elif [ "${DRV_SUM:-0}" != "$N_DRV" ]; then
+  echo "  DRIVER SURFACE TRUNCATED: trailers sum to ${DRV_SUM:-0}, observed $N_DRV lines"
+  INVFAIL=1
+elif [ ! -s "$KERN_NAMES" ]; then
+  echo "  ACCOUNTING FAILED: Phase 2b reported no constant names — the scan was vacuous"
+  INVFAIL=1
+elif [ -n "$UNACCOUNTED" ]; then
+  echo "  ACCOUNTING FAILED: the kernel holds constants that neither walk accounts for:"
+  printf '%s\n' "$UNACCOUNTED" | head -20 | sed 's/^/    /'
+  INVFAIL=1
+else
+  echo "  accounting: every one of $(wc -l < "$KERN_NAMES") kernel constants is covered by the corpus inventory or the instrument surface"
+fi
+rm -f "$KERN_NAMES" "$ACCT_NAMES"
+rm -f "$INVLOG" "$OBS" "$KERNLOG"
 
 # The drivers' corpus lists must together BE the compile manifest, minus the
 # audit infrastructure and the scalar layer. Checked in both directions so a