Lane R Formal Verification TCB analysis

状态：Phase 1 complete

日期：2026-08-31

这里的 TCB 指：组件出错时，是否可能让一个数学上假的 AmbientIsotopic conclusion 被接受。

1. 当前 TypeScript Lane R 的 TCB

当前链路：

Typed Field IR
  → GeneralImplicit analysis
  → certified PL producer
  → independent TypeScript checker
  → schema/canonical hash/sealed evidence
  → validation prose supplies the topology theorem

1.1 Soundness-critical

组件	为什么在当前 TCB
Typed Field IR evaluator	grid samples 必须对应被 claim 的 `F`
GeneralImplicit interval evaluator	value/gradient ranges 的 inclusion 与 outward rounding 是 candidate confinement、smooth separator 的前提
`smooth-implicit-certified-pl-spec.ts`	定义 grid、Freudenthal tet、PL gradient、candidate band、separator interval dot；producer/checker共享这层
certified PL TypeScript checker	重建 prerequisite、mesh、star coverage、margins、topology 与 hashes
contracts/schema construction	它把验证结果绑定为最终 `pass` claims；错误绑定可把别的数据声明为同一 certificate
Node/V8 binary64 与 TypedArray semantics	interval rounding、root placement、buffer hash 都依赖这些精确语义
canonical serialization 与 SHA-256 binding	防止 field/prerequisite/witness/mesh 混用；hash collision 或 canonicalization bug 会破坏 source binding
validation 文档中的数学论证	flow、isotopy extension、normal-disk stitching 目前不是机器证明，由人工论证承担 soundness
运行环境的 code/data integrity	checker 可执行文件或 sealed bytes 被替换会破坏裁决

constructor 本身不应是 TCB：checker 不导入 constructor，且独立重建 mesh。separator 搜索也主要影响 completeness；但 producer 与 checker 共享 spec.ts 的定义和 interval helpers，因此该共享层仍在 TCB。

1.2 只影响 completeness/performance（在 checker 无 bug 的前提下）

closestConvexPoint 的 separator 搜索 heuristic；找不到 witness 可以拒绝，不应签发假证明；
constructor 的 traversal、polygon ordering 与 buffer emission；checker 重建不一致就拒绝；
fixture 数量、并行度、evidence collection UI；
GPU、Manifold、provider、backend；current checker 不调用它们；
subdivision depth 选择；过粗应 fail closed，只影响能否找到 certificate。

2. Phase 1 Formal Lane 的实际 TCB

当前 Lean prototype 证明的是 abstract exact-real conditional theorem，还没有解析 production certificate。因此它已缩小一段数学推理的 TCB，但没有把完整 Lane R checker 从 TCB 中移除。

2.1 已进入 Lean kernel 的部分

interval endpoint dot lower bound；
barycentric interpolation 的 convex margin；
smooth/PL homotopy gradient convexity；
gradient nonvanishing / no-critical-zero。

这些结论的 TCB 是：

Lean 4 kernel executable；
Real、finite-sum、ordered-field 等 mathlib definitions/theorem statements 与其 kernel-checked proof terms；
公理 propext、Classical.choice、Quot.sound；
.olean/source/toolchain 的 integrity；
对 theorem statement 是否表达目标数学语义的人工审计。

Lean elaborator、tactics 与 mathlib build tools产生 proof term；从逻辑 soundness 角度，最终 kernel 重新检查 proof term，所以不需要把 tactic heuristic 当成独立数学公理。不过实际部署若直接信任预编译 artifact 而不复核，则 compiler/build pipeline 仍是 operational TCB。

2.2 仍在 Phase 1 TCB / assumption boundary

JSON/decimal 到 exact real/rational 的 parser 尚未实现；
gradient box 的 inclusion 仍作为 Lean theorem premise，而非由 Lean Field IR evaluator推出；
smooth/PL gradient 与实际 F/F_PL 的对应关系仍是 premise；
simplex incidence 与 barycentric weights 的几何来源仍是 premise；
flow、isotopy extension、normal surface 与 mesh binding 未 formalize。

