Erdoes #503 - working report - Erdős Problem a Day

Erdős problem #503 — wave 9o

Date of live check: 2026-07-28 UTC Problem page: <https://www.erdosproblems.com/503> Discussion page: <https://www.erdosproblems.com/forum/thread/503> Verifier: runs/erdos503_wave9o_reverify.py

Claim labels used throughout

(a) elementary-rigorous: proved here from elementary algebra, geometry, or finite exact data.
(b) rigorous-modulo-named-theorem: the deduction is rigorous, conditional only on the explicitly named published theorem.
(c) plausible/structural-unverified: a useful structural claim not promoted to a theorem here.
(d) computational-only: established by the exact program, but not offered as a hand proof.

Statements about what the live website displayed are source observations rather than mathematical claims. Claims made only in website comments are marked (c) until separately proved or tied to a named theorem.

0. Mandatory live-page and collision check

I accessed both the problem page and its discussion page through the Bright Data browser path, not by datacenter curl.

Verbatim current statement

What is the size of the largest \(A\subseteq \mathbb{R}^d\) such that every three points from \(A\) determine an isosceles triangle? That is, for any three points \(x,y,z\) from \(A\), at least two of the distances \(\lvert x-y\rvert,\lvert y-z\rvert,\lvert x-z\rvert\) are equal.

Current flags

The live page displayed all of the following on 2026-07-28:

status: OPEN;
16 comments on this problem;
0 claimed proofs for this problem;
“Interested in collaborating”: None;
“Currently working on this problem”: None;
“Likes this problem”: Alfaiz;
last body edit: 28 October 2025.

Thus the mandatory stop condition did not trigger. This is worth stating carefully: one comment proposes and revises a reduction theorem, but the site's formal proof-claim count is still zero, its status is OPEN, and it lists no current worker.

Known-results text on the live problem body

The page states:

\(f(2)=6\), due to Kelly, with an alternative proof by Kovács;
\(f(3)=8\), due to Croft;
Blokhuis's general bound

\[ f(d)\leq \binom{d+2}{2}; \]

the edge-midpoint lower bound \(\binom{d+1}{2}\);
Weisenberg's one-point extension, giving

\[ f(d)\geq \binom{d+1}{2}+1; \]

a pointer to problem #1088 for a generalisation.

The page bibliography gives:

A. Blokhuis, Few-distance sets, 1984;
H. T. Croft, 9-point and 7-point configurations in 3-space, 1962;
P. Erdős and L. M. Kelly, solution to E735, 1947;
Z. Kovács, A note on Erdős's mysterious remark,

arXiv:2412.05190, 2024.

All 16 live comments read

The comments are user content and the page itself warns that they are unverified. Here is the complete substantive inventory, with one item for each displayed comment.

Desmond Weisenberg, 9 Aug 2025. Adds the all-\(2/(n+1)\) point to

the simplex-edge construction, claiming \(\binom{n+1}{2}+1\). This construction is independently checked below, so the mathematical claim is (a).

Przemek Chojecki, 22 Apr 2026. Posts a note and Lean file claiming

\[ h(d)\leq\max\{s(d)+1,s(d-1)+3\}, \quad f(d)=\max\{g(d),s(d)+1,s(d-1)+3\}. \] The comment was later edited to link a rewritten note. As a comment this is (c); an independent proof audit appears below.

Nat Sothanaphan, 22 Apr 2026. Reports that a “standard check” found

no issue in the first note, but that the Lean file was incomplete. (c)

Przemek Chojecki, 22 Apr 2026. Replies that the Lean file omits

external/cited works by design. (c)

Takahiro Koizumi (J_Koizumi_144), 26 May 2026. Identifies the

gap: Ionin requires non-last blocks to have size at least \(2\), not at least \(3\); a two-point first block remains. (c as a comment; confirmed directly against Ionin below.)

Nat Sothanaphan, 27 May 2026. Calls the first proof likely wrong and

explains how the automated check missed the \(2\) versus \(3\) mismatch. (c)

Nat Sothanaphan, 27 May 2026. Reports a model confirmation that the

omission is a major gap. (c)

Przemek Chojecki, 27 May 2026. Says the gap was fixed in a rewritten

note. (c)

