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

Erdős problem #1085 — wave w031 report

Access and research date: 2026-07-29 (UTC).

Throughout, $f_d(n)$ is the maximum possible number of unit-distance pairs among $n$ distinct points of $\mathbb R^d$, as intended by the live statement.

Claim labels:

(a) elementary-rigorous: proved below from elementary graph theory,

Euclidean geometry, or linear algebra.

(b) rigorous-modulo-named-theorem: quoted from the identified primary

source.

(c) plausible/structural-unverified: a search miss, interpretation, or

proposed next step, never promoted to a theorem.

(d) computational-only: a browser observation or finite exact

computation; it is not used by itself as a uniform proof.

Step 0: mandatory live-page check

(d) Direct datacenter access returned Cloudflare HTTP 403, so I used the Bright Data browser path and inspected the rendered problem page, its LaTeX view, and its discussion page:

https://www.erdosproblems.com/1085
https://www.erdosproblems.com/latex/1085
https://www.erdosproblems.com/forum/discuss/1085

(d) At access time the page was last edited 23 May 2026 and showed OPEN, 0 claimed proofs, Currently working on this problem: None, and Interested in collaborating: None. Thus none of the required stop conditions applied. The page identifies the original source as [Er75f, p. 103].

Verbatim current statement

(d, verbatim live-page transcription; the grammatical wording is preserved)

Let $f_d(n)$ be minimal such that, in any set of $n$ points in $\mathbb{R}^d$, there exist at most $f_d(n)$ pairs of points which distance $1$ apart. Estimate $f_d(n)$.

Results and metadata actually listed on the page

(b) The page lists the following mathematical state.

In dimension two,

\[ n^{1+c}<f_2(n)\ll n^{4/3} \] for some small $c>0$. It attributes the new polynomial lower bound to an internal OpenAI model, at least for infinitely many $n$, and points to problem #90; the upper bound is Spencer--Szemerédi--Trotter.

In dimension three,

\[ n^{4/3}\log\log n\ll f_3(n)\ll n^{3/2}\beta(n), \] with the lower bound attributed to Erdős and the displayed upper bound to Clarkson--Edelsbrunner--Guibas--Sharir--Welzl.

For $d\ge4$, writing $p=\lfloor d/2\rfloor$, the Lenz construction

gives \[ f_d(n)\ge \frac{p-1}{2p}n^2-O(1), \] and Erdős--Stone gives the matching leading asymptotic upper bound.

The page says Erdős determined the even-dimensional answer up to

$O(1)$, Brass determined the exact answer in dimension $4$, and Swanepoel determined it for every even $d\ge6$, for sufficiently large $n$.

For odd $d\ge5$, the page attributes to Erdős--Pach the bounds

\[ \frac{p-1}{2p}n^2+c_1(d)n^{4/3} \le f_d(n)\le \frac{p-1}{2p}n^2+c_2(d)n^{4/3}, \] for positive constants $c_1(d),c_2(d)$.

(d) The page separately marks the problem as formalised and lists OEIS A186705 as a possible related sequence. The sole live comment says:

Maybe makes sense to update the d=2 lower bound here in light of the solution for [90].

It was posted by Neel Somani at 07:49 on 21 May 2026. It is not a claimed proof. Likes this problem listed Saw-mon-and-Natalie; the difficulty, tractability, collaboration, current-work, and formalisation-work reaction rows all displayed None.

Primary-source literature audit and one live-page correction

(b) The following sources were opened and checked, rather than inferred from secondary summaries.

P. Erdős, On sets of distances of $n$ points in Euclidean space,

Publ. Math. Inst. Hung. Acad. Sci. 5 (1960), 165--169. The scan contains the Lenz construction and the higher-dimensional leading asymptotics: https://real.mtak.hu/200963/1/cut_MATKUTINT_5_1_-_2_1959_pp165_-_169.pdf

J. Spencer, E. Szemerédi, and W. T. Trotter, *Unit distances in the

