Sign sequences

One can define a sequence of approximations for any surreal number x, such that the n-th approximant is the number {s | t} where s and t are the numbers with birthday less than n which are lesser and greater to x, respectively. This yields an ordinal-indexed sequence of signs, where the n-th entry represents whether the n-th approximant to x is lesser, equal, or greater than x.

As it turns out, the correspondence between surreal numbers and sign sequences is both bijective and order-preserving, where the order given to sign sequences is the lexicographic ordering.

Todo

• Define the sign sequence for a surreal number
• Prove that the correspondence is an order isomorphism
• Define the operation x : y on games.

Signs

inductive Sign : Type

Represents a sign in a SignSeq, which is either plus, zero, or minus.

For convenience, and to avoid introducing more notation, we write ⊤ for plus, 0 for zero, and ⊥ for minus.

• plus : Sign
• zero : Sign
• minus : Sign

instance instFintypeSign : Fintype Sign

Equations

• instFintypeSign = { elems := { val := ↑Sign.enumList, nodup := Sign.enumList_nodup }, complete := instFintypeSign._proof_1 }

instance Sign.instTop : Top Sign

Equations

• Sign.instTop = { top := Sign.plus }

instance Sign.instZero : Zero Sign

Equations

• Sign.instZero = { zero := Sign.zero }

instance Sign.instBot : Bot Sign

Equations

• Sign.instBot = { bot := Sign.minus }

@[simp]

theorem Sign.top_def : plus = ⊤

@[simp]

theorem Sign.zero_def : zero = 0

@[simp]

theorem Sign.bot_def : minus = ⊥

instance Sign.instNeg : Neg Sign

Equations

• Sign.instNeg = { neg := fun (x : Sign) => match x with | Sign.plus => Sign.minus | Sign.zero => Sign.zero | Sign.minus => Sign.plus }

@[simp]

theorem Sign.neg_top : -⊤ = ⊥

@[simp]

theorem Sign.neg_zero : -0 = 0

@[simp]

theorem Sign.neg_bot : -⊥ = ⊤

instance Sign.instInvolutiveNeg : InvolutiveNeg Sign

Equations

• Sign.instInvolutiveNeg = { toNeg := Sign.instNeg, neg_neg := Sign.instInvolutiveNeg._proof_1 }

@[simp]

theorem Sign.neg_eq_zero {x : Sign} : -x = 0 ↔ x = 0

def Sign.toInt : Sign → ℤ

Turns a sign into an integer in the obvious way.

Equations

• Sign.plus.toInt = 1
• Sign.zero.toInt = 0
• Sign.minus.toInt = -1

@[simp]

theorem Sign.toInt_plus : ⊤.toInt = 1

@[simp]

theorem Sign.toInt_zero : toInt 0 = 0

@[simp]

theorem Sign.toInt_minus : ⊥.toInt = -1

theorem Sign.toInt_injective : Function.Injective toInt

@[simp]

theorem Sign.toInt_inj {x y : Sign} : x.toInt = y.toInt ↔ x = y

instance Sign.instLinearOrder : LinearOrder Sign

Equations

• Sign.instLinearOrder = LinearOrder.lift' Sign.toInt Sign.toInt_injective

instance Sign.instOrderBot : OrderBot Sign

Equations

• Sign.instOrderBot = { toBot := Sign.instBot, bot_le := Sign.instOrderBot._proof_1 }

instance Sign.instOrderTop : OrderTop Sign

Equations

• Sign.instOrderTop = { toTop := Sign.instTop, le_top := Sign.instOrderTop._proof_1 }

Sign sequences

def SignSeq : Type (u + 1)

A sign sequence is a sequence Ordinal → Sign, which is equal to 0 after some point, and only takes ⊥ or ⊤ as values before that point.

Sign sequences are ordered lexicographically. We show that sign sequences are order-isomorphic to the surreal numbers.

Equations

