Math and TheoryA 64-point spectral tile in F₂⁹ with no periodic complement
Problem and result
- Problem
- Ferguson–Iosevich Question 8.1: subspace tiling complements of spectral sets in F₂⁹
- Posed in
- Ferguson and Iosevich, arXiv:2610.36417, Question 8.1 (subspace-complement part) and its equivalent Question 8.2
- Status
- Counterexample
- Result
- An explicit 64-point set E ⊂ F₂⁹ is spectral and tiles F₂⁹, but its tiling complements are exactly the 512 translates of one aperiodic 8-point set, so no subspace complements E and F₂⁹ fails the periodic tiling property.
Abstract
An explicit 64-point set E ⊂ F₂⁹ is spectral and tiles by translation, but has no periodic tiling complement: its complements are exactly the 512 translates of one aperiodic eight-point set. In particular no linear subspace complements E, and F₂⁹ fails the periodic tiling property of Fan and Zhang. The construction places eight three-dimensional subspaces in parallel six-dimensional fibres; the shifts disjoint from E are the 28 pair sums of an affine eight-circuit, which form the line graph of K₈ and contain no three-dimensional subspace. This answers negatively the stronger subspace-complement part of Question 8.1 of Ferguson and Iosevich and its equivalent Question 8.2. Whether every spectral 64-point subset of F₂⁹ tiles remains open.
Details
- Year
- 2026
- Discipline
- Mathematics
- Area
- Spectral sets and tilings
- Subject
- Discrete analysis, tilings, probability and entropy
- Result type
- Explicit counterexample, classification of complements and reproducible proof package
- Formal proof
- Standalone Lean package
- Family
binary-spectral-tile- Keywords
- Fuglede conjecture, spectral sets, translational tiling, periodic tiling property, finite abelian groups, binary vector spaces, subspace tiling complement, Ferguson–Iosevich
Statement and scope
Formal scope. Spectrality with an actual basis of all complex functions on E, the tiling E ⊕ T = F₂⁹, aperiodicity of E, the exclusion of every periodic and every subspace complement, the classification of all complements as the 512 translates of T, and the failure of the periodic tiling property for F₂⁹ are formalized in 16 Lean modules. Minimality of dimension nine depends on an external dimension-eight theorem and is not formalized.
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.pdf353 KB- PDF on GitHub
papers/mathematics/ binary-spectral-tile/ manuscript.pdf - LaTeX source
papers/mathematics/ binary-spectral-tile/ 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/ binary-spectral-tile/ - Lean project
papers/18 Lean filesmathematics/ binary-spectral-tile/ lean/ - Lakefile
papers/mathematics/ binary-spectral-tile/ lean/ lakefile.lean - Toolchain
leanprover/lean4:v4.19.0 - Library roots
Reproduce
The commands below are quoted from papers/, which gives their context and working directory.
lake exe cache get
python3 verify_release.py --lean-home "$(lean --print-prefix)" \
--mathlib .lake/packages/mathlib --packages-dir .lake/packages --out /tmp/binary-tile-verification- README
papers/mathematics/ binary-spectral-tile/ README.md - Verification guide
papers/mathematics/ binary-spectral-tile/ verification/ README.md - Verification record
papers/mathematics/ binary-spectral-tile/ VERIFICATION.md - Authorship
papers/mathematics/ binary-spectral-tile/ AUTHORSHIP.md - Repository guide
verification/README.md - Unfinished proofs
UNFINISHED.md
Source and prior work
Priority and subsequent correspondence. On 30 October 2026, through correspondence with Dr. Samuel Ferguson, I learned that he and Professor Joshua Iosevich had become aware of counterexamples to the stronger statement shortly after submitting their arXiv paper. Whether their examples are equivalent to this construction has not been established; an AI-generated comparison he shared later that day provisionally suggests that they are not affinely equivalent, but it has not been verified. Priority and novelty record.
Questions and answers
Does every spectral 64-point set in F₂⁹ have a subspace tiling complement?
No. The preprint gives an explicit 64-point spectral set E ⊂ F₂⁹ (spectrum C × F₂³) that tiles with complement T = C × {0}, and proves that its tiling complements are exactly the 512 translates of T, none of which is periodic, so no linear subspace complements E. This answers the subspace-complement part of Ferguson–Iosevich Question 8.1, and via their stated equivalence Question 8.2, negatively.
Were counterexamples already known?
Yes. Ferguson and Iosevich reported in correspondence that they had become aware of counterexamples to the stronger subspace-complement statement shortly after submitting their paper, so no priority is claimed. Whether their examples are equivalent to this construction is not established; an AI-generated comparison suggesting they are not affinely equivalent is unverified.
Does this settle Fuglede's conjecture in F₂⁹, and is it formally verified?
No; whether every spectral 64-point subset of F₂⁹ tiles remains open, and this set does tile. Spectrality, the tiling, aperiodicity, the classification of all complements and the failure of the periodic tiling property are formalized in 16 Lean 4 modules; minimality of dimension nine depends on Ferguson and Iosevich's dimension-eight theorem and is not formalized.
Cite
Citation file papers/. For the whole collection, use CITATION.cff or CITATION.bib.
@misc{goyal2026binaryspectraltile,
author = {Goyal, Dev D.},
title = {A 64-Point Spectral Tile in $\mathbb{F}_2^9$ with No Periodic Complement},
year = {2026},
month = oct,
note = {Preprint. Fully autonomous agentic research; publication responsibility: Dev D. Goyal},
url = {https://github.com/dvgyl/math-and-theory/tree/main/papers/mathematics/binary-spectral-tile}
}