Nimbers

Stream: maths

[Violeta Hernández]

I just realized we don't have nimbers in mathlib!

[Violeta Hernández]

That could be a really nice project. Defining nimber addition and multiplication, and proving that ordinals under it are a ring → field → algebraically closed field

[Violeta Hernández]

The API design could be lifted directly from docs#NatOrdinal. Basically, we prove most things for ordinals, but create the type alias Nimber for whenever we need to use more general properties about rings / fields / whatnot.

[Violeta Hernández]

What would be some good notation for nimber addition and multiplication?

[Violeta Hernández]

I'm tempted to use ^^^ for the former but I don't have good ideas for the latter

[Violeta Hernández]

All sources I've found just use ⊕ and ⊗ which are of course unacceptable to us

[Violeta Hernández]

I guess we could always use something boring like +ₙ and ×ₙ, but being able to use ♯ and ⨳ in the NatOps file was really fun and I really wish there was an analog of that

[Violeta Hernández]

That being said. Maybe the solution here is to not define these operations on ordinals at all.

[Violeta Hernández]

This design works great for NatOrdinal since that type shares a lot of structure with Ordinal. They have the exact same order, and there's many connections between usual ordinal addition and natural addition, e.g. docs#Ordinal.add_le_nadd and everything to do with the Cantor normal forms.

[Violeta Hernández]

This is not at all the case for nimbers. They can't be ordered, and the arithmetic is completely distinct. I guess you can do things like a ^^^ b ≤ a + b but that's about it.

[Violeta Hernández]

It might make sense to define ≤ on nimbers. After all, how else are you supposed to talk about minimum excluded values? This relation wouldn't nicely interact with the arithmetic, but still

[Ted Hwa]

Why are ⊕ and ⊗ unacceptable?

[Violeta Hernández]

⊕ already has the much more common usage as a sum type α ⊕ β

[Violeta Hernández]

⊗ is a bit better, but it's still way too firmly associated with tensors in my opinion

[Violeta Hernández]

That being said, I think I've convinced myself that defining these operation on ordinals isn't the best idea. Nimbers are an algebraically closed field, and surely we don't expect to have special symbols for "nimber division on ordinals" or worse, "nimber roots on ordinals".

[Violeta Hernández]

These problems didn't exist on NatOrdinal since that's only a (commutative) semiring

[Violeta Hernández]

All we really need to do to talk about the nimber sum on ordinals is to use the casts toNimber and toOrdinal

[Violeta Hernández]

Starting work on https://github.com/leanprover-community/mathlib4/tree/vi.nimber

[Ruben Van de Velde]

Maybe the existing operators with a subscript?

[Violeta Hernández]

Wait, I think I know a good compromise

[Violeta Hernández]

I can implement Xor for Ordinal as nimber addition, but keep all other operations specific to Nimber

[Violeta Hernández]

XOR-ing ordinals can be a useful concept, but all the other operations really only make sense in the context of nimbers proper

[Violeta Hernández]

...except, maybe in the contexts where we XOR ordinals, we should be using Nimber instead?

[Violeta Hernández]

Yeah, I'm not sure anymore

[Violeta Hernández]

#16088

[Daniel Weber]

Violeta Hernández said:

...except, maybe in the contexts where we XOR ordinals, we should be using Nimber instead?

When do you XOR ordinals?

[Violeta Hernández]

Daniel Weber said:Nimbers/near/464580426):

When do you XOR ordinals?

To add together Sprague-Grundy values for games, and basically nowhere else

[Violeta Hernández]

That's kinda my point, it might be better if we simply make docs#SetTheory.PGame.grundyValue return Nimber

[Violeta Hernández]

btw just proved that nimbers are a commutative domain

[Violeta Hernández]

I'll build up probably up to division in https://github.com/leanprover-community/mathlib4/tree/vi.nimber_mul while the initial PR gets approved

[Violeta Hernández]

I have no idea how to show nimbers are algebraically closed, I'll have to look that up and see if it's feasible

[Violeta Hernández]

I looked it up

[Violeta Hernández]

It seems hard but definitely feasible

[Violeta Hernández]

