diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index dc28085..1a0415b 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -18,7 +18,7 @@ jobs:
         with:
           python-version: ${{ matrix.python-version }}
       - run: pip install -e ".[dev]"
-      - run: ruff check src tests scripts/vv.py
+      - run: ruff check src tests scripts
       - run: pytest
       - run: realize demo three_state
       - run: realize demo max_formula
diff --git a/NONCLAIMS.md b/NONCLAIMS.md
index 7161300..85a0139 100644
--- a/NONCLAIMS.md
+++ b/NONCLAIMS.md
@@ -13,7 +13,7 @@ Read this before the README examples.
 7. **Checker independence reduces one self-confirmation path.** Separate generator and checker implementations do not certify the Python runtime, the papers’ mathematics, or that a formal `R` matches anyone’s linguistic intention.
 8. **`UNSAT` is scoped.** It means the declared finite class is empty (or the encoder fibre is obstructed). It never means “no operator exists.”
 9. **Agents may propose. They may not certify.** Calling another model to judge an answer does not discharge `realize check`.
-10. **Lean corroboration is not a verdict.** The files in `vv/lean/` re-state finite facts and check them in Lean's kernel. Agreement means two implementations, written by different means, reached the same answer about the same small finite object. It does not verify the Python code, the CLI, the CI, or the papers' mathematics, and a Lean file cannot mint `PASS`. Disagreement means one of the two is wrong and does not say which.
+10. **Lean corroboration is not a verdict.** The files in `vv/lean/` re-state finite facts, and derive from them what verdict the checker has to report for each spec that ships; both are checked in Lean's kernel. Agreement means two implementations, written by different means, reached the same answer about the same small finite object. It does not verify the Python code, the CLI, the CI, or the papers' mathematics, and a Lean file cannot mint `PASS` — nothing in `vv/lean/` sits on the path that produces a certificate. Lean does not read the spec files either: each is transcribed into Lean by hand, so the comparison catches an edit to one side and not a matching edit to both. Disagreement means one of the two is wrong and does not say which.
 11. **A green V&V run is not validation.** `scripts/vv.py` checks that each declared domain does what it says it does (verification). Whether a formal `R` matches anyone's intention is a separate question this repository does not answer. See [VV.md](VV.md).
 
 If a README sentence appears to contradict this file, this file wins.
diff --git a/README.md b/README.md
index 4d30262..82d7773 100644
--- a/README.md
+++ b/README.md
@@ -102,7 +102,7 @@ Tools: `realize_check`, `realize_synthesize`, `realize_explain`, `realize_demo`.
 ```bash
 pip install -e ".[dev]"
 pytest
-ruff check src tests scripts/vv.py
+ruff check src tests scripts
 python3 scripts/vv.py
 ```
 
diff --git a/VV.md b/VV.md
index ee61426..74a7420 100644
--- a/VV.md
+++ b/VV.md
@@ -32,7 +32,7 @@ are the bookkeeping that keeps someone from mistaking verification for it.
 | Verification (IEEE 1012) | `realize check` | the thing does what the words say |
 | Validation (IEEE 1012) | not dischargeable; only provenance and scope | the words say what someone wanted |
 | The oracle problem | the spec is the oracle; the model is not | something else has to say what is true, and it cannot be the one that made the thing |
-| Separation of duties | `tests/test_isolation.py`; `no_self_grading` | the one who makes a thing is not the one who says it is good |
+| Separation of duties | `tests/test_isolation.py`; `synthesize_emits_no_verdict` | the one who makes a thing is not the one who says it is good |
 | N-version / dissimilar redundancy (DO-178C) | [`vv/lean/`](vv/lean/) | two different ones do the same work apart; then you see if they say the same |
 | Soundness | `PASS` is scoped, never global | when it says yes, it is true |
 | Refusal of completeness | `UNKNOWN` is required (NONCLAIMS §2) | when it cannot know, it says so |
@@ -80,9 +80,45 @@ Per domain:
 |---|---|
 | `declared_semantics` | Matrix, kernel table, and every referenced spec agree on family / grammar / semantics. |
 | `outcome_coverage` | The domain is seen reaching `PASS`, `COUNTEREXAMPLE`, `UNSAT`, `UNKNOWN`, and adapter reject. All five. |
-| `tamper_evidence` | Change one field of the spec, and the passing candidate becomes an adapter reject. |
-| `no_self_grading` | `realize synthesize` returns candidates and no `verdict`, anywhere in the payload. |
-| `provenance` | Every non-null `R` and `K` clause cites a source. |
+| `tamper_evidence` | Change `bound.budget` by one, and the candidate bound to that spec is refused rather than judged. |
+| `synthesize_emits_no_verdict` | `realize synthesize` returns candidates, and no `verdict` key at any depth of the payload. |
+| `provenance` | Every non-null `R` and `K` clause names an origin, or declares with `unsourced` that it has none. |
+
+### What `provenance` can and cannot decide
+
+Three things about a citation are decidable, and the objective checks all three: that a clause
+which constrains is cited at all, that the citation is not blank, and that it does not point at
+one of this repository's own documents. `NONCLAIMS.md`, `README.md` and `VV.md` explain what the
+package does and refuses to claim; none of them is ever where a clause came from.
+
+That third rule is not hypothetical. Four specs in the first version of this matrix cited
+`NONCLAIMS.md §2` — the section explaining why a zero budget yields `UNKNOWN` — as the source of
+the relation in `R`. The gate passed them, because a citation that does not cite still looks like
+a citation. A reviewer caught it; the gate could not. It can now, and
+`tests/test_vv.py` keeps that specific failure caught.
+
+**What stays undecidable: whether a source names anything real.** `VCOS §8.1 Table 2` and `asdf`
+are the same shape, and nothing in a finite checker tells them apart. A clause with no origin
+declares that with `"unsourced": true` *and* a `source` giving the reason, and the gate takes
+the author's word for it — so that marker is a bypass, deliberately a visible one. The reason is
+required precisely because an unexplained bypass is one nobody can audit. Counting the `unsourced` clauses in `vv/specs/` is
+a minute's work for a person; noticing a plausible-looking citation that names nothing is not.
+
+This is V₂ reaching into a V₁ check, and it does not close. What the objective changed is where
+the gap sits: it used to hide inside citations that looked fine, and now it sits in a marker you
+can grep for. Countable is the most a finite checker can make it.
+
+### What the objective names mean
+
+An objective is named for **what it reads**, not for the property someone might hope it
+establishes. `synthesize_emits_no_verdict` says a payload carried no `verdict` key; it does not
+say an agent refrained from grading itself, which is what NONCLAIMS §9 forbids and what no check
+here can see. `tamper_evidence` says one named field was changed and the bound candidate was
+refused; the general property comes from the digest, not from the test.
+
+This is not pedantry about naming. A report line reading `[ok] no_self_grading` is read as
+"self-grading has been ruled out," and that is a claim this harness cannot make. In a repository
+whose product is refusing to overclaim, the harness is the last place that should start.
 
 `outcome_coverage` is the one worth reading twice. Every domain must be *observed* reaching all four
 verdicts and the adapter reject — not merely be capable of it in principle. A domain that can only
@@ -112,9 +148,31 @@ The runner refuses a file that reaches for any of those before `lean` is even in
 file that may assume things corroborates nothing.
 
 Proving things in a second language is not yet a cross-check, though: two implementations can drift
