/-
Copyright 2026 The Formal Conjectures Authors.
Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at
https://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/
module
public import Mathlib.Analysis.RCLike.Basic
public import Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite
public import Mathlib.Combinatorics.SimpleGraph.Metric
public import Mathlib.Tactic.IntervalCases
public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Connectivity@[expose] public sectionnamespace SimpleGraphvariable {α : Type*} [Fintype α] [DecidableEq α]Distance from a vertex to a finite set.
noncomputable def distToSet (G : SimpleGraph α) (v : α) (S : Set α) : ℕ :=
open scoped Classical in
if h : S.toFinset.Nonempty then
(S.toFinset.image (fun s => G.dist v s)).min' (Finset.Nonempty.image h _)
else 0
Average distance of G.
noncomputable def averageDistance (G : SimpleGraph α) : ℝ :=
if Fintype.card α > 1 then
(∑ u ∈ Finset.univ, ∑ v ∈ Finset.univ, (G.dist u v : ℝ)) /
((Fintype.card α : ℝ) * ((Fintype.card α : ℝ) - 1))
else
0
Check if a list of vertices forms an induced path in G.
def isInducedPath (G : SimpleGraph α) (l : List α) : Prop :=
l.Nodup ∧ ∀ i j : Fin l.length, G.Adj (l.get i) (l.get j) ↔ i.val + 1 = j.val ∨ j.val + 1 = i.valThe path number of a graph: The number of vertices of a largest induced path of the graph.
noncomputable def path (G : SimpleGraph α) : ℕ :=
open scoped Classical in
let induced_paths := Finset.univ.filter (fun s : Finset α =>
∃ l : List α, l.toFinset = s ∧ isInducedPath G l)
(induced_paths.image Finset.card).max.getD 0
Auxiliary quantity ecc used in conjecture 34.
noncomputable def ecc (G : SimpleGraph α) (S : Set α) : ℕ :=
open scoped Classical in
let s_comp := Finset.univ.filter (fun v => v ∉ S)
if h : s_comp.Nonempty then
(s_comp.image (fun v => distToSet G v S)).max' (Finset.Nonempty.image h _)
else 0
The minimum distance between distinct vertices of $S$:
$\min {\operatorname{dist}_G(u, v) \mid u, v \in S, u \ne v}$. Returns 0 when $S$
contains fewer than two vertices.
noncomputable def distMin (G : SimpleGraph α) (S : Set α) : ℕ :=
open scoped Classical in
let pairs := (S.toFinset ×ˢ S.toFinset).filter (fun p => p.1 ≠ p.2)
if h : pairs.Nonempty then
(pairs.image (fun p => G.dist p.1 p.2)).min' (Finset.Nonempty.image h _)
else 0
The eccentricity of a set S: the maximum, over all vertices v of G, of the
minimum distance from v to any vertex in S. (This includes vertices in S itself,
which contribute distance 0.) Returns 0 when S is empty.
Unlike ecc, which restricts the outer maximum to vertices v ∉ S, eccSet does
not exclude any vertex; it is the conventional definition of "set eccentricity"
used in DeLaVina's WOWII conjectures 142, 145 and 146.
noncomputable def eccSet (G : SimpleGraph α) (S : Set α) : ℕ :=
let dists := Finset.univ.image (fun v => distToSet G v S)
if h : dists.Nonempty then dists.max' h else 0
The maximum distance between two vertices of a set S:
$\operatorname{dist}_{\max}(S) = \max{\operatorname{dist}_G(u,v) \mid u, v \in S}$.
Returns 0 when S is empty or a singleton.
This is DeLaVina's dist_max(S) invariant ("distance between maximum degree
vertices" when S = M), used in WOWII conjecture 18. It is distinct from
eccSet, which measures distances from arbitrary vertices to the set.
noncomputable def distMaxSet (G : SimpleGraph α) (S : Set α) : ℕ :=
open scoped Classical in
let members := Finset.univ.filter (fun v : α => v ∈ S)
(members ×ˢ members).sup (fun p => G.dist p.1 p.2)Average distance from all vertices to a given set.
noncomputable def distavg (G : SimpleGraph α) (S : Set α) : ℝ :=
if Fintype.card α > 0 then
(∑ v ∈ Finset.univ, (distToSet G v S : ℝ)) / (Fintype.card α : ℝ)
else
0
The square of a graph G, denoted G²: two distinct vertices are adjacent
iff their distance in G is at most 2.
def graphSquare (G : SimpleGraph α) : SimpleGraph α where
Adj u v := u ≠ v ∧ G.dist u v ≤ 2
symm.symm _ _ := fun ⟨hne, hd⟩ => ⟨hne.symm, α:Type u_1inst✝¹:Fintype αinst✝:DecidableEq αG:SimpleGraph αx✝²:αx✝¹:αx✝:x✝² ≠ x✝¹ ∧ G.dist x✝² x✝¹ ≤ 2hne:x✝² ≠ x✝¹hd:G.dist x✝² x✝¹ ≤ 2⊢ G.dist x✝¹ x✝² ≤ 2 rwa [α:Type u_1inst✝¹:Fintype αinst✝:DecidableEq αG:SimpleGraph αx✝²:αx✝¹:αx✝:x✝² ≠ x✝¹ ∧ G.dist x✝² x✝¹ ≤ 2hne:x✝² ≠ x✝¹hd:G.dist x✝² x✝¹ ≤ 2⊢ G.dist x✝² x✝¹ ≤ 2α:Type u_1inst✝¹:Fintype αinst✝:DecidableEq αG:SimpleGraph αx✝²:αx✝¹:αx✝:x✝² ≠ x✝¹ ∧ G.dist x✝² x✝¹ ≤ 2hne:x✝² ≠ x✝¹hd:G.dist x✝² x✝¹ ≤ 2⊢ G.dist x✝² x✝¹ ≤ 2⟩
loopless.irrefl v := α:Type u_1inst✝¹:Fintype αinst✝:DecidableEq αG:SimpleGraph αv:α⊢ ¬(v ≠ v ∧ G.dist v v ≤ 2) All goals completed! 🐙
Check whether four distinct vertices form an induced 4-cycle in G.
We test all three perfect-matching pairings of the four vertices to find
a cyclic ordering and verify that the induced subgraph has exactly those 4 edges.
noncomputable def isInducedC4 (G : SimpleGraph α) [DecidableRel G.Adj]
(a b c d : α) : Bool :=
-- Cyclic orderings up to symmetry: (a-b-c-d), (a-b-d-c), (a-c-b-d)
let check (p q r s : α) : Bool :=
G.Adj p q && G.Adj q r && G.Adj r s && G.Adj s p &&
!G.Adj p r && !G.Adj q s
check a b c d || check a b d c || check a c b d
Count of induced C₄ subgraphs of G. We count ordered 4-tuples (a,b,c,d)
of distinct vertices for which isInducedC4 G a b c d = true, then divide by
24 = 4!.
Why 24 (and not 8)? isInducedC4 tests all three perfect-matching
pairings of the four vertices, so any of the 4! = 24 orderings of a fixed
unordered induced 4-cycle satisfies the predicate. Dividing by 8 (the size
of the dihedral group D₄) would overcount each induced 4-cycle by a factor
of 3 — once for each of the three cyclic structures isInducedC4 accepts.
noncomputable def countInducedC4 (G : SimpleGraph α) [DecidableRel G.Adj] : ℕ :=
(∑ a : α, ∑ b : α, ∑ c : α, ∑ d : α,
if a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d ∧
isInducedC4 G a b c d = true then 1 else 0) / 24def bfs_dist_aux (G : SimpleGraph α) [DecidableRel G.Adj] (target : α) : ℕ → ℕ → Finset α → ℕ
| 0, _, _ => 0
| fuel + 1, depth, reached =>
if target ∈ reached then depth
else bfs_dist_aux G target fuel (depth + 1) (G.bfsStep reached)Computable graph distance via BFS. Returns 0 if u = v or if v is unreachable from u.
def computable_dist (G : SimpleGraph α) [DecidableRel G.Adj] (u v : α) : ℕ :=
if u = v then 0
else bfs_dist_aux G v (Fintype.card α) 1 (G.bfsStep {u})
A computable version of distMin for a Finset of vertices.
def computableDistMin (G : SimpleGraph α) [DecidableRel G.Adj] (S : Finset α) : ℕ :=
let pairs := (S ×ˢ S).filter (fun p => p.1 ≠ p.2)
if h : pairs.Nonempty then
(pairs.image (fun p => computable_dist G p.1 p.2)).min' (Finset.Nonempty.image h _)
else 0Computable average distance as a rational.
def computable_avg_dist (G : SimpleGraph α) [DecidableRel G.Adj] : ℚ :=
if Fintype.card α > 1 then
(∑ u ∈ Finset.univ, ∑ v ∈ Finset.univ, (computable_dist G u v : ℚ)) /
((Fintype.card α : ℚ) * ((Fintype.card α : ℚ) - 1))
else 0α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adju:αn:ℕih:∀ w ∈ G.bfsStep^[n] {u}, G.dist u w ≤ nw:αa:αha_mem:a ∈ G.bfsStep^[n] {u}hadj:G.Adj a wha:¬a = uhd:¬G.Reachable u athis:¬G.Reachable u w⊢ 0 ≤ n + 1; All goals completed! 🐙
α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adju:αn:ℕih:∀ w ∈ G.bfsStep^[n] {u}, G.dist u w ≤ nw:αa:αha_mem:a ∈ G.bfsStep^[n] {u}hadj:G.Adj a wha:¬a = uhd:¬G.dist u a = 0⊢ G.dist u w ≤ n + 1 α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adju:αn:ℕih:∀ w ∈ G.bfsStep^[n] {u}, G.dist u w ≤ nw:αa:αha_mem:a ∈ G.bfsStep^[n] {u}hadj:G.Adj a wha:¬a = uhd:¬G.dist u a = 0p:G.Walk u ahp:p.length = G.dist u a⊢ G.dist u w ≤ n + 1
α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adju:αn:ℕih:∀ w ∈ G.bfsStep^[n] {u}, G.dist u w ≤ nw:αa:αha_mem:a ∈ G.bfsStep^[n] {u}hadj:G.Adj a wha:¬a = uhd:¬G.dist u a = 0p:G.Walk u ahp:p.length = G.dist u aha_dist:G.dist u a ≤ n⊢ G.dist u w ≤ n + 1
exact le_trans (dist_le (p.append (.cons hadj .nil)))
(α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adju:αn:ℕih:∀ w ∈ G.bfsStep^[n] {u}, G.dist u w ≤ nw:αa:αha_mem:a ∈ G.bfsStep^[n] {u}hadj:G.Adj a wha:¬a = uhd:¬G.dist u a = 0p:G.Walk u ahp:p.length = G.dist u aha_dist:G.dist u a ≤ n⊢ (p.append (Walk.cons hadj Walk.nil)).length ≤ n + 1 α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adju:αn:ℕih:∀ w ∈ G.bfsStep^[n] {u}, G.dist u w ≤ nw:αa:αha_mem:a ∈ G.bfsStep^[n] {u}hadj:G.Adj a wha:¬a = uhd:¬G.dist u a = 0p:G.Walk u ahp:p.length = G.dist u aha_dist:G.dist u a ≤ n⊢ G.dist u a ≤ n; All goals completed! 🐙)α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adju:αn:ℕih:∀ (w : α), G.dist u w ≤ n → w = u ∨ G.Reachable u w → w ∈ G.bfsStep^[n] {u}w:αhdist:G.dist u w ≤ n + 1hreach:w = u ∨ G.Reachable u whle:¬G.dist u w ≤ nhdist_eq:G.dist u w = n + 1p:G.Walk u whp:p.length = G.dist u whlen:p.length = n + 1this:G.Adj (p.getVert n) (p.getVert (n + 1))⊢ G.Adj (p.getVert n) w
rwa [show n + 1 = p.length from α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adju:αn:ℕih:∀ (w : α), G.dist u w ≤ n → w = u ∨ G.Reachable u w → w ∈ G.bfsStep^[n] {u}w:αhdist:G.dist u w ≤ n + 1hreach:w = u ∨ G.Reachable u whle:¬G.dist u w ≤ nhdist_eq:G.dist u w = n + 1p:G.Walk u whp:p.length = G.dist u whlen:p.length = n + 1this:G.Adj (p.getVert n) (p.getVert (n + 1))⊢ n + 1 = p.length All goals completed! 🐙, α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adju:αn:ℕih:∀ (w : α), G.dist u w ≤ n → w = u ∨ G.Reachable u w → w ∈ G.bfsStep^[n] {u}w:αhdist:G.dist u w ≤ n + 1hreach:w = u ∨ G.Reachable u whle:¬G.dist u w ≤ nhdist_eq:G.dist u w = n + 1p:G.Walk u whp:p.length = G.dist u whlen:p.length = n + 1this:G.Adj (p.getVert n) w⊢ G.Adj (p.getVert n) wα:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adju:αn:ℕih:∀ (w : α), G.dist u w ≤ n → w = u ∨ G.Reachable u w → w ∈ G.bfsStep^[n] {u}w:αhdist:G.dist u w ≤ n + 1hreach:w = u ∨ G.Reachable u whle:¬G.dist u w ≤ nhdist_eq:G.dist u w = n + 1p:G.Walk u whp:p.length = G.dist u whlen:p.length = n + 1this:G.Adj (p.getVert n) w⊢ G.Adj (p.getVert n) w at thisα:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adju:αv:αh:¬u = vfuel:ℕih:∀ (depth : ℕ) (reached : Finset α),
(∀ (w : α), w ∈ reached ↔ w ∈ G.bfsStep^[depth] {u}) →
(∀ d < depth, v ∉ G.bfsStep^[d] {u}) →
fuel + depth ≥ Fintype.card α + 1 → G.bfs_dist_aux v fuel depth reached = G.dist u vdepth:ℕreached:Finset αh_inv:∀ (w : α), w ∈ reached ↔ w ∈ G.bfsStep^[depth] {u}h_not_found:∀ d < depth, v ∉ G.bfsStep^[d] {u}h_fuel:fuel + 1 + depth ≥ Fintype.card α + 1hv:v ∉ reachedh_inv':∀ (w : α), w ∈ G.bfsStep reached ↔ w ∈ G.bfsStep^[depth + 1] {u}⊢ G.bfs_dist_aux v fuel (depth + 1) (G.bfsStep reached) = G.dist u v
exact ih (depth + 1) (G.bfsStep reached) h_inv'
(fun d hd => α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adju:αv:αh:¬u = vfuel:ℕih:∀ (depth : ℕ) (reached : Finset α),
(∀ (w : α), w ∈ reached ↔ w ∈ G.bfsStep^[depth] {u}) →
(∀ d < depth, v ∉ G.bfsStep^[d] {u}) →
fuel + depth ≥ Fintype.card α + 1 → G.bfs_dist_aux v fuel depth reached = G.dist u vdepth:ℕreached:Finset αh_inv:∀ (w : α), w ∈ reached ↔ w ∈ G.bfsStep^[depth] {u}h_not_found:∀ d < depth, v ∉ G.bfsStep^[d] {u}h_fuel:fuel + 1 + depth ≥ Fintype.card α + 1hv:v ∉ reachedh_inv':∀ (w : α), w ∈ G.bfsStep reached ↔ w ∈ G.bfsStep^[depth + 1] {u}d:ℕhd:d < depth + 1⊢ v ∉ G.bfsStep^[d] {u}
α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adju:αv:αh:¬u = vfuel:ℕih:∀ (depth : ℕ) (reached : Finset α),
(∀ (w : α), w ∈ reached ↔ w ∈ G.bfsStep^[depth] {u}) →
(∀ d < depth, v ∉ G.bfsStep^[d] {u}) →
fuel + depth ≥ Fintype.card α + 1 → G.bfs_dist_aux v fuel depth reached = G.dist u vdepth:ℕreached:Finset αh_inv:∀ (w : α), w ∈ reached ↔ w ∈ G.bfsStep^[depth] {u}h_not_found:∀ d < depth, v ∉ G.bfsStep^[d] {u}h_fuel:fuel + 1 + depth ≥ Fintype.card α + 1hv:v ∉ reachedh_inv':∀ (w : α), w ∈ G.bfsStep reached ↔ w ∈ G.bfsStep^[depth + 1] {u}d:ℕhd✝:d < depth + 1hd:d < depth⊢ v ∉ G.bfsStep^[d] {u}α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adju:αv:αh:¬u = vfuel:ℕih:∀ (depth : ℕ) (reached : Finset α),
(∀ (w : α), w ∈ reached ↔ w ∈ G.bfsStep^[depth] {u}) →
(∀ d < depth, v ∉ G.bfsStep^[d] {u}) →
fuel + depth ≥ Fintype.card α + 1 → G.bfs_dist_aux v fuel depth reached = G.dist u vdepth:ℕreached:Finset αh_inv:∀ (w : α), w ∈ reached ↔ w ∈ G.bfsStep^[depth] {u}h_not_found:∀ d < depth, v ∉ G.bfsStep^[d] {u}h_fuel:fuel + 1 + depth ≥ Fintype.card α + 1hv:v ∉ reachedh_inv':∀ (w : α), w ∈ G.bfsStep reached ↔ w ∈ G.bfsStep^[depth + 1] {u}d:ℕhd✝:d < depth + 1hd:d = depth⊢ v ∉ G.bfsStep^[d] {u}
α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adju:αv:αh:¬u = vfuel:ℕih:∀ (depth : ℕ) (reached : Finset α),
(∀ (w : α), w ∈ reached ↔ w ∈ G.bfsStep^[depth] {u}) →
(∀ d < depth, v ∉ G.bfsStep^[d] {u}) →
fuel + depth ≥ Fintype.card α + 1 → G.bfs_dist_aux v fuel depth reached = G.dist u vdepth:ℕreached:Finset αh_inv:∀ (w : α), w ∈ reached ↔ w ∈ G.bfsStep^[depth] {u}h_not_found:∀ d < depth, v ∉ G.bfsStep^[d] {u}h_fuel:fuel + 1 + depth ≥ Fintype.card α + 1hv:v ∉ reachedh_inv':∀ (w : α), w ∈ G.bfsStep reached ↔ w ∈ G.bfsStep^[depth + 1] {u}d:ℕhd✝:d < depth + 1hd:d < depth⊢ v ∉ G.bfsStep^[d] {u} exact h_not_found d (α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adju:αv:αh:¬u = vfuel:ℕih:∀ (depth : ℕ) (reached : Finset α),
(∀ (w : α), w ∈ reached ↔ w ∈ G.bfsStep^[depth] {u}) →
(∀ d < depth, v ∉ G.bfsStep^[d] {u}) →
fuel + depth ≥ Fintype.card α + 1 → G.bfs_dist_aux v fuel depth reached = G.dist u vdepth:ℕreached:Finset αh_inv:∀ (w : α), w ∈ reached ↔ w ∈ G.bfsStep^[depth] {u}h_not_found:∀ d < depth, v ∉ G.bfsStep^[d] {u}h_fuel:fuel + 1 + depth ≥ Fintype.card α + 1hv:v ∉ reachedh_inv':∀ (w : α), w ∈ G.bfsStep reached ↔ w ∈ G.bfsStep^[depth + 1] {u}d:ℕhd✝:d < depth + 1hd:d < depth⊢ d < depth All goals completed! 🐙)
α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adju:αv:αh:¬u = vfuel:ℕih:∀ (depth : ℕ) (reached : Finset α),
(∀ (w : α), w ∈ reached ↔ w ∈ G.bfsStep^[depth] {u}) →
(∀ d < depth, v ∉ G.bfsStep^[d] {u}) →
fuel + depth ≥ Fintype.card α + 1 → G.bfs_dist_aux v fuel depth reached = G.dist u vdepth:ℕreached:Finset αh_inv:∀ (w : α), w ∈ reached ↔ w ∈ G.bfsStep^[depth] {u}h_not_found:∀ d < depth, v ∉ G.bfsStep^[d] {u}h_fuel:fuel + 1 + depth ≥ Fintype.card α + 1hv:v ∉ reachedh_inv':∀ (w : α), w ∈ G.bfsStep reached ↔ w ∈ G.bfsStep^[depth + 1] {u}d:ℕhd✝:d < depth + 1hd:d = depth⊢ v ∉ G.bfsStep^[d] {u} α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adju:αv:αh:¬u = vfuel:ℕih:∀ (depth : ℕ) (reached : Finset α),
(∀ (w : α), w ∈ reached ↔ w ∈ G.bfsStep^[depth] {u}) →
(∀ d < depth, v ∉ G.bfsStep^[d] {u}) →
fuel + depth ≥ Fintype.card α + 1 → G.bfs_dist_aux v fuel depth reached = G.dist u vreached:Finset αhv:v ∉ reachedd:ℕh_inv:∀ (w : α), w ∈ reached ↔ w ∈ G.bfsStep^[d] {u}h_not_found:∀ d_1 < d, v ∉ G.bfsStep^[d_1] {u}h_fuel:fuel + 1 + d ≥ Fintype.card α + 1h_inv':∀ (w : α), w ∈ G.bfsStep reached ↔ w ∈ G.bfsStep^[d + 1] {u}hd:d < d + 1⊢ v ∉ G.bfsStep^[d] {u}; rwa [α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adju:αv:αh:¬u = vfuel:ℕih:∀ (depth : ℕ) (reached : Finset α),
(∀ (w : α), w ∈ reached ↔ w ∈ G.bfsStep^[depth] {u}) →
(∀ d < depth, v ∉ G.bfsStep^[d] {u}) →
fuel + depth ≥ Fintype.card α + 1 → G.bfs_dist_aux v fuel depth reached = G.dist u vreached:Finset αd:ℕhv:v ∉ G.bfsStep^[d] {u}h_inv:∀ (w : α), w ∈ reached ↔ w ∈ G.bfsStep^[d] {u}h_not_found:∀ d_1 < d, v ∉ G.bfsStep^[d_1] {u}h_fuel:fuel + 1 + d ≥ Fintype.card α + 1h_inv':∀ (w : α), w ∈ G.bfsStep reached ↔ w ∈ G.bfsStep^[d + 1] {u}hd:d < d + 1⊢ v ∉ G.bfsStep^[d] {u}α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adju:αv:αh:¬u = vfuel:ℕih:∀ (depth : ℕ) (reached : Finset α),
(∀ (w : α), w ∈ reached ↔ w ∈ G.bfsStep^[depth] {u}) →
(∀ d < depth, v ∉ G.bfsStep^[d] {u}) →
fuel + depth ≥ Fintype.card α + 1 → G.bfs_dist_aux v fuel depth reached = G.dist u vreached:Finset αd:ℕhv:v ∉ G.bfsStep^[d] {u}h_inv:∀ (w : α), w ∈ reached ↔ w ∈ G.bfsStep^[d] {u}h_not_found:∀ d_1 < d, v ∉ G.bfsStep^[d_1] {u}h_fuel:fuel + 1 + d ≥ Fintype.card α + 1h_inv':∀ (w : α), w ∈ G.bfsStep reached ↔ w ∈ G.bfsStep^[d + 1] {u}hd:d < d + 1⊢ v ∉ G.bfsStep^[d] {u} at hv)
(α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adju:αv:αh:¬u = vfuel:ℕih:∀ (depth : ℕ) (reached : Finset α),
(∀ (w : α), w ∈ reached ↔ w ∈ G.bfsStep^[depth] {u}) →
(∀ d < depth, v ∉ G.bfsStep^[d] {u}) →
fuel + depth ≥ Fintype.card α + 1 → G.bfs_dist_aux v fuel depth reached = G.dist u vdepth:ℕreached:Finset αh_inv:∀ (w : α), w ∈ reached ↔ w ∈ G.bfsStep^[depth] {u}h_not_found:∀ d < depth, v ∉ G.bfsStep^[d] {u}h_fuel:fuel + 1 + depth ≥ Fintype.card α + 1hv:v ∉ reachedh_inv':∀ (w : α), w ∈ G.bfsStep reached ↔ w ∈ G.bfsStep^[depth + 1] {u}⊢ fuel + (depth + 1) ≥ Fintype.card α + 1 All goals completed! 🐙)
computableDistMin agrees with distMin on a finite vertex set.
theorem distMin_eq_computableDistMin (G : SimpleGraph α) [DecidableRel G.Adj]
(S : Finset α) : distMin G (S : Set α) = computableDistMin G S := α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.AdjS:Finset α⊢ G.distMin ↑S = G.computableDistMin S
α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.AdjS:Finset α⊢ (let pairs := {p ∈ (↑S).toFinset ×ˢ (↑S).toFinset | p.1 ≠ p.2};
if h : pairs.Nonempty then (Finset.image (fun p ↦ G.dist p.1 p.2) pairs).min' ⋯ else 0) =
let pairs := {p ∈ S ×ˢ S | p.1 ≠ p.2};
if h : pairs.Nonempty then (Finset.image (fun p ↦ G.computable_dist p.1 p.2) pairs).min' ⋯ else 0
α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.AdjS:Finset α⊢ (if h : {p ∈ S ×ˢ S | p.1 ≠ p.2}.Nonempty then (Finset.image (fun p ↦ G.dist p.1 p.2) ({p ∈ S ×ˢ S | p.1 ≠ p.2})).min' ⋯
else 0) =
if h : {p ∈ S ×ˢ S | p.1 ≠ p.2}.Nonempty then
(Finset.image (fun p ↦ G.computable_dist p.1 p.2) ({p ∈ S ×ˢ S | p.1 ≠ p.2})).min' ⋯
else 0
α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.AdjS:Finset αh✝:{p ∈ S ×ˢ S | p.1 ≠ p.2}.Nonempty⊢ (Finset.image (fun p ↦ G.dist p.1 p.2) ({p ∈ S ×ˢ S | p.1 ≠ p.2})).min' ⋯ =
(Finset.image (fun p ↦ G.computable_dist p.1 p.2) ({p ∈ S ×ˢ S | p.1 ≠ p.2})).min' ⋯α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.AdjS:Finset αh✝:¬{p ∈ S ×ˢ S | p.1 ≠ p.2}.Nonempty⊢ 0 = 0
α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.AdjS:Finset αh✝:{p ∈ S ×ˢ S | p.1 ≠ p.2}.Nonempty⊢ (Finset.image (fun p ↦ G.dist p.1 p.2) ({p ∈ S ×ˢ S | p.1 ≠ p.2})).min' ⋯ =
(Finset.image (fun p ↦ G.computable_dist p.1 p.2) ({p ∈ S ×ˢ S | p.1 ≠ p.2})).min' ⋯ α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.AdjS:Finset αh✝:{p ∈ S ×ˢ S | p.1 ≠ p.2}.Nonempty⊢ Finset.image (fun p ↦ G.dist p.1 p.2) ({p ∈ S ×ˢ S | p.1 ≠ p.2}) =
Finset.image (fun p ↦ G.computable_dist p.1 p.2) ({p ∈ S ×ˢ S | p.1 ≠ p.2})
α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.AdjS:Finset αh✝:{p ∈ S ×ˢ S | p.1 ≠ p.2}.Nonemptyn:ℕ⊢ n ∈ Finset.image (fun p ↦ G.dist p.1 p.2) ({p ∈ S ×ˢ S | p.1 ≠ p.2}) ↔
n ∈ Finset.image (fun p ↦ G.computable_dist p.1 p.2) ({p ∈ S ×ˢ S | p.1 ≠ p.2})
α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.AdjS:Finset αh✝:{p ∈ S ×ˢ S | p.1 ≠ p.2}.Nonemptyn:ℕ⊢ (∃ a ∈ {p ∈ S ×ˢ S | p.1 ≠ p.2}, G.dist a.1 a.2 = n) ↔ ∃ a ∈ {p ∈ S ×ˢ S | p.1 ≠ p.2}, G.computable_dist a.1 a.2 = n
α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.AdjS:Finset αh✝:{p ∈ S ×ˢ S | p.1 ≠ p.2}.Nonemptyn:ℕ⊢ (∃ a ∈ {p ∈ S ×ˢ S | p.1 ≠ p.2}, G.dist a.1 a.2 = n) → ∃ a ∈ {p ∈ S ×ˢ S | p.1 ≠ p.2}, G.computable_dist a.1 a.2 = nα:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.AdjS:Finset αh✝:{p ∈ S ×ˢ S | p.1 ≠ p.2}.Nonemptyn:ℕ⊢ (∃ a ∈ {p ∈ S ×ˢ S | p.1 ≠ p.2}, G.computable_dist a.1 a.2 = n) → ∃ a ∈ {p ∈ S ×ˢ S | p.1 ≠ p.2}, G.dist a.1 a.2 = n
α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.AdjS:Finset αh✝:{p ∈ S ×ˢ S | p.1 ≠ p.2}.Nonemptyn:ℕ⊢ (∃ a ∈ {p ∈ S ×ˢ S | p.1 ≠ p.2}, G.dist a.1 a.2 = n) → ∃ a ∈ {p ∈ S ×ˢ S | p.1 ≠ p.2}, G.computable_dist a.1 a.2 = n α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.AdjS:Finset αh✝:{p ∈ S ×ˢ S | p.1 ≠ p.2}.Nonemptyp:α × αhp:p ∈ {p ∈ S ×ˢ S | p.1 ≠ p.2}⊢ ∃ a ∈ {p ∈ S ×ˢ S | p.1 ≠ p.2}, G.computable_dist a.1 a.2 = G.dist p.1 p.2
All goals completed! 🐙
α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.AdjS:Finset αh✝:{p ∈ S ×ˢ S | p.1 ≠ p.2}.Nonemptyn:ℕ⊢ (∃ a ∈ {p ∈ S ×ˢ S | p.1 ≠ p.2}, G.computable_dist a.1 a.2 = n) → ∃ a ∈ {p ∈ S ×ˢ S | p.1 ≠ p.2}, G.dist a.1 a.2 = n α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.AdjS:Finset αh✝:{p ∈ S ×ˢ S | p.1 ≠ p.2}.Nonemptyp:α × αhp:p ∈ {p ∈ S ×ˢ S | p.1 ≠ p.2}⊢ ∃ a ∈ {p ∈ S ×ˢ S | p.1 ≠ p.2}, G.dist a.1 a.2 = G.computable_dist p.1 p.2
All goals completed! 🐙
α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.AdjS:Finset αh✝:¬{p ∈ S ×ˢ S | p.1 ≠ p.2}.Nonempty⊢ 0 = 0 All goals completed! 🐙α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adjh:Fintype.card α > 1hnum:∑ u, ∑ v, ↑(G.dist u v) = ↑(∑ u, ∑ v, ↑(G.computable_dist u v))⊢ ↑(∑ u, ∑ v, ↑(G.computable_dist u v)) / (↑(Fintype.card α) * (↑(Fintype.card α) - 1)) =
↑((∑ u, ∑ v, ↑(G.computable_dist u v)) / (↑(Fintype.card α) * (↑(Fintype.card α) - 1)))
α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adjh:Fintype.card α > 1hnum:∑ u, ∑ v, ↑(G.dist u v) = ↑(∑ u, ∑ v, ↑(G.computable_dist u v))⊢ (∑ x, ∑ x_1, ↑(G.computable_dist x x_1)) / (↑(Fintype.card α) * (↑(Fintype.card α) - 1)) =
(∑ x, ∑ x_1, ↑(G.computable_dist x x_1)) / (↑(Fintype.card α) * (↑(Fintype.card α) - 1))
All goals completed! 🐙
α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adjh:¬Fintype.card α > 1⊢ 0 = ↑0 All goals completed! 🐙
distEven G v counts the vertices at even distance from v in G. This is
DeLaVina's dist_even(v) invariant appearing in several WOWII conjectures.
Distance zero is even, so v itself is always counted.
noncomputable def distEven (G : SimpleGraph α) (v : α) : ℕ :=
(Finset.univ.filter fun w => Even (G.dist v w)).cardThe set of pairs of distinct vertices with even distance > 0.
noncomputable def evenDistancePairs (G : SimpleGraph α) : Finset (α × α) :=
Finset.univ.filter (fun p => G.dist p.1 p.2 % 2 = 0 ∧ G.dist p.1 p.2 > 0)
Minimum even distance between distinct vertices in G.
Only positive even distances are considered. Returns 0 if no such distance exists.
noncomputable def minEvenDistance (G : SimpleGraph α) : ℕ :=
letI pairs := G.evenDistancePairs
if h : pairs.Nonempty then
letI dists := pairs.image (fun p => G.dist p.1 p.2)
(dists.min' (Finset.Nonempty.image h _))
else 0
Maximum even distance between distinct vertices in G.
Only positive even distances are considered. Returns 0 if no such distance exists.
noncomputable def maxEvenDistance (G : SimpleGraph α) : ℕ :=
letI pairs := G.evenDistancePairs
if h : pairs.Nonempty then
letI dists := pairs.image (fun p => G.dist p.1 p.2)
(dists.max' (Finset.Nonempty.image h _))
else 0
Average even distance between distinct vertices in G.
Only positive even distances are considered. Returns 0 if no such distance exists.
noncomputable def averageEvenDistance (G : SimpleGraph α) : ℚ :=
letI pairs := G.evenDistancePairs
if pairs.card > 0 then
(∑ p ∈ pairs, (G.dist p.1 p.2 : ℚ)) / (pairs.card : ℚ)
else 0end SimpleGraph