LargeClique.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The initial clique bounds

The triangle bound is manuscript Lemma clq:triangle. Its proof below establishes the elementary triangle Ramsey recurrence directly, without assuming any cycle–clique Ramsey theorem.

theorem OAI.CycleClique.Construction.cycleNext_ne line 15
theorem OAI.CycleClique.Construction.clique_contains_cycle line 28
Source documentation
A clique contains a cycle through any specified number of at least three of its vertices.
```
theorem clique_contains_cycle {V : Type*} {G : SimpleGraph V} {Q : Finset V} {m : ℕ}
    (hm : 3 ≤ m) (hQ : G.IsClique (Q : Set V)) (hcard : m ≤ Q.card) : HasCycle G m := by
…
```
Mentions: OAI.CycleClique.Construction.HasCycle
theorem OAI.CycleClique.Construction.triangle_free_order_bound line 43
Source documentation
The elementary triangle Ramsey bound, in doubled form to avoid division: a triangle-free graph of independence number at most a has at most a * (a + 3) / 2 vertices.
```
theorem triangle_free_order_bound (a : ℕ) :
    ∀ {V : Type*} [Fintype V] {G : SimpleGraph V},
      IndependenceBound G a → ¬ HasCycle G 3 →
      2 * Fintype.card V ≤ a * (a + 3) := by
…
```
Mentions: OAI.CycleClique.Construction.IndependenceBound, OAI.CycleClique.Construction.HasCycle
theorem OAI.CycleClique.Construction.cliqueNum_le_of_no_cycle line 88
Source documentation
A cycle-free graph has no clique larger than the forbidden cycle order.
```
theorem cliqueNum_le_of_no_cycle {V : Type*} [Fintype V] {G : SimpleGraph V}
    {k : ℕ} (hk : 2 ≤ k) (hcycle : ¬ HasCycle G (k + 1)) : G.cliqueNum ≤ k := by
…
```
Mentions: OAI.CycleClique.Construction.HasCycle

theorem OAI.CycleClique.Construction.triangle_clique_bounds line 97

Source documentation

Manuscript Lemma clq:triangle, valid before using expansion.

theorem triangle_clique_bounds {V : Type*} [Fintype V] {G : SimpleGraph V}
    {k a : ℕ} (hk : 3 ≤ k) (_ha : 2 ≤ a) (hak : a ≤ k)
    (hcard : Fintype.card V = k * a + 1)
    (hI : IndependenceBound G a) (hcycle : ¬ HasCycle G (k + 1)) :
    3 ≤ G.cliqueNum ∧ G.cliqueNum ≤ k := by
…

Mentions: OAI.CycleClique.Construction.IndependenceBound, OAI.CycleClique.Construction.HasCycle

theorem OAI.CycleClique.Construction.large_clique_small_k line 120

Source documentation

For the first five cycle lengths, the triangle already gives the complete quantitative clique bound of Theorem clq:bound.

theorem large_clique_small_k {V : Type*} [Fintype V] {G : SimpleGraph V}
    {k a : ℕ} (hk : 3 ≤ k) (hk7 : k ≤ 7) (ha : 2 ≤ a) (hak : a ≤ k)
    (hcard : Fintype.card V = k * a + 1)
    (hI : IndependenceBound G a) (hcycle : ¬ HasCycle G (k + 1)) :
    max 3 (k / 2) ≤ G.cliqueNum ∧ G.cliqueNum ≤ k := by
…

Mentions: OAI.CycleClique.Construction.IndependenceBound, OAI.CycleClique.Construction.HasCycle