lemmaroutine

Unit distances persist under algebraic perturbation

Lemma·inc:specialization·§2.1 Preserving incidences under algebraic specialization

Statement (paper)

Let

x_1,\ldots,x_n

be distinct points of

\R^2

, and let

\mathcal E

be any collection of pairs

(i,j)

for which

\norm{x_i-x_j}_2=1

. There are distinct points

x'_1,\ldots,x'_n

with real algebraic coordinates, arbitrarily close to the respective original points, such that

\norm{x'_i-x'_j}_2=1

for every

(i,j)\in\mathcal E

In plain English

Given distinct planar points

x_1,\ldots,x_n

and any set

\mathcal E

of index pairs at unit distance, there are distinct points

x'_1,\ldots,x'_n

with real algebraic coordinates, arbitrarily close to the originals, such that

\norm{x'_i-x'_j}_2=1

for every

(i,j)\in\mathcal E

Why it's here

This lets the paper replace an arbitrary real unit-distance configuration by one with real algebraic coordinates without losing any of the specified unit pairs. That reduction is what allows the later algebraic and incidence arguments, such as the proof of the piece proposition, to be applied. The idea is that the unit-distance conditions define a real algebraic variety containing the original configuration, and algebraic points are dense in it.

Classified routine:

Follows from the standard fact that real algebraic points are dense in a real algebraic variety defined over Q (a consequence of the Tarski–Seidenberg transfer principle), applied to the variety cut out by the unit-distance equations; distinctness is preserved because it is an open condition.

Uses

Nothing else in the paper

Used by

propIncidence piece with degree and expansion controlclaimCutting deletion loses few incidences

Sources

PaperOpen

Section: §2.1 Preserving incidences under algebraic specialization
Page: —
Label: inc:specialization
Line: sections/01-incidence.tex:25

Leannot aligned

Phase 2 aligns this node to a Lean declaration.