Morley’s Theorem and real algebraic geometry

Consider the following attempt at a thought-free'' proof of Morley's Theorem.

Let $(x_1,y_1)$, $(x_2,y_2)$ and $(x_3,y_3)$ denote three vertices of a generic triangle.

Let $(a_1,b_1)$, $(a_2,b_2)$ and $(a_3,b_3)$ denote three more points in the plane.

For all $\lbrace i,j,k\rbrace=\lbrace 1,2,3\rbrace$, we want to impose the condition that the line determined by $(x_i,y_i)$ and $(a_k,b_k)$ bisects the angle from $(a_j,b_j)$ to $(x_i,y_i)$ to $(x_j,y_j)$. Capturing this algebraically amounts to equating two squared cosines: $$\frac{((x_i-a_k)(x_i-a_j)+(y_i-b_k)(y_i-b_j))^2} {((x_i-a_k)^2+(y_i-b_k)^2)((x_i-a_j)^2+(y_i-b_j)^2)}$$ $$= \frac{((x_i-a_k)(x_i-x_j)+(y_i-b_k)(y_i-x_j))^2} {((x_i-a_k)^2+(y_i-b_k)^2)((x_i-x_j)^2+(y_i-x_j)^2)}$$ which simplifies first to $$((x_i-a_k)(x_i-a_j)+(y_i-b_k)(y_i-b_j))^2((x_i-x_j)^2+(y_i-x_j)^2)$$ $$- ((x_i-a_k)(x_i-x_j)+(y_i-b_k)(y_i-x_j))^2((x_i-a_j)^2+(y_i-b_j)^2)=0.$$ Then expanding the left side and dividing out by the condition $$-a_jy_i - b_jx_j + x_ib_j - x_ix_j + y_ix_j + a_jx_j$$ (of having $(a_j,b_j)$,$(x_i,y_i)$ and $(x_j,y_j)$ collinear) leaves $$C_{ijk}:=a_jy_i^3-x_i^3b_j+2x_ix_jy_ib_j-2x_ia_jy_ix_j-2a_ky_i^3+2x_i^3b_k+b_k^2x_ix_j+y_i^3x_j-x_i^3x_j$$ $$-a_k^2y_ix_j+2a_kx_ib_kx_j-2a_kx_jb_ky_i-2a_kb_kb_jy_i+2x_ja_kb_kb_j+2x_jb_ky_ib_j-2x_ja_ky_ib_j$$ $$-2x_jx_ib_kb_j+2a_ky_i^2b_j-a_k^2x_ib_j+2a_kx_i^2b_j+b_k^2x_ib_j-2b_k^2y_ix_i+2a_k^2x_iy_i+x_ja_k^2b_j$$ $$-x_jb_k^2b_j-a_jx_jb_k^2+a_jx_ja_k^2-a_ja_k^2y_i+a_jb_k^2y_i-2a_jb_kx_i^2-2a_jb_ky_i^2-2x_ja_kx_ib_j$$ $$+2a_jx_ja_ky_i-2a_jx_ja_kb_k-2a_jx_ja_kx_i+2a_jx_jb_ky_i+2a_jx_ib_kx_j+2a_ja_kx_ib_k+2a_kx_jy_i^2$$ $$-2y_i^2b_kx_j+b_k^2y_ix_j+2x_i^2a_kx_j+x_i^2y_ix_j-2x_i^2b_kx_j-x_ix_jy_i^2-a_k^2x_ix_j+x_i^2x_ja_j$$ $$-x_jy_i^2b_j+a_jy_ix_i^2-a_jy_i^2x_j+x_i^2b_jx_j-x_ib_jy_i^2-2a_kb_kx_i^2+2a_kb_ky_i^2-2a_ky_ix_i^2+2x_ib_ky_i^2\ .$$

Now for Morley's theorem we would like to conclude that points $(a_1,b_1)$, $(a_2,b_2)$ and $(a_3,b_3)$ form an equilateral triangle. We can easily write down polynomials in $a_1,b_1,a_2,b_2,a_3$ and $b_3$ all of whose vanishing would capture this. For example, it would suffice to prove the vanishing of $$I_{123}:=-2a_1a_2+a_2^2+2b_1^2-2b_1b_2+b_2^2+2a_1a_3-a_3^2-2b_1b_3+b_3^2\ .$$

