Birthday of game product

Stream: maths

[Violeta Hernández]

In #15716 I prove that

theorem birthday_add_le (x y : Game) : (x + y).birthday ≤ x.birthday ♯ y.birthday := sorry

where ♯ is natural addition. I'm wondering if there's any analogous version for multiplication, namely

theorem birthday_mul_le (x y : Surreal) : (x * y).birthday ≤ x.birthday ⨳ y.birthday := sorry

where ⨳ is natural multiplication, but I'm coming up blank. I haven't been able to find a reference, nor to prove this myself.

[Violeta Hernández]

This result is important since it allows proving the subset of games with birthday less than ω^ω^o forms a ring.

[Violeta Hernández]

(at least, if I'm correct about it)

[Violeta Hernández]

The problem is that a priori, the games xᴸy + xyᴸ – xᴸyᴸ, etc. seem like they should have a birthday at least thrice that of xᴸyᴸ. In fact, for the pre-game birthday, this is the case, which makes that version of the theorem false.

[Violeta Hernández]

This is an open problem :sob:
https://mathoverflow.net/a/476829/147705

[Mario Carneiro]

Is the weaker result in the edit ((x * y).birthday <= omega ⨳ x.birthday ⨳ x.birthday ⨳ y.birthday ⨳ y.birthday) sufficient to prove your theorem about games up to ω^ω^o forming a ring?

[Violeta Hernández]

It is, and that's actually what they do in the paper

[Violeta Hernández]

It requires expanding the surreals into a "Conway form" though, so it's going to be a while until we get there

[Kim Morrison]

Some nice synergy between Mathlib and Mathoverflow there. :heart: