Trusted statement layer for Sabidussi compatibility

This module contains only the public data and predicates occurring in the headline theorem. It is the trusted import boundary for leanprover/comparator; proof modules build on it, but it does not import them.

structure Sabidussi.LoopMultigraph (V : Type u_1) (E : Type u_2) [Fintype V] [Fintype E] : Type (max u_1 u_2)

A finite labelled endpoint multigraph. Parallel edges and loops are allowed.

• endAt : E → Fin 2 → V

  The two numbered endpoints of each labelled edge.

@[reducible, inline]

abbrev Sabidussi.LoopMultigraph.HalfEdge (E : Type u_3) : Type u_3

A labelled edge together with one of its two numbered ends.

Equations

• Sabidussi.LoopMultigraph.HalfEdge E = (E × Fin 2)

def Sabidussi.LoopMultigraph.vertex {V : Type u_1} {E : Type u_2} [Fintype V] [Fintype E] (G : LoopMultigraph V E) (h : HalfEdge E) : V

The endpoint vertex of a half-edge.

Equations

• G.vertex h = G.endAt h.1 h.2

def Sabidussi.LoopMultigraph.halfEdgesAt {V : Type u_1} {E : Type u_2} [Fintype V] [Fintype E] (G : LoopMultigraph V E) (v : V) : Type u_2

Half-edges incident with a vertex. A loop contributes both of its numbered ends.

Equations

