Lane R S1：certificate-driven published theorem ledger

状态：Locked for fixed single-sphere / uniform Freudenthal profile

日期：2026-09-01

该 ledger 证明 Aira 如何满足已发表定理的实例化前提；它不宣称一般拓扑定理已由 Lean 内核重证。

1. 被认证的三个数学对象

本 profile 严格区分：

f       = field.sphere@1.0.0 的数学函数 ||x-c||-r
g       = 以实际 binary64 evaluate(v) 作为精确 dyadic 顶点值的连续 PL 函数
Sactual = certificate 中 hash-bound binary64 positions / integer triangles 所表示的曲面

平滑到 PL 的 homotopy 是 H(x,t)=(1-t)f(x)+t g(x)。它不是 PL(exact mathematical f(v))，因此本 profile 不直接调用 Boissonnat–Wintraecken Theorem 25 的数值充分条件， 也不把 rounded samples 偷换成 exact mathematical samples。

2. 实际依赖的已发表结果

TD-01：广义隐函数定理

• 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；
• journal version §2.3.1，Theorem 20，p.983；该 theorem 引用 Clarke 1990 p.256；
• 本 profile 使用的结论：若 Lipschitz map 的相关 generalized Jacobian 中每个矩阵都 maximal rank，则零集局部是 Lipschitz graph。

TD-02：非消失分段光滑梯度流产生 ambient isotopy

• 同一论文 §2，Lemma 3，pp.974–975；
• §2 的结果说明和 Theorem 25 前的证明段明确把该 gradient-flow construction 称为 ambient isotopy；
• 本 profile 只复用这项一般机制，不声称满足 Theorem 25 的 equations (22)/(27)。

TD-03：normal coordinates 唯一决定 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 simplices invariant 的 ambient isotopy；每个 tetrahedron 有四种 triangle type 与三种 quadrilateral type，normal surface 由 7t normal coordinates 唯一决定 up to normal isotopy。

不列为实际 dependency：Palais 1960

Palais 的 embedding restriction / isotopy extension 结果属于 differentiable embeddings。Aira 的中间终点是 PL surface，直接把 Palais 当作 PL endpoint 的延拓定理会产生 category mismatch。Boissonnat–Wintraecken 已在其 piecewise-smooth construction 中给出所需 ambient conclusion，Agol 的 normal isotopy 本身也是 ambient；因此最终 certificate 不依赖 Palais。Palais 只作为历史背景保留，不进入 theorem dependency hash。

3. Machine-checked premise IDs

这些条目由 smooth-implicit-certified-pl-published-premise-certificate.ts 独立重建，不信任 producer 的 pass 字段。

ID	事实	Evidence
PP-01	Field 恰为单个 field.sphere@1.0.0，level 为 0	Field validation + exact operator allowlist
PP-02	prerequisite 与 Field/domain/budget canonical recomputation 完全一致且 eligible	semantic hash equality
PP-03	ambient complex 是固定 main-diagonal 0--6、每 cube 六 tetrahedra 的 conforming uniform Freudenthal complex	fixed construction version
PP-04	所有 grid values finite/nonzero，candidate band 非空	checker rebuild
PP-05	candidate tetrahedra 是有限集合且不接触 finite domain boundary	incidence/boundary rebuild
PP-06	candidate 定义覆盖 H=0：其外 smooth interval 与 PL vertex hull 具有相同 strict sign	interval + vertex-value rebuild
PP-07	每个 relevant closed vertex star 都有 smooth gradient interval；sphere center singularity不在这些 stars	interval gradient availability
PP-08	每个 relevant vertex 具有一个 hash-bound separator；其 smooth full-star margin 严格为正	outward interval dot product
PP-09	同一 separator 对所有 incident PL tetrahedral gradients 的 full-star margin 严格为正	exact incidence + interval dot product

S1.2/S1.3 nested certificates 另外重建：

