SixPointNonStarThrackleSupportBoundCertificate
plain-language theorem explainer
Packages the six-point-or-larger non-star thrackle support bound as a bare Prop: on any planar point set of size at least six, a non-star edge set in which every pair of ordered edges meets has unordered support at most the number of points. Downstream assembly of the five-point-or-larger non-star theorem cites it as the residual half. Definition only; no proof obligation is discharged here.
Claim. For every finite set $A$ of planar points and every finite set $E$ of ordered pairs with distinct endpoints in $A$: if every pair of edges in $E$ fails to be geometrically disjoint, $|A|\ge 6$, 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 inside Recognition Science: classical distance values become two-body recognition-energy shells, and shell multiplicity is occupancy. Ordered pairs are used for Lean bookkeeping; for a positive distance the ordered multiplicity is twice the unordered one, so classical thresholds of the form $\le n$ become $\le 2n$.
The certificate lives in the thrackle-support layer of that development. An ordered edge set $E$ on a point set $A$ is required to have both endpoints in $A$ and distinct ends. Geometric non-disjointness of every ordered pair replaces the classical thrackle meeting condition. The non-star hypothesis rules out a common vertex incident to every edge. Unordered edge support collapses each undirected pair once, so the bound compares that support size to $|A|$.
Sibling notions in the same file (ordered distance spectrum, shell multiplicity, diameter shells, sparse-shell divergence) supply the ambient language; this Prop isolates only the six-point residual case.
proof idea
There is no proof. The declaration is a def whose body is the quantified Prop above: universal quantification over finite point sets and ordered edge sets, four hypotheses (endpoint validity, pairwise geometric non-disjointness, cardinality at least six, non-star), and the conclusion that unordered support size is at most $|A|$. It is a named hypothesis interface, not a proved theorem.
why it matters
The parent theorem fivepoint_nonstar_support_bound_from_exact_five_and_six_residual takes an exact five-point non-star certificate together with this six-point-or-larger residual and returns the five-point-or-larger non-star support bound, by case-splitting on whether $|A|=5$ or $|A|\ge 6$. The module doc frames the whole development as the RS reading of Erdős #132 (distance shells as recognition-energy shells). Closing or discharging this certificate is therefore a concrete step toward a fully proved non-star support theorem in that chain; until then it remains a definitional obligation rather than a forcing-chain landmark (T0–T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.