跳转到内容
Aira 3D

Lane R Formal Verification：Phase 1 feasibility 与 Lean proof-kernel 起点

状态：Phase 1 delivered / full ambient isotopy not formalized

日期：2026-08-31

Lean project：formal/aira-lane-r

Proof mapping：lane-r-formal-proof-obligations.md

TCB：lane-r-formal-tcb.md

Certificate：lane-r-formal-certificate-v0.1.md

1. 裁决

Section titled “1. 裁决”

Lane R 可以从一个小而真实的 Lean kernel 开始，但不能在第一阶段诚实地直接形式化

LaneRCertificate(F, M, C) → AmbientIsotopic(F⁻¹(0), M).

原因不是 separator algebra 困难，而是完整结论横跨目前 mathlib 尚未直接提供的一整层基础设施： Freudenthal complex 的具体 realization、连续 PL function 的跨 simplex 微分语义、piecewise-smooth/Clarke regularity、带紧支撑的 flow、relative-boundary isotopy、isotopy extension，以及 tetrahedral normal surface 的 几何 stitching。

第一阶段选择了最靠近现有 checker、又能真正进入 Lean kernel 的中间结论：

  1. sign-aware interval dot lower bound 对 box 内任意真实 gradient 都 sound；
  2. vertex separator 的 barycentric interpolation 保留 smooth 与 PL gradient margin；
  3. 对任意 t ∈ [0,1]，该 interpolated field 与 grad F_t = (1-t) grad F + t grad F_PL 的 dot product 严格为正；
  4. 因而一个 certified simplex 内的 homotopy gradient 非零，特别是在 zero level 上没有 critical zero。

这些结论直接形式化 Lane R validation 文档 §3.2 的代数核心，但没有把 flow、isotopy 或 mesh correctness 偷渡成假设或布尔输入。

2. 工作隔离与主线审计

Section titled “2. 工作隔离与主线审计”
  • 独立 worktree（临时本机路径不作为证据身份）；
  • 独立分支：codex/lane-r-formal-verification；
  • 基线：本地 main 的 a52fb08990b2c44051a690a22c77b555cc3f18c4；
  • 仓库没有配置 Git remote，所以没有可抓取的 origin/main；“最新 main”在本任务中明确指上述本地 main；
  • 另一个 codex/lane-r-extensions worktree 位于独立路径，本任务没有复用或改写它。

审计并复用的主线资产包括：

  • Lane R 研究与方案 C 裁决： lane-r-pv-isotopy-research.md；
  • certified Gate： smooth-implicit-certified-pl-isotopy.md；
  • 18 项 proof matrix： smooth-implicit-pv-proof-obligations-v0.1.json；
  • schema、constructor、checker 与 spec；
  • current sealed report 和 adversarial corpus；
  • GeneralImplicit prerequisite、outward interval arithmetic、Freudenthal grid reconstruction、vertex-star separator、normal-surface rebuild 与 evidence reproducibility Gate。

Formal Lane 没有重写 production mesher，没有降低 checker 标准，没有修改 proof matrix，也没有把任何 unknown 升级成 pass。

3. 外部资料与 mathlib 可行性审计

Section titled “3. 外部资料与 mathlib 可行性审计”

3.1 数学路线

Section titled “3.1 数学路线”

主线所选 F_t 路线与 Boissonnat–Wintraecken 的 PL approximation 论文一致：论文以 (1-τ)f + τf_PL 和 generalized implicit-function argument 推导 smooth zero set 与 PL zero set 的 isotopy。 Plantinga–Vegter 提供 Lane R 既有 regular-grid/PV 语境；Boissonnat–Cohen-Steiner–Vegter 提供另一种 Morse/watershed 全局参照；Palais 的 restriction-map theorem 是最终 isotopy-extension 层的一项经典来源。

3.2 mathlib v4.33.1 的可复用层

Section titled “3.2 mathlib v4.33.1 的可复用层”

本项目锁定 Lean/mathlib v4.33.1。对该精确 revision 的本地源码审计结论：

  • Mathlib.Analysis.Calculus.Implicit 已有 Banach-space implicit function theorem、 ImplicitFunctionData 与 local/open partial homeomorphism 构造；
  • Mathlib.Analysis.Convex.SimplicialComplex.Basic 已有 geometric SimplicialComplex、faces、space、 vertices 与 facets；
  • Mathlib.AlgebraicTopology.SimplicialComplex.Basic 已有 abstract simplicial complex；
  • mathlib 有一般 homotopy 与 Homeomorph 基础；
  • 没有发现现成的 Isotopy/AmbientIsotopy structure、isotopy-extension theorem、Freudenthal tetrahedralization、normal-surface library，或直接把 regular level set 打包成 embedded submanifold 的 Lane R 专用 theorem。

因此可复用的是 calculus/topology/convex-complex 基础，而不是最终 Lane R theorem。完整形式化需要在 mathlib 之上新增项目层定义和若干可复用拓扑定理。

4. 已实现 Lean kernel

Section titled “4. 已实现 Lean kernel”

核心源码：

  • Basic.lean：有限维 vector、dot、barycentric interpolation、homotopy gradient；
  • Interval.lean：interval membership 与 sign-aware dot lower bound；
  • Certificate.lean：不含最终 claim 的低层 VertexStarCertificate 与 reconstructed ValidFor predicate；
  • Transversality.lean：正式 theorem。

