Disproof of the Aharoni–Korman conjecture

The Aharoni–Korman conjecture (sometimes called the fishbone conjecture) says that every partial order satisfies at least one of the following:

• It contains an infinite antichain
• It contains a chain C, together with a partition into antichains such that every part meets C.

In November 2024, Hollom disproved this conjecture. In this file, we construct Hollom's counterexample P_5 and show it satisfies neither of the above, and thus disprove the conjecture. See [Hol25] for further details.

We show a number of key properties of P_5:

1. It is a partial order
2. It is countable
3. It has no infinite antichains
4. It is scattered (it does not contain a suborder which is order-isomorphic to ℚ)
5. It does not contain a chain C and a partition into antichains such that every part meets C

Points 1, 3, 5 are sufficient to disprove the conjecture, but we include points 2 and 4 nonetheless as they represent other important properties of the partial order.

The final point is the most involved, so we sketch its proof here.

The proof structure is as follows:

• Begin by defining the type Hollom as a synonym for ℕ³ and giving it the partial order structure as required.
• Define the levels level of the partial order, corresponding to L in the informal proof.
• Show that this partial order has no infinite antichains (Hollom.no_infinite_antichain).
• Given a chain C, show that for infinitely many n, C ∩ level n must be finite (exists_finite_intersection).
• Given a chain C, the existence of a partition with the desired properties is equivalent to the existence of a "spinal map" (exists_partition_iff_nonempty_spinalMap). A spinal map is a function from the partial order to C, which is identity on C and for which each fiber is an antichain.

From this point forward, we assume C is a chain and that we have a spinal map to C, with the aim of reaching a contradiction (as then, no such partition can exist). We may further assume that n ≠ 0 and C ∩ level n is finite.

• Define a subset S of level n, and we will aim to show a contradiction by considering the image of S under the spinal map. By construction, no element of S can be mapped into level n.
• The subset S \ (C ∩ level n) contains some "infinite square", i.e. a set of the form {(x, y, n) | a ≤ x ∧ a ≤ y} for some a (square_subset_S).
• For two points of C in the same level, the intersection of C with the interval between them is exactly the length of a maximal chain between them (card_C_inter_Icc_eq).
• For two points of C in the same level, and two points (a, b, n) and (c, d, n) between them, if a + b = c + d then f (a, b, n) = f (c, d, n) (apply_eq_of_line_eq).
• No element of S \ (C ∩ level n) can be mapped into level (n + 1) (not_S_hits_next). This step vitally uses the previous two facts.
• If all of S \ (C ∩ level n) is mapped into level (n - 1), then we have a contradiction (not_S_mapsTo_previous).
• But as f maps each element of S \ (C ∩ level n) to level (n - 1) ∪ level n ∪ level (n + 1), we have a contradiction (no_spinalMap), and therefore show that no spinal map exists.