Almost-equidistant sets in R^4 have at most 12 points: an independent, certified verification of a conjecture of Balko, Pór, Scheucher, Swanepoel and Valtr

A set of points in Rd is almost-equidistant if among any three of its points some two are at unit distance, and f(d) is the largest size of such a set. Balko, Pór, Scheucher, Swanepoel and Valtr (Graphs Combin. 36 (2020) 729–754) proved 12 ≤ f(4) ≤ 13, reducing the question to the realisability in R4 of twelve explicit 13-vertex graphs, and conjectured f(4) = 12. A public code repository (scinet-ai/math-discrete-geometry, July 2026) has since reported a computation that settles the conjecture, without an accompanying paper. This record provides an independent, certified verification of f(4) = 12, together with the full manuscript (f4-almost-equidistant.pdf) and reproduction package (release_f4_v2.zip, 840 files): Independent re-derivation of the enumeration of the 12 minimal abstract almost-equidistant graphs on 13 vertices in R4, matched one-to-one against both the original authors’ graph6 files and the scinet-ai list. Exact Gröbner-basis decisions over Q in two coordinate models (Model A in R5 with Rabinowitsch saturation; Model B in R4 with radical coordinates), where all 24 systems reduce to {1} under both Singular (slimgb) and msolve, and 11 of the 24 systems are additionally confirmed by Macaulay2. Engine-free certificates for 11 of the 12 graphs: exact rational case-distinction trees whose leaves carry Nullstellensatz identities 1 = ∑ gifi checked by two independent verifiers (with 2 graphs closing by pure rational case analysis, also written out by hand). Six negative controls and one 13-vertex positive control with an explicit integer realisation.