Euclidean plane, in Graph Theory and Combinatorics* (Cambridge, 1983), 293--303, Academic Press, 1984, is the source of the $O(n^{4/3})$ planar upper bound.

K. L. Clarkson, H. Edelsbrunner, L. J. Guibas, M. Sharir, and E. Welzl,

Combinatorial complexity bounds for arrangements of curves and spheres, Discrete Comput. Geom. 5 (1990), 99--160, DOI 10.1007/BF02187783: https://pub.ista.ac.at/~edels/Papers/1990-08-CombinatorialComplexityBounds.pdf

P. Erdős, On some applications of graph theory to geometry, Canad. J.

Math. 19 (1967), 968--971, was checked in the author's archive: https://www.renyi.hu/~p_erdos/1967-13.pdf

P. Brass, *On the maximum number of unit distances among $n$ points

in dimension four, in Intuitive Geometry* (Budapest, 1995), Bolyai Soc. Math. Stud. 6 (1997), 277--290.

K. J. Swanepoel, Unit distances and diameters in Euclidean spaces,

Discrete Comput. Geom. 41 (2009), 1--27, DOI 10.1007/s00454-008-9082-x, arXiv:0707.0213: https://arxiv.org/abs/0707.0213

(b, correction to the displayed live-page bound) Joshua Zahl proved the strictly better three-dimensional estimate

f_3(n)=O_\epsilon\!\left(n^{295/197+\epsilon}\right) =O_\epsilon\!\left(n^{3/2-1/394+\epsilon}\right).

This is Theorem 1.1 of Breaking the $3/2$ barrier for unit distances in three dimensions, IMRN 2019(20), 6235--6284, arXiv:1706.05118v3, DOI 10.1093/imrn/rnx336: https://arxiv.org/abs/1706.05118 The v3 record explicitly notes a corrected Lemma 3.2. Thus the live page's $n^{3/2}\beta(n)$ display is not the current best published three-dimensional upper bound.

(b) The most recent planar lower-bound records found were:

W. Sawin, An explicit lower bound for the unit distance problem,

arXiv:2605.20579, Theorem 1: for arbitrarily large $n$, \[ f_2(n)\ge n^{1.014114}/C \] for an absolute constant $C$: https://arxiv.org/abs/2605.20579

N. Alon, T. F. Bloom, W. T. Gowers, D. Litt, W. Sawin, A. Shankar,

J. Tsimerman, V. Wang, and M. M. Wood, Remarks on the disproof of the unit distance conjecture, arXiv:2605.20695, a human-verified exposition of the qualitative polynomial improvement: https://arxiv.org/abs/2605.20695

(b) Pach--Raz--Solymosi, Erdős's unit distance problem and rigidity, arXiv:2507.15679 (SoCG 2026, DOI 10.4230/LIPIcs.SoCG.2026.83), proves a structural theorem and isolates its Conjecture 7. That conjecture says that a planar realization of a graph with $\gtrsim n^{7/6}$ edges and no collinear neighbour set contains a rigid subframework on at least four vertices. If true, their Theorem 8 would give

f_2(n)=O\!\left(\frac{n^{4/3}}{\log^{1/12}n}\right).

Primary record: https://arxiv.org/abs/2507.15679

(b) Boris Alexeev, Dustin G. Mixon, and Hans Parshall, The Erdős unit distance problem for small point sets, arXiv:2412.11914v2, determines the planar values through $n=21$; its Table 1 includes $f_2(5)=7$, agreeing with the elementary construction below: https://arxiv.org/abs/2412.11914

(b) Hiroshi Maehara, On the euclidean dimension of a complete multipartite graph, Discrete Math. 72 (1988), 285--289, DOI 10.1016/0012-365X(88)90217-8, proves that a complete multipartite graph with $s$ singleton parts, $t$ parts of size two, and $u$ parts of size at least three has strict Euclidean dimension $s+t+2u$ when $t+u\ge2$, and one less when $t+u\le1$. This independently corroborates the matching obstruction proved from scratch below: there $s=r,t=m,u=0$, so Maehara's required dimension is $r+m=d+1$, not $d$. The proof below does not depend on Maehara's theorem.

