Cota para conjuntos livres de cubos a partir de um par x, 2x e um período de x

Proved

Z2nFiveEighths.cubeFree_card_bound_of_period

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

additive-combinatoricscombinatorics

Let $G$ be a finite abelian group and let $A\subseteq G$ be free of three-dimensional projective cubes, allowing repeated generators. If $x\in A$ , $2x\in A$ , and $mx=0$ for an integer $m\ge0$ , then

m|A|\le\left\lfloor\frac{2m}{3}\right\rfloor|G|.

The period $m$ need not be the exact order of $x$ . In particular, $m=8$ or $m=16$ implies $8|A|\le5|G|$ , and $m=4$ implies $2|A|\le|G|$ . The hypotheses that $x$ and $2x$ belong to $A$ are essential; this statement does not assert the bound $5/8$ for all cube-free sets.

Preamble

import Definitions.Def_Z2nCubeFreeLayers

Formal statement

theorem Z2nFiveEighths.cubeFree_card_bound_of_period
    {G : Type*} [AddCommGroup G] [Fintype G] [DecidableEq G]
    (A : Finset G) (hA : Z2nFiveEighths.CubeFree A)
    (x : G) (hx : x ∈ A) (h2x : x + x ∈ A)
    (m : ℕ) (hperiodo : m • x = 0) :
    m * A.card ≤ (2 * m / 3) * Fintype.card G := by sorry

Source

Lemma derived by counting periodic windows. Context: Yuchen Meng, On Cube-Free Problems, EJC 33(1) (2026), #P1.16, p. 5, proof of Theorem 9 (bound 2N/3 using the cube with generators x,x,y); https://doi.org/10.37236/14052. Application to Long and Wagner's Conjecture 5.1, Section 5, https://arxiv.org/html/1810.01225#S5.

View graph