Indeed, (2) is the first place where the membership decisions for the tail

\(A(n)-n\) differ from those for \(C\).

Proof

(a) Suppose inductively that all decisions at offsets below \(b\) agree

with \(C\). A 3-term progression ending at \(n+b\) whose first two terms

are both in the translated tail has the form

After subtracting \(n\), this is exactly the obstruction used by the greedy

construction of \(C\). Consequently such an obstruction exists exactly

when the canonical greedy process rejects \(b\).

(a) The only other possible progression uses the isolated original term

0. Since 0 is the smallest term, it must be the first endpoint, and the

progression has the form

It exists exactly when \(b=n+2x\). Before the first member of

\(C\cap(n+2C)\), this adds no obstruction to a canonical member \(b\).

Every nonmember of \(C\) is already rejected by a pair in the translated

tail. At \(b=d(n)\), the canonical process would accept \(b\), but

is an arithmetic progression, so \(n+d(n)\) is rejected. Induction proves

(1)–(2).

The first obstruction is computable in \(O(\log n)\)

(a) Let \(n=\sum_{i=0}^{L-1}\nu_i3^i\). To find the least \(x\), use

digits \(e_i\in\{0,1\}\) for \(x\), output digits \(f_i\in\{0,1\}\) for

\(n+2x\), and a carry \(c_i\in\{0,1\}\):

For each pair \((\nu_i,c_i)\) at least one of \(e_i=0,1\) makes the residue

0 or 1. Dynamic programming retains, for each outgoing carry, the least

partial value \(\sum_{h\leq i}e_h3^h\). A final carry 1 is cleared with one

extra output digit 1 and \(e_L=0\). Thus the automaton never dies and its

least path is exactly \(x(n)\). This is the routine

first_conflict_digit_dp in the checker.

(a) The construction also gives

Hence (1) explicitly determines

\(\Theta(n^{\log_3 2})\) initial terms, uniformly in the seed \(n\).

Some exact examples are:

| seed \(n\) | \(x(n)\) | \(d(n)\) | \(r(n)\) | translated terms proved by (1) |

|---:|---:|---:|---:|:---|

| 1 | 0 | 1 | 1 | \(1\) |

| 2 | 1 | 4 | 3 | \(2,3,5\) |

| 3 | 0 | 3 | 2 | \(3,4\) |

| 4 | 0 | 4 | 3 | \(4,5,7\) |

| 5 | 4 | 13 | 7 | \(5,6,8,9,14,15,17\) |

| 14 | 13 | 40 | 15 | \(14+\phi(0),\ldots,14+\phi(14)\) |

All table entries follow from the digit DP and equations (1)–(3), so the

table is (a); the checker also recomputes them as (d).

Sharp fixed-index corollary

(a) For every fixed \(k\geq1\),

For every \(k\geq2\), the threshold is sharp as a uniform assertion: at

\(n=\phi(k-1)\), all earlier translated terms occur, but the proposed

\(k\)-th term \(2n\) is excluded by \(0,n,2n\). Thus

This gives a complete, sharp answer for every fixed index in the

large-seed regime, but it does not address \(k\to\infty\) with the seed

fixed.

I did not find this prefix/first-conflict formulation stated in the sources

inspected. I make no publication-level novelty claim for an elementary

observation.

Exact \(A(4)\) computation and two indexing corrections

The standalone checker is

erdos271_wave8p_reverify.py.

It uses no third-party packages.

Independent checks performed

• (d) A forward generator marks every future endpoint \(2y-x\) after

accepting \(y\).

• (d) A separate direct candidate oracle, which scans earlier middle

terms and performs set lookups, gives identical first 192 terms for every

\(1\leq n\leq64\).

• (d) The digit DP agrees with definition-level brute force for every

\(1\leq n\leq5000\).

• (d) Formula (1), including rejection of its first conflicting

translate, agrees with direct greedy generation for every

\(1\leq n\leq1000\).

• (d) For \(A(4)\) through \(a_{20000}\), an independent second pass

rebuilds \(2y-x\) for all \(\binom{20001}{2}=200{,}010{,}000\) accepted

pairs. It checks both directions: no accepted value is covered

(3-freeness), and every omitted integer from 5 through \(a_{20000}\) is

covered (greedy completeness).

The full sequence certificate is

SHA256(le64(a_0..a_20000))
= 845d8b86c929fdeaa48d439f9f8db717cc572de98796d9b3b001d8615f2d7923

Here each term is encoded as one unsigned 8-byte little-endian integer.

Let

The benchmark \(a_j=j^2/(2\log j)\) is \(q_j=1/2\). Exact certified

checkpoints are:

| zero-based \(j\) | \(a_j\) | \(q_j\) |

|---:|---:|---:|

| 1,999 | 259,183 | 0.492966612937 |

| 2,000 | 262,751 | 0.499286180537 |

