ExactFourPointNonStarThrackleSupportBoundCertificate
plain-language theorem explainer
Certificate proposition for the exact four-vertex non-star thrackle support bound: on four ambient plane points, a straight-line ordered edge system with no geometrically disjoint pair and no common vertex has at most four unordered support edges. Downstream thrackle and distance-shell arguments cite it as the finite K4 boundary after stars and triangles. The declaration is a pure Prop definition, not a proved theorem.
Claim. The proposition that for every finite set $A$ of points in the plane and every finite set $E$ of ordered pairs with both endpoints in $A$ and distinct ends: if no two members of $E$ are geometrically disjoint as segments, $|A|=4$, and $E$ is not a star (no vertex is incident to every edge of $E$), then the number of unordered support edges of $E$ is at most $|A|$.
background
The module physicalizes Erdős problem #132: a Euclidean distance value is a two-body recognition-energy shell, and shell multiplicity is occupancy. Ordered pairs are used for Lean bookkeeping; for positive distances, ordered multiplicity is twice the classical unordered count, so classical thresholds $\le n$ become $\le 2n$.
A thrackle-style straight-line system here is a finite set $E$ of ordered edges on an ambient point set $A$. Geometric disjointness of ordered edges means the underlying segments do not meet (the obstruction that forces the support bound). Non-star means no single vertex is incident to every edge of $E$. Unordered edge support collapses each undirected pair once.
This certificate is the first genuinely geometric finite case after pure counting closes stars and triangles: the exact four-vertex boundary left as a K4-type obstruction.
proof idea
No proof body: the declaration is a def equating the certificate name to a Prop. The right-hand side is a single universal quantification over ambient point sets $A$ and ordered edge sets $E$, packaging the edge-validity, pairwise non-disjointness, cardinality-four, and non-star hypotheses, and concluding that unordered support size is at most $|A|$. Downstream theorems discharge or consume this Prop rather than expand it inline.
why it matters
In the Recognition Science treatment of distance-shell multiplicity, this certificate isolates the exact four-point non-star thrackle boundary so larger arguments can case-split cleanly. exact_fourpoint_support_bound_from_k4_obstruction proves the certificate from the exact K4 obstruction under pairwise intersection. fourpoint_nonstar_support_bound_from_exact_four_and_five_residual consumes it together with the five-point residual to obtain the four-point-or-larger non-star support theorem. The geometric heart feeding the obstruction is the four-point matching dichotomy: in any non-all-collinear 4-point set, at least one perfect matching of $K_4$ consists of two geometrically disjoint segments. That is the finite geometric residue after counting finishes triangles; it sits inside the broader RS physicalization of Erdős #132 shell occupancy.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.