Lane R：PV regular-isotopy 证明研究

状态：Research complete / tetrahedral route implemented by a later Gate

日期：2026-08-31

研究范围：确认 Lane R 的项目内语义、证据现状、R1 可行路线与下一验证 Gate

本文件是架构选择前的研究记录；最终 implementation verdict 见 Smooth implicit certified PL isotopy Gate。

1. 结论摘要

后续实现已经采用本文件的方案 C（tetrahedral F_t），但把原先设想的 Hessian 路线收紧为更直接的一阶 vertex-star certificate：完整 incident star 的 outward gradient enclosure 与所有入射 PL gradients 共享严格 separator；这些 separator 在 conforming Freudenthal complex 上插值成一个连续 PL transverse field。新 Gate 已将 in-scope proof matrix 更新为 16 satisfied、0 source-mapped、0 blocked、2 out-of-scope。以下内容保留当时的 问题陈述、否定性 midpoint-fan probe 和架构比较，用于解释为何没有重复修补旧 constructor。

Lane R 在 Aira 中有一个准确且窄的含义：为 smooth、bounded、0 为 regular value 的隐式零集，研究可机器复验的 Plantinga–Vegter（PV）regular-isotopy 证明链。它不是 Lane F 的别名，也不是泛化的“研究泳道”。它的产品出口是 Lane F 的 F3 bounded meshing 与 F5 certified export，但两条 Lane 有独立预算、证据与启用条件。

当前证据链并非从零开始。18 项 proof obligation 已固定为 10 satisfied、2 source-mapped、4 blocked、 2 out-of-scope；当前 R1 是 PV3D-13 local relative-boundary deformation witness，并允许同时处理 PV3D-10/11 的 face-bubble / repeated-edge normalization。PV3D-14/15/16 的跨 cell stitching、全局几何无自交和 regular-isotopy 结论仍必须留给后续 Gate。

本轮新增的关键发现是一个可复现的否定性实验：**“沿现有 certificate 的 parameter axis，把原零集 graph 直接线性 插值到当前 midpoint + strict cell-center fan”不能作为通用 R1 捷径。**在全部 1,536 个 sign×axis×direction membership 中，486 个与单调方向相容；现有 extractor 可接受的 426 个 single-loop membership 里，只有 90 个 fan 沿该轴投影为无退化、无折叠的 PL graph，336 个失败。对现有真实 fixture：centered sphere 为 24/56 pass，off-grid sphere 为 57/306 pass。这个 probe 不否定更一般的 isotopy；它只排除了最简单、最容易误用的 graph interpolation 证明方案。

建议不要立即扩张 production 代码或直接发明 deformation schema。先开一个有界的 R1-design Gate，在两条路线间 做证据裁决：

1. 保留现有 cubical midpoint fan，补出 paper 中 normalization 与 block-local deformation 的显式、可拒绝 witness；
2. 改用 tetrahedral PL zero set，并证明 F_t=(1-t)F+tF_PL 的全过程 regularity，让一个全局 homotopy certificate 同时覆盖 local mapping、stitching 和 embeddedness。

第二条路线的证明出口更强，但需要 Hessian/二阶导 enclosure 与构造变化；第一条改动较小，却仍要独立解决后续全局 义务。R1-design Gate 的目标是用小型 checker spike 选定证明架构，不是预先承诺其中一条。

2. 问题定义与治理边界

2.1 Lane R 的项目内定义

权威路线图把 Lane R 定义为 “PV isotopy proof research”。恢复裁决位于 AIRA-LONG-TERM-ARCHITECTURE-PLAN.md，执行账本位于 ACTIVE_TASK.md。Git 历史中的首次命名提交为 4a7579a docs: resume PV isotopy proof research as Lane R；该提交说明：

• 下一 Gate 是 local relative-boundary deformation witness；
• 接续现有 proof matrix，不重开已经关闭的义务；
• 产品出口是 Lane F F3/F5；
• actualIsotopy、globalHausdorff、selfIntersection 在各自义务关闭前保持 unknown；
• Lane R 只能在独立任务、独立预算、独立证据提交中运行。

本仓库未配置 Git remote，也没有仓库内 issue 数据库；未发现专门的 Lane R TODO/FIXME。因而当前可审计的“issue”来源 是路线图、验证文档、机器 proof matrix、实现中的 fail-closed 状态和 Git 提交历史，而不是外部 issue tracker。

