Snort

DefinitionSnort positions with a move bound#✓fully proved

Let \(G\) be a finite simple graph, let \(k\) be a natural number, and let \(A\) and \(B\) be finite sets of vertices of \(G\), the vertices coloured so far by the player to move and by the opponent. A legal move colours a vertex \(v\) that lies in neither \(A\) nor \(B\) and has no neighbour in \(B\). With move bound \(0\) the player to move loses. With move bound \(k + 1\) the player to move wins at \((A, B)\) exactly when some legal move \(v\) leaves a position \((B, A \cup \{v\})\) that the opponent, now to move with move bound \(k\), does not win.

def snortMoverWins [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] :
    ℕ → Finset V → Finset V → Bool
  | 0, _, _ => false
  | k + 1, mine, theirs =>
      decide (∃ v : V, v ∉ mine ∧ v ∉ theirs ∧ (∀ w ∈ theirs, ¬ G.Adj v w) ∧
        snortMoverWins G k theirs (insert v mine) = false)
Sources
  • Ashmore, Austin, Davies, Dyer, Kellough, On Graph Automorphisms Related to SNORT, INTEGERS 26 (2026), Article G2, Section 1 (rules of Snort).
Used by 5
Used bySnort response pairs · First player wins Snort · Second-player win in Snort · Snort on the \(2 \times 2\) queen's and rook's graphs · Snort on two vertices

DefinitionFirst player wins Snort#✓fully proved

Let \(G\) be a finite simple graph. In Snort on \(G\) the two players alternately colour a vertex that is not yet coloured and is not adjacent to any vertex coloured by the opponent, and a player with no legal move loses. The first player wins Snort on \(G\) when the player who moves first has a winning strategy from the position in which no vertex is coloured.

def SnortFirstPlayerWins [Fintype V] [DecidableEq V] (G : SimpleGraph V)
    [DecidableRel G.Adj] : Prop :=
  snortMoverWins G (Fintype.card V) ∅ ∅ = true
Sources
  • Ashmore, Austin, Davies, Dyer, Kellough, On Graph Automorphisms Related to SNORT, INTEGERS 26 (2026), Article G2, Section 1.
Uses 1 · Used by 5
Statement usesSnort positions with a move bound
Used byFirst player wins Peaceable Kings · Almost opposable graphs are first-player wins in Snort · First player wins Peaceable Queens on boards with an odd side · Snort on the \(2 \times 2\) queen's and rook's graphs · Snort on two vertices

DefinitionSecond-player win in Snort#✓fully proved

Let \(G\) be a finite simple graph. In Snort on \(G\), two players alternately colour a vertex of \(G\) that is not yet coloured, each with their own colour, and a player may not colour a vertex adjacent to a vertex of the opponent's colour; a player with no legal move loses. The second player wins Snort on \(G\) if, starting from the position in which no vertex is coloured, the player who moves first has no winning strategy.

Every move colours a new vertex, so the game ends after at most \(|V(G)|\) moves and has no draws; hence this says that the second player has a winning strategy.

def SnortSecondPlayerWins [Fintype V] [DecidableEq V] (G : SimpleGraph V)
    [DecidableRel G.Adj] : Prop :=
  snortMoverWins G (Fintype.card V) ∅ ∅ = false
Sources
  • Ashmore, Austin, Davies, Dyer, Kellough, On Graph Automorphisms Related to SNORT, INTEGERS 26 (2026), Article G2, Section 1.
Uses 1 · Used by 8
Statement usesSnort positions with a move bound
Used byArbitrarily large trees on which the second player wins Snort · Second player wins Peaceable Bishops exactly when a side is even · Fireworks preserve second-player wins in Snort · Snort on the knight's graph · The second player wins Snort on opposable graphs · Snort on the rook's graph · Snort on the \(2 \times 2\) queen's and rook's graphs · Snort on two vertices

DefinitionSnort response pairs#✓fully proved

In Snort on a finite graph \(G\), a pair \((u, v)\) of vertices is a response pair if \(u \neq v\), \(u\) and \(v\) are not adjacent (so the first player colouring \(u\) and the second answering \(v\) is legal), and the first player, now to move, loses from the position in which the first player has coloured \(u\) and the second player has coloured \(v\).

The outcome is computed with a bound of \(|V(G)| - 2\) further moves, the number of uncoloured vertices, so the bound never cuts the game short.

def IsSnortResponsePair [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj]
    (u v : V) : Prop :=
  u ≠ v ∧ ¬ G.Adj u v ∧ snortMoverWins G (Fintype.card V - 2) {u} {v} = false
Sources
  • Ashmore, Austin, Davies, Dyer, Kellough, On Graph Automorphisms Related to SNORT, INTEGERS 26 (2026), Article G2, Section 3 (response pair).
Uses 1 · Used by 1
Statement usesSnort positions with a move bound
Used byFireworks preserve second-player wins in Snort

DefinitionOppositions#✓fully proved

An opposition of a graph \(G\) is an automorphism \(f\) of \(G\) such that for every vertex \(v\), \(f(f(v)) = v\), \(f(v) \neq v\), and \(f(v)\) is not adjacent to \(v\); that is, an involutive automorphism moving every vertex outside its closed neighbourhood.

