关于粘性立方体的斯托克斯定理：Lean 4 中的真实拉回、与 mathlib4 的桥接以及链级 d^2=0
几何拓扑
2026-05-05 v1 量子代数
摘要
我们在 Lean 4/mathlib4 中实现了无惊叹号（sorry-free）的斯托克斯定理形式化，适用于任意维度的光滑粘性立方体，采用真实微分形式拉回机制（基于Frechet 导数）。该开发还包括与 mathlib4 抽象 extDeriv 的桥接、以 Z-线性形式延伸的链级斯托克斯定理、粘性立方链的 d^2=0 性质、轴对齐立方体的盒子斯托克斯、维度特化，以及与 Harrison 的 HOL Light 形式化的结构化比较。
引用
@article{arxiv.2605.01026,
title = {A HOMFLYPT-type invariant for pseudo links via a resolution in Hecke algebras},
author = {Ioannis Diamantis},
journal= {arXiv preprint arXiv:2605.01026},
year = {2026}
}
备注
21 pages, 6 figures