Dead Ends in Misère Play: the Misère Monoid of Canonical Numbers

This module records the formalisation of [Rebecca Milley, Gabriel Renault. Dead Ends in Misère Play: The Misère Monoid of Canonical Numbers] [MR13].

2. Preliminary results

def DeadEndsInMiserePlay.definition_1_deadEnd {G : Type (u + 1)} [Form G] (p : Player) (g : G) : Prop

Equations

• @DeadEndsInMiserePlay.definition_1_deadEnd = @Form.IsDeadEnd

def DeadEndsInMiserePlay.definition_1_deadEnding {G : Type (u + 1)} [Form G] (g : G) : Prop

Equations

• @DeadEndsInMiserePlay.definition_1_deadEnding = @Form.IsDeadEnding

theorem DeadEndsInMiserePlay.lemma_1 {G : Type (u + 1)} [Form G] {g h : G} {p : Player} (h1 : Form.IsDeadEnding g) (h2 : h ∈ Moves.moves p g) : Form.IsDeadEnding h

theorem DeadEndsInMiserePlay.lemma_2 {G : Type (u + 1)} [Form G] {g h : G} (h1 : Form.IsDeadEnding g) (h2 : Form.IsDeadEnding h) : Form.IsDeadEnding (g + h)

theorem DeadEndsInMiserePlay.lemma_3_left (g : GameForm) (h1 : g ≠ 0) (h2 : Form.IsDeadEnd Player.left g) : Form.Misere.Outcome.MisereOutcome g = Outcome.L

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

theorem DeadEndsInMiserePlay.lemma_3_right (g : GameForm) (h1 : g ≠ 0) (h2 : Form.IsDeadEnd Player.right g) : Form.Misere.Outcome.MisereOutcome g = Outcome.R

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

noncomputable def DeadEndsInMiserePlay.definition_2_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

• DeadEndsInMiserePlay.definition_2_race = GameForm.LeftDeadEnd.race

3. Integers and other dead ends

theorem DeadEndsInMiserePlay.lemma_5 (a b : GameForm) : GameForm.LeftDeadEnd.IsLde a → GameForm.LeftDeadEnd.IsLde b → (GameForm.LeftDeadEnd.race a ≤ GameForm.LeftDeadEnd.race b → Form.Misere.Outcome.WinsGoingFirst Player.left (-a + b)) ∧ (GameForm.LeftDeadEnd.race a < GameForm.LeftDeadEnd.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).

theorem DeadEndsInMiserePlay.theorem_6 {k : GameForm} (hk : GameForm.LeftDeadEnd.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).

theorem DeadEndsInMiserePlay.corollary_7 {A : GameForm → Prop} [self : IntegerInvertible A] (n : ℤ) : (↑n + -↑n) =m A 0

theorem DeadEndsInMiserePlay.corollary_7_inst : IntegerInvertible Form.DeadEnding.ShortDeadEnding

TODO: Theorem 8

TODO: Theorem 9

TODO: Lemma 10

TODO: Theorem 11

4. Numbers

TODO: Proposition 12

TODO: Lemma 13

TODO: Lemma 14

TODO: Corollary 15

TODO: Theorem 16

TODO: Lemma 17

TODO: Theorem 18

TODO: Theorem 19

TODO: Corollary 20

TODO: Lemma 21

TODO: Lemma 22

TODO: Theorem 23

TODO: Corollary 24

TODO: Theorem 25

5. Zeros in the dead-ending universe

TODO: Lemma 26

TODO: Theorem 27