orientation_fiber_at_most_two
plain-language theorem explainer
Any finite set of ordered planar pairs has orientation fibers of size at most two: each undirected edge admits only the two directed lifts (a,b) and (b,a). Discrete geometers and thrackle theorists cite this when converting undirected support bounds into ordered multiplicity bounds. The argument is pure Finset bookkeeping: the fiber sits inside {e0, e0.swap}, so its cardinality is at most two.
Claim. For every finite set $E$ of ordered pairs of planar points, and every undirected edge $u$ in the unordered support of $E$, the filtered subset of ordered pairs in $E$ that map to $u$ has cardinality at most $2$. Equivalently, each unordered pair has at most the two directed representatives $(a,b)$ and $(b,a)$.
background
The module physicalizes Erdős problem #132 inside Recognition Science: a classical distance shell becomes a two-body recognition-energy shell, and shell occupancy is its multiplicity. Lean works with ordered pairs for convenience. For a positive distance the ordered multiplicity is exactly twice the unordered one, so classical thresholds of the form $\le n$ become $\le 2n$.
Point2 is the planar point type imported from the bipartite distance spectrum. The unordered support of a finite ordered edge set $E$ is the image of $E$ under the map that forgets orientation (via Sym2). The predicate OrientationFiberAtMostTwo asserts that every undirected edge $u$ in that support has at most two ordered preimages in $E$. The present theorem discharges that predicate universally, with no geometric hypotheses on $E$.
proof idea
Work classically. Fix an undirected edge $u$ in the unordered support; it is the image of some ordered pair $e_0\in E$. Let $T:={e_0,e_0.\mathrm{swap}}$. Any ordered $e\in E$ with the same unordered image as $e_0$ satisfies $\mathrm{Sym2.mk},e=\mathrm{Sym2.mk},e_0$, hence by the standard Sym2.mk equality criterion equals $e_0$ or its swap, so the fiber is a subset of $T$. Therefore its card is $\le |T|\le 2$ by the elementary two-element Finset bound. No geometry is used.
why it matters
This is the pure bookkeeping step that lets undirected thrackle or Conway support theorems upgrade to ordered multiplicity bounds. Downstream, ordered_thrackle_bound_from_undirected_support_only quotes it directly: "Since orientation fibers are universally bounded by two, the undirected support theorem alone implies the ordered thrackle bound," via $E.\mathrm{card}\le 2\cdot(\mathrm{unorderedEdgeSupport},E).\mathrm{card}$. The same fiber bound feeds diameter_conway_bound_from_support_conway, which specializes the Conway thrackle support bound to diameter shells.
In the module's RS reading of Erdős #132, ordered multiplicity is the physical shell occupancy. Closing the universal fiber bound once, rather than re-proving it at each use site, keeps the ordered/unordered conversion honest and local. It does not itself resolve the thrackle conjecture or the sparse-shell divergence statements; it only supplies the factor-of-two bridge those statements need.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.