Lane R S1.1：published theorem contract audit

状态：Closed / certificate-driven theorem integration locked

日期：2026-09-01

当前入口：Lane R 总体计划与规范；原 S1 阶段计划由 Git 历史保存

本记录不修改 sealed v0.1 evidence；它决定后续 certificate 可以诚实发布的 theorem dependency。

1. 本轮裁决

现有验证文档把 smooth→PL 路线描述为与 Boissonnat–Wintraecken 一致，这是正确的研究方向，但当前证书不能直接宣称满足该文版本记录 Theorem 25 的全部原始前提。至少存在四个需要显式关闭的错位：

论文假设 f : R^d → R^(d-n) 为 smooth（C² 足够）；当前 field.sphere@1.0.0 的数学语义是 ‖x-c‖-r，在球心不可微；
论文的 f_PL 是数学函数 f 在 triangulation vertices 上的精确值所作的 PL interpolation；当前 constructor 使用 JavaScript number 求值并把这些 binary64 值当作 PL vertex values；
Theorem 25 的直接条件是论文等式 (22) 与 (27)，依赖 γ_max, λ_min, α_max, D, T；当前 checker 不重建 Hessian bound α_max，也不计算这两条不等式；
论文陈述在 R^d 的 ambient triangulation 上；Aira 序列化的是有限 box 内的 tetrahedral complex。已有 boundary separation 很接近所需 localization，但从有限 complex 到论文 theorem domain 的扩展尚未成为正式 premise/glue lemma。

因此，sealed v0.1 中的 actualIsotopy=pass 不能作为新的 publishedTheoremBacked assurance 直接复用。本轮已完成两条候选路线的可行性裁决：

BW-strict route（不选）：实现 Theorem 25 的原始常数、精确采样/采样误差语义和 localization 前提；
certificate-driven route（选定）：使用现有 separator certificate 直接证明 rounded-PL homotopy 的 generalized Jacobian maximal-rank 与 time transversality，再明确引用 generalized implicit-function、compact flow/isotopy 和 isotopy-extension theorem；所有新增 glue lemma 单独列出，不能把它们冒充 Theorem 25 本身。

选择依据不是“论文错了”，而是它的通用充分界对 Aira 当前 uniform grid 过于保守，且不直接覆盖 Aira 实际认证的 rounded binary64 PL 对象。我们将复用论文中的一般定理层，而不重做通用拓扑学。

normal-surface 方向仍然成立，但只有在 actual binary64 vertices 被精确证明位于相同 open edges、且每个输出 triangle/quad union 是 properly embedded normal disk 后，才能调用 normal-coordinate uniqueness。

2. 锁定的一手来源

2.1 Smooth → PL

主来源锁定为期刊版本记录：

Jean-Daniel Boissonnat、Mathijs Wintraecken，The Topological Correctness of PL Approximations of Isomanifolds，Foundations of Computational Mathematics 22 (2022), 967–1012； DOI 10.1007/s10208-021-09520-0。

使用该版本的编号：

§2 开头：f : R^d → R^(d-n) smooth，C² suffices；0 是 regular value；f⁻¹(0) compact；
Definition 2 / equations (2)–(6)：γ_max, λ_min, α_max, D, T；
equation (22)：local time-transversality condition；
Lemma 22、Lemma 23 / equation (26)：global star variation bound g_PL 与 eigenvalue error e_PL；
equation (27)：generalized-Jacobian regularity condition；
Theorem 25：在 (22)、(27) 下，f_PL⁻¹(0) 与 f⁻¹(0) isotopic；论文摘要、§2.1 和证明文字明确把结论描述为 ambient isotopy；
Lemma 3：compact manifold 上 non-vanishing piecewise-smooth gradient flow 给出 level-set isotopy；
Theorem 48 是真正的 isomanifold-with-boundary 版本，但 Aira 当前目标是闭曲面位于 finite box interior，不应把 box boundary 误当成 zero-set boundary 后机械套用 Theorem 48。

