LeanPool.MisereGames.Misere.IntegerInvertible

Misere combinatorial games.

class MisereGames.IntegerInvertible (A : GameForm → Prop) extends MisereGames.Form.HasInt A :

A set of games $\mathcal{A}$ is integer-invertible if it contains every integer $n$ and $n + \overline{n} =_{\mathcal{A}} 0$.

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

has_int (n : ℤ) : A ↑n
int_add_neg_misereEQ (n : ℤ) : (↑n + -↑n) =m A 0

Instances

source

instance MisereGames.instIntegerInvertiblePFreeSubsetGameForm {A : GameForm → Prop} [IntegerInvertible A] :

IntegerInvertible (PFreeSubset A)

If $\mathcal{A}$ is integer-invertible then so is $\operatorname{pf}(\mathcal{A})$.

source

theorem MisereGames.IntegerInvertible.misereOutcome_eq_of_misereEQ {A : GameForm → Prop} [Form.HasZero A] {g h : GameForm} (h1 : g =m A h) :

Form.Misere.Outcome.MisereOutcome g = Form.Misere.Outcome.MisereOutcome h

If $0 \in \mathcal{A}$ and $G =_{\mathcal{A}} H$ then $\operatorname{o}(G) = \operatorname{o}(H)$.

source

theorem MisereGames.IntegerInvertible.misereEQ_shift {A : GameForm → Prop} [Form.ClosedUnderAdd A] [IntegerInvertible A] {g h : GameForm} (hg : A g) (hh : A h) (n : ℤ) :

(g + h) =m A g + ↑n + (h + -↑n)

If $\mathcal{A}$ is integer-invertible, $G, H \in \mathcal{A}$, and $n \in \mathbb{Z}$ then $$ G + H =_{\mathcal{A}} (G + n) + (H - n). $$

source

theorem MisereGames.IntegerInvertible.misereOutcome_add_shift {A : GameForm → Prop} [Form.ClosedUnderAdd A] [IntegerInvertible A] {g h : GameForm} (hg : A g) (hh : A h) (n : ℤ) :

Form.Misere.Outcome.MisereOutcome (g + h) = Form.Misere.Outcome.MisereOutcome (g + ↑n + (h + -↑n))

If $\mathcal{A}$ is integer-invertible, $G, H \in \mathcal{A}$, and $n \in \mathbb{Z}$ then $$ \operatorname{o}(G + H) = \operatorname{o}((G + n) + (H - n)). $$

source

theorem MisereGames.IntegerInvertible.misereOutcome_add_neg_NTippingPoint_N_of_misereOutcome_R {A : GameForm → Prop} {g : GameForm} [OutcomeStable A] [PFree A] [Form.ClosedUnderAddNat A] [Form.HasInt A] [Form.ClosedUnderNeg A] (hA : A g) (hsg : Form.IsShort g) (hR : Form.Misere.Outcome.MisereOutcome g = Outcome.R) :

Form.Misere.Outcome.MisereOutcome (g + -↑(NTippingPoint hsg)) = Outcome.N

source

theorem MisereGames.IntegerInvertible.misereOutcome_add_RTippingPoint_pred_N_of_misereOutcome_L {A : GameForm → Prop} {g : GameForm} [OutcomeStable A] [Form.ClosedUnderAddNat A] [Form.HasInt A] [Form.ClosedUnderNeg A] (hA : PFreeSubset A g) (hsg : Form.IsShort g) (hL : Form.Misere.Outcome.MisereOutcome g = Outcome.L) :

Form.Misere.Outcome.MisereOutcome (g + ↑(↑(RTippingPoint hsg) - 1)) = Outcome.N

source

theorem MisereGames.IntegerInvertible.misereOutcome_add_NTippingPoint_pred_L_of_misereOutcome_L {A : GameForm → Prop} {g : GameForm} [OutcomeStable A] [Form.ClosedUnderAddNat A] [Form.HasInt A] [Form.ClosedUnderNeg A] (hA : PFreeSubset A g) (hsg : Form.IsShort g) (hL : Form.Misere.Outcome.MisereOutcome g = Outcome.L) :

Form.Misere.Outcome.MisereOutcome (g + ↑(↑(NTippingPoint hsg) - 1)) = Outcome.L

source

theorem MisereGames.IntegerInvertible.misereOutcome_add_int_neg_LTippingPoint_L {g : GameForm} (hsg : Form.IsShort g) :

Form.Misere.Outcome.MisereOutcome (g + ↑(-↑(LTippingPoint hsg))) = Outcome.L

source