Since we hope $I_{123}$ will vanish whenever $C_{123},C_{213},C_{312},C_{132},C_{231},C_{321}$ do, we look to find $I_{123}$ in (the radical of) the ideal $$C:=\langle C_{123},C_{213},C_{312},C_{132},C_{231},C_{321}\rangle.$$ Unfortunately, as one can see from the above, all the generators of $C$ vanish if $x_1=y_1=x_2=y_2=x_3=y_3=0$, and so the same must hold for every element of $C$. Nevertheless $I_{123}$ does not vanish on this condition.

The classical nullstellensatz leaves only one way out: the vanishing of $I_{123}$ doesn't follow from the vanishing of all the $C_{ijk}$ without the exploitation of some restriction on the range of the variables such as confining them to the reals.

Question: What insight does the machinery of real algebraic geometry shed on the shape of a proof of Morley's Theorem along the lines of this sketch?

-
Real algebraic geometry is not needed for most elementary geometrical theorems. Either interpret statements as "if A then B" as "at least one irreducible component of the variety which describes the solution set of A also satisfies B". Or, which is simpler, make the theorem into a purely polynomial-identity type statement (so there is no A but only B) by using the correct starting variables. In the case of Morley, start with three angles adding up to 60°, instead of the original triangle (so the original triangle's angle will be 3 times these angles), and you won't have to trisect anything. – darij grinberg Apr 17 2012 at 4:41
The first method bears the name of Wu Wen-Tsün (modulo spelling) and uses Gröbner bases. Sorry for not being more detailed (and I won't be able to elaborate for a while); I hope these are enough keywords to google for. – darij grinberg Apr 17 2012 at 4:44
Only marginally related to your question, but Patrick Ion would argue that the "right" thought-free way of proving such theorems of geometry does not lie with polynomial system solving but rather through the Discrete Fourier Transform. See e.g.: ams.org/samplings/feature-column/fcarc-geo-dft – Thierry Zell Apr 17 2012 at 15:09

This isn't a matter of real versus complex geometry -- the equations you give aren't enough to encode Morley's theorem over the reals. Let $z_1 z_2 z_3$ be our original triangle; I will use indices that are cyclic modulo $3$. Let $\ell^0_i$ be the trisector of the angle at $z_i$ which is closer to $z_{i-1}$ and let $m^0_i$ be the trisector which is closer to $z_i$. Let $\ell^1_i$ and $\ell^2_i$ be the rotations of $\ell^0_i$ by $120^{\circ}$ and $240^{\circ}$, and define $m^1_i$ and $m^2_i$ likewise.

For $r=1$, $2$ and $3$, let $(\delta_r, \epsilon_r)$ equal to one of $(0,0)$, $(1,2)$ or $(2,1)$. Let $c_r$ be the intersection of $m^{\epsilon_r}_r$ and $\ell^{\delta_{r+1}}_{r+1}$. Then $\angle z_r z_{r+1} c_r = \angle c_r z_{r+1} c_{r+1} = \angle c_{r+1} z_{r+1} z_{r+2}$ so your equations hold for $(x_r, y_r) = z_r$ and $(a_r, b_r) = c_r$.

Of the $81$ possible choices for $(\delta_r, \epsilon_r)$, I believe that the triangle $c_1 c_2 c_3$ is equilateral only for $54$ of them. I am basing this on Connes' proof of Morley's theorem, where a key hypothesis is that $$\sum_{r=1}^3 \angle c_{r-1} z_{r} c_{r} = \pm 60^{\circ} \ \mbox{not} \ 180^{\circ}.$$ Connes' rotation $g_r$ is a rotation around $z_r$ by angle $2 \angle c_{r-1} z_{r} c_{r}$, so what he says is that $g_1 g_2 g_3$ should be a nontrivial rotation.

It's easy enough to encode this condition algebraically. (If you have trouble with it I'll write more, but I bet you won't.) Once you do that, I think it should be easy to convert Connes proof into the sort of proof you are looking for. You'll also need to impose that certain things are nonzero, because Connes divides at times.

-
 This seems basically right to me...but why 81 and 54 rather than 108 and 72? One can stage Morley's theorem in the closed triangle or in any of 3 external triangles, making 4 altogether, with 27 choices of trisectors in each case, of which 18 satisfy the "key hypothesis." Right? – David Feldman Apr 18 2012 at 1:13