SoCG 2020 版本可作为开放存档，但 theorem contract 和编号以期刊版本记录为准： LIPIcs.SoCG.2020.20。

2.2 Exact PL → actual mesh

normal-surface 来源锁定为：

Ian Agol，Criteria for virtual fibering，Journal of Topology 1(2), 2008, 269–284； DOI 10.1112/jtopol/jtn003，§4，p.275。

该节给出本阶段实际使用的标准事实：

normal isotopy 是保持 triangulation 各 simplex 集合不变的 ambient isotopy；
tetrahedron 中有四种 triangle disk type 和三种 quadrilateral disk type；
normal coordinates 记录每个 tetrahedron 中七种 disk type 的数量；
normal surface 由 normal coordinates 唯一决定 up to normal isotopy；
可实现向量还必须满足每个 tetrahedron 最多一个 quadrilateral type，以及共享 face 上每种 normal arc type 的 matching equations。

Agol 的论文把这些作为标准 normal-surface 基础事实使用，而不是它的主要创新定理。S1 引用该页时仍会在 R3 前追加一个更直接面向 compact triangulated 3-manifold/3-ball 的标准来源交叉核验；这不改变需要 checker 重建的有限前提。

2.3 Ambient-isotopy category correction

初轮审计曾把 Palais 列为候选 ambient extension 来源：

Richard S. Palais，Local Triviality of the Restriction Map for Embeddings，Commentarii Mathematici Helvetici 34 (1960), 305–312；DOI 10.1007/BF02565942。

Palais 证明 compact differentiable submanifold embeddings 的 restriction map 局部平凡。终点 g^{-1}(0) 是 PL surface，所以把该 smooth theorem 直接用于 Aira 会产生 category mismatch。期刊 PDF 复核确认 Boissonnat–Wintraecken §2 的 Lemma 3 与 Theorem 25 前证明段已把 piecewise-smooth gradient-flow construction 明确描述为 ambient isotopy；Agol 的 normal isotopy 定义也是保持 simplices 的 ambient isotopy。因此 Palais 仅保留为背景文献，不进入最终 certificate dependency hash。

3. Theorem 25 在 Aira `d=3, n=2` 的直接条件

对 scalar field，d-n=1，Gram matrix 只有一项，因此：

γ = sup_T0 ‖∇f‖
λ = inf_T0 ‖∇f‖²
α = sup_T0 ‖Hess(f)‖₂
D = maximum tetrahedron edge length in T0
T = minimum tetrahedron thickness in T0

g_PL = 6 D α + 24 D α / T + 4 D² α
e_PL = g_PL · (γ + 12 D α / T + 2 D² α)

transversality (22):  λ > (12 D α / T)²
regularity      (27):  λ > e_PL

论文推导还在相关估计中使用 dD < T。这些量有物理量纲/坐标尺度依赖，因此 certificate 必须固定数学坐标语义，不能只复制 asymptotic D=O(...) 文字。

对 isotropic cube step h 的标准 Freudenthal tetrahedron，可解析得到 longest edge D=√3 h、smallest altitude h/√2、thickness T=1/√6。但 Aira 的 uniform depth 只固定各轴 cell 数，不自动保证 domain 三轴 extent 相同；一般 box 必须逐 tetrahedron 重建 D,T，或把 S1 接受域明确收窄到 isotropic grid。

4. Smooth→PL premise matrix

状态词：covered 表示现有 checker 已有足够直接证据；partial 表示有相近证据但 contract 尚不等价； missing 表示没有证据；contradicted 表示当前实现与直接 theorem premise 不一致。

