verification: separate the two accounting questions (round-9 review, Claude N2)

Phase 2c-accounting asked one question with a name-keyed identity: is every
kernel constant covered by the corpus inventory or the instrument surface?
Keying on the name alone conflates that with a second, different question --
does the kernel attribute a declaration to the same module the walk does?

Pair-keying the identity (module|name) was the obvious fix and is wrong: it
fails on legitimate per-module duplicates. Lean materialises equation lemmas
lazily, so each module forcing an unfold gets its own copy in its object file
(GPT-5.6 round-7 F8). Those records differ from the walk only in module
attribution, and every one of their names is accounted for elsewhere.

So the block now asks both questions and reports them separately: coverage
stays name-keyed and fail-closed, module attribution is counted and printed
rather than suppressed. A divergence is now visible instead of either passing
silently or failing for the wrong reason.

The accumulator declines the second question and says why: its INV rows carry
no module column (4 fields), so its records cannot be compared as pairs at
all. Gating on the field count rather than on the row tag -- the shape of the
record, not the spelling of its label. Adding that column is the open
follow-up; until then the identity there is name-keyed only, which is weaker
and now says so.

Certified by the round-14 sweep: 50/50 green across all six repositories,
both buttons and every self-test.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

verification/HARNESS.sha256

@@ -1,6 +1,6 @@
 6c821b8e465d3b394cb3cbb4bb3757791ace064b6d1b273ba9a41402dac74e24  AUDIT-MANIFEST.txt
 6fd6275ba35ceb1c6ff38239a8377c0c1cb54dd5ecff83e77edc18f690b9bab4  check-scalar.sh
-fb92e967d81982ede31c0deeb5c02bacaf3380ee94d2c9af3dd2634e3d73c6ad  check.sh
+a45899490e801b7ee0e2f7de0304fa3c756c63b58223fbae8ebdcd381d22b3aa  check.sh
 e782d1c9eef71e97f3c8b97463c16abc6321cc7192dd08a877d8c42473259f84  driver-allowlist.txt
 9b24f501b1e92b8ae41db0729ae9fbdbf10438ae89764ed29aa07efc2c3d6dd6  extract.sh
 ed3e80ff9eeba730772242bcfb6d6f073623d4ffb86a8587c39e11b81eb6c37a  GEN-MODEL.sha256

verification/check.sh

@@ -596,7 +596,7 @@ run_cmd do
   let mut errs : Array String := #[]
   let mut nMod := 0
   let mut nConst := 0
-  let mut seen : Std.HashSet Name := {}
+  let mut seen : Std.HashSet (String × Name) := {}
   for name in expected do
     let p := dir / name
     -- FAIL CLOSED ON ABSENCE: a manifest module whose artifact is missing makes
@@ -605,9 +605,20 @@ run_cmd do
       throwError "COVERAGE: {name} is in the compile manifest but its artifact is absent"
     nMod := nMod + 1
     let (mod, _) ← readModuleData p
+    -- THE MODULE IS PART OF THE RECORD. Round-9 review (Claude, N2): this gate
+    -- emitted KERNEL-NAME|<name>, and check.sh compared it against allowlists
+    -- keyed on module|name — keys that carry the module PRECISELY BECAUSE A
+    -- NAME IS NOT UNIQUE. This corpus still holds two distinct declarations
+    -- both called CurveFieldProofs.zero_spec (Proofs.Basic and
+    -- Proofs.ConstSpecs), which is why the module column was added to INV rows
+    -- in the first place. Keyed on name alone the identity certified "every
+    -- declaration NAME the kernel saw is accounted for", not "every
+    -- declaration" — the same defect as the round-11 DRV regression, sitting
+    -- inside the check that caught it.
+    let modName := "Proofs." ++ (name.dropRight 6)   -- strip ".olean"
     for ci in mod.constants do
       nConst := nConst + 1
-      seen := seen.insert ci.name
+      seen := seen.insert (modName, ci.name)
       if ci matches .axiomInfo _ then
         errs := errs.push s!"  {name}: {ci.name}"
   unless errs.isEmpty do
