import Erdos776.Uniform.ProblemStatement /-! # Three parameter cases of Erdős Problem 776 — Kairos, 2026-09-05 Machine-checked statements of * `n₀(5) = 14`, `n₀(6) = 16`, `n₀(11) = 27` (published formulation, strict convention `n > N`), and * the exact values at the last failing ground set: `g(14,5) = 10`, `g(16,6) = 12`, `g(27,11) = 23`. The threshold statements are corollaries of `Erdos776.Uniform.erdos776_threshold` from M. Thiim's package (Erdős-problems proof claim #78, 17 July 2026, tag `v0.4.1-proof-claim`), which proves the piecewise formula for every `r ≥ 4`. Nothing here is an independent proof of those thresholds. The exact values combine that package's occupied-level upper bound (`card_occupiedLevels_le_middle`), the failure half of the threshold, and three explicit antichains produced by the colex construction of the profile criterion (the same families as in the Kairos/GPT-6 note of 2026-09-05), whose antichain, multiplicity and level-count properties are checked by `native_decide` (kernel `decide` on these Finset literals did not finish in 10 minutes; `native_decide` is the same trust class as the package's own three finite certificates). -/ set_option autoImplicit false namespace Kairos open Finset Erdos776.Antichain Erdos776.Uniform /-! ## Thresholds as corollaries -/ theorem n0_5 : ProblemThreshold 5 14 := by simpa [erdosThresholdFromFour] using erdos776_threshold 5 (by norm_num) theorem n0_6 : ProblemThreshold 6 16 := by simpa [erdosThresholdFromFour] using erdos776_threshold 6 (by norm_num) theorem n0_11 : ProblemThreshold 11 27 := by simpa [erdosThresholdFromFour] using erdos776_threshold 11 (by norm_num) theorem lastFailure_5 : ProblemLastFailure 5 14 := by simpa [erdosThresholdFromFour] using erdos776_lastFailure 5 (by norm_num) theorem lastFailure_6 : ProblemLastFailure 6 16 := by simpa [erdosThresholdFromFour] using erdos776_lastFailure 6 (by norm_num) theorem lastFailure_11 : ProblemLastFailure 11 27 := by simpa [erdosThresholdFromFour] using erdos776_lastFailure 11 (by norm_num) /-- No 5-multiplicity antichain on 14 points occupies 11 sizes. -/ theorem no_eleven_sizes_on_14 : ¬ ∃ F : Family (Fin 14), ProblemAdmissible F 5 ∧ (occupiedLevels F).card = 11 := by simpa [ProblemTargetExists] using lastFailure_5.1 theorem no_thirteen_sizes_on_16 : ¬ ∃ F : Family (Fin 16), ProblemAdmissible F 6 ∧ (occupiedLevels F).card = 13 := by simpa [ProblemTargetExists] using lastFailure_6.1 theorem no_twentyfour_sizes_on_27 : ¬ ∃ F : Family (Fin 27), ProblemAdmissible F 11 ∧ (occupiedLevels F).card = 24 := by simpa [ProblemTargetExists] using lastFailure_11.1 /-- Every larger ground set admits `n - 3` sizes (the success half). -/ theorem success_above_14 : ∀ n, 14 < n → ProblemTargetExists n 5 := lastFailure_5.2 theorem success_above_16 : ∀ n, 16 < n → ProblemTargetExists n 6 := lastFailure_6.2 theorem success_above_27 : ∀ n, 27 < n → ProblemTargetExists n 11 := lastFailure_11.2 /-! ## Explicit witnesses for the exact values -/ /-- List-level subset test: every element of `l₁` occurs in `l₂`. -/ def lsub {α : Type*} [DecidableEq α] (l₁ l₂ : List α) : Bool := l₁.all fun x => decide (x ∈ l₂) theorem lsub_eq_true_iff {α : Type*} [DecidableEq α] {l₁ l₂ : List α} : lsub l₁ l₂ = true ↔ l₁.toFinset ⊆ l₂.toFinset := by simp [lsub, List.all_eq_true, Finset.subset_iff] /-- Executable antichain check on a list of lists: no row is contained in another. -/ def pairwiseOK {α : Type*} [DecidableEq α] : List (List α) → Bool | [] => true | a :: rest => (rest.all fun b => !lsub a b && !lsub b a) && pairwiseOK rest theorem pairwiseOK_iff {α : Type*} [DecidableEq α] (L : List (List α)) : pairwiseOK L = true ↔ L.Pairwise fun a b => lsub a b = false ∧ lsub b a = false := by induction L with | nil => simp [pairwiseOK] | cons a rest ih => simp only [pairwiseOK, Bool.and_eq_true, List.all_eq_true, List.pairwise_cons, ih, Bool.not_eq_eq_eq_not, Bool.not_true] /-- Soundness of the executable check for the family `(L.map List.toFinset).toFinset`. -/ theorem isSperner_of_pairwiseOK {α : Type*} [DecidableEq α] (L : List (List α)) (h : pairwiseOK L = true) : IsSperner (L.map List.toFinset).toFinset := by have hp := (pairwiseOK_iff L).mp h intro a ha b hb hne hab rw [Finset.mem_coe, List.mem_toFinset, List.mem_map] at ha hb obtain ⟨la, hla, rfl⟩ := ha obtain ⟨lb, hlb, rfl⟩ := hb have hne' : la ≠ lb := fun e => hne (by rw [e]) have hsym : Symmetric fun a b : List α => lsub a b = false ∧ lsub b a = false := fun x y hxy => ⟨hxy.2, hxy.1⟩ have hr := List.Pairwise.forall hsym hp hla hlb hne' exact absurd (lsub_eq_true_iff.mpr hab) (by simp [hr.1]) /-- 50 sets on `Fin 14`: exactly 5 of every size 2..11 (colex construction, 0-based labels). -/ def w14L : List (List (Fin 14)) := [[0, 13], [1, 13], [9, 12], [10, 12], [11, 12], [0, 8, 12], [1, 8, 12], [2, 8, 12], [3, 8, 12], [4, 8, 12], [0, 6, 7, 12], [1, 6, 7, 12], [2, 6, 7, 12], [3, 6, 7, 12], [4, 5, 7, 12], [0, 1, 5, 7, 12], [0, 2, 5, 7, 12], [0, 3, 5, 7, 12], [1, 2, 5, 7, 12], [1, 3, 5, 7, 12], [0, 1, 2, 3, 7, 12], [0, 1, 2, 4, 7, 12], [0, 1, 3, 4, 7, 12], [0, 2, 3, 4, 7, 12], [2, 3, 4, 5, 6, 12], [0, 1, 2, 3, 4, 5, 12], [0, 1, 2, 3, 4, 6, 12], [0, 1, 2, 3, 5, 6, 12], [0, 1, 2, 4, 5, 6, 12], [0, 1, 3, 4, 5, 6, 12], [0, 5, 6, 7, 8, 9, 10, 11], [1, 5, 6, 7, 8, 9, 10, 11], [2, 4, 6, 7, 8, 9, 10, 11], [2, 5, 6, 7, 8, 9, 10, 11], [3, 4, 6, 7, 8, 9, 10, 11], [0, 1, 2, 6, 7, 8, 9, 10, 11], [0, 1, 3, 6, 7, 8, 9, 10, 11], [0, 1, 4, 6, 7, 8, 9, 10, 11], [0, 2, 3, 6, 7, 8, 9, 10, 11], [1, 2, 3, 6, 7, 8, 9, 10, 11], [0, 1, 2, 3, 4, 7, 8, 9, 10, 11], [0, 1, 2, 3, 5, 7, 8, 9, 10, 11], [0, 1, 2, 4, 5, 7, 8, 9, 10, 11], [0, 1, 3, 4, 5, 7, 8, 9, 10, 11], [0, 2, 3, 4, 5, 7, 8, 9, 10, 11], [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10], [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 11], [0, 1, 2, 3, 4, 5, 6, 7, 8, 10, 11], [0, 1, 2, 3, 4, 5, 6, 7, 9, 10, 11], [0, 1, 2, 3, 4, 5, 6, 8, 9, 10, 11]] def w14 : Finset (Finset (Fin 14)) := (w14L.map List.toFinset).toFinset /-- 72 sets on `Fin 16`: exactly 6 of every size 2..13 (colex construction, 0-based labels). -/ def w16L : List (List (Fin 16)) := [[0, 15], [1, 15], [10, 14], [11, 14], [12, 14], [13, 14], [0, 9, 14], [1, 9, 14], [2, 9, 14], [3, 9, 14], [4, 9, 14], [5, 9, 14], [0, 7, 8, 14], [1, 7, 8, 14], [2, 7, 8, 14], [3, 7, 8, 14], [4, 7, 8, 14], [5, 7, 8, 14], [0, 5, 6, 8, 14], [1, 5, 6, 8, 14], [2, 5, 6, 8, 14], [3, 4, 6, 8, 14], [3, 5, 6, 8, 14], [4, 5, 6, 8, 14], [0, 1, 2, 6, 8, 14], [0, 1, 3, 6, 8, 14], [0, 1, 4, 6, 8, 14], [0, 2, 3, 6, 8, 14], [0, 2, 4, 6, 8, 14], [1, 2, 3, 6, 8, 14], [0, 1, 2, 3, 4, 8, 14], [0, 1, 2, 3, 5, 8, 14], [0, 1, 2, 4, 5, 8, 14], [0, 1, 3, 4, 5, 8, 14], [0, 2, 3, 4, 5, 8, 14], [2, 3, 4, 5, 6, 7, 14], [0, 1, 2, 3, 4, 5, 6, 14], [0, 1, 2, 3, 4, 5, 7, 14], [0, 1, 2, 3, 4, 6, 7, 14], [0, 1, 2, 3, 5, 6, 7, 14], [0, 1, 2, 4, 5, 6, 7, 14], [0, 1, 3, 4, 5, 6, 7, 14], [0, 6, 7, 8, 9, 10, 11, 12, 13], [1, 6, 7, 8, 9, 10, 11, 12, 13], [2, 6, 7, 8, 9, 10, 11, 12, 13], [3, 6, 7, 8, 9, 10, 11, 12, 13], [4, 6, 7, 8, 9, 10, 11, 12, 13], [5, 6, 7, 8, 9, 10, 11, 12, 13], [0, 3, 5, 7, 8, 9, 10, 11, 12, 13], [0, 4, 5, 7, 8, 9, 10, 11, 12, 13], [1, 3, 5, 7, 8, 9, 10, 11, 12, 13], [1, 4, 5, 7, 8, 9, 10, 11, 12, 13], [2, 3, 5, 7, 8, 9, 10, 11, 12, 13], [2, 4, 5, 7, 8, 9, 10, 11, 12, 13], [0, 1, 2, 3, 7, 8, 9, 10, 11, 12, 13], [0, 1, 2, 4, 7, 8, 9, 10, 11, 12, 13], [0, 1, 2, 5, 7, 8, 9, 10, 11, 12, 13], [0, 1, 3, 4, 7, 8, 9, 10, 11, 12, 13], [0, 2, 3, 4, 7, 8, 9, 10, 11, 12, 13], [1, 2, 3, 4, 7, 8, 9, 10, 11, 12, 13], [0, 1, 2, 3, 4, 5, 8, 9, 10, 11, 12, 13], [0, 1, 2, 3, 4, 6, 8, 9, 10, 11, 12, 13], [0, 1, 2, 3, 5, 6, 8, 9, 10, 11, 12, 13], [0, 1, 2, 4, 5, 6, 8, 9, 10, 11, 12, 13], [0, 1, 3, 4, 5, 6, 8, 9, 10, 11, 12, 13], [0, 2, 3, 4, 5, 6, 8, 9, 10, 11, 12, 13], [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12], [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 13], [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 12, 13], [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 11, 12, 13], [0, 1, 2, 3, 4, 5, 6, 7, 8, 10, 11, 12, 13], [0, 1, 2, 3, 4, 5, 6, 7, 9, 10, 11, 12, 13]] def w16 : Finset (Finset (Fin 16)) := (w16L.map List.toFinset).toFinset /-- 253 sets on `Fin 27`: exactly 11 of every size 2..24 (colex construction, 0-based labels). -/ def w27L : List (List (Fin 27)) := [[0, 26], [1, 26], [16, 25], [17, 25], [18, 25], [19, 25], [20, 25], [21, 25], [22, 25], [23, 25], [24, 25], [0, 15, 25], [1, 15, 25], [2, 15, 25], [3, 15, 25], [4, 15, 25], [5, 15, 25], [6, 15, 25], [7, 15, 25], [11, 14, 25], [12, 14, 25], [13, 14, 25], [0, 10, 14, 25], [1, 10, 14, 25], [2, 10, 14, 25], [3, 10, 14, 25], [4, 9, 14, 25], [4, 10, 14, 25], [5, 9, 14, 25], [5, 10, 14, 25], [6, 9, 14, 25], [7, 9, 14, 25], [8, 9, 14, 25], [0, 1, 9, 14, 25], [0, 2, 9, 14, 25], [0, 3, 9, 14, 25], [0, 7, 8, 14, 25], [1, 2, 9, 14, 25], [1, 7, 8, 14, 25], [2, 7, 8, 14, 25], [3, 7, 8, 14, 25], [4, 7, 8, 14, 25], [5, 7, 8, 14, 25], [6, 7, 8, 14, 25], [0, 3, 6, 8, 14, 25], [0, 4, 6, 8, 14, 25], [0, 5, 6, 8, 14, 25], [1, 3, 6, 8, 14, 25], [1, 4, 6, 8, 14, 25], [1, 5, 6, 8, 14, 25], [2, 3, 6, 8, 14, 25], [2, 4, 6, 8, 14, 25], [2, 5, 6, 8, 14, 25], [3, 4, 6, 8, 14, 25], [3, 5, 6, 8, 14, 25], [0, 1, 2, 5, 8, 14, 25], [0, 1, 2, 6, 8, 14, 25], [0, 1, 3, 5, 8, 14, 25], [0, 1, 4, 5, 8, 14, 25], [0, 2, 3, 5, 8, 14, 25], [0, 2, 4, 5, 8, 14, 25], [0, 3, 4, 5, 8, 14, 25], [1, 2, 3, 5, 8, 14, 25], [1, 2, 4, 5, 8, 14, 25], [1, 3, 4, 5, 8, 14, 25], [2, 3, 4, 5, 8, 14, 25], [0, 1, 2, 3, 4, 8, 14, 25], [0, 1, 2, 5, 6, 7, 14, 25], [0, 1, 3, 5, 6, 7, 14, 25], [0, 1, 4, 5, 6, 7, 14, 25], [0, 2, 3, 5, 6, 7, 14, 25], [0, 2, 4, 5, 6, 7, 14, 25], [0, 3, 4, 5, 6, 7, 14, 25], [1, 2, 3, 5, 6, 7, 14, 25], [1, 2, 4, 5, 6, 7, 14, 25], [1, 3, 4, 5, 6, 7, 14, 25], [2, 3, 4, 5, 6, 7, 14, 25], [0, 1, 2, 3, 4, 5, 6, 14, 25], [0, 1, 2, 3, 4, 5, 7, 14, 25], [0, 1, 2, 3, 4, 6, 7, 14, 25], [0, 7, 8, 9, 10, 11, 12, 13, 25], [1, 7, 8, 9, 10, 11, 12, 13, 25], [2, 7, 8, 9, 10, 11, 12, 13, 25], [3, 7, 8, 9, 10, 11, 12, 13, 25], [4, 7, 8, 9, 10, 11, 12, 13, 25], [5, 6, 8, 9, 10, 11, 12, 13, 25], [5, 7, 8, 9, 10, 11, 12, 13, 25], [6, 7, 8, 9, 10, 11, 12, 13, 25], [0, 1, 6, 8, 9, 10, 11, 12, 13, 25], [0, 2, 6, 8, 9, 10, 11, 12, 13, 25], [0, 3, 6, 8, 9, 10, 11, 12, 13, 25], [0, 4, 6, 8, 9, 10, 11, 12, 13, 25], [1, 2, 6, 8, 9, 10, 11, 12, 13, 25], [1, 3, 6, 8, 9, 10, 11, 12, 13, 25], [1, 4, 6, 8, 9, 10, 11, 12, 13, 25], [2, 3, 6, 8, 9, 10, 11, 12, 13, 25], [2, 4, 5, 8, 9, 10, 11, 12, 13, 25], [2, 4, 6, 8, 9, 10, 11, 12, 13, 25], [3, 4, 5, 8, 9, 10, 11, 12, 13, 25], [0, 1, 2, 3, 8, 9, 10, 11, 12, 13, 25], [0, 1, 2, 4, 8, 9, 10, 11, 12, 13, 25], [0, 1, 2, 5, 8, 9, 10, 11, 12, 13, 25], [0, 1, 3, 4, 8, 9, 10, 11, 12, 13, 25], [0, 1, 3, 5, 8, 9, 10, 11, 12, 13, 25], [0, 1, 4, 5, 8, 9, 10, 11, 12, 13, 25], [0, 2, 3, 4, 8, 9, 10, 11, 12, 13, 25], [0, 2, 3, 5, 8, 9, 10, 11, 12, 13, 25], [1, 2, 3, 4, 8, 9, 10, 11, 12, 13, 25], [1, 2, 3, 5, 8, 9, 10, 11, 12, 13, 25], [3, 4, 5, 6, 7, 9, 10, 11, 12, 13, 25], [0, 1, 2, 3, 6, 7, 9, 10, 11, 12, 13, 25], [0, 1, 2, 4, 6, 7, 9, 10, 11, 12, 13, 25], [0, 1, 2, 5, 6, 7, 9, 10, 11, 12, 13, 25], [0, 1, 3, 4, 6, 7, 9, 10, 11, 12, 13, 25], [0, 1, 3, 5, 6, 7, 9, 10, 11, 12, 13, 25], [0, 1, 4, 5, 6, 7, 9, 10, 11, 12, 13, 25], [0, 2, 3, 4, 6, 7, 9, 10, 11, 12, 13, 25], [0, 2, 3, 5, 6, 7, 9, 10, 11, 12, 13, 25], [0, 2, 4, 5, 6, 7, 9, 10, 11, 12, 13, 25], [1, 2, 3, 4, 6, 7, 9, 10, 11, 12, 13, 25], [1, 2, 3, 5, 6, 7, 9, 10, 11, 12, 13, 25], [0, 1, 2, 3, 4, 5, 6, 7, 10, 11, 12, 13, 25], [0, 1, 2, 3, 4, 5, 6, 8, 10, 11, 12, 13, 25], [0, 1, 2, 3, 4, 5, 6, 9, 10, 11, 12, 13, 25], [0, 1, 2, 3, 4, 5, 7, 8, 10, 11, 12, 13, 25], [0, 1, 2, 3, 4, 5, 7, 9, 10, 11, 12, 13, 25], [0, 1, 2, 3, 4, 6, 7, 8, 10, 11, 12, 13, 25], [0, 1, 2, 3, 5, 6, 7, 8, 10, 11, 12, 13, 25], [0, 1, 2, 4, 5, 6, 7, 8, 10, 11, 12, 13, 25], [0, 1, 3, 4, 5, 6, 7, 8, 10, 11, 12, 13, 25], [0, 2, 3, 4, 5, 6, 7, 8, 10, 11, 12, 13, 25], [1, 2, 3, 4, 5, 6, 7, 8, 10, 11, 12, 13, 25], [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 25], [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 13, 25], [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 12, 13, 25], [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 11, 12, 13, 25], [5, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24], [6, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24], [7, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24], [8, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24], [9, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24], [10, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24], [11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24], [0, 1, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24], [0, 2, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24], [0, 3, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24], [0, 4, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24], [1, 2, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24], [1, 3, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24], [1, 4, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24], [2, 3, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24], [7, 10, 11, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24], [8, 10, 11, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24], [9, 10, 11, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24], [0, 4, 10, 11, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24], [0, 5, 10, 11, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24], [0, 6, 10, 11, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24], [1, 4, 10, 11, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24], [1, 5, 10, 11, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24], [1, 6, 10, 11, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24], [2, 4, 10, 11, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24], [2, 5, 10, 11, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24], [3, 4, 10, 11, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24], [3, 5, 10, 11, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24], [4, 5, 10, 11, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24], [0, 1, 2, 10, 11, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24], [0, 1, 3, 10, 11, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24], [0, 2, 3, 10, 11, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24], [0, 7, 8, 9, 11, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24], [1, 7, 8, 9, 11, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24], [2, 7, 8, 9, 11, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24], [3, 7, 8, 9, 11, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24], [4, 7, 8, 9, 11, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24], [5, 6, 8, 9, 11, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24], [5, 7, 8, 9, 11, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24], [6, 7, 8, 9, 11, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24], [0, 1, 6, 8, 9, 11, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24], [0, 2, 6, 8, 9, 11, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24], [0, 3, 6, 8, 9, 11, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24], [0, 4, 6, 8, 9, 11, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24], [1, 2, 6, 8, 9, 11, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24], [1, 3, 6, 8, 9, 11, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24], [1, 4, 6, 8, 9, 11, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24], [2, 3, 6, 8, 9, 11, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24], [2, 4, 5, 8, 9, 11, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24], [2, 4, 6, 8, 9, 11, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24], [3, 4, 5, 8, 9, 11, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24], [0, 1, 2, 3, 8, 9, 11, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24], [0, 1, 2, 4, 8, 9, 11, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24], [0, 1, 2, 5, 8, 9, 11, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24], [0, 1, 3, 4, 8, 9, 11, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24], [0, 1, 3, 5, 8, 9, 11, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24], [0, 1, 4, 5, 8, 9, 11, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24], [0, 2, 3, 4, 8, 9, 11, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24], [0, 2, 3, 5, 8, 9, 11, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24], [1, 2, 3, 4, 8, 9, 11, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24], [1, 2, 3, 5, 8, 9, 11, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24], [3, 4, 5, 6, 7, 9, 11, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24], [0, 1, 2, 3, 6, 7, 9, 11, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24], [0, 1, 2, 4, 6, 7, 9, 11, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24], [0, 1, 2, 5, 6, 7, 9, 11, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24], [0, 1, 3, 4, 6, 7, 9, 11, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24], [0, 1, 3, 5, 6, 7, 9, 11, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24], [0, 1, 4, 5, 6, 7, 9, 11, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24], [0, 2, 3, 4, 6, 7, 9, 11, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24], [0, 2, 3, 5, 6, 7, 9, 11, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24], [0, 2, 4, 5, 6, 7, 9, 11, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24], [1, 2, 3, 4, 6, 7, 9, 11, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24], [1, 2, 3, 5, 6, 7, 9, 11, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24], [0, 1, 2, 3, 4, 5, 6, 7, 11, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24], [0, 1, 2, 3, 4, 5, 6, 8, 11, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24], [0, 1, 2, 3, 4, 5, 6, 9, 11, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24], [0, 1, 2, 3, 4, 5, 7, 8, 11, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24], [0, 1, 2, 3, 4, 5, 7, 9, 11, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24], [0, 1, 2, 3, 4, 6, 7, 8, 11, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24], [0, 1, 2, 3, 5, 6, 7, 8, 11, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24], [0, 1, 2, 4, 5, 6, 7, 8, 11, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24], [0, 1, 3, 4, 5, 6, 7, 8, 11, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24], [0, 2, 3, 4, 5, 6, 7, 8, 11, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24], [1, 2, 3, 4, 5, 6, 7, 8, 11, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24], [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24], [0, 1, 2, 3, 4, 5, 6, 7, 8, 10, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24], [0, 1, 2, 3, 4, 5, 6, 7, 9, 10, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24], [0, 1, 2, 3, 4, 5, 6, 8, 9, 10, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24], [0, 1, 2, 3, 4, 5, 7, 8, 9, 10, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24], [0, 1, 2, 3, 4, 6, 7, 8, 9, 10, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24], [0, 1, 2, 3, 5, 6, 7, 8, 9, 10, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24], [0, 1, 2, 4, 5, 6, 7, 8, 9, 10, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24], [0, 1, 3, 4, 5, 6, 7, 8, 9, 10, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24], [0, 2, 3, 4, 5, 6, 7, 8, 9, 10, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24], [2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24], [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24], [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 12, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24], [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 11, 12, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24], [0, 1, 2, 3, 4, 5, 6, 7, 8, 10, 11, 12, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24], [0, 1, 2, 3, 4, 5, 6, 7, 9, 10, 11, 12, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24], [0, 1, 2, 3, 4, 5, 6, 8, 9, 10, 11, 12, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24], [0, 1, 2, 3, 4, 5, 7, 8, 9, 10, 11, 12, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24], [0, 1, 2, 3, 4, 6, 7, 8, 9, 10, 11, 12, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24], [0, 1, 2, 3, 5, 6, 7, 8, 9, 10, 11, 12, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24], [0, 1, 2, 4, 5, 6, 7, 8, 9, 10, 11, 12, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24], [0, 1, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24], [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23], [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 24], [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 23, 24], [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 22, 23, 24], [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 21, 22, 23, 24], [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 20, 21, 22, 23, 24], [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 19, 20, 21, 22, 23, 24], [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 18, 19, 20, 21, 22, 23, 24], [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 17, 18, 19, 20, 21, 22, 23, 24], [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 16, 17, 18, 19, 20, 21, 22, 23, 24], [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24]] def w27 : Finset (Finset (Fin 27)) := (w27L.map List.toFinset).toFinset theorem w14_admissible : ProblemAdmissible w14 5 := by rw [problemAdmissible_iff_isMultiplicityAntichain] exact ⟨isSperner_of_pairwiseOK _ (by native_decide), by native_decide⟩ theorem w16_admissible : ProblemAdmissible w16 6 := by rw [problemAdmissible_iff_isMultiplicityAntichain] exact ⟨isSperner_of_pairwiseOK _ (by native_decide), by native_decide⟩ theorem w27_admissible : ProblemAdmissible w27 11 := by rw [problemAdmissible_iff_isMultiplicityAntichain] exact ⟨isSperner_of_pairwiseOK _ (by native_decide), by native_decide⟩ theorem w14_levels : (occupiedLevels w14).card = 10 := by native_decide theorem w16_levels : (occupiedLevels w16).card = 12 := by native_decide theorem w27_levels : (occupiedLevels w27).card = 23 := by native_decide /-! ## Exact values `g(n₀, r)` -/ /-- `g(14,5) = 10`: ten sizes are attained, eleven are impossible. -/ theorem g_14_5 : (∃ F : Family (Fin 14), ProblemAdmissible F 5 ∧ (occupiedLevels F).card = 10) ∧ ∀ F : Family (Fin 14), ProblemAdmissible F 5 → (occupiedLevels F).card ≤ 10 := by refine ⟨⟨w14, w14_admissible, w14_levels⟩, ?_⟩ intro F hF have hle : (occupiedLevels F).card ≤ 14 - 3 := card_occupiedLevels_le_middle (by norm_num) (by norm_num) (problemAdmissible_iff_isMultiplicityAntichain.mp hF) have hne : (occupiedLevels F).card ≠ 11 := fun h => no_eleven_sizes_on_14 ⟨F, hF, h⟩ omega theorem g_16_6 : (∃ F : Family (Fin 16), ProblemAdmissible F 6 ∧ (occupiedLevels F).card = 12) ∧ ∀ F : Family (Fin 16), ProblemAdmissible F 6 → (occupiedLevels F).card ≤ 12 := by refine ⟨⟨w16, w16_admissible, w16_levels⟩, ?_⟩ intro F hF have hle : (occupiedLevels F).card ≤ 16 - 3 := card_occupiedLevels_le_middle (by norm_num) (by norm_num) (problemAdmissible_iff_isMultiplicityAntichain.mp hF) have hne : (occupiedLevels F).card ≠ 13 := fun h => no_thirteen_sizes_on_16 ⟨F, hF, h⟩ omega theorem g_27_11 : (∃ F : Family (Fin 27), ProblemAdmissible F 11 ∧ (occupiedLevels F).card = 23) ∧ ∀ F : Family (Fin 27), ProblemAdmissible F 11 → (occupiedLevels F).card ≤ 23 := by refine ⟨⟨w27, w27_admissible, w27_levels⟩, ?_⟩ intro F hF have hle : (occupiedLevels F).card ≤ 27 - 3 := card_occupiedLevels_le_middle (by norm_num) (by norm_num) (problemAdmissible_iff_isMultiplicityAntichain.mp hF) have hne : (occupiedLevels F).card ≠ 24 := fun h => no_twentyfour_sizes_on_27 ⟨F, hF, h⟩ omega end Kairos #print axioms Kairos.n0_5 #print axioms Kairos.n0_6 #print axioms Kairos.n0_11 #print axioms Kairos.g_14_5 #print axioms Kairos.g_16_6 #print axioms Kairos.g_27_11