Basically, you proceed by contradiction. If they weren't algebraically closed, you could take the smallest polynomial (in lexicographic order) without a root. Consider the least ordinal containing all roots of previous polynomials closed under all four (three) field operations. Prove that this is a root of said polynomial.

[Violeta Hernández]

There is an issue... Conway does operations on both ordinals and nimbers!

[Violeta Hernández]

His notation is that he does ordinal operations in square brackets. So [2 × 2] = 4 while 2 × 2 = 3. Clearly this won't work for us.

[Violeta Hernández]

(deleted)

[Violeta Hernández]

I'm still not sure if this justifies defining these operations on the Ordinal type. By doing so, we lose all of the cool field theorems and tactics.

[Violeta Hernández]

And if we're going to have to cast things anyways, casting operations from Ordinal into Nimber is probably better than the converse

[Violeta Hernández]

I'll just keep going like this. If we ever need to define nim arithmetic on ordinals, we do it. Otherwise, we don't.

[Violeta Hernández]

Anyways... I managed to show nimbers form a field!

[Violeta Hernández]

The proof for showing that the nimbers are algebraically complete is a bit convoluted, and Conway as usual skims over a few important details. So here's an attempt at giving a more thorough explanation to be used as a blueprint for formalization. This is all adapted from pages 57 and 58 of On Numbers And Games.

First, to contextualize Conway's notation. Conway uses the standard x + y and xy notation for nimber operations, and square brackets [x + y] and [xy] for ordinal operations. I think the best way to handle this ourselves is to just define local notation x +ₒ y = toNimber (toOrdinal x + toOrdinal y), etc. so I'll write the proof in this style too. Confusingly, Conway sometimes writes x - y even though nimbers are of characteristic 2 (to perhaps suggest y is less than x?), so I'll just change that to x + y.

Conway also talks about nimbers being groups, rings, or fields. The Mathlib translation would be that certain intervals Iio a are closed under addition, multiplication, and multiplicative inverses, respectively.

A final thing to note: the "excludents" of a Nim sum or product simply refer to the nimbers in the minimum excluded values of their respective definitions.

[Violeta Hernández]

Lemma 1: If x is a group, then x *ₒ y + z = x *ₒ y +ₒ z for any y and for z < x.

This is a very standard inductive proof, where you just show the excludents of the nim sum x *ₒ y + zprecisely coincide with the nimbers less than x *ₒ y +ₒ z. Specifically, the excludents either take the form (x *ₒ y' +ₒ w) + z = x *ₒ y' + (w + z) for y' < y and w < x or x *ₒ y + z' = x *ₒ y +ₒ z' for z' < z. Since x is a group, the expression w + z in the first set ranges over all values less than x as w does.

[Violeta Hernández]

...actually, wait a second

[Violeta Hernández]

I'm not at all convinced that Conway's proof actually works.

[Violeta Hernández]

Oh, of course. There's a note a few pages later about how the proof for theorem 44 is incomplete. And I don't really know how to fix it.

[Violeta Hernández]

In fact, I'd argue the usage of theorem 44 in theorem 45 (the main result) is incorrect too.

[Violeta Hernández]

Theorem 44 says that if x is a ring but not a field, and y is the largest group less than the least non-invertible element in x, then x ^ n * cₙ + ... + x * c₁ + a = x *ₒ (y ^ₒ (n - 1) *ₒ cₙ₋₁ +ₒ ... +ₒ c₁) +ₒ a for cᵢ < y and a < x.

[Violeta Hernández]

But Theorem 45 uses 44 in the case where x is a field, by setting y = x. I don't believe that's correct.

[Violeta Hernández]

And moreso, Conway reduces the proof of theorem 44 to proving x ^ (n + 1) = x *ₒ y ^ₒ n. That might be correct, but at least I can't see how the proof follows from that.

[Violeta Hernández]

...does anyone know of any other exposition of the proof? This is hurting my head.

[Violeta Hernández]

I believe I know of a way to make the proof work if you can show theorem 46 first, which is that for x a field and cᵢ < x, you have x ^ n * cₙ + ... + c₀ = x ^ₒ n *ₒ cₙ +ₒ ... +ₒ c₀. Conway seems to imply theorem 46 follows from 45, but again, I don't really see how that can be the case.

[Violeta Hernández]

And from Lemma 1, which seems completely correct to me, I think this should follow from just knowing x ^ n * c = x ^ₒ n *ₒ c, since x ^ n should be a group whenever x is.

[Violeta Hernández]

Unfortunately x ^ n won't always be a ring, which means you can't use theorem 42 for this.

[Violeta Hernández]

Wait... isn't theorem 46 false? 2 is a field yet 2 ^ 2 = 3 does not match 2 ^ₒ 2 = 4.

[Violeta Hernández]

I hope this is just a big misunderstanding on my part. If not, what a mess.

[Violeta Hernández]

Oh, never mind. I see that theorem 46 only works for exponents less than the degree of the least polynomial in lexicographic order without a root.

[Violeta Hernández]

But then I don't really understand where the theorem comes from.

[Violeta Hernández]

Is theorem 44 even being used in theorem 45? In fact, can we not just prove theorem 45 directly? I don't know.

[Violeta Hernández]

I think the course of action is to ask on MathOverflow.

[Violeta Hernández]

https://mathoverflow.net/q/477566/147705

[Violeta Hernández]

Alright, I've got another exposition of the proof that's hopefully clearer.

[Violeta Hernández]

image.png
Ok, this all makes much more sense

[Violeta Hernández]

This is page 440 of Siegel's Combinatorial Game Theory

[Violeta Hernández]

This is proven alongside the simplest extension theorem, but I don't think we need that with the explicit definition of the inverse I showed. That can be a separate project for someone else that's interested.

[Violeta Hernández]

That is, we just need to show lemma 4.4 and theorem 4.3 (d)

[Violeta Hernández]

In fact... I don't think we even need lemma 4.4 (b')