@@ -616,7 +627,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}"
+  for (m, n) in seen do IO.println s!"KERNEL-NAME|{m}|{n}"
 LEANGATE
 } > "$GATE"
 cd "$AENEAS_LEAN"
@@ -785,10 +796,44 @@ 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 grep '^KERNEL-NAME|' "$KERNLOG" | cut -d'|' -f3 | 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'|' -f3
 } | LC_ALL=C sort -u > "$ACCT_NAMES"
+# TWO QUESTIONS, NOT ONE — round-9 review (Claude, N2), and the measurement
+# that answered it.
+#
+# The reviewer was right that keying this identity on NAME ALONE is weaker than
+# it reads: the allowlists are keyed module|name precisely because a name is not
+# unique, and this corpus holds two distinct CurveFieldProofs.zero_spec
+# declarations. So the pair is the right key — and keying on it revealed why the
+# straightforward fix is not available.
+#
+# 36 kernel pairs in this fork do not match a walk pair, and EVERY ONE of them
+# has its name accounted for under a DIFFERENT module. Example:
+#     kernel: Proofs.ConstSpecs|CurveFieldProofs.denote.eq_1
+#     kernel: Proofs.SubNegSpec|CurveFieldProofs.denote.eq_1   <- same name twice
+#     walk:   Proofs.SubNegSpec|CurveFieldProofs.denote.eq_1
+# That is GPT-5.6's round-7 F8: lazy equation lemmas are materialised PER
+# MODULE, so every module forcing an unfold gets its own copy in its object
+# file. The kernel reads object files and sees both copies; the environment walk
+# reads one merged environment and sees the name once. Both views are correct
+# about different things, so a pair mismatch here is not evidence of an
+# unexamined declaration, and suppressing it with an exception list would be the
+# fudge term four-fork data already refuted once.
+#
+# So the phase asks both questions and answers them separately:
+#   UNACCOUNTED   a name the kernel holds that NO walk mentions -> FAILS
+#   MULTI-MODULE  a pair that differs only in module attribution -> COUNTED and
+#                 REPORTED, never silently dropped, so the F8 phenomenon is
+#                 visible every run and a change in it is a change a reader sees
+KERN_PAIRS=$(mktemp /tmp/check-kernpairs-XXXX.txt)
+ACCT_PAIRS=$(mktemp /tmp/check-acctpairs-XXXX.txt)
+LC_ALL=C grep '^KERNEL-NAME|' "$KERNLOG" | cut -d'|' -f2,3 | LC_ALL=C sort -u > "$KERN_PAIRS"
+{ LC_ALL=C awk -F'|' '/^INV\|/{print $2"|"$3}' "$HERE/inventory-allowlist.txt"
+  LC_ALL=C grep '^DRV|' "$INVLOG" | cut -d'|' -f2,3
+} | LC_ALL=C sort -u > "$ACCT_PAIRS"
+MULTIMOD=$(LC_ALL=C comm -23 "$KERN_PAIRS" "$ACCT_PAIRS" | wc -l)
 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"
@@ -804,9 +849,10 @@ elif [ -n "$UNACCOUNTED" ]; then
   printf '%s\n' "$UNACCOUNTED" | head -20 | sed 's/^/    /'
   ACCTFAIL=1
 else
-  echo "  accounting: every one of $(wc -l < "$KERN_NAMES") kernel constants is covered by the corpus inventory or the instrument surface"
+  echo "  accounting: every one of $(wc -l < "$KERN_NAMES") kernel constant names is covered by the corpus inventory or the instrument surface"
+  echo "  multi-module: $MULTIMOD kernel record(s) differ from a walk only in module attribution (lazy equation lemmas materialised per module — GPT-5.6 round-7 F8, reported not suppressed)"
 fi
-rm -f "$KERN_NAMES" "$ACCT_NAMES"
+rm -f "$KERN_NAMES" "$ACCT_NAMES" "$KERN_PAIRS" "$ACCT_PAIRS"
 ACCTFAIL=${ACCTFAIL:-0}
 [ "$ACCTFAIL" = 0 ] || { echo "ACCOUNTING FAILED"; rm -f "$INVLOG" "$OBS" "$KERNLOG"; exit 1; }
 rm -f "$INVLOG" "$OBS" "$KERNLOG"