Dyadic' games

A combinatorial game that is both Short and Numeric is called dyadic. We show that the dyadic games are in correspondence with the Dyadic' rationals, in the sense that there exists a map Dyadic'.toIGame such that:

• Dyadic'.toIGame x is always a dyadic game.
• For any dyadic game y, there exists x with Dyadic'.toIGame x ≈ y.
• The game Dyadic'.toGame x is equivalent to the RatCast of x.

Future projects

Since dyadic rationals are easy to do computations with, there are some projects we could pursue in the future:

• Define the birthday of a dyadic number computably, prove that x.birthday = x.toIGame.birthday.
• Define the simplest dyadic number between two others computably, use that to define IGame.toDyadic.

Upper and lower dyadic fractions

def Dyadic'.lower (x : Dyadic') : Dyadic'

For a dyadic number m / n, returns (m - 1) / n.

Equations

• x.lower = Dyadic'.mkRat (x.num - 1) ⋯

def Dyadic'.upper (x : Dyadic') : Dyadic'

For a dyadic number m / n, returns (m + 1) / n.

Equations

• x.upper = Dyadic'.mkRat (x.num + 1) ⋯

theorem Dyadic'.den_lower_lt {x : Dyadic'} (h : x.den ≠ 1) : x.lower.den < x.den

theorem Dyadic'.den_upper_lt {x : Dyadic'} (h : x.den ≠ 1) : x.upper.den < x.den

def Dyadic'.tacticDyadic_wf : Lean.ParserDescr

An auxiliary tactic for inducting on the denominator of a Dyadic'.

Equations

• Dyadic'.tacticDyadic_wf = Lean.ParserDescr.node `Dyadic'.tacticDyadic_wf 1024 (Lean.ParserDescr.nonReservedSymbol "dyadic_wf" false)

@[simp]

theorem Dyadic'.lower_neg (x : Dyadic') : (-x).lower = -x.upper

@[simp]

theorem Dyadic'.upper_neg (x : Dyadic') : (-x).upper = -x.lower

theorem Dyadic'.le_lower_of_lt {x y : Dyadic'} (hd : x.den ≤ y.den) (h : x < y) : x ≤ y.lower

theorem Dyadic'.upper_le_of_lt {x y : Dyadic'} (hd : y.den ≤ x.den) (h : x < y) : x.upper ≤ y

theorem Dyadic'.lower_eq_of_den_eq_one {x : Dyadic'} (h : x.den = 1) : x.lower = ↑x.num - 1

theorem Dyadic'.upper_eq_of_den_eq_one {x : Dyadic'} (h : x.den = 1) : x.upper = ↑x.num + 1

@[simp]

theorem Dyadic'.lower_lt (x : Dyadic') : x.lower < x

@[simp]

theorem Dyadic'.lt_upper (x : Dyadic') : x < x.upper

theorem Dyadic'.lower_lt_upper (x : Dyadic') : x.lower < x.upper

theorem Dyadic'.val_lower (x : Dyadic') : ↑x.lower = ↑x - (↑x.den)⁻¹

theorem Dyadic'.val_upper (x : Dyadic') : ↑x.upper = ↑x + (↑x.den)⁻¹

theorem Dyadic'.lower_add_le_of_den_le {x y : Dyadic'} (h : x.den ≤ y.den) : (x + y).lower ≤ x + y.lower

theorem Dyadic'.lower_add_le_of_den_ge {x y : Dyadic'} (h : y.den ≤ x.den) : (x + y).lower ≤ x.lower + y

theorem Dyadic'.le_upper_add_of_den_le {x y : Dyadic'} (h : x.den ≤ y.den) : x + y.upper ≤ (x + y).upper

theorem Dyadic'.le_upper_add_of_den_ge {x y : Dyadic'} (h : y.den ≤ x.den) : x.upper + y ≤ (x + y).upper

Dyadic' numbers to games

@[irreducible]

noncomputable def Dyadic'.toIGame (x : Dyadic') : IGame

Converts a dyadic rational into an IGame. This map is defined so that:

• If x : ℤ, then toIGame x = ↑x.
• Otherwise, if x = m / n with n even, then toIGame x = !{(m - 1) / n | (m + 1) / n}. Note that both options will have smaller denominators.

Equations

• ↑x = if x_1 : x.den = 1 then ↑x.num else !{{↑x.lower} | {↑x.upper}}

