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 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| 3 are handled by pigeonhole and star-graph shattering. For |S| 4, a 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 (CombinatorialBasics CollisionAttack TopologicalEndgame Assembly). The formalization compiles with 0 sorry markers and 0 errors, conditional on a single axiom---the Stanley Geometric Identity---encoding the volume-extension correspondence of the order polytope~stanley1986.