Birthday of ω^x

Stream: combinatorial-games

[Violeta Hernández]

I've been thinking a lot about surreal birthdays lately. I have the vague hope that there could be some way to compute the birthday of a surreal from its Hahn series expansion. If there were, we could potentially find a proof (or disproof), even if a horrible one, of conjectures such as b(xy) ≤ b(x)b(y).

Obviously the first step of this would be to find a formula for b(ω^x). As far as I'm aware, the "state of the art" are the following theorems, from Field of Surreal numbers and Exponentiation by van den Dries and Ehrlich (2001):
imagen.png

[Violeta Hernández]

I believe I have a proof of b(ω^-α) = ωα for α an ordinal, so there's at least more to be said about this function than what's contained in these theorems.

[Violeta Hernández]

Seems like the proofs of all of these are just deferred to Gonshor, so I'll have to check that source.

[Violeta Hernández]

imagen.png
imagen.png
Oh wait so apparently this is all a known result apparently

[Violeta Hernández]

imagen.png
Proof by "Conway said he had it but he didn't"

[Kevin Buzzard]

I'm not sure there's a tactic for that :-/

[Jelmer Firet]

macro "by_conway" : tactic => `(tactic| sorry)

[Scott Fenton]

The multiplication inequality is actually proven here: https://www.impan.pl/pl/wydawnictwa/czasopisma-i-serie-wydawnicze/fundamenta-mathematicae/all/all/167/2/89226/fields-of-surreal-numbers-and-exponentiation

[Violeta Hernández]

I've read that paper, it only proves it for the specific case of surreals of the form rw^x.