def IsOpposition (G : SimpleGraph V) (f : G ≃g G) : Prop :=
  ∀ v, f (f v) = v ∧ f v ≠ v ∧ ¬ G.Adj v (f v)
Sources
  • Ashmore, Austin, Davies, Dyer, Kellough, On Graph Automorphisms Related to SNORT, INTEGERS 26 (2026), Article G2, Section 1 (after Kakihara).
Used by 4
Used byCompatibly almost opposable graphs · Cartesian products of compatibly almost opposable graphs · Opposable graphs · Gluing oppositions of blocks

DefinitionOpposable graphs#✓fully proved

A graph \(G\) is opposable if it has an opposition: an automorphism \(f\) of \(G\) such that for every vertex \(v\), \(f(f(v)) = v\), \(f(v) \neq v\), and \(f(v)\) is not adjacent to \(v\).

def IsOpposable (G : SimpleGraph V) : Prop :=
  ∃ f : G ≃g G, IsOpposition G f
Sources
  • Ashmore, Austin, Davies, Dyer, Kellough, On Graph Automorphisms Related to SNORT, INTEGERS 26 (2026), Article G2, Section 1.
Uses 1 · Used by 7
Statement usesOppositions
Used byOpposability of Cartesian grids · Almost opposable graph · Formula products with an opposable first factor · Oppositions and opposition matchings · Gluing oppositions of blocks · Standard products with an opposable first factor · The second player wins Snort on opposable graphs

DefinitionAlmost opposable graph#✓fully proved

A graph \(G\) is almost opposable if there are a vertex \(u\) and a set \(S\) of vertices with \(u \in S \subseteq N[u]\), where \(N[u]\) is the closed neighbourhood of \(u\) (\(u\) together with its neighbours), such that the subgraph \(G - S\) induced on the vertices outside \(S\) is opposable.

def IsAlmostOpposable (G : SimpleGraph V) : Prop :=
  ∃ u : V, ∃ S : Set V, u ∈ S ∧ S ⊆ insert u (G.neighborSet u) ∧ IsOpposable (G.induce Sᶜ)
Sources
  • Ashmore, Austin, Davies, Dyer, Kellough, On Graph Automorphisms Related to SNORT, INTEGERS 26 (2026), Article G2, Section 4 (almost opposable graphs).
Uses 1 · Used by 4
Statement usesOpposable graphs
Used byOpposability of Cartesian grids · Almost opposability of strong grids · Strong products with a graph that has a universal vertex · Almost opposable graphs are first-player wins in Snort

DefinitionCompatibly almost opposable graphs#✓fully proved

A graph \(G\) is compatibly almost opposable if there are a vertex \(u\), a set \(S\) of vertices with \(u \in S \subseteq N[u]\) (the closed neighbourhood of \(u\)), an automorphism \(\alpha\) of \(G\) with \(\alpha(\alpha(v)) = v\) for every vertex \(v\), and an opposition \(f\) of the subgraph \(G - S\) induced on the vertices outside \(S\), such that \(\alpha(x) = f(x)\) for every vertex \(x \notin S\).

def IsCompatiblyAlmostOpposable (G : SimpleGraph V) : Prop :=
  ∃ u : V, ∃ S : Set V, u ∈ S ∧ S ⊆ insert u (G.neighborSet u) ∧
    ∃ α : G ≃g G, (∀ v, α (α v) = v) ∧
      ∃ f : G.induce Sᶜ ≃g G.induce Sᶜ, IsOpposition _ f ∧ ∀ x : ↥Sᶜ, α x = (f x : V)
Sources
  • Ashmore, Austin, Davies, Dyer, Kellough, On Graph Automorphisms Related to SNORT, INTEGERS 26 (2026), Article G2, Section 4 (compatibly almost opposable graphs).
Uses 1 · Used by 2
Statement usesOppositions
Used byCartesian products of compatibly almost opposable graphs · Strong products of compatibly almost opposable graphs

DefinitionOpposition matchings#✓fully proved

Let \(K\) be a graph. A subgraph \(M\) of \(K\) is an opposition matching of \(K\) if it is a perfect matching of \(K\) and for any two distinct edges \(ab\) and \(cd\) of \(M\), \(ac \in E(K) \iff bd \in E(K)\) and \(ad \in E(K) \iff bc \in E(K)\).

Since both matching edges are present, this says that \(K\) induces on \(\{a, b, c, d\}\) either \(K_4\), a \(4\)-cycle, or just the two matching edges.

def IsOppositionMatching (K : SimpleGraph V) (M : K.Subgraph) : Prop :=
  M.IsPerfectMatching ∧ ∀ a b c d, M.Adj a b → M.Adj c d → s(a, b) ≠ s(c, d) →
    (K.Adj a c ↔ K.Adj b d) ∧ (K.Adj a d ↔ K.Adj b c)
Sources
  • Ashmore, Austin, Davies, Dyer, Kellough, On Graph Automorphisms Related to SNORT, INTEGERS 26 (2026), Article G2, Section 2 (opposition matchings).
