Conjectura de Long-Wagner para n = 6: no máximo 40 resíduos módulo 64

Proved

Z2nFiveEighths.cubeFree_card_le_five_eighths_six

by BrunoDCDO · Sep 23, 2026 · Mathlib 0df444a (Lean v4.33.1)

additive-combinatoricscombinatorics

Every set $A\subseteq\mathbb Z/64\mathbb Z$ containing no configuration of the form

\{x,y,z,x+y,y+z,z+x,x+y+z\}

satisfies

|A|\le40,

or, equivalently, $8|A|\le5\cdot64$ . The generators $x,y,z$ may coincide, and all sums are taken modulo 64.

This is the case $n=6$ of Long and Wagner's Conjecture 5.1 on projective cube-free subsets of $\mathbb Z/2^n\mathbb Z$ . The constant $5/8$ is attained by the set of residues congruent to $1,3,4,5,7$ modulo 8. The result does not assert the general case of the conjecture.

After Conjecture 5.1, the authors report a Gurobi verification of a stronger statement for $n\le7$ . This theorem provides a formalization of the case $n=6$ with explicit certificates checked by the Lean kernel.

Preamble

import Definitions.Def_Z2nCubeFreeLayers

Formal statement

theorem Z2nFiveEighths.cubeFree_card_le_five_eighths_six
    (A : Finset (ZMod (2 ^ 6))) (hA : Z2nFiveEighths.CubeFree A) :
    8 * A.card ≤ 5 * 2 ^ 6 := by sorry

Source

Jason Long and Adam Zsolt Wagner, The largest projective cube-free subsets of Z_{2^n}, arXiv:1810.01225v1, Conjecture 5.1, https://arxiv.org/html/1810.01225#S5. Instance n = 6; proof by explicit integer certificates.

View graph