2.2 R1 的准确问题

输入是一个已经通过现有 prerequisite 的 cell 或相邻 cell block：

• F 在有界 domain 中光滑，0 为 regular value；
• interval enclosure 要么排除零，要么证明一个 gradient component 严格同号；
• corner signs、parameter axis/direction、face connectivity 与单环接受边界已经封存；
• 当前输出 patch 是由 grid-edge midpoint 和 strict cell center 构成的 embedded fan disk。

R1 必须给出或拒绝以下可检查对象：

1. 原始 F^{-1}(0) patch；
2. face bubble / repeated edge intersection 被处理后的 normalized representative；
3. 最终 PL patch；
4. 三者之间在 cell boundary 上兼容的 deformation，以及该 deformation 的全部 interval 前提。

“relative-boundary”在工程合同中不能只写一个布尔值。至少要明确：边界是逐点固定、按一个共享 face deformation 移动， 还是先 canonicalize 成共同边界后再固定。相邻 cells 必须引用同一份 face witness；否则 local pass 无法成为 PV3D-14 的输入。

2.3 明确非目标

• R1 通过最多可移动 PV3D-10/11/13；不得自动移动 PV3D-14/15/16。
• 一个 closed oriented combinatorial 2-manifold 不等于几何嵌入或 isotopy。
• midpoint、低 residual、Manifold NoError、视觉检查与 deterministic hash 都不是 isotopy 证明。
• 当前 uniform-grid v0.1 不承担 balanced octree、annulus 或 adaptive stitching。
• PV 论文明确没有直接提供本项目所需的全局 Hausdorff certificate；该 claim 保持独立。

3. 现状盘点

层	已有资产	已证明	仍未证明
Field / prerequisite	general-implicit-analysis.ts	outward value/gradient interval，excluded/regular/unresolved，proven axis/direction	Hessian enclosure；non-smooth seams
extraction	smooth-implicit-extraction.ts	deterministic midpoint buffers，single-loop fail closed，face connectivity，closed combinatorial manifold	actual isotopy；几何无自交
local fan	smooth-implicit-local-patch.md	当前 strict-center fan 是相对其 constructed loop 的 embedded disk	原 zero-set patch 到 fan 的 deformation
theorem applicability	smooth-implicit-pv-applicability.md	80/306 cell 的 axis direction + signs；1,536 membership 穷举	normalization；local/global isotopy
normalization subset	smooth-implicit-normalization-absence.md	off-grid sphere 全部 13,056 faces / 13,872 edges 无需 normalization	exact-zero fixture；一般 normalization deformation
proof ledger	smooth-implicit-pv-proof-obligations-v0.1.json	18 项状态、依赖与 forbidden shortcut 固定	6 个 pass 前置 blocker 尚未关闭

3.1 18 项矩阵的当前边界

机器矩阵是比路线图摘要更精确的状态源：

• PV3D-01..09 与 PV3D-12：satisfied；
• PV3D-10/11：source-mapped，paper 有论证，当前一般 witness 缺失；
• PV3D-13..16：blocked；
• PV3D-17/18：out-of-scope。

其中 exact-zero 存在两层不同语义，不应混写：PV3D-04 已证明 extractor 使用 symbolicPositive 的确定性 sign policy；但 normalization Gate 明确拒绝 centered exact-zero fixture，因为该 sign policy 对应的几何 perturbation 尚未成为可复验 isotopy witness。

3.2 当前实现对候选证明的约束

当前 local fan 的几何证明依赖：strict cube center、精确 edge midpoint、离散 boundary cycle 和凸 cell 的 radial uniqueness。它不依赖 parameter axis，也不保证 fan 沿 parameter axis 是 graph。另一方面，原零集的 PV interval 条件只保证它沿至少一个轴局部可参数化。两边使用的是不同的几何结构；R1 不能把它们仅凭“都是 disk”拼在一起。

4. 外部一手资料核验

4.1 Plantinga–Vegter 2004

主来源是 Plantinga 与 Vegter，Isotopic Approximation of Implicit Curves and Surfaces：

• Eurographics 条目与 DOI
• University of Groningen 作者存档 PDF

论文 §5 的 regular-grid 路径与仓库矩阵一致：cell interval condition 给出 axis parametrizability；ambiguous face 必须让相邻 cell 采用相同连接；face-interior bubble 通过 flatten/push 移除；同一 edge 上的连续交点对通过四-cell gradient cone 论证移除。论文这里提供的是几何论证，不是可直接序列化的 witness schema；尤其没有替当前 strict-center fan 给出逐 cell deformation map。

