feat(tri): census audit says what it does not check, and why

.claude/skills/ci-gates/SKILL.md

@@ -9581,3 +9581,46 @@ file, not the crate") does not hold when the single file is a root.
 --stat` before every commit: five unrelated files is not a thing you notice in
 the test output, and on a shared repository it is somebody else's conflict
 tomorrow.
+
+## 382. A matcher-defined population cannot be counted twice
+
+Two candidates for a second opinion were measured and refused, and the refusals
+name a rule the three working rows had been obeying by luck.
+
+`types dup` prints **1180** struct definitions. A counter loose enough to be
+independent reads **1182**, and the two extra are
+
+```
+specs/lsp/schema.t27:155   struct = 21,
+specs/lsp/schema.t27:204   struct = 22,
+```
+
+enum members *named* `struct`, which the census correctly rejects by requiring
+the name to start with an ascii letter. **The census is right.** Any counter
+accurate enough to agree with it is a copy of its matcher -- exactly why the
+`seals hollow` row was removed one pass earlier, where both sides tested the
+same json field and a planted seal moved both numbers.
+
+> **A census whose population is defined by a MATCHER cannot have an independent
+> counter, because any counter precise enough to agree IS that matcher. Only a
+> population defined by something EXTERNAL -- files on disk, workspace members,
+> a marker in a different file -- can honestly be counted twice.**
+
+The rows that work obey it: `.t27` on disk, `.rs` under the cargo workspace, the
+bare letters of a keyword, `theorem` lines in a file the census reads for
+something else. Before building a differential row, ask what defines its
+population. If the answer is "the code under test", stop.
+
+## 383. An exclusion is a measurement, not a shrug
+
+Having refused two rows, the audit had three green rows and no statement of what
+it was not checking -- its own coverage in exactly the shape it exists to catch.
+It now prints the uncovered censuses with the measurement behind each: what was
+tried, what it read, and why the two routes cannot disagree.
+
+Enforced rather than intended: a test refuses a census that appears in both
+lists, and refuses a reason shorter than sixty characters. `"too hard"` fails.
+
+The distinction being preserved is the one this whole document keeps circling:
+a reader must be able to tell **"looked and could not"** from **"never looked"**,
+and a blank space says the second while meaning the first.

cli/tri/src/census.rs

@@ -61,7 +61,7 @@ struct Row {
     reading: &'static str,
 }
 
-const ROWS: [Row; 3] = [
+const ROWS: [Row; 4] = [
     Row {
         census: "unparsed report",
         args: &["unparsed", "report"],
@@ -89,6 +89,48 @@ const ROWS: [Row; 3] = [
         soft: false,
         reading: "the census walked a list; this walks the cargo workspace",
     },
+    Row {
+        census: "lean vacuous",
+        args: &["lean", "vacuous"],
+        marker: "models in the file",
+        nth: 0,
+        what: "`theorem` lines in Completeness.lean",
+        soft: false,
+        reading: "the census counts `def NAME : Module := {`; this counts the theorems, \
+                  one per model, and a hand-transcribed file can gain either without the other",
+    },
+];
+
+/// A census this audit does NOT check, and the reason.
+///
+/// Without this list the audit is narrow in exactly the way it exists to
+/// catch: a page of green rows looks like coverage until somebody asks what is
+/// not on it. Each entry is a measurement, not a shrug.
+struct Uncovered {
+    census: &'static str,
+    why: &'static str,
+}
+
+const UNCOVERED: [Uncovered; 3] = [
+    Uncovered {
+        census: "seals hollow",
+        why: "built and removed. Its counter tested json text for `\"spec_path\"` while the \
+              census parses that same field, so planting one more seal moved BOTH numbers \
+              to 1314 and the row stayed green. No input makes them disagree.",
+    },
+    Uncovered {
+        census: "types dup",
+        why: "measured: a counter loose enough to be independent reads 1182 where the census \
+              reads 1180, and the two extra are `struct = 21,` -- enum members named `struct`, \
+              which the census correctly rejects. Any counter accurate enough to agree is a \
+              copy of its matcher.",
+    },
+    Uncovered {
+        census: "discard classify",
+        why: "its population is parser events produced at run time, not artefacts on disk. \
+              Counting them a second way means running the same parser, which is not a \
+              second opinion.",
+    },
 ];
 
 /// Every number on a line, in order.
@@ -282,10 +324,45 @@ fn independent(census: &str, repo: &Path) -> Result<usize> {
             }
             Ok(n)
         }
