1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
//! Certificates on a parametric polyhedron (symplex 0.4).
//!
//! A decision procedure over a polytope whose facets move with a real
//! parameter `j ≥ j₀` has to show, for each cell, that a goal inequality
//! holds on the cell for *every* `j` — or that the cell is empty. Both are
//! exact Farkas-type identities with a polynomial multiplier `λ(j)` on the
//! goal, found by a staged exact LP and re-verified with polynomial
//! arithmetic. Every certificate exports as a Lean 4 / Mathlib theorem, or
//! as the bare `have …`/`linarith only […]` lines for an existing proof.
//!
//! Run with: `cargo run --example polyhedron_certificates`
use symplex::certificates::{
ParamBound, PolyhedronLeanNames, PolyhedronOpts, PolyhedronOutcome,
prove_nonnegative_on_polyhedron, prove_polyhedron_empty,
};
use symplex::lean::LeanOpts;
use symplex::prelude::*;
fn main() {
println!("=== Certificates on a parametric polyhedron ===\n");
let ctx = Context::new();
let (j, r, t) = (ctx.symbol("j"), ctx.symbol("r"), ctx.symbol("t"));
// The parameter bound j ≥ 2.
let param = ParamBound {
var: j.clone(),
lower: ctx.int(2),
};
let half = ctx.rational(1, 2);
// A cell of the (r, t) plane whose facets depend on j:
// 0 ≤ r ≤ 1/2, 0 ≤ t ≤ 1, (2j + 1)·t ≥ j·r + 1 (a j-dependent facet).
let hyps = [
r.clone(),
&half - &r,
t.clone(),
1 - &t,
(&j * 2 + 1) * &t - &j * &r - 1,
];
// ── 1. A goal on the cell: λ = 1 suffices ─────────────────────────────
let goal = (&j * 2 + 1) * &t * 4 - &j * &r * 4 - &r - 3;
let out =
prove_nonnegative_on_polyhedron(&goal, &hyps, Some(¶m), &PolyhedronOpts::default())
.unwrap();
match &out {
PolyhedronOutcome::Proved(c) => {
println!("certificate: {c}");
assert!(c.verify());
println!(
"λ = {}, terms = {}, degree = {}\n",
c.lambda(),
c.terms().len(),
c.degree()
);
println!("{}", c.to_lean("cell_goal").unwrap());
}
other => println!("{other:?}"),
}
// ── 1b. A goal that needs the multiplier λ(j) ────────────────────────
// On { t ≥ r, t + j·r ≥ j + 1 } the goal t − 1 ≥ 0 holds for every j ≥ 0,
// but its Farkas multipliers are 1/(1 + j) and j/(1 + j): no polynomial
// combination exists until the goal is multiplied by λ(j) = 1 + j.
let needs_lambda = [&t - &r, &t + &j * &r - &j - 1];
let j_nonneg = ParamBound {
var: j.clone(),
lower: ctx.int(0),
};
let out = prove_nonnegative_on_polyhedron(
&(&t - 1),
&needs_lambda,
Some(&j_nonneg),
&PolyhedronOpts::default(),
)
.unwrap();
match &out {
PolyhedronOutcome::Proved(c) => {
println!("certificate: {c}");
assert!(c.verify());
assert!(!c.lambda_is_one());
println!("λ = {}\n", c.lambda());
println!("{}", c.to_lean("needs_lambda").unwrap());
}
other => println!("{other:?}"),
}
// λ = 1 alone cannot do it:
let out = prove_nonnegative_on_polyhedron(
&(&t - 1),
&needs_lambda,
Some(&j_nonneg),
&PolyhedronOpts::single(3, 0),
)
.unwrap();
println!(
"with λ forced to 1: {}",
match out {
PolyhedronOutcome::Unknown { .. } => "no certificate (as expected)".to_string(),
other => format!("{other:?}"),
}
);
// ── 2. A false claim: refuted with an exact point ────────────────────
let false_goal = &t - &half - &r;
match prove_nonnegative_on_polyhedron(
&false_goal,
&hyps,
Some(¶m),
&PolyhedronOpts::default(),
)
.unwrap()
{
PolyhedronOutcome::Refuted { point, value, .. } => {
let shown: Vec<String> = point.iter().map(|(v, q)| format!("{v} = {q}")).collect();
println!("refuted: goal = {value} at {}", shown.join(", "));
}
other => println!("{other:?}"),
}
// ── 3. An empty cell for every j ≥ 2 ─────────────────────────────────
// r ≥ 1/2 together with (2j + 1)·t ≥ j·r + 1 and t ≤ 1/4 has no point once
// j ≥ 2 (the facet forces t ≥ (j/2 + 1)/(2j + 1) > 1/4 … exactly at j = 2 the
// bound is 2/5 > 1/4).
let empty_hyps = [
&r - &half,
(&j * 2 + 1) * &t - &j * &r - 1,
ctx.rational(1, 4) - &t,
];
match prove_polyhedron_empty(&empty_hyps, Some(¶m), &PolyhedronOpts::default()).unwrap() {
PolyhedronOutcome::Proved(c) => {
println!("\nemptiness certificate: {c}");
let steps = c
.lean_steps(
&PolyhedronLeanNames {
hyps: &["e0", "e1", "e2"],
param_nonneg: "hJ0",
shift_nonneg: "hK0",
},
&LeanOpts::default(),
)
.unwrap();
println!(
"\nproof steps for an existing skeleton:\n{}",
steps.to_block(" ")
);
println!("{}", c.to_lean("cell_empty").unwrap());
}
other => println!("{other:?}"),
}
// ── 4. The same machinery without a parameter: plain Farkas ─────────
let fixed = [r.clone(), 1 - &r, &t - &r];
let out =
prove_nonnegative_on_polyhedron(&(&t * 2 - &r), &fixed, None, &PolyhedronOpts::default())
.unwrap();
println!("\nno parameter: {}", out.certificate().unwrap());
}