Used by 1
Used byOppositions and opposition matchings

DefinitionGraph product given by a Boolean formula#✓fully proved

Let \(G\) and \(H\) be graphs with vertex sets \(V\) and \(W\), and let \(\varphi\) be a Boolean function of four Boolean arguments. The product \(G \varphi H\) is the graph on \(V \times W\) in which two distinct vertices \((g_1, h_1)\) and \((g_2, h_2)\) are adjacent exactly when \(\varphi(g_1 g_2 \in E(G), h_1 h_2 \in E(H), g_1 = g_2, h_1 = h_2)\) is true.

def formulaProduct [DecidableEq V] [DecidableEq W] (φ : Bool → Bool → Bool → Bool → Bool)
    (G : SimpleGraph V) (H : SimpleGraph W) [DecidableRel G.Adj] [DecidableRel H.Adj] :
    SimpleGraph (V × W) :=
  SimpleGraph.fromRel fun x y => φ (G.Adj x.1 y.1) (H.Adj x.2 y.2) (x.1 = y.1) (x.2 = y.2)
Sources
  • Ashmore, Austin, Davies, Dyer, Kellough, On Graph Automorphisms Related to SNORT, INTEGERS 26 (2026), Article G2, Section 2 (graph products GφH).
Used by 3
Used byFormula products with an opposable first factor · Standard products with an opposable first factor · Strong product of graphs

AbbreviationStrong product of graphs#✓fully proved

For simple graphs \(G\) on \(V\) and \(H\) on \(W\), the strong product \(G \boxtimes H\) is the simple graph on \(V \times W\) in which \((g_1, h_1)\) and \((g_2, h_2)\) are adjacent if and only if \(g_1 = g_2\) and \(h_1 h_2\) is an edge of \(H\), or \(g_1 g_2\) is an edge of \(G\) and \(h_1 = h_2\), or \(g_1 g_2\) is an edge of \(G\) and \(h_1 h_2\) is an edge of \(H\).

abbrev strongProd [DecidableEq V] [DecidableEq W] (G : SimpleGraph V) (H : SimpleGraph W)
    [DecidableRel G.Adj] [DecidableRel H.Adj] : SimpleGraph (V × W) :=
  formulaProduct (fun eG eH qG qH => (qG && eH) || (eG && qH) || (eG && eH)) G H
Sources
  • Ashmore, Austin, Davies, Dyer, Kellough, On Graph Automorphisms Related to SNORT, INTEGERS 26 (2026), Article G2, Section 2 (table of products).
Uses 1 · Used by 3
Statement usesGraph product given by a Boolean formula
Used byStrong products with a graph that has a universal vertex · Strong products of compatibly almost opposable graphs · Standard products with an opposable first factor

DefinitionFirework of a graph#✓fully proved

For a graph \(G\), vertices \(u\) and \(v\) of \(G\) and a natural number \(n\), the \(n\)-firework of \(G\) at \((u, v)\) is the graph obtained from \(G\) by adding \(2n\) new vertices, \(n\) of which are adjacent only to \(u\) and the other \(n\) adjacent only to \(v\).

def firework (G : SimpleGraph V) (u v : V) (n : ℕ) : SimpleGraph (V ⊕ (Fin n × Bool)) :=
  SimpleGraph.fromRel fun x y => match x, y with
    | Sum.inl a, Sum.inl b => G.Adj a b
    | Sum.inl a, Sum.inr (_, false) => a = u
    | Sum.inl a, Sum.inr (_, true) => a = v
    | _, _ => False
Sources
  • Ashmore, Austin, Davies, Dyer, Kellough, On Graph Automorphisms Related to SNORT, INTEGERS 26 (2026), Article G2, Section 3 (the n-firework).
Used by 1
Used byFireworks preserve second-player wins in Snort

DefinitionStrong grid#✓fully proved

For \(k \in \mathbb{N}\) and natural numbers \(n_0, \dots, n_{k-1}\), the \(k\)-dimensional strong grid \(P_{n_0} \boxtimes \cdots \boxtimes P_{n_{k-1}}\) is the simple graph whose vertices are the tuples \((x_0, \dots, x_{k-1})\) of integers with \(0 \le x_i < n_i\) for each \(i\), in which two vertices \(x\) and \(y\) are adjacent if and only if \(x \ne y\) and \(|x_i - y_i| \le 1\) for every \(i\).

def strongGrid {k : ℕ} (n : Fin k → ℕ) : SimpleGraph ((i : Fin k) → Fin (n i)) :=
  SimpleGraph.fromRel fun x y => ∀ i, (x i : ℕ) ≤ y i + 1 ∧ (y i : ℕ) ≤ x i + 1
Sources
  • Ashmore, Austin, Davies, Dyer, Kellough, On Graph Automorphisms Related to SNORT, INTEGERS 26 (2026), Article G2, Corollary 3 (strong grids).
Used by 1
Used byAlmost opposability of strong grids

DefinitionCartesian grid#✓fully proved