4.2 Boissonnat–Cohen-Steiner–Vegter 2008

Isotopic Implicit Surface Meshing 给出另一类全局证书：在 tetrahedral PL interpolant F_PL 周围构造 watershed/thickening，并用 smooth/PL Morse theory、collapse 与 index 条件推出 isotopy。 它的优点是结论全局；代价是算法假设 critical-point 信息，并引入 PL criticality、collapse 与 index matching，和 Aira 现有 PV cell witness 的距离较大。因此它适合作为“不要只看 local disk”的证明参照，不是首选增量实现。

4.3 Boissonnat–Wintraecken 2020

The Topological Correctness of PL-Approximations of Isomanifolds 给出更直接的候选架构：令

F_PL(x,t) = (1-t)F(x) + t F_PL(x)，

证明整个时空零集是 manifold，且对 t=constant 不相切，再由非消失 gradient flow 生成 isotopy。其可计算条件使用：

• 零集邻域上的 Jacobian/gradient 下界；
• gradient 上界；
• Hessian 上界；
• simplex 最大边长与 thickness。

这条路线和 Aira 的 interval/certificate 风格相容，但当前 Field checker只有一阶 value/gradient enclosure，没有 Hessian 合同，也没有与现有 midpoint cubical fan 等价的 F_PL。

4.4 Lin–Yap–Yu 2013

Non-local Isotopic Approximation of Nonsingular Surfaces 明确指出三维中 local rules 不足以自动推出正确全局曲面，并讨论把 local constructions 拼成 global isotopy 的额外困难。这直接支持 当前 proof matrix 把 PV3D-13 与 PV3D-14/15/16 分开，而不是在 R1 后自动升级全部 claim。

5. 本轮隔离实验

脚本：research-lane-r-axis-graph-probe.mjs

5.1 假设与判据

probe 只检验一个候选捷径：对每个 monotone-compatible 的 cube sign case，取当前 extractor 的 edge midpoints、boundary loop 与 strict cell center，将 fan 投影到 parameter axis 的正交平面。若所有 projected fan triangles 都非退化且方向 一致，则这个 PL fan 是该轴上的单值 graph；否则最简单的 graph-height interpolation 不能以它为终点。

这是针对该证明策略的必要结构检查，不是一般 isotopy 判定。失败不说明两个 disk 不 isotopic；成功也不证明原零集、 边界 normalization 或全局 stitching。

5.2 运行方法

pnpm --filter @aira/contracts build
pnpm --filter @aira/field-spike build
node scripts/research-lane-r-axis-graph-probe.mjs

5.3 结果

Corpus / fixture	候选数	axis-graph pass	fail
monotone-compatible memberships	486	—	—
extractor-accepted single-loop memberships	426	90	336
centered sphere meshed cells	56	24	32
off-grid sphere meshed cells	306	57	249

336 个 corpus failure 中，288 个含 projected degenerate triangle，48 个围绕 cell-center 投影发生 orientation fold。 当前两个 fixture 的结果证明这不是只存在于未使用 sign cases 的理论边界。

5.4 推论与限制

• 不能把 “原 patch 沿 axis 是 graph” 直接转写成 “当前 midpoint center-fan 沿同一 axis 也是 graph”。
• 若保留 graph-homotopy 思路，需要改变 boundary vertex placement、interior triangulation/apex，或先证明一个更一般的 boundary-compatible isotopy；这会重开当前 constructor-specific PV3D-12 的部分证据。
• 该 probe 不评估 paper 的更一般 block deformation，也不评估 F_t 全局 PL homotopy；二者仍是有效候选。

6. 候选方案与权衡

6.1 方案 A：保留当前 PV cubical fan，显式化 paper deformation

最小增量路径：

1. 先把 exact-zero-free 作为 R1 的明确接受子集，复用 normalization-absence 证书；
2. 对需要 normalization 的一般 cell/face/edge，序列化 bubble region、四-cell gradient cone、shared face map 与 deformation stage；
3. 为 normalized patch 到当前 fan 给出独立 block-local checker；
4. exact-zero symbolic perturbation 作为后续独立 branch，不能只沿用 sign policy。

