OrientationFiberAtMostTwo
plain-language theorem explainer
The finite orientation-fiber condition: for any finite set E of ordered planar pairs, each undirected edge in the unordered support has at most two directed representatives in E. Cited by anyone bridging ordered shell multiplicity to classical unordered counts in the Erdős #132 physicalization. Pure Prop definition encoding the two-orientation bookkeeping bound.
Claim. For a finite set $E$ of ordered pairs of planar points, every undirected edge $u$ belonging to the unordered support of $E$ satisfies $\#\{e\in E:\,\mathrm{unorder}(e)=u\}\le 2$.
background
The module physicalizes Erdős problem #132: a classical distance value is a shell in the pairwise Euclidean spectrum; in RS it is a two-body recognition-energy shell whose occupancy is the shell multiplicity. Lean works with ordered pairs for simplicity, so for positive distances the ordered multiplicity is exactly twice the unordered one, and classical thresholds $\le n$ become $\le 2n$.
Point2 is the planar point type from the bipartite distance spectrum. The unordered support of an ordered edge set $E$ is the image of $E$ under the forget-orientation map that sends $(a,b)$ to the undirected pair ${a,b}$. The orientation fiber of an undirected edge $u$ is the subset of $E$ that maps to $u$; classically it can contain only the two directed representatives $(a,b)$ and $(b,a)$.
This definition isolates that fiber-size bound as a named hypothesis so later theorems can assume it without committing yet to a preferred Sym2 API for unordered edges.
proof idea
Definitional Prop, not a proved theorem. The body is the universal quantification over the unordered support: for each undirected $u$, the cardinality of the filter of ordered edges in $E$ that forget to $u$ is at most two. No tactics or lemmas are applied; the companion theorem orientation_fiber_at_most_two later discharges the Prop for every finite $E$ by a classical filter-and-image argument.
why it matters
Bookkeeping hinge between ordered Lean edge sets and classical unordered multiplicity in the RS reading of Erdős #132. Downstream, ordered_card_le_two_mul_unordered_support takes this Prop as hypothesis and concludes $|E|\le 2\cdot|\mathrm{unorderedSupport}(E)|$. The asymptotic package OrderedOrientationFiberBound packages the same fiber bound for edge sets relevant to the thrackle bridge, kept as a named finite bridge until the unordered-edge API expands. The companion theorem orientation_fiber_at_most_two proves the Prop holds universally: an unordered pair has at most the two directed representatives $(a,b)$ and $(b,a)$. Without this separation, ordered-to-unordered shell comparisons would re-inline the same filter cardinality argument at every use site.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.