Module certificates

Expand description

Exact, machine-checkable non-negativity certificates: Handelman (boxes), half-lines, parametric polyhedra and sums of squares, with Lean export. Exact, machine-checkable certificates that a polynomial is non-negative on a box, on a half-line, or on a polyhedron whose facets depend on a parameter — each exportable as a Lean 4 / Mathlib proof.

§Parametric polyhedra

prove_nonnegative_on_polyhedron takes hypotheses h₁, …, hₘ ∈ ℚ[j, x], a goal g ∈ ℚ[j, x] and a parameter bound j ≥ j₀, and searches for the identity

λ(j) · g  =  Σₖ Σ_{a,b} μ_{k,a,b} · jᵃ (j − j₀)ᵇ · hₖ
           + Σ_{k≤l} Σ_{a+b≤1} μ_{k,l,a,b} · jᵃ (j − j₀)ᵇ · hₖ hₗ      (optional)
           + Σ_{a+b≥1} μ_{a,b} · jᵃ (j − j₀)ᵇ  +  μ₀ ,
λ(j) = 1 + Σ_{a≥1} νₐ jᵃ ,        all μ, ν ≥ 0 .

Every term on the right is non-negative wherever the hypotheses hold and j ≥ j₀ (powers of j itself are only used when j₀ ≥ 0), and λ(j) > 0, so the identity proves g ≥ 0 for every admissible j. The polynomial multiplier λ on the goal is what makes the parametric case work: the Farkas multipliers of j-dependent facets are rational functions of j, and clearing their denominators puts a polynomial in front of g. With the goal −1 (prove_polyhedron_empty) the same identity proves the polyhedron empty for every j ≥ j₀. The search is a sequence of exact LPs staged from the smallest basis upwards (PolyhedronOpts); every PolyhedronCertificate is re-verified with exact polynomial arithmetic, exports as a theorem (PolyhedronCertificate::to_lean) or as bare proof steps for an existing skeleton (PolyhedronCertificate::lean_steps).

§Sums of squares

prove_sos proves g ≥ 0 on all of ℝⁿ by an exact decomposition g = Σ dₖ pₖ² (SosCertificate): the Gram semidefinite program is solved by a built-in interior-point method, rounded, projected back onto the coefficient constraints exactly and checked with a rational L·D·Lᵀ; goals with real zeros are handled by numerically guided exact facial reduction. This is the class the hypothesis-based certificates cannot reach ((x − 1)² + (y − 1)², x⁴ + y⁴ + z⁴ + 1 − 4xyz).

§Boxes

prove_nonnegative_on_box searches for a Handelman certificate: a representation

goal(x) = Σₖ λₖ · Πᵢ (xᵢ − lᵢ)^{aₖᵢ} · (uᵢ − xᵢ)^{bₖᵢ},      λₖ ≥ 0

over the box lᵢ ≤ xᵢ ≤ uᵢ, with all products of total degree at most degree. Every factor is non-negative on the box, so the identity is a proof of goal ≥ 0 there. Handelman’s theorem guarantees such a certificate exists for some degree whenever goal is strictly positive on the (compact) box; when goal touches zero in the interior none may exist, and the search reports that honestly.

The search is an exact rational linear program (linprog): the products are expanded with Poly arithmetic, their coefficient vectors form the columns of a matrix, and nonneg_combination finds λ ≥ 0 exactly or returns a Farkas vector proving that no certificate of that degree exists. Before a certificate is returned it is re-verified by recomputing Σ λₖ·productₖ with exact polynomial arithmetic and checking structural equality with goal — so a BoxCertificate can be trusted without trusting the LP solver.

BoxCertificate::to_lean renders the result as a Lean 4 / Mathlib theorem whose proof is nlinarith fed with exactly the products that appear with non-zero weight (so it is a linear-arithmetic check, not a search).

§Half-lines

prove_nonnegative_on_halfline and prove_nonnegative_on_reals handle univariate goals on x ≥ a / x ≤ a / all of ℝ with a shift, a Pólya multiplier (1 + k)ᴺ and square factors for interior double zeros (HalfLineCertificate, RealLineCertificate).

§Outcomes and the `BoxCertificate` trait