Przemek Chojecki, 27 May 2026. Describes the repaired two-point-block

analysis and identifies the extremal suspension case requiring the new polynomial argument. (c before the audit below.)

RealBelgian, 28 May 2026. Reports checking the revised note and

finding it correct. (c)

Adenwalla, 28 May 2026. Discusses when the upper bound for \(h(d)\)

is an equality and combines it with Musin's spherical results. (c as posted; the cited Musin ranges were checked.)

Adenwalla, 28 May 2026. Deduces

\(g(d)\leq f(d)\leq g(d)+2\). (c as posted; proved below from the audited reduction.)

Adenwalla, 28 May 2026. Gives

\[ f(1),\ldots,f(8)=3,6,8,11,17,28,30,45. \] This is (b), independently confirmed from Ionin and exact lower certificates below.

Kenta Kitamura, 29 May 2026. Notes \(f(22)=276\), by adjoining the

centre to a tight \(275\)-point spherical two-distance set and using Blokhuis's upper bound. This is reproved with a from-scratch graph certificate below, so the result is (b), with its finite certificate also checked under (d).

Nat Sothanaphan, 29 May 2026. Reports a complementary automated

check of the revised note. (c)

Alfaiz, 23 Apr 2026. Points to Kido for \(f(4)=11\) and to Ionin

for related results. This literature claim is verified below, hence (b).

1. Primary-source literature audit

Sources that were found and checked

Blokhuis, 1984.

Few-distance sets, CWI Tract 7. Chapter 7 is explicitly titled “Isosceles point sets.” Theorem 7.2.5 states that an isosceles \(X\subset\mathbb R^d\) satisfies \[ |X|\leq \tfrac12(d+1)(d+2)=\binom{d+2}{2}, \] and says equality forces either a two-distance set or a spherical two-distance set together with its centre. This directly verifies the tracker attribution. (b)

Ionin, 2009.

Y. J. Ionin, Isosceles Sets, Electronic Journal of Combinatorics 16 (2009), R141. Definition 4.1 has the correct complete-decomposition condition \(|S_i|\geq2\) for non-last blocks and \(|S_k|\geq1\) for the last block. Proposition 4.2 gives a complete decomposition and the affine dimension inequality. Section 5 determines the exact maximum through dimension \(8\), giving \[ 3,6,8,11,17,28,30,45. \] (b)

Lisoněk, 1997.

P. Lisoněk, New Maximal Two-Distance Sets, J. Combin. Theory A 77 (1997), 318–338. The paper classifies maximum Euclidean two-distance sets through dimension \(7\) and constructs a \(45\)-point maximum set in dimension \(8\). The explicit rational realisation \[ J(9,2)\ \cup\ \left\{\text{permutations of } \left((1/3)^8,-2/3\right)\right\} \] is also recorded in Bannai–Sato–Shigezumi, arXiv:1202.1352 and is exactly checked by the verifier. (b)

Kido, 2010.

H. Kido, On Isosceles Sets in the 4-Dimensional Euclidean Space. Its abstract and Corollary 1.2 state that the maximum is \(11\), with exactly two similarity classes of extremisers. (b)

Musin, 2008/2009.

O. R. Musin, Spherical two-distance sets. In the notation \(s(d)\) used here, it states \(s(d)=d(d+1)/2\) for \(6<d<22\) and \(23<d<40\), and records tightness of the Delsarte–Goethals–Seidel bound in dimensions \(2,6,22\). (b)

Inoue, 2012.

K. Inoue, A construction of the McLaughlin graph from the Hoffman–Singleton graph, Australasian Journal of Combinatorics 52 (2012), 197–204. Theorem 3.3 constructs an \(\operatorname{srg}(275,112,30,56)\). The verifier reconstructs the entire graph rather than downloading an adjacency matrix. (b), with an independent (d) check

Croft, 1962, and corrigendum, 1963.

H. T. Croft, 9-point and 7-point configurations in 3-space, Proc. London Math. Soc. (3) 12 (1962), 400–424. The publication exists with the stated metadata. A 1963 corrigendum replaces an incorrect paragraph in Lemma 22. Ionin's peer-reviewed paper separately records Croft's conclusion that no \(9\)-point isosceles set exists in \(\mathbb R^3\). (b)