优点：保留现有 extractor、buffer identity 与 PV3D-12；和现有 proof matrix 最接近。缺点：PV 论文的“linear interpolation”需要被补成无自交、边界兼容、可组合的具体映射；本轮 probe 排除了最简单的 axis-graph 版本；即使成功， PV3D-14/15/16 仍未关闭。

6.2 方案 B：把 local target 改成 parameter-axis graph mesh

为每个 regular cell 选择一个经过 interval 证明的 parameter axis；对 sign-changing edges 做唯一 root bracket，而不是固定 midpoint；在正交投影域内构造不折叠 triangulation，并让 interior vertex 的投影位于 domain kernel 内。原 zero-set graph 和 PL height graph 可通过高度插值连接，face boundary deformation 由共享 face witness 唯一定义。

优点：local witness 公式简单，checker 可以主要使用 interval monotonicity、2D exact predicates 与 root brackets。缺点： 会改变当前 mesh constructor 和 buffer identity；当前 embedded-center-fan 证明不能原样复用；不同 cells 选不同 axis 时的 face agreement仍是独立问题。这个方案应先只做 isolated constructor prototype。

6.3 方案 C：全局 tetrahedral F_t / PL-homotopy certificate

用一致的 tetrahedralization 定义 F_PL，对 F_t=(1-t)F+tF_PL 的 generalized Jacobian/gradient 做 interval 下界； checker 同时绑定 tetrahedra、vertex samples、simplex thickness、gradient/Hessian bounds 与失败 cell。若全过程 regular， gradient flow 给出 global isotopy。

优点：证明对象和输出 mesh 由同一个 F_PL 定义；天然处理跨 simplex continuity；成功时有机会同时关闭 local mapping、 global stitching、geometric embeddedness 与 theorem conclusion，并可进一步导出 Fréchet bound。缺点：需要 Field IR/interval checker 增加二阶导 enclosure；需要 tetrahedral target，不能直接认证现有 midpoint cubical fan；完整 theorem constant 与 finite-precision outward rounding 都必须在 checker 中落地。

6.4 方案 D：Morse/watershed/collapse certificate

按 Boissonnat–Cohen-Steiner–Vegter 的全局条件封存 PL critical points、watershed collapse sequence、smooth/PL index matching 与 thickening separation。

优点：全局结论明确，不依赖逐 cell fan graph。缺点：critical-point oracle、PL Morse 与 collapse checker 是一套新的重型 基础设施，和当前 Field operator/interval evaluator 的复用最少。除非方案 C 的 quantitative bounds 在实际 Field corpus 上 长期无法通过，否则不应优先实施。

7. 建议的下一步与可执行验证计划

7.1 先关闭 R1-design Gate

建议把下一提交限定为 proof-design evidence，不修改 production path：

1. 合同草图：定义 original / normalized / target 三阶段 identity、shared-face witness identity、claim boundary 和 unknown 传播；先不冻结公开 schema version。
2. 方案 A probe：只对 off-grid exact-zero-free sphere 尝试一个真实 cell 的 block-local deformation；要求 checker 从 Field + interval bounds 重放，而不是信任 pass 字段。
3. 方案 C probe：为 sphere primitive 增加 isolated analytic Hessian enclosure，构造固定 Freudenthal tetrahedra，验证 F_t gradient/non-tangency bound能否在 depth 3/4 通过。
4. 裁决：若方案 C 能在现有 sphere corpus 上以合理 subdivision 通过，并且 checker 不依赖未封存浮点采样，则选 C； 否则保留 A，但 R1 首版只接受 exact-zero-free subset，并把 symbolic perturbation 留作显式 follow-up。

7.2 两个 probe 的共同验收条件

• 所有 interval 运算 outward-rounded；任何 unsupported operator 返回 unknown/reject。
• witness 绑定 Field ID、domain/cell/block、上游 certificate hash、constructor version 与完整输入 hash。
• 独立 checker 从原输入重建核心量；producer 不能自签 theorem conclusion。
• 至少包含：正向 sphere、exact-zero、ambiguous face、two-loop、gradient near-zero、tampered bounds、stale upstream、 shared-face mismatch 八类 fixture。
• 重复运行 identity 稳定；负向 fixture 有固定 rejection code。
• R1-design 结束时 actualIsotopy/globalRegularIsotopy/globalSelfIntersection 仍为 unknown。

7.3 基线与回归命令