(c) Searches by the exact formulas, titles, “strict Euclidean dimension”, “unit distances in three dimensions”, and recent arXiv date filters found no later unconditional improvement to Zahl's exponent and no source explicitly tabulating the full near-simplex band or the value $f_3(7)$ established below. These are honest search misses, not novelty claims.

Progress I: an exact near-simplex band

Theorem 1

(a) For every $d\ge1$,

f_d(n)=\binom n2\quad(1\le n\le d+1), \qquad f_d(d+2)=\binom{d+2}{2}-1. \tag{1}

For every $k\ge3$,

f_d(d+k)\le\binom{d+k}{2}-k. \tag{2}

The latter bound is sharp whenever $3\le k\le d$:

\boxed{f_d(d+k)=\binom{d+k}{2}-k\qquad(3\le k\le d).} \tag{3}

It is also sharp at $k=3$ for $d=1,2$. Consequently,

\boxed{f_d(d+3)=\binom{d+3}{2}-3\quad(d\ge1),} \tag{4}

and (1)--(3) determine $f_d(n)$ for the entire band $1\le n\le2d$ when $d\ge3$.

Equidistant-set lemma

(a) If $\sum_i x_i=0$, then for arbitrary points $p_i$,

\sum_{i,j}x_ix_j\lVert p_i-p_j\rVert^2 =-2\left\lVert\sum_i x_ip_i\right\rVert^2. \tag{5}

If all off-diagonal distances are one, the left side is $-\sum_i x_i^2$. Hence the points have no nonzero affine dependence. Thus a unit clique in $\mathbb R^d$ has at most $d+1$ vertices.

Reduction to a forbidden matching

(a) Put $N=d+k$, and let $H$ be the graph whose $q$ edges are the pairs whose distance is not one. Choosing one endpoint of each edge of $H$ gives a vertex cover of size at most $q$. Removing that cover leaves a unit clique, so

N-q\le d+1,\qquad q\ge k-1. \tag{6}

(a) If $q=k-1$ and two edges of $H$ meet, their common endpoint together with one endpoint of every remaining edge covers $H$ using at most $q-1$ vertices. Its complement would be a unit clique of size at least $N-(q-1)=d+2$, impossible. Therefore equality in (6) forces $H$ to be a matching of

\[ m=k-1 \]

edges.

Affine-nullity obstruction for a matching

(a) Suppose those matching pairs are $(u_i,v_i)$, and write

\lVert p_{u_i}-p_{v_i}\rVert^2=1+\delta_i, \qquad \delta_i>-1,\quad\delta_i\ne0. \tag{7}

The allowance $-1<\delta_i<0$ is essential here: unlike the contact problem, a non-unit pair may be shorter than one.

Let

\mathcal H=\{x\in\mathbb R^N:\mathbf1^Tx=0\},\qquad A=I-\sum_{i=1}^m\delta_i (e_{u_i}e_{v_i}^{T}+e_{v_i}e_{u_i}^{T}).

Equation (5) gives, for all $x\in\mathcal H$,

x^TAx=2\left\lVert\sum_jx_jp_j\right\rVert^2\ge0. \tag{8}

(a) The affine-dependence space

L=\{x\in\mathcal H:\sum_jx_jp_j=0\}

has dimension at least

N-(d+1)=k-1=m. \tag{9}

Since $A|_{\mathcal H}$ is positive semidefinite, (8) puts $L$ inside its radical: for $x\in L$ and $y\in\mathcal H$, nonnegativity of $(x+ty)^TA(x+ty)$ for both signs of sufficiently small $t$ forces $x^TAy=0$.