[Violeta Hernández]

Ok, so, for the blueprint

[Violeta Hernández]

Lemma 1 is unchanged

[Michael Rothgang]

It seems you already solved this, but: does https://arxiv.org/abs/math/0410026 clarify some questions about rigours? I'm not sure if it covers nimbers, but it does explain the basics about games.

[Violeta Hernández]

Haha, I've read that paper before. It was a key aid in the surreal multiplication proof. Unfortunately it doesn't cover much about nimbers.

[Violeta Hernández]

But yeah, I think I've solved my problems. Currently writing down Lemma 2...

[Violeta Hernández]

Lemma 2: if x is a field where all polynomials of degree less or equal to n have roots, then x ^ m * a = x ^ₒ m *ₒ a for m ≤ n and a < x.

Proceed by induction on m. The case m = 0 is trivial. We first show the general case for a = 1. Any y < x ^ₒ m can be written as x ^ₒ (m - 1) *ₒ aₘ₋₁ +ₒ ... +ₒ aₒ = x ^ (m - 1) * aₘ₋₁ + ... + aₒ = x ^ m + f(x) for a monic degree m polynomial f. By hypothesis, f has at least one root r, so we can rewrite x ^ m + f(x) = x ^ m + (x + r) * g(x) = x ^ (m - 1) * r + (x + r) * (x ^ (m - 1) + g(x)). Since r < x and x ^ (m - 1) + g(x) < x ^ (m - 1), we conclude this is an excludent for x ^ (m - 1) * x = x ^ m.

Conversely, every excludent for x ^ (m - 1) * x has the form a * x + x ^ (m - 1) * b + a * b for a < x ^ (m - 1) and b < x. This can be written as a polynomial over x of degree m - 1. By induction, we can rewrite that as an ordinal sum, which will be less than x ^ₒ m. We conclude x ^ m = x ^ₒ m.

Notice also that by this same argument of rewriting as a polynomial,x ^ m is closed under addition, and under multiplication by nimbers less than x.

For arbitrary a < x, we have that x ^ m * a is the mex of x ^ m * a' + x' * (a + a') for x' < x ^ m and a' < a. Since x is a field, a + a' is invertible, and thus x' * (a + a') takes all values less thanx ^ m as x' < x ^ m varies. Therefore, x ^ m * a is the mex of x ^ m * a' + b for a' < a and b < x ^ m. By Lemma 1, we can rewrite this as x ^ m * a' +ₒ b, and by induction we can rewrite as x ^ m *ₒ a' +ₒ b = x ^ₒ m *ₒ a' +ₒ b. This is the typical ordinal less than x ^ₒ m *ₒ a, so we conclude x ^ m * a = x ^ₒ m *ₒ a.

