TriangleFacts.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

The elementary six-vertex argument and the complementary pentagons prove R(C₃,K₃) = 6, the exceptional clause of the manuscript's main theorem.

theorem OAI.CycleClique.Construction.hasCycle_three_of_edges line 15
theorem OAI.CycleClique.Construction.hasIndependent_three_of_distinct_nonadjacent line 26
theorem OAI.CycleClique.Construction.triangle_upper line 40
Source documentation
Every graph on six vertices has a triangle or three independent vertices.
```
theorem triangle_upper : RamseyProperty 3 3 6 := by
…
```
Mentions: OAI.CycleClique.Construction.RamseyProperty
def OAI.CycleClique.Construction.pentagon line 78
Source documentation
The pentagon coloring: red edges have cyclic difference one.
```
def pentagon : SimpleGraph (Fin 5) where
…
```
instance OAI.CycleClique.Construction.(instance at line 83) line 83
theorem OAI.CycleClique.Construction.pentagon_no_triangle line 85
theorem OAI.CycleClique.Construction.pentagon_no_independent_triple line 89
theorem OAI.CycleClique.Construction.triangle_lower line 96
Source documentation
Five vertices do not force a monochromatic triangle.
```
theorem triangle_lower : ¬ RamseyProperty 3 3 5 := by
…
```
Mentions: OAI.CycleClique.Construction.RamseyProperty