Lifting Sets and Comparison

The main results are

• g_misereEQ_h_lift
• g_h_incomparable
• g_h_incomparable_longUniverse

noncomputable def AugmentedForm.adjointsOfSmall : Set AugmentedForm

The set of all adjoints $J^\circ$ (lifted to $u + 1$) for all $J$ in universe $u$.

Equations

• AugmentedForm.adjointsOfSmall = Set.range fun (J : AugmentedForm) => J°.liftSucc

instance AugmentedForm.smallAdjointsOfSmall : Small.{u + 1, u + 2} ↑adjointsOfSmall

noncomputable def AugmentedForm.g : AugmentedForm

$G = \{ J^\circ \mid J^\circ \}$ for all $J$ in universe $u$.

Equations

• AugmentedForm.g = !{AugmentedForm.adjointsOfSmall | AugmentedForm.adjointsOfSmall}

instance AugmentedForm.smallInsertG : Small.{u + 1, u + 2} ↑(insert g adjointsOfSmall)

noncomputable def AugmentedForm.h : AugmentedForm

$H = \{ G, J^\circ \mid G, J^\circ \}$ for all $J$ in universe $u$.

Equations

• AugmentedForm.h = !{insert AugmentedForm.g AugmentedForm.adjointsOfSmall | insert AugmentedForm.g AugmentedForm.adjointsOfSmall}

@[simp]

theorem AugmentedForm.moves_g (p : Player) : Moves.moves p g = adjointsOfSmall

@[simp]

theorem AugmentedForm.moves_h (p : Player) : Moves.moves p h = insert g adjointsOfSmall

theorem AugmentedForm.liftAdjoint_mem_adjointsOfSmall (x : AugmentedForm) : x°.liftSucc ∈ adjointsOfSmall

theorem AugmentedForm.g_not_isEndLike (p : Player) : ¬Form.IsEndLike p g

theorem AugmentedForm.misereOutcome_add_liftSucc_adjoint_eq_P (x : AugmentedForm) : Form.Misere.Outcome.MisereOutcome (x.liftSucc + x°.liftSucc) = Outcome.P

The sum of a (lifted) adjoint and its base game is a $\mathscr{P}$-position.

theorem AugmentedForm.misereOutcome_g_add_lift (x : AugmentedForm) : Form.Misere.Outcome.MisereOutcome (g + x.liftSucc) = Outcome.N

For all games in universe $u$ and $G$ in $u + 1$, $\operatorname{o}(G + X) = \mathscr{N}$.

theorem AugmentedForm.misereOutcome_h_add_lift (x : AugmentedForm) : Form.Misere.Outcome.MisereOutcome (h + x.liftSucc) = Outcome.N

For all games in universe $u$ and $H$ in $u + 1$, $\operatorname{o}(G + X) = \mathscr{N}$.

def AugmentedForm.liftSet (A : AugmentedForm → Prop) : AugmentedForm → Prop

Lift a set on AugmentedForm.{u} to one on AugmentedForm.{u + 1} via the range of AugmentedForm.liftSucc.

Equations

• AugmentedForm.liftSet A x = ∃ (y : AugmentedForm), A y ∧ y.liftSucc = x

theorem AugmentedForm.g_misereEQ_h_lift (A : AugmentedForm → Prop) : g =m (liftSet A)h

If $G, H$ are in universe $u$ then there are indistinguishable modulo set $\mathcal{A}$ lifted to $u + 1$.

theorem AugmentedForm.misereOutcome_g_add_g : Form.Misere.Outcome.MisereOutcome (g + g) = Outcome.P

$o(G + G) = \mathscr{P}$

theorem AugmentedForm.misereOutcome_h_add_g : Form.Misere.Outcome.MisereOutcome (h + g) = Outcome.N

$\operatorname{o}(H + G) = \mathscr{N}$.

theorem AugmentedForm.g_h_incomparable {A : AugmentedForm → Prop} (h_Ag : A g) : ¬g ≥m A h ∧ ¬h ≥m A g

$G$ and $H$ are incomparable modulo any set $\mathcal{A}$ in $u + 1$.

theorem AugmentedForm.g_mem_longUniverse (U : AugmentedForm → Prop) [LongUniverse U] : U g

$G$ is in any universe $\mathcal{U}$ in $u + 1$.

theorem AugmentedForm.g_h_incomparable_longUniverse (U : AugmentedForm → Prop) [LongUniverse U] : ¬g ≥m U h ∧ ¬h ≥m U g

$G$ and $H$ are incomparable modulo any universe $\mathcal{U}$ in $u + 1$.