LowerBound.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

The disjoint-clique lower bound

The red graph consists of a disjoint complete graphs of order k. A red cycle stays within one block, while an independent set uses at most one vertex from each block. This is the lower-bound construction in the proof of Theorem 1 of Cycle--clique Ramsey numbers.

def OAI.CycleClique.Construction.blockGraph line 17
Source documentation
Disjoint red cliques: the first coordinate records the block.
```
def blockGraph (a k : ℕ) : SimpleGraph (Fin a × Fin k) where
…
```
theorem OAI.CycleClique.Construction.blockGraph_adj line 22
theorem OAI.CycleClique.Construction.cycleNext_castSucc line 25
theorem OAI.CycleClique.Construction.blockGraph_cycle_bound line 31
Source documentation
Every red cycle in the disjoint-clique construction lies in a single block.
```
theorem blockGraph_cycle_bound {a k m : ℕ} (hm : 0 < m)
    (h : HasCycle (blockGraph a k) m) : m ≤ k := by
…
```
Mentions: OAI.CycleClique.Construction.HasCycle, OAI.CycleClique.Construction.blockGraph
theorem OAI.CycleClique.Construction.blockGraph_independent_bound line 50
Source documentation
An independent set uses at most one vertex in every block.
```
theorem blockGraph_independent_bound {a k n : ℕ}
    (h : HasIndependent (blockGraph a k) n) : n ≤ a := by
…
```
Mentions: OAI.CycleClique.Construction.HasIndependent, OAI.CycleClique.Construction.blockGraph
theorem OAI.CycleClique.Construction.blockGraph_not_ramsey line 60
Source documentation
The lower-bound coloring on a linearly labelled set of k * a vertices.
```
theorem blockGraph_not_ramsey {a k m n : ℕ} (hkm : k < m) (han : a < n) :
    ¬ RamseyProperty m n (k * a) := by
…
```
Mentions: OAI.CycleClique.Construction.RamseyProperty
theorem OAI.CycleClique.Construction.cycle_clique_lower_bound line 77
Source documentation
The sharp lower bound in the manuscript's main parameter range.
```
theorem cycle_clique_lower_bound {m n : ℕ} (hm : 3 ≤ m) (hn : 3 ≤ n) :
    ¬ RamseyProperty m n ((m - 1) * (n - 1)) := by
…
```
Mentions: OAI.CycleClique.Construction.RamseyProperty