[Violeta Hernández]

This is probably going to be the hardest part of the proof by far.

[Violeta Hernández]

Lemma 3: The nimbers forming a field are unbounded.

This one is a very standard argument. For any nimber x₀, take the set of all sums, products, and inverses in x₀, as well as any nimbers below them, to create x₁. Build a sequence indexed by ℕ in this manner. The supremum of all xᵢ will be a field at least larger than x₀.

[Violeta Hernández]

Lemma 4: If x is a field that isn't algebraically closed, then x is a root of the smallest polynomial f in x in lexicographic order without a root.

Let n be the degree of f. Clearly f is monic, so we write f = X ^ n + g for g of degree at most n - 1. For any g' ≺ g, we have X ^ n + g' ≺ X ^ n + g, meaning it has a root r and we can write g'(x) = x ^ n + (x ^ n + g'(x)) = x ^ n + (x + r) * h(x) = r * x ^ (n - 1) + (x + r) * (x ^ (n - 1) + h(x)). Again, this is an excludent for x ^ n. By Lemma 3, this implies all ordinals less than g(x) are excludents for x ^ n.

Conversely (just as in Lemma 2), every excludent of x ^ n = x * x ^ (n - 1) has the form a * x + x ^ (n - 1) * b + a * b. If g(x) were an excludent, we could write g(x) = a * x + x ^ (n - 1) * b + a * b, then compare the base x ordinal expansions of both (by Lemma 2) to deduce g = a * X + X ^ (n - 1) * b + a * b as polynomials (this is a subtle point not adressed in Siegel!) Thus f = X ^ n + g can be straightforwardly be shown to have the root b, a contradiction.

We conclude x ^ n = g(x)and thus f(x) = 0.

[Violeta Hernández]

Theorem: Nimbers are algebraically closed.

We prove that every (non-constant) polynomial has a root, by induction on the lexicographic order. If f has no root but all previous polynomials do, we first build a field x₀ containing all coefficients of f (Lemma 3). Then we construct a sequence of fields F : ℕ → ON₂ such that each subsequent field F(n + 1) contains F(n), as well as all roots of lexicographically earlier polynomials to p within F(n) (as otherwise this might be a proper class!) The union of all these fields is a field such that f is the smallest polynomial in it without a root, so by Lemma 4, we conclude it actually did have a root.

[Violeta Hernández]

I think all of this is doable in Lean. But it's probably going to take me a month or even two.

[Violeta Hernández]

If anyone else wants to join in, that'd be awesome.

[Daniel Weber]

I'd love to help, although I'm not sure if I'll have the time

[Violeta Hernández]

I think either Lemma 1 or Lemma 3 is a good starting point. You can build off my branch which already proves nimbers are a field.

[Violeta Hernández]

Unfortunately I won't have time to start the proof for the next few days.

[Daniel Weber]

Conway also talks about nimbers being groups, rings, or fields. The Mathlib translation would be that certain intervals Iio a are closed under addition, multiplication, and multiplicative inverses, respectively.

How are you planning to do that? I think the most natural way would've been to use docs#IsAddSubgroup, docs#IsSubring and docs#IsSubfield on Set.Iio x, but those are deprecated so it's not a good idea.

[Violeta Hernández]

I asked about this on Xena. The conclusion I ended up with is that it's probably better to just define these predicates ourselves. For instance:

def IsGroup (x : Nimber) : Prop :=
  ∀ y < x, ∀ z < x, y + z < x

The proofs should hold by vacuity for 0, so we don't need to specify it in our definition. Also, there's no need to specify closure under inverses, since x - y is the same as x + y. So really, all we care about are the closure properties.

[Violeta Hernández]

It'd be a bit awkward to use docs#AddSubgroup, not only because of the unneeded extra conditions, but also because it's a type rather than a predicate on a set. We'd have to write ∃ s : AddSubgroup Nimber, x = ↑s, which of course isn't very ideal.

[Daniel Weber]

Defining IsGroup.toAddSubgroup should be fine though, right?

[Violeta Hernández]

Sure, though I don't think it'll be needed for the proof.