For \(k \in \mathbb{N}\) and side lengths \(n_1, \dots, n_k \in \mathbb{N}\), the \(k\)-dimensional Cartesian grid has as vertices the tuples \((x_1, \dots, x_k)\) of integers with \(0 \le x_i < n_i\) for each \(i\), and two tuples are adjacent when they differ in exactly one coordinate, and there by exactly one. It is the Cartesian product \(P_{n_1} \square \cdots \square P_{n_k}\) of the paths \(P_{n_i}\) on \(n_i\) vertices.

def cartesianGrid {k : ℕ} (n : Fin k → ℕ) : SimpleGraph ((i : Fin k) → Fin (n i)) :=
  SimpleGraph.fromRel fun x y => ∃ i, (x i : ℕ) + 1 = y i ∧ ∀ j, j ≠ i → x j = y j
Sources
  • Ashmore, Austin, Davies, Dyer, Kellough, On Graph Automorphisms Related to SNORT, INTEGERS 26 (2026), Article G2, Corollary 4 (Cartesian grids).
Used by 1
Used byOpposability of Cartesian grids

DefinitionKing's graph#✓fully proved

For natural numbers \(n\) and \(m\), the king's graph of the \(n \times m\) board is the simple graph whose vertices are the pairs \((i, j)\) with \(0 \le i < n\) and \(0 \le j < m\), in which two distinct pairs \((i, j)\) and \((i', j')\) are adjacent when \(|i - i'| \le 1\) and \(|j - j'| \le 1\).

def kingGraph (n m : ℕ) : SimpleGraph (Fin n × Fin m) :=
  SimpleGraph.fromRel fun x y => |(x.1 : ℤ) - y.1| ≤ 1 ∧ |(x.2 : ℤ) - y.2| ≤ 1
Sources
  • Ashmore, Austin, Davies, Dyer, Kellough, On Graph Automorphisms Related to SNORT, INTEGERS 26 (2026), Article G2, Section 5.
Used by 1
Used byFirst player wins Peaceable Kings

DefinitionKnight's graph#✓fully proved

For natural numbers \(n\) and \(m\), the knight's graph of the \(n \times m\) board is the simple graph whose vertices are the pairs \((i, j)\) with \(0 \le i < n\) and \(0 \le j < m\), in which two pairs \((i, j)\) and \((i', j')\) are adjacent when either \(|i - i'| = 1\) and \(|j - j'| = 2\), or \(|i - i'| = 2\) and \(|j - j'| = 1\).

def knightGraph (n m : ℕ) : SimpleGraph (Fin n × Fin m) :=
  SimpleGraph.fromRel fun x y =>
    (|(x.1 : ℤ) - y.1| = 1 ∧ |(x.2 : ℤ) - y.2| = 2) ∨
      (|(x.1 : ℤ) - y.1| = 2 ∧ |(x.2 : ℤ) - y.2| = 1)
Sources
  • Ashmore, Austin, Davies, Dyer, Kellough, On Graph Automorphisms Related to SNORT, INTEGERS 26 (2026), Article G2, Section 5 (proof of Theorem 9).
Used by 1
Used bySnort on the knight's graph

DefinitionBishop's graph#✓fully proved

For natural numbers \(n\) and \(m\), the bishop's graph on the \(n \times m\) board has as vertices the cells \((i, j)\) with \(0 \le i < n\) and \(0 \le j < m\), and two distinct cells \((i, j)\) and \((i', j')\) are adjacent when they lie on a common diagonal, that is, when \(|i - i'| = |j - j'|\).

def bishopGraph (n m : ℕ) : SimpleGraph (Fin n × Fin m) :=
  SimpleGraph.fromRel fun x y => |(x.1 : ℤ) - y.1| = |(x.2 : ℤ) - y.2|
Sources
  • Ashmore, Austin, Davies, Dyer, Kellough, On Graph Automorphisms Related to SNORT, INTEGERS 26 (2026), Article G2, Section 5 (proof of Theorem 10).
Used by 1
Used bySecond player wins Peaceable Bishops exactly when a side is even

DefinitionQueen's graph#✓fully proved

For natural numbers \(n\) and \(m\), the queen's graph of the \(n \times m\) board is the simple graph whose vertices are the pairs \((i, j)\) with \(0 \le i < n\) and \(0 \le j < m\), in which two distinct pairs \((i, j)\) and \((i', j')\) are adjacent when \(i = i'\), or \(j = j'\), or \(|i - i'| = |j - j'|\); that is, when they share a row, a column or a diagonal.

def queenGraph (n m : ℕ) : SimpleGraph (Fin n × Fin m) :=
  SimpleGraph.fromRel fun x y =>
    x.1 = y.1 ∨ x.2 = y.2 ∨ |(x.1 : ℤ) - y.1| = |(x.2 : ℤ) - y.2|
Sources
  • Ashmore, Austin, Davies, Dyer, Kellough, On Graph Automorphisms Related to SNORT, INTEGERS 26 (2026), Article G2, Section 5.
Used by 2
Used byFirst player wins Peaceable Queens on boards with an odd side · Snort on the \(2 \times 2\) queen's and rook's graphs

TheoremSnort on two vertices#✓fully proved

The first player wins Snort on the complete graph \(K_2\), and the second player wins Snort on the graph with two vertices and no edges.

theorem snort_two_vertices :
    SnortFirstPlayerWins (⊤ : SimpleGraph (Fin 2)) ∧
      SnortSecondPlayerWins (⊥ : SimpleGraph (Fin 2))
Sources
  • Ashmore, Austin, Davies, Dyer, Kellough, On Graph Automorphisms Related to SNORT, INTEGERS 26 (2026), Article G2, Section 1; characteristic check of snortMoverWins.
Uses 3
Statement usesFirst player wins Snort · Second-player win in Snort
Proof usesSnort positions with a move bound

TheoremSnort on the \(2 \times 2\) queen's and rook's graphs#✓fully proved

The first player wins Snort on the queen's graph of the \(2 \times 2\) board (the Peaceable Queens game), and the second player wins Snort on the rook's graph of the \(2 \times 2\) board (the Peaceable Rooks game).

theorem snort_two_by_two :
    SnortFirstPlayerWins (queenGraph 2 2) ∧ SnortSecondPlayerWins (SimpleGraph.rookGraph 2 2)
Sources
  • Ashmore, Austin, Davies, Dyer, Kellough, On Graph Automorphisms Related to SNORT, INTEGERS 26 (2026), Article G2, Section 5; characteristic check of queenGraph and SimpleGraph.rookGraph.
Uses 5
Statement usesFirst player wins Snort · Second-player win in Snort · Queen's graph · Rook graph
Proof usesSnort positions with a move bound

TheoremThe second player wins Snort on opposable graphs#●ready to prove

If a finite simple graph \(G\) is opposable, then the second player wins Snort on \(G\).

public theorem_wanted snortSecondPlayerWins_of_isOpposable [Fintype V] [DecidableEq V]
    (G : SimpleGraph V) [DecidableRel G.Adj] (h : IsOpposable G) : SnortSecondPlayerWins G
Sources
  • Ashmore, Austin, Davies, Dyer, Kellough, On Graph Automorphisms Related to SNORT, INTEGERS 26 (2026), Article G2, Lemma 1 (Kakihara, Proposition 3.6).
Uses 2
Statement usesOpposable graphs · Second-player win in Snort

TheoremOppositions and opposition matchings#●ready to prove

A graph \(G\) is opposable if and only if its complement \(\overline{G}\) has an opposition matching.

public theorem_wanted isOpposable_iff_exists_oppositionMatching (G : SimpleGraph V) :
    IsOpposable G ↔ ∃ M : Gᶜ.Subgraph, IsOppositionMatching Gᶜ M
Sources
  • Ashmore, Austin, Davies, Dyer, Kellough, On Graph Automorphisms Related to SNORT, INTEGERS 26 (2026), Article G2, Theorem 1.
Uses 2
Statement usesOpposable graphs · Opposition matchings

TheoremGluing oppositions of blocks#●ready to prove

Let \(G\) be a graph, let \(p\) be a map from its vertices to an index set, with blocks \(B_i = \{v : p(v) = i\}\), and let \(f\) be a map from the vertices of \(G\) to themselves. Suppose that for every index \(i\) there is an opposition of the subgraph of \(G\) induced on \(B_i\) that agrees with \(f\) on \(B_i\), and that for all vertices \(u, w\) with \(p(u) \neq p(w)\) we have \(uw \in E(G) \iff f(u)f(w) \in E(G)\) and \(uf(w) \in E(G) \iff f(u)w \in E(G)\). Then \(G\) is opposable.

Since \(uf(u)\) and \(wf(w)\) are non-edges, the second condition says that the four vertices \(u, f(u), w, f(w)\) induce \(C_4\), \(2K_2\) or \(4K_1\).

public theorem_wanted isOpposable_of_blocks {ι : Type*} (G : SimpleGraph V) (p : V → ι)
    (f : V → V)
    (hf : ∀ i, ∃ φ : G.induce {v | p v = i} ≃g G.induce {v | p v = i},
      IsOpposition _ φ ∧ ∀ x, (φ x : V) = f x)
    (hpair : ∀ u w, p u ≠ p w →
      (G.Adj u w ↔ G.Adj (f u) (f w)) ∧ (G.Adj u (f w) ↔ G.Adj (f u) w)) :
    IsOpposable G
Sources
  • Ashmore, Austin, Davies, Dyer, Kellough, On Graph Automorphisms Related to SNORT, INTEGERS 26 (2026), Article G2, Theorem 2.
Uses 2
Statement usesOpposable graphs · Oppositions

TheoremFormula products with an opposable first factor#●ready to prove

Let \(G\) and \(H\) be graphs, let \(\varphi\) be a Boolean function of four truth values, and let \(G \varphi H\) be the formula product, in which distinct pairs \((g_1, h_1)\) and \((g_2, h_2)\) are adjacent when \(\varphi\) is true at the atoms \(g_1g_2 \in E(G)\), \(h_1h_2 \in E(H)\), \(g_1 = g_2\), \(h_1 = h_2\). Suppose that for all distinct non-adjacent vertices \(g_1, g_2\) of \(G\) and every vertex \(h\) of \(H\), \(\varphi\) is false at the atoms \(g_1g_2 \in E(G)\), \(hh \in E(H)\), \(g_1 = g_2\), \(h = h\) (whose values are false, false, false, true). If \(G\) is opposable, then \(G \varphi H\) is opposable.

public theorem_wanted isOpposable_formulaProduct [DecidableEq V] [DecidableEq W]
    (φ : Bool → Bool → Bool → Bool → Bool) (G : SimpleGraph V) (H : SimpleGraph W)
    [DecidableRel G.Adj] [DecidableRel H.Adj]
    (hφ : ∀ g₁ g₂ : V, ∀ h : W, g₁ ≠ g₂ → ¬ G.Adj g₁ g₂ →
      φ (G.Adj g₁ g₂) (H.Adj h h) (g₁ = g₂) (h = h) = false)
    (hG : IsOpposable G) : IsOpposable (formulaProduct φ G H)
Sources
  • Ashmore, Austin, Davies, Dyer, Kellough, On Graph Automorphisms Related to SNORT, INTEGERS 26 (2026), Article G2, Theorem 3.
Uses 2
Statement usesOpposable graphs · Graph product given by a Boolean formula

TheoremStandard products with an opposable first factor#●ready to prove

If \(G\) is an opposable graph, then for every graph \(H\) the Cartesian product \(G \mathbin{\square} H\), the strong product \(G \boxtimes H\), and the tensor, lexicographic, co-normal and homomorphic products of \(G\) with \(H\) are opposable. Here distinct pairs \((g_1, h_1)\) and \((g_2, h_2)\) are adjacent in the tensor product when \(g_1g_2 \in E(G)\) and \(h_1h_2 \in E(H)\); in the lexicographic product when \(g_1g_2 \in E(G)\), or \(g_1 = g_2\) and \(h_1h_2 \in E(H)\); in the co-normal product when \(g_1g_2 \in E(G)\) or \(h_1h_2 \in E(H)\); and in the homomorphic product when \(g_1 = g_2\), or \(g_1g_2 \in E(G)\) and \(h_1h_2 \notin E(H)\).

public theorem_wanted isOpposable_products [DecidableEq V] [DecidableEq W]
    (G : SimpleGraph V) (H : SimpleGraph W) [DecidableRel G.Adj] [DecidableRel H.Adj]
    (hG : IsOpposable G) :
    IsOpposable (G □ H) ∧ IsOpposable (strongProd G H) ∧
      IsOpposable (formulaProduct (fun eG eH _ _ => eG && eH) G H) ∧
      IsOpposable (formulaProduct (fun eG eH qG _ => eG || (qG && eH)) G H) ∧
      IsOpposable (formulaProduct (fun eG eH _ _ => eG || eH) G H) ∧
      IsOpposable (formulaProduct (fun eG eH qG _ => qG || (eG && !eH)) G H)
Sources
  • Ashmore, Austin, Davies, Dyer, Kellough, On Graph Automorphisms Related to SNORT, INTEGERS 26 (2026), Article G2, Corollary 1.
Uses 3
Statement usesOpposable graphs · Graph product given by a Boolean formula · Strong product of graphs

TheoremFireworks preserve second-player wins in Snort#●ready to prove

Let \(G\) be a finite simple graph and let \((u, v)\) be a response pair of \(G\) whose distance in \(G\) is at least \(3\) (infinite distance, when \(u\) and \(v\) lie in different components, is allowed). If the second player wins Snort on \(G\), then for every natural number \(n\) at least the number \(|V(G)|\) of vertices of \(G\), the second player wins Snort on the \(n\)-firework of \(G\) at \((u, v)\).

public theorem_wanted snortSecondPlayerWins_firework [Fintype V] [DecidableEq V]
    (G : SimpleGraph V) [DecidableRel G.Adj] (u v : V) (hG : SnortSecondPlayerWins G)
    (huv : IsSnortResponsePair G u v) (hdist : 3 ≤ G.edist u v) (n : ℕ)
    (hn : Fintype.card V ≤ n) [DecidableRel (firework G u v n).Adj] :
    SnortSecondPlayerWins (firework G u v n)
Sources
  • Ashmore, Austin, Davies, Dyer, Kellough, On Graph Automorphisms Related to SNORT, INTEGERS 26 (2026), Article G2, Theorem 4.
Uses 3
Statement usesSnort response pairs · Second-player win in Snort · Firework of a graph

TheoremArbitrarily large trees on which the second player wins Snort#●ready to prove

For every natural number \(N\) there is a tree \(T\) on \(n \ge N\) vertices such that the second player wins Snort on \(T\).

public theorem_wanted exists_large_tree_snortSecondPlayerWins (N : ℕ) :
    ∃ n ≥ N, ∃ T : SimpleGraph (Fin n), ∃ _ : DecidableRel T.Adj,
      T.IsTree ∧ SnortSecondPlayerWins T
Sources
  • Ashmore, Austin, Davies, Dyer, Kellough, On Graph Automorphisms Related to SNORT, INTEGERS 26 (2026), Article G2, Corollary 2.
Uses 1
Statement usesSecond-player win in Snort

TheoremAlmost opposable graphs are first-player wins in Snort#●ready to prove

For every finite simple graph \(G\) that is almost opposable, the first player wins Snort on \(G\).

public theorem_wanted snortFirstPlayerWins_of_isAlmostOpposable [Fintype V] [DecidableEq V]
    (G : SimpleGraph V) [DecidableRel G.Adj] (h : IsAlmostOpposable G) : SnortFirstPlayerWins G
Sources
  • Ashmore, Austin, Davies, Dyer, Kellough, On Graph Automorphisms Related to SNORT, INTEGERS 26 (2026), Article G2, Lemma 3.
Uses 2
Statement usesAlmost opposable graph · First player wins Snort

TheoremStrong products of compatibly almost opposable graphs#●ready to prove

If \(G\) and \(H\) are compatibly almost opposable graphs, then their strong product \(G \boxtimes H\) is compatibly almost opposable.

public theorem_wanted isCompatiblyAlmostOpposable_strongProd [DecidableEq V] [DecidableEq W]
    (G : SimpleGraph V) (H : SimpleGraph W) [DecidableRel G.Adj] [DecidableRel H.Adj]
    (hG : IsCompatiblyAlmostOpposable G) (hH : IsCompatiblyAlmostOpposable H) :
    IsCompatiblyAlmostOpposable (strongProd G H)
Sources
  • Ashmore, Austin, Davies, Dyer, Kellough, On Graph Automorphisms Related to SNORT, INTEGERS 26 (2026), Article G2, Theorem 5.
Uses 2
Statement usesCompatibly almost opposable graphs · Strong product of graphs

TheoremStrong products with a graph that has a universal vertex#●ready to prove

Let \(G\) and \(H\) be graphs. If \(G\) is almost opposable and \(H\) has a universal vertex, that is, a vertex adjacent to every other vertex of \(H\), then the strong product \(G \boxtimes H\) is almost opposable.

public theorem_wanted isAlmostOpposable_strongProd [DecidableEq V] [DecidableEq W]
    (G : SimpleGraph V) (H : SimpleGraph W) [DecidableRel G.Adj] [DecidableRel H.Adj]
    (hG : IsAlmostOpposable G) (hH : ∃ v, ∀ w, w ≠ v → H.Adj v w) :
    IsAlmostOpposable (strongProd G H)
Sources
  • Ashmore, Austin, Davies, Dyer, Kellough, On Graph Automorphisms Related to SNORT, INTEGERS 26 (2026), Article G2, Theorem 6.
Uses 2
Statement usesAlmost opposable graph · Strong product of graphs

TheoremCartesian products of compatibly almost opposable graphs#●ready to prove

Let \(G\) and \(H\) be compatibly almost opposable graphs. Suppose that for some vertex \(u\) of \(G\) there are an involutive automorphism \(\alpha\) of \(G\) and an opposition \(f\) of the induced subgraph \(G - u\) on the vertices other than \(u\) such that \(\alpha(x) = f(x)\) for every vertex \(x \neq u\). Then the Cartesian product \(G \square H\) is compatibly almost opposable.

public theorem_wanted isCompatiblyAlmostOpposable_boxProd (G : SimpleGraph V)
    (H : SimpleGraph W) (hG : IsCompatiblyAlmostOpposable G) (hH : IsCompatiblyAlmostOpposable H)
    (hu : ∃ u : V, ∃ α : G ≃g G, (∀ v, α (α v) = v) ∧
      ∃ f : G.induce ({u}ᶜ : Set V) ≃g G.induce ({u}ᶜ : Set V),
        IsOpposition _ f ∧ ∀ x : ↥({u}ᶜ : Set V), α x = (f x : V)) :
    IsCompatiblyAlmostOpposable (G □ H)
Sources
  • Ashmore, Austin, Davies, Dyer, Kellough, On Graph Automorphisms Related to SNORT, INTEGERS 26 (2026), Article G2, Theorem 7.
Uses 2
Statement usesCompatibly almost opposable graphs · Oppositions

TheoremAlmost opposability of strong grids#●ready to prove

Let \(k \ge 1\) and \(n_1, \dots, n_k \ge 1\). Then the \(k\)-dimensional strong grid \(P_{n_1} \boxtimes \cdots \boxtimes P_{n_k}\), the strong product of the paths \(P_{n_i}\) on \(n_i\) vertices, is almost opposable.

public theorem_wanted isAlmostOpposable_strongGrid {k : ℕ} (hk : 1 ≤ k) (n : Fin k → ℕ)
    (hn : ∀ i, 1 ≤ n i) : IsAlmostOpposable (strongGrid n)
Sources
  • Ashmore, Austin, Davies, Dyer, Kellough, On Graph Automorphisms Related to SNORT, INTEGERS 26 (2026), Article G2, Corollary 3.
Uses 2
Statement usesAlmost opposable graph · Strong grid

TheoremOpposability of Cartesian grids#●ready to prove

Let \(k \ge 1\) and \(n_1, \dots, n_k \ge 1\), and let \(G = P_{n_1} \square \cdots \square P_{n_k}\) be the \(k\)-dimensional Cartesian grid, the Cartesian product of the paths \(P_{n_i}\) on \(n_i\) vertices. Then \(G\) is almost opposable if and only if at most one of \(n_1, \dots, n_k\) is even, and \(G\) is opposable if more than one of them is even.

public theorem_wanted cartesianGrid_opposability {k : ℕ} (hk : 1 ≤ k) (n : Fin k → ℕ)
    (hn : ∀ i, 1 ≤ n i) :
    (IsAlmostOpposable (cartesianGrid n) ↔ (Finset.univ.filter fun i => Even (n i)).card ≤ 1) ∧
      (1 < (Finset.univ.filter fun i => Even (n i)).card → IsOpposable (cartesianGrid n))
Sources
  • Ashmore, Austin, Davies, Dyer, Kellough, On Graph Automorphisms Related to SNORT, INTEGERS 26 (2026), Article G2, Corollary 4.
Uses 3
Statement usesAlmost opposable graph · Opposable graphs · Cartesian grid

TheoremFirst player wins Peaceable Kings#●ready to prove

For all natural numbers \(n \ge 1\) and \(m \ge 1\), the first player wins Snort on the king's graph of the \(n \times m\) board (the Peaceable Kings game).

public theorem_wanted snortFirstPlayerWins_kingGraph (n m : ℕ) (hn : 1 ≤ n) (hm : 1 ≤ m) :
    SnortFirstPlayerWins (kingGraph n m)
Sources
  • Ashmore, Austin, Davies, Dyer, Kellough, On Graph Automorphisms Related to SNORT, INTEGERS 26 (2026), Article G2, Theorem 8.
Uses 2
Statement usesFirst player wins Snort · King's graph

TheoremSnort on the knight's graph#●ready to prove

For natural numbers \(n \ge 1\) and \(m \ge 1\), the second player wins Snort on the knight's graph of the \(n \times m\) board (the Peaceable Knights game) if and only if \(n\) is even or \(m\) is even.

public theorem_wanted snortSecondPlayerWins_knightGraph_iff (n m : ℕ) (hn : 1 ≤ n)
    (hm : 1 ≤ m) : SnortSecondPlayerWins (knightGraph n m) ↔ Even n ∨ Even m
Sources
  • Ashmore, Austin, Davies, Dyer, Kellough, On Graph Automorphisms Related to SNORT, INTEGERS 26 (2026), Article G2, Theorem 9.
Uses 2
Statement usesSecond-player win in Snort · Knight's graph

TheoremSecond player wins Peaceable Bishops exactly when a side is even#●ready to prove

For all natural numbers \(n \ge 1\) and \(m \ge 1\), the second player wins Snort on the bishop's graph of the \(n \times m\) board (the Peaceable Bishops game) if and only if \(n\) or \(m\) is even.

public theorem_wanted snortSecondPlayerWins_bishopGraph_iff (n m : ℕ) (hn : 1 ≤ n)
    (hm : 1 ≤ m) : SnortSecondPlayerWins (bishopGraph n m) ↔ Even n ∨ Even m
Sources
  • Ashmore, Austin, Davies, Dyer, Kellough, On Graph Automorphisms Related to SNORT, INTEGERS 26 (2026), Article G2, Theorem 10.
Uses 2
Statement usesSecond-player win in Snort · Bishop's graph

TheoremSnort on the rook's graph#●ready to prove

For natural numbers \(n \ge 1\) and \(m \ge 1\), the second player wins Snort on the rook's graph of the \(n \times m\) board (the Peaceable Rooks game) if and only if \(n\) and \(m\) are both even.

public theorem_wanted snortSecondPlayerWins_rookGraph_iff (n m : ℕ) (hn : 1 ≤ n)
    (hm : 1 ≤ m) : SnortSecondPlayerWins (SimpleGraph.rookGraph n m) ↔ Even n ∧ Even m
Sources
  • Ashmore, Austin, Davies, Dyer, Kellough, On Graph Automorphisms Related to SNORT, INTEGERS 26 (2026), Article G2, Theorem 11.
Uses 2
Statement usesSecond-player win in Snort · Rook graph

TheoremFirst player wins Peaceable Queens on boards with an odd side#●ready to prove

Let \(n \ge 1\) and \(m \ge 1\) be natural numbers such that \(n\) or \(m\) is odd. Then the first player wins Snort on the queen's graph of the \(n \times m\) board (the Peaceable Queens game).

public theorem_wanted snortFirstPlayerWins_queenGraph (n m : ℕ) (hn : 1 ≤ n) (hm : 1 ≤ m)
    (h : Odd n ∨ Odd m) : SnortFirstPlayerWins (queenGraph n m)
Sources
  • Ashmore, Austin, Davies, Dyer, Kellough, On Graph Automorphisms Related to SNORT, INTEGERS 26 (2026), Article G2, Theorem 12.
Uses 2
Statement usesFirst player wins Snort · Queen's graph
20 fully proved18 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.