Cross-check the verdicts, not just the arithmetic; close the lint debt

.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

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.

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
 ```
 

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.

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] = []