跳转到内容
Aira 3D

Lane R R6.1 系统性 prior-art review 协议与初始矩阵

状态：Internal corpus Verified / awaiting second human reviewer and submission-date rerun 检索日期：2026-09-01 目标：判断 Lane R 的可发表贡献边界，不为“首次”声明倒推检索结果。

1. 研究问题

Section titled “1. 研究问题”

R6.1 分别回答，不把多个较弱问题混成一个 novelty claim：

  1. 是否已有算法对 smooth implicit surface 输出 ambient-isotopic PL mesh？
  2. 是否已有实现为每次 isosurface extraction 输出 independently checkable certificate？
  3. 是否已有 proof assistant 形式化 Marching Cubes、implicit meshing 或 normal-surface bridge？
  4. 是否已有系统把真实 binary64 vertex/index buffers 与 exact edge/normal data 做内容哈希绑定？
  5. 是否已有系统让小型 proof kernel 检查这些有限前提，同时把一般拓扑结论明确保留为外部 theorem？
  6. 是否已有 CAD/runtime 产品采用 Standard 默认、Certified 可选、fail-closed/no-fallback 的同类接口？

只有对六问均高度重合的工作才是“直接等价”；任何单项先例都必须进入 related work 和贡献降级判断。

2. 检索协议

Section titled “2. 检索协议”

数据源

Section titled “数据源”
  • 论文/元数据主源：Dagstuhl DROPS、Eurographics Digital Library、ACM/STOC 记录、IEEE/作者存档、Springer DOI、arXiv、DBLP；
  • normal-surface 主源：作者存档论文及期刊 DOI；
  • 工业能力基线：CGAL 官方文档；
  • web 搜索只用于发现候选，技术结论必须回到论文、作者页面或官方文档。

查询族

Section titled “查询族”

保存的核心查询包括：

"isotopic implicit surface meshing" certificate
"isotopic approximation of implicit curves and surfaces"
"topological correctness" PL approximations isomanifolds
"topology verification" isosurface extraction
"proof of correctness" Marching Cubes Coq
formal verified isosurface extraction proof assistant topology mesh
"normal isotopic" "standard vector representations"
"checking geometric programs" geometric structures
"certifying algorithms" checker witness computational geometry
"verification of certifying computations" Isabelle VCC
"proof-carrying" mesh geometry certificate verifier
Lean simplicial complex stellar subdivision formalization

纳入标准

Section titled “纳入标准”
  • 同位/拓扑保证的 implicit or isosurface meshing；
  • 可独立验证的几何/拓扑输出证书或 checker 架构；
  • proof assistant 中的 meshing、triangulation、simplicial/normal-surface 形式化；
  • 与 exact arithmetic、actual floating buffers、serialization identity 直接相关的工作；
  • 2026-09-01 前公开、可核对题录或全文的论文/软件文档。

排除标准

Section titled “排除标准”
  • 只讨论视觉质量、Hausdorff error 或 manifold repair 而无拓扑/同位 claim；
  • 只对输入 B-rep 拓扑做保形网格化，且不处理 implicit zero set；
  • 仅有营销页、二手摘要或不可核对的“verified”用语；
  • 与网格/证书/形式化都无关的一般 proof-carrying 系统只保留为方法背景。

外部与投稿关闭步骤

Section titled “外部与投稿关闭步骤”
  1. 由第二位真人研究者复核纳排、题录身份与“直接等价”判定；
  2. 投稿前用冻结的 query family 重新跑增量检索，并记录新的 cutoff；
  3. 若目标 venue 或 reviewer 要求，再扩大 theses、artifact proceedings 与 cited-by 去重范围。

内部 corpus、题录映射和越界措辞 Gate 已 Verified；在第二研究者与投稿前增量检索完成前，R6.1 不能标记 External Complete，也不能把 provisional novelty wording 升级为 priority claim。

机器证据：

3. 初始证据矩阵

