orient2_swap

The module physicalizes Erdős problem #132: classical distance shells become two-body recognition-energy shells, with multiplicity as shell occupancy. Ordered pairs are used for Lean simplicity; for a positive distance, ordered multiplicity is twice the unordered count, so the classical bound $\le n$ becomes $\le 2n$.

Point2 is the planar point type imported from the bipartite distance spectrum layer. The orientation form orient2 is the standard signed area (twice the oriented triangle area, equivalently the 2D cross product of edge vectors from the first point). It is alternating under odd permutations of its arguments; this lemma records the transposition of the first two slots.

One-step algebraic proof: unfold the definition of the orientation form, then apply ring to cancel the resulting bilinear polynomial identity. No external lemmas are required.

Orientation antisymmetry is bookkeeping infrastructure for ordered-pair geometry in the distance-shell multiplicity development. Sibling swap lemmas (last two arguments; first and last) and the cyclic-invariance statement sit beside it, so signed-area identities can be rewritten without casework when counting ordered shells or diameter shells.

In the Recognition Science framing, distance shells are recognition-energy shells whose multiplicities feed sparse-shell and flux-bridge arguments tied to Erdős #132. This lemma does not itself touch the forcing chain (T0–T8) or the J-cost; it keeps planar combinatorial geometry clean so those physicalization steps can quote orientation signs safely. No downstream edges are recorded yet; the immediate consumers are the other orientation identities and any later uniqueness or diameter-shell arguments that rearrange vertices.