LargeNonStarConwayThrackleSupportBound
plain-language theorem explainer
Defines the large non-star residual of Conway's straight-line thrackle support bound: for planar point sets of size at least four with no star vertex, any Conway thrackle has unordered edge support at most the number of points. Discrete geometers and anyone closing the Erdős #132 counting residual would cite it. As a Prop abbreviation it carries no proof; it packages the remaining infinite family after stars and |A|≤3 are bookkept away.
Claim. For every finite planar point set $A$ and every set $E$ of ordered pairs with distinct endpoints in $A$, if $E$ is a Conway thrackle, $|A|\ge 4$, and no vertex is incident to every ordered edge of $E$, then the number of unordered edges supporting $E$ is at most $|A|$.
background
The module physicalizes Erdős problem #132: classical distance shells become two-body recognition-energy shells, and shell multiplicity is occupancy. Ordered pairs are used for Lean bookkeeping; for positive distances, ordered multiplicity is twice the unordered count, so the classical $\le n$ threshold becomes $\le 2n$.
A Conway thrackle here is a straight-line thrackle on a finite point set in the plane: edges meet only at shared endpoints under the Conway crossing rules encoded by IsConwayThrackle. The unordered edge support counts distinct undirected pairs underlying the ordered edge set. A star system is one in which some vertex is incident to every ordered edge; the predicate OrderedEdgesIncidentTo flags that case.
The surrounding development splits Conway support into finite bookkeeping (stars and ambient sets of size at most three) and this residual large non-star family. That residual is the first genuinely infinite counting target on the Conway side of the #132 program.
proof idea
No proof: this is a bare Prop definition packaging a universal statement. The body is the quantified implication itself (edge set supported on $A$, Conway thrackle hypothesis, cardinality lower bound $|A|\ge 4$, universal negation of star incidence, conclusion on unordered support size). Downstream theorems treat the name as a hypothesis to discharge or as one conjunct of a residual.
why it matters
This is the live Conway counting residual after stars and small ambients are closed. The theorem conway_support_bound_from_large_nonstar shows that assuming this Prop yields the full Conway thrackle support bound, by case-splitting on $|A|\le 2$, the size-three bookkeeping, and star incidence. It is also the first conjunct of Erdos132CurrentLargeNonStarResidual (paired with the convex-layer screening bridge); that residual is documented as sufficient to prove Erdős #132 once discharged. The four-point noncollinear support theorem sits nearby as an unconditional special case on $|A|=4$. In the RS ledger this is pure discrete geometry scaffolding for the distance-shell multiplicity bound, not a forcing-chain (T0–T8) step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.