-apart happily if nobody puts their answers side by side. So each Lean file also *reports* the
-finite quantities it settled — 29 of them — and `scripts/vv.py` recomputes every one from the Python
-kernel and compares. A disagreement fails the run; so does a fact that quietly stops being reported.
+apart happily if nobody puts their answers side by side. So each Lean file also *reports* what it
+settled, and `scripts/vv.py` answers the same questions from Python and compares. A disagreement
+fails the run; so does a fact that quietly stops being reported.
+
+### Two bands: the parts, and the effect
+
+The questions come in two kinds, and the second one is the point.
+
+| Band | Facts | Lean reports | Python reports | What only this band sees |
+|---|---|---|---|---|
+| parts | 29 | what a search contains — 625 template members, ten series reaching 7, the obstructed fibre | the same, recomputed from kernel internals | a kernel that counts wrong |
+| effect | 22 | the verdict the checker **has to** give a spec that ships, worked out from the branch order the checker uses | the verdict `check_search` **did** give that same spec file | a kernel whose parts are each right and whose verdict is assembled from them wrongly |
+
+The effect band is what makes this a check on the repository rather than on its arithmetic. Python
+answers it by running the real entry point on the real spec file and reading the certificate: the
+verdict, how settled it is, and why.
+
+Two injected faults show the difference. Move the histogram pre-check in `_search_grid` to after the
+enumeration: `grid_preserve_histogram` still reports `UNSAT`, still exits 3, so the domain matrix
+passes, the whole Python suite passes, and all 29 part-facts agree — only the effect band sees it
+change reason from `histogram_contradicts_R` to `no_typed_realization`. Report an exhaustive `UNSAT`
+as `unresolved` instead of `proved` and the same thing happens again.
+
+Coverage of that band is structural, not a list someone remembers to extend: `tests/test_vv.py`
+fails when a spec lands in `vv/specs/` or `demos/` that no Lean file derives a verdict for.
 
 What agreement buys: two implementations written in different languages, by different means, reached
 the same answer about the same small finite object. NONCLAIMS §7 says checker independence "reduces
@@ -123,12 +181,16 @@ count edited to match a drifting kernel, which the Python suite alone cannot cat
 suite is what would have been edited.
 
 What it does not buy: Lean does not verify the Python kernel, the CLI, the CI, or the papers'
-mathematics, and **a Lean file cannot mint a verdict**. If Lean and Python disagree, the V&V job goes
-red and one of them is wrong — the job does not say which.
+mathematics, and **a Lean file cannot mint a verdict** — nothing in `vv/lean/` sits on the path that
+produces a certificate. Lean does not read the spec files either: each one is transcribed into Lean
+by hand, so the comparison catches an edit to one side and not a matching edit to both. If Lean and
+Python disagree, the V&V job goes red and one of them is wrong — the job does not say which.
 
 ## What this does not establish
 
-1. That `R` means what anyone intended. That is V₂, and it stays open. NONCLAIMS §7.
+1. That `R` means what anyone intended. That is V₂, and it stays open. NONCLAIMS §7. The
+   `provenance` objective checks the *form* of a citation, never that it names something real —
+   see above.
 2. That a `PASS` says anything outside the declared finite scope. NONCLAIMS §6.
 3. That the counts are a benchmark result. They are coverage. NONCLAIMS §5.
 4. That the Python runtime, the OS, or GitHub Actions are correct.
diff --git a/scripts/export_web_fixtures.py b/scripts/export_web_fixtures.py
old mode 100644
new mode 100755
index df87593..3e7e9fe
--- a/scripts/export_web_fixtures.py
+++ b/scripts/export_web_fixtures.py
@@ -7,23 +7,32 @@
 import sys
 from pathlib import Path
 
-ROOT = Path(__file__).resolve().parents[1]
-sys.path.insert(0, str(ROOT / "src"))
-
-from realize import __version__  # noqa: E402
-from realize.demos import load_demo_spec, run_demo  # noqa: E402
+try:
+    from realize import __version__
+    from realize.demos import load_demo_spec, run_demo
+except ModuleNotFoundError as missing:  # a bare checkout, before `pip install -e .`
+    # Only an absent top-level package means "not installed yet". A missing submodule
+    # means the install is broken, and falling back would hide that.
+    if missing.name != "realize":
+        raise
+    sys.path.insert(0, str(Path(__file__).resolve().parents[1] / "src"))
+    from realize import __version__
+    from realize.demos import load_demo_spec, run_demo
 
+ROOT = Path(__file__).resolve().parents[1]
 
 OUT = ROOT / "web" / "fixtures"
 
 
 def write(name: str, obj: dict) -> None:
+    """Write one fixture, sorted and newline-terminated so reruns produce no diff."""
     path = OUT / name
     path.write_text(json.dumps(obj, indent=2, sort_keys=True) + "\n", encoding="utf-8")
     print(f"wrote {path.relative_to(ROOT)}")
 
 
 def main() -> None:
+    """Dump every demo certificate the pages display, plus a manifest naming them."""
     OUT.mkdir(parents=True, exist_ok=True)
     files: list[str] = []
 
diff --git a/scripts/serve_web.py b/scripts/serve_web.py
old mode 100644
new mode 100755
diff --git a/scripts/vv.py b/scripts/vv.py
index d40dcfc..9ade9bd 100755
--- a/scripts/vv.py
+++ b/scripts/vv.py
@@ -26,7 +26,11 @@
     from realize.digest import canonical_bytes
     from realize.spec import load_spec
     from realize.verdicts import EXIT, GRAMMARS, PROBLEM_FAMILIES, SEMANTICS, Verdict
-except ModuleNotFoundError:  # a bare checkout, before `pip install -e ".[dev]"`
+except ModuleNotFoundError as missing:  # a bare checkout, before `pip install -e .`
+    # Only an absent top-level package means "not installed yet". A missing submodule
+    # means the install is broken, and falling back would hide that.
+    if missing.name != "realize":
+        raise
     sys.path.insert(0, str(Path(__file__).resolve().parents[1] / "src"))
     from realize import __version__
     from realize.checker import check_search
@@ -50,6 +54,30 @@
 OUTCOMES = frozenset({v.value for v in Verdict} | {ADAPTER})
 PROVENANCE_CLAUSES = ("R", "K")
 
+# A repository document says what this package does or refuses to claim. It is never
+# where a clause came from. Citing one as an origin is the confusion this gate exists
+# to catch; a clause that genuinely has no origin says so with `unsourced`.
+REPO_DOCUMENTS = ("NONCLAIMS.md", "README.md", "VV.md", "SKILL.md")
+
+# Specs that ship, the verdict each one draws out of the checker, and the witness
+# fields worth comparing. Lean derives what the verdict has to be; `effect_facts`
+# reads what it was. These are the repository's effect, not its internals.
+EFFECT_SPECS = (
+    ("max_formula", "demos/max_formula/spec.json", ("universe", "n_valid")),
+    ("formula_affine_only", "vv/specs/formula_affine_only.spec.json", ("universe",)),
+    ("formula_unrecognized_phrase", "vv/specs/formula_unrecognized_phrase.spec.json", ()),
+    ("three_state", "demos/three_state/spec.json", ("obstructions",)),
+    ("encoder_separating", "vv/specs/encoder_separating.spec.json", ("adequate_encoders",)),
+    ("encoder_zero_budget", "vv/specs/encoder_zero_budget.spec.json", ()),
+    ("series_seven", "vv/specs/series_seven.spec.json", ("n_valid", "min_len")),
+    ("series_even_repertoire", "vv/specs/series_even_repertoire.spec.json", ("n_valid",)),
+    ("series_target_nine", "vv/specs/series_target_nine.spec.json", ()),
+    ("series_zero_budget", "vv/specs/series_zero_budget.spec.json", ()),
+    ("grid_recolor", "demos/grid_recolor/spec.json", ("n_valid",)),
+    ("grid_preserve_histogram", "vv/specs/grid_preserve_histogram.spec.json", ()),
+    ("grid_zero_budget", "vv/specs/grid_zero_budget.spec.json", ()),
+)
+
 
 # ---------------------------------------------------------------- primitives
 
