The two encodings of the forbidden configuration agree
ProvedZ2nFiveEighths.cubeFree_iff_configFreeFor a finite subset of an additive abelian group, has a cube exactly when some config x y z is a subset of .
HasCube lists the seven memberships separately; config x y z collects the same seven elements into a Finset and asks for a subset. The two are not definitionally equal, because the Finset collapses duplicates when the triple is degenerate: at modulo 16 the configuration has three elements, not seven.
The claim is that deduplication changes nothing, because subset of a Finset literal is the conjunction of the memberships either way.
import Mathlib import Definitions.Def_Z2nCubeFreeLayers
namespace Z2nFiveEighths
theorem cubeFree_iff_configFree {G : Type} [AddCommGroup G] [DecidableEq G]
(A : Finset G) : CubeFree A ↔ ConfigFree A := by sorry
end Z2nFiveEighths
Read-back
What the Lean code literally says, in plain math · claude-opus-5
READ-BACK
Let G be an abelian group living in the lowest universe, with decidable equality, and let A be a finite subset of G. The theorem asserts an equivalence between two phrasings of "A contains no seven-term configuration". Left side: it is not the case that there exist elements x, y, z of G with all seven of x, y, z, x+y, y+z, z+x, x+y+z lying in A. Right side: for every triple x, y, z of elements of G, the finite set {x, y, z, x+y, y+z, z+x, x+y+z} is not a subset of A. Since that set has x, y and z among its members, "subset of A" imposes the same seven membership conditions the left side lists one by one, so the two sides expand to the identical conjunction. Nothing requires x, y, z to be distinct, to be nonzero, or to differ from their sums, so collapsed configurations count: x = y = z = 0 is admissible, and then the seven-element list is the singleton {0}.
QUANTIFIER ORDER G: implicit type variable, fixed to universe zero (the auxiliary definitions are universe polymorphic; the theorem is not). A: explicit finite subset of G, universally quantified, fixed before both sides. Left: negated existential over x, y, z ranging over all of G, with membership in A asserted as conjuncts. Right: universal over x, y, z ranging over all of G, of a negated subset claim.
HYPOTHESES AddCommGroup G: commutative, with inverses. Rules out noncommutative groups and bare monoids. The statement itself uses only addition; inverses are never applied. DecidableEq G: required to build the finite set literal. No mathematical restriction. A is finite: infinite subsets of G are outside the scope. No bound on the size of A, no exclusion of 0 from A, no distinctness or nonzeroness for x, y, z.
DEGENERATE CASES A empty: both sides hold. No element lies in the empty set, and the configuration set always contains x, so it is never a subset of the empty set. 0 in A: both sides fail, via x = y = z = 0, for every such A regardless of size. Trivial G: the only subsets are empty and {0}, both covered above. Neither side is vacuous or unsatisfiable; each holds for some A and fails for some A.
UNREADABLE Nothing. Note the proof body is omitted, so the file asserts the statement and does not establish it.
Confirmed by the mission captain (proposal self-audit).