RamseyReduction.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

The precise minimal-parameter reduction in manuscript Section 2.

theorem OAI.CycleClique.Construction.cycleNext_ne_self line 11
theorem OAI.CycleClique.Construction.complete_hasCycle line 22
theorem OAI.CycleClique.Construction.independent_pair line 35
theorem OAI.CycleClique.Construction.independenceBound_zero line 44
theorem OAI.CycleClique.Construction.independenceBound_one line 53
theorem OAI.CycleClique.Construction.card_lt_of_ramseyProperty line 66
Source documentation
A Ramsey property bounds every larger cycle-free graph with the given independence bound, by restricting it to exactly the forcing order.
```
theorem card_lt_of_ramseyProperty {G : SimpleGraph V} {m n N : ℕ}
    (hRamsey : RamseyProperty m (n + 1) N)
    (hcycle : ¬ HasCycle G m) (hbound : IndependenceBound G n) :
    Fintype.card V < N := by
…
```
Mentions: OAI.CycleClique.Construction.RamseyProperty, OAI.CycleClique.Construction.HasCycle, OAI.CycleClique.Construction.IndependenceBound

theorem OAI.CycleClique.Construction.smaller_parameter_bound line 83

Source documentation

Manuscript Lemma red:smaller, including the zero and one cases.

theorem smaller_parameter_bound {k a b : ℕ} (hk : 3 ≤ k) (hb : b < a)
    (hprior : ∀ c, 2 ≤ c → c < a → RamseyProperty (k + 1) (c + 1) (k * c + 1))
    (G : SimpleGraph V) (hcycle : ¬ HasCycle G (k + 1))
    (hbound : IndependenceBound G b) : Fintype.card V ≤ k * b := by
…

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

theorem OAI.CycleClique.Construction.expansion_of_smaller_ramsey line 98

Source documentation

The expansion premise is supplied by induction on the independence parameter, rather than assumed as an additional graph theorem.

theorem expansion_of_smaller_ramsey {k a : ℕ} (hk : 3 ≤ k)
    (hprior : ∀ b, 2 ≤ b → b < a → RamseyProperty (k + 1) (b + 1) (k * b + 1))
    (G : SimpleGraph V) (hcard : Fintype.card V = k * a + 1)
    (hcycle : ¬ HasCycle G (k + 1)) (hbound : IndependenceBound G a)
    (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.RamseyProperty, OAI.CycleClique.Construction.HasCycle, OAI.CycleClique.Construction.IndependenceBound, OAI.CycleClique.Construction.closedNeighborhood

theorem OAI.CycleClique.Construction.exists_minimal_counterexample line 112

Source documentation

A failure in the main range supplies precisely the expanded graph used by the rest of the manuscript, at the least failed parameter.

theorem exists_minimal_counterexample {k a₀ : ℕ} (hk : 3 ≤ k)
    (ha₀ : 2 ≤ a₀) (ha₀k : a₀ ≤ k)
    (hfail : ¬ RamseyProperty (k + 1) (a₀ + 1) (k * a₀ + 1)) :
    ∃ (a : ℕ) (G : SimpleGraph (Fin (k * a + 1))),
      2 ≤ a ∧ a ≤ k ∧ ¬ HasCycle G (k + 1) ∧ IndependenceBound G a ∧
      ∀ I : Finset (Fin (k * a + 1)),
        G.IsIndepSet (I : Set _) → I.Nonempty →
        k * I.card + 1 ≤ (closedNeighborhood G I).card := by
…

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