ExactFivePointNonStarThrackleSupportBoundCertificate
plain-language theorem explainer
Packages the exact five-vertex non-star thrackle support bound as a standalone proposition: on five planar points, any ordered edge set with no geometrically disjoint pair and no universal vertex has unordered support size at most five. Cited by the five-point-or-larger non-star support theorem, which splits the |A|≥5 case into this exact-five certificate plus a six-or-larger residual. Definitional Prop only; no proof body.
Claim. For every finite set $A$ of planar points and every finite set $E$ of ordered pairs from $A\times A$ with distinct endpoints: if no two edges of $E$ are geometrically disjoint, $|A|=5$, and no vertex is incident to every edge of $E$ (non-star), then the unordered edge support of $E$ has cardinality 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 convenience; for positive distances, ordered multiplicity is twice the unordered count, so the classical bound $\le n$ becomes $\le 2n$.
Here the combinatorial object is a thrackle-style edge set on a finite point set in the plane: every pair of ordered edges fails geometric disjointness (they share a vertex or cross). The non-star hypothesis says no single vertex meets every edge. The unordered edge support collapses $(u,v)$ with $(v,u)$ and counts distinct geometric edges.
The certificate is kept separate from the large support theorem so the finite five-point boundary geometry can be attacked on its own, without carrying the six-or-larger residual.
proof idea
No proof: this is a bare Prop definition packaging the exact-five non-star support statement. Downstream theorems take an inhabitant of this Prop as a hypothesis and discharge the $|A|=5$ branch by case split on cardinality.
why it matters
Feeds fivepoint_nonstar_support_bound_from_exact_five_and_six_residual, whose doc-comment states that the exact five-point support plus the six-point-or-larger residual supplies the five-point-or-larger non-star support theorem. That parent is the bridge from finite thrackle geometry into the distance-shell multiplicity program (Erdős #132 in RS units).
Isolating the five-point case matches the module strategy: small cardinalities are pure planar combinatorial geometry and can be closed independently of asymptotic shell-flux arguments. In the RS reading, a support bound $\le |A|$ limits how many distinct two-body recognition edges can sit on a five-point configuration without a star vertex or a disjoint pair, which constrains shell occupancy at the sparse end of the spectrum.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.