The sharp level-one Fourier weight at density one eighth

Dev D. Goyal

The sharp level-one Fourier weight at density one eighth

Dev D. Goyal · 2026 · Research preprint, not externally peer reviewed

Selected result in this collection

Problem and result

Problem: Lei Yu's problem on the level-1 Fourier weight W(1/8) of Boolean functions of density 1/8
Posed in: Lei Yu, 'On Average Distance, Level-1 Fourier Weight, and Chang's Lemma', arXiv:2504.02593 (v2, 2026 revision), Section VII, Problem 2
Status: Determined exactly
Result: Every Boolean function of mean 1/8 on {−1,1}^n has level-one Fourier weight at most 3/64, attained by a codimension-three subcube for n ≥ 3; equivalently, density-1/8 sets have average Hamming distance ≥ (n − 3)/2.

Abstract

For every Boolean indicator of mean 1/8 on a finite uniform cube, the level-one Fourier weight is at most 3/64. A codimension-three subcube attains the bound in every dimension at least three.

Details

Year: 2026
Discipline: Mathematics
Area: Discrete analysis
Subject: Discrete analysis, tilings, probability and entropy
Result type: Sharp finite-cube Fourier bound
Formal proof: Standalone Lean package
Family: sharp-eighth
Keywords: Fourier analysis of Boolean functions, level-one Fourier weight, level-one inequality, Boolean cube, subcubes, sharp inequality

Statement and scope

Formal scope. The formal proof includes arbitrary dimensions, the exact moment identities, the Hamming-distance bound, and sharpness witnesses.

A Lean check establishes only the formal statement that is checked. It does not establish novelty, historical priority or a faithful transcription of an external source. Known gaps are listed in UNFINISHED.md; the authorship disclosure describes how the results were produced.

Manuscript

PDF on this site: manuscript.pdf 329 KB
PDF on GitHub: papers/mathematics/sharp-eighth/manuscript.pdf
LaTeX source: papers/mathematics/sharp-eighth/manuscript.tex

Formal proof

This result has a standalone Lean 4 package, separate from the shared library. Build it with the toolchain and instructions given in its README.

Proof package

papers/mathematics/sharp-eighth/ 3 Lean files

Lakefile

papers/mathematics/sharp-eighth/lakefile.lean

Toolchain

leanprover/lean4:v4.19.0

Library roots

SharpEighth.lean

Reproduce

The commands below are quoted from papers/mathematics/sharp-eighth/README.md, which gives their context and working directory.

Reproduce the proof

lake exe cache get
lake build
lake env lean -DwarningAsError=true Audit.lean

README: papers/mathematics/sharp-eighth/README.md
Repository guide: verification/README.md
Unfinished proofs: UNFINISHED.md

Source and prior work

Prior work. Yu, On Average Distance, Level-1 Fourier Weight, and Chang’s Lemma, 2026 revision.

Priority and subsequent correspondence. On 30 October 2026, Professor Lei Yu informed me that Yijia Fang and Hao Huang had already proved this bound, with the equality cases, in a manuscript shared privately about a month earlier and submitted to arXiv on 29 October 2026 (arXiv:2610.40486). I make no originality or priority claim for the bound. Priority and novelty record.

Questions and answers

What is the maximal level-one Fourier weight at density 1/8?

It is 3/64 in every dimension n ≥ 3: every Boolean indicator of mean 1/8 has level-one Fourier weight at most 3/64, and a codimension-three subcube attains it. Equivalently, a subset of density 1/8 of the Boolean cube has average pairwise Hamming distance at least (n − 3)/2.

Was this bound proved before?

Yes. Yijia Fang and Hao Huang proved it earlier, together with a characterization of the equality cases (arXiv:2610.40486, submitted 29 October 2026; reported to have circulated privately about a month before). This note gives an independent certificate-based proof, does not classify equality cases and makes no originality or priority claim.

Is the proof formally verified?

The Lean 4 formalization covers arbitrary dimensions, the exact moment identities, the Fourier and Hamming-distance bounds and the sharpness witnesses, and a separate Python checker verifies the rational certificate in exact arithmetic. The note is an unrefereed preprint.

Cite

Citation file papers/mathematics/sharp-eighth/CITATION.bib. For the whole collection, use CITATION.cff or CITATION.bib.

@misc{goyal2026sharpeighth,
  author = {Goyal, Dev D.},
  title = {The sharp level-one Fourier weight at density one eighth},
  year = {2026},
  howpublished = {Preprint},
  url = {https://github.com/dvgyl/math-and-theory/tree/main/papers/mathematics/sharp-eighth},
  note = {Fully autonomous agentic research generated by AI systems.}
}