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.coe_lower (x : Dyadic) : ↑x.lower = ↑x - (↑x.den)⁻¹

theorem Dyadic.coe_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

theorem Dyadic.max_den_lower_upper {x : Dyadic} (hx : x.den ≠ 1) : max x.lower.den x.upper.den = x.den / 2

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}}

@[instance_reducible]

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]

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 ⋯

@[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

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

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

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