The exact locator before approximation
A Lean 4 formalization of finite Fourier coefficients with an exhaustive locator proved to return a maximum-magnitude frequency.
This development builds the finite Fourier setting, implements a concrete exhaustive locator, and proves that its returned frequency attains the largest absolute coefficient.
It also proves threshold correctness and records the 2^n size of the search cube.
The difficult part of Goldreich-Levin is not estimating one coefficient. It is avoiding an exponential scan across all candidates. The project makes that boundary explicit.
where the effort went
the numbers
built with
delivery record
I wanted the exact search specification and its correctness proof fixed in Lean before reasoning about the randomized algorithm that avoids exhaustive frequency search.
Finite Boolean-cube Fourier coefficient definitions
Executable exhaustive maximum-magnitude locator
Proof that the returned frequency is globally maximal
Threshold soundness and completeness lemmas
Explicit proof that the candidate cube contains 2^n frequencies
The constraints mattered as much as the finished interface.
after shipping
Proving an argmax implementation exposes tie cases and finiteness assumptions that paper notation usually suppresses.
The expensive dimension should be visible in the formal object being searched.