noncomputable def SimpleGraph.distToSet {α : Type u_1} [Fintype α] (G : SimpleGraph α) (v : α) (S : Set α) : ℕ

Distance from a vertex to a finite set.

Equations

• G.distToSet v S = if h : S.toFinset.Nonempty then (Finset.image (fun (s : α) => G.dist v s) S.toFinset).min' ⋯ else 0

noncomputable def SimpleGraph.averageDistance {α : Type u_1} [Fintype α] (G : SimpleGraph α) : ℝ

Average distance of G.

Equations

• G.averageDistance = if Fintype.card α > 1 then (∑ u : α, ∑ v : α, ↑(G.dist u v)) / (↑(Fintype.card α) * (↑(Fintype.card α) - 1)) else 0

def SimpleGraph.isInducedPath {α : Type u_1} (G : SimpleGraph α) (l : List α) : Prop

Check if a list of vertices forms an induced path in G.

Equations

• G.isInducedPath l = (l.Nodup ∧ ∀ (i j : Fin l.length), G.Adj (l.get i) (l.get j) ↔ ↑i + 1 = ↑j ∨ ↑j + 1 = ↑i)

noncomputable def SimpleGraph.path {α : Type u_1} [Fintype α] [DecidableEq α] (G : SimpleGraph α) : ℕ

The path number of a graph: The number of vertices of a largest induced path of the graph.

Equations

• G.path = Option.getD (Finset.image Finset.card {s : Finset α | ∃ (l : List α), l.toFinset = s ∧ G.isInducedPath l}).max 0

noncomputable def SimpleGraph.ecc {α : Type u_1} [Fintype α] (G : SimpleGraph α) (S : Set α) : ℕ

Auxiliary quantity ecc used in conjecture 34.

Equations

• G.ecc S = if h : {v : α | v ∉ S}.Nonempty then (Finset.image (fun (v : α) => G.distToSet v S) {v : α | v ∉ S}).max' ⋯ else 0

noncomputable def SimpleGraph.distMin {α : Type u_1} [Fintype α] (G : SimpleGraph α) (S : Set α) : ℕ

The minimum, over all vertices $v \notin S$, of the distance from $v$ to the set $S$: $\min_{v \notin S} \operatorname{dist}(v, S)$. Returns 0 when $S = \mathrm{univ}$ (no vertex outside $S$).

Counterpart to ecc: the outer minimum (instead of maximum) of the distance-to-set function, restricted to vertices outside $S$.

Equations

• G.distMin S = if h : {v : α | v ∉ S}.Nonempty then (Finset.image (fun (v : α) => G.distToSet v S) {v : α | v ∉ S}).min' ⋯ else 0

noncomputable def SimpleGraph.eccSet {α : Type u_1} [Fintype α] (G : SimpleGraph α) (S : Set α) : ℕ

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 18, 145 and 146.

Equations

• G.eccSet S = if h : (Finset.image (fun (v : α) => G.distToSet v S) Finset.univ).Nonempty then (Finset.image (fun (v : α) => G.distToSet v S) Finset.univ).max' h else 0

noncomputable def SimpleGraph.distavg {α : Type u_1} [Fintype α] (G : SimpleGraph α) (S : Set α) : ℝ

Average distance from all vertices to a given set.

Equations

• G.distavg S = if Fintype.card α > 0 then (∑ v : α, ↑(G.distToSet v S)) / ↑(Fintype.card α) else 0

def SimpleGraph.graphSquare {α : Type u_1} (G : SimpleGraph α) : SimpleGraph α

The square of a graph G, denoted G²: two distinct vertices are adjacent iff their distance in G is at most 2.

Equations

• G.graphSquare = { Adj := fun (u v : α) => u ≠ v ∧ G.dist u v ≤ 2, symm := ⋯, loopless := ⋯ }

noncomputable def SimpleGraph.isInducedC4 {α : Type u_1} (G : SimpleGraph α) [DecidableRel G.Adj] (a b c d : α) : Bool

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.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def SimpleGraph.countInducedC4 {α : Type u_1} [Fintype α] [DecidableEq α] (G : SimpleGraph α) [DecidableRel G.Adj] : ℕ

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.

Equations

