{
 "cells": [
  {
   "cell_type": "markdown",
   "id": "3ab7f4fc",
   "metadata": {},
   "source": [
    "# Wodzicki–Chern–Simons Invariant on the Thurston Example\n",
    "\n",
    "This notebook reproduces the symbolic computation in Section 4 of\n",
    "*Diffeomorphism Groups of Circle Bundles over Integral Symplectic\n",
    "Manifolds*.  It builds the metric, curvature, and lifted curvature\n",
    "tensor and then reduces the Wodzicki–Chern–Simons integrand to a\n",
    "compact rational expression.\n",
    "\n",
    "The original research program is maintained in\n",
    "[EMR-Paper-Computation](https://github.com/egisatoshi/EMR-Paper-Computation).\n"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "a1b172c6",
   "metadata": {},
   "source": [
    "## Thurston metric\n",
    "\n",
    "Write $\\beta=1+\\theta_2-\\theta_2^2$.  The metric and inverse metric\n",
    "below are expressed in the coordinate frame\n",
    "$(\\theta_1,\\theta_2,\\theta_3,\\theta_4)$.  Quoting the two recurring\n",
    "polynomial expressions keeps the intermediate tensor calculation\n",
    "compact.\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "id": "e6d0a621",
   "metadata": {},
   "outputs": [],
   "source": [
    "declare symbol θ₁, θ₂, θ₃, θ₄, κ, p\n",
    "\n",
    "def x~i := [| θ₁, θ₂, θ₃, θ₄ |]~i\n",
    "def β := `(1 + θ₂ - θ₂^2)\n",
    "\n",
    "def g_i_j :=\n",
    "  [|[| 1, 0, 0, 0 |],\n",
    "    [| 0, 1, 0, 0 |],\n",
    "    [| 0, 0, κ / sqrt β, (-1 * θ₂ * κ) / sqrt β |],\n",
    "    [| 0, 0, (-1 * θ₂ * κ) / sqrt β, (`(1 + θ₂) * κ) / sqrt β |]|]\n",
    "\n",
    "def g~i~j :=\n",
    "  [|[| 1, 0, 0, 0 |],\n",
    "    [| 0, 1, 0, 0 |],\n",
    "    [| 0, 0, `(1 + θ₂) / (κ * sqrt β), θ₂ / (sqrt β * κ) |],\n",
    "    [| 0, 0, θ₂ / (sqrt β * κ), 1 / (sqrt β * κ) |]|]\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "id": "6b7aea4b",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/html": [
       "$\\begin{pmatrix} 1 & 0 & 0 & 0 \\\\ 0 & 1 & 0 & 0 \\\\ 0 & 0 & \\sqrt{(-θ₂^{2} + θ₂ + 1)}^{-1} κ & -\\sqrt{(-θ₂^{2} + θ₂ + 1)}^{-1} θ₂ κ \\\\ 0 & 0 & -\\sqrt{(-θ₂^{2} + θ₂ + 1)}^{-1} θ₂ κ & \\sqrt{(-θ₂^{2} + θ₂ + 1)}^{-1} (θ₂ + 1) κ \\\\ \\end{pmatrix}_{\\#\\#}^{\\;\\;}$"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "g_#_#\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "id": "0509336a",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/html": [
       "$\\begin{pmatrix} 1 & 0 & 0 & 0 \\\\ 0 & 1 & 0 & 0 \\\\ 0 & 0 & -(-θ₂^{2} + θ₂ + 1)^{-1} θ₂^{2} + (-θ₂^{2} + θ₂ + 1)^{-1} (θ₂ + 1) & 0 \\\\ 0 & 0 & 0 & -(-θ₂^{2} + θ₂ + 1)^{-1} θ₂^{2} + (-θ₂^{2} + θ₂ + 1)^{-1} (θ₂ + 1) \\\\ \\end{pmatrix}$"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "withSymbols [i, j, k] g_i_j . g~j~k\n"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "54a496ff",
   "metadata": {},
   "source": [
    "## Levi-Civita connection and curvature\n",
    "\n",
    "Egison's symbolic tensor indices transcribe the usual formulas\n",
    "\n",
    "$$\n",
    "\\Gamma^c{}_{ab}=\\frac12g^{ce}\n",
    "  (\\partial_ag_{be}+\\partial_bg_{ae}-\\partial_eg_{ab}),\n",
    "$$\n",
    "\n",
    "followed by $R_{ijk}{}^l$.  Repeated upper and lower indices are\n",
    "contracted by `.`.\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "id": "fb955469",
   "metadata": {},
   "outputs": [],
   "source": [
    "def Γ~c_a_b := withSymbols [e]\n",
    "  (1 / 2) * g~c~e . (∂/∂ g_b_e x~a + ∂/∂ g_a_e x~b - ∂/∂ g_a_b x~e)\n",
    "\n",
    "def R_i_j_k~l := withSymbols [a]\n",
    "  ∂/∂ Γ~l_j_k x~i - ∂/∂ Γ~l_i_k x~j\n",
    "    + Γ~l_i_a . Γ~a_j_k - Γ~l_j_a . Γ~a_i_k\n",
    "\n",
    "def R_i_j_k_l := withSymbols [a] R_i_j_k~a . g_a_l\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "id": "ea426b5f",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/html": [
       "$0$"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "Γ~1_1_1\n"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "cae61ba3",
   "metadata": {},
   "source": [
    "## Complex structure and lifted curvature\n",
    "\n",
    "The complex structure $J$ and its covariant derivative determine the\n",
    "curvature $R'$ on the circle bundle.  The first coordinate is the\n",
    "fibre direction; the remaining four coordinates belong to the\n",
    "Thurston base.\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "id": "03fe8cda",
   "metadata": {},
   "outputs": [],
   "source": [
    "def J_a_b :=\n",
    "  [|[| 0, 1, 0, 0 |],\n",
    "    [| -1, 0, 0, 0 |],\n",
    "    [| 0, 0, 0, κ |],\n",
    "    [| 0, 0, -1 * κ, 0 |]|]\n",
    "\n",
    "def J_a~c := withSymbols [b] J_a_b . g~b~c\n",
    "\n",
    "def ∇_c T~(a_1)...~(a_r)_(b_1)..._(b_k) := withSymbols [d]\n",
    "  ∂/∂ T~(a_1)...~(a_r)_(b_1)..._(b_k) x~c\n",
    "  + sum (map (\\i -> Γ~(a_i)_d_c .\n",
    "                T~(a_1)...~(a_(i - 1))~d~(a_(i + 1))...~(a_r)_(b_1)..._(b_k))\n",
    "             [1..r])\n",
    "  - sum (map (\\i -> Γ~d_(b_i)_c .\n",
    "                T~(a_1)...~(a_r)_(b_1)..._(b_(i - 1))_d_(b_(i + 1))..._(b_k))\n",
    "             [1..k])\n",
    "\n",
    "def ∇J_m_a_b := ∇_m J_a_b\n",
    "\n",
    "def ∇J~m_a_b := withSymbols [t] ∇J_t_a_b . g~t~m\n",
    "def ∇J_m~a_b := withSymbols [t] ∇J_m_t_b . g~t~a\n",
    "def ∇J_m_a~b := withSymbols [t] ∇J_m_a_t . g~t~b\n",
    "\n",
    "def δ :=\n",
    "  generateTensor\n",
    "    (\\match as list integer with\n",
    "       | [$n, #n] -> 1\n",
    "       | [_, _] -> 0)\n",
    "    [5, 5]\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "id": "07c6aa2b",
   "metadata": {},
   "outputs": [],
   "source": [
    "def R'{_i_j}_k~l : Tensor MathValue :=\n",
    "  generateTensor\n",
    "    (\\match as list integer with\n",
    "       | [#1, #1, _, _] -> 0\n",
    "       | [_, _, #1, #1] -> 0\n",
    "       | [#1, $b, #1, $d] -> -1 * p^2 * δ~(b - 1)_(d - 1)\n",
    "       | [$a, #1, #1, $d] ->      p^2 * δ~(a - 1)_(d - 1)\n",
    "       | [#1, $b, $c, #1] ->      p^2 * g_(b - 1)_(c - 1)\n",
    "       | [$a, #1, $c, #1] -> -1 * p^2 * g_(a - 1)_(c - 1)\n",
    "       | [#1, $b, $c, $d] -> -1 * p * ∇J_(b - 1)_(c - 1)~(d - 1)\n",
    "       | [$a, #1, $c, $d] ->      p * ∇J_(a - 1)_(c - 1)~(d - 1)\n",
    "       | [$a, $b, #1, $d] -> -1 * p * ∇J~(d - 1)_(a - 1)_(b - 1)\n",
    "       | [$a, $b, $c, #1] ->      p * ∇J_(c - 1)_(a - 1)_(b - 1)\n",
    "       | [$a, $b, $c, $d] -> R_(a - 1)_(b - 1)_(c - 1)~(d - 1)\n",
    "                             - p^2 * J_(b - 1)_(c - 1) * J_(a - 1)~(d - 1)\n",
    "                             + p^2 * J_(a - 1)_(c - 1) * J_(b - 1)~(d - 1)\n",
    "                             + 2 * p^2 * J_(a - 1)_(b - 1) * J_(c - 1)~(d - 1))\n",
    "    [5, 5, 5, 5]\n"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "da3db121",
   "metadata": {},
   "source": [
    "## Wodzicki–Chern–Simons contraction\n",
    "\n",
    "The alternating contraction contains three copies of $R'$.  Its raw\n",
    "result uses negative powers of the quoted atom $\\beta$.  Multiplying\n",
    "by $16\\beta^8$ clears those Laurent denominators.  A Gröbner basis for\n",
    "the defining quote relations then gives a canonical polynomial normal\n",
    "form, after which the denominator is restored.\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 8,
   "id": "b8597a63",
   "metadata": {},
   "outputs": [],
   "source": [
    "def S := withSymbols [i, j, k]\n",
    "  let (es, os) := evenAndOddPermutations 5 in\n",
    "    sum (map (\\σ -> R'_(σ 1)_j_1~i . R'_(σ 2)_(σ 3)_k~j . R'_(σ 4)_(σ 5)_i~k) es) -\n",
    "    sum (map (\\σ -> R'_(σ 1)_j_1~i . R'_(σ 2)_(σ 3)_k~j . R'_(σ 4)_(σ 5)_i~k) os)\n",
    "\n",
    "def quoteGb :=\n",
    "  groebnerBasis ['(1 + θ₂ - θ₂^2 - β), '(1 + θ₂ - `(1 + θ₂))]\n",
    "\n",
    "def sSimplified := polyNF quoteGb (16 * β^8 * S) / (16 * β^8)\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 9,
   "id": "06b1d092",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/html": [
       "$192 p^{6} κ - 40 (-θ₂^{2} + θ₂ + 1)^{-2} p^{4} κ + \\frac{-25}{16} (-θ₂^{2} + θ₂ + 1)^{-4} p^{2} κ$"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "sSimplified\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 10,
   "id": "14d481dd",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/html": [
       "$True$"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "def sClosedForm :=\n",
    "  p^2 * κ * (-25 - 640 * p^2 * β^2 + 3072 * p^4 * β^4) / (16 * β^4)\n",
    "\n",
    "sSimplified = sClosedForm\n"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "b369a39c",
   "metadata": {},
   "source": [
    "## Result\n",
    "\n",
    "Egison reduces the full contraction to\n",
    "\n",
    "$$\n",
    "S=192p^6\\kappa-\\frac{40p^4\\kappa}{\\beta^2}\n",
    "  -\\frac{25p^2\\kappa}{16\\beta^4}\n",
    " =\\frac{p^2\\kappa(-25-640p^2\\beta^2+3072p^4\\beta^4)}\n",
    "        {16\\beta^4}.\n",
    "$$\n",
    "\n",
    "Thus the expression previously simplified with an external computer\n",
    "algebra system is now calculated and normalized entirely by Egison.\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
}