Misere combinatorial games.

class MisereGames.IntegerInvertible.PropertyX (A : GameForm → Prop) : Prop

A set of games $\mathcal{A}$ has Property X if, for all $G, H \in \operatorname{pf}(\mathcal{A})$ with $\operatorname{o}(G) = \operatorname{o}(H) = \mathscr{N}$

1. if $\operatorname{r}(G) = \operatorname{l}(H) = 1$, where $G$ is a Left end but $H$ is not, then $\operatorname{o}(G + H) = N$; and
2. if $\operatorname{l}(G) = \operatorname{r}(H) = 1$, where $H$ is a Right end but $G$ is not, then $\operatorname{o}(G + H) = N$.

This is [Davies, Miller, Milley (Definition 3.16 on p. 18)][davies:SumsPFreeForms:2025].

• prop_left {g h : GameForm} (hAg : PFreeSubset A g) (hAh : PFreeSubset A h) (hsg : Form.IsShort g) (hsh : Form.IsShort h) (hNg : Form.Misere.Outcome.MisereOutcome g = Outcome.N) (hNh : Form.Misere.Outcome.MisereOutcome h = Outcome.N) (hge : Form.IsEnd Player.left g) (hnge : ¬Form.IsEnd Player.left h) (hrg : RTippingPoint hsg = 1) (hlh : LTippingPoint hsh = 1) : Form.Misere.Outcome.MisereOutcome (g + h) = Outcome.N
• prop_right {g h : GameForm} (hAg : PFreeSubset A g) (hAh : PFreeSubset A h) (hsg : Form.IsShort g) (hsh : Form.IsShort h) (hNg : Form.Misere.Outcome.MisereOutcome g = Outcome.N) (hNh : Form.Misere.Outcome.MisereOutcome h = Outcome.N) (hge : Form.IsEnd Player.right h) (hnge : ¬Form.IsEnd Player.right g) (hlg : LTippingPoint hsg = 1) (hrh : RTippingPoint hsh = 1) : Form.Misere.Outcome.MisereOutcome (g + h) = Outcome.N

structure MisereGames.IntegerInvertible.Lemma317Claim (g h : GameForm) (hsg : Form.IsShort g) (hsh : Form.IsShort h) : Prop

The conjunction of the eight implications of Lemma 3.17 for a fixed pair $(G, H)$. We package them in a structure so that the (mutual) induction can return all of them at once.

• p1a : Form.Misere.Outcome.MisereOutcome g = Outcome.L → Form.Misere.Outcome.MisereOutcome h = Outcome.N → NTippingPoint hsg = LTippingPoint hsh → Form.Misere.Outcome.MisereOutcome (g + h) = Outcome.L

  1(a): if $\operatorname{o}(G) = \mathscr{L}$, $\operatorname{o}(H) = \mathscr{N}$, $\operatorname{n}(G) = \operatorname{l}(H)$ then $\operatorname{o}(G + H) = \mathscr{L}$.

• p1b : Form.Misere.Outcome.MisereOutcome g = Outcome.L → Form.Misere.Outcome.MisereOutcome h = Outcome.N → RTippingPoint hsg = LTippingPoint hsh → Form.Misere.Outcome.MisereOutcome (g + h) = Outcome.N

  1(b): if $\operatorname{o}(G) = \mathscr{L}$, $\operatorname{o}(H) = \mathscr{N}$, $\operatorname{r}(G) = \operatorname{l}(H)$ then $\operatorname{o}(G + H) = \mathscr{N}$.

• p2a : Form.Misere.Outcome.MisereOutcome g = Outcome.R → Form.Misere.Outcome.MisereOutcome h = Outcome.N → NTippingPoint hsg = RTippingPoint hsh → Form.Misere.Outcome.MisereOutcome (g + h) = Outcome.R

  2(a): if $\operatorname{o}(G) = \mathscr{R}$, $\operatorname{o}(H) = \mathscr{N}$, $\operatorname{n}(G) = \operatorname{r}(H)$ then $\operatorname{o}(G + H) = \mathscr{R}$.

• p2b : Form.Misere.Outcome.MisereOutcome g = Outcome.R → Form.Misere.Outcome.MisereOutcome h = Outcome.N → LTippingPoint hsg = RTippingPoint hsh → Form.Misere.Outcome.MisereOutcome (g + h) = Outcome.N

  2(b): if $\operatorname{o}(G) = \mathscr{R}$, $\operatorname{o}(H) = \mathscr{N}$, $\operatorname{l}(G) = \operatorname{r}(H)$ then $\operatorname{o}(G + H) = \mathscr{N}$.

• p3 : Form.Misere.Outcome.MisereOutcome g = Outcome.N → Form.Misere.Outcome.MisereOutcome h = Outcome.N → RTippingPoint hsg = LTippingPoint hsh ∨ LTippingPoint hsg = RTippingPoint hsh → Form.Misere.Outcome.MisereOutcome (g + h) = Outcome.N

  3: if $\operatorname{o}(G), \operatorname{o}(H) = \mathscr{N}$, $\operatorname{r}(G) = \operatorname{l}(H)$ or $\operatorname{l}(G) = \operatorname{r}(H)$ then $\operatorname{o}(G + H) = \mathscr{N}$.