Section titled “3. 初始证据矩阵”
工作 已证明/检查的核心 与 Lane R 重合 明确差异 裁决
Plantinga–Vegter 2004 interval arithmetic 驱动的 implicit curve/surface isotopic PL approximation smooth implicit、certified meshing、isotopy 未见 proof-assistant proof object、actual binary64 buffer identity 或内容哈希 artifact 强直接先例；Lane R 不得声称首次同位 implicit meshing
Plantinga–Vegter 2007 journal-scale interval/octree isotopic implicit-surface meshing algorithm 与实现 可实现的 certified implicit meshing、实际性能讨论 输出保证仍针对算法构造的 PL approximation；未见 per-output kernel artifact 或实际 buffer identity 2004 工作的重要延伸；强化“数学/算法目标已有成熟先例”
Plantinga–Vegter 2007, Certified meshing of families of isosurfaces 对远离 singularities 的一族 level sets 生成 isotopic meshes，uncertain boxes 显式标记 fail-to-certify/refine 思路、多个 isovalue 的 certified meshing 不是每次生产输出的 independent proof artifact；不绑定 binary64 buffers 直接反驳“只有 Lane R 才会在不确定时拒绝认证”的宽泛说法
Boissonnat–Cohen-Steiner–Vegter 2004 判据与 provably correct isotopic implicit surface meshing algorithm smooth→PL ambient topology 与 certifying algorithm 目标 Morse/mesh algorithm 路线不同；未见 per-output Lean/hash-bound artifact 强直接先例；论文贡献必须定位在实际 buffer/证据边界
Boissonnat–Wintraecken 2020 PL isomanifold topology conditions、Fréchet bound、带边界版本 Lane R smooth→PL theorem backbone 是一般数学 theorem，不是 Aira runtime/checker/formal artifact 外部 theorem dependency，不是系统 novelty
Lin–Yap–Yu 2013 numerical primitives 与 subdivision 驱动的 non-local isotopic approximation of nonsingular implicit surfaces 实用 isotopic implicit meshing、non-local correctness composition 不处理 Lane R 的 actual-buffer certificate/Lean boundary 另一条强算法先例；related work 不能只列 PV/BCSV
Burton 2010, Lemma 2.2 standard normal coordinates 相等 iff embedded normal surfaces normal-isotopic Lane R exact PL→actual mesh bridge normal-surface 基础理论，不处理 binary64、implicit meshing或证书系统 外部 normal-coordinate dependency；桥接实例化可能是 Aira glue
Chernikov–Xu 2013 Coq 检查 Marching Cubes lookup 的局部 cohesion/watertightness proof assistant + isosurface triangulation correctness 不证明 smooth zero set→actual mesh ambient isotopy；不绑定 runtime buffer/hash 形式化 meshing 强先例；禁止“首次形式化网格算法”
Etiene et al. 2009 用收敛/特征检查验证 isosurface extraction implementations 对真实实现做独立 verification V&V/实验验证，不是 per-output machine proof 工程验证先例，和 proof-carrying soundness 分开比较
Etiene et al. 2012 用 stratified Morse theory/digital topology 检查 isosurface topological invariants 独立拓扑验证、真实代码 bug detection 作者明确不是完整形式保证；未见 proof object/kernel 最接近的 topology-verification 工程先例之一
Custodio et al. 2013 修复 MC33 算法/实现的 topological-correctness 缺口，并发布可复现实例和 datasets 算法与实现分离审计、topology attacks、executable/reproducible artifact 保证相对 trilinear interpolant；不是 smooth true surface→actual buffer proof object 重要工程/复现先例，说明“topologically correct”实现会有隐藏 gap
Mehlhorn et al. 1999 基础几何任务的 program checker / geometric structure verification producer/checker 分离、几何输出检查 不针对 implicit isotopy，也无 Lean artifact checker 架构先例
McConnell et al. 2011 certifying algorithms 的一般 witness/checker 理论 certificate + independent verifier 设计原则 领域无关，不提供 Lane R 数学 方法论先例
Alkassar et al. 2013 VCC 验 checker implementation、Isabelle/HOL 验高层 witness property formal kernel + checker + certificate 分层 Lane R 当前 verifier implementation 未形式化；parser/hash 仍 TCB 比 Lane R 更强的 checker-verification 先例，必须在限制中承认
Cunningham–Zach–Friedl 2026 Lean 中 abstract simplicial complexes、links/joins/stars、stellar subdivisions Lean + combinatorial topology 基础 不处理 implicit meshing、normal surfaces、binary64 artifact 最新相邻 formal-topology 工作；可能成为 R4B 基础而非 R4A 替代
Lean sphere-eversion project Lean 中形式化 open ample h-principle，并导出 sphere eversion 证明助手可承载大规模 differential/geometric topology 研究 immersion regular homotopy，不是 embedded-surface ambient isotopy、meshing或 serialization R4B 可行性的强邻近先例，但不替代 Lane R 所需定理
CGAL 6.2 3D Isosurfacing production library 的 MC/Topologically Correct MC/Flying Edges 工业 isosurface implementation 与 topology-aware option 官方文档仍警告离散采样可能漏真实 surface/产生 artifact；无 Aira 式 proof artifact 工业 baseline，不支持 smooth true-surface ambient-isotopy 等价 claim
Topology-First B-Rep Meshing 2026 从 B-Rep 拓扑驱动、对 admissible tolerance 保持拓扑正确 近期 topology-guaranteed meshing 输入是 B-Rep 而非 smooth implicit zero set；未见 proof assistant/hash-bound certificate 邻近但非直接等价；R6 需追踪最终版本

