Real Closed Fields Project

Stream: mathlib4

[Artie Khovanov]

I'm formalising some real algebra in Mathlib :slight_smile:
https://artie2000.github.io/real_closed_field/
I've got a blueprint, which should make it relatively easy to contribute if you are interested!
I've already formalised some material on orderings of rings and fields.
I think a good target is the characterisation of real closed fields (Theorem 40 / RCF_tfae).
I have some material beyond this (Sturm's theorem, real closures, Artin-Schreier theorem) but I haven't fully worked out a path to formalising it.
Eventually I want to prove the Tarski-Seidenberg principle, but that's quite far away and I'm not really sure how equipped Lean is to handle the computational aspects of the theory.
I'm doing this in my spare time, so progress will be slow, but any contributions are very welcome! The ultimate goal is to upstream everything to Mathlib.

[Kenny Lau]

wow that's quite quick!

[Violeta Hernández]

Hi! I'm interested in this. I kind of need this in order to show surreals are real closed.

[Artie Khovanov]

@Violeta Hernández what results do you need? See the blueprint for what I have planned

[Violeta Hernández]

I need the result that for $R$ a real-closed field and $\Gamma$ a divisible group, the field of Hahn series $R[[X^\Gamma]]$ is also real-closed

[Violeta Hernández]

I'm not really sure if this is more of a Hahn series result or a real-closed field result

[Violeta Hernández]

Found this on ncatlab
image.png

[Artie Khovanov]

Yep OK so the only bit of real closed field theory you need there is that index 2 in algebraic closure implies real closed (so, Theorem 50 in the current version of my blueprint)

[Artie Khovanov]

The rest is Hahn series stuff eg k[t^G][i]=k[i][t^G]

[Artie Khovanov]

At the moment that result (Theorem 50) is a while away, at least the way I want to prove it, due to missing API around quadratic extensions (see Lemma 3)
But any contributions in this direction would of course be very welcome :)

[Violeta Hernández]

How do you even write down K[i] in Mathlib?

[Artie Khovanov]

AdjoinRoot K (X^2 + 1)

[Artie Khovanov]

And, if you already have your field, use IsAdjoinRoot

[Violeta Hernández]

Thanks!

[Violeta Hernández]

I'll read about this. Hope I'm not jumping into something far beyond my depth...

[Artie Khovanov]

Nothing in the blueprint is really beyond the level of a first course in number fields, if you take the ordering stuff as given
And much of the proofs is just polynomial manipulation
I'm still getting to grips with this part of the library though; it feels like there's definitely missing API

[Violeta Hernández]

Polynomials in Mathlib my beloathed

[Artie Khovanov]

There isn't even a normal form for them

[Weiyi Wang]

