Adding self-loops

Powering names a vertex within distance k ≤ h of v by a length-h walk that takes k real steps and then stays put, so the graph it runs on must have a self-loop at every vertex (RegGraph.Loops). This module adds them.

A self-loop at every vertex is itself a RegGraph — loopGraph, of degree one, whose rotation map is the identity — so adding loops is just union with it, and the spectral bound comes free from spectralBound_union: the loops contribute their full weight 1 and the original graph its lam, giving (1 + deg · lam) / (1 + deg), still below one.

On the constraint side the loops carry the trivially true constraint. They are never violated, so the number of broken darts is unchanged while the number of darts grows by a factor (deg + 1) / deg; the value is scaled by exactly deg / (deg + 1), which unsatFrac_addLoops records.

Main definitions

• RegGraph.loopGraph — one self-loop at every vertex
• RegGraph.addLoops, RegGraph.addLoopsLoops — the graph with loops, and its canonical Loops
• RegCSP.addLoops — the constraint system with loops

Main results

• RegGraph.deg_addLoops, RegGraph.spectralBound_addLoops
• RegCSP.unsatFrac_addLoops, unsatVal_addLoops — the value scales by deg / (deg + 1)
• RegCSP.satisfiable_addLoops_iff

def Complexity.RegGraph.loopGraph (V : Type) [DecidableEq V] [Fintype V] : RegGraph

The graph with exactly one self-loop at each vertex.

Equations

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

@[simp]

theorem Complexity.RegGraph.V_loopGraph (V : Type) [DecidableEq V] [Fintype V] : (loopGraph V).V = V

@[simp]

theorem Complexity.RegGraph.deg_loopGraph (V : Type) [DecidableEq V] [Fintype V] : (loopGraph V).deg = 1

def Complexity.RegGraph.addLoops (G : RegGraph) : RegGraph

G with a self-loop added at every vertex.

Equations

• G.addLoops = (Complexity.RegGraph.loopGraph G.V).union G (Equiv.refl G.V)

@[simp]

theorem Complexity.RegGraph.V_addLoops (G : RegGraph) : G.addLoops.V = G.V

@[simp]

theorem Complexity.RegGraph.order_addLoops (G : RegGraph) : G.addLoops.order = G.order

@[simp]

theorem Complexity.RegGraph.deg_addLoops (G : RegGraph) : G.addLoops.deg = 1 + G.deg

def Complexity.RegGraph.addLoopsLoops (G : RegGraph) : G.addLoops.Loops

The canonical self-loop at each vertex of G.addLoops.

Equations

• G.addLoopsLoops = { loop := fun (x : G.addLoops.V) => Sum.inl (), rot_loop := ⋯ }

theorem Complexity.RegGraph.spectralBound_addLoops (G : RegGraph) {lam : ℝ} (hlam : 0 ≤ lam) (h : G.SpectralBound lam) : G.addLoops.SpectralBound ((1 + ↑G.deg * lam) / (1 + ↑G.deg))

Adding loops keeps a spectral bound below one.

theorem Complexity.RegGraph.addLoops_bound_lt_one (G : RegGraph) {lam : ℝ} (hlam1 : lam < 1) : (1 + ↑G.deg * lam) / (1 + ↑G.deg) < 1

def Complexity.RegCSP.addLoops {α : Type} (R : RegCSP α) : RegCSP α

R with a trivially satisfied self-loop added at every vertex.

Equations

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

@[simp]

theorem Complexity.RegCSP.graph_addLoops {α : Type} (R : RegCSP α) : R.addLoops.graph = R.graph.addLoops

theorem Complexity.RegCSP.card_unsatDarts_addLoops {α : Type} (R : RegCSP α) (a : R.Assignment) : (R.addLoops.unsatDarts a).card = (R.unsatDarts a).card

The broken darts are unchanged: only the original constraints can fail.

theorem Complexity.RegCSP.unsatFrac_addLoops {α : Type} (R : RegCSP α) (a : R.Assignment) : R.addLoops.unsatFrac a = R.unsatFrac a * ↑R.graph.deg / (↑R.graph.deg + 1)

Adding loops scales the value by deg / (deg + 1).

theorem Complexity.RegCSP.unsatVal_addLoops {α : Type} (R : RegCSP α) [Fintype α] [Nonempty α] : R.addLoops.unsatVal = R.unsatVal * ↑R.graph.deg / (↑R.graph.deg + 1)

The scaling passes to the value.

theorem Complexity.RegCSP.satisfiable_addLoops_iff {α : Type} (R : RegCSP α) : R.addLoops.Satisfiable ↔ R.Satisfiable