Documentation

Counterexamples.GameMultiplication

Multiplication of pre-games can't be lifted to the quotient #

We show that there exist equivalent pregames x₁ ≈ x₂ and y such that x₁ * y ≉ x₂ * y. In particular, we cannot define the multiplication of games in general.

The specific counterexample we use is x₁ = y = {0 | 0} and x₂ = {-1, 0 | 0, 1}. The first game is colloquially known as star, so we use the name star' for the second. We prove that star ≈ star' and star * star ≈ star, but star' * star ≉ star.

source
def Counterexample.PGame.star' :
SetTheory.PGame

The game {-1, 0 | 0, 1}, which is equivalent but not identical to *.

Equations
Instances For
    source
    theorem Counterexample.PGame.neg_star' :
    -star' = star'

    *' is its own negative.

    source
    theorem Counterexample.PGame.star'_equiv_star :
    star' ≈ SetTheory.PGame.star

    *' is equivalent to *.

    source
    theorem Counterexample.PGame.star_sq :
    SetTheory.PGame.star * SetTheory.PGame.star ≈ SetTheory.PGame.star

    The equation ** = * is an identity, though not a relabelling.

    source
    theorem Counterexample.PGame.star'_mul_star_lf :
    (star' * SetTheory.PGame.star).LF SetTheory.PGame.star

    *'* ⧏ * implies *'* ≉ *.

    source
    theorem Counterexample.PGame.mul_not_lift :
    ∃ (x₁ : SetTheory.PGame) (x₂ : SetTheory.PGame) (y : SetTheory.PGame), x₁ ≈ x₂ ∧ ¬x₁ * y ≈ x₂ * y

    Pre-game multiplication cannot be lifted to games.