Surreals as Hahn series

Stream: combinatorial-games

[Aaron Liu]

I remember #maths > Real-closed Hahn series @ 💬

[Violeta Hernández]

Oh yeah of course I had asked this before

[Violeta Hernández]

I'll have to add Hahn series to my reading list.

[Violeta Hernández]

I first need to figure out how infinite sums of w^x are even defined.

[Aaron Liu]

The simplest number that has all the correct coefficients

[Violeta Hernández]

... How are the coefficients defined?

[Aaron Liu]

The next coefficient is the real part of the quotient of the difference between your number and its coefficients so far by the appropriate omega-power to make it the same archimedean class as one

[Aaron Liu]

I think

[Aaron Liu]

yeah that sounds about right

[Violeta Hernández]

Hm

[Violeta Hernández]

That sounds correct

[Violeta Hernández]

Would it be correct to say that the leading coefficient of x is w^e * r where e and r are the unique numbers with x / (w^e * r) ≈ 1?

[Aaron Liu]

In the sense that their difference is infinitesimal

[Violeta Hernández]

The quotient, rather than the difference

[Violeta Hernández]

The difference between w^-1 and w^-1 is infinitesimal, as is the difference between w^-1 and 2 * w^-1

[Aaron Liu]

no I mean the difference x / (w^e * r) - 1

[Violeta Hernández]

Oh yeah that's what I meant by the approx sign

[Violeta Hernández]

Same archimedean class

[Aaron Liu]

yeah I think that should be correct

[Aaron Liu]

I've pulled up ONAG so I can double check

[Violeta Hernández]

So that's the leading coefficient

[Aaron Liu]

yes

[Violeta Hernández]

It's pretty obvious how to calculate the nth coefficient for natural n

[Violeta Hernández]

But what about the wth coefficient?

[Aaron Liu]

the leading coefficient of the difference with the simplest number which agrees on all the finite coefficients

[Violeta Hernández]

Huh

[Violeta Hernández]

I think I get it

[Violeta Hernández]

But that sounds like a doozy to formalize

[Aaron Liu]

it's mutually recursive

[Aaron Liu]

you should be able to get that the numbers agreeing with a sequence of coefficients fall between two gaps generated by sets

[Violeta Hernández]

Wait I get it! You formalize the o-th coefficient and sums of length o at once, for o an ordinal, using recursion

[Violeta Hernández]

The o-th coefficient is the leading coefficient of the difference with the simplest number agreeing on all coefficients a < o

[Violeta Hernández]

Wait

[Violeta Hernández]

That's not even mutual recursion

[Violeta Hernández]

That's just recursion

[Aaron Liu]

well you've pulled the sum and the coefficients into one function so it's not mutual anymore

[Aaron Liu]

by the way, that's how the equation compiler handles mutual recursion

[Aaron Liu]

it creates an auxiliary function which does all of them at once

[Violeta Hernández]

Violeta Hernández said:

The o-th coefficient is the leading coefficient of the difference with the simplest number agreeing on all coefficients a < o

I like how you don't even need to use limit recursion

[Violeta Hernández]

Yet again proving my mantra of "you probably don't need limit recursion"

[Violeta Hernández]

I guess there is something I'm omitting - how do you know such a number agreeing on all the coefficients even exists?

[Aaron Liu]

the number the coefficients are coming from

[Aaron Liu]

you can show that the proper class of numbers agreeing with all the coefficients is the interval between two small cuts

[Aaron Liu]

uhm

[Aaron Liu]

I'll see what ONAG has to say about this

[Violeta Hernández]

...we're no longer talking about the summary file btw

[Violeta Hernández]

Do I have the power to move messages within this channel?

[Aaron Liu]

yes

[Aaron Liu]

you can't move them to a different channel though

[Notification Bot]

49 messages were moved here from #combinatorial-games > Summary file by Violeta Hernández.

[Violeta Hernández]

There goes

[Violeta Hernández]

Actually, how do you even prove that every positive surreal is commensurate to some ω^ x?

[Violeta Hernández]

oh nvm that's theorem 19 in ONAG

[Violeta Hernández]

should be simple enough to formalize

