orient2
plain-language theorem explainer
Signed twice-area of the triangle formed by three points in the Euclidean plane, equivalently the 2D cross product of the edge vectors from the first vertex. Downstream collinearity, segment-separation, and thrackle arguments in the distance-shell multiplicity development cite it as the basic orientation test. The body is the explicit determinant formula; no proof content.
Claim. For $a,b,c\in\mathbb{R}^2$, define $\mathrm{orient}_2(a,b,c):=(b_0-a_0)(c_1-a_1)-(b_1-a_1)(c_0-a_0)$. This is the signed twice-area of triangle $abc$ (positive for counterclockwise order, zero on a line, negative for clockwise).
background
The ambient module physicalizes Erdős problem #132 inside Recognition Science: classical pairwise distance values become two-body recognition-energy shells, and shell multiplicity is occupancy. Points live in the visible plane Point2, an abbreviation for the Euclidean space $\mathbb{R}^2$.
The orientation form is the standard planar determinant. Vanishing detects collinearity of three points; the sign separates half-planes. Downstream certificates such as collinear segment separation explicitly require both orient2 a b c = 0 and orient2 a b d = 0 together with geometric disjointness of the closed segments.
Ordered pairs are used for Lean bookkeeping: for a positive distance, ordered multiplicity is twice the unordered count, so classical thresholds scale by two.
proof idea
Pure definition: expand the 2-by-2 determinant of the vectors $b-a$ and $c-a$ in coordinates. No lemmas are applied; the value is the real number $(b_0-a_0)(c_1-a_1)-(b_1-a_1)(c_0-a_0)$. Noncomputable only because the ambient Euclidean space is noncomputable.
why it matters
This is the local geometric primitive for the entire distance-shell multiplicity stack. Collinear segment separation is defined by simultaneous vanishing of two orientations plus ordered-edge disjointness. Endpoint-disjoint two-point intersection forces collinearity by showing both diameter representatives share a line via orientation zero on closed segments. Collinear diameter-endpoint contradictions, the collinear four-point Conway residual, and the exact four-point Conway thrackle support bounds all route through the same test when the algebraic dichotomy degenerates to a line.
In the RS reading of Erdős #132, diameter shells and sparse shells are recognition-energy shells; orientation supplies the planar incidence language that separates collinear residual geometry from the noncollinear case that closes immediately. It does not itself invoke the forcing chain (T5–T8) or the J-cost, but it underwrites the combinatorial geometry those physical claims rest on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.