Surreals with finite birthdays

Stream: combinatorial-games

[Scott Fenton]

I found an interesting proof that might be useful for showing Surreal.Dyadic.toDyadic constructively. The key lemma is theorem 25 at Mizar's SURREALN (https://mizar.uwb.edu.pl/version/current/html/surrealn.html). It involves a lot of case splitting but otherwise gives a direct birthday.

[Violeta Hernández]

I can't really read this at all... what does it say?

[Violeta Hernández]

I did have an idea as to how to do this. Every finite set is either empty or has a maximum, so you really only need to consider four cases.

• {∅ | ∅}: the dyadic is 0
• {a | ∅}: the dyadic is an ordinal, so either 0 (if a < 0) or floor (a + 1) otherwise
• {∅ | a}: the dyadic is the negative of an ordinal, this is just the negative of the previous case
• {a | b}: if an integer fits, the dyadic is whichever one has the least absolute value. Otherwise, let n be smallest such that m/2^n fits. Then the dyadic is m/2^n.

[Violeta Hernández]

This of course requires us to first prove the birthday formula for dyadics, which is tedious but not difficult.

[Aaron Liu]

Violeta Hernández said:

This of course requires us to first prove the birthday formula for dyadics, which is tedious but not difficult.

I don't think we have to do that

[Aaron Liu]

it's pretty obvious in each case that no option fits

[Violeta Hernández]

oh, you're right

[Violeta Hernández]

Also, I'm pretty sure we already have "game with no right/left options is an ordinal/negative ordinal" somewhere

[Aaron Liu]

CGT#309

[Aaron Liu]

the statement doesn't specify which ordinal though :(

[Violeta Hernández]

the proof does

[Violeta Hernández]

though I should probably have written it with sInf instead of with WellFounded.min