同构惊讶 9 · 具体 9 · 可行 9

现代 SAT 流程把”找证明”和”验证明”劈成两半：求解器可以任意启发式、任意出错，只要它吐出一份可校验的证明（DRAT/LRAT），一个很小的内核就能独立判定。De Bruijn 判据要的正是这个——信任基只剩校验器。这和 Simon 的 satisficing 是同一刀：证明搜寻是高成本、只能”够用即停”的启发式搜索，校验是廉价、可做到确定的判定。约束把它钉到硬件上：ATmega328P 只有 2KB SRAM，放得下只做校验的小内核，放不下任何像样的搜索。2KB 不是”缩小版的全能机器”，2KB 是对”谁负责搜、谁负责验”的一次物理表态。

如果要做在 Arduino UNO 上写一个只吃 DIMACS + 一小段 DRAT 片段的校验器，对 PHP(3,2)（三只鸽两只笼，UNSAT）返回”校验通过”；串口打印 verdict，板载 LED 亮起；把内核的信任边界写成注释贴在代码顶部。

文化隐喻惊讶 9 · 具体 9 · 可行 7

一篇 2025 年论文用 Lean 4 给出 satisficing 的机器验证刻画（把”够好就停”归约为一个容忍度参数 ε，并给出 ε<1/2 时阈值唯一的结论）。但公开复核指出：核心定理在代入辅助引理后塌缩为定义的重述，“有界理性溢价”是写进定义而不是推出来的；更关键的是，附录自己声明那段证明代码是 illustrative。也就是说，这篇论文在”验证”这件事上恰好执行了它自己的结论——用到手的最佳近似交付，而不是走到完全形式化。认知偏误与证明工程的交汇点不是”人会算错”，而是”人会选择在哪里停下”。

如果要做写一篇短文加一张”信任预算台账”：把一份形式化产物拆成”定义 / 重述 / 真证明 / 未验证代码”四栏，逐条标注每栏的置信来源；用同一张表审计自己手上任意一个形式化项目。

装置/原型惊讶 8 · 具体 8 · 可行 9

上述论文把 bounded rationality 归约为一个可调容忍度 ε，并在 ε<1/2 时给出阈值唯一性。这个 ε 在数学上是参数，在硬件上就是一个比较器的阈值。2KB 的机器做不了搜索，但完全做得了”按阈值判定”——这正是 aspiration level 的物理形态。把它做成装置：电位器就是 ε，输入一段被逐位喂入的候选证明，比较器在残差跨过阈值的瞬间给出 accept/reject，人转动旋钮就能看见”理性有多有限”这条曲线在什么位置翻面。形式化验证里最贵的从来不是算力，而是决定在哪一档停下的那份判断。

如果要做Arduino + 电位器 + 8 个 LED：LED 排表示阈值 ε 的 8 个刻度，串口喂入一串”证明步骤质量”数值，装置在跨阈值时锁定并亮灯；旋钮两端标成”最省事的通过”到”最严格的不过”。

同构惊讶 9 · 具体 8 · 可行 7

Frank-Wolfe 求 Wardrop 均衡是不动点迭代，收敛 O(1/k)——慢，而且早期迭代极不稳定（主流开源实现文档直言前几轮常出现线搜索数值错误）。16-bit 定点数只能表达约 4.8 位十进制精度，溢出高度非线性。两者合起来产生一个真实后果：城市交通均衡是自组织临界系统（在 I-24 MOTION 的轨迹数据里，拥塞同时表现出渗流相变与 1+1 维 KPZ 普适类），临界系统的不动点对扰动不稳健，量化误差不是”更粗糙的答案”，而是可能把求解器推往另一个不动点。计量学决定结论，不只决定小数位。

如果要做用 Q8.8 整数实现一个 20 节点双路由网络的分配，给每条链路的成本函数加上定点溢出注记，跑两种舍入模式（截断 / 四舍五入），对比最终流量分布差异，画成一张”同一座城市，两种不动点”的对照图。

方法论惊讶 8 · 具体 8 · 可行 8

有研究把交通流建模成 Ising 格上的元胞自动机，再用重整化群做空间粗粒化，粗粒化尺度可以是单辆车长的任意整数倍——这正是”自旋块求和”，只用到加法与比较。首尔公交客流数据也印证了这一点：站点强度的相关函数是幂律，强度涨落具有尺度不变性。幂律与尺度不变意味着可以跳过中间尺度，而整数块求和天然只表达”块内和”这一层信息。约束在这里不是妥协而是契合：整数版重整化少了浮点，却保住了真正承重的那部分——哪些量在尺度变换下不变。

如果要做取一小块 OSM 路网，用 int16 流量值实现 3 级块粗粒化，逐级打印块和与块内方差，验证”数据塌缩”是否只用整数就可见；再把它做成一个可交互的小页面。

文化隐喻惊讶 8 · 具体 8 · 可行 7

