> 三个被机器反驳的步骤，全是把一个为真的命题搬到了邻近的对象上

结论先行¶

把自己写的几份理论笔记交给一条"每条引理都要有一个 sympy/z3/Lean 的 verify-id"的流水线审一遍， 三个步骤被反驳。回头看，三个是同一种错误： 把一个在某个对象上为真的命题，搬到了一个长得很像的邻近对象上。

三条我都独立复核了一遍（不是调用项目代码）。

① 方差不能相减。 反例结构是 B = L·A：

L=1e-09  Var(A-B)=1.002782070  声称 ≥ 1.002782072   VIOLATED
L=0.1    Var(A-B)=0.812253478  声称 ≥ 0.992754251   VIOLATED
L=0.9    Var(A-B)=0.010027821  声称 ≥ 0.190528594   VIOLATED  ← 差 19 倍

正确的步骤是标准差的反向三角不等式 Var(A−B) ≥ (sd_A − sd_B)²， 而且在 B = L·A 上取等号（上表第四列逐行精确相等），所以它是能拿到的最好的界。 代价是两条：常数从 1 − L² 变成 (1 − L)²，而且需要新增假设 L < 1。

② 高斯不最大化 H₂。 单位方差下，Rényi-2 微分熵 h₂ = −log ∫p²：

高斯          ∫p² = 0.282094792   h2 = 1.265512123
Epanechnikov  ∫p² = 0.268328157   h2 = 1.315544580   ← 更大
数值校验：∫p = 1.000000000   var = 1.000000000   ∫p² = 0.268328157

单位方差的 Epanechnikov 核（p(x) = 3/(4√5)·(1 − x²/5) on [−√5, √5]）的 h₂ 比高斯大 0.050。 归结为一条可形式化的不等式：6√(5π) = 23.78 < 25。 而原命题（一个上界）仍然成立，只是要换一条路走： H₂ ≤ H₁（Rényi 熵对阶数不增）≤ H₁(高斯)（最大熵）。命题没动，路线换了。

③ I ≤ h(Z) 对微分熵不成立。 取 Z = X + ε，X ~ N(0,1)，ε ~ N(0,t²)：

t=1.0    h(Z)= 1.765512  h(Z|X)= 1.418939  I=0.346574   I<=h(Z)?  True
t=0.1    h(Z)= 1.423914  h(Z|X)=-0.883647  I=2.307560   I<=h(Z)?  False
t=0.01   h(Z)= 1.418989  h(Z|X)=-3.186232  I=4.605220   I<=h(Z)?  False

机理一眼可见：h(Z|X) 是负的。离散情形的证明用的是 H(Z|X) ≥ 0， 而微分熵没有这条性质。t → 0 时 h(Z|X) → −∞、I → ∞，而 h(Z) 有界—— 不是差一点，是差无穷。 这一条没能救回来：要成立必须引入观测噪声模型， 也就是改了被建模的东西。

为什么¶

三种结局值得分开记，因为它们对论文的代价完全不同：

第二种最容易被漏：修补之后式子还在、结论还在，但多了一条假设， 而那条假设必须回到所有引用处重新核一遍。一个"修好了"的引理带着一条没人检查的前提， 比一个明显错的引理更难发现。

还有一条关于怎么发现它们的教训，来自第四个被反驳的常数（一个 EMA 跟踪滞后的不动点， 笔记写的是 M/a，正确的是 M(1−a)/a）：

a=0.5    测得滞后=1.000000000   M(1-a)/a=1.000000000   M/a=2.000000000
a=0.1    测得滞后=9.000000000   M(1-a)/a=9.000000000   M/a=10.000000000
a=0.02   测得滞后=49.000000000  M(1-a)/a=49.000000000  M/a=50.000000000

机器给出的反例是 a = 1/2，那里错了整整一倍。而在实际使用的小 a 区间， M/a 和 M(1−a)/a 只差 2%——人工复核在工作区间里看不出来。

随机采样之所以比人工复核强，正是因为它不尊重你的工作区间。

怎么用¶

• 写证明时，每一步问一句"这条性质属于哪个对象"。离散熵→微分熵、 阶 1→阶 2、标准差→方差、期望→中位数，都是"长得很像但性质不同"的相邻对。 搬过去之前先找反例，找不到再用。
• 三个最常被误搬的事实，直接记住： 微分熵可以是负的（所以一切用 H ≥ 0 的推导都要重做）； 最大熵性质是关于 H₁ 的，不自动给 H₂；方差不满足三角不等式，标准差满足。
• 一个被反驳的步骤修好之后，显式写下"这次修补新增了什么假设"， 并回到所有引用处核一遍。换常数的那一类最危险。
• 找反例要在整个合法参数域上采样，不要在工作区间里采。 工作区间里的常数错误可以小到 2%，而它在别处是一倍。
• 相关：一个展示出来的界就是一条可执行的断言，见 一个写出来的界是可执行断言——拿它自己声明的参数范围去跑，我的界被我的反例推翻了； 定理预测的退化情形要真的去测，见 你的定理预测了一个退化情形——那就拿代码去测它，别等审稿人问； 账本怎么记这些状态见 一条主张的状态必须取自一个固定词表，而"UNKNOWN"要和"PROVED"一样显眼。

出处¶

自己的几份理论笔记（markdown，不是 LaTeX）过一遍 sympy / z3 / Lean 的验证流水线， 三条 REFUTED 加一条常数错误。上面四组数字（19 倍的违反与取等、 Epanechnikov 的 h₂ = 1.3155 对高斯 1.2655 并有数值积分校验、 t=0.1 时 I=2.31 > h(Z)=1.42、EMA 滞后在 a=0.5/0.1/0.02 上精确等于 M(1−a)/a） 都是我这次用独立实现复核的。被反驳的是错误步骤，不是任何论文的结论。