ID	Published premise	Current Aira evidence	状态	S1 关闭动作
BW-01	`f : R³→R` smooth，`C²` suffices	allowlist 排除 hard CSG；sphere evaluator 使用 `sqrt(sum(delta²))-r`	contradicted	证明 theorem 可 localize 到 `T0` 的 `C²` neighbourhood，或提供不改相关 samples/zero set 的全局 `C²` extension
BW-02	0 regular；`f⁻¹(0)` compact	candidate-band separator 给 gradient 正 margin；surface bounds/domain interior	partial	从 interval cover 明确推出全部 zeros 位于 cover、gradient nonzero、zero set closed+bounded
BW-03	ambient triangulation of `R³`	finite box 内 conforming Freudenthal complex	missing	构造 conceptual global lattice/collar extension并证明全部 relevant simplices 位于 serialized interior
BW-04	`f_PL(v)=f(v)` 的精确 vertex samples	`analyzeCertifiedPlComplex` line 104 使用 `program.evaluate(point): number`	contradicted	精确采样、带误差的 theorem，或改走直接验证 rounded-PL homotopy 的 certificate-driven route
BW-05	`f_PL` 在共享 simplices 上连续	canonical grid vertex ids；每 tet 读取同一 `grid.values`	covered	把 grid-to-complex incidence 和 shared-face restriction 写入 premise report
BW-06	finite positive `γ,λ,α,D,T` on `T0`	gradient interval + separator margins；fixed grid geometry	partial	增加 Hessian enclosure/`α`，从 separator 导出 `λ`，精确重建 `D,T`
BW-07	theorem estimates使用 `dD<T`	未序列化/检查	missing	checker 明确验证；失败则 refine/reject
BW-08	equation (22)	smooth/PL separator margins是另一种 transversality certificate	missing for direct theorem	BW-strict 计算原式；certificate-driven route 则把 separator→spatial generalized gradient nonzero 作为单独 lemma
BW-09	equation (27)	Lean 只证明 simplex 内 exact-real separator algebra；TS 检查 star margins	missing for direct theorem	BW-strict 计算 `e_PL`；certificate-driven route 直接证明 star generalized Jacobian every convex combination maximal-rank
BW-10	total zero set compact/proper over time	candidate band interior + finite grid	partial	明确证明所有 `F_t=0` 被 confinement 在 compact interior band，且 band/collar identity hash-bound
BW-11	flow/isotopy regularity	validation 文档 prose；未形成 theorem dependency ledger	missing	锁定 B&W Lemma 3/Clarke/Palais 的 category 与 premises，或直接满足 Theorem 25
BW-12	conclusion uses the same `f_PL` as actual exact PL certificate	exact-root bundle 对 binary64 vertex values 定义 rational PL roots	contradicted under direct theorem	关闭 BW-04 后统一数学对象 identity，禁止同名 `F_PL` 指代 exact samples与rounded samples两种函数

4.1 最重要的对象身份问题

当前至少有三个不能混名的对象：

f                         mathematical Field denotation
PL(exact f(v))            B&W Theorem 25 的 f_PL
PL(binary64 evaluate(v))  Aira exact-root bundle 实际认证的 dyadic PL function

现有 exact-root kernel 对第三个对象是精确的，但这不使第二、第三个对象相等。S1 的 theorem manifest 必须为它们使用不同 object ID；在 sampling bridge 关闭以前，禁止从第一箭头直接跳到第三个对象。

5. Normal-surface premise matrix

