The tight case: a cube-free set containing every odd residue

Proved

Z2nFiveEighths.cubeFree_containing_odds

by aarontcao · Sep 17, 2026 · Mathlib 0df444a (Lean v4.33.1)

additive-combinatoricscombinatorics

Let $8 \mid N$ and let $A \subseteq \mathbb{Z}/N\mathbb{Z}$ be cube-free and contain every residue of odd value. Then $8|A| \le 5N$ .

This is the case where the conjecture is tightest: a cube-free set that already contains all $N/2$ odd residues cannot beat the construction by adding even ones, and the bound says exactly how many even residues it may add.

Preamble

import Mathlib
import Definitions.Def_Z2nCubeFreeLayers

Formal statement

namespace Z2nFiveEighths

theorem cubeFree_containing_odds (N : ℕ) [NeZero N] (hN : (8 : ℕ) ∣ N)
    (A : Finset (ZMod N)) (hA : CubeFree A)
    (hodd : ∀ x : ZMod N, x.val % 2 = 1 → x ∈ A) :
    8 * A.card ≤ 5 * N := by sorry

end Z2nFiveEighths

Source

Jason Long and Adam Zsolt Wagner, "The largest projective cube-free subsets of Z_{2^n}", arXiv:1810.01225, https://arxiv.org/abs/1810.01225; the all-odds bound stated here, for every modulus divisible by 8, is a step of this formalization rather than a numbered result of the paper

Read-back

What the Lean code literally says, in plain math · claude-opus-5

READ-BACK

Let N be a nonzero natural number divisible by 8, and let A be a finite set of residues mod N. Call a triple (x,y,z) of elements of A closed when x+y, y+z, z+x and x+y+z all lie in A too; x, y, z need not be distinct and none is required to be nonzero. The theorem assumes A contains no closed triple, and assumes A contains every residue whose canonical representative in {0,...,N-1} is odd. Under those assumptions it concludes 8|A| <= 5N, that is |A| <= 5N/8. The constant 5/8 is fixed rather than existentially quantified, the inequality is non-strict, and it is stated over the naturals with no division.

QUANTIFIER ORDER N : natural, universal, scopes over all that follows. A : finite set in Z/NZ, universal, after N. x, y, z in the no-closed-triple hypothesis: universal over Z/NZ (a negated existential), scope local to that hypothesis. x in the odd hypothesis: universal over Z/NZ, scope local.

HYPOTHESES NeZero N: rules out N = 0, where Z/0Z would be the integers. 8 divides N: restricts to N in {8,16,24,...}; nothing is claimed for other N. With NeZero this forces N >= 8. No closed triple: for all x, y, z in A, at least one of x+y, y+z, z+x, x+y+z lies outside A. Taking x=y=z=0 shows this rules out 0 in A. Taking x=y=z=a shows no a in A can have both 2a and 3a in A. Odd hypothesis: forces all N/2 odd-representative residues into A, so A is nonempty and |A| >= N/2. Even residues are neither required nor forbidden, beyond what the triple condition excludes. Additive commutative group typeclass on the two auxiliary definitions: satisfied by Z/NZ, so it constrains nothing at the point of use.

DEGENERATE CASES The hypotheses are jointly satisfiable for every admissible N: take A to be exactly the odd residues. N is even, so a sum of two odd representatives is even, hence no closed triple exists, and 8|A| = 4N <= 5N. The statement is therefore not vacuous. A can be neither empty nor a set containing 0. N = 0 and N not divisible by 8 carry no claim. Smallest instance N = 8: with 1, 3, 5, 7 forced into A, the claim is |A| <= 5.

UNREADABLE nothing.

Human review

Endorsed by Shuze Chen · Sep 17, 2026
Endorsed by aarontcao · Sep 17, 2026
Confirmed by the mission captain (proposal self-audit).

View graph