+        "lean vacuous" => {
+            // A different marker for the same population: the census counts
+            // `def NAME : Module := {`, this counts the theorem each model is
+            // supposed to carry. The file is found by name rather than by the
+            // path the census uses.
+            let mut v = Vec::new();
+            walk(&repo.join("proofs"), "Completeness.lean", &mut v);
+            let p = v.first().ok_or_else(|| {
+                anyhow::anyhow!("no Completeness.lean under proofs/ -- nothing to count")
+            })?;
+            let src = std::fs::read_to_string(p)?;
+            Ok(src
+                .lines()
+                .filter(|l| l.trim_start().starts_with("theorem "))
+                .count())
+        }
         other => anyhow::bail!("no independent counter for {other}"),
     }
 }
 
+/// Break a sentence into lines of at most `w` characters, on word boundaries.
+fn wrap(s: &str, w: usize) -> Vec<String> {
+    let mut out = Vec::new();
+    let mut cur = String::new();
+    for word in s.split_whitespace() {
+        if !cur.is_empty() && cur.len() + 1 + word.len() > w {
+            out.push(std::mem::take(&mut cur));
+        }
+        if !cur.is_empty() {
+            cur.push(' ');
+        }
+        cur.push_str(word);
+    }
+    if !cur.is_empty() {
+        out.push(cur);
+    }
+    out
+}
+
 fn repo_root() -> Result<PathBuf> {
     let out = std::process::Command::new("git")
         .args(["rev-parse", "--show-toplevel"])
@@ -369,6 +446,16 @@ pub fn run(cmd: &CensusCmd) -> Result<()> {
         );
     }
     println!("  AGREED. Every census speaks about the population it prints.");
+    println!();
+    println!("  Not checked here, and why -- because a page of green rows looks");
+    println!("  like coverage until somebody asks what is missing from it:");
+    for u in &UNCOVERED {
+        println!();
+        println!("      {}", u.census);
+        for chunk in wrap(u.why, 68) {
+            println!("          {chunk}");
+        }
+    }
     Ok(())
 }
 
@@ -422,6 +509,41 @@ mod tests {
         }
     }
 
+    /// A census is either checked or explicitly not, never neither.
+    ///
+    /// The audit's own coverage is the same class it exists to catch: a page
+    /// of green rows looks like the whole story. A name in both lists, or an
+    /// exclusion with no measurement behind it, puts it back there.
+    #[test]
+    fn nothing_is_both_checked_and_excused() {
+        for u in &UNCOVERED {
+            assert!(
+                !ROWS.iter().any(|r| r.census == u.census),
+                "{} is listed as unchecked and also has a row",
+                u.census
+            );
+            assert!(
+                u.why.len() > 60,
+                "{}: an exclusion is a measurement, not a shrug -- {:?}",
+                u.census,
+                u.why
+            );
+        }
+    }
+
+    /// The reasons are printed, so they have to fit the page.
+    #[test]
+    fn a_reason_wraps_on_word_boundaries() {
+        let w = wrap("one two three four five", 9);
+        assert_eq!(w, vec!["one two", "three", "four five"]);
+        assert!(wrap("", 10).is_empty());
+        // A word longer than the width is not cut in half.
+        assert_eq!(
+            wrap("supercalifragilistic ok", 8),
+            vec!["supercalifragilistic", "ok"]
+        );
+    }
+
     /// A soft row states why its difference is not a defect.
     ///
     /// Without that sentence a reader cannot tell "measured and forgiven" from

docs/now/2026-08-30-the-audit-says-what-it-does-not-check-and-why.md

@@ -0,0 +1,10 @@
+# NOW -- The audit says what it does not check, and why (2026-08-30)
+
+## The audit says what it does not check, and why (Refs #2864)
+
+- New row: `lean vacuous` prints 250 models; the counter counts `theorem` lines in Completeness.lean. Different marker, same population, and a real invariant -- one theorem per model -- that a hand-transcribed file can break in either direction. Mutation: comment out one theorem and the row reads 250 against 249, exit 1.
+- Two candidates were measured and REFUSED. `types dup` prints 1180 struct definitions; a counter loose enough to be independent reads 1182, and the two extra are `struct = 21,` -- enum members named struct, which the census correctly rejects. Any counter accurate enough to agree is a copy of its matcher.
+- `discard classify` counts parser events produced at run time, not artefacts on disk; counting them a second way means running the same parser, which is not a second opinion.
+- So the audit now prints what it does NOT check and why. Its own coverage was the same class it exists to catch: a page of green rows looks like the whole story until somebody asks what is missing from it.
+- A test refuses a census that is in both lists, and refuses an exclusion under 60 characters -- an exclusion is a measurement, not a shrug. Both directions mutation-checked.
+- Pattern that fell out of two refusals: a census whose population is defined by a MATCHER cannot have an independent counter, because any counter precise enough to agree is that matcher. Only populations defined by something external -- files on disk, workspace members, a marker in another file -- can be counted twice.