Lane R Formal audit：binary64 diagonal-root soundness finding

状态：Open soundness blocker；exact-root kernel/bundle checker 已落地，rounding isotopy 尚未关闭

日期：2026-08-31

影响边界：freudenthal-linear-normal-surface@0.1.0 的多轴 tetrahedral edge root

本记录不修改既有 checker、proof matrix 或 sealed evidence。

0. 修复进度

下一阶段分支已经加入两层精确根基础：

• TypeScript 将每个 finite binary64 端点坐标和值无损解码成 dyadic rational，并序列化约分后的 gridEdge + parameter + exact point；共享边按 grid vertex id 规范化端点次序；
• Lean 证明 sign-changing linear edge 的 exact parameter 严格属于 (0,1)、插值值严格为零，且 exact point 位于开仿射线段上。

独立的 exact-root projection producer 在不修改 sealed v0.1 constructor 的前提下，随浮点 positions 一同返回 exactEdgeRoots。新的 bundle checker 会独立枚举 sign-changing grid edges、重建并哈希绑定 exact roots，同时绑定 field/domain/grid 与浮点 mesh buffers。current v0.1 isotopy checker 和 sealed evidence 仍不消费该 bundle，且 bundle 明确把 binary64 position semantics 标为 unproved perturbation。因此此 finding 尚未关闭。剩余关闭条件是证明 exact-root embedding 到 binary64 output embedding 的受控扰动保持嵌入/同痕，或明确把生产输出改为可表达 exact coordinates 的格式。

1. 发现

checkedReferenceRoot 与 constructor 的 strictInteriorRoot 先用一个 binary64 parameter 对每个坐标分别执行

left[axis] + (right[axis] - left[axis]) * parameter

然后只验证：相等坐标保持相等，变化坐标严格位于两个端点之间。这个判据对 axis-aligned grid edge 充分， 但对 Freudenthal face/body diagonal 不充分：坐标分别舍入后，结果可以不再对应同一个精确仿射参数，因而不在 Euclidean edge 上。

可复现实例：

left  = [10000000000000000, 10000000000000000, 10000000000000000]
right = [10000000000000004, 10000000000000008, 10000000000000012]
F(left) = 3, F(right) = -7, binary64 parameter = 0.3

computed point = [10000000000000002, 10000000000000002, 10000000000000004]
normalized parameters = [0.5, 0.25, 0.3333333333333333]

三个坐标都通过当前 strict-interior predicate；但 xy 二维叉积残差为 8，所以该点不在端点连线上。

运行：

node scripts/research-lane-r-binary64-diagonal-root-probe.mjs

2. 为什么影响 soundness

Freudenthal body diagonal 被同一个 cube 的六个 tetrahedra 共享。当前证明文字使用：

1. 每条 sign-changing tetrahedral edge 有一个共享 open-edge root；
2. 每个 crossing tetrahedron 内，这些 edge roots 张成一个 normal triangle/quad；
3. normal disks 沿共享 faces/edges 拼接，并可在 cell 内从 exact root 移到 binary64 root。

上面的 binary64 point 若不在 edge 上，就不再同时属于全部 incident tetrahedra；因此第 1 步的前提没有由 checker 建立，第 2、3 步也不能仅由 combinatorial manifold 检查恢复。schema 的 canonical decimal 没有量级上界， orderedAxis 只要求每轴有正 extent，因此当前公开 theorem domain 没有显式排除该数值形态。

这是 checker 局部验证条件中的真实证明缺口。当前 probe 没有构造一个通过全部 GeneralImplicit 与 separator Gate 的 端到端伪造证书，也没有证明现有三个 sealed sphere fixtures 受影响；因此本记录不回写、重签或删除已有 evidence。

3. 必须满足的修复条件

在 Formal Lane 把 F_PL⁻¹(0) ≃ M 标为 proved 以前，至少选择并验证一种方案：

• 以 exact rational/dyadic normal coordinate 表示 root，在 mesh 写出时另做有界 rounding；
• 存储一个共享标量 u，用可证明保持同一 edge 的 exact/filtered construction 生成坐标；
• 或对 binary64 point 做完整 affine edge-membership certificate，并给出 rounding 后仍在 incident normal disks 内的界。

只增加坐标包围盒、residual tolerance 或现有 closed-manifold 检查不能关闭这个 obligation。