theorem
conjecture_1_3_to_2_3 :
(∀ (P : Type) [inst : Finite P] [inst : PartialOrder P],
(¬IsTotal P fun (x1 x2 : P) => x1 ≤ x2) →
∀ (total_ext : Set (P →o ℕ)),
(∀ (σ : P →o ℕ), σ ∈ total_ext ↔ Set.range ⇑σ = Set.Icc 1 (Nat.card P)) →
∃ (x : P) (y : P),
↑{σ : P →o ℕ | σ ∈ total_ext ∧ σ x < σ y}.ncard / ↑total_ext.ncard ∈ Set.Icc (1 / 3) (2 / 3)) ↔ sorry
Does every finite partially ordered set that is not totally ordered contain two elements $x$ and $y$ such that the probability that $x$ appears before $y$ in a random linear extension is between $\frac 1 3$ and $\frac 2 3$?
The set of all total order extensions is represented as order preserving bijections $P$ of $1, ..., n$.