exact_fourpoint_conway_thrackle_support_bound_noncollinear_thm
plain-language theorem explainer
For any four-point planar set that is not entirely collinear, a Conway straight-line thrackle on those vertices has unordered edge support of size at most four. Discrete geometers working the thrackle conjecture or the four-vertex boundary of Erdős-type distance problems would cite it. The proof enumerates the four vertices, embeds the support in the six possible pairs, converts non-collinearity into a nonzero orientation witness, and applies the conditional four-point bound.
Claim. Let $A\subset\mathbb{R}^2$ be a finite set with $|A|=4$, and let $E$ be a finite set of ordered pairs of distinct points of $A$. Suppose every two distinct edges of $E$ meet simply (share exactly one point: a common endpoint or a proper crossing), i.e.\ $E$ is a Conway straight-line thrackle. If the four points of $A$ are not all collinear, then the number of distinct unordered edges supporting $E$ is at most $|A|=4$.
background
The ambient module physicalizes Erdős problem #132: classical distance shells become two-body recognition-energy shells, with ordered multiplicity twice the unordered count. The present declaration sits in the geometric thrackle layer that bounds support size before shell-multiplicity estimates.
A Conway straight-line thrackle is an edge system in which every pair of distinct edges meets simply: they share exactly one point, either a common endpoint or a proper crossing. Points are planar (Point2). The unordered edge support forgets orientation and collapses both directions of an undirected segment to one support edge.
The four-point case is the exact $K_4$ boundary. Earlier certificates failed on all-collinear configurations because overlap counts as meeting yet supplies no geometrically disjoint pair. The corrected target separates the noncollinear case (this theorem) from an all-collinear residual handled later by sorting on the supporting line.
proof idea
Classical mode. From $|A|=4$, extract four pairwise-distinct points $a,b,c,d$ whose set equals $A$. The support of $E$ sits inside the six unordered pairs on those points (subset lemma from the edge-incidence hypothesis and the enumeration).
Non-collinearity of $A$ is rewritten as: at least one of the four triple orientations $\mathrm{orient2}(a,b,c)$, $\mathrm{orient2}(a,b,d)$, $\mathrm{orient2}(a,c,d)$, $\mathrm{orient2}(b,c,d)$ is nonzero. The contrapositive uses the quadruple-zero lemma: if all four orientations vanish, every triple in $A$ is collinear.
The conditional four-point Conway support bound then yields $|\mathrm{support}(E)|\le 4$. Rewrite the right-hand side by $|A|=4$.
why it matters
This is the unconditional noncollinear half of the corrected exact four-point Conway thrackle support bound. Bridge notes list it as step 3 toward exact_fourpoint_conway_thrackle_support_bound_thm, which must then lift through the five- and six-point boundary chain to close the large non-star support bound and ultimately the full Conway thrackle support bound.
In the Recognition Science reading, thrackle support controls how many distinct two-body channels a finite planar configuration can carry under the simple-meeting law; that feeds distance-shell multiplicity (Erdős #132 physicalized). The module already isolates the collinear residual and the pending symmetric SOS-Plücker pair lemmas needed for a stronger two-matching dichotomy. No downstream consumers are wired yet; the declaration is a proved leaf waiting for the combine-and-lift step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.