On Sums of P-Free Forms Under Misère Play #
This module records the formalisation of Alfie Davies, Sarah Miller, Rebecca Milley. On Sums of P-Free Forms Under Misère Play.
2. Preliminaries #
If A is downlinking and hereditary, comparison modulo A is characterised by
the maintenance–proviso test.
Equations
Instances For
Equations
Instances For
TODO: Definition 2.3
3. Tipping point basics #
Equations
Instances For
Equations
Instances For
Equations
Instances For
Theorem 3.2 is implied by definition of tipping points in Lean.
Open problem 3.5
TODO: Theorem 3.6
If $\mathcal{A}$ is outcome-stable, hereditary monoid containing $1$ and $-1$, and $G \in \operatorname{pf}(\mathcal{A})$, then $\operatorname{n}(G^L) \le \operatorname{r}(G)$ for all Left options $G^L$ of $G$ with $\operatorname{o}(G^L) \ne \mathscr{R}$.
If $\mathcal{A}$ is outcome-stable, hereditary monoid containing $1$ and $-1$, and $G \in \operatorname{pf}(\mathcal{A})$, then $\operatorname{n}(G^R) \le \operatorname{l}(G)$ for all Right options $G^R$ of $G$ with $\operatorname{o}(G^R) \ne \mathscr{L}$.
This is the mirror of Davies, Miller, Milley (Lemma 3.7 on p. 13).
If $G$ is a $\mathscr{P}$-free Left end with $\operatorname{o}(G) = \mathscr{N}$, then $\operatorname{r}(G) = 1$.
If $\mathcal{A}$ is outcome-stable, hereditary monoid containing $1$ and $-1$, and $G \in \operatorname{pf}(\mathcal{A})$ with $\operatorname{o}(G) = \mathscr{N}$, then either $G$ is Left end-like with $\operatorname{r}(G) = 1$, or else there exists a Left option $G^L$ of $G$ with $\operatorname{o}(G^L) = \mathscr{L}$ such that $\operatorname{n}(G^L) = r(G)$.
If $\mathcal{A}$ is outcome-stable, hereditary monoid containing $1$ and $-1$, and $G \in \operatorname{pf}(\mathcal{A})$ with $\operatorname{o}(G) = \mathscr{N}$, then either $G$ is Right end-like with $\operatorname{l}(G) = 1$, or else there exists a Left option $G^R$ of $G$ with $\operatorname{o}(G^R) = \mathscr{R}$ such that $\operatorname{n}(G^R) = l(G)$.
This is mirror of Davies, Miller, Milley (Lemma 3.9 on p. 13).
If $\mathcal{A}$ is outcome-stable, hereditary monoid containing $1$ and $-1$, and $G \in \operatorname{pf}(\mathcal{A})$ is a Left end then $\operatorname{r}(G) = \operatorname{n}(G) + 1$.
If $\mathcal{A}$ is outcome-stable, hereditary monoid containing $1$ and $-1$, and $G \in \operatorname{pf}(\mathcal{A})$ is a Right end then $\operatorname{l}(G) = \operatorname{n}(G) + 1$.
This is the mirror of Davies, Miller, Milley (Lemma 3.10 on p. 13).
If $\mathcal{A}$ is outcome-stable, hereditary monoid containing $1$ and $-1$, and $G \in \operatorname{pf}(\mathcal{A})$ with $\operatorname{o}(G) = \mathscr{L}$, then if $\operatorname{n}(G) \ne \operatorname{r}(G) - 1$ then there exists some option $G^L$ with $\operatorname{o}(G^L) = \mathscr{L}$ such that $\operatorname{n}(G^L) = \operatorname{r}(G)$.
This is (1) in Davies, Miller, Milley (Lemma 3.11 on p. 14).
If $\mathcal{A}$ is outcome-stable, hereditary monoid containing $1$ and $-1$, and $G \in \operatorname{pf}(\mathcal{A})$ with $\operatorname{o}(G) = \mathscr{R}$, then if $\operatorname{n}(G) \ne \operatorname{l}(G) - 1$ then there exists some option $G^R$ with $\operatorname{o}(G^R) = \mathscr{R}$ such that $\operatorname{n}(G^R) = \operatorname{l}(G)$.
This is mirror of (1) in Davies, Miller, Milley (Lemma 3.11 on p. 14).
TODO: Theorem 3.11 (2) and (3)
A set of games $\mathcal{A}$ is integer-invertible if it contains every integer $n$ and $n + \overline{n} =_{\mathcal{A}} 0$.
This is Davies, Miller, Milley (Definition 3.12 on p. 15).
Equations
Instances For
If $\mathcal{A}$ is an outcome-stable and integer-invertible monoid, and $G, H \in \operatorname{pf}(\mathcal{A})$ with $\operatorname{o}(G) = \mathscr{L}$ then if $\operatorname{n}(G) > \operatorname{l}(H)$ then $\operatorname{o}(G + H) = \mathscr{L}$.
This is (1) in Davies, Miller, Milley (Lemma 3.13 on p. 16).
If $\mathcal{A}$ is an outcome-stable and integer-invertible monoid, and $G, H \in \operatorname{pf}(\mathcal{A})$ with $\operatorname{o}(G) = \mathscr{R}$ then if $\operatorname{r}(H) < \operatorname{n}(G)$ then $\operatorname{o}(G + H) = \mathscr{R}$.
This is mirror of (1) in Davies, Miller, Milley (Lemma 3.13 on p. 16).
If $\mathcal{A}$ is an outcome-stable and integer-invertible monoid, and $G, H \in \operatorname{pf}(\mathcal{A})$ with $\operatorname{o}(G) = \mathscr{L}$ and $\operatorname{o}(H) = \mathscr{N}$, then if $\operatorname{r}(G) < \operatorname{l}(H)$ then $\operatorname{o}(G + H) = \mathscr{N}$.
This is (2) in Davies, Miller, Milley (Lemma 3.13 on p. 16).
If $\mathcal{A}$ is an outcome-stable and integer-invertible monoid, and $G, H \in \operatorname{pf}(\mathcal{A})$ with $\operatorname{o}(G) = \mathscr{R}$ and $\operatorname{o}(H) = \mathscr{N}$, then if $\operatorname{l}(G) < \operatorname{r}(H)$ then $\operatorname{o}(G + H) = \mathscr{N}$.
This is mirror of (2) in Davies, Miller, Milley (Lemma 3.13 on p. 16).
If $\mathcal{A}$ is an outcome-stable and integer-invertible monoid, and $G, H \in \operatorname{pf}(\mathcal{A})$ with $\operatorname{o}(G) = \operatorname{o}(H) = \mathscr{N}$ then if $\operatorname{r}(G) > \operatorname{l}(H)$ or $\operatorname{l}(G) < \operatorname{r}(H)$ then $\operatorname{o}(G + H) \ge \mathscr{N}$.
If $\mathcal{A}$ is an outcome-stable and integer-invertible monoid, and $G, H \in \operatorname{pf}(\mathcal{A})$ with $\operatorname{o}(G) = \operatorname{o}(H) = \mathscr{N}$ then if $\operatorname{r}(G) < \operatorname{l}(H)$ or $\operatorname{l}(G) > \operatorname{r}(H)$ then $\operatorname{o}(G + H) \le \mathscr{N}$.
This is mirror of Davies, Miller, Milley (Lemma 3.14 on p. 16).
If $\mathcal{A}$ is an outcome-stable and integer-invertible monoid, and $G, H \in \operatorname{pf}(\mathcal{A})$ with $\operatorname{o}(G) = \mathscr{L}$ and $\operatorname{l}(H) < \operatorname{n}(G)$, then $\operatorname{o}(G + H) = \mathscr{L}$.
This is (1) in Davies, Miller, Milley (Lemma 3.15 on p. 17).
If $\mathcal{A}$ is an outcome-stable and integer-invertible monoid, and $G, H \in \operatorname{pf}(\mathcal{A})$ with $\operatorname{o}(G) = \mathscr{R}$ and $\operatorname{r}(H) < \operatorname{n}(G)$, then $\operatorname{o}(G + H) = \mathscr{R}$.
This is mirror of (1) in Davies, Miller, Milley (Lemma 3.15 on p. 17).
If $\mathcal{A}$ is an outcome-stable and integer-invertible monoid, and $G, H \in \operatorname{pf}(\mathcal{A})$ with $\operatorname{o}(G) = \mathscr{L}$, $\operatorname{o}(H) = \mathscr{R}$ and $\operatorname{n}(G) > \operatorname{n}(H)$ or $\operatorname{r}(G) > \operatorname{l}(H)$, then $\operatorname{o}(G + H) \ge \mathscr{N}$.
This is (2) in Davies, Miller, Milley (Lemma 3.15 on p. 17).
If $\mathcal{A}$ is an outcome-stable and integer-invertible monoid, and $G, H \in \operatorname{pf}(\mathcal{A})$ with $\operatorname{o}(G) = \mathscr{R}$, $\operatorname{o}(H) = \mathscr{L}$ and $\operatorname{n}(G) < \operatorname{n}(H)$ or $\operatorname{r}(H) < \operatorname{l}(G)$, then $\operatorname{o}(G + H) \le \mathscr{N}$.
This is mirror of (2) in Davies, Miller, Milley (Lemma 3.15 on p. 17).
TODO: Theorem 3.15 (3) and (4)
A set of games $\mathcal{A}$ has Property X if, for all $G, H \in \operatorname{pf}(\mathcal{A})$ with $\operatorname{o}(G) = \operatorname{o}(H) = \mathscr{N}$
- if $\operatorname{r}(G) = \operatorname{l}(H) = 1$, where $G$ is a Left end but $H$ is not, then $\operatorname{o}(G + H) = N$; and
- if $\operatorname{l}(G) = \operatorname{r}(H) = 1$, where $H$ is a Right end but $G$ is not, then $\operatorname{o}(G + H) = N$.
This is Davies, Miller, Milley (Definition 3.16 on p. 18).
Equations
Instances For
If $\mathcal{A}$ is an outcome-stable, hereditary, and integer-invertible
monoid that has Property X, and $G, H \in \operatorname{pf}(\mathcal{A})$, then
Lemma317Claim holds.
If $\mathcal{A}$ is an outcome-stable, hereditary, and integer-invertible monoid with Property X, and $G, H \in \operatorname{pf}(\mathcal{A})$, then $\operatorname{o}(G + H) \ne \mathscr{P}$.
If $\mathcal{A}$ is an outcome-stable, hereditary, and integer-invertible monoid with Property X, then $\operatorname{pf}(\mathcal{A})$ is a monoid.
TODO: Corollary 3.20
If $\mathcal{A}$ is a subsemigroup of an outcome-stable, hereditary, and integer-invertible monoid that has Property X, then either $\operatorname{pf}(\mathcal{A})$ is a semigroup or else $\operatorname{pf}(\mathcal{A}) = \emptyset$.
4. Blocking games: an application #
If G, H ∈ pf(B) with o(G) = L and H a Left end, then o(G + H) = L.
If G, H ∈ pf(B) with o(G) = L and H a Left end, then o(G + H) = L.
This is one direction of Davies, Milley (Theorem 3.1 on p. 7)
TODO: Proposition 4.6
TODO: Proposition 4.11
TODO: Theorem 4.12
TODO: Proposition 4.13
TODO: Proposition 4.14
TODO: Corollary 4.15