Charney、Fjørtoft 与 von Neumann 1950 年在 ENIAC 上跑出第一份数值天气预报，那份 24 小时预报的机时也接近 24 小时——团队只能勉强跟上天气，前提是机器中途不出故障。ENIAC 用的不是浮点硬件，而是十进制定点机。而 Lynch 在 2008 年做了那个复算：把同一个正压涡度方程写成一段小程序，在诺基亚 6300 手机上重跑 1949 年 1 月 5 日的同一组初始场，主循环不到一秒，结果与原稿非常接近。从 24 小时到不到一秒，跨过的不是精度——这套模型的精度一直是同一档——而是那个“刚好够用”的门槛。交通流建模与气象处在同一处境：模型尺度的选择（重整化群正是回答“哪个空间尺度最适合建模涌现行为”）比精度位数更决定成败。

如果要做用一块 16-bit MCU 实现一维平流方程的 Q8.8 版本，喂入一组历史观测做 24 小时外推，把输出与同期再分析场并排画出来，标题写”精度换可运行时间”。

装置/原型惊讶 9 · 具体 9 · 可行 8

CDLI 的转写格式 ATF 最初被定义成”只用 ASCII 字符的小规格”，今天仍然如此：Oracc 的扩展 ATF 必须转换成 Canonical ATF 才能进入 CDLI 仓库本体——扩展语法可以做研究，但不能做归档。CDLI 收录约 39 万件带楔文的器物及其转写，能被机器一代代重读，靠的正是这条”归档只收可降级为纯 ASCII 的形式”的硬规则。编译器这边有一条完全平行的线：GCC 内部的中间表示是 LISP 方言，而 SectorLISP 本身就是一个 C / JavaScript / Thompson Shell 的多语言混写文件。能长期存活的表示，总是那个能被最多种工具重新读出的表示。

如果要做写一个把编译器中间表示强制降级为”canonical 纯文本”的 pass：任何 pass 的输出必须先序列化成可读文本、再解析进下一 pass，禁止在内存里传二进制结构；用 awk/grep 就能在任意两步之间检查中间产物。

方法论惊讶 8 · 具体 8 · 可行 8

长期数字保存领域对格式的四条判据是 open / standard / non-proprietary / well-established，并明确指出 TXT、CSV 这类纯文本”更可能被今天的各类软件读到，也更可能在未来读到”。有趣的是，这个领域自己也承认：文件格式过时并没有成为当初预言的压倒性灾难，真正难的是规模与”什么时候动手迁移”。把这条经验搬到语言设计上：一个中间表示的可保存性不来自规范完备度，而来自”能否被最笨的工具读出来”。约束下的语言设计因此会偏向一个反常目标——不是表达力最大，而是每次 pass 的输出都能被 grep 与手工编辑。

如果要做拿一个现有小语言（例如一个小 Lisp 解释器），在每一步之间强制 dump/parse 纯文本、禁止任何内存内传递，统计总耗时与总字节数，写一份”文本化流水线的真实代价”报告。

声化惊讶 8 · 具体 8 · 可行 7

楔文有一类特殊文本叫 lexical lists（词表 / 符号表），从公元前三千纪中期一直抄到楔文文化结束，Oracc 的 Digital Corpus of Cuneiform Lexical Texts 中有一个专门子项目要把这批表全部数字化。这些表在书吏学校里被反复抄写、按顺序诵读——它同时是教材、词典和发音手册。把它和编译器并置：一份符号表在能被机器解析之前，先要能被人口头复述；而在纯文本约束下，一个语言的符号集合必须小到能被写进一张可通读的清单里，编译器读它，就像书吏读词表。声化在这里不是装饰：词汇表被读出来的那部分才是活的。

如果要做把一门小语言的 token 表导出成一张纯文本符号表，逐条标注”字形 / 读音 / 在语料中出现的顺序”，再录一段按出现频次降序朗读的音频，比较朗读顺序与代码里 token 的编码顺序。

同构惊讶 8 · 具体 9 · 可行 7

Unicode 的字符编码稳定性政策规定：已赋值的字符名是 immutable，永远不在后续版本里修改，连拼写错误也不会被”订正”，而每一个已发布的字符数据库版本是绝对稳定的。楔文研究里有一条平行规则：符号的同音读法编号必须跨符号表保持一致，因为没有这条约束，三千年间的文本就无法用同一套名字互相指称。两者交换的是同一件东西——用”错误不可修正”换取”任何年代的文本都能被同一个名字寻址”。编译器这边有这条契约的低配版：GCC 的 RTL 同时保有内部结构与可打印的文本形式，后者才是能被存档、被 dump、被逐版比对的那一半。

如果要做给自己手上一门小语言写一份”稳定性政策”：明确规定哪些 token 名与编码一旦发布就永不修改（包括错别字），并把这份政策做成一个 CI 检查，阻止任何后续改动触及已发布条目。