3 Brackets and Projective Geometry

When we restrict ourselves to geometric theorems that are invariant under projective transformations, we can prove geometric theorems much faster than when we would have used

Gröbner bases. The method we use is based on a paper by Jürgen Richter-Gebert in 1995[8]. For now, we only consider configurations and theses of the form:

• The three points A,B, and C lie on one line (the points A,B, and C are collinear), denoted by ‘h(A,B,C)’,

• The three lines through A and B, C and D, and E and F, respectively, go through one point, denoted by ‘m((A,B),(C,D),(E,F))’,

• The six points A,B,C,D,E, and F lie on one conic, denoted by ‘c(A,B,C,D,E,F)’.

We again observe the homogeneous coordinates in the plane, elements of $\mathbb P^3$. This means the coordinates are in $(\mathbb R^3\setminus\{0\})/\mathbb R\setminus\{0\}$, in words: all scalar multiples of a vector denote the same point. We will denote the determinant $\left|\begin{array}{lll}x_{A} & x_{B} & x_{C} \\ y_{A} & y_{B} & y_{C} \\ z_{A} & z_{B} & z_{C}\end{array}\right|$ corresponding to the points A, B, and C by [ABC]. This notation is referred to as the bracket notation, a determinant [ABC] as a bracket. In the mathematical foundation in this section parts from the masters thesis by one of Jürgen Richter-Gebert’s students, Andreas Umbach, were consulted [10].

3.1 Collinearity

First, we focus on the collinearity conditions, described by h(A,B,C). It is commonly known that three points A,B, and C are collinear if and only if [ABC] = 0. To create a proof (as shown in the next section) we need to make a connection between several conditions. This can be done using the following theorem. In order to make reading easier, we write $k$ for the point defined by coordinates $(x_k, y_k, z_k)^T$.

This method of describing a geometry theorem implicitly introduces a number of nondegeneracy conditions. For example, the fact that 1,4, and 5 are not collinear. On the one hand, this is an advantage, as we do not have to express this kind of non-degeneracy conditions explicitly. On the other hand, this is a disadvantage, as we might add some nondegeneracy conditions we are not aware of and which might be unnecessary. However, in this specific situation the disadvantage seems less important, since the user will construct a certain theorem in Cinderella, thus (in general) avoiding degenerated cases himself.

3.2 Concurrency and Conics

In this section we show how to translate the assertions m((A,B),(C,D),(E,F)) and c(A,B,C,D,E,F) to bracket equations.

This assertion is equivalent to, [ABC][CDE][EFA]=−[ABE][CDA][EFC], and to [ABF][CDE]=[ABE][CDF].

Using Theorem 3.1 we find the following three equations. Notice how we have to use the fact that all 6 points are distinct and none of them is the point of concurrency.\begin{align}

\nonumber[ABC][AZE]=[ABE][AZC],\\

\nonumber[CDE][CZA]=[CDA][CZE],\\

[EFA][EZC]=[EFC][EZA].\end{align}We multiply the left- and right-hand sides and cancel terms that occur on both sides, and obtain\begin{equation}[ABC][CDE][EFA]=−[ABE][CDA][EFC],\end{equation}thus proving the first equation.

As m((A,B),(C,D),(E,F)) is equivalent to (for example) the assertion m((A,B),(C,D),(F,E)) we obtain from Equation 2:\begin{equation}−[ABF][CDA][FEC]=[ABC][CDF][FEA].\end{equation}Again, we multiply the left- and right-hand sides from Equations 2 and 3 and cancel terms that occur on both sides, and we obtain\begin{equation}[ABF][CDE]=[ABE][CDF],\end{equation}which proves the second equation of the theorem.

We just showed two possible encodings of the m(..)-assertion. However, it appears that using only the second one suffices in practice. An assertion m(..) gives us only three different instances of Equation 4, all other permutations are equivalent to one of those three.

The next theorem describes how to encode six points on a conic into bracket expressions.

no three of the points are collinear, thus implicitly adding non-degeneracy conditions every time we use this assertion.

This assertion is equivalent to the following bracket equation$$[ACE][BDE][ABF][CDF] = [ABE][CDE][ACF][BDF]$$

In general, a single c(..)-assertion gives us 6!=720 possible equations. However, in the configuration a basis of the subspace spanned by these 720 equations will suffice. Such a basis is a set of equations such that the other equations can be obtained by multiplying sides and removing pairs that occur on both sides. With basic linear algebra we can obtain a basis for this [10, p. 36]. The basis can be found in Table 1. So, every c(..)-assertion only adds five equations to the set of configuration equations. However, if the thesis is a c(..)-assertion, we have to include

[ABC][ADE][BDF][CEF] = [ABD][ACE][BCF][DEF],\\

[ABE][ACD][BDF][CEF] = [ABD][ACE][BEF][CDF],\\

[ABE][BCD][ADF][CEF] = [ABD][BCE][AEF][CDF],\\

[ABD][AEF][BCF][CDE] = [ABF][ADE][BCD][CEF],\\

[ABE][ACF][BDF][CDE] = [ABF][ACE][BDE][CDF].\\\\\quad\text{Table 1: A basis for c(..)-assertions in the configuration}\end{array}\end{equation}4 Non-Projective Geometry

