Whitney's cut–cycle duality on the square lattice

DefinitionFour nearest neighbours of a site#✓fully proved

The four nearest neighbours of v: right, left, up, down.

def jce_nbr (v : Site 2) : Fin 4 → Site 2
  | 0 => ![v 0 + 1, v 1]
  | 1 => ![v 0 - 1, v 1]
  | 2 => ![v 0, v 1 + 1]
  | 3 => ![v 0, v 1 - 1]

Uses 1 · Used by 3

Statement usesSite of the hypercubic lattice

Used byBounded faces of a finite lattice graph are counted by its cycle rank · Cells on either side of a step lie in different faces · Degree of a site in an edge set

DefinitionDegree of a site in an edge set#✓fully proved

The number of edges of E at the site v.

noncomputable def jce_degree (E : Set (Sym2 (Site 2))) (v : Site 2) : ℕ := by
  classical
  exact (Finset.univ.filter (fun i : Fin 4 => s(v, jce_nbr v i) ∈ E)).card

Uses 2 · Used by 3

Statement usesSite of the hypercubic lattice · Four nearest neighbours of a site

Used byBounded faces of a finite lattice graph are counted by its cycle rank · Cells on either side of a step lie in different faces · Closed contour as an even-degree edge set

DefinitionClosed contour as an even-degree edge set#✓fully proved

Every site has even degree in the edge set E.

def jce_ClosedContour (E : Set (Sym2 (Site 2))) : Prop :=
  ∀ v : Site 2, Even (jce_degree E v)

Uses 2 · Used by 8

Statement usesSite of the hypercubic lattice · Degree of a site in an edge set

Used byEven-degree subgraphs have as many regions as their face count · Peeling a cycle from an even-degree subgraph · Bounded faces of a finite lattice graph are counted by its cycle rank · Region step property for even-degree subgraphs · Veblen step property for even-degree subgraphs · Cells on either side of a step lie in different faces · Parity coloring changes across vertical contour edges · Even-degree image of a planar lattice subgraph

DefinitionHorizontal edges below a face in its column#✓fully proved

The horizontal edges in the column [a, a + 1] at heights at most b.

def jce_horizBelow (a b : ℤ) : Sym2 (Site 2) → Prop := by
  classical
  refine Sym2.lift ⟨fun x y =>
    (x 1 = y 1) ∧ (x 1 ≤ b) ∧ ((x 0 = a ∧ y 0 = a + 1) ∨ (x 0 = a + 1 ∧ y 0 = a)), ?_⟩
  intro x y; simp only [eq_iff_iff]
  constructor <;> (rintro ⟨h1, h2, h3⟩; exact ⟨h1.symm, h1 ▸ h2, by tauto⟩)

Uses 1 · Used by 4

Statement usesSite of the hypercubic lattice

Used byBounded faces of a finite lattice graph are counted by its cycle rank · Cells on either side of a step lie in different faces · Number of horizontal contour edges below a height · Parity coloring of faces by an edge set

DefinitionParity coloring of faces by an edge set#✓fully proved

The parity coloring of faces: f is colored when an odd number of horizontal edges of E lie directly below it in its column.

noncomputable def jce_phi (E : Finset (Sym2 (Site 2))) (f : Site 2) : Prop :=
  Odd (E.filter (fun e => jce_horizBelow (f 0) (f 1) e)).card

Uses 2 · Used by 3

Statement usesSite of the hypercubic lattice · Horizontal edges below a face in its column

Used byBounded faces of a finite lattice graph are counted by its cycle rank · Cells on either side of a step lie in different faces · Parity coloring changes across vertical contour edges

DefinitionParity coloring changes across vertical contour edges#✓fully proved

For every closed contour E, the parity coloring changes between horizontally adjacent faces exactly when the vertical edge between them is in E.

def jce_HorizStepResidue : Prop :=
  ∀ (E : Finset (Sym2 (Site 2))), jce_ClosedContour (E : Set (Sym2 (Site 2))) →
    ∀ a b : ℤ, (s(![a + 1, b], ![a + 1, b + 1]) ∈ E ↔
      (jce_phi E ![a, b] ↔ ¬ jce_phi E ![a + 1, b]))

Uses 3 · Used by 2

Statement usesSite of the hypercubic lattice · Closed contour as an even-degree edge set · Parity coloring of faces by an edge set

