orient2_zero_of_quadruple_zero
plain-language theorem explainer
If the four canonical orientation determinants on a labeled quadruple vanish, every triple drawn from those four points is collinear. Discrete geometers and anyone closing the noncollinear Conway–thrackle K4 bound cite it. The proof expands the four zeros to all 24 ordered triples by swap/cyclic identities, then finishes by exhaustive case split on membership.
Claim. Let $a,b,c,d\in\mathbb{R}^2$. Suppose the four orientation determinants $\mathrm{orient}(a,b,c)$, $\mathrm{orient}(a,b,d)$, $\mathrm{orient}(a,c,d)$, and $\mathrm{orient}(b,c,d)$ all vanish. Then for every $p,q,r\in\{a,b,c,d\}$ one has $\mathrm{orient}(p,q,r)=0$.
background
The module physicalizes Erdős problem #132: classical distance shells become two-body recognition-energy shells, with ordered multiplicity twice the unordered count. Points live in the visible plane Point2 $\simeq \mathbb{R}^2$.
The signed orientation orient2 a b c is the twice-area determinant $(b_x-a_x)(c_y-a_y)-(b_y-a_y)(c_x-a_x)$. It vanishes precisely when $a,b,c$ are collinear (or coincident). Cyclic permutations preserve the sign (orient2_cyclic, orient2_cyclic'); pairwise swaps negate it.
Downstream noncollinearity is stated as “not every triple from a four-point set has vanishing orientation.” The four canonical triples on a labeled quadruple are a convenient generating set; this lemma shows that vanishing on those four forces vanishing on every ordered triple from the set.
proof idea
First close under the orientation algebra: from the four given zeros, apply orient2_swap₁₂, orient2_swap₂₃, orient2_swap₁₃, orient2_cyclic, and orient2_cyclic' (each followed by linarith) to obtain zeros for every distinct ordered triple among ${a,b,c,d}$.
Then rcases on the three membership hypotheses for $p,q,r$ (four alternatives each) and subst_vars. In every goal, either the triple matches one of the precomputed zeros, or two of $p,q,r$ coincide, in which case orient2_eq_zero_of_two_eq_first/second/third finishes. The all_goals first | ... block is pure case dispatch.
why it matters
This is the bridge named in the doc-comment: it converts the compact four-orient form of collinearity into the universal quantifier “every triple from $A$ is collinear.” The sole downstream consumer is exact_fourpoint_conway_thrackle_support_bound_noncollinear_thm, the unconditional noncollinear Conway-conditioned $K_4$ support bound, which combines the six-pair subset inclusion with the conditional thrackle bound.
That $K_4$ bound is a discrete-geometry step inside the distance-shell multiplicity program (Erdős #132 physicalized as recognition-energy shell occupancy). Without the bridge, the noncollinear hypothesis on a four-point ambient set cannot be fed into the conditional Conway argument. No forcing-chain landmark (T5–T8) is touched directly; the lemma is pure planar combinatorial geometry supporting the shell-multiplicity side of the monolith.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.