theorem MisereGames.IntegerInvertible.misereOutcome_add_ge_N_of_misereOutcome_L_left {A : GameForm → Prop} {g h : GameForm} [OutcomeStable A] (hAg : PFreeSubset A g) (hAh : PFreeSubset A h) (hL : Form.Misere.Outcome.MisereOutcome g = Outcome.L) (hh : Form.Misere.Outcome.MisereOutcome h = Outcome.N ∨ Form.Misere.Outcome.MisereOutcome h = Outcome.L) :

Form.Misere.Outcome.MisereOutcome (g + h) ≥ Outcome.N

source

theorem MisereGames.IntegerInvertible.pf_misereOutcome_add_L_of_LTippingPoint_lt_NTippingPoint {A : GameForm → Prop} [OutcomeStable A] [Form.ClosedUnderAddNat A] [Form.ClosedUnderNeg A] [Form.ClosedUnderAdd A] [IntegerInvertible A] {g h : GameForm} (hAg : PFreeSubset A g) (hAh : PFreeSubset A h) (hsg : Form.IsShort g) (hsh : Form.IsShort h) (hLg : Form.Misere.Outcome.MisereOutcome g = Outcome.L) (hgt : LTippingPoint hsh < NTippingPoint hsg) :

Form.Misere.Outcome.MisereOutcome (g + h) = Outcome.L

If $\mathcal{A}$ is an outcome-stable and integer-invertible monoid, and $G, H \in \operatorname{pf}(\mathcal{A})$ with $\operatorname{o}(G) = \mathscr{L}$ then if $\operatorname{n}(G) > \operatorname{l}(H)$ then $\operatorname{o}(G + H) = \mathscr{L}$.

This is (1) in [Davies, Miller, Milley (Lemma 3.13 on p. 16)][davies:SumsPFreeForms:2025].

source

theorem MisereGames.IntegerInvertible.pf_misereOutcome_add_N_of_RTippingPoint_lt_LTippingPoint {A : GameForm → Prop} [OutcomeStable A] [Form.ClosedUnderAddNat A] [Form.ClosedUnderNeg A] [Form.ClosedUnderAdd A] [IntegerInvertible A] {g h : GameForm} (hAg : PFreeSubset A g) (hAh : PFreeSubset A h) (hsg : Form.IsShort g) (hsh : Form.IsShort h) (hLg : Form.Misere.Outcome.MisereOutcome g = Outcome.L) (hNh : Form.Misere.Outcome.MisereOutcome h = Outcome.N) (hlt : RTippingPoint hsg < LTippingPoint hsh) :

Form.Misere.Outcome.MisereOutcome (g + h) = Outcome.N

If $\mathcal{A}$ is an outcome-stable and integer-invertible monoid, and $G, H \in \operatorname{pf}(\mathcal{A})$ with $\operatorname{o}(G) = \mathscr{L}$ and $\operatorname{o}(H) = \mathscr{N}$, then if $\operatorname{r}(G) < \operatorname{l}(H)$ then $\operatorname{o}(G + H) = \mathscr{N}$.

This is (2) in [Davies, Miller, Milley (Lemma 3.13 on p. 16)][davies:SumsPFreeForms:2025].

source

theorem MisereGames.IntegerInvertible.pf_misereOutcome_add_ge_N_of_NN {A : GameForm → Prop} [OutcomeStable A] [Form.ClosedUnderAddNat A] [Form.ClosedUnderNeg A] [Form.ClosedUnderAdd A] [IntegerInvertible A] {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) (hcond : LTippingPoint hsh < RTippingPoint hsg ∨ LTippingPoint hsg < RTippingPoint hsh) :

Form.Misere.Outcome.MisereOutcome (g + h) ≥ Outcome.N

If $\mathcal{A}$ is an outcome-stable and integer-invertible monoid, and $G, H \in \operatorname{pf}(\mathcal{A})$ with $\operatorname{o}(G) = \operatorname{o}(H) = \mathscr{N}$ then if $\operatorname{r}(G) > \operatorname{l}(H)$ or $\operatorname{l}(G) < \operatorname{r}(H)$ then $\operatorname{o}(G + H) \ge \mathscr{N}$.

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

source

theorem MisereGames.IntegerInvertible.pf_misereOutcome_add_L_of_LTippingPoint_lt_NTippingPoint_LR {A : GameForm → Prop} [OutcomeStable A] [Form.ClosedUnderAddNat A] [Form.ClosedUnderNeg A] [Form.ClosedUnderAdd A] [IntegerInvertible A] {g h : GameForm} (hAg : PFreeSubset A g) (hAh : PFreeSubset A h) (hsg : Form.IsShort g) (hsh : Form.IsShort h) (hLg : Form.Misere.Outcome.MisereOutcome g = Outcome.L) (hlt : LTippingPoint hsh < NTippingPoint hsg) :

