LargeNonStarThrackleSupportBoundCertificate
plain-language theorem explainer
Packages the cardinal residual for straight-line thrackles on at least three points that are not stars: every pair of edges meets, and the unordered support size is at most the number of vertices. Anyone closing the thrackle side of the distance-shell program cites this interface. It is a bare Prop definition, not a proved bound; three-point systems are already discharged elsewhere.
Claim. The following residual statement holds: for every finite point set $A\subset\mathbb{R}^2$ and every finite set $E$ of ordered pairs on $A$ with distinct endpoints, if no two members of $E$ are geometrically disjoint, $|A|\ge 3$, and $E$ is not a star (no vertex is incident to every edge of $E$), 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, 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 threshold $\le n$ becomes $\le 2n$.
A thrackle here is a straight-line system in which every pair of edges meets geometrically (the negation of ordered geometric disjointness). Star systems (all edges share a common vertex) and systems with $|A|\le 2$ are treated separately. The three-point boundary is already closed by the finite triangle bound on unordered support cardinality.
This certificate is the weakest remaining finite cardinal statement on the thrackle side once those small cases are removed: large non-star systems must still satisfy $|\mathrm{support}(E)|\le |A|$.
proof idea
Definitional packaging only: the declaration is a Prop alias for a universal residual, not a proved theorem. No tactics or lemmas discharge the bound. Downstream, the three-point case is split off by a card equality case and fed to the already-proved unordered support bound at cardinality three; the four-point-or-larger residual is the remaining obligation that implies this certificate.
why it matters
In the thrackle residual ladder, this is the cardinal bottleneck after stars and tiny vertex sets are closed. Downstream, assuming the certificate yields the large-non-star endpoint-charging residual via finite cardinal comparison producing an injection, and that in turn yields the full straight-line thrackle endpoint-charging certificate.
The four-point residual implies this certificate because the exact three-point boundary is already settled. Within the Recognition Science reading of Erdős #132, thrackle-type intersection constraints bound shell support against vertex count, feeding the distance-shell multiplicity program. It does not itself touch the forcing chain (T5–T8) or the RCL; it is pure combinatorial geometry scaffolding for the shell-occupancy side.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.