PropertyT.jl/src/certify.jl

function augment_columns!(Q::AbstractMatrix)
    for c in eachcol(Q)
        c .-= sum(c) ./ length(c)
    end
    return Q
end

function __sos_via_sqr!(
    res::StarAlgebras.AlgebraElement,
    P::AbstractMatrix;
    augmented::Bool,
    id = (b = basis(parent(res)); b[one(first(b))]),
)
    A = parent(res)
    mstr = A.mstructure
    @assert size(mstr) == size(P)

    StarAlgebras.zero!(res)
    for j in axes(mstr, 2)
        for i in axes(mstr, 1)
            p = P[i, j]
            x_star_y = mstr[-i, j]
            res[x_star_y] += p
            # either result += P[x,y]*(x'*y)
            if augmented
                # or result += P[x,y]*(1-x)'*(1-y) == P[x,y]*(1-x'-y+x'y)
                res[id] += p
                x_star, y = mstr[-i, id], j
                res[x_star] -= p
                res[y] -= p
            end
        end
    end

    return res
end

function __sos_via_cnstr!(
    res::StarAlgebras.AlgebraElement,
    Q²::AbstractMatrix,
    cnstrs,
)
    StarAlgebras.zero!(res)
    for (g, A_g) in cnstrs
        res[g] = dot(A_g, Q²)
    end
    return res
end

function compute_sos(
    A::StarAlgebras.StarAlgebra,
    Q::AbstractMatrix;
    augmented::Bool,
)
    Q² = Q' * Q
    res = StarAlgebras.AlgebraElement(zeros(eltype(Q²), length(basis(A))), A)
    res = __sos_via_sqr!(res, Q²; augmented = augmented)
    return res
end

function sufficient_λ(residual::StarAlgebras.AlgebraElement, λ; halfradius)
    L1_norm = norm(residual, 1)
    suff_λ = λ - 2.0^(2ceil(log2(halfradius))) * L1_norm

    eq_sign = let T = eltype(residual)
        if T <: Interval
            "∈"
        elseif T <: Union{Rational,Integer}
            "="
        else # if T <: AbstractFloat
            "≈"
        end
    end

    info_strs = [
        "Numerical metrics of the obtained SOS:",
        "ɛ(elt - λu - ∑ξᵢ*ξᵢ) $eq_sign $(StarAlgebras.aug(residual))",
        "‖elt - λu - ∑ξᵢ*ξᵢ‖₁ $eq_sign $(L1_norm)",
        " λ $eq_sign $suff_λ",
    ]
    @info join(info_strs, "\n")

    return suff_λ
end

function sufficient_λ(
    elt::StarAlgebras.AlgebraElement,
    order_unit::StarAlgebras.AlgebraElement,
    λ,
    sos::StarAlgebras.AlgebraElement;
    halfradius,
)
    @assert parent(elt) === parent(order_unit) == parent(sos)
    residual = (elt - λ * order_unit) - sos

    return sufficient_λ(residual, λ; halfradius = halfradius)
end

function certify_solution(
    elt::StarAlgebras.AlgebraElement,
    orderunit::StarAlgebras.AlgebraElement,
    λ,
    Q::AbstractMatrix{<:AbstractFloat};
    halfradius,
    augmented = iszero(StarAlgebras.aug(elt)) &&
        iszero(StarAlgebras.aug(orderunit)),
)
    should_we_augment =
        !augmented && StarAlgebras.aug(elt) == StarAlgebras.aug(orderunit) == 0

    Q = should_we_augment ? augment_columns!(Q) : Q
    @time sos = compute_sos(parent(elt), Q; augmented = augmented)

    @info "Checking in $(eltype(sos)) arithmetic with" λ

    λ_flpoint = sufficient_λ(elt, orderunit, λ, sos; halfradius = halfradius)

    if λ_flpoint ≤ 0
        return false, λ_flpoint
    end

    λ_int = @interval(λ)
    Q_int = [@interval(q) for q in Q]

    check, sos_int = @time if should_we_augment
        @info("Projecting columns of Q to the augmentation ideal...")
        Q_int = augment_columns!(Q_int)
        @info "Checking that sum of every column contains 0.0..."
        check_augmented = all(0 ∈ sum(c) for c in eachcol(Q_int))
        check_augmented || @error(
            "Augmentation failed! The following numbers are not certified!"
        )
        sos_int = compute_sos(parent(elt), Q_int; augmented = augmented)
        check_augmented, sos_int
    else
        true, compute_sos(parent(elt), Q_int; augmented = augmented)
    end

    @info "Checking in $(eltype(sos_int)) arithmetic with" λ_int

    λ_certified =
        sufficient_λ(elt, orderunit, λ_int, sos_int; halfradius = halfradius)

    return check && inf(λ_certified) > 0.0, λ_certified
end