[Violeta Hernández]

It hasn't been simple to formalize

[Violeta Hernández]

But I'm getting there!

[Violeta Hernández]

I'm facing some slight annoyances with docs#ArchimedeanClass.mk, the most relevant of which being the length of the name. I'm not a fan of writing archimedeanClassMk all over our statements, and even though mk is much nicer it introduces ambiguity with docs#Surreal.mk.

[Aaron Liu]

what does using docs#ArchimedeanClass buy you?

[Violeta Hernández]

It's commensurability

[Aaron Liu]

there don't seem to be a plethora of lemmas about it

[Violeta Hernández]

We can expand the API as needed

[Aaron Liu]

sure I guess

[Violeta Hernández]

I was wondering if we could introduce notation, kind of how we did for lf. Specifically, write x ≪ y for ArchimedeanClass.mk y < ArchimedeanClass.mk x (the order on ArchimedeanClass is backwards for Hahn series reasons), and write something else for ArchimedeanClass.mk x = Archimedean class.mk y.

[Aaron Liu]

I was thinking just write the map from surreals to surreals which is the inverse of the omega map up to commeasurability

[Violeta Hernández]

Well the thing is that commensurability is precisely what ArchimedeanClass represents

[Violeta Hernández]

We could define a wlog map and prove that commensurable surreals have the same wlog

[Violeta Hernández]

But that would still be written down in terms of ArchimedeanClass

[Aaron Liu]

I guess yeah

[Violeta Hernández]

Well, what would the alternative be? Define our own Commensurable predicate with even less API? Or write down that whole thing about "there exists a natural number whose product is greater" every single time?

[Violeta Hernández]

In fact, there isn't really a canonical way to write down commensurability. You can use natural numbers in the definition, but you can also use positive rationals, or positive dyadic rationals, or positive reals.

[Violeta Hernández]

I'd argue that's more reason to use ArchimedeanClass, since we get a canonical way to write things down from which we can prove all the other equivalences.

[Aaron Liu]

no yeah that makes sense

[Aaron Liu]

the name is long though

[Violeta Hernández]

That's why I was asking about notation

[Violeta Hernández]

What do you think about using llt and commensurable on theorem names?

[Violeta Hernández]

For the < and = relations on ArchimedeanClass

[Violeta Hernández]

Just an idea, suggestions open

[Violeta Hernández]

Or we could use comm for the latter, surely there's no ambiguity with commutativity

[Violeta Hernández]

I mean, given that we already use lf and equiv even though there aren't any definitions with these names, I don't think it should be a problem.

[Aaron Liu]

yeah it's fine as long as you can justify those names

[Violeta Hernández]

llt -> much lesser than -> every finite multiple of x is lesser than y
comm -> commensurate

[Aaron Liu]

does that mean the other way is ggt

[Aaron Liu]

what if I want an le version

[Violeta Hernández]

Hmm yeah not sure how to name the le version

[Violeta Hernández]

lle might work but it would be really silly

[Violeta Hernández]

Though if we use the symbol ⪣ for it, it would make sense

[Aaron Liu]

U+2AA3 : DOUBLE NESTED LESS-THAN WITH UNDERBAR

[Aaron Liu]

that's new to me

[Aaron Liu]

it's an under bar and not just "or equal to"?

[Aaron Liu]

where do you get these unicode

[Violeta Hernández]

Shapecatcher is a great website

[Aaron Liu]

amazing

[Violeta Hernández]

This does beg the question, what notation should we use for commensurable elements?

[Violeta Hernández]

We could bring back ≡, it follows the "double symbol" theme and we aren't using it anymore thanks to the IGame refactor.

[Violeta Hernández]

These are my suggestions:
image.png

[Violeta Hernández]

Hmm, apparently there's a clash with ≡
image.png

[Violeta Hernández]

How come we never had this problem with PGame.Identical?

[Violeta Hernández]

I guess an alternative might be to just use ~, and make all of these notations scoped.

[Violeta Hernández]

I don't know. Maybe we don't even need notation.

[Violeta Hernández]

Having a hard time finding anything that simultaneously makes sense and works

[Violeta Hernández]