Used byBounded faces of a finite lattice graph are counted by its cycle rank · Cells on either side of a step lie in different faces

DefinitionNumber of horizontal contour edges below a height#✓fully proved

The number of horizontal edges of E below height b in the column [c, c + 1].

noncomputable def jce_Hc (E : Finset (Sym2 (Site 2))) (c b : ℤ) : ℕ :=
  (E.filter (fun e => jce_horizBelow c b e)).card

Uses 2 · Used by 2

Statement usesSite of the hypercubic lattice · Horizontal edges below a face in its column

Used byBounded faces of a finite lattice graph are counted by its cycle rank · Cells on either side of a step lie in different faces

DefinitionEdge flip relation of an edge set#✓fully proved

The flip relation of E: the primal edge between the faces a and b is in E.

def jce_edgeFlip (E : Finset (Sym2 (Site 2))) (a b : Site 2) : Prop :=
  sharedPrimalEdge a b ∈ E

Uses 2 · Used by 2

Statement usesSite of the hypercubic lattice · Primal edge shared by adjacent faces

Used byBounded faces of a finite lattice graph are counted by its cycle rank · Cells on either side of a step lie in different faces

DefinitionFace-region graph of a square-lattice subgraph#✓fully proved

The face-region graph of G: two adjacent faces of ℤ² are joined unless the primal edge between them (sharedPrimalEdge) is an edge of G. This is the faithful planar dual complement of G.

noncomputable def whb_faceRegion (G : SimpleGraph (Site 2)) : SimpleGraph (Site 2) where
  Adj f g := (hypercubicLattice 2).Adj f g ∧ sharedPrimalEdge f g ∉ G.edgeSet
  symm := by
    refine ⟨?_⟩
    intro f g ⟨hadj, hs⟩
    exact ⟨hadj.symm, by rwa [sharedPrimalEdge_comm_of_adj hadj] at hs⟩
  loopless := ⟨fun f h => (hypercubicLattice 2).irrefl h.1⟩

Uses 3 · Used by 38

Statement usesSite of the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\) · Primal edge shared by adjacent faces

Used byBounded regions of a planar lattice subgraph · Bounded regions indexed by the cycle rank · Even-degree subgraphs have as many regions as their face count · Peeling a cycle from an even-degree subgraph · Bounded faces of a finite lattice graph are counted by its cycle rank · Interior region of the unit square · Outer face region of a planar lattice subgraph · Whitney cut-cycle duality for a planar lattice subgraph · Exterior of a box maps into the face-region graph · Number of face regions of a subgraph's image · Keep-reconnect residue for finite graphs · Region step property for even-degree subgraphs · Face-graph adjacency as absence of a walk step between cells · Ray-parity interior equals the bounded face components · Lattice Jordan curve theorem for simple closed walks · The inner face component is finite · Horizontally face-adjacent cells have the same ray parity · Vertically face-adjacent cells have the same ray parity · Face graph of a closed walk · Lattice Jordan curve theorem, even-odd form · Cells on either side of a step lie in different faces · Number of cells is at most the nullity of the skeleton · Bounded face formed by a cell · Distinct cells form distinct bounded faces · Face component containing a cell · The face component of a cell is bounded · The face of a cell is enclosed on all four sides · The face of a cell is alone in its component · Hopf's Umlaufsatz · Whitney duality in the bridge direction · Cut coloring separating the ends of a dual edge · Whitney's cut–cycle duality · Faithful discrete Jordan statement for the face count · Number of bounded faces of a lattice subgraph · Shift isomorphism: lattice minus barrier edges to face region graph · Plus and minus box measures on \(\mathbb{Z}^2\) differ for large \(\beta\) · Peierls bound · Peierls' theorem

DefinitionWhitney's cut–cycle duality#✓fully proved

Whitney's cut–cycle duality for subgraphs of ℤ² (H. Whitney, Planar graphs, 1933): for every H and lattice edge pq not in H, with fg the dual edge across pq, the endpoints p and q are connected in H iff f and g are disconnected in the face-region graph of H with fg deleted.

