Polynomial Inequality Certificates
Problem
You want to prove — not numerically check — that a polynomial is non-negative on a box. Concretely, for
0 ≤ r ≤ 1/2, 0 ≤ f ≤ 1
show that
goal(r, f) = 1/4 − (r − f/2)² ≥ 0.
The inequality is true (|r − f/2| ≤ 1/2 on the box) and tight at the corners (1/2, 0) and (0, 1), so sampling cannot prove it and any floating-point slack would be suspicious.
Background: Handelman certificates
The four hypothesis polynomials
g₁ = r, g₂ = 1/2 − r, g₃ = f, g₄ = 1 − f
are non-negative on the box by definition, and so is every product of them. If we can find non-negative rationals λᵢ with
goal = Σ λᵢ · hᵢ, hᵢ ∈ { 1, gⱼ, gⱼ·gₖ, … }
then goal ≥ 0 follows immediately, and the identity can be checked by expanding both sides — a proof that fits on one line. Handelman’s theorem says such a representation always exists for a polynomial that is strictly positive on a polytope, if you allow products of high enough degree.
Finding λ is a linear feasibility problem: match coefficients monomial by monomial, and require λ ≥ 0. That is exactly what Poly::coefficient_matrix builds and linprog::feasible_nonneg solves — over ℚ, so the certificate is exact.
Solution
Build the family of products of degree ≤ 2 (fifteen polynomials), lay them out as a coefficient matrix, ask for a non-negative solution, and verify the identity two independent ways.
use num_rational::Ratio;
use num_traits::{Signed, Zero};
use symplex::linprog::{LpProblem, Q, feasible_nonneg};
use symplex::ntheory::rational_lcm_of_denominators;
use symplex::poly_ex::Poly;
use symplex::prelude::*;
fn show(v: &[Q]) -> String {
format!("({})", v.iter().map(|x| x.to_string()).collect::<Vec<_>>().join(", "))
}
fn main() {
let ctx = Context::new();
symplex::syms!(ctx; r, f);
let gens: [&Ex; 2] = [&r, &f];
// ── Hypotheses: each is ≥ 0 on the box 0 ≤ r ≤ 1/2, 0 ≤ f ≤ 1 ─────────────
let g: Vec<(String, Ex)> = vec![
("r".into(), r.clone()),
("(1/2 - r)".into(), ctx.rational(1, 2) - &r),
("f".into(), f.clone()),
("(1 - f)".into(), ctx.int(1) - &f),
];
// Family: 1, gᵢ, gᵢ·gⱼ (i ≤ j) — every product of at most two hypotheses.
let mut family: Vec<(String, Ex)> = vec![("1".into(), ctx.int(1))];
family.extend(g.iter().cloned());
for i in 0..g.len() {
for j in i..g.len() {
family.push((format!("{}·{}", g[i].0, g[j].0), &g[i].1 * &g[j].1));
}
}
println!("{} hypothesis polynomials", family.len());
let hyps: Vec<Poly> = family.iter().map(|(_, e)| e.as_poly(&gens).unwrap()).collect();
let hyp_refs: Vec<&Poly> = hyps.iter().collect();
// ── Goal ──────────────────────────────────────────────────────────────────
let goal_ex = ctx.rational(1, 4) - (&r - &f / 2).powi(2);
let goal = goal_ex.as_poly(&gens).unwrap();
println!("goal = {}", goal.to_ex());
// ── Coefficient matrix: rows = monomials, columns = hypotheses ───────────
let mut all = hyp_refs.clone();
all.push(&goal);
let basis = Poly::monomial_basis(&all).unwrap();
println!("basis: {basis:?}");
let m = Poly::coefficient_matrix(&hyp_refs, &basis).unwrap();
println!("M is {}×{}", m.nrows(), m.ncols());
let b: Vec<Q> = basis
.iter()
.map(|mono| goal.coeff_monomial(mono).unwrap().as_rational().unwrap())
.collect();
println!("b = {}", show(&b));
// ── Solve M·λ = b, λ ≥ 0 exactly ──────────────────────────────────────
let a_rows = m.to_rational_rows().unwrap();
let lambda = feasible_nonneg(&a_rows, &b).unwrap().expect("certificate exists");
for ((name, _), l) in family.iter().zip(&lambda) {
if !l.is_zero() {
println!("λ = {l:>4} · {name}");
}
}
// ── Verify 1: Poly arithmetic ─────────────────────────────────────────────
let mut acc = Poly::zero(&ctx, &gens).unwrap();
for (h, l) in hyps.iter().zip(&lambda) {
acc = acc.add(&h.scale(&ctx.from_ratio(l.clone())).unwrap()).unwrap();
}
println!("Σ λᵢhᵢ == goal (Poly::equals): {}", acc.equals(&goal));
// ── Verify 2: ratsimp on the unexpanded certificate ──────────────────────
let cert: Ex = ctx.sum(
&family
.iter()
.zip(&lambda)
.filter(|(_, l)| !l.is_zero())
.map(|((_, e), l)| ctx.from_ratio(l.clone()) * e)
.collect::<Vec<_>>(),
);
println!("certificate = {cert}");
println!("(goal − certificate).ratsimp() = {}", (&goal_ex - &cert).ratsimp());
// ── An integer certificate ───────────────────────────────────────────────
let n = rational_lcm_of_denominators(&lambda);
let ints: Vec<String> = family
.iter()
.zip(&lambda)
.filter(|(_, l)| !l.is_zero())
.map(|((name, _), l)| format!("{}·{name}", l * Ratio::from_integer(n.clone())))
.collect();
println!("{n}·goal = {}", ints.join(" + "));
// ── Infeasible: a false inequality and its Farkas certificate ────────────
let bad_ex = ctx.rational(1, 8) - (&r - &f / 2).powi(2);
let bad = bad_ex.as_poly(&gens).unwrap();
println!("\nbad goal = {}", bad.to_ex());
println!("bad(1/2, 0) = {}", bad.eval(&[&ctx.rational(1, 2), &ctx.int(0)]).unwrap());
let b_bad: Vec<Q> = basis
.iter()
.map(|mono| bad.coeff_monomial(mono).unwrap().as_rational().unwrap())
.collect();
// Same equalities through LpProblem so that we get the certificate back.
let mut lp = LpProblem::minimize(vec![Q::zero(); hyps.len()]);
for (row, rhs) in a_rows.iter().zip(&b_bad) {
lp = lp.eq(row.clone(), rhs.clone());
}
let sol = lp.solve().unwrap();
println!("status = {:?}", sol.status);
let y = sol.farkas.clone().unwrap();
for (mono, yi) in basis.iter().zip(&y) {
println!("y[r^{} f^{}] = {yi}", mono[0], mono[1]);
}
// y defines a linear functional L(p) = Σ_m y_m · coeff_m(p) on polynomials.
let functional = |p: &Poly| -> Q {
basis
.iter()
.zip(&y)
.map(|(mono, yi)| p.coeff_monomial(mono).unwrap().as_rational().unwrap() * yi)
.sum()
};
let mins: Vec<Q> = hyps.iter().map(|h| functional(h)).collect();
println!("min over hypotheses of L(hᵢ) = {}", mins.iter().min().unwrap());
println!("L(bad goal) = {}", functional(&bad));
assert!(mins.iter().all(|v| !v.is_negative()));
// ── Infeasible but true: an interior zero ────────────────────────────────
let touch_ex = (&r - ctx.rational(1, 4)).powi(2);
let touch = touch_ex.as_poly(&gens).unwrap();
let b_touch: Vec<Q> = basis
.iter()
.map(|mono| touch.coeff_monomial(mono).unwrap().as_rational().unwrap())
.collect();
println!("\n(r − 1/4)² : {:?}", feasible_nonneg(&a_rows, &b_touch).unwrap().map(|v| show(&v)));
println!("(r − 1/4)² ≥ 0 on [0, 1/2]: {:?}",
touch_ex.poly_is_nonnegative_on(&r, &ctx.int(0), &ctx.rational(1, 2)));
}Output
15 hypothesis polynomials
goal = -1/4*f^2 + f*r - r^2 + 1/4
basis: [[2, 0], [1, 1], [1, 0], [0, 2], [0, 1], [0, 0]]
M is 6×15
b = (-1, 1, 0, -1/4, 0, 1/4)
λ = 1 · r·(1/2 - r)
λ = 1/2 · r·f
λ = 1/2 · (1/2 - r)·(1 - f)
λ = 1/4 · f·(1 - f)
Σ λᵢhᵢ == goal (Poly::equals): true
certificate = 1/2*f*r + 1/4*f*(-f + 1) + r*(-r + 1/2) + 1/2*(-r + 1/2)*(-f + 1)
(goal − certificate).ratsimp() = 0
4·goal = 4·r·(1/2 - r) + 2·r·f + 2·(1/2 - r)·(1 - f) + 1·f·(1 - f)
bad goal = -1/4*f^2 + f*r - r^2 + 1/8
bad(1/2, 0) = -1/8
status = Infeasible
y[r^2 f^0] = 1
y[r^1 f^1] = 0
y[r^1 f^0] = 2
y[r^0 f^2] = 1
y[r^0 f^1] = 1
y[r^0 f^0] = 5
min over hypotheses of L(hᵢ) = 0
L(bad goal) = -5/8
(r − 1/4)² : None
(r − 1/4)² ≥ 0 on [0, 1/2]: Some(true)
Reading the result
The certificate. The solver found
1/4 − (r − f/2)² = r(1/2 − r) + ½·r·f + ½·(1/2 − r)(1 − f) + ¼·f(1 − f)
Every term on the right is a product of factors that are non-negative on the box, multiplied by a non-negative rational, so the left side is non-negative on the box. That is the whole proof. Multiplying through by the lcm of the denominators (rational_lcm_of_denominators) gives the integer form 4·goal = 4·r(1/2 − r) + 2·rf + 2·(1/2 − r)(1 − f) + f(1 − f), which a reader can expand by hand. (For this goal the multipliers are in fact unique — the LP polytope is a single point — but in general feasible_nonneg returns some vertex of the feasible set, and any one of them is a valid certificate.)
Two verifications. Poly::equals compares the normalised coefficient lists of Σ λᵢhᵢ and goal — a structural check that uses no simplification. (goal − certificate).ratsimp() starts from the unexpanded certificate (products of linear factors) and reduces the difference to rational normal form; 0 is the only normal form of the zero function. Agreeing by two different routes is cheap insurance against a bug in either.
The Farkas certificate. Lowering the constant to 1/8 makes the inequality false (bad(1/2, 0) = −1/8), and the LP is Infeasible. Instead of a witness λ, LpProblem returns a vector y with one entry per monomial row. Because all our constraints are equalities with λ ≥ 0, the module’s certificate condition reduces to Mᵀy ≥ 0 and yᵀb < 0. Read y as a linear functional on polynomials, L(p) = Σₘ yₘ·coeffₘ(p): the first condition says L(hᵢ) ≥ 0 for every hypothesis product (the smallest value is 0), and the second says L(bad) = −5/8 < 0. Any non-negative combination of the hᵢ would have L ≥ 0, so bad is not one — a proof of non-existence that is just as checkable as the certificate itself. (A point evaluation p ↦ p(r₀, f₀) is one such functional; the LP’s y is generally not a point, which is why the argument works even when the inequality is true but the family is too small.)
Infeasible does not mean false. (r − 1/4)² is non-negative on [0, 1/2] — poly_is_nonnegative_on confirms it exactly via a Sturm sequence — yet no Handelman certificate exists at any degree, because the polynomial has a zero in the interior of the box and products of the gⱼ vanish only on its boundary. Handelman’s theorem needs strict positivity. When a search comes back None for an inequality you believe, the options are: raise the degree of the products (for strictly positive goals this eventually works, at the price of O(dⁿ) columns), add squares such as (r − 1/4)² to the family (moving toward a Positivstellensatz / sum-of-squares certificate), or shrink the box away from the zero.
Key symplex features used
Ex::as_poly/Poly— the polynomial view with exact coefficients (Polynomials as Data)Poly::monomial_basis,Poly::coefficient_matrix,Poly::coeff_monomial— from polynomials to a linear systemMatrix::to_rational_rows—Matrix→Vec<Vec<Ratio<BigInt>>>for the LPlinprog::feasible_nonneg,LpProblem::eq+LpSolution::farkas— exact feasibility and certificates (Exact Linear Programming)Poly::scale,Poly::add,Poly::equalsandEx::ratsimp— two independent verificationsntheory::rational_lcm_of_denominators— the integer form of the certificateEx::poly_is_nonnegative_on— exact sign of a univariate polynomial on an interval
The one-call version, and a proof Lean can check
Everything above is what symplex::certificates::prove_nonnegative_on_box does for you: it enumerates the products of the box inequalities up to a degree, solves the exact LP (preferring few, low-degree products), re-verifies the identity with exact polynomial arithmetic, and — when the claim is false — returns an exact counterexample instead. Certificate::to_lean then writes the result as a Mathlib theorem whose proof is nlinarith over precisely the products of the certificate, so Lean only has to check linear arithmetic.
use symplex::certificates::{prove_nonnegative_on_box, BoxBound, BoxOutcome};
use symplex::prelude::*;
fn main() {
let ctx = Context::new();
let (r, f) = (ctx.symbol("r"), ctx.symbol("f"));
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) => {
println!("{cert}");
// -1/4*f^2 + f*r - r^2 + 1/4 = 1/2*f*r + 1/4*f*(-f + 1) + r*(-r + 1/2) + 1/2*(-r + 1/2)*(-f + 1), 0 ≤ r ≤ 1/2, 0 ≤ f ≤ 1
assert!(cert.verify());
print!("{}", cert.to_lean("quarter_bound").unwrap());
}
BoxOutcome::Refuted { point, value, .. } => println!("false: goal = {value} at {point:?}"),
BoxOutcome::Unknown(u) => println!("no certificate of degree {}", u.degree),
}
}The emitted theorem:
theorem quarter_bound (r f : ℝ) (h_r_lo : (0 : ℝ) ≤ r) (h_r_hi : r ≤ (1 / 2 : ℝ))
(h_f_lo : (0 : ℝ) ≤ f) (h_f_hi : f ≤ (1 : ℝ)) :
0 ≤ -(f ^ 2 / 4) + f * r - r ^ 2 + (1 / 4 : ℝ) := by
nlinarith [mul_nonneg (sub_nonneg.mpr h_r_hi) (sub_nonneg.mpr h_f_hi),
mul_nonneg (sub_nonneg.mpr h_f_lo) (sub_nonneg.mpr h_f_hi),
mul_nonneg (sub_nonneg.mpr h_r_lo) (sub_nonneg.mpr h_r_hi),
mul_nonneg (sub_nonneg.mpr h_r_lo) (sub_nonneg.mpr h_f_lo)]
This compiles against Mathlib (Lean 4.30.0) without errors or warnings — including with linter.style.longLine on, since every emitter wraps at 100 columns (lean::wrap_lean); cargo run --example certificates_to_lean out.lean writes a file with several such theorems that you can check with lake env lean out.lean inside any Mathlib project. The (r − ¼)²-style case from the previous section comes back as BoxOutcome::Unknown at every degree — exactly the interior-zero limitation of Handelman’s theorem — and a false claim such as xy − ½ ≥ 0 on the unit square is Refuted { point: [(x, 0), (y, 0)], value: -1/2, .. }.
Half-lines, interior double zeros, and the whole real line
Handelman needs a compact box and a goal that stays strictly positive inside it. Two extensions cover the cases that come up in practice:
- Half-lines
x ≥ a(orx ≤ a): withk = x − a, if every coefficient ofp(a + k)is non-negative that is already a proof, and when it is not, a Pólya multiplier(1 + k)^Nmakes it so (guaranteed for a strictly positive goal).prove_nonnegative_on_halflinedoes both, refutes false claims with an exact point, andprove_nonnegative_on_realsglues two half-lines into a proof for all of ℝ. - Even-multiplicity zeros inside the domain:
goal = g²·his split off by exact factoring andhgets the certificate; in Lean every hint becomesmul_nonneg (sq_nonneg g) (…). This works for boxes and half-lines alike.
use symplex::certificates::{prove_nonnegative_on_halfline, HalfLineOutcome, Ray};
use symplex::prelude::*;
fn main() {
let ctx = Context::new();
let j = ctx.symbol("j");
// (j − 5)²·(j² + 1) ≥ 0 for j ≥ 3: the double zero at 5 is inside the half-line.
let goal = (&j - 5).powi(2) * (&j.powi(2) + 1);
match prove_nonnegative_on_halfline(&goal, &j, &ctx.int(3), Ray::AtLeast, 12).unwrap() {
HalfLineOutcome::Proved(cert) => {
println!("{cert}");
// j^4 - 10*j^3 + 26*j^2 - 10*j + 25 = (j - 5)^2*(6*j + (j - 3)^2 - 8), j ≥ 3
println!("Pólya exponent {}, square {}", cert.polya_power(), cert.square().unwrap());
// Pólya exponent 0, square Poly(j - 5, j)
print!("{}", cert.to_lean("square_inside").unwrap());
}
HalfLineOutcome::Refuted { point, value, .. } => println!("false at {}: {value}", point[0].1),
HalfLineOutcome::Unknown(u) => println!("no certificate up to N = {}", u.max_polya_power),
}
}theorem square_inside (j : ℝ) (h_j_lo : (3 : ℝ) ≤ j) :
0 ≤ j ^ 4 - 10 * j ^ 3 + 26 * j ^ 2 - 10 * j + 25 := by
have hk : 0 ≤ j - (3 : ℝ) := sub_nonneg.mpr h_j_lo
nlinarith [sq_nonneg (j - 5), mul_nonneg (sq_nonneg (j - 5)) (hk),
mul_nonneg (sq_nonneg (j - 5)) (pow_nonneg hk 2)]
When the shift alone is not enough — j² − j + 1 on j ≥ 0 has a negative coefficient — the certificate carries the multiplier: (j + 1)·(j² − j + 1) = j³ + 1, and the Lean proof shows 0 ≤ (1 + (j - 0)) ^ 1 * (j ^ 2 - j + 1) with nlinarith [pow_nonneg hk 3] and divides by the positive factor with nonneg_of_mul_nonneg_right. A tight minimum costs a larger exponent (4j² − 6j + 3 needs N = 12), which is Pólya’s theorem being honest about how close to zero the goal gets.
Parametric polyhedra: a multiplier on the goal
A decision procedure over a polytope whose facets move with a real parameter j ≥ j₀ has to show, cell by cell, that a goal holds on the cell for every j — or that the cell is empty for every j. The certificate is again an exact identity with non-negative weights, but with one twist: the Farkas multipliers of j-dependent facets are rational functions of j, so a polynomial identity only exists after the goal is multiplied by a polynomial λ(j):
λ(j)·g = Σ μ · jᵃ (j − j₀)ᵇ · hₖ + Σ μ · jᵃ (j − j₀)ᵇ + μ₀ (+ Σ μ · hₖ hₗ), λ(j) = 1 + Σ νₐ jᵃ, μ, ν ≥ 0.
prove_nonnegative_on_polyhedron (0.4) runs the search staged — degree-1 multipliers with λ = 1 first, then higher degrees, pairwise products last — and returns the first certificate, re-verified by polynomial arithmetic. prove_polyhedron_empty is the same call with the goal −1.
use symplex::prelude::*;
use symplex::certificates::{ParamBound, PolyhedronOpts, PolyhedronOutcome, prove_nonnegative_on_polyhedron};
fn main() {
let ctx = Context::new();
let (j, r, t) = (ctx.symbol("j"), ctx.symbol("r"), ctx.symbol("t"));
// On { t ≥ r, t + j·r ≥ j + 1 } the goal t − 1 ≥ 0 holds for every j ≥ 0,
// but its multipliers are 1/(1 + j) and j/(1 + j): λ(j) = 1 + j is needed.
let hyps = [&t - &r, &t + &j * &r - &j - 1];
let param = ParamBound { var: j.clone(), lower: ctx.int(0) };
match prove_nonnegative_on_polyhedron(&(&t - 1), &hyps, Some(¶m), &PolyhedronOpts::default()).unwrap() {
PolyhedronOutcome::Proved(c) => {
println!("{c}");
// (j + 1)*(t - 1) = j*h0 + h1; h0 = -r + t, h1 = j*r - j + t - 1; j ≥ 0
print!("{}", c.to_lean("needs_lambda").unwrap());
}
PolyhedronOutcome::Refuted { point, value, .. } => println!("false: {value} at {point:?}"),
PolyhedronOutcome::Unknown(u) => println!("no certificate: {u}"),
}
}theorem needs_lambda (r t j : ℝ) (hj : (0 : ℝ) ≤ j) (h0 : 0 ≤ -r + t) (h1 : 0 ≤ j * r - j + t - 1) :
0 ≤ t - 1 := by
have hJ0 : (0 : ℝ) ≤ j := by linarith
have h0J := mul_nonneg hJ0 h0
have hg : (0 : ℝ) ≤ (j + 1) * (t - 1) := by
linarith only [h0J, h1]
have hg' := nonneg_of_mul_nonneg_right hg (by linarith only [hJ0])
linarith only [hg']
The proof shape is the one a person writes: one have … := mul_nonneg … per product the certificate uses (h0J is j·h₀; h0K would be (j − j₀)·h₀, h0xh1 a pairwise product, pJJ the pure power j²), then linarith only […] over exactly those facts; with λ ≠ 1, 0 ≤ λ·g is shown first and divided out with nonneg_of_mul_nonneg_right. An emptiness certificate concludes False. When the theorem statement is not yours to write — the goal lives inside a larger lemma — cert.lean_steps(&PolyhedronLeanNames { hyps: &["e0", "e1"], param_nonneg: "hJ0", shift_nonneg: "hK0" }, &opts) gives the same have lines, hint names and closing block with your hypothesis names, and to_block(" ") indents and re-flows them to Mathlib’s width. If the proof’s parameter is a cast natural, LeanOpts::default().with_symbol_text("j", "(j : ℝ)") renders it that way everywhere (0.5). To certify many goals against the same hypotheses, build a PolyhedronProver once and call .prove(&goal) per facet — or .prove_poly(&poly) when the goal is already an exact polynomial (a MultiPoly through Poly::from_multipoly, in any generator order), which skips the expression round trip (0.6.1). A goal polynomial may carry generators that occur in none of its terms — a tool’s ring has the parameter J on every row whether or not the row mentions it — and prove_poly ignores those even when the prover does not know them; only a generator that actually occurs and is not a variable of the hypotheses is an InvalidArgument (0.9.1). cert.used_hyps() names the hypotheses the identity really uses, so a generated lemma’s signature can list exactly those instead of scanning the emitted text for names.
Budgets (0.9.1). A deep cell with a couple of dozen j-dependent hypotheses can make the degree-3 pairwise stage run for minutes, and nothing in a tree builder should be able to do that unbounded. PolyhedronOpts::default().with_time_limit(Duration::from_secs(5)) gives every prove/prove_poly/prove_empty call five seconds from the moment it starts (so one PolyhedronProver built once gets a fresh allowance per goal; with_deadline(Instant) is the absolute form, and the earlier of the two applies), and with_max_pivots(n) caps the total simplex pivots across all of a call’s LPs — the stage LPs and the refutation’s sample LPs share one meter. When the budget runs out the answer is Unknown with u.budget_exhausted == Some(BudgetHit::Deadline | BudgetHit::MaxPivots) and a Display ending budget exhausted: deadline; a budget the search fits inside never changes a Proved or Refuted answer, and the certificate is byte-identical to the unbudgeted one. Underneath, LpProblem::with_budget(Budget::within(d).with_max_pivots(n)) is the same mechanism on a single exact LP: the simplex checks the budget at every pivot (the count is shared by the i64 → i128 → 256-bit → BigInt attempts, so an overflowed attempt does not get its pivots back) and reports LpStatus::BudgetExhausted — an answer with empty x/objective, not an error. Without a budget every pivot sequence is exactly what it was.
Assembling a whole proof: lean::Block
A generator that stitches many certificates into one lemma — a refine frame_lemma … ?_ ?_ followed by one bullet per facet, inside rcases case splits — should not concatenate strings with hand-counted spaces: Lean’s tactic blocks are column-sensitive (the tactics of a by block must sit strictly right of the tactic that opened it, and a · bullet moves that column by two), and a mis-indented line silently changes which block a tactic belongs to. symplex::lean::{Block, Tactic, Proof, Decl} (0.8) is a small structured model of exactly this: Tactic::have(name, Some(ty), Proof::by(block)), Tactic::bullet(block), Tactic::raw("linarith only […]"), and Block::render(indent) places every line from its tactic column and wraps past it. steps.block() gives a certificate’s closing steps as such a block, so a leaf is
use symplex::lean::{Block, Tactic};
let mut leaf = Block::new(vec![Tactic::raw(format!("refine {call}\n {}", vec!["?_"; facets.len()].join(" ")))]);
for steps in &facet_steps {
leaf.push(Tactic::bullet(steps.block()));
}
lemma_body.push_str(&leaf.render(" "));and the dispatcher’s rcases le_or_gt (0 : ℝ) (g) with h | h with its two bullets is Tactic::raw(…) followed by two Tactic::bullet(…), each bullet starting with Tactic::have("e6", Some("(0 : ℝ) ≤ …"), Proof::term("h6")). Decl::new(DeclKind::Lemma, name, statement, body).with_binders(…).with_doc(…) renders the header in Mathlib’s style (binders packed, : at the end of the binder lines, the statement on its own line, := by). lean::lean_ident quotes a name with «…» when it is not a plain identifier. The renderer’s output for the generator’s leaf shape is pinned to text that compiled against Mathlib.
Two refinements for generated files (0.9.1). The refine … ?_ ?_ … line above is better written as Tactic::apply("refine leafG346_single_poly", args) with the arguments — (20 * (j : ℝ) + 10), ρ, hx, twenty-eight ?_ — as a Vec<String>: the renderer packs them greedily onto the head’s line and onto continuation lines two columns past the tactic column, and because each argument is an atom it never breaks inside a parenthesised term the way a generic re-flow of a long string might; the result is a fixed point of wrap_lean, so a file that mixes both stays stable. And Decl has a preamble: Vec<String> (.with_preamble(vec!["set_option maxHeartbeats 400000 in".into(), "-- generated".into()])): lines emitted verbatim, unwrapped, before the doc comment — the place for set_option … in, open … in and a provenance comment. Adding the field means a Decl { … } struct literal from 0.8 now needs preamble: vec![]; Decl::new and the builders avoid the question.
Every shape the emitter produces (λ = 1, λ of degree 1 and 2, j₀ > 0, j₀ = 0, j₀ < 0, mixed J/K chains, pairwise products, emptiness with and without λ, pure parameter powers, no parameter at all) was compiled against Mathlib with the long-line linter on, and the emitted text is pinned to that compiled file in the test suite.
PolyhedronOutcome::Refuted carries an exact point of the set where the goal is negative (for the emptiness question: a point in the set), found by sampling j and minimising the goal over the cell with the exact LP when everything is affine in the free variables. The staged search costs a few milliseconds per facet for a cell with a dozen j-dependent hypotheses in a release build, which is what makes it usable inside a tree builder that asks thousands of times.
Where a leaf’s time goes. Certifying the ~50 facets of one leaf against one prover was profiled on the floor generator: assembling each LP from the stage columns is negligible (under 3 % of the certificate time), and the simplex itself was dominated not by pivot count but by arithmetic width — the fraction-free tableau’s entries are minors of the scaled system, so a 16-row certificate LP peaks around 70–120 bits and a 20-row one around 130–190, which sent almost every LP to i128 and the heaviest few percent to BigInt, where they cost ten times as much per pivot as all the others together. Three changes, each leaving every pivot sequence exactly as it was: the exact divisions of the fraction-free update are now a multiplication by the inverse of the pivot’s odd part modulo the word size, checked by one multiplication (Jebelean), instead of a long division; a 256-bit fixed-width cell type sits between i128 and BigInt, so those LPs never touch the heap; and a PolyhedronProver builds each stage’s product basis on the first goal that reaches it (most goals settle in the first stage, so the pairwise basis with its ½·m² products is usually never built). The certificate pipeline of a class run is 2.3× faster and the emitted Lean is byte-identical. A warm-started simplex (dual simplex from the previous facet’s basis) was measured and set aside: the LPs it could serve — those without λ columns, which change with the goal — are the cheap ones, and it would land on a different, equally optimal vertex when the optimum is degenerate (it always is here), changing certificates for a few percent of the remaining time. Since a PolyhedronProver now shares nothing mutable beyond those once-built bases, one prover may be used from several threads at once (&prover in a std::thread::scope); the certificates are the same as a sequential run’s.
See cargo run --example polyhedron_certificates and, for the exact geometry of the cells themselves (vertices, volume, cuts), symplex::polytope.
Sums of squares: interior zeros without a square factor
Everything above multiplies non-negative hypotheses. A polynomial that is non-negative on all of ℝⁿ with no hypotheses at all — (x − 1)² + (y − 1)², or x⁴ + y⁴ + z⁴ + 1 − 4xyz — needs a different certificate: a sum of squares g = Σ dₖ·pₖ². prove_sos (0.6) finds one exactly:
use symplex::prelude::*;
use symplex::certificates::{prove_sos, SosOpts, SosOutcome};
fn main() {
let ctx = Context::new();
let (x, y, z) = (ctx.symbol("x"), ctx.symbol("y"), ctx.symbol("z"));
let amgm = x.powi(4) + y.powi(4) + z.powi(4) - &x * &y * &z * 4 + 1;
match prove_sos(&amgm, &[x.clone(), y.clone(), z.clone()], &SosOpts::default()).unwrap() {
SosOutcome::Proved(c) => {
println!("{c}");
// x^4 + y^4 + z^4 - 4*x*y*z + 1 = (-1/3*x^2 - 1/3*y^2 - 1/3*z^2 + 1)^2 + 2/3*(-y*z + x)^2
// + 2/3*(-x*z + y)^2 + 2/3*(-x*y + z)^2 + 2/3*(-x^2 + y^2)^2 + 8/9*(-1/2*x^2 - 1/2*y^2 + z^2)^2
print!("{}", c.to_lean("amgm3").unwrap());
}
SosOutcome::Refuted { point, value, .. } => println!("negative: {value} at {point:?}"),
SosOutcome::Unknown(u) => println!("no decomposition found: {u}"),
}
}theorem amgm3 (x y z : ℝ) : 0 ≤ x ^ 4 + y ^ 4 + z ^ 4 - 4 * x * y * z + 1 := by
have h : x ^ 4 + y ^ 4 + z ^ 4 - 4 * x * y * z + 1 = (-(x ^ 2 / 3) - y ^ 2 / 3 - z ^ 2 / 3 + 1) ^
2 + (2 / 3 : ℝ) * (-(x * y) + z) ^ 2 + (2 / 3 : ℝ) * (-(x * z) + y) ^ 2 + (2 / 3 : ℝ) *
(-(y * z) + x) ^ 2 + (8 / 9 : ℝ) * (-(x ^ 2 / 2) - y ^ 2 / 2 + z ^ 2) ^ 2 + (2 / 3 : ℝ) *
(-x ^ 2 + y ^ 2) ^ 2 := by ring
rw [h]
positivity
The search is the Peyrl–Parrilo pipeline made exact: write g = mᵀ Q m over the monomials of half the degree, solve the semidefinite program for Q numerically (a small dense interior-point method is built in — no external solver), round the solution to rationals, project it back onto the coefficient constraints exactly, and test positive semidefiniteness with the rational L·D·Lᵀ of QMatrix::ldl_psd — whose factorisation is the decomposition. The Lean proof is two deterministic steps: ring checks the identity, positivity closes a sum of non-negative terms.
A goal with real zeros — every certificate the tree builder cares about touches zero somewhere — has only singular Gram matrices, which rounding cannot hit. prove_sos then does facial reduction: it reads the kernel off the numerical solution, makes it exact (directly when the kernel is rational, otherwise through its integer relations, found by LLL after Newton-refining the zeros of the goal to double precision), restricts the search to that face and solves again. Sums of two random squares whose common zeros are irrational algebraic points come back as exactly those two squares.
What it cannot do, it says so: Refuted carries an exact point where the goal is negative; Motzkin’s polynomial x⁴y² + x²y⁴ − 3x²y² + 1 (non-negative but not a sum of squares) is Unknown, never Proved. Certificates round-trip through JSON with re-verification like the others, and lean_hints gives the sq_nonneg (pₖ) terms for an nlinarith skeleton of your own.
The SDP has a budget too (0.9.1): SosOpts::default().with_time_limit(Duration::from_secs(10)) (or with_deadline(Instant)) is checked between interior-point iterations and between facial-reduction rounds, and when it passes the answer is Unknown with a reason starting budget exhausted: deadline that names the round it was in. The cheap answers that come before the SDP — an exact counterexample, a constant, odd degree — are unaffected, and a roomy limit gives the same certificate as none.