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 @@
 12dc724bffd590e6f706573d97bf07425b8f268a1be2d72a3bbd9aef48f9c277  AUDIT-MANIFEST.txt
 9bafc9666196041e4a46f6cd332e899a9aa86fbdae54513dd873c89670821371  check-scalar.sh
-3832f0648caee17679f3826c8db6b17eaee43c9bfb147141373a01724dff0328  check.sh
+2249f78839ac91865c33ef852b41f66baa246aaff2c89875f9739c6b819364e3  check.sh
 20797552647da51d0646370cf11be1fb86fadb27f28f01fde391b451377a63f9  driver-allowlist.txt
 fdd1337f1f44fa73fdb14e6cda001e4e7358513b9c178c517456b24511d96a8e  extract.sh
 5a5fd8a0e1d29033e00b98fd0d37b860a3754205d7a46d2c5168d68c26b3dc25  GEN-MODEL.sha256

verification/check.sh

@@ -595,7 +595,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
@@ -604,9 +604,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
@@ -615,7 +626,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"
@@ -784,10 +795,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"
@@ -803,9 +848,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"