Formal Resolution of the Maximum Nonlinearity of Balanced 8-Variable Boolean Functions

This record contains a formally verified proof that the maximum nonlinearity of a balanced 8-variable Boolean function is exactly 116. Equivalently, no balanced 8-variable Boolean function with nonlinearity 118 exists. The accompanying verification package contains the complete minimal Lean source required to reproduce the result, together with pinned build configuration and verification material. The proof package was independently rebuilt from source on a separate Windows 10 machine using the pinned Lean toolchain. The complete build returned exit code 0, fresh axiom checks returned exit code 0, and an intentionally false theorem was correctly rejected. SHA256 of BOOLEAN_NL118_MINIMAL_VERIFY.zip: FCA66A3489C4DC2ADFD2E06C26C235486BBF43F2E63E6A9B1EBBC78DDA354777 A short verification note is included for external review. A conventional mathematical manuscript and further independent expert review are in preparation.