OrderedThrackleBound
plain-language theorem explainer
Packages the ordered straight-line thrackle bound as a Prop: for all large n, any ordered edge set on an n-point planar set with no geometrically disjoint pair has size at most 2n. Diameter-shell and Erdős #132 assembly theorems take it as a hypothesis. Pure definition of the asymptotic inequality (factor 2 from ordered-pair normalization).
Claim. The property that eventually as $n\to\infty$, for every finite set $A\subset\mathbb{R}^2$ with $|A|=n$ and every finite set $E$ of ordered pairs from $A$ with distinct endpoints, if no two edges of $E$ have geometrically disjoint closed segments, then $|E|\le 2|A|$.
background
The module physicalizes Erdős problem #132: classical distance shells become two-body recognition-energy shells, with multiplicity as occupancy. Ordered pairs are used for Lean bookkeeping; for a positive distance, ordered multiplicity is twice the unordered count, so classical thresholds $\le n$ become $\le 2n$.
Points live in the Euclidean plane (Point2). Two ordered edges are geometrically disjoint when their closed straight-line segments do not meet; that is the Hopf–Pannwitz thrackle predicate (endpoint-disjointness alone is too strong and would exclude crossing diameter diagonals).
The bound asserts that a thrackle-like ordered edge set on $A$ cannot exceed twice the vertex count, matching the ordered-pair normalization.
proof idea
Definition only: no proof body. The Prop is the filter statement ∀ᶠ n in atTop quantifying over finite point sets $A$ of cardinality $n$ and ordered edge sets $E$ supported on $A$, requiring that absence of geometrically disjoint pairs forces $|E|\le 2|A|$. Downstream lemmas discharge it from undirected thrackle support plus orientation-fiber bounds.
why it matters
Named hypothesis in the Hopf–Pannwitz route to diameter-shell control. diameter_ordered_bound_from_thrackle_components combines it with no-disjoint-diameter-edges to get the ordered diameter multiplicity bound; sparsity and the final erdos132_from_thrackle_and_no_deep_layer assembly inherit that. Companion lemmas ordered_thrackle_bound_from_undirected_support (and the support-only variant) show how undirected thrackle plus orientation bookkeeping imply this Prop. In the RS reading, diameter shells are the extremal two-body recognition shells whose occupancy must stay linear, feeding the physicalized Erdős #132 statement.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.