Solved

@[irreducible]

def GameForm.IsSolved (p : Player) (g : GameForm) : Prop

Intuitively, a position is solved for a given player if they win regardless of the moves they make.

Equations

• GameForm.IsSolved p g = (0 ∉ Moves.moves p g ∧ (g ≠ 0 → ¬Form.IsEnd (-p) g) ∧ ∀ (gp : GameForm), Moves.IsOption gp g → GameForm.IsSolved p gp)

theorem GameForm.isSolved_def (p : Player) (g : GameForm) : IsSolved p g ↔ 0 ∉ Moves.moves p g ∧ (g ≠ 0 → ¬Form.IsEnd (-p) g) ∧ ∀ (gp : GameForm), Moves.IsOption gp g → IsSolved p gp

theorem GameForm.isSolved_zero_not_mem {p : Player} {g : GameForm} (h_isSolved : IsSolved p g) : 0 ∉ Moves.moves p g

theorem GameForm.isSolved_zero_mem {p : Player} {g : GameForm} (h_isSolved : IsSolved p g) (h_isOption : Moves.IsOption 0 g) : 0 ∈ Moves.moves (-p) g

theorem GameForm.isSolved_not_isEnd {p : Player} {g : GameForm} (h_isSolved : IsSolved p g) (h_ne_zero : g ≠ 0) : ¬Form.IsEnd (-p) g

theorem GameForm.isSolved_of_isOption {g gp : GameForm} {p : Player} (h1 : IsSolved p g) (h2 : Moves.IsOption gp g) : IsSolved p gp

@[irreducible]

theorem GameForm.isSolved_of_subposition {g gp : GameForm} {p : Player} (h1 : IsSolved p g) (h2 : Moves.Subposition gp g) : IsSolved p gp

theorem GameForm.isSolved_of_mem_moves {p : Player} {g g' : GameForm} {q : Player} (h : IsSolved p g) (hm : g' ∈ Moves.moves q g) : IsSolved p g'

@[simp]

theorem GameForm.isSolved_neg_iff {p : Player} {g : GameForm} : IsSolved (-p) (-g) ↔ IsSolved p g

@[simp]

theorem GameForm.isSolved_neg_iff' {p : Player} {g : GameForm} : IsSolved p (-g) ↔ IsSolved (-p) g

@[irreducible]

theorem GameForm.isSolved_winsGoingFirst {p : Player} {g : GameForm} (h_isSolved : IsSolved p g) : Form.Misere.Outcome.WinsGoingFirst p g

theorem GameForm.isSolved_ne_zero_misereOutcome {p : Player} {g : GameForm} (h_isSolved : IsSolved p g) (h_ne_zero : g ≠ 0) : Form.Misere.Outcome.MisereOutcome g = Outcome.ofPlayer p

@[irreducible]

theorem GameForm.isSolved_add {p : Player} {g h : GameForm} (h_isSolved_g : IsSolved p g) (h_isSolved_h : IsSolved p h) : IsSolved p (g + h)

The sum of two solved games is solved.

@[irreducible]

theorem GameForm.not_isSolved_add_left {p : Player} {g h : GameForm} (hg : ¬IsSolved p g) : ¬IsSolved p (g + h)

theorem GameForm.not_isSolved_add_right {p : Player} {g h : GameForm} (hh : ¬IsSolved p h) : ¬IsSolved p (g + h)

theorem GameForm.isSolved_add_iff {p : Player} {g h : GameForm} : IsSolved p g ∧ IsSolved p h ↔ IsSolved p (g + h)

Ordinal sums

@[irreducible]

theorem GameForm.isSolved_of_isSolved_ordinalSum {p : Player} {x y : GameForm} (h : IsSolved p (x.ordinalSum y)) : IsSolved p x

Solvedness of an ordinal sum only sees the base: the branch can only be reached through the base, and every subposition of the base is a subposition of the ordinal sum.

@[irreducible]

theorem GameForm.isSolved_ordinalSum {p : Player} {x : GameForm} (y : GameForm) (h_ne_zero : x ≠ 0) (h : IsSolved p x) : IsSolved p (x.ordinalSum y)

