精读笔记
Problem Setting
这篇论文实际打的是 homogeneous polynomial Lyapunov converse conjecture：一个 globally asymptotically stable 的齐次多项式向量场，是否一定能找到齐次多项式 Lyapunov 函数。难点在于齐次系统通常是 converse Lyapunov 最友好的场景：局部/全局稳定等价，系统由单位球面上的动力学决定，而且已有结果保证任意有限光滑阶的齐次 Lyapunov 函数存在。因此如果连这里都没有 polynomial 证书，说明障碍不是一般非齐次系统的病态，而是 polynomial 类本身表达能力不足。
关键矛盾是：稳定性可以由一个角向依赖的齐次 Lyapunov 函数精确捕获，但这个角向 profile 不是三角多项式，且不能被任何正三角多项式以满足 Lie derivative 不等式的方式替代。以前路线卡在两个地方：rational converse 说明 denominator 可能有用但没排除去分母；degree lower bound 说明低阶 polynomial 不够但没排除所有阶。本文直接做 degree-independent obstruction。
Motivation
已有工作给出的图景是：smooth converse 太宽，polynomial/SOS 证书太窄，rational 证书夹在中间。真正缺的是一个能说明“不是 degree 不够，而是 polynomial 类型根本不够”的例子。齐次 cubic planar case 是最小非平凡场景：一维稳定系统有 x^2，线性系统有二次 Lyapunov，偶数次齐次向量场不能渐近稳定。因此如果存在反例，二维三次就是最干净的位置。
作者的核心观察不是从数值搜索一个难系统开始，而是把问题改写成单位圆上的 angular certificate 问题。只要能设计一个角向 forcing，使真实 Lyapunov 的 log-angular derivative 需要一个过大的 second harmonic，而正三角多项式的 logarithmic derivative 天生有 universal Fourier bound，就可以一次性排除所有多项式阶数。
Core Idea
论文的核心思想是把“多项式 Lyapunov 是否存在”从原空间的代数不等式问题，转成单位圆上正三角多项式的 Fourier 几何问题。齐次多项式 P 的 restriction 是 p(theta)>0；Lie derivative 不等式只约束 p'/p 与系统的角向/径向项。这样候选次数 2N 只进入归一化因子，而 Fejer-Riesz 分解把所有正三角多项式的 logarithmic derivative 控制在一个与 N 无关的 Fourier ball 内。
本质区别在于它不是尝试证明某个搜索松弛失败，也不是构造高 degree lower bound，而是找到 polynomial positivity 本身带来的硬约束。系统的 polar dynamics 被设计成有一个显式非多项式齐次 Lyapunov：H=r^2 exp(-5 sin 2theta)。这个 H 的作用是证明稳定性完全没有疑问，同时暴露出 polynomial restriction 的失配：需要指数型角向权重来抵消 cos 2theta forcing，而有限 Fourier 模式的正多项式无法在 logarithmic derivative 上提供足够幅度。
Method
第一步是构造二维三次齐次系统，使 polar 形式为 rdot=r^3(-1+5 cos 2theta), thetadot=r^2。它解决的是稳定性和反例结构的可控性问题：径向项有正有负，但角向速度始终正，轨道不断扫过角度，平均收缩可以通过角向 Lyapunov profile 捕获。
第二步是显式 Lyapunov H=r^2 exp(-5 sin 2theta)。它不是一个装饰性证书，而是整个构造的生成原则：H 的 log derivative 中 -10 cos 2theta * thetadot 精确抵消径向项里的 +10 cos 2theta，留下 -2r^2。代价是 H 只有 C1，不是 C2；而对二次齐次函数而言，C2 会强迫它是二次多项式。
第三步是排除齐次多项式 P。令 P=r^{2N}p(theta)，Lie derivative <=0 等价于 w(theta)=1-5 cos 2theta-g(theta)>=0，其中 g=(1/2N)p'/p。非负 w 且均值为 1 给 |w_hat_2|<=1；Fejer-Riesz 给 |g_hat_2|<1；但 w_hat_2+g_hat_2=-5/2，三者不兼容。这个证明的强点是完全不依赖 N。
第四步是排除局部实解析函数。解析 Lyapunov 的最低阶齐次 Taylor 项 P_m 必须非负，并且继承 Lie derivative <=0。论文再证明 P_m 不能在单位圆上有零点，因此它是正定齐次多项式 Lyapunov 候选，和前一步矛盾。
Key Insight / Why It Works
最关键的 insight 是：正定齐次多项式在圆上的 restriction 不只是“某个正函数”，而是正三角多项式；其 logarithmic derivative 的 Fourier 系数受 Fejer-Riesz 零点位置严格限制。这个限制是结构性的，不会因 degree 增大而消失。通常我们会以为增加 polynomial degree 可以逼近任意 smooth angular profile，但 Lyapunov 不等式需要控制的是 p'/p，而不是 p 的点态逼近；这正是本文抓住的缝隙。
真正有效的部分是 second harmonic obstruction。系统 forcing 的 cos 2theta 系数 b=5 太大，要求 g 和 nonnegative slack w 合起来提供 -5/2 的 second Fourier coefficient。非负 slack 的预算由均值控制，最多 1；positive trigonometric polynomial 的 log-derivative 预算也小于 1；总预算小于 2，抵不过 2.5。这是非常干净的 budget argument。
辅助但重要的是显式 H。它证明系统确实稳定，并说明缺失的不是 Lyapunov 函数，而是 polynomial/analytic regularity。rational Lyapunov R 进一步说明问题不是 algebraic certificate 全部失败，而是 denominator 在表达角向权重时提供了 polynomial 无法替代的自由度。
这不是 scaling，不是 data coverage，不是 engineering。它是一个表示类边界结果：polynomial positivity + derivative inequality 在 harmonic domain 里有不可突破的几何约束。可迁移的核心不是这个具体 cubic 系数，而是“用球面上的正函数因子化约束 certificate 的 logarithmic derivative”。
Relation To Prior Work
最接近的是 Ahmadi / Parrilo 关于 homogeneous polynomial Lyapunov converse 的问题，以及 Ahmadi-El Khadir 的 rational Lyapunov converse。此前结果已经说明 polynomial degree 没有统一上界，也说明 rational certificate 可以存在，但没有回答 denominator 是否总能去掉。本文的实质新增信息是：denominator 不能一般性去掉；更强地，连局部 real-analytic Lyapunov 都可能不存在。
和早期“无 polynomial Lyapunov”的非齐次反例相比，本文更锋利，因为齐次系统本来是最有希望保留 polynomial converse 的子类。和 SOS failure 也不同：这不是某个 SOS relaxation 不够强，而是所有多项式 Lyapunov 函数都不存在。
从技术谱系看，它属于 Lyapunov converse / real algebraic geometry / positive trigonometric polynomial 之间的交叉。看似新的是具体反例；真正创新是把非存在性证明压缩成 Fejer-Riesz 后的 Fourier coefficient budget，从而绕开逐 degree 代数消元。
Dataset / Evaluation
这篇论文没有 dataset / benchmark，evaluation 是数学证明。验证核心 claim 的证据形式是反例构造、解析证明、两参数族鲁棒性以及 Lean 4 formalization。对这类论文来说，这比实验 benchmark 更直接，因为 claim 是存在性/非存在性命题。
证明覆盖了几个关键层次：全局渐近稳定、显式 C1 齐次 Lyapunov、无齐次多项式 Lyapunov、无局部实解析 Lyapunov。两参数族 a>0, |b|>=2(a+1) 说明机制有开放区域，不是单点巧合。不过它没有说明如何在更一般系统中系统搜索或分类此类 obstruction；Lean formalization 支持正确性，但不扩大理论适用范围。
Limitation
主要限制是构造高度利用二维齐次系统的 polar reduction。单位圆上的 Fourier 分析在二维非常自然；到高维后对应的是球面调和、多变量正多项式和更复杂的因子化/矩问题，未必有同样干净的 universal bound。文中未充分说明这种 obstruction 的系统生成方法。
第二个限制是它解决的是 homogeneous polynomial Lyapunov converse 的否定，不直接给出稳定性不可判定性的完整答案。Tarski + degree bound 的路线被击穿，但 Arnold 问题的判定边界仍然没有由本文直接闭合。
第三，反例依赖较强的 angular forcing 幅度。两参数族给出鲁棒区域，但机制上仍是“second harmonic budget 不够”的特定设计。是否存在不依赖单一 harmonic、或在更自然动力系统中出现的同类障碍，文中未充分说明。
第四，smooth Lyapunov 仍然存在，甚至 flat C-infinity Lyapunov 可以由 exp(-1/H) 构造；因此该结果不是说稳定性证书不存在，而是说 analytic/polynomial 表示类不够。方法实际上把问题转移到 certificate regularity 和代数表达能力的边界上。
Takeaway
- 1. 齐次稳定系统也不能保证 polynomial Lyapunov；这个 conjecture 不是缺少 degree bound，而是存在性本身错误。
- 2. 对 Lyapunov certificate，逼近 V 本身不够，关键是能否逼近/满足 log-derivative 约束；这个视角比普通函数逼近更接近稳定性证明的本质。
- 3. rational Lyapunov 的 denominator 不是技术冗余，它可能承担真正的 angular reweighting 能力。
- 4. 值得迁移的工具是把齐次 certificate 降到球面，再用 positive polynomial factorization 给 derivative profile 建立 degree-independent obstruction。
一句话总结
这篇论文用一个二维三次齐次整数系数反例和 Fourier/Fejer-Riesz obstruction，终结了 homogeneous polynomial Lyapunov converse conjecture，并把问题本质定位为多项式正性证书在角向 logarithmic derivative 表达能力上的结构性不足。