On the Nonexistence of Binary Singly Even Self-Dual [56,28,12] Codes

This preprint proves the nonexistence of binary singly even (Type I) self-dual codes with parameters [56,28,12]. Two proofs are given: a short design-theoretic argument combining earlier results of Yorgov and Bachoc–Gaborit, and an independent character/Krawtchouk proof deriving the required shadow-incidence identities directly. The latter proof has been formalized and checked in Lean 4. A concurrent public-review manuscript by Maciej Nowicki and Artificial Hyperintelligence Eve was posted on 10 September 2026 and is cited in the preprint. The accompanying reproducibility artifact contains the Lean sources and clean replay logs, exact certificate checker, dependency pins, hashes, and RFC 3161 timestamp material relating to the frozen research evidence. Independent expert review and comprehensive historical priority assessment remain in progress.