Form.Misere.Outcome.MisereOutcome (g + h) = Outcome.L

If $\mathcal{A}$ is an outcome-stable and integer-invertible monoid, and $G, H \in \operatorname{pf}(\mathcal{A})$ with $\operatorname{o}(G) = \mathscr{L}$ and $\operatorname{l}(H) < \operatorname{n}(G)$, then $\operatorname{o}(G + H) = \mathscr{L}$.

This is (1) in [Davies, Miller, Milley (Lemma 3.15 on p. 17)][davies:SumsPFreeForms:2025].

source

theorem MisereGames.IntegerInvertible.pf_misereOutcome_add_ge_N_of_LR {A : GameForm → Prop} [OutcomeStable A] [Form.ClosedUnderAddNat A] [Form.ClosedUnderNeg A] [Form.ClosedUnderAdd A] [IntegerInvertible A] {g h : GameForm} (hAg : PFreeSubset A g) (hAh : PFreeSubset A h) (hsg : Form.IsShort g) (hsh : Form.IsShort h) (hLg : Form.Misere.Outcome.MisereOutcome g = Outcome.L) (hRh : Form.Misere.Outcome.MisereOutcome h = Outcome.R) (hcond : NTippingPoint hsh < NTippingPoint hsg ∨ LTippingPoint hsh < RTippingPoint hsg) :

Form.Misere.Outcome.MisereOutcome (g + h) ≥ Outcome.N

If $\mathcal{A}$ is an outcome-stable and integer-invertible monoid, and $G, H \in \operatorname{pf}(\mathcal{A})$ with $\operatorname{o}(G) = \mathscr{L}$, $\operatorname{o}(H) = \mathscr{R}$ and $\operatorname{n}(G) > \operatorname{n}(H)$ or $\operatorname{r}(G) > \operatorname{l}(H)$, then $\operatorname{o}(G + H) \ge \mathscr{N}$.

This is (2) in [Davies, Miller, Milley (Lemma 3.15 on p. 17)][davies:SumsPFreeForms:2025].

source

theorem MisereGames.IntegerInvertible.pf_misereOutcome_add_le_N_of_LR {A : GameForm → Prop} [OutcomeStable A] [Form.ClosedUnderAddNat A] [Form.ClosedUnderNeg A] [Form.ClosedUnderAdd A] [IntegerInvertible A] {g h : GameForm} (hAg : PFreeSubset A g) (hAh : PFreeSubset A h) (hsg : Form.IsShort g) (hsh : Form.IsShort h) (hLg : Form.Misere.Outcome.MisereOutcome g = Outcome.L) (hRh : Form.Misere.Outcome.MisereOutcome h = Outcome.R) (hcond : NTippingPoint hsg < NTippingPoint hsh ∨ RTippingPoint hsg < LTippingPoint hsh) :

Form.Misere.Outcome.MisereOutcome (g + h) ≤ Outcome.N

source

theorem MisereGames.IntegerInvertible.pf_misereOutcome_add_R_of_RTippingPoint_lt_NTippingPoint {A : GameForm → Prop} [OutcomeStable A] [Form.ClosedUnderAddNat A] [Form.ClosedUnderNeg A] [Form.ClosedUnderAdd A] [IntegerInvertible A] {g h : GameForm} (hAg : PFreeSubset A g) (hAh : PFreeSubset A h) (hsg : Form.IsShort g) (hsh : Form.IsShort h) (hRg : Form.Misere.Outcome.MisereOutcome g = Outcome.R) (hgt : RTippingPoint hsh < NTippingPoint hsg) :

Form.Misere.Outcome.MisereOutcome (g + h) = Outcome.R

If $\mathcal{A}$ is an outcome-stable and integer-invertible monoid, and $G, H \in \operatorname{pf}(\mathcal{A})$ with $\operatorname{o}(G) = \mathscr{R}$ then if $\operatorname{r}(H) < \operatorname{n}(G)$ then $\operatorname{o}(G + H) = \mathscr{R}$.

This is mirror of (1) in [Davies, Miller, Milley (Lemma 3.13 on p. 16)][davies:SumsPFreeForms:2025].

source

theorem MisereGames.IntegerInvertible.pf_misereOutcome_add_N_of_LTippingPoint_lt_RTippingPoint {A : GameForm → Prop} [OutcomeStable A] [Form.ClosedUnderAddNat A] [Form.ClosedUnderNeg A] [Form.ClosedUnderAdd A] [IntegerInvertible A] {g h : GameForm} (hAg : PFreeSubset A g) (hAh : PFreeSubset A h) (hsg : Form.IsShort g) (hsh : Form.IsShort h) (hRg : Form.Misere.Outcome.MisereOutcome g = Outcome.R) (hNh : Form.Misere.Outcome.MisereOutcome h = Outcome.N) (hlt : LTippingPoint hsg < RTippingPoint hsh) :