• G.countInducedC4 = (∑ a : α, ∑ b : α, ∑ c : α, ∑ d : α, if a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d ∧ G.isInducedC4 a b c d = true then 1 else 0) / 24

def SimpleGraph.bfs_expand {α : Type u_1} [Fintype α] [DecidableEq α] (G : SimpleGraph α) [DecidableRel G.Adj] (S : Finset α) : Finset α

BFS expansion: add all neighbors of S to S.

Equations

• G.bfs_expand S = S ∪ S.biUnion fun (v : α) => Finset.filter (G.Adj v) Finset.univ

def SimpleGraph.bfs_dist_aux {α : Type u_1} [DecidableEq α] [Fintype α] (G : SimpleGraph α) [DecidableRel G.Adj] (target : α) : ℕ → ℕ → Finset α → ℕ

Equations

• G.bfs_dist_aux target 0 x✝¹ x✝ = 0
• G.bfs_dist_aux target fuel.succ x✝¹ x✝ = if target ∈ x✝ then x✝¹ else G.bfs_dist_aux target fuel (x✝¹ + 1) (G.bfs_expand x✝)

def SimpleGraph.computable_dist {α : Type u_1} [Fintype α] [DecidableEq α] (G : SimpleGraph α) [DecidableRel G.Adj] (u v : α) : ℕ

Computable graph distance via BFS. Returns 0 if u = v or if v is unreachable from u.

Equations

• G.computable_dist u v = if u = v then 0 else G.bfs_dist_aux v (Fintype.card α) 1 (G.bfs_expand {u})

def SimpleGraph.computable_avg_dist {α : Type u_1} [Fintype α] [DecidableEq α] (G : SimpleGraph α) [DecidableRel G.Adj] : ℚ

Computable average distance as a rational.

Equations

• G.computable_avg_dist = if Fintype.card α > 1 then (∑ u : α, ∑ v : α, ↑(G.computable_dist u v)) / (↑(Fintype.card α) * (↑(Fintype.card α) - 1)) else 0

theorem SimpleGraph.dist_eq_computable {α : Type u_1} [Fintype α] [DecidableEq α] (G : SimpleGraph α) [DecidableRel G.Adj] (u v : α) : G.dist u v = G.computable_dist u v

theorem SimpleGraph.avg_dist_eq_computable {α : Type u_1} [Fintype α] [DecidableEq α] (G : SimpleGraph α) [DecidableRel G.Adj] : G.averageDistance = ↑G.computable_avg_dist

noncomputable def SimpleGraph.evenDistancePairs {α : Type u_1} [Fintype α] (G : SimpleGraph α) : Finset (α × α)

The set of pairs of distinct vertices with even distance > 0.

Equations

• G.evenDistancePairs = {p : α × α | G.dist p.1 p.2 % 2 = 0 ∧ G.dist p.1 p.2 > 0}

noncomputable def SimpleGraph.minEvenDistance {α : Type u_1} [Fintype α] (G : SimpleGraph α) : ℕ

Minimum even distance between distinct vertices in G. Only positive even distances are considered. Returns 0 if no such distance exists.

Equations

• G.minEvenDistance = if h : G.evenDistancePairs.Nonempty then (Finset.image (fun (p : α × α) => G.dist p.1 p.2) G.evenDistancePairs).min' ⋯ else 0

noncomputable def SimpleGraph.maxEvenDistance {α : Type u_1} [Fintype α] (G : SimpleGraph α) : ℕ

Maximum even distance between distinct vertices in G. Only positive even distances are considered. Returns 0 if no such distance exists.

Equations

• G.maxEvenDistance = if h : G.evenDistancePairs.Nonempty then (Finset.image (fun (p : α × α) => G.dist p.1 p.2) G.evenDistancePairs).max' ⋯ else 0

noncomputable def SimpleGraph.averageEvenDistance {α : Type u_1} [Fintype α] (G : SimpleGraph α) : ℚ

Average even distance between distinct vertices in G. Only positive even distances are considered. Returns 0 if no such distance exists.

Equations

• G.averageEvenDistance = if G.evenDistancePairs.card > 0 then (∑ p ∈ G.evenDistancePairs, ↑(G.dist p.1 p.2)) / ↑G.evenDistancePairs.card else 0