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)