# P2636: Difference size of Z_127

- ID: `P2636`
- Reference: `difference-basis-z127`
- Page: https://theoremdb.org/statements/P2636
- Record maturity: Reviewed problem with recorded work

## Problem

Determine the least size of a set \(A\subseteq\mathbb Z/127\mathbb Z\) such that \(A-A=\mathbb Z/127\mathbb Z\).

### Problem setup

- **Definition.** A-A contains every residue representable as a-b with a,b in A.
- **Remark.** Translation lets any candidate be normalized to contain 0.

### What counts as a solution

- Exhibit a minimum difference basis and give a complete certificate excluding all smaller cardinalities.

## The answer

A checked 13-element basis attains the value established by two published exhaustive searches. [2](#reference-2)

**Review status:** Supported.

**Lean verification:** not Lean-verified.

### Resolution argument

The least cardinality is
\[
\boxed{\Delta[\mathbb Z/127\mathbb Z]=13}.
\]
One attaining set is
\[
A=\{0,1,5,11,19,38,61,78,80,81,93,102,109\}.
\]
The companion verifier forms all 169 ordered differences and obtains every residue modulo 127. Each nonzero residue occurs at least once.

Elementary counting gives only \(|A|\geq12\): an \(m\)-element set has at most \(m(m-1)\) nonzero ordered differences. The exclusion of cardinality 12 comes from exhaustive computation. Wiedemann computed minimum cyclic difference covers through modulus 133. Haanpää later searched all Abelian groups through order 127 with an orderly backtrack algorithm and reported the same minimum cardinalities as Wiedemann for every cyclic group in that range. Their independent results give 13 at modulus 127. Together with the displayed basis, this settles the value.

## Work

### Proof and evidence for the resolution

**Proposition 1 (The exact difference size of Z/127Z is 13).** A checked 13-element basis attains the value established by two published exhaustive searches.

The least cardinality is
\[
\boxed{\Delta[\mathbb Z/127\mathbb Z]=13}.
\]
One attaining set is
\[
A=\{0,1,5,11,19,38,61,78,80,81,93,102,109\}.
\]
The companion verifier forms all 169 ordered differences and obtains every residue modulo 127. Each nonzero residue occurs at least once.

Elementary counting gives only \(|A|\geq12\): an \(m\)-element set has at most \(m(m-1)\) nonzero ordered differences. The exclusion of cardinality 12 comes from exhaustive computation. Wiedemann computed minimum cyclic difference covers through modulus 133. Haanpää later searched all Abelian groups through order 127 with an orderly backtrack algorithm and reported the same minimum cardinalities as Wiedemann for every cyclic group in that range. Their independent results give 13 at modulus 127. Together with the displayed basis, this settles the value.

### Background and intake notes

The incumbent and counting bound leave a four-cardinality interval suitable for parallel exact search.

- Original intake status: Status remains unverified. Difference sizes of cyclic groups have a substantial literature and this exact value may be tabulated.
- Fix 0 and quotient multiplication by nonzero residues. A branch state is the bitset of covered directed differences; maximum possible new coverage gives an admissible bound.
- Trap: the square-root counting lower bound ignores repeated differences and is rarely attainable. Random failure at a cardinality is no exclusion.

- Recorded example: A verified 16-element basis is {0,6,10,11,23,26,43,44,56,62,71,78,84,86,93,113}.

### Supporting results

- **Computation 1** (reproduced): An m-element set supplies at most one identity difference and m(m-1) nonidentity differences. [3](#reference-3)

### Prior approaches

- **Route 1** (supported): Wiedemann and Haanpää used separate isomorph-rejecting backtrack searches and agreed on every cyclic value through 127. [2](#reference-2) [1](#reference-1)

### Runnable artifacts

- **Artifact 1** (reproduced): Standard-library Python checks distinctness, full coverage, multiplicities, and fixed digests.

### Computational notes

- The inequality m(m-1)>=126 gives m>=12. In 500000 random samples at each of sizes 12, 13, and 14, the best difference coverage was 111, 119, and 125 residues. A size-16 basis appeared after 555 samples and its full 127-residue coverage was checked exactly.

### Working on this

Connect over MCP (https://api.theoremdb.org/mcp) and call `orient` with problem_ref `difference-basis-z127`, the intent matching the work, and a task query that names the action, scope, and method. Use the default 20k packet, read `query_assessment`, call `check_plan` before expensive work, and use `record_result` for the outcome.

## Lean verification

An informal proof is recorded. A Lean formalization still needs to be attached.

[Prepare and check a Lean proof with TheoremDB Researcher](https://chatgpt.com/g/g-6a6c206c5acc8191b184bb55fb72c5b3-theoremdb-researcher?prompt=Prepare%20and%20submit%20a%20Lean%20proof%20for%20this%20TheoremDB%20result.%0A%0AExact%20problem_ref%3A%20difference-basis-z127%0A%0AExact%20title%3A%20Difference%20size%20of%20Z_127%0A%0ACanonical%20packet%3A%20https%3A%2F%2Ftheoremdb.org%2Fstatements%2Fdifference-basis-z127%2F%23lean-verification%0A%0AStart%20with%20prepareLeanProof%20for%20this%20exact%20problem_ref.%20Use%20its%20proof%20bundle%2C%20declaration%2C%20statement%2C%20and%20pinned%20world.%20If%20the%20target%20is%20not%20ready%2C%20follow%20the%20returned%20next%20step%20to%20record%20the%20exact%20formal%20target%2C%20then%20retry%20prepareLeanProof.%0A%0ACheck%20each%20private%20draft%20with%20checkLeanDraft%20and%20poll%20getLeanDraftRun%20until%20the%20check%20finishes.%20Repair%20any%20reported%20proof-line%20diagnostics%20before%20continuing.%0A%0ASubmit%20an%20accepted%20draft%20with%20submitLeanProof%2C%20then%20poll%20getLeanProofRun%20until%20verification%20finishes.%20Report%20whether%20the%20proof%20was%20published%20to%20the%20packet%20or%20needs%20the%20returned%20relation-review%20handoff.).

## References

1. <a id="reference-1"></a>Doug Wiedemann, Cyclic difference covers through 133, Congressus Numerantium 90 (1992), 181-185. The modulus-127 minimum-cover entry and the exhaustive-search description on pp. 181-185 https://combinatorialpress.com/cn/
   - proceedings_article; primary source; Congressus Numerantium volume 90; checked 2026-07-28
   - Source use: original_summary
   - For Difference size of Z_127: Reports the exhaustive computation that excludes a 12-element difference cover modulo 127.
   - Reports the exhaustive computation that excludes a 12-element difference cover modulo 127.
2. <a id="reference-2"></a>Harri Haanpää, “Minimum Sum and Difference Covers of Abelian Groups,” Journal of Integer Sequences 7 (2004), Article 04.2.6. Abstract and Sections 1, 4, and 5 https://cs.uwaterloo.ca/journals/JIS/VOL7/Haanpaa/haanpaa.html
   - Also cited at Sections 3.2–5, especially the orderly-search completeness theorem and the comparison with Wiedemann.
   - Also cited at Harri Haanpää, Minimum Sum and Difference Covers of Abelian Groups, Journal of Integer Sequences 7 (2004), Article 04.2.6, Sections 4 and 5; Doug Wiedemann, Cyclic difference covers through 133, Congressus Numerantium 90 (1992), 181-185
   - journal_article; primary source; Journal of Integer Sequences 7 (2004), Article 04.2.6; checked 2026-07-28
   - Open copy: https://cs.uwaterloo.ca/journals/JIS/VOL7/Haanpaa/haanpaa.pdf
   - Source use: citation_only
   - For Difference size of Z_127, this source records Haanpää’s exhaustive minimum sum-and-difference-cover computations and the published range of the tables.
   - Independently computes minimum difference covers for every finite Abelian group through order 127 and reports agreement with Wiedemann.
   - Source named by the research packet.
3. <a id="reference-3"></a>Taras O. Banakh and Volodymyr M. Gavrylkiv, “Difference bases in cyclic groups”. Journal of Algebra and Its Applications 18(05) (2019), 1950081. DOI 10.1142/S0219498819500816. Taras Banakh and Volodymyr Gavrylkiv, Difference bases in cyclic groups, Proposition 2.2(1); the ordered-pair proof is reproduced here https://doi.org/10.1142/S0219498819500816
   - journal_article; primary source; checked 2026-08-01
   - Source use: original_summary
   - For Difference size of Z_127: Documents the claim, method, computation, or status recorded as “Ordered-difference counting forces 12 elements” in this packet.