G12 statement check: census of every Lean declaration in Math- (3,782 targets) and the reader repairs it forced

cbz/evidence/g12-statement-fuzz-01n/README.md

@@ -273,6 +273,56 @@ recognised and is reported Infeasible/UNSUPPORTED rather than guessed (`ExactRea
 (real-indexed family). **Zero FAIL on 56 kernel-proved statements** remains the soundness check of the
 reader; the class-1 kills (every negated conclusion refuted on the models) show the evaluation has content.
 
+## Census of every Lean declaration in Math- (4 November 2026; `census_math_dfa9b30a_20261104/`)
+
+The tool gained a census mode, `--lean-dir <dir> [--exclude <substring>]…`: every `theorem`/`lemma` in every
+`.lean` file under a directory is a target with no manifest, byte-identical files are evaluated once,
+definitions and carriers are shared across the group, and UNSUPPORTED reasons are classified. Run over the
+16 Lean groups of Math- at `dfa9b30a` (3,782 declarations; raw evidence snapshots excluded): **7 PASS ·
+128 CORROBORATED · 0 FAIL · 3,647 UNSUPPORTED** — see [CENSUS.md](census_math_dfa9b30a_20261104/CENSUS.md)
+for the per-group table, the reason classes, the forty binder types the interpreter does not model, the
+list of decided statements and the reproduce commands. The first run found two reader defects
+(structural predicates on arguments the finite model does not carry were taken as true: `Measurable
+(sourceA L)` for a function on ℝ, `Integrable … (gaussianReal 0 1)`), fixed with regression tests before
+the receipts were taken. Parser repairs that the corpus forced: attribute-prefixed declarations
+(`@[simp] theorem …` on one line), Unicode subscript identifiers (`x₀`), nested projections (`p.2.1`),
+multi-token ascription types, and a parser exception now fails one declaration instead of its module.
+
+**Review repairs (4 November; Codex's review of #752, findings 4471516437 · 4471516451 · 4471516464; receipts
+`*_r4*` and the census re-taken).** Three defects of the reader, each confirmed with a reproduction before
+it was fixed, each covered by a regression test (`NameResolutionTests`): (1) a function returned by a
+definition bound its parameters at the codomain type (`def f : ℕ → ℝ := fun n => if n - 1 = 0 then 1 else 0`
+made `f 0 = 1` FAIL and accepted `f 0 = 0`) — parameters now take the domain types of the declared arrow
+type, an explicit binder type wins, and arrow types split at bracket depth 0 only; (2) a group's
+definitions were pooled by short name, first module wins (`A.f`/`B.f` collapsed, verdicts depending on file
+order) — definitions are kept by Lean-qualified name, `namespace`/`section`/`end`/`open` are tracked as
+scopes, a statement resolves a name from its namespace outward and through its `open`s, in its own module
+first and then across the group only when exactly one definition (up to identical text) carries the name,
+otherwise UNSUPPORTED "ambiguous definition"; (3) the splitter saw declaration keywords at column 0 only —
+indented declarations and `open … in` / `set_option … in` prefixes now start declarations, and a
+`theorem`/`lemma` keyword the splitter still cannot separate becomes an UNSUPPORTED target "declaration not
+reached by the parser", so a census accounts for every declaration. Measured exposure of the landed
+receipts: none — no decided statement depended on a collision, a returned function or an unreached
+declaration — and the re-run changed **0 of 3,782** census verdicts and **0** package verdicts
+(`main_formal_ec6962ff_r4.json`, `math_formal_19a55750_r4.json` equal r3 per target); 695 census targets now
+carry their Lean-qualified names, which is what lets every record of the #695 index bind by exact name
+(see [CENSUS.md](census_math_dfa9b30a_20261104/CENSUS.md), "Per-record annotation"). The suite is **85
+tests** (normal, `-O`, `-W error`); the module-level `defs` of a parsed file are now keyed by qualified name
+(`Demo.fact`), and the test fixtures that append a theorem after a closed namespace write the `open … in`
+prefix Lean itself would need.
+
+**Declaration-scope repair (6 November; Codex review finding 4472023769).** A selected definition was
+looked up in the caller's namespace correctly, but the reader then evaluated its body, pattern clauses and
+returned closures in that caller's namespace and `open` set. Thus `A.f` could read `B.x` when called from
+`namespace B`, producing both a false FAIL and a false PASS. Commit `55571918ed8772c5c260aa44855af68add8d0a2d`
+records each definition's declaration namespace and opens and restores the caller after evaluation; closures
+carry the same scope. The regression covers ordinary bodies, returned functions, pattern clauses and
+`open Shared in def` with both true and false assertions. The suite is now **86 tests**, passing under normal,
+`-O`, and `-W error` modes. The exact Math- `dfa9b30a27ea8f8ee647bb067549fa53c7d06ef6`
+census was rerun from a native archive: after normalising only the environment-specific `lean_dir` field,
+all 16 JSON reports match the stored receipts exactly, so **0 of 3,782 verdicts changed**. The additive
+machine-readable receipt is `declaration_scope_repair_20261106.json`; no historical receipt was rebound.
+
 **Proposed registration amendment (for Root; the landed GOVERNANCE.md section of #741 governs until
 amended):** the coverage row for Math- `formal/` at `19a55750` becomes `63 | 3 PASS | 56 CORROBORATED |
 4 UNSUPPORTED`; the sentence "The tool does not cover Mathlib real analysis, binders before the colon or
@@ -282,11 +332,17 @@ exactly in ℚ(√d₁, …, √dₖ), and samples measure-theoretic statements
 rational weights, tables, subsets); a sampled statement is CORROBORATED or FAIL, never PASS. Structural
 conclusions, real-indexed families, nested radicals, transcendental functions and unbounded quantifiers
 inside a statement remain explicitly unsupported; no registered statement uses `Real.exp`/`log`, so no
-interval backend is pending."; the test count becomes 78; and the gate
+interval backend is pending."; the test count becomes 85; and the gate
 mapping gains: "For a statement with sampled binders, CORROBORATED at the same source cut as the kernel
 receipt is the applicable empirical validation (recorded with seed, sample count and the report's
-SHA-256); it is admitted evidence, not an exact check, and is marked as such." The B-007 statute is
-unchanged: a `PROOF_INDEX` row needs PASS or, for sampled statements, CORROBORATED — never UNSUPPORTED.
+SHA-256); it is admitted evidence, not an exact check, and is marked as such." The B-007 statute
+becomes: a `PROOF_INDEX` row carries `G12: PASS | CORROBORATED | not applicable (<construct>)`, taken from the
+registered run or the census at the row's source cut; PASS or CORROBORATED is the applicable empirical
+validation, *not applicable* names the construct the interpreter does not model (a structure, a function
+on ℝ, an existential, a family) and is never written for a statement the interpreter reaches, and
+UNSUPPORTED is never upgraded or left silent. The census shows the CLOSED-track Gaussian-field packages
+have no reachable declaration at all; their rows read *not applicable* throughout, and the index should
+say so rather than let the addendum rule be read as satisfied.
 
 ## Proposed gate row and registry entries (for Root; B-003)