I think I'll just go notationless for now. Once I prove the math results I want we can think about how to make them look nice.

[Violeta Hernández]

Just filed #222

[Violeta Hernández]

I just realized something pretty substantial: the claim Surreal ≃+*o HahnSeries ℝ Surreal is false!

[Aaron Liu]

Violeta Hernández said:

I just realized something pretty substantial: the claim Surreal ≃+*o HahnSeries ℝ Surreal is false!

oh no what's wrong

[Violeta Hernández]

In fact, the embedding is strict. There are Hahn series that don't correspond to surreal numbers.

[Violeta Hernández]

As an example: X ^ (toSurreal o) summed over all ordinals o.

[Aaron Liu]

oh I think I get it

[Violeta Hernández]

Violeta Hernández said:

I just realized something pretty substantial: the claim Surreal ≃+*o HahnSeries ℝ Surreal is false!

This is one of those claims like "the cardinals are a complete lattice" which are only really true due to shenanigans with proper classes, i.e. are false in Lean

[Aaron Liu]

you need to take the "eventually zero" ones probably

[Violeta Hernández]

More precisely I think what we need is a type of Hahn series where the cardinality of the support is bounded

[Violeta Hernández]

As I understand it these satisfy basically all the same relevant algebraic properties when the cardinal is uncountable

[Violeta Hernández]

Then we'd have Surreal ≃+*o BoundedHahnSeries ℝ Surreal univ

[Aaron Liu]

Violeta Hernández said:

As I understand it these satisfy basically all the same relevant algebraic properties when the cardinal is uncountable

What are the relevant properties?

[Violeta Hernández]

Being a field, and being real-closed when the base field is real-closed and the value group is divisible.

[Violeta Hernández]

@Weiyi Wang What do you think about the BoundedHahnSeries idea? Is that something that would be difficult to incorporate into Mathlib?

[Weiyi Wang]

:sweat:I am not a maintainer and can't answer whether something can be in mathlib

[Weiyi Wang]

btw is it correct to say that this has the same intuition as card < 2^card? Since HahnSeries works like exponentiation

[Violeta Hernández]

Well, the question is moreso whether it'd be difficult to adapt results about Hahn series for this new type.

[Violeta Hernández]

Weiyi Wang said:

btw is it correct to say that this has the same intuition as card < 2^card? Since HahnSeries works like exponentiation

The inequality #Surreal < #(HahnSeries ℝ Surreal) is true, if that's what you're asking.

[Violeta Hernández]

Surreals have the cardinality of the ordinals, and every subset of ordinals corresponds to a Hahn series.

[Aaron Liu]

what's the proof that hahn series with algebraically closed base field and divisible exponents are algebraically closed?

[Violeta Hernández]

I think we could largely build BoundedHahnSeries on top of the existing HahnSeries API, without having to duplicate everything. If ℵ₀ < c, it should be relatively straightforward to prove that the support of the addition, multiplication, or inverse of any BoundedHahnSeries R Γ c retains the same property.

[Violeta Hernández]

So they're at the very least a field.

[Violeta Hernández]

Aaron Liu said:

what's the proof that hahn series with algebraically closed base field and divisible exponents are algebraically closed?

I don't know :frown:

[Aaron Liu]

could be make it a Subfield or an IntermediateField

[Violeta Hernández]

Oh, that's an even better idea

[Weiyi Wang]

Is the map Surreal →+*o HahnSeries ℝ Surreal canonical / constructive or you will need to use Hahn embedding theorem or such to show the existence non-constructively?

[Violeta Hernández]

It is canonical, it's the Conway normal form

[Violeta Hernández]

Though funnily enough its definition is very similar to the one you're using to prove the embedding theorem!

[Violeta Hernández]

Specifically, there exists a map ω ^ · : Surreal → Surreal such that the composition with ArchimedeanClass.mk is bijective on non-top Archimedean classes

[Violeta Hernández]

You can define ordinal-indexed sums of the form rᵢ * ω ^ xᵢ through transfinite induction

[Violeta Hernández]

And you basically get Hahn series verbatim out of this

[Violeta Hernández]

