ExactFourPointConwayThrackleSupportBoundCertificate
plain-language theorem explainer
Packages the Conway-conditioned K4 support bound as a bare proposition: any Conway thrackle on four planar points, with edges among those points and with no ordered-edge-incident vertex, has unordered support size at most four. Downstream noncollinear K4 theorems cite this shape. Definition only; no proof obligations discharged here.
Claim. For every finite point set $A\subset\mathbb{R}^2$ and every finite set $E$ of ordered pairs of distinct points of $A$, if $E$ is a Conway thrackle, $|A|=4$, and no point of the plane is an ordered-edge-incident vertex of $E$, then the cardinality of the unordered edge support of $E$ is at most $|A|$.
background
The ambient 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 bookkeeping; for positive distances the ordered multiplicity is exactly twice the unordered one, so classical thresholds $\le n$ become $\le 2n$.
The present declaration isolates the exact four-point Conway thrackle support bound. A Conway thrackle is a geometric edge set in which every pair of edges meets exactly once under the Conway crossing rules. The K4 boundary case asks how large the unordered support of such an $E$ can be when the vertex set has cardinality four and no ordered-edge-incident vertex is present. The collinear residual is deliberately separated: when all four points lie on a line the algebraic dichotomy degenerates and one must sort by line parameter.
proof idea
There is no proof. The declaration is a Prop-valued definition whose body is the universal quantification over finite point sets $A$ and ordered edge sets $E$ of the support inequality under the Conway, cardinality-four, and no-incident-vertex hypotheses. It exists so later theorems can name and discharge (or condition on) this exact shape rather than inline the quantifiers.
why it matters
This is the correct shape of the Conway-conditioned K4 boundary used in the distance-shell program. The immediate consumer is exact_fourpoint_conway_thrackle_support_bound_noncollinear_thm, which obtains an unconditional noncollinear bound by combining a six-unordered-pair subset lemma with a conditional four-point support theorem. Packaging the inequality as a named certificate lets the noncollinear case close immediately while the collinear residual remains a separate hand-geometry obligation. In the broader RS reading of Erdős #132, controlling support size on four-point thrackles limits how a single recognition-energy shell can sit on a small vertex set, feeding the sparse-shell and diameter-shell analysis elsewhere in the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.