Well-covered powers with unbounded diameter

Abstract

Cartesian products with a sufficiently large clique preserve well-covered powers and increase the diameter by one. Starting from the seven-cycle gives arbitrary diameters at least three.

Definition 1.1 (Graph powers).

$$\forall V\in \mathrm{Type},[\mathrm{Fintype}\left(V\right)],[\mathrm{DecidableEq}\left(V\right)],\forall G\in \mathrm{SimpleGraph}\left(V\right),\forall d\in \mathrm{Nat},\forall u\in V,\forall v\in V,\mathrm{Adj}\left(\mathrm{power}\left(G,d\right),u,v\right)\iff \left(u\ne v\wedge \mathrm{dist}\left(G,u,v\right)\le d\right)$$

Formalization. D5/S3/Combinatorics/Graph/WellCoveredPowerCliqueProduct.power (✓ std3).

Source. Repository-derived.

Commentary.

The d-th power joins distinct vertices whose graph distance is at most d. Only connected finite graphs are used.

Definition 1.2 (Maximal independent finite sets).

$$\forall V\in \mathrm{Type},[\mathrm{Fintype}\left(V\right)],[\mathrm{DecidableEq}\left(V\right)],\forall G\in \mathrm{SimpleGraph}\left(V\right),\forall I\in \mathrm{Finset}\left(V\right),\mathrm{IsMaximalIndep}\left(G,I\right)\iff \left(\left(\forall u\in V,\mathrm{mem}\left(u,I\right)\Rightarrow \left(\forall v\in V,\left(\mathrm{mem}\left(v,I\right)\wedge u\ne v\right)\Rightarrow \left(\neg \mathrm{Adj}\left(G,u,v\right)\right)\right)\right)\wedge \left(\forall v\in V,\left(\neg \mathrm{mem}\left(v,I\right)\right)\Rightarrow \left(\exists u\in V,\mathrm{mem}\left(u,I\right)\wedge \mathrm{Adj}\left(G,v,u\right)\right)\right)\right)$$

Formalization. D5/S3/Combinatorics/Graph/WellCoveredPowerCliqueProduct.IsMaximalIndep (✓ std3).

Source. Repository-derived.

Commentary.

The set is independent and every vertex outside it has a neighbor inside it. This is precisely maximality under inclusion.

Definition 1.3 (Well-covered graphs).

$$\forall V\in \mathrm{Type},[\mathrm{Fintype}\left(V\right)],[\mathrm{DecidableEq}\left(V\right)],\forall G\in \mathrm{SimpleGraph}\left(V\right),\mathrm{WellCovered}\left(G\right)\iff \left(\forall I\in \mathrm{Finset}\left(V\right),\forall J\in \mathrm{Finset}\left(V\right),\left(\mathrm{IsMaximalIndep}\left(G,I\right)\wedge \mathrm{IsMaximalIndep}\left(G,J\right)\right)\Rightarrow \mathrm{card}\left(I\right)=\mathrm{card}\left(J\right)\right)$$

Formalization. D5/S3/Combinatorics/Graph/WellCoveredPowerCliqueProduct.WellCovered (✓ std3).

Source. Repository-derived.

Commentary.

Any two maximal independent finite sets have equal cardinalities, equivalently all minimal vertex covers have the same cardinality.

Definition 1.4 (Connected graphs with well-covered powers).

$$\forall V\in \mathrm{Type},[\mathrm{Fintype}\left(V\right)],[\mathrm{DecidableEq}\left(V\right)],\forall G\in \mathrm{SimpleGraph}\left(V\right),\mathrm{WCP}\left(G\right)\iff \left(\mathrm{Connected}\left(G\right)\wedge \left(\forall d\in \mathrm{Nat},1\le d\Rightarrow \mathrm{WellCovered}\left(\mathrm{power}\left(G,d\right)\right)\right)\right)$$

Formalization. D5/S3/Combinatorics/Graph/WellCoveredPowerCliqueProduct.WCP (✓ std3).

Source. Repository-derived.

Commentary.

The graph is connected and its d-th power is well-covered for every positive integer d.

Theorem 1.5 (Distance in a clique product).

