I am taking a break from writing and working on my Lean project on \(Out(F_n)\) to instead work on fun Project Euler problems on the weekends (turns out programming and debugging for the majority of the working day does not lend itself very well to writing Lean in the post work hours). Project Euler is a good substitute on the weekends: they have a good mix of fun and interesting math, and I can go nuts optimizing away the final program to make it run as fast as possible. Problem 208 had a 70% difficulty rating, and involved some interesting math: I figured it might be worthwhile recording my solution on the blog.

I won't replicate the full problem statement here, since it's already available via the link, but here's a more concise mathematical description. We have an action on \(S^1 \mathbb{R}^2\) (the unit tangent bundle over \(\mathbb{R}^2\)), generated by two generators TL (turn left) and TR (turn right), where the TL action moves the tangent vector \(\frac{2\pi}{5}\) radians along a unit circle counterclockwise, and the TR action moves it the same way clockwise.

Question: How many length 70 trajectories bring the tangent vector to the original basepoint \((0,0)\)?

The naïve way to do this in a programming language that does not support working over mathematical fields (that are not \(\mathbb{Q}\)) would be to represent the basepoint of the tangent vector as a pair of floats, and the direction as an int (really, and element of \(\mathbb{Z}/5\mathbb{Z}\)), and then enumerate over all length 70 paths to see which of them end up at the starting basepoint. This is both slow, since it involves searching over \(2^70\) paths, and also likely to be incorrect, because floating point roundoff errors might erroneously lead you to believe that you are not at the starting point, even though you actually are.

There are (at least) two more mathematically sophisticated approaches that lead to better algorithms: I went with the latter one, but I also feel obligated to list the former since it's closely related to the work I did for my PhD.

Approach 1: A \(\mathrm{GL}_2(\mathbb{R})\) representation

Since we're looking at an isometric group action on \(S^1 \mathbb{R}^2\) generated by TR and TL, the action must factor through \(\mathrm{GL}_2(\mathbb{R})\), since that is the full group of isometries of \(S^1\mathbb{R}^2\). The image of \(\langle \mathrm{TL}, \mathrm{TR} \rangle\) forms a subgroup of \(\mathrm{GL}_2(\mathbb{R})\), and we can explicitly compute the relations between these two elements to get a presentation for the generated group \(\langle \mathrm{TL}, \mathrm{TR} \rangle\). The problem now reduces to determinining the length 70 words in this group which are trivial (with the additional constraint that we only use the words, and not their inverses). While word problems are aribtrary presented groups are undecidable, in this case, not only are they decidable, but there are fast automata based algorithms for solving the word problem, because the group is automatic.

I decided not to go with this approach, since I have worked with automatic groups in the past in a computational setting so the novelty was not a motivating factor, and the automata based approach seemed overkill.

Approach 2: Chebyshev polynomials and vector spaces over \(\mathbb{Q}\)

Consider now a point \((p, \theta)\) in \(S^1\mathbb{R}^2\), where \(p\) is the basepoint, and \(\theta\) the direction the tangent vector is pointing in: since we only ever need to consider \(\theta \in \left[ \frac{2\pi}{5}, \frac{4\pi}{5}, \frac{6\pi}{5}, \frac{8\pi}{5}, 0 \right]\), we can explicitly compute the effects of the TR and TL action on these points.

TL Initial point TR
\((p + v_5, \frac{2\pi}{5})\) \((p, 0)\) \((p + v_1, \frac{8\pi}{5})\)
\((p + v_4, \frac{4\pi}{5})\) \((p, \frac{2\pi}{5})\) \((p + v_5, 0)\)
\((p + v_3, \frac{6\pi}{5})\) \((p, \frac{4\pi}{5})\) \((p + v_4, \frac{2\pi}{5})\)
\((p + v_2, \frac{8\pi}{5})\) \((p, \frac{6\pi}{5})\) \((p + v_3, \frac{4\pi}{5})\)
\((p + v_1, 0)\) \((p, \frac{8\pi}{5})\) \((p + v_2, \frac{6\pi}{5})\)

Here, the vectors \(v_i\) for \(i \in \{1,2,3,4,5\}\) are the counter-clockwise oriented edges of a pentagon inscribed inside a unit circle centered at the origin in \(\mathbb{R}^2\), such that one of the vertices is at \((1, 0)\).

Claim: The vectors \(\{v_i\}_{i=1}^{5}\) span a \(4\) dimensional vector space over \(\mathbb{Q}\), and the only relation they satisfy is \(\sum_{i=1}^5 v_i = 0\).

