I am trying to (re)compute the Groebner basis used for proving the theorem of Pappus (plane geometry) as done here on pages 22-23. Since I have no Mathematica license, I used e.g. REDUCE:
load_package groebner;
f := {u3*u4-u2*u5-u3*u7+u5*u7+u2*x1-u4*x1, u5*x2-u4*x3, -u1*u2+u1*x2-u3*x2+u2*x3, x1*x4-u7*x5, -u2*u6-u3*x4+u6*x4+u2*x5, u1*u7-u1*x6+x1*x6-u7*x7, -u4*u6-u5*x6+u6*x6+u4*x7, 1-v*(x3*x4-x2*x5-x3*x6+x5*x6+x2*x7-x4*x7)};
groebner f;
But the result is not the expected {1}, it is a list of 70 polynomials. Similar results I get when using Singular.
I have double (triple, quadruple, ...) checked the input polynomials. Placing the "input" points at A(0,0), B(0,u1=1), C(0,u6=5/2), A1(u2=1,u3=-1), B1(u4=2,u5=-1), C1(u7=3,x1=-1), s.t. the configuration looks like in the image below, I computed P(x2=2/3,x3=-1/3), Q(x4=15/19,x5-5/19), S(x6=18/13,x7=1/13).
When plugging these values into the input polynomials I get the expected "cancellations":
s := {u1=1, u6=5/2, u2=1, u3=-1, u4=2, u5=-1, u7=3, x1=-1, x2=2/3, x3=-1/3, x4=15/19, x5=-5/19, x6=18/13, x7=1/13};
sub(s, f);
--> {0, 0, 0, 0, 0, 0, 0, 1}
The 7 0s come from the 7 given collinearities (the eighth collinearity of A,B,C is implicit by placing them on the y-axis), the 1 from the Rabinowitch trick (the factor of v for the concluded collinearity of P,Q,S is also 0). I am stuck now. Am I missing something? Can someone verify the Groebner basis calculation in Mathematica? The input should be:
GroebnerBasis[{u3*u4-u2*u5-u3*u7+u5*u7+u2*x1-u4*x1,u5*x2-u4*x3,-u1*u2+u1*x2-u3*x2+u2*x3,x1*x4-u7*x5,-u2*u6-u3*x4+u6*x4+u2*x5,u1*u7-u1*x6+x1*x6-u7*x7,-u4*u6-u5*x6+u6*x6+u4*x7,1-v*(x3*x4-x2*x5-x3*x6+x5*x6+x2*x7-x4*x7)},{u1,u2,u3,u4,u5,u6,u7,v,x1,x2,x3,x4,x5,x6,x7}]
The equations obviously have a lot of trivial solutions, for example, $$ vx_4(x_3- x_7) = 1,\; u_6=u_3, \quad u_4=u_2=x_2=x_6=u_7=x_1=0. $$ So the set of equations is perhaps not correct. So far we don't obtain any contradiction, i.e., the Groebner basis is not equal to $\{1\}$, and Reduce is fine (and for free).