Erdős problem 567 - part i

-- Erdős 567 (i): the pinned statement uses the SIZE Ramsey number
-- `SimpleGraph.sizeRamsey` (minimum EDGES in an arrowing host), whereas the
-- problem asks about the ordinary Ramsey number. The size-Ramsey reading is
-- false, and this file refutes it: with H = Kₙ, a biased first moment shows no
-- host with O(n²) edges arrows (Q₃, Kₙ), while e(Kₙ) = C(n,2).

open Erdos567 SimpleGraph
open scoped Finset

-- (Everything below is extracted verbatim by assemble.py into the submission's
-- Main.lean, where `Q3`, `sizeRamsey` and `IsRamseySizeLinear` resolve to the
-- imported originals instead of the local copies above.)

theorem q3_adj_matching (a b : Bool) : Q3.Adj ![false, a, b] ![true, a, b] := by
  have h : ∀ a b : Bool,
      Finset.card {k | (![false, a, b] : Fin 3 → Bool) k ≠ (![true, a, b] : Fin 3 → Bool) k} = 1 := by
    decide
  exact h a b

/-- Every vertex of `Q3` is an endpoint of one of the four matching edges. -/
theorem q3_matching_cover (u : Fin 3 → Bool) :
    ∃ a b : Bool, u = ![false, a, b] ∨ u = ![true, a, b] := by
  refine ⟨u 1, u 2, ?_⟩
  cases hu : u 0 with
  | false => exact Or.inl (by funext k; fin_cases k <;> simp [hu])
  | true => exact Or.inr (by funext k; fin_cases k <;> simp [hu])