def whb_CorrectWhitney : Prop :=
  ∀ (H : SimpleGraph (Site 2)) (p q f g : Site 2),
    (hypercubicLattice 2).Adj p q → s(p, q) ∉ H.edgeSet →
    (hypercubicLattice 2).Adj f g → sharedPrimalEdge f g = s(p, q) →
    (H.Reachable p q ↔
      ¬ ((whb_faceRegion H).deleteEdges {s(f, g)}).Reachable f g)

Uses 4

Statement usesSite of the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\) · Primal edge shared by adjacent faces · Face-region graph of a square-lattice subgraph

DefinitionNumber of edge crossings of a face walk#✓fully proved

The number of steps of the face walk w across an edge of H.

noncomputable def whc_dualCross (H : SimpleGraph (Site 2)) {x y : Site 2}
    (w : (hypercubicLattice 2).Walk x y) : ℕ := by
  classical
  exact w.edges.countP (fun e => decide (Sym2.lift ⟨fun a b =>
      sharedPrimalEdge a b ∈ H.edgeSet ∨ sharedPrimalEdge b a ∈ H.edgeSet, by
    intro a b; simp only [eq_iff_iff]; tauto⟩ e))

Uses 3

Statement usesSite of the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\) · Primal edge shared by adjacent faces

DefinitionPrimal edge between two faces lies in a subgraph#✓fully proved

The primal edge between the faces a and b is an edge of H.

def whc_isCross (H : SimpleGraph (Site 2)) (a b : Site 2) : Prop :=
  sharedPrimalEdge a b ∈ H.edgeSet ∨ sharedPrimalEdge b a ∈ H.edgeSet

Uses 2 · Used by 5

Statement usesSite of the hypercubic lattice · Primal edge shared by adjacent faces

Used byBounded faces of a finite lattice graph are counted by its cycle rank · Cells on either side of a step lie in different faces · Cut flip relation of a lattice graph and a dual edge · Face coloring compatible with a subgraph · Cut coloring of a subgraph with an extra dual edge

DefinitionFace coloring compatible with a subgraph#✓fully proved

φ changes value exactly across the dual edges of H.

def whc_CompatColoring (H : SimpleGraph (Site 2)) (φ : Site 2 → Prop) : Prop :=
  ∀ a b, (hypercubicLattice 2).Adj a b → (whc_isCross H a b ↔ (φ a ↔ ¬ φ b))

Uses 3

Statement usesSite of the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\) · Primal edge between two faces lies in a subgraph

DefinitionCut coloring of a subgraph with an extra dual edge#✓fully proved

φ changes value exactly across the dual edges of H and the extra dual edge f0g0.

def whc_CutColoring (H : SimpleGraph (Site 2)) (f0 g0 : Site 2) (φ : Site 2 → Prop) : Prop :=
  ∀ a b, (hypercubicLattice 2).Adj a b →
    ((whc_isCross H a b ∨ s(a, b) = s(f0, g0)) ↔ (φ a ↔ ¬ φ b))

Uses 3 · Used by 3

Statement usesSite of the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\) · Primal edge between two faces lies in a subgraph

Used byBounded faces of a finite lattice graph are counted by its cycle rank · Cells on either side of a step lie in different faces · Cut coloring separating the ends of a dual edge

DefinitionUnit square with its bottom edge removed#✓fully proved

The unit square with its bottom edge removed.

noncomputable def whc_Htest : SimpleGraph (Site 2) :=
  (imageGraph jbc_Pce).deleteEdges {s(![(0 : ℤ), 0], ![1, 0])}

Uses 3

Statement usesSite of the hypercubic lattice · Image of a planar lattice subgraph in the square lattice · Unit square as a planar lattice subgraph

DefinitionFace coloring supported at a single face#✓fully proved

The face coloring that is true only at the face (0, 0).

def whc_phiWitness : Site 2 → Prop := fun f => f = ![(0:ℤ), 0]

Uses 1

Statement usesSite of the hypercubic lattice

DefinitionNumber of bounded faces of a lattice subgraph#✓fully proved

The number of finite components of the face-region graph of P: the bounded faces of P.

