Documentation

def GameForm.LeftDeadEnd.IsLde (g : GameForm) :

Equations

GameForm.LeftDeadEnd.IsLde g = (Form.IsShort g ∧ Form.IsDeadEnd Player.left g)

Instances For

def GameForm.LeftDeadEnd.«term_≥ₗ_» :

Lean.TrailingParserDescr

Comparison of Left dead ends is multiversal, so we fix the dead-ending universe $\mathcal{E}$ as the ambient set, writing $G \ge H$ for $G \ge_{\mathcal{E}} H$ and $G = H$ for $G =_{\mathcal{E}} H$.

Equations

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

Instances For

def GameForm.LeftDeadEnd.«term_≡ₗ_» :

Lean.TrailingParserDescr

Equations

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

Instances For

theorem GameForm.LeftDeadEnd.isLde_zero :

IsLde 0

theorem GameForm.LeftDeadEnd.IsLde.short {g : GameForm} (h : IsLde g) :

Form.IsShort g

theorem GameForm.LeftDeadEnd.IsLde.deadEnd {g : GameForm} (h : IsLde g) :

Form.IsDeadEnd Player.left g

theorem GameForm.LeftDeadEnd.IsLde.add {g h : GameForm} (hg : IsLde g) (hh : IsLde h) :

IsLde (g + h)

theorem GameForm.LeftDeadEnd.isLde_sum {s : Multiset GameForm} (hs : ∀ a ∈ s, IsLde a) :

IsLde s.sum

theorem GameForm.LeftDeadEnd.IsLde.of_mem_rightMoves {g gr : GameForm} (hg : IsLde g) (h : gr ∈ Moves.moves Player.right g) :

IsLde gr

@[irreducible]

theorem GameForm.LeftDeadEnd.IsDeadEnd.isDeadEnding {g : GameForm} (hg : Form.IsDeadEnd Player.left g) :

Form.IsDeadEnding g

Form.DeadEnding.ShortDeadEnding g

theorem GameForm.LeftDeadEnd.IsLde.shortDeadEnding {g : GameForm} (hg : IsLde g) :

theorem GameForm.LeftDeadEnd.IsLde.rightMoves_nonempty {g : GameForm} (hg : IsLde g) (hne : g ≠ 0) :

(Moves.moves Player.right g).Nonempty

theorem GameForm.LeftDeadEnd.isLde_neg_intCast (n : ℕ) :

IsLde (-↑n)

theorem GameForm.LeftDeadEnd.isLde_neg_one :

IsLde (-1)

theorem GameForm.LeftDeadEnd.rightMoves_neg_one :

Moves.moves Player.right (-1) = {0}

theorem GameForm.LeftDeadEnd.rightMoves_neg_intCast_succ (n : ℕ) :

Moves.moves Player.right (-↑(n + 1)) = {-↑n}

theorem GameForm.LeftDeadEnd.leftMoves_neg_intCast (n : ℕ) :

Moves.moves Player.left (-↑n) = ∅

theorem GameForm.LeftDeadEnd.leftMoves_neg_one :

Moves.moves Player.left (-1) = ∅

def GameForm.LeftDeadEnd.waitingGame :

ℕ → GameForm

Equations

GameForm.LeftDeadEnd.waitingGame 0 = 0
GameForm.LeftDeadEnd.waitingGame n.succ = !{∅ | {0, GameForm.LeftDeadEnd.waitingGame n}}

Instances For

theorem GameForm.LeftDeadEnd.isLde_waitingGame (n : ℕ) :

IsLde (waitingGame n)

theorem GameForm.LeftDeadEnd.rightMoves_waitingGame (n : ℕ) :

Moves.moves Player.right (waitingGame (n + 1)) = {0, waitingGame n}

theorem GameForm.LeftDeadEnd.waitingGame_succ_ne_zero (n : ℕ) :

waitingGame (n + 1) ≠ 0

theorem GameForm.LeftDeadEnd.misereGE_lde_iff {g h : GameForm} (hg : IsLde g) (hh : IsLde h) :

g ≥m Form.DeadEnding.ShortDeadEnding h ↔ (Form.IsEnd Player.right g → Form.IsEnd Player.right h) ∧ ∀ gr ∈ Moves.moves Player.right g, ∃ hr ∈ Moves.moves Player.right h, gr ≥m Form.DeadEnding.ShortDeadEnding hr

If $\mathcal{U}$ is a universe, and $G$ and $H$ are Left dead ends, then $G \ge_{\mathcal{U}} H$ if and only if the following hold:

if $G \cong 0$, then $H \cong 0$; otherwise,
for every $G^R \in G^{\mathcal{R}}$, there exists some $H^R \in H^{\mathcal{R}}$ such that $G^R \ge_{\mathcal{U}} H^R$.

This is Davies (Theorem 2.4 on p. 7).

Runs #

def GameForm.LeftDeadEnd.IsRun :

List GameForm → Prop

Equations

GameForm.LeftDeadEnd.IsRun [] = False
GameForm.LeftDeadEnd.IsRun [head] = True
GameForm.LeftDeadEnd.IsRun (a :: b :: l) = (b ∈ Moves.moves Player.right a ∧ GameForm.LeftDeadEnd.IsRun (b :: l))

Instances For

theorem GameForm.LeftDeadEnd.IsLde.of_mem_isRun {g : GameForm} (hg : IsLde g) {l : List GameForm} (hl : IsRun (g :: l)) (x : GameForm) :

x ∈ g :: l → IsLde x

theorem GameForm.LeftDeadEnd.exists_run_dominated {g h : GameForm} (hg : IsLde g) (hh : IsLde h) (hge : g ≥m Form.DeadEnding.ShortDeadEnding h) {l : List GameForm} (hl : IsRun (g :: l)) :

∃ (m : List GameForm), IsRun (h :: m) ∧ List.Forall₂ (fun (a b : GameForm) => a ≥m Form.DeadEnding.ShortDeadEnding b) (g :: l) (h :: m)

If $G$ and $H$ are Left dead ends with $G \ge H$, and $k$ is an integer satisfying $0 \le k \le \tilde{b}(G)$, then, for any run $(G_0, G_1, \ldots, G_k)$ of $G$ of length $k$, there exists a run $(H_0, H_1, \ldots, H_k)$ of $H$ of length $k$ such that $G_i \ge H_i$ for every $0 \le i \le k$.

This is Davies (Corollary 3.2 on p. 10).

Good options #

def GameForm.LeftDeadEnd.LdeGt (a b : GameForm) :

Equations

GameForm.LeftDeadEnd.LdeGt a b = (a ≥m Form.DeadEnding.ShortDeadEnding b ∧ ¬b ≥m Form.DeadEnding.ShortDeadEnding a)

Instances For

def GameForm.LeftDeadEnd.IsGoodOption (gr g : GameForm) :

If $G$ is a combinatorial game, then we will say that a (Left, respectively Right) option $G'$ of $G$ is good if it is not strictly dominated by another (Left, respectively Right) option of $G$.

This is Davies (Definition 3.3 on p. 11).

Equations

GameForm.LeftDeadEnd.IsGoodOption gr g = (gr ∈ Moves.moves Player.right g ∧ ¬∃ gr' ∈ Moves.moves Player.right g, GameForm.LeftDeadEnd.LdeGt gr gr')

Instances For

@[irreducible]

theorem GameForm.LeftDeadEnd.exists_isGoodOption_le_of_mem_rightMoves {g x : GameForm} (hg : IsLde g) (hx : x ∈ Moves.moves Player.right g) :

∃ (gr : GameForm), IsGoodOption gr g ∧ x ≥m Form.DeadEnding.ShortDeadEnding gr

theorem GameForm.LeftDeadEnd.lde_good_option_dominates {g h gr : GameForm} (hg : IsLde g) (hh : IsLde h) (hge : g ≥m Form.DeadEnding.ShortDeadEnding h) (hgr : IsGoodOption gr g) :

∃ (hr : GameForm), IsGoodOption hr h ∧ gr ≥m Form.DeadEnding.ShortDeadEnding hr

If $G \ge H$ and $G^R$ is a good option of $G$, then some (good) option $H^R$ of $H$ has $G^R \ge H^R$.

This is the $\ge$ case of Davies (Corollary 3.4 on p. 11).

theorem GameForm.LeftDeadEnd.lde_good_option_misereEQ {g h gr : GameForm} (hg : IsLde g) (hh : IsLde h) (heq : g =m Form.DeadEnding.ShortDeadEnding h) (hgr : IsGoodOption gr g) :

∃ (hr : GameForm), IsGoodOption hr h ∧ gr =m Form.DeadEnding.ShortDeadEnding hr

If $G = H$ and $G^R$ is a good option of $G$, then some (good) option $H^R$ of $H$ has $G^R = H^R$.

This is the $=$ case of Davies (Corollary 3.4 on p. 11).

def GameForm.LeftDeadEnd.HasUniqueGoodOption (g : GameForm) :

Equations

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

Instances For

