Documentation

LeanPool.MisereGames.Misere.OutcomeStable

Misere combinatorial games.

class MisereGames.OutcomeStable {G : Type (u + 1)} [Form G] (A : GProp) :

This is [Davies, Miller, Milley (Definition 3.4 on p. 9)][davies:SumsPFreeForms:2025].

Instances
    @[simp]

    If $\mathcal{A}$ is outcome-stable, $n \in \mathbb{N}$ then $0 \ge_{\operatorname{pf}(\mathcal{A})} 1$.

    If $\mathcal{A}$ is outcome-stable, $n \in \mathbb{N}$ then $n \ge_{\operatorname{pf}(\mathcal{A})} 1 + n$.

    If $\mathcal{A}$ is outcome-stable, $n, m \in \mathbb{N}$, and $n \le m$ then $n \ge_{\operatorname{pf}(\mathcal{A})} m$.

    If $\mathcal{A}$ is outcome-stable, $n \in \mathbb{Z}$ then $n \ge_{\operatorname{pf}(\mathcal{A})} 1 + n$.

    If $\mathcal{A}$ is outcome-stable, $n \in \mathbb{N}$, $k \in \mathbb{Z}$ then $k \ge_{\operatorname{pf}(\mathcal{A})} n + k$.

    If $\mathcal{A}$ is outcome-stable, $n, m \in \mathbb{Z}$, and $n \le m$ then $n \ge_{\operatorname{pf}(\mathcal{A})} m$.

    If $\mathcal{A}$ is outcome-stable and $G \in \operatorname{pf}(\mathcal{A})$ then $\operatorname{o}(G + 1) \le \operatorname{o}(G)$.

    If $\mathcal{A}$ is outcome-stable and $G \in \operatorname{pf}(\mathcal{A})$ then $\operatorname{o}(G) \le \operatorname{o}(G - 1)$.

    If $\mathcal{A}$ is outcome-stable, $G \in \operatorname{pf}(\mathcal{A})$, and $n \in \mathbb{N}$ then $\operatorname{o}(G + n) \le \operatorname{o}(G)$.

    If $\mathcal{A}$ is outcome-stable, $G \in \operatorname{pf}(\mathcal{A})$, and $k, m \in \mathbb{Z}$ and $k \le m$ then $\operatorname{o}(G + m) \le \operatorname{o}(G + k)$.

    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].

    The $\mathscr{L}$-region is downward closed: if $\operatorname{o}(G + m) = \mathscr{L}$ and $k \le m$, then $\operatorname{o}(G + k) = \mathscr{L}$.

    The $\mathscr{R}$-region is upward closed: if $\operatorname{o}(G + k) = \mathscr{R}$ and $k \le m$, then $\operatorname{o}(G + m) = \mathscr{R}$.

    The outcome of an integer shift is always one of $\mathscr{L}$, $\mathscr{N}$, $\mathscr{R}$ (never $\mathscr{P}$).

    The $\mathscr{N}$-tipping point of a Left-win game lies strictly above $0$, and its witness is the positive shift: $\operatorname{o}(G + \operatorname{n}(G)) = \mathscr{N}$.

    Positive $\mathscr{N}$-region for a next-win game: if $\operatorname{o}(G) = \mathscr{N}$ and $k < \operatorname{r}(G)$, then $\operatorname{o}(G + k) = \mathscr{N}$.

    Negative $\mathscr{N}$-region for a next-win game: if $\operatorname{o}(G) = \mathscr{N}$ and $k < \operatorname{l}(G)$, then $\operatorname{o}(G - k) = \mathscr{N}$.

    For a Left-win game, the $\mathscr{N}$-tipping point lies strictly below the $\mathscr{R}$-tipping point.

    Shifting by a natural translates the $\mathscr{R}$-tipping point: $\operatorname{r}(G + k) = \operatorname{r}(G) - k$.

    For a Left-win game, shifting by a natural $k \le \operatorname{n}(G)$ translates the $\mathscr{N}$-tipping point: $\operatorname{n}(G + k) = \operatorname{n}(G) - k$.

    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, integer-invertible monoid, and $G \in \operatorname{pf}(\mathcal{A})$ with $\operatorname{o}(G) = \mathscr{L}$ and $G^R$ is a Right option of $G$, then $\operatorname{r}(G^R) \ge \operatorname{n}(G)$.

    If $\mathcal{A}$ is outcome-stable, hereditary, integer-invertible monoid, and $G \in \operatorname{pf}(\mathcal{A})$ with $\operatorname{o}(G) = \mathscr{L}$ and $G^L$ is a Left option of $G$, then $\operatorname{l}(G^L) \ge \operatorname{n}(G)$.

    If $\mathcal{A}$ is outcome-stable, hereditary, integer-invertible monoid, and $G \in \operatorname{pf}(\mathcal{A})$ with $\operatorname{o}(G) = \mathscr{L}$ then there exists a Right option $G^R$ of $G$ with $\operatorname{r}(G^R) = \operatorname{n}(G)$.

    If $\mathcal{A}$ is outcome-stable, hereditary, integer-invertible monoid, and $G \in \operatorname{pf}(\mathcal{A})$ with $\operatorname{o}(G) = \mathscr{R}$ then there exists a Left option $G^L$ of $G$ with $\operatorname{l}(G^L) = \operatorname{n}(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{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].