#Theorem24.maple
#interface(quiet=true):
kernelopts(gcfreq=2*10^6):
#
#   This file shows that each of the 5 3-planes in C^5 which meet 6 2-planes
#  osculating the rational normal curve at real points are real.
#  (This instance of Shapiros' conjecture is Theorem 2.4 in "Real Schubert
#  Calculus: Polynomial systems and a conjecture of Shapiro and Shapiro".)
#	
#	Frank Sottile		updated:
#	November 25, 1997	2 August 1998
#	Toronto, Canada		Berkeley, CA
#
with(linalg):
with(Groebner):
readlib(realroot):
#
# SYMMETRIZE contains a routine to symmetrize a polynomial in Vars = s,t,u,v
# ELEMENTARIZE contains a procedure write a symmetric polynomial in 
#              Vars in terms of the elementary symmetric polynomials.
read SYMMETRIZE:
read ELEMENTARIZE:
#
#  We choose coordinates for C^5 so that the rational normal curve is the 
# (1, s, s^2, s^3, s^4), and assume that one of the 5-tuple 2-planes 
# osculates the rational normal curve at s=0, and another osculates 
# at s = infinity.  (This can be done with a projective transformation 
# preserving the form of the rational normal curve.)    We work in local 
# coordinates K for the set of 3-planes in C^5 meeting these 2 2-planes.  
# Here, the 3-plane is the row space of the given matrix.
#
K :=matrix([
[1,x12, 0 , 0 , 0 ],
[0, 1 ,x23,x24, 0 ],
[0, 0,  0 , 1 ,x35]]):
#
#  In these  coordinates,  the equation that a 3-plane meets the 2-plane
# osculating the rational normal curve at a point s is:  (we divide by the
# parameter s, as s cannot equal zero.)
#
A := s ->  simplify(det(stackmatrix(matrix([
[1,s,s^2,  s^3,  s^4],
[0,1,2*s,3*s^2,4*s^3]]),K))/s):
#
# Next, we compute a purely lexicographic Gr\"obner basis for the ideal
# generated by the equations for the 3-plane to meet 4 2-planes osculating 
# the rational normal curve at the points s, t, u, and v.
# We do this over the ring Z(s,t,u,v).  (In fact,the calculations proceed
# over the ring Z[s,t,u,v][D^{-1}], where D is the product of the vanderMonde
# of s,t,u,v and the monomial stuv.)
#
G:= gbasis([A(s),A(t),A(u),A(v)],plex(x12,x23,x24,x35)):
#
#  The Gr\"obner basis has 4 elements, with its first element a homogeneous
# polynomial of degree 5 in the variable x35 and symmetric in the parameters 
# s,t,u,v.  This is the UniversalEliminant for this set of equations.
# The first equation is linear in a and polynomial in d, and the same may be
# said of the second equation for b and the third for c.  Thus, for any
# value of the parameters s, t, u, and v, the number of real roots of the
# system equals the number of real roots of the UniversalEliminant.
#
UniversalEliminant:=sort(collect(op(1,G),x35),[x35]):
print(sort(Elementarize(UniversalEliminant,[s,t,u,v]),[x35]));
#
# We compute the Discriminant of the UniversalEliminant. 
#
Discriminant:=discrim(UniversalEliminant,x35):
print(simplify(Elementarize(Discriminant,[s,t,u,v])/4096));
#
# The following symmetric polynomials are all sums of squares
#
A1:=SYMMETRIZE((s*t*u*v*(s-t)*(s-u)*(s-v)*(t-u)*(t-v)*(u-v))^2):
#
A2:=SYMMETRIZE(s^4*t^2*u^2*v^2*(s-u)^2*(s-v)^2*(t-u)^2*(t-v)^2*(u-v)^2):
#
A3:=SYMMETRIZE(s^4*t^2*u^2*(s-t)^2*(s-u)^2*(s-v)^2*(t-u)^2*(t-v)^2*(u-v)^2):
#
A4:=SYMMETRIZE(s^2*t^2*u^2*(s-t)^2*(s-u)^2*(s-v)^2*(t-u)^2*(t-v)^2*(u-v)^4):
#
A5:=SYMMETRIZE(s^4*t^4*u^2*(s-u)^2*(s-v)^2*(t-u)^2*(t-v)^2*(u-v)^2):
#
A6:=SYMMETRIZE(s^2*t^2*u^2*v^2*(s-t)^4*(s-u)^4*(t-v)^2*(u-v)^2):
#
A7:=SYMMETRIZE(t^2*u^2*v^2*(s-t)^4*(s-u)^4*(s-v)^2*(t-v)^2*(u-v)^2):
#
A8:=SYMMETRIZE(s^4*t^4*u^2*(s-t)^2*(s-v)^2*(t-u)^2*(t-v)^2*(u-v)^2):
#
A9:=SYMMETRIZE(s^4*t^2*u^2*v^2*(s-t)^4*(s-u)^2*(t-v)^2*(u-v)^2):
#
A10:=SYMMETRIZE(t^2*u^2*v^2*(s-t)^4*(s-u)^4*(s-v)^2*(t-u)^2*(u-v)^2):
#
A11:=SYMMETRIZE(s^4*t^2*u^2*(s-u)^2*(s-v)^2*(t-u)^4*(t-v)^2*(u-v)^2):
#
A12:=SYMMETRIZE(s^2*t^2*v^2*(s-u)^2*(s-v)^4*(t-u)^4*(t-v)^2*(u-v)^2):
#
A13:=SYMMETRIZE(s^2*t^2*u^2*v^2*(s-t)^4*(t-u)^2*(t-v)^2*(u-v)^4):
#
A14:=SYMMETRIZE(s^4*t^2*u^2*(s-u)^2*(s-v)^2*(t-u)^2*(t-v)^4*(u-v)^2):
#
A15:=SYMMETRIZE(s^2*t^2*u^2*v^2*(s-t)^4*(s-v)^2*(t-u)^2*(u-v)^4):
# 
# These have a positive linear combination which equals the discriminant
#
simplify(6144*A1 + 12288*A2  + 14336*A3  + 14336*A4  + 4096*A5  + 4096*A6
      + 4096*A7  +  2048*A8  +  4096*A9  +  2048*A10 + 2048*A11 + 2048*A12
     + 12288*A13 + 20480*A14 +  6144*A15 - Discriminant);
#
# Since the Discriminant is a sum of squares, its non-zero locus is
# connected.  Hence the UniversalEliminant has the same number of real roots
# for any value of the  parameters s,t,u,v. At the point s=1, t=2, u=3, and
# v=4, it has five real roots: 
#
solve(subs(s=1,t=2,u=3,v=4,UniversalEliminant));
#
# This completes the proof that each of the 5 3-planes meeting 6 2-planes
# which osculate the rational normal curve at real points are real.
#
quit;

A1 is S4-invariant
A15 has stabilizer the D_8!  acting on the square:  s - v
                                                    |   |
                                                    t - u
These each are stabilized by a transposition:
    A2 (uv),  A3 (tu),  A4 (st),  A5 (st),  A6 (tu),  
    A7 (tu),  A13 (uv).

A8, A9, A10, A11, A12, A14 do not have a stabilizer in S4

Thus the Discriminant is a sum of 232 = 1 + 3 + 12 x 7 + 6 x 24
squares.