FivePointNonStarThrackleSupportBoundCertificate
plain-language theorem explainer
The five-point-or-larger non-star thrackle support certificate asserts that any straight-line thrackle on at least five plane points, with no universal vertex, has unordered edge support of size at most the number of vertices. Workers closing the residual of the straight-line thrackle bound after the four-vertex boundary would cite it. It is a bare Prop definition packaging that quantified claim so exact-five and six-or-larger residual theorems can discharge it independently.
Claim. For every finite set $A$ of plane points and every finite set $E$ of ordered pairs from $A$ with distinct endpoints: if every pair of edges in $E$ fails to be geometrically disjoint, $|A|\ge 5$, and 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 records the Recognition Science physicalization of Erdős problem #132. Classically a distance value is a shell in the set of pairwise Euclidean distances; physically it is a two-body recognition-energy shell whose multiplicity is the shell occupancy. Ordered pairs are used for Lean simplicity: for a positive distance, ordered multiplicity is twice the unordered multiplicity, so the classical threshold $\le n$ becomes $\le 2n$.
This certificate sits on the thrackle side of that geometry. Edges are ordered pairs of distinct points drawn from a finite plane set $A$. The non-disjointness hypothesis forces every pair of edges to meet (share a vertex or cross), the straight-line thrackle condition. The non-star hypothesis excludes configurations in which a single vertex is incident to every edge. Unordered edge support collapses each ordered pair and its reverse to one undirected edge.
The Prop isolates the five-or-more vertex non-star case after the exact four-vertex boundary has been peeled off, matching the module strategy of separating finite boundary geometry from the large residual.
proof idea
This is a definition of a proposition, not a proved theorem. The body is the quantified claim itself: for all finite point sets $A$ and ordered edge sets $E$, if edges stay inside $A$ with distinct ends, every pair of edges is geometrically non-disjoint, $|A|\ge 5$, and the drawing is non-star, then the unordered support of $E$ has size at most $|A|$. No tactics or lemmas fire; the definition simply names that Prop so later residual-combination theorems can target it.
why it matters
The certificate is the genuinely large residual half of the remaining straight-line thrackle support bound once the exact four-vertex boundary is separated (per the doc-comment). Downstream, the exact-five-plus-six residual theorem assembles an exact-five certificate and a six-or-larger certificate into this Prop by case-splitting on whether $|A|=5$. In turn, the four-point residual theorem consumes this Prop as the five-or-larger hypothesis to obtain the four-point-or-larger non-star bound.
In the RS reading, the thrackle edge bound limits how many two-body recognition edges can occupy a distance shell without geometric independence, feeding the shell-multiplicity side of the Erdős #132 physicalization. Naming the five-or-larger claim as a standalone Prop lets finite boundary geometry (exact five) be attacked independently of the asymptotic residual, exactly as the inline comment intends.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.