Reduction.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Minimal-counterexample deletion and expansion

The argument is Section 2 of Cycle--clique Ramsey numbers. The hypothesis on smaller independence parameters is an induction hypothesis, not a new published input and not a substitute for the upper-bound theorem.

def OAI.CycleClique.Construction.IndependenceBound line 17
Source documentation
Every independent set has at most a vertices.
```
def IndependenceBound (G : SimpleGraph V) (a : ℕ) : Prop :=
…
```
def OAI.CycleClique.Construction.closedNeighborhood line 21
Source documentation
The union of an independent set and all of its neighbours.
```
noncomputable def closedNeighborhood (G : SimpleGraph V) (I : Finset V) : Finset V := by
…
```
theorem OAI.CycleClique.Construction.mem_closedNeighborhood line 25
theorem OAI.CycleClique.Construction.subset_closedNeighborhood line 30
theorem OAI.CycleClique.Construction.independenceBound_iff_not_hasIndependent line 36
theorem OAI.CycleClique.Construction.independent_union_outside line 63
Source documentation
The part of an independent set outside its closed neighbourhood is anticomplete to it, so independent sets in the remainder can be adjoined.
```
theorem independent_union_outside [DecidableEq V] {G : SimpleGraph V} {I J : Finset V}
    (hI : G.IsIndepSet (I : Set V)) (hJ : G.IsIndepSet (J : Set V))
    (hout : ∀ v ∈ J, v ∉ closedNeighborhood G I) :
    G.IsIndepSet ((I ∪ J : Finset V) : Set V) := by
…
```
Mentions: OAI.CycleClique.Construction.closedNeighborhood
theorem OAI.CycleClique.Construction.independent_outside_bound line 78

theorem OAI.CycleClique.Construction.minimal_counterexample_expansion line 104

Source documentation

Independent-set expansion from the smaller-parameter extremal bounds. This is manuscript Lemma red:expansion, with its minimality premise explicit.

theorem minimal_counterexample_expansion {G : SimpleGraph V} {k a : ℕ}
    (hcard : Fintype.card V = k * a + 1)
    (hcycle : ¬ HasCycle G (k + 1)) (hbound : IndependenceBound G a)
    (hsmall : ∀ (b : ℕ), b < a →
      ∀ (Y : Finset V),
        ¬ HasCycle (G.induce (Y : Set V)) (k + 1) →
        IndependenceBound (G.induce (Y : Set V)) b → Y.card ≤ k * b)
    (I : Finset V) (hI : G.IsIndepSet (I : Set V)) (hne : I.Nonempty) :
    k * I.card + 1 ≤ (closedNeighborhood G I).card := by
…

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