证书——收敛的单边证明

上级：relaxing-undecidability

你无法判定收敛性，但往往可以给出一个见证（witness）来证明它。找到见证 ⇒ 收敛性得证；找不到 ⇒ 结论不明。可靠但不完备——这是半可判定式的松弛版本。

Lyapunov 证书

一个函数 V(x) ≥ 0，仅在平衡点处为零，且沿轨迹严格递减（V̇ < 0），就证明了渐近稳定性。V 是一种只会耗散、绝不回补的能量——所以状态必然跌落到谷底。

这一步的实质，是把全局的、语义层面的问题（"所有轨迹都收敛吗？"）换成一个局部的、可检验的问题（"这个 V 是否处处递减？"）。

• SOS 规划（Parrilo；Positivstellensatz）：搜索一个可表示为平方和的多项式 V——这本质上是一个半正定规划问题。它把证书搜索自动化到某个次数上界之内（一个资源上界）。
• 秩函数（ranking function）：程序的终止性是不可判定的，但一个映到良序集、且每一步都严格递减的映射能证明它——这正是 [[pc-well-founded-recursion|P×C 良基递归]]。
• 屏障证书（Prajna）：一个把轨迹与不安全集合分隔开的函数，就证明了安全性。

联系： 门（gate）就是一次证书检查；recursion-convergence-contraction 的收缩系数 k<1 就是一个 Lyapunov 证书（V = 到不动点的距离）。harness 之所以能收敛，是因为它携带证书，而不是因为它能判定。