/-- The number of ordered adjacent pairs of `R` is twice its number of edges. -/
theorem card_directed_edges {N : ℕ} (R : SimpleGraph (Fin N)) [DecidableRel R.Adj] :
    Nat.card {p : Fin N × Fin N // R.Adj p.1 p.2} = 2 * R.edgeSet.ncard := by
  have hne : R.edgeSet.ncard = R.edgeFinset.card := by
    rw [← SimpleGraph.coe_edgeFinset, Set.ncard_coe_finset]
  rw [hne, SimpleGraph.two_mul_card_edgeFinset, Nat.card_eq_fintype_card, Fintype.card_subtype]

/-- **Obligation O1 + O2.** A graph with `m` edges contains at most `(2m)^4` copies of `Q3`. -/
theorem q3_copy_count {N : ℕ} (R : SimpleGraph (Fin N)) [DecidableRel R.Adj] :
    Nat.card (SimpleGraph.Copy Q3 R) ≤ (2 * R.edgeSet.ncard) ^ 4 := by
  have hadj : ∀ (φ : SimpleGraph.Copy Q3 R) (a b : Bool),
      R.Adj (φ ![false, a, b]) (φ ![true, a, b]) := fun φ a b =>
    φ.toHom.map_adj (q3_adj_matching a b)
  refine le_trans (Nat.card_le_card_of_injective
    (fun φ : SimpleGraph.Copy Q3 R => fun ab : Bool × Bool =>
      (⟨(φ ![false, ab.1, ab.2], φ ![true, ab.1, ab.2]), hadj φ ab.1 ab.2⟩ :
        {p : Fin N × Fin N // R.Adj p.1 p.2})) ?_) ?_
  · intro φ ψ h
    refine SimpleGraph.Copy.ext fun u => ?_
    obtain ⟨a, b, hu | hu⟩ := q3_matching_cover u <;>
      · have h' := congrFun h (a, b)
        rw [Subtype.mk.injEq, Prod.mk.injEq] at h'
        rw [hu]
        first
          | exact h'.1
          | exact h'.2
  · rw [Nat.card_fun, card_directed_edges]
    simp

/-! ### The finite Ramsey theorem

Stated for finsets of an arbitrary vertex type so that the induction can pass to
the neighbourhood / non-neighbourhood of a chosen vertex. An independent set of
`G` is recorded as a clique of `Gᶜ`. -/

/-- **Finite Ramsey theorem.** For all `s t` there is an `N` such that every
finset of at least `N` vertices contains either an `s`-clique of `G` or a
`t`-clique of `Gᶜ` (i.e. an independent set of size `t`). -/
theorem ramsey_exists_bound : ∀ s t : ℕ, ∃ N : ℕ,
    ∀ (V : Type) (G : SimpleGraph V) (S : Finset V), N ≤ S.card →
      (∃ T ⊆ S, G.IsNClique s T) ∨ (∃ T ⊆ S, Gᶜ.IsNClique t T) := by
  intro s
  induction s with
  | zero =>
    intro t
    exact ⟨0, fun _ _ _ _ => Or.inl ⟨∅, Finset.empty_subset _, isNClique_empty.mpr rfl⟩⟩
  | succ s ihs =>
    intro t
    induction t with
    | zero =>
      exact ⟨0, fun _ _ _ _ => Or.inr ⟨∅, Finset.empty_subset _, isNClique_empty.mpr rfl⟩⟩
    | succ t iht =>
      obtain ⟨N₁, hN₁⟩ := ihs (t + 1)
      obtain ⟨N₂, hN₂⟩ := iht
      classical
      refine ⟨N₁ + N₂ + 1, fun V G S hS => ?_⟩
      obtain ⟨v, hv⟩ : S.Nonempty := Finset.card_pos.mp (by omega)
      obtain ⟨A, hAdef⟩ : ∃ A, A = (S.erase v).filter (fun w => G.Adj v w) := ⟨_, rfl⟩
      obtain ⟨B, hBdef⟩ : ∃ B, B = (S.erase v).filter (fun w => ¬ G.Adj v w) := ⟨_, rfl⟩
      have hAmem : ∀ w ∈ A, w ∈ S ∧ v ≠ w ∧ G.Adj v w := by
        intro w hw
        rw [hAdef, Finset.mem_filter, Finset.mem_erase] at hw
        exact ⟨hw.1.2, Ne.symm hw.1.1, hw.2⟩
      have hBmem : ∀ w ∈ B, w ∈ S ∧ v ≠ w ∧ ¬ G.Adj v w := by
        intro w hw
        rw [hBdef, Finset.mem_filter, Finset.mem_erase] at hw
        exact ⟨hw.1.2, Ne.symm hw.1.1, hw.2⟩
      have hcard : (S.erase v).card = S.card - 1 := Finset.card_erase_of_mem hv
      have hAB : A.card + B.card = (S.erase v).card := by
        rw [hAdef, hBdef]
        exact Finset.card_filter_add_card_filter_not _
      have hsplit : N₁ ≤ A.card ∨ N₂ ≤ B.card := by omega
      rcases hsplit with h | h
      · -- `v` has many neighbours: an `s`-clique among them extends by `v`.
        rcases hN₁ V G A h with ⟨T, hTA, hT⟩ | ⟨T, hTA, hT⟩
        · refine Or.inl ⟨insert v T, ?_, hT.insert fun b hb => (hAmem b (hTA hb)).2.2⟩
          rw [Finset.insert_subset_iff]
          exact ⟨hv, fun w hw => (hAmem w (hTA hw)).1⟩
        · exact Or.inr ⟨T, fun w hw => (hAmem w (hTA hw)).1, hT⟩
      · -- `v` has many non-neighbours: a `t`-clique of `Gᶜ` among them extends by `v`.
        rcases hN₂ V G B h with ⟨T, hTB, hT⟩ | ⟨T, hTB, hT⟩
        · exact Or.inl ⟨T, fun w hw => (hBmem w (hTB hw)).1, hT⟩
        · refine Or.inr ⟨insert v T, ?_, hT.insert fun b hb => ?_⟩
          · rw [Finset.insert_subset_iff]
            exact ⟨hv, fun w hw => (hBmem w (hTB hw)).1⟩
          · rw [SimpleGraph.compl_adj]
            exact ⟨(hBmem b (hTB hb)).2.1, (hBmem b (hTB hb)).2.2⟩

/-- A clique on `Fintype.card α` vertices is exactly a (not necessarily induced)
copy of the complete graph on `α`. -/
theorem top_isContained_of_isNClique {V α : Type*} [Fintype α]
    {H : SimpleGraph V} {T : Finset V} (hT : H.IsNClique (Fintype.card α) T) :
    (⊤ : SimpleGraph α).IsContained H := by
  have h : ¬ H.CliqueFree (Fintype.card α) := hT.not_cliqueFree
  rw [SimpleGraph.cliqueFree_iff_top_free] at h
  exact SimpleGraph.not_free.mp h

/-- On a complete host, deleting the red graph leaves exactly the complement. -/
theorem top_sdiff_eq_compl {N : ℕ} (R : SimpleGraph (Fin N)) :
    (⊤ : SimpleGraph (Fin N)) \ R = Rᶜ := by
  ext a b
  simp [SimpleGraph.compl_adj]

/-- **Obligation O5.** Some host graph arrows `(Q₃, Kₙ)`: the complete graph on
`R(8, n)` vertices does. Every red subgraph either has an `8`-clique — which
contains `Q₃`, since containment is not required to be induced — or leaves an
independent set of size `n`, i.e. a blue `Kₙ`. -/
theorem exists_arrows (n : ℕ) :
    ∃ (N : ℕ) (F : SimpleGraph (Fin N)),
      ∀ (R : SimpleGraph (Fin N)), R ≤ F →
        Q3.IsContained R ∨ (⊤ : SimpleGraph (Fin n)).IsContained (F \ R) := by
  obtain ⟨N, hN⟩ := ramsey_exists_bound 8 n
  refine ⟨N, ⊤, fun R _ => ?_⟩
  have huniv : N ≤ (Finset.univ : Finset (Fin N)).card := by simp
  rcases hN (Fin N) R Finset.univ huniv with ⟨T, -, hT⟩ | ⟨T, -, hT⟩
  · -- A red `K₈` contains `Q₃`, because containment is not induced.
    have h8 : R.IsNClique (Fintype.card (Fin 3 → Bool)) T := by
      rw [show Fintype.card (Fin 3 → Bool) = 8 by simp]
      exact hT
    exact Or.inl (SimpleGraph.IsContained.mono_left le_top
      (top_isContained_of_isNClique (α := Fin 3 → Bool) h8))
  · -- An independent `n`-set of `R` is a blue `Kₙ`.
    have hn : Rᶜ.IsNClique (Fintype.card (Fin n)) T := by
      rw [Fintype.card_fin]
      exact hT
    refine Or.inr ?_
    rw [top_sdiff_eq_compl]
    exact top_isContained_of_isNClique (α := Fin n) hn

/-- The defining set of `sizeRamsey` is nonempty, so `Nat.sInf` is not junk `0`. -/
theorem sizeRamsey_set_nonempty (n : ℕ) :
    { m | ∃ (N : ℕ) (F : SimpleGraph (Fin N)),
        F.edgeSet.ncard = m ∧
        ∀ (R : SimpleGraph (Fin N)), R ≤ F →
          Q3.IsContained R ∨ (⊤ : SimpleGraph (Fin n)).IsContained (F \ R) }.Nonempty := by
  obtain ⟨N, F, hF⟩ := exists_arrows n
  exact ⟨F.edgeSet.ncard, N, F, rfl, hF⟩

/-- The ordered pairs of adjacent `Q3` vertices, as a `Finset`.  Stating the
adjacency test inline keeps this decidable without a `DecidableRel Q3.Adj`
declaration. -/
private def q3Pairs : Finset ((Fin 3 → Bool) × (Fin 3 → Bool)) :=
  Finset.univ.filter
    (fun q => Finset.card (Finset.univ.filter (fun j => q.1 j ≠ q.2 j)) = 1)

/-- The edges of `Q3`, as a `Finset` of `Sym2`. -/
private def q3Edges : Finset (Sym2 (Fin 3 → Bool)) :=
  q3Pairs.image (fun q => s(q.1, q.2))

private theorem mem_q3Edges {e : Sym2 (Fin 3 → Bool)} :
    e ∈ q3Edges ↔ ∃ q ∈ q3Pairs, s(q.1, q.2) = e := Finset.mem_image

private theorem q3Pairs_adj {q : (Fin 3 → Bool) × (Fin 3 → Bool)} (hq : q ∈ q3Pairs) :
    Q3.Adj q.1 q.2 := (Finset.mem_filter.mp hq).2

private theorem q3Pairs_mem {u v : Fin 3 → Bool} (huv : Q3.Adj u v) : (u, v) ∈ q3Pairs :=
  Finset.mem_filter.mpr ⟨Finset.mem_univ _, huv⟩

/-- `Q3` has twelve edges. -/
private theorem q3Edges_card : q3Edges.card = 12 := by decide

/-! ### Part M — the weighted first moment (copied verbatim from
`parts/FirstMomentPart.lean`) -/

section PartM

variable {ι : Type*} [DecidableEq ι]

/-- The weights `w S = p ^ S.card * (1 - p) ^ (E.card - S.card)` sum to `1` over all subsets
of `E`.  This is `Finset.sum_pow_mul_eq_add_pow` plus `p + (1 - p) = 1`. -/
theorem weight_total (E : Finset ι) (p : ℝ) (hp₀ : 0 ≤ p) (hp₁ : p ≤ 1) :
    ∑ S ∈ E.powerset, p ^ S.card * (1 - p) ^ (E.card - S.card) = 1 := by
  have hsum : p + (1 - p) = 1 := by ring
  rw [Finset.sum_pow_mul_eq_add_pow, hsum, one_pow]

/-- The mass of the colourings whose red set contains a fixed `T ⊆ E` is exactly
`p ^ T.card`.  Proved by the bijection `S ↦ S \ T` onto `(E \ T).powerset`, with
inverse `S ↦ S ∪ T`, which factors `p ^ T.card` out of the sum. -/
theorem weight_superset (E T : Finset ι) (hT : T ⊆ E) (p : ℝ) (hp₀ : 0 ≤ p) (hp₁ : p ≤ 1) :
    ∑ S ∈ E.powerset.filter (T ⊆ ·), p ^ S.card * (1 - p) ^ (E.card - S.card)
      = p ^ T.card := by
  have key : ∑ S ∈ E.powerset.filter (T ⊆ ·), p ^ S.card * (1 - p) ^ (E.card - S.card)
      = ∑ S ∈ (E \ T).powerset,
          p ^ T.card * (p ^ S.card * (1 - p) ^ ((E \ T).card - S.card)) := by
    refine Finset.sum_nbij' (fun S => S \ T) (fun S => S ∪ T) ?_ ?_ ?_ ?_ ?_
    · intro S hS
      simp only [Finset.mem_filter, Finset.mem_powerset] at hS
      simp only [Finset.mem_powerset]
      exact Finset.subset_sdiff.mpr ⟨Finset.sdiff_subset.trans hS.1, Finset.sdiff_disjoint⟩
    · intro S hS
      simp only [Finset.mem_powerset] at hS
      simp only [Finset.mem_filter, Finset.mem_powerset]
      exact ⟨Finset.union_subset (hS.trans Finset.sdiff_subset) hT, Finset.subset_union_right⟩
    · intro S hS
      simp only [Finset.mem_filter, Finset.mem_powerset] at hS
      exact Finset.sdiff_union_of_subset hS.2
    · intro S hS
      simp only [Finset.mem_powerset] at hS
      show (S ∪ T) \ T = S
      rw [Finset.union_sdiff_right]
      exact Finset.sdiff_eq_self_of_disjoint (Finset.subset_sdiff.mp hS).2
    · intro S hS
      simp only [Finset.mem_filter, Finset.mem_powerset] at hS
      obtain ⟨hSE, hTS⟩ := hS
      have hTScard : T.card ≤ S.card := Finset.card_le_card hTS
      have hSEcard : S.card ≤ E.card := Finset.card_le_card hSE
      have h1 : (S \ T).card = S.card - T.card := Finset.card_sdiff_of_subset hTS
      have h2 : (E \ T).card = E.card - T.card := Finset.card_sdiff_of_subset hT
      have e2 : (E \ T).card - (S \ T).card = E.card - S.card := by omega
      have e1 : S.card = (S \ T).card + T.card := by omega
      rw [e2, e1, pow_add]
      ring
  rw [key, ← Finset.mul_sum, weight_total _ p hp₀ hp₁, mul_one]

/-- The mass of the colourings whose red set avoids a fixed `T ⊆ E` is exactly
`(1 - p) ^ T.card`.  Here the index set is literally `(E \ T).powerset`, and the
factor `(1 - p) ^ T.card` splits off the exponent
`E.card - S.card = ((E \ T).card - S.card) + T.card`. -/
theorem weight_disjoint (E T : Finset ι) (hT : T ⊆ E) (p : ℝ) (hp₀ : 0 ≤ p) (hp₁ : p ≤ 1) :
    ∑ S ∈ E.powerset.filter (fun S => Disjoint S T), p ^ S.card * (1 - p) ^ (E.card - S.card)
      = (1 - p) ^ T.card := by
  have hset : E.powerset.filter (fun S => Disjoint S T) = (E \ T).powerset := by
    ext S
    simp [Finset.mem_filter, Finset.mem_powerset, Finset.subset_sdiff]
  have key : ∀ S ∈ (E \ T).powerset,
      p ^ S.card * (1 - p) ^ (E.card - S.card)
        = (1 - p) ^ T.card * (p ^ S.card * (1 - p) ^ ((E \ T).card - S.card)) := by
    intro S hS
    simp only [Finset.mem_powerset] at hS
    obtain ⟨hSE, hd⟩ := Finset.subset_sdiff.mp hS
    have h2 : (E \ T).card = E.card - T.card := Finset.card_sdiff_of_subset hT
    have hle : S.card + T.card ≤ E.card := by
      rw [← Finset.card_union_of_disjoint hd]
      exact Finset.card_le_card (Finset.union_subset hSE hT)
    have e2 : E.card - S.card = ((E \ T).card - S.card) + T.card := by omega
    rw [e2, pow_add]
    ring
  rw [hset, Finset.sum_congr rfl key, ← Finset.mul_sum, weight_total _ p hp₀ hp₁, mul_one]

end PartM

/-! ### A generic weighted union bound -/

section UnionBound

variable {ι κ : Type*}

/-- Union bound.  If every element of `Bad ⊆ P` satisfies at least one of the
events `Ev k` (`k` ranging over the finite index set `I`), and each event has
mass at most `b` inside `P`, then the mass of `Bad` is at most `I.card * b`. -/
theorem sum_bad_le [DecidableEq ι]
    (P Bad : Finset (Finset ι)) (I : Finset κ)
    (Ev : κ → Finset ι → Prop) [∀ k S, Decidable (Ev k S)]
    (w : Finset ι → ℝ) (hw : ∀ S, 0 ≤ w S)
    (hBad : Bad ⊆ P)
    (hcov : ∀ S ∈ Bad, ∃ k ∈ I, Ev k S)
    (b : ℝ) (hb : ∀ k ∈ I, ∑ S ∈ P.filter (fun S => Ev k S), w S ≤ b) :
    ∑ S ∈ Bad, w S ≤ I.card * b := by
  have hnn : ∀ (k : κ) (S : Finset ι), 0 ≤ (if Ev k S then w S else 0) := by
    intro k S
    split
    · exact hw S
    · exact le_rfl
  have step1 : ∑ S ∈ Bad, w S ≤ ∑ S ∈ Bad, ∑ k ∈ I, (if Ev k S then w S else 0) := by
    refine Finset.sum_le_sum ?_
    intro S hS
    obtain ⟨k, hk, hEv⟩ := hcov S hS
    have h := Finset.single_le_sum (f := fun k => if Ev k S then w S else 0)
      (fun m _ => hnn m S) hk
    simpa [hEv] using h
  have step3 : ∀ k ∈ I, ∑ S ∈ Bad, (if Ev k S then w S else 0) ≤ b := by
    intro k hk
    rw [← Finset.sum_filter]
    refine le_trans (Finset.sum_le_sum_of_subset_of_nonneg ?_ (fun x _ _ => hw x)) (hb k hk)
    exact Finset.filter_subset_filter _ hBad
  calc ∑ S ∈ Bad, w S
      ≤ ∑ S ∈ Bad, ∑ k ∈ I, (if Ev k S then w S else 0) := step1
    _ = ∑ k ∈ I, ∑ S ∈ Bad, (if Ev k S then w S else 0) := Finset.sum_comm
    _ ≤ ∑ k ∈ I, b := Finset.sum_le_sum step3
    _ = I.card * b := by rw [Finset.sum_const, nsmul_eq_mul]

end UnionBound

/-! ### Turning the copy-count hypothesis into a `Finset` bound -/

/-- The number of adjacency-preserving embeddings `Q3 ↪ F` is bounded by the
number of copies of `Q3` in `F`. -/
theorem card_copies_le {N : ℕ} (F : SimpleGraph (Fin N)) [DecidableRel F.Adj]
    (hcopy : Nat.card (SimpleGraph.Copy Q3 F) ≤ (2 * F.edgeSet.ncard) ^ 4) :
    (Finset.univ.filter
        (fun φ : (Fin 3 → Bool) ↪ Fin N => ∀ q ∈ q3Pairs, F.Adj (φ q.1) (φ q.2))).card
      ≤ (2 * F.edgeSet.ncard) ^ 4 := by
  classical
  haveI : Finite (SimpleGraph.Copy Q3 F) :=
    Finite.of_injective (fun f : SimpleGraph.Copy Q3 F => (⇑f : (Fin 3 → Bool) → Fin N))
      DFunLike.coe_injective
  refine le_trans ?_ hcopy
  rw [← Nat.card_eq_finsetCard]
  refine Nat.card_le_card_of_injective
    (fun x => (⟨⟨fun v => (x : (Fin 3 → Bool) ↪ Fin N) v,
        fun {a b} hab => (Finset.mem_filter.mp x.2).2 (a, b) (q3Pairs_mem hab)⟩,
      (x : (Fin 3 → Bool) ↪ Fin N).injective⟩ : SimpleGraph.Copy Q3 F)) ?_
  intro x y hxy
  apply Subtype.ext
  exact DFunLike.ext _ _ (fun a => DFunLike.congr_fun hxy a)

/-! ### The core estimate -/

/-- **Core estimate.**  Assuming the copy-count bound, for every `c ≥ 1` and all
large `n`, no graph `F` with at most `c * C(n,2)` edges arrows `(Q₃, Kₙ)`. -/
theorem no_small_host_of_copy_bound
    (hcopy : ∀ {N : ℕ} (R : SimpleGraph (Fin N)) [DecidableRel R.Adj],
      Nat.card (SimpleGraph.Copy Q3 R) ≤ (2 * R.edgeSet.ncard) ^ 4)
    (c : ℝ) (hc : 1 ≤ c) :
    ∀ᶠ n in Filter.atTop, ∀ (N : ℕ) (F : SimpleGraph (Fin N)),
      (F.edgeSet.ncard : ℝ) ≤ c * (n.choose 2) →
      ¬ (∀ (R : SimpleGraph (Fin N)), R ≤ F →
          Q3.IsContained R ∨ (⊤ : SimpleGraph (Fin n)).IsContained (F \ R)) := by
  classical
  -- The constants.  `B = 2 ^ ⌈c⌉₊` bounds the number of `n`-cliques by `B ^ n`,
  -- and `A` is chosen so that `(1 - A/n) ^ C(n,2)` beats `B ^ n`.
  set C : ℕ := ⌈c⌉₊ with hCdef
  set B : ℕ := 2 ^ C with hBdef
  have hB1 : (1 : ℝ) ≤ (B : ℝ) := by
    rw [hBdef]
    exact_mod_cast Nat.one_le_two_pow
  have hB0 : (0 : ℝ) < (B : ℝ) := by linarith only [hB1]
  have hlogB : 0 ≤ Real.log (B : ℝ) := Real.log_nonneg hB1
  set A : ℝ := 2 * Real.log (B : ℝ) + 4 with hAdef
  have hA4 : (4 : ℝ) ≤ A := by rw [hAdef]; linarith only [hlogB]
  have hA0 : (0 : ℝ) < A := by linarith only [hA4]
  clear_value A B C
  filter_upwards [Filter.eventually_ge_atTop 2,
    Filter.eventually_ge_atTop ⌈A⌉₊,
    Filter.eventually_gt_atTop ⌈2 * c ^ 4 * A ^ 12⌉₊,
    Filter.eventually_ge_atTop ⌈(Real.log (B : ℝ) + 3) / 2⌉₊]
    with n hn2 hnA hnRed hnBlue
  intro N F hMle harrow
  haveI : DecidableRel F.Adj := Classical.decRel _
  -- Numeric preliminaries about `n`.
  have hnR : (2 : ℝ) ≤ (n : ℝ) := by exact_mod_cast hn2
  have hn0 : (0 : ℝ) < (n : ℝ) := by linarith only [hnR]
  have hAn : A ≤ (n : ℝ) := le_trans (Nat.le_ceil A) (by exact_mod_cast hnA)
  have hRedn : 2 * c ^ 4 * A ^ 12 < (n : ℝ) :=
    lt_of_le_of_lt (Nat.le_ceil _) (by exact_mod_cast hnRed)
  have hBluen : (Real.log (B : ℝ) + 3) / 2 ≤ (n : ℝ) :=
    le_trans (Nat.le_ceil _) (by exact_mod_cast hnBlue)
  -- The host's edge set.
  have hncard : F.edgeSet.ncard = F.edgeFinset.card := Set.ncard_eq_toFinset_card' _
  have hMcast : (F.edgeFinset.card : ℝ) ≤ c * (n.choose 2 : ℕ) := by
    rw [← hncard]; exact hMle
  have hchoose2 : ((n.choose 2 : ℕ) : ℝ) = (n : ℝ) * ((n : ℝ) - 1) / 2 := by
    rw [Nat.cast_choose_two]
  -- The bias.
  set p : ℝ := A / (n : ℝ) with hpdef
  have hp0 : 0 ≤ p := by rw [hpdef]; exact div_nonneg hA0.le hn0.le
  have hp1 : p ≤ 1 := by
    rw [hpdef, div_le_one hn0]; exact hAn
  have h1p : (0 : ℝ) ≤ 1 - p := by linarith only [hp1]
  clear_value p
  -- Weights.
  set w : Finset (Sym2 (Fin N)) → ℝ :=
    fun S => p ^ S.card * (1 - p) ^ (F.edgeFinset.card - S.card) with hwdef
  have hwnn : ∀ S, 0 ≤ w S := by
    intro S; rw [hwdef]
    exact mul_nonneg (pow_nonneg hp0 _) (pow_nonneg h1p _)
  -- Red subgraphs, encoded as subsets of the host's edge set.
  have hsubF : ∀ S ∈ F.edgeFinset.powerset,
      SimpleGraph.fromEdgeSet (↑S : Set (Sym2 (Fin N))) ≤ F := by
    intro S hS a b hab
    rw [SimpleGraph.fromEdgeSet_adj] at hab
    have h1 : s(a, b) ∈ S := by simpa using hab.1
    have h2 : s(a, b) ∈ F.edgeFinset := Finset.mem_powerset.mp hS h1
    rw [SimpleGraph.mem_edgeFinset, SimpleGraph.mem_edgeSet] at h2
    exact h2
  -- The two bad families.
  set Red : Finset (Finset (Sym2 (Fin N))) :=
    F.edgeFinset.powerset.filter
      (fun S => Q3.IsContained (SimpleGraph.fromEdgeSet (↑S : Set (Sym2 (Fin N))))) with hReddef
  set Blue : Finset (Finset (Sym2 (Fin N))) :=
    F.edgeFinset.powerset.filter
      (fun S => (⊤ : SimpleGraph (Fin n)).IsContained
        (F \ SimpleGraph.fromEdgeSet (↑S : Set (Sym2 (Fin N))))) with hBluedef
  have hcover : F.edgeFinset.powerset ⊆ Red ∪ Blue := by
    intro S hS
    rcases harrow _ (hsubF S hS) with h | h
    · exact Finset.mem_union_left _ (Finset.mem_filter.mpr ⟨hS, h⟩)
    · exact Finset.mem_union_right _ (Finset.mem_filter.mpr ⟨hS, h⟩)
  have hsplit : (1 : ℝ) ≤ ∑ S ∈ Red, w S + ∑ S ∈ Blue, w S := by
    have hone : ∑ S ∈ F.edgeFinset.powerset, w S = 1 := weight_total _ p hp0 hp1
    have h1 : ∑ S ∈ F.edgeFinset.powerset, w S ≤ ∑ S ∈ Red ∪ Blue, w S :=
      Finset.sum_le_sum_of_subset_of_nonneg hcover (fun x _ _ => hwnn x)
    have h2 : ∑ S ∈ Red ∪ Blue, w S + ∑ S ∈ Red ∩ Blue, w S
        = ∑ S ∈ Red, w S + ∑ S ∈ Blue, w S := Finset.sum_union_inter
    have h3 : 0 ≤ ∑ S ∈ Red ∩ Blue, w S := Finset.sum_nonneg (fun x _ => hwnn x)
    linarith only [hone, h1, h2, h3]
  -- The red mass
  set Copies : Finset ((Fin 3 → Bool) ↪ Fin N) :=
    Finset.univ.filter (fun φ => ∀ q ∈ q3Pairs, F.Adj (φ q.1) (φ q.2)) with hCopiesdef
  set T : ((Fin 3 → Bool) ↪ Fin N) → Finset (Sym2 (Fin N)) :=
    fun φ => q3Edges.image (Sym2.map φ) with hTdef
  have hTcard : ∀ φ : (Fin 3 → Bool) ↪ Fin N, (T φ).card = 12 := by
    intro φ
    rw [hTdef]
    simp only
    rw [Finset.card_image_of_injective _ (Sym2.map.injective φ.injective), q3Edges_card]
  have hTsub : ∀ φ ∈ Copies, T φ ⊆ F.edgeFinset := by
    intro φ hφ e he
    have hφ' : ∀ q ∈ q3Pairs, F.Adj (φ q.1) (φ q.2) := (Finset.mem_filter.mp hφ).2
    rw [hTdef] at he
    simp only [Finset.mem_image] at he
    obtain ⟨e', he', rfl⟩ := he
    obtain ⟨q, hq, rfl⟩ := mem_q3Edges.mp he'
    rw [Sym2.map_pair_eq, SimpleGraph.mem_edgeFinset, SimpleGraph.mem_edgeSet]
    exact hφ' q hq
  have hredcov : ∀ S ∈ Red, ∃ φ ∈ Copies, T φ ⊆ S := by
    intro S hS
    obtain ⟨hSmem, hcon⟩ := Finset.mem_filter.mp hS
    obtain ⟨ψ⟩ := hcon
    refine ⟨ψ.toEmbedding, ?_, ?_⟩
    · rw [hCopiesdef]
      simp only [Finset.mem_filter, Finset.mem_univ, true_and]
      intro q hq
      exact hsubF S hSmem (ψ.toHom.map_rel' (q3Pairs_adj hq))
    · intro e he
      rw [hTdef] at he
      simp only [Finset.mem_image] at he
      obtain ⟨e', he', rfl⟩ := he
      obtain ⟨q, hq, rfl⟩ := mem_q3Edges.mp he'
      have hadj := ψ.toHom.map_rel' (q3Pairs_adj hq)
      rw [SimpleGraph.fromEdgeSet_adj] at hadj
      rw [Sym2.map_pair_eq]
      simpa using hadj.1
  have hredmass : ∑ S ∈ Red, w S ≤ (Copies.card : ℝ) * p ^ 12 := by
    refine sum_bad_le F.edgeFinset.powerset Red Copies (fun φ S => T φ ⊆ S) w hwnn
      (Finset.filter_subset _ _) hredcov (p ^ 12) ?_
    intro φ hφ
    have := weight_superset F.edgeFinset (T φ) (hTsub φ hφ) p hp0 hp1
    rw [hwdef]
    simp only
    rw [this, hTcard φ]
  have hCopiesCard : (Copies.card : ℝ) ≤ (2 * (F.edgeFinset.card : ℝ)) ^ 4 := by
    have h := card_copies_le F (hcopy F)
    rw [hncard] at h
    have h' : (Copies.card : ℝ) ≤ ((2 * F.edgeFinset.card) ^ 4 : ℕ) := by exact_mod_cast h
    simpa using h'
  have hredlt : ∑ S ∈ Red, w S < 1 / 2 := by
    have hMbound : 2 * (F.edgeFinset.card : ℝ) ≤ c * (n : ℝ) ^ 2 := by
      rw [hchoose2] at hMcast
      have h2M : 2 * (F.edgeFinset.card : ℝ) ≤ c * (n : ℝ) * ((n : ℝ) - 1) := by
        linarith only [hMcast]
      have hcn0 : (0 : ℝ) ≤ c * (n : ℝ) := mul_nonneg (by linarith only [hc]) hn0.le
      have hring : c * (n : ℝ) * ((n : ℝ) - 1) = c * (n : ℝ) ^ 2 - c * (n : ℝ) := by ring
      linarith only [h2M, hcn0, hring]
    have hstep1 : (Copies.card : ℝ) * p ^ 12 ≤ (c * (n : ℝ) ^ 2) ^ 4 * p ^ 12 := by
      have h1 : (Copies.card : ℝ) ≤ (c * (n : ℝ) ^ 2) ^ 4 := by
        refine hCopiesCard.trans ?_
        gcongr
      have h2 : (0 : ℝ) ≤ p ^ 12 := pow_nonneg hp0 12
      exact mul_le_mul_of_nonneg_right h1 h2
    have hstep2 : (c * (n : ℝ) ^ 2) ^ 4 * p ^ 12 = c ^ 4 * A ^ 12 / (n : ℝ) ^ 4 := by
      rw [hpdef, div_pow]
      field_simp
    have hstep3 : c ^ 4 * A ^ 12 / (n : ℝ) ^ 4 < 1 / 2 := by
      have hn1 : (1 : ℝ) ≤ (n : ℝ) := by linarith only [hnR]
      have hpow : (n : ℝ) ≤ (n : ℝ) ^ 4 := le_self_pow₀ hn1 (by norm_num)
      have hnum : (0 : ℝ) ≤ c ^ 4 * A ^ 12 :=
        mul_nonneg (pow_nonneg (by linarith only [hc]) 4) (pow_nonneg hA0.le 12)
      have h4 : c ^ 4 * A ^ 12 / (n : ℝ) ^ 4 ≤ c ^ 4 * A ^ 12 / (n : ℝ) :=
        div_le_div_of_nonneg_left hnum hn0 hpow
      have h5 : c ^ 4 * A ^ 12 / (n : ℝ) < 1 / 2 := by
        rw [div_lt_iff₀ hn0]
        linarith only [hRedn]
      linarith only [h4, h5]
    calc ∑ S ∈ Red, w S ≤ (Copies.card : ℝ) * p ^ 12 := hredmass
      _ ≤ (c * (n : ℝ) ^ 2) ^ 4 * p ^ 12 := hstep1
      _ = c ^ 4 * A ^ 12 / (n : ℝ) ^ 4 := hstep2
      _ < 1 / 2 := hstep3
  -- The blue mass
  set D : Finset (Fin N) := Finset.univ.filter (fun v => n - 1 ≤ F.degree v) with hDdef
  set TK : Finset (Fin N) → Finset (Sym2 (Fin N)) :=
    fun K => F.edgeFinset.filter (fun e => ∀ x ∈ e, x ∈ K) with hTKdef
  set Cl : Finset (Finset (Fin N)) :=
    (D.powersetCard n).filter (fun K => n.choose 2 ≤ (TK K).card) with hCldef
  have hTKsub : ∀ K, TK K ⊆ F.edgeFinset := by
    intro K; rw [hTKdef]; exact Finset.filter_subset _ _
  have hbluecov : ∀ S ∈ Blue, ∃ K ∈ Cl, Disjoint S (TK K) := by
    intro S hS
    obtain ⟨hSmem, hcon⟩ := Finset.mem_filter.mp hS
    obtain ⟨ψ⟩ := hcon
    set φ : Fin n ↪ Fin N := ψ.toEmbedding with hφdef
    have hψadj : ∀ a b : Fin n, a ≠ b →
        (F \ SimpleGraph.fromEdgeSet (↑S : Set (Sym2 (Fin N)))).Adj (φ a) (φ b) := by
      intro a b hab
      exact ψ.toHom.map_rel' (by simpa using hab)
    have hFadj : ∀ a b : Fin n, a ≠ b → F.Adj (φ a) (φ b) := by
      intro a b hab
      have h := hψadj a b hab
      rw [SimpleGraph.sdiff_adj] at h
      exact h.1
    set K : Finset (Fin N) := Finset.univ.image φ with hKdef
    have hKcard : K.card = n := by
      rw [hKdef, Finset.card_image_of_injective _ φ.injective, Finset.card_univ,
        Fintype.card_fin]
    have hKD : K ⊆ D := by
      intro v hv
      rw [hKdef] at hv
      simp only [Finset.mem_image, Finset.mem_univ, true_and] at hv
      obtain ⟨a, rfl⟩ := hv
      rw [hDdef]
      simp only [Finset.mem_filter, Finset.mem_univ, true_and]
      have hsub : (Finset.univ.erase a).image φ ⊆ F.neighborFinset (φ a) := by
        intro x hx
        simp only [Finset.mem_image, Finset.mem_erase, Finset.mem_univ, and_true] at hx
        obtain ⟨b, hb, rfl⟩ := hx
        rw [SimpleGraph.mem_neighborFinset]
        exact hFadj a b (Ne.symm hb)
      have hcard : ((Finset.univ.erase a).image φ).card = n - 1 := by
        rw [Finset.card_image_of_injective _ φ.injective, Finset.card_erase_of_mem
          (Finset.mem_univ a), Finset.card_univ, Fintype.card_fin]
      calc n - 1 = ((Finset.univ.erase a).image φ).card := hcard.symm
        _ ≤ (F.neighborFinset (φ a)).card := Finset.card_le_card hsub
        _ = F.degree (φ a) := rfl
    have hTKbig : n.choose 2 ≤ (TK K).card := by
      have hsub : ((⊤ : SimpleGraph (Fin n)).edgeFinset).image (Sym2.map φ) ⊆ TK K := by
        intro e he
        simp only [Finset.mem_image] at he
        obtain ⟨e', he', rfl⟩ := he
        revert he'
        induction e' using Sym2.ind with
        | _ a b =>
          intro he'
          rw [SimpleGraph.mem_edgeFinset, SimpleGraph.mem_edgeSet, SimpleGraph.top_adj] at he'
          rw [hTKdef]
          simp only [Sym2.map_pair_eq, Finset.mem_filter, SimpleGraph.mem_edgeFinset,
            SimpleGraph.mem_edgeSet]
          refine ⟨hFadj a b he', ?_⟩
          intro x hx
          rw [Sym2.mem_iff] at hx
          rw [hKdef]
          rcases hx with rfl | rfl <;>
            simp only [Finset.mem_image, Finset.mem_univ, true_and] <;> [exact ⟨a, rfl⟩; exact ⟨b, rfl⟩]
      have hcard : (((⊤ : SimpleGraph (Fin n)).edgeFinset).image (Sym2.map φ)).card
          = n.choose 2 := by
        rw [Finset.card_image_of_injective _ (Sym2.map.injective φ.injective),
          SimpleGraph.card_edgeFinset_top_eq_card_choose_two, Fintype.card_fin]
      calc n.choose 2 = (((⊤ : SimpleGraph (Fin n)).edgeFinset).image (Sym2.map φ)).card :=
            hcard.symm
        _ ≤ (TK K).card := Finset.card_le_card hsub
    refine ⟨K, ?_, ?_⟩
    · rw [hCldef]
      simp only [Finset.mem_filter, Finset.mem_powersetCard]
      exact ⟨⟨hKD, hKcard⟩, hTKbig⟩
    · rw [Finset.disjoint_left]
      intro e heS heTK
      rw [hTKdef] at heTK
      simp only [Finset.mem_filter] at heTK
      obtain ⟨heF, heK⟩ := heTK
      revert heS heK
      induction e using Sym2.ind with
      | _ x y =>
        intro heS heK
        have hxy : x ≠ y := by
          have := SimpleGraph.not_isDiag_of_mem_edgeSet F (SimpleGraph.mem_edgeFinset.mp heF)
          simpa using this
        have hxK : x ∈ K := heK x (by simp)
        have hyK : y ∈ K := heK y (by simp)
        rw [hKdef] at hxK hyK
        simp only [Finset.mem_image, Finset.mem_univ, true_and] at hxK hyK
        obtain ⟨a, rfl⟩ := hxK
        obtain ⟨b, rfl⟩ := hyK
        have hab : a ≠ b := fun h => hxy (by rw [h])
        have h := hψadj a b hab
        rw [SimpleGraph.sdiff_adj] at h
        refine h.2 ?_
        rw [SimpleGraph.fromEdgeSet_adj]
        exact ⟨by simpa using heS, hxy⟩
  have hbluemass : ∑ S ∈ Blue, w S ≤ (Cl.card : ℝ) * (1 - p) ^ (n.choose 2) := by
    refine sum_bad_le F.edgeFinset.powerset Blue Cl (fun K S => Disjoint S (TK K)) w hwnn
      (Finset.filter_subset _ _) hbluecov ((1 - p) ^ (n.choose 2)) ?_
    intro K hK
    have hbig : n.choose 2 ≤ (TK K).card := (Finset.mem_filter.mp hK).2
    have heq := weight_disjoint F.edgeFinset (TK K) (hTKsub K) p hp0 hp1
    rw [hwdef]
    simp only
    rw [heq]
    exact pow_le_pow_of_le_one h1p (by linarith) hbig
  -- The number of candidate cliques.
  have hDdegsum : D.card * (n - 1) ≤ 2 * F.edgeFinset.card := by
    have h1 : D.card • (n - 1) ≤ ∑ v ∈ D, F.degree v :=
      Finset.card_nsmul_le_sum D (fun v => F.degree v) (n - 1)
        (fun v hv => (Finset.mem_filter.mp hv).2)
    have h2 : ∑ v ∈ D, F.degree v ≤ ∑ v : Fin N, F.degree v :=
      Finset.sum_le_sum_of_subset (Finset.subset_univ D)
    rw [smul_eq_mul] at h1
    have h3 : ∑ v : Fin N, F.degree v = 2 * F.edgeFinset.card :=
      SimpleGraph.sum_degrees_eq_twice_card_edges F
    calc D.card * (n - 1) ≤ ∑ v ∈ D, F.degree v := h1
      _ ≤ ∑ v : Fin N, F.degree v := h2
      _ = 2 * F.edgeFinset.card := h3
  have hDnat : D.card ≤ C * n := by
    have hcastsub : ((n - 1 : ℕ) : ℝ) = (n : ℝ) - 1 := by
      rw [Nat.cast_sub (by omega : 1 ≤ n), Nat.cast_one]
    have h1 : (D.card : ℝ) * ((n : ℝ) - 1) ≤ 2 * (F.edgeFinset.card : ℝ) := by
      have := hDdegsum
      have hcast : ((D.card * (n - 1) : ℕ) : ℝ) ≤ ((2 * F.edgeFinset.card : ℕ) : ℝ) := by
        exact_mod_cast this
      push_cast [hcastsub] at hcast
      linarith only [hcast]
    have h2 : 2 * (F.edgeFinset.card : ℝ) ≤ c * (n : ℝ) * ((n : ℝ) - 1) := by
      rw [hchoose2] at hMcast
      linarith only [hMcast]
    have h3 : (D.card : ℝ) * ((n : ℝ) - 1) ≤ (c * (n : ℝ)) * ((n : ℝ) - 1) := by
      have hassoc : c * (n : ℝ) * ((n : ℝ) - 1) = (c * (n : ℝ)) * ((n : ℝ) - 1) := by ring
      linarith only [h1, h2, hassoc]
    have h4 : (0 : ℝ) < (n : ℝ) - 1 := by linarith only [hnR]
    have h5 : (D.card : ℝ) ≤ c * (n : ℝ) := le_of_mul_le_mul_right h3 h4
    have h6 : c ≤ (C : ℝ) := by rw [hCdef]; exact Nat.le_ceil c
    have h7 : (D.card : ℝ) ≤ ((C * n : ℕ) : ℝ) := by
      have hcn : c * (n : ℝ) ≤ (C : ℝ) * (n : ℝ) :=
        mul_le_mul_of_nonneg_right h6 hn0.le
      have hchain : (D.card : ℝ) ≤ (C : ℝ) * (n : ℝ) := le_trans h5 hcn
      push_cast
      exact hchain
    exact_mod_cast h7
  have hClcard : (Cl.card : ℝ) ≤ (B : ℝ) ^ n := by
    have h1 : Cl.card ≤ (D.powersetCard n).card := Finset.card_filter_le _ _
    have h2 : (D.powersetCard n).card = D.card.choose n := Finset.card_powersetCard _ _
    have h3 : D.card.choose n ≤ B ^ n := by
      calc D.card.choose n ≤ 2 ^ D.card := Nat.choose_le_two_pow _ _
        _ ≤ 2 ^ (C * n) := Nat.pow_le_pow_right (by norm_num) hDnat
        _ = B ^ n := by rw [hBdef, ← pow_mul]
    have h4 : Cl.card ≤ B ^ n := le_trans (h1.trans (le_of_eq h2)) h3
    exact_mod_cast h4
  have hbluelt : ∑ S ∈ Blue, w S < 1 / 2 := by
    have hexpbound : (1 - p) ^ (n.choose 2) ≤ Real.exp (-(A * ((n : ℝ) - 1) / 2)) := by
      have hle : (1 - p) ≤ Real.exp (-p) := by
        have h := Real.add_one_le_exp (-p); linarith only [h]
      calc (1 - p) ^ (n.choose 2) ≤ (Real.exp (-p)) ^ (n.choose 2) := by gcongr
        _ = Real.exp ((n.choose 2 : ℕ) * (-p)) := (Real.exp_nat_mul (-p) _).symm
        _ = Real.exp (-(A * ((n : ℝ) - 1) / 2)) := by
            congr 1
            rw [hchoose2, hpdef]
            field_simp
    have hBexp : (B : ℝ) ^ n = Real.exp ((n : ℝ) * Real.log (B : ℝ)) := by
      rw [Real.exp_nat_mul, Real.exp_log hB0]
    have hprod : (B : ℝ) ^ n * Real.exp (-(A * ((n : ℝ) - 1) / 2))
        = Real.exp ((n : ℝ) * Real.log (B : ℝ) - A * ((n : ℝ) - 1) / 2) := by
      rw [hBexp, ← Real.exp_add]
      ring_nf
    have harg : (n : ℝ) * Real.log (B : ℝ) - A * ((n : ℝ) - 1) / 2 ≤ -1 := by
      have hid : (n : ℝ) * Real.log (B : ℝ) - (2 * Real.log (B : ℝ) + 4) * ((n : ℝ) - 1) / 2
          = Real.log (B : ℝ) - 2 * (n : ℝ) + 2 := by ring
      rw [hAdef, hid]
      linarith only [hBluen]
    have hexp1 : Real.exp (-1 : ℝ) < 1 / 2 := by
      have h2e : (2 : ℝ) < Real.exp 1 := by
        have h := Real.exp_one_gt_d9; linarith only [h]
      rw [Real.exp_neg, inv_eq_one_div, div_lt_div_iff₀ (Real.exp_pos 1) (by norm_num)]
      linarith only [h2e]
    have hfinal : (B : ℝ) ^ n * (1 - p) ^ (n.choose 2) < 1 / 2 := by
      have hBpos : (0 : ℝ) < (B : ℝ) ^ n := pow_pos hB0 n
      calc (B : ℝ) ^ n * (1 - p) ^ (n.choose 2)
          ≤ (B : ℝ) ^ n * Real.exp (-(A * ((n : ℝ) - 1) / 2)) := by
            exact mul_le_mul_of_nonneg_left hexpbound (le_of_lt hBpos)
        _ = Real.exp ((n : ℝ) * Real.log (B : ℝ) - A * ((n : ℝ) - 1) / 2) := hprod
        _ ≤ Real.exp (-1 : ℝ) := Real.exp_le_exp.mpr harg
        _ < 1 / 2 := hexp1
    have hstep : (Cl.card : ℝ) * (1 - p) ^ (n.choose 2) ≤ (B : ℝ) ^ n * (1 - p) ^ (n.choose 2) :=
      mul_le_mul_of_nonneg_right hClcard (pow_nonneg h1p _)
    linarith only [hbluemass, hstep, hfinal]
  linarith only [hsplit, hredlt, hbluelt]

/-- Core estimate: no host with few edges can arrow `(Q3, Kₙ)`. -/
theorem no_small_host (c : ℝ) (hc : 1 ≤ c) :
    ∀ᶠ n in Filter.atTop, ∀ (N : ℕ) (F : SimpleGraph (Fin N)),
      (F.edgeSet.ncard : ℝ) ≤ c * (n.choose 2) →
      ¬ (∀ (R : SimpleGraph (Fin N)), R ≤ F →
          Q3.IsContained R ∨ (⊤ : SimpleGraph (Fin n)).IsContained (F \ R)) :=
  no_small_host_of_copy_bound (fun R => q3_copy_count R) c hc

/-! ### Assembly -/

/-- `Kₙ` has `n.choose 2` edges. -/
theorem top_edgeSet_ncard (n : ℕ) :
    (⊤ : SimpleGraph (Fin n)).edgeSet.ncard = n.choose 2 := by
  classical
  rw [Set.ncard_eq_toFinset_card', ← SimpleGraph.edgeFinset,
    SimpleGraph.card_edgeFinset_top_eq_card_choose_two, Fintype.card_fin]

/-- `Kₙ` has no isolated vertices once `2 ≤ n`. -/
theorem top_degree_pos {n : ℕ} (hn : 2 ≤ n) (v : Fin n) :
    0 < (⊤ : SimpleGraph (Fin n)).degree v := by
  classical
  have : (⊤ : SimpleGraph (Fin n)).degree v = n - 1 := by
    simpa using SimpleGraph.complete_graph_degree (V := Fin n) v
  omega

/-- **The refutation.** -/
theorem not_isRamseySizeLinear_Q3 : ¬ IsRamseySizeLinear Q3 := by
  classical
  rintro ⟨c, hc, h⟩
  -- Enlarging `c` only weakens the hypothesis, so we may assume `1 ≤ c`.
  set c' : ℝ := max c 1 with hc'def
  have hc1 : 1 ≤ c' := le_max_right _ _
  have hcc' : c ≤ c' := le_max_left _ _
  have h' : ∀ (n : ℕ) (H : SimpleGraph (Fin n)) [DecidableRel H.Adj],
      (∀ v, 0 < H.degree v) → (sizeRamsey Q3 H : ℝ) ≤ c' * H.edgeSet.ncard := by
    intro n H _ hH
    refine (h n H hH).trans ?_
    have : (0 : ℝ) ≤ H.edgeSet.ncard := Nat.cast_nonneg _
    nlinarith
  -- Pick `n` large enough for the core estimate, and at least `2`.
  obtain ⟨n, hn, hn2⟩ :=
    ((no_small_host c' hc1).and (Filter.eventually_ge_atTop 2)).exists
  -- The size-Ramsey value is attained by some host `F`.
  obtain ⟨N, F, hFcard, hFarrows⟩ :=
    Nat.sInf_mem (sizeRamsey_set_nonempty n)
  -- That host has few edges, by the assumed linear bound.
  have hbound : (F.edgeSet.ncard : ℝ) ≤ c' * (n.choose 2) := by
    have hle := h' n (⊤ : SimpleGraph (Fin n)) (top_degree_pos hn2)
    rw [top_edgeSet_ncard] at hle
    -- `hFcard` identifies `e(F)` with the size-Ramsey value definitionally.
    rwa [show F.edgeSet.ncard = sizeRamsey Q3 (⊤ : SimpleGraph (Fin n)) from hFcard]
  exact hn N F hbound hFarrows

/-- The bundle's target statement. -/
theorem main : ¬ (True ↔ IsRamseySizeLinear Q3) := by
  intro h
  exact not_isRamseySizeLinear_Q3 (h.mp trivial)

theorem target : ¬ (fcTypeOfName% "Erdos567.erdos_567.parts.i") := main