Revised 2026 reduction note.

The live comment links <https://www.ulam.ai/research/erdos503-final.pdf>. The downloaded file is 11 pages, has PDF creation time 2026-05-27 14:15:38 UTC, and SHA-256 00659229ae22158b9e3b29a05d69ed70d2546f0169a353ecc46cad29f89b05ec. I found no arXiv record or journal version under its exact title or theorem formula. It is therefore treated as an unrefereed note; its proof is independently audited in Section 5 below.

Search miss and rejected source

Searches by the exact revised-note title, “two-shell polynomial lemma,”

and the displayed formula found only the Ulam PDF and tracker thread, not a separately archived paper. This is a genuine literature miss, not evidence of nonexistence.

A recent preprint,

Chen–Yu, arXiv:2509.00858, exists and gives ratio-dependent spectral bounds. I did not use its small-dimensional table: the displayed values in its current text conflict with Lisoněk, Ionin, and explicit elementary constructions (for example it lists values incompatible with the \(16\)-point half-cube in \(\mathbb R^5\)). No claim here depends on that table.

2. Notation

Let

\begin{aligned} f(d)&=\max\{|S|:S\subset\mathbb R^d\text{ is isosceles}\},\\ g(d)&=\max\{|S|:S\subset\mathbb R^d\text{ has at most two nonzero distances}\},\\ s(d)&=\max\{|S|:S\subset\mathbb R^d\text{ is spherical and has at most two nonzero distances}\},\\ h(d)&=\max\{|S|:S\subset\mathbb R^d\text{ is isosceles but not a two-distance set}\}. \end{aligned}

Also put

L(m)=\binom{m+1}{2},\qquad U(m)=\frac{m(m+3)}2,\qquad G(m)=\binom{m+2}{2}=U(m)+1.

The elementary simplex-edge construction gives \(s(m)\geq L(m)\). The Delsarte–Goethals–Seidel spherical bound and Blokhuis Euclidean bound give

s(m)\leq U(m),\qquad g(m)\leq G(m).

These statements are (b).

3. Exact result in dimension 22

Theorem

\boxed{f(22)=276.}

This conclusion was already observed in the live comments. What is added here is a completely explicit, offline-verifiable certificate that does not merely quote the existence of \(275\) spherical points.

3.1 From-scratch construction of the graph

Define the Hoffman–Singleton graph \(H\) on

\{P_{i,j},Q_{i,j}:i,j\in\mathbb F_5\}.

For each fixed \(i\), join \(P_{i,j}\) to \(P_{i,j\pm1}\), join \(Q_{i,j}\) to \(Q_{i,j\pm2}\), and join

P_{i,j}\sim Q_{k,ik+j}\qquad(k\in\mathbb F_5).

The verifier directly checks that this is an \(\operatorname{srg}(50,7,0,1)\). (d)

It then performs an exact bitset branch-and-bound enumeration of all independent \(15\)-sets of \(H\). There are exactly \(100\) in the enumeration. Their intersection-\(\{0,5\}\) relation has two connected components \(\mathcal D_1,\mathcal D_2\), each of size \(50\); within a component intersections have size \(0\) or \(5\), while cross-component intersections have size \(3\) or \(8\). (d)

Applying Inoue's four adjacency rules to

\mathcal D_1\sqcup\mathcal D_2\sqcup E(H)

produces \(50+50+175=275\) vertices. The verifier checks, pair by pair, that every degree is \(112\), adjacent pairs have \(30\) common neighbours, and nonadjacent pairs have \(56\). Thus the generated adjacency matrix \(A\) satisfies

A^2=56I-26A+56J,\qquad AJ=112J.

This finite check is (d); existence and the same parameters also follow from Inoue's named theorem, making their use below (b).

3.2 Exact rank-22 Gram certificate

Set

E=\frac1{15}I-\frac1{30}A+\frac1{75}J.

Using only the two displayed adjacency-algebra identities gives

E^2=E,\qquad \operatorname{tr}E =275\left(\frac1{15}+\frac1{75}\right)=22.

Because \(E\) is a real symmetric idempotent, it is positive semidefinite and has rank \(22\). Therefore

