Ordinal arithmetic via CNF

Stream: maths

[Eric Vergo]

Hey all, 

I’m a student relatively early in my math education and decided to go ‘all in’ on interactive theorem provers. @Alex Kontorovich has been getting me up to speed on Lean this summer, and I was hoping to formalize some results about ordinal numbers using the Cantor normal form. Unfortunately, the vast majority of the tooling needed to do so doesn’t exist, so I’ll have to make it first.

It’s not lost on me that that is a big effort, but it looks like there are a few smaller tasks that I may be able to break off and tackle. To start, I was hoping to get some guidance/instruction on how to best implement ordinal arithmetic listed in the “to do” items here. As it stands I have a decent handle on the math, but lack the knowledge about how to write code/API’s that integrate well into the existing environment.

[Alex Kontorovich]

Maybe team up with @Violeta Hernández? https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.2315915.20Cantor.20Normal.20Form/near/463098320

[Eric Vergo]

Y'all move fast! closing this toping and will join in on the other threads.

[Notification Bot]

Eric Vergo has marked this topic as resolved.

[Notification Bot]

Violeta Hernández has marked this topic as unresolved.

[Violeta Hernández]

I'm having some trouble and I wanted to ask for advice

[Violeta Hernández]

I've defined CNF_coeff b o : Ordinal →₀ Ordinal, which corresponds to the finitely supported function assigning coefficients to each exponent in the base b Cantor normal form of o

[Violeta Hernández]

This has been pretty successful, and I've developed a decently large API for this.

[Violeta Hernández]

The issue is that I want to prove two particular statements about natural operations, namely that the natural sum adds together the base ω CNFs, and the natural product multiplies them as polynomials

[Violeta Hernández]

I've already proven the first, and I have all the necessary lemmas to prove the second, but I'm having trouble even stating it

[Violeta Hernández]

The "product as polynomials" refers to the product in AddMonoidAlgebra ℕ NatOrdinal, which is notably not equal to Ordinal →₀ Ordinal

[Violeta Hernández]

I can't even easily define the product manually. Since Ordinal isn't commutative, the sums that appear on docs#AddMonoidAlgebra.hasMul are not in general well-defined, even though of course the values in the base ω expansion are always naturals and thus do commute over addition and multiplication

[Violeta Hernández]

And I can't easily cast CNF_coeff ω o into AddMonoidAlgebra ℕ NatOrdinal either. I know the coefficients are less than ω and thus equal to some natural, but this is nonconstructive. So I'd have to use Classical.choice, which means no nice def-eqs are possible.

[Violeta Hernández]

I see two ways out of this. Option A is that I make a full API for CNF_coeff_omega : Ordinal →₀ ℕ and state the result in terms of that. That might be useful to someone else later down the line, but it does entail a lot of boilerplate.

[Violeta Hernández]

Option B is to define the product on Ordinal →₀ Ordinal through choice shenanigans. Basically, I can noncomputably convert a finsupp's finset into a list, and use that to emulate Finsupp.sum without commutativity. Of course, it makes my proof pretty painful and probably useless to anyone else.

[Violeta Hernández]

I'm leaning heavily towards option A, but I wanted to get some feedback since it might be hard to justify duplicating my results like that otherwise.

[Violeta Hernández]

Well, I chose to take option A. I don't think the duplicated API is too much of an issue - it's actually kind of nice not having to pass arguments like 1 < ω or Principal (· + ·) ω manually

[Violeta Hernández]

I think I've managed to prove everything I wanted to within my branch. I characterized the addition of CNFs, as well as their natural addition and multiplication. I'll slowly PR all of this over the following weeks.

[Violeta Hernández]

Something cool I realize I can now do is define the ordinal XOR, i.e. the sum of nim heaps

[Violeta Hernández]

And yeah, that only works thanks to CNF_coeff_omega

[Eric Vergo]

Violeta Hernández said:

I'm leaning heavily towards option A, but I wanted to get some feedback since it might be hard to justify duplicating my results like that otherwise.

Option A is what I was thinking of doing; even though it seems like a heavy lift. I'm going to poke around your branch for a bit, and will likely come back with a bunch of questions.

Curious to see what others say.

[Violeta Hernández]

Thanks! I desperately need feedback on all of this

[Eric Vergo]

FWIW I wouldn't put any weight on my opinions. I've never worked on large software projects before, so I'm just guessing.

[Violeta Hernández]

There's one particular thing that would help a lot. The names CNF_coeff and particularly CNF_omega_coeff are very wordy

[Violeta Hernández]

Does anyone have a better idea? The former is the function Ordinal →₀ Ordinal mapping exponents to coefficients in a base b CNF, while the latter is for base ω and is specialized to Ordinal →₀ ℕ.

[Violeta Hernández]

btw, my branch now contains a definition of the ordinal XOR and a proof of docs#Nat.xor_trichotomy for it!

[Violeta Hernández]

This will allow us to state a more general form of docs#SetTheory.PGame.grundyValue_nim_add_nim

[Violeta Hernández]

...PRing all of this might take a while
image.png