Hessenberg operations

Stream: combinatorial-games

[Violeta Hernández]

There's some work regarding Hessenberg (natural) operations on ordinals that I never was able to get into Mathlib. I'm wondering if it might be worth putting it in this repo instead.

[Violeta Hernández]

The main results I'm interested in are:

• w^x # w^y = w^x + w^y for y < x
• w^(x # y) = w^x ⨳ w^y

[Violeta Hernández]

These essentially formalize the concept that natural addition is equivalent to adding up Cantor Normal Forms term by term, and that natural multiplication is equivalent to multiplying Cantor Normal Forms as polynomials.

[Violeta Hernández]

I do have somewhat of a general design question. Should we be defining natural operations as belonging in Ordinal, or do we keep them to NatOrdinal?

[Violeta Hernández]

I think the latter should be better. It does require us to use more casts to write down results, but in return we don't have to transfer all of the order/ring theorems fromNatOrdinal back to Ordinal

[Violeta Hernández]

We have about 150 boilerplate lines of code to set up the type aliases docs#NatOrdinal and docs#Nimber, which are basically identical save for replacing the word NatOrdinal with Nimber.

[Violeta Hernández]

Would it be feasible/make sense/be nice to turn these into a single macro, and put it in some other file?

[Violeta Hernández]

It'd be nice if we could simply write #ordinal_alias NatOrdinal or whatnot and be done with that.

[Violeta Hernández]

If nothing else it'd keep those two aliases in sync

[Violeta Hernández]

Actually, what do you think about renaming Ordinal.toNatOrdinal → NatOrdinal.of and NatOrdinal.toOrdinal → NatOrdinal.val?

[Violeta Hernández]

Not only does it make writing the macro much easier, but it also should make a lot of theorem names much shorter.

[Violeta Hernández]

#186 for the rename and #188 for the macro

[Violeta Hernández]

Ok I have a more mathematical question now

[Violeta Hernández]

As I mentioned earlier, base w exponentiation interacts nicely with natural operations, as you have w^(x # y) = w^x ⨳ w^y

[Violeta Hernández]

In fact this identity still holds if you replace w by any finite ordinal, or by any additively principal ordinal.

[Violeta Hernández]

But it doesn't work in general, as e.g. (w + 1)^(1 # 1) = w^2 + w + 1 ≠ w^2 + w * 2 + 1 = (w + 1) ⨳ (w + 1).

[Violeta Hernández]

Which means that we can't really define exponentiation on NatOrdinal as just exponentiation on Ordinal and expect it to work

[Violeta Hernández]

Now, here's my idea

[Violeta Hernández]

What if we defined exponentiation on NatOrdinal through transfinite recursion?

[Violeta Hernández]

Specifically, x^0 = 1, x^(y + 1) = x^y ⨳ x, and for limit ordinals, take limits

[Aaron Liu]

I think if you do that you just get regular ordinal exponentiation

[Violeta Hernández]

Nope

[Violeta Hernández]

The (w + 1)^2 example is different

[Aaron Liu]

oh wait you're using the natural product

[Violeta Hernández]

Yeah

[Aaron Liu]

yeah that's different

[Violeta Hernández]

This natural exponentiation should be the same as ordinal exponentiation for finite bases and base w

[Violeta Hernández]

My conjecture is that this exponentiation satisfies x^(y # z) = x^y ⨳ x^z always

[Aaron Liu]

so here's my thoughts

[Junyan Xu]

image.png
image.png
Has this paper https://arxiv.org/abs/1501.05747 been discussed before?

[Junyan Xu]

maybe you've defined the super-Jacobsthal exponentiation?

[Violeta Hernández]

Oh yeah Theorem 3.2 is exactly what I wanted

[Aaron Liu]

regular addition x + y is the order type of x ⊕ₗ y (lexographic order)
natural addition x # y can be defined as the largest ordinal admitting a monotone surjection from x ⊕ y (disjoint union order)

regular multiplication x * y is the order type of y ×ₗ x (lexographic order)
natural multiplication x ⨳ y can be defined as the largest ordinal admitting a monotone surjection from y × x (pointwise order)

regular exponentiation x ^ y is the order type of Lex (y →₀ x) (lexographic order)

what properties does "the largest ordinal admitting a monotone surjection from y →₀ x (pointwise order)" satisfy?

[Aaron Liu]

is this one of the operations in that table shown above?

[Violeta Hernández]

Actually x * y is the order type of y × x because Cantor really wanted normality on the right argument

[Aaron Liu]

oh whoops

[Aaron Liu]

yeah that tracks

[Violeta Hernández]

This is a great question though

[Violeta Hernández]

Since 2 -> x with the pointwise order is order isomorphic to x × x with the pointwise order, this agrees with the natural product

[Aaron Liu]

does this only depend on the cardinality of y?

[Aaron Liu]

I think you can permute y however you want

[Aaron Liu]

I guess this is actually taking an ordinal to a cardinal power, since the order type of y doesn't actually matter

[Aaron Liu]

hmmmm

[Aaron Liu]

the coproduct in the category of preorders is the disjoint sum
the product in the category of preorders is the pointwise cartesian product
maybe what we actually want here is the internal hom in the category of preorders???

[Aaron Liu]

that would be the monotone functions y →o x, with the pointwise order

[Aaron Liu]

and then take the largest ordinal admitting a monotone surjection

[Aaron Liu]

this gives you an order which actually depends on the order in y

[Violeta Hernández]

Hi sorry I'm back

[Aaron Liu]

welcome back

[Violeta Hernández]

Yeah you're right this is a cardinal exponentiation

[Violeta Hernández]

Restricting to monotone functions wouldn't work

[Violeta Hernández]

Or rather you'd get something where m^n isn't even equal to natural number exponentiation for finite m, n

[Aaron Liu]

so do we just use super-jacobsthal exponentiation?

[Violeta Hernández]

I think it's by far the best choice

[Violeta Hernández]

We can then prove

• a^(b + c) = a^b * a^c
• of (w^a) = (of w)^a
• of (w^a) + of (w^b) = of (w^a + w^b) for b ≤ a

[Violeta Hernández]

These three results combined prove that natural addition/multiplication is indeed the sum and product of CNFs as polynomials

[Violeta Hernández]

(though it's probably more of a chore to prove and use that result verbatim than to just use these results instead)

[Violeta Hernández]

I have a proof of the third bullet point in an old Mathlib branch. I could revive it.

[Violeta Hernández]

I don't know proofs for 1 and 2, but I imagine they're a "follow your gut" argument

[Violeta Hernández]

Oh yeah, 1 is pretty easy. If c is a successor, then a^(b + c + 1) = a^(b + c) * a = a^b * a^(c + 1) by induction. Likewise for b. So suppose both are limits.

[Violeta Hernández]

Then you can prove that every ordinal less than a^(b + c) is less than a^b * a^c, and viceversa.

[Violeta Hernández]

Specifically, if x < a^(b + c), then x < a^(b' + c) for some b' < b, meaning x < a^b' * a^c < a^b * a^c, or analogously with c.

[Violeta Hernández]

And if x < a^b * a^c, then x + y * z < a^b * y + a^c * z for some y < a^b and c < a^z, meaning x < a^b' * a^c + a^b * a^c' for some b' < b, c' < c, and thus x < a^(max (b' + c) (b + c') + 1) < a^(b + c).

[Violeta Hernández]

I recently tried to define super-jacobsthal exponentiation. I was able to prove that a^(b + c) = a^b * a^c. But generally this just wasn't very useful in proving results about w^x.

[Violeta Hernández]

There isn't really any application of this exponentiatial to game theory (it doesn't even match surreal exponentiation). So I'm split on whether we could formalize it for its own sake, or whether it's better to just not.

[Violeta Hernández]

Leaning towards the latter, because there's a lot of these intermediate operations on ordinals and they just aren't relevant to what we're doing

[Aaron Liu]

Violeta Hernández said:

There isn't really any application of this exponentiatial to game theory (it doesn't even match surreal exponentiation).

What is surreal exponentiation?

[Violeta Hernández]

exp(a * ln(b))

[Violeta Hernández]

Where the exponential is Gonshor's exponential and the logarithm is its inverse

[Violeta Hernández]

Actually, here's an idea

[Violeta Hernández]

What if we overload the ω^ notation for NatOrdinal?

[Violeta Hernández]

That's probably the easiest way to talk about ω-exponentiation in NatOrdinal

[Violeta Hernández]

That way we don't have to constantly write of (ω ^ x.val), nor do we have to define any other kinds of exponentiation

[Aaron Liu]

which exponential is this

[Violeta Hernández]

My proposal is doing the following:

noncomputable instance : Wpow NatOrdinal where
  wpow x := of (ω ^ x.val)

[Violeta Hernández]

Where Wpow is our custom notation typeclass that we currently use on IGame and Surreal

[Aaron Liu]

this is copying exponentiation from Ordinal (but only with base ω)?

[Violeta Hernández]

Yes

[Violeta Hernández]

ω-exponentation on NatOrdinal is much better behaved than exponentiation in general

[Violeta Hernández]

So I think it's fine to special-case it

[Aaron Liu]

what's the use case for this

[Violeta Hernández]

Proving the characterization of natural operations

[Violeta Hernández]

Natural addition is adding the base-ω Cantor normal forms, natural multiplication is multiplying them as polynomials

[Violeta Hernández]

I don't think we need to prove these results verbatim

[Violeta Hernández]

The same way I don't think we need to prove "nimber addition is XORing the base 2 CNFs"

[Violeta Hernández]

But we should prove the results that lead to this

[Violeta Hernández]

Which are:

• a ≤ b → ω^ b * n + ω^ a = of (ω ^ b.val * n + ω ^ a.val)
• ω^ (a + b) = ω^ a * ω^ b

[Violeta Hernández]

The first of these is actually needed to prove ω-exponentiation on Surreal matches that of NatOrdinal

[Aaron Liu]

seems fine enough

[Aaron Liu]

I don't disapprove

[Violeta Hernández]

#240

[Violeta Hernández]

I prove both of these results, and use them to show the ω-map on NatOrdinal coincides with that of Surreal

[Kevin Buzzard]

Violeta Hernández said:

#240

Do you not have a fancy linky thing like FLT#123 ? You should ask for one! Decide on what string you want before the # and my guess is that someone will sort it out.

[Aaron Liu]

vihdzp/combinatorial-games#240

[Aaron Liu]

It works

[Violeta Hernández]

Can we get a custom CGT#123 string? Much easier to write down.

[Aaron Liu]

that would definitely be better

[Kevin Buzzard]

Violeta Hernández said:

Can we get a custom CGT#123 string? Much easier to write down.

My guess is "yes but you have to ping the right person and this person is almost certainly not subscribed to this channel". Try asking in #general or something?

[Violeta Hernández]

CGT#240

[Violeta Hernández]

It works!

[Violeta Hernández]

(deleted)

[Violeta Hernández]

CGT#Nimber

[Violeta Hernández]

There we go