Exact finite testing, no hidden gap
A Lean 4 development of the exact finite core of Boolean Fourier sparsity testing and a proved nonadaptive exhaustive tester.
The repository formalizes Boolean functions on the finite cube, exact Fourier coefficients and support, Hamming distance, farness from sparse functions, and a deterministic nonadaptive query model.
It proves a perfect tester that queries the whole cube, computes the exact spectrum, and decides sparsity with precisely 2^n queries.
That theorem is intentionally not presented as the sought dimension-independent randomized result. The publication records the unresolved gap as part of the deliverable.
where the effort went
the numbers
built with
delivery record
I wanted a checked baseline where every definition and query count is explicit before attempting the much harder randomized sparsity-testing bound.
Exact Fourier coefficients and support on the Boolean cube
Hamming distance and farness from the sparse-function class
Deterministic nonadaptive oracle-query model
Perfect exhaustive tester with an exact 2^n query count
Audited Lean build with the open randomized gap clearly marked
The constraints mattered as much as the finished interface.
after shipping
A formal baseline makes the distance between an exact exhaustive argument and a sublinear tester impossible to hand-wave away.
Query complexity belongs in the theorem interface, not only in explanatory prose.