4. 初始裁决

Section titled “4. 初始裁决”
  1. 已被先例覆盖： implicit isotopic meshing、normal-coordinate uniqueness、Marching Cubes 形式化、 isosurface implementation verification、certifying/checker 架构；这些都不能作为 Aira 的首次贡献。
  2. 初扫尚未发现直接等价： 同一系统把 production binary64 positions/indices、exact same-open-edge witness、 normal coordinates、canonical bytes/hash、independent verifier 与 Lean-checked finite premises组合起来，并只发布 published-theorem-backed-ambient-isotopy。
  3. 目前允许的 novelty 措辞： “Our initial review did not identify a directly equivalent end-to-end combination.”
  4. 目前禁止的措辞： “the first certified/isotopic implicit mesher”“the first formally verified mesh algorithm” “the first proof-carrying geometry system”。
  5. 最可能的论文贡献： 不是新的一般拓扑定理，而是 actual binary64/on-edge soundness bridge、真实 buffer 的 canonical identity、有限 premise proof object、fail-closed production integration 和透明 TCB/claim 分层。

5. 第一轮 citation-chasing 结果

Section titled “5. 第一轮 citation-chasing 结果”
  • Plantinga–Vegter 2004 的 journal 延伸、level-set family 工作以及 Lin–Yap–Yu 的 non-local isotopy 路线均强化了 “isotopic implicit meshing 已有多条成熟算法路线”的裁决；
  • Etiene 2012 的后续/相邻 MC33 修复工作表明，论文算法、公开实现和实际 topology behavior 必须分别审计；这与 Lane R producer/verifier/tamper separation 高度相关，但不是 proof-kernel artifact；
  • Chernikov–Xu 的公开元数据与作者 PDF 仍只支持 Coq 对 lookup-table/local cohesion/watertightness 的范围，未找到 smooth true surface 到实际 runtime buffer ambient-isotopy 的扩大结论；
  • Lean package/index 初扫发现 sphere eversion 与 abstract simplicial-complex formalization 等强几何拓扑先例， 但未发现 normal-surface coordinates、implicit meshing、binary64 buffer identity 三者的现成组合；
  • 本轮新增工作没有直接等价于 Lane R 的完整链，但显著收窄了可发表贡献：算法 correctness、拒绝不确定输入、 topology-aware reproducibility 和 proof-assistant geometry 均不能单独声称创新。

6. 当前不确定性

Section titled “6. 当前不确定性”
  • BCSV/PV/BW 的 theorem category 与 Lane R certificate-driven route 仍需在 R6.2 逐 theorem 对齐；
  • normal-surface bridge 应优先引用 Burton Lemma 2.2/Haken 基础来源，而不是只借 Agol 的背景段落；
  • Coq Marching Cubes proof 的准确范围需以完整脚本和 journal version 复核；
  • 2026 年新 Lean combinatorial-topology 工作需要做 forward citation/source-code review；
  • 缺少第二研究者与计算几何/低维拓扑专家的独立 novelty 和 theorem-statement 复核。