theorem GameForm.LeftDeadEnd.hasUniqueGoodOption_or_multi {g : GameForm} (hg : IsLde g) (hg0 : g ≠ 0) :

HasUniqueGoodOption g ∨ ∃ (a : GameForm) (b : GameForm), IsGoodOption a g ∧ IsGoodOption b g ∧ ¬a =m Form.DeadEnding.ShortDeadEnding b

theorem GameForm.LeftDeadEnd.lde_misereEQ_zero_iff {g : GameForm} (hg : IsLde g) :

g =m Form.DeadEnding.ShortDeadEnding 0 ↔ g = 0

The monoid of Left dead ends $\mathcal{L}$ is reduced.

This is Davies (Theorem 3.1 on p. 10).

Terminal lengths, race and birthday #

@[irreducible]

def GameForm.LeftDeadEnd.terminalLengths (g : GameForm) :

Set ℕ

If $G$ is a short game, then we define the set of terminal lengths of $G$, denoted $T(G)$, as the set of all $n$ such that there exists a terminal run of $G$ of length $n$.

This is Davies (Definition 3.12 on p. 14), taken here in the equivalent recursive form of Lemma 3.13.

Equations

GameForm.LeftDeadEnd.terminalLengths g = if g = 0 then {0} else ⋃ gr ∈ Moves.moves Player.right g, (fun (x : ℕ) => x + 1) '' GameForm.LeftDeadEnd.terminalLengths gr

Instances For

theorem GameForm.LeftDeadEnd.terminalLengths_zero :

terminalLengths 0 = {0}

theorem GameForm.LeftDeadEnd.terminalLengths_of_ne_zero {g : GameForm} (hne : g ≠ 0) :

terminalLengths g = ⋃ gr ∈ Moves.moves Player.right g, (fun (x : ℕ) => x + 1) '' terminalLengths gr

