Recovery note (2026-08-16 afternoon): this is the q1 walkthrough recovered from the Codex rollout. The Math-agent memory log later recorded that q1 used the wrong predicate (r=1 rather than r ∉ {1,2}), commit 77d43c5. Treat the p≤200 completeness claim below as invalidated. q2 recoded the predicate; recovered compute/green_m_p.csv matches OEIS A398173 through p=47 only.

Walkthrough — From unique sums to a normalized midpoint search

• Problem: problems/unique-sum
• Run: recovered q1-overnight history
• Model: gpt-5.6-sol max
• Date: 2026-08-16 (America/Los_Angeles)
• Argument status: invalidated historical computation; current continuation in section 11
• Problem status: open; the exact table is independently replayed through $p=61$

0. What was actually missing

The missing ingredient was not a stronger generic SAT solver. It was the right local invariant and the full affine normal form it permits. A literal encoding treats every residue and every ordered sum as independent data. In an odd prime field, however, all off-diagonal representations arrive in opposite-order pairs. Only a diagonal sum can be unique. Once this is noticed, the problem becomes a small system of midpoint equations, and one of those equations normalizes three selected residues at once. That change removes the large ambient group from the hard part of the search.

1. False starts (named obstacles)

• The full ordered-sum model. We first contemplated variables for all members and all sum multiplicities. The obstruction was structural: it encoded the automatic pairing $(b,c),(c,b)$ repeatedly and concealed that only $(a,a)$ can contribute a lone ordered representation.
• A Boolean membership SAT grid. With membership variables $x_r$, a center clause can be expressed using auxiliary variables for each endpoint pair. Even after fixing $0,1$, the $p=199$, $k=9$ instance had about 23,000 variables and 66,000 clauses and did not decide in the first minute with several standard SAT engines. The issue was not formula size alone: the solver still had to rediscover affine copies of the same sparse set.
• Optimization before normalization. A CP-SAT objective on the same residue grid found small examples, but the lower bound remained the hard half. An extremal witness proves only $m(p)\le k$; it says nothing about $k-1$.
• Random local search. Simulated mutations quickly found a 10-element set for $p=199$, while repeated 9-element attempts stopped with one unsupported point. This was useful evidence about the boundary but could never certify UNSAT.
• Only two fixed residues. Translating and scaling an arbitrary selected pair to $0,1$ was valid, but it discarded the midpoint relation that had justified choosing the pair. The sorted integer model became much smaller, yet the last lower-bound cases were still unnecessarily symmetric.

2. The useful failure

The local search separated the two computational burdens. Producing a witness was easy; excluding the preceding size was expensive. At $p=199$, it found 10 selected residues in seconds, whereas size 9 repeatedly left exactly one center without a pair. This suggested that the model should name a witnessing progression, not merely two arbitrary selected points. The failed Boolean model supplied the same clue from another direction: its useful variables were precisely the endpoint pairs centered at selected residues.

The leftover of both failures was therefore the same. A selected center comes with a nontrivial three-term progression. We should spend the affine symmetry on that whole progression.

3. The click

Choose any $a\in A$. Its midpoint witness has the form $a-d,a+d$, with $d\ne0$. Translate by $-a$, then multiply by $d^{-1}$. Because $p$ is prime, the result is an affine-equivalent set containing

After sorting, three positions are fixed: $v_0=0$, $v_1=1$, and $v_{k-1}=p-1$. This was the decisive change of setting. The ambient $p$-cell membership vector disappeared; the solver only had to choose the remaining $k-3$ residues and one midpoint witness per chosen residue. With this normalization the $p=199,k=9$ boundary instance became a completed UNSAT check rather than an open-ended search.

4. The argument, in the order it became inevitable

Unique sums are unsupported diagonals

Let $p$ be odd. If $b\ne c$, every representation $b+c=x$ is paired with the distinct ordered representation $c+b=x$. Also, multiplication by 2 is injective, so a fixed sum has at most one diagonal representation. Therefore