[Violeta Hernández]

...actually, it might be. On Lemma 4 we employ properties about the factorization of polynomials on x, which means we need a field instance somewhere.

[Violeta Hernández]

We might be able to get away with just using the instance from Nimber though. That remains to be seen.

[Daniel Weber]

Violeta Hernández said:

I think either Lemma 1 or Lemma 3 is a good starting point. You can build off my branch which already proves nimbers are a field.

How should I work with the branch? Make a branch off of it and then PR back to it?

[Violeta Hernández]

I think it's fine if you push directly. This is supposed to be somewhat of a test branch, from which we can then extract stuff for PRs. Just do tell me if and what you start work on, so we don't end up doing the same thing twice!

[Violeta Hernández]

By the way. All of this should probably go in a different file than the existing nimber file. I'm thinking we can have SetTheory/Ordinal/Nimber/Basic.lean and SetTheory/Ordinal/Nimber/Algebraic.lean

[Daniel Weber]

Do we have a < b + c <-> (a < b or exists d < c, a = b + d) (for ordinals a b c)?

[Violeta Hernández]

This can be deduced from docs#Ordinal.add_sub_cancel_of_le

[Violeta Hernández]

Ordinal subtraction a - b is defined so that b + (a - b) = a for b ≤ a, and a - b = 0 otherwise. So it explicitly gives you the value of d in your theorem.

[Violeta Hernández]

We also have ordinal division and moduli, which encode the result that for any ordinals x and y ≠ 0, you can write x = y * q + r for r < y.

[Daniel Weber]

I'm almost done with Lemma 1

[Violeta Hernández]

Tell me when you push it to the branch!

[Daniel Weber]

I pushed it

[Daniel Weber]

I also proved lemma 3

[Violeta Hernández]

Nice!

[Violeta Hernández]

I've got some time tonight to work on this, I'll try to do the final part of the proof after Lemma 4.

[Violeta Hernández]

I golfed the proofs down a bit :smile:

[Violeta Hernández]

I'm having a bit of trouble even writing the statement for the prerequisite lemma 4 down though.

[Violeta Hernández]

How do we talk about "the least polynomial with coefficients within this subset without a root under lexicographic order?"

[Violeta Hernández]

I think the relation would be p ≺ q ↔ Finsupp.lex (· > ·) (· < ·) p q

[Violeta Hernández]

Oh yeah, that's definitely it

/-- The lexicographic ordering on polynomials. -/
def polynomial_LT (p q : Polynomial Nimber) : Prop :=
  Finsupp.Lex (· > ·) (· < ·) p.toFinsupp q.toFinsupp

theorem wellFounded_polynomial_LT : WellFounded polynomial_LT := by
  apply InvImage.wf
  exact Finsupp.Lex.wellFounded' Nimber.not_lt_zero lt_wf Nat.lt_wfRel.wf

[Violeta Hernández]

I'd like to thank @Junyan Xu for having Finsupp.Lex.wellFounded in Mathlib, haha

[Violeta Hernández]

That would've been a struggle otherwise

[Violeta Hernández]

It's been quite painful to show that for any nimber, the set of polynomials with coefficients less than it is a small type. Not because it's hard, the API around enum and typein is just kind of bad.

[Violeta Hernández]

There's some stuff I want to change I'll write out here for future reference

• Rename Ordinal.out.α to a much more discoverable Ordinal.toType
• Make the type in typein and enum explicit
• Make auxiliary definitions typein_lt and enum_lt for interfacing with toType that avoid the instance inference issues, and having to awkwardly rewrite o.toType.type = o yourself

[Violeta Hernández]

Just managed to show it. I think that's all I can work on this for today.

[Violeta Hernández]

Pushed my progress onto the branch

[Violeta Hernández]

Actually, I don't think typein and such are even really necessary for this proof

[Violeta Hernández]

Something else I really need to do is add some API for Small

[Violeta Hernández]

This result should follow relatively easily from a Small instance on finsupps

[Violeta Hernández]

Eventually we should work on getting rid of blsub2 and all that stuff

[Daniel Weber]

I tried to write the proof of lemma 2 in full detail, please tell me if I'm missing something:

