Summary file

Stream: combinatorial-games

[Violeta Hernández]

Martin Dvořák said:

I suggest that every project should have a "summary" in the sink file (the file that is usually named the same as the project, lies in the root folder, and imports all other .lean files) that recalls the main results and all nontrivial definitions they depend on (dependencies of the statements, not the proofs). It is very little extra work and a huge advantage for visitors!

[Violeta Hernández]

What do you think about this? What would such a file for the CGT repo contain?

[Aaron Liu]

Yaël Dillies said:

Martin Dvořák said:

I suggest that every project should have a "summary" in the sink file (the file that is usually named the same as the project, lies in the root folder, and imports all other .lean files) that recalls the main results and all nontrivial definitions they depend on (dependencies of the statements, not the proofs). It is very little extra work

It is in fact a lot of (continuous) extra work because those recall commands would get wiped out every time I run lake exe mk_all to update that file. This happens > 20 times a week

[Violeta Hernández]

Oh :frown:

[Aaron Liu]

we can still have a summary file, just don't make it be the file that imports everything

[Violeta Hernández]

I like that idea.

[Violeta Hernández]

I think the most important result we have so far is that surreal numbers form a field

[Violeta Hernández]

There's two other results I'd like to have in this recall file:

• nimbers are algebraically closed
• short games have a unique canonical form

But we have neither of those yet.

[Aaron Liu]

how to prove nimbers are algebraically closed?

[Violeta Hernández]

It's a consequence of the simplest extension theorems I've been proving

[Aaron Liu]

oh that's what that was about

[Violeta Hernández]

If x is a nimber that's a field but not algebraically closed, then x is the root of a polynomial in x, namely, the lexicographically smallest non-constant polynomial without a root in x.

[Violeta Hernández]

(that's the fourth theorem we're currently missing)

[Violeta Hernández]

After that, it's a proof by contradiction. Suppose some non-constant polynomial p in the nimbers has no roots. Take a nimber x large enough so that x is a field that contains roots for every non-constant polynomial with coefficients in x lexicographically smaller than p - this exists by a closure argument. Then x is a root of p, contradiction.

[Aaron Liu]

this seems like just a regular argument, which is not by contradiction

[Violeta Hernández]

Oh yeah you're right

[Aaron Liu]

you are given a polynomial, and you find a root

[Violeta Hernández]

It's just an inductive argument

[Violeta Hernández]

Force of habit

[Violeta Hernández]

Something else that's important and that we need to prove: surreals are a real closed field

[Violeta Hernández]

That one I think is really an argument about Hahn series. I hear other people are working on that.

[Aaron Liu]

do we have a definition of real-closed field?

[Violeta Hernández]

No idea.