OrderedOrientationFiberBound
plain-language theorem explainer
Names the asymptotic hypothesis that, for all large finite point sets in the plane, every admissible ordered edge set has orientation fibers of size at most two. Cited by the thrackle-bridge lemmas that convert undirected support into the ordered thrackle bound for the diameter-shell attack on Erdős #132. Pure Prop abbreviation: no proof body beyond the quantified statement.
Claim. The following holds eventually as $n\to\infty$: for every finite point set $A\subset\mathbb{R}^2$ with $|A|=n$ and every finite set $E$ of ordered pairs of distinct points of $A$, each orientation fiber of $E$ has cardinality at most $2$.
background
The module physicalizes Erdős problem #132 inside Recognition Science: a classical distance value is a two-body recognition-energy shell, and shell multiplicity is occupancy. Ordered pairs are used for Lean bookkeeping; for any positive distance the ordered multiplicity is exactly twice the unordered one, so the classical bound $\le n$ becomes $\le 2n$.
An orientation fiber groups ordered edges that share the same geometric orientation data (direction class up to the discrete bookkeeping used by the thrackle bridge). The predicate asserts that those fibers stay size $\le 2$ on the edge sets that appear in the diameter-shell argument.
The surrounding development works with finite point sets Point2, ordered pair events, and ordered distance spectra. This named Prop is an intermediate bridge kept until an unordered-edge API can absorb the same bookkeeping.
proof idea
Definitional Prop, not a proved theorem. The body is a filter statement at atTop: eventually in $n$, every $n$-point finset $A$ and every ordered edge finset $E$ supported on distinct pairs from $A$ satisfies the orientation-fiber bound of size at most two. No tactics or lemmas are applied; downstream theorems take the Prop as a hypothesis and combine it with undirected thrackle support via filter_upwards.
why it matters
Feeds the ordered thrackle bound used by the diameter-shell proof of the ordered Erdős #132 statement. Concretely, ordered_thrackle_bound_from_undirected_support assumes undirected thrackle support together with this orientation bookkeeping and concludes the ordered thrackle bound. The legacy assembly erdos132_from_undirected_thrackle_and_no_deep_layer likewise lists it among its hypotheses (alongside no-disjoint-diameter-edges and no-deep-layer in the low-shell regime).
In the RS reading, controlling ordered multiplicity on distance shells is the combinatorial half of the recognition-energy shell occupancy bound. The doc-comment flags this as a temporary named finite bridge until the preferred unordered edge API expands, so it is scaffolding for API cleanup rather than a deep new geometric fact. It does not itself invoke the forcing chain (T5–T8) or the Recognition Composition Law; those enter only through the broader mass and geometry stack that motivates treating distance shells as recognition energies.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.