Euler circuits and single dual circuits for planar contours

7 fully proved

A. Closed trails and splicing

LemmaDegree of a vertex equals the number of edges containing it#✓fully proved

The degree of a vertex is the number of edges containing it. See also SimpleGraph.card_incidenceFinset_eq_degree.

lemma degree_eq_card_filter_edges (G : SimpleGraph V) [DecidableRel G.Adj] (x : V) :
    G.degree x = (G.edgeFinset.filter (fun e => x ∈ e)).card

Used by 1

Used byEuler's theorem

DefinitionSplicing a closed walk into another at a shared vertex#✓fully proved

Splice a closed walk c at a vertex w of the closed walk p into p.

noncomputable def spliceWalk (G : SimpleGraph V) {u w : V} (p : G.Walk u u)
    (hw : w ∈ p.support) (c : G.Walk w w) : G.Walk u u :=
  (p.takeUntil w hw).append (c.append (p.dropUntil w hw))

Used by 1

Used byEuler's theorem

B. Existence of Euler circuits

TheoremEuler's theorem#✓fully proved

Euler's theorem (existence direction): a finite connected graph with all degrees even has a closed trail through every edge, based at any vertex. See also SimpleGraph.Connected.exists_isEulerian in MathlibExt, which does not prescribe the base vertex.

theorem exists_closed_eulerian (G : SimpleGraph V) [DecidableRel G.Adj] (hconn : G.Connected)
    (heven : ∀ x, Even (G.degree x)) (u : V) :
    ∃ p : G.Walk u u, p.IsTrail ∧ ∀ e ∈ G.edgeFinset, e ∈ p.edges

Uses 3 · Used by 2

Proof usesDegree of a vertex equals the number of edges containing it · Splicing a closed walk into another at a shared vertex · Every edge of a finite even-degree graph lies on a cycle

Used byEuler's theorem for a graph supported on a finite connected set · Eulerian circuit at any vertex of a finite connected even graph

LemmaEulerian circuit at any vertex of a finite connected even graph#✓fully proved

The closed trail of exists_closed_eulerian is an Eulerian circuit in Mathlib's sense, based at any prescribed vertex. See also SimpleGraph.Connected.exists_isEulerian.

lemma exists_closed_isEulerian (G : SimpleGraph V) [DecidableRel G.Adj]
    (hconn : G.Connected) (heven : ∀ x, Even (G.degree x)) (u : V) :
    ∃ p : G.Walk u u, p.IsEulerian

Uses 1

Proof usesEuler's theorem

LemmaEuler's theorem for a graph supported on a finite connected set#✓fully proved

Euler's theorem for a locally finite graph whose support lies in a finite set T on which the induced graph is connected. See also SimpleGraph.ConnectedSupport.exists_isEulerian in MathlibExt.

lemma exists_closed_eulerian_of_finite_support
    (T : Finset V) (hsupp : G.support ⊆ (T : Set V))
    (hconn : (G.induce (T : Set V)).Connected)
    (heven : ∀ x, Even (G.degree x)) {u : V} (huT : u ∈ (T : Set V)) :
    ∃ p : G.Walk u u, p.IsTrail ∧ ∀ e ∈ G.edgeSet, e ∈ p.edges

Uses 1 · Used by 5

Proof usesEuler's theorem

Used byClosed Eulerian walk of a component of an even edge set · Even subgraphs of a finite graph decompose into closed walks · Plus and minus box measures on \(\mathbb{Z}^2\) differ for large \(\beta\) · Peierls bound · Peierls' theorem

C. Single dual circuits for planar contours

DefinitionConnectedness of the face-boundary graph on a face set#✓fully proved

The face-boundary graph of K is connected on the finite set of faces T.

def FaceBoundaryConnected (K : Set (Site 2)) (T : Finset (Site 2)) : Prop :=
  ((faceBoundaryGraph K).induce (T : Set (Site 2))).Connected

Uses 2 · Used by 7

Statement usesSite of the hypercubic lattice · Face-boundary graph of a set

Used byConnected face-boundary graphs at the axis for all connected clusters · Connected face-boundary graphs at the axis for all realised contours · Filled-cluster winding hypothesis · Origin-only minus configuration satisfies the filled-cluster data · Plus and minus box measures on \(\mathbb{Z}^2\) differ for large \(\beta\) · Peierls bound · Peierls' theorem

DefinitionFinite face set containing the face-boundary support#✓fully proved

A finite set of faces containing the support of the face-boundary graph of a finite set K.

noncomputable def boundarySupport {K : Set (Site 2)} (hK : K.Finite) : Finset (Site 2) :=
  (exists_finset_support_faceBoundaryGraph K hK).choose

Uses 16 · Used by 2

Statement usesNearest neighbours in \(\mathbb{Z}^d\) · Site of the hypercubic lattice · Boundary edge of a set · Boundary indicator of an edge · Nearest neighbours of a lattice site · Neighbour of a site in a coordinate direction · Four unit faces at a lattice site · Boundary degree of a unit face · Face-boundary graph of a set · Lower left corner of the unit face at \((a, b)\) · Upper left corner of the unit face at \((a, b)\) · Lower right corner of the unit face at \((a, b)\) · Upper right corner of the unit face at \((a, b)\) · Hypercubic lattice \(\mathbb{Z}^d\) · Primal edge shared by adjacent faces · Shift of a site along a coordinate

Used byConnected face-boundary graphs at the axis for all connected clusters · Connected face-boundary graphs at the axis for all realised contours

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.