---

Source. Published pp. 1–4 and 6 (canonical PDF). This page records interfaces and proof provenance. It contains no additional complete proof component.

The only non-elementary Ramsey input used for the source's consequence is Kříž (1991), Theorem 4.3: if a finite Euclidean configuration admits a soluble isometry group $G$, then for every $q\ge1$ some dimension forces an isometric copy on which each $G$-orbit is monochromatic. For a transitive action this is ordinary Ramsey. Only the transitive specialization is needed here. The canonical Kříž proof includes its same-paper prerequisites and records its precise external finite Ramsey and Rado inputs. It is not duplicated in this unit. Subset and congruence closure use the existing closure proof.

Lemma 10 uses the canonical finite negative-type/Gram criterion: a symmetric zero-diagonal array $d_{ij}$ is realizable as squared Euclidean distances if and only if $\sum_{i<j}c_ic_jd_{ij}\le0$ for every zero-sum real vector $c$; strict inequality for nonzero such vectors is equivalent to affine independence. The finite-dimensional proof and the compactness of its strict unit-vector margin are already compiled there. This supplies the exact content needed from the source's Schoenberg reference. No claim of full review of Schoenberg's 1938 paper is made.

Lemma 4 reproduces, in rewritten form, the entire argument which Karamanlis quotes from Frankl–Pach–Reiher–Rödl, Borsuk and Ramsey type questions in Euclidean space, Lemma 4.9. Consequently that lemma is not an unproved outside input here; the earlier chapter's remaining contents are outside this unit.

The source's Section 3 opening says that the proof of Theorem 2 uses a result of Matoušek–Rödl (1995); this clause was added in arXiv v3 to an opening already present in v1 and v2, and the publication retains it. It does not specify a further numbered statement from that paper in the displayed dependency chain. All finite approximation steps needed here are proved in Lemma 7 and Proposition 8, and the contraction in Lemma 10 is justified above. Thus the present reconstruction does not require an unspecified Matoušek–Rödl assertion. This does not fill the separate primary-source acquisition gap for that paper or prove the stronger spread-vector sphere approximation used in Frankl–Rödl (2004).

The ancillary abelian-orbit proof uses the standard finite-dimensional spectral theorem for commuting unitary operators and the already compiled finite isometry extension. The approximation uses only elementary floor, trigonometric and integral inequalities. No numerical certificate, infinite computation or local formal build is an input to these arguments.

The introduction's Graham and Leader–Russell–Walters conjectures and its account of known examples are historical context from 2022. This source unit neither updates their current status nor promotes a theorem about simplices to a characterization of all spherical or Ramsey sets.