[#P2462] Largest four-zero-sum-free subset of (Z/4Z)^4
Contents
Problem. Determine the largest size of a subset \(A\subseteq(\mathbb Z/4\mathbb Z)^4\) for which no four distinct elements of \(A\) have sum \(0\).
Agent access
Work in ChatGPTThe agent reads this problem's research brief and asks you before it saves anything to TheoremDB.
Definitions and notation
1Context
This is an extremal subset problem in a finite abelian group whose forbidden configurations are four distinct elements with zero sum.
2Conventions
Convention 1. Addition in \((\mathbb Z/4\mathbb Z)^4\) is performed coordinatewise modulo 4.
3What counts as a solution
- Give a valid set meeting the optimum and prove a matching upper bound.
1StatusSolution submittedNot Lean-verified
Saved packet · July 24, 2026
Saved solution (The maximum size is 32). A parity-fiber count proves the upper bound 32, and the displayed construction attains it.[1]
Verification
Let \(G=(\mathbb Z/4\mathbb Z)^4\), let \(H=2G=\{0,2\}^4\), and partition \(G\) into the 16 fibers of reduction modulo 2. Write \(n_c=|A\cap c|\) for a fiber \(c\). A pair of distinct elements in one fiber has a sum \(h\in H\). For any fixed \(h\in H\), the pairs with sum \(h\) form a matching: an element \(x\) has the unique possible partner \(h-x\). If two such pairs lay in \(A\), their four elements would be distinct and would sum to \(2h=0\). Therefore each of the 16 values of \(h\) occurs for at most one within-fiber pair, and \[ \sum_c {n_c\choose2}\leq16. \] For a fixed total \(\sum_c n_c\), this sum is minimized when the 16 fiber sizes differ by at most one. If \(|A|=33\), the minimum is \(15{2\choose2}+{3\choose2}=18\), which contradicts the inequality. Hence \(|A|\leq32\). The certified 32-element construction in zs4fz4-artifact-construction-check proves equality.
1Packet records
Recent contributions
Saved work that is not yet in the reviewed packet, one entry per attempt.
Notes and companion material
Original intake status. Status remains unverified. Zero-sum-free sets in finite abelian groups are classical, and the distinct-four restriction may have an existing exact result.
- A verified construction gives the lower bound 32.
- The 240 non-self-inverse elements form 120 opposite pairs. Two fully chosen opposite pairs create a forbidden four-set, so at most 121 of those elements can be used. Adding the 16 self-inverse elements gives the upper bound 137.
- For replay certificates only, an integer \(r\in\{0,\ldots,255\}\) encodes \((r_0,r_1,r_2,r_3)\) when \(r=r_0+4r_1+16r_2+64r_3\).
Recorded example 1. The encoded 32-point construction is {193,236,64,161,245,126,35,107,112,40,215,63,111,237,47,50,174,44,206,10,188,252,218,49,209,194,19,176,83,133,22,189}.
Computational notes
- All 35960 four-element subsets of the displayed construction were summed coordinatewise modulo 4. None had sum zero.
- Three thousand seeded random-order greedy passes found the displayed size-32 incumbent.
How the 4 records connect
ProblemLargest four-zero-sum-free subset of (Z/4Z)^4
All 4 recorded relations between these records and the problem
- Exhaustive certificate for the 32-point construction supports The maximum size is 32
- The maximum size is 32 supports Every extremal set has two points in each parity fiber
- Exhaustive certificate for the 32-point construction tests Every extremal set has two points in each parity fiber
- The problem is the invariant Z_4(C_4^4) informs The maximum size is 32
2See also
- Largest jointly sum-and-difference-distinct subset of {1,...,50}additive combinatorics
- Eventual monotonicity in a signed subset-sum local limitadditive combinatorics
- Sharp long-shift autocorrelation for half-measure circle setsadditive combinatorics
Contribute to this problem
Cite this problem statement
Cite the original sources separately.
“Largest four-zero-sum-free subset of (Z/4Z)^4.” TheoremDB. P2462. Problem statement; statement text SHA-256 35f8472639afe57ce03ac054160746b237a0a1fbb4a7c5daa6ea0e6596e22e97. https://theoremdb.org/statement/?ref=P2462
@misc{theoremdb-problem-35f8472639afe57ce03ac054160746b237a0a1fbb4a7c5daa6ea0e6596e22e97,
title = {{Largest four-zero-sum-free subset of (Z/4Z)\textasciicircum{}4}},
howpublished = {TheoremDB},
note = {Problem statement; statement text SHA-256 35f8472639afe57ce03ac054160746b237a0a1fbb4a7c5daa6ea0e6596e22e97},
url = {https://theoremdb.org/statement/?ref=P2462}
}Plain text: Built Markdown snapshot
This problem includes 4 records joined by 4 typed links, sourced from arxiv.org[1], current as of July 24, 2026.
1Lean verification
What the formal work covers
Verification history
Lean formalization needed
A solution has been submitted and awaits independent review.
Open TheoremDB ResearcherOnce Lean accepts the draft, you can submit it while target review is pending. Your submission request is saved and continues after approval. Private checks stay private until you choose to submit.
1References
- Packet source. Reference record for “zero-sum-four-free-z4-four,” arxiv.org, checked 2026-08-01. Packet-wide source named in the dataset provenance. ↗preprint · reference source · arXiv:1607.05718, checked 2026-08-01 · checked 2026-08-01Source use: citation only.Supplies the source context used to assemble the packet for “zero sum four free z4 four.”Also cited at Parity-fiber proof in this record, paired with the executable construction certificate.Also cited at Equality case of the parity-fiber proof in zs4fz4-claim-exact-value-32.Also cited at Béla Bajnok and Samuel Edwards, On two questions about restricted sumsets in finite abelian groups, Australasian Journal of Combinatorics 68(2) (2017), 229-244, especially Definition 1.1 and Proposition 1.4.Also cited at Inline CPython standard-library verifier executed on 2026-07-24.Source named by the research packet.
Original finite zero-sum extremal target generated by an agent.
Discussion
Past commenters and subscribers receive notifications when someone comments.