Commit 2025-03-12 15:37 0dfdbd44

View on Github →

feat(Counterexamples): disproof of the Aharoni–Korman conjecture (#20082) Disprove the Aharoni–Korman conjecture by constructing and verifying Hollom's counterexample. Additionally show this counterexample is countable and scattered. Zulip thread: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Aharoni.E2.80.93Korman.20conjecture.20formally.20disproved

Estimated changes

added inductive Hollom.HollomOrder
added def Hollom.R
added theorem Hollom.R_diff_infinite
added theorem Hollom.R_subset_level
added theorem Hollom.S_infinite
added theorem Hollom.S_subset_R
added theorem Hollom.S_subset_level
added theorem Hollom.SpinalMap.ext
added theorem Hollom.SpinalMap.mem
added structure Hollom.SpinalMap
added def Hollom.embed
added theorem Hollom.embed_apply
added theorem Hollom.embed_image_Icc
added theorem Hollom.induction
added def Hollom.level
added theorem Hollom.level_eq
added theorem Hollom.level_eq_range
added theorem Hollom.level_isPWO
added def Hollom.line
added theorem Hollom.line_injOn
added theorem Hollom.line_mapsTo
added theorem Hollom.line_toHollom
added theorem Hollom.no_spinalMap
added theorem Hollom.not_R_hits_same
added theorem Hollom.not_S_hits_next
added theorem Hollom.scattered
added theorem Hollom.square_subset_R
added theorem Hollom.square_subset_S
added theorem Hollom.x0_y0_mem
added theorem Hollom.x0_y0_min
added theorem Hollom.x0y0_mem
added theorem Hollom.x0y0_min
added theorem Hollom.«exists»
added theorem Hollom.«forall»
added theorem Hollom.«forall₂»
added theorem Hollom.«forall₃»
added structure Hollom
added theorem aharoni_korman_false
added def equivHollom
added theorem ofHollom_toHollom
added theorem toHollom_ofHollom