Papers With

← All papers
First page of The Aharoni–Korman conjecture is false

The Aharoni–Korman conjecture is false

Lawrence Hollom

math.CO Nov 25, 2024 · v5
formalization mathlib combinatorics
Read PDF arXiv abstract Code
TL;DR
The key Proposition 2.2 of the counterexample was formally verified in Lean by Bhavik Mehta, with the code available in Mathlib4.
Abstract
A poset $P$ is said to satisfy the finite antichain condition, or FAC, if it has no infinite antichain. It was conjectured by Aharoni and Korman in 1992 that any FAC poset $P$ possesses a chain $C$ and a partition into antichains such that $C$ meets every antichain of the partition. In this work we provide a counterexample to this conjecture, demonstrating that it is false. We also discuss variations of the conjecture which may yet be true.
Problem

Aharoni and Korman conjectured in 1992 that every poset with no infinite antichain has a chain C and a partition into antichains such that C meets every antichain of the partition. The conjecture had resisted many attempts at proof.

Approach

A countable counterexample is built on N×N×N as an infinite non-increasing sequence of levels, each order-isomorphic to ω×ω. Adjacent levels are linked by extra order relations based on min coordinates and coordinate sums. The central Proposition 2.2 shows that no chain in this poset is a spine. Bhavik Mehta formally verified that proposition in Lean, and the code is part of Mathlib4.

Results

The Aharoni–Korman (fishbone) conjecture is false, witnessed by a countable poset of width ℵ0. Open problems are posed: whether finite-width posets have spines, and whether every FAC poset has a strongly maximal chain.