feat(Combinatorics/SimpleGraph/Hamiltonian): the Bondy-Chvátal theorem

[SnirBroshi]

Proves the Bondy-Chvátal theorem and its corollaries, Ore's theorem and Dirac's theorem.

Wikipedia

---

The proof is detailed on the wiki page of Ore's theorem, with a nice illustration.

The wikidata item in 1000.yaml points to Hamiltonian path, but I found one specifically about the theorem.

I'm not sure about the BondyChvatalRel spelling, but it seems more faithful to the "Bondy-Chvátal closure" spelling (on Wikipedia and other places). We could also modify the def to remove self loops (by adding G ≠ G' ∧ ..., or more explicitly u ≠ v ∧ ¬G.Adj u v), prove it has no directed cycles and that it satisfies Church-Rosser, then define the closure of G as the (unique) normal form of it under this relation.

Wikipedia also mentions this theorem about Hamiltonian paths:

/-- **Rahman-Kaykobad theorem**: If for every pair of non-adjacent vertices the sum of their degrees
and the distance between them is greater than the number of vertices, then there exists a
Hamiltonian path. -/
theorem exists_isHamiltonian_of_pairwise_not_adj_imp_card_lt_degree_add_dist {V : Type*}
    [DecidableEq V] [Nonempty V] [Fintype V] {G : SimpleGraph V} [G.LocallyFinite]
    (h : Pairwise fun u v ↦ ¬G.Adj u v → Fintype.card V < G.degree u + G.degree v + G.dist u v) :
    ∃ (u v : V) (p : G.Walk u v), p.IsHamiltonian := by
  sorry

I'm not sure if it's a corollary of Bondy-Chvátal, but I think the proof is similar, so it's a good next target.

• depends on: feat(Combinatorics/SimpleGraph/Hamiltonian): (G ⊔ edge u v).IsHamiltonian iff #41721
• depends on: feat(SimpleGraph): the cycle graph and complete graph are Hamiltonian #34799

[github-actions]

PR summary a5a2cad2ef

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff (regex)

+ BondyChvatalRel
+ isHamiltonian_iff_of_eqvGen_bondyChvatalRel
+ isHamiltonian_of_forall_card_le_two_mul_degree
+ isHamiltonian_of_pairwise_not_adj_imp_card_le_degree_add_degree
+ isHamiltonian_sup_edge
+ isHamiltonian_sup_edge_iff_of_card_le_degree_add_degree
+ isHamiltonian_top
+ support_take_append_support_drop

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit a5a2cad).

• +8 new declarations
• −0 removed declarations

+SimpleGraph.BondyChvatalRel
+SimpleGraph.Walk.support_take_append_support_drop
+SimpleGraph.isHamiltonian_iff_of_eqvGen_bondyChvatalRel
+SimpleGraph.isHamiltonian_of_forall_card_le_two_mul_degree
+SimpleGraph.isHamiltonian_of_pairwise_not_adj_imp_card_le_degree_add_degree
+SimpleGraph.isHamiltonian_sup_edge
+SimpleGraph.isHamiltonian_sup_edge_iff_of_card_le_degree_add_degree
+SimpleGraph.isHamiltonian_top

---

No changes to strong technical debt.

No changes to weak technical debt.

Current commit a5a2cad2ef
Reference commit 9e039082d0

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[SnirBroshi]

FYI #15720 is an attempt from 2 years ago

[mathlib-dependent-issues]

This PR/issue depends on:

• feat(Combinatorics/SimpleGraph/Hamiltonian): (G ⊔ edge u v).IsHamiltonian iff #41721
• feat(SimpleGraph): the cycle graph and complete graph are Hamiltonian #34799
  By Dependent Issues (🤖). Happy coding!