因此 Phase 1 的正式 verdict 是 kernel-checked local algebra under explicit premises，不是 end-to-end certified ambient isotopy。

3. Target Formal Lane TCB

理想链路：

untrusted geometry engine / producer
        │
        ▼
small exact certificate bytes
        │
        ▼
verified or deliberately trusted parser + source binding
        │
        ▼
Lean definitions + executable premise checks + theorem
        │
        ▼
Lean kernel

3.1 Soundness-critical target

组件	Target treatment
certificate parser	留在 TCB，或用 Lean parser/verified roundtrip 移入 kernel-checked code；必须绑定原始 bytes 与 decoded data
exact scalar semantics	canonical integers/rationals/dyadics，由 Lean 重验 denominator、order、dot、root parameter
Field IR denotation	Lean definitions；production evaluator 只提供候选 trace
interval enclosure trace	Lean executable checker重放；TS natural-interval evaluator只影响 performance/completeness
grid/Freudenthal reconstruction	Lean 从 bounds/depth 重建，不信任 producer 的 adjacency/coverage boolean
mesh binding	Lean 对 exact roots/triangles 或可证明 rounding certificate 重建，并绑定 sealed buffers
topology/isotopy theorems	Lean theorem；不从 `actualIsotopy=true` 输入
proof checking	Lean kernel + three standard axioms（除非后续进一步做 constructive reduction）

3.2 Target 中应退出 TCB 的组件

TypeScript/Rust producer；
separator optimizer；
production mesher；
current TypeScript checker；它仍可作为快速 preflight/diagnostics，但不能成为 formal verdict 的唯一来源；
JS runtime 与 floating-point heuristic；
fixture corpus、visual QA、performance profiling；
evidence collector；只要 Lean 对原始 source/certificate/mesh bytes 的 binding 独立可验。

这些组件出错时应最多导致 reject、timeout、较差 mesh 或无法找到 witness，不能导致 Lean 接受假 theorem。

4. Certificate/parser 的特殊风险

“Lean proof 通过”并不自动说明它证明了用户看到的 field 和 mesh。如果 parser 把两个 vertex 交换、丢掉 minus sign、错误解释 binary64，Lean 可能正确证明错误 decoded object 的 theorem。因此 source binding 必须包含：

Field IR canonical hash 与完整 denotation version；
domain/grid/Freudenthal version；
mesh position/index bytes 的 exact hash 与 endian/layout；
certificate exact-scalar encoding；
parser version 与 decode roundtrip test；
theorem scope/version。

在 verified parser 完成前，parser 与 binding layer明确留在 TCB；不能仅因为 core lemma在 Lean 中就把它们列为 untrusted。

5. Soundness finding 对 TCB 的影响

binary64 diagonal-root finding 说明当前 root placement/checker 与“root 位于 exact tetrahedral edge”之间还缺一个 sound bridge。Formal target 应优先使用 exact rational/dyadic root parameter；若必须输出 binary64，则 rounding proof必须证明：

rounded point 仍在同一 affine edge；
对所有 incident tetrahedra 使用同一点；
disk realization仍在对应 tetrahedron内；
rounding homotopy不穿过 vertex/edge/相邻 disk。

只把当前 TS strictInteriorEdgeRoots=true 复制进 Lean certificate 会把 soundness bug原样搬入新 TCB，禁止这样做。

6. TCB 缩减里程碑

里程碑	从 TCB 移除	仍在 TCB
Phase 1（当前）	separator convexity 的人工代数论证	TS enclosure、parser、geometry/topology prose
exact certificate bridge	decimal/dot/margin JS arithmetic	Field enclosure、complex/mesh/topology
Lean Field interval replay	GeneralImplicit TS inclusion correctness	parser binding、complex/mesh/topology
Lean normal surface	mesher/checker root/stitching correctness	parser binding、smooth→PL isotopy theorem
Level 3	current TS checker与全部人工 topology steps	parser（若未 verified）、Lean kernel、mathlib/axioms、system integrity