# Classification of finite Euclidean Ramsey configurations

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

- [A classification of finite Euclidean Ramsey configurations](../../preprints/A-classification-of-finite-Euclidean-Ramsey-configurations-September-23-2026/paper.pdf)

## Scope

A finite configuration is Euclidean Ramsey if every finite coloring of some sufficiently high-dimensional Euclidean space contains a monochromatic congruent copy at the original scale. The formalization gives the tensor-field classification for full-affine-span configurations, covers singleton and affine-span reductions, and proves that every Ramsey configuration is cospherical. It also proves that every nonempty subset of a finite transitive configuration and every nonempty set of at most five points on a circle is Ramsey. A further sufficient condition uses linear independence of the quadratic evaluation rows of a spherical configuration.

The formalization also gives spherical non-Ramsey examples: the specified twelve-point set on the unit circle has a fifty-color obstruction in every positive dimension, and a nine-point circle configuration built from algebraically independent parameters is non-Ramsey.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Tensor-field classification of Ramsey configurations | [EuclideanRamsey.lean](../ComparatorChallenges/EuclideanRamsey.lean) |
| Twelve-point spherical non-Ramsey example | [GrahamSpherical.lean](../ComparatorChallenges/GrahamSpherical.lean) |
| Ramsey property for at most five circle points | [EuclideanRamseyCircle.lean](../ComparatorChallenges/EuclideanRamseyCircle.lean) |
| Nine-point non-Ramsey circle configuration | [EuclideanRamseyNine.lean](../ComparatorChallenges/EuclideanRamseyNine.lean) |
| Quadratic-independence criterion for spherical configurations | [EuclideanRamseyQuadratic.lean](../ComparatorChallenges/EuclideanRamseyQuadratic.lean) |
| Cosphericity of Ramsey configurations | [EuclideanRamseySpherical.lean](../ComparatorChallenges/EuclideanRamseySpherical.lean) |
| Ramsey property for subsets of finite transitive configurations | [EuclideanRamseyTransitive.lean](../ComparatorChallenges/EuclideanRamseyTransitive.lean) |