论文专著
每篇论文拆解为概览、方法、实验结果、代码和数据集五个子页， 与文档中心的理论框架相互对照——框架文档讲"是什么"，论文文档讲"怎么做到的"。
系列框架：端到端安全保证链
为什么 EICPS 拒绝统计近似？三篇论文如何串联为一条安全保证链？FAILSAFE 的三种形态、规范闭合性与现有 LLM 规划方法的根本区别。
Paper-01 · SEC 语义覆盖完备性
规程封闭性下 LLM 任务语义覆盖的精确形式化保证——SEC(Q,τ*)=1 确定性等式与 Theorem Q-18——IEEE RA-L
Brain-LLM 领域微调：Proposal 质量的形式化保证
QLoRA 微调 3B 模型使 Q(f) 0.480→0.944、危险对幻觉率降 16.5×——IEEE RA-L 投稿
纵深防御执行层
跨域正交化原理、三层防御架构（L1/L2/L3）、STL-101/102 执行监控——IEEE T-ASE 投稿
src/content/papers/<paper-id>/
创建子文件夹，添加 5 个 MDX 文件，论文自动出现在此页。
具身空间是比三篇论文更上位的原创概念——三篇论文是用具身空间语言得出的工程结论。 流形几何是理论主干（三流形 · SE(3) · Flow-Jump · SEC）， 形式化自主是工程目标（自主执行 + 形式等式保证，而非统计近似）。 网站五大模块的内容已可直接蒸馏为各章初稿。
规划中论文
构思中现有三篇覆盖的是单机器人 · 闭合规范域 · 三层独立形式保证。 以下沿四个维度自然延伸——补齐流形理论空白、建立系统级组合定理、突破闭合域假设、扩展到多机协同。
三篇论文均在仿真环境验证，但 𝓜lat（隐变量流形）与真实物理空间之间的迁移误差从未被形式化。 在 Gromov-Hausdorff 距离框架下证明 𝓜lat,sim → 𝓜lat,real 的映射误差有界， 并推导该误差对 FPR 的形式传播上界，直接堵住 Paper-01/02/03 的已知局限。
Paper-01/02/03 分别独立给出 SEC=1 / Q(f)≥0.944 / FPR=0%，但无一篇形式上证明三者组合后的系统级安全界。 在 Flow-Jump 混合系统框架下，用组合 Lyapunov 方法证明三层独立保证的可组合性， 给出组合成立的充分条件（层间解耦假设的精确刻画），将现有非正式估算 P(unsafe)≤H·(1−RL2)·(1−RL3) 升级为形式定理。
Paper-03 的 L1/L2/L3 是离散检测与拦截；本文在 SE(3) 流形上建立 CBF 连续时间前向不变性保证—— 机器人轨迹从一开始就不进入危险区，而非事后检测。 "Paper-03 解决发现异常后怎么拦，P-06 解决轨迹从不进入危险区。"
当前所有形式保证依赖"规范闭合性"。本文定义部分形式化自主（Partial Formal Autonomy）： 已知区域维持形式等式保证，未知区域自动降级为统计下界并标记"形式保证失效区"，触发人机协同接管协议。 从认识论上回答"形式化自主的边界在哪里"。
证明持续接触作业方案因导线 PDE 耦合（状态 ∈ [L²]⁴）导致 CBF/STL 形式化验证结构性失败（三重障碍互相独立）， 由此推导形式化可处理性三条件（有限维 · 解析动力学 · 实时 QP），并逆向反推出分离式末端执行器设计—— 硬件方案由数学约束决定而非工程经验。以 Prj167 销钉插拔实物作业为验证载体。 引言框架：与 Paper-01 规范闭合性构成方法论对偶——识别前提（P01）/ 诊断坍塌（本文）/ 改造问题（本文），"让形式化可能"即研究对象（→ Q-31）。
将三层形式保证扩展到分布式多机场景（如双机协同带电换线）： 分布式 SEC（集合覆盖条件）、多机 STL 组合规约、去中心化纵深防御。 每台机器人独立维护 Brain-Spine-Body，机器之间建立形式化协同协议。