Cooling

Stream: combinatorial-games

[Jelmer Firet]

I have been talking with @Violeta Hernández a bit about left and right stops. We came to the conclusion that they already exist as Surreal.Cut.leftGame and Surreal.Cut.rightGame

I have been thinking a bit about how to implement cooling.

Define
leftWall (G : IGame) : (t : Surreal) → Cut
rightWall (G : IGame) : (t : Surreal) → Cut
recursively

We need two helper functions
collideLeft (lw : Surreal → Cut) (rw : Surreal → Cut) : Surreal → Cut
collideRight (lw : Surreal → Cut) (rw : Surreal → Cut) : Surreal → Cut
With the semantics that if T is the smallest t such that lw t ≤ rw t then
collideLeft lw rw t = lw t if t < T
collideLeft lw rw t = lw T if t ≥ T
collideRight lw rw t = rw t if t < T
collideRight lw rw t = rw T if t ≥ T

Then for Surreal x we have
leftWall x.toGame = collideLeft (fun t ↦ x.leftSurreal - t ) (fun t ↦ x.rightSurreal + t)
rightWall x.toGame = collideRight (fun t ↦ x.leftSurreal - t) (fun t ↦ x.rightSurreal + t)

And for the other games !{Gᴸ|Gᴿ} we have
leftWall G = collideLeft (fun t ↦ ⨆ gl ∈ Gᴸ, rightWall gl t - t) (fun t ↦ ⨅ gr ∈ Gᴿ, leftWall gr t + t)
rightWall G = collideRight (fun t ↦ ⨆ gl ∈ Gᴸ, rightWall gl t - t) (fun t ↦ ⨅ gr ∈ Gᴿ, leftWall gr t + t)

We can then define

cool (G : IGame) (t : Surreal) : IGame
where when leftWall G t < rightWall G t we have
cool G t = simplestBtwn (leftWall G t) (rightWall G t)
and otherwise
cool G t = !{(fun Gl ↦ cool Gl t - t) '' Gᴸ | (fun Gr ↦ cool Gr t + t) '' Gᴿ}

This is the just-after definition.

Note:
Addition between a Surreal and a Cut can be defined, but between two Cut's this runs into issues
In particular, should x.leftSurreal + y.rightSurreal contain x+y in its left or right set?
By defining temperature as a Surreal I sidestep this issue.

[Violeta Hernández]

This seems to mostly make sense, though how would you know that such a smallest t does exist?

[Violeta Hernández]

I'm unclear on whether you need a short hypothesis for that. I don't know very much about this specific game-theoretic construction.

[Jelmer Firet]

Siegel uses the intermediate value theorem for that.
The left and right wall are (piecewise linear) continuous functions.
They have an infinite mast on top, so there exists a T such that for all t >= T leftWall G t = leftWall G T
If we then take leftWall G t - t this heads off to -infinity, and similarly rightWall G t + t heads off to infinity.
By intermediate value theorem they must intersect somewhere.

[Violeta Hernández]

IVT for piecewise linear functions should work over any ordered field.

[Violeta Hernández]

This all looks good to me. Would you like to start work on a PR?

[Jelmer Firet]

Sure, but not before the weekend

[Jelmer Firet]

Have an exam on friday

[Violeta Hernández]

Good luck with that

[Violeta Hernández]

I've got a mostly unrelated question but one which would still affect your work. Should we rename CGT#Surreal.Cut.simplestBtwn to Surreal.ofCuts? With analogy to CGT#OfSets.

[Jelmer Firet]

Question back:
is simplestBtwn x y = !{x.left | y.right}?

[Violeta Hernández]

Morally yes, technically no.

[Jelmer Firet]

probably because we don't want proper classes in there, and x.left and y.right would be a proper class?

[Jelmer Firet]

I am fine with renaming it ofCuts, but do mention the "simplest between" understanding in the doccomment

[Violeta Hernández]

OfSets only allows you to build a surreal out of two small sets of surreals. But we can prove after the fact that actually, every order connected non-empty set of surreals has a unique surreal with least birthday (see CGT#298), and that's what simplestBtwn represents.

[Violeta Hernández]

Thinking about this further, I'm less convinced that this works. Suppose that your left and right walls are -∞ and ∞, where ∞ is the supremum of the natural numbers (as either left or right cuts). Then there is no single least surreal with ∞ - t ≤ -∞ + t, since any t < ∞ won't work, but any t > ∞ will.

[Violeta Hernández]

You likely need the condition that your cuts are numeric, which you can only reliably guarantee when the game is short.

[Jelmer Firet]

It is probably good to focus on short games first, since the theory seems well-developed for that. And after that see if it extends to long games

[Violeta Hernández]

Yes, that'd make sense.