CollinearFourPointConwayResidual
plain-language theorem explainer
Packages the residual collinear K4 claim for Conway thrackles: four collinear points with a thrackle edge set and no incident vertex force unordered edge support at most 4. Cited by the unconditional noncollinear four-point thrackle support bound, which splits off this case so algebra can finish elsewhere. The declaration is a bare Prop definition, not a proved theorem.
Claim. The residual collinear Conway claim is the proposition: for every finite set $A$ of plane points and every finite set $E$ of ordered pairs from $A$ with distinct endpoints, if $E$ is a Conway thrackle, $|A|=4$, no vertex has an ordered edge of $E$ incident to it, and every triple in $A$ is collinear (orientation zero), then the cardinality of the unordered edge support of $E$ is at most $|A|$.
background
The module physicalizes Erdős problem #132: classical distance shells become two-body recognition-energy shells, with ordered-pair multiplicity twice the unordered count, so classical occupancy $\le n$ becomes $\le 2n$.
Here the local obstruction is a Conway thrackle on four points in the plane. Orientation orient2 vanishes on a triple precisely when the three points are collinear. The unordered edge support forgets direction of each ordered pair. The no-incident-vertex hypothesis excludes stars and forces the thrackle to live purely on the complete graph $K_4$ skeleton.
The surrounding development splits collinear from noncollinear geometry. Algebraic same-side and SOS-Plücker dichotomies handle the noncollinear branch; when all four points lie on a line those sign products degenerate, so the collinear residual is isolated as its own proposition.
proof idea
No proof body: the declaration is a Prop abbreviation. It conjoins the standard thrackle edge hypotheses (endpoints in $A$, distinct, Conway thrackle, $|A|=4$, no ordered incident vertex) with the global collinearity assumption that every triple has vanishing orientation, and asserts the support bound $\mathrm{card}(\mathrm{unorderedEdgeSupport}, E)\le |A|$. Downstream theorems either assume this proposition or discharge the complementary noncollinear case.
why it matters
This residual is the only remaining hand-geometry case for the Conway-conditioned $K_4$ support bound inside the distance-shell multiplicity program. The parent theorem exact_fourpoint_conway_thrackle_support_bound_noncollinear_thm quotes the complementary hypothesis (not all triples collinear) and closes unconditionally by combining a six-pair support subset with a conditional thrackle bound; isolating collinearity here lets that noncollinear theorem finish without sorting on a line parameter.
In the broader RS reading of Erdős #132, shell occupancy controls recognition-energy multiplicity on the phi-ladder. Bounding thrackle support on four-point configurations is a combinatorial gate on how many ordered pairs can share one distance shell. The collinear case is flagged in the doc-comment as the sole place where algebraic dichotomy fails and one must sort by line parameter, so stating it separately keeps the main noncollinear chain clean.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.