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 #
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), where all forms were short, and the sets were short universes.
Equations
- Form.Downlinked A g h = ∃ (t : G), A t ∧ ¬Form.Misere.Outcome.WinsGoingFirst Player.left (g + t) ∧ ¬Form.Misere.Outcome.WinsGoingFirst Player.right (h + t)
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 AreLeftSeparating and
AreRightSeparating.)
Equations
- Form.AreSeparating A Player.left g h = ∃ (x : G), A x ∧ ¬Form.Misere.Outcome.WinsGoingFirst Player.left (g + x) ∧ Form.Misere.Outcome.WinsGoingFirst Player.left (h + x)
- Form.AreSeparating A Player.right g h = ∃ (x : G), A x ∧ Form.Misere.Outcome.WinsGoingFirst Player.right (g + x) ∧ ¬Form.Misere.Outcome.WinsGoingFirst Player.right (h + x)
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 AreSeparating.)
Equations
- Form.AreLeftSeparating A g h = Form.AreSeparating A Player.left g h
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 AreSeparating.)
Equations
- Form.AreRightSeparating A g h = Form.AreSeparating A Player.right g h
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
- Form.Separation.rightSeparatorLeftSet r h = {r} ∪ Set.range fun (hr : ↑(Moves.moves Player.right h)) => 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.separating_pair_of_not_misereGE to show that $G$ and $H$ must be both
AreLeftSeparating and AreRightSeparating 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
- Form.Separation.leftSeparatorRightSet r g = {r} ∪ Set.range fun (gl : ↑(Moves.moves Player.left g)) => 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 AreLeftSeparating, and
$\form<r,\operatorname{adj}_r(H^\mathcal{R})>[X]\in\mathcal{A}$ for every
$X\in\mathcal{A}$, then $G$ and $H$ are AreRightSeparating.
$\def\form<#1>[#2]{\left\{#1 \mid #2\right\}}$
If $G$ and $H$ are AreRightSeparating, and
$\form<X>[r,\operatorname{adj}_r(G^\mathcal{L})]\in\mathcal{A}$ for every
$X\in\mathcal{A}$, then $G$ and $H$ are AreLeftSeparating. The Left/Right mirror
of rightSeparating_of_leftSeparating_of_rightSeparatorCandidate_mem.
Equations
- Form.Separation.downlinkZero r p g h = if Form.IsEnd (-p) g ∧ Form.IsEnd (-p) h then {r} else ∅
Instances For
Equations
- Form.Separation.downlinkOptions r p g h z = (Set.range z ∪ Set.range fun (gp : ↑(Moves.moves (-p) g)) => Form.rootedAdjoint r ↑gp) ∪ Form.Separation.downlinkZero r p g h
Instances For
Equations
- Form.Separation.downlinkLeftSet r g h y = Form.Separation.downlinkOptions r Player.left g h y
Instances For
Equations
- Form.Separation.downlinkRightSet r g h x = Form.Separation.downlinkOptions r Player.right h g x
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) 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
- Form.Separation.downlinkWitness r g h x y = !{Form.Separation.downlinkLeftSet r g h y | Form.Separation.downlinkRightSet r g h x}
Instances For
If $G$ and $H$ are AreRightSeparating, then $\overline{H}$ and $\overline{G}$
must be AreLeftSeparating.
If $\overline{H}$ and $\overline{G}$ are AreRightSeparating, then $G$ and $H$
must be AreLeftSeparating.