noncomputable def whc_faithfulRegionCount (P : PlanarZ2Subgraph) : ℕ :=
  Nat.card {c : (whb_faceRegion (imageGraph P)).ConnectedComponent // c.supp.Finite}

Uses 4 · Used by 4

Statement usesPlanar lattice subgraph of the square lattice · Site of the hypercubic lattice · Image of a planar lattice subgraph in the square lattice · Face-region graph of a square-lattice subgraph

Used byBounded faces of a finite lattice graph are counted by its cycle rank · Plus and minus box measures on \(\mathbb{Z}^2\) differ for large \(\beta\) · Peierls bound · Peierls' theorem

DefinitionFaithful discrete Jordan statement for the face count#✓fully proved

The face count of a finite subgraph of ℤ²: the bounded components of its face-region graph are equinumerous with Fin (nullity P.G), so the number of bounded faces is the cycle rank. Only the number of faces is asserted, not which cycle bounds which face.

def whc_FaithfulDiscreteJordan (P : PlanarZ2Subgraph) : Prop :=
  Nonempty ({c : (whb_faceRegion (imageGraph P)).ConnectedComponent // c.supp.Finite} ≃
    Fin (nullity P.G))

Uses 5 · Used by 6

Statement usesPlanar lattice subgraph of the square lattice · Site of the hypercubic lattice · Image of a planar lattice subgraph in the square lattice · Cycle rank of a finite graph · Face-region graph of a square-lattice subgraph

Used byBounded faces of a finite lattice graph are counted by its cycle rank · Lattice Jordan curve theorem for simple closed walks · Faithful discrete Jordan property for even-degree subgraphs · Plus and minus box measures on \(\mathbb{Z}^2\) differ for large \(\beta\) · Peierls bound · Peierls' theorem

DefinitionClosed face walk around a lattice vertex#✓fully proved

The closed walk through the four faces having the site (c, d) as a corner.

noncomputable def jwc_vertexLoop (c d : ℤ) :
    (hypercubicLattice 2).Walk ![c, d] ![c, d] :=
  .cons (jwc_faceAdj_NE_NW c d)
    (.cons (jwc_faceAdj_NW_SW c d)
      (.cons (jwc_faceAdj_SW_SE c d)
        (.cons (jwc_faceAdj_SE_NE c d) .nil)))

Uses 2 · Used by 2

Statement usesSite of the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\)

Used byBounded faces of a finite lattice graph are counted by its cycle rank · Cells on either side of a step lie in different faces

DefinitionSpanning subgraph formed by a path#✓fully proved

The spanning subgraph formed by a path from y to x in K.

noncomputable def jwc_cyclePath {V : Type*} [DecidableEq V] {K : SimpleGraph V} {x y : V}
    (hreach : K.Reachable x y) : SimpleGraph V :=
  (hreach.symm).some.toPath.val.toSubgraph.spanningCoe

Used by 1

Used byBounded faces of a finite lattice graph are counted by its cycle rank

DefinitionWhitney duality in the bridge direction#✓fully proved

Whitney's duality in the bridge direction for P: for every subgraph K of P and edge xy of P not in K with dual edge f0g0, if x and y are disconnected in K, then f0 and g0 are connected in the face-region graph of K with f0g0 deleted.

def jwc_KeepResidue (P : PlanarZ2Subgraph) : Prop :=
  ∀ (K : SimpleGraph P.V), K ≤ P.G → ∀ {x y : P.V}, P.G.Adj x y → ¬ K.Adj x y →
    ∀ {f0 g0 : Site 2}, (hypercubicLattice 2).Adj f0 g0 →
      sharedPrimalEdge f0 g0 = s(P.emb x, P.emb y) →
      ¬ K.Reachable x y →
        ((whb_faceRegion (jei_pushGraph P K)).deleteEdges {s(f0, g0)}).Reachable f0 g0

Uses 6 · Used by 1

Statement usesPlanar lattice subgraph of the square lattice · Site of the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\) · Pushforward of a subgraph into the square lattice · Primal edge shared by adjacent faces · Face-region graph of a square-lattice subgraph

Used byBounded faces of a finite lattice graph are counted by its cycle rank

DefinitionInduced subgraphs of locally finite graphs are locally finite#✓fully proved

An induced subgraph of a locally finite graph is locally finite.

@[reducible]
noncomputable def jeb_induceLF {V : Type*} (H : SimpleGraph V) [SimpleGraph.LocallyFinite H]
    (s : Set V) : SimpleGraph.LocallyFinite (H.induce s) := by
  classical
  intro v
  rw [SimpleGraph.neighborSet_induce]
  apply Set.Finite.fintype
  apply Set.Finite.preimage (Function.Injective.injOn Subtype.coe_injective)
  exact (H.neighborSet ↑v).toFinite

