协调者，而非仲裁者——谁来处理失败
root-protocol第5条说失败要大声报出来——但报给谁？树结构是否需要一个常设的仲裁者/协调者角色来处理失败？答案借自 SAT 求解器最终收敛到的架构：这个功能是必需的；但常设的、有智能的仲裁者是一种反模式。
先例：DPLL(T) 的分工
在一个 SMT 求解器中（llm-as-fallible-theory-solver），SAT 核心就是协调者：它掌管赋值、已学子句（learned-clause）存储、以及回跳（backjump）计算——全部都是机械式的。理论求解器（theory solver）只负责校验或报告冲突。没有谁凭判断力去"仲裁"；架构把仲裁变成了一次图计算。
为什么这个功能是必需的——两样东西没有单个节点能独占
- 坏例库（no-good store）必须是全局的。 一个已学到的冲突（"这种分解形状会崩溃，因为 X"）如果锁在失败的父节点内部，兄弟子树就会重走同一条死路。按 conflict-learning-and-backjumping 的说法：赋值的回退是局部的，但知识是单调递增且全局的。
- 回跳目标是跨子树的。 一个失败子节点背后的元凶，可能是祖父节点层面的架构决策，也可能是某个兄弟子树的产物通过共享接口伸进来作的祟。把失败逐层往上传递是按时间顺序回溯（chronological backtracking）——每一个中间层级都会浪费预算去重试局部修补，而真正的元凶却在三层之上。回跳目标必须从冲突本身计算出来，而不是从树的形状推出来。
关键的改造：蕴含图 = 溯源图
CDCL 的冲突分析之所以是机械式的，正是因为蕴含图被记录了下来。放到 harness 里的对应做法：root-protocol 第4条已经要求每一步都声明自己的输入和方向——把"哪些决策产出了哪个产物"记录为依赖边（round-tree-flight-recorder），于是冲突分析就变成了图遍历：纯机械操作。 CDCL 给出的教训不是"要有一个仲裁者"，而是"把溯源记下来，仲裁就不再需要智能"。
为什么不要常设的 LLM 仲裁者
仲裁这个席位决定整个搜索接下来跳到哪里——它是系统里杠杆效应最高的位置。在最高杠杆点上安装一个会犯错的组件（它自己的 ε、自己的 α），会把 honest-caveats 描述的放大器拧到最大：一次错误的回跳会浪费掉整棵子树，而一个被 Goodhart 化的仲裁者会带偏整个搜索。所以：
- 协调者 = 机械内核：坏例库 + 溯源图 + root-protocol 的 B/
α账本 + 回跳计算。确定性的、可审计的、α为零。（具体而言：状态机加 sqlite 的 harness 内核——SAT 核心的同位素。） - 语义层面的冲突诊断，仅在溯源不够用时才需要（"这两个兄弟产物互不相容——是谁的锅？"）不是一个常设角色，而是又一个受门控约束、会犯错的动作：它产出一个产物（被诊断出的坏例/冲突子句），像其他一切一样要过一道门。
闭合回路：可读的检查会预先定位冲突
coupling-to-the-learner 的原则——检查产出的是梯度，不是裁决——在这里再次派上用场：一个抵达时已经被定位好的冲突（哪个断言、哪个输入、预期值与实际值）根本不需要语义层面的仲裁。门控越可读，协调就越机械。
处理失败需要的是记账员，不是法官——把溯源记下来，裁决就退化成图遍历；哪里还留有判断的余地，那也只是又一个受门控约束的动作，绝不是一把宝座。