@@ -184,14 +212,41 @@ def objective_tamper(domain: dict) -> dict:
             "tamper_evidence",
             f"budget changed by one and the candidate still scored exit {code}",
         )
-    return meet("tamper_evidence", "a one-field spec edit turns PASS into an adapter reject")
+    return meet(
+        "tamper_evidence",
+        "bound.budget changed by one and the bound candidate was refused, not judged",
+    )
+
 
+def verdict_keys(node: Any, path: str = "") -> list[str]:
+    """Every place a `verdict` key appears in a decoded JSON document, by path.
 
-def objective_no_self_grading(domain: dict) -> dict:
-    """The proposer channel must never hand back something that reads as a verdict."""
+    A synthesize payload is a proposal. A grade nested three levels down still reads
+    as a grade, so the whole document is walked rather than its first two levels.
+    """
+    found: list[str] = []
+    if isinstance(node, dict):
+        for key, value in node.items():
+            here = f"{path}.{key}" if path else key
+            if key == "verdict":
+                found.append(here)
+            found += verdict_keys(value, here)
+    elif isinstance(node, list):
+        for index, value in enumerate(node):
+            found += verdict_keys(value, f"{path}[{index}]")
+    return found
+
+
+def objective_synthesize_emits_no_verdict(domain: dict) -> dict:
+    """The proposer channel must not hand back something that reads as a verdict.
+
+    This is one mechanical consequence of NONCLAIMS §9, not a check of the principle.
+    It reads one `synthesize` payload, every key of it; it cannot see an agent calling
+    another model to grade an answer, which is the thing §9 actually forbids.
+    """
     case = next((c for c in domain["cases"] if c["expect"]["outcome"] == "PASS"), None)
     if case is None:
-        return fail("no_self_grading", "domain declares no PASS case to synthesize from")
+        return fail("synthesize_emits_no_verdict", "domain declares no PASS case to synthesize from")
     proc = subprocess.run(
         [sys.executable, "-m", "realize", "synthesize", case["spec"]],
         capture_output=True,
@@ -201,31 +256,90 @@ def objective_no_self_grading(domain: dict) -> dict:
         check=False,
     )
     if proc.returncode != 0:
-        return fail("no_self_grading", f"synthesize exited {proc.returncode}: {proc.stderr.strip()}")
+        return fail("synthesize_emits_no_verdict", f"synthesize exited {proc.returncode}: {proc.stderr.strip()}")
     payload = json.loads(proc.stdout)
-    if "verdict" in payload:
-        return fail("no_self_grading", "synthesize output carries a top-level verdict")
-    graded = [c for c in payload.get("candidates", []) if "verdict" in c]
+    graded = verdict_keys(payload)
     if graded:
-        return fail("no_self_grading", f"{len(graded)} synthesized candidates carry a verdict")
+        return fail(
+            "synthesize_emits_no_verdict",
+            f"synthesize output carries a verdict at {', '.join(graded)}",
+        )
     return meet(
-        "no_self_grading",
-        f"{len(payload.get('candidates', []))} candidates, none carrying a verdict",
+        "synthesize_emits_no_verdict",
+        f"{len(payload.get('candidates', []))} candidates, no verdict key at any depth",
     )
 
 
+def provenance_gaps(label: str, specification: dict) -> list[str]:
+    """The decidable part of the provenance rule, over one specification.
+
+    Three things about a citation are decidable and are checked here: that a clause
+    which constrains is cited at all, that the citation is not blank, and that it
+    does not point at one of this repository's own documents — those explain what the
+    package does and refuses to claim, and are never where a clause came from. A
+    clause with no origin declares that with `unsourced` rather than narrating it, and
+    still owes a `source` giving the reason -- an unexplained bypass is not a bypass
+    anyone can audit.
+
+    Whether a source names anything real is NOT decidable, here or anywhere in this
+    package, and nothing in this function claims it. See VV.md.
+    """
+    entries = [e for e in specification.get("provenance", []) if isinstance(e, dict)]
+    cited = {e.get("clause") for e in entries}
+    gaps = [
+        f"{label}:{clause} constrains but cites nothing"
+        for clause in PROVENANCE_CLAUSES
+        if specification.get(clause) is not None and clause not in cited
+    ]
+    for entry in entries:
+        clause = entry.get("clause")
+        # Types are checked rather than coerced: str(1) is a nonblank string, and the
+        # string "false" is truthy. A gate this easy to fool is not a gate.
+        unsourced = entry.get("unsourced", False)
+        if not isinstance(unsourced, bool):
+            gaps.append(
+                f"{label}:{clause} declares unsourced as {unsourced!r}, which is not a boolean"
+            )
+            continue
+        source = entry.get("source")
+        if not isinstance(source, str) or not source.strip():
+            # A declared absence of origin still owes a reason. An unexplained bypass is
+            # the one thing this objective exists to keep visible.
+            gaps.append(
+                f"{label}:{clause} declares itself unsourced but gives no reason"
+                if unsourced
+                else f"{label}:{clause} cites an empty source"
+            )
+            continue
+        source = source.strip()
+        if unsourced:
+            continue
+        named = next((d for d in REPO_DOCUMENTS if d in source), None)
+        if named:
+            gaps.append(
+                f"{label}:{clause} cites {named}, which explains this package rather "
+                'than being where the clause came from (use "unsourced": true if it '
+                "genuinely has no origin)"
+            )
+    return gaps
+
+
 def objective_provenance(domain: dict) -> dict:
-    """Validation gate: a clause that constrains must say where it came from."""
-    gaps = []
+    """An authoring rule with a lint: a clause that constrains must name where it came from.
+
+    Not a validation gate, whatever it may look like from the outside. It checks the
+    form of a citation, never that the citation names anything real. VV.md says why
+    that distinction is the whole point.
+    """
+    gaps: list[str] = []
     for path in sorted({c["spec"] for c in domain["cases"]}):
-        spec = load_spec(ROOT / path)
-        cited = {p.get("clause") for p in spec["specification"]["provenance"] if isinstance(p, dict)}
-        for clause in PROVENANCE_CLAUSES:
-            if spec["specification"][clause] is not None and clause not in cited:
-                gaps.append(f"{path}:{clause}")
+        gaps += provenance_gaps(path, load_spec(ROOT / path)["specification"])
     if gaps:
-        return fail("provenance", f"clauses constrain but cite no source: {gaps}")
-    return meet("provenance", "every non-null R and K clause cites a source")
+        return fail("provenance", "; ".join(gaps))
+    return meet(
+        "provenance",
+        "every non-null R and K clause names an origin, or declares it has none",
+    )
 
 
 def objective_declared_semantics(domain: dict) -> dict:
@@ -285,7 +399,7 @@ def run_domain(domain: dict) -> dict:
         objective_declared_semantics(domain),
         objective_outcome_coverage(domain),
         objective_tamper(domain),
