{"id":"palomar/PALOMAR-2026-10-07-000011","url":"https://github.com/JD-Jones-ASES/six-concyclic-lean/tree/6bf3f4019bf0ced69f609abe3d517f9d7c31e55e","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-07-000011-v1.json","repo":"https://github.com/JD-Jones-ASES/six-concyclic-lean","tags":["math.CO","math.MG","msc:05D10","msc:52C10","euclidean-ramsey","discrete-geometry","lean-formalization"],"score":0,"title":"Six concyclic points satisfy the Euclidean Ramsey tensor criterion, as does every spherical set of at most m + 4 points of affine dimension m and every algebraic spherical set; given the classification's sufficiency half, these sets are Ramsey (the algebraic ones when spanning)","trust":"high","domain":"math.CO","source":"palomar","authors":["JD Jones"],"reviews":0,"subject":"math.CO","summary":"A Lean 4 development around the tensor criterion of the classification of finite Euclidean Ramsey configurations (openai/math, family 172). With the criterion's definitions restated character for character from that project's challenge file: every set of six distinct points on a circle satisfies the criterion, by an explicit certificate (the product of the two bilinear forms through the first three and the last three points of a homogeneous parametrisation of the circle, scaled and conjugated by the parametrisation); the sharp dimension theorem: every spherical set of at most m + 4 distinct…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-07","reactions":{},"formalized":true}