\Gamma=\frac{25}{2}E

is the Gram matrix of \(275\) unit vectors in \(\mathbb R^{22}\). Its off-diagonal entries are exactly

\langle x_i,x_j\rangle= \begin{cases} -\frac14,&i\sim j,\\[2mm] \frac16,&i\not\sim j. \end{cases}

Consequently their two squared distances are

2-2\left(-\frac14\right)=\frac52,\qquad 2-2\left(\frac16\right)=\frac53.

This Gram derivation is (a) once the finite graph is supplied, and (b) unconditionally modulo Inoue's existence theorem.

3.3 Add the centre and match the upper bound

Adjoin the zero vector. Any triple of nonzero vectors has at most the two distances above. Any triple containing zero has its two zero-incident distances both equal to \(1\). Hence the \(276\) vectors form an isosceles set in \(\mathbb R^{22}\). (a)

Blokhuis's Theorem 7.2.5 gives

f(22)\leq\binom{24}{2}=276.

The construction and upper bound match, proving \(f(22)=276\). (b)

4. An explicit 278-point construction in dimension 23

Embed the \(275\) unit McLaughlin vectors as \((x,0)\in\mathbb R^{23}\). Add

o=(0,0),\qquad p=(0,1),\qquad q=(0,-1),

where the first component belongs to \(\mathbb R^{22}\). The resulting set has \(278\) points and affine dimension \(23\).

The possible squared distances are

1,\quad \frac53,\quad 2,\quad \frac52,\quad 4.

Nevertheless every triple is isosceles:

three McLaughlin points use only \(5/3,5/2\);
\(o\) with two McLaughlin points has two radius-\(1\) sides;
\(p\) or \(q\) with two McLaughlin points has two squared-distance-\(2\)

sides;

\(\{p,q,x\}\) has \(|p-x|=|q-x|\);
\(\{p,q,o\}\) has \(|p-o|=|q-o|\);
\(\{p,o,x\}\) and \(\{q,o,x\}\) have the two squared distances from

\(o\) equal to \(1\).

Thus

\boxed{f(23)\geq278.}

The geometric deduction is (a) given the rank-22 Gram certificate and (b) modulo Inoue. The program also checks all \(\binom{278}{3}=3{,}542{,}276\) triples exactly, so there is an independent (d) check. This improves the problem-body lower bound \(\binom{24}{2}+1=277\) by one, although the same improvement is already present in the 2026 comments.

No matching upper bound is claimed: Blokhuis only gives \(\binom{25}{2}=300\) in dimension \(23\).

5. Audit of the revised reduction

Audited conclusion

The revised 2026 argument supports

\boxed{ h(d)\leq\max\{s(d)+1,s(d-1)+3\} }

and hence

\boxed{ f(d)=\max\{g(d),s(d)+1,s(d-1)+3\} }\qquad(d\geq2).

After checking Ionin's actual hypotheses, every dimension count, and the new polynomial lemma, I find the revised proof internally complete. This is (b): it uses Ionin's complete-decomposition theorem and the Delsarte–Goethals–Seidel and Blokhuis bounds. It is not represented as a refereed new theorem; the only current manuscript found is the unrefereed Ulam PDF pinned above.

5.1 Lower constructions

Every Euclidean two-distance set is isosceles, giving \(f(d)\geq g(d)\).

If \(X\subset\mathbb R^d\) is a spherical two-distance set with centre \(c\), then \(X\cup\{c\}\) is isosceles, because a triple containing \(c\) has two equal radii. Hence \(f(d)\geq s(d)+1\).

If \(X\) is a spherical two-distance set in a hyperplane \(H\cong\mathbb R^{d-1}\), with centre \(c\) and radius \(r\), add \(c\) and the two points \(p,q\) on the normal through \(c\) with

\[ |p-c|=|q-c|=r. \]

Then

|x-c|=|p-c|=|q-c|=r,\quad |p-x|=|q-x|=\sqrt2\,r,\quad |p-q|=2r.

Every triple is isosceles, and the set has at least three global distances. Thus

f(d)\geq s(d-1)+3,\qquad h(d)\geq s(d-1)+3.

All three constructions are (a).

5.2 Complete-decomposition count