• p4a : Form.Misere.Outcome.MisereOutcome g = Outcome.L → Form.Misere.Outcome.MisereOutcome h = Outcome.R → NTippingPoint hsg = LTippingPoint hsh → Form.Misere.Outcome.MisereOutcome (g + h) = Outcome.L

  4(a): if $\operatorname{o}(G) = \mathscr{L}$, $\operatorname{o}(H) = \mathscr{R}$, $\operatorname{n}(G) = \operatorname{l}(H)$ then $\operatorname{o}(G + H) = \mathscr{L}$.

• p4b : Form.Misere.Outcome.MisereOutcome g = Outcome.L → Form.Misere.Outcome.MisereOutcome h = Outcome.R → NTippingPoint hsg = NTippingPoint hsh ∨ RTippingPoint hsg = LTippingPoint hsh → Form.Misere.Outcome.MisereOutcome (g + h) = Outcome.N

  4(b): if $\operatorname{o}(G) = \mathscr{L}$, $\operatorname{o}(H) = \mathscr{R}$, $\operatorname{n}(G) = \operatorname{n}(H)$ or $\operatorname{r}(G) = \operatorname{l}(H)$ then $\operatorname{o}(G + H) = \mathscr{N}$.

• p4c : Form.Misere.Outcome.MisereOutcome g = Outcome.L → Form.Misere.Outcome.MisereOutcome h = Outcome.R → RTippingPoint hsg = NTippingPoint hsh → Form.Misere.Outcome.MisereOutcome (g + h) = Outcome.R

  4(c): if $\operatorname{o}(G) = \mathscr{L}$, $\operatorname{o}(H) = \mathscr{R}$, $\operatorname{r}(G) = \operatorname{n}(H)$ then $\operatorname{o}(G + H) = \mathscr{R}$.

theorem MisereGames.IntegerInvertible.lemma_3_17 {A : GameForm → Prop} [OutcomeStable A] [Form.Hereditary A] [Form.ClosedUnderAddNat A] [Form.ClosedUnderNeg A] [Form.ClosedUnderAdd A] [IntegerInvertible A] [PropertyX A] {g h : GameForm} (hsg : Form.IsShort g) (hsh : Form.IsShort h) (hAg : PFreeSubset A g) (hAh : PFreeSubset A h) : Lemma317Claim g h hsg hsh

If $\mathcal{A}$ is an outcome-stable, hereditary, and integer-invertible monoid that has Property X, and $G, H \in \operatorname{pf}(\mathcal{A})$, then Lemma317Claim holds.

This is [Davies, Miller, Milley (Lemma 3.17 on p. 18)][davies:SumsPFreeForms:2025].

theorem MisereGames.IntegerInvertible.misereOutcome_ne_P_of_propertyX {A : GameForm → Prop} [OutcomeStable A] [Form.Hereditary A] [Form.ClosedUnderAddNat A] [Form.ClosedUnderNeg A] [Form.ClosedUnderAdd A] [IntegerInvertible A] [PropertyX A] {g h : GameForm} (hAg : PFreeSubset A g) (hAh : PFreeSubset A h) (hsg : Form.IsShort g) (hsh : Form.IsShort h) : Form.Misere.Outcome.MisereOutcome (g + h) ≠ Outcome.P

If $\mathcal{A}$ is an outcome-stable, hereditary, and integer-invertible monoid with Property X, and $G, H \in \operatorname{pf}(\mathcal{A})$, then $\operatorname{o}(G + H) \ne \mathscr{P}$.

This is [Davies, Miller, Milley (Lemma 3.18 on p. 22)][davies:SumsPFreeForms:2025].

theorem MisereGames.IntegerInvertible.isPFree_of_propertyX {A : GameForm → Prop} [OutcomeStable A] [Form.Hereditary A] [Form.ClosedUnderAddNat A] [Form.ClosedUnderNeg A] [Form.ClosedUnderAdd A] [IntegerInvertible A] [PropertyX A] {g h : GameForm} (hAg : PFreeSubset A g) (hAh : PFreeSubset A h) (hsg : Form.IsShort g) (hsh : Form.IsShort h) : IsPFree (g + h)

If $\mathcal{A}$ is an outcome-stable, hereditary, and integer-invertible monoid with Property X, then $\operatorname{pf}(\mathcal{A})$ is a monoid.

This is [Davies, Miller, Milley (Lemma 3.19 on p. 23)][davies:SumsPFreeForms:2025].

theorem MisereGames.IntegerInvertible.isPFree_of_subset_propertyX {S A : GameForm → Prop} [OutcomeStable S] [Form.Hereditary S] [Form.ClosedUnderAddNat S] [Form.ClosedUnderNeg S] [Form.ClosedUnderAdd S] [IntegerInvertible S] [PropertyX S] (hAS : ∀ {x : GameForm}, PFreeSubset A x → PFreeSubset S x) (hAadd : ∀ {x y : GameForm}, A x → A y → A (x + y)) {g h : GameForm} (hAg : PFreeSubset A g) (hAh : PFreeSubset A h) (hsg : Form.IsShort g) (hsh : Form.IsShort h) : IsPFree (g + h) ∧ A (g + h)

If $\mathcal{A}$ is a subsemigroup of an outcome-stable, hereditary, and integer-invertible monoid that has Property X, then either $\operatorname{pf}(\mathcal{A})$ is a semigroup or else $\operatorname{pf}(\mathcal{A}) = \emptyset$.

This is [Davies, Miller, Milley (Corollary 3.21 on p. 23)][davies:SumsPFreeForms:2025].