Certification

certify(F, solutions, [p, certify_cache]; options...)
certify(F, result, [p, certify_cache]; options...)

Attempt to certify that the given approximate solutions correspond to true solutions of the polynomial system $F(x;p)$. The system $F$ has to be an (affine) square polynomial system. Also attemps to certify for each solutions whether it approximates a real solution. The certification is done using interval arithmetic and the Krawczyk method^[Moo77]. Returns a CertificationResult which additionall returns the number of distinct solutions. For more details of the implementation see ^[BRT20].

Options

• show_progress = true: If true shows a progress bar of the certification process.
• max_precision = 256: The maximal accuracy (in bits) that is used in the certification process.
• compile = false: See the solve documentation.

Example

We take the first example from our introduction guide.

@var x y
# define the polynomials
f₁ = (x^4 + y^4 - 1) * (x^2 + y^2 - 2) + x^5 * y
f₂ = x^2+2x*y^2 - 2y^2 - 1/2
F = System([f₁, f₂], variables = [x,y])
result = solve(F)

Result with 18 solutions
========================
• 18 paths tracked
• 18 non-singular solutions (4 real)
• random seed: 0xcaa483cd
• start_system: :polyhedral

We see that we obtain 18 solutions and it seems that 4 solutions are real. However, this is based on heuristics. To be absolute certain we can certify the result

certify(F, result)

CertificationResult
===================
• 18 solution candidates given
• 18 certified solution intervals (4 real, 14 complex)
• 18 distinct certified solution intervals (4 real, 14 complex)

and see that there are indeed 18 solutions and that they are all distinct.

CertificationResult

The result of certify for multiple solutions. Contains a vector of SolutionCertificate as well as a list of certificates which correspond to the same true solution.

certificates(R::CertificationResult)

Obtain the stored SolutionCertificates.

distinct_certificates(R::CertificationResult)

Obtain the certificates corresponding to the determined distinct solution intervals.

ncertified(R::CertificationResult)

Returns the number of certified solutions.

nreal_certified(R::CertificationResult)

Returns the number of certified real solutions.

ncomplex_certified(R::CertificationResult)

Returns the number of certified complex solutions.

ndistinct_certified(R::CertificationResult)

Returns the number of distinct certified solutions.

ndistinct_real_certified(R::CertificationResult)

Returns the number of distinct certified real solutions.

ndistinct_complex_certified(R::CertificationResult)

Returns the number of distinct certified complex solutions.

save(filename, C::CertificationResult)

Store a text representation of the certification result C on disk.

show_straight_line_program(R::CertificationResult)
show_straight_line_program(io::IO, R::CertificationResult)

Print a representation of the used straight line program.

SolutionCertificate

Result of certify for a single solution. Contains the initial solutions and if the certification was successfull a vector of complex intervals where the true solution is contained in.

is_certified(certificate::SolutionCertificate)

Returns true if certificate is a certificate that certified_solution_interval(certificate) contains a unique zero.

is_real(certificate::SolutionCertificate)

Returns true if certificate certifies that the certified solution interval contains a true real zero of the system. If false is returned then this does not necessarily mean that the true solution is not real.

is_complex(certificate::SolutionCertificate)

Returns true if certificate certifies that the certified solution interval contains a true complex zero of the system.

is_positive(certificate::SolutionCertificate)

Returns true if is_certified(certificate) is true and the unique zero contained in certified_solution_interval(certificate) is real and positive.

solution_candidate(certificate::SolutionCertificate)

Returns the given provided solution candidate.

certified_solution_interval(certificate::SolutionCertificate)

Returns an Arblib.AcbMatrix representing a vector of complex intervals where a unique zero of the system is contained in. Returns nothing if is_certified(certificate) is false.

certified_solution_interval_after_krawczyk(certificate::SolutionCertificate)

Returns an Arblib.AcbMatrix representing a vector of complex intervals where a unique zero of the system is contained in. This is the result of applying the Krawczyk operator to certified_solution_interval(certificate). Returns nothing if is_certified(certificate) is false.

certificate_index(certificate::SolutionCertificate)

Return the index of the solution certificate. Here the index refers to the index of the provided solution candidates.

solution_approximation(certificate::SolutionCertificate)

If is_certified(certificate) is true this returns the midpoint of the certified_solution_interval of the given certificate as a Vector{ComplexF64}. Returns nothing if is_certified(certificate) is false.