pnpm run verify:smooth-implicit-pv-proof
node scripts/research-lane-r-axis-graph-probe.mjs
pnpm run format:check
pnpm --filter @aira/contracts typecheck
pnpm --filter @aira/field-spike typecheck

8. 风险

风险	影响	止损线
把 paper prose 当 executable proof	产生无法独立重放的“证书”	每个 deformation 前提和 map 都必须被 checker 重建
exact-zero sign policy 冒充几何 perturbation	centered fixture 被错误纳入	两层 claim 分开；无 perturbation witness 就 reject
local pass 冒充 global isotopy	跨 face discontinuity或远端 self-intersection漏检	R1 不改 PV3D-14/15/16；shared-face identity 必须先设计
为证明迁就一个 sphere fixture	对一般 Field op 无效	加入至少一个非球 smooth GeneralImplicit fixture与 near-degenerate negatives
方案 C 的 Hessian contract污染 public Field IR	提前冻结错误协议	先留在 field-spike；通过 theorem/corpus Gate 后再 RFC
constructor 改动破坏既有证据 identity	历史报告与新证明混版	新 constructor/version/report；不重写历史 evidence
证明研究抢占 Lane F/主线	违反三轨治理	独立 task、预算、提交；production enablement 仍由 Lane F Gate 决定

9. 尚未解决的问题

1. R1 所称 relative-boundary 最终要采用“逐点固定”还是“共享 face deformation 后固定”的正式语义？
2. 当前 parameterAxis 只封存一个轴；若多个 gradient components 可证同号，是否应允许 checker 选择对 target mesh 更有利的轴？
3. 方案 A 能否为 strict-center fan 构造不依赖 axis-graph 的通用 block isotopy，且被有限 witness 表达？
4. 方案 C 所需 Hessian bounds 对 future smooth blend、gyroid/lattice 和 bounded repeat 如何组合传播？
5. F_t theorem 的 quantitative constants在 binary64 outward interval 下是否足够实用，还是会造成不可接受的过细 subdivision？
6. global geometric self-intersection 应由 isotopy theorem 蕴含，还是仍保留一个独立 exact/interval triangle checker 作为 defense-in-depth？
7. 当 Lane F 只需要可制造 export 而某个 Field 超出 certified subset 时，产品应 fail closed、降级为 uncertified export， 还是要求显式用户政策？该产品裁决不属于 Lane R。

10. 本轮研究的证据边界

本轮执行并通过现有 pnpm run verify:smooth-implicit-pv-proof；结果保持 10/2/4/2，下一 Gate 仍为 local relative-boundary witness。新增 probe 只读取/调用 isolated contracts 与 field-spike，不启动 backend/provider，不调用 Manifold/GPU，不改产品代码。它提供的是候选证明路线的反例边界，不是新的 isotopy certificate。

format:check、contracts typecheck 与 field-spike typecheck 通过。全 workspace pnpm run typecheck 也被尝试，但当前独立 worktree 没有 ignored/generated 的 packages/aira-occt-spike/custom-runtime/aira_occt_minimal.js，因此 OCCT spike 的四个 既有 import 报 TS2307；该失败与本轮文档/probe 无关，Lane R 的两个目标包已经单独通过。

11. 后续实现裁决与结果

在本研究提交之后，现有 midpoint fan 的 radial probe 又区分出两个关键事实：

• centered sphere 的 216 个 oriented triangles 对 sphere center 全部有严格同号 radial determinant；
• 既有 off-grid fixture 有 28 个反向 face 与 12 个 through-center face，因此不能把 radial theorem 泛化到全部 accepted extraction。

据此没有重开现有 constructor 或 PV3D-01..09/12，而是新增一个 fail-closed companion Gate：只在 exact sphere、 bounded dyadic coordinates、embedded projected one-skeleton、same-sign faces 与 degree-one regular ray 全部通过时给出 isotopy pass。centered fixture 最终通过 5,995 个 vertex-pair 与 52,326 个 edge-pair exact BigInt checks；off-grid、 non-dyadic、non-sphere、tamper 与 binding mismatch 全部被固定 rejection code 拒绝。

该子集使用一个 global radial ambient map，因而由更强证明 discharge PV3D-10/11/13/14，并直接满足 PV3D-15/16。generic proof matrix 仍为 10/2/4/2，generic extraction 仍为 actualIsotopy=unknown。完整 theorem、 claim boundary 与复验命令见 Smooth implicit radial isotopy Gate。