• G.halfEdgesAt v = { h : Sabidussi.LoopMultigraph.HalfEdge E // G.vertex h = v }

@[implicit_reducible]

instance Sabidussi.LoopMultigraph.instFintypeHalfEdgesAt {V : Type u_1} {E : Type u_2} [Fintype V] [Fintype E] [DecidableEq V] (G : LoopMultigraph V E) (v : V) : Fintype (G.halfEdgesAt v)

Equations

• G.instFintypeHalfEdgesAt v = Subtype.fintype fun (h : Sabidussi.LoopMultigraph.HalfEdge E) => G.vertex h = v

def Sabidussi.LoopMultigraph.degree {V : Type u_1} {E : Type u_2} [Fintype V] [Fintype E] [DecidableEq V] (G : LoopMultigraph V E) (v : V) : ℕ

Degree counted in half-edge incidences.

Equations

• G.degree v = Fintype.card (G.halfEdgesAt v)

structure Sabidussi.LoopMultigraph.EulerTour {V : Type u_3} {E : Type u_4} [Fintype V] [Fintype E] (G : LoopMultigraph V E) : Type u_4

A nonempty closed Euler tour using every labelled edge exactly once.

• n : ℕ

  The edge positions are Fin (n + 1).

• edge : Fin (self.n + 1) ≃ E

  Every edge object occurs at exactly one position.

• depart : Fin (self.n + 1) → Fin 2

  The end from which the edge at a position is traversed.

• continuous (i : Fin (self.n + 1)) : G.endAt (self.edge i) (self.depart i).rev = G.endAt (self.edge ((finRotate (self.n + 1)) i)) (self.depart ((finRotate (self.n + 1)) i))

  The arrival end at a position is the departure vertex at the next position.

@[reducible, inline]

abbrev Sabidussi.LoopMultigraph.EulerTour.Pos {V : Type u_3} {E : Type u_4} [Fintype V] [Fintype E] {G : LoopMultigraph V E} (T : G.EulerTour) : Type

Positions in the cyclic edge word.

Equations

• T.Pos = Fin (T.n + 1)

def Sabidussi.LoopMultigraph.EulerTour.next {V : Type u_3} {E : Type u_4} [Fintype V] [Fintype E] {G : LoopMultigraph V E} (T : G.EulerTour) (i : T.Pos) : T.Pos

The next edge position.

Equations

• T.next i = (finRotate (T.n + 1)) i

def Sabidussi.LoopMultigraph.EulerTour.prev {V : Type u_3} {E : Type u_4} [Fintype V] [Fintype E] {G : LoopMultigraph V E} (T : G.EulerTour) (i : T.Pos) : T.Pos

The previous edge position.

Equations

• T.prev i = (Equiv.symm (finRotate (T.n + 1))) i

def Sabidussi.LoopMultigraph.degreeIn {V : Type u_5} {E : Type u_6} [Fintype V] [Fintype E] [DecidableEq V] (G : LoopMultigraph V E) (F : Finset E) (v : V) : ℕ

The ordinary natural-number degree of v in an edge set. Edge ends are counted, so this definition also has the standard behavior for multigraphs.

Equations

• G.degreeIn F v = {h ∈ F ×ˢ Finset.univ | G.endAt h.1 h.2 = v}.card

def Sabidussi.LoopMultigraph.EdgeAdjacent {V : Type u_5} {E : Type u_6} [Fintype V] [Fintype E] (G : LoopMultigraph V E) (e f : E) : Prop

Two labelled edges meet if some numbered end of one has the same endpoint as some numbered end of the other. An edge meets itself, and parallel edges meet at both endpoints.

Equations

• G.EdgeAdjacent e f = ∃ (i : Fin 2) (j : Fin 2), G.endAt e i = G.endAt f j

def Sabidussi.LoopMultigraph.EdgeConnected {V : Type u_5} {E : Type u_6} [Fintype V] [Fintype E] (G : LoopMultigraph V E) (F : Finset E) : Prop

Edge-chain connectivity of a nonempty edge-supported subgraph.

Equations

• G.EdgeConnected F = ∃ root ∈ F, ∀ e ∈ F, Relation.ReflTransGen (fun (x y : E) => x ∈ F ∧ y ∈ F ∧ G.EdgeAdjacent x y) root e

def Sabidussi.LoopMultigraph.edgeSupport {V : Type u_5} {E : Type u_6} [Fintype V] [Fintype E] [DecidableEq V] (G : LoopMultigraph V E) (F : Finset E) : Finset V

The vertices incident with at least one edge of F.

Equations

• G.edgeSupport F = {v : V | ∃ e ∈ F, ∃ (i : Fin 2), G.endAt e i = v}

structure Sabidussi.LoopMultigraph.OrdinaryCircuit {V : Type u_5} {E : Type u_6} [Fintype V] [Fintype E] [DecidableEq V] (G : LoopMultigraph V E) : Type u_6

An ordinary circuit: a nonempty connected edge-supported subgraph in which every supported vertex has degree two.

• edges : Finset E

  The edges of the circuit.

• nonempty : self.edges.Nonempty

  An ordinary circuit is nonempty.

• connected : G.EdgeConnected self.edges

  The circuit is edge-connected.

• twoRegular (v : V) : v ∈ G.edgeSupport self.edges → G.degreeIn self.edges v = 2

  Every supported vertex has ordinary degree two.

structure Sabidussi.LoopMultigraph.OrdinaryCircuitDecomposition {V : Type u_5} {E : Type u_6} [Fintype V] [Fintype E] [DecidableEq V] [DecidableEq E] (G : LoopMultigraph V E) : Type u_6

A partition of all labelled edges into ordinary connected 2-regular circuits.

• circuits : List G.OrdinaryCircuit

  The list of ordinary circuits partitioning the edges.

• coveredOnce (e : E) : (List.filter (fun (C : G.OrdinaryCircuit) => decide (e ∈ C.edges)) self.circuits).length = 1

  Every labelled edge lies in exactly one circuit.

def Sabidussi.LoopMultigraph.OrdinaryCircuitDecomposition.Compatible {V : Type u_5} {E : Type u_6} [Fintype V] [Fintype E] [DecidableEq V] [DecidableEq E] {G : LoopMultigraph V E} (S : G.OrdinaryCircuitDecomposition) (T : G.EulerTour) : Prop

Compatibility stated for ordinary circuits.

Equations

• S.Compatible T = ∀ (i : T.Pos), ∀ C ∈ S.circuits, ¬(T.edge (T.prev i) ∈ C.edges ∧ T.edge i ∈ C.edges)