Size.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

The manuscript's size test, conditional on Chvátal–Erdős

An induced vertex set larger than both k and twice the clique number has an independent triple in a graph with no exact (k + 1)-cycle. The only published hypothesis is CEAlphaTwo; the disconnected and cutvertex cases and exact-cycle shortening are proved here.

structure OAI.CycleClique.Construction.TwoCliquePartition line 16
theorem OAI.CycleClique.Construction.two_clique_partition line 26
theorem OAI.CycleClique.Construction.TwoCliquePartition.card line 67
theorem OAI.CycleClique.Construction.connected_of_no_independent_triple line 73
theorem OAI.CycleClique.Construction.joined_clique_card line 85
theorem OAI.CycleClique.Construction.deletion_connected_of_no_independent_triple line 108
theorem OAI.CycleClique.Construction.size_test_graph line 151
Source documentation
The size test on the whole finite graph, conditional only on the published Chvátal–Erdős input.
```
theorem size_test_graph (hCE : CEAlphaTwo) {V : Type} [Fintype V]
    {G : SimpleGraph V} {k t : ℕ} (hk : 5 ≤ k) (ht : 1 ≤ t)
    (hcycle : ¬ HasCycle G (k + 1)) (hclique : G.cliqueNum ≤ t)
    (hcard : max k (2 * t) < Fintype.card V) : HasIndependent G 3 := by
…
```
Mentions: OAI.CycleClique.Construction.CEAlphaTwo, OAI.CycleClique.Construction.HasCycle, OAI.CycleClique.Construction.HasIndependent
theorem OAI.CycleClique.Construction.size_test line 166
Source documentation
Manuscript Lemma size:test: every sufficiently large vertex set contains three independent vertices.
```
theorem size_test (hCE : CEAlphaTwo) {V : Type} [Fintype V]
    {G : SimpleGraph V} {k t : ℕ} (hk : 5 ≤ k) (ht : 1 ≤ t)
    (hcycle : ¬ HasCycle G (k + 1)) (hclique : G.cliqueNum ≤ t)
    (Y : Finset V) (hY : max k (2 * t) < Y.card) :
    HasIndependent (G.induce (Y : Set V)) 3 := by
…
```
Mentions: OAI.CycleClique.Construction.CEAlphaTwo, OAI.CycleClique.Construction.HasCycle, OAI.CycleClique.Construction.HasIndependent