An example from the tutorial

Tangent and secant
For any
given circle and given external point, we trace tangent and secant lines. Then the product of distances (from given point) to secant points equals the square of distance to point of tangency.

Hypotheses :

TM=AM H1:=(x[3]-a)^2+(y-b)^2-(x[1]-a)^2-b^2;

AM=BM H2:=(x[1]-a)^2-(x[2]-a)^2;

OT
^ MT H3:=x[3](x[3]-a)+y(y-b);

Thesis : x[3]^2+y^2=x[1]*x[2]

Remarks on the choice of privileged variables:

Use R::=Q[x[1..3],y,a,b]
-------------------------------
Dim(R/Ideal(H1,H2,H3));
3
-------------------------------

-In our settings, the given external point has been fixed to the origin and the circle has been set to pass through some points in the x-axis.

In general a circle is determined by its center (a,b) and the coordinates of one more point on the circle. So in our case the free variables could be

{a,b,x[2]}

or

{a,b,x[1]}

or

{a,b,x[3],y}!!
No, this latter case does not represent the fact that the circle passes through the x-axis. Moreover, there is a tangency condition expressed in terms of these variables.

or

{a,b,x[3]}

or

{x[1],x[2],x[3}}
since x[1], x[2] give the idea of circle passing through x-axis and x[3] is enough to determine the construction, by the tangency condition? Anyway, it is a 3-equations, 3-free variables system...

We can also describe our circle as given by the two points in the x-axis and the b-coordinate of its center (since the a-coordinate must be x[1]+x[2]/2), that is, we could take as independent variables

{x[1],x[2],b}, etc....

-Thus the dimension is as expected, since to give a circle amounts to give

---a center (two coordinates)

+

---a radius (one more degree of freedom).

==================================

-We check that (some of)
our privileged variables are truly independent ...

¥ {a,b,x[2]} are independent

Elim([y,x[1],x[3]], Ideal(H1,H2,H3))
Ideal(0)
-------------------------------

¥ {a,b,x[1]} are independent

Elim([y,x[2],x[3]], Ideal(H1,H2,H3))
Ideal(0)
-------------------------------

¥ {b,x[2],x[1]} are independent

Elim([y,a,x[3]], Ideal(H1,H2,H3))
Ideal(0)
-------------------------------
¥{x[1],x[2],x[3]} are independent

Elim([y,a,b], Ideal(H1,H2,H3))
Ideal(0)

etc....

So our potential independent variables are really independent.
===================================================

Working out the theorem for some choices of variables.

First we find

S:=Saturation(Ideal(H1,H2,H3),Ideal(T));

S
Ideal(x[1] - x[2], x[2]^2 - 2x[2]a + x[3]a + yb, x[3]^2 + y^2 - x[3]a - yb)
-------------------------------

thus theorem NOT ALGEBRAICALLY TRUE, SINCE S­(1)

--Next we consider as independent variables
{a,b,x[2]}

Elim([y,x[1],x[3]], S)
Ideal(0)
-------------------------------

In this case the thesis does not vanish over all privileged components.
It is
Not generally true .

We try to see what happens if we look for discovery conditions:

Elim([y,x[1],x[3]], Ideal(H1,H2,H3, T))
Ideal(0)
-------------------------------
So the theorem is true just over some (perhaps small) subset of the privileged components. There is nothing we can do?

--Ditto for
{a,b,x[1]}

Elim([y,x[2],x[3]], S)
Ideal(0)
-------------------------------

In this case the thesis does not vanish over all privileged components.
It is Not generally true.
We try to see what happens if we look for discovery conditions:

Elim([y,x[2],x[3]], Ideal(H1,H2,H3, T))
Ideal(0)
-------------------------------

So the theorem is true just over some small subset of the privileged components. There is nothing we can do?

--Ditto for
{b,x[1],x[2]}

Elim([y,a,x[3]], S)
Ideal(x[1] - x[2])
-------------------------------