theorem GameForm.isSolved_ordinalSum_iff {p : Player} {x y : GameForm} (h_ne_zero : x ≠ 0) : IsSolved p (x.ordinalSum y) ↔ IsSolved p x

Integers

@[simp]

theorem GameForm.isSolved_zero (p : Player) : IsSolved p 0

@[simp]

theorem GameForm.isSolved_right_natCast (n : ℕ) : IsSolved Player.right ↑n

@[simp]

theorem GameForm.isSolved_right_one : IsSolved Player.right 1

@[irreducible]

theorem GameForm.isSolved_iff_zero {g : GameForm} : IsSolved Player.left g ∧ IsSolved Player.right g ↔ g = 0

Zero is the only game solved for both players

@[simp]

theorem GameForm.isSolved_right_intCast_iff (k : ℤ) : IsSolved Player.right ↑k ↔ 0 ≤ k

@[simp]

theorem GameForm.isSolved_left_intCast_iff (k : ℤ) : IsSolved Player.left ↑k ↔ k ≤ 0

@[simp]

theorem GameForm.not_isSolved_left_one : ¬IsSolved Player.left 1

@[irreducible]

theorem GameForm.isSolved_deadEnd {p : Player} {g : GameForm} (h_deadEnd : Form.IsDeadEnd p g) : IsSolved p g

Strides

@[irreducible]

def GameForm.HasStride (p : Player) (g : GameForm) (n : ℕ) : Prop

Stride measures exactly how many moves away each player is from a solved position: the p-stride of g is 0 iff g is solved for p, every p-move lowers it by at most one, some p-move lowers it by exactly one without changing the opponent's stride, and no opponent move raises it.

The last requirement on the best move refers to the opponent's stride of g itself, which would make the definition loopy. Instead we compare against the opponent's candidate stride, the value the opponent's stride would have to take judged from the opponent's options alone (see StrideCandidate); when the opponent's stride exists the two agree (hasStride_strideCandidate).

Stride is not well-defined for all game forms: * has none, and neither does {0 | -1}.

Equations

• One or more equations did not get rendered due to their size.
• GameForm.HasStride p g 0 = GameForm.IsSolved p g

def GameForm.StrideCandidate (p : Player) (g : GameForm) (m : ℕ) : Prop

The value that the p-stride of g must take if it exists, determined by the strides of the p-options alone: 0 when g is solved, otherwise one more than the smallest stride of a p-option.

Equations

• One or more equations did not get rendered due to their size.
• GameForm.StrideCandidate p g 0 = GameForm.IsSolved p g

@[simp]

theorem GameForm.hasStride_eq_zero_iff {p : Player} {g : GameForm} : HasStride p g 0 ↔ IsSolved p g

The stride equals zero if the game is solved.

theorem GameForm.hasStride_isSolved_iff_zero {p : Player} {g : GameForm} {n : ℕ} (h_hasStride : HasStride p g n) : IsSolved p g ↔ n = 0

A game is solved if its stride equals zero.

theorem GameForm.hasStride_not_isSolved_iff_pos {p : Player} {g : GameForm} {n : ℕ} (h_hasStride : HasStride p g n) : ¬IsSolved p g ↔ 0 < n

theorem GameForm.hasStride_succ_iff {p : Player} {g : GameForm} {n : ℕ} : HasStride p g (n + 1) ↔ ¬IsSolved p g ∧ (∀ g' ∈ Moves.moves p g, ∃ (k : ℕ), n ≤ k ∧ HasStride p g' k) ∧ (∃ (g' : GameForm) (_ : g' ∈ Moves.moves p g), HasStride p g' n ∧ ∃ (m : ℕ), HasStride (-p) g' m ∧ StrideCandidate (-p) g m) ∧ ∀ g' ∈ Moves.moves (-p) g, ∃ k ≤ n + 1, HasStride p g' k

@[simp]

theorem GameForm.strideCandidate_zero_iff {p : Player} {g : GameForm} : StrideCandidate p g 0 ↔ IsSolved p g

theorem GameForm.strideCandidate_succ_iff {p : Player} {g : GameForm} {m : ℕ} : StrideCandidate p g (m + 1) ↔ ¬IsSolved p g ∧ (∀ g' ∈ Moves.moves p g, ∃ (k : ℕ), m ≤ k ∧ HasStride p g' k) ∧ ∃ (g' : GameForm) (_ : g' ∈ Moves.moves p g), HasStride p g' m

