# 算法与信任边界

## 精确关系代数

13 种 proper interval 关系仅取决于四个端点的弱序。composition 涉及三个区间、最多六个端点；将任意实际端点的不同值压缩到 `0..5` 保留所有相等和严格小于关系。因此枚举这六个坐标上 15 种 proper interval 的 3,375 个三元组，就能构造全部 169 个原子 composition 项，而非近似采样。位集按析取分配，converse 交换方向。

这段枚举在 `Algebra::new` 执行一次；同一批任务应复用实例。它不是构建生成器，也没有从外部表拷贝常量。单关系分类只做比较，不做可能溢出的坐标减法。

## 网络与路径一致性

`Network` 封装名称数组、n² 域矩阵和原始来源。外部不能构造内部不对称/非法对角状态；数组输入和输出复制以隔离修改。每条约束取交集，并同步逆向关系。

传播反复对 `i<j` 执行 `Rij := Rij ∩ (Rik ∘ Rkj)` 并同步 converse，直到无变化、空域或预算用尽。每次成功缩减至少删一个 bit，因此无预算版本是有限的；单轮 n³ 级三元组检查，每次 composition 至多 13² 原子并集。实现按可解释的三元组操作计数，而不是壁钟超时。`is_path_consistent` 从完整矩阵复检；`verify_trace` 重放每步真实 composition 和 before/after，拒绝截断或伪造缩减。报告公开字段不等于不可篡改证书。

## SAT、UNSAT、Unknown

一般析取网络的路径一致性不足以证明 SAT。搜索对当前最小非单元素域做 MRV 分支，每个子分支只保留一个 atom；节点和传播操作预算在整棵搜索树共享。未耗尽的完整分支排除才能给 UNSAT。达到预算立即返回 Unknown；不会跳过未搜索分支后仍宣称不可满足。

原子叶子转为端点等式及严格不等式：union 合并等式，在等价类 DAG 上拓扑排序并赋不同秩；严格自环/有向环则不可实现。为不同等价类分配不同秩不会破坏原子关系约束。生成见证最后检查全部域。搜索最多 24 区间、最大 276 层两两关系选择；最坏复杂度指数级，不承诺大型网络实时可解。

`possible_relations` 对每个候选 atom 分别求解；结果分成 possible/impossible/unknown，可行 atom 有见证。已不在输入域的 atom 可直接列 impossible。查询的假设不追加用户来源，因此满 sources 容量时仍可查询。蕴含先排除矛盾/未知前提，再求 claim 补集上的反例。

## 来源解释、变换和观测

删除式核提取从原始 sources 重建网络，先证实 UNSAT；只有删去约束后仍证实 UNSAT 才真删除。Unknown 不能作为删除依据。单调性保证，成功遍历且没有 Unknown 才能宣称 subset-minimal；它不是最小基数核。各删除尝试有独立搜索预算，检查次数另受上界约束。

观测导入只保留两两定性关系，丢弃数值时长。部分观测只检查已给的名称；合并按名称而非位置。诱导子矩阵不保留所有可能的高阶依赖，不声称逻辑投影完备。

## 测试独立性与局限

生产分类和 composition 共享比较函数，单纯代数律不足以排除共同错误。`oracle_wbtest.mbt` 另写 13 个端点谓词，枚举 0..5 上全部端点赋值，对 2,197 种原子网络和 256 种确定性析取网络比较 SAT/UNSAT，并检查 witness。样本有限；这不是形式化证明或全部 24 节点网络穷举。其余测试覆盖位集、极值、预算、来源容量、轨迹伪造、核、数据交换和三个下游流程。不发布未实测的性能或覆盖率百分比。