noncomputable instance Dyadic'.instCoeIGame : Coe Dyadic' IGame

Equations

• Dyadic'.instCoeIGame = { coe := Dyadic'.toIGame }

theorem Dyadic'.toIGame_of_den_eq_one {x : Dyadic'} (hx : x.den = 1) : ↑x = ↑x.num

@[simp]

theorem Dyadic'.toIGame_intCast (n : ℤ) : ↑↑n = ↑n

@[simp]

theorem Dyadic'.toIGame_natCast (n : ℕ) : ↑↑n = ↑n

@[simp]

theorem Dyadic'.toIGame_zero : ↑0 = 0

@[simp]

theorem Dyadic'.toIGame_one : ↑1 = 1

theorem Dyadic'.toIGame_of_den_ne_one {x : Dyadic'} (hx : x.den ≠ 1) : ↑x = !{{↑x.lower} | {↑x.upper}}

@[simp]

theorem Dyadic'.toIGame_half : ↑half = ½

@[simp, irreducible]

theorem Dyadic'.toIGame_neg (x : Dyadic') : ↑(-x) = -↑x

theorem Dyadic'.eq_lower_of_mem_leftMoves_toIGame {x : Dyadic'} {y : IGame} (h : y ∈ IGame.moves Player.left ↑x) : y = ↑x.lower

theorem Dyadic'.eq_upper_of_mem_rightMoves_toIGame {x : Dyadic'} {y : IGame} (h : y ∈ IGame.moves Player.right ↑x) : y = ↑x.upper

theorem Dyadic'.toIGame_equiv_lower_upper (x : Dyadic') : ↑x ≈ !{{↑x.lower} | {↑x.upper}}

A dyadic number x is always equivalent to !{lower x | upper x}, though this may not necessarily be the canonical form.

@[irreducible]

instance IGame.Short.dyadic (x : Dyadic') : (↑x).Short

@[irreducible]

instance IGame.Numeric.dyadic (x : Dyadic') : (↑x).Numeric

noncomputable def Dyadic'.toIGameEmbedding : Dyadic' ↪o IGame

Dyadic'.toIGame as an OrderEmbedding.

Equations

• Dyadic'.toIGameEmbedding = OrderEmbedding.ofStrictMono Dyadic'.toIGame Dyadic'.toIGameEmbedding._proof_1

@[simp]

theorem Dyadic'.toIGameEmbedding_apply (x : Dyadic') : toIGameEmbedding x = ↑x

@[simp]

theorem Dyadic'.toIGame_le_toIGame {x y : Dyadic'} : ↑x ≤ ↑y ↔ x ≤ y

@[simp]

theorem Dyadic'.toIGame_lt_toIGame {x y : Dyadic'} : ↑x < ↑y ↔ x < y

@[simp]

theorem Dyadic'.toIGame_equiv_toIGame {x y : Dyadic'} : ↑x ≈ ↑y ↔ x = y

@[simp]

theorem Dyadic'.toIGame_inj {x y : Dyadic'} : ↑x = ↑y ↔ x = y

@[irreducible]

theorem Dyadic'.toIGame_add_equiv (x y : Dyadic') : ↑(x + y) ≈ ↑x + ↑y

theorem Dyadic'.toIGame_sub_equiv (x y : Dyadic') : ↑(x - y) ≈ ↑x - ↑y

@[irreducible]

theorem Dyadic'.toIGame_equiv (x : Dyadic') : ↑x ≈ ↑↑x

@[simp]

theorem Game.mk_dyadic (x : Dyadic') : mk ↑x = ↑↑x

@[simp]

theorem Surreal.mk_dyadic (x : Dyadic') : mk ↑x = ↑↑x

theorem Dyadic'.toIGame_mul_equiv (x y : Dyadic') : ↑(x * y) ≈ ↑x * ↑y

Simp lemmas

ℚ

@[simp]

theorem Dyadic'.toIGame_lt_ratCast {x : Dyadic'} {y : ℚ} : ↑x < ↑y ↔ ↑x < y

@[simp]

theorem Dyadic'.toIGame_le_ratCast {x : Dyadic'} {y : ℚ} : ↑x ≤ ↑y ↔ ↑x ≤ y

@[simp]

theorem Dyadic'.ratCast_lt_toIGame {x : ℚ} {y : Dyadic'} : ↑x < ↑y ↔ x < ↑y

