论文与源码

---

这里发布公开仓库无法撤回的 Lean 源码等资料；部分论文处于审稿期，暂不可破盲，请理解。

分级

级	规则
T0	T0 规则保留：任何处于匿名评审中的版本，其标题、场馆与标识符都不在本站出现；若某版本进入匿名评审，本站随即撤下相关可检索信息。
T1	占位：显示标题与状态，不出文件。等待作者本人人工核验。
T2	外链，指向站外已存在的位置。
T3	全文存缴，含可下载文件。须经显式人工核验方可出现。

当前条目

三篇论文 · 单页简介

论文	标题	状态	计数	一句话
A	共享参数边界势 · Shared-Parameter Boundary Potential	大纲 · 在写	A 模块 1 / 33 / 7	V(κ)=c₀κ+αC_F/κ，κ*=√(αC_F/c₀)，σ*=αC_F/C₀；有效域判据纠错 + 反例族；C_H=π²/3 机检链
B	有如何发生 · How There Is: A Machine-Checked Programme for Boundary, Level and Identification	预印本在写 · 形式脊柱完成	B 规范 53 / 417 / 77	边界＝闭包不动点，判据＝核的阈值水平集；接缝 Fix(c_{Lθ})=S_θ（L(θ)=ln((2−θ)/θ)）；no-go：仅水平的规范不变信息不能唯一选水平
C	边界的形式与位置 · Boundary Form and Boundary Position	v3 写作计划 · 在写	无新 Lean	模型先行重构康德 Grenze/Schranke：一个边界结构的两种描述，不是两种边界

源码与存档

源码快照：limisys.github.io/boundary-axiom/（推送后可用）。统一仓 56/467/90。CausModel 去身份公开版仍为 T1 占位，规则不变。

许可

资产	许可	允许什么
文字作品（论文）	CC BY 4.0	可自由阅读、引用、转载，须署名。
源码（Lean 等）	Apache-2.0	可自由使用、修改、分发，须保留声明。
本站文字	CC BY 4.0	可自由阅读、引用、转载，须署名。

AI 使用披露

大语言模型作为起草工具，产出了 Lean 4 形式化证明的候选代码与三个 Python 验证脚本。所有机检结论都以重跑编译器与独立脚本为准——从不以生成者的身份为准。一条结论之所以是机器检验的，是因为检验通过，而不是因为写它的是谁、或是什么。

什么没有挂出，以及为什么

项	理由
任何匿名评审中的版本	公开即破匿名。不公开
边界势纲领开发体（更大的那套 Lean 语料）	尚未去身份，仍含本机绝对路径。去身份之后必须重新编译复验才能挂出。
被评审过的投稿稿	已以 T3 级挂出（原样存档）。