{
 "cells": [
  {
   "cell_type": "markdown",
   "id": "19b8b35a",
   "metadata": {},
   "source": [
    "# The 17th Roots of Unity\n",
    "\n",
    "The regular $17$-gon is constructible because\n",
    "$17=2^{2^2}+1$ is a Fermat prime. Algebraically, the Galois group\n",
    "of\n",
    "\n",
    "$$\n",
    "\\Phi_{17}(x)=x^{16}+x^{15}+\\cdots+x+1\n",
    "$$\n",
    "\n",
    "has order $16$. A chain of index-two subgroups therefore resolves\n",
    "a primitive root using square roots alone.\n"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "19fc5f6d",
   "metadata": {},
   "source": [
    "## Eight real Gaussian periods\n",
    "\n",
    "Let $\\zeta=\\exp(2\\pi i/17)$. Pairing each power with its inverse\n",
    "gives eight real quantities\n",
    "\n",
    "$$\n",
    "a_k=\\zeta^k+\\zeta^{-k}=2\\cos(2\\pi k/17).\n",
    "$$\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "id": "e285ff5e",
   "metadata": {},
   "outputs": [],
   "source": [
    "def z : MathValue := rtu 17\n",
    "\n",
    "def a1 : MathValue := z ^ 1 + z ^ 16\n",
    "def a2 : MathValue := z ^ 2 + z ^ 15\n",
    "def a3 : MathValue := z ^ 3 + z ^ 14\n",
    "def a4 : MathValue := z ^ 4 + z ^ 13\n",
    "def a5 : MathValue := z ^ 5 + z ^ 12\n",
    "def a6 : MathValue := z ^ 6 + z ^ 11\n",
    "def a7 : MathValue := z ^ 7 + z ^ 10\n",
    "def a8 : MathValue := z ^ 8 + z ^ 9\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "id": "7316c9f1",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/html": [
       "$-1$"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "a1 + a2 + a3 + a4 + a5 + a6 + a7 + a8\n"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "e9d764e0",
   "metadata": {},
   "source": [
    "## Successive two-point transforms\n",
    "\n",
    "The multiplicative group modulo $17$ is cyclic. The definitions\n",
    "below follow its subgroup chain, repeatedly recording sums and\n",
    "differences. At the top level $d_{10}$ is the sum of all sixteen\n",
    "nontrivial roots and hence equals $-1$.\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "id": "71b31950",
   "metadata": {},
   "outputs": [],
   "source": [
    "def b11 : MathValue := a1 + a4\n",
    "def b12 : MathValue := a1 - a4\n",
    "def b21 : MathValue := a2 + a8\n",
    "def b22 : MathValue := a2 - a8\n",
    "def b31 : MathValue := a3 + a5\n",
    "def b32 : MathValue := a3 - a5\n",
    "def b41 : MathValue := a6 + a7\n",
    "def b42 : MathValue := a6 - a7\n",
    "\n",
    "def c11 : MathValue := b11 + b21\n",
    "def c12 : MathValue := b11 - b21\n",
    "def c21 : MathValue := b31 + b41\n",
    "def c22 : MathValue := b31 - b41\n",
    "\n",
    "def d10 : MathValue := c11 + c21\n",
    "def d11 : MathValue := c11 - c21\n",
    "def d12 : MathValue := c21 - c11\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "id": "911de8f0",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/html": [
       "$(-1, -2 rtu(17)^{14} - 2 rtu(17)^{12} - 2 rtu(17)^{11} - 2 rtu(17)^{10} - 2 rtu(17)^{7} - 2 rtu(17)^{6} - 2 rtu(17)^{5} - 2 rtu(17)^{3} - 1, 2 rtu(17)^{14} + 2 rtu(17)^{12} + 2 rtu(17)^{11} + 2 rtu(17)^{10} + 2 rtu(17)^{7} + 2 rtu(17)^{6} + 2 rtu(17)^{5} + 2 rtu(17)^{3} + 1)$"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "(d10, d11, d12)\n"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "bfb93da0",
   "metadata": {},
   "source": [
    "## Invert the subgroup chain\n",
    "\n",
    "Each difference has a square that can be expressed using quantities\n",
    "already known one level higher. Choosing compatible square-root\n",
    "branches and repeatedly applying\n",
    "\n",
    "$$\n",
    "u=\\frac{(u+v)+(u-v)}{2}\n",
    "$$\n",
    "\n",
    "reconstructs the first period $a_1$.\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "id": "0effda84",
   "metadata": {},
   "outputs": [],
   "source": [
    "def d10' : MathValue := -1\n",
    "def d11' : MathValue := sqrt 17\n",
    "\n",
    "def c11' : MathValue := (d10' + d11') / 2\n",
    "def c21' : MathValue := (d10' - d11') / 2\n",
    "def c12' : MathValue := sqrt (8 + (- c11'))\n",
    "def c22' : MathValue := sqrt (8 + (- c21'))\n",
    "\n",
    "def b11' : MathValue := (c11' + c12') / 2\n",
    "def b21' : MathValue := (c11' - c12') / 2\n",
    "def b31' : MathValue := (c21' + c22') / 2\n",
    "def b41' : MathValue := (c21' - c22') / 2\n",
    "\n",
    "def b12' : MathValue := sqrt (4 + b21' + (-2) * b31')\n",
    "def b22' : MathValue := sqrt (4 + b21' + (-2) * b41')\n",
    "def b32' : MathValue := sqrt (4 + b41' + (-2) * b21')\n",
    "def b42' : MathValue := sqrt (4 + b31' + (-2) * b21')\n",
    "\n",
    "def a1' : MathValue := (b11' + b12') / 2\n"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "39231b18",
   "metadata": {},
   "source": [
    "## Gauss's cosine formula\n",
    "\n",
    "Since $a_1'=2\\cos(2\\pi/17)$, dividing by two displays the classical\n",
    "nested-square-root construction of the regular $17$-gon:\n",
    "\n",
    "$$\n",
    "\\cos\\frac{2\\pi}{17}\n",
    "=\\frac1{16}\\left(\n",
    "  -1+\\sqrt{17}+\\sqrt{34-2\\sqrt{17}}\n",
    "  +2\\sqrt{17+3\\sqrt{17}-\\sqrt{34-2\\sqrt{17}}\n",
    "    -2\\sqrt{34+2\\sqrt{17}}}\n",
    "\\right).\n",
    "$$\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "id": "887f336c",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/html": [
       "$\\frac{1}{16} \\sqrt{-\\sqrt{17} + 17} \\sqrt{2} + \\frac{1}{16} \\sqrt{17} + \\frac{1}{8} \\sqrt{-\\sqrt{-\\sqrt{17} + 17} \\sqrt{2} - 2 \\sqrt{\\sqrt{17} + 17} \\sqrt{2} + 3 \\sqrt{17} + 17} + \\frac{-1}{16}$"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "a1' / 2\n"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "4ef0a2dd",
   "metadata": {},
   "source": [
    "## Root-of-unity check\n",
    "\n",
    "Egison's exact root-of-unity value retains the defining relation\n",
    "without numerical rounding.\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "id": "bb7d35f4",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/html": [
       "$1$"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "z ^ 17\n"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "21ea4efa",
   "metadata": {},
   "source": [
    "## Takeaway\n",
    "\n",
    "The nested radicals are a direct trace of four successive\n",
    "index-two reductions in the Galois group. The computation explains\n",
    "not only the value of the cosine but also why straightedge-and-\n",
    "compass construction is possible.\n"
   ]
  }
 ],
 "metadata": {
  "kernelspec": {
   "display_name": "Egison",
   "language": "egison",
   "name": "egison"
  },
  "language_info": {
   "codemirror_mode": "egison",
   "file_extension": ".egi",
   "mimetype": "text/x-egison",
   "name": "egison"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 5
}