theorem GameForm.hasStride_strideCandidate {p : Player} {g : GameForm} {n : ℕ} (h : HasStride p g n) : StrideCandidate p g n

A stride is in particular a stride candidate.

theorem GameForm.hasStride_succ_support {p : Player} {g : GameForm} {n : ℕ} (h : HasStride p g (n + 1)) (g' : GameForm) (hg' : g' ∈ Moves.moves p g) : ∃ (k : ℕ), n ≤ k ∧ HasStride p g' k

If the stride of $G$ is not zero, then every response lowers the stride by at most one.

theorem GameForm.hasStride_succ_exists_best {p : Player} {g : GameForm} {n : ℕ} (h : HasStride p g (n + 1)) : ∃ (g' : GameForm) (_ : g' ∈ Moves.moves p g), HasStride p g' n ∧ ∃ (m : ℕ), HasStride (-p) g' m ∧ StrideCandidate (-p) g m

If the stride of $G$ is not zero, then there exist some response lowering the stride by exactly one which keeps the opponent's stride candidate.

theorem GameForm.hasStride_succ_support_neg {p : Player} {g : GameForm} {n : ℕ} (h : HasStride p g (n + 1)) (g' : GameForm) (hg' : g' ∈ Moves.moves (-p) g) : ∃ k ≤ n + 1, HasStride p g' k

If the stride of $G$ is not zero, then no opponent move raises the stride.

theorem GameForm.hasStride_succ_not_isEnd {p : Player} {g : GameForm} {n : ℕ} (h : HasStride p g (n + 1)) : ¬Form.IsEnd p g

@[irreducible]

theorem GameForm.hasStride_unique {p : Player} {g : GameForm} {n k : ℕ} (h_n : HasStride p g n) (h_k : HasStride p g k) : n = k

If a game has stride, then the value is unique.

This is a workaround for not defining stride as a function to option ℕ.

theorem GameForm.strideCandidate_unique {p : Player} {g : GameForm} {n k : ℕ} (h_n : StrideCandidate p g n) (h_k : StrideCandidate p g k) : n = k

A stride candidate is unique, since it is determined by the strides of the options.

theorem GameForm.hasStride_mk_iff {p : Player} (n : ℕ) {k : ℕ} {g : GameForm} (h_stride : HasStride p g n) : HasStride p g k ↔ k = n

Helper for building iff lemmas

theorem GameForm.hasStride_good_move_neg_stride {p : Player} {g : GameForm} {n r : ℕ} (h : HasStride p g (n + 1)) (h_r : HasStride (-p) g r) : ∃ (g' : GameForm) (_ : g' ∈ Moves.moves p g), HasStride p g' n ∧ HasStride (-p) g' r

The good move preserves (-p)-stride: if HasStride p g (n+1) and HasStride (-p) g r, then the good p-move has (-p)-stride exactly r.

theorem GameForm.hasStride_of_mem_moves_neg {p : Player} {g g' : GameForm} {n : ℕ} (hg : HasStride p g n) (hm : g' ∈ Moves.moves (-p) g) : ∃ k ≤ n, HasStride p g' k

Opponent moves have stride ≤ n.

theorem GameForm.hasStride_succ_iff' {p : Player} {g : GameForm} {n m : ℕ} (h_hasStride_m : HasStride (-p) g m) : HasStride p g (n + 1) ↔ ¬IsSolved p g ∧ (∀ g' ∈ Moves.moves p g, ∃ (k : ℕ), n ≤ k ∧ HasStride p g' k) ∧ (∃ (g' : GameForm) (_ : g' ∈ Moves.moves p g), HasStride p g' n ∧ HasStride (-p) g' m) ∧ ∀ g' ∈ Moves.moves (-p) g, ∃ k ≤ n + 1, HasStride p g' k

A variant of hasStride_succ_iff for when the (-p)-stride is known: the good move then simply has to preserve it.

theorem GameForm.hasStride_succ_exists_best' {p : Player} {g : GameForm} {n m : ℕ} (h_n : HasStride p g (n + 1)) (h_m : HasStride (-p) g m) : ∃ (g' : GameForm) (_ : g' ∈ Moves.moves p g), HasStride p g' n ∧ HasStride (-p) g' m

Variant of hasStride_succ_exists_best with known opponent stride

theorem GameForm.hasStride_of_mem_moves {p : Player} {g g' : GameForm} {n : ℕ} (hg : HasStride p g n) (hm : g' ∈ Moves.moves p g) : ∃ (j : ℕ), n - 1 ≤ j ∧ HasStride p g' j

theorem GameForm.hasStride_of_options (g : GameForm) (n : Player → ℕ) (h_solved : ∀ (q : Player), n q = 0 → IsSolved q g) (h_not_solved : ∀ (q : Player), n q ≠ 0 → ¬IsSolved q g) (h_support : ∀ (q : Player), ∀ g' ∈ Moves.moves q g, ∃ (k : ℕ), n q ≤ k + 1 ∧ HasStride q g' k) (h_best : ∀ (q : Player), n q ≠ 0 → ∃ (g' : GameForm) (_ : g' ∈ Moves.moves q g), HasStride q g' (n q - 1) ∧ HasStride (-q) g' (n (-q))) (h_support_neg : ∀ (q : Player), ∀ g' ∈ Moves.moves (-q) g, ∃ k ≤ n q, HasStride q g' k) (q : Player) : HasStride q g (n q)

Build the strides of both players of g from their values n at g and the strides of the options. This is the interface for rulesets: the hypotheses are the "race" conditions on the ruleset's stride function at g.

Addition

@[irreducible]

theorem GameForm.hasStride_add {p : Player} {g h : GameForm} {sL_g sL_h sR_g sR_h : ℕ} (h_sL_g : HasStride p g sL_g) (h_sL_h : HasStride p h sL_h) (h_sR_g : HasStride (-p) g sR_g) (h_sR_h : HasStride (-p) h sR_h) : HasStride p (g + h) (sL_g + sL_h)

The stride of a sum is the sum of the strides.

@[simp]

theorem GameForm.hasStride_neg_iff {p : Player} {g : GameForm} {n : ℕ} : HasStride (-p) (-g) n ↔ HasStride p g n

@[simp]

theorem GameForm.hasStride_neg_iff' {p : Player} {g : GameForm} {n : ℕ} : HasStride p (-g) n ↔ HasStride (-p) g n

Ordinal sums

@[irreducible]

theorem GameForm.hasStride_ordinalSum {p : Player} {x : GameForm} (y : GameForm) {l r : ℕ} (h_ne_zero : x ≠ 0) (h_l : HasStride p x l) (h_r : HasStride (-p) x r) : HasStride p (x.ordinalSum y) l

Ordinal sums forget their branch: the strides of x : y are the strides of the base x, for every branch y whatsoever. The base must be nonzero since 0 : y = y.

Together with hasStride_add this recovers the strides of Hackenbush trees, Σ (ground edge : subtree), without any graph argument; see Hackenbush.hasStride_groundCount for the general graph case.

theorem GameForm.hasStride_ordinalSum_iff {p : Player} {x : GameForm} (y : GameForm) {l r k : ℕ} (h_ne_zero : x ≠ 0) (h_l : HasStride p x l) (h_r : HasStride (-p) x r) : HasStride p (x.ordinalSum y) k ↔ k = l

Integers

theorem GameForm.hasStride_zero (p : Player) : HasStride p 0 0

@[simp]

theorem GameForm.hasStride_zero_iff {p : Player} {n : ℕ} : HasStride p 0 n ↔ n = 0

theorem GameForm.hasStride_right_natCast (n : ℕ) : HasStride Player.right (↑n) 0

@[simp]

theorem GameForm.hasStride_right_natCast_iff (n : ℕ) {k : ℕ} : HasStride Player.right (↑n) k ↔ k = 0

theorem GameForm.hasStride_right_one : HasStride Player.right 1 0

@[simp]

theorem GameForm.hasStride_right_one_iff {n : ℕ} : HasStride Player.right 1 n ↔ n = 0

theorem GameForm.hasStride_left_one : HasStride Player.left 1 1

theorem GameForm.hasStride_left_natCast (n : ℕ) : HasStride Player.left (↑n) n

@[simp]

theorem GameForm.hasStride_left_natCast_iff (n : ℕ) {k : ℕ} : HasStride Player.left (↑n) k ↔ k = n

theorem GameForm.hasStride_left_intCast (n : ℤ) : HasStride Player.left (↑n) n.toNat

@[simp]

theorem GameForm.hasStride_left_intCast_iff (n : ℤ) {k : ℕ} : HasStride Player.left (↑n) k ↔ k = n.toNat

@[simp]

theorem GameForm.hasStride_right_intCast_iff (n : ℤ) {k : ℕ} : HasStride Player.right (↑n) k ↔ k = (-n).toNat

Dyadic rationals

Strides of the canonical forms of 1/2 = {0 | 1} and 3/4 = {1/2 | 1}. The latter is the smallest number whose stride only exists because the good move is required to preserve the opponent's stride rather than the opponent being required to be able to preserve ours: Right's only move from 3/4 is to 1, which lowers Left's stride from 2 to 1.

theorem GameForm.isSolved_right_half : IsSolved Player.right !{{0} | {1}}

theorem GameForm.hasStride_left_half : HasStride Player.left !{{0} | {1}} 1

theorem GameForm.isSolved_right_threeQuarters : IsSolved Player.right !{{!{{0} | {1}}} | {1}}

theorem GameForm.hasStride_left_threeQuarters : HasStride Player.left !{{!{{0} | {1}}} | {1}} 2

Outcomes

theorem GameForm.hasStride_winsGoingFirst_iff {p : Player} {g : GameForm} {l r : ℕ} (h_l : HasStride p g l) (h_r : HasStride (-p) g r) : Form.Misere.Outcome.WinsGoingFirst p g ↔ l ≤ r

If a game has both strides, then they determine who wins going first.

theorem GameForm.hasStride_misereOutcome_iff_lt {p : Player} {g : GameForm} {l r : ℕ} (h_l : HasStride p g l) (h_r : HasStride (-p) g r) : Form.Misere.Outcome.MisereOutcome g = Outcome.ofPlayer p ↔ l < r

If a game has both strides, then they determine the outcome.

theorem GameForm.hasStride_misereOutcome_iff_ge {p : Player} {g : GameForm} {l r : ℕ} (h_l : HasStride p g l) (h_r : HasStride (-p) g r) : Form.Misere.Outcome.MisereOutcome g = Outcome.ofPlayer (-p) ↔ l > r

theorem GameForm.hasStride_misereOutcome_iff_eq {p : Player} {g : GameForm} {l r : ℕ} (h_l : HasStride p g l) (h_r : HasStride (-p) g r) : Form.Misere.Outcome.MisereOutcome g = Outcome.N ↔ l = r

If a game has both strides, then they determine the outcome.

theorem GameForm.misereOutcome_eq_of_hasStride {g : GameForm} {h : GameForm} {l r : ℕ} (h_lg : HasStride Player.left g l) (h_rg : HasStride Player.right g r) (h_lh : HasStride Player.left h l) (h_rh : HasStride Player.right h r) : Form.Misere.Outcome.MisereOutcome g = Form.Misere.Outcome.MisereOutcome h

Games with the same strides have the same outcome.

@[irreducible]

theorem GameForm.hasStride_isPFree {p : Player} {g : GameForm} {l r : ℕ} (h_l : HasStride p g l) (h_r : HasStride (-p) g r) : IsPFree g

If a game has both strides, then it is $\mathscr{P}$-free.

class GameForm.Strided (A : GameForm → Prop) : Prop

• mk_with_strides (l r : ℕ) : ∃ (g : GameForm), A g ∧ HasStride Player.left g l ∧ HasStride Player.right g r
• has_stride (p : Player) {g : GameForm} (h_g : A g) : ∃ (n : ℕ), HasStride p g n

theorem GameForm.ClosedUnderAdd.closure_has_stride_aux {R : Type u} [Ruleset R] (p : Player) {g : GameForm} (stride : R → Player → ℕ) (hasStride : ∀ (r : R) (p : Player), HasStride p (Ruleset.toGameForm r) (stride r p)) (h_g : Form.ClosedUnderAdd.closure (Ruleset.Forms R) g) : ∃ (n : ℕ), HasStride p g n

theorem GameForm.ClosedUnderAdd.closure_mk_with_strides_aux {A : GameForm → Prop} (mk_stride_other_zero : ∀ (p : Player) (n : ℕ), ∃ (g : GameForm), A g ∧ HasStride p g n ∧ HasStride (-p) g 0) (l r : ℕ) : ∃ (t : GameForm), Form.ClosedUnderAdd.closure A t ∧ HasStride Player.left t l ∧ HasStride Player.right t r

instance GameForm.instStridedClosure {A : GameForm → Prop} [Strided A] : Strided (Form.ClosedUnderAdd.closure A)

theorem GameForm.stride_diff_eq_of_misereEQ {A : GameForm → Prop} [Strided A] {g h : GameForm} (h_eq : g =m A h) {sL_g sR_g sL_h sR_h : ℕ} (h_ng : HasStride Player.left g sL_g) (h_rg : HasStride Player.right g sR_g) (h_nh : HasStride Player.left h sL_h) (h_rh : HasStride Player.right h sR_h) : ↑sL_g - ↑sR_g = ↑sL_h - ↑sR_h

theorem GameForm.misereEQ_of_stride_diff_eq {A : GameForm → Prop} [Strided A] {g h : GameForm} {sL_g sR_g sL_h sR_h : ℕ} (h_ng : HasStride Player.left g sL_g) (h_rg : HasStride Player.right g sR_g) (h_nh : HasStride Player.left h sL_h) (h_rh : HasStride Player.right h sR_h) (h_diff : ↑sL_g - ↑sR_g = ↑sL_h - ↑sR_h) : g =m A h

theorem GameForm.misereEQ_iff_stride_diff_eq {A : GameForm → Prop} [Strided A] {g h : GameForm} {ng rg nh rh : ℕ} (h_ng : HasStride Player.left g ng) (h_rg : HasStride Player.right g rg) (h_nh : HasStride Player.left h nh) (h_rh : HasStride Player.right h rh) : g =m A h ↔ ↑ng - ↑rg = ↑nh - ↑rh

The stride difference characterises misère equivalence for strided games.

theorem GameForm.ordinalSum_misereEQ {A : GameForm → Prop} [Strided A] {x : GameForm} (y : GameForm) {l r : ℕ} (h_ne_zero : x ≠ 0) (h_l : HasStride Player.left x l) (h_r : HasStride Player.right x r) : x.ordinalSum y =m A x

Modulo a strided class, an ordinal sum with a nonzero strided base is equal to its base, whatever the branch. This is the misère counterpart of the colon principle.

theorem GameForm.misereGE_of_stride_diff_le {A : GameForm → Prop} [Strided A] {g h : GameForm} {sL_g sR_g sL_h sR_h : ℕ} (h_sL_g : HasStride Player.left g sL_g) (h_sR_g : HasStride Player.right g sR_g) (h_sL_h : HasStride Player.left h sL_h) (h_sR_h : HasStride Player.right h sR_h) (h_le : ↑sL_g - ↑sR_g ≤ ↑sL_h - ↑sR_h) : g ≥m A h

theorem GameForm.misereQuotient_linearOrder {A : GameForm → Prop} [Strided A] (a b : MisereQuotient A) : a ≤ b ∨ b ≤ a

The misère quotient of a strided class is totally ordered. This follows from the fact that the ordering is determined by stride differences.

noncomputable def GameForm.Strided.strideDiff {A : GameForm → Prop} [Strided A] (g : GameForm) (hg : A g) : ℤ

The stride difference of a game in a strided class A. This is the left stride minus the right stride, as an integer.

Equations

• GameForm.Strided.strideDiff g hg = ↑⋯.choose - ↑⋯.choose

theorem GameForm.strideDiff_eq {A : GameForm → Prop} [Strided A] {g : GameForm} {hg : A g} {l r : ℕ} (hl : HasStride Player.left g l) (hr : HasStride Player.right g r) : Strided.strideDiff g hg = ↑l - ↑r

The stride difference is well-defined regardless of which stride witnesses are used.

theorem GameForm.Strided.strideDiff_eq_of_misereEQ {A : GameForm → Prop} [Strided A] {g h : GameForm} (hg : A g) (hh : A h) (heq : g =m A h) : strideDiff g hg = strideDiff h hh

Misère equivalent games have the same stride difference.

noncomputable def GameForm.MisereQuotient.strideDiff {A : GameForm → Prop} [Strided A] : MisereQuotient A → ℤ

The stride difference function on the misère quotient, defined via representative. This is well-defined because misère equivalent games have the same stride difference.

Equations

• GameForm.MisereQuotient.strideDiff = Quotient.lift (fun (g : { g : GameForm // A g }) => GameForm.Strided.strideDiff ↑g ⋯) ⋯

theorem GameForm.MisereQuotient.strideDiff_mk {A : GameForm → Prop} [Strided A] (g : GameForm) (hg : A g) : strideDiff (Form.MisereQuotient.mk ⟨g, hg⟩) = Strided.strideDiff g hg

theorem GameForm.MisereQuotient.strideDiff_injective {A : GameForm → Prop} [Strided A] : Function.Injective strideDiff

The stride difference function on the quotient is injective.

theorem GameForm.MisereQuotient.strideDiff_surjective {A : GameForm → Prop} [Strided A] : Function.Surjective strideDiff

The stride difference function on the quotient is surjective: for any integer d, there is a game in A with stride difference d.

noncomputable def GameForm.MisereQuotient.stridedEquivInt {A : GameForm → Prop} [Strided A] : MisereQuotient A ≃ ℤ

The misère quotient of a strided class is equivalent to the integers. The equivalence sends each equivalence class to its stride difference.

Equations

• GameForm.MisereQuotient.stridedEquivInt = Equiv.ofBijective GameForm.MisereQuotient.strideDiff ⋯

theorem GameForm.stride_diff_le_of_misereGE {A : GameForm → Prop} [Strided A] {g h : GameForm} (h_ge : g ≥m A h) {ng rg nh rh : ℕ} (h_ng : HasStride Player.left g ng) (h_rg : HasStride Player.right g rg) (h_nh : HasStride Player.left h nh) (h_rh : HasStride Player.right h rh) : ↑ng - ↑rg ≤ ↑nh - ↑rh

If g ≥m A h then the stride difference of g is ≤ that of h. The converse of misereGE_of_stride_diff_le.

theorem GameForm.misereGE_iff_stride_diff_le {A : GameForm → Prop} [Strided A] {g h : GameForm} {ng rg nh rh : ℕ} (h_ng : HasStride Player.left g ng) (h_rg : HasStride Player.right g rg) (h_nh : HasStride Player.left h nh) (h_rh : HasStride Player.right h rh) : g ≥m A h ↔ ↑ng - ↑rg ≤ ↑nh - ↑rh

Misère GE is equivalent to stride difference inequality.

theorem GameForm.MisereQuotient.mk_le_iff_strideDiff {A : GameForm → Prop} [Strided A] (g h : GameForm) (hg : A g) (hh : A h) : Form.MisereQuotient.mk ⟨g, hg⟩ ≤ Form.MisereQuotient.mk ⟨h, hh⟩ ↔ Strided.strideDiff g hg ≥ Strided.strideDiff h hh

The ordering on the misère quotient corresponds to ≥ on stride differences: mk A g hg ≤ mk A h hh iff strideDiff A g hg ≥ strideDiff A h hh.

theorem GameForm.MisereQuotient.le_iff_strideDiff_ge {A : GameForm → Prop} [Strided A] (a b : MisereQuotient A) : a ≤ b ↔ strideDiff a ≥ strideDiff b

theorem GameForm.MisereQuotient.le_iff_equiv_ge {A : GameForm → Prop} [Strided A] (a b : MisereQuotient A) : a ≤ b ↔ stridedEquivInt a ≥ stridedEquivInt b

The misère quotient ordering via the integer equivalence: a ≤ b iff the image of a under the equivalence is ≥ the image of b. Equivalently, the equivalence is an order-reversing bijection.