add script check_SAutF5.jl

check_SAutF5.jl

@@ -0,0 +1,41 @@
+using Pkg
+Pkg.activate(".")
+using Groups
+using GroupRings
+using PropertyT
+using SparseArrays
+using LinearAlgebra
+using IntervalArithmetic
+using JLD
+
+@show Threads.nthreads()
+BLAS.set_num_threads(Threads.nthreads());
+
+G = SAut(FreeGroup(5))
+pm = load("oSAutF5_r2/pm.jld", "pm");
+RG = GroupRing(G, pm)
+@info RG
+
+S_size = 80
+Δ_coeff = SparseVector(maximum(pm), collect(1:(1+S_size)), [S_size; -ones(S_size)])
+Δ = GroupRingElem(Δ_coeff, RG);
+Δ² = Δ^2;
+
+@info "Loading solution"
+λ₀ = load("oSAutF5_r2/1.3/lambda.jld", "λ")
+P₀ = load("oSAutF5_r2/1.3/SDPmatrix.jld", "P");
+
+@info "Taking square root of P"
+@time Q = real(sqrt(P₀));
+
+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
+
+@info "Computing SOS decomposition"
+@time sos = PropertyT.compute_SOS(RG, Q_aug);
+
+residual = Δ² - @interval(λ₀)*Δ - sos;
+@show norm(residual, 1)