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)​\ (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.

structure Hollom : Type

A type synonym on ℕ³ on which we will construct Hollom's partial order P_5.

• toHollom :: (
• ofHollom : ℕ × ℕ × ℕ

  The backward equivalence between ℕ³ and the underlying set in Hollom's partial order. Note that this equivalence does not respect the partial order relation.

• )

theorem Hollom.ext {x y : Hollom} (ofHollom : x.ofHollom = y.ofHollom) : x = y

instance instDecidableEqHollom : DecidableEq Hollom

Equations

• instDecidableEqHollom = decEqHollom✝

@[simp]

theorem ofHollom_toHollom (x : ℕ × ℕ × ℕ) : { ofHollom := x }.ofHollom = x

@[simp]

theorem toHollom_ofHollom (x : Hollom) : { ofHollom := x.ofHollom } = x

def equivHollom : ℕ × ℕ × ℕ ≃ Hollom

toHollom and ofHollom as an equivalence.

Equations

• equivHollom = { toFun := Hollom.toHollom, invFun := Hollom.ofHollom, left_inv := equivHollom.proof_1, right_inv := equivHollom.proof_2 }

@[simp]

theorem equivHollom_symm_apply (self : Hollom) : equivHollom.symm self = self.ofHollom

@[simp]

theorem equivHollom_apply_ofHollom (ofHollom : ℕ × ℕ × ℕ) : (equivHollom ofHollom).ofHollom = ofHollom

@[simp]

theorem Hollom.forall {p : Hollom → Prop} : (∀ (x : Hollom), p x) ↔ ∀ (x : ℕ × ℕ × ℕ), p { ofHollom := x }

@[simp]

theorem Hollom.forall₂ {p : Hollom → Hollom → Prop} : (∀ (x y : Hollom), p x y) ↔ ∀ (x y : ℕ × ℕ × ℕ), p { ofHollom := x } { ofHollom := y }

@[simp]

theorem Hollom.forall₃ {p : Hollom → Hollom → Hollom → Prop} : (∀ (x y z : Hollom), p x y z) ↔ ∀ (x y z : ℕ × ℕ × ℕ), p { ofHollom := x } { ofHollom := y } { ofHollom := z }

@[simp]

theorem Hollom.exists {p : Hollom → Prop} : (∃ (x : Hollom), p x) ↔ ∃ (x : ℕ × ℕ × ℕ), p { ofHollom := x }

theorem Hollom.induction {p : Hollom → Prop} (h : ∀ (x y z : ℕ), p { ofHollom := (x, y, z) }) (x : Hollom) : p x

instance Hollom.instCountable : Countable Hollom

The Hollom partial order is countable. This is very easy to see, since it is just ℕ³ with a different order.

inductive Hollom.HollomOrder : ℕ × ℕ × ℕ → ℕ × ℕ × ℕ → Prop

The ordering on ℕ³ which is used to define Hollom's example P₅

• twice {x y n u v m : ℕ} : m + 2 ≤ n → HollomOrder (x, y, n) (u, v, m)
• within {x y u v m : ℕ} : x ≤ u → y ≤ v → HollomOrder (x, y, m) (u, v, m)
• next_min {x y u v m : ℕ} : x ⊓ y + 1 ≤ u ⊓ v → HollomOrder (x, y, m + 1) (u, v, m)
• next_add {x y u v m : ℕ} : x + y ≤ 2 * (u + v) → HollomOrder (x, y, m + 1) (u, v, m)

theorem Hollom.hollomOrder_iff (a✝ a✝¹ : ℕ × ℕ × ℕ) : HollomOrder a✝ a✝¹ ↔ (∃ (x : ℕ) (y : ℕ) (n : ℕ) (u : ℕ) (v : ℕ) (m : ℕ), m + 2 ≤ n ∧ a✝ = (x, y, n) ∧ a✝¹ = (u, v, m)) ∨ (∃ (x : ℕ) (y : ℕ) (u : ℕ) (v : ℕ) (m : ℕ), x ≤ u ∧ y ≤ v ∧ a✝ = (x, y, m) ∧ a✝¹ = (u, v, m)) ∨ (∃ (x : ℕ) (y : ℕ) (u : ℕ) (v : ℕ) (m : ℕ), x ⊓ y + 1 ≤ u ⊓ v ∧ a✝ = (x, y, m + 1) ∧ a✝¹ = (u, v, m)) ∨ ∃ (x : ℕ) (y : ℕ) (u : ℕ) (v : ℕ) (m : ℕ), x + y ≤ 2 * (u + v) ∧ a✝ = (x, y, m + 1) ∧ a✝¹ = (u, v, m)

theorem Hollom.HollomOrder.trans (x y z : ℕ × ℕ × ℕ) (h₁ : HollomOrder x y) (h₂ : HollomOrder y z) : HollomOrder x z

Transitivity of the hollom order. This needs to be split out from the instance otherwise it's painfully slow to compile.

instance Hollom.instPartialOrder : PartialOrder Hollom

Equations

• Hollom.instPartialOrder = PartialOrder.mk Hollom.instPartialOrder.proof_4

@[simp]

theorem Hollom.toHollom_le_toHollom_iff_fixed_right {a b c d n : ℕ} : { ofHollom := (a, b, n) } ≤ { ofHollom := (c, d, n) } ↔ a ≤ c ∧ b ≤ d

theorem Hollom.le_of_toHollom_le_toHollom {a b c d e f : ℕ} : { ofHollom := (a, b, c) } ≤ { ofHollom := (d, e, f) } → f ≤ c

theorem Hollom.toHollom_le_toHollom {a b c d e f : ℕ} (h : (a, b) ≤ (d, e)) (hcf : f ≤ c) : { ofHollom := (a, b, c) } ≤ { ofHollom := (d, e, f) }

def Hollom.level (n : ℕ) : Set Hollom

The Hollom partial order is divided into "levels", indexed by the natural numbers. These correspond to the third coordinate of the tuple. This is written $L_n$ in the [Hol25].

Equations

• Hollom.level n = {x : Hollom | ∃ (x_1 : ℕ) (y : ℕ), { ofHollom := (x_1, y, n) } = x}

theorem Hollom.level_eq (n : ℕ) : level n = {x : Hollom | x.ofHollom.2.2 = n}

@[simp]

theorem Hollom.toHollom_mem_level_iff {n : ℕ} {x : ℕ × ℕ × ℕ} : { ofHollom := x } ∈ level n ↔ x.2.2 = n

theorem Hollom.induction_on_level {n : ℕ} {p : (x : Hollom) → x ∈ level n → Prop} (h : ∀ (x y : ℕ), p { ofHollom := (x, y, n) } ⋯) {x : Hollom} (h✝ : x ∈ level n) : p x h✝

def Hollom.embed (n : ℕ) : ℕ × ℕ ↪o Hollom

For each n, there is an order embedding from ℕ × ℕ (which has the product order) to the Hollom partial order.

Equations

• Hollom.embed n = { toFun := fun (x : ℕ × ℕ) => { ofHollom := (x.1, x.2, n) }, inj' := ⋯, map_rel_iff' := ⋯ }

theorem Hollom.embed_apply (n x y : ℕ) : (embed n) (x, y) = { ofHollom := (x, y, n) }

theorem Hollom.embed_strictMono {n : ℕ} : StrictMono ⇑(embed n)

theorem Hollom.level_eq_range (n : ℕ) : level n = Set.range ⇑(embed n)

theorem Hollom.level_isPWO {n : ℕ} : (level n).IsPWO

theorem Hollom.no_infinite_antichain_level {n : ℕ} {A : Set Hollom} (hA : A ⊆ level n) (hA' : IsAntichain (fun (x1 x2 : Hollom) => x1 ≤ x2) A) : A.Finite

If A is a subset of level n and is an antichain, then A is finite. This is a special case of the fact that any antichain in the Hollom order is finite, but is a useful lemma to prove that fact later: no_infinite_antichain.

theorem Hollom.ordConnected_level {n : ℕ} : (level n).OrdConnected

Each level is order-connected, i.e. for any x ∈ level n and y ∈ level n we have [x, y] ⊆ level n. This corresponds to 5.8 (i) in the [Hol25].

def Hollom.line (x : Hollom) : ℕ

The map from (x, y, n) to x + y.

Equations

• Hollom.line x = x.ofHollom.1 + x.ofHollom.2.1

@[simp]

theorem Hollom.line_toHollom (x : ℕ × ℕ × ℕ) : line { ofHollom := x } = x.1 + x.2.1

theorem Hollom.line_injOn {C : Set Hollom} (n : ℕ) (hC : IsChain (fun (x1 x2 : Hollom) => x1 ≤ x2) C) (hCn : C ⊆ level n) : Set.InjOn line C

theorem Hollom.add_lt_add_of_lt {a b c d n : ℕ} (h : { ofHollom := (a, b, n) } < { ofHollom := (c, d, n) }) : a + b < c + d

theorem Hollom.line_mapsTo {x y : Hollom} (hxy : x.ofHollom.2.2 = y.ofHollom.2.2) : Set.MapsTo line (Set.Icc x y) (Set.Icc (line x) (line y))

theorem Hollom.embed_image_Icc {a b c d n : ℕ} : ⇑(embed n) '' Set.Icc (a, b) (c, d) = Set.Icc { ofHollom := (a, b, n) } { ofHollom := (c, d, n) }

theorem Hollom.scattered {f : ℚ → Hollom} (hf : StrictMono f) : False

The Hollom partial order is scattered: it does not contain a suborder which is order-isomorphic to ℚ. We state this as saying there is no strictly monotone function from ℚ to Hollom.

theorem Hollom.no_infinite_antichain {A : Set Hollom} (hC : IsAntichain (fun (x1 x2 : Hollom) => x1 ≤ x2) A) : A.Finite

Any antichain in the Hollom partial order is finite. This corresponds to Lemma 5.9 in [Hol25].

theorem Hollom.exists_finite_intersection {C : Set Hollom} (hC : IsChain (fun (x1 x2 : Hollom) => x1 ≤ x2) C) : ∃ᶠ (n : ℕ) in Filter.atTop, (C ∩ level n).Finite

Show that every chain in the Hollom partial order has a finite intersection with infinitely many levels. This corresponds to Lemma 5.10 from [Hol25].

In this section we define spinal maps, and prove important properties about them.

structure Hollom.SpinalMap {α : Type u_1} [PartialOrder α] (C : Set α) : Type u_1

A spinal map is a function f : α → C which is the identity on C, and for which each fiber is an antichain. Provided C is a chain, the existence of a spinal map is equivalent to the fact that C is a spine.

• toFun : α → α

  The underlying function of a spinal map.

• mem' (x : α) : self.toFun x ∈ C
• eq_self_of_mem' (x : α) : x ∈ C → self.toFun x = x
• fibre_antichain' (x : α) : IsAntichain (fun (x1 x2 : α) => x1 ≤ x2) (self.toFun ⁻¹' {x})

instance Hollom.instFunLikeSpinalMap {α : Type u_1} [PartialOrder α] {C : Set α} : FunLike (SpinalMap C) α α

Equations

• Hollom.instFunLikeSpinalMap = { coe := Hollom.SpinalMap.toFun, coe_injective' := ⋯ }

Basic lemmas for spinal maps

theorem Hollom.SpinalMap.ext {α : Type u_1} [PartialOrder α] {C : Set α} {f g : SpinalMap C} (h : ∀ (x : α), f x = g x) : f = g

@[simp]

theorem Hollom.SpinalMap.toFun_eq_coe {α : Type u_1} [PartialOrder α] {C : Set α} (f : SpinalMap C) : f.toFun = ⇑f

@[simp]

theorem Hollom.SpinalMap.mem {α : Type u_1} [PartialOrder α] {C : Set α} (f : SpinalMap C) (x : α) : f x ∈ C

theorem Hollom.SpinalMap.eq_self_of_mem {α : Type u_1} [PartialOrder α] {C : Set α} (f : SpinalMap C) {x : α} (hx : x ∈ C) : f x = x

theorem Hollom.SpinalMap.fibre_antichain {α : Type u_1} [PartialOrder α] {C : Set α} (f : SpinalMap C) (x : α) : IsAntichain (fun (x1 x2 : α) => x1 ≤ x2) (⇑f ⁻¹' {x})

theorem Hollom.SpinalMap.range_subset {α : Type u_1} [PartialOrder α] {C : Set α} (f : SpinalMap C) : Set.range ⇑f ⊆ C

@[simp]

theorem Hollom.SpinalMap.idempotent {α : Type u_1} [PartialOrder α] {C : Set α} (f : SpinalMap C) (x : α) : f (f x) = f x

theorem Hollom.SpinalMap.not_le_of_eq {α : Type u_1} [PartialOrder α] {C : Set α} (f : SpinalMap C) {x y : α} (hfxy : f x = f y) (hxy : x ≠ y) : ¬x ≤ y

theorem Hollom.SpinalMap.eq_of_le {α : Type u_1} [PartialOrder α] {C : Set α} (f : SpinalMap C) {x y : α} (hfxy : f x = f y) (hxy : x ≤ y) : x = y

theorem Hollom.SpinalMap.not_lt_of_eq {α : Type u_1} [PartialOrder α] {C : Set α} (f : SpinalMap C) {x y : α} (hfxy : f x = f y) : ¬x < y

theorem Hollom.SpinalMap.incomp_of_eq {α : Type u_1} [PartialOrder α] {C : Set α} (f : SpinalMap C) {x y : α} (hfxy : f x = f y) (hxy : x ≠ y) : ¬(x ≤ y ∨ y ≤ x)

theorem Hollom.SpinalMap.incomp_apply {α : Type u_1} [PartialOrder α] {C : Set α} (f : SpinalMap C) {x : α} (hx : f x ≠ x) : ¬(f x ≤ x ∨ x ≤ f x)

theorem Hollom.SpinalMap.not_apply_lt {α : Type u_1} [PartialOrder α] {C : Set α} (f : SpinalMap C) {x : α} : ¬f x < x

theorem Hollom.SpinalMap.not_lt_apply {α : Type u_1} [PartialOrder α] {C : Set α} (f : SpinalMap C) {x : α} : ¬x < f x

theorem Hollom.SpinalMap.le_apply_of_le {α : Type u_1} [PartialOrder α] {C : Set α} (f : SpinalMap C) {x y : α} (hC : IsChain (fun (x1 x2 : α) => x1 ≤ x2) C) (hy : y ∈ C) (hx : y ≤ x) : y ≤ f x

theorem Hollom.SpinalMap.apply_le_of_le {α : Type u_1} [PartialOrder α] {C : Set α} (f : SpinalMap C) {x y : α} (hC : IsChain (fun (x1 x2 : α) => x1 ≤ x2) C) (hy : y ∈ C) (hx : x ≤ y) : f x ≤ y

theorem Hollom.SpinalMap.lt_apply_of_lt {α : Type u_1} [PartialOrder α] {C : Set α} (f : SpinalMap C) {x y : α} (hC : IsChain (fun (x1 x2 : α) => x1 ≤ x2) C) (hy : y ∈ C) (hx : y < x) : y < f x

theorem Hollom.SpinalMap.apply_lt_of_lt {α : Type u_1} [PartialOrder α] {C : Set α} (f : SpinalMap C) {x y : α} (hC : IsChain (fun (x1 x2 : α) => x1 ≤ x2) C) (hy : y ∈ C) (hx : x < y) : f x < y

theorem Hollom.SpinalMap.apply_mem_Icc_of_mem_Icc {α : Type u_1} [PartialOrder α] {C : Set α} (f : SpinalMap C) {x y z : α} (hC : IsChain (fun (x1 x2 : α) => x1 ≤ x2) C) (hy : y ∈ C) (hz : z ∈ C) (hx : x ∈ Set.Icc y z) : f x ∈ Set.Icc y z

theorem Hollom.SpinalMap.mapsTo_Icc_self {α : Type u_1} [PartialOrder α] {C : Set α} (f : SpinalMap C) {y z : α} (hC : IsChain (fun (x1 x2 : α) => x1 ≤ x2) C) (hy : y ∈ C) (hz : z ∈ C) : Set.MapsTo (⇑f) (Set.Icc y z) (Set.Icc y z)

theorem Hollom.SpinalMap.injOn_of_isChain {α : Type u_1} [PartialOrder α] {C : Set α} (f : SpinalMap C) {D : Set α} (hD : IsChain (fun (x1 x2 : α) => x1 ≤ x2) D) : Set.InjOn (⇑f) D

theorem Hollom.exists_partition_iff_nonempty_spinalMap {α : Type u_1} [PartialOrder α] {C : Set α} (hC : IsChain (fun (x1 x2 : α) => x1 ≤ x2) C) : (∃ (S : Set (Set α)), Setoid.IsPartition S ∧ ∀ A ∈ S, IsAntichain (fun (x1 x2 : α) => x1 ≤ x2) A ∧ (A ∩ C).Nonempty) ↔ Nonempty (SpinalMap C)

Given a chain C in a partial order α, the existence of the following are equivalent:

• a partition of α into antichains, each which meets C
• a function f : α → C which is the identity on C and for which each fiber is an antichain

In fact, these two are in bijection, but we only need the weaker version that their existence is equivalent.

Explicit chains

In this section we construct an explicit chain in ℕ × ℕ that will be useful later. These comprise part of 5.8(iv) from [Hol25]: the full strength of that observation is not actually needed.

def Hollom.chainBetween (a b c d : ℕ) : Finset (ℕ × ℕ)

An explicit contiguous chain between (a, b) and (c, d) in ℕ × ℕ. We implement this as the union of two disjoint sets: the first is the chain from (a, b) to (a, d), and the second is the chain from (a, d) to (c, d).

Equations

• Hollom.chainBetween a b c d = if a ≤ c ∧ b ≤ d then Finset.Ico (a, b) (a, d) ∪ Finset.Icc (a, d) (c, d) else ∅

theorem Hollom.chainBetween_isChain {a b c d : ℕ} : IsChain (fun (x1 x2 : ℕ × ℕ) => x1 ≤ x2) ↑(chainBetween a b c d)

theorem Hollom.image_chainBetween_isChain {a b c d n : ℕ} : IsChain (fun (x1 x2 : Hollom) => x1 ≤ x2) ↑(Finset.image (⇑(embed n)) (chainBetween a b c d))

theorem Hollom.card_chainBetween {a b c d : ℕ} (hac : a ≤ c) (hbd : b ≤ d) : (chainBetween a b c d).card = c + d + 1 - (a + b)

theorem Hollom.chainBetween_subset {a b c d : ℕ} : chainBetween a b c d ⊆ Finset.Icc (a, b) (c, d)

theorem Hollom.mapsTo_Icc_image {C : Set Hollom} {f : SpinalMap C} (hC : IsChain (fun (x1 x2 : Hollom) => x1 ≤ x2) C) {a b c d n : ℕ} (hab : { ofHollom := (a, b, n) } ∈ C) (hcd : { ofHollom := (c, d, n) } ∈ C) : Set.MapsTo ⇑f ↑(Finset.image (⇑(embed n)) (Finset.Icc (a, b) (c, d))) ↑(Finset.image (⇑(embed n)) (Finset.Icc (a, b) (c, d)))

theorem Hollom.C_inter_Icc_large {C : Set Hollom} (f : SpinalMap C) {n xl yl xh yh : ℕ} (hC : IsChain (fun (x1 x2 : Hollom) => x1 ≤ x2) C) (hx : xl ≤ xh) (hy : yl ≤ yh) (hlo : { ofHollom := (xl, yl, n) } ∈ C) (hhi : { ofHollom := (xh, yh, n) } ∈ C) : xh + yh + 1 - (xl + yl) ≤ {x ∈ Finset.image (⇑(embed n)) (Finset.Icc (xl, yl) (xh, yh)) | x ∈ C}.card

The collection of points between (xl, yl, n) and (xh, yh, n) that are also in C has at least xh + yh + 1 - (xl + yl) elements. In other words, this collection must be a maximal chain relative to the interval it is contained in. Note card_C_inter_Icc_eq strengthens this to an equality.

theorem Hollom.card_C_inter_Icc_eq {C : Set Hollom} (f : SpinalMap C) {n xl yl xh yh : ℕ} (hC : IsChain (fun (x1 x2 : Hollom) => x1 ≤ x2) C) (hx : xl ≤ xh) (hy : yl ≤ yh) (hlo : { ofHollom := (xl, yl, n) } ∈ C) (hhi : { ofHollom := (xh, yh, n) } ∈ C) : {x ∈ Finset.image (⇑(embed n)) (Finset.Icc (xl, yl) (xh, yh)) | x ∈ C}.card = xh + yh + 1 - (xl + yl)

The collection of points between (xl, yl, n) and (xh, yh, n) that are also in C has exactly xh + yh + 1 - (xl + yl) elements. In other words, this collection must be a maximal chain relative to the interval it is contained in. Alternatively speaking, it has the same size as any maximal chain in that interval.

theorem Hollom.apply_eq_of_line_eq_step {C : Set Hollom} (f : SpinalMap C) {n xl yl xh yh : ℕ} (hC : IsChain (fun (x1 x2 : Hollom) => x1 ≤ x2) C) (hlo : { ofHollom := (xl, yl, n) } ∈ C) (hhi : { ofHollom := (xh, yh, n) } ∈ C) (hx : xl ≤ xh) (hy : yl ≤ yh) {x y : ℕ} (h₁l : { ofHollom := (xl, yl, n) } ≤ { ofHollom := (x + 1, y, n) }) (h₂l : { ofHollom := (xl, yl, n) } ≤ { ofHollom := (x, y + 1, n) }) (h₁h : { ofHollom := (x + 1, y, n) } ≤ { ofHollom := (xh, yh, n) }) (h₂h : { ofHollom := (x, y + 1, n) } ≤ { ofHollom := (xh, yh, n) }) : f { ofHollom := (x + 1, y, n) } = f { ofHollom := (x, y + 1, n) }

The important helper lemma to prove apply_eq_of_line_eq. That lemma says that given (xl, yl, n) and (xh, yh, n) in a chain C, and two points (a, b, n) and (c, d, n) between them, if a + b = c + d then a spinal map f : SpinalMap C sends them to the same place. Here we show the special case where the two points are (x + 1, y, n) and (x, y + 1, n), i.e. they are beside each other.

theorem Hollom.apply_eq_of_line_eq_aux {C : Set Hollom} (f : SpinalMap C) {n xl yl xh yh : ℕ} (hC : IsChain (fun (x1 x2 : Hollom) => x1 ≤ x2) C) (hlo : { ofHollom := (xl, yl, n) } ∈ C) (hhi : { ofHollom := (xh, yh, n) } ∈ C) (hx : xl ≤ xh) (hy : yl ≤ yh) {x y k : ℕ} (h₁l : { ofHollom := (xl, yl, n) } ≤ { ofHollom := (x + k, y, n) }) (h₂l : { ofHollom := (xl, yl, n) } ≤ { ofHollom := (x, y + k, n) }) (h₁h : { ofHollom := (x + k, y, n) } ≤ { ofHollom := (xh, yh, n) }) (h₂h : { ofHollom := (x, y + k, n) } ≤ { ofHollom := (xh, yh, n) }) : f { ofHollom := (x + k, y, n) } = f { ofHollom := (x, y + k, n) }

A simple helper lemma to prove apply_eq_of_line_eq. Here we show the special case where the two points are (x + k, y, n) and (x, y + k, n) by induction on k with apply_eq_of_line_eq_step.

theorem Hollom.apply_eq_of_line_eq {C : Set Hollom} (f : SpinalMap C) {n : ℕ} (hC : IsChain (fun (x1 x2 : Hollom) => x1 ≤ x2) C) {lo hi : Hollom} (hlo : lo ∈ C ∩ level n) (hhi : hi ∈ C ∩ level n) (hlohi : lo ≤ hi) {x y : Hollom} (h : line x = line y) (h₁l : lo ≤ x) (h₂l : lo ≤ y) (h₁h : x ≤ hi) (h₂h : y ≤ hi) : f x = f y

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

def Hollom.R (n : ℕ) (C : Set Hollom) : Set Hollom

Construction of the set R, which has the following key properties:

• It is a subset of level n.
• Each of its elements is comparable to all of C ∩ level n.
• There exists an a such that {(x, y, n) | x ≥ a ∧ y ≥ a} ⊆ R.

Equations

• Hollom.R n C = {x : Hollom | x ∈ Hollom.level n ∧ ∀ y ∈ C ∩ Hollom.level n, x ≤ y ∨ y ≤ x}

theorem Hollom.R_subset_level {C : Set Hollom} {n : ℕ} : R n C ⊆ level n

theorem Hollom.square_subset_above {C : Set Hollom} {n : ℕ} (h : (C ∩ level n).Finite) : ∀ᶠ (a : ℕ) in Filter.atTop, ⇑(embed n) '' Set.Ici (a, a) ⊆ {x : Hollom | ∀ y ∈ C ∩ level n, y ≤ x} \ (C ∩ level n)

A helper lemma to show square_subset_R. In particular shows that if C ∩ level n is finite, the set of points x such that x is at least as large as every element of C ∩ level n contains an "infinite square", i.e. a set of the form {(x, y, n) | x ≥ a ∧ y ≥ a}. The precise statement here is stronger in two ways:

• Instead of showing that some a works, we instead show that any sufficiently large a work. This is not much of a strengthening, but is convenient to have for chaining "sufficiently large" choices later.
• We also exclude C ∩ level n itself on the right.

theorem Hollom.square_subset_R {C : Set Hollom} {n : ℕ} (h : (C ∩ level n).Finite) : ∀ᶠ (a : ℕ) in Filter.atTop, ⇑(embed n) '' Set.Ici (a, a) ⊆ R n C \ (C ∩ level n)

theorem Hollom.R_diff_infinite {C : Set Hollom} {n : ℕ} (h : (C ∩ level n).Finite) : (R n C \ (C ∩ level n)).Infinite

theorem Hollom.not_R_hits_same {C : Set Hollom} {f : SpinalMap C} {n : ℕ} {x : Hollom} (hx : x ∈ R n C) (hx' : x ∉ C ∩ level n) : f x ∉ C ∩ level n

noncomputable def Hollom.x0y0 (n : ℕ) (C : Set Hollom) : ℕ × ℕ

Given a subset C of the Hollom partial order, and an index n, find the smallest element of C ∩ level (n + 1), expressed as (x₀, y₀, n + 1). This is only the global minimum provided C is a chain, which it is in context.

Equations

• Hollom.x0y0 n C = if h : (C ∩ Hollom.level (n + 1)).Nonempty then Hollom.x0y0.proof_1.min {x : ℕ × ℕ | (Hollom.embed (n + 1)) x ∈ C} ⋯ else 0

theorem Hollom.x0y0_mem {C : Set Hollom} {n : ℕ} (h : (C ∩ level (n + 1)).Nonempty) : (embed (n + 1)) (x0y0 n C) ∈ C

theorem Hollom.x0y0_min {C : Set Hollom} {n : ℕ} (z : ℕ × ℕ) (hC : IsChain (fun (x1 x2 : Hollom) => x1 ≤ x2) C) (h : (embed (n + 1)) z ∈ C) : (embed (n + 1)) (x0y0 n C) ≤ (embed (n + 1)) z

noncomputable def Hollom.x0 (n : ℕ) (C : Set Hollom) : ℕ

Given a subset C of the Hollom partial order, and an index n, find the smallest element of C ∩ level (n + 1), and x0 n C will be the x-coordinate thereof.

Equations

• Hollom.x0 n C = (Hollom.x0y0 n C).1

noncomputable def Hollom.y0 (n : ℕ) (C : Set Hollom) : ℕ

Given a subset C of the Hollom partial order, and an index n, find the smallest element of C ∩ level (n + 1), and y0 n C will be the y-coordinate thereof.

Equations

• Hollom.y0 n C = (Hollom.x0y0 n C).2

theorem Hollom.x0_y0_mem {C : Set Hollom} {n : ℕ} (h : (C ∩ level (n + 1)).Nonempty) : { ofHollom := (x0 n C, y0 n C, n + 1) } ∈ C

theorem Hollom.x0_y0_min {C : Set Hollom} {n : ℕ} (hC : IsChain (fun (x1 x2 : Hollom) => x1 ≤ x2) C) {a b : ℕ} (h : { ofHollom := (a, b, n + 1) } ∈ C) : { ofHollom := (x0 n C, y0 n C, n + 1) } ≤ { ofHollom := (a, b, n + 1) }

noncomputable def Hollom.S (n : ℕ) (C : Set Hollom) : Set Hollom

Construction of the set S, which has the following key properties:

• It is a subset of R.
• No element of it can be mapped to an element of C ∩ level (n + 1) by f.
• There exists an a such that {(x, y, n) | x ≥ a ∧ y ≥ a} ⊆ S.

If C ∩ level (n + 1) is finite, it is all elements of R which are comparable to C ∩ level (n + 1). Otherwise, say (x0, y0, n + 1) is the smallest element of C ∩ level (n + 1), and take all elements of R of the form (a, b, n) with max x0 y0 + 1 ≤ min a b.

Equations

• One or more equations did not get rendered due to their size.

theorem Hollom.S_subset_R {C : Set Hollom} {n : ℕ} : S n C ⊆ R n C

theorem Hollom.S_subset_level {C : Set Hollom} {n : ℕ} : S n C ⊆ level n

theorem Hollom.square_subset_S_case_1 {C : Set Hollom} {n : ℕ} (h : (C ∩ level n).Finite) (h' : (C ∩ level (n + 1)).Finite) : ∀ᶠ (a : ℕ) in Filter.atTop, ⇑(embed n) '' Set.Ici (a, a) ⊆ S n C \ (C ∩ level n)

Assuming C ∩ level n is finite, and C ∩ level (n + 1) is finite, that there exists cofinitely many a such that {(x, y, n) | x ≥ a ∧ y ≥ a} ⊆ S \ (C ∩ level n). We will later show the same assuming C ∩ level (n + 1) is infinite.

theorem Hollom.square_subset_S_case_2 {C : Set Hollom} {n : ℕ} (h : (C ∩ level n).Finite) (h' : (C ∩ level (n + 1)).Infinite) : ∀ᶠ (a : ℕ) in Filter.atTop, ⇑(embed n) '' Set.Ici (a, a) ⊆ S n C \ (C ∩ level n)

Assuming C ∩ level n is finite, and C ∩ level (n + 1) is infinite, that there exists cofinitely many a such that {(x, y, n) | x ≥ a ∧ y ≥ a} ⊆ S \ (C ∩ level n). We earlier showed the same assuming C ∩ level (n + 1) is finite.

theorem Hollom.square_subset_S {C : Set Hollom} {n : ℕ} (h : (C ∩ level n).Finite) : ∀ᶠ (a : ℕ) in Filter.atTop, ⇑(embed n) '' Set.Ici (a, a) ⊆ S n C \ (C ∩ level n)

theorem Hollom.S_infinite {C : Set Hollom} {n : ℕ} (h : (C ∩ level n).Finite) : (S n C \ (C ∩ level n)).Infinite

theorem Hollom.left_or_right_bias {C : Set Hollom} {n : ℕ} (a b : ℕ) (hab : ∀ (x y : ℕ), { ofHollom := (x, y, n) } ∈ C → { ofHollom := (a, b, n) } ≤ { ofHollom := (x, y, n) }) (hCn : (C ∩ level n).Infinite) : (∀ (i : ℕ), ∃ j ∈ C ∩ level n, { ofHollom := (a, i, n) } ≤ j) ∨ ∀ (i : ℕ), ∃ j ∈ C ∩ level n, { ofHollom := (i, b, n) } ≤ j

Given (a, b, n) which is a lower bound on C ∩ level n, and assuming C ∩ level n is infinite, we either have:

• for any i, there is an element of C ∩ level n greater than (a, i, n)
• for any i, there is an element of C ∩ level n greater than (i, b, n)

theorem Hollom.not_S_hits_next {C : Set Hollom} {n : ℕ} (f : SpinalMap C) (hC : IsChain (fun (x1 x2 : Hollom) => x1 ≤ x2) C) {x : Hollom} (hx : x ∈ S n C) (hx' : x ∉ C ∩ level n) : f x ∉ C ∩ level (n + 1)

Given a point x in S which is not in C ∩ level n, its image under f cannot be in C ∩ level (n + 1).

theorem Hollom.S_mapsTo_previous {C : Set Hollom} {n : ℕ} (f : SpinalMap C) (hC : IsChain (fun (x1 x2 : Hollom) => x1 ≤ x2) C) (hn : n ≠ 0) (x : Hollom) : x ∈ S n C \ (C ∩ level n) → f x ∈ C ∩ level (n - 1)

Every element of S \ (C ∩ level n) must be mapped into C ∩ level (n - 1).

theorem Hollom.not_S_mapsTo_previous {C : Set Hollom} {f : SpinalMap C} {n : ℕ} (hC : IsChain (fun (x1 x2 : Hollom) => x1 ≤ x2) C) (hCn : (C ∩ level n).Finite) (hn : n ≠ 0) (h : ∀ x ∈ S n C \ (C ∩ level n), f x ∈ C ∩ level (n - 1)) : False

Supposing that all of S \ (C ∩ level n) is sent to C ∩ level (n - 1), we deduce a contradiction.

theorem Hollom.no_spinalMap {C : Set Hollom} (hC : IsChain (fun (x1 x2 : Hollom) => x1 ≤ x2) C) (f : SpinalMap C) : False

The Hollom partial order has no spinal maps.

theorem aharoni_korman_false : ¬∀ (α : Type) (x : PartialOrder α), (∃ (A : Set α), IsAntichain (fun (x1 x2 : α) => x1 ≤ x2) A ∧ A.Infinite) ∨ ∃ (C : Set α), IsChain (fun (x1 x2 : α) => x1 ≤ x2) C ∧ ∃ (S : Set (Set α)), Setoid.IsPartition S ∧ ∀ A ∈ S, IsAntichain (fun (x1 x2 : α) => x1 ≤ x2) A ∧ (A ∩ C).Nonempty

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

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

In November 2024, Hollom disproved this conjecture.

This statement says that it is not the case that every partially ordered set satisfies one of the above conditions.