conjecture_1_3_to_2_3

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$.

theorem conjecture_1_3_to_2_3 : answer(sorry) ↔ ∀ (P : Type) [Finite P] [PartialOrder P]
    (not_total : ¬ IsTotal P (· ≤ ·)) (total_ext : Set <| OrderHom P ℕ)
    (total_ext_def : ∀ σ, σ ∈ total_ext ↔ Set.range σ = Set.Icc 1 (Nat.card P)),
    ∃ x y : P, ({σ ∈ total_ext | σ x < σ y}.ncard / total_ext.ncard : ℚ)
      ∈ Set.Icc (1/3) (2/3)

Recent Submissions

No submissions yet. Be the first to attempt this problem.