Documentation

LeanPool.MisereGames.Misere.TippingPoints

Misere combinatorial games.

noncomputable def MisereGames.NTippingPoint {g : GameForm} (h1 : Form.IsShort g) :

The least absolute integer shift at which a short game has outcome N.

Equations
Instances For

    The defining property of the $\mathscr{N}$-tipping point: at $\operatorname{n}(G)$ itself, either the positive or the negative shift has outcome $\mathscr{N}$.

    Minimality of the $\mathscr{N}$-tipping point: below $\operatorname{n}(G)$, neither the positive nor the negative shift has outcome $\mathscr{N}$.

    @[simp]

    $\operatorname{n}(-G) = \operatorname{n}(G)$

    noncomputable def MisereGames.RTippingPoint {g : GameForm} (h1 : Form.IsShort g) :

    The least nonnegative shift at which a short game has outcome R.

    Equations
    Instances For
      noncomputable def MisereGames.LTippingPoint {g : GameForm} (h1 : Form.IsShort g) :

      The least nonnegative negative shift at which a short game has outcome L.

      Equations
      Instances For

        Negation sends the $\mathscr{R}$-tipping point to the $\mathscr{L}$-tipping point: $\operatorname{r}(-G) = \operatorname{l}(G)$.

        Negation sends the $\mathscr{L}$-tipping point to the $\mathscr{R}$-tipping point: $\operatorname{l}(-G) = \operatorname{r}(G)$.

        The $\mathscr{R}$-tipping point is a witness: $\operatorname{o}(G + \operatorname{r}(G)) = \mathscr{R}$.

        The $\mathscr{L}$-tipping point is a witness: $\operatorname{o}(G - \operatorname{l}(G)) = \mathscr{L}$.

        Minimality of the $\mathscr{R}$-tipping point: below $\operatorname{r}(G)$, the positive shift is not $\mathscr{R}$.

        For a Left-win game, $1 \le \operatorname{n}(G)$.

        For a next-win game, $\operatorname{n}(G) = 0$.