• SignSeq = { s : Lex (Ordinal.{?u.6} → Sign) // ∃ (l : Ordinal.{?u.6}), ∀ (a : Ordinal.{?u.6}), s a = 0 ↔ l ≤ a }

instance SignSeq.instLinearOrder : LinearOrder SignSeq

Equations

• SignSeq.instLinearOrder = inferInstanceAs (LinearOrder { s : Lex (Ordinal.{?u.8} → Sign) // ∃ (l : Ordinal.{?u.8}), ∀ (a : Ordinal.{?u.8}), s a = 0 ↔ l ≤ a })

def SignSeq.mk (s : Ordinal.{u} → Sign) (l : Ordinal.{u}) (h : ∀ (o : Ordinal.{u}), s o = 0 ↔ l ≤ o) : SignSeq

Construct a sign sequence from a function.

Equations

• SignSeq.mk s l h = ⟨toLex s, ⋯⟩

instance SignSeq.instGetElemOrdinalSignTrue : GetElem SignSeq Ordinal.{u_1} Sign fun (x : SignSeq) (x : Ordinal.{u_1}) => True

Equations

• SignSeq.instGetElemOrdinalSignTrue = { getElem := fun (s : SignSeq) (o : Ordinal.{?u.15}) (x : True) => ofLex (↑s) o }

@[simp]

theorem SignSeq.get_mk (s : Ordinal.{u_1} → Sign) (l : Ordinal.{u_1}) (h : ∀ (o : Ordinal.{u_1}), s o = 0 ↔ l ≤ o) (o : Ordinal.{u_1}) : (mk s l h)[o] = s o

theorem SignSeq.ext {s t : SignSeq} (h : ∀ (o : Ordinal.{u_1}), s[o] = t[o]) : s = t

theorem SignSeq.ext_iff {s t : SignSeq} : s = t ↔ ∀ (o : Ordinal.{u_1}), s[o] = t[o]

def SignSeq.length (s : SignSeq) : Ordinal.{u_1}

The length of a sign sequence is the first ordinal o such that s[o] = 0.

Equations

• s.length = Classical.choose ⋯

@[simp]

theorem SignSeq.get_eq_zero_iff {s : SignSeq} {o : Ordinal.{u_1}} : s[o] = 0 ↔ s.length ≤ o

theorem SignSeq.length_eq_iff {s : SignSeq} {a : Ordinal.{u_1}} : s.length = a ↔ ∀ (o : Ordinal.{u_1}), s[o] = 0 ↔ a ≤ o

@[simp]

theorem SignSeq.length_mk (s : Ordinal.{u} → Sign) (l : Ordinal.{u}) (h : ∀ (o : Ordinal.{u}), s o = 0 ↔ l ≤ o) : (mk s l h).length = l

instance SignSeq.instZero : Zero SignSeq

The constant 0 sequence.

Equations

• SignSeq.instZero = { zero := SignSeq.mk (fun (x : Ordinal.{?u.3}) => 0) 0 SignSeq.instZero._proof_1 }

@[simp]

theorem SignSeq.get_zero (o : Ordinal.{u_1}) : 0[o] = 0

@[simp]

theorem SignSeq.length_zero : length 0 = 0

instance SignSeq.instNeg : Neg SignSeq

The negative of a sign sequence is created by flipping all signs.

Equations

• SignSeq.instNeg = { neg := fun (s : SignSeq) => SignSeq.mk (fun (a : Ordinal.{?u.6}) => -s[a]) s.length ⋯ }

@[simp]

theorem SignSeq.get_neg (s : SignSeq) (o : Ordinal.{u_1}) : (-s)[o] = -s[o]

@[simp]

theorem SignSeq.length_neg (s : SignSeq) : (-s).length = s.length

instance SignSeq.instAppend : Append SignSeq

Append two sequences by putting one after the other ends.

Equations

• SignSeq.instAppend = { append := fun (s t : SignSeq) => SignSeq.mk (fun (o : Ordinal.{?u.7}) => if o < s.length then s[o] else t[o - s.length]) (s.length + t.length) ⋯ }

theorem SignSeq.get_append_of_lt (s t : SignSeq) {o : Ordinal.{u_1}} (h : o < s.length) : (s ++ t)[o] = s[o]

theorem SignSeq.get_append_of_le (s t : SignSeq) {o : Ordinal.{u_1}} (h : s.length ≤ o) : (s ++ t)[o] = t[o - s.length]

@[simp]

theorem SignSeq.get_append_add (s t : SignSeq) (o : Ordinal.{u_1}) : (s ++ t)[s.length + o] = t[o]

@[simp]

theorem SignSeq.length_append (s t : SignSeq) : (s ++ t).length = s.length + t.length