Definitions
Modern algebra: non constructive proofs
Proof theory: primitive recursive degree bounds
Computer algebra: elementary recursive degree bounds
Discussion

Elementary recursive complexity results in real
algebraic geometry
Marie-Françoise Roy
Université de Rennes 1
Women in Mathematics (Japan), 7 september 2022
June 21, 2022

Marie-Françoise Roy Université de Rennes 1

Elementary recursive complexity results in real algebraic geometry

Definitions
Modern algebra: non constructive proofs
Proof theory: primitive recursive degree bounds
Computer algebra: elementary recursive degree bounds
Discussion

Definitions
Modern algebra: non constructive proofs
Hilbert 17th problem
Artin’s proof
Positivstellensatz
Proof theory: primitive recursive degree bounds
Strategy for constructive proofs
Constructions of algebraic identities
Computer algebra: elementary recursive degree bounds
Sign determination
Thom encodings
Elementary recursive degree bounds
Discussion
Marie-Françoise Roy Université de Rennes 1

Elementary recursive complexity results in real algebraic geometry

Definitions
Modern algebra: non constructive proofs
Proof theory: primitive recursive degree bounds
Computer algebra: elementary recursive degree bounds
Discussion

Real algebraic geometry▶ solution of polynomial equalities and inequalities in Rk▶ R: real closed field, totally ordered field, positive elements are
square, IVT: Intermediate Value Theorem. If P ∈ R[X ]P(a)P(b) < 0, a < b then ∃c P(c) = 0▶ examples of real closed field : (such as R field of real numbers,
Ralg field of real algebraic numbers , and also and also nonarchimedean models such as R⟨ϵ⟩ the field of Puiseux series▶ R[i] is algebraically closed, using an algebraic proof due toLaplace of the Fundamental Theorem of Algebra.

Marie-Françoise Roy Université de Rennes 1

Elementary recursive complexity results in real algebraic geometry

Definitions
Modern algebra: non constructive proofs
Proof theory: primitive recursive degree bounds
Computer algebra: elementary recursive degree bounds
Discussion

Primitive recursive/elementary recursive▶ primitive recursive functions obtained from 0, successor,
chosing one coordinate, composition and recursion▶ example: addition from successor, multiplication fromaddition, exponentiation from multiplication using recursion▶ example: associate to n a tower of exponential whose height2
is n. f (0) = 2, f (1) = 22 , f (2) = 22 ... easy to constructusing recursion▶ elementary recursive functions are functions obtained fromaddition, multiplication, substraction and division usingchosing one coordinate, composition, finite summation andproduct. Typically: exponential function 2n , doublynexponential function 22 , a tower of exponentials of fixedheight (example: 5 or 4).
Marie-Françoise Roy Université de Rennes 1

Elementary recursive complexity results in real algebraic geometry

Definitions
Modern algebra: non constructive proofs
Proof theory: primitive recursive degree bounds
Computer algebra: elementary recursive degree bounds
Discussion

Positivity and sums of squares▶ Is a polynomial with real coefficients taking only non negativevalues a sum of squares of polynomials?
▶ Yes if the number of variables is 1.
▶ Hint : decompose the polynomial in powers of irreducible
factors: degree two factors (corresponding to complex roots)
are sums of squares, degree 1 factors (corresponding to realroots appear with even degree)▶ Yes if the degree is 2.
▶ Hint: a quadratic form taking only non negative values is asum of squares of linear polynomials

Marie-Françoise Roy Université de Rennes 1

Elementary recursive complexity results in real algebraic geometry

Definitions
Modern algebra: non constructive proofs
Proof theory: primitive recursive degree bounds
Computer algebra: elementary recursive degree bounds
Discussion

Positivity and sums of squares▶ Is a non-negative polynomial a sum of squares of polynomials?
▶ Yes if the number of variables is 1.
▶ Yes if the degree is 2.
▶ Also if the number of variables is 2 and the degree is 4
▶ No in all other cases.
▶ First explicit counter-example Motzkin ’69
1 + X 4 Y 2 + X 2 Y 4 − 3X 2 Y 2takes only non negative values and is not a sum of squares ofpolynomials.

Marie-Françoise Roy Université de Rennes 1

Elementary recursive complexity results in real algebraic geometry

Definitions
Modern algebra: non constructive proofs
Proof theory: primitive recursive degree bounds
Computer algebra: elementary recursive degree bounds
Discussion

Motzkin’s counter-example (degree 6, 2 variables)

M = 1 + X 4 Y 2 + X 2 Y 4 − 3X 2 Y 2▶ M takes only non negative values. Hint: arithmetic mean isalways at least geometric mean.
▶ M is not a sum of squares. Hint : try to write it as a sum ofsquares of polynomials of degree 3 and check that it is
impossible.
▶ Example: no monomial X 3 can appear in the sum of squares.
Etc ...

Marie-Françoise Roy Université de Rennes 1

Elementary recursive complexity results in real algebraic geometry

Definitions
Modern algebra: non constructive proofs
Proof theory: primitive recursive degree bounds
Computer algebra: elementary recursive degree bounds
Discussion

Hilbert 17th problem▶ Reformulation proposed by Minkowski.
▶ Question Hilbert ’1900.
▶ Is a non-negative polynomial a sum of squares of rational
functions ?
▶ Artin ’27: Affirmative answer. Non-constructive.

Marie-Françoise Roy Université de Rennes 1

Elementary recursive complexity results in real algebraic geometry

Definitions
Modern algebra: non constructive proofs
Proof theory: primitive recursive degree bounds
Computer algebra: elementary recursive degree bounds
Discussion

Outline of Artin’s proof▶ Suppose P is not a sum of squares of the field rational
functions.
▶ Sums of squares: proper cone of rational functions, and do
not contain P (a cone contains squares, closed under addition
and multiplication, a proper cone does not contain −1).
▶ Using Zorn’s lemma, get a maximal proper cone of the field ofrational functions which does not contain P. Such a maximal
cone defines a total order on the field of rational functions.
▶ Every totally ordered field has a real closure.
▶ Taking the real closure of the field of rational functions forthis order, get a field in which P takes negative values (whenevaluated at the ”generic point” = the point (X1 , . . . , Xk )).
▶ Then P takes negative values over the reals. First instance ofa transfer principle in real algebraic geometry. Based on
Sturm’stheorem, or Hermite quadratic
form.
Marie-Françoise Roy Université de Rennes 1
Elementary recursive complexity results in real algebraic geometry

Definitions
Modern algebra: non constructive proofs
Proof theory: primitive recursive degree bounds
Computer algebra: elementary recursive degree bounds
Discussion

Definition (Hermite’s Matrix)
Let P, Q ∈ R[X ] with deg P = p ≥ 1. The Hermite’s matrix
Her(P; Q) ∈ Rp×p is the matrix defined for 1 ≤ j1 , j2 ≤ p by
Her(P; Q)j1 ,j2 = Tra(Q(X ) · X j1 +j2 −2 )where Tra(A(X )) is the trace of the linear mapping ofmultiplication by A(X ) ∈ R[X ] in the R-vector space R[X ]/P(X ).
Hermite matrix easy to compute, its entries correspond to linear
combination of the Newton sums (moments) of P.

Marie-Françoise Roy Université de Rennes 1

Elementary recursive complexity results in real algebraic geometry

Definitions
Modern algebra: non constructive proofs
Proof theory: primitive recursive degree bounds
Computer algebra: elementary recursive degree bounds
Discussion

Hermite method
Theorem (Hermite’s Theory)
Let P, Q ∈ R[X ] with deg P = p ≥ 1. Then
TaQu(P, Q) = Si(Her(P; Q))
where
X

TaQu(P, Q) :=sign(Q(x)),

x∈R|P(x)=0

Si(Her(P; Q)) is the signature of the symmetric matrix Her(P; Q).
Moreover Si(Her(P; Q)) is determined by the signs of the principal
minors of Her(P; Q).
Proof: uses complex conjugate roots.
Marie-Françoise Roy Université de Rennes 1

Elementary recursive complexity results in real algebraic geometry

Definitions
Modern algebra: non constructive proofs
Proof theory: primitive recursive degree bounds
Computer algebra: elementary recursive degree bounds
Discussion

Transfer principe▶ A statement involving elements of R which is true in a real
closed field containing R (such as the real closure of the fieldof rational functions for a chosen total order) is true in R.
▶ Not any statement, only ”first order logic statement”.
▶ Example of such statement∃x1 . . . ∃xk P(x1 , . . . , xk ) < 0
is true in a real closed field containing R if and only if it istrue in R▶ Special case of quantifier elimination.

Marie-Françoise Roy Université de Rennes 1

Elementary recursive complexity results in real algebraic geometry

Definitions
Modern algebra: non constructive proofs
Proof theory: primitive recursive degree bounds
Computer algebra: elementary recursive degree bounds
Discussion

Remaining problems▶ Very indirect proof (by contraposition, uses Zorn).
▶ No hint on denominators: what are the degree bounds ?
▶ Artin notes effectivity is desirable but difficult.
▶ Effectivity problems : is there an algorithm checking whether
a given polynomial is everywhere nonnegative?
▶ Can we use this algorithm to provide a representation as asum of squares?

Marie-Françoise Roy Université de Rennes 1

Elementary recursive complexity results in real algebraic geometry

Definitions
Modern algebra: non constructive proofs
Proof theory: primitive recursive degree bounds
Computer algebra: elementary recursive degree bounds
Discussion

Positivstellensatz (Krivine ’64, Stengle ’74)
▶ Find algebraic identities certifying that a system of signcondition is empty.
▶ In the spirit of Nullstellensatz.
K a field, C an algebraically closed extension of K,
P1 , . . . , Ps ∈ K[x1 , . . . , xk ]P1 = . . . = Ps = 0 no solution in Ck⇐⇒∃ (A1 , . . . , As ) ∈ K[x1 , . . . , xk ]sA1 P1 + · · · + As Ps = 1.
▶ Grete Hermann, a female student from Hilbert has given in
her Ph D dissertation an algorithmic proof of the classicalNullstellensatz, with elementary recursive complexity (doubly
exponential in the number of variables).
▶ For real numbers, statement more complicated.
Marie-Françoise Roy Université de Rennes 1

Elementary recursive complexity results in real algebraic geometry

Definitions
Modern algebra: non constructive proofs
Proof theory: primitive recursive degree bounds
Computer algebra: elementary recursive degree bounds
Discussion

Positivstellensatz• K an ordered field, R a real closed extension of K,• P1 , . . . , Ps ∈ K[x1 , . . . , xk ], Pi (x) ̸= 0
Pi (x) ≥ 0
H(x) :Pi (x) = 0
∃ S=

Y
i∈I̸=

Pi2ei ,

• I̸= , I≥ , I= ⊂ {1, . . . , s},fori ∈ I̸=fori ∈ I≥

fori ∈ I=

N=

X X
I ⊂I≥

no solution in Rk

kI ,j QI2,j

Y

j

Pi

⇐⇒

(kI ,j > 0),i∈IZ ∈ ⟨Pi | i ∈ I= ⟩ ⊂ K[xsuch that.

S + |{z}N + |{z}Z = 0.
|{z}
>0
≥0
=0

Marie-Françoise Roy Université de Rennes 1

Elementary recursive complexity results in real algebraic geometry

Definitions
Modern algebra: non constructive proofs
Proof theory: primitive recursive degree bounds
Computer algebra: elementary recursive degree bounds
Discussion

Incompatibilities̸0 Pi (x) =Pi (x) ≥ 0
H(x) :Pi (x) = 0↓ H ↓:

fori ∈ I̸=fori ∈ I≥

fori ∈ I=

S+ |{z}
N + |{z}
Z
= 0
|{z}
>0
≥0
=0

with
S∈

nQ

N∈

nP

2ei
i∈I̸= PiI ⊂I≥o2
j kI ,j QI ,jP← monoid associated to H
Qi∈I PiZ ∈ ⟨Pi | i ∈ I= ⟩Marie-Françoise Roy Université de Rennes 1o← cone associated to H
← ideal associated to H

Elementary recursive complexity results in real algebraic geometry

Definitions
Modern algebra: non constructive proofs
Proof theory: primitive recursive degree bounds
Computer algebra: elementary recursive degree bounds
Discussion

Positivstellensatz implies Hilbert 17th problem
P ≥ 0 in Rk

⇐⇒

⇐⇒

=⇒

⇐⇒

P(x) < 0

P(x) =
̸
0−P(x) ≥ 0

no solution

no solution

P 2
P 2
P 2e += 0
i Qi − ( j Rj )P
|{z}
|
{z
}
>0
≥0
2
(P 2e + i Qi2 )(
i Qi
P
=
2
( j Rj2 )2
j Rj

P 2e +PP=

PMarie-Françoise Roy Université de Rennes 1

P

2
j Rj )P.

Elementary recursive complexity results in real algebraic geometry

Definitions
Modern algebra: non constructive proofs
Proof theory: primitive recursive degree bounds
Computer algebra: elementary recursive degree bounds
Discussion

Positivstellensatz: proofs▶ Classical proofs of Positivstellensatz based on Modern Algebra.
▶ Zorn’s lemma and Tranfer principle, very similar to Artin’s
proof for Hilbert 17th problem.
▶ non-constructive▶ no degree bounds

Marie-Françoise Roy Université de Rennes 1

Elementary recursive complexity results in real algebraic geometry

Definitions
Modern algebra: non constructive proofs
Proof theory: primitive recursive degree bounds
Computer algebra: elementary recursive degree bounds
Discussion

Remaining problems▶ Very indirect proof (by contraposition, uses Zorn).
▶ Effectivity is desirable but difficult.
▶ What are the degree bounds in the Positivstellensatz Identity ?
▶ Effectivity problems : is there an algorithm checking whether
a given system of polynomial inequalities is empty?
▶ If the answer is yes, can we use this algorithm to construct a
Positivstellensatz equality ?

Marie-Françoise Roy Université de Rennes 1

Elementary recursive complexity results in real algebraic geometry

Definitions
Modern algebra: non constructive proofs
Proof theory: primitive recursive degree bounds
Computer algebra: elementary recursive degree bounds
Discussion

Quantifier elimination▶ Classical proofs of Positivstellensatz based on Modern Algebra.
▶ Constructive proofs use a quantifier elimination algorithm over
the reals.
▶ What is quantifier elimination ?
▶ High school mathematics∃ x

ax 2 + bx + c = 0, a ̸= 0⇐⇒
b 2 − 4ac ≥ 0, a ̸= 0
▶ Valid for any formula, due to Tarski, using Tarski-queries andinduction on the number of variables, algorithm !
▶ Deciding emptyness of a system of inequalities is algorithmic.
Marie-Françoise Roy Université de Rennes 1

Elementary recursive complexity results in real algebraic geometry

Definitions
Modern algebra: non constructive proofs
Proof theory: primitive recursive degree bounds
Computer algebra: elementary recursive degree bounds
Discussion

Strategy of Lombardi▶ For every system of sign conditions with no solution, find asimple algorithmic proof of the fact there is no solution, basedon quantifier elimination▶ Use this proof to construct an algebraic incompatibility andcontrol the degrees for the Positivstellensatz.
▶ Uses notions introduced by Henri Lombardi.
▶ Key concept : weak inference.

Marie-Françoise Roy Université de Rennes 1

Elementary recursive complexity results in real algebraic geometry

Definitions
Modern algebra: non constructive proofs
Proof theory: primitive recursive degree bounds
Computer algebra: elementary recursive degree bounds
Discussion

Quantifier elimination methods▶ Many existing methods▶ The older ones have a primitive recursive complexity : Tarski,
Seidenberg, Cohen-Hormander.
▶ The one chosen by Henri Lombardi for a constructive proof of
Positivstellensatz is Cohen-Hormander algorithm as explainedin [BCR].

Marie-Françoise Roy Université de Rennes 1

Elementary recursive complexity results in real algebraic geometry

Definitions
Modern algebra: non constructive proofs
Proof theory: primitive recursive degree bounds
Computer algebra: elementary recursive degree bounds
Discussion

Degree ofan incompatibility̸0 Pi (x) =Pi (x) ≥ 0
H(x) :Pi (x) = 0↓ H ↓:S=

Y

Pi2ei ,

i∈I̸=

for

i ∈ I̸=fori ∈ I≥

fori ∈ I=

S+ |{z}
N + |{z}
Z
= 0
|{z}
>0
≥0
=0
N=

X X
I ⊂I≥

j

kI ,j QI2,jYi∈I

the degree of H is the maximum degree of
Y 2e
Y
S=
Pi i ,QI2,j
Pi (I ⊂ I≥ , j),
i∈I̸=

Pi ,

Z=

X

Qi Pi

i∈I=

Qi Pi (i ∈ I= ).

i∈I

Marie-Françoise Roy Université de Rennes 1

Elementary recursive complexity results in real algebraic geometry

Definitions
Modern algebra: non constructive proofs
Proof theory: primitive recursive degree bounds
Computer algebra: elementary recursive degree bounds
Discussion

Example:








x

̸= 0

y − x2 − 1 ≥ 0xy

no solution in R2= 0↓ x ̸= 0, y − x 2 − 1 ≥ 0, xy = 0 ↓:x 2 + x 2 (y − x 2 − 1) + x 4 + (−x 2 y ) = 0.
|{z}
|
{z
}
| {z }>0≥0=0
The degree of this is incompatibility is 4.
Marie-Françoise Roy Université de Rennes 1

Elementary recursive complexity results in real algebraic geometry

Definitions
Modern algebra: non constructive proofs
Proof theory: primitive recursive degree bounds
Computer algebra: elementary recursive degree bounds
Discussion

Weak Inference(in the particular case we need) F, G systems of sign conditions
K[u] and K[u, t]. A weak inferenceF(u)⊢∃ t G(u, t)

is a construction which for every system of sign condition H in
K[v ] with v ⊃ u not containing t and every incompatibility↓ G(u, t), H(v ) ↓K[v ,t]produces an incompatibility↓ F(u), H(v ) ↓K[v ] .
From right to left.
Marie-Françoise Roy Université de Rennes 1

Elementary recursive complexity results in real algebraic geometry

Definitions
Modern algebra: non constructive proofs
Proof theory: primitive recursive degree bounds
Computer algebra: elementary recursive degree bounds
Discussion

Weak inferences: case by case reasoning
A ̸= 0 ⊢

∨

A<0

A>0

↓ H, A < 0 ↓ ← degree δ1↓ H, A > 0 ↓ ← degree δ2A2e1 S1 + N1 − N1′ A + Z1 = 0| {z } | {z } |{z}A2e2 S2 + N2 + N2′ A + Z2 = 0| {z } | {z } |{z}A2e1 S1 + N1 + Z1 = N1′ A

A2e2 S2 + N2 + Z2 = −N2′ A

>0

=0

≥0

>0

≥0

=0

A2e1 +2e2 S1 S2 + N3 + Z3 = −N1′ N2′ A2A2e1 +2e2 S1 S2 + N1′ N2′ A2 + N3 + Z3 = 0
|
{z
} |
{z
} |{z}>0Marie-Françoise Roy Université de Rennes 1≥0=0Elementary recursive complexity results in real algebraic geometry

Definitions
Modern algebra: non constructive proofs
Proof theory: primitive recursive degree bounds
Computer algebra: elementary recursive degree bounds
Discussion

Weak inferences: case by case reasoning
Starting from two incompatibilities↓ H, A < 0 ↓ ← degree δ1↓ H, A > 0 ↓ ← degree δ2A2e1 S1 + N1 − N1′ A + Z1 = 0| {z } | {z } |{z}A2e2 S2 + N2 + N2′ A + Z2 = 0| {z } | {z } |{z}

>0

=0

≥0

>0

≥0

=0

we constructed (by making a product) a new incompatibility
A2e1 +2e2 S1 S2 + N1′ N2′ A2 + N3 + Z3 = 0
|
{z
} |
{z
} |{z}>0≥0=0↓ H, A ̸= 0 ↓ ← degree δ1 + δ2
Marie-Françoise Roy Université de Rennes 1

Elementary recursive complexity results in real algebraic geometry

Definitions
Modern algebra: non constructive proofs
Proof theory: primitive recursive degree bounds
Computer algebra: elementary recursive degree bounds
Discussion

List of statements needed into weak inferences form
▶ Many simple weak inferences of that kind are combined toobtain more interesting weak inferences.
▶ In particular: IVT, the Intermediate Value Theorem, has to betransformed into a weak inference▶ Finally Henri Lombardi proved primitive recursive degreebounds for Positivstellensatz, hence of the Hilbert 17 th
problem Lombardi ’90.
▶ There are prior or other contributions for the 17 th problem
only. • Kreisel ’57 - Daykin ’61 - - Schmid ’00▶ All these constructive proofs ⇝ primitive recursive degreebounds k and d = deg P.
Marie-Françoise Roy Université de Rennes 1

Elementary recursive complexity results in real algebraic geometry

Definitions
Modern algebra: non constructive proofs
Proof theory: primitive recursive degree bounds
Computer algebra: elementary recursive degree bounds
Discussion

Sign determination▶ R a real closed field (such as R, Ralg , R⟨ϵ⟩)▶ a univariate non zero polynomial P and a list of otherunivariate polynomials Q1 , . . . , Qs all in R[X ]▶ find the list of non-empty sign conditions (i.e. elements of{0, 1, −1}s ) realized by Q1 , . . . , Qs at the real roots of P (i.e.
roots in R)▶ variant: compute also the corresponding cardinalities

Marie-Françoise Roy Université de Rennes 1

Elementary recursive complexity results in real algebraic geometry

Definitions
Modern algebra: non constructive proofs
Proof theory: primitive recursive degree bounds
Computer algebra: elementary recursive degree bounds
Discussion

Special case 1: real root counting▶ a univariate non zero polynomial P ∈ R[X ]▶ decide whether P has a real root (i.e. a root in R) or not▶ variant: compute also the number of roots of P in R
▶ using Hermite’s method

Marie-Françoise Roy Université de Rennes 1

Elementary recursive complexity results in real algebraic geometry

Definitions
Modern algebra: non constructive proofs
Proof theory: primitive recursive degree bounds
Computer algebra: elementary recursive degree bounds
Discussion

Special case 2: Tarski query▶ a univariate non zero polynomial P ∈ R[X ] and anotherpolynomial Q ∈ R[X ]▶ decide the signs of Q at the roots of P in R (variant: countthe cardinalities)▶ tool : Tarski-query
TaQu(P, Q) :=X

sign(Q(x))

x∈R|P(x)=0▶ using Hermite’s method

Marie-Françoise Roy Université de Rennes 1

Elementary recursive complexity results in real algebraic geometry

Definitions
Modern algebra: non constructive proofs
Proof theory: primitive recursive degree bounds
Computer algebra: elementary recursive degree bounds
Discussion

Special case 2: Tarski queryc(P = 0, Q = 0) is the number of roots of P in R where Q = 0 etc


 

1 1 1
c(P = 0, Q = 0)
TaQu(P, 1)
0 1 −1 c(P = 0, Q > 0) =  TaQu(P, Q) 
0 1 1
c(P = 0, Q < 0)
TaQu(P, Q 2 )Compute three Tarski-queries, then compute three cardinals anddecide which are the non-empty sign conditions.
Using Hermite’s method.

Marie-Françoise Roy Université de Rennes 1

Elementary recursive complexity results in real algebraic geometry

Definitions
Modern algebra: non constructive proofs
Proof theory: primitive recursive degree bounds
Computer algebra: elementary recursive degree bounds
Discussion

General case▶ Tarski-queries are considered as black-boxes▶ compute Tarski-queries of P and products of the Qi or theirsquares (using Hermite’s method for example)▶ solve a linear system,▶ compute the cardinals of sign conditions at the roots of P,▶ gives sign determination

Marie-Françoise Roy Université de Rennes 1

Elementary recursive complexity results in real algebraic geometry

Definitions
Modern algebra: non constructive proofs
Proof theory: primitive recursive degree bounds
Computer algebra: elementary recursive degree bounds
Discussion

Naive algorithm
Order the elements of {0, 1, −1}s lexicographically and consider
the elements of {0, 1, 2}s as coding all natural numbers smaller
than 3s − 1.
▶ Perform the 3s products of the Qi and Qi2▶ Compute the 3s corresponding Tarski-queries, which defined avector t▶ Define the 3s × 3s matrix of signs M whose columns areindexed by {0, 1, −1}s and rows are indexed by {0, 1, 2}s , theσ, α entry being the sign taken by Q1α1 . . . , Qsαs at σ.
▶ solve the linear system M · c = t where c is the unknown▶ keep the non-zero elements of c which are the cardinals of the
non-empty sign conditions
Marie-Françoise Roy Université de Rennes 1

Elementary recursive complexity results in real algebraic geometry

Definitions
Modern algebra: non constructive proofs
Proof theory: primitive recursive degree bounds
Computer algebra: elementary recursive degree bounds
Discussion

Naive algorithm
Example for s = 2, the matrix of signs is

1
0

0

0

0

0

0

0
0


1 1 1 1 1
1
1
1
0 0 1 1 1 −1 −1 −1

0 0 1 1 11
11
1 −1 0 1 −1 0
1 −1
0 0 0 1 −1 0 −1 1 
0 0 0 1 −1 0
1 −1
1 1 0 1 10
11
0 0 0 1 1
0 −1 −1
0 0 0 1 10
1
1

and is invertible.
Marie-Françoise Roy Université de Rennes 1

Elementary recursive complexity results in real algebraic geometry

Definitions
Modern algebra: non constructive proofs
Proof theory: primitive recursive degree bounds
Computer algebra: elementary recursive degree bounds
Discussion

Naive algorithm
Rows are numbered from 0 to 8. The row of number 4 (fifth row)is the sign of the polynomial Q1 Q2 on the list of signs (since 4 iswritten 1+3 in basis 3)
sign(Q1 ) 0 0 0 1 1 1 −1 −1 −1sign(Q2 ) 0 1 −1 0 1 −1 0
1 −1
sign(Q1 Q2 ) 0 0 0 0 1 −1 0 −1 1
The correctness is proved by induction on s.
The number of calls to the Tarski-query black box is exponential ins.

Marie-Françoise Roy Université de Rennes 1

Elementary recursive complexity results in real algebraic geometry

Definitions
Modern algebra: non constructive proofs
Proof theory: primitive recursive degree bounds
Computer algebra: elementary recursive degree bounds
Discussion

Improved algorithm▶ Notice that the number of non-empty sign conditions is at
most the number r ≤ d of real roots▶ Remove non-empty sign conditions at each induction step
▶ Use the special structure of the matrix to solve the linear
system in quadratic time
▶ Prove that the Q1α1 . . . , Qsαs whose Tarski-query is
computed in the algorithm have at most log2 d non zero
entries.

Marie-Françoise Roy Université de Rennes 1

Elementary recursive complexity results in real algebraic geometry

Definitions
Modern algebra: non constructive proofs
Proof theory: primitive recursive degree bounds
Computer algebra: elementary recursive degree bounds
Discussion

Complexity▶ The total number of calls to the Tarski-query blackbox is 3sd▶ The Tarski-query blackbox is called for P and polynomials ofdegree at most 2d log2 dMarie-Françoise Roy Université de Rennes 1

Elementary recursive complexity results in real algebraic geometry

Definitions
Modern algebra: non constructive proofs
Proof theory: primitive recursive degree bounds
Computer algebra: elementary recursive degree bounds
Discussion

Real algebraic numbers▶ Real algebraic numbers can be characterized by the signs theygive to their derivatives (Thom encodings) : easy by induction
on the degree▶ Thom encodings can be computed by sign determination▶ No numerical approach needed, valid on any real closed field▶ Once we know the Thom encodings, sign determination gets
simplified, only products of (a few) derivatives and one of theother polynomial (or its square) are used.

Marie-Françoise Roy Université de Rennes 1

Elementary recursive complexity results in real algebraic geometry

Definitions
Modern algebra: non constructive proofs
Proof theory: primitive recursive degree bounds
Computer algebra: elementary recursive degree bounds
Discussion

Sign determination and quantifier elimination▶ Eliminating one variable corresponds (basically) to parametricsign determination▶ P, Q1 , . . . , Qs are polynomials in parameters u and main
variable X▶ compute polynomials in the parameters u whose signs fix thelist of non-empty sign conditions realized by
Q1 [u][X ], . . . , Qs [u][X ], at the real roots of P[u][X ]Marie-Françoise Roy Université de Rennes 1

Elementary recursive complexity results in real algebraic geometry

Definitions
Modern algebra: non constructive proofs
Proof theory: primitive recursive degree bounds
Computer algebra: elementary recursive degree bounds
Discussion

Sign determination and quantifier elimination▶ Tarski’s proof of quantifier elimination is basically naive sign
determination▶ Complexity primitive recursive
There are much better quantifier elimination methods▶ Cynlindrical algebraic decomposition is doubly exponential▶ Polynomial when the number of variables is fixed▶ Uses the notion of connected component of a sign condition
More recent methods doubly exponential in the number of blocksof quantifiers and polynomial when this number if fixed. Use evenmore geometry (critical points ...).

Marie-Françoise Roy Université de Rennes 1

Elementary recursive complexity results in real algebraic geometry

Definitions
Modern algebra: non constructive proofs
Proof theory: primitive recursive degree bounds
Computer algebra: elementary recursive degree bounds
Discussion

Sign determination and quantifier elimination▶ New purely algebraic quantifier elimination method using sign
determination and Thom encodings▶ Complexity elementary recursive▶ Polynomial in the number of polynomials when the number ofvariables is fixed but NOT in the degree of the polynomials▶ Does not need the notion of a connected component of a signcondition

Marie-Françoise Roy Université de Rennes 1

Elementary recursive complexity results in real algebraic geometry

Definitions
Modern algebra: non constructive proofs
Proof theory: primitive recursive degree bounds
Computer algebra: elementary recursive degree bounds
Discussion

Elementary recursive degree bounds for Positivstellensatz▶ strategy: transform a simple proof that a system ofinequalities has no solution into the construction of analgebraic identity▶ turn the preceding ingredients : computation of signature ofHermite quadratic form, Thom encodings, sign determination
into construction of algebraic identities▶ control the degree of these identities▶ not having to deal sign connected components of signconditions is crucial(Joint work with Daniel Perrucci and Henri Lombardi)

Marie-Françoise Roy Université de Rennes 1

Elementary recursive complexity results in real algebraic geometry

Definitions
Modern algebra: non constructive proofs
Proof theory: primitive recursive degree bounds
Computer algebra: elementary recursive degree bounds
Discussion

Construct specific algebraic identities expressing that

▶ a real polynomial of odd degree has a real root
▶ a real polynomial has a complex root (by Laplace’s algebraic
proofof the Fudamental Theorem of Algebra)▶ Tarski queries computed by Hermite quadratic forms▶ the Sylvester’s inertia law for quadratic forms is valid▶ realizable sign conditions for a family of univariate
polynomials at the roots of a polynomial, fixed by sign ofminors of Hermite quadratic forms (uses Thom’s encoding,and sign determination),▶ realizable sign conditions for P ⊂ K[x1 , . . . , xk ] are fixed bylist of non empty sign conditions for
Proj(P) ⊂ K[x1 , . . . , xk−1 ] : efficient projection method using
only algebra
and at the end produce a sum of squares, with elementary
recursive
complexity (tower of five exponentials)!
Marie-Françoise Roy Université de Rennes 1
Elementary recursive complexity results in real algebraic geometry

Definitions
Modern algebra: non constructive proofs
Proof theory: primitive recursive degree bounds
Computer algebra: elementary recursive degree bounds
Discussion

How is produced the sum of squares ?
Suppose that P takes always non negative values. The proof thatP≥0
is transformed, step by step, in a proof of the weak inference⊢P ≥ 0.

Which means that if we have an initial incompatibility of H withP ≥ 0, we know how to construct a final incompability of H itself
Going right to left.

Marie-Françoise Roy Université de Rennes 1

Elementary recursive complexity results in real algebraic geometry

Definitions
Modern algebra: non constructive proofs
Proof theory: primitive recursive degree bounds
Computer algebra: elementary recursive degree bounds
Discussion

How is produced the sum of squares ?
In particular P < 0, i.e. P ̸= 0, −P ≥ 0, is incompatible withP ≥ 0, sinceP 2 + P × (−P) = 0|{z}| {z }>0≥0
is an initial incompatibility of P ≥ 0, P ̸= 0, −P ≥ 0 !
Hence, taking H = [P ̸= 0, −P ≥ 0] we know how to construct anincompatibility of H itself !
P 2
P 2
P 2e += 0
i Qi − ( j Rj )P
|{z}
|
{z
}
>0
≥0
which is the final incompatibility we are looking for !!
We expressed P as a sum of squares of rational functions !!!
Marie-Françoise Roy Université de Rennes 1

Elementary recursive complexity results in real algebraic geometry

Definitions
Modern algebra: non constructive proofs
Proof theory: primitive recursive degree bounds
Computer algebra: elementary recursive degree bounds
Discussion

Elementary recursive Hilbert 17 th problem

A non negative polynomials of degree d in k variables can be
represented as a sum of squares of rational functions withelementary recursive degree bound:
d4

2
22

k

.

[LPR]
and similar results for Positivstellensatz and Real Nullestellensatz

Marie-Françoise Roy Université de Rennes 1

Elementary recursive complexity results in real algebraic geometry

Definitions
Modern algebra: non constructive proofs
Proof theory: primitive recursive degree bounds
Computer algebra: elementary recursive degree bounds
Discussion

Discussion▶ Why a tower of five exponentials ?
▶ outcome of our method ... no other reason ...
▶ the existence of a real root for an univariate polynomials ofdegree d already gives a construction of algebraic identities
with two level of exponentials▶ the proof of Laplace starts from a polynomial of degree d andproduces a polynomial of degree d d : triple exponential forthe construction of algebraic identities corresponding to thefundamental theorem of algebra▶ our projection method based only on algebra then gives
univariate polynomials of doubly exponential degrees(eliminating variables one after the other using Hermite’s
method)▶ finally : a tower of 5 exponentials▶ long paper, appeared in Memoirs of the AMS ...
Marie-Françoise Roy Université de Rennes 1
Elementary recursive complexity results in real algebraic geometry

Definitions
Modern algebra: non constructive proofs
Proof theory: primitive recursive degree bounds
Computer algebra: elementary recursive degree bounds
Discussion

If you want to read moreMarie-Françoise Roy Université de Rennes 1

Elementary recursive complexity results in real algebraic geometry

Definitions
Modern algebra: non constructive proofs
Proof theory: primitive recursive degree bounds
Computer algebra: elementary recursive degree bounds
Discussion

References[BGP] Blekherman G., Gouveia J. and Pfeiffer J. Sums of Squares on theHypercube Manuscript. arXiv:1402.4199. [BCR] J. Bochnak , M. Coste ,M.-F. Roy. Real algebraic geometry. Second edition in english.Ergebnisseder Mat., vol. 36. Berlin Heidelberg New York: Springer (1998)[BPR] S. Basu, R. Pollack, M.-F. Roy, Algorithms in real algebraic
geometry, Algorithms and Computation in Mathematics, 10, Second
edition. Springer-Verlag, Berlin, 2006.
[PR] D. Perrucci, M.-F. Roy. Elementary recursive quantifier elimination
based on Thom encoding and sign determination. Annals of Pure andApplied Logic, Volume 168, Issue 8, August 2017, Pages 1588-1604(preliminary version, arXiv:1609.02879v2) .
[LPR] H. Lombardi, D. Perrucci, M.-F. Roy, An elementary recursive
bound for effective Positivstellensatz and Hilbert 17-th problem(preliminary version, arXiv:1404.2338).

(and many other references there)
Marie-Françoise Roy Université de Rennes 1

Elementary recursive complexity results in real algebraic geometry