The construction is "canonical" in the sense that it relates to the representation of surreals as left and right sets of surreals, and isn't just an arbitrary chosen construction that's consequence of only the field structure

[Weiyi Wang]

Yep that's what I meant to ask. I was not familiar with Surreal numbers and was wondering whether its additional structure locks in a specific map

[Violeta Hernández]

In fact there's a very easy description of ω ^ x

[Violeta Hernández]

It's the simplest surreal in an archimedean class between ω ^ xᴸ and ω ^ xᴿ for all left/right options of x

[Weiyi Wang]

Aha, I think this matches my naive attempt to prove Hahn embedding theorem (before looking up a complete proof). My first idea was to do transfinite induction that peels away Archimedean classes layer by layer. This didn't work for arbitrary group because the set of Archimedean classes can be "too large" to do this. It looks like it is just at the right size for Surreals to do this

[Aaron Liu]

Weiyi Wang said:

because the set of Archimedean classes can be "too large" to do this. It looks like it is just at the right size for Surreals to do this

explain?

[Weiyi Wang]

Such as a group with uncountable Archimedean classes

[Aaron Liu]

I still don't get it

[Aaron Liu]

what do you mean "peels away" and what do you mean "too large"

[Aaron Liu]

the surreals have uncountably many archimedean classes

[Weiyi Wang]

hmm, uncountable isn't exactly the right word I was thinking...

[Weiyi Wang]

Let me just read more before I say random things :sweat_smile:

[Violeta Hernández]

The archimedean classes of the surreals are in bijection with the surreals

[Violeta Hernández]

That's basically what the ω-map shows

[Weiyi Wang]

Is ω^1 + ω^2 + ω^3... (summing over all natural numbers) a surreal number?

[Violeta Hernández]

(deleted)

[Violeta Hernández]

It's not

[Violeta Hernández]

And actually that leads to another subtlety I forgot about

[Violeta Hernández]

The exponents are actually given the opposite order

[Violeta Hernández]

For instance, ω^-1 + ω^-2 + ω^-3 + ... is a surreal number

[Violeta Hernández]

It's the simplest surreal number x in archimedean class -1, such that x - ω^-1 is in archimedean class -2, such that x - ω^-1 - ω^-2 is in Archimedean class -3, ...

[Weiyi Wang]

yeah I might have accidentally asked a trick question. Basically surreal numbers should always have a leading term with the largest exponent, and what I wrote didn't

[Weiyi Wang]

But what I wrote was a valid Hahn series, and that's the kind of the element in an arbitrary group/field that gave me headache (Wait I probably got the direction wrong)

[Violeta Hernández]

So the correct claim is that Surreal is isomorphic to the subring of Hahn series whose support has cardinal bounded by docs#Cardinal.univ, with base field ℝ and value group Surrealᵒᵖ

[Violeta Hernández]

Admittedly much uglier than the "surreals are Hahn series over themselves" soundbite

[Violeta Hernández]

Could I get a review on CGT#243? It advances a bit on this by defining Surreal.wlog and proving among other things that a numeric game not commensurate with its positive options is a power of ω.

[Violeta Hernández]

Violeta Hernández said:

The o-th coefficient is the leading coefficient of the difference with the simplest number agreeing on all coefficients a < o

Wait a sec, how do we know this simplest number exists?

[Aaron Liu]

Violeta Hernández said:

Violeta Hernández said:

The o-th coefficient is the leading coefficient of the difference with the simplest number agreeing on all coefficients a < o

Wait a sec, how do we know this simplest number exists?

(you asked this already btw) I took a look at ONAG and Conway just skips over that part

[Aaron Liu]

probably you can construct it as the simplest surreal lying between two sets

[Aaron Liu]

yeah isn't this pretty easy

[Aaron Liu]

just construct the set of smaller and larger series and find it in between

[Aaron Liu]

this doesn't work when the cofinality of the limit ordinal you're building up to is greater than the size of your universe

[Aaron Liu]

but that's probably fine

[Violeta Hernández]

I asked in gamesters

[Violeta Hernández]

turns out this is yet another case of "Siegel has all the details"

[Aaron Liu]

what's gamesters

[Violeta Hernández]

a discord server I share with Aaron Siegel