Let a non-two-distance isosceles set have an Ionin complete decomposition

S=S_1\sqcup\cdots\sqcup S_k.

Put \(q=k-1\),

a_i=\dim_{\rm aff}S_i\ (1\leq i\leq q),\qquad N=\sum_{i=1}^q a_i,\qquad e=\dim_{\rm aff}S_k.

Ionin gives \(N+e\leq d\). Every non-last block is spherical, \(a_i\geq1\), and

|S_i|\leq U(a_i).

The last block satisfies \(|S_k|\leq G(e)\), with the evident special interpretations \(e=0\Rightarrow|S_k|=1\) and \(e=1\Rightarrow|S_k|\leq3\). These inputs are (b).

The elementary counting lemma is

\sum_{i=1}^q U(a_i)\leq L(N)+1,

and in fact the right side improves to \(L(N)\) unless

q=2,\qquad \{a_1,a_2\}=\{1,N-1\}.

Indeed

L(N)-\sum_iU(a_i)=\sum_{i<j}a_ia_j-N.

For \(q=2\) this is \((a_1-1)(a_2-1)-1\). For \(q\geq3\), the cross-term sum is minimised, at fixed \(N\), by \((N-q+1,1,\ldots,1)\), and is at least \(N\). This lemma is (a).

Now let

M(d)=\max\{s(d)+1,s(d-1)+3\}.

All ordinary cases give \(|S|\leq M(d)\):

If \(q=1\), \(a_1\geq2\), and \(e=0\) or \(1\), monotonicity gives

\(s(a_1)+1\leq s(d)+1\) or \(s(a_1)+3\leq s(d-1)+3\).

If \(q=1\), \(a_1,e\geq2\), then

\[ L(a_1+e)+1-U(a_1)-G(e)=a_1e-a_1-e\geq0. \]

If \(q=1,a_1=1\), the non-last block has exactly two points. When

\(e\leq d-2\), \[ |S|\leq2+G(d-2)\leq L(d)+1\leq s(d)+1. \] The only remaining subcase is a two-point first block and \(e=d-1\).

If \(q\geq2\) and the counting-lemma exception does not occur, the cases

\(e=0,1,\geq2\) follow respectively from \[ L(N)+1,\qquad L(N)+3,\qquad L(N)+G(e)\leq L(N+e)+1, \] where the last difference is \(e(N-1)\).

In the exceptional dimensions \(\{1,N-1\}\), the one-dimensional block

contributes exactly two points. For \(e=0\) one gets \(2+s(N-1)+1\leq s(d-1)+3\); for \(e=1\), \(2+U(N-1)+3\leq L(d)+1\); and for \(e\geq2\), \[ L(N+e)+1-\bigl(2+U(N-1)+G(e)\bigr)=e(N-1)-1\geq0. \]

This case split is (a) once the named block bounds are granted. The verifier independently checks every displayed integer identity and all instances through dimension \(100\), which is an additional (d) audit. Therefore, except for one configuration type, \(|S|\leq M(d)\). The sole survivor is

S=\{p,q\}\sqcup X,

where \(X\) is a full \((d-1)\)-dimensional two-distance set in the perpendicular bisector of \(pq\).

5.3 Reduction of the two-point block

Write \(n=d-1\), put the midpoint of \(pq\) at the origin of the perpendicular bisector \(H\cong\mathbb R^n\), and take

p=(0,h),\qquad q=(0,-h),\qquad h>0.

Let \(X\subset H\) have squared distances \(0<\alpha<\beta\), and define

\[ t(x)=|p-x|^2=|q-x|^2=|x|^2+h^2. \]

There is at most one value of \(t(x)\) outside \(\{\alpha,\beta\}\). Indeed, if \(t(x)\ne t(y)\), then the isosceles triangle \(pxy\) forces \(|x-y|^2\) to equal one of \(t(x),t(y)\); since \(|x-y|^2\in\{\alpha,\beta\}\), two distinct outside values are impossible. This is (a).

Suppose an outside value \(\gamma\) occurs, and let

C=\{x\in X:t(x)=\gamma\}.

For \(c\in C\), \(y\in X\setminus C\), the triangle \(pcy\) forces

\[ |c-y|^2=t(y). \]

