# Final proof-material audit

**All 20 sampled papers provide inspectable written proof material. Eleven have main-result Lean coverage, four have supporting or partial coverage only, and five have no linked Lean material found. No proof checker was run.**

The sample is unchanged: one first-listed paper from each of 20 families drawn with seed `20261008`, at commit `fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb`. Coverage means inspected correspondence between the paper statement, scope note and formal target—not successful verification or an independent correctness judgment.

| Finding | Final count |
|---|---:|
| PDF and TeX written proof material | 20/20 papers |
| Main-result Lean coverage | 11/20 |
| Supporting / partial Lean coverage only | 4/20 |
| No linked Lean material found | 5/20 |
| Configured solution-module files supplied | 23/23 configurations |
| Proof-checker executions | 0 |

The 15 new modules close all previously missing **entry-file** gaps. Their hashes and byte lengths pass, and the declared commit matches. Combined inputs contain 24 OAI implementation files. Static inspection found no `sorry`, `admit`, `sorryAx` tokens or `axiom` declarations in their code after comments and strings were excluded. Challenge-file `sorry` placeholders specify comparison targets and were not counted as implementation gaps.

Entry-file completeness is not dependency completeness. Of 30 selected declarations, 25 have bodies in their configured entry file and one in another supplied import. Four auxiliary declaration bodies remain unavailable behind imports: the totient companion zero case, refined matching entropy, and two self-similar dimension corollaries. These are **gaps in supplied evidence**, not demonstrated proof defects. In total, 270 distinct direct OAI imports remain unavailable; transitive dependencies and external libraries were not audited.

The four scope limitations remain: annular variation has only a maximal-estimate target; sixth-power Foulkes covers b≥30 rather than all b≥6; O(3) has finite-volume decay rather than the continuum-limit theorem; SLE has positivity rather than positive finite measure. Additional implementation entry files do not broaden these statements.

Shared checking instructions exist, but 19 individual paper READMEs contain citation information only. The Foulkes README distinguishes expected-data checking from executing the C++ computations. Neither mode was run. Every execution status remains **not run**, not passed or failed.

See [the detailed evidence table](final-material-evidence.md) for all 20 papers, pinned theorem/configuration/implementation links and declaration locations; [CSV](final-material-evidence.csv) and [JSON](final-material-audit.json) preserve the structured evidence and provenance. The previously generated scope chart remains numerically unchanged.
