LeanPool.ErdosTuzaValtr.Main.InductionStep

Imported Lean Pool material for LeanPool.ErdosTuzaValtr.Main.InductionStep.

noncomputable def Config.delta {α : Type u_1} [LinearOrder α] (C : Config α) (n : ℕ) (S : Finset α) : Finset α

The set of row-minimal points of S whose beta value is below n.

Equations

• C.delta n S = {p ∈ S | C.beta S p < n ∧ ↑p = {q ∈ S | C.beta S q = C.beta S p}.min}

theorem Config.delta_card {α : Type u_1} [LinearOrder α] (C : Config α) (n : ℕ) (S : Finset α) : (C.delta n S).card ≤ n

theorem Config.not_mem_delta {α : Type u_1} [LinearOrder α] (C : Config α) {n : ℕ} {S : Finset α} {p' : α} (h : p' ∈ S \ C.delta n S) : n ≤ C.beta S p' ∨ ∃ p ∈ C.delta n S, C.beta S p = C.beta S p' ∧ p < p'

theorem Config.find_join {α : Type u_1} [LinearOrder α] (C : Config α) {n : ℕ} {S : Finset α} (l : C.Label S) (cup_free : ¬C.HasNCup (n + 4) S) (no_join : ¬C.HasJoin (n + 3) (n + 2) S) (o p : α) (c : List α) (m : ℕ) (o_in_S : o ∈ S) (p_in_S : p ∈ S) (o_le_p : o ≤ p) (c_in_S : c.In S) (c_ncup : C.NCup m c) (c_head : p ∈ c.head?) (le_m : n + 2 ≤ m) (ho : n + 2 ≤ C.beta S o) : False

theorem Config.laced_extension {α : Type u_1} [LinearOrder α] (C : Config α) {n : ℕ} {S D : Finset α} (l : C.Label S) (cup_free : ¬C.HasNCup (n + 4) S) (def_D : D = C.delta (n + 2) S) (no_join : ¬C.HasJoin (n + 3) (n + 2) S) {p' r : α} (p'r_laced : C.HasLaced (n + 2) (S \ D) p' r) : l.alpha p' = 1 ∧ ∃ (p : α), C.HasLaced (n + 3) S p r ∧ p < p' ∧ l.alpha p = 0 ∧ C.beta S p = C.beta S p'

theorem Config.main_induction_wlog {α : Type u_1} [LinearOrder α] (C : Config α) (n : ℕ) : C.MainGoal n → C.MainGoalWlog (n + 1)