• binary64-as-exact-rational common affine parameter 与 strict-open-edge membership；
• exact root grid-edge identity；
• actual triangle 到 crossing tetrahedron 的唯一归属；
• 四 triangle / 三 quad normal disk type；
• quad 两三角 union 与合法内部对角线；
• shared-face normal arc matching equations；
• finite domain boundary normal arc count 为 0；
• exact/actual sparse 7 × #tet normal-coordinate hashes 相等。

4. Aira-specific glue lemmas

这些是短的实例化证明，不是外部论文中的新通用 theorem，也不标记为 Lean-kernel proof。它们的 statement 被逐字放入 最终 certificate identity，因此任何改写都会改变 certificate ID。

AIRA-GLUE-01：candidate confinement

对 candidate 外任一 tetrahedron，checker 已证明存在一个 strict sign，使 f 的整个 interval enclosure 与 g 的全部 vertex values 同号。g(x) 是 vertex values 的凸组合，故 f(x)、g(x) 和 (1-t)f(x)+t g(x) 对所有 t∈[0,1] 均保持该 strict sign。于是 H=0 全部位于 candidate subcomplex。

AIRA-GLUE-02：continuous separator field

给每个 relevant grid vertex 的 separator 记为 s_v。在每个 tetrahedron 内定义 V(x)=Σ_v λ_v(x)s_v。conforming complex 的共享 face 使用相同 vertex IDs 与相同 barycentric restrictions，故两侧 定义一致，V 是 candidate complex 上的 continuous PL field。

AIRA-GLUE-03：generalized spatial rank

若 x 位于 tetrahedron σ，则每个 λ_v(x)>0 的 vertex v 都含有 x 于其 closed star。PP-08 给出 s_v·∇f(x)>0，所以 V(x)·∇f(x)=Σ λ_v s_v·∇f(x)>0。在 simplex boundary，g 的 Clarke generalized gradient 是相邻 tetrahedral gradients 的凸包；PP-09 对每个 incident gradient 都给 strict positive dot product， 所以对凸包中每个 ξ 也有 V(x)·ξ>0。因此对 H 的每个 spatial generalized derivative， V·((1-t)∇f+tξ)>0，scalar generalized Jacobian rank 为 1。

AIRA-GLUE-04：time transversality

由 TD-01，H^{-1}(0) 局部为 Lipschitz/piecewise-smooth manifold。由于 spatial block 已 rank 1，可在 generalized IFT 中把任一具有正 separator component 的 spatial coordinate 取为 dependent variable，并把 t 保留为 local independent coordinate。因此 t|H^{-1}(0) 没有 critical point，满足 TD-02 的非消失梯度前提。

AIRA-GLUE-05：compact interior support

candidate subcomplex 是有限 closed tetrahedra 的 union，故 compact；PP-05 使其与 domain boundary 分离。 H^{-1}(0) 是 candidate×[0,1] 的 closed subset，因而 compact。TD-02 的 flow 可取 support 于该 interior neighbourhood，并在其外延拓为 identity。

AIRA-GLUE-06：composition

TD-01/TD-02 给出 f^{-1}(0) → g^{-1}(0) 的 ambient isotopy。S1.2/S1.3 证明 g^{-1}(0) 与 Sactual 是同一 triangulated 3-ball 中、具有相同 normal coordinates 的 properly embedded normal surfaces；TD-03 给出 simplex-preserving normal isotopy。两个 ambient isotopies 的 composition 仍是 ambient isotopy。

5. 可信边界与最终允许声明

最终允许的唯一拓扑 assurance：

published-theorem-backed-ambient-isotopy

含义：Aira checker 重建并 hash-bind 这个固定接受子集的有限前提；一般 generalized IFT、piecewise-smooth gradient-flow ambient isotopy 与 normal-surface uniqueness 依赖上述发表成果。

明确禁止的声明：

full-Lean ambient isotopy
Lean kernel proved the general topology theorem
directly satisfies Boissonnat--Wintraecken Theorem 25

当前 Lean kernel 对 exact affine root 的局部代数结果仍有价值，但 JSON/parser/runtime 与一般拓扑 theorem 不在其 trusted kernel closure 内。