Swap-2C · provable control

The Lyapunov certificate

An inverted pendulum, stabilized. A quadratic Lyapunov function is checked by interval branch-and-bound — a real proof, not a sample. Green where V̇<0 is certified; red where a counterexample exists.

Verdict

—

Boxes proven

—

Certified ROA

—

Proportional gain k_p

Derivative gain k_d

V̇<0 certified counterexample undecided ROA {V<c*}

Click the phase plane to drop a trajectory. Interval enclosures are inflated for float-safety — the certificate is sound, not just sampled.