orient2_zero_transitive_swap
plain-language theorem explainer
If two points lie on the line through a distinct pair, the orientation of that pair against those two points vanishes. Plane-geometry arguments in the distance-shell module cite this when the fixed line is given by the second pair rather than the first. The proof is a one-line reordering of the base orientation-transitivity lemma.
Claim. Let $a,b,c,d\in\mathbb{R}^{2}$ with $c\neq d$. If the planar orientation form satisfies $\mathrm{orient}(c,d,a)=0$ and $\mathrm{orient}(c,d,b)=0$, then $\mathrm{orient}(c,a,b)=0$. Equivalently: if $a$ and $b$ both lie on the line through distinct points $c$ and $d$, then $c,a,b$ are collinear.
background
The module records the Recognition Science physicalization of Erdős problem #132. Classically a distance value is a shell in the pairwise Euclidean spectrum; physically it is a two-body recognition-energy shell whose multiplicity is the shell occupancy. Ordered pairs are used for Lean simplicity, so positive-distance ordered multiplicity is twice the unordered count.
Points are vectors in the Euclidean plane $\mathbb{R}^{2}$ (the bipartite spectrum's Point2). The orientation form is the signed twice-area determinant
$\mathrm{orient}(a,b,c)=(b_{0}-a_{0})(c_{1}-a_{1})-(b_{1}-a_{1})(c_{0}-a_{0})$,
vanishing exactly on collinear triples.
The upstream lemma states that orientation zero is transitive through a fixed line: if $c$ and $d$ both lie on the line through distinct $a,b$, then $a,c,d$ are collinear. The present statement is the symmetric reindexing of that incidence fact.
proof idea
One-line term proof. Apply the base orientation-transitivity lemma with the fixed distinct pair taken to be $(c,d)$ and the two points on that line taken to be $a$ and $b$. The hypotheses $c\neq d$, $\mathrm{orient}(c,d,a)=0$, and $\mathrm{orient}(c,d,b)=0$ match the upstream signature exactly after this argument reorder, so no further algebra or case split is required.
why it matters
Supplies the swapped collinearity transfer used in four-point diameter analysis. The parent result on endpoint-disjoint two-point intersection forcing collinearity invokes it as pure affine incidence: two distinct common points determine a line, so both endpoint-disjoint diameter representatives lie on that same line.
In the RS reading of Erdős #132, shell-multiplicity bounds depend on controlling how many pairs can realize a fixed distance without forcing planar degeneracies. Collinearity certificates of this kind are the geometric bottleneck between sparse shells and the ordered-multiplicity threshold (classical $\le n$ becomes ordered $\le 2n$). The lemma itself is elementary Euclidean incidence; its place in the chain is as a reusable reindexing step inside the diameter-shell uniqueness and flux-bridge arguments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.