Misere combinatorial games.

@[irreducible]

noncomputable def MisereGames.Form.rootedAdjoint {G : Type (u + 1)} [Form G] (r g : G) : G

$\def\form<#1>[#2]{\left\{#1 \mid #2\right\}}\def\adjr#1{\operatorname{adj}_r\left(#1\right)}$ The rooted adjoint of g with root r. It is the same construction as the adjoint, except that we place an arbitrary root r at the ends rather than 0: $$ \adjr{G} = \begin{cases} \form<r>[r] & \text{if } G \text{ has no ordinary options},\\ \form<\adjr{G^\mathcal{R}}>[r] & \text{if } G \text{ has ordinary Right options, but no ordinary Left options},\\ \form<r>[\adjr{G^\mathcal{L}}] & \text{if } G \text{ has ordinary Left options, but no ordinary Right options},\\ \form<\adjr{G^\mathcal{R}}>[\adjr{G^\mathcal{L}}] & \text{otherwise}. \end{cases} $$

Taking r = 0 recovers the standard adjoint.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MisereGames.Form.adjoint {G : Type (u + 1)} [Form G] (g : G) : G

$\def\form<#1>[#2]{\left\{#1 \mid #2\right\}}$ This extends the notion of the adjoint of a short augmented form, as defined by [Siegel (Definition 5.6 on p. 214)][siegel:GeneralDeadendingUniverse:2025], to transfinite forms: $$ G^\circ = \begin{cases} * & \text{if } G \text{ has no ordinary options},\\ \form<\left(G^\mathcal{R}\right)^\circ>[0] & \text{if} G \text{ has ordinary Right options, but no ordinary Left options},\\ \form<0>[\left(G^\mathcal{L}\right)^\circ] & \text{if} G \text{ has ordinary Left options, but no ordinary Right options},\\ \form<\left(G^\mathcal{R}\right)^\circ>[\left(G^\mathcal{L}\right)^\circ] & \text{otherwise}. \end{cases} $$

[Siegel (Definition 3.2 on p. 228)][siegel:CanonicalPartizan:2015] originally defined this just for short game forms, which was a partizan analogue to the impartial mate due to [Conway (p. 147)][conway:NumbersAndGames:2001].

It is the special case of rootedAdjoint with root 0.

Conventions for notations in identifiers:

• The recommended spelling of ° in identifiers is adjoint.

Equations

• g° = MisereGames.Form.rootedAdjoint 0 g

def MisereGames.Form.«term_°» : Lean.TrailingParserDescr

$\def\form<#1>[#2]{\left\{#1 \mid #2\right\}}$ This extends the notion of the adjoint of a short augmented form, as defined by [Siegel (Definition 5.6 on p. 214)][siegel:GeneralDeadendingUniverse:2025], to transfinite forms: $$ G^\circ = \begin{cases} * & \text{if } G \text{ has no ordinary options},\\ \form<\left(G^\mathcal{R}\right)^\circ>[0] & \text{if} G \text{ has ordinary Right options, but no ordinary Left options},\\ \form<0>[\left(G^\mathcal{L}\right)^\circ] & \text{if} G \text{ has ordinary Left options, but no ordinary Right options},\\ \form<\left(G^\mathcal{R}\right)^\circ>[\left(G^\mathcal{L}\right)^\circ] & \text{otherwise}. \end{cases} $$

[Siegel (Definition 3.2 on p. 228)][siegel:CanonicalPartizan:2015] originally defined this just for short game forms, which was a partizan analogue to the impartial mate due to [Conway (p. 147)][conway:NumbersAndGames:2001].

It is the special case of rootedAdjoint with root 0.

Conventions for notations in identifiers:

• The recommended spelling of ° in identifiers is adjoint.

Equations

