GitHub

Certification

The high-level entry point is certify_posteriori. It first collects a numerical HomotopyContinuation.jl trace and then certifies the trace with CHT interval checks. By default, each trace segment is certified in an adaptively chosen local parameter: CHT may use t, Re(x_i), or Im(x_i) instead of forcing the whole argument to use t.

julia> @variables x y;
julia> CC = AcbField(128);
julia> F = [x^2 + 3*y - 4, y^2 + 3];
julia> G = [x^2 - 1, y^2 - 1];
julia> H = straight_line_homotopy(F, G, [x, y]; CCRing=CC, gamma=CC(0.5, 0.5));Compilation Done.
julia> cert = certify_posteriori(H, [CC(1), CC(-1)]; max_step_size=Inf, max_depth=6)PosterioriPathResult(success=true, method=adaptive_local_parameter_endpoint_box, trace_points=10, original_segments=9, boxes=9, failed=0, max_depth=0, hc_status=success)
julia> cert.successtrue
julia> success(cert)true
julia> solution(cert)2-element Vector{ComplexF64}:
 2.2975463569101278 + 1.1308046967319336im
                0.0 - 1.7320508075688772im
julia> certified_region(cert)2-element Vector{AcbFieldElem}:
 [2.3 +/- 0.0864] + [1e+0 +/- 0.215]*im
 [+/- 0.0839] + [-2e+0 +/- 0.352]*im
julia> cert.total_boxes9
julia> cert.failed_segmentsNamedTuple[]

For a successful result, certified_region returns the certified endpoint enclosure stored in the a posteriori result. solution returns the midpoint of that enclosure as a Vector{ComplexF64} for display and downstream numerical use.

CertifiedHomotopyTracking.certify_posteriori — Function
certify_posteriori(sys, x_start; kwargs...)
certify_posteriori(compiled::CompiledHomotopy, x_start; kwargs...)

Collect an HC.jl numerical trace for a specialized homotopy and certify the trace a posteriori.

The default verifier does not force every segment to use t as its parameter. For each trace segment it can choose a local parameter from t, Re(x_i), or Im(x_i), then certifies the remaining coordinates with an interval Krawczyk test.

Example

@variables x y;
CC = AcbField(128);
F = [x^2 + 3*y - 4, y^2 + 3];
G = [x^2 - 1, y^2 - 1];

H = straight_line_homotopy(F, G, [x, y]; CCRing=CC, gamma=CC(0.5, 0.5));
cert = certify_posteriori(H, [CC(1), CC(-1)]; max_step_size=Inf, max_depth=6)

cert.success
cert.total_boxes
cert.failed_segments

Public options are intentionally compact:

  • max_step_size = nothing: first use HC.jl's adaptive step choice, then retry failed certifications with smaller trace spacing. Give a positive number, Inf, or a tuple such as (Inf, 0.005, 0.0025) to override this schedule.
  • max_depth = nothing: use the internal depth schedule (6, 8, 10, 12). Give an integer to try only that depth.
  • local_parameter_variables = (): optionally restrict adaptive local-parameter candidates to selected variables by name or index. The homotopy parameter t is always kept as a candidate. By default, CHT may choose among t, Re(x_i), and Im(x_i) on each segment, which helps certify paths where t alone is a poor local coordinate.
  • local_parameter_method = :endpoint_box: validate each segment by enclosing the endpoints in an interval box for the chosen local parameter and applying an interval Krawczyk test to the remaining coordinates.
  • certification_chart = :affine: use :projective to certify the same HC trace in a projective chart. Use :auto to try affine certification first and retry in a projective chart only if affine certification fails. With projective_chart = :auto, a projective chart is chosen from the trace.
  • store_boxes = :summary: use :full only for visualization/debugging.
  • visualize = false: when not false, keep visualization boxes and optionally export them. Pass true, a filename, or a named tuple such as (filename = "posteriori.tex", axes = (:t, 1), show_trace = true).
  • visualize_options = (;): visualization/export options. See Visualization for related export helpers.
    • filename: output filename for automatic export.
    • axes: two or three axes. Axis entries may be :t, an integer coordinate, or (i, :real), (i, :imag), (i, :abs).
    • show_trace: draw the HC.jl trace when exporting.
  • diagnostics = :off: use :basic to record certification counters such as node refinements, segment attempts, Krawczyk validation calls, and chosen local parameters. Use :timing to include timing fields as well.
  • show_progress = false
  • throw_on_failure = false: return a PosterioriPathResult with failure details when certification fails. Set to true to throw an exception instead of returning a failed result.
  • threading = false, ntasks = Threads.nthreads(): certify independent trace segments concurrently when threading is enabled.
source
CertifiedHomotopyTracking.certified_region — Method
certified_region(cert::PosterioriPathResult)

Return the certified endpoint region obtained by a posteriori certification.

This is the Moore-refined endpoint box for the final trace node, stored as an ACB vector. For projective a posteriori certification, the endpoint box is converted back to the original affine coordinates when possible.

source

Threading

Start Julia with multiple threads before enabling threaded certification:

julia --threads=4 --project

or:

JULIA_NUM_THREADS=4 julia --project

Then pass threading=true. ntasks controls the maximum number of concurrent segment-certification tasks used by CHT.

cert = certify_posteriori(
    H,
    [CC(1), CC(-1)];
    threading=true,
    ntasks=4,
)

Diagnostics

Set diagnostics=:basic to record certification counters and local-parameter choices. Use :timing to include timing fields as well.

julia> cert = certify_posteriori(
           H,
           [CC(1), CC(-1)];
           max_step_size=Inf,
           max_depth=6,
           diagnostics=:basic,
       );
julia> cert.diagnostics(node_refinements = 10, midpoint_refinements = 0, segment_attempts = 9, krawczyk_validation_calls = 9, velocity_computations = 10, preconditioner_computations = 10, local_parameter_choices = Dict(:y_im => 4, :x_im => 4, :x_re => 1), max_Y = 0.013899552418604608, max_Z = 0.024128423085102938, max_Y_over_r = 0.40154430218400294)
julia> cert.diagnostics.local_parameter_choicesDict{Symbol, Int64} with 3 entries:
  :y_im => 4
  :x_im => 4
  :x_re => 1

With diagnostics=:timing, the same summary includes timing fields such as time_in_refinement, time_in_validation, and time_in_local_parameter_search.