Form.Misere.Outcome.MisereOutcome (g + h) = Outcome.N

If $\mathcal{A}$ is an outcome-stable and integer-invertible monoid, and $G, H \in \operatorname{pf}(\mathcal{A})$ with $\operatorname{o}(G) = \mathscr{R}$ and $\operatorname{o}(H) = \mathscr{N}$, then if $\operatorname{l}(G) < \operatorname{r}(H)$ then $\operatorname{o}(G + H) = \mathscr{N}$.

This is mirror of (2) in [Davies, Miller, Milley (Lemma 3.13 on p. 16)][davies:SumsPFreeForms:2025].

source

theorem MisereGames.IntegerInvertible.pf_misereOutcome_add_le_N_of_NN {A : GameForm → Prop} [OutcomeStable A] [Form.ClosedUnderAddNat A] [Form.ClosedUnderNeg A] [Form.ClosedUnderAdd A] [IntegerInvertible A] {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) (hcond : RTippingPoint hsh < LTippingPoint hsg ∨ RTippingPoint hsg < LTippingPoint hsh) :

Form.Misere.Outcome.MisereOutcome (g + h) ≤ Outcome.N

If $\mathcal{A}$ is an outcome-stable and integer-invertible monoid, and $G, H \in \operatorname{pf}(\mathcal{A})$ with $\operatorname{o}(G) = \operatorname{o}(H) = \mathscr{N}$ then if $\operatorname{r}(G) < \operatorname{l}(H)$ or $\operatorname{l}(G) > \operatorname{r}(H)$ then $\operatorname{o}(G + H) \le \mathscr{N}$.

This is mirror of [Davies, Miller, Milley (Lemma 3.14 on p. 16)][davies:SumsPFreeForms:2025].

source

theorem MisereGames.IntegerInvertible.pf_misereOutcome_add_R_of_RTippingPoint_lt_NTippingPoint_RL {A : GameForm → Prop} [OutcomeStable A] [Form.ClosedUnderAddNat A] [Form.ClosedUnderNeg A] [Form.ClosedUnderAdd A] [IntegerInvertible A] {g h : GameForm} (hAg : PFreeSubset A g) (hAh : PFreeSubset A h) (hsg : Form.IsShort g) (hsh : Form.IsShort h) (hRg : Form.Misere.Outcome.MisereOutcome g = Outcome.R) (hlt : RTippingPoint hsh < NTippingPoint hsg) :

Form.Misere.Outcome.MisereOutcome (g + h) = Outcome.R

If $\mathcal{A}$ is an outcome-stable and integer-invertible monoid, and $G, H \in \operatorname{pf}(\mathcal{A})$ with $\operatorname{o}(G) = \mathscr{R}$ and $\operatorname{r}(H) < \operatorname{n}(G)$, then $\operatorname{o}(G + H) = \mathscr{R}$.

This is mirror of (1) in [Davies, Miller, Milley (Lemma 3.15 on p. 17)][davies:SumsPFreeForms:2025].

source

theorem MisereGames.IntegerInvertible.pf_misereOutcome_add_le_N_of_RL {A : GameForm → Prop} [OutcomeStable A] [Form.ClosedUnderAddNat A] [Form.ClosedUnderNeg A] [Form.ClosedUnderAdd A] [IntegerInvertible A] {g h : GameForm} (hAg : PFreeSubset A g) (hAh : PFreeSubset A h) (hsg : Form.IsShort g) (hsh : Form.IsShort h) (hRg : Form.Misere.Outcome.MisereOutcome g = Outcome.R) (hLh : Form.Misere.Outcome.MisereOutcome h = Outcome.L) (hcond : NTippingPoint hsh < NTippingPoint hsg ∨ RTippingPoint hsh < LTippingPoint hsg) :

Form.Misere.Outcome.MisereOutcome (g + h) ≤ Outcome.N

If $\mathcal{A}$ is an outcome-stable and integer-invertible monoid, and $G, H \in \operatorname{pf}(\mathcal{A})$ with $\operatorname{o}(G) = \mathscr{R}$, $\operatorname{o}(H) = \mathscr{L}$ and $\operatorname{n}(G) < \operatorname{n}(H)$ or $\operatorname{r}(H) < \operatorname{l}(G)$, then $\operatorname{o}(G + H) \le \mathscr{N}$.

This is mirror of (2) in [Davies, Miller, Milley (Lemma 3.15 on p. 17)][davies:SumsPFreeForms:2025].