In this section we present some theory that enables us to represent assertions in non-projective geometry in brackets. Someone might think that calculating with expressions that are invariant with respect to linear transformations, as described in the previous chapter, automatically makes it impossible to prove any theorems containing for example circles. This is not such a strange thought, since circles might become conics (and lose their circularity) under linear transformations. However, by adding two special points to the configuration, we can prove such theorems.

4.1 Complex Numbers

With the following procedure we can use complex numbers to express conditions involving distances, angles, etc. Given a point $P = (x, y) ∈\mathbb R^2$ in the plane, we define $z_p∈\mathbb C := x+iy$. Moreover, $z_p = r · e^{iϕ}$ for certain $r,ϕ∈\mathbb R$. We know $z∈\mathbb R ⇔ z =\bar z$, and $z ∈ i\mathbb R ⇔ z = −\bar z$.

We go back to homogeneous coordinates and introduce two new ‘points’: $I = (i, −1, 0)$ and $J = (−i, −1, 0)$. Now observe the bracket [ABI], where $A = (x_a, y_a, 1)$ and $B = (x_b, y_b, 1)$:\begin{equation}[A B I]=\left|\begin{array}{ccc}x_{a} & x_{b} & i \\ y_{a} & y_{b} & -1 \\ 1 & 1 & 0\end{array}\right|=x_{a}+i y_{a}-x_{b}-i y_{b}=z_{a}-z_{b}\end{equation}Likewise, the bracket [ABJ] evaluates to\begin{equation}[A B J]=\left|\begin{array}{ccc}x_{a} & x_{b} & -i \\ y_{a} & y_{b} & -1 \\ 1 & 1 & 0\end{array}\right|=x_{a}-i y_{a}-x_{b}+i y_{b}=\overline{z_{a}-z_{b}}\end{equation}

4.2 Circles

We will now show how to encode the fact that four points are on one circle in brackets.

Note that this matches the bracket equation for a conic through the points A,B,C,D,I, and J (See Theorem 3.4).

5 The Prover

Suppose we are given a certain theorem in planar geometry, containing points and some collinearity conditions. This means we know that certain brackets (i.e. expressions of the form [ABC]) are equal to zero. We define B to be the set of all brackets, i.e. all combinations of three points from the geometry theorem, so $|B| =\dbinom p3$, where $p$ denotes the number of points in the configuration.

Suppose we have a geometry statement, and by Theorems 3.1, 3.2 and 3.4 we obtained a set of $n$ equations following from the configuration\begin{equation}\begin{array}cc_{1 l} & \equiv & c_{1 r} \\ c_{2 l} & \equiv & c_{2 r} \\ & \vdots & \\ c_{n l} & \equiv & c_{n r}\end{array}\end{equation}where ‘l’ denotes the left hand side of the equation, and ‘r’ the right hand side. Each of the factors of the cil and cir denotes a determinant of three points in the geometry statement, so each ci,l/r is a product of elements of B. Note that we use the equivalence sign ‘≡’ rather than

the normal equation sign ‘=’ to make it clear that we are calculating with brackets, elements of B, rather than with the elements in R or Q they evaluate to. From Theorem 3.1 it follows directly that each of the factors of the cil and cir is not equal to zero. Moreover, we have an (at least one) equation that implies the thesis we want to test:\begin{equation}t_{l} \equiv t_{r}\end{equation}Note that all factors in $t_{l,r}$ should be a factor of at least one $c_{i,l/r}$. This means that the brackets in the thesis equation should occur somewhere in the configuration equation.

Now suppose we have a certain oracle that gives us a vector $g∈\mathbb Q^n, g\ne0$ such that\begin{equation}\frac{1}{t_{l}} \prod_{i=1}^{n}\left(c_{i l}\right)^{g_{i}} \equiv \frac{1}{t_{r}} \prod_{i=1}^{n}\left(c_{i r}\right)^{g_{i}}\end{equation}By multiplying both sides by the greatest common divisor $q$ of the denominators in $g_1,\cdots,g_n$, thus clearing the denominators, we obtain the following equation:\begin{equation}\left(\frac{1}{t_{l}}\right)^{q} \prod_{i=1}^{n}\left(c_{i l}\right)^{v_{i}} \equiv\left(\frac{1}{t_{r}}\right)^{q} \prod_{i=1}^{n}\left(c_{i r}\right)^{v_{i}} \text {, where } v_{i}=q \cdot g_{i} \text {, so } v_{i} \in \mathbb{Z}\end{equation}

By the definition of the $c_{i,l/r}$ we know\begin{equation}\left(c_{i l}\right)^{a} \equiv\left(c_{i r}\right)^{a} \quad \forall 1 \leq i \leq n, \forall a \in \mathbb{Z}\end{equation}and since q≠0 we obtain from Equation 18:\begin{equation}\left(\frac{1}{t_{l}}\right)^{q} \equiv\left(\frac{1}{t_{r}}\right)^{q}, \quad \text { so } t_{l} \equiv t_{r}\end{equation}This means such a vector $g ∈\mathbb Q^n$ gives us a verifiable