Before we sketch out a proof of this claim, let's see why this is computationally useful. This claim lets us convert a group action on \(S^1 \mathbb{R}^2\) into an action on \(\mathbb{Z}^4 \times \mathbb{Z}/5\mathbb{Z}\). Here the 4 \(\mathbb{Z}\) coordinates are the coefficients in \(v_1\), \(v_2\), \(v_3\), and \(v_4\), and the \(\mathbb{Z}/5\mathbb{Z}\) coordinate is the direction. Now to compute the number of length 70 paths that brings the tangent vector back to its starting point is a matter of search over a \(L^\infty\) ball of radius \(70\) in this new space, i.e. a search over \(70^4\) terms. And even this is a crude upper bound: the actual program ends up searching over much smaller space. For context, the program resulting from this claim ends up running 650 ms on a 2012 era laptop processor.

Proof of claim: Observe that the \(x\) coordinates of the vectors are terms in \(\cos\left(\frac{2\pi}{5}\right)\) and \(\cos\left(\frac{4\pi}{5}\right)\), and the \(y\)-coordindates are terms in \(\sin\left(\frac{2\pi}{5}\right)\) and \(\sin\left(\frac{4\pi}{5}\right)\). In fact, after moving terms around, it suffices to show that \(\cos\left(\frac{2\pi}{5}\right)\) and \(\cos\left(\frac{4\pi}{5}\right)\) are linearly independent over \(\mathbb{Q}\), and the same holds for the \(\sin\) terms as well.

This is where Chebyshev polynomials come in: Chebyshev polynomials are precisely the relationship between cosines of angles, and cosines of an integer multiple of an angle. More precisely, the \(n\)th Chebyshev polynomial of the first kind \(T_n\) satisfies the following relation.

$$\cos(nx) = T_n(\cos(x))$$

In particular, we have that \(\cos\left(\frac{2\pi}{5}\right)\) and \(\cos\left(\frac{4\pi}{5}\right)\) are roots of the polynomial \(q(x) = T_5(x) - 1\). Looking up the coefficients of \(T_5\) on OEIS, we have that \(q(x)\) is the following.

$$q(x) = 16x^5 - 20x^3 + 5x - 1$$

Note that one of the roots of this polynomial is \(x=1\): this is a simple root and does not correspond to either of \(\cos\left(\frac{2\pi}{5}\right)\) or \(\cos\left(\frac{4\pi}{5}\right)\). One can show that there are two other roots, both of which have multiplicity greater than 1: those two roots must be \(\cos\left(\frac{2\pi}{5}\right)\) and \(\cos\left(\frac{4\pi}{5}\right)\), and since those two roots have multiplicity, we can compute them by computing the roots of \(q'(x)\). The roots of \(q'(x)\) can be computed by hand, since it's really a quadratic in disguise. Computing the two roots, we see that they are rationally independent. A similar argument works for the \(\sin\) version as well, which proves the claim.


Notes on learning Lean (4/?)

Posted: Wed 12 June 2024
Filed under mathematics
Tags: lean

Updates on learning Lean

I have now made it all the way to the end of the metric spaces chapter of the MIL, which means in principle, I should have everything I needed from the book to start the \(Out(F_n)\) project. The last exercise in the section was formalizing …

read more

Notes on learning Lean (3/?)

Posted: Thu 09 May 2024
Filed under mathematics
Tags: lean

Now that I'm done writing and defending my thesis (and submitting the associated paper to a journal), I can dive back into Lean full time (for the next few months at least). I just wrapped up Chapter 5 of MIL, and the final theorem of the chapter, namely the fact …

read more

Notes on learning Lean (2/?)

Posted: Mon 26 February 2024
Filed under mathematics
Tags: lean

On how Lean gave me the hypotheses I needed to prove a correct theorem

Working my way through Mathematics in Lean, I came across an exercise that required proving the standard monomial summation identities, e.g. \(\sum_{i=1}^{n} i = \frac{n(n+1)}{2}\), and \(\sum_{i=1 …

read more

Notes on learning Lean (1/?)

Posted: Tue 13 February 2024
Filed under mathematics
Tags: lean

Now that I am almost done with my dissertation, I have decided to switch focus and concentrate on doing math that can be formally checked by the Lean Theorem Prover. The ideal sub-field of math for me to start formalizing would be Teichüller theory, and results on mapping class groups …

read more

Counting orbit points (part 3): Asymptotics for convex-cocompact groups

Posted: Sun 12 January 2020
Filed under mathematics
Tags: geometry dynamics topology

In the previous post, we proved Sullivan's shadow lemma, which gave us concrete estimates for special subsets of the boundary, namely shadows. Recall that the shadow of a ball of radius \(r\) based at \(y\), with the source at \(x\), denoted by \(\mathcal{O}_r(x, y)\), is the set …

read more