ExactFourPointK4ObstructionCertificate
plain-language theorem explainer
Names the geometric K4 thrackle obstruction on four ambient points: any non-star straight-line edge system whose unordered support exceeds four edges must contain two ordered edges that are geometrically disjoint. Downstream thrackle-bound theorems cite this Prop as the certificate they discharge or assume. The body is a pure universal statement, not a proved theorem.
Claim. The following property holds: for every finite set $A$ of planar points and every finite set $E$ of ordered pairs of distinct points of $A$, if $|A|=4$, no vertex is incident to every edge of $E$ (non-star), and the unordered support of $E$ has more than four edges, then there exist $e,f\in E$ that are geometrically disjoint as segments.
background
The module physicalizes Erdős problem #132: classical distance shells become two-body recognition-energy shells, with ordered multiplicity twice the unordered count, so the classical bound $\le n$ becomes $\le 2n$.
Here $A\subset\mathbb{R}^2$ is a four-point ambient set and $E$ a straight-line system of ordered edges on $A$. The unordered support forgets orientation and doubles; a system is a star when some vertex meets every ordered edge. Geometric disjointness means the two open segments do not meet (the thrackle-forbidden configuration).
After pure counting closes the triangle boundary, the remaining finite obstruction is exactly this K4 statement: excess support on four points forces a disjoint pair unless the drawing is a star.
proof idea
Definitional abbreviation only: the body is the Prop itself, quantifying over ambient four-point sets and ordered edge systems, imposing edge-wellformedness, cardinality four, the non-star hypothesis, and support excess, then asserting existence of a geometrically disjoint ordered pair. No tactics or lemmas are applied; sibling theorems later assume or discharge this certificate.
why it matters
This certificate is the geometric half of the exact four-vertex thrackle boundary used throughout the module's Conway–K4 assembly. Downstream, exact_fourpoint_support_bound_from_k4_obstruction turns the certificate into the non-star support bound under pairwise intersection; the converse bridge lifts a support-level obstruction to this ordered form. The unconditional noncollinear Conway thrackle support bound and the four-point matching dichotomy both route through it: every non-degenerate four-point configuration yields a disjoint perfect matching of $K_4$.
In the RS reading of Erdős #132, shell multiplicity bounds become recognition-energy occupancy bounds; the K4 obstruction is the last finite combinatorial gate before those shell bounds close. It sits after counting finishes the triangle case and before the global sparse-shell divergence arguments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.