正式通过 kernel 的主要 theorem：

productLower_le_product
dotLower_le_dot
separator_margin_of_interval
interpolated_dot_ge_margin
vertexStarWitness_implies_homotopyTransverse
intervalVertexStarWitness_implies_homotopyTransverse
intervalVertexStarWitness_implies_gradient_ne_zero
intervalVertexStarWitness_implies_noCriticalZero

其中最后四项是直接 Lane R 结论。正式 theorem 对 simplex vertex 数 m 和 ambient dimension n 泛化； production 使用 m=4, n=3。

4.1 精确 theorem boundary

Section titled “4.1 精确 theorem boundary”

Lean 已证明：给定 nonnegative、sum-to-one barycentric weights；给定每个 vertex 的 separator；给定 smooth/PL gradient 分别落在已验证 interval boxes 中；若每个 separator 的 interval dot lower bound 至少为两个正 margin， 则对任意 0≤t≤1：

0 < dot(interpolate(weights, separators),
        (1-t)·smoothGradient + t·plGradient).

于是该 local homotopy gradient 不等于零，并满足 NoCriticalZero。

Lean 尚未证明：

  • TS binary64 interval evaluator 确实生成这些 exact-real boxes；
  • smoothGradient 是 Field IR 对应 smooth function 的 derivative；
  • plGradient 是 conforming Freudenthal interpolant 的 simplex derivative；
  • vertex-star AABB enclosure 覆盖 simplex 中所有目标点；
  • interpolated separator field 跨 simplex 连续/Lipschitz；
  • total zero set 对 t 投影 proper/submersive；
  • flow 存在、唯一、全程留在 candidate band，或 relative-boundary isotopy；
  • isotopy extension；
  • F_PL⁻¹(0) 与 sealed triangle mesh 的 ambient isotopy。

5. Axioms、imports 与 sorry

Section titled “5. Axioms、imports 与 sorry”

lake build 中的 #print axioms 输出表明关键 theorem 依赖：

propext
Classical.choice
Quot.sound

这些是 Lean/mathlib 的标准公理依赖；没有项目自定义 axiom，也没有 sorryAx。所有 .lean 文件中没有 sorry 或 admit。证明使用 mathlib 的 real ordered-field、finite sums 和基本 tactic infrastructure；最终 proof terms 由 Lean kernel 检查。

6. 构建与复现结果

Section titled “6. 构建与复现结果”

工具链：

Lean 4.33.1
Lake 5.0.0
mathlib tag v4.33.1 / commit 0df444a360eaa60ab8c11dca51a86af692955474

命令：

终端窗口
cd formal/aira-lane-r
lake update
lake exe cache get
lake build
rg -n "\bsorry\b|\badmit\b" -g "*.lean" .

Phase 1 实测 lake build 成功；最终交付前再次执行完整命令并在提交报告中记录。

7. Formal audit soundness finding

Section titled “7. Formal audit soundness finding”

审计发现 current binary64 multi-axis edge-root predicate 不足以证明 affine edge membership。确定性 probe 与影响 分析见 lane-r-binary64-diagonal-root-soundness.md。

该 finding 是把 F_PL⁻¹(0) ≃ M 纳入 Lean 前的 blocker。它没有导致本任务静默修改 sealed evidence，也没有被 用来降低现有 Gate。Phase 1 transversality theorem 不依赖 binary64 mesh root，因此不受该问题影响。

8. 后续阶段与 Level 3 成本

Section titled “8. 后续阶段与 Level 3 成本”
阶段 交付 估算
L1（本阶段） exact-real interval lower bound、barycentric separator、homotopy transversality、no-critical-zero 已完成
L1.5 JSON/rational certificate parser、TS→Lean fixture bridge、closed concrete proof term、CI replay 4–8 engineer-weeks
L2-A uniform grid 与 Freudenthal complex、PL scalar continuity/gradient、candidate-band confinement 8–14 engineer-weeks
L2-B exact shared roots、tet normal triangle/quad uniqueness、stitching、embedded mesh；同时关闭 diagonal-root blocker 10–18 engineer-weeks
L2-C regular level-set/local implicit charts、piecewise-smooth generalized transversality、compact-support flow 16–28 engineer-weeks
L3 relative-boundary isotopy、ambient isotopy extension、composition、end-to-end certificate theorem 12–22 engineer-weeks
hardening parser/binding TCB reduction、negative certificates、proof performance、release CI 6–12 engineer-weeks

Level 3 总量约 52–102 engineer-weeks（12–24 engineer-months）。两名熟悉 Lean 与 differential/PL topology 的工程师可有限并行，但拓扑主链存在强依赖，现实 calendar time 约 8–15 个月；单人更接近 12–24 个月。 mathlib 缺失的 isotopy/PL topology 基础和 binary64 root blocker 是主要不确定性，估算应保留约 ±50% 风险。

这个估算针对真正的 kernel-checked end-to-end theorem；若把 smooth enclosure、isotopy extension 或 normal-surface correctness作为 axiom，工期会缩短，但 TCB 不会达到本任务定义的 Level 3。

9. 一手资料

Section titled “9. 一手资料”