This post documents replication details for paper $\operatorname{Aut}(\mathbb{F}_5)$ has property (T) by M. Kaluba, P.W. Nowak and N. Ozawa.

Table of Contents

Setting up the environment

The code below is designed to run on julia 1.1.0.

Before running any computations we need to set-up the environment and download the pre-computed data.

Getting julia project

git clone https://git.wmi.amu.edu.pl/kalmar/1712.07167.git

using Pkg
Pkg.activate("1712.07167")
Pkg.instantiate()

Pkg.status()

Running tests (optional)

Now everything seems to be installed, but let’s check that things run as they should:

Pkg.test("PropertyT")

Getting the pre-computed data

We need to download and unpack the data from Zenodo

wget -O oSAutF5_r2.tar.xz "https://zenodo.org/record/1913734/files/oSAutF5_r2.tar.xz?download=1"
tar xvf oSAutF5_r2.tar.xz

The above commands need to be typically run only once.

Replicating computations for 1712.07167

This section shows how one should be able to replicate the computations presented in $\operatorname{Aut}(\mathbb{F}_5)$ has property (T) by M. Kaluba, P.W. Nowak and N. Ozawa.

To speed-up certain computations you may wish to set the environmental variable JULIA_NUM_THREADS to the number of (the physical) cores of cpu.

using Pkg
Pkg.activate("1712.07167")
using Groups
using GroupRings
using PropertyT

using SparseArrays
using LinearAlgebra
using IntervalArithmetic
using JLD
BLAS.set_num_threads(Threads.nthreads())

In the cell below we define the group ring of the special automorphism group of the free group (by reading the division table from pm.jld file) and construct the Laplacian $$ \Delta_5 = |S_5| - \sum_{s\in S_5} s $$

remembering that in the ordered basis of $\mathbb{R}\operatorname{SAut}(\mathbb{F}_5)$ the identity comes first with generators following directly after. Note that the generating set $S = S_5$ of $\operatorname{SAut}(\mathbb{F}_5)$ consists of exactly $80$ transvections (due to technical issue with the transition from julia-0.6 to julia-1.0 we can not load the supplied oSAutF5_r2/delta.jld file directly).

G = SAut(FreeGroup(5))
pm = load("oSAutF5_r2/pm.jld", "pm")
RG = GroupRing(G, pm)
@show RG
S_size = 80
Δ_coeff = SparseVector(maximum(pm), collect(1:(1+S_size)), [S_size; -ones(S_size)])
Δ = GroupRingElem(Δ_coeff, RG);
Δ² = Δ^2;

Recomputing from scratch group ring structure

The computations above could be re-done from scratch (i.e. without relying on the provided pm) by executing

radius = 2
G = SAut(FreeGroup(5))
S = AbstractAlgebra.gens(G);
@time E₄, sizes = Groups.generate_balls(S, Id, radius=2radius) # takes lots of time and space
E₄_rdict = GroupRings.reverse_dict(E₄)
@time pm = GroupRings.create_pm(E₄, E₄_rdict, sizes[radius]; twisted=true) # takes lots of time and space
RG = GroupRing(G, E₄, E₄_rdict, pm)
Δ = PropertyT.spLaplacian(RG, S)
Δ² = Δ^2

Loading the solution

Next we load the solution $(\lambda_0, P_0)$:

λ₀ = load("oSAutF5_r2/1.3/lambda.jld", "λ")

As can be seen, we will be comparing the accuracy of $P_0​$ below against the numerical value of $\lambda_0 = 1.3​$.

P₀ = load("oSAutF5_r2/1.3/SDPmatrix.jld", "P")
@time Q = real(sqrt(P₀))

Certification

Now we project the columns of $Q$ to the augmentation ideal, in interval arithmetic. The returned check_columns_augmentation is a boolean flag to detect if the projection was successful, i.e. if we can guarantee that each column of Q_aug can be represented by an element from the augmentation ideal. (If it were not successful, one may project Q = PropertyT.augIdproj(Q) in the floating point arithmetic prior to the cell below).

Q_aug, check_columns_augmentation = PropertyT.augIdproj(Interval, Q);
@show check_columns_augmentation
if !check_columns_augmentation
  @warn "Columns of Q are not guaranteed to represent elements of the augmentation ideal!"
end

Finally we compute the actual sum of squares decomposition represented by Q_aug:

@time sos = PropertyT.compute_SOS(RG, Q_aug);

The residual of the solution and $\Delta^2 - \lambda_0\Delta$ is

residual = Δ² - @interval(λ₀)*Δ - sos;
norm(residual, 1)
[8.35381e-06, 8.42859e-06]

thus we can certify that the spectral gap $\lambda(\operatorname{SAut}(\mathbb{F}_5), S_5)$ is at least the lower end of the interval

certified = @interval(λ₀) - 2^2*norm(residual, 1)
[1.29996, 1.29997]

which is exactly

print(certified.lo)

This, via estimate $\kappa \geqslant \sqrt{\frac{2\lambda}{|S|}}$ leads to the lower bound on the Kazhdan constant of

κ = (sqrt(2certified/S_size)).lo
0.180275

Deprecated Instructions for running with julia-0.6.

Clone https://git.wmi.amu.edu.pl/kalmar/GroupsWithPropertyT and checkout the 1712.07167 branch:

git clone https://git.wmi.amu.edu.pl/kalmar/GroupsWithPropertyT.git
cd ./GroupsWithPropertyT
git checkout 1712.07167

In julias REPL execute

Pkg.add("ArgParse")
Pkg.add("Nemo")
Pkg.clone("https://git.wmi.amu.edu.pl/kalmar/Groups.jl.git")
Pkg.checkout("Groups", "1712.07167")
Pkg.clone("https://git.wmi.amu.edu.pl/kalmar/GroupRings.jl.git")
Pkg.checkout("GroupRings", "1712.07167")
Pkg.clone("https://git.wmi.amu.edu.pl/kalmar/PropertyT.jl.git")
Pkg.checkout("PropertyT", "1712.07167")
Pkg.checkout("SCS")
Pkg.build("SCS")

This should resolve all the dependencies. Quit julia and place the oSAutF5_r2 folder downloaded from Zenodo research data repository inside GroupsWithPropertyT folder. To verify the decomposition of $\Delta^2 - \lambda \Delta$ for the group run (if You have a 4-core CPU at Your disposal)

julia AutFN_orbit.jl -N 5 --upper-bound=1.2 --cpus 4

If You want to generate the (twisted) multiplication table (and other required files) on Your own delete all *.jld files from the oSAutF5_r2 folder (except for 1.2 folder and its contents) and run the same command again.