Kneser's conjecture in Lean/Mathlib via Greene's proof: layout

Once you have Borsuk–Ulam for any f continuous on S(E) → F with finrank F + 1 = finrank E, χ(KG(n,k)) = n-2k+2 takes about 300 lines. (1) Lusternik–Schnirelmann for covers by sets that are each open or closed. Use D i := if IsClosed (C i) then C i else (C i)ᶜ and f x := (infDist x (D i))ᵢ; membership in C i is symmetric under x ↦ -x exactly when it is for D i, and handle empty D separately. (2) General position: put wⱼ = (j^i)ᵢ in EuclideanSpace ℝ (Fin (d+1)). If x ⊥ d+1 of them, then Σ C(xᵢ)Xⁱ has d+1 roots, and Polynomial.eq_zero_of_natDegree_lt_card_of_eval_eq_zero gives x = 0. (3) Let Uᵢ := ⋃ s (_ : #s = k ∧ c s = i), ⋂ j ∈ s, {x | 0 < ⟪x, wⱼ⟫}; it is open by isOpen_iUnion/isOpen_biInter_finset. F is the complement of their union. An antipodal pair in Uᵢ gives disjoint k-sets. A pair in F means P, Q (filters by sign of ⟪x,wⱼ⟫) have card < k, so the zero filter has card ≥ d+1. (4) Upper bound: colour s by min (s.min' _).val D. omega handles min. Mathlib has no Kneser graph; define Adj s t := Disjoint s.1 t.1 ∧ s ≠ t on {s : Finset (Fin n) // s.card = k}. SimpleGraph fields are now symm := ⟨…⟩, loopless := ⟨…⟩ (Std.Symm/Std.Irrefl structures). Then use chromaticNumber_eq_iff_colorable_not_colorable. Gotcha: set d := n+1-2k after c : _ → Fin (n+1-2k) is in context shadows c. Prove an aux lemma with d free and d + 2k = n + 1 instead.