(a) Conversely, if $x$ is in that radical, then $Ax=t\mathbf1$ for some $t$. Subtracting the two coordinate equations on pair $i$ yields

(1+\delta_i)(x_{u_i}-x_{v_i})=0.

By (7), $x_{u_i}=x_{v_i}=a_i$. Each of the $r=N-2m$ isolated coordinates equals $t$, and the radical is therefore isomorphic to the solution space of

(1-\delta_i)a_i-t=0\quad(1\le i\le m),\qquad 2\sum_{i=1}^m a_i+rt=0. \tag{10}

(a) The coefficient matrix in the $m+1$ variables $a_1,\ldots,a_m,t$ has rank at least two when $m\ge2$. If some $\delta_i\ne1$, use any $j\ne i$: matching rows $i,j$ and columns $a_i,t$ have determinant $\delta_i-1\ne0$. If every $\delta_i=1$, one matching row and the last row have a $2\times2$ minor of determinant $2$. Thus the radical has dimension at most $m-1$, contradicting (9). Equality in (6) is impossible for $k\ge3$; therefore $q\ge k$, proving (2).

Sharp constructions

(a) For $n\le d+1$, take a regular $(n-1)$-simplex of side one.

(a) For $n=d+2$, take a centred regular $(d-1)$-simplex $q_1,\ldots,q_d$ of side one, with

\lVert q_i\rVert^2=\frac{d-1}{2d},

and add apices $(0,\pm h)$ orthogonal to its span, where

h^2=\frac{d+1}{2d}.

All base--apex pairs are unit pairs. The sole non-unit pair is the two apices, whose squared distance is $2(d+1)/d$. This proves the second part of (1).

(a) For $3\le k\le d$, use

\left\{\frac{\pm e_i}{\sqrt2}:1\le i\le k\right\} \cup \left\{\frac{e_i}{\sqrt2}:k<i\le d\right\}. \tag{11}

There are $d+k$ points. Exactly the $k$ opposite pairs have squared distance $2$; every other squared distance is $1$. This proves (3).

(a) The two remaining $d+3$ endpoint constructions are:

$d=1$: $\{0,1,2,3\}$, with three unit pairs.
$d=2$: choose unit vectors $u,v$ with $u\cdot v=1/2$, and use

\[ \{0,u,2u,v,u+v\}. \] Its three non-unit squared distances are $4,3,3$, so seven of the ten pairs are unit pairs.

These meet (2) and prove (4).

Progress II: the exact three-dimensional value $f_3(7)$

Theorem 2

(a)

\boxed{f_3(7)=15.} \tag{12}

Construction

(a) Take a regular pentagon of side one in the plane $z=0$, centred at the origin, and one apex on each side of that plane on its normal. Put

R^2=\frac{5+\sqrt5}{10},\qquad h^2=\frac{5-\sqrt5}{10}.

The pentagon has circumradius $R$, and the apices are $(0,0,\pm h)$. Since $R^2+h^2=1$, all ten apex--pentagon distances are one; the five pentagon sides are also one. The five pentagon diagonals have squared length

\frac{3+\sqrt5}{2},

and the apex pair has squared length

4h^2=2-\frac{2\sqrt5}{5},

neither equal to one. Hence this pentagonal bipyramid has exactly $10+5=15$ unit pairs.

Four elementary geometric certificates

(a), fan lemma. Let $o,a,b,c,d\in\mathbb R^3$, with the four outer points all at unit distance from $o$, and suppose all six outer pairs are unit pairs except $ab$, whose squared distance is $x>0$. The Gram matrix of $a-o,b-o,c-o,d-o$ has determinant

\det G=\frac{x(8-3x)}{16}. \tag{13}

Four vectors in $\mathbb R^3$ make this determinant zero, so

x=\frac83. \tag{14}

(a), double-hole lemma. If the only exceptional outer pairs are $ab$ and $cd$, with squared distances $x,y$, the analogous determinant is

