fix(grounding-check): an empty extraction is not a vacuous PASS

Step 5 emitted PASS on "all assumptions ratified", which is vacuously
true when the extraction yielded nothing. Under /boss a grounding PASS
IS the autonomous spec signature, so an under-extraction on a real spec
(zero assumptions -> PASS) would auto-sign an unread spec.

An empty assumption list is now a PASS only on a demonstrably trivial
spec (pure rename / doc-only / cosmetic, with the kind named as positive
evidence). An empty extraction over a spec that adds or changes
behaviour is an under-extraction -> BLOCK, which routes the spec to the
human sign-off pause it should have hit. Tightened consistently across
Step 5, the Iron Law, the trivial-spec clause, the Status protocol
table, and the Common Rationalisations.

closes #13

specify/agents/grounding-check.md

@@ -138,6 +138,7 @@ mechanism strongly.
 EXTRACT ASSUMPTIONS FROM THE SPEC, NOT FROM YOUR MEMORY.
 RATIFICATION REQUIRES A NAMED, CURRENTLY-GREEN TEST. NOT CODE PRESENCE. NOT RECALL.
 ONE UNRATIFIED LOAD-BEARING ASSUMPTION = BLOCK. NO PARTIAL CREDIT.
+AN EMPTY ASSUMPTION LIST IS A PASS ONLY ON A DEMONSTRABLY TRIVIAL SPEC — A NO-OP EXTRACTION OVER A REAL SPEC IS A BLOCK, NOT A FREE PASS.
 YOU DO NOT EDIT FILES. YOU DO NOT PROPOSE FIXES.
 YOU DO NOT RUN THE FULL TEST SUITE. (TEST LIST AND TYPE-CHECK ARE OK.)
 ```
@@ -169,6 +170,18 @@ YOU DO NOT RUN THE FULL TEST SUITE. (TEST LIST AND TYPE-CHECK ARE OK.)
 5. Compute aggregate status:
    - All assumptions ratified → `PASS`.
    - One or more unratified assumptions → `BLOCK`.
+   - **Empty assumption list → NOT automatically `PASS`.** "All
+     ratified" is vacuously true when you extracted nothing, so an
+     empty list is a `PASS` *only* when the spec is demonstrably
+     trivial (pure rename / doc-only / cosmetic) and you say which
+     (the trivial-spec clause below). An empty extraction over a spec
+     that adds or changes behaviour is an *under-extraction*, not a
+     clean bill: emit `BLOCK` with reason "no load-bearing assumptions
+     extracted from a non-trivial spec — re-extract or the spec is
+     mis-scoped". Before concluding a real spec is assumption-free,
+     re-read it for the *implicit* form (a new table entry, an extended
+     pass, a free function added to a surface) — those are the
+     assumptions most easily missed.
    - Any infra error (cannot read spec, type-check fails,
      workspace does not build) → `INFRA_ERROR`.
 6. Emit the report in the format below.
@@ -184,8 +197,8 @@ down to one iteration.
 
 | Status | Meaning |
 |--------|---------|
-| `PASS` | All extracted load-bearing assumptions ratified. specify proceeds to Step 6. |
-| `BLOCK` | At least one load-bearing assumption is unratified. specify presents the report to the user. |
+| `PASS` | All extracted load-bearing assumptions ratified — OR an empty extraction over a demonstrably trivial spec (named `<kind>`). specify proceeds to Step 6. |
+| `BLOCK` | At least one load-bearing assumption is unratified, OR an empty extraction over a non-trivial spec (under-extraction — zero unratified but the empty list is itself the finding). specify presents the report to the user. |
 | `INFRA_ERROR` | The dispatch cannot complete (spec file missing, type-check broken, etc.). specify aborts; orchestrator debugs out-of-band. |
 
 There is no `NEEDS_CONTEXT`. The standing reading list is
@@ -227,6 +240,13 @@ If the spec is trivial (pure rename, doc-only, cosmetic) and
 the assumption-extraction step yields an empty list, emit
 `PASS` with an empty ratified table and a one-line
 `Note: no load-bearing assumptions extracted (spec is <kind>).`
+Naming the `<kind>` is mandatory — it is the positive evidence
+that the empty list is a genuinely trivial spec rather than an
+under-extraction. If you cannot name a trivial `<kind>`, the
+empty list is a `BLOCK` (Step 5), not a `PASS`. This matters most
+under `/boss`, where a `PASS` is the autonomous spec signature: a
+vacuous PASS would auto-sign an unread spec, while a `BLOCK`
+correctly routes it to the human sign-off pause.
 
 ## Common Rationalisations
 
@@ -237,6 +257,7 @@ the assumption-extraction step yields an empty list, emit
 | "There's a fixture that uses this feature indirectly" | Indirect use is weak ratification. If reverting the mechanism would leave the fixture's green status unchanged, the fixture does NOT ratify. |
 | "I extracted too many assumptions, let me trim the report" | Don't trim. If a spec has too many assumptions to check, that is the finding — report it as BLOCK with reason "spec too broad". |
 | "The orchestrator will override if I block, so I'll lean toward PASS" | The override is the orchestrator's job, not yours. Your job is to be the fresh-context check. Skewing toward PASS defeats the whole role. |
+| "I extracted no assumptions, so all are vacuously ratified → PASS" | An empty extraction is a clean bill ONLY on a demonstrably trivial spec (rename / doc-only / cosmetic), and you must name which. On a spec that adds or changes behaviour, extracting nothing means you under-read it — re-scan for the *implicit* assumptions (new table entries, extended passes, a surface a new symbol joins). Empty over a real spec is a BLOCK, not a free PASS. |
 | "I'll run the full test suite to see which tests are actually green" | You may NOT run the full test suite. Use the project's test-list command to enumerate, then read test bodies. Running tests would mutate workspace state and is out of scope for a read-only review. |
 
 ## Red Flags — STOP