Proposal: per-repo kernel-receipt records so the census can show kernel results beside text matches #28

Problem

The census counts holes, axioms and unsafe markers by text matching (scripts/census/proof-holes.sh). The catalogue says so: "textual candidates, not kernel verdicts". Two cases show where text matching and the kernel disagree:

• hyperpolymath/ephapax had 15 "holes" in the catalogue. A Print Assumptions census of its whole Coq development finds 0: 257 of 257 named results are closed under the global context, and coqchk finds no ephapax axiom. fix(census): comment-aware proof-holes.sh, Idris2 undefined-declaration axioms; refresh 13 rows #27 closes most of that gap by making the scanner skip comments, but a text scan still cannot see a proof's assumptions.
• PROOF-POLICY §8.4–§8.5 says grades are derived from receipts and that mathesis "may catalogue grades; it derives them from those receipts". Today mathesis has nowhere to put a receipt, so it cannot derive or show a single Proof Witness Grade, even ungraded.

Proposal

The home repo owns its proofs and evidence (§2.2, §8.5). Mathesis would only ingest a small, machine-readable kernel receipt from each repo that publishes one, and show it next to the text census. It would never assign anything itself.

A receipt is one I-JSON/JCS record per checker run, with:

• repo and the full 40-character commit;
• checker and its version (coqc 8.18.0, agda 2.6.3 + stdlib 2.3, lean, idris2);
• invocation, including flags (for Agda, the §2.1 --safe --without-K --cubical-compatible);
• results: the count of named results checked and the count that are closed or assumption-free;
• axioms: the reported axioms by name, from Print Assumptions, #print axioms, or the Agda import-cone postulate scan;
• independent_recheck: for example coqchk -o or agda --ignore-interfaces, with its own result;
• result: pass or fail, plus a receipt state of current, superseded or regressed (§8.4).

Mathesis would then:

1. read receipts from a known path in each repo (to be agreed) or from a nomination PR;
2. add kernel columns to the catalogue (results closed / checked, axioms, recheck);
3. derive a PWG per theorem only where an Agda receipt and RECONCILED correspondence records exist, and otherwise show ungraded. That last case is everything today.

Worked example already available

hyperpolymath/ephapax#425 adds formal/scripts/no-false-gate.sh. It already produces every field above for Coq: a census of 257/257 closed results, the axioms reported, and a coqchk -o recheck. Emitting a receipt from it is a small change, and that would make it the pilot.

Open questions for the owner

• Where receipts live: a fixed path in each home repo, or nomination PRs into mathesis.
• Whether CI-produced receipts only count as PWG-1 evidence when they come from the pinned, headless runs §8.2 describes.
• Whether the schema belongs in standards (for example next to proof-witness-grades.k9.ncl) rather than in mathesis.