Thus $A$ is unique-sum-free exactly when every $a\in A$ is the center of a nontrivial three-term progression in $A$. Sizes 1 and 2 are immediately impossible for odd $p$. The invalid run then claimed $m(2)=2$ from ordered multiplicity two. Under the unordered definition, however, $0+1$ has the single representation $\{0,1\}$, so no admissible set exists and $m(2)$ is undefined.

The affine normal form is exhaustive

For an odd prime and any admissible nonempty $A$, choose a center $a$ and distinct endpoints $b,c$. Writing $d=b-a$, the midpoint equation gives $c-a=-d$, and $d\ne0$ has an inverse. The affine map

preserves all midpoint equations and sends $a,b,c$ to $0,1,-1$. Consequently no candidate is lost by searching only sorted residues

This is the completeness argument behind the symmetry breaking; it is not a heuristic preference for symmetric-looking sets.

A compact exact feasibility model

For each selected center $v_i$ other than the already supported $v_0=0$, the model chooses indices $j<\ell$, both different from $i$, and imposes

Those are all possible wrap values because every $v_i$ lies between 0 and $p-1$. Strict ordering makes the residues and endpoints distinct. The disjunction over endpoint pairs is exactly the midpoint condition, so SAT produces a valid set and UNSAT excludes every set of that cardinality after the exhaustive affine normalization.

The search tries $k=3,4,\ldots$ in order and stops at the first SAT model. It nevertheless records every earlier status rather than assuming that existence is monotone in $k$. This matters in spirit because the resulting function of the prime is itself not monotone: $m(41)=8$ but $m(43)=7$.

Replay separates witnesses from lower bounds

The CSV witness is checked without trusting solver internals. For every ordered pair in $A^2$, the verifier recomputes its sum modulo $p$ and rejects if any multiplicity equals 1. It also independently rebuilds all smaller-cardinality instances. The primary model selects an integer wrap $q$; the replay expands the three wrap values into separate Boolean alternatives. The full replay checked 3,159 ordered pairs and 235 lower instances and returned VALID.

A hand-sized example shows both halves. For $p=5$, $A=\{0,1,3,4\}$ has ordered representation counts $(3,3,3,3,4)$, so none is unique. Its four centers are supported by the pairs $(1,4),(3,4),(0,1),(0,3)$, respectively. The size-3 normalized model is UNSAT, giving $m(5)=4$.

5. Figures, numeric checks, and computer search

The invalidated first run reported a table for all 46 primes at most 200. Its claimed distribution of minima $2,3,\ldots,10$ was

Those numbers use the weaker balanced-set predicate and are not values of $m(p)$.

The associated shape counts are invalid for the same reason. The current CSV records one genuine no-unique-sum witness per odd prime through $p=53$; it does not classify all affine orbits of extremizers.

The current table is the 15 primes through $p=53$ in compute/green_m_p.csv, not the invalidated $p\le200$ claim above. On that range the linear fit against $\log p$ has $R^2\approx0.979$; the fit against $(\log p)^2$ has $R^2\approx0.995$. Those numbers are descriptive diagnostics, not evidence for a new asymptotic theorem.

6. Proven vs still open

• Now established. The values for the 15 odd primes through $p=53$ in compute/green_m_p.csv have directly checked witnesses. A separate progression-driven Rust search excludes all smaller sizes; at $p=53$ its boundary run visited 333,555,078 nodes and returned UNSAT.
• Not claimed. We do not classify all extremal sets, extract an infinite construction, improve either known asymptotic bound, or infer growth from the two least-squares lines. The overall problem remains open. (Section 10 later completed the local value at $p=59$.)
• Certificate scope. There is no Lean or DRAT proof object. The finite certificate is computational and replayable: a SAT-produced witness table, direct arithmetic checks, and an independent exact branching algorithm.
• Scope check. The normalization uses both that 2 is invertible and that every nonzero $d$ is a unit. The computation restricts to odd primes and does not transfer unchanged to odd composite moduli, where a midpoint difference can be a nonunit and cannot necessarily be scaled to 1.