[Aaron Liu]

oh ok

[Aaron Liu]

so I don't think this one is complicated

[Aaron Liu]

you just take a cut

[Aaron Liu]

and then the surreal you get must have the properties simply by how it's ordered

[Aaron Liu]

and it must be the simplest one also by looking at the order

[Violeta Hernández]

Sorry I don't get what you mean by this

[Aaron Liu]

ok maybe if we had an example

[Aaron Liu]

do you have an example I can use

[Violeta Hernández]

alternating sum of w^-n?

[Aaron Liu]

so we want 1-w^-1+w^-2-...

[Aaron Liu]

and assume we have all the finite series

[Aaron Liu]

then for each a_i a Nat-indexed sequence of real numbers consider a_0+a_1w^-1+a_2w^-2+...

[Aaron Liu]

the set of all such sequences is not a proper class

[Aaron Liu]

consider the subset which are lexographically earlier than the alternating sequence of 1 and -1

[Aaron Liu]

and the subset which are lexographically later

[Aaron Liu]

then we can form the simplest surreal between these sets

[Aaron Liu]

and I claim this is the one we want

[Aaron Liu]

ok wait we need to truncate these

[Aaron Liu]

uhm

[Aaron Liu]

for each n you consider the set of all Fin n-indexed sequences of reals

[Aaron Liu]

we have defined earlier by induction hypothesis the surreal a_0+a_1w^-1+a_2w^-2+...

[Aaron Liu]

since it's Fin n-indexed these are finitely long

[Aaron Liu]

then we can partition them and then take the union over all n

[Aaron Liu]

that should work

[Aaron Liu]

would it be better to see some Lean code

[Aaron Liu]

do I need to be more rigorous

[Aaron Liu]

