> 一条主张的状态必须取自一个固定词表，而"UNKNOWN"要和"PROVED"一样显眼
一条把理论笔记和形式化验证绑起来的流水线，产出是一份主张账本： 每条主张一个 id、一段文本、一组 verify id、一组 artifact 路径。 三件设计值得抄。
结论先行¶
一条把理论笔记和形式化验证绑起来的流水线，产出是一份主张账本：
每条主张一个 id、一段文本、一组 verify id、一组 artifact 路径。
三件设计值得抄。
① 状态取自固定词表，而且 UNKNOWN 是一等状态。
{"id": "t9-corrected-h2-le-h1-gauss", "backend": "sympy", "status": "UNKNOWN",
"detail": "no symbolic proof; 2000 random samples satisfy it (not a proof)
| z3: ERROR translate: unsupported for SMT: BooleanTrue in True"}
2000 个随机样本全过，账本仍然写 UNKNOWN，并且在同一行里括注 "(not a proof)"。
而 z3 的失败被记成 ERROR，不是记成通过。这是整份账本里最有价值的一行——
2000/2000 是极其诱人的"已验证"。
账本里还分得出：PROVED（本地证了）、REFUTED（有反例）、UNKNOWN（没证、也没反例）、
以及写在主张文本里的 "cite + assumption, not fully proved here" 和 "stays a CONJECTURE
in general, but the ⟨具体实例⟩ is now proved"。后两个很要紧：
一条"引了文献 + 带一条假设"的主张和一条"自己证了"的主张，在论文里能承担的重量不同。
② 被反驳的那一版，活在取代它的那一条里。 账本头部明写：
REFUTED note-errors are recorded in the claim text of the corrected claim that replaces them.
于是修正后的主张长成这样："……不动点是 M(1−a)/a，不是笔记里的 M/a
（那个常数已 REFUTED：t6-note-lemma1-constant，反例 a=1/2）"。
错误没有被删掉，它被钉在继承者身上。
③ 引文带页码，而且说明是哪一种页码。
"Borovkov, Probability Theory, Thm 11.3.2, printed p.324"——
printed 这个词在干活：它区分印刷页码和 PDF 页序。
另外有一条引文找不到对应教材，被回填成本地书库的一条 miss，而不是悄悄留着。
为什么¶
一份主张账本的全部价值在于：论文里每一句话都能回答"你凭什么这么说"，
而答案的种类是有限的几种，不是一段散文。 固定词表让这件事可查：
写正文的时候，一条 UNKNOWN 的主张就不能用"我们证明了"的句式。
UNKNOWN 必须和 PROVED 一样显眼，因为它是唯一会被四舍五入的状态。
没有反例、而且 2000 个样本都过——这在心理上和"证了"几乎没区别，
而在论文里差别是"我们证明"和"我们验证了一个实例"。
一个只有 PASS/FAIL 两种结果的检查器，会把所有 UNKNOWN 挤进其中一边，
而挤进哪一边取决于默认值。
而我在这份账本里也量到一处缺陷，正好说明词表不够：
三条 REFUTED 里有一条的反例字段是空的 {}。
| verify-id | 反例记录 |
|---|---|
| EMA 常数 | {"a": 0.5, "M": 130.83…} |
| 方差相减 | {"L": 1e-09} |
| 高斯最大化 H₂ | {} ← 空 |
空反例的 REFUTED 等于一句没有证据的断言。那条反例之所以没丢， 只因为人把它写进了主张文本（"the unit-variance Epanechnikov counterexample"）。 原因可以理解——那个反例不是一个被采样的数值参数，而是"换一个分布族"， 所以采样器没有东西可记。但这恰恰说明：反例字段必须能装下"结构"，不只是"一个点"。
同一张表还有第二层。方差那条机器记的是 L = 1e-09，
那里的违反在第 9 位小数上（1.002782070 对 1.002782072）；
而人写进账本的结构性反例 B = L·A 在 L = 0.9 处差 19 倍。
机器给你一个点，结构要人自己写下来。 点足以反驳，但只有结构能让你看出错得多厉害， 以及修补该往哪个方向走。
怎么用¶
- 主张账本的状态用固定词表，至少要有：本地已证 / 形式化已证 / 引用 / 假设 / 猜想 / 未知。写正文时按状态挑动词。
UNKNOWN要带上"我试了什么、为什么没成"，并且把数值抽样的结果 明确标成"不是证明"。抽样通过的数量越大，这行括注越必要。- 反例字段要能装结构，不只是采样点。 机器找到点之后，人补一句 "反例形态是 X"，并记下最坏情形下差多少。
- 被反驳的那一版写进取代它的那一条，不要删。否则同一个错误会在下一稿回来， 而且没人记得它曾被反驳过。
- 教材引文写章节号 + 定理号 + 页码，并说明页码种类； 找不到对应书的引文要回填成书库的缺口（见 检索工具说"没有相关工作"之前，先让它找一篇你已经知道存在的论文）。
- 相关：三条被反驳的步骤本身见 三个被机器反驳的步骤，全是把一个为真的命题搬到了邻近的对象上； 一个数要带上自己的来源戳见 仓里有四个稿件目录，一张没有出处的图传得很顺，然后到错的地方； "检测到了但没强制执行"见 自审的失效模式不是"没发现"，是"发现了没执行"。
出处¶
自己的 theory-audit 流水线第 4 步：THEORY_CLAIMS.yaml（主张↔verify-id↔artifact）
与 theory_verify.json（11 条记录，backend 为 sympy / z3 / lean）。
UNKNOWN 那条的原文、"recorded in the claim text of the corrected claim" 的头部注释、
以及 printed p. 的写法都在文件里；三条 REFUTED 的反例字段对比（一条为空）
和 19 倍 vs 第 9 位小数的对照是我这次数的。