7. Digestion notes

The main artifacts are:

• compute/search_green_m_p.py — the cardinality-SAT search;
• compute/green_m_p.csv — all published values through $p=53$ and one extremal witness per prime;
• compute/q3/verify_exact.rs — the independent progression-driven lower search;
• compute/verify_green_m_p.py — direct witness checks, small full enumerations, and the Rust replay driver;
• compute/q3/p59_upper.json and compute/q3/verify_upper.py — the checked 15-element upper-bound witness at the unresolved next prime;
• compute/plot_m_p.py and figures/m_p.png — the finite comparison plot;
• compute/run_all.sh — the full replay.

From the repository root, the decisive replay command is:

bash problems/unique-sum/compute/run_all.sh

No Lean file is needed because the claim is a finite, independently rerun computation rather than a formal theorem about all primes.

8. The 2026-08-23 continuation

What was actually missing

The first missing object was not another witness. It was an independent lower check that did not trust statuses saved by the same SAT program. There was also a moving literature boundary: OEIS had acquired $m(53)=14$, making $p=59$ the first unpublished prime.

False starts and the useful failure

The recovered Python verifier only checked that a JSON log said UNSAT. That is bookkeeping, not independent verification. At $p=59$, four SAT engines also failed to decide exact size 14 in their initial runs. Local search repeatedly stopped at one unique sum, and an exhaustive radius-four neighborhood of 49,168,350 normalized 14-sets contained no solution. The near miss was useful as a boundary diagnostic, but neither it nor a timeout excludes any cardinality.

The click and the exact argument

Start with any partial selected set $S$. If a sum $s$ has exactly one active unordered representation in $S$, every admissible completion must contain the two endpoints of some other unordered representation of $s$. Branch over all those pairs, add their missing endpoints, and repeat. A branch either exceeds the size limit, reaches a set with no unique sum, or exhausts every forced choice. The same affine normalization as before starts the search from $\{-1,0,1\}$.

The Rust implementation additionally canonicalizes a partial set using every nontrivial three-term progression it already contains. This only identifies affine-equivalent states; it does not delete a possible completion. Memoizing those canonical masks turns the branching rule into an exact lower search whose code shares neither the SAT formula nor a solver library with the primary computation.

Computer search and the remaining wall

At $p=53$, the independent search excluded size at most 13 after 333,555,078 nodes in 1,428.475 seconds. The saved 14-set passes a direct ordered-sum count, so this replays $m(53)=14$, already published in A398173.

At $p=59$, the saved 15-set proves only $m(59)\le15$. A node-limited run at size at most 14 stopped UNKNOWN after 100,000,000 nodes and 72,327,605 memoized states in 523.030 seconds. That incomplete run is not a lower bound. Section 10 later finished the named-cover leftover.

9. The 2026-09-09 progression ladder

The missing degree of freedom was the second representation of each selected endpoint's diagonal. The affine root {-1,0,1} supports 0, but its other selected points still need midpoint witnesses. Naming those witnesses gives small, explicit families to search. It does not remove the separate requirement to repair off-diagonal unique sums.

Two obstacles persisted. The full size-at-most-14 search had no decision, and a SAT replay of the five-term progression family stopped at its first conflict budget. The Rust repair-cover search did finish that restricted family, as well as the six-term family. Moving to four terms was harder: the next Rust run reached its 600-second limit without a decision.

That failure made the leftover concrete. If every set containing an AP4 could be excluded, a remaining normalized set would avoid AP4. The selected point 1 must be the midpoint of one of 29 distinct endpoint pairs. Three choices already create an AP4; the other 26 roots fall into 25 affine classes. An alternative ladder starts from the completed AP5 exclusion: there are 27 named classes containing the normalized AP4 and avoiding AP5, followed by the same 25 AP4-free classes. A direct audit checks the pair lists, the affine maps, and coverage on small sets. It does not search those classes or prove that they are impossible.