ok by the induction hypothesis for each n : Nat and a : Fin n → Real we have defined the surreal number a 0 + a 1 * w^-1 + ... + a (n-1) * w^-(n-1) (it's a finite sum)
each sequence a : Fin n → Real can be extended to a sequence Nat → Real by setting the tail to zero
then this extension is either lexographically earlier or later than the sequence k ↦ (-1)^k
partition the sequences into the earlier ones l : (n : Nat) → Set (Fin n → Real) and the later ones r : (n : Nat) → Set (Fin n → Real)
set li : (n : Nat) → Set Surreal to be the image of l under this finite sum function in the induction hypothesis, and define ri : (n : Nat) → Set Surreal similarly
set L = ⋃ n, li n and R = ⋃ n, ri n, it is easily checked that these are small sets and that each element of L is smaller than each element of R
then we can form the surreal {L | R}ˢ and it has all the properties we want

[Aaron Liu]

ok I think that should be sufficiently explain what I mean

[Violeta Hernández]

This is what Siegel told me btwScreenshot_2025-09-20-16-51-30-788_com.discord-edit.jpg

[Aaron Liu]

that sounds like what I said

[Aaron Liu]

that's good

[Aaron Liu]

so I think this time we have to use limit recursion

[Aaron Liu]

distinguish the limit ordinal case from the other cases

[Violeta Hernández]

Yeah

[Violeta Hernández]

I think you're right

[Violeta Hernández]

Just opened #32648 which shows that for any uncountable cardinal c, the set of Hahn series with length < c forms a subfield

[Violeta Hernández]

In the notation of that PR, we have Surreal ≃+*o cardLTSubfield Surrealᵒᵈ ℝ univ

[Violeta Hernández]

Gonna start work on defining the map from Hahn series to surreals and back

[Violeta Hernández]

Ugh. Turns out I can't get very far without both #32648 and #29687.

[Violeta Hernández]

Started work on the type of surreal Hahn series over at this branch. There was a somewhat surprising amount of machinery I had to add for indexing the support by an ordinal.

[Violeta Hernández]

Unfortunately there's a few major sorries that I can't fill out until the aforementioned PRs are merged

[Violeta Hernández]

Ok wow 500 lines of code down and I still can't even define the map from Hahn series into games

[Violeta Hernández]

Guess I'll continue tomorrow

[Violeta Hernández]

There's a lot of, how to put it? Annoyances

[Violeta Hernández]

The fact that we have well-founded > rather than <, the fact that we have to work with subtypes everywhere, the fact that surreals bump up the universe by one

[Violeta Hernández]

obviously none of these are some foundational issue, but they all make setting our API up quite more tedious

[Violeta Hernández]

Just finished a sorry-free (modulo open PRs) definition of the map SurrealHahnSeries → IGame. Only took 700 lines of code.

[Violeta Hernández]

I'm temporarily putting everything on CGT#263, will split up that material as I'm able

[Violeta Hernández]

@Aaron Liu I'm having trouble filling out some sorries

[Violeta Hernández]

Specifically I haven't been able to show that this map is strictly monotone and that it takes on numeric values

[Violeta Hernández]

It's really annoying that the definition of this embedding uses limit recursion and not just recursion

[Violeta Hernández]

I was able to make things easier by noticing the zero and limit case could be merged, but even then

[Violeta Hernández]

To make matters worse I don't believe this proof is in Siegel or Conway

[Aaron Liu]

sure I'll take a look

[Violeta Hernández]

To be explicit this is what I want to prove:

proof_wanted strictMono_toIGame : StrictMono SurrealHahnSeries.toIGame
proof_wanted numeric_toIGame : ∀ x, Numeric (SurrealHahnSeries.toIGame x)

[Violeta Hernández]

I suspect the proofs hinge on this lemma that Siegel mentions on page 427
image.png

[Violeta Hernández]

Σ_α is the α-th partial sum of a Hahn series

[Violeta Hernández]

I've no idea how to show this in the case where α is a successor

[Violeta Hernández]

I found this notation on a paperScreenshot_2025-12-18-05-28-42-784_org.mozilla.firefox-edit.jpg

[Violeta Hernández]

What do you think? I'd really like to avoid having to write down ArchimedeanClass.mk x < ArchimedeanClass.mk y all over.

[Aaron Liu]

well if it's scoped notation I don't see a problem

[Violeta Hernández]

awesome

[Aaron Liu]

but I think one of those is already taken (docs#HEq)

[Violeta Hernández]

oh :frown:

[Violeta Hernández]

so close

[Violeta Hernández]

would you be opposed to just coming up with some ad-hoc notation? Like perhaps x <_a y

[Violeta Hernández]

Basically I'm trying to avoid writing down ArchimedeanClass.mk all over the place, as well as the cognitive load from the order being opposite to the expected one

[Aaron Liu]

if it's just notation you aren't making any nothing-definitions for the notation then I'm fine with it

[Violeta Hernández]

Awesome

[Violeta Hernández]

CGT#276

[Weiyi Wang]

You can use the notation for ValuativeRel a <_v b. Unfortunately it flips the direction from Archimedean class, but it is in the same direction as this paper

[Violeta Hernández]

Oh, awesome! Let me try to implement that

[Violeta Hernández]

I take it that rel is the recommended spelling for ≤ᵥ, and that srel is the recommended spelling for <ᵥ

[Violeta Hernández]

Is there any notation for =ᵥ?

[Violeta Hernández]

...seems like =ᵥ doesn't exist. Should we add it?

[Violeta Hernández]

Specifically, I'd like to define x =ᵥ y as AntisymmRel (· ≤ᵥ ·) x y

[Violeta Hernández]

In surreals, this would be the commensurancy relation

[Violeta Hernández]

Actually, does it make sense to make a new def for AntisymmRel Rel? How would we even call it? Or should we just define =ᵥ as notation?

[Violeta Hernández]

I see the issue that if we don't give a name to this, then we end up with very different names for basically analogous theorems. For instance, x * z ≤ᵥ y * z ↔ x ≤ᵥ y is mul_rel_mul_iff_left, whereas x * z =ᵥ y * z ↔ x =ᵥ y would have to be something much clunkier like antisymmRel_rel_mul_iff_antisymmRel_rel_left

[Weiyi Wang]

I am surprised they aren't named vle, vlt and veq

[Violeta Hernández]

Yeah, I like these names much better. @Aaron Liu @Adam Topaz what do you think?

[Violeta Hernández]

I've opened #33040 in case we want to make this rename.