Misere combinatorial games.
Separation and downlinking #
This file defines downlinked and separated pairs of forms, and develops the
machinery necessary to prove that $G\ge_\mathcal{U}H$ implies that both
Form.Maintenance and Form.Proviso are satisfied.
Here, $G$ and $H$ will always refer to arbitrary forms (possibly augmented,
possibly not), $\mathcal{A}$ to an arbitrary set of forms, and $\mathcal{U}$ to
a universe (which may or may not be Short).
References #
- [A. N. Siegel, On the general dead-ending universe of partizan games (Section 5 on pp. 207–222)][siegel:GeneralDeadendingUniverse:2025]
We say $G$ is downlinked to $H$ (with respect to $\mathcal{A}$) if there exists some $T\in\mathcal{A}$ with $\operatorname{o_L}(G+T)=\mathscr{R}$ and $\operatorname{o_R}(H+T)=\mathscr{L}$.
This generalises the definition given by [Siegel (Definition 5.9 on p. 214)][siegel:GeneralDeadendingUniverse:2025], where all forms were short, and the sets were short universes.
Equations
- One or more equations did not get rendered due to their size.
Instances For
If there exists some $X\in\mathcal{A}$ whereby
$\operatorname{o_L}(G+X)=\mathscr{R}$ and
$\operatorname{o_L}(H+X)=\mathscr{L}$, then we say that $G$ and $H$ are Left
separated (with respect to $\mathcal{A}$). (See LeftSeparating and
RightSeparating.)
Equations
- One or more equations did not get rendered due to their size.
Instances For
There exists some $X\in\mathcal{A}$ whereby
$\operatorname{o_L}(G+X)=\mathscr{R}$ and
$\operatorname{o_L}(H+X)=\mathscr{L}$. (See Separating.)
Equations
Instances For
There exists some $X\in\mathcal{A}$ whereby
$\operatorname{o_R}(G+X)=\mathscr{R}$ and
$\operatorname{o_R}(H+X)=\mathscr{L}$. (See Separating.)
Equations
Instances For
We have g ≥ h modulo A exactly when g and h are neither Left- nor
Right-separating.
Negation of misereGE_iff_not_separating.
Given $H$ and a root $r$, this constructs the set of games
$\{r,\operatorname{adj}_r(H^\mathcal{R})\}$, which will act as Left's set of
options in the construction of rightSeparatorCandidate. Taking $r=0$ recovers
the set $\{0,(H^\mathcal{R})^\circ\}$.
Equations
- MisereGames.Form.Separation.rightSeparatorLeftSet r h = {r} ∪ Set.range fun (hr : ↑(MisereGames.Moves.moves MisereGames.Player.right h)) => MisereGames.Form.rootedAdjoint r ↑hr
Instances For
$\def\form<#1>[#2]{\left\{#1 \mid #2\right\}}$
Given forms $H$ and $X$ and a root $r$, this constructs the form
$\form<r,\operatorname{adj}_r(H^\mathcal{R})>[X]$, which is used by
Separating.pair_of_not_misereGE to show that $G$ and $H$ must be both
LeftSeparating and RightSeparating whenever $G\ngeq_\mathcal{U}H$.
Equations
Instances For
Given $G$ and a root $r$, this constructs the set of games
$\{r,\operatorname{adj}_r(G^\mathcal{L})\}$, the Left/Right mirror of
rightSeparatorLeftSet, which will act as Right's set of options in the
construction of leftSeparatorCandidate.
Equations
- MisereGames.Form.Separation.leftSeparatorRightSet r g = {r} ∪ Set.range fun (gl : ↑(MisereGames.Moves.moves MisereGames.Player.left g)) => MisereGames.Form.rootedAdjoint r ↑gl
Instances For
$\def\form<#1>[#2]{\left\{#1 \mid #2\right\}}$
Given forms $G$ and $X$ and a root $r$, this constructs the form
$\form<X>[r,\operatorname{adj}_r(G^\mathcal{L})]$, the Left/Right mirror of
rightSeparatorCandidate.
Equations
Instances For
The Left separator is the conjugate of a Right separator, with the root conjugated.
$\def\form<#1>[#2]{\left\{#1 \mid #2\right\}}$
If $G$ and $H$ are LeftSeparating, and
$\form<r,\operatorname{adj}_r(H^\mathcal{R})>[X]\in\mathcal{A}$ for every
$X\in\mathcal{A}$, then $G$ and $H$ are RightSeparating.
$\def\form<#1>[#2]{\left\{#1 \mid #2\right\}}$
If $G$ and $H$ are RightSeparating, and
$\form<X>[r,\operatorname{adj}_r(G^\mathcal{L})]\in\mathcal{A}$ for every
$X\in\mathcal{A}$, then $G$ and $H$ are LeftSeparating. The Left/Right mirror
of rightSeparating_of_leftSeparating_of_rightSeparatorCandidate_mem.
The optional root contribution to a downlink witness.
Equations
- MisereGames.Form.Separation.downlinkZero r p g h = if MisereGames.Form.IsEnd (-p) g ∧ MisereGames.Form.IsEnd (-p) h then {r} else ∅
Instances For
The Left option set of a downlink witness.
Equations
Instances For
The Right option set of a downlink witness.
Equations
Instances For
$\def\form<#1>[#2]{\left\{#1 \mid #2\right\}}$ This constructs the following game form, which is similar to a construction by [Siegel (Proof of Lemma 5.10 on p. 215)][siegel:GeneralDeadendingUniverse:2025] for short forms: $$ T= \begin{cases} \form<r>[r] & \text{if neither }G\text{ nor }H\text{ has any ordinary options},\\ \form<r>[X_i,\operatorname{adj}_r(H^\mathcal{L})] & \text{if }G,H\text{ are both Right ends but not both Left ends},\\ \form<Y_j,\operatorname{adj}_r(G^\mathcal{R})>[r] & \text{if }G,H\text{ are both Left ends but not both Right ends},\\ \form<Y_j,\operatorname{adj}_r(G^\mathcal{R})>[X_i,\operatorname{adj}_r(H^\mathcal{L})] & \text{otherwise}. \end{cases} $$ Here $r$ is the root; taking $r=0$ recovers Siegel's construction.
(Note that the $X_i$ and $Y_j$ are chosen as a function of the Left and Right options of $G$ and $H$ respectively.)
Equations
- MisereGames.Form.Separation.downlinkWitness r g h x y = !{MisereGames.Form.Separation.downlinkLeftSet r g h y | MisereGames.Form.Separation.downlinkRightSet r g h x}
Instances For
If $G$ and $H$ are RightSeparating, then $\overline{H}$ and $\overline{G}$
must be LeftSeparating.
If $\overline{H}$ and $\overline{G}$ are RightSeparating, then $G$ and $H$
must be LeftSeparating.