Long-Wagner Conjecture 5.1: a cube-free set mod $2^n$ has size at most $\frac{5}{8}2^n$

READ-BACK

For every natural number n with n at least 4, and every finite subset A of the additive group of residues modulo 2^n (cyclic of order 2^n), if A contains no triple x, y, z of its own elements for which the three pairwise sums x+y, y+z, z+x and the total x+y+z also lie in A, then 8*|A| is at most 5*2^n; that is, A occupies at most five eighths of the group. Unpacking the local definitions: the forbidden configuration asks for elements x, y, z (not required to be distinct, and not required to be nonzero) such that all seven values x, y, z, x+y, y+z, z+x, x+y+z belong to A, these being the sums over the seven nonempty sub-multisets of {x, y, z}. The hypothesis is the negation, so equivalently: for all x, y, z in A, at least one of x+y, y+z, z+x, x+y+z lies outside A. The bound is non-strict, stated in natural numbers with no division, and the constant 5/8 and the exponent n are fixed, not existentially quantified. The proof is admitted (sorry), so only the statement is present.

QUANTIFIER ORDER n : natural number, universal, outermost; everything after depends on it. hn : the assumption 4 <= n. A : a finite subset of Z/2^n, universal, its type depending on n. hA : the assumption that A avoids the configuration. Inside that assumption: x, y, z are existentially quantified over the group, all three under one negation, hence universally quantified in the hypothesis as used.

HYPOTHESES 4 <= n: rules out groups of order below 16 (n = 0,1,2,3), so Z/1 through Z/8 are excluded. Ambient group is Z/2^n specifically: the target is not stated for a general abelian group, even though the two auxiliary definitions are. AddCommGroup on the auxiliary definitions: commutativity makes z+x the same as x+z and x+y+z unambiguous; it is satisfied here automatically. hA: rules out every A containing a full seven-element sum pattern. In particular taking x = y = z = 0 shows 0 in A alone violates it, so any admissible A omits 0; taking x = y = z = a shows no a can have a, 2a, 3a all in A.

DEGENERATE CASES A empty: the hypothesis holds vacuously and the conclusion reads 0 <= 52^n, true. The hypothesis is satisfiable with large sets, so the theorem is not vacuous: the odd residues form a set of size 2^(n-1) = 42^(n-3) whose pairwise sums are all even, and every singleton {a} with a nonzero qualifies. The forced exclusion of 0 gives |A| <= 2^n - 1 for free, which is weaker than the stated 5*2^(n-3) for every n >= 4. No subtraction or division appears, so no truncation effects in the natural numbers.

UNREADABLE nothing