An End-to-End Lean Verification of the Eleven-Vertex Case of Erdős Problem 97

This deposit contains a preprint and supporting proof artifacts for the eleven-vertex case of the four-equidistant-neighbours question associated with Erdős Problem 97. For eleven real planar points satisfying StrictCCW11, the checked theorem excludes a four-equidistant-witness set at every centre; equivalently, some vertex has at most three other vertices at every fixed positive distance from it. The theorem is specific to n=11 and does not resolve the unrestricted question. The Lean development closes the geometric reduction, certified finite tables, 210 root cases and the final declaration T34Closed.erdos97_n11_strict_ccw. A staged clean replay compiled 680 project modules from pinned sources without importing the earlier V38 release's project objects. The three final declarations report only propext, Classical.choice and Quot.sound. The compiler is Lean 4.36.0-rc1 (commit c9afcddf514a6772bd4d649f7cfc04eff0b9f15e), with mathlib revision 625d8914199bc567cca9b91f90e8e5afafa5ae51 and the recorded package pins. Files: a readable manuscript PDF; its editable LaTeX source and identical embedded PDF; the immutable 9,984,504,611-byte proof-evidence ZIP containing frozen source/tokens, objects, receipts and logs; and a small Python offline-audit toolkit. A README, licensing statement and external checksum list accompany them. The evidence SHA-256 is 19c8e183a40f298f721b20ae4cce640e0711c4b6adb35395c84de7ca5815c5ee. The public verifier checks archive integrity, recorded source/object mappings, receipts and dependency closures without running Lean. It is not a turnkey Lean rebuild and does not constitute an independent researcher rerunning the kernel or mathematical peer review. Source build requirements and verification boundaries are described in the manuscript and toolkit. The preprint does not claim journal acceptance. AI assistance is disclosed in the manuscript. Licensing: CC BY 4.0 for author-owned manuscript text, documentation and research data; MIT for author-owned program source. Third-party material retains its upstream terms. See LICENSES.md for the precise scope.