Thus every \(y\in X\setminus C\) is a centre of a sphere containing \(C\).

If \(C=X\), then \(X\) is spherical and

\(|S|\leq s(n)+2\).

If \(|C|=1\), say \(C=\{c\}\), then

\(c\cdot y=(|c|^2-h^2)/2\) for \(y\notin C\), so \(X\setminus C\) lies in an \((n-1)\)-flat and \[ |S|\leq3+G(n-1)\leq L(d)+1. \]

If \(b=\dim_{\rm aff}C\geq1\), then

\(|C|\leq U(b)\), while all possible centres of spheres through \(C\) lie in an affine subspace of dimension at most \(n-b\). If \(b=n\), \(|X\setminus C|\leq1\). If \(b<n\), then \[ |X|\leq U(b)+G(n-b)=G(n)-b(n-b)\leq G(n)-1. \]

Every outside-value case therefore has \(|S|\leq M(d)\). This is (b) only because the \(U,G\) bounds are named theorems; all geometry and arithmetic here are (a).

It remains that \(t(x)\in\{\alpha,\beta\}\) for every \(x\). Put

X_1=\{x:t(x)=\alpha\},\qquad X_2=\{x:t(x)=\beta\}.

If a shell is empty, \(X\) is spherical. If a shell is a singleton, the other shell is a spherical two-distance set. Both cases give \(|S|\leq s(n)+3\). The only delicate case is

|X_1|\geq2,\qquad |X_2|\geq2.

5.4 The two-shell polynomial lemma

The required statement is:

If \(X\subset\mathbb R^m\) is a two-distance set with squared distances \(0<\alpha<\beta\), \(h>0\), \(|x|^2+h^2\in\{\alpha,\beta\}\) for every \(x\), and both resulting shells have at least two points, then \[ > |X|\leq G(m)-1=U(m). > \]

Here is the proof audit. Put

\eta=h^2,\quad r_1=\alpha-\eta,\quad r_2=\beta-\eta,\quad \Delta=\beta-\alpha.

The first shell has positive radius, so \(0<\eta<\alpha\). If the affine dimension is below \(m\), Blokhuis already gives the desired bound. Assume for contradiction full affine dimension and equality \(|X|=G(m)\).

For \(u\in\mathbb R^m\) and an auxiliary \(z\), define

\sigma=|u|^2+z^2,\qquad \rho=|u|^2,

F_x(u,z)= \frac{(\sigma-2x\cdot u+|x|^2-\alpha) (\sigma-2x\cdot u+|x|^2-\beta)} {\alpha\beta},

Q(u,z)=(\sigma-r_1)(\sigma-r_2),

and, with fixed nonzero \(\varepsilon\) and a free real parameter \(R\),

\Phi_x=F_x+ \left(-\frac1{\alpha\beta}+\varepsilon(2|x|^2-R)\right)Q.

For \(x,y\in X\),

\Phi_x(y,0)=\delta_{xy}.

Every \(\Phi_x\) lies in

W=\operatorname{span}\{\sigma^2,\sigma u_i,u_iu_j,\sigma,u_i,1\}, \qquad \dim W=\binom{m+3}{2}.

The displayed spanning polynomials are independent: different total degrees separate, and at degree two \(\sigma\) is independent of the \(u_i u_j\) because it contains \(z^2\). Since

|X|+(m+3)=\binom{m+3}{2}+1,

the family

\{\Phi_x:x\in X\}\cup\{u_1,\ldots,u_m,\sigma,\rho,1\}

is linearly dependent. Write a dependence as

\sum_{x\in X}c_x\Phi_x+a\cdot u+b\sigma+c\rho+d=0.

Set

C=\sum_xc_x,\quad V=\sum_xc_x|x|^2x,\quad M=\sum_xc_xxx^\mathsf T,\quad P=b+c.

Exact coefficient comparison gives

\sum_xc_x(2|x|^2-R)=0,\qquad \sum_xc_x|x|^2=\frac R2C,\qquad \sum_xc_xx=0,

M=\frac{RC}{2m}I,\qquad a=\frac4{\alpha\beta}V,

P=\frac C{\alpha\beta} \left(2\eta-\frac{m+2}{m}R\right),

