Comment by Animats

"Polish this paper. Check all proofs with Lean. Try to find shorter proofs of lemmas where possible. Write for a undergraduate math student. Add brief explanatory material as needed. Cite previous work where relevant. Check all citations. Convert to LaTeX."