A C implementation was prepared to complete a chosen root. It computes ordered counts by reflection intersections and asks whether all currently unique sums can be repaired within the remaining cardinality budget. Its 104 small control decisions agree with full subset enumeration through 13. The first run at 59 was interrupted when the user requested a wrap, so the C code supplies controls and a reproducible next step, with no completed exclusion at 59.

During wrap, the later independent SAT artifact arrived with AP5 UNSAT. Its formula hash matches a fresh build of the audited encoding; the Rust and SAT runs agree on that restricted predicate. The earlier UNKNOWN log remains alongside it. The exact artifacts and falsifiers are in compute/q4/CLAIM.md, and the argument for the partitions and completion search is in compute/q4/METHOD.md.

The publication boundary also moved. OEIS now reports exact values through 73, including m(59)=15. The local witness still proves only $m(59)\le15$, and the local unrestricted lower search is incomplete. This continuation did not improve a published bound. It stopped at the user's request with the named cases available for a future run.

10. The 2026-09-09 named covers

What was actually missing

The missing search was not another membership SAT run. q4 had already named the leftover: after the AP5 family is excluded, every remaining normalized 14-set is in one of 27 AP4-but-not-AP5 midpoint classes or one of 25 AP4-free classes. Those classes had been audited, not searched.

False starts and the useful failure

Seeding from the 15-sets failed for a structural reason. Both witnesses contain an AP6. Any 14-subset therefore still contains a long progression, and q4 had already excluded that family through size 14. One-, two-, and three-swap neighborhoods of 31 seeds (162,932,311 fourteen-sets) never beat the inherited near-miss of one unique sum. That neighborhood is a finite diagnostic; it taught that the construction side of the boundary sits away from the known 15-sets, in the AP5-free leftover.

The click

A six-point named root leaves eight free places, so the completion checker hits its cover test immediately. The first such class returned UNSAT in seconds. The four-point AP4-free root, which looked like the hard case, returned UNSAT in about a minute. The leftover was finite and small enough to finish.

The argument, in the order it was run

Affine-normalize to $\{-1,0,1\}$. If the set contains an AP5, map that progression to the five-term root; that family is UNSAT through size 14 in Rust and in C. Otherwise, if it contains an AP4, map to $\{-1,0,1,2\}$ and name a midpoint pair for $-1$: 27 classes, all UNSAT. Otherwise name a midpoint pair for the still-unsupported point $1$: 25 classes, all UNSAT. Every admissible set is balanced, so those named pairs exist. C uses reflection intersections; Rust uses unordered pair counts. They agree on every representative.

Computer search

AP5: Rust 1,559,513 nodes, C 925,228 nodes, both UNSAT. AP4-but-not-AP5: 27/27 UNSAT in both languages, max RSS 61 MiB. AP4-free: 25/25 UNSAT, including the 4-point root. No class timed out. No 14-set appeared.

Proven vs still open

Locally $m(59)=15$, matching OEIS A398173. That is a record match, not a new bound. The exact table at 61 through 73 is still only published, not independently replayed here. Primes from 79 onward are absent from the record. Green's #27 remains open.

11. The 2026-09-09 table step at 61

The q5 engines already take any odd prime below 64. At 61 the published 15-set contains an AP5, so the leftover after that family is again a list of named midpoint classes. Annealing size 14 and an unrestricted C search for a 15-set from $\{-1,0,1\}$ both failed to produce a witness; the published set was checked directly instead. AP5 at size 14 is UNSAT in C and in Rust. Completing 28 AP4-but-not-AP5 classes and 26 AP4-free classes, each in both languages, excludes every smaller size. Locally $m(61)=15$, matching OEIS, new to this notebook. Not a new bound. The next primes 67, 71, 73 sit above the 64-bit mask.