Certificates — a one-sided proof of convergence

Parent: relaxing-undecidability

You can't decide convergence, but you can often exhibit a witness that proves it. Finding the witness ⇒ convergence proved; failing to find one ⇒ inconclusive. Sound, incomplete — the semi-decidable relaxation.

Lyapunov certificate

A function V(x) ≥ 0, zero only at the equilibrium, that strictly decreases along trajectories (V̇ < 0), proves asymptotic stability. V is an energy that only ever drains — so the state must fall to the bottom.

The move: replace the global, semantic question ("do all trajectories converge?") with a local, checkable one ("does this V decrease everywhere?").

• SOS programming (Parrilo; Positivstellensatz): search for a polynomial V expressible as a sum of squares — a semidefinite program. Automates certificate search up to a degree bound (a resource bound).
• Ranking functions: program termination is undecidable, but a map into a well-order that strictly decreases each step proves it — this is exactly [[pc-well-founded-recursion|P×C-well-founded recursion]].
• Barrier certificates (Prajna): a function separating trajectories from an unsafe set proves safety.

Tie: a gate is a certificate check; the contraction factor k<1 of recursion-convergence-contraction is a Lyapunov certificate (V = distance to the fixed point). The harness converges because it carries certificates, not because it decides.