Misere combinatorial games.

@[reducible, inline]

abbrev MisereGames.Form.Misere.Adjoint.IsRoot {G : Type (u + 1)} [Form G] (A : G → Prop) (r : G) : Prop

r is a root for A if adding it to any p end in A leaves p winning going first, just as 0 does (isRoot_zero). This is what lets the r-rooted adjoint behave like the standard adjoint in misereOutcome_add_rootedAdjoint_eq_P.

Equations

• MisereGames.Form.Misere.Adjoint.IsRoot A r = ∀ ⦃p : MisereGames.Player⦄ ⦃d : G⦄, A d → MisereGames.Form.IsEnd p d → MisereGames.Form.Misere.Outcome.WinsGoingFirst p (d + r)

theorem MisereGames.Form.Misere.Adjoint.isRoot_of_isZeroLike {G : Type (u + 1)} [Form G] (A : G → Prop) {r : G} (hr : IsZeroLike r) : IsRoot A r

Every zero-like form is a root for every set of forms.

theorem MisereGames.Form.Misere.Adjoint.isRoot_zero {G : Type (u + 1)} [Form G] (A : G → Prop) : IsRoot A 0

0 is a root for every set of forms: adding 0 to an end yields an end.

theorem MisereGames.Form.Misere.Adjoint.misereOutcome_add_rootedAdjoint_eq_P {G : Type (u + 1)} [Form G] {A : G → Prop} [Hereditary A] {r : G} (h_isRoot : IsRoot A r) {g : G} (hg : A g) : Outcome.MisereOutcome (g + rootedAdjoint r g) = Outcome.P

For every form g in A, the sum g + rootedAdjoint r g is a $\mathscr{P}$-position, provided r is a root for the hereditary set A (IsRoot).

This generalises misereOutcome_add_adjoint_eq_P, which is the case where A is arbitrary and r = 0.

theorem MisereGames.Form.Misere.Adjoint.misereOutcome_add_adjoint_eq_P {G : Type (u + 1)} [Form G] (g : G) : Outcome.MisereOutcome (g + g°) = Outcome.P

[Siegel, (Proposition 3.3 on p. 228)][siegel:CanonicalPartizan:2015] showed that, for every short game form $G$, the sum $G+G^\circ$ is always a $\mathscr{P}$-position. (See also [Siegel, (Proposition 6.4 on p. 270)][siegel:CombinatorialGameTheory:2013].) [Siegel, (Proposition 5.7 on p. 214)][siegel:GeneralDeadendingUniverse:2025] later extended this result to short augmented forms. The present result generalises further to transfinite augmented forms.