In this case, the thesis vanishes over all privileged components.
It is
generally true .
We get rid of the components where x[1]=x[2], which are not privileged, of course, and we will have a true theorem.

---Ditto for
{x[1],x[2],x[3]}

Elim([y,a,b], S)
Ideal(x[1] - x[2])
-------------------------------

In this case, the thesis vanishes over all privileged components.
It is
generally true .
We get rid of the components where x[1]=x[2], which are not privileged, of course, and we will have a true theorem.
============================================

Analyzing it furthermore

{a,b,x[2]}

that yield

Elim([y,x[1],x[3]], S)
Ideal(0)
-----------------------

Elim([y,x[1],x[3]], Ideal(H1,H2,H3, T))
Ideal(0)

Then we notice that this theorem must hold over some parts of privileged components and also must fail over some privileged components.
Let us find these components:

S:=Saturation(Ideal(H1,H2,H3),Ideal(T));
S
Ideal(x[1] - x[2], x[2]^2 - 2x[2]a + x[3]a + yb, x[3]^2 + y^2 - x[3]a - yb)
-------------------------------
NF(x[2]^2 - 2x[2]a + x[3]a + yb, Ideal(H1,H2,H3))
0

GenRepr(x[2]^2 - 2x[2]a + x[3]a + yb, Ideal(H1,H2,H3))
[-1, -1, 1]
-------------------------------
So this condition is trivial.

NF(x[3]^2 + y^2 - x[3]a - yb, Ideal(H1,H2,H3))
0

GenRepr(x[3]^2 + y^2 - x[3]a - yb,Ideal(H1,H2,H3))
[0, 0, 1]
-------------------------------
So this condition is trivial

Finally

NF(x[1]- x[2], Ideal(H1,H2,H3))
x[1] - x[2]
-------------------------------
So this one is not trivial

Moreover we know that S is the intersection of the components where the theorem fails. It is of dimension

Dim(R/S)
3
============================

On the other hand, we know that the components where the theorem holds are

SS:=Saturation(Ideal(H1,H2,H3), S);
SS
Ideal(x[1] + x[2] - 2a, x[3]^2 + y^2 - x[3]a - yb, x[2]^2 - 2x[2]a + x[3]a + yb)
H3
--

So these are the equations of the good components.

Dim(R/SS)
3
=======================
In fact we can check
that these are two prime ideals, S and SS.

So we have something like this:

So over the component were theorem fails we can further investigate our theorem

Elim([y,x[1],x[3]], Ideal(x[1] - x[2], x[2]^2 - 2x[2]a + x[3]a + yb, x[3]^2 + y^2 - x[3]a - yb,T))

Ideal(2x[2]^2 - 2x[2]a)
-------------------------------
Saturation(Ideal(x[1] - x[2], x[2]^2 - 2x[2]a + x[3]a + yb, x[3]^2 + y^2 - x[3]a - yb,x[2] ),Ideal(T))
Ideal(1)
-------------------------------
Saturation(Ideal(x[1] - x[2], x[2]^2 - 2x[2]a + x[3]a + yb, x[3]^2 + y^2 - x[3]a - yb,x[2]-a ),Ideal(T))
Ideal(1)
-------------------------------

So the theorem is true over such component if the construction degenerates (the origin is equal to the intersection point in the x-axis, everything collapses) or if x[2]=a, thus, the common point on the x-axis is a tangency point, this was expected and guessed by many!!!

And this component is described just by adding x[1] - x[2] to the given hypotheses

ReducedGBasis(Ideal(x[1] - x[2],H1,H2,H3))
[x[1] - x[2], x[3]^2 + y^2 - x[3]a - yb, x[2]^2 - 2x[2]a + x[3]a + yb]
--------------------
ReducedGBasis(Ideal(x[1] - x[2], x[2]^2 - 2x[2]a + x[3]a + yb, x[3]^2 + y^2 - x[3]a - yb))
[x[1] - x[2], x[3]^2 + y^2 - x[3]a - yb, x[2]^2 - 2x[2]a + x[3]a + yb]