Cube-free sets and layers in
DefinitionZ2nCubeFreeLayersThe six definitions the Long-Wagner cube-free mission is stated in.
HasCube A says some triple , not required distinct, has all seven of , , , , , , inside . CubeFree A is its negation.
config x y z is the same seven elements as a Finset, which collapses duplicates on a degenerate triple, and ConfigFree A says no config is a subset of . The equivalence of the two encodings is a milestone of the mission, not an assumption of it.
layerIdx n x is the layer of in the Long-Wagner partition of : layer for is the residues congruent to mod , and layer is . It is defined through the 2-adic valuation rather than through a congruence, because the congruence form leaves in no layer at all. IsLayerUnion n A says contains a whole layer whenever it contains one element of it.
import Mathlib
/-!
# Definition item: cube-free sets and layers in `ZMod (2^n)`
The one definition item of the `z2n-five-eighths` mission proposal. `p2m
item-add --kind definition` uploads this file whole, as the module
`Definitions.Def_Z2nCubeFreeLayers`, and every theorem item of the mission
imports it.
A definition item is a module rather than a declaration. The platform's own
corpus works that way: `Def_NgoRootDatumIsogeny` carries a structure and two
definitions, none of them named `NgoRootDatumIsogeny`. So `definition_name` is
the module name here and the six declarations below keep the names the
mathematics gives them.
Two encodings of the same forbidden configuration sit here side by side.
`HasCube` lists the seven memberships and `config` collects the same seven
elements into a `Finset` and asks for a subset. They are not definitionally
equal, because the `Finset` collapses duplicates when the triple is degenerate.
Proving them equivalent is a milestone of the mission, not an assumption of it.
Every binder is explicit. A `variable` line would be dropped when this file is
read for upload, and the module would arrive missing a hypothesis.
Ported on 2026-09-16 from `Workbench/Bench/z2n-five-eighths/Defs.lean`.
-/
namespace Z2nFiveEighths
/-- `HasCube A` says some triple `x, y, z` has all seven of its nonzero subset
sums inside `A`. The triple is unconstrained, so `x = y = z = 0` is allowed. -/
def HasCube {G : Type*} [AddCommGroup G] (A : Finset G) : Prop :=
∃ x y z : G, x ∈ A ∧ y ∈ A ∧ z ∈ A ∧
x + y ∈ A ∧ y + z ∈ A ∧ z + x ∈ A ∧ x + y + z ∈ A
/-- `CubeFree A` is the hypothesis of the problem: `A` contains no affine
3-cube. -/
def CubeFree {G : Type*} [AddCommGroup G] (A : Finset G) : Prop := ¬ HasCube A
/-- The forbidden 7-element configuration generated by `x`, `y`, `z`. As a
`Finset` this has fewer than seven elements when the triple is degenerate. -/
def config {G : Type*} [AddCommMonoid G] [DecidableEq G] (x y z : G) : Finset G :=
{x, y, z, x + y, y + z, z + x, x + y + z}
/-- `A` is configuration free: no triple `x, y, z` has its whole configuration
inside `A`. The triple need not consist of distinct elements. -/
def ConfigFree {G : Type*} [AddCommMonoid G] [DecidableEq G] (A : Finset G) :
Prop := ∀ x y z : G, ¬ config x y z ⊆ A
/-- The layer index of a residue mod `2^n`.
Long and Wagner partition `ZMod (2^n)` into `n + 1` layers, where layer `i` for
`1 ≤ i ≤ n` is the residues congruent to `2^(i-1)` mod `2^i`, and layer `n + 1`
is `{0}`. So layer 1 is the odd residues, layer 2 those congruent to 2 mod 4,
and so on, with layer `i` of size `2^(n-i)`.
Written through the 2-adic valuation rather than through a congruence, because
the congruence form needs the last layer special-cased: `0` is congruent to
`2^n` mod `2^(n+1)` only outside the stated range, so a filter would put it in
no layer at all. The valuation form gives the same partition with the `x = 0`
case stated once and visibly. -/
noncomputable def layerIdx (n : ℕ) (x : ZMod (2 ^ n)) : ℕ :=
if x = 0 then n + 1 else padicValNat 2 x.val + 1
/-- `A` is a union of layers: whenever it contains one element of a layer it
contains the whole layer.
This is the hypothesis of Long-Wagner Theorem 1.10, which is proved mathematics,
unlike their Conjecture 5.1 for arbitrary sets. -/
def IsLayerUnion (n : ℕ) (A : Finset (ZMod (2 ^ n))) : Prop :=
∀ x y : ZMod (2 ^ n), x ∈ A → layerIdx n x = layerIdx n y → y ∈ A
end Z2nFiveEighths
Read-back
What the Lean code literally says, in plain math · claude-opus-5
HasCube
READ-BACK
The payload contains one definition and no theorem. It names a property of a finite subset A of an arbitrary abelian group G, written additively. The property holds exactly when one can choose three group elements x, y, z, not required to be distinct and not required to be nonzero, such that all seven of x, y, z, x+y, y+z, z+x and x+y+z lie in A. These are the sums over the seven nonempty sub-multisets of the triple; the empty sum 0 is not required to lie in A. The condition is symmetric under permuting x, y, z, since addition commutes, and x+y+z is unambiguous. The payload asserts nothing about any particular A: as a definition it carries no proof obligation, and it imposes no cardinality, density or structural condition on A, nor any condition on G beyond being an abelian group.
QUANTIFIER ORDER G: implicit, universally quantified type. Instance argument: G carries an abelian group structure. A: explicit argument, a finite subset of G; the property is about this A. Then inside the body, in order: exists x in G, exists y in G, exists z in G, jointly scoping all seven membership conditions.
HYPOTHESES Abelian group on G: gives associativity, commutativity, a zero and inverses. Rules out nonabelian groups and structures without inverses. Satisfied by every abelian group, of any order, torsion or not. A is typed as a finite set. Finiteness is never used in the body; the same words read identically for an arbitrary subset. Absent: no nonemptiness of A, no distinctness among x, y, z, no requirement that any of them be nonzero, no lower bound on the size of A, no condition on the order or exponent of G.
DEGENERATE CASES A empty: the property is false, since x in A cannot be satisfied. 0 in A: the property holds for free, taking x = y = z = 0, since all seven sums are 0. x = y = z = a is permitted, so the property reduces in that case to a, 2a and 3a all lying in A; hence a three-element set of the form {a, 2a, 3a} satisfies it with no zero present. A a singleton {a}: holds if and only if a = 0. G the trivial group: the property holds if and only if A is nonempty. Because the witnesses may coincide, the seven listed memberships can name as few as one distinct element, so the property does not force A to have seven elements.
UNREADABLE nothing.
CubeFree
READ-BACK
The payload holds two definitions and no theorem, so it asserts nothing and proves nothing. Both definitions take an arbitrary additive commutative group G and a finite subset A of G. The first, aux1 A, says there exist group elements x, y, and z, not required to be distinct and not required to be nonzero, such that all seven of x, y, z, x+y, y+z, z+x, and x+y+z lie in A. The second, target A, is the negation of that: for every choice of x, y, and z in G, at least one of those seven elements lies outside A. No cardinality, density, bound, constant, or exponent appears anywhere in the payload. target is a property a finite set may or may not have, and no set is claimed to have it.
QUANTIFIER ORDER G: implicit type variable, universal over both definitions. [AddCommGroup G]: instance argument, same scope. A : Finset G: explicit argument of each predicate. x, y, z: existential inside aux1, all three in one block with no dependence between them, so their relative order carries no content. Under the negation in target they read as universal.
HYPOTHESES AddCommGroup G: addition is associative and commutative, with a zero and inverses. The bodies use only addition, so the natural numbers satisfy the written conditions yet are excluded by the typeclass. Non-commutative groups are excluded. Finset G: A is finite. Nothing demands it be nonempty, and nothing demands 0 not in A. The seven memberships are separate conjuncts. x + y + z parses as (x + y) + z, which equals the other grouping by associativity.
DEGENERATE CASES A empty: no witnesses exist, so aux1 A fails and target A holds for free. 0 in A: take x = y = z = 0. All seven memberships collapse to 0 in A, so aux1 A holds and target A fails. So target A forces 0 not in A. Repeats are allowed, so x = y = z = a forces a second consequence: no a can have a, 2a, and 3a all in A when target A holds. A singleton {a} with a nonzero satisfies target, since 2a in A would force a = 0.
UNREADABLE nothing.
config
READ-BACK
The payload contains no theorem, no proposition and no claim. It is a single definition. Given a type G carrying a commutative additive monoid structure with decidable equality, and three elements x, y, z of G, it returns the finite subset of G whose members are the seven expressions x, y, z, x+y, y+z, z+x, and (x+y)+z. In words: the set of all sums over the nonempty subsets of the three-element list (x, y, z), one term per nonempty subset, the empty sum 0 deliberately absent. Because this is set-builder notation over a finite set and not a list or multiset, repeated values collapse. The result is the image of those seven expressions, so its cardinality is anywhere from 1 to 7 depending on coincidences among the values. Nothing in the payload asserts that the seven are distinct, and nothing asserts any property of the set at all: no cardinality claim, no sum-free claim, no membership claim. A definition of this shape cannot be true or false, so whatever the surrounding argument needs of it is stated elsewhere.
QUANTIFIER ORDER G implicit, universe-polymorphic type, outermost. Instance argument: G is an additive commutative monoid. Instance argument: equality on G is decidable. x, y, z explicit elements of G, in that order, innermost. The body is a term, so there is no further quantification.
HYPOTHESES Commutative additive monoid on G: gives 0, associativity, commutativity. Rules out non-associative or non-commutative addition. Does not supply negation or subtraction, so G need not be a group; the natural numbers qualify. The identity 0 is never used in the body. Decidable equality on G: needed only to form the finite set; it constrains which types can be instantiated but adds no mathematical content. No hypothesis separates x, y and z, no nonzero or distinctness condition, no positivity, no finiteness of G.
DEGENERATE CASES If G is trivial, or x = y = z = 0, the result is the one-element set {0}. If x, y, z coincide in pairs, or if a pairwise sum equals a singleton or the triple sum, the set shrinks below 7 elements silently. For instance in the integers modulo 2 with x = y = z = 1 the result is {0, 1}, of size 2. The result is never empty: x always belongs to it. Nothing is vacuous, since there are no hypotheses to fail and the definition is total.
UNREADABLE nothing.
ConfigFree
READ-BACK
The payload contains no theorem and no proof obligation. It defines a property, target, of a finite subset A of an additive commutative monoid G. A has the property exactly when, for every triple x, y, z of elements of G, the finite collection consisting of x, y, z, x+y, y+z, z+x and x+y+z is NOT a subset of A. In words: A contains no full set of nonempty subset sums of any triple drawn from G. The triple is completely unrestricted: x, y, z need not be distinct from one another, need not be nonzero, and are not required in advance to lie in A (though containment would force them in). Because a finite-set literal collapses duplicates, the collection can have fewer than seven distinct members. Taking x = y = z = a it is {a, 2a, 3a}; taking x = y = a and z = 0 it is {0, a, 2a}; taking x = y = z = 0 it is the singleton {0}. Consequently the property, as written, forces 0 not in A, and forces that no a in A has both 2a and 3a in A. Only commutativity, associativity and a zero are assumed; no subtraction, so the definition is available on monoids such as the naturals as well as on groups.
QUANTIFIER ORDER G: implicit type, universal, outermost. Two instance arguments on G (below), universal. A: a finite subset of G, universal, the argument of the predicate. x, y, z: universal over all of G, inside the body of the predicate, innermost; independent of each other and of A. The negation sits inside all three, so the assertion is "for every triple, not a subset", not "not (for every triple ...)".
HYPOTHESES AddCommMonoid G: addition is associative and commutative with a zero; rules out noncommutative addition; does not supply inverses or cancellation. Note x + y + z parses as (x + y) + z, which equals every other bracketing here. DecidableEq G: equality on G is decidable. Needed to form the finite set and collapse repeats; classically no mathematical restriction. There are no hypotheses on A (no nonemptiness, no finiteness bound beyond being a finite set, no sum-free or distinctness condition), and none on x, y, z.
DEGENERATE CASES A empty: the property holds vacuously, since the collection always contains x and so is nonempty. 0 in A: the property fails immediately, via x = y = z = 0. G a one-element monoid: the property holds only for A empty. Torsion or repeats in the triple reduce the collection to 1, 2, 3, 4, 5 or 6 elements rather than 7; the condition applies to all these reduced cases with equal force. Nothing here is unsatisfiable; the empty set satisfies the predicate in every G.
UNREADABLE nothing.
layerIdx
READ-BACK
The payload contains no proposition, no theorem and no proof obligation. It is a single function definition, so it asserts nothing; it can only be read for what it computes. There are no auxiliary declarations.
The declaration takes a natural number n and an element x of the ring of integers modulo 2^n, and returns a natural number. If x is the zero element of that ring, the result is n + 1. Otherwise the result is one more than the 2-adic valuation of the canonical representative of x, where the representative is the integer in {0, 1, ..., 2^n - 1} congruent to x, and the 2-adic valuation of a positive integer m is the largest k with 2^k dividing m. For n at least 1 and x nonzero, the representative lies in {1, ..., 2^n - 1}, so its valuation runs from 0 (odd representative) up to n - 1 (representative 2^(n-1)), and the returned value runs over the whole of {1, ..., n}. Zero is assigned n + 1, exactly one above the maximum of the nonzero branch, so the function is onto {1, ..., n + 1}.
The zero guard is doing real work rather than avoiding a junk value: the Mathlib convention is that the 2-adic valuation of 0 is 0, so without the guard zero would have received the value 1, the same value as every odd representative. The guard replaces that with n + 1.
QUANTIFIER ORDER n : natural number, explicit argument, scopes over the type of x and over the body. x : element of the integers modulo 2^n, explicit argument, its type depends on n. No existential binder anywhere, and no quantified claim about the outputs.
HYPOTHESES None. No hypothesis that n is nonzero, none on x, and no primality or Fact assumption. The only typeclass appeal is decidable equality on the integers modulo 2^n, resolved by instance, which rules out nothing mathematically. The definition is marked noncomputable, a consequence of how the valuation function is defined in Mathlib, with no effect on the mathematical content.
DEGENERATE CASES n = 0: the modulus is 1, the ring has a single element and that element is zero, so the value is 1 and the nonzero branch is unreachable. n = 1: the one nonzero element has representative 1, valuation 0, value 1; zero gives 2. x = 0 at any n: the value is n + 1, which the nonzero branch never produces. No hypothesis can fail, so nothing here is vacuous; the function is total and every case is reachable except as noted at n = 0.
UNREADABLE Nothing.
IsLayerUnion
READ-BACK
The payload contains no theorem; it defines a predicate. Fix a natural number n and work in the ring of residues modulo 2^n (for n = 0 this is the one element ring). Each element x gets a label: if x = 0 the label is n+1, otherwise it is 1 plus the exponent of 2 in the factorization of the canonical representative of x in {0,...,2^n - 1}. For nonzero x that representative lies in [1, 2^n - 1], so its 2-adic valuation is at most n-1 and the label lies in [1, n]; the label n+1 thus belongs to 0 alone. The predicate says of a finite set A of residues: whenever x lies in A and y is any residue with the same label as x, then y lies in A. Equivalently, A is a union of label classes, closed under the equivalence "representatives have equal 2-adic valuation", with 0 its own class. The class with label k, for 1 <= k <= n, is the residues divisible by 2^(k-1) but not by 2^k, of size 2^(n-k). Nothing is asserted to hold: no bound, no existence claim, no proof obligation.
QUANTIFIER ORDER n : natural number, parameter of both declarations, outermost. A : finite set of residues mod 2^n, second parameter of the predicate. x : universally quantified over all residues, in the body. y : universally quantified over all residues, after x, independent of x. No existential binder occurs.
HYPOTHESES x in A: membership premise; rules out saying anything when A is empty. label x = label y: equality of assigned labels. Symmetric, so this is closure under an equivalence relation, not a one-way condition. y is drawn from the whole ring, not from A. No written typeclass hypothesis. Decidable equality for the finite set comes from instances; the valuation function is marked noncomputable. No primality hypothesis appears, since the base 2 is a literal.
DEGENERATE CASES A empty: the condition holds vacuously. A the whole ring: holds. n = 0: the ring has one element, which is 0 with label 1; both possible sets A satisfy the condition. The 0 class is a singleton, so 0 in A forces no other membership. The off-by-one in the labels matters: without it, 0 would collide with the odd residues, since the valuation of 0 is 0 by convention. As written, no nonzero element reaches label n+1. Being a definition, it carries no proof obligation, so no question of a vacuous theorem arises here.
UNREADABLE nothing.
Confirmed by the mission captain (proposal self-audit).