Game product cannot be lifted

Stream: maths

[Violeta Hernández]

A common theme throughout the combinatorial game library in Lean is that although we can define products on pre-games, we can't do so on games, since the operation can't be lifted. But do we have an actual counterexample?

[Violeta Hernández]

I think this would make for a nice file in the Counterexamples folder

[Violeta Hernández]

I don't know of any myself

[Violeta Hernández]

Just found this: https://math.stackexchange.com/a/2922745/718671

[Eric Wieser]

Watch out, I spent over a year trying to formalize a counterexample from Math.SE! Maybe this one is easier :)

[Violeta Hernández]

The game

$$K = \ast + \{-1, 0|0, 1\}$$

apparently satisfies K ≈ 0 but K² ≉ 0

[Violeta Hernández]

This counterexample was built to satisfy the additional constraint of being equivalent to a number, though

[Violeta Hernández]

So there might exist something simpler

[Violeta Hernández]

That being said this is a pretty simple game already

[Violeta Hernández]

...I think I found a mistake

[Violeta Hernández]

Let G = {0 | 0}, H = {-1, 0 | 0, 1}. For GH ≈ 0, each left move of it must be ⧏ than 0, but the moves 0 * H + G * 0 + 0 * 0 are not.

[Violeta Hernández]

I did prove K ≈ 0, so there's a chance the result still works

[Violeta Hernández]

Oh wait I think this can be salvaged

[Violeta Hernández]

G ≈ H but GG ≉ GH

[Violeta Hernández]

#15764