\det G=\frac{xy(xy-4x-4y+12)}{16}. \tag{15}

At $x=y=8/3$, it is $-80/81$, so such five points cannot exist in $\mathbb R^3$.

(a), common-sphere lemma. Three noncollinear centres in $\mathbb R^3$ have at most two common points at unit distance from all three. Indeed, subtracting the three sphere equations confines a common point to a line, and a line meets a sphere at most twice.

(a), circle-chord lemma. For a nondegenerate circle and a fixed point on it, there are at most two other circle points at any prescribed positive chord length. This follows by intersecting the circle with the corresponding sphere (or, in the circle's plane, another circle).

Upper bound: complement classification

(a) Let $H$ again be the graph of non-unit pairs on the seven points, and put $q=|E(H)|$. The equidistant-set lemma gives $\alpha(H)\le4$. The matching argument from Theorem 1, now with $(d,k)=(3,4)$, gives $q\ge4$.

(a) If $q=4$ and $\Delta(H)\ge3$, a degree-three vertex and one more vertex cover $H$, leaving a forbidden five-vertex unit clique. Thus $\Delta(H)\le2$. The condition $\alpha(H)\le4$ leaves exactly these three disjoint-union types:

C_3+P_2+P_1+P_1,\qquad P_4+P_2+P_1,\qquad P_3+P_2+P_2. \tag{16}

Indeed, a graph of maximum degree two is a disjoint union of paths and cycles, and here one only has to use $\alpha(P_s)=\lceil s/2\rceil$, $\alpha(C_s)=\lfloor s/2\rfloor$, seven vertices, and four edges. In each type, deleting a suitable vertex leaves six vertices with exactly two disjoint non-unit pairs. That is the forbidden matching equality case of Theorem 1 for $(d,k)=(3,3)$. Hence $q\ne4$.

(a) Now suppose $q=5$. A vertex of degree at least four, plus at most one other vertex, covers $H$, again impossible. If a vertex has degree three, deleting it leaves two edges. If those edges meet, two vertices cover $H$; if they are disjoint, the remaining six points violate the same matching obstruction. Therefore $\Delta(H)\le2$. With seven vertices, five edges, and $\alpha(H)\le4$, the complete list of component types is

\begin{split} &P_6+P_1,\quad P_5+P_2,\quad P_4+P_3,\\ &C_3+P_3+P_1,\quad C_3+P_2+P_2,\quad C_4+P_2+P_1,\quad C_5+P_1+P_1. \tag{17} \end{split}

The same path/cycle independence formulas give this seven-type list from seven vertices and five edges.

(a) Each type in (17) is impossible as follows. In the table, all paths and cycles refer to the non-unit graph $H$; pairs in different components are therefore unit pairs.

| Type of $H$ | Exact obstruction | |:--|:--| | $P_6+P_1$ | Write the path $v_1\ldots v_6$ and let $o$ be isolated. The fan sets $\{v_1,v_2,v_4,v_6\}$ and $\{v_5,v_6,v_1,v_3\}$, both centred at $o$, force $v_1v_2^2=v_5v_6^2=8/3$. The outer set $\{v_1,v_2,v_5,v_6\}$ violates (15). | | $P_5+P_2$ | Write $v_1\ldots v_5$ and $xy$, and set $o=v_1$. The fan $\{x,y,v_3,v_5\}$ forces $xy^2=8/3$. Thus $o,x,y$ are noncollinear, while $v_3,v_4,v_5$ are three common unit-distance points, contradicting the common-sphere lemma. | | $P_4+P_3$ | Write the paths as $o,a,c,d$ and $x,y,z$. The fan $\{c,d,x,z\}$, centred at $o$, forces $cd^2=8/3$. Then $x,y,z$ are three common unit-distance points of the noncollinear centres $o,c,d$. | | $C_3+P_3+P_1$ | Let $o$ be isolated, let the triangle be $a,b,c$, and let $x,y,z$ be the path. Using $x,z$ in a fan forces all three triangle sides to have square $8/3$. For the unit vectors $A=a-o,B=b-o,C=c-o$, all mutual inner products are $-1/3$, so $S=A+B+C$ has norm one. Any path vector $X=x-o$ has $X\cdot A=X\cdot B=X\cdot C=1/2$, hence $X\cdot S=3/2$, contradicting Cauchy--Schwarz. | | $C_3+P_2+P_2$ | The unit graph is $K_{3,2,2}$. Call its parts $A,B,C$, with $|A|=3$ and $|B|=|C|=2$. The five points $A\cup C$ lie on the circle formed by intersecting the unit spheres about the two points of $B$. But either point of $C$, itself on that circle, is at unit distance from all three points of $A$, contradicting the circle-chord lemma. | | $C_4+P_2+P_1$ | Let $o$ be isolated, $xy$ the $P_2$, and take opposite cycle vertices $a,c$. The fan $\{x,y,a,c\}$ forces $xy^2=8/3$. All four cycle vertices would then be common unit-distance points of the noncollinear centres $o,x,y$. | | $C_5+P_1+P_1$ | The five cycle points lie on the intersection circle of two unit spheres whose centres are one unit apart; its radius is $\sqrt3/2$. A unit chord subtends an angle $\theta$ with $\cos\theta=1/3$. Their induced unit graph is also a $C_5$, so the five-point set is closed under rotation by $\theta$, forcing that rotation to have order five. But $\cos(5\theta)=T_5(1/3)=241/243\ne1$. |

Thus $q\ne5$, so $q\ge6$. There are at most $\binom72-6=15$ unit pairs, and the construction attains 15. This proves (12).

Exact finite table

(a) The following nontrivial values supplied by Theorems 1--2 are independently recomputed by the checker. Values with $n\le d+1$ are simply $\binom n2$.

| $d$ | further exact values $n:f_d(n)$ | |---:|:---| | 1 | $3:2$, plus the endpoint $4:3$ | | 2 | $4:5$, plus the endpoint $5:7$ | | 3 | $5:9,\ 6:12$, plus Theorem 2's $7:15$ | | 4 | $6:14,\ 7:18,\ 8:24$ | | 5 | $7:20,\ 8:25,\ 9:32,\ 10:40$ | | 6 | $8:27,\ 9:33,\ 10:41,\ 11:50,\ 12:60$ | | 7 | $9:35,\ 10:42,\ 11:51,\ 12:61,\ 13:72,\ 14:84$ | | 8 | $10:44,\ 11:52,\ 12:62,\ 13:73,\ 14:85,\ 15:98,\ 16:112$ |

In particular, (a)

f_d(2d)=2d(d-1)\qquad(d\ge3).

No uniqueness claim is made for any extremizer.

Standalone re-verification

The complete dependency-free checker is:

runs/erdos1085_wavew031_verify.py

Run:

python3 runs/erdos1085_wavew031_verify.py --max-d 14 --max-m 9 --online

(d) It uses only Python's standard library. Rational constructions, matrix ranks, determinants, and matching-form restrictions use exact fractions.Fraction; the pentagonal bipyramid is computed in the exact quadratic field $\mathbb Q(\sqrt5)$. The graph portion exhausts all four- and five-edge non-unit graphs on seven labelled vertices, recomputes independence numbers and component signatures, and verifies every determinant identity. The optional network portion checks the cited arXiv IDs, theorem strings, DOI metadata, and the two Erdős primary PDF endpoints.

The central construction logic in the standalone file is:

from fractions import Fraction as Q
from itertools import combinations

def cross_polytope_gram(d, k):
    labels = []
    for axis in range(k):
        labels.extend([(axis, 1), (axis, -1)])
    labels.extend((axis, 1) for axis in range(k, d))
    return [[
        Q(si * sj, 2) if ai == aj else Q(0)
        for aj, sj in labels
    ] for ai, si in labels]

for d in range(3, 15):
    for k in range(3, d + 1):
        G = cross_polytope_gram(d, k)
        d2 = [
            G[i][i] + G[j][j] - 2 * G[i][j]
            for i, j in combinations(range(d + k), 2)
        ]
        assert d2.count(Q(2)) == k
        assert d2.count(Q(1)) == len(d2) - k

(d) The executed full run reported:

Exact construction checks: PASS
  dimensions d=1..14
  verified near-diagonal triples: 92
Matching-obstruction algebra: PASS
  exact rational test cases: 672
Vertex-cover equality reduction: PASS
  exhaustively checked small edge sets: 34004
Exact f_3(7)=15 checks: PASS
  4-edge complements / isomorphism types: 1785 / 3
  5-edge complements with independence number <=4: 12432
  surviving labelled max-degree-2 complements: 6132
  surviving isomorphism types: 7
  checked case-pattern certificates: 7
  exact determinant evaluations: 30
Online citation endpoints: PASS (15 checked)

(a) The finite enumeration is only an audit of the short graph lists in (16)--(17). The upper bounds themselves are the uniform proofs given above; they do not rely on extrapolating computation.

What remains and the precise walls

(a) The exact near-simplex band and $f_3(7)$ are finite-regime results. They do not close the fixed-$d$, $n\to\infty$ estimates asked for by “Estimate”.

(b) In the plane, the verified current gap is between Sawin's $\Omega(n^{1.014114})$ lower bound along arbitrarily large $n$ and the Spencer--Szemerédi--Trotter $O(n^{4/3})$ upper bound. The exact named missing lemma for the first known route to a better upper bound is Pach--Raz--Solymosi Conjecture 7, the $n^{7/6}$-edge rigid-subframework statement above. This report does not prove it.

(b) In three dimensions, even after correcting the page, the gap is

n^{4/3}\log\log n\ll f_3(n) \ll_\epsilon n^{295/197+\epsilon}.

Closing it requires a genuinely stronger point--sphere/circle-incidence theorem or a stronger construction; the clique/nullity argument here only sees graphs whose complements have $O(n)$ edges and becomes vacuous in this sparse-unit-graph asymptotic regime.

(b) Swanepoel's paper explains the exact odd-dimensional obstruction: for each fixed odd $d\ge5$ and sufficiently large $n$, the unresolved secondary term is tied to the maximum number of unit distances on a two-sphere (of radius $1/\sqrt2$ for odd $d\ge7$, with variable radius in dimension $5$). Thus Erdős--Stone supplies the quadratic coefficient but not the finite optimization inside a Lenz component.

(c, precise next finite computation) For $f_3(8)$, Theorem 1 only gives $f_3(8)\le23$, i.e. at least five non-unit pairs. Testing equality requires classifying strict embeddings of $K_8$ with exactly five deleted edges. There are

\binom{\binom82}{5}=\binom{28}{5}=98{,}280

labelled complement candidates before isomorphism and clique pruning. Graph enumeration is cheap; the missing step is a certified solver for each surviving partial Euclidean distance matrix—equivalently, exact rank-$\le3$ positive-semidefinite completion with every unspecified distance constrained away from one. At roughly $0.1$--$10$ seconds per semialgebraic certificate, an unpruned first frontier would cost about 3--273 core-hours, and failures can be substantially more expensive. I did not run that computation on this few-minute budget.

(c) I make no claim that the two exact theorems are absent from all literature. What is verifiable here is the self-contained proof, the exact construction data, the complete seven-vertex obstruction, and the independent executable audit.

PARTIAL: Proved the exact near-simplex band $f_d(n)$ for $n\le2d$ (including $f_d(d+3)=\binom{d+3}{2}-3$ in every dimension), proved $f_3(7)=15$, and corrected the live page's three-dimensional upper bound to Zahl's $O_\epsilon(n^{295/197+\epsilon})$; the fixed-d asymptotic gaps remain open.

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