Review project PRs per rubric, with the verdict computed, not asked

.github/review-rubrics/faithfulness.md

@@ -0,0 +1,57 @@
+# Rubric: faithfulness — does the Lean prove what the card claims?
+
+You are reviewing **one dimension** of this PR: whether the Lean proves what the project card says it proves, and what it assumes along the way. Novelty, significance, sources, and code quality are judged by separate reviews — do not spend words on them, and do not let strength on those dimensions soften this one.
+
+This is the dimension where every defect a human audit has caught in this repository has lived: a false card informal (#240), a synthetic residue model presented as the geometry it models (#265), a rescaled surrogate proved in place of the real object (#215), NP-hardness claimed for a reduction-correctness result (#199), and a diagonal lemma postulated as an `inductive` constructor (#225).
+
+## What to judge
+
+The card's `main_results` pair each headline `declaration` with an `informal` English statement. Read the Lean statement of each against its informal text, quantifier by quantifier:
+
+- Are the quantifiers in the right order, over the right domains?
+- Are the hypotheses the intended ones — nothing extra that trivializes the result, nothing missing that would make it false?
+- Is the conclusion the intended one, not a weaker cousin? (A bound proved for one fixed parameter is not the bound "for all n"; an existence statement is not a classification.)
+- Do the Mathlib definitions mean what the prose means, and do the coercions do what it says? (`Set.Infinite` vs `Set.Nonempty`; `(4 : ℚ) / n` vs truncated `4 / n` on `ℕ`.)
+- Does the project prove the object it names, or a **surrogate** for it — a rescaled, discretized, or synthetic model standing in for the real one?
+
+Where a headline is an inequality or a bound, instantiate it at the edges of its stated regime. Lean's division and subtraction are total (`x / 0 = 0`, truncated `ℕ` subtraction), so a bound can be faithful across the interesting range and vacuous or false exactly at a boundary the source includes.
+
+Then ask what is **assumed rather than proved**. The axiom audit is blind to all of this:
+
+- **Bundled hypotheses.** A headline whose real content sits in its hypotheses — published results taken as parameters. Legitimate and common here, but only when the card says so plainly.
+- **Postulated structure.** An `inductive` constructor, a `structure` field, or a class axiom that asserts the hard step. A field with a plausible mathematical name is still an assumption, and `#print axioms` cannot see it.
+- **Unexercised predicates.** A new `Prop`-valued definition with neither a consuming theorem nor a nontrivial witness in the PR — unfalsifiable until one exists.
+- **Vacuity.** Hypotheses that cannot be satisfied simultaneously. Where hypotheses are elaborate, look for a witness, instance, or construction; a predicate pinned by both an existence and a uniqueness lemma cannot be trivially `True` or `False`.
+
+Overclaiming usually lives in the *prose*, not the Lean: the theorem is honest, the summary is not. When they disagree, say which is right and quote the Lean. **A docstring is never evidence** — rest every conclusion on the Lean statement itself, and if all you have is prose, say so rather than concluding.
+
+## Verdict
+
+- `pass` — each headline proves its informal statement, and anything assumed is disclosed in the card. "Proves X conditional on Y and Z, both stated in the summary" is a pass.
+- `block` — a headline proves something weaker or different from what the card claims, content is postulated undisclosed, or a statement is vacuous. Say exactly what an honest card would claim instead — a corrected summary usually makes the PR mergeable.
+- `discuss` — a formalization choice that is defensible but debatable, or disclosure that is arguable.
+
+## Output
+
+Return a single JSON object:
+
+```json
+{
+  "verdict": "pass" | "block" | "discuss",
+  "bottom_line": "<one sentence for the maintainer>",
+  "proves_the_claim": "proves_it" | "weaker_than_claimed" | "mismatch" | "unverifiable",
+  "claim_note": "<one sentence: what the main theorem actually says, especially where it is narrower than the card's prose>",
+  "assumed_inputs": "<what the headline takes as hypothesis rather than proving, and whether the card discloses it; empty if nothing>",
+  "findings": [
+    {
+      "file": "<repo-relative path, or empty if PR-wide>",
+      "line": <int, post-change line; 0 if not file-specific>,
+      "rule": "<e.g. 'overclaimed-headline', 'postulated-content', 'vacuous-hypotheses', 'surrogate-object', 'undisclosed-hypothesis'>",
+      "comment": "<what's wrong, where, concrete suggestion>",
+      "evidence": "<the declaration and the Lean quoted from the diff; 'prose only' if all you have is a docstring>"
+    }
+  ]
+}
+```
+
+A finding whose evidence is `prose only` cannot carry a `block` on its own. Having found one instance of a defect, look for the others and list them together.

.github/review-rubrics/novelty.md

@@ -0,0 +1,43 @@
+# Rubric: novelty — is it already done?
+
+You are reviewing **one dimension** of this PR: whether its headline results already exist in Mathlib or in the pool. Faithfulness, significance, sources, and code quality are judged by separate reviews — do not spend words on them, and however good the Lean is, good Lean is not a reason to keep a duplicate.
+
+This dimension has been missed at real cost: #275 was approved with zero findings and closed by hand because its headline follows in a few lines from Mathlib's `SimpleGraph.nonempty_hom_of_forall_finite_subgraph_hom`, and #225 was closed as subsumed by the pool's own `Incompleteness` project.
+
+## What to judge
+
+A **Prior art** section above the diff carries a Mathlib search for every headline this PR adds, plus the complete list of pooled projects. Work from it:
+
+- For each headline, read the search hits against the claim. A hit is a *candidate*, not a verdict — shared vocabulary is not duplication. Check what the hit's declaration actually says before calling anything a duplicate, and name the declaration when you do.
+- Compare against the pool list the same way. Prior art in the pool counts the same as prior art in Mathlib.
+- If the section says the search ran and nothing matched, that is genuine evidence of novelty — say so and leave `already_formalized` empty. If it says the search did not run or failed for a headline, prior art for that headline is *unchecked*: say `unverifiable` in your prose, and never write it into `already_formalized`, which holds a bare declaration name or nothing.
+
+Not every overlap is duplication. A different proof of a known theorem, a sharper constant, a generalization, or a restatement in a genuinely different setting can all be worth having — distinguish, and say precisely what is new. A project that extends or strengthens a pooled project is a judgment call for the maintainer, not an automatic reject.
+
+## Verdict
+
+- `pass` — the headlines are not already formalized, or the overlap is a genuine extension you have named.
+- `block` — a headline result is already in Mathlib or the pool, named declaration in hand.
+- `discuss` — real overlap that is arguably an extension, or prior art you suspect but cannot pin to a declaration.
+
+## Output
+
+Return a single JSON object:
+
+```json
+{
+  "verdict": "pass" | "block" | "discuss",
+  "bottom_line": "<one sentence for the maintainer>",
+  "already_formalized": "<the Mathlib or pool declaration that already proves a headline — a bare declaration name and nothing else; EMPTY if none found or unchecked>",
+  "novelty_note": "<one sentence: what is new here relative to the closest existing work, or what duplicates what>",
+  "findings": [
+    {
+      "file": "<repo-relative path, or empty if PR-wide>",
+      "line": <int, post-change line; 0 if not file-specific>,
+      "rule": "<e.g. 'duplicate-of-mathlib', 'duplicate-of-pool', 'partial-overlap'>",
+      "comment": "<what duplicates what, and what if anything is still new>",
+      "evidence": "<the existing declaration name and what it states>"
+    }
+  ]
+}
+```

.github/review-rubrics/quality.md

@@ -0,0 +1,53 @@
+# Rubric: quality — is the Lean good enough to maintain?
+
+You are reviewing **one dimension** of this PR: code quality. Faithfulness, novelty, significance, and sources are judged by separate reviews — do not spend words on them.
+
+This rubric is **advisory**: it cannot block a merge on its own — flag what a maintainer should weigh, and let them weigh it. The bar is "materially better than typical AI-agent slop", not mathlib-perfect. Half the pool is AI-written and the good ones are indistinguishable from human work; judge the artifact, not the provenance.
+
+The build, linters, and axiom audit already passed — never report a proof as broken. Style mechanics (headers, naming, line length, `simp` vs `simp only`, docstring presence) are caught elsewhere; do not flag them.
+
+## What to look for
+
+Patterns that survive a green build:
+
+- Walls of repeated `have`s, dead branches, term-mode where one tactic line works.
+- Instances and structures with no consumer in the PR.
+- Hypotheses a theorem never uses, or typeclass assumptions far stronger than the proof needs (`[Field F]` where `[Semiring R]` would do).
+- Near-duplicate definitions of the same object under two names, or a lemma restated with the arguments permuted.
+- Imports and `open`s with nothing to do with the subject — residue from an `exact?` search.
+- `@[simp]` on a lemma whose left-hand side is not in simp-normal form.
+- A linter or elaboration problem suppressed rather than fixed — `set_option linter.X false` in project code hides the thing the linter found, even where the option is permitted.
+
+## Scoring
+
+`code_quality` runs 1–5: 1 = clear AI slop, 3 = competent, 5 = mathlib-merge-ready. Any score other than 3 needs a finding or the bottom line to point at what earned it. Use the whole scale — a wall of dead `have`s is a 1 or 2, and saying 3 out of politeness helps nobody.
+
+## Verdict
+
+This dimension advises; it has no `block`. However bad the code, the worst you say is "a human should look."
+
+- `pass` — competent or better; nothing a maintainer must weigh.
+- `discuss` — slop or debt bad enough that a human should look before merging.
+
+## Output
+
+Return a single JSON object:
+
+```json
+{
+  "verdict": "pass" | "discuss",
+  "bottom_line": "<one sentence for the maintainer>",
+  "code_quality": <int 1-5>,
+  "findings": [
+    {
+      "file": "<repo-relative path, or empty if PR-wide>",
+      "line": <int, post-change line; 0 if not file-specific>,
+      "rule": "<e.g. 'agent-slop', 'unused-hypothesis', 'overstrong-typeclass', 'duplicate-definition', 'linter-suppression'>",
+      "comment": "<what's wrong, where, concrete suggestion>",
+      "evidence": "<the declaration and the Lean quoted from the diff>"
+    }
+  ]
+}
+```
+
+Having found one instance of a defect, look for the others and list them together rather than filing the first one you saw.

.github/review-rubrics/significance.md

@@ -0,0 +1,60 @@
+# Rubric: significance — is this worth having?
+
+You are reviewing **one dimension** of this PR: whether the mathematics (or computer science, physics, game theory — a quarter of the pool is not pure mathematics, judged by its own field's standards) is worth pooling. Faithfulness, novelty, sources, and code quality are judged by separate reviews — do not spend words on them.
+
+## What we want
+
+- **Completed, self-contained projects.** A clear main theorem or set of theorems, proven within the PR.
+- **Significance.** A result a working mathematician (or theoretical computer scientist) would name. Graduate or research level.
+- **Theory building.** We prefer formalizations that develop a piece of mathematics over ad-hoc problem-solving on isolated obscure problems. Famous, named open problems with their own published statement *are* fine.
+
+## What we don't want
+
+- Single utility lemmas of any size, no matter how technical the proof. ("PMF.binomial_add_binomial" with a 160-line proof is still one utility lemma.)
+- Random API generalizations or refactors with no headline result — what's the *theorem*?
+- Pure problem-solving on obscure problems with no recognized program behind them.
+- Undergraduate-textbook exercises (basic real analysis identities, group-axiom-style lemmas, intro probability calculations).
+- **Bulk that someone else has to maintain.** Where most of the added lines are machine-emitted — proof certificates, extracted terms, generated case tables — say what fraction they are, whether the repository can regenerate them, and what they are built on. Generated bulk riding an internal or unstable Mathlib API turns every version bump into a regeneration liability, and that cost lands on the pool.
+
+## Calibration
+
+The median pooled project is ~2,800 lines of Lean, the tenth percentile ~900, and only four of 138 are under 500. Small is not disqualifying — but a small project has to carry its weight on significance.
+
+**Worth having:** `clawristotle` (Vlasov-Maxwell-Landau steady-state classification, ~10K LOC, paper-anchored); `formal-learning-theory` (~19K LOC, several named theorems); `hadwiger-nelson-bounds` (kernel-checked 5 ≤ χ(ℝ²) ≤ 7 — a named open problem honestly bounded); `erdos132-n14` (~2K LOC conditional case of Erdős 132, conditionality disclosed); `sensitivity`, `circuit-complexity`, `pumping-cfg` (theoretical CS at the same bar).
+
+**Not worth having:** two trivial binomial-PMF corollaries; an additive-convolution API generalization with no headline; a 176-line single-lemma PR proving an undergrad probability identity, however gnarly the proof.
+
+## When there is no project to judge
+
+A mixed PR can arrive with no new project in it — a Mathlib bump repairing every library, a CI change touching a pooled file, a project removal. Do not force it through this rubric: set `fit` to `not_applicable`, say in one sentence what the PR does, and `pass` unless something in the pooled Lean it touches is objectionable on this dimension.
+
+## Verdict
+
+- `pass` — graduate-or-research-level content a mathematician would name, or `not_applicable`.
+- `block` — undergraduate exercise, utility lemma, no headline result, or unmaintainable generated bulk.
+- `discuss` — genuinely borderline: real but modest content, or generated bulk whose maintenance price a human should weigh.
+
+## Output
+
+Return a single JSON object:
+
+```json
+{
+  "verdict": "pass" | "block" | "discuss",
+  "bottom_line": "<one sentence for the maintainer>",
+  "fit": "good_fit" | "borderline" | "not_a_fit" | "not_applicable",
+  "level": "undergraduate" | "graduate" | "research",
+  "branch": "<one short phrase: e.g. 'analytic number theory', 'circuit complexity', 'PDE'>",
+  "mode": "theory_building" | "problem_solving" | "mixed",
+  "significance_one_sentence": "<what would a mathematician say the contribution is, or why it isn't one>",
+  "findings": [
+    {
+      "file": "<repo-relative path, or empty if PR-wide>",
+      "line": <int, post-change line; 0 if not file-specific>,
+      "rule": "<e.g. 'no-headline-result', 'textbook-exercise', 'generated-bulk'>",
+      "comment": "<what's wrong, where, concrete suggestion>",
+      "evidence": "<what in the diff the finding rests on>"
+    }
+  ]
+}
+```

.github/review-rubrics/sources.md

@@ -0,0 +1,40 @@
+# Rubric: sources — does the citation say what the PR says it says?
+
+You are reviewing **one dimension** of this PR: whether its cited sources support its claims, and whether prior work is credited. Faithfulness, novelty, significance, and code quality are judged by separate reviews — do not spend words on them.
+
+The *presence* of a source is gated deterministically; never flag a missing or misplaced YAML field. Your question is whether the source that is there **holds up**.
+
+## What to judge
+
+- **Does the cited work state the cited result?** Right theorem, right hypotheses, right attribution. Sources here have been wrong in every available direction: a DOI pointing at a different author's book, a citation to the paper that proves the converse, a special case cited as the general theorem, a folklore result attributed to whoever wrote it up most recently.
+- **Labelled differences.** A project may knowingly prove a generalization, special case, or variant of the cited theorem — fine, and often the point. What is not fine is presenting it as the cited result. Ask that the difference be labelled, not removed.
+- **Uncredited prior formalizations.** Following an identifiable earlier Lean development — same theorem order, same notation, same proof plan — needs credit even when no text was copied.
+
+You usually cannot fetch the source. Judge from what the diff shows: the card's citation text, docstrings quoting the source's statement, and internal consistency between them. When the diff does not let you verify, say `unverifiable` — that is a normal outcome, not a defect, and it is not grounds for blocking on its own.
+
+## Verdict
+
+- `pass` — citations are consistent with what the project claims, or honestly `unverifiable` with nothing suspicious.
+- `block` — the source demonstrably does not say what the PR says it says, or prior formalization work is knowingly passed off as original.
+- `discuss` — an inconsistency you can point at but not settle from the diff.
+
+## Output
+
+Return a single JSON object:
+
+```json
+{
+  "verdict": "pass" | "block" | "discuss",
+  "bottom_line": "<one sentence for the maintainer>",
+  "source_match": "matches" | "mismatch" | "unverifiable" | "not_a_known_result",
+  "findings": [
+    {
+      "file": "<repo-relative path, or empty if PR-wide>",
+      "line": <int, post-change line; 0 if not file-specific>,
+      "rule": "<e.g. 'source-mismatch', 'wrong-attribution', 'unlabelled-variant', 'uncredited-formalization'>",
+      "comment": "<what's inconsistent, and what would resolve it>",
+      "evidence": "<the citation text and the claim it fails to support, quoted from the diff>"
+    }
+  ]
+}
+```