ID	Published premise / standard fact	Current Aira evidence	状态	S1 关闭动作
NS-01	compact triangulated 3-manifold（允许 boundary）	finite box 的 conforming tetrahedralization；目标 surface 在 interior	partial	明确 box complex 是 triangulated 3-ball，crossing support 与 boundary 分离
NS-02	surface 与 0/1-skeleton 横截，避开 vertices；每 tet 是 normal disk union	grid values strict nonzero；exact affine roots在 open edges	partial	形式化 exact PL zero slice 的 triangle/quad classification
NS-03	actual mesh vertices 位于同一 open edges	当前仅 coordinate-wise strict interior	contradicted	S1.2 exact affine membership checker；已知 diagonal counterexample 必须拒绝
NS-04	每 tet 中 actual triangle/quad 是 properly embedded normal disk	arity/order/topology checks；quad 被拆成两个 triangles	partial	exact predicate 证明两 triangles 的 union embedded、boundary 是四条 normal arcs
NS-05	quadrilateral compatibility	affine scalar tet 每 crossing tet 最多一种 quad；actual combinatorics复制该类型	partial	checker 重建，不信任 producer disk type
NS-06	shared-face matching equations	canonical edge roots和全局 mesh incidence	partial	对每个 shared face、每种 arc type精确计数两侧相等
NS-07	两 surfaces normal coordinates完全相同	combinatorial intent相同，但 NS-03/04 未关闭	missing	从 exact/actual buffers独立生成并逐项比较 `7 × #tet` coordinates
NS-08	normal isotopy是 ambient isotopy，保持 simplices invariant	Agol §4 p.275 标准事实	source locked	确认 closed interior surface 情形可取 boundary-fixed support

6. 当前推荐的 theorem-contract 结构

在 S1.1 最终裁决前，certificate manifest 应预留而不冻结以下分层：

theoremDependencies:
  smoothToPl:
    route: bw-strict | certificate-driven
    sourceVersion: journal-2022
    mathematicalFieldObjectId
    plObjectId
    premiseLedgerHash
  plToActual:
    route: normal-coordinates
    triangulatedAmbientObjectId
    exactNormalSurfaceObjectId
    actualNormalSurfaceObjectId
    premiseLedgerHash

publishedTheoremBacked 只有在两个 ledger 均无 missing/partial/contradicted 时生成。历史 actualIsotopy=pass 字段不自动迁移到该 assurance vocabulary。

7. BW-strict 可行性探针与路线裁决

可复验脚本： research-lane-r-bw-theorem25-probe.mjs。脚本按论文 equations (22)、(24)、(26)、(27) 特化到 d=3 的 signed-distance sphere，并对 Aira 等距 cube Freudenthal tetrahedron 使用：

D = √3 h
T = 1/√6
γ = 1
λ = 1
α ≤ 1/(1-D)  when a T0 tetrahedron intersects the unit sphere

2026-09-01 实测结果：

Fixture	当前 depth	当前 direct checks	首个通过 depth	对应 full-grid 规模
off-grid sphere, `r=1`	4	三项均失败	10	1,073,741,824 cubes / 6,442,450,944 tets
decimal sphere, `r=.85`	5	三项均失败	10	1,073,741,824 cubes / 6,442,450,944 tets
shifted/scaled sphere, `r=1.2`	4	三项均失败	9	134,217,728 cubes / 805,306,368 tets

“三项”指 dD<T、equation (22) 和 equation (27)。这只证明该组 published sufficient bounds 在当前 uniform implementation 上工程不实用，不证明存在不可能性，也不排除更紧的特化界。但它足以作为 S1 的路线裁决：选择 certificate-driven route，并保留 Theorem 25 probe 作为反对误用该 theorem 名义的 regression evidence。

8. 关闭结果

PP-01–PP-09 machine premise entries 已由 published-premise checker 重建；
AIRA-GLUE-01–06 已在 certificate-driven theorem ledger 给出可审计证明；
S1.2 exact-on-edge 与 S1.3 normal-coordinate certificates 已关闭初始 NS-01–NS-08 的 partial/missing/contradicted 项；初始 matrix 保留为问题发现时的历史快照；
S1.4 manifest 已绑定 Field/domain/grid、algorithm versions、positions/triangles、theorem metadata 与全部 nested certificates；
官方 clean-worktree verifier 已通过，完成证据见 validation report。

9. 本轮证据边界

初轮审计本身没有修改 sealed v0.1 evidence，并正确证明“直接调用 Theorem 25 不成立”。后续 S1 在新 versioned certificates 中关闭全部账本，不重签、不升级旧 actualIsotopy=pass 语义。最终只有新 manifest 可发布 published-theorem-backed-ambient-isotopy，且显式带有 fullLeanAmbientIsotopy=not-proved。