| 4,999 | 1,110,974 | 0.378637758823 |

| 5,000 | 1,110,988 | 0.378499977174 |

| 8,192 | 2,664,273 | 0.357740121134 |

| 9,999 | 5,159,139 | 0.475264150844 |

| 10,000 | 5,159,756 | 0.475231089963 |

| 14,178 | 7,028,273 | 0.334234623517 |

| 14,956 | 11,976,983 | 0.514718160586 |

| 19,999 | 14,757,163 | 0.365403144913 |

| 20,000 | 14,757,568 | 0.365378477484 |

Every integer entry and decimal in this table is (d). The visible

oscillation is finite evidence only; it neither proves nor disproves a

\(\Theta(j^2/\log j)\) law.

Live-comment indexing correction

• (d) In the live statement's notation,

\[ a_{1999}=259{,}183,\qquad a_{2000}=262{,}751. \]

Moreover

\[ \frac{1999^2}{2\log1999}=262{,}880.886\ldots, \]

which explains both numbers quoted in the comment: it counted the 2000th

list entry but called it \(a_{2000}\). Using the page's actual

zero-based \(a_{2000}\), the ratio to its benchmark is

\(262751/263126.649847\ldots=0.998572361\ldots\), not 0.986.

The 2025 preprint's appendix uses the same shifted plotting convention:

its array has seq[0]=0, but it plots seq[1:] against labels

\(k=2,\ldots,N\). For example, its labelled trough \(k=14179\) is

\(a_{14178}\), and its labelled peak \(k=14957\) is \(a_{14956}\).

That is an (a) reading of the printed code; the corresponding values

above are (d).

A typo in the 1978 memo

(a) The official Odlyzko--Stanley scan prints the ninth displayed term

of \(S(2)\) as 17. This cannot be correct because the same displayed prefix

already contains \(11,14\), and \(11,14,17\) is a 3-term arithmetic

progression. (d) Both independent generators and the all-pairs check

give the correct next accepted term 27:

What remains, and the exact wall

The proposition solves a sharp finite/large-seed regime, not the fixed-seed

asymptotic question. For \(n=4\), it stops after offsets \(0,1,3\), exactly

where the extra seed 0 first forbids the translated-canonical offset 4.

After that deletion, later coverage depends recursively on the entire

altered prefix; the finite-state digit mechanism no longer closes.

(a) If \(B(x)=A(n)\cap[0,x]\), greediness says every omitted integer

above the seed is an endpoint \(2y-z\) of a pair \(z

Counting pairs only gives

which is the square-root counting mechanism behind Moy's quadratic upper

bound. It contains no logarithmic gain.

(c) A concrete lemma sufficient for the conjectured upper estimate

\(a_k=O(k^2/\log k)\) would be a logarithmic collision lemma for this

specific greedy set: among relevant pairs \(z

\(2y-z\leq x\) would need to be only

uniformly in \(x\). Greedy completeness would then force

\(|B(x)|=\Omega(\sqrt{x\log x})\). No theorem located in the search

supplies such control, and a claim of this form for arbitrary 3-free sets

would need separate scrutiny.

(c) To prove the opposite Type-2 inequality

\(a_k=\Omega(k^2/\log k)\), one needs an upper bound

\(|B(x)|=O(\sqrt{x\log x})\) for this deterministic greedy sequence.

General progression-free-set density theorems operate far above the

square-root scale and do not provide it. To prove the 2025 preprint's

suggested failure instead, one would need a uniform multiscale construction

of troughs showing, for example,

\(\liminf a_k\log k/k^2=0\); a finite list of troughs cannot do that.

(d) On the final verified run, the complete 20,001-term generation plus

independent 200,010,000-pair rebuild took 31.21 CPU-seconds and 61,700 KiB

peak RSS.

(a) The present Python method performs \(\Theta(K^2)\) pair writes.

(c) Straight scaling estimates \(K=100{,}000\) at about 0.23

core-hours and roughly 0.6 GB under the observed \(A(4)\) scale, and

\(K=10^6\) at about 23 core-hours and tens of GB with a byte-per-endpoint

sieve. I did not run either. Even those finite ranges could add

oscillations but cannot supply the missing uniform lemma.

Reproduction

From the repository root:

python runs/erdos271_wave8p_reverify.py

The verified run ended with:

small cross-checks: PASS
A(4) through a_20000: pair certificate PASS
SHA256(le64(a_0..a_20000))=845d8b86c929fdeaa48d439f9f8db717cc572de98796d9b3b001d8615f2d7923
ALL CHECKS PASSED

PARTIAL: proved a sharp explicit formula for every fixed index in the large-seed regime and an O(log n) exact first-obstruction reduction; independently certified A(4) through a_20000, corrected two indexing/printing errors, but no fixed-seed asymptotic law is proved.