Every prover returns an Outcome<C, U> — Proved(C) with a re-verified certificate, Refuted { point, value, .. } with an exact counterexample, or Unknown(U) with a method-specific account of the search — under the aliases BoxOutcome, HalfLineOutcome, PolyhedronOutcome and SosOutcome. All certificate types implement the Certificate trait (goal, verify, to_lean, to_json / from_json) so generic code can treat them alike.

§Example

use symplex::prelude::*;
use symplex::certificates::{prove_nonnegative_on_box, BoxBound, BoxOutcome};

let ctx = Context::new();
let (r, f) = (ctx.symbol("r"), ctx.symbol("f"));
// 1/4 − (r − f/2)² ≥ 0 on [0, 1/2] × [0, 1]
let goal = ctx.rational(1, 4) - (&r - &f / 2).powi(2);
let bounds = [
    BoxBound { var: r.clone(), lo: ctx.int(0), hi: ctx.rational(1, 2) },
    BoxBound { var: f.clone(), lo: ctx.int(0), hi: ctx.int(1) },
];
match prove_nonnegative_on_box(&goal, &bounds, 2).unwrap() {
    BoxOutcome::Proved(cert) => {
        assert!(cert.verify());
        assert!(cert.to_lean("quarter_bound").unwrap().contains("nlinarith"));
    }
    other => panic!("expected a certificate, got {other:?}"),
}

Re-exports§

pub use crate::domains::linprog::BudgetHit;

Structs§

BoxBound: One variable of the box: lo ≤ var ≤ hi with exact rational endpoints.
BoxBoundTree: One side of the box in a BoxCertificateData: lo ≤ var ≤ hi as expression trees (the serialisable form of a BoxBound).
BoxCertificate: A verified Handelman certificate: goal = square² · Σ weightₖ · productₖ on the box, every weightₖ > 0. The square factor is 1 unless the goal had even-multiplicity zeros inside the box (see prove_nonnegative_on_box).
BoxCertificateData: Serialisable form of a BoxCertificate (see BoxCertificate::to_json).
BoxUnknown: Why prove_nonnegative_on_box could not decide: no certificate of the requested degree exists and no counterexample was found on the sampled grid. Try a higher degree; if the goal has a zero in the interior of the box, Handelman certificates may not exist at any degree.
HalfLineCertificate: A verified certificate that a univariate polynomial is non-negative on a half-line.
HalfLineCertificateData: Serialisable form of a HalfLineCertificate (see HalfLineCertificate::to_json).
HalfLineUnknown: Why prove_nonnegative_on_halfline could not decide: the goal is non-negative on the half-line (decided exactly by Sturm’s theorem) but no certificate was found within the Pólya budget — this happens when the goal has an interior zero that is not an even-multiplicity factor over ℚ (an irreducible sum of squares with an irrational double root).
HandelmanTerm: One product Πᵢ (xᵢ − lᵢ)^{aᵢ} (uᵢ − xᵢ)^{bᵢ} of a Handelman certificate.
HandelmanTermData: One Handelman term in a BoxCertificateData: weight · Π (xᵢ − lᵢ)^lower_powers[i] · Π (uᵢ − xᵢ)^upper_powers[i] (the serialisable form of a HandelmanTerm).
ParamBound: The parameter bound var ≥ lower of a parametric polyhedron: the input of PolyhedronProver::new / prove_nonnegative_on_polyhedron and what PolyhedronCertificate::parameter reports back.
ParamBoundTree: Serialisable form of a ParamBound (see PolyhedronCertificateData).
PolyhedronCertificate: A verified certificate λ(j)·goal = Σ weight · jᵃ (j − j₀)ᵇ · Π hₖ.
PolyhedronCertificateData: Serialisable form of a PolyhedronCertificate (see PolyhedronCertificate::to_json).
PolyhedronLeanNames: Hypothesis names for PolyhedronCertificate::lean_steps.
PolyhedronLeanSteps: The tactic lines of a polyhedron proof, without indentation.
PolyhedronOpts: Search limits for prove_nonnegative_on_polyhedron.
PolyhedronProver: A prover for a fixed hypothesis set and parameter: parses the hypotheses once, builds each stage’s product basis once (on the first goal that reaches the stage), and then certifies any number of goals (or the emptiness of the set) against them. prove_nonnegative_on_polyhedron is PolyhedronProver::new(hyps, param, opts)?.prove(goal).
PolyhedronTerm: One weighted product of a PolyhedronCertificate: weight · jᵃ (j − j₀)ᵇ · Π hₖ over the listed hypotheses.
PolyhedronTermData: One term of a PolyhedronCertificateData (the serialisable form of a PolyhedronTerm): weight · Π hₖ · jᵃ · (j − j₀)ᵇ.
PolyhedronUnknown: Why prove_nonnegative_on_polyhedron could not decide: no certificate up to these limits, and no counterexample on the sampled parameter values — or the call’s budget ran out first (budget_exhausted), in which case the limits are those of the stage that was interrupted and the stages after it were not tried.
RealLineCertificate: A verified proof that a univariate polynomial is non-negative on all of ℝ: a pair of half-line certificates meeting at split.
RealLineCertificateData: Serialisable form of a RealLineCertificate: its two halves.
SosCertificate: A verified decomposition goal = Σₖ dₖ · pₖ².
SosCertificateData: Serialisable form of an SosCertificate.
SosOpts: Search limits for prove_sos.
SosUnknown: Why prove_sos could not decide: the goal may be non-negative without being a sum of squares (Motzkin), or the numerical search did not converge.

