Property (T) in julia

1. 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.

1.1. Julia environment

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

1.2s

Bash in JuliaJulia 1.1

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

502.7s

JuliaJulia 1.1

Pkg.status()

1.0s

JuliaJulia 1.1

1.2. Running tests (optional)

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

Pkg.test("PropertyT")

611.1s

JuliaJulia 1.1

1.3. 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

14.2s

Bash in JuliaJulia 1.1

The above commands need to be typically run only once.

2. Replicating computations for ArXiv:1712.07167

This section shows how one should be able to replicate the computations presented in 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())

8.5s

JuliaJulia 1.1

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 = |S_5| - \sum_{s\in S_5} s

remembering that in the ordered basis of the identity comes first with generators following directly after. Note that the generating set of consists of exactlytransvections (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).

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;

9.3s

JuliaJulia 1.1

2.1. 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

2.2. Loading the solution

Next we load the solution :

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

1.1s

lambda_0JuliaJulia 1.1

1.3

As can be seen, we will be comparing the accuracy ofbelow against the numerical value of .

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

355.6s

JuliaJulia 1.1

2.3. Certification

Now we project the columns of 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

33.3s

JuliaJulia 1.1

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

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

2139.9s

JuliaJulia 1.1

The residual of the solution and is

residual = Δ² - @interval(λ₀)*Δ - sos;
norm(residual, 1)

6.4s

residual_normJuliaJulia 1.1

[8.35381e-06, 8.42859e-06]

thus we can certify that the spectral gapis at least the lower end of the interval

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

1.1s

JuliaJulia 1.1

[1.29996, 1.29997]

which is exactly

print(certified.lo)

0.9s

JuliaJulia 1.1

This, via estimateleads to the lower bound on the Kazhdan constant of

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

0.7s

JuliaJulia 1.1

0.180275