The 1/3–2/3 Poset Conjecture — Lean 4 Formalization

The Result

A Lean 4 / Mathlib formalization of the Causal Flow framework for the 1/3–2/3 Conjecture (Kislitsyn 1968, Fredman 1976, Linial 1984).

Main Result (Corollary in paper, sorry-free in Lean). The 1/3–2/3 Conjecture holds for every finite poset whose dominant linear extension has at most three disjoint adjacent bottleneck pairs — a structural class defined for all n:

$$3 \cdot \min(c(x,y),; k - c(x,y)) ;\ge; k$$

for some incomparable pair (x, y), where k = |L(P)| and c(x,y) counts extensions with x before y.

This reduces the full conjecture to a single explicit obstruction: posets admitting four or more disjoint bottleneck pairs in their dominant extension.

The Causal Flow Partition

The proof introduces a new decomposition of linear extensions for any incomparable pair (a, b):

1. Partition: k = 2A + N — every extension is adjacent or non-adjacent
2. Adjacency Involution: |A⁺| = |A⁻| — swap at distance 1 is a bijection
3. Flexible Buffer Involution: |F⁺| = |F⁻| — position-swap for all-incomparable buffers
4. Skewness Equation: c(a,b) − c(b,a) = R⁺ − R⁻ — all skewness comes from rigid buffers

Rigid Necessity: Under AllSkewed, every incomparable pair has a comparability witness — an element comparable to exactly one endpoint.

See docs/proof_overview.pdf for the full paper.

Status

Metric	Value
Sorry count (main path)	1 (allskewed_k_ge10_false — the
Sorry count (off-path)	2 (SmallCases: n = 6, 7 native_decide timeouts)
**Main result (	S
Lean errors	0

Sorry Inventory

Sorry	File	On main path?	Description
allskewed_k_ge10_false	BackboneDichotomy.lean:523	Yes	AllSkewed + k ≥ 10 → False (handles
poset6_one_third_two_thirds	SmallCases.lean:299	No	native_decide valid (~30 min); verified by Rust
poset7_one_third_two_thirds	SmallCases.lean:359	No	native_decide OOMs (>32 GB); verified by Rust

Proved sorry-free (key lemmas)

• adj_involution_card (Defs.lean): |A⁺| = |A⁻| for any incomparable pair
• flexible_buffer_involution_card (BackboneDichotomy.lean): |F⁺| = |F⁻|
• skewness_eq_rigid_diff (BackboneDichotomy.lean): c(a,b) − c(b,a) = R⁺ − R⁻
• rigid_nonempty_of_allskewed (BackboneDichotomy.lean): AllSkewed → rigid buffers exist
• pigeonhole_two_bottlenecks (CombinatorialBasics.lean): |S| ≤ 2 → False (all n)
• star_graph_shattered (CombinatorialBasics.lean): |S| = 3 → False (all n)
• core_extraction (CombinatorialBasics.lean): AllSkewed preserves under restriction to all-active core

Module DAG

SmallCases ──→ CombinatorialBasics ──→ Defs ──→ BackboneDichotomy
                      │                                  │
                      ↓                                  ↓
              CollisionAttack*         TopologicalEndgame ──→ Assembly

* CollisionAttack contains dead code (geometric |S| ≥ 4 analysis, superseded by algebraic bypass). Not on the main proof path.

File Hierarchy

Math/
  Kislitsyn.lean                ← barrel import
  Kislitsyn/
    SmallCases.lean              ← Poset3–5 native_decide (sorry-free); n=6,7 sorry'd
    CombinatorialBasics.lean     ← FinPoset API, majority tournament, core extraction
    CollisionAttack.lean         ← geometric |S|≥4 cases (DEAD CODE, not on main path)
    Defs.lean                    ← Buffer API: adjacency, buffers, skewness
    BackboneDichotomy.lean       ← flex/rigid involution, Rigid Necessity (1 sorry)
    TopologicalEndgame.lean      ← bottleneck case router
    Assembly.lean                ← main theorem: kislitsyn_fredman
    FEATURE_DICTIONARY.lean      ← architecture documentation
    docs/
      proof_overview.pdf         ← the paper
      proof_overview.tex         ← paper source
lakefile.toml                    ← build config (Mathlib v4.28.0)

Build Instructions

Requires Lean 4 + Mathlib v4.28.0. From the repository root:

# First time: fetch Mathlib cache
lake exe cache get

# Build the main theorem
lake build Math.Kislitsyn.Assembly

The build will succeed with one warning (declaration uses sorry) for allskewed_k_ge10_false.

References

• Kislitsyn (1968). Finite partially ordered sets and their associated sets of permutations.
• Fredman (1976). How good is the information theory bound in sorting?
• Linial (1984). The information-theoretic bound is good for merging.
• Kahn & Saks (1984). Balancing poset extensions.
• Brightwell, Felsner & Trotter (1995). Balancing pairs and the cross product conjecture.
• Peczarski (2006). The gold partition conjecture.

License

This formalization is released for academic review.