@[simp]

theorem Dyadic'.ratCast_le_toIGame {x : ℚ} {y : Dyadic'} : ↑x ≤ ↑y ↔ x ≤ ↑y

@[simp]

theorem Dyadic'.toIGame_equiv_ratCast {x : Dyadic'} {y : ℚ} : ↑x ≈ ↑y ↔ ↑x = y

@[simp]

theorem Dyadic'.ratCast_equiv_toIGame {x : ℚ} {y : Dyadic'} : ↑x ≈ ↑y ↔ x = ↑y

ℤ

@[simp]

theorem Dyadic'.toIGame_lt_intCast {x : Dyadic'} {y : ℤ} : ↑x < ↑y ↔ x < ↑y

@[simp]

theorem Dyadic'.toIGame_le_intCast {x : Dyadic'} {y : ℤ} : ↑x ≤ ↑y ↔ x ≤ ↑y

@[simp]

theorem Dyadic'.intCast_lt_toIGame {x : ℤ} {y : Dyadic'} : ↑x < ↑y ↔ ↑x < y

@[simp]

theorem Dyadic'.intCast_le_toIGame {x : ℤ} {y : Dyadic'} : ↑x ≤ ↑y ↔ ↑x ≤ y

@[simp]

theorem Dyadic'.toIGame_equiv_intCast {x : Dyadic'} {y : ℤ} : ↑x ≈ ↑y ↔ x = ↑y

@[simp]

theorem Dyadic'.intCast_equiv_toIGame {x : ℤ} {y : Dyadic'} : ↑x ≈ ↑y ↔ ↑x = y

@[simp]

theorem Dyadic'.toIGame_eq_intCast {x : Dyadic'} {y : ℤ} : ↑x = ↑y ↔ x = ↑y

@[simp]

theorem Dyadic'.intCast_eq_toIGame {x : ℤ} {y : Dyadic'} : ↑x = ↑y ↔ ↑x = y

ℕ

@[simp]

theorem Dyadic'.toIGame_lt_natCast {x : Dyadic'} {y : ℕ} : ↑x < ↑y ↔ x < ↑y

@[simp]

theorem Dyadic'.toIGame_le_natCast {x : Dyadic'} {y : ℕ} : ↑x ≤ ↑y ↔ x ≤ ↑y

@[simp]

theorem Dyadic'.natCast_lt_toIGame {x : ℕ} {y : Dyadic'} : ↑x < ↑y ↔ ↑x < y

@[simp]

theorem Dyadic'.natCast_le_toIGame {x : ℕ} {y : Dyadic'} : ↑x ≤ ↑y ↔ ↑x ≤ y

@[simp]

theorem Dyadic'.toIGame_equiv_natCast {x : Dyadic'} {y : ℕ} : ↑x ≈ ↑y ↔ x = ↑y

@[simp]

theorem Dyadic'.natCast_equiv_toIGame {x : ℕ} {y : Dyadic'} : ↑x ≈ ↑y ↔ ↑x = y

@[simp]

theorem Dyadic'.toIGame_eq_natCast {x : Dyadic'} {y : ℕ} : ↑x = ↑y ↔ x = ↑y

@[simp]

theorem Dyadic'.natCast_eq_toIGame {x : ℕ} {y : Dyadic'} : ↑x = ↑y ↔ ↑x = y

0

@[simp]

theorem Dyadic'.toIGame_lt_zero {x : Dyadic'} : ↑x < 0 ↔ x < 0

@[simp]

theorem Dyadic'.toIGame_le_zero {x : Dyadic'} : ↑x ≤ 0 ↔ x ≤ 0

@[simp]

theorem Dyadic'.zero_lt_toIGame {x : Dyadic'} : 0 < ↑x ↔ 0 < x

@[simp]

theorem Dyadic'.zero_le_toIGame {x : Dyadic'} : 0 ≤ ↑x ↔ 0 ≤ x

@[simp]

theorem Dyadic'.toIGame_equiv_zero {x : Dyadic'} : ↑x ≈ 0 ↔ x = 0

@[simp]

theorem Dyadic'.zero_equiv_toIGame {x : Dyadic'} : 0 ≈ ↑x ↔ 0 = x

@[simp]

theorem Dyadic'.toIGame_eq_zero {x : Dyadic'} : ↑x = 0 ↔ x = 0