d=\frac C{\alpha\beta} \left(\eta R+\alpha\beta-2(\alpha+\beta)\eta+2\eta^2\right).

Evaluating at the points and summing over the second shell yields

0= \sum_{y\in X_2}c_y^2+ \frac4{\alpha\beta\Delta}\|V\|^2+ \frac{C^2}{\alpha\beta\Delta} \left(\frac R2-r_1\right)\ell(R),

where

\ell(R)= \alpha(\beta-2\eta)+ \frac{2(m+1)\eta-(m+2)\beta}{m}R.

If some \(R\) makes \((R/2-r_1)\ell(R)>0\), the three terms force all coefficients to vanish, contradicting a nontrivial dependence.

Otherwise the product of the two nonzero linear factors is never positive. Its two roots must coincide, so \(\ell(2r_1)=0\). Taking \(R=2r_1\) forces \(c_y=0\) on \(X_2\) and \(V=0\). The case \(C=0\) again makes the dependence trivial, so \(C\ne0\). The coefficients on \(X_1\) are equal, and

\sum_{y\in X_1}y=0.

Let \(n_1=|X_1|\) and

D=(m+4)\alpha^2-4(m+2)\alpha\eta+4(m+1)\eta^2.

The common-root equation and the constant coefficient give

n_1=\frac{\alpha\eta m}{D}.

