MinorBound.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The integral Hadwiger bound from pairwise touching matchings.

The small-branch counting argument is Proposition matching-minor of A counterexample to Hadwiger's conjecture, following the connected-matching approach of Cambie.

theorem OAI.HadwigerMatching.small_branch_deficit_le line 21

Source documentation

The singleton and doubleton deficits of an actual clique-minor model are controlled by a touching matching constructed from those very branches.

theorem small_branch_deficit_le {t : ℕ} (B : Fin t → Finset V)
    (hconn : ∀ i, (G.induce (B i : Set V)).Connected)
    (hne : ∀ i, (B i).Nonempty)
    (hdisj : Pairwise (fun i j => Disjoint (B i) (B j)))
    (htouch : ∀ i j, i ≠ j → ∃ v ∈ B i, ∃ w ∈ B j, G.Adj v w) :
    2 * singletonBranchCount B + doubletonBranchCount B ≤
      4 * connectedMatchingNumber G + 2 := by
…

Mentions: OAI.HadwigerMatching.singletonBranchCount, OAI.HadwigerMatching.doubletonBranchCount, OAI.HadwigerMatching.connectedMatchingNumber

theorem OAI.HadwigerMatching.clique_minor_matching_bound line 42
Source documentation
Every clique minor satisfies the integral matching bound.
```
theorem clique_minor_matching_bound {t : ℕ}
    (h : LinearListHadwiger.HasCliqueMinor G t) :
    3 * t ≤ Fintype.card V + 4 * connectedMatchingNumber G + 2 := by
…
```
Mentions: OAI.LinearListHadwiger.HasCliqueMinor, OAI.HadwigerMatching.connectedMatchingNumber
theorem OAI.HadwigerMatching.hadwiger_matching_bound line 53
Source documentation
The maximum is attained by an actual clique-minor branch model. This proves the bound for the literal Hadwiger number, including the empty graph.
```
theorem hadwiger_matching_bound (G : SimpleGraph V) :
    3 * LinearListHadwiger.hadwigerNumber G ≤
      Fintype.card V + 4 * connectedMatchingNumber G + 2 :=
…
```
Mentions: OAI.LinearListHadwiger.hadwigerNumber, OAI.HadwigerMatching.connectedMatchingNumber