TheoremTwo odd-degree vertices lie in one component#✓fully proved

In a locally finite graph with finite support, two vertices of odd degree whose other vertices all have even degree lie in the same component (the handshake lemma applied to a component).

theorem jeb_two_odd_reachable {V : Type*} (H : SimpleGraph V) [SimpleGraph.LocallyFinite H]
    (hfin : H.support.Finite) (p q : V)
    (hp : Odd (H.degree p)) (hq : Odd (H.degree q))
    (hother : ∀ v, v ≠ p → v ≠ q → Even (H.degree v)) : H.Reachable p q

Used by 1

Used byBounded faces of a finite lattice graph are counted by its cycle rank

DefinitionEven-degree image of a planar lattice subgraph#✓fully proved

Every site has even degree in the image of P.

def jeb_EvenDegreeSubgraph (P : PlanarZ2Subgraph) : Prop :=
  jce_ClosedContour (imageGraph P).edgeSet

Uses 4 · Used by 2

Statement usesPlanar lattice subgraph of the square lattice · Site of the hypercubic lattice · Image of a planar lattice subgraph in the square lattice · Closed contour as an even-degree edge set

Used byWhitney duality for even-degree planar lattice subgraphs · Faithful discrete Jordan property for even-degree subgraphs

DefinitionFaithful discrete Jordan property for even-degree subgraphs#✓fully proved

Every PlanarZ2Subgraph with all degrees even satisfies whc_FaithfulDiscreteJordan.

def jeb_FaithfulCountResidue : Prop :=
  ∀ (P : PlanarZ2Subgraph), jeb_EvenDegreeSubgraph P → whc_FaithfulDiscreteJordan P

Uses 3

Statement usesPlanar lattice subgraph of the square lattice · Even-degree image of a planar lattice subgraph · Faithful discrete Jordan statement for the face count

DefinitionSymmetry of a flip relation on lattice edges#✓fully proved

The flip relation is symmetric on lattice edges.

def wcl_SymmFlip (flip : Site 2 → Site 2 → Prop) : Prop :=
  ∀ a b, (hypercubicLattice 2).Adj a b → (flip a b ↔ flip b a)

Uses 2 · Used by 2

Statement usesSite of the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\)

Used byBounded faces of a finite lattice graph are counted by its cycle rank · Cells on either side of a step lie in different faces

DefinitionNumber of flips along a lattice walk#✓fully proved

The number of steps of the walk w that are flips (in either direction).

noncomputable def wcl_flipCount (flip : Site 2 → Site 2 → Prop) {x y : Site 2}
    (w : (hypercubicLattice 2).Walk x y) : ℕ := by
  classical
  exact w.edges.countP (fun e => decide (Sym2.lift ⟨fun a b => flip a b ∨ flip b a, by
    intro a b; simp only [eq_iff_iff]; tauto⟩ e))

Uses 2 · Used by 5

Statement usesSite of the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\)

Used byBounded faces of a finite lattice graph are counted by its cycle rank · Cells on either side of a step lie in different faces · Cut-flip count along a walk · Even-flip condition on closed lattice walks · Face coloring by parity of flips

DefinitionEven-flip condition on closed lattice walks#✓fully proved

Every closed lattice walk has an even number of flips.

def wcl_ClosedEven (flip : Site 2 → Site 2 → Prop) : Prop :=
  ∀ {x : Site 2} (w : (hypercubicLattice 2).Walk x x), Even (wcl_flipCount flip w)

Uses 3 · Used by 3

Statement usesSite of the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\) · Number of flips along a lattice walk

Used byBounded faces of a finite lattice graph are counted by its cycle rank · Cells on either side of a step lie in different faces · Cut coloring separating the ends of a dual edge

DefinitionChosen lattice walk between two faces#✓fully proved

A fixed lattice walk from o to f, chosen using connectedness of ℤ².

noncomputable def wcl_chosenWalk (o f : Site 2) : (hypercubicLattice 2).Walk o f :=
  (hypercubicLattice_two_reachable o f).some

Uses 3 · Used by 3

Statement usesSite of the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\) · Square lattice is connected

Used byBounded faces of a finite lattice graph are counted by its cycle rank · Cells on either side of a step lie in different faces · Face coloring by parity of flips