@[simp]

theorem Dyadic'.zero_eq_toIGame {x : Dyadic'} : 0 = ↑x ↔ 0 = x

1

@[simp]

theorem Dyadic'.toIGame_lt_one {x : Dyadic'} : ↑x < 1 ↔ x < 1

@[simp]

theorem Dyadic'.toIGame_le_one {x : Dyadic'} : ↑x ≤ 1 ↔ x ≤ 1

@[simp]

theorem Dyadic'.one_lt_toIGame {x : Dyadic'} : 1 < ↑x ↔ 1 < x

@[simp]

theorem Dyadic'.one_le_toIGame {x : Dyadic'} : 1 ≤ ↑x ↔ 1 ≤ x

@[simp]

theorem Dyadic'.toIGame_equiv_one {x : Dyadic'} : ↑x ≈ 1 ↔ x = 1

@[simp]

theorem Dyadic'.one_equiv_toIGame {x : Dyadic'} : 1 ≈ ↑x ↔ 1 = x

@[simp]

theorem Dyadic'.toIGame_eq_one {x : Dyadic'} : ↑x = 1 ↔ x = 1

@[simp]

theorem Dyadic'.one_eq_toIGame {x : Dyadic'} : 1 = ↑x ↔ 1 = x

Dyadic games as numbers

noncomputable def IGame.toDyadic (x : IGame) [x.Short] [x.Numeric] : Dyadic'

Any dyadic game (meaning a game that is Short and Numeric) is equivalent to a Dyadic' rational number.

TODO: it should be possible to compute this value explicitly, given the finsets of Dyadic' rationals corresponding to the left and right moves.

Equations

• x.toDyadic = Classical.choose ⋯

@[simp]

theorem IGame.equiv_toIGame_toDyadic (x : IGame) [x.Short] [x.Numeric] : x ≈ ↑x.toDyadic

@[simp]

theorem IGame.toIGame_toDyadic_equiv (x : IGame) [x.Short] [x.Numeric] : ↑x.toDyadic ≈ x

@[simp]

theorem Game.ratCast_toDyadic (x : IGame) [x.Short] [x.Numeric] : ↑↑x.toDyadic = mk x

@[simp]

theorem Surreal.ratCast_toDyadic (x : IGame) [x.Short] [x.Numeric] : ↑↑x.toDyadic = mk x

theorem IGame.equiv_toIGame_iff_toDyadic_eq {x : IGame} [x.Short] [x.Numeric] {y : Dyadic'} : x ≈ ↑y ↔ x.toDyadic = y

theorem IGame.toIGame_equiv_iff_eq_toDyadic {x : IGame} [x.Short] [x.Numeric] {y : Dyadic'} : ↑y ≈ x ↔ y = x.toDyadic

@[simp]

theorem IGame.toDyadic_toIGame (x : Dyadic') : (↑x).toDyadic = x

@[simp]

theorem IGame.toDyadic_zero : toDyadic 0 = 0

@[simp]

theorem IGame.toDyadic_one : toDyadic 1 = 1

@[simp]

theorem IGame.toDyadic_half : ½.toDyadic = Dyadic'.half

@[simp]

theorem IGame.toDyadic_natCast (n : ℕ) : (↑n).toDyadic = ↑n

@[simp]

theorem IGame.toDyadic_ofNat (n : ℕ) [n.AtLeastTwo] : (OfNat.ofNat n).toDyadic = ↑n

@[simp]

theorem IGame.toDyadic_intCast (n : ℤ) : (↑n).toDyadic = ↑n

@[simp]

theorem IGame.toDyadic_neg (x : IGame) [x.Short] [x.Numeric] : (-x).toDyadic = -x.toDyadic

@[simp]

theorem IGame.toDyadic_add (x y : IGame) [x.Short] [x.Numeric] [y.Short] [y.Numeric] : (x + y).toDyadic = x.toDyadic + y.toDyadic

@[simp]

theorem IGame.toDyadic_sub (x y : IGame) [x.Short] [x.Numeric] [y.Short] [y.Numeric] : (x - y).toDyadic = x.toDyadic - y.toDyadic

@[simp]

theorem IGame.toDyadic_mul (x y : IGame) [x.Short] [x.Numeric] [y.Short] [y.Numeric] : (x * y).toDyadic = x.toDyadic * y.toDyadic