Enums§

Outcome: The result of a certificate search: Proved with a verified certificate of type C, Refuted with an exact point where the goal is negative, or Unknown with a method-specific account U of what was tried.
Ray: Which unbounded domain a HalfLineCertificate covers.

Traits§

Certificate: What every certificate type offers: the goal it certifies, exact re-verification, Lean export and a JSON round trip. Implemented by BoxCertificate, HalfLineCertificate, RealLineCertificate, PolyhedronCertificate and SosCertificate, whose inherent methods of the same names do the work — the trait lets generic code (a prover that falls back to another, a report that prints whatever it was given) treat them alike.

Functions§

is_nonnegative_on_box: Convenience: is goal ≥ 0 on the box? Some(true) with a verified certificate up to max_degree, Some(false) with an exact counterexample, None when undecided.
is_sos: Convenience: Some(true) with a verified SOS certificate, Some(false) with an exact counterexample, None when undecided.
prove_nonnegative_on_box: Prove goal ≥ 0 on the box bounds (one BoxBound per variable, with rational literal endpoints) by a Handelman certificate of total degree at most degree, or refute it with an exact counterexample.
prove_nonnegative_on_halfline: Prove goal ≥ 0 for var ≥ a (Ray::AtLeast) or var ≤ a (Ray::AtMost) with a HalfLineCertificate, or refute it exactly.
prove_nonnegative_on_polyhedron: Prove goal ≥ 0 on {x : hₖ(j, x) ≥ 0 ∀k} for every real j ≥ j₀ (param = Some(&ParamBound { var: j, lower: j₀ })), or on the fixed polyhedron {hₖ(x) ≥ 0} (param = None), by the identity described in the certificates module documentation; refute it with an exact point of the set where the goal is negative; or report Unknown. To certify many goals against the same hypotheses, build a PolyhedronProver once.
prove_nonnegative_on_reals: Prove goal ≥ 0 on all of ℝ (univariate) by splitting at split into two half-line certificates.
prove_polyhedron_empty: Prove that {x : hₖ(j, x) ≥ 0 ∀k} is empty for every j ≥ j₀ (Proved), exhibit a point of it (Refuted { point, .. }), or report Unknown. This is prove_nonnegative_on_polyhedron with the goal −1: the certificate λ(j)·(−1) = Σ μ·(…) with μ ≥ 0 is a contradiction on the set.
prove_sos: Prove goal ≥ 0 on ℝⁿ by an exact sum-of-squares decomposition, refute it with an exact point, or report Unknown.

Type Aliases§

BoxOutcome: Result of prove_nonnegative_on_box: an Outcome with a BoxCertificate or a BoxUnknown.
HalfLineOutcome: Result of prove_nonnegative_on_halfline: an Outcome with a HalfLineCertificate or a HalfLineUnknown. A refutation’s point has the single entry (var, value).
PolyhedronOutcome: Result of prove_nonnegative_on_polyhedron: an Outcome with a PolyhedronCertificate or a PolyhedronUnknown. A refutation’s point lists the free variables then the parameter, and param_value is the sampled parameter value; for the emptiness question the point lies in the polyhedron.
SosOutcome: Result of prove_sos: an Outcome with an SosCertificate or an SosUnknown. A refutation’s point lists the variables in the order given to prove_sos.