FourPointNonStarThrackleSupportBoundCertificate
plain-language theorem explainer
A certificate proposition asserting that any straight-line thrackle on at least four points that is not a star has unordered edge support at most the vertex count. Researchers working the thrackle/endpoint-charging side of the Erdős #132 distance-shell program cite it as the four-point-or-larger residual. It is a pure Prop definition, not a proved bound; downstream lemmas discharge or consume it.
Claim. The following assertion holds as a named certificate: for every finite point set $A\subset\mathbb{R}^2$ and every finite set $E$ of ordered pairs of distinct points of $A$, if no two members of $E$ are geometrically disjoint as ordered edges, $|A|\ge 4$, 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 a positive distance, ordered multiplicity is twice the unordered count, so the classical $\le n$ threshold becomes $\le 2n$.
A straight-line thrackle here is an edge system on a finite planar point set in which every pair of edges fails geometric disjointness (they cross or share a vertex in the thrackle sense). Stars (all edges through one common vertex) and the exact three-point case are already handled separately; the three-point boundary is closed by the existing unordered-support bound at cardinality three.
This declaration packages the remaining four-point-or-larger non-star residual as a single proposition, so later charging and support lemmas can take it as a hypothesis rather than restate the quantifiers.
proof idea
There is no proof body beyond the definition of a Prop. The declaration is the universal statement itself: quantify over finite point sets and ordered edge sets, impose the thrackle non-disjointness hypothesis, the cardinality lower bound $|A|\ge 4$, and the non-star condition, and assert that unordered edge support is at most $|A|$. Downstream theorems either assume this certificate or build it from exact four-point and five-point residual certificates.
why it matters
In the thrackle ladder toward endpoint charging, this is the first genuinely geometric finite residual after stars and triangles. Downstream, fourpoint_nonstar_support_bound_from_exact_four_and_five_residual assembles it from an exact four-vertex certificate plus a five-point-or-larger residual. large_nonstar_support_bound_from_fourpoint_residual then closes the large non-star support residual, because the three-point case reduces to the known triangle bound. Finally thrackle_endpoint_charging_from_fourpoint_nonstar_support_bound lifts the certificate to the full endpoint-charging form of the straight-line thrackle bound.
Within Recognition Science this sits in the mathematics layer that feeds distance-shell multiplicity (Erdős #132 physicalized as recognition-energy shells). Closing the certificate is a finite combinatorial gate on the path from ordered spectra to shell-occupancy control; it does not itself invoke the forcing chain (T5–T8) or the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.