claimroutine
Generic horizontal direction exists
Statement (paper)
There exists an auxiliary horizontal direction such that an input point and an intersection point of two original circles have different horizontal coordinates unless they are the same point, and an input point has a horizontal coordinate different from that of a horizontal extremum of an original circle unless it is that extremum. Only finitely many directions are excluded.
In plain English
One can choose a direction, used as the horizontal axis, so that no input point shares its horizontal coordinate with an intersection point of two original circles or with a horizontal extremum of an original circle, unless it coincides with that point. Only finitely many directions are ruled out.
Why it's here
This is a genericity step for the sweep in the proof of the cutting lemma. Choosing the direction this way means a vertical line through an input point meets no other critical point (intersection or extremum) of the circle arrangement, which lets later claims treat sweep pieces and point assignments cleanly. It works because each coincidence of horizontal coordinates forbids only finitely many directions among the finitely many points, intersections and extrema.
Classified routine:
Standard general-position argument: each pair of distinct points (and each point versus a circle's horizontal extremum) rules out only finitely many directions, as in the usual vertical-decomposition setup for cuttings (e.g. Clarkson–Shor style constructions).
Uses
Nothing else in the paper
Used by
Sources
PaperOpen
- Section
- §2.2 Cuttings and the incidence bound
- Page
- —
- Label
—- Line
sections/01-incidence.tex:86
Leannot aligned
Phase 2 aligns this node to a Lean declaration.