DefinitionFace coloring by parity of flips#✓fully proved

The face coloring given by the parity of the number of flips along the chosen walk from o.

noncomputable def wcl_windingColoring (flip : Site 2 → Site 2 → Prop) (o : Site 2) :
    Site 2 → Prop :=
  fun f => Odd (wcl_flipCount flip (wcl_chosenWalk o f))

Uses 3 · Used by 2

Statement usesSite of the hypercubic lattice · Chosen lattice walk between two faces · Number of flips along a lattice walk

Used byBounded faces of a finite lattice graph are counted by its cycle rank · Cells on either side of a step lie in different faces

DefinitionCut flip relation of a lattice graph and a dual edge#✓fully proved

The cut flip relation: steps across a dual edge of H or across the extra dual edge f0g0.

def wcl_cutFlip (H : SimpleGraph (Site 2)) (f0 g0 : Site 2) (a b : Site 2) : Prop :=
  whc_isCross H a b ∨ s(a, b) = s(f0, g0)

Uses 2 · Used by 4

Statement usesSite of the hypercubic lattice · Primal edge between two faces lies in a subgraph

Used byBounded faces of a finite lattice graph are counted by its cycle rank · Cells on either side of a step lie in different faces · Cut-flip count along a walk · Cut coloring separating the ends of a dual edge

DefinitionClosed walk around a unit square#✓fully proved

The closed walk around the unit square with corners (0, 0) and (1, -1).

noncomputable def wcl_squareLoop : (hypercubicLattice 2).Walk ![(0:ℤ), 0] ![(0:ℤ), 0] := by
  have a1 : (hypercubicLattice 2).Adj ![(0:ℤ), 0] ![(0:ℤ), -1] := by
    rw [hypercubicLattice_adj, Fin.sum_univ_two]; norm_num
  have a2 : (hypercubicLattice 2).Adj ![(0:ℤ), -1] ![(1:ℤ), -1] := by
    rw [hypercubicLattice_adj, Fin.sum_univ_two]; norm_num
  have a3 : (hypercubicLattice 2).Adj ![(1:ℤ), -1] ![(1:ℤ), 0] := by
    rw [hypercubicLattice_adj, Fin.sum_univ_two]; norm_num
  have a4 : (hypercubicLattice 2).Adj ![(1:ℤ), 0] ![(0:ℤ), 0] := by
    rw [hypercubicLattice_adj, Fin.sum_univ_two]; norm_num
  exact .cons a1 (.cons a2 (.cons a3 (.cons a4 .nil)))

Uses 2

Statement usesSite of the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\)

DefinitionCut coloring separating the ends of a dual edge#✓fully proved

For every graph H of ℤ² and dual edge f0g0 such that the cut flip relation has even loops, there is a cut coloring distinguishing f0 from g0, and f0, g0 are disconnected in the face-region graph of H with f0g0 deleted.

def wcl_CorrectColoringResidue : Prop :=
  ∀ (H : SimpleGraph (Site 2)) (f0 g0 : Site 2),
    (hypercubicLattice 2).Adj f0 g0 → wcl_ClosedEven (wcl_cutFlip H f0 g0) →
    ∃ φ : Site 2 → Prop, whc_CutColoring H f0 g0 φ ∧ ¬ (φ f0 ↔ φ g0) ∧
      ¬ ((whb_faceRegion H).deleteEdges {s(f0, g0)}).Reachable f0 g0

Uses 6

Statement usesSite of the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\) · Even-flip condition on closed lattice walks · Cut flip relation of a lattice graph and a dual edge · Face-region graph of a square-lattice subgraph · Cut coloring of a subgraph with an extra dual edge

DefinitionCut-flip count along a walk#✓fully proved

The number of cut flips of H and f0g0 along w; equal to wcl_flipCount (wcl_cutFlip H f0 g0) w.

noncomputable def jwn_cutCount (H : SimpleGraph (Site 2)) (f0 g0 : Site 2) {x y : Site 2}
    (w : (hypercubicLattice 2).Walk x y) : ℕ :=
  wcl_flipCount (wcl_cutFlip H f0 g0) w

Uses 4

Statement usesSite of the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\) · Cut flip relation of a lattice graph and a dual edge · Number of flips along a lattice walk

34 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.