-        objective_no_self_grading(domain),
+        objective_synthesize_emits_no_verdict(domain),
         objective_provenance(domain),
     ]
     return {
@@ -405,14 +519,56 @@ def hist(g) -> str:
     return out
 
 
+def _fact_value(value: Any) -> str:
+    """A witness field as the Lean side prints it: a list joined, a list of lists twice."""
+    if isinstance(value, list):
+        return ";".join(
+            ",".join(str(v) for v in item) if isinstance(item, list) else str(item)
+            for item in value
+        )
+    return "" if value is None else str(value)
+
+
+def effect_facts() -> dict[str, str]:
+    """What the package emits, read from the entry point that emits it.
+
+    `python_facts` recomputes quantities from kernel internals, so it and Lean agree
+    about the parts of a search. These run `check_search` on the spec files that
+    ship and read the certificate: the verdict, how settled it is, and why. That is
+    the effect. A kernel whose parts are each right and whose verdict is assembled
+    from them wrongly disagrees here and nowhere else.
+    """
+    out: dict[str, str] = {}
+    for name, relative, witness_keys in EFFECT_SPECS:
+        cert = check_search(ROOT / relative)
+        witness = cert["witness"]
+        out[f"verdict.{name}"] = (
+            f"{cert['verdict']}/{cert['optimality']}/{witness.get('reason', '')}"
+        )
+        for key in witness_keys:
+            out[f"verdict.{name}.{key}"] = _fact_value(witness.get(key))
+    return out
+
+
 def compare_facts(reported: dict[str, str], repeated: list[str]) -> dict:
     """Two implementations, one set of questions. Every fact must be compared.
 
+    The questions come in two bands: what the search finds (`python_facts`) and what
+    the checker then reports (`effect_facts`). Lean answers both from its own
+    enumeration, so agreement on the first does not buy agreement on the second.
+
     A fact reported twice is a failure even when both copies agree: the second
     would overwrite the first, so one file could quietly supply the value another
     file got wrong.
     """
     expected = python_facts()
+    effects = effect_facts()
+    claimed_twice = sorted(set(expected) & set(effects))
+    if claimed_twice:
+        # One name, two sources: the second would overwrite the first and the
+        # comparison would silently drop a question.
+        raise RuntimeError(f"fact name claimed by two sources: {claimed_twice}")
+    expected.update(effects)
     disagreements = [
         {"fact": k, "lean": reported.get(k), "python": v}
         for k, v in sorted(expected.items())
@@ -493,7 +649,8 @@ def run_lean(require: bool) -> dict:
     return {
         "status": "checked",
         "ok": all(r["ok"] for r in results) and cross["ok"],
-        "detail": "Lean corroborates the finite facts. It does not certify the Python kernel.",
+        "detail": "Lean corroborates the finite facts and the verdicts drawn from them. "
+        "It does not certify the Python kernel.",
         "files": results,
         "cross_check": cross,
     }
diff --git a/tests/test_vv.py b/tests/test_vv.py
index cdd44c5..40c22c8 100644
--- a/tests/test_vv.py
+++ b/tests/test_vv.py
@@ -6,6 +6,9 @@
 
 import importlib.util
 import json
+import os
+import subprocess
+import sys
 from pathlib import Path
 
 import pytest
@@ -26,6 +29,7 @@ def _load_runner():
 
 
 vv = _load_runner()
+provenance_gaps = vv.provenance_gaps
 CONFIG = json.loads((ROOT / "vv" / "domains.json").read_text(encoding="utf-8"))
 DOMAINS = CONFIG["domains"]
 IDS = [d["id"] for d in DOMAINS]
@@ -63,3 +67,183 @@ def test_domain_reaches_all_four_verdicts_and_the_adapter(domain):
     """Four verdicts plus adapter reject, in every domain. No domain gets a pass on one."""
     reached = {c["expect"]["outcome"] for c in domain["cases"]}
     assert reached >= vv.OUTCOMES, sorted(vv.OUTCOMES - reached)
+
+
+def _spec(provenance, *, k=None):
+    """A minimal specification carrying just the clauses the provenance rule reads."""
+    return {"R": {"phrase": "larger"}, "K": k, "provenance": provenance}
+
+
+def test_provenance_accepts_a_named_origin():
+    """A paper and a section is what a citation is supposed to look like."""
+    assert provenance_gaps("s", _spec([{"clause": "R", "source": "VCOS §8.1 Table 2"}])) == []
+
+
+def test_provenance_rejects_a_repo_document_as_an_origin():
+    """The gate exists because a citation that does not cite still looks like one.
+
+    Four specs in the first version of this matrix cited NONCLAIMS.md — which explains
+    why a zero budget yields UNKNOWN — as the source of the relation in R. A reviewer
+    caught it; the gate could not. Now it can.
+    """
+    gaps = provenance_gaps("s", _spec([{"clause": "R", "source": "NONCLAIMS.md §2"}]))
+    assert len(gaps) == 1
+    assert "NONCLAIMS.md" in gaps[0]
+
+
+def test_provenance_rejects_a_blank_source():
+    """Whitespace and a missing key are both the absence of a source, not a source."""
+    assert provenance_gaps("s", _spec([{"clause": "R", "source": "   "}])) != []
+    assert provenance_gaps("s", _spec([{"clause": "R"}])) != []
+
+
+def test_provenance_rejects_a_constraining_clause_that_cites_nothing():
+    """A K that constrains is as answerable for its origin as an R."""
+    gaps = provenance_gaps("s", _spec([{"clause": "R", "source": "VCOS §8.1"}], k={"inv": "x"}))
+    assert any("K constrains but cites nothing" in g for g in gaps)
+
+
+def test_provenance_allows_a_declared_absence_of_origin():
+    """`unsourced` is a bypass. It is meant to be one, and meant to be visible."""
+    entry = {"clause": "R", "unsourced": True, "source": "deliberately outside the declared set"}
+    assert provenance_gaps("s", _spec([entry])) == []
+
+
+def test_provenance_requires_a_reason_for_a_declared_absence():
+    """A bypass nobody can read the reason for is not the visible bypass VV.md claims.
+
+    The message must also say which rule failed: reporting "cites an empty source"
+    for a deliberately originless clause sends the author looking for the wrong fix.
+    """
+    gaps = provenance_gaps("s", _spec([{"clause": "R", "unsourced": True}]))
+    assert len(gaps) == 1
+    assert "unsourced but gives no reason" in gaps[0]
+
+
+def test_shipped_specs_carry_no_provenance_gaps():
+    """The rule is only worth having if what ships already obeys it."""
+    for path in sorted((ROOT / "vv" / "specs").glob("*.json")) + sorted(
+        (ROOT / "demos").glob("*/spec.json")
+    ):
+        spec = json.loads(path.read_text(encoding="utf-8"))
+        assert provenance_gaps(path.name, spec["specification"]) == []
+
+
+def test_provenance_rejects_a_non_string_source():
+    """`str(1)` is a nonblank string. Types are checked, not coerced."""
+    gaps = provenance_gaps("s", _spec([{"clause": "R", "source": 1}]))
+    assert len(gaps) == 1
+    assert "empty source" in gaps[0]
+
+
+def test_provenance_rejects_a_non_boolean_unsourced():
+    """The string "false" is truthy, and would otherwise wave a clause through."""
+    for value in ("false", 1, "yes", []):
+        entry = {"clause": "R", "unsourced": value, "source": "NONCLAIMS.md §2"}
+        gaps = provenance_gaps("s", _spec([entry]))
+        assert gaps, f"unsourced={value!r} slipped through"
+        assert "not a boolean" in gaps[0] or "NONCLAIMS.md" in gaps[0]
+
+
+def test_import_fallback_does_not_mask_a_broken_install(tmp_path):
+    """A missing submodule means the install is broken, not that it is absent.
+
+    Falling back to the checkout there would load working code over a broken
+    package and hide the breakage, so the runner re-raises instead.
+    """
+    # Mirror the real package: its __init__ imports a submodule. When that submodule
+    # is missing, Python purges `realize` from sys.modules, so a bare `sys.path`
+    # fallback would re-resolve to the checkout and report success over a broken
+    # install. A stub whose __init__ succeeds would not reproduce that.
+    stub = tmp_path / "realize"
+    stub.mkdir()
+    (stub / "__init__.py").write_text(
+        "from realize.verdicts import Verdict\n__version__ = 'stub'\n", encoding="utf-8"
+    )
+    env = dict(os.environ, PYTHONPATH=str(tmp_path))
+    proc = subprocess.run(
+        [sys.executable, str(ROOT / "scripts" / "vv.py"), "--domain", "encoder.finite_case_table"],
+        capture_output=True, text=True, cwd=ROOT, env=env, check=False,
+    )
+    assert proc.returncode != 0
+    assert "ModuleNotFoundError" in proc.stderr
+    assert "realize.verdicts" in proc.stderr
+
+
+# ---------------------------------------------------------------- the effect band
+
+
+def test_every_effect_fact_names_a_verdict_an_optimality_and_a_reason():
+    """The fact Lean is compared against must carry all three, or it compares less."""
+    verdicts = {"PASS", "COUNTEREXAMPLE", "UNSAT", "UNKNOWN"}
+    optimalities = {"proved", "unresolved", "not_requested"}
+    facts = vv.effect_facts()
+    named = [k for k in facts if k.count(".") == 1]
+    assert len(named) == len(vv.EFFECT_SPECS)
+    for key in named:
+        verdict, optimality, reason = facts[key].split("/")
+        assert verdict in verdicts, key
+        assert optimality in optimalities, key
+        assert reason, f"{key} reports no reason"
+
+
+def test_every_shipped_spec_is_cross_checked():
+    """A spec nobody corroborates is a claim nobody has read twice.
+
+    This is the ratchet: add a spec to `vv/specs/` or `demos/` and this fails until
+    a Lean file derives the verdict it should draw.
+    """
+    shipped = {p.relative_to(ROOT).as_posix() for p in ROOT.glob("vv/specs/*.spec.json")}
+    shipped |= {p.relative_to(ROOT).as_posix() for p in ROOT.glob("demos/*/spec.json")}
+    covered = {relative for _name, relative, _keys in vv.EFFECT_SPECS}
+    assert shipped - covered == set(), "shipped but never cross-checked"
+    assert covered - shipped == set(), "cross-checked but no longer shipped"
+
+
+def test_effect_facts_come_from_the_entry_point_not_from_the_kernel():
+    """Both bands must be answered, and neither may stand in for the other."""
+    parts = vv.python_facts()
+    effects = vv.effect_facts()
+    assert not set(parts) & set(effects)
+    assert all(k.startswith("verdict.") for k in effects)
+    assert not any(k.startswith("verdict.") for k in parts)
+
+
+def test_compare_facts_refuses_two_sources_for_one_name(monkeypatch):
+    """A collision would let one band overwrite the other and drop a question."""
+    monkeypatch.setattr(vv, "python_facts", lambda: {"verdict.max_formula": "x"})
+    with pytest.raises(RuntimeError, match="claimed by two sources"):
+        vv.compare_facts({}, [])
+
+
+def test_compare_facts_catches_a_verdict_that_lean_derives_differently():
+    """The disagreement the band exists for: right parts, wrong verdict.
+
+    The stand-in reason is one no branch of the checker can produce. Naming a real
+    alternative would tie this test to the checker's wording, so a kernel that drifted
+    onto that wording would turn the test green for the wrong reason.
+    """
+    agreed = {**vv.python_facts(), **vv.effect_facts()}
+    agreed["verdict.grid_preserve_histogram"] = "UNSAT/proved/no_branch_reports_this"
+    result = vv.compare_facts(agreed, [])
+    assert not result["ok"]
+    assert [row["fact"] for row in result["disagreements"]] == ["verdict.grid_preserve_histogram"]
+
+
+def test_fact_value_renders_a_list_of_sets_the_way_lean_prints_it():
+    """`obstructions` is a list of subsets; flattening it would compare the wrong thing."""
+    assert vv._fact_value([[0, 1, 2]]) == "0,1,2"
+    assert vv._fact_value([[0, 1], [1, 2]]) == "0,1;1,2"
+    assert vv._fact_value(["separate_all"]) == "separate_all"
+    assert vv._fact_value(None) == ""
+    assert vv._fact_value(3) == "3"
+
+
+def test_verdict_keys_finds_a_grade_nested_anywhere():
+    """The shallow check this replaced waved `{"metadata": {"verdict": ...}}` through."""
+    assert vv.verdict_keys({"candidates": [], "exhausted": True}) == []
+    assert vv.verdict_keys({"verdict": "PASS"}) == ["verdict"]
+    assert vv.verdict_keys({"candidates": [{"verdict": "PASS"}]}) == ["candidates[0].verdict"]
+    assert vv.verdict_keys({"metadata": {"verdict": "PASS"}}) == ["metadata.verdict"]
+    assert vv.verdict_keys({"a": [{"b": {"verdict": "PASS"}}]}) == ["a[0].b.verdict"]
+    assert vv.verdict_keys({"verdict": {"verdict": "PASS"}}) == ["verdict", "verdict.verdict"]
diff --git a/vv/README.md b/vv/README.md
index b34ebbd..8fdc8a0 100644
--- a/vv/README.md
+++ b/vv/README.md
@@ -26,7 +26,10 @@ grammar — `grammar_coverage` will fail until you do.
 1. Add the grammar to `GRAMMARS` in `src/realize/verdicts.py` and to `schema/realize.v0.json`.
 2. Add a domain entry to `domains.json` with cases reaching all five outcomes: `PASS`,
    `COUNTEREXAMPLE`, `UNSAT`, `UNKNOWN`, adapter reject. `outcome_coverage` will fail until you do.
-3. Write the specs under `specs/` with `provenance` for every clause that constrains.
+3. Write the specs under `specs/` with `provenance` for every clause that constrains. A
+   source names where the clause came from — a paper, a section. This repository's own
+   documents are not origins; a clause that genuinely has none says so with
+   `"unsourced": true` and explains why.
 4. Write the candidates under `candidates/`, each carrying the spec's digest.
 5. Add a Lean file under `lean/` re-stating that domain's finite facts.
 
diff --git a/vv/lean/Encoder.lean b/vv/lean/Encoder.lean
index 3b09331..f8554f5 100644
--- a/vv/lean/Encoder.lean
+++ b/vv/lean/Encoder.lean
@@ -1,8 +1,11 @@
 /-
   Cross-check for the `encoder.finite_case_table` domain (VCMS Example 4.3).
 
-  Lean agrees or disagrees with the finite facts the Python kernel reports.
-  It does not certify the Python kernel, and it cannot mint a verdict.
+  Lean agrees or disagrees with the finite facts the Python kernel reports, and with
+  the verdict it reports for each spec that ships in this domain.
+
+  It does not certify the Python kernel, and it cannot mint a verdict: working out
+  what a verdict has to be is not issuing one.
 -/
 
 namespace Realize.Encoder
@@ -87,4 +90,72 @@ def showList (l : List Nat) : String := String.intercalate "," (l.map toString)
 #eval IO.println s!"fact encoder.pair_12={showList (inter (A 1) (A 2))}"
 #eval IO.println s!"fact encoder.pair_02={showList (inter (A 0) (A 2))}"
 
+/-! ## What the checker has to report
+
+    Everything above is a quantity found *inside* the search. These are the effect:
+    the verdict `realize.checker.check_search` must emit for a spec file that ships
+    in this repository. `scripts/vv.py` runs the real entry point on the real file
+    and compares the two.
+
+    The branch order below is the checker's, transcribed. The numbers fed to it are
+    computed here. -/
+
+def subsetsOf : List Nat → List (List Nat)
+  | [] => [[]]
+  | x :: rest => (subsetsOf rest).flatMap (fun s => [s, x :: s])
+
+/-- Subsets shortest first, matching the order the Python side walks them in. -/
+def bySize (l : List Nat) : List (List Nat) :=
+  (List.range (l.length + 1)).flatMap (fun k => (subsetsOf l).filter (fun s => s.length == k))
+
+def covers (a b : List Nat) : Bool := a.all (fun x => b.contains x)
+
+/-- Inclusion-minimal B ⊆ dom whose acceptable sets have nothing in common.
+    This is the content of the UNSAT, not just its name. -/
+def obstructions : List (List Nat) :=
+  (bySize dom).foldl
+    (fun acc b =>
+      if b.isEmpty || acc.any (fun p => covers p b) then acc
+      else if (interAll (b.map A)).isEmpty then acc ++ [b] else acc)
+    []
+
+/-- The encoders `demos/three_state/spec.json` and `vv/specs/encoder_separating.spec.json`
+    put in the library, in file order. -/
+def library : List (String × (Nat → Nat)) :=
+  [("collapse_all", collapseAll), ("separate_all", separateAll)]
+
+def adequateIds (lib : List (String × (Nat → Nat))) : List String :=
+  (lib.filter (fun e => adequate e.2)).map (·.1)
+
+/-- What `_search_encoder` reports, given how many encoders it may read and how many hold. -/
+def searchVerdict (budget nEncoders nAdequate : Nat) : String :=
+  if budget == 0 then "UNKNOWN/unresolved/zero_budget"
+  else if nEncoders > budget then "UNKNOWN/unresolved/incomplete_coverage"
+  else if nAdequate == 0 then "UNSAT/proved/no_adequate_encoder"
+  else "UNKNOWN/proved/realizations_exist_supply_a_candidate"
+
+/-- `demos/three_state/spec.json`: one encoder is offered, and it collapses. -/
+def threeState : String :=
+  searchVerdict 100 1 (adequateIds [("collapse_all", collapseAll)]).length
+
+/-- `vv/specs/encoder_separating.spec.json`: the same R, with a separating encoder offered. -/
+def separating : String := searchVerdict 100 library.length (adequateIds library).length
+
+/-- `vv/specs/encoder_zero_budget.spec.json`: nothing may be read, so nothing is settled. -/
+def zeroBudget : String := searchVerdict 0 1 0
+
+theorem three_state_verdict : threeState = "UNSAT/proved/no_adequate_encoder" := by decide
+theorem separating_verdict :
+    separating = "UNKNOWN/proved/realizations_exist_supply_a_candidate" := by decide
+theorem zero_budget_verdict : zeroBudget = "UNKNOWN/unresolved/zero_budget" := by decide
+theorem obstruction_is_the_triple : obstructions = [[0, 1, 2]] := by decide
+
+def showSets (l : List (List Nat)) : String := String.intercalate ";" (l.map showList)
+
+#eval IO.println s!"fact verdict.three_state={threeState}"
+#eval IO.println s!"fact verdict.three_state.obstructions={showSets obstructions}"
+#eval IO.println s!"fact verdict.encoder_separating={separating}"
+#eval IO.println s!"fact verdict.encoder_separating.adequate_encoders={String.intercalate ";" (adequateIds library)}"
+#eval IO.println s!"fact verdict.encoder_zero_budget={zeroBudget}"
+
 end Realize.Encoder
diff --git a/vv/lean/Formula.lean b/vv/lean/Formula.lean
index cf9f39f..6fd14a7 100644
--- a/vv/lean/Formula.lean
+++ b/vv/lean/Formula.lean
@@ -1,8 +1,11 @@
 /-
   Cross-check for the `formula.bounded_coeff_template` domain (VCOS §8.1 / Table 2).
 
-  Lean agrees or disagrees with the finite facts the Python kernel reports.
-  It does not certify the Python kernel, and it cannot mint a verdict.
+  Lean agrees or disagrees with the finite facts the Python kernel reports, and with
+  the verdict it reports for each spec that ships in this domain.
+
+  It does not certify the Python kernel, and it cannot mint a verdict: working out
+  what a verdict has to be is not issuing one.
 
   Every coefficient in D = {-1, -1/2, 0, 1/2, 1} is a whole number of halves, so
   the template is carried here in halves: `h` stands for the value `h/2`. That
@@ -94,4 +97,48 @@ def showHalves (cs : List Coeffs) : String :=
 #eval IO.println s!"fact formula.midpoint_solution={showHalves (solutions .midpoint)}"
 #eval IO.println s!"fact formula.absdiff_solution={showHalves (solutions .absdiff)}"
 
+/-! ## What the checker has to report
+
+    Everything above is a quantity found *inside* the search. These are the effect:
+    the verdict `realize.checker.check_search` must emit for a spec file that ships
+    in this repository. `scripts/vv.py` runs the real entry point on the real file
+    and compares the two.
+
+    The branch order below is the checker's, transcribed. The numbers fed to it are
+    computed here. A kernel whose parts are each right and whose verdict is assembled
+    from them wrongly disagrees here and nowhere else. -/
+
+/-- What `_search_formula` reports, as a function of what the search finds.
+    `known` is whether R names a phrase the checker recognizes. -/
+def searchVerdict (budget card nValid : Nat) (known : Bool) : String :=
+  if budget == 0 then "UNKNOWN/unresolved/zero_budget"
+  else if !known then "UNKNOWN/unresolved/unrecognized_phrase"
+  else if card > budget then "UNKNOWN/unresolved/incomplete_coverage"
+  else if nValid == 0 then "UNSAT/proved/empty_template"
+  else "UNKNOWN/proved/realizations_exist_supply_a_candidate"
+
+/-- `demos/max_formula/spec.json`: phrase `larger`, whole template, budget 10000. -/
+def maxFormula : String :=
+  searchVerdict 10000 template.length (solutions .larger).length true
+
+/-- `vv/specs/formula_affine_only.spec.json`: the `|a-b|` leg is withdrawn. -/
+def affineOnly : String :=
+  searchVerdict 10000 affine.length (affine.filter (realizes · .larger)).length true
+
+/-- `vv/specs/formula_unrecognized_phrase.spec.json`: R names `mostly_bigger_ish`. -/
+def unrecognizedPhrase : String := searchVerdict 10000 template.length 0 false
+
+theorem max_formula_verdict :
+    maxFormula = "UNKNOWN/proved/realizations_exist_supply_a_candidate" := by decide
+theorem affine_only_verdict : affineOnly = "UNSAT/proved/empty_template" := by decide
+theorem unrecognized_verdict :
+    unrecognizedPhrase = "UNKNOWN/unresolved/unrecognized_phrase" := by decide
+
+#eval IO.println s!"fact verdict.max_formula={maxFormula}"
+#eval IO.println s!"fact verdict.max_formula.universe={template.length}"
+#eval IO.println s!"fact verdict.max_formula.n_valid={(solutions .larger).length}"
+#eval IO.println s!"fact verdict.formula_affine_only={affineOnly}"
+#eval IO.println s!"fact verdict.formula_affine_only.universe={affine.length}"
+#eval IO.println s!"fact verdict.formula_unrecognized_phrase={unrecognizedPhrase}"
+
 end Realize.Formula
diff --git a/vv/lean/Grid.lean b/vv/lean/Grid.lean
index 5b523cc..2a51f1b 100644
--- a/vv/lean/Grid.lean
+++ b/vv/lean/Grid.lean
@@ -1,8 +1,11 @@
 /-
   Cross-check for the `term_series.typed_grid` domain (IGVF-CTS §7.1).
 
-  Lean agrees or disagrees with the finite facts the Python kernel reports.
-  It does not certify the Python kernel, and it cannot mint a verdict.
+  Lean agrees or disagrees with the finite facts the Python kernel reports, and with
+  the verdict it reports for each spec that ships in this domain.
+
+  It does not certify the Python kernel, and it cannot mint a verdict: working out
+  what a verdict has to be is not issuing one.
 -/
 
 namespace Realize.Grid
@@ -61,4 +64,98 @@ def showHist (g : Grid) : String :=
 #eval IO.println s!"fact grid.hist_input={showHist X}"
 #eval IO.println s!"fact grid.hist_goal={showHist (goal X)}"
 
+/-! ## What the checker has to report
+
+    Everything above is a quantity found *inside* the search. These are the effect:
+    the verdict `realize.checker.check_search` must emit for a spec file that ships
+    in this repository. `scripts/vv.py` runs the real entry point on the real file
+    and compares the two.
+
+    The branch order below is the checker's, transcribed. The class is enumerated
+    here rather than assumed: the checker reports `realizations_exist` only after
+    walking every term the grammar can name, so Lean walks them too. -/
+
+inductive Op where
+  | extractOp | render2Op
+deriving DecidableEq, Repr, BEq
+
+inductive Ty where
+  | grid | mask
+deriving DecidableEq, Repr, BEq
+
+def ops : List Op := [.extractOp, .render2Op]
+
+def sig : Op → Ty × Ty
+  | .extractOp => (.grid, .mask)
+  | .render2Op => (.mask, .grid)
+
+def ofLength : Nat → List (List Op)
+  | 0 => [[]]
+  | n + 1 => (ofLength n).flatMap (fun s => ops.map (fun o => s ++ [o]))
+
+/-- Every term the grammar can name up to `bound.max_term_size` = 4. -/
+def terms : List (List Op) := (List.range 5).flatMap ofLength
+
+/-- `compose.type_of_prefix`: a term's type, or none where a step does not fit. -/
+def typeOf : List Op → Option (Ty × Ty)
+  | [] => some (.grid, .grid)
+  | o :: rest =>
+      rest.foldl
+        (fun acc o' =>
+          match acc with
+          | none => none
+          | some (i, out) =>
+              let s := sig o'
+              if s.1 == out then some (i, s.2) else none)
+        (some (sig o))
+
+def apply : Op → Grid → Grid
+  | .extractOp => extract
+  | .render2Op => render2
+
+/-- Ill-typed terms and terms that are not `Grid → Grid` produce nothing to judge. -/
+def evalTerm (t : List Op) (g : Grid) : Option Grid :=
+  match typeOf t with
+  | some (.grid, .grid) => some (t.foldl (fun acc o => apply o acc) g)
+  | _ => none
+
+/-- R: the output is the recolouring, and it moved no cell on or off. -/
+def meetsR (x y : Grid) : Bool := y == goal x && extract y == extract x
+
+def valid (x : Grid) : List (List Op) :=
+  terms.filter (fun t => match evalTerm t x with
+                         | none => false
+                         | some y => meetsR x y)
+
+/-- What `_search_grid` reports. `histogramBlocks` is K's pre-check, which runs first. -/
+def searchVerdict (budget card nValid : Nat) (histogramBlocks : Bool) : String :=
+  if budget == 0 then "UNKNOWN/unresolved/zero_budget"
+  else if histogramBlocks then "UNSAT/proved/histogram_contradicts_R"
+  else if card > budget then "UNKNOWN/unresolved/incomplete_coverage"
+  else if nValid == 0 then "UNSAT/proved/no_typed_realization"
+  else "UNKNOWN/proved/realizations_exist_supply_a_candidate"
+
+/-- `demos/grid_recolor/spec.json`: K is null, so nothing blocks the search. -/
+def recolor : String := searchVerdict 100 terms.length (valid X).length false
+
+/-- `vv/specs/grid_preserve_histogram.spec.json`: K asks the colour counts to be kept. -/
+def preserveHistogram : String :=
+  searchVerdict 100 terms.length (valid X).length (histogram X != histogram (goal X))
+
+/-- `vv/specs/grid_zero_budget.spec.json`. -/
+def zeroBudget : String := searchVerdict 0 terms.length 0 false
+
+theorem term_count : terms.length = 31 := by decide
+theorem two_terms_realize : (valid X).length = 2 := by decide
+theorem recolor_verdict :
+    recolor = "UNKNOWN/proved/realizations_exist_supply_a_candidate" := by decide
+theorem preserve_histogram_verdict :
+    preserveHistogram = "UNSAT/proved/histogram_contradicts_R" := by decide
+theorem zero_budget_verdict : zeroBudget = "UNKNOWN/unresolved/zero_budget" := by decide
+
+#eval IO.println s!"fact verdict.grid_recolor={recolor}"
+#eval IO.println s!"fact verdict.grid_recolor.n_valid={(valid X).length}"
+#eval IO.println s!"fact verdict.grid_preserve_histogram={preserveHistogram}"
+#eval IO.println s!"fact verdict.grid_zero_budget={zeroBudget}"
+
 end Realize.Grid
diff --git a/vv/lean/README.md b/vv/lean/README.md
index f9a2c2b..62fc763 100644
--- a/vv/lean/README.md
+++ b/vv/lean/README.md
@@ -1,14 +1,15 @@
 # vv/lean — independent corroboration
 
-Four files. Each re-states the finite facts of one domain in Lean 4 and proves them with
+Four files. Each re-states the finite facts of one domain in Lean 4, derives from them what verdict
+the checker has to report for the specs that ship in that domain, and proves both with
 kernel-checked `decide`.
 
-| File | Domain | What it settles |
-|---|---|---|
-| `Formula.lean` | `formula.bounded_coeff_template` | the template has 625 members; each phrase is realized by exactly one tuple; the affine sub-template is empty for `larger` |
-| `Encoder.lean` | `encoder.finite_case_table` | the collapsing encoder's one fibre is obstructed while every pair still meets; the separating encoder is adequate and its decoder is sound |
-| `Series.lean` | `term_series.guarded_integer_sequence` | 121 and 31 syntactic series; ten reach 7 and none in under three steps; the even repertoire and the above-cap target are both empty |
-| `Grid.lean` | `term_series.typed_grid` | `Extract` then `Render2` meets `R`; the empty series does not; the histogram of the input and of the goal differ |
+| File | Domain | Facts it settles | Verdicts it derives |
+|---|---|---|---|
+| `Formula.lean` | `formula.bounded_coeff_template` | the template has 625 members; each phrase is realized by exactly one tuple; the affine sub-template is empty for `larger` | `max_formula`, `formula_affine_only`, `formula_unrecognized_phrase` |
+| `Encoder.lean` | `encoder.finite_case_table` | the collapsing encoder's one fibre is obstructed while every pair still meets; the separating encoder is adequate and its decoder is sound; `{0,1,2}` is the one inclusion-minimal obstruction | `three_state`, `encoder_separating`, `encoder_zero_budget` |
+| `Series.lean` | `term_series.guarded_integer_sequence` | 121 and 31 syntactic series; ten reach 7 and none in under three steps; the even repertoire and the above-cap target are both empty | `series_seven`, `series_even_repertoire`, `series_target_nine`, `series_zero_budget` |
+| `Grid.lean` | `term_series.typed_grid` | `Extract` then `Render2` meets `R`; the empty series does not; the histogram of the input and of the goal differ; 2 of the 31 terms realize `R` | `grid_recolor`, `grid_preserve_histogram`, `grid_zero_budget` |
 
 ## Ground rules
 
@@ -26,15 +27,32 @@ of halves, so `h` stands for the value `h/2`. That keeps the arithmetic exact wi
 
 Proving something in Lean corroborates nothing on its own — two implementations drift apart quite
 happily when nobody compares them. So each file ends with `#eval IO.println "fact <name>=<value>"`
-lines reporting the quantities it settled. `scripts/vv.py` recomputes all 29 from the Python kernel
-and compares them. A disagreement fails the run, and so does a fact that stops being reported.
+lines reporting what it settled, and `scripts/vv.py` answers the same questions from Python and
+compares. A disagreement fails the run, and so does a fact that stops being reported.
 
-This is the check that bites when a frozen count in `tests/test_counts.py` is edited to match a
-drifting kernel. The Python suite cannot catch that, because the suite is the thing that was edited.
+The 51 facts come in two bands:
+
+- **the parts** (29, named `formula.*`, `encoder.*`, `series.*`, `grid.*`) — quantities found inside
+  a search. Python answers these in `python_facts()`, recomputing from kernel internals. This is the
+  band that bites when a frozen count in `tests/test_counts.py` is edited to match a drifting
+  kernel; the Python suite cannot catch that, because the suite is the thing that was edited.
+- **the effect** (22, named `verdict.*`) — the verdict, optimality and reason the checker has to
+  report for a spec file that ships, as `VERDICT/optimality/reason`. Lean works it out from the
+  branch order in `realize.checker`, applied to numbers it computed itself. Python answers it in
+  `effect_facts()` by running `check_search` on the real spec file and reading the certificate.
+
+The second band is the one that catches a kernel whose parts are each right and whose verdict is
+assembled from them wrongly — a mis-ordered branch, a wrong verdict constant, an exhaustive result
+reported as unresolved. `vv/domains.json` records outcome and exit status, so a fault that keeps
+both and changes only the reason is invisible to it.
 
 Facts are derived, not written down: `series.witness` asks Lean to enumerate and take the shortest
-valid series rather than restating a known answer, so the two sides have to agree about the
-enumeration as well as the result.
+valid series rather than restating a known answer, and `Grid.lean` walks all 31 terms the grammar
+can name rather than assuming the two that work. The two sides have to agree about the enumeration
+as well as the result.
+
+Every spec that ships is covered: `tests/test_vv.py` fails when a file lands in `vv/specs/` or
+`demos/` that no Lean file derives a verdict for.
 
 ## Run
 
@@ -50,5 +68,11 @@ Toolchain is pinned in `lean-toolchain`. Install with
 ## What this is not
 
 Lean does not verify the Python kernel, the CLI, the CI, or the papers' mathematics, and **a Lean
-file cannot mint a verdict**. If Lean and Python disagree, the V&V job goes red and one of them is
-wrong. The job does not say which. See [../../NONCLAIMS.md](../../NONCLAIMS.md) §10.
+file cannot mint a verdict** — nothing here sits on the path that produces a certificate. Deriving
+what a verdict *has to be* is not issuing one.
+
+Lean also does not read the spec files. Each spec is transcribed into Lean by hand — `budget 10000`,
+`cap 8`, `target 7` — so the comparison catches an edit to one side and not a matching edit to both.
+
+If Lean and Python disagree, the V&V job goes red and one of them is wrong. The job does not say
+which. See [../../NONCLAIMS.md](../../NONCLAIMS.md) §10.
diff --git a/vv/lean/Series.lean b/vv/lean/Series.lean
index 7e2c2d5..79685ad 100644
--- a/vv/lean/Series.lean
+++ b/vv/lean/Series.lean
@@ -1,8 +1,11 @@
 /-
   Cross-check for the `term_series.guarded_integer_sequence` domain (VCOS §8.3).
 
-  Lean agrees or disagrees with the finite facts the Python kernel reports.
-  It does not certify the Python kernel, and it cannot mint a verdict.
+  Lean agrees or disagrees with the finite facts the Python kernel reports, and with
+  the verdict it reports for each spec that ships in this domain.
+
+  It does not certify the Python kernel, and it cannot mint a verdict: working out
+  what a verdict has to be is not issuing one.
 
   This is the grammar that shipped no spec before `vv/specs/series_seven.spec.json`.
 -/
@@ -85,4 +88,54 @@ def minValid : List (List Op) :=
 
 #eval IO.println s!"fact series.witness={showSeq (minValid.headD [])}"
 
+/-! ## What the checker has to report
+
+    Everything above is a quantity found *inside* the search. These are the effect:
+    the verdict `realize.checker.check_search` must emit for a spec file that ships
+    in this repository. `scripts/vv.py` runs the real entry point on the real file
+    and compares the two.
+
+    The branch order below is the checker's, transcribed. The numbers fed to it are
+    computed here. `_search_series` also refuses a negative target; `Nat` cannot
+    name one, so that branch is not modelled and not claimed. -/
+
+/-- What `_search_series` reports, given the guard, the class size and what it finds. -/
+def searchVerdict (budget cap target card nValid : Nat) : String :=
+  if budget == 0 then "UNKNOWN/unresolved/zero_budget"
+  else if target > cap then "UNSAT/proved/target_outside_invariant"
+  else if card > budget then "UNKNOWN/unresolved/incomplete_coverage"
+  else if nValid == 0 then "UNSAT/proved/no_valid_sequence"
+  else "UNKNOWN/proved/realizations_exist_supply_a_candidate"
+
+/-- `vv/specs/series_seven.spec.json`. -/
+def seven : String :=
+  searchVerdict 10000 8 7 (upTo repertoire 4).length (valid repertoire 8 7 4).length
+
+/-- `vv/specs/series_even_repertoire.spec.json`: 7 is odd and the steps are not. -/
+def evenRepertoireSpec : String :=
+  searchVerdict 10000 8 7 (upTo evenRepertoire 4).length (valid evenRepertoire 8 7 4).length
+
+/-- `vv/specs/series_target_nine.spec.json`: R asks for a state the invariant forbids. -/
+def targetNine : String :=
+  searchVerdict 10000 8 9 (upTo repertoire 4).length (valid repertoire 8 9 4).length
+
+/-- `vv/specs/series_zero_budget.spec.json`. -/
+def zeroBudget : String := searchVerdict 0 8 7 0 0
+
+theorem seven_verdict :
+    seven = "UNKNOWN/proved/realizations_exist_supply_a_candidate" := by decide
+theorem even_repertoire_verdict :
+    evenRepertoireSpec = "UNSAT/proved/no_valid_sequence" := by decide
+theorem target_nine_verdict :
+    targetNine = "UNSAT/proved/target_outside_invariant" := by decide
+theorem zero_budget_verdict : zeroBudget = "UNKNOWN/unresolved/zero_budget" := by decide
+
+#eval IO.println s!"fact verdict.series_seven={seven}"
+#eval IO.println s!"fact verdict.series_seven.n_valid={(valid repertoire 8 7 4).length}"
+#eval IO.println s!"fact verdict.series_seven.min_len={((valid repertoire 8 7 4).map List.length).min?.getD 0}"
+#eval IO.println s!"fact verdict.series_even_repertoire={evenRepertoireSpec}"
+#eval IO.println s!"fact verdict.series_even_repertoire.n_valid={(valid evenRepertoire 8 7 4).length}"
+#eval IO.println s!"fact verdict.series_target_nine={targetNine}"
+#eval IO.println s!"fact verdict.series_zero_budget={zeroBudget}"
+
 end Realize.Series
diff --git a/vv/specs/formula_unrecognized_phrase.spec.json b/vv/specs/formula_unrecognized_phrase.spec.json
index 87e3aec..af8241f 100644
--- a/vv/specs/formula_unrecognized_phrase.spec.json
+++ b/vv/specs/formula_unrecognized_phrase.spec.json
@@ -10,7 +10,13 @@
     "K": null,
     "preferences": [],
     "evidence_mode": "exhaustive_finite",
-    "provenance": [{"clause": "R", "source": "no source: the phrase is deliberately outside the declared set (NONCLAIMS.md §1)"}]
+    "provenance": [
+      {
+        "clause": "R",
+        "unsourced": true,
+        "source": "the phrase is deliberately outside the declared set; NONCLAIMS.md §1 refuses to invent an R for it"
+      }
+    ]
   },
   "library": {
     "encoders": [],