Conjectura de Long-Wagner para n = 7: no máximo 80 resíduos módulo 128

Open

Z2nFiveEighths.cubeFree_card_le_five_eighths_seven

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

additive-combinatoricscombinatorics

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

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

satisfies

|A|\le80,

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

This is the case $n=7$ 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=7$ with explicit certificates checked by the Lean kernel.

Preamble

import Definitions.Def_Z2nCubeFreeLayers

Formal statement

theorem Z2nFiveEighths.cubeFree_card_le_five_eighths_seven
    (A : Finset (ZMod (2 ^ 7))) (hA : Z2nFiveEighths.CubeFree A) :
    8 * A.card ≤ 5 * 2 ^ 7 := 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 = 7; proof by explicit integer certificates, checked by positional encoding of the coefficients.

View graph