I reminded myself about this project as I stumbled upon some theory mentioning real-closeness. Specifically this lemma: a Gamma-valued, real-closed or algebraically closed field F has a section (a group homomorphism Gamma->F that's right inverse of the valuation. I wonder if it is in the scope of the project, or when the definition of real closed field will be ready in mathlib to express this.

[Aaron Liu]

for any Gamma?

[Aaron Liu]

or does the valuation have to be surjective

[Aaron Liu]

wait what do you mean the field has a section, and where did the valuation come from

[Weiyi Wang]

For any valuation. Gamma just refers to the value group (so surjectivity implied). "Section" is just name given to the homomorphism in the article I am reading

[Artie Khovanov]

I have "real closed field" stated but I haven't proved much about them yet
the API around finite extensions of fields needs work

[Weiyi Wang]

:smile: Would be nice to see it in mathlib even with just simple definition and lemmas. I think the actual lemma I need is "you can take n-th root in real closed fields"

[Artie Khovanov]

Well, you can't take nth roots, necessarily. You can take them when n is odd, or when n is even and your element is non-negative. Stuff about real closed fields is generally proved from the algebraically closed field version using the characterisation of real closed fields as non-algebraically-closed fields whose extension by $\sqrt{-1}$ is algebraically closed.

[Weiyi Wang]

sorry I should clarify I meant taking n-th root of a positive number

[Artie Khovanov]

Here is the definition I have right now:

/- An ordered field is real closed if every nonegative element is a square and
   every odd-degree polynomial has a root. -/
class IsRealClosed (R : Type*) [Field R] [LinearOrder R] : Prop extends IsStrictOrderedRing R where
  isSquare_of_nonneg {x : R} (hx : 0 ≤ x) : IsSquare x
  exists_isRoot_of_odd_natDegree {f : R[X]} (hf : Odd f.natDegree) : ∃ x, f.IsRoot x

I don't have much else (you can check out the project blueprint to see current scope and progress)

[Violeta Hernández]

I'd love to see the definition in Mathlib too. That way I can add the relevant proof_wanted for my project!

[Filippo A. E. Nuccio]

I think @Florent Schaffhauser had somethink on this.

[Artie Khovanov]

Yes, this project comes as a result of his work on real algebra.

[Artie Khovanov]

@Violeta Hernández just proved the result you wanted - it's very_weak_Artin_Schreier in my project

[Artie Khovanov]

unfortunately it's built on top of some custom field extension API but yeah working on it

[Violeta Hernández]

Thank you very much! This is really nice.

[Aaron Liu]

is this the result we wanted?

[Violeta Hernández]

Hmm... I think what we really want eventually is the converse? So as to show that the surcomplex numbers are algebraically closed.

[Aaron Liu]

I feel like that shouldn't be too hard

[Artie Khovanov]

Converse is also proved in that file (and yes is much easier, was proved months ago)

[Aaron Liu]

since every polynomial factors into degree-at-most-two irreducibles which then factor over the field extension by the quadratic formula

[Artie Khovanov]

Artie Khovanov said:

Converse is also proved in that file (and yes is much easier, was proved months ago)

Wait no I got confused
Your converse I just proved last night and is the harder direction lmao

[Violeta Hernández]

It feels a bit weird to write any theorem as ∃! _ : LinearOrder, _. Would it make sense to make a type-valued RealClosed structure which bundles the ring ordering and uses it to define a LinearOrder instance? Or am I saying nonsense?

[Artie Khovanov]

I am very close to having the whole thing (RealClosedField.TFAE) finished, and then I can work on making it closer to Mathlib. Just got one implication (IVT) to go.

[Aaron Liu]

the ordering is unique anyways

[Artie Khovanov]

Violeta Hernández said:

It feels a bit weird to write any theorem as ∃! _ : LinearOrder, _. Would it make sense to make a type-valued RealClosed structure which bundles the ring ordering and uses it to define a LinearOrder instance? Or am I saying nonsense?

Normally we say an ordered field is real closed if...

I suppose you could say a field is real closed if... which works as Aaron says by uniqueness, but that would be quite strange

Really what's best to do is to use the 3 or 4 theorems that that result uses. So, show it's real, then create the order on it, then show it's real closed.

[Violeta Hernández]

Aaron Liu said:

the ordering is unique anyways

Yes, but I believe we like it when we're able to specify data, even if said data is uniquely characterized.

[Violeta Hernández]

Wait, any field with a finite dimensional algebraically closed extension is real closed??? I had no idea

[Aaron Liu]

artin schrICANTSPELL

[Violeta Hernández]

TIL

[Aaron Liu]

any finite extension where the upper field is algebraically closed, the lower field is either algebraically closed or real closed

[Aaron Liu]

it kind of intuitively makes sense maybe

[Violeta Hernández]

your intuition is clearly more calibrated than mine

[Aaron Liu]

everything is intuitive of you've played with it too much

[Violeta Hernández]

I imagine the idea is if some other polynomial is missing a root then you can start constructing an infinite set of other polynomials that are also missing roots?

[Aaron Liu]

like consider the finite fields

[Aaron Liu]

a finite extension $\overline{\mathbb{F}_p}/K$ corresponds to a finite closed subgroup of $\widehat{\mathbb{Z}}$

[Aaron Liu]

but $\widehat{\mathbb{Z}}$ is $\mathbb{Z}$-torsion free so every element has infinite order

[Violeta Hernández]

That makes sense

[Florent Schaffhauser]

Artie Khovanov said:

Violeta Hernández said:

It feels a bit weird to write any theorem as ∃! _ : LinearOrder, _. Would it make sense to make a type-valued RealClosed structure which bundles the ring ordering and uses it to define a LinearOrder instance? Or am I saying nonsense?

Normally we say an ordered field is real closed if...

I suppose you could say a field is real closed if... which works as Aaron says by uniqueness, but that would be quite strange

Not really, no :blush:

Define a real-closed field to be a real field with no non-trivial real extension. Then such a field indeed has a canonical linear ordering. Note that, in this approach, a real field does not come with an ordering.

Conversely, given a real field, there is an ordering, but it is not canonical in general. The upshot of starting with an ordered field is that you get a canonical real closure.

@Artie Khovanov I remember we discussed it after your talk in Heidelberg :blush:

[Violeta Hernández]

Perhaps these could be separate things? We could have IsRealClosed for a field with non-trivial real extensions, and something else like IsOrderedRealClosed for a real closed field with a compatible linear order.

[Florent Schaffhauser]

Yes, I guess it depends what the end goal is :slight_smile: The important thing is: if the real field is real-closed, then the ordering is unique.

In principle, you have a theory of real fields and a theory of ordered fields. Ordered fields are real and real fields admit an ordering, which is not unique in general but is unique when the real field is real-closed.

Moreover, the following characterisation of real-closed fields holds, which makes no reference to an ordering.

Let $K$ be a field. Then the following conditions are equivalent.

1. $K$ is a real-closed field.
2. $K$ is a real field and, for all $a \in K$, either $a$ or $-a$ is a square in $K$, and, moreover, every polynomial of odd degree with coefficients in $K$ has a root in $K$.
3. The $K$-algebra $K[T]/(T^2 + 1)$ is an algebraically closed field.
   

[Artie Khovanov]

Violeta Hernández said:

Wait, any field with a finite dimensional algebraically closed extension is real closed??? I had no idea

Yeah it's a really cool result. Needs a bunch more algebra though, which is where I'm hoping my new concrete field extension API will really start to pay off.

[Artie Khovanov]

Florent Schaffhauser said:

Yes, I guess it depends what the end goal is :slight_smile: The important thing is: if the real field is real-closed, then the ordering is unique.

In principle, you have a theory of real fields and a theory of ordered fields. Ordered fields are real and real fields admit an ordering, which is not unique in general but is unique when the real field is real-closed.

Moreover, the following characterisation of real-closed fields holds, which makes no reference to an ordering.

Let $K$ be a field. Then the following conditions are equivalent.

1. $K$ is a real-closed field.
2. $K$ is a real field and, for all $a \in K$, either $a$ or $-a$ is a square in $K$, and, moreover, every polynomial of odd degree with coefficients in $K$ has a root in $K$.
3. The $K$-algebra $K[T]/(T^2 + 1)$ is an algebraically closed field.
   

Just proved IsSemireal.TFAE_RCF in the same file :tada:

[Violeta Hernández]

Florent Schaffhauser said:

Yes, I guess it depends what the end goal is :slight_smile: The important thing is: if the real field is real-closed, then the ordering is unique.

The fact that you can state meaningful results about real-closed fields without reference to orderings suggest to me that this intermediate notion is useful. We could then have as a theorem that there's a unique ordering which makes them into an ordered real closed field.

[Violeta Hernández]

Basically, I think we should be able to ask is a field is real closed without having to awkwardly ask "does there exist a linear ordering which makes it real closed".

[Artie Khovanov]

The "right" definition of that notion is imv a real field $F$ such that, for all $x$ in $F$, either $x$ or $-x$ is a square, and moreover all odd-degree polynomials over $F$ have a root - ie Florent's condition 2. And yeah it's a general fact that real fields have a unique ordering iff for all $x$ in $F$, either $x$ or $-x$ is a square (or if you like you can even drop real and say for all nonzero $x$ in $F$, exactly one of $x$ and $-x$ is a square).

[Violeta Hernández]

Actually, is the condition that a linear order be a ring ordering equivalent to docs#IsOrderedRing ? Or are these separate things?

[Artie Khovanov]

We usually want IsStrictOrderedRing, which is equivalent over domains to IsOrderedRing, but the instance isn't in Mathlib, so we spell "(totally) ordered field" as [Field F] [LinearOrder F] [IsStrictOrderedRing F] .

[Artie Khovanov]

But, to answer your question, depending on the source you read, an "order compatible with ring operations" means, usually, IsOrderedRing and, more rarely, IsStrictOrderedRing.

[Violeta Hernández]

I believe we recently did make this into an instance: docs#IsOrderedRing.toIsStrictOrderedRing

[Artie Khovanov]

huh
my PR got turned down iirc :sob:

[Violeta Hernández]

Second time's the charm?

[Artie Khovanov]

Oh I am silly, just checked the blame
That was my PR!
What got turned down was me weakening the typeclasses everywhere!
Because it added about 1% to Mathlib's compile time, spread out over pretty much all the algebra/order files.

[Artie Khovanov]

So the instance is there but you shouldn't use it unless you really need to.

[Violeta Hernández]

Artie Khovanov said:

But, to answer your question, depending on the source you read, an "order compatible with ring operations" means, usually, IsOrderedRing and, more rarely, IsStrictOrderedRing.

Hmm, so what so you think about this? Having the IsRealClosedinstance not depend on orders, and proving theorems about real closed fields with their canonical ordering using the typeclasses IsRealClosed + LinearOrder + IsStrictOrderedRing

[Artie Khovanov]

That could work yeah! (But IsStrictOrderedRing because of what I said)

[Artie Khovanov]

Like the first thing you prove is that x ≥ 0 ↔ IsSquare x, and then you proceed as normal

[Artie Khovanov]

I'm very happy to announce that the main theorem of the project, the characterisation of real closed fields, has been proved (sorry-free). It's IsRealClosed.TFAE in this file. The project blueprint is at https://artie2000.github.io/real_closed_field.

Let $R$ be an ordered field. TFAE:

1. $R$ is a real closed field; that is, all non-negative elements of $R$ have a square root and all odd-degree polynomials over $R$ have a root.
2. $\bar{R}\cong_{R}R[X]/(X^2+1)=R(i)$.
3. $R$ has no nontrivial ordered algebraic extensions.
4. $R$ has no nontrivial algebraic extensions by ordered fields.
5. Polynomials over $R$ satisfy the intermediate value (Darboux) property.

[Ruben Van de Velde]

Planning to pr it to mathlib?

[Artie Khovanov]

(deleted)

[Artie Khovanov]

Ruben Van de Velde said:

Planning to pr it to mathlib?

Yes. I am in the process of PRing some preliminaries, but I could do with more eyes on the process, which is proceeding very slowly right now (tbf also because I've been slow to respond). Please help out at #PR reviews > #27282 Real algebra

[Artie Khovanov]

A lot of my work is technically independent of these real algbera preliminaries, so I'll start upstreaming in parallel when I get a chance.

[Artie Khovanov]

Weiyi Wang said:

:smile: Would be nice to see it in mathlib even with just simple definition and lemmas. I think the actual lemma I need is "you can take n-th root in real closed fields"

Now proved in the same place as IsRealClosed.exists_eq_pow_of_nonneg. This one should get into Mathlib sooner rather than later, modulo the definitional questions above.

[Artie Khovanov]

Violeta Hernández said:

I imagine the idea is if some other polynomial is missing a root then you can start constructing an infinite set of other polynomials that are also missing roots?

Yeah, the vibe is like, if you can do the Artin-Schreier (positive char) and Kummer (char 0) constructions once, you can iterate them over and over. And Galois theory says we always have prime-index subextensions, so that gets us started. This note by Keith Conrad has an elementary proof that I can understand, although it's probably not the one to write up in Mathlib (instead we should develop Artin-Schreier and Kummer theory more fully).

[Violeta Hernández]

Kummer and Artin-Schrier extensions? It's actually uncanny just how related your projects are to our combinatorial games project haha

[Florent Schaffhauser]

Artie Khovanov said:

I'm very happy to announce that the main theorem of the project, the characterisation of real closed fields, has been proved (sorry-free). It's IsRealClosed.TFAE in this file. The project blueprint is at https://artie2000.github.io/real_closed_field.

Let $R$ be an ordered field. TFAE:

1. $R$ is a real closed field; that is, all non-negative elements of $R$ have a square root and all odd-degree polynomials over $R$ have a root.
2. $\bar{R}\cong_{R}R[X]/(X^2+1)=R(i)$.
3. $R$ has no nontrivial ordered algebraic extensions.
4. $R$ has no nontrivial algebraic extensions by ordered fields.
5. Polynomials over $R$ satisfy the intermediate value (Darboux) property.

Congratulations! How about the following, slightly modified statement, though?

Let $R$ be a field. TFAE:

1. $R$ is a real closed field; that is, all non-negative elements of $R$ have a square root and all odd-degree polynomials over $R$ have a root.
2. $\bar{R}\cong_{R}R[X]/(X^2+1)=R(i)$.
3. $R$ admits an ordering and has no nontrivial ordered algebraic extensions.
4. $R$ admits an ordering and has no nontrivial algebraic extensions by ordered fields.
5. $R$ admits an ordering and polynomials over $R$ satisfy the intermediate value (Darboux) property.
   

The point is that it is not necessary to fix an ordering on $R$ at the outset.

[Artie Khovanov]

Florent Schaffhauser said:

Congratulations! How about the following, slightly modified statement, though?

...

The point is that it is not necessary to fix an ordering on $R$ at the outset.

As I said, I already have a version of this statement. But yeah I am planning to change the definition to not require an order as per your and Violeta's suggestion.

I don't think I will state it the way you have, though. Rather, I plan to have one TFAE for real fields and one for ordered fields. There isn't a nice way to state conditions (3) and (5) if you don't assume an order.

[Artie Khovanov]

So:

Let $R$ be a real field. TFAE:

1. $R$ is real closed.
2. $\bar{R}\cong_R R(i)$.
3. $R$ has no nontrivial real extensions.

Let $R$ be an ordered field. TFAE:

1. $R$ is real closed.
2. $R$ has no nontrivial ordered extensions.
3. Polynomials over $R$ satisfy the IVP.

[Artie Khovanov]

(Note: since typeclass search finds ordered -> real, we don't need to repeat conditions (2) and (3)).

[Artie Khovanov]

Violeta Hernández said:

Kummer and Artin-Schrier extensions? It's actually uncanny just how related your projects are to our combinatorial games project haha

Please support my IsAdjoinRoot refactor when it comes through upstreaming so it's easier to work with concrete algebraic extensions! :slight_smile:

[Artie Khovanov]

image.png
$R$ is a RCF. Anyone know an order-free argument for this bit? I removed the order from everything else. Not mathematically necessary of course, but would be nice.

[Aaron Liu]

everything has a square root and every cubic+ polynomial has a root

[Aaron Liu]

so by repeatedly taking out roots every polynomial factors into degree-at-most-two factors over $R$

[Aaron Liu]

then the quadratic factors split over $R[i]$ by the quadratic formula

[Artie Khovanov]

It's clear $-(a^2+b^2)$ isn't a square because it's the negation of a sum of squares. But why can't $-(a+\sqrt{a^2+b^2})$ be a square?

[Aaron Liu]

wait what

[Aaron Liu]

every element of $R[i]$ has a square root

[Aaron Liu]

oh wait that's what you were proving

[Artie Khovanov]

@Aaron Liu see the blueprint for the proof I am using. I am not doing the symmetric polynomials proof.
It is not true that everything has a square root, nor that every cubic+ polynomial has a root. Rather, exactly one of $x$ or $-x$ has a square root for every $x\neq 0$, and every odd-degree polynomial has a root. These two facts together do imply that $R(i)$ is the only nontrivial finite extension of $R$, and this lemma is one step in the Galois-theoretic proof of this fact.

[Aaron Liu]

yeah I have a proof

[Aaron Liu]

for the lemma you showed

[Aaron Liu]

I think I have a proof

[Aaron Liu]

just gotta think about it a bit more make sure my proof isn't bogus

[Artie Khovanov]

ah OK
I misunderstood what you were saying slightly but we're on the same page now!

[Aaron Liu]

so everything or its negative is a square

[Aaron Liu]

do I get that a sum of squares is a square or is that difficult

[Artie Khovanov]

That's the same difficulty as this lemma
You do get that negation of sum of squares isn't a square (ie no nontrivial sums of squares to 0)

[Aaron Liu]

well if the negation of a sum of squares isn't a square

[Aaron Liu]

then either the sum of squares is a square or the negation of the sum of squares is a square

[Aaron Liu]

therefore the sum of squares is a square

[Artie Khovanov]

oh yeah good point!

[Artie Khovanov]

lol that's what I said above, I'm so silly
but yeah is there a trick for the $a+\sqrt{a^2+b^2}$ when $a<0$ (or a different approach entirely)

[Aaron Liu]

I'm quite confident now that my proof isn't bogus

[Aaron Liu]

alright so we want to prove that $a+bi$ isn't a square

[Aaron Liu]

the norm of $a+bi$ is $(a+bi)(a-bi) = a^2 + b^2$

[Aaron Liu]

this is a square

[Aaron Liu]

dividing by $\sqrt{a^2+b^2}$ we obtain an element of norm one

[Aaron Liu]

by hilbert 90 this is of the form $\frac{a+bi}{\sqrt{a^2+b^2}} = (c+di)/(c-di)$ for some $c, d \in R$

[Aaron Liu]

then $(c+di)\sqrt{\frac{a^2+b^2}{c^2+d^2}}$ is a square root of $a+bi$

[Artie Khovanov]

nice!
Hilbert 90 seems a bit overkill
I think I can find something completely elementary here

[Aaron Liu]

well you use the tools available

[Artie Khovanov]

yeah I mean
such as the axioms of an ordered ring!

[Artie Khovanov]

right so unpacking the axioms it comes down to, if $a^2-b^2$ is a square, then so are $a+b$ and $a-b$, which is the heart of your proof

[Aaron Liu]

this feels false?

[Aaron Liu]

surely if I put $a = -1$ and $b = -1$ then we get $a^2-b^2=0=0^2$ but $a+b=-2$ isn't a square

[Artie Khovanov]

sorry uh
here $a$ is a square and $b$ is not

[Artie Khovanov]

yeah OK this is too complicated without the notion of "order"

[Aaron Liu]

order is just whether or not it's a square

[Aaron Liu]

so I was looking at your lemma 16

[Artie Khovanov]

yes but I mean, how does the proof of $a^2\geq b^2\implies a\geq|b|$ go in this formalism?

[Aaron Liu]

Artie Khovanov said:

image.png

the proof you had in an image

[Aaron Liu]

can't you just avoid showing positivity at all

[Artie Khovanov]

I need $c$ and $d$ to be in $R$, not in $R(i)$.
This is like, the dumbest possible proof: write out a general square, compare coefficients, rearrange.

[Aaron Liu]

why do you need them to be in $R$

[Aaron Liu]

what goes wrong if they're in $R(i)$

[Artie Khovanov]

(removed)

[Artie Khovanov]

Aaron Liu said:

what goes wrong if they're in $R(i)$

we are trying to prove that everything in $R(i)$ has a square root
so we can't just be taking square roots in $R(i)$
I've thoroughly confused myself at this point lol

[Aaron Liu]

but you proved every element of $R$ has a square root in $R(i)$

[Aaron Liu]

$\frac{a+\sqrt{a^2+b^2}}{2} \in R$ so it has a square root in $R(i)$

[Artie Khovanov]

oh right yep (I just came to this conclusion too lol)
yeah that's how you do it, just case split
in which case the formula isn't nearly as monstrous, either

[Artie Khovanov]

thanks for figuring it out, I'm really being silly today

[Violeta Hernández]

Artie Khovanov said:

image.png
$R$ is a RCF. Anyone know an order-free argument for this bit? I removed the order from everything else. Not mathematically necessary of course, but would be nice.

Not an answer to your question, but I think we should have some mechanism for declaring an ordering within a proof, so that statements don't need the order assumption, but proofs can freely use it.

[Artie Khovanov]

Yes, I have this already. In my project it's letI := IsSemireal.toLinearOrder K.

[Artie Khovanov]

@Aaron Liu I checked the standard textbooks and it looks like you can't really avoid this nasty computation (unless you start with a different definition ofc).

[Aaron Liu]

wait what does that mean

[Artie Khovanov]

like, there's not an obvious approach that's simpler than what you / we came up with

[Aaron Liu]

is hilbert 90 really that nasty

[Violeta Hernández]

We could just wrap it in an auxiliary lemma

[Artie Khovanov]

the proof doesn't use Hilbert 90?

[Violeta Hernández]

If x^2 = a^2 + b^2 then x^2 + a is a square

[Artie Khovanov]

I just mean you looking at my arument and observing that we don't need a+sqrt{a^2+b^2} to be a square

[Ruben Van de Velde]

Is this the same Hilbert 90 proved in regular flt?

[Aaron Liu]

Aaron Liu said:

I'm quite confident now that my proof isn't bogus

see my proof above

[Violeta Hernández]

I don't even need to know what Hilbert 90 is to know this is overkill

[Aaron Liu]

I think something similar was mentioned on the wikipedia page

[Aaron Liu]

the page for hilbert 90

[Aaron Liu]

you can classify pythagorean triples or something

[Artie Khovanov]

apparently the argument in my blueprint is actually Gauss' original argument
he just, solved the equations lol

[Aaron Liu]

algebra used to be the art of solving equations

[Violeta Hernández]

people had weird tastes back then

[Artie Khovanov]

image.png
OK the revised blueprint is ready. Will rewrite the file at some point.

[Artie Khovanov]

image.png
The new definition @Florent Schaffhauser. I thought it would be better to not assume realness either.

[Artie Khovanov]

I know this is all pretty "trivial" but computation in Lean is pain. Someday if I have time I'll write a tactic for computations in finite extensions...

[Aaron Liu]

this feels grindable

[Artie Khovanov]

The proofs are available on my repo; feel free to try golfing them!

[Artie Khovanov]

Well, the old order-based proofs are, but the new proofs are very similar.

[Aaron Liu]

I'll see what I can do

[Artie Khovanov]

Artie Khovanov said:

image.png
The new definition Florent Schaffhauser. I thought it would be better to not assume realness either.

Oops this definition was wrong (consider $\mathbb{F}_p$). Sticking to the standard definition!

[Aaron Liu]

what happens in oh I get it

[Aaron Liu]

actually no I don't get it

[Aaron Liu]

what's up with $\mathbb{F}_p$

[Aaron Liu]

yeah this definition seems fine

[Aaron Liu]

ah yeah I think I get it now

[Artie Khovanov]

quadratic residues

[Artie Khovanov]

indeed I think "sums of squares in F are squares in F" is equivalent to "all elements of F(i) are squares"

[Artie Khovanov]

@Aaron Liu
The map $x\to x^2$ on $\mathbb{F}_p^\times$ has kernel $\{\pm1\}$, so exactly half of the nonzero residues modulo $p$ are squares (these are called quadratic residues in number theory). Moreover, since $\mathbb{F}_p^\times$ is cyclic and $-1$ has order 2, $-1$ is not a square. Therefore exactly one of $a$ and $-a$ is a square for every $a\in\mathbb{F}_p^\times=\mathbb{F}_p\setminus\{0\}$. However, $\mathbb{F}_p$ is not even real, let alone real closed, since $-1=1+\cdots+1$ is a sum of squares.

[Aaron Liu]

Artie Khovanov said:

Moreover, since $\mathbb{F}_p^\times$ is cyclic and $-1$ has order 2, $-1$ is not a square.

no I'm pretty sure that only happens if $p \equiv 3 \pmod{4}$

[Aaron Liu]

and what happened to the part where all odd degree polynomials have a root

[Artie Khovanov]

Oh damn I'm so bad at this :skull:
And sorry I thought you were saying you didn't know what residues were!

[Aaron Liu]

oh sorry I know what residues are

[Artie Khovanov]

Aaron Liu said:

and what happened to the part where all odd degree polynomials have a root

yeah ik it's not strictly a counterexample but it shows the argument can't work
just need to think of a field F with no odd-degree extensions such that F(i) has a quadratic extension
probably the limit of odd-degree finite extensions of $\mathbb{Q}$ works

[Aaron Liu]

Artie Khovanov said:

probably the limit of odd-degree finite extensions of $\mathbb{Q}$ works

I don't think you get that everything or its minus is a square

[Aaron Liu]

I think the limit colimit of the odd-degree finite extensions of $\mathbb{F}_p$ works when $p \equiv 3 \pmod{4}$

[Artie Khovanov]

Yep that works I think
Nice
Thanks!

[Florent Schaffhauser]

Artie Khovanov said:

[...]
However, $\mathbb{F}_p$ is not even real, let alone real closed, since $-1=1+\cdots+1$ is a sum of squares.

If not yet included in your development, you could add that real fields necessarily have characteristic zero.

[Artie Khovanov]

Florent Schaffhauser said:

Artie Khovanov said:

[...]
However, $\mathbb{F}_p$ is not even real, let alone real closed, since $-1=1+\cdots+1$ is a sum of squares.

If not yet included in your development, you could add that real fields necessarily have characteristic zero.

Yeah I will do. Changing the definition has forced me to add a bunch of facts about real fields.

[Artie Khovanov]

Was just giving an elementary proof ^^

[Artie Khovanov]

Artie Khovanov said:

OK the revised blueprint is ready. Will rewrite the file at some point.

Rewrite done! The definition of RCF no longer requires an ordered field:

class IsRealClosed (R : Type*) [Field R] : Prop extends IsSemireal R where
  isSquare_or_isSquare_neg (x : R) : IsSquare x ∨ IsSquare (-x)
  exists_isRoot_of_odd_natDegree {f : R[X]} (hf : Odd f.natDegree) : ∃ x, f.IsRoot x

[Artie Khovanov]

Now tracking upstreaming PRs at this topic - please help out with reviews if you can!

[Elliot Glazer]

Artie Khovanov said:

Eventually I want to prove the Tarski-Seidenberg principle, but that's quite far away and I'm not really sure how equipped Lean is to handle the computational aspects of the theory.

I believe Lean can prove termination of all primitive recursive functions, so it should be able to directly implement the CAD algorithm for deciding the theory of a real-closed field. This should even be able to decide propositions about e.g. $(\mathbb{R}, +, \cdot, <, 0, 1, \pi)$ thanks to the effective bounds on transcendentality of $\pi$ provided by Baker's Theorem.

Of course, proving this algorithm correctly resolves propositions about these fields would be much more involved than merely implementing it.

[Artie Khovanov]

Yeah I mean in practice rather than in principle