Misere combinatorial games.
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 Misere Play][davies:SumsPFreeForms:2025].
2. Preliminaries #
If A is downlinking and hereditary, comparison modulo A is characterised by
the maintenance–proviso test.
Literature alias for Definition 2.2: P-free forms.
Equations
Instances For
Literature alias for Definition 2.2: the set pf(A).
Equations
Instances For
TODO: Definition 2.3
3. Tipping point basics #
Literature alias for Definition 3.1: N tipping points.
Equations
Instances For
Literature alias for Definition 3.1: R tipping points.
Equations
Instances For
Literature alias for Definition 3.1: L tipping points.
Equations
Instances For
Theorem 3.2 is implied by definition of tipping points in Lean.
If $G$ is $\mathscr{P}$-free and $n$ is an integer then $G + n$ is also $\mathscr{P}$-free.
This is [Davies, Miller, Milley (Lemma 3.3 on p. 9)][davies:SumsPFreeForms:2025].
Literature alias for Definition 3.4: outcome stability.
Equations
Instances For
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}$.
This is [Davies, Miller, Milley (Lemma 3.7 on p. 13)][davies:SumsPFreeForms:2025].
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)][davies:SumsPFreeForms:2025].
If $G$ is a $\mathscr{P}$-free Left end with $\operatorname{o}(G) = \mathscr{N}$, then $\operatorname{r}(G) = 1$.
This is [Davies, Miller, Milley (Lemma 3.8 on p. 13)][davies:SumsPFreeForms:2025].
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)$.
This is [Davies, Miller, Milley (Lemma 3.9 on p. 13)][davies:SumsPFreeForms:2025].
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)][davies:SumsPFreeForms:2025].
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$.
This is [Davies, Miller, Milley (Lemma 3.10 on p. 13)][davies:SumsPFreeForms:2025].
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)][davies:SumsPFreeForms:2025].
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)][davies:SumsPFreeForms:2025].
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)][davies:SumsPFreeForms:2025].
TODO: Theorem 3.11 (2) and (3)
Literature alias for Definition 3.12: integer invertibility.
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)][davies:SumsPFreeForms:2025].
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)][davies:SumsPFreeForms:2025].
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)][davies:SumsPFreeForms:2025].
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)][davies:SumsPFreeForms:2025].
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}$.
This is [Davies, Miller, Milley (Lemma 3.14 on p. 16)][davies:SumsPFreeForms:2025].
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)][davies:SumsPFreeForms:2025].
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)][davies:SumsPFreeForms:2025].
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)][davies:SumsPFreeForms:2025].
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)][davies:SumsPFreeForms:2025].
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)][davies:SumsPFreeForms:2025].
TODO: Theorem 3.15 (3) and (4)
Literature alias for Definition 3.16: Property X.
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.
This is [Davies, Miller, Milley (Lemma 3.17 on p. 18)][davies:SumsPFreeForms:2025].
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}$.
This is [Davies, Miller, Milley (Lemma 3.18 on p. 22)][davies:SumsPFreeForms:2025].
If $\mathcal{A}$ is an outcome-stable, hereditary, and integer-invertible monoid with Property X, then $\operatorname{pf}(\mathcal{A})$ is a monoid.
This is [Davies, Miller, Milley (Lemma 3.19 on p. 23)][davies:SumsPFreeForms:2025].
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$.
This is [Davies, Miller, Milley (Corollary 3.21 on p. 23)][davies:SumsPFreeForms:2025].
4. Blocking games: an application #
If G, H ∈ pf(B) with o(G) = L and H a Left end, then o(G + H) = L.
This is [Davies, Miller, Milley (Lemma 4.1 on p. 24)][davies:SumsPFreeForms:2025]
This is the mirror of [Davies, Miller, Milley (Lemma 4.1 on p. 24)][davies:SumsPFreeForms:2025].
This is [Davies, Miller, Milley (Lemma 4.2 on p. 25)][davies:SumsPFreeForms:2025].
TODO: Theorem 4.3
TODO: Lemma 4.4
This is [Davies, Miller, Milley (Lemma 4.5 on p. 26)][davies:SumsPFreeForms:2025]
TODO: Proposition 4.6
This is [Davies, Miller, Milley (Lemma 4.7 on p. 26)][davies:SumsPFreeForms:2025].
This is [Davies, Miller, Milley (Lemma 4.8 on p. 26)][davies:SumsPFreeForms:2025].
This is [Davies, Miller, Milley (Lemma 4.9 on p. 27)][davies:SumsPFreeForms:2025].
TODO: Lemma 4.10
TODO: Proposition 4.11
TODO: Theorem 4.12
TODO: Proposition 4.13
TODO: Proposition 4.14
TODO: Corollary 4.15