Main.lean`

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

abbrev OAI.CycleClique.CEAlphaTwo line 192
Source documentation
The Hamiltonicity specialization for graphs with no independent triple.
```
abbrev CEAlphaTwo := Construction.CEAlphaTwo
```
Mentions: OAI.CycleClique.Construction.CEAlphaTwo
theorem OAI.CycleClique.ceAlphaTwo_proved line 195
Source documentation
Chvátal–Erdős Hamiltonicity at order at least six, with independence at most two.
```
theorem ceAlphaTwo_proved : CEAlphaTwo := Construction.ceAlphaTwo_proved
```
Mentions: OAI.CycleClique.CEAlphaTwo, OAI.CycleClique.Construction.ceAlphaTwo_proved
theorem OAI.CycleClique.cycle_clique_main_unconditional line 198
Source documentation
Exact cycle–clique Ramsey numbers away from the exceptional triangle pair.
```
theorem cycle_clique_main_unconditional {m n : ℕ}
    (hn : 3 ≤ n) (hnm : n ≤ m) (hexcept : (m, n) ≠ (3, 3)) :
    IsRamseyNumber m n ((m - 1) * (n - 1) + 1) :=
…
```
Mentions: OAI.CycleClique.IsRamseyNumber
theorem OAI.CycleClique.cycle_clique_ramsey_unconditional line 205
Source documentation
The exact least forcing order, including the exceptional value six.
```
theorem cycle_clique_ramsey_unconditional {m n : ℕ}
    (hn : 3 ≤ n) (hnm : n ≤ m) :
    IsRamseyNumber m n (if m = 3 ∧ n = 3 then 6 else (m - 1) * (n - 1) + 1) :=
…
```
Mentions: OAI.CycleClique.IsRamseyNumber
theorem OAI.CycleClique.cycleCliqueRamsey_unconditional line 212
Source documentation
The labelled construction computes the same Ramsey number as graph containment.
```
theorem cycleCliqueRamsey_unconditional {m n : ℕ} (hn : 3 ≤ n) (hnm : n ≤ m) :
    cycleCliqueRamsey m n =
      if m = 3 ∧ n = 3 then 6 else (m - 1) * (n - 1) + 1 :=
…
```
Mentions: OAI.CycleClique.cycleCliqueRamsey