Projective-plane determinant bounds for sparse binary matrices

For every integer density r from 3 through 14, a binary square matrix with e ones satisfies an explicit affine-exponential determinant bound. Under e <= r n this gives the projective-plane determinant rate, with equality precisely for direct sums of projective-plane incidence matrices of order r-1. Individual row and column degrees are unrestricted. The written proof uses an exact finite scalar certificate with rigorous unbounded-degree tails; the companion contains a pinned 98-module Lean mathematics closure. Manuscript and research prose: CC BY 4.0. Original reproduction code: MIT. Third-party notices are preserved. OpenAI tools assisted mathematical exploration, proof engineering, coding, computational verification, literature research, and manuscript drafting. Internal AI-assisted review and independently structured computations are distinct from external human peer review. No external specialist review or fresh Lean compilation is claimed. John Tripodo is the sole named author and approved public release with this disclosure. See AI_ASSISTANCE.md and FORMAL_SCOPE.md in the accompanying standalone archive. Administrative correction (22 October 2026): the companion archive was replaced to remove internal approval records and private-origin locators, update publication and provenance metadata, and regenerate integrity manifests. The manuscript PDF and TeX, Lean sources, reproduction/checker code, and license texts are unchanged. This correction does not claim a fresh Lean compilation or new proof review. Dedicated public repository: https://github.com/jjtripodo-lgtm/sparse-projective-plane-determinants.