Approximate sum of squares decompositions for 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>1812.03456-cf6dee7.zip</code> contains a julia environment specification (<code>Project.toml</code> and <code>Manifest.toml</code>) as well as <code>1812.03456.jl</code> script used for automatic certification and jupyter noteboks in <code>./notebooks</code> directory. <code>SAutF5_r2.tar.xz</code> contains the precomputed solutions for expressing <code>Adj₅+2·Op₅-0.28Δ₅</code> and <code>Adj₅+3·Op₅-1.4Δ₅</code> as sum of (hermitian) squares in the group ring of <code>SAut(F₅)</code>. The contents of this archive must be placed inside `<code>1812.03456`</code>directory from the <code>zip</code> file. <strong>Preparation</strong> The code needs to be run with <code>julia-1.4.0</code> or higher (tested versions include also versions <code>julia-1.5</code>). In principle any version in <code>[1.4-2.0)</code> should work due to the promise of forward compatibility. While located in the main directory (<code>1812.03456</code>) you should run the following code in <code>julia</code>s <code>REPL</code> console to instantiate the environment for computations: <pre><code class="language-julia">using Pkg Pkg.activate(".") Pkg.instantiate()</code></pre> (this needs to be done once per installation). Then the directory <code>SAutF5_r2</code> (from the <code>SAutF5_r2.tar.xz</code> archive) needs to be placed in <code>1812.03456</code>. <strong>Replication: Jupyter notebook</strong> A jupyter server may be launched then within the directory <code>1812.03456</code> by issuing from julia command-line (<code>REPL</code>) the following commands. <pre><code>using Pkg Pkg.activate(".") using IJulia notebook(dir=".")</code></pre> During the first run the user may be asked for installation of <code>Jupyter</code> program (a server for running this notebook) within <code>miniconda</code> environment, which will happen automatically after confirmation. To execute the commands in the notebook, one needs to navigate to <code>notebooks</code> subdirectory of <code>1812.03456</code> and click either of the notebooks. One can replicate the main computational results of the paper by executing all the cells in the <code>Positivity of Adj_n + kOp_n in ISAut(F_n)</code> notebook. <strong>Replication: script</strong> To verify that <em>(Adj₅ + 3.0·Op₅) - 1.4·Δ₅</em> admits an approximate sum of squares decomposition run in <code>1812.03456</code> directory <code>julia --project=. --color=yes 1812.03456.jl -n 5 -k 3 -l 1.4</code> On a modern laptop computer this should finish in less than 2h. At the end of computations you will see lines such as: ┌ Info: λ is certified to be &gt;<br> └ λ_cert.lo = 1.3701131733828074<br> [ Info: i.e Adj_5 + 3.0·Op_5 - (1.3701131733828074)·Δ_5 ∈ Σ²₂ ISAut(F_5) 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.370....</code> A similar verification for <em>Adj₅ + 2.0·Op₅ - 0.28·Δ₅</em> can be run by executing <code>julia --project=. --color=yes 1812.03456.jl -n 5 -k 2 -l 0.28</code> <strong>Generating the provided files</strong> If you wish to produce the whole certificate on your own (including the generation of group ring and its multiplication table), delete all <code>*.jld</code> files from the <code>SAutF5_r2</code> folder and run one of the above commands with the same (or different) parameters again. Note: To do this you need at least 16GB of RAM and spare 24h of your CPU. This research was supported in part by National Science Center, Poland, grant 2017/26/D/ST1/00103.