• MisereGames.Form.«term_°» = Lean.ParserDescr.trailingNode `MisereGames.Form.«term_°» 1022 0 (Lean.ParserDescr.symbol "°")

theorem MisereGames.Form.adjoint_def {G : Type (u + 1)} [Form G] (g : G) : g° = if IsEnd Player.left g ∧ IsEnd Player.right g then !{{0} | {0}} else if IsEnd Player.left g then !{Set.range fun (gr : ↑(moves Player.right g)) => ↑gr° | {0}} else if IsEnd Player.right g then !{{0} | Set.range fun (gl : ↑(moves Player.left g)) => ↑gl°} else !{Set.range fun (gr : ↑(moves Player.right g)) => ↑gr° | Set.range fun (gl : ↑(moves Player.left g)) => ↑gl°}

The defining equation of adjoint, for when things like unfold adjoint (now just rootedAdjoint 0) won't expose the cases.

theorem MisereGames.Form.Adjoint.rootedAdjoint_zero {G : Type (u + 1)} [Form G] (r : G) : rootedAdjoint r 0 = !{{r} | {r}}

@[simp]

theorem MisereGames.Form.Adjoint.adjoint_zero_eq_star {G : Type (u + 1)} [Form G] : 0° = !{{0} | {0}}

theorem MisereGames.Form.Adjoint.rootedAdjoint_not_isEnd {G : Type (u + 1)} [Form G] (r g : G) (p : Player) : ¬IsEnd p (rootedAdjoint r g)

theorem MisereGames.Form.Adjoint.adjoint_not_isEnd {G : Type (u + 1)} [Form G] (g : G) (p : Player) : ¬IsEnd p (g°)

theorem MisereGames.Form.Adjoint.rootedAdjoint_not_isEndLike {G : Type (u + 1)} [Form G] (r g : G) (p : Player) : ¬IsEndLike p (rootedAdjoint r g)

theorem MisereGames.Form.Adjoint.adjoint_not_isEndLike {G : Type (u + 1)} [Form G] (g : G) (p : Player) : ¬IsEndLike p (g°)

theorem MisereGames.Form.Adjoint.mem_rootedAdjoint_mem_opposite {G : Type (u + 1)} [Form G] {r g gp : G} {p : Player} (h1 : gp ∈ moves p g) : rootedAdjoint r gp ∈ moves (-p) (rootedAdjoint r g)

theorem MisereGames.Form.Adjoint.mem_adjoint_mem_opposite {G : Type (u + 1)} [Form G] {g gp : G} {p : Player} (h1 : gp ∈ moves p g) : gp° ∈ moves (-p) (g°)

theorem MisereGames.Form.Adjoint.mem_rootedAdjoint_exists_opposite {G : Type (u + 1)} [Form G] {r g gp : G} {p : Player} (h1 : gp ∈ moves p (rootedAdjoint r g)) (h2 : ¬IsEnd (-p) g) : ∃ gnp ∈ moves (-p) g, gp = rootedAdjoint r gnp

theorem MisereGames.Form.Adjoint.mem_adjoint_exists_opposite {G : Type (u + 1)} [Form G] {g gp : G} {p : Player} (h1 : gp ∈ moves p (g°)) (h2 : ¬IsEnd (-p) g) : ∃ gnp ∈ moves (-p) g, gp = gnp°

theorem MisereGames.Form.Adjoint.mem_rootedAdjoint_end_opposite {G : Type (u + 1)} [Form G] {r g gp : G} {p : Player} (h1 : gp ∈ moves p (rootedAdjoint r g)) (h2 : IsEnd (-p) g) : gp = r

theorem MisereGames.Form.Adjoint.mem_adjoint_end_opposite {G : Type (u + 1)} [Form G] {g gp : G} {p : Player} (h1 : gp ∈ moves p (g°)) (h2 : IsEnd (-p) g) : gp = 0

theorem MisereGames.Form.Adjoint.short_rootedAdjoint {G : Type (u + 1)} [Form G] {r : G} (h_root_short : IsShort r) {g : G} (h1 : IsShort g) : IsShort (rootedAdjoint r g)

The rooted adjoint of a short game is short, provided the root is short.

theorem MisereGames.Form.Adjoint.short_adjoint {G : Type (u + 1)} [Form G] {g : G} (h1 : IsShort g) : IsShort (g°)

The adjoint of a short game is also short.

theorem MisereGames.Form.Adjoint.rootedAdjoint_moves {G : Type (u + 1)} [Form G] (r : G) (p : Player) (g : G) : moves p (rootedAdjoint r g) = if IsEnd (-p) g then {r} else (fun (x : G) => rootedAdjoint r x) '' moves (-p) g

theorem MisereGames.Form.Adjoint.moves {G : Type (u + 1)} [Form G] (p : Player) (g : G) : moves p (g°) = if IsEnd (-p) g then {0} else (fun (x : G) => x°) '' moves (-p) g

theorem MisereGames.Form.Adjoint.rootedAdjoint_neg {G : Type (u + 1)} [Form G] (r g : G) : rootedAdjoint (-r) (-g) = -rootedAdjoint r g

The rooted adjoint of the conjugate is the conjugate of the rooted adjoint, with the root conjugated.

theorem MisereGames.Form.Adjoint.adjoint_neg {G : Type (u + 1)} [Form G] (g : G) : (-g)° = -g°

The adjoint of the conjugate is the conjugate of the adjoint.