For \(y\in X_1\), let \(k_y\) count those \(y'\in X_1\setminus\{y\}\) at squared distance \(\beta\). The centroid identity gives

(n_1-1)\alpha+k_y(\beta-\alpha)=2n_1r_1.

Eliminating \(\beta\) with \(\ell(2r_1)=0\) yields

k_y= \frac{\alpha(\eta-\alpha) \left(2(m+2)\eta-(m+4)\alpha\right)^2}{D^2}<0.

Here \(D>0\): as a quadratic in \(\eta\), its leading coefficient is positive and its discriminant is \(-16m\alpha^2<0\). Also \(\eta-\alpha<0\), and the square factor cannot vanish under the common-root equation. This contradicts \(k_y\geq0\).

Therefore equality in Blokhuis's bound is impossible and \(|X|\leq G(m)-1\). This lemma is (b) because its first step invokes Blokhuis; all subsequent algebra is (a). The verifier uses SymPy to rederive, from the definitions, the identities for \(P r_2+d\), the common-root expression for \(\beta\), the formula for \(D\), the formula for \(n_1\), the displayed \(k_y\), and the discriminant. This is an independent (d) check of the fragile algebra.

Applying the lemma with \(m=n=d-1\) gives

|S|=|X|+2\leq G(n)+1=L(d)+1\leq s(d)+1.

Thus every two-point-block case is also at most \(M(d)\). Combined with the lower constructions, this proves the audited formula. (b)

5.5 Immediate bracket

The midpoint construction and spherical upper bound give

s(d)\geq L(d)=U(d-1)+1\geq s(d-1)+1.

Also \(g(d)\geq s(d)\). Therefore the formula implies

\boxed{g(d)\leq f(d)\leq g(d)+2.}

This deduction is (b).

6. Exact small-dimensional table and exact lower certificates

Ionin's Section 5 proves (b)

\boxed{ \begin{array}{c|rrrrrrrr} d&1&2&3&4&5&6&7&8\\ \hline f(d)&3&6&8&11&17&28&30&45 \end{array}}

The verifier independently supplies and checks the following lower certificates. Every coordinate calculation and every triple check is exact, not floating point. These are (a) constructions with an additional (d) exhaustive check.

| \(d\) | size | exact construction | |---:|---:|---| | 1 | 3 | endpoints and midpoint of a segment | | 2 | 6 | regular pentagon and centre | | 3 | 8 | regular pentagon, centre, and two unit poles | | 4 | 11 | the ten \(e_i+e_j\) in \(\mathbb R^5\), plus \((2/5)^5\) | | 5 | 17 | the 16 even-parity vertices of the \(5\)-cube, plus its centre | | 6 | 28 | Coxeter's \(27\)-point two-distance set and its centre, in Ionin's integer coordinates | | 7 | 30 | the \(d=6\) spherical \(27\)-set, its centre, and two radius-length poles | | 8 | 45 | \(J(9,2)\) plus the nine permutations of \(((1/3)^8,-2/3)\) |

For the \(d=8\) certificate, all squared distances are exactly \(2\) or \(4\), and its affine rank is exactly \(8\).

7. What remains: a precise first wall

Even if the audited reduction is accepted, the general problem is not closed. It has been reduced to the exact Euclidean and spherical two-distance extremal functions \(g(d)\) and \(s(d)\). This is a genuine reduction, not a closed form in known elementary quantities.

The first unresolved dimension already isolates the obstacle sharply. Musin gives

s(8)=36,\qquad s(9)=45.

Hence the audited formula gives

\boxed{f(9)=\max\{g(9),46\}}, \qquad 46\leq f(9)\leq55.

Thus one concrete missing lemma would be:

Exclude every \(47\)-point Euclidean two-distance set in \(\mathbb R^9\).

That lemma would prove \(f(9)=46\). Conversely, a \(47\)-point construction would immediately improve the lower bound and move the target to the exact value of \(g(9)\). This diagnosis is (b) modulo the audited reduction and Musin.

A naive graph enumeration is not a viable computation. Marking one of the two distances turns a \(47\)-point candidate into a graph on \(47\) vertices, before Euclidean-rank constraints are applied. The raw space has

2^{\binom{47}{2}}=2^{1081}>10^{325}

labelled graphs. Even at \(10^9\) graph tests per second this exceeds \(10^{312}\) core-hours; quotienting by all \(47!\) relabellings still leaves roughly \(10^{253}\) cases. A credible attack must use spectral classification, switching, forbidden substructures, or a new analytic bound, not brute force. This cost statement is (a) arithmetic; it is not a claim that every smarter search has that cost.

8. Reproduction

Run:

python -u runs/erdos503_wave9o_reverify.py

The final checked run used Python 3 and SymPy 1.14.0, took about 7.2 seconds, and used about 55 MB resident memory. Its output was:

Exact coordinate certificates for d=1,...,8
 d=1: size=  3, affine_dim= 1, global_squared_distances=['1', '4']
 d=2: size=  6, affine_dim= 2, global_squared_distances=['1', '5/2 - sqrt(5)/2', 'sqrt(5)/2 + 5/2']
 d=3: size=  8, affine_dim= 3, global_squared_distances=['1', '2', '4', '5/2 - sqrt(5)/2', 'sqrt(5)/2 + 5/2']
 d=4: size= 11, affine_dim= 4, global_squared_distances=['2', '4', '6/5']
 d=5: size= 17, affine_dim= 5, global_squared_distances=['2', '4', '5/4']
 d=6: size= 28, affine_dim= 6, global_squared_distances=['16', '16/3', '8']
 d=7: size= 30, affine_dim= 7, global_squared_distances=['16', '16/3', '32/3', '64/3', '8']
 d=8: size= 45, affine_dim= 8, global_squared_distances=['2', '4']

From-scratch sporadic graph and high-dimensional certificates
d=22: McLaughlin projector rank=22, size=276 with centre; Blokhuis upper arithmetic=276
d=23: suspension size=278; checked 3,542,276 triples; squared distances=[Fraction(1, 1), Fraction(5, 3), Fraction(2, 1), Fraction(5, 2), Fraction(4, 1)]

Revised-reduction proof audit
two-shell lemma: all displayed symbolic identities recomputed exactly
complete-decomposition arithmetic: audited through d=100
first unresolved dimension arithmetic: f(9)=max(g(9),46), 46<=f(9)<=55

ALL CHECKS PASSED

The standalone verifier contains the full construction and checking code; it downloads nothing and uses no solver. It reconstructs the sporadic graph from \(\mathbb F_5\), rather than trusting an adjacency file.

PARTIAL: Verified \(f(22)=276\), an explicit \(278\)-point construction in \(\mathbb R^{23}\), the exact \(d\leq8\) table, and the revised reduction \(f(d)=\max\{g(d),s(d)+1,s(d-1)+3\}\); the first remaining concrete wall is excluding \(47\)-point Euclidean two-distance sets in \(\mathbb R^9\).

This is the AI working report, labelled by outcome — not an independently verified claim unless marked PROVED. ← ledger