$$\forall V\in \mathrm{Type},[\mathrm{Fintype}\left(V\right)],[\mathrm{DecidableEq}\left(V\right)],\forall G\in \mathrm{SimpleGraph}\left(V\right),\forall t\in \mathrm{Nat},\mathrm{Connected}\left(G\right)\Rightarrow \left(\forall x\in \mathrm{Prod}\left(V,\mathrm{Fin}\left(t\right)\right),\forall y\in \mathrm{Prod}\left(V,\mathrm{Fin}\left(t\right)\right),\mathrm{dist}\left(\mathrm{boxProd}\left(G,\mathrm{completeGraph}\left(\mathrm{Fin}\left(t\right)\right)\right),x,y\right)=\mathrm{dist}\left(G,\mathrm{fst}\left(x\right),\mathrm{fst}\left(y\right)\right)+\mathrm{if}\left(\mathrm{snd}\left(x\right)=\mathrm{snd}\left(y\right),0,1\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Graph/WellCoveredPowerCliqueProduct.distance_cliqueProduct (✓ std3). ∎

Source. Repository-derived.

Commentary.

In G □ K_t the distance from (u,a) to (v,b) is dist_G(u,v) plus zero when a=b and one otherwise.

Theorem 1.6 (Maximality survives projection).

$$\forall V\in \mathrm{Type},[\mathrm{Fintype}\left(V\right)],[\mathrm{DecidableEq}\left(V\right)],\forall G\in \mathrm{SimpleGraph}\left(V\right),\forall t\in \mathrm{Nat},\forall d\in \mathrm{Nat},\forall I\in \mathrm{Finset}\left(\mathrm{Prod}\left(V,\mathrm{Fin}\left(t\right)\right)\right),\left(\mathrm{Connected}\left(G\right)\wedge \left(\mathrm{LT}\left(\mathrm{FintypeCard}\left(V\right),t\right)\wedge \left(1\le d\wedge \mathrm{IsMaximalIndep}\left(\mathrm{power}\left(\mathrm{boxProd}\left(G,\mathrm{completeGraph}\left(\mathrm{Fin}\left(t\right)\right)\right),d\right),I\right)\right)\right)\right)\Rightarrow \mathrm{IsMaximalIndep}\left(\mathrm{power}\left(G,d-1\right),\mathrm{imageFst}\left(I\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Graph/WellCoveredPowerCliqueProduct.projection_maximal (✓ std3). ∎

Source. Repository-derived.

Commentary.

For d at least one and t greater than the number of vertices of G, a maximal independent set of (G □ K_t)^d projects to a maximal independent set of G^(d-1). If an omitted base vertex could be added, choose a clique label absent from the original set. Its distance to every selected point is then greater than d, contradicting maximality.

Theorem 1.7 (Clique products preserve well-covered powers).

$$\forall V\in \mathrm{Type},[\mathrm{Fintype}\left(V\right)],[\mathrm{DecidableEq}\left(V\right)],\forall G\in \mathrm{SimpleGraph}\left(V\right),\forall t\in \mathrm{Nat},\left(\mathrm{WCP}\left(G\right)\wedge \mathrm{LT}\left(\mathrm{FintypeCard}\left(V\right),t\right)\right)\Rightarrow \mathrm{WCP}\left(\mathrm{boxProd}\left(G,\mathrm{completeGraph}\left(\mathrm{Fin}\left(t\right)\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Graph/WellCoveredPowerCliqueProduct.wcp_cliqueProduct (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let G be a finite connected graph all of whose positive powers are well-covered. If t exceeds its order, then G □ K_t also has this property. Projection is injective on each independent set and preserves cardinality. The zero-th power is edgeless and has a single maximal independent set.

Theorem 1.8 (Clique products increase diameter).

$$\forall V\in \mathrm{Type},[\mathrm{Fintype}\left(V\right)],[\mathrm{DecidableEq}\left(V\right)],\forall G\in \mathrm{SimpleGraph}\left(V\right),\forall t\in \mathrm{Nat},\left(\mathrm{Connected}\left(G\right)\wedge 2\le t\right)\Rightarrow \mathrm{diam}\left(\mathrm{boxProd}\left(G,\mathrm{completeGraph}\left(\mathrm{Fin}\left(t\right)\right)\right)\right)=\mathrm{diam}\left(G\right)+1$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Graph/WellCoveredPowerCliqueProduct.diam_cliqueProduct (✓ std3). ∎

Source. Repository-derived.

Commentary.

If t is at least two, the diameter of G □ K_t is diam(G)+1. A pair attaining diam(G), equipped with two different clique labels, attains this bound.

Theorem 1.9 (The seven-cycle has well-covered powers).

$$\mathrm{WCP}\left(\mathrm{cycle}\left(7\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Graph/WellCoveredPowerCliqueProduct.cycle_seven_wcp (✓ std3). ∎

Source. Repository-derived.

Commentary.

The cyclic distance on Fin 7 is min(|u-v|,7-|u-v|). It gives the seven-cycle. The maximal independent sets of its first, second and third powers have cardinalities three, two and one. All higher powers equal the third.

Theorem 1.10 (Every diameter at least three occurs).

$$\forall D\in \mathrm{Nat},3\le D\Rightarrow \left(\exists V\in \mathrm{Type},\exists [\mathrm{Fintype}\left(V\right)],\exists [\mathrm{DecidableEq}\left(V\right)],\exists G\in \mathrm{SimpleGraph}\left(V\right),\mathrm{WCP}\left(G\right)\wedge \mathrm{diam}\left(G\right)=D\right)$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Graph/WellCoveredPowerCliqueProduct.exists_wcp_diameter (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every natural number D at least three there exists a finite connected graph with well-covered positive powers and diameter D. The initial graph is the seven-cycle. At each step take the Cartesian product with the clique of order one greater than the current graph’s order.

Definition 1.11 (The proposed diameter bound).

$$claim\iff \left(\forall V\in \mathrm{Type},[\mathrm{Fintype}\left(V\right)],[\mathrm{DecidableEq}\left(V\right)],\forall G\in \mathrm{SimpleGraph}\left(V\right),[\mathrm{DecidableRel}\left(\mathrm{Adj}\left(G\right)\right)],\mathrm{WCP}\left(G\right)\Rightarrow \mathrm{diam}\left(G\right)\le 3\right)$$

Formalization. D5/S3/Combinatorics/Graph/WellCoveredPowerCliqueProduct.claim (✓ std3).

Source. Repository-derived.

Commentary.

Question 3.9 asks: Let G be a simple connected graph such that G^d is well-covered for all d at least one. Is it true that diam(G) is at most three? The quantified statement ranges over every finite vertex type and every simple graph on it.

Theorem 1.12 (The diameter bound is false).

$$\neg claim$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Graph/WellCoveredPowerCliqueProduct.result (✓ std3). ∎

Resolves. Problems/pham-vu-2026-well-covered-powers-diameter (refuted) by D5/S3/Combinatorics/Graph/WellCoveredPowerCliqueProduct.result.

Source. Repository-derived.

Commentary.

The seven-cycle □ K_8 has 56 vertices, well-covered positive powers and diameter four. It refutes the proposed bound.

References

• Truth anchor: D5/S3/Combinatorics/Graph/WellCoveredPowerCliqueProduct.IsMaximalIndep
• Truth anchor: D5/S3/Combinatorics/Graph/WellCoveredPowerCliqueProduct.WCP
• Truth anchor: D5/S3/Combinatorics/Graph/WellCoveredPowerCliqueProduct.WellCovered
• Truth anchor: D5/S3/Combinatorics/Graph/WellCoveredPowerCliqueProduct.claim
• Truth anchor: D5/S3/Combinatorics/Graph/WellCoveredPowerCliqueProduct.cycle_seven_wcp
• Truth anchor: D5/S3/Combinatorics/Graph/WellCoveredPowerCliqueProduct.diam_cliqueProduct
• Truth anchor: D5/S3/Combinatorics/Graph/WellCoveredPowerCliqueProduct.distance_cliqueProduct
• Truth anchor: D5/S3/Combinatorics/Graph/WellCoveredPowerCliqueProduct.exists_wcp_diameter
• Truth anchor: D5/S3/Combinatorics/Graph/WellCoveredPowerCliqueProduct.power
• Truth anchor: D5/S3/Combinatorics/Graph/WellCoveredPowerCliqueProduct.projection_maximal
• Truth anchor: D5/S3/Combinatorics/Graph/WellCoveredPowerCliqueProduct.result
• Truth anchor: D5/S3/Combinatorics/Graph/WellCoveredPowerCliqueProduct.wcp_cliqueProduct