The 1/3--2/3 Poset Conjecture: Proof via Bottleneck Dichotomy and Order Polytope Geometry

We prove the 1/3--2/3 Conjecture (Kislitsyn~1968, Fredman~1976): for every finite partially ordered set that is not a total order, there exist incomparable elements $x, y$ such that the fraction of linear extensions placing $x$ before $y$ lies in $[1/3,\, 2/3]$. The proof proceeds by contradiction. Assuming every incomparable pair is \emph{skewed} (minority fraction $<1/3$), we construct a dominant linear extension via a majority tournament, then analyze its bottleneck positions---where consecutive elements are incomparable. Cases $|S| \leq 3$ are handled by pigeonhole and star-graph shattering. For $|S| \geq 4$, a \emph{four-bottleneck dichotomy} splits the argument into a collision attack (adjacent minority sets overlap) and a crystalline analysis (all adjacent overlaps vanish), the latter further splitting into diamond, N-shape, and full-spacing sub-cases. The modular architecture and structural decomposition of this proof were derived using an experimental proof-engineering framework based on an applied Kuratowski calculus, designed to systematically isolate geometric extremizers. The entire logical structure is formalized in Lean~4 with Mathlib~4 as a modular DAG of four compilation units (\texttt{CombinatorialBasics} $\to$ \texttt{CollisionAttack} $\to$ \texttt{TopologicalEndgame} $\to$ \texttt{Assembly}). The formalization compiles with \textbf{0 sorry markers} and \textbf{0 errors}, conditional on a \textbf{single axiom}---the Stanley Geometric Identity---encoding the volume-extension correspondence of the order polytope~\cite{stanley1986}.