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$.
Theorem 3.1. Let 1,2,3,4, and 5 be 5 points in the plane, such that 1,4, and 5 are not collinear. Then the following equivalence holds:$$[123]=0 ⇔ [124][135]=[125][134]$$Proof. The bracket is a 3-linear alternating form: Observe $a = [123][145]−[124][135]+[125][134].$ Fix 1 in $a$. Then $a$ is a 4-linear alternating form on {2,3,4,5}. However, there is no such thing as a non degenerate 4-linear alternating form in a 3-dimensional space, so $a = 0$. Since this implies [123][145]=[124][135]−[125][134] the theorem is proved. Using this theorem, we can translate a set of conditions of the form h(A,B,C) to biquadratic equations: [ABD][ACE] = [ABE][ACD] for any D and E such that A,D, and E are not collinear.
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.
Theorem 3.2. Observe the assertion m((A,B),(C,D),(E,F)). This means that the lines through A and B, C and D, and E and F go through one point. This assertion implies that all these 6 points and 3 lines are distinct, and that the point of concurrency is not one of A,B,C,D,E,F, thus implicitly adding non-degeneracy conditions every time we use this assertion.
This assertion is equivalent to, [ABC][CDE][EFA]=−[ABE][CDA][EFC], and to [ABF][CDE]=[ABE][CDF].
Proof. Observe the assertion m((A,B),(C,D),(E,F)), i.e. the lines through A and B, C and D, and E and F go through one point, say Z. This is equivalent to the combination of the three assertions h(A,B,Z),h(C,D,Z) and h(E,F,Z).
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}
[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.
Remark 3.3. Because of the implicit degeneration conditions introduced, we have to be careful when using m(..) as an assertion representing the thesis. Additionally, in practice it appears a proof using m(..) as configuration assertions is harder to understand than a proof using h(..) as configuration assertions. However, the m(..)-assertion still has the huge advantage that it represents three h(..)-assertions, thus considerably reducing the amount of configuration assertions and configuration equations. As this shows that using the m(..)-assertion has both advantages we do not want to loose and disadvantages we do not want to have, we chose to leave the choice to the user of Cinderella. When trying to obtain a proof, he can decide whether he wants to use m(..)-assertions in the configuration, and whether he wants to use m(..)-assertions in the thesis. This enables the user to find the ‘golden mean’ between the shortness and the clarity of the proof.
The next theorem describes how to encode six points on a conic into bracket expressions.
Theorem 3.4. Observe the assertion c(A,B,C,D,E,F), meaning that the six points A,B,C,D,E, and F are on one conic. This assertion implies that all these six points are distinct and
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]$$Proof. First, observe four distinct points, A,B,C, and D, and the two degenerate conics $c_1$ and $c_2$. The conic $c_1$ is given by the line through A and B and the line through C and D, the conic $c_2$ is given by the line through A and C and the line through B and D. For an arbitrary point $x$ we have $x∈c_1$ if and only if $x$ on AB or $x$ on CD, so $[ABx][CDx]=0$.\begin{equation}x ∈ c_2\text{ if and only if $x$ on AC or $x$ on BD, so }[ACx][BDx] = 0\end{equation}Now, for all $λ, µ ∈\mathbb R$, the equation $λ[ABx][CDx] + µ[ACx][BDx]$ describes a conic through A,B,C, and D. Now let\begin{align}\nonumber λ&= [ACE][BDE]\\µ&= −[ABE][CDE],\end{align}and observe the expression\begin{equation}[ACE][BDE][ABx][CDx] − [ABE][CDE][ACx][BDx].\end{equation}Since this is a bi-quadratic expression of degree two, which evaluates to zero for $x$∈{A,B,C,D,E}, this defines a conic on the points A,B,C,D, and E. This means F is on that conic if and only if\begin{equation}[ACE][BDE][ABF][CDF] = [ABE][CDE][ACF][BDF],\end{equation}which concludes the proof.
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 all 720 possible equations, as each of those equations is equivalent to the thesis.\begin{equation}\begin{array}l
[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}Example (Collinearity) Now suppose A,B, and C are collinear. Observe the complex numbers $z_1=r_1e^{iϕ_1}$ of the vector (B−A), and $z_2=r_2e^{iϕ_2}$ of (C−A). The points A,B, and C are collinear if and only if the two angles $ϕ_1$ and $ϕ_2$ are either the same or opposed to each other. This means $ϕ_1=ϕ_2$ or $ϕ_1=π+ϕ_2$, which means $z_1/z_2∈\mathbb R$, or equivalently\begin{equation}\frac{B-A}{C-A}=\overline{\left(\frac{B-A}{C-A}\right)}\end{equation}Using Equations 10 and 11 this is equal to\begin{equation}\frac{[B A I]}{[C A I]}=\frac{[B A J]}{[C A J]}\end{equation}which evaluates to,\begin{equation}[A B I][A C J]=[A C I][A B J]\end{equation}which indeed fulfills the claim at Theorem 3.1.
4.2 Circles
We will now show how to encode the fact that four points are on one circle in brackets.
Theorem 4.1. Suppose the four points A,B,C, and D are on one circle, then the following bracket equation holds:$$[ACI][BDI][ADJ][BCJ] = [BCI][ADI][ACJ][BDJ].$$This assertion will be denoted by ci(A,B,C,D).
Note that this matches the bracket equation for a conic through the points A,B,C,D,I, and J (See Theorem 3.4).
Proof. It is a well known theorem that four points A,B,C, and D are on one circle if and only if the angle between AC and BC is equal to the angle between AD and BD. We now switch to complex numbers as described in the start of this section, and find that this is equivalent to$$\frac{z_{A}-z_{C}}{z_{B}-z_{C}} / \frac{z_{A}-z_{D}}{z_{B}-z_{D}} \in \mathbb{R}$$with arguing as in the example on collinearity above. This equation can be rewritten to$$\frac{z_{A}-z_{C}}{z_{B}-z_{C}} / \frac{z_{A}-z_{D}}{z_{B}-z_{D}}=\overline{\frac{z_{A}-z_{C}}{z_{B}-z_{C}} / \frac{z_{A}-z_{D}}{z_{B}-z_{D}}}$$Using Equations 10 and 11 this transforms to$$[ACI][BDI][BCJ][ADJ] = [BCI][ADI][ACJ][BDJ],$$which concludes the proof.
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.
Example Suppose we have a configuration with the points A,B,C, and D. Then B:={[ABC],[ABD],[ACD],[BCD]} and $|B|=\dbinom43$.
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.
Remark 5.1. Note that it is almost always possible to express the thesis in various different equations. For the remainder of the section we will just pick one, for ease of reading. In practice we will test all of them, checking which gives us the shortest proof, if any.
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}Remark 5.2. In words: For each of the $n$ equations we multiply a certain power of the left sides with each other, and the same power of the right sides. Then all terms cancel, except for $(t_l)^q$ on the left side, and $(t_r)^q$ on the right side.
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 proof that the thesis logically follows from the configuration. In the next section it will be shown how we can obtain such a $g$.