Regular Graph Covers and Domination

Abstract

Every finite regular simple graph has a positive-fold cover dominated by one section.

Definition 1.1 (Covering projection and fold).

$$\begin{array}{c}\forall V:\mathrm{Type},W:\mathrm{Type},F:\mathrm{SimpleGraph}\left(V\right),G:\mathrm{SimpleGraph}\left(W\right),p:W\to V,k:\mathbb{N},\\ \mathrm{IsCover}\left(G,F,p,k\right)⟺(\mathrm{Surjective}\left(p\right))\wedge (\forall x:W,\mathrm{BijOn}\left(p,\mathrm{neighborSet}\left(G,x\right),\mathrm{neighborSet}\left(F,p\left(x\right)\right)\right))\wedge (\forall v:V,\mathrm{card}\left(\{x:W\mid p\left(x\right)=v\}\right)=k)\end{array}$$

Formalization. D5/S3/ConceptDynamics/GraphColoring/GraphCoverDomination.IsCover (✓ std3).

Source. Repository-derived.

Commentary.

Here N_H(x) is the open neighborhood, and card is Nat.card. The map is onto, locally bijective, and has a constant fiber size. SimpleGraph supplies symmetry and excludes loops. No connectedness of G is imposed.

Theorem 1.2 (A cover dominated by stars).

$$\begin{array}{c}\forall V:\mathrm{Type},fv:\mathrm{Fintype}\left(V\right),F:\mathrm{SimpleGraph}\left(V\right),dec:\mathrm{DecidableRel}\left(\mathrm{Adj}\left(F\right)\right),d:\mathbb{N},\mathrm{IsRegularOfDegree}\left(F,d\right)\Rightarrow \\ \exists G:\mathrm{SimpleGraph}\left(V\times \mathrm{Option}\left(\mathrm{Fin}\left(d\right)\right)\right),(\mathrm{IsCover}\left(G,F,pr1,(d+1)\right))\wedge (\mathrm{dominationNumber}\left(G\right)\le \mathrm{card}\left(V\right))\end{array}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/GraphColoring/GraphCoverDomination.regular_cover_small_domination (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Walter D. Neumann (2009). On Leighton’s graph covering theorem. DOI: 10.48550/arXiv.0906.2496.

Commentary.

Gamma is the minimum size of a dominating set: every vertex belongs to it or has a neighbor in it. The definitions and minimum lemmas are a scoped licensed source port, identified in the Lean file. For each vertex choose a bijection between its neighbors and Fin d. The matching across an edge pairs each endpoint star with the opposite endpoint port; reverse transport is inverse transport. The stars dominate. Here pr1 denotes Prod.fst and card(V) equals Fintype.card V for a finite type. The port bijections are constructed from regularity, not assumed as an extra hypothesis. Existence of some finite cover admitting a perfect code already follows from the classical common-cover theorem; the present explicit construction is proof engineering.

References

• Truth anchor: D5/S3/ConceptDynamics/GraphColoring/GraphCoverDomination.IsCover
• Truth anchor: D5/S3/ConceptDynamics/GraphColoring/GraphCoverDomination.regular_cover_small_domination