If $G$ is a non-zero Left dead end, then $T(G) = \bigcup (T(G') + 1)$, where $G'$ ranges over all options of $G$.

This is Davies (Lemma 3.13 on p. 14).

@[irreducible]

theorem GameForm.LeftDeadEnd.terminalLengths_finite_nonempty {g : GameForm} (hg : IsLde g) :

(terminalLengths g).Finite ∧ (terminalLengths g).Nonempty

def GameForm.LeftDeadEnd.race (g : GameForm) :

ℕ

If $G$ is a short game, define the race of $G$, denoted $r(G)$, as $r(G) := \min(T(G))$.

This is Davies (Definition 3.14 on p. 15).

Equations

GameForm.LeftDeadEnd.race g = sInf (GameForm.LeftDeadEnd.terminalLengths g)

Instances For

def GameForm.LeftDeadEnd.IsInteger (g : GameForm) :

A Left dead end is an integer if it is isomorphic either to $0 := \{\cdot \mid \cdot\}$ or to $\overline{n} := \{\cdot \mid \overline{n - 1}\}$ for some $n \ge 1$ (where $\overline{0} := 0$).

This is Davies (p. 15).

Equations

GameForm.LeftDeadEnd.IsInteger g = ∃ (n : ℤ), g = ↑n

Instances For

@[irreducible]

def GameForm.LeftDeadEnd.flexibility (g : GameForm) :

ℕ

If $G$ is a Left dead end, then we define the flexibility of $G$, written $f(G)$, recursively as $f(G) = 1 + \max(f(G'))$, where $G'$ ranges over all options of $G$, when $G$ is not an integer, and as $f(G) := 0$ otherwise.

This is Davies (Definition 5.1 on p. 22).

Equations

GameForm.LeftDeadEnd.flexibility g = if GameForm.LeftDeadEnd.IsInteger g then 0 else 1 + ⨆ (gr : ↑(Moves.moves Player.right g)), GameForm.LeftDeadEnd.flexibility ↑gr

Instances For

theorem GameForm.LeftDeadEnd.flexibility_of_isInteger {g : GameForm} (hg : IsInteger g) :

flexibility g = 0

theorem GameForm.LeftDeadEnd.flexibility_of_not_isInteger {g : GameForm} (hne : ¬IsInteger g) :

flexibility g = 1 + sSup ((fun (gr : GameForm) => flexibility gr) '' Moves.moves Player.right g)

theorem GameForm.LeftDeadEnd.flexibility_succ_le_of_mem_rightMoves {g gr : GameForm} (hg : IsLde g) (hgi : ¬IsInteger g) (hgr : gr ∈ Moves.moves Player.right g) :

flexibility gr + 1 ≤ flexibility g

theorem GameForm.LeftDeadEnd.terminalLengths_neg_intCast (n : ℕ) :

terminalLengths (-↑n) = {n}

theorem GameForm.LeftDeadEnd.exists_eq_neg_intCast_of_isInteger {g : GameForm} (hg : IsLde g) (hi : IsInteger g) :

∃ (n : ℕ), g = -↑n

@[irreducible]

theorem GameForm.LeftDeadEnd.isInteger_iff_terminalLengths_subsingleton {g : GameForm} (hg : IsLde g) :

IsInteger g ↔ (terminalLengths g).Subsingleton

A Left dead end $G$ is an integer if and only if $|T(G)| = 1$. In particular, $G = \overline{n}$ if and only if $T(G) = \{n\}$.

This is Davies (Lemma 3.15 on p. 15).

theorem GameForm.LeftDeadEnd.lde_race_zero_iff {g : GameForm} (hg : IsLde g) :

race g = 0 ↔ g = 0

See lde_zero_tfae.

theorem GameForm.LeftDeadEnd.race_le_succ_race_of_mem_rightMoves {g gr : GameForm} (hg : IsLde g) (hgr : gr ∈ Moves.moves Player.right g) :

race g ≤ race gr + 1

theorem GameForm.LeftDeadEnd.exists_mem_rightMoves_race_succ {g : GameForm} (hg : IsLde g) (hg0 : g ≠ 0) :

∃ gr ∈ Moves.moves Player.right g, race g = race gr + 1

@[irreducible]

theorem GameForm.LeftDeadEnd.terminalLengths_subset_of_ge {g h : GameForm} (hg : IsLde g) (hh : IsLde h) (hge : g ≥m Form.DeadEnding.ShortDeadEnding h) :

terminalLengths g ⊆ terminalLengths h

If $G$ and $H$ are Left dead ends with $G \ge H$, then $T(G) \subseteq T(H)$.

This is Davies (Theorem 3.17 on p. 16).

def GameForm.LeftDeadEnd.IsTerminalRun (l : List GameForm) :

If $G$ is a combinatorial game and $(G_0, G_1, \ldots, G_k)$ is a run of $G$ such that $G_k \cong 0$, then we say the run is terminal.

This is Davies (Definition 3.11 on p. 14).

Equations

GameForm.LeftDeadEnd.IsTerminalRun l = (GameForm.LeftDeadEnd.IsRun l ∧ l.getLast? = some 0)

Instances For

@[irreducible]

theorem GameForm.LeftDeadEnd.mem_terminalLengths_iff_exists_terminalRun {g : GameForm} (hg : IsLde g) {n : ℕ} :

n ∈ terminalLengths g ↔ ∃ (l : List GameForm), IsTerminalRun (g :: l) ∧ l.length = n

$n \in T(G)$ if and only if there exists a terminal run of $G$ of length $n$.

This is Davies (Definition 3.12 on p. 14), recovered as a theorem from the recursive definition of terminalLengths.

theorem GameForm.LeftDeadEnd.exists_run_terminalLengths_subset {g h : GameForm} (hg : IsLde g) (hh : IsLde h) (hge : g ≥m Form.DeadEnding.ShortDeadEnding h) {l : List GameForm} (hl : IsRun (g :: l)) :

∃ (m : List GameForm), IsRun (h :: m) ∧ List.Forall₂ (fun (a b : GameForm) => terminalLengths a ⊆ terminalLengths b) (g :: l) (h :: m)

This is Davies (Corollary 3.19 on p. 17).

theorem GameForm.LeftDeadEnd.race_ge_of_ge {g h : GameForm} (hg : IsLde g) (hh : IsLde h) (hge : g ≥m Form.DeadEnding.ShortDeadEnding h) :

race h ≤ race g

If $G$ and $H$ are Left dead ends with $G \ge H$, then $r(G) \ge r(H)$.

This is the race half of Davies (Corollary 3.18 on p. 16).

@[irreducible]

theorem GameForm.LeftDeadEnd.birthday_eq_sSup_terminalLengths {g : GameForm} (hg : IsLde g) :

Form.birthday g = ↑(sSup (terminalLengths g))

On a Left dead end, $b(G) = \max(T(G))$.

theorem GameForm.LeftDeadEnd.birthday_le_of_ge {g h : GameForm} (hg : IsLde g) (hh : IsLde h) (hge : g ≥m Form.DeadEnding.ShortDeadEnding h) :

Form.birthday g ≤ Form.birthday h

If $G$ and $H$ are Left dead ends with $G \ge H$, then $b(G) \le b(H)$.

This is the birthday half of Davies (Corollary 3.18 on p. 16).

theorem GameForm.LeftDeadEnd.terminalLengths_eq_of_misereEQ {g h : GameForm} (hg : IsLde g) (hh : IsLde h) (heq : g =m Form.DeadEnding.ShortDeadEnding h) :

terminalLengths g = terminalLengths h

theorem GameForm.LeftDeadEnd.birthday_eq_of_misereEQ {g h : GameForm} (hg : IsLde g) (hh : IsLde h) (heq : g =m Form.DeadEnding.ShortDeadEnding h) :

Form.birthday g = Form.birthday h

theorem GameForm.LeftDeadEnd.isInteger_iff_of_misereEQ {g h : GameForm} (hg : IsLde g) (hh : IsLde h) (heq : g =m Form.DeadEnding.ShortDeadEnding h) :

IsInteger g ↔ IsInteger h

theorem GameForm.LeftDeadEnd.birthday_pos_of_ne_zero {g : GameForm} (hg : IsLde g) (hg0 : g ≠ 0) :

0 < Form.birthday g

theorem GameForm.LeftDeadEnd.lde_zero_tfae {g : GameForm} (hg : IsLde g) :

[g =m Form.DeadEnding.ShortDeadEnding 0, g = 0, 0 ∈ terminalLengths g, race g = 0, Form.birthday g = 0].TFAE

If $G$ is a Left dead end, then the following are equivalent: $G = 0$; $G \cong 0$; $0 \in T(G)$; $r(G) = 0$; $b(G) = 0$.

This is Davies (Lemma 3.16 on p. 15).

theorem GameForm.LeftDeadEnd.race_eq_of_misereEQ {g h : GameForm} (hg : IsLde g) (hh : IsLde h) (heq : g =m Form.DeadEnding.ShortDeadEnding h) :

race g = race h

theorem GameForm.LeftDeadEnd.exists_mem_rightMoves_birthday_succ {g : GameForm} (hg : IsLde g) (hg0 : g ≠ 0) :

∃ gr ∈ Moves.moves Player.right g, Form.birthday g = Form.birthday gr + 1

@[irreducible]

theorem GameForm.LeftDeadEnd.terminalLengths_add {g h : GameForm} (hg : IsLde g) (hh : IsLde h) :

terminalLengths (g + h) = {x : ℕ | ∃ a ∈ terminalLengths g, ∃ b ∈ terminalLengths h, a + b = x}

If $G$ and $H$ are Left dead ends, then $T(G + H) = T(G) + T(H)$, a Minkowski sum.

This is Davies (Proposition 3.20 on p. 18).

theorem GameForm.LeftDeadEnd.not_isInteger_add_of_not_isInteger_right {h k : GameForm} (hh : IsLde h) (hk : IsLde k) (hk_ni : ¬IsInteger k) :

¬IsInteger (h + k)

theorem GameForm.LeftDeadEnd.isInteger_add_neg_intCast_iff {h : GameForm} (hh : IsLde h) (n : ℕ) :

IsInteger (h + -↑n) ↔ IsInteger h

@[irreducible]

theorem GameForm.LeftDeadEnd.birthday_lt_flexibility_add_of_not_isInteger {h k : GameForm} (hh : IsLde h) (hk : IsLde k) (hh0 : h ≠ 0) (hk_ni : ¬IsInteger k) :

Form.birthday h < ↑(flexibility (h + k))

theorem GameForm.LeftDeadEnd.race_add {g h : GameForm} (hg : IsLde g) (hh : IsLde h) :

race (g + h) = race g + race h

If $G$ and $H$ are Left dead ends, then $r(G + H) = r(G) + r(H)$.

This is the race half of Davies (Proposition 3.20 on p. 18).

theorem GameForm.LeftDeadEnd.race_lt_sSup_terminalLengths {g : GameForm} (hg : IsLde g) (hgi : ¬IsInteger g) :

race g < sSup (terminalLengths g)

theorem GameForm.LeftDeadEnd.ncard_terminalLengths_add_ge {g h : GameForm} (hg : IsLde g) (hh : IsLde h) :

max (terminalLengths g).ncard (terminalLengths h).ncard ≤ (terminalLengths (g + h)).ncard

If $G$ and $H$ are Left dead ends, then $|T(G + H)| \ge \max(|T(G)|, |T(H)|)$.

This is the inequality half of Davies (Corollary 3.21 on p. 18).

theorem GameForm.LeftDeadEnd.ncard_terminalLengths_add_eq_max_iff {g h : GameForm} (hg : IsLde g) (hh : IsLde h) :

(terminalLengths (g + h)).ncard = max (terminalLengths g).ncard (terminalLengths h).ncard ↔ IsInteger g ∨ IsInteger h

If $G$ and $H$ are Left dead ends, then $|T(G + H)| \ge \max(|T(G)|, |T(H)|)$, with equality if and only if at least one of $G$ and $H$ is an integer.

This is Davies (Corollary 3.21 on p. 18).

Pocancellativity and cancellativity #

def GameForm.LeftDeadEnd.IsPocancellativeIn (A : GameForm → Prop) (j : GameForm) :

Equations

GameForm.LeftDeadEnd.IsPocancellativeIn A j = ∀ (g h : GameForm), A g → A h → (g + j) ≥m A h + j → g ≥m A h

Instances For

def GameForm.LeftDeadEnd.IsCancellativeIn (A : GameForm → Prop) (j : GameForm) :

Equations

GameForm.LeftDeadEnd.IsCancellativeIn A j = ∀ (g h : GameForm), A g → A h → (g + j) =m A h + j → g =m A h

Instances For

theorem GameForm.LeftDeadEnd.lde_ge_of_add_pocancellative {A : GameForm → Prop} {g h j : GameForm} (hgA : A g) (hhA : A h) (hj : IsPocancellativeIn A j) (hge : (g + j) ≥m A h + j) :

g ≥m A h

If $\mathcal{U}$ is a universe, $G, H \in \mathcal{U}$ are Left dead ends, and $J$ is a pocancellative element of $\mathcal{U}$ satisfying $G + J \ge H + J$, then $G \ge H$.

This is Davies (Lemma 3.5 on p. 12).

theorem GameForm.LeftDeadEnd.lde_misereEQ_of_add_cancellative {A : GameForm → Prop} {g h j : GameForm} (hgA : A g) (hhA : A h) (hj : IsCancellativeIn A j) (heq : (g + j) =m A h + j) :

g =m A h

If $\mathcal{U}$ is a universe, $G, H \in \mathcal{U}$ are Left dead ends, and $J$ is a cancellative element of $\mathcal{U}$ satisfying $G + J = H + J$, then $G = H$.

This is Davies (Lemma 3.6 on p. 12).

theorem GameForm.LeftDeadEnd.isPocancellativeIn_of_add_neg {A : GameForm → Prop} [Form.ClosedUnderAdd A] [Form.ClosedUnderNeg A] {j : GameForm} (hj : A j) (hinv : (j + -j) =m A 0) :

IsPocancellativeIn A j

theorem GameForm.LeftDeadEnd.isCancellativeIn_of_add_neg {A : GameForm → Prop} [Form.ClosedUnderAdd A] [Form.ClosedUnderNeg A] {j : GameForm} (hj : A j) (hinv : (j + -j) =m A 0) :

IsCancellativeIn A j

@[irreducible]

theorem GameForm.LeftDeadEnd.winsGoingFirst_left_neg_add (a b : GameForm) :

IsLde a → IsLde b → (race a ≤ race b → Form.Misere.Outcome.WinsGoingFirst Player.left (-a + b)) ∧ (race a < race b → ¬Form.Misere.Outcome.WinsGoingFirst Player.right (-a + b))

If $G$ is a dead Right end and $H$ is a dead Left end, then $o^-(G + H)$ is $\mathcal{N}^-$ when $l(G) = r(H)$, $\mathcal{L}^-$ when $l(G) < r(H)$, and $\mathcal{R}^-$ when $l(G) > r(H)$.

This is Milley, Renault (Lemma 5 on p. 7).

@[irreducible]

theorem GameForm.LeftDeadEnd.lde_add_neg_misereEQ {k : GameForm} (hk : IsLde k) :

(k + -k) =m Form.DeadEnding.ShortDeadEnding 0

If $G$ is a dead end then $G + \overline{G} \equiv 0 \pmod{\mathcal{E}}$.

This is Milley, Renault (Theorem 6 on p. 8).

IsPocancellativeIn Form.DeadEnding.ShortDeadEnding k

theorem GameForm.LeftDeadEnd.isPocancellativeIn_of_isLde {k : GameForm} (hk : IsLde k) :

theorem GameForm.LeftDeadEnd.lde_pocancellative {g h k : GameForm} (hg : IsLde g) (hh : IsLde h) (hk : IsLde k) (hge : (g + k) ≥m Form.DeadEnding.ShortDeadEnding h + k) :

g ≥m Form.DeadEnding.ShortDeadEnding h

The monoid of Left dead ends $\mathcal{L}$ is pocancellative.

This is Davies (Theorem 3.7 on p. 12).

theorem GameForm.LeftDeadEnd.lde_cancellative {g h k : GameForm} (hg : IsLde g) (hh : IsLde h) (hk : IsLde k) (heq : (g + k) =m Form.DeadEnding.ShortDeadEnding h + k) :

g =m Form.DeadEnding.ShortDeadEnding h

The monoid of Left dead ends $\mathcal{L}$ is cancellative.

This is Davies (Theorem 3.7 on p. 12).

theorem GameForm.LeftDeadEnd.isLde_nsmul {g : GameForm} (hg : IsLde g) (n : ℕ) :

IsLde (n • g)

theorem GameForm.LeftDeadEnd.add_nsmul_mem_rightMoves {g gr : GameForm} (hgr : gr ∈ Moves.moves Player.right g) (n : ℕ) :

gr + n • g ∈ Moves.moves Player.right ((n + 1) • g)

theorem GameForm.LeftDeadEnd.exists_eq_add_nsmul_of_mem_rightMoves {g : GameForm} (n : ℕ) {x : GameForm} (hx : x ∈ Moves.moves Player.right ((n + 1) • g)) :

∃ gr ∈ Moves.moves Player.right g, x = gr + n • g

theorem GameForm.LeftDeadEnd.nsmul_misereEQ_nsmul {a b : GameForm} (ha : IsLde a) (hb : IsLde b) (hab : a =m Form.DeadEnding.ShortDeadEnding b) (n : ℕ) :

(n • a) =m Form.DeadEnding.ShortDeadEnding n • b

theorem GameForm.LeftDeadEnd.lde_nsmul_cancel {g h : GameForm} (hg : IsLde g) (hh : IsLde h) {n : ℕ} (hn : 0 < n) (heq : (n • g) =m Form.DeadEnding.ShortDeadEnding n • h) :

g =m Form.DeadEnding.ShortDeadEnding h

If $G$ and $H$ are Left dead ends with $n \cdot G = n \cdot H$ for some $n > 0$, then $G = H$.

This is Davies (Proposition 3.8 on p. 13).

def GameForm.LeftDeadEnd.pocancellativeNotInvertible (A : GameForm → Prop) :

Set GameForm

This is Davies (Open problem E.1 on p. 49).

Equations

GameForm.LeftDeadEnd.pocancellativeNotInvertible A = {j : GameForm | A j ∧ GameForm.LeftDeadEnd.IsPocancellativeIn A j ∧ ¬∃ (k : GameForm), A k ∧ (j + k) =m A 0}

Instances For

Divisibility, atoms, primes and factorisations #

def GameForm.LeftDeadEnd.LdeDvd (g h : GameForm) :

Equations

GameForm.LeftDeadEnd.LdeDvd g h = ∃ (k : GameForm), GameForm.LeftDeadEnd.IsLde k ∧ h =m Form.DeadEnding.ShortDeadEnding g + k

Instances For

def GameForm.LeftDeadEnd.IsLdeAtom (g : GameForm) :

Equations

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

Instances For

def GameForm.LeftDeadEnd.IsMolecule (g : GameForm) :

In a monoid $M$, we call a non-invertible element $m \in M$ a molecule if $m$ is atomic but not an atom.

This is Davies (Definition 2.6 on p. 9).

Equations

GameForm.LeftDeadEnd.IsMolecule g = (GameForm.LeftDeadEnd.IsLde g ∧ g ≠ 0 ∧ ¬GameForm.LeftDeadEnd.IsLdeAtom g)

Instances For

def GameForm.LeftDeadEnd.IsLdePrime (p : GameForm) :

Equations

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

Instances For

def GameForm.LeftDeadEnd.IsFactorisation (s : Multiset GameForm) (g : GameForm) :

Equations

GameForm.LeftDeadEnd.IsFactorisation s g = ((∀ a ∈ s, GameForm.LeftDeadEnd.IsLdeAtom a) ∧ s.sum =m Form.DeadEnding.ShortDeadEnding g)

Instances For

def GameForm.LeftDeadEnd.UniquelyFactorisable (g : GameForm) :

Equations

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

Instances For

def GameForm.LeftDeadEnd.IsPrimeFactorisable (g : GameForm) :

Equations

GameForm.LeftDeadEnd.IsPrimeFactorisable g = ∃ (s : Multiset GameForm), (∀ a ∈ s, GameForm.LeftDeadEnd.IsLdePrime a) ∧ s.sum =m Form.DeadEnding.ShortDeadEnding g

Instances For

theorem GameForm.LeftDeadEnd.lde_atomic {g : GameForm} (hg : IsLde g) :

∃ (s : Multiset GameForm), IsFactorisation s g

The monoid of Left dead ends $\mathcal{L}$ is atomic.

This is Davies (Lemma 3.23 on p. 19).

theorem GameForm.LeftDeadEnd.birthday_lt_of_add {g h k : GameForm} (hg : IsLde g) (hh : IsLde h) (hk : IsLde k) (hk0 : k ≠ 0) (heq : g =m Form.DeadEnding.ShortDeadEnding h + k) :

Form.birthday h < Form.birthday g

If $G$, $H$, and $K$ are non-zero Left dead ends with $G = H + K$, then $b(H) < b(G)$.

This is Davies (Lemma 3.22 on p. 19).

theorem GameForm.LeftDeadEnd.card_le_race_sum {s : Multiset GameForm} (hs : ∀ a ∈ s, IsLdeAtom a) :

s.card ≤ race s.sum

theorem GameForm.LeftDeadEnd.factorisation_length_le_race {g : GameForm} (hg : IsLde g) {s : Multiset GameForm} (hs : IsFactorisation s g) :

s.card ≤ race g

The monoid of Left dead ends $\mathcal{L}$ is a BF-monoid. In particular, if $G$ is a Left dead end, then the length of each factorisation of $G$ is at most $r(G)$; that is, $\overline{\mathsf{L}(G)} \le r(G)$.

This is Davies (Lemma 3.24 on p. 19).

theorem GameForm.LeftDeadEnd.lde_atom_of_race_one {g : GameForm} (hg : IsLde g) (hr : race g = 1) :

If $G$ is a Left dead end with $r(G) = 1$, then $G$ is an atom.

This is Davies (Corollary 3.25 on p. 20).

theorem GameForm.LeftDeadEnd.IsLdeAtom.of_misereEQ {a g : GameForm} (ha : IsLdeAtom a) (hg : IsLde g) (heq : a =m Form.DeadEnding.ShortDeadEnding g) :

theorem GameForm.LeftDeadEnd.lde_ff {g : GameForm} (hg : IsLde g) :

{s : Multiset GameForm | IsFactorisation s g}.Finite

The monoid of Left dead ends $\mathcal{L}$ is an FF-monoid.

This is Davies (Theorem 3.26 on p. 20).

The prime $\overline{1}$ #

@[irreducible]

theorem GameForm.LeftDeadEnd.neg_one_add_option_ge {g gr : GameForm} (hg : IsLde g) (hgr : gr ∈ Moves.moves Player.right g) :

(-1 + gr) ≥m Form.DeadEnding.ShortDeadEnding g

If $G$ is a Left dead end, then $\overline{1} + G' \ge G$ for every option $G'$ of $G$.

This is Davies (Lemma 4.1 on p. 20).

theorem GameForm.LeftDeadEnd.isLde_singletonRight {g : GameForm} (hg : IsLde g) :

IsLde !{∅ | {g}}

theorem GameForm.LeftDeadEnd.rightMoves_singletonRight {g : GameForm} :

Moves.moves Player.right !{∅ | {g}} = {g}

theorem GameForm.LeftDeadEnd.neg_one_add_eq_singleton {g : GameForm} (hg : IsLde g) :

(-1 + g) =m Form.DeadEnding.ShortDeadEnding !{∅ | {g}}

If $G$ is a Left dead end, then $\overline{1} + G = \{\cdot \mid G\}$.

This is Davies (Proposition 4.2 on p. 21).

theorem GameForm.LeftDeadEnd.unique_good_option_iff {g gr : GameForm} (hg : IsLde g) (hgr : IsLde gr) :

(∃ (x : GameForm), IsGoodOption x g ∧ x =m Form.DeadEnding.ShortDeadEnding gr ∧ ∀ (y : GameForm), IsGoodOption y g → y =m Form.DeadEnding.ShortDeadEnding gr) ↔ g =m Form.DeadEnding.ShortDeadEnding-1 + gr

If $G$ and $G'$ are Left dead ends, then $G$ has exactly one good option (equal to) $G'$ if and only if $G = \overline{1} + G'$.

This is Davies (Proposition 4.3 on p. 21).

theorem GameForm.LeftDeadEnd.neg_one_prime :

IsLdePrime (-1)

The game $\overline{1}$ is prime in the monoid of Left dead ends $\mathcal{L}$.

This is Davies (Theorem 4.4 on p. 21).

theorem GameForm.LeftDeadEnd.neg_intCast_add (a b : ℕ) :

-↑(a + b) = -↑a + -↑b

theorem GameForm.LeftDeadEnd.neg_intCast_injective :

Function.Injective fun (n : ℕ) => -↑n

@[simp]

theorem GameForm.LeftDeadEnd.neg_intCast_eq_zero_iff {n : ℕ} :

-↑n = 0 ↔ n = 0

theorem GameForm.LeftDeadEnd.nsmul_neg_one (n : ℕ) :

n • -1 = -↑n

theorem GameForm.LeftDeadEnd.neg_intCast_eq_of_misereEQ {a b : ℕ} (hab : (-↑a) =m Form.DeadEnding.ShortDeadEnding -↑b) :

a = b

theorem GameForm.LeftDeadEnd.eq_neg_one_of_isLdeAtom_of_isInteger {a : GameForm} (ha : IsLdeAtom a) (hi : IsInteger a) :

a = -1

theorem GameForm.LeftDeadEnd.eq_replicate_of_isFactorisation_neg_intCast {n : ℕ} {s : Multiset GameForm} (hs : IsFactorisation s (-↑n)) :

s = Multiset.replicate n (-1)

theorem GameForm.LeftDeadEnd.neg_intCast_uniquelyFactorisable (n : ℕ) :

UniquelyFactorisable (-↑n)

@[irreducible]

theorem GameForm.LeftDeadEnd.neg_intCast_ge_of_mem_terminalLengths {y : GameForm} (hy : IsLde y) {k : ℕ} (hk : k ∈ terminalLengths y) :

(-↑k) ≥m Form.DeadEnding.ShortDeadEnding y

def GameForm.LeftDeadEnd.LdeOtherPrimeProblem :

This is Davies (Open problem 4.5 on p. 22).

Equations

GameForm.LeftDeadEnd.LdeOtherPrimeProblem = ∃ (p : GameForm), GameForm.LeftDeadEnd.IsLdePrime p ∧ ¬p =m Form.DeadEnding.ShortDeadEnding-1

Instances For

def GameForm.LeftDeadEnd.LdeNonPrimeAtomProblem :

This is Davies (Open problem 4.5 on p. 22).

Equations

GameForm.LeftDeadEnd.LdeNonPrimeAtomProblem = ∃ (a : GameForm), GameForm.LeftDeadEnd.IsLdeAtom a ∧ ¬GameForm.LeftDeadEnd.IsLdePrime a

Instances For

Flexibility and the atom criteria #

theorem GameForm.LeftDeadEnd.ge_of_flexibility_le_one {g h : GameForm} (hg : IsLde g) (hh : IsLde h) (hf : flexibility g ≤ 1) (hT : terminalLengths g ⊆ terminalLengths h) :

g ≥m Form.DeadEnding.ShortDeadEnding h

If $G$ and $H$ are Left dead ends with $f(G) \le 1$ and $T(G) \subseteq T(H)$, then $G \ge H$.

This is Davies (Proposition 5.2 on p. 23).

def GameForm.LeftDeadEnd.IsVersatileOption (gr g : GameForm) :

If $G$ is a Left dead end, then we say an option $G'$ of $G$ is versatile if $f(G') \ge f(G) - 1$.

This is Davies (Definition 5.3 on p. 23).

Equations

GameForm.LeftDeadEnd.IsVersatileOption gr g = (gr ∈ Moves.moves Player.right g ∧ GameForm.LeftDeadEnd.flexibility g ≤ GameForm.LeftDeadEnd.flexibility gr + 1)

Instances For

theorem GameForm.LeftDeadEnd.exists_isVersatileOption {g : GameForm} (hg : IsLde g) (hg0 : g ≠ 0) :

∃ (gr : GameForm), IsVersatileOption gr g

theorem GameForm.LeftDeadEnd.flexibility_eq_of_isVersatileOption {g gr : GameForm} (hg : IsLde g) (hgi : ¬IsInteger g) (hgr : IsVersatileOption gr g) :

flexibility g = flexibility gr + 1

theorem GameForm.LeftDeadEnd.two_le_sSup_terminalLengths {g : GameForm} (hg : IsLde g) (hg0 : g ≠ 0) (hgi : ¬IsInteger g) :

2 ≤ sSup (terminalLengths g)

@[irreducible]

theorem GameForm.LeftDeadEnd.flexibility_lt_birthday_of_ne_zero {g : GameForm} (hg : IsLde g) (hg0 : g ≠ 0) :

↑(flexibility g) < Form.birthday g

See flexibility_le_birthday.

theorem GameForm.LeftDeadEnd.flexibility_le_birthday {g : GameForm} (hg : IsLde g) :

↑(flexibility g) ≤ Form.birthday g

If $G$ is a Left dead end, then $f(G) \le b(G)$, with equality if and only if $G = 0$.

This is Davies (Lemma 5.4 on p. 24).

theorem GameForm.LeftDeadEnd.flexibility_eq_birthday_iff {g : GameForm} (hg : IsLde g) :

↑(flexibility g) = Form.birthday g ↔ g = 0

See flexibility_le_birthday.

@[irreducible]

theorem GameForm.LeftDeadEnd.flexibility_le_of_ge {g h : GameForm} (hg : IsLde g) (hh : IsLde h) (hge : g ≥m Form.DeadEnding.ShortDeadEnding h) :

flexibility g ≤ flexibility h

If $G$ and $H$ are Left dead ends with $G \ge H$, then $f(G) \le f(H)$.

This is Davies (Proposition 5.5 on p. 24).

theorem GameForm.LeftDeadEnd.flexibility_eq_of_misereEQ {g h : GameForm} (hg : IsLde g) (hh : IsLde h) (heq : g =m Form.DeadEnding.ShortDeadEnding h) :

flexibility g = flexibility h

def GameForm.LeftDeadEnd.IsFlexibleRun (l : List GameForm) :

If $G$ is a Left dead end, then we say a run $(G_0, G_1, \ldots, G_n)$ of $G$ of length $n > 0$ is flexible if $G_i$ is not an integer for $i < n$. We define all runs of length $0$ to be flexible.

This is Davies (Definition 5.6 on p. 25).

Equations

GameForm.LeftDeadEnd.IsFlexibleRun l = (GameForm.LeftDeadEnd.IsRun l ∧ ∀ x ∈ l.dropLast, ¬GameForm.LeftDeadEnd.IsInteger x)

Instances For

def GameForm.LeftDeadEnd.IsMaximalFlexibleRun (l : List GameForm) :

A flexible run is maximal if it ends at an integer; that is, if it cannot be extended to a longer flexible run.

This is Davies (Definition 5.6 on p. 25).

Equations

GameForm.LeftDeadEnd.IsMaximalFlexibleRun l = (GameForm.LeftDeadEnd.IsFlexibleRun l ∧ ∀ x ∈ l.getLast?, GameForm.LeftDeadEnd.IsInteger x)

Instances For

theorem GameForm.LeftDeadEnd.length_le_flexibility_of_isFlexibleRun {g : GameForm} (hg : IsLde g) {l : List GameForm} (hl : IsFlexibleRun (g :: l)) :

l.length ≤ flexibility g

@[irreducible]

theorem GameForm.LeftDeadEnd.exists_isMaximalFlexibleRun_length_eq {g : GameForm} (hg : IsLde g) :

∃ (l : List GameForm), IsMaximalFlexibleRun (g :: l) ∧ l.length = flexibility g

theorem GameForm.LeftDeadEnd.flexibility_eq_sSup_flexibleRun_length {g : GameForm} (hg : IsLde g) :

flexibility g = sSup {n : ℕ | ∃ (l : List GameForm), IsFlexibleRun (g :: l) ∧ l.length = n}

If $G$ is a Left dead end, then $f(G)$ is equal to the length of a longest flexible run of $G$.

This is Davies (Lemma 5.7 on p. 25).

def GameForm.LeftDeadEnd.IsRacingOption (gr g : GameForm) :

If $G$ is a Left dead end, then we define a racing option of $G$ to be an option $G'$ such that $r(G') = r(G) - 1$.

This is Davies (Definition 5.8 on p. 25).

Equations

GameForm.LeftDeadEnd.IsRacingOption gr g = (gr ∈ Moves.moves Player.right g ∧ GameForm.LeftDeadEnd.race g = GameForm.LeftDeadEnd.race gr + 1)

Instances For

def GameForm.LeftDeadEnd.IsStallingOption (gr g : GameForm) :

If $G$ is a Left dead end, then we define a stalling option of $G$ to be an option $G'$ such that $b(G') = b(G) - 1$.

This is Davies (Definition 5.9 on p. 25).

Equations

GameForm.LeftDeadEnd.IsStallingOption gr g = (gr ∈ Moves.moves Player.right g ∧ Form.birthday g = Form.birthday gr + 1)

Instances For

theorem GameForm.LeftDeadEnd.exists_isRacingOption {g : GameForm} (hg : IsLde g) (hg0 : g ≠ 0) :

∃ (gr : GameForm), IsRacingOption gr g

theorem GameForm.LeftDeadEnd.exists_isStallingOption {g : GameForm} (hg : IsLde g) (hg0 : g ≠ 0) :

∃ (gr : GameForm), IsStallingOption gr g

theorem GameForm.LeftDeadEnd.flexibility_singletonRight {x : GameForm} (hx : IsLde x) (hxi : ¬IsInteger x) :

flexibility !{∅ | {x}} = flexibility x + 1

theorem GameForm.LeftDeadEnd.flexibility_add_neg_intCast {g : GameForm} (hg : IsLde g) (hgi : ¬IsInteger g) (n : ℕ) :

flexibility (g + -↑n) = flexibility g + n

If $G$ is a non-integer Left dead end, then $f(G + \overline{n}) = f(G) + n$ for all $n \ge 0$.

This is Davies (Proposition 5.10(1) on p. 26).

theorem GameForm.LeftDeadEnd.flexibility_neg_intCast_add {h : GameForm} (hh : IsLde h) (hhi : ¬IsInteger h) (n : ℕ) :

flexibility (-↑n + h) = flexibility h + n

See flexibility_add_neg_intCast.

@[irreducible]

theorem GameForm.LeftDeadEnd.flexibility_add {g h : GameForm} (hg : IsLde g) (hh : IsLde h) (hgi : ¬IsInteger g) (hhi : ¬IsInteger h) :

↑(flexibility (g + h)) = max (Form.birthday g + ↑(flexibility h)) (↑(flexibility g) + Form.birthday h)

If $G$ and $H$ are non-integer Left dead ends, then $f(G + H) = \max(b(G) + f(H), f(G) + b(H))$.

This is Davies (Proposition 5.10(2) on p. 26).

theorem GameForm.LeftDeadEnd.birthday_lt_flexibility_of_ge {g h k : GameForm} (hg : IsLde g) (hh : IsLde h) (hk : IsLde k) (hh0 : h ≠ 0) (hk_ni : ¬IsInteger k) (hge : (h + k) ≥m Form.DeadEnding.ShortDeadEnding g) :

Form.birthday h < ↑(flexibility g)

If $G$, $H$, and $K$ are Left dead ends such that $H$ is non-zero, $K$ is not an integer, and $H + K \ge G$, then $b(H) < f(G)$.

This is Davies (Proposition 5.11 on p. 27).

theorem GameForm.LeftDeadEnd.isInteger_neg_intCast (n : ℕ) :

IsInteger (-↑n)

theorem GameForm.LeftDeadEnd.not_isInteger_of_multi_good {g h k : GameForm} (hg : IsLde g) (hh : IsLde h) (hk : IsLde k) (hk0 : k ≠ 0) (hmulti : ∃ (a : GameForm) (b : GameForm), IsGoodOption a g ∧ IsGoodOption b g ∧ ¬a =m Form.DeadEnding.ShortDeadEnding b) (heq : g =m Form.DeadEnding.ShortDeadEnding h + k) :

¬IsInteger k

theorem GameForm.LeftDeadEnd.birthday_lt_flexibility_of_multi_good {g h k : GameForm} (hg : IsLde g) (hh : IsLde h) (hk : IsLde k) (hh0 : h ≠ 0) (hk0 : k ≠ 0) (hmulti : ∃ (a : GameForm) (b : GameForm), IsGoodOption a g ∧ IsGoodOption b g ∧ ¬a =m Form.DeadEnding.ShortDeadEnding b) (heq : g =m Form.DeadEnding.ShortDeadEnding h + k) :

Form.birthday h < ↑(flexibility g) ∧ Form.birthday k < ↑(flexibility g)

If $G$ is a Left dead end with more than one good option, then, for any non-zero Left dead ends $H$ and $K$ with $H + K = G$, it holds that $b(H), b(K) < f(G)$.

This is Davies (Corollary 5.12 on p. 28).

theorem GameForm.LeftDeadEnd.atom_of_birthday_gt {g : GameForm} (hg : IsLde g) (hmulti : ∃ (a : GameForm) (b : GameForm), IsGoodOption a g ∧ IsGoodOption b g ∧ ¬a =m Form.DeadEnding.ShortDeadEnding b) (hb : ↑(flexibility g) + ↑(flexibility g) < Form.birthday g + 2) :

If $G$ is a Left dead end with more than one good option, and $b(G) > 2 \cdot f(G) - 2$, then $G$ is an atom.

This is Davies (Corollary 5.13 on p. 28).

theorem GameForm.LeftDeadEnd.atom_of_flexibility_one {g : GameForm} (hg : IsLde g) (hf : flexibility g = 1) :

If $G$ is a Left dead end with $f(G) = 1$, then $G$ is an atom.

This is Davies (Proposition 5.14 on p. 28).

theorem GameForm.LeftDeadEnd.atom_of_flexibility_two {g : GameForm} (hg : IsLde g) (hf : flexibility g = 2) :

HasUniqueGoodOption g ∨ IsLdeAtom g

If $G$ is a Left dead end with $f(G) = 2$, then either $G$ has exactly one good option (i.e. $\overline{1} \mid G$), or $G$ is an atom.

This is Davies (Proposition 5.14 on p. 28).

theorem GameForm.LeftDeadEnd.misereEQ_of_flexibility_le_one {g h : GameForm} (hg : IsLde g) (hh : IsLde h) (hfg : flexibility g ≤ 1) (hfh : flexibility h ≤ 1) (hT : terminalLengths g = terminalLengths h) :

g =m Form.DeadEnding.ShortDeadEnding h

theorem GameForm.LeftDeadEnd.terminalLengths_of_birthday_two {g : GameForm} (hg : IsLde g) (hgi : ¬IsInteger g) (hb : Form.birthday g = 2) :

terminalLengths g = {1, 2}

theorem GameForm.LeftDeadEnd.terminalLengths_waitingGame_one :

terminalLengths (waitingGame 1) = {1}

theorem GameForm.LeftDeadEnd.terminalLengths_waitingGame_two :

terminalLengths (waitingGame 2) = {1, 2}

theorem GameForm.LeftDeadEnd.birthday_waitingGame_two :

Form.birthday (waitingGame 2) = 2

theorem GameForm.LeftDeadEnd.not_isInteger_waitingGame_two :

¬IsInteger (waitingGame 2)

theorem GameForm.LeftDeadEnd.eq_neg_two_or_misereEQ_waitingGame_two {g : GameForm} (hg : IsLde g) (hb : Form.birthday g = 2) :

g = -2 ∨ g =m Form.DeadEnding.ShortDeadEnding waitingGame 2

theorem GameForm.LeftDeadEnd.atom_of_flexibility_three {g : GameForm} (hg : IsLde g) (hf : flexibility g = 3) :

HasUniqueGoodOption g ∨ g =m Form.DeadEnding.ShortDeadEnding 2 • waitingGame 2 ∨ IsLdeAtom g

If $G$ is a Left dead end with $f(G) = 3$, then either $G$ has exactly one good option, $G = 2 \cdot W_2$, or $G$ is an atom.

This is Davies (Proposition 5.14 on p. 28).

Lengths of factorisations #

def GameForm.LeftDeadEnd.longestFactorisationLen (g : GameForm) :

ℕ

$\overline{\mathsf{L}(G)}$, the length of a longest factorisation of $G$, with $\overline{\mathsf{L}(0)} = 0$.

Equations

GameForm.LeftDeadEnd.longestFactorisationLen g = sSup {n : ℕ | ∃ (s : Multiset GameForm), GameForm.LeftDeadEnd.IsFactorisation s g ∧ s.card = n}

Instances For

theorem GameForm.LeftDeadEnd.bddAbove_factorisationLen {g : GameForm} (hg : IsLde g) :

BddAbove {n : ℕ | ∃ (s : Multiset GameForm), IsFactorisation s g ∧ s.card = n}

theorem GameForm.LeftDeadEnd.card_le_longestFactorisationLen {g : GameForm} (hg : IsLde g) {s : Multiset GameForm} (hs : IsFactorisation s g) :

s.card ≤ longestFactorisationLen g

theorem GameForm.LeftDeadEnd.exists_isFactorisation_card_longestFactorisationLen {g : GameForm} (hg : IsLde g) :

∃ (s : Multiset GameForm), IsFactorisation s g ∧ s.card = longestFactorisationLen g

theorem GameForm.LeftDeadEnd.longestFactorisationLen_eq_of_misereEQ {g h : GameForm} (heq : g =m Form.DeadEnding.ShortDeadEnding h) :

longestFactorisationLen g = longestFactorisationLen h

theorem GameForm.LeftDeadEnd.exists_eq_add_sum_of_mem_rightMoves_sum {s : Multiset GameForm} {x : GameForm} (hx : x ∈ Moves.moves Player.right s.sum) :

∃ (a : GameForm) (t : Multiset GameForm), s = a ::ₘ t ∧ ∃ ar ∈ Moves.moves Player.right a, x = ar + t.sum

theorem GameForm.LeftDeadEnd.longestLen_le_good_option {g gr : GameForm} (hg : IsLde g) (hgr : IsGoodOption gr g) :

longestFactorisationLen g ≤ longestFactorisationLen gr + 1

If $G$ is a Left dead end, then $\overline{\mathsf{L}(G)} \le \overline{\mathsf{L}(G')} + 1$ for every good option $G'$ of $G$.

This is Davies (Lemma 6.1 on p. 30).

theorem GameForm.LeftDeadEnd.isLdeAtom_neg_one :

IsLdeAtom (-1)

theorem GameForm.LeftDeadEnd.longestLen_of_unique_good {g gr : GameForm} (hg : IsLde g) (hgr : IsLde gr) (hgood : IsGoodOption gr g) (huniq : ∀ (gr' : GameForm), IsGoodOption gr' g → gr' =m Form.DeadEnding.ShortDeadEnding gr) :

longestFactorisationLen g = longestFactorisationLen gr + 1

If $G$ is a Left dead end with exactly one good option $G'$, then $\overline{\mathsf{L}(G)} = \overline{\mathsf{L}(G')} + 1$.

This is Davies (Theorem 6.2 on p. 30).

theorem GameForm.LeftDeadEnd.longestLen_bound {g : GameForm} (hg : IsLde g) (hmulti : ∃ (a : GameForm) (b : GameForm), IsGoodOption a g ∧ IsGoodOption b g ∧ ¬a =m Form.DeadEnding.ShortDeadEnding b) :

longestFactorisationLen g ≤ race g ∧ (∀ (gr : GameForm), IsGoodOption gr g → longestFactorisationLen g ≤ longestFactorisationLen gr + 1) ∧ longestFactorisationLen g + 1 ≤ (terminalLengths g).ncard ∧ 2 * longestFactorisationLen g ≤ flexibility g + 1

If $G$ is a Left dead end with more than one good option, then $$\overline{\mathsf{L}(G)} \le \min\left\{r(G),\ \overline{\mathsf{L}(G')} + 1,\ |T(G)| - 1,\ \frac{f(G) + 1}{2}\right\},$$ where $G'$ ranges over all good options of $G$.

This is Davies (Theorem 6.3 on p. 30).

@[simp]

theorem GameForm.LeftDeadEnd.longestFactorisationLen_zero :

longestFactorisationLen 0 = 0

theorem GameForm.LeftDeadEnd.longestFactorisationLen_isLdeAtom {a : GameForm} (ha : IsLdeAtom a) :

longestFactorisationLen a = 1

theorem GameForm.LeftDeadEnd.isLdeAtom_of_longestLen_le_one {g : GameForm} (hg : IsLde g) (hg0 : g ≠ 0) (hL : longestFactorisationLen g ≤ 1) :

Uniqueness of factorisations #

theorem GameForm.LeftDeadEnd.LdeDvd.of_misereEQ {p x y : GameForm} (h : LdeDvd p x) (heq : x =m Form.DeadEnding.ShortDeadEnding y) :

LdeDvd p y

theorem GameForm.LeftDeadEnd.LdeDvd.of_misereEQ_left {p q x : GameForm} (hp : IsLde p) (heq : p =m Form.DeadEnding.ShortDeadEnding q) (h : LdeDvd q x) :

LdeDvd p x

theorem GameForm.LeftDeadEnd.IsLdePrime.of_misereEQ {p q : GameForm} (hp : IsLdePrime p) (hq : IsLde q) (heq : p =m Form.DeadEnding.ShortDeadEnding q) :

IsLdePrime q

theorem GameForm.LeftDeadEnd.misereEQ_of_isLdePrime_dvd_isLdeAtom {p a : GameForm} (hp : IsLdePrime p) (ha : IsLdeAtom a) (hdvd : LdeDvd p a) :

a =m Form.DeadEnding.ShortDeadEnding p

theorem GameForm.LeftDeadEnd.exists_mem_of_isLdePrime_dvd_sum {p : GameForm} (hp : IsLdePrime p) {s : Multiset GameForm} (hs : ∀ a ∈ s, IsLde a) (hdvd : LdeDvd p s.sum) :

∃ a ∈ s, LdeDvd p a

theorem GameForm.LeftDeadEnd.misereRel_symm {s t : Multiset GameForm} (h : Multiset.Rel (instForm =m GameForm Form.DeadEnding.ShortDeadEnding) s t) :

Multiset.Rel (instForm =m GameForm Form.DeadEnding.ShortDeadEnding) t s

instance GameForm.LeftDeadEnd.instIsTransMisereEQShortDeadEnding :

IsTrans GameForm (instForm =m GameForm Form.DeadEnding.ShortDeadEnding)

theorem GameForm.LeftDeadEnd.isGoodOption_of_add_isGoodOption {g h gr : GameForm} (hg : IsLde g) (hh : IsLde h) (hgr : gr ∈ Moves.moves Player.right g) (hgood : IsGoodOption (gr + h) (g + h)) :

IsGoodOption gr g

If $G + H$ is a sum of Left dead ends, and $G' + H$ is a good option of $G + H$, then $G'$ is a good option of $G$.

This is Davies (Lemma 7.7 on p. 35).

theorem GameForm.LeftDeadEnd.isGoodOption_add_nsmul_iff {g gr : GameForm} (hg : IsLde g) (hgr : gr ∈ Moves.moves Player.right g) (n : ℕ) :

IsGoodOption (gr + n • g) ((n + 1) • g) ↔ IsGoodOption gr g

If $G$ is a Left dead end, then, for every $n \in \mathbb{N}_1$, $G'$ is a good option of $G$ if and only if $G' + (n - 1) \cdot G$ is a good option of $n \cdot G$.

This is Davies (Lemma 7.13 on p. 38).

theorem GameForm.LeftDeadEnd.sum_misereEQ_sum_of_rel {s t : Multiset GameForm} (h : Multiset.Rel (instForm =m GameForm Form.DeadEnding.ShortDeadEnding) s t) :

(∀ a ∈ s, IsLde a) → (∀ a ∈ t, IsLde a) → s.sum =m Form.DeadEnding.ShortDeadEnding t.sum

theorem GameForm.LeftDeadEnd.exists_split_isFactorisation_of_primes {G : GameForm} (hG : IsLde G) {u : Multiset GameForm} (hu : ∀ p ∈ u, IsLdePrime p) {s : Multiset GameForm} (hs : IsFactorisation s (G + u.sum)) :

∃ (v : Multiset GameForm) (w : Multiset GameForm), s = v + w ∧ Multiset.Rel (instForm =m GameForm Form.DeadEnding.ShortDeadEnding) v u ∧ IsFactorisation w G

If $G = J + p_1 + \cdots + p_m$ with every $p_i$ prime, then every factorisation of $G$ splits as atoms matching the $p_i$ one-for-one together with a factorisation of $J$.

theorem GameForm.LeftDeadEnd.UniquelyFactorisable.of_misereEQ {g h : GameForm} (hgu : UniquelyFactorisable g) (heq : g =m Form.DeadEnding.ShortDeadEnding h) :

UniquelyFactorisable h

theorem GameForm.LeftDeadEnd.IsLdeAtom.uniquelyFactorisable {a : GameForm} (ha : IsLdeAtom a) :

UniquelyFactorisable a

theorem GameForm.LeftDeadEnd.isLdePrime_of_mem_isFactorisation_of_isPrimeFactorisable {x : GameForm} (hpf : IsPrimeFactorisable x) {w : Multiset GameForm} (hw : IsFactorisation w x) {a : GameForm} (ha : a ∈ w) :

IsLdePrime a

theorem GameForm.LeftDeadEnd.isLdePrime_of_isLdeAtom_dvd {a x : GameForm} (ha : IsLdeAtom a) (hpf : IsPrimeFactorisable x) (hdvd : LdeDvd a x) :

IsLdePrime a

theorem GameForm.LeftDeadEnd.isPrimeFactorisable_of_dvd {x y : GameForm} (hx : IsLde x) (hpf : IsPrimeFactorisable y) (hdvd : LdeDvd x y) :

IsPrimeFactorisable x

theorem GameForm.LeftDeadEnd.IsPrimeFactorisable.add {x y : GameForm} (hx : IsLde x) (hxp : IsPrimeFactorisable x) (hyp : IsPrimeFactorisable y) :

IsPrimeFactorisable (x + y)

theorem GameForm.LeftDeadEnd.IsPrimeFactorisable.nsmul {x : GameForm} (hx : IsLde x) (hxp : IsPrimeFactorisable x) (n : ℕ) :

IsPrimeFactorisable (n • x)

theorem GameForm.LeftDeadEnd.isFactorisation_erase_of_longestLen_eq {g h : GameForm} (hg : IsLde g) (hh : IsLde h) (hgood : IsGoodOption h g) (hlen : longestFactorisationLen g = longestFactorisationLen h + 1) {s : Multiset GameForm} (hs : IsFactorisation s g) (hcard : s.card = longestFactorisationLen g) :

∃ (a : GameForm) (t : Multiset GameForm), s = a ::ₘ t ∧ IsLdeAtom a ∧ race a = 1 ∧ IsFactorisation t h ∧ t.card = longestFactorisationLen h

Every longest factorisation of $G$ is of the form $H_1 + \cdots + H_k + K$, where $H_1 + \cdots + H_k$ is a longest factorisation of $H$.

This is Davies (Proposition 7.1(3) on p. 32).

theorem GameForm.LeftDeadEnd.exists_isLdeAtom_add_of_longestLen_eq {g h : GameForm} (hg : IsLde g) (hh : IsLde h) (hgood : IsGoodOption h g) (hlen : longestFactorisationLen g = longestFactorisationLen h + 1) :

∃ (k : GameForm), IsLdeAtom k ∧ race k = 1 ∧ g =m Form.DeadEnding.ShortDeadEnding h + k

There exists an atom $K$ such that $G = H + K$, and $K$ is terminable.

This is the existence half of Davies (Proposition 7.1(2) on p. 32).

theorem GameForm.LeftDeadEnd.isRacingOption_and_exists_unique_isLdeAtom_add {g h : GameForm} (hg : IsLde g) (hh : IsLde h) (hgood : IsGoodOption h g) (hlen : longestFactorisationLen g = longestFactorisationLen h + 1) :

IsRacingOption h g ∧ ∃ (k : GameForm), IsLdeAtom k ∧ race k = 1 ∧ g =m Form.DeadEnding.ShortDeadEnding h + k ∧ ∀ (k' : GameForm), IsLdeAtom k' → g =m Form.DeadEnding.ShortDeadEnding h + k' → k' =m Form.DeadEnding.ShortDeadEnding k

If $G$ is a Left dead end with a good option $H$ such that $\overline{\mathsf{L}(G)} = \overline{\mathsf{L}(H)} + 1$, then

$H$ is a racing option of $G$; and
there exists a unique atom $K$ such that $G = H + K$, and $K$ is terminable.

This is Davies (Proposition 7.1 on p. 32).

theorem GameForm.LeftDeadEnd.uniquelyFactorisable_of_good_atom {g h : GameForm} (hg : IsLde g) (hh : IsLdeAtom h) (hgo : IsGoodOption h g) :

UniquelyFactorisable g

If $G$ is a Left dead end with a good option to an atom $H$, then either $G$ is an atom, or $H$ is a racing option of $G$ and there exists a unique (terminable) atom $K$ such that $G = H + K$; in particular, $G$ is uniquely factorisable.

This is the "in particular" of Davies (Corollary 7.2 on p. 33).

theorem GameForm.LeftDeadEnd.isLdeAtom_or_isFactorisation_of_good_atoms {g h k : GameForm} (hg : IsLde g) (hh : IsLdeAtom h) (hk : IsLdeAtom k) (hgh : IsGoodOption h g) (hgk : IsGoodOption k g) (hne : ¬h =m Form.DeadEnding.ShortDeadEnding k) :

IsLdeAtom g ∨ IsFactorisation {h, k} g

If $G$ is a Left dead end with good options to distinct atoms $H$ and $K$, then either $G$ is an atom, or $H + K$ is the unique factorisation of $G$.

This is Davies (Corollary 7.3 on p. 33).

theorem GameForm.LeftDeadEnd.isLdeAtom_of_good_atoms_of_race_ne_two {g h k : GameForm} (hg : IsLde g) (hh : IsLdeAtom h) (hk : IsLdeAtom k) (hgh : IsGoodOption h g) (hgk : IsGoodOption k g) (hne : ¬h =m Form.DeadEnding.ShortDeadEnding k) (hrace : race g ≠ 2) :

If either of $H$ or $K$ is not terminable (i.e. if $r(G) \ne 2$), then $G$ is an atom.

This is the "in particular" of Davies (Corollary 7.3 on p. 33).

theorem GameForm.LeftDeadEnd.isLdeAtom_of_three_good_atoms {g a b c : GameForm} (hg : IsLde g) (ha : IsLdeAtom a) (hb : IsLdeAtom b) (hc : IsLdeAtom c) (hga : IsGoodOption a g) (hgb : IsGoodOption b g) (hgc : IsGoodOption c g) (hab : ¬a =m Form.DeadEnding.ShortDeadEnding b) (hbc : ¬b =m Form.DeadEnding.ShortDeadEnding c) (hac : ¬a =m Form.DeadEnding.ShortDeadEnding c) :

If $G$ is a Left dead end with at least three good options to pairwise distinct atoms, then $G$ is an atom.

This is Davies (Corollary 7.4 on p. 33).

theorem GameForm.LeftDeadEnd.factor_eq_of_good_pf {a : GameForm} {s' t : Multiset GameForm} (hs : IsFactorisation (a ::ₘ s') (a + s'.sum)) (ht : IsFactorisation t (a + s'.sum)) {ar : GameForm} (har : ar ∈ Moves.moves Player.right a) (hgood : IsGoodOption (ar + s'.sum) (a + s'.sum)) (hpf : IsPrimeFactorisable ar) :

∃ b ∈ t, a =m Form.DeadEnding.ShortDeadEnding b

If $G := G_1 + \cdots + G_n = H_1 + \cdots + H_m =: H$ are factorisations of a Left dead end $G$, and there is a good option of $G$ playing on the component $G_1$ to some prime-factorisable $G'_1$, then there exists an index $j$ such that $G_1 = H_j$.

This is Davies (Lemma 7.5 on p. 34).

inductive GameForm.LeftDeadEnd.IsGoodPfChain :

Multiset GameForm → Prop

Reading a factorisation as $G_1 + \cdots + G_k$: for every $1 \le i \le k$, there exists a good option of $G_i + \cdots + G_k$ on the component $G_i$ to some prime-factorisable $G'_i$.

This is the hypothesis of Davies (Theorem 7.6 on p. 35).

nil : IsGoodPfChain 0
cons {a : GameForm} {s : Multiset GameForm} {ar : GameForm} (har : ar ∈ Moves.moves Player.right a) (hgood : IsGoodOption (ar + s.sum) (a + s.sum)) (hpf : IsPrimeFactorisable ar) (hrest : IsGoodPfChain s) : IsGoodPfChain (a ::ₘ s)

Instances For

theorem GameForm.LeftDeadEnd.rel_of_isGoodPfChain {s : Multiset GameForm} (hchain : IsGoodPfChain s) :

(∀ a ∈ s, IsLdeAtom a) → ∀ (t : Multiset GameForm), IsFactorisation t s.sum → Multiset.Rel (instForm =m GameForm Form.DeadEnding.ShortDeadEnding) s t

theorem GameForm.LeftDeadEnd.uniquelyFactorisable_of_chain {g : GameForm} {s : Multiset GameForm} (hs : IsFactorisation s g) (hchain : IsGoodPfChain s) :

UniquelyFactorisable g

If $G := G_1 + \cdots + G_k$ is a factorisation of a Left dead end such that, for every $1 \le i \le k$, there exists a good option of $G_i + \cdots + G_k$ on the component $G_i$ to some prime-factorisable $G'_i$, then $G$ is uniquely factorisable.

This is Davies (Theorem 7.6 on p. 35).

theorem GameForm.LeftDeadEnd.exists_isGoodOption_isRacingOption {g : GameForm} (hg : IsLde g) (hg0 : g ≠ 0) :

∃ (gr : GameForm), IsGoodOption gr g ∧ IsRacingOption gr g

theorem GameForm.LeftDeadEnd.exists_isGoodOption_isStallingOption {g : GameForm} (hg : IsLde g) (hg0 : g ≠ 0) :

∃ (gr : GameForm), IsGoodOption gr g ∧ IsStallingOption gr g

theorem GameForm.LeftDeadEnd.uniquelyFactorisable_S_racing {S : GameForm → Prop} (hS : ∀ (a : GameForm), S a → IsLdeAtom a) (hpf : ∀ (a : GameForm), S a → ∀ (ar : GameForm), IsGoodOption ar a → IsRacingOption ar a → IsPrimeFactorisable ar) {s : Multiset GameForm} (hs : ∀ a ∈ s, S a) :

UniquelyFactorisable s.sum

If $S \subseteq \mathcal{L}$ is a set of atoms such that every good racing option of every $G \in S$ is prime-factorisable, then every $S$-factorisation is uniquely factorisable.

This is Davies (Theorem 7.8 on p. 36).

theorem GameForm.LeftDeadEnd.uniquelyFactorisable_S_stalling {S : GameForm → Prop} (hS : ∀ (a : GameForm), S a → IsLdeAtom a) (hpf : ∀ (a : GameForm), S a → ∀ (ar : GameForm), IsGoodOption ar a → IsStallingOption ar a → IsPrimeFactorisable ar) {s : Multiset GameForm} (hs : ∀ a ∈ s, S a) :

UniquelyFactorisable s.sum

If $S \subseteq \mathcal{L}$ is a set of atoms such that every good stalling option of every $G \in S$ is prime-factorisable, then every $S$-factorisation is uniquely factorisable.

This is Davies (Theorem 7.9 on p. 36).