Set K = IsField.toSubfield x.
Sub-lemma 1 (this has to be inside of the induction):
For every natural number d ≤ m and nimber y < x ^ₒ d there exists a polynomial p : K[X] with degree less than d such that y = p(x).
Proof:
Induction on d. We can write y = x ^ₒ (d - 1) *ₒ (y /ₒ (x ^ₒ (d - 1)) +ₒ y %ₒ (x ^ (d - 1)). By lemma 1 this is equal to x ^ₒ (d - 1) *ₒ (y /ₒ (x ^ₒ (d - 1)) + y %ₒ (x ^ (d - 1)), by the large induction this is equal to x ^ (d - 1) * (y /ₒ (x ^ₒ (d - 1)) + y %ₒ (x ^ (d - 1)), and by the sub-lemma induction, we can write y %ₒ (x ^ (d - 1)) = aeval x q for degree x < d - 1. Now set p = ((y /ₒ (x ^ₒ (d - 1))) * X ^ (d - 1) + q.

Sub-lemma 2:
For every natural number d ≤ m and polynomial p : K[X] with degree less than d, p(x) < x ^ₒ d.
Proof:
By induction on d. We can write p(x) = x ^ (d - 1) * a + q(x) with a < x. By the large induction, this is x ^ₒ (d - 1) *ₒ a + q(x). By the induction hypothesis, q(x) < x ^ₒ (d - 1), so by lemma 1 this is x ^ₒ (d - 1) *ₒ a +ₒ q(x) < x ^ₒ (d - 1) *ₒ a +ₒ x ^ₒ (d - 1) = x ^ₒ (d - 1) *ₒ (succ a) ≤ x ^ₒ (d - 1) *ₒ x = x ^ₒ d.

Sub-lemma 3:
For every nimber y < x ^ₒ m and nimber a < x, y * a < x ^ₒ m
Proof:
By sub-lemma 1, y = p(x) for deg(p) < m. Now y * a = (p*a)(x), and deg(p*a) < m. Applying sub-lemma 2, the result follows.

We start by showing that x ^ₒ m = x ^ m. By definition we have x ^ m = x ^ (m - 1) * x = mex {a * x + x ^ (m - 1) * b + a * b | a < x ^ (m - 1), b < x}. We will show that {a * x + x ^ (m - 1) * b + a * b | a < x ^ (m - 1), b < x} = Set.Iio (x ^ₒ m).
By the induction we have x ^ (m - 1) = x ^ₒ (m - 1)

For one direction of the inclusion, let there be y < x ^ₒ m. We use sub-lemma 1 to write it as aeval p x for degree p < m. Now set f = X^m + p, which has degree m and is monic. By hypothesis, f has a root r < x, so we can write f = (X + r) * g for a monic g, and rewrite y = x^m + f(x) = x ^ m + (x + r) * g(x) = (x ^ (m - 1) + g(x)) * x + x ^ (m - 1) * r + (x ^ (m - 1) + g(x)) * r, which is exactly the form of an excludent. We have r < x, and x ^ (m - 1) + g(x) < x ^ (m - 1) = x ^ₒ (m - 1) by applying sub-lemma 2 to g + X ^ (m - 1).

For the other direction of the inclusion, we need to show a * x + x ^ (m - 1) * b + a * b < x ^ₒ m, for a < x ^ₒ (m - 1), b < x = x ^ₒ 1.
Using sub-lemma 1 we can write a, b as polynomials evaluated at x, and computing the degree of a * X + X ^ (m - 1) * b + a * b it's at most m, so sub-lemma 2 gives the desired conclusion.

Now we have to prove x ^ₒ m * y = x ^ₒ m *ₒ y for y < x. We will use induction on y.
By definition x ^ₒ m * y = mex {a * y + x ^ₒ m * b + a * b | a < x ^ₒ m, b < y}, and again we will prove {a * y + x ^ₒ m * b + a * b | a < x ^ₒ m, b < y} = Set.Iio (x ^ₒ m *ₒ y).

For one direction of the inclusion, let there be z < x ^ₒ m *ₒ y. We can write z = x ^ₒ m * (z /ₒ (x ^ₒ m)) + z %ₒ (x ^ₒ m), which is an excludent, setting b = z /ₒ (x ^ₒ m), a = (z %ₒ (x ^ₒ m)) / (b + y) (we have a < x ^ₒ m because b + y < x, and as x is a field (b + y)⁻¹ < x, then applying sub-lemma 3).

For the other direction, we can write a * y + x ^ₒ m * b + a * b = x ^ₒ m * b + a * (y + b). By the induction we have x ^ₒ m * b + a * (y + b) = x ^ₒ m *ₒ b + a * (y + b). By lemma 1, this is x ^ₒ m *ₒ b + a * (y + b). By sub-lemma 3, a * (y + b) < x ^ₒ m, so x ^ₒ m *ₒ b + a * (y + b) < x ^ₒ m *ₒ b + x ^ₒ m = x ^ₒ m *ₒ (succ b) ≤ x ^ₒ m *ₒ y.

[Violeta Hernández]

For sub-lemmas 1 and 2, in order to use lemma 1, you need to argue that x ^ₒ (d - 1) is closed under addition. This follows from the induction though, as for a, b < x ^ₒ (d - 1), you can write a + b = p(x) + q(x) = (p + q)(x) < x ^ₒ (d - 1) by the closure of K under addition.

[Violeta Hernández]

I think it might be slightly cleaner to include the statements of sub-lemma 1 and 2 for m = n as part of the main induction. That way, you don't have to nest inductions.

[Violeta Hernández]

Your proof seems correct to me. I really like that you managed to avoid having to evaluate p : K[X] as an ordinal, that's something I didn't really know how to deal with.

[Violeta Hernández]

Hopefully Lemma 4 doesn't require this either.

[Daniel Weber]

I want to merge master, as docs#pow_pos on the branch is outdated and requires a semiring. Is that OK?

[Daniel Weber]

I (mostly) proved the sublemmas for lemma 2

[Violeta Hernández]

I think it should be fine merging master. Just note that I have some major refactors to Ordinal coming up, so moving forward it's probably best not to keep the branch up to date until it's ready to PR.

[Daniel Weber]

Is (2 : Nimber) equal to zero, or is it the ordinal 2 as a nimber?

[Violeta Hernández]

The former

[Violeta Hernández]

Since the NatCast instance is derived from the ring structure

[Daniel Weber]

I proved the x ^ₒ m = x ^ m part of the lemma, but it's getting really slow, so I'll try to split some things to lemmas

[Kevin Buzzard]

I guess Conway would typically emphasize that number 2 is *2 not 2.

[Violeta Hernández]

I'll try and continue the last part of the proof soon

[Violeta Hernández]

Haven't had a lot of time unfortunately

[Daniel Weber]

I finished the proof of lemma 2 :smile:

[Violeta Hernández]

Back and working! Is there a problem if I merge Mathlib? There seems to have been some large refactor recently, since I had to rebuild the entire thing when switching to the branch

[Violeta Hernández]

Oh also, o.out.α for ordinals is now o.toType

[Violeta Hernández]

I finally got algify x to work, by which I mean that I proved that it is in fact a value larger than all roots of polynomials with coefficients less than x.

[Violeta Hernández]

The final step of the proof requires something even larger, which is the nfp of algify

[Daniel Weber]

Violeta Hernández said:

Back and working! Is there a problem if I merge Mathlib? There seems to have been some large refactor recently, since I had to rebuild the entire thing when switching to the branch

There shouldn't be a problem

[Violeta Hernández]

Just proved a bunch more lemmas on algify. Most notably, I now have a construction algify' satisfying x ≤ algify' x and

lemma mem_algify' {x y : Nimber} {p : Nimber[X]}
    (hp : ∀ c ∈ p.coeffs, c < x.algify') (hy : y ∈ p.roots) : y < x.algify' := sorry

With this, I should now be able to get the final induction to work

[Violeta Hernández]

We've clearly collected a lot of auxiliary lemmas, I'll try and PR a few of them

[Violeta Hernández]

What do you think the best way to write lemma 4 is?

[Violeta Hernández]

We're saying that a non-algebraically complete field is the root of the least polynomial that doesn't have one. How do we write that last part?

Should we use hx.toSubfield? Do we require the polynomial to be irreducible and monic, or just of degree 1 or greater?

[Daniel Weber]

I think using hx.toSubfield would be good. I don't think irreducibility is used in the proof, so I don't see a reason to include it. You'll have to show at some point that the minimal polynomial without a root is monic, either in lemma 4 or in the final theorem to apply lemma 4, and I think doing it in lemma 4 might be a bit cleaner.

[Violeta Hernández]

Oh oops, just pushed a commit "Lemma 4" when I meant to say we're now only missing Lemma 4!

[Violeta Hernández]

I had to tweak our definitions of addify, mulify, etc. a bit in order to prove monotonicity, but I think that's for the better since I plan on deprecating blsub₂ at some point

[Violeta Hernández]

I also strengthened fieldify x so that it also contains all the roots of polynomials with coefficients less than x, this ensures it can be used at all steps of the proof

[Violeta Hernández]

The last part of the proof employs the even stronger nextField, which is the algify' from before, i.e. the next fixed point of fieldify

[Violeta Hernández]

Unfortunately I won't have much time to close out the proof these next few days

[Violeta Hernández]

Ah by the way, we didn't end up needing Lemma 3 in its original form, instead I used that proof to show that nextField is a field

[Violeta Hernández]

Back at this again! Merging master was pretty nasty with all the refactors that have been going on, but I got it to work.

[Violeta Hernández]

There seems to have been some change with refine? This lemma

theorem inv'_recOn {p : Nimber → Prop} (a : Nimber) (h0 : p 0)
    (hi : ∀ a' < a, a' ≠ 0 → ∀ b, p b → p (inv' a' * (1 + (a + a') * b))) {x : Nimber}
    (hx : x ∈ inv'_set a) : p x := sorry

previously worked fine as refine inv'_recOn a ?_ ?_ hx, but now that doesn't work - I had to make x an explicit argument.

[Violeta Hernández]

There's some pretty frustrating omissions in the polynomial library... do we really not have the fact that p ≠ 0 → p.leadingCoeff ∈ p.coeffs? Or that p ≠ 0 → Monic (p.leadingCoeff⁻¹ • p)?

[Violeta Hernández]

I'll have a lot to PR once I complete the proof and start to clean it up.

[Violeta Hernández]

Also, that a value in a field is smul-regular iff it's non-zero

[Violeta Hernández]

That would be a nice simp lemma to have available

[Kevin Buzzard]

I don't know it's true that if you multiply a polynomial by the inverse of its leading coefficient you always get something monic. It would not surprise me if 3/3 were a junk value in Z/9, for example

[Violeta Hernández]

It should be true in a field, at least

[Kevin Buzzard]

Yes

[Violeta Hernández]

Should have specified that...

[Violeta Hernández]

That lemma should probably be taking in a smul-regular assumption

[Daniel Weber]

Kevin Buzzard said:

I don't know it's true that if you multiply a polynomial by the inverse of its leading coefficient you always get something monic. It would not surprise me if 3/3 were a junk value in Z/9, for example

I don't think division is defined in Z/9Z

[Violeta Hernández]

I'm starting to wonder if my statement of Lemma 4 was suboptimal. I defined a somewhat ad-hoc noRoots predicate to state it, but I could probably have used toSubfield instead.

[Violeta Hernández]

As in, if x is a field, and p is the smallest polynomial lexicographically without a root in x.toSubfield[X], then p casted to a polynomial Nimber[X] has x as a root.

[Violeta Hernández]

Or actually, I don't think I even need to cast the polynomial, I can just use aeval

[Violeta Hernández]

It's a bit unfortunate having to refactor my proofs when they're not even finished, but I suspect writing things like this should make them slightly less painful.

[Kevin Buzzard]

Daniel Weber said:

I don't think division is defined in Z/9Z

Sure, I was just being sloppy. I should have said "It would not surprise me if 3 * 3⁻¹ is not 1 in ZMod 9" (that's what's being proposed, except that this is a red herring anyway because Violeta is only interested in fields)

[Violeta Hernández]

I guess this discrepancy does explain why I've been having trouble with the polynomial API, it's tailored to more general and less well-behaved cases

[Daniel Weber]

I think it's just that the preferred spelling of p.leadingCoeff⁻¹ • p is normalize p and then it's docs#Polynomial.monic_normalize

[Violeta Hernández]

Oh, nice!