Approximate sum of squares decompositions for 36(Adj₅ + k·Op₅) - λΔ₅ ∈ ISAut(F₅)

This is the dataset accompanying <em>On property (T) for Aut(Fₙ) and SLₙ(</em>ℤ<em>) </em>paper (https://arxiv.org/abs/1812.03456). See the appendix thereof and Section 4 of (Aut(F₅) has property (T)) for more details. <strong>Content</strong> <code>check_positivity.jl</code> is the script to (re)-produce sum of squares decompositions. In <code>sqadjop.jl</code> the helper functions are defined. <code>Positivity in SL(n,Z).ipynb</code> is the ipython notebook which contains replication for special linear groups. <code>SAutF5_r2/delta.jld</code> contains the Laplacian element (and the multiplication table) of the Group Ring of <code>SAut(F₅)</code>. <code>SAutF5_r2/OrbitData.jld</code> contains the data for decomposition and block decomposition. <code>SAutF5_r2/SqAdjOp_coeffs.jld</code> contains the coefficients of elements <code>Sq</code>, <code>Adj</code>, and <code>Op</code>. <code>SAutF5_r2/5.0/</code> contains the approximate sum of squares decomposition for <code>Adj-2·Op + 5.0Δ</code>. <code>SAutF5_r2/50.0/</code> contains the approximate sum of squares decomposition for <code>Adj-3·Op + 50.0Δ</code>. <code>drwxr-xr-x 0 oSAutF5_r2/<br> -rw-r--r-- 257218404 oSAutF5_r2/OrbitData.jld<br> -rw-r--r-- 86472 oSAutF5_r2/SqAdjOp_coeffs.jld<br> -rw-r--r-- 172357682 oSAutF5_r2/delta.jld<br> drwxr-xr-x 0 oSAutF5_r2/50.0/<br> -rw-r--r-- 5166 oSAutF5_r2/50.0/Adj+3Op.log<br> -rw-r--r-- 344628928 oSAutF5_r2/50.0/solution.jld<br> drwxr-xr-x 0 oSAutF5_r2/5.0/<br> -rw-r--r-- 5236 oSAutF5_r2/5.0/Adj+2Op.log<br> -rw-r--r-- 172315832 oSAutF5_r2/5.0/solution.jld</code> <strong>Preparation</strong> The code needs to be run with <code>julia-0.6.</code> To install all of the dependencies run the following code in <code>julia</code>s <code>REPL</code> console: <pre><code class="language-julia">Pkg.add("AbstractAlgebra") Pkg.add("Nemo") # this may take some time to compile Pkg.clone("https://git.wmi.amu.edu.pl/kalmar/Groups.jl") Pkg.checkout("Groups", "AutFn") Pkg.clone("https://git.wmi.amu.edu.pl/kalmar/GroupRings.jl") Pkg.checkout("GroupRings", "AutFn") Pkg.clone("https://git.wmi.amu.edu.pl/kalmar/PropertyT.jl") Pkg.checkout("PropertyT", "AutFn") Pkg.resolve()</code></pre> <strong>Replication</strong> To replicate the computations of the approximate sum of squares from the paper you need to unpack the content of <code>oSAutF5_r2.tar.xz</code> in the same folder where <code>check_positivity.jl</code> and <code>sqadjop.jl</code> reside. To verify that <em>36(Adj₅ + 3.0·Op₅) - 50.0Δ₅</em> admits an approximate sum of squares decomposition run <code>julia check_positivity.jl -k 3 -lambda 50.0</code> On a modern laptop computer with 8GB of RAM this should finish in less than 3h. <strong>Note:</strong> The execution will produce numerous warnings, eg. <code>WARNING: Scalar and coeffs are in different rings! Promoting result to ...<br> WARNING: Basis of the GroupRing is not defined.</code> These are safe to ignore. At the end of computations you will see lines such as: <code>INFO: λ is certified to be &gt; 47.40050266779858</code> <code>INFO: i.e Adj₅ + 3.0·Op₅ - 1.3166806296610716·Δ₅ ∈ Σ²₂ ISAut(F₅)</code> This means that <em>Adj₅ + 3.0·Op₅ - λΔ₅</em> is a sum of Hermitian squares of elements from <em>ISAut(F₅)</em> for every <code>λ &lt; 1.316....</code> A similar verification for <em>36(Adj₅ + 2.0·Op₅) - 5.0Δ₅</em> can be run by executing <code>julia check_positivity.jl -k 2 -lambda 5.0</code> <strong>Generating the provided files</strong> If You want to generate the multiplication table, orbit decomposition, etc. on Your own delete all <code>*.jld</code> files from the <code>oSAutF5_r2</code> folder and run <code>check_positivity.jl</code> script with the same parameters again. Note: To do this You need at least 32GB of RAM and spare 24h of Your CPU. The solutions could be also recreated, but this takes considerably more time (several days, depending on the solver's version and CPU). This research was supported in part by National Science Center, Poland, grant 2017/26/D/ST1/00103.