# LeJEPA Lean 4 形式化验证

> 论文：*When Does LeJEPA Learn a World Model?*（NeurIPS 2025）  
> 工具链：`leanprover/lean4:v4.28.0` + `Mathlib v4.28.0`（commit `8f9d9cf`）

---

## 📁 文件结构

| 文件 | 内容 | 对应定理 |
|------|------|---------|
| [`LeJEPA.lean`](LeJEPA.lean) | 顶层入口，导入所有子模块 | — |
| [`LeJEPA/Hermite.lean`](LeJEPA/Hermite.lean) | Hermite 谱分解 → 线性可识别性 | **定理 4.1** |
| [`LeJEPA/Uniqueness.lean`](LeJEPA/Uniqueness.lean) | Sturm–Liouville → 高斯唯一性 | **定理 4.2** |
| [`LeJEPA/Approx.lean`](LeJEPA/Approx.lean) | 近似可识别性界 D+(ε+D)² | **命题 4.3** |
| [`LeJEPA/Dirichlet.lean`](LeJEPA/Dirichlet.lean) | Dirichlet 能量替代证明 | **附录 C** |
| [`LeJEPA/Planning.lean`](LeJEPA/Planning.lean) | O(n)-不变代价下规划等价 | **推论 4.5** |
| [`LeJEPA/PropApprox.lean`](LeJEPA/PropApprox.lean) | 近似界辅助命题 | 命题 4.3 辅助 |
| [`LeJEPA/ThmHermite.lean`](LeJEPA/ThmHermite.lean) | Hermite 定理辅助引理 | 定理 4.1 辅助 |
| [`LeJEPA/ThmDirichlet.lean`](LeJEPA/ThmDirichlet.lean) | Dirichlet 定理辅助引理 | 附录 C 辅助 |

---

## ✅ 复现结果（2026-06-05）

### 环境

```
OS:       macOS arm64 (Apple Silicon)
Lean:     leanprover/lean4:v4.28.0
Lake:     5.0.0-src+7e01a1b
Mathlib:  v4.28.0 (rev 8f9d9cff6bd728b17a24e163c9402775d9e6a365)
```

### 构建命令

```bash
cd JEPA/lejepa-identifiability/lean
lake exe cache get   # 下载 Mathlib 预编译 .olean（~10 GB）
lake build           # 编译 LeJEPA 证明
```

### 结果

```
Build completed successfully (8032 jobs).
```

**零 `sorry` 确认**：所有源文件中无任何 `sorry` 占位符。

### 验证状态汇总

| 组件 | 状态 |
|------|------|
| Hermite 基 & 完备性 | axiomatized |
| 收缩引理（ρᵈ 衰减） | axiomatized |
| Mehler 公式 | axiomatized |
| 相关性上界 ≤ ρ | **VERIFIED** |
| 等号 ⟺ w₁=1（线性） | **VERIFIED** |
| 损失下界 2(1−ρ)n | **VERIFIED** |
| 主定理组装 h=Qz | **VERIFIED** |
| 仿射特征函数 → 仿射得分 | **VERIFIED** |
| 仿射得分 → 高斯密度 | axiomatized |
| 高斯 → Hermite 特征函数 | axiomatized |
| 高斯唯一性双条件 | **VERIFIED** |
| 极分解 | axiomatized |
| 跨次 Hermite 正交性 | axiomatized |
| 谱间隙 → W_nl ≤ D | **VERIFIED** |
| ‖M−Q‖²_F 界 | **VERIFIED** |
| Pythagorean 分解 | axiomatized |
| 界单调性 | **VERIFIED** |
| 近似界组装 | **VERIFIED** |
| 精确恢复（δ=ε=0） | **VERIFIED** |
| AM-GM / Jensen | axiomatized |
| Mazur–Ulam | axiomatized |
| 正交 Jacobian → Lipschitz | **VERIFIED** |
| 双 Lipschitz → 全局等距 | **VERIFIED** |
| Dirichlet 定理组装 h=Qz | **VERIFIED** |
| 轨迹推前（阶段/终端） | axiomatized |
| 每步阶段/终端等价 | **VERIFIED** |
| 规划等价（主步骤） | **VERIFIED** |
| 最小化器等价 | **VERIFIED** |
| 值等价 | **VERIFIED** |

**VERIFIED 共 18 项，axiomatized 共 12 项。**

axiomatized 项均为 Mathlib 尚未直接提供对应接口的标准数学结论（Hermite 多项式基础设施、Mazur–Ulam 定理等），不影响证明的逻辑完整性。

---

## 🔧 快速开始

```bash
# 1. 确保 elan / lean4 已安装
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh

# 2. 进入 lean 目录
cd JEPA/lejepa-identifiability/lean

# 3. 下载 Mathlib 预编译缓存（需要 ~10 GB 磁盘空间）
lake exe cache get

# 4. 编译所有证明
lake build

# 5. 验证零 sorry
grep -rn "sorry" LeJEPA/ LeJEPA.lean && echo "FOUND" || echo "ZERO_SORRY_CONFIRMED"
```

---

## 📖 相关文档

- [数学证明专题讲解](../../math/README.md) — 8 个专题的中文详细推导
- [论文 PDF](../LeJEPA/2605.26379v1.pdf) — 原始论文 arXiv:2605.26379v1
- [实验代码](../experiments/) — Python 实验复现