[#P2462] Largest four-zero-sum-free subset of (Z/4Z)^4

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 ChatGPT

The 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.

1Status

Saved packet · July 24, 2026

What counts as a solution

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

Show recorded summaries

Record	Kind	Assessment
A parity-fiber count proves the upper bound 32, and the displayed construction attains it.	Result	Evidence: Reproduced A replay is recorded for this computation. Inspect the replay record for its procedure and scope.
claim · Computation 1 A parity-fiber count proves the upper bound 32, and the displayed construction attains it.^[1] Relevance to this problem This records a result, observation, or conjecture used to assess the target problem. Evidence ReproducedA replay is recorded for this computation. Inspect the replay record for its procedure and scope. Record state established Scope subsets of (Z/4Z)^4 with four distinct zero-sums forbidden Sources Reference 1 Details 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. Related: Computation 2 Open full record →
Equality in the upper-bound count fixes all 16 fiber sizes and all 16 within-fiber pair sums.	Result	Evidence: Reproduced A replay is recorded for this computation. Inspect the replay record for its procedure and scope.
claim · Computation 2 Equality in the upper-bound count fixes all 16 fiber sizes and all 16 within-fiber pair sums.^[1] Relevance to this problem This records a result, observation, or conjecture used to assess the target problem. Evidence ReproducedA replay is recorded for this computation. Inspect the replay record for its procedure and scope. Record state established Scope every 32-element four-zero-sum-free subset of (Z/4Z)^4 Sources Reference 1 Details When \(\|A\|=32\), the convexity minimum of \(\sum_c{n_c\choose2}\) is 16. The proved upper inequality is also 16, so equality holds throughout. Every parity fiber contains exactly two points. Their 16 sums are distinct elements of \(H\), hence they use every element of \(H\) exactly once. The displayed construction has this forced structure. Open full record →
Primary literature supplies the standard invariant and nearby results; the fixed exponent-four value was not located.	Trace	Outcome: Inconclusive Evidence: Inconclusive The recorded search or audit ended without settling the question.
attempt · Route 1 Primary literature supplies the standard invariant and nearby results; the fixed exponent-four value was not located.^[1] Relevance to this problem This records a line of attack on the target problem, including what it establishes and where it stops. Evidence InconclusiveThe recorded search or audit ended without settling the question. Scope published results on weakly four-zero-sum-free subsets of finite abelian groups Sources Reference 1 What happened Bajnok and Edwards define \(Z_h(G)\) as the largest size of a subset of \(G\) containing no \(h\) distinct elements with sum zero. The present answer is \(Z_4(C_4^4)=32\). Their Proposition 1.4 identifies weak four-zero-sum-freeness with the weak Sidon property for elementary abelian 2-groups. That equivalence uses every element being self-inverse and does not extend directly to \(C_4^4\). Their exact theorems concern large values of \(h\) relative to \(\|G\|\). A focused search using the invariant, group, and distinct-four formulation did not locate the fixed value proved here. Publication novelty remains unverified. Related: Computation 1 Open full record →
The script checks all 35,960 four-subsets and records the equality structure behind the upper bound.	Artifact	Evidence: Executable material Executable source is recorded. Inspect its inputs and instructions before attempting a replay.
artifact · Artifact 1 The script checks all 35,960 four-subsets and records the equality structure behind the upper bound.^[1] Relevance to this problem This supplies a computation, dataset, or executable check used to assess the target problem. Evidence Executable materialExecutable source is recorded. Inspect its inputs and instructions before attempting a replay. Record state available Scope the displayed encoded 32-point subset of (Z/4Z)^4 Sources Reference 1 Entry point `join source_lines with newline and run with python3` Runtime CPython 3.9 or later Details The encoded set 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\}. \] The verifier decodes each integer in base 4, checks every four-element subset, and asserts that none sums to zero coordinatewise modulo 4. It also checks that every parity fiber has size two and that the 16 within-fiber pair sums are exactly \(\{0,2\}^4\). Related: Computation 1 · Computation 2 Open full record →
No records match these filters.

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

The overview places each record once. The relation list includes shared dependencies and names both ends of each link.

ProblemLargest four-zero-sum-free subset of (Z/4Z)^4

All 4 recorded relations between these records and the problem

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.

Plain text

“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

BibTeX

@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

Lean formalization needed

A solution has been submitted and awaits independent review.

Open TheoremDB Researcher

Upload a Lean project archive

Once 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.

[#P2462] Largest four-zero-sum-free subset of (Z/4Z)^4

1Context

2Conventions

3What counts as a solution

1Status

1Packet records

Recent contributions

Computational notes

2See also

1Lean verification

What the formal work covers

1References

Discussion

Report comment

Background

Definitions

What counts as a solution

What's known

Formal statement

Recorded work

Record & provenance

Flag this problem

Sign in to follow

Report a problem

1Context

2Conventions

3What counts as a solution

1StatusSolution submittedNot Lean-verified

1Packet records

Recent contributions

Computational notes

2See also

1Lean verification

What the formal work covers

1References

Add a comment

Background

Definitions

What counts as a solution

What's known

Formal statement

Recorded work

Related work

Record & provenance

1Status