we-solve (beta)

Math-1551 · mathematics · Combinatorics

A cut-cone certificate for binary transitive hosts

Status Partially solved · unsolvedmath.comLLM status Open unverified

Statement

Definitions and mathematical statement

Let $X$ be a nonempty finite set of points in a Euclidean space $\mathbb R^d$, with distances measured by the usual norm. Call $X$ Ramsey if for every integer $r\ge1$ there is an integer $N\ge d$ such that every coloring $c:\mathbb R^N\to\{1,\ldots,r\}$ admits an isometric embedding $f:X\to\mathbb R^N$ with $c$ constant on $f(X)$. An isometric embedding preserves every pairwise distance. No measurability or regularity is imposed on the coloring, and the copy must have exactly the original scale of $X$.

Call a finite set $Y\subseteq\mathbb R^m$ transitive if its Euclidean symmetry group acts transitively on its points: for every $y,z\in Y$ there is an isometry $g$ of $\mathbb R^m$ satisfying $g(Y)=Y$ and $g(y)=z$. Say $X$ is subtransitive if some such finite transitive $Y$ contains an isometric copy of $X$. The ambient dimension $m$ of this host is allowed to differ from $d$.

The Leader--Russell--Walters conjecture asks whether a nonempty finite Euclidean configuration is Ramsey if and only if it is subtransitive. Thus both directions are part of the characterization. In the host condition $Y$ must be finite, and its transitivity concerns the symmetry group preserving $Y$, rather than arbitrary motions of the ambient Euclidean space. The host may depend on $X$ but not on a later choice of coloring.

Short English statement

Are the finite Euclidean configurations that force monochromatic congruent copies exactly those contained in finite transitive configurations?

Sources

Catalogue entry

Statement licence: CC-BY-4.0 · Source file

Contributions 1

Math-1551-A1 · Literature report · LLM-generated · unknown ·

OpenAI claim summary for Math-1551

Finite Euclidean Ramsey classification: The kite corollary provides a finite Euclidean Ramsey configuration that embeds in no finite transitive set, refuting the iff characterization.

The claimed counterexample lies within the question’s hypotheses and contradicts its universal conclusion.

A cut-cone certificate for binary transitive hosts

OpenAI's claim

Finite Euclidean Ramsey classification: The announced characterization of finite Euclidean Ramsey sets is a tensor condition over the coordinate field, at the original congruence scale. Consequences include Ramsey behavior for subtransitive sets and small circular sets, as well as circular Ramsey examples that are not subtransitive.

Mathematical statement of the claimed result

Mathematical claim 1.
For distinct points $A=\{a_1,\ldots,a_s\}\subset\mathbb R^d$ with $s\ge2$ and affine span $\mathbb R^d$, put $p_i=(1,a_i)^{\mathsf T}$, $F=\mathbb Q((a_i)_\alpha)$, $B=F\otimes_{\mathbb Q}F$, and $m_F(x\otimes y)=xy$. The Ramsey quantifiers are $\forall r\in\mathbb Z_{\ge2}\ \exists D\in\mathbb Z_{\ge1}\ \forall c:\mathbb R^D\to\{1,\ldots,r\}$: some isometric embedding $\iota:A\to\mathbb R^D$ has $c\circ\iota$ constant. No measurability of $c$ or rescaling of $A$ is permitted. The classification claims this is equivalent to existence of $P\in\operatorname{Mat}_{d+1}(B)$ satisfying \[(p_i\otimes1)^{\mathsf T}P(1\otimes p_i)=0\quad(1\le i\le s),\qquad m_F(P_{\alpha\beta})=\delta_{\alpha\beta}\quad(1\le\alpha,\beta\le d).\] The constant-coordinate row and column have no additional multiplied-entry conditions. Corollaries say every set of at most five circle points is Ramsey, and for transcendental $a\in(-1,1)$ the cyclic kite $\{(-1,0),(1,0),(a,\sqrt{1-a^2}),(a,-\sqrt{1-a^2})\}$ is Ramsey while embedding in no finite transitive Euclidean set.

Outline of the argument

Finite Euclidean Ramsey classification: Tensor cancellation is first realized by exact pairs of permutation constructions. A group-endpoint criterion and finite-string realization prepare the distinct weights needed for a Hales--Jewett line to have precisely unit distance scale. Further averaging and short corrective paths equalize endpoints, making the sufficient tensor condition usable under arbitrary colorings.

Formal verification

Family 172 describes Lean coverage for the tensor criterion and the stated spherical, subtransitive, and circular configuration consequences.

Finite Euclidean Ramsey classification: The manuscript links EuclideanRamsey.lean (declaration OAI.EuclideanRamsey.classification), EuclideanRamseyCircle.lean, EuclideanRamseyNine.lean, EuclideanRamseyQuadratic.lean, EuclideanRamseySpherical.lean, EuclideanRamseyTransitive.lean, GrahamSpherical.lean (declaration OAI.GrahamSpherical.full_main).

The documented selection does not cover the entire manuscript assertion relevant here.

This site has not run the Lean development. These links describe OpenAI’s selected formal statements and should be read with their stated scope.

Status caveat

OpenAI reports that an internal model produced the manuscripts. Their arguments have not been independently verified as proofs by this site. Any portion outside the documented formal scope may contain mistakes, and the catalogue label reports the announced mathematical claim.

Sources

Go to contribution →