ExactFourPointSupportK4ObstructionCertificate
plain-language theorem explainer
Support-level certificate for an exact four-vertex K4 obstruction: on any 4-point planar set whose ordered edge set is non-star and whose unordered support is larger than the vertex count, two support edges admit geometrically disjoint representatives. Downstream assembly cites it to lift support obstruction to the ordered-representative K4 certificate. Pure Prop definition; no proof obligations.
Claim. For every finite planar point set $A$ and every finite set $E$ of ordered pairs with both endpoints in $A$ and distinct ends: if $|A|=4$, no vertex is an ordered star of $E$, and $|A|$ is strictly smaller than the number of unordered edges supporting $E$, then there exist two unordered support edges of $E$ that have geometrically disjoint representatives.
background
The module physicalizes Erdős problem #132 inside Recognition Science: a classical distance value is a shell in the pairwise Euclidean spectrum; physically it is a two-body recognition-energy shell whose multiplicity is shell occupancy. Ordered pairs are used for Lean bookkeeping; for positive distances ordered multiplicity is twice the unordered count, so classical thresholds scale by two.
This declaration is the support-level form of the exact four-vertex K4 obstruction. As the doc-comment states, it "asks for two unordered support edges with geometrically disjoint representatives" and is "the natural next geometric target because the finite graph bookkeeping can first find the two unordered candidates, and the segment geometry then supplies the representatives."
Point2 is the planar point type. The non-star hypothesis uses ordered incidence on $E$. The surplus hypothesis compares $|A|$ to the cardinality of the unordered edge support of $E$. The conclusion is existence of a pair of support edges with disjoint geometric representatives.
proof idea
Definitional Prop, not a proved theorem. The body is a single universal quantifier over vertex finsets $A$ and ordered-edge finsets $E$, packing four hypotheses (edges internal to $A$ with distinct ends; $|A|=4$; no ordered star vertex; edge-support surplus) and concluding existence of two unordered support edges with disjoint representatives. No tactics, no lemmas applied, no sorry.
why it matters
Feeds the bridge theorem exact_fourpoint_k4_obstruction_from_support_obstruction, whose doc-comment records that "the support-level K4 obstruction implies the ordered-representative K4 obstruction used by the final assembly." That bridge simply instantiates this Prop and unpacks the two support edges.
Inside the distance-shell multiplicity development, the four-point K4 obstruction is the discrete geometric gate that forces non-star four-point configurations with too many edges to carry a pair of edges with disjoint representatives. That gate is the support-side half of the bookkeeping that converts classical shell-multiplicity constraints (Erdős #132) into RS recognition-energy shell occupancy statements. It does not itself touch the forcing chain T0–T8 or the RCL; it is pure finite planar graph geometry serving the shell-multiplicity pipeline.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.