worldmodel/JEPA/lejepa_world_model_notes.md

# 论文阅读笔记：*When Does LeJEPA Learn a World Model?*

**作者：** David Klindt (CSHL)、Yann LeCun (NYU)、Randall Balestriero (Brown)
**发表：** arXiv:2605.26379v1 [stat.ML]，2026年5月25日
**官网：** https://klindtlab.github.io/lejepa-identifiability/（2026-05-27）
**代码：** [`JEPA/lejepa-identifiability/`](JEPA/lejepa-identifiability/)（已本地 clone）
**原文：** `research/papers/2605.26379v1.pdf`
**视频：** https://youtu.be/EioGDo67ZDs（官方演示，AI and the Brain 频道）

---

## 🎯 核心问题

> **LeJEPA 学到的表示，什么时候才算真正学到了世界模型（World Model）？**

答案：当且仅当它能**线性恢复**世界的潜在变量（latent variables）时。

---

## 🧠 背景与动机

### 什么是 JEPA？
Joint-Embedding Predictive Architecture（JEPA）是 LeCun 提出的自监督学习框架：
- 训练编码器 `f` 对同一内容的两个视图产生相似的嵌入
- 用正则化器防止表示坍塌（collapse）

### 什么是 LeJEPA？
`LeJEPA` = JEPA + **SIGReg**（Sketched Isotropic Gaussian Regularization）：
- **对齐损失（Alignment）：** 拉近正样本对的嵌入
- **高斯正则化（SIGReg）：** 强制嵌入分布接近各向同性高斯分布 `h(z) ~ N(0, I_n)`

### 核心缺口
此前没有任何 JEPA 的**可识别性（identifiability）理论**——不知道学到的表示是否真正恢复了世界的潜在结构。

---

## 🌍 世界模型的数学框架

### 世界假设（三条）

| 假设 | 含义 |
|------|------|
| **独立性** | 潜变量各分量相互独立 |
| **平稳性** | 两个视图共享同一边际分布 |
| **加性噪声** | `z'_i = m_i(z_i) + η_i`，噪声独立于状态 |

### 高斯世界（Gaussian World）
最大熵选择：`z ~ N(0, I_n)`，转移过程为 **Ornstein-Uhlenbeck（OU）过程**：

```
z' = ρz + √(1-ρ²) η,   η ~ N(0, I_n)
```

其中 `ρ ∈ (0,1)` 控制两个视图的相关性。

### 学习目标

```
min_h  E[‖h(z') - h(z)‖²]    (对齐损失)
s.t.   h(z) ~ N(0, I_n)       (高斯约束)
```

---

## 📐 四大定理

### 定理 1：LeJEPA 线性可识别性（正向）

> 在高斯世界中，满足 LeJEPA 目标的最优表示 `h` **当且仅当** `h(z) = Qz`，其中 `Q ∈ O(n)` 为正交矩阵。

**证明核心思路（Hermite 多项式谱分解）：**

1. 任意函数 `h_i(z)` 可展开为 Hermite 多项式：`h_i = Σ c_α H_α(z)`
2. OU 转移对 d 阶 Hermite 分量的衰减因子为 `ρ^d`
3. 由 Mehler 公式：`E[h_i(z')h_i(z)] = Σ_d w_d · ρ^d ≤ ρ`
4. 等号成立 **当且仅当** `w_1 = 1`（即 `h_i` 是线性的）
5. 任何非线性扭曲都会**严格降低**正样本对的相关性

**直觉：** 高斯 OU 过程对高阶非线性成分的衰减更快，因此线性映射是唯一最优解。

---

### 定理 2：高斯分布的唯一性（逆向）

> 在满足世界假设的所有分布中，**高斯分布是唯一**使 LeJEPA 实现线性可识别性的分布。

**证明思路（Sturm-Liouville 理论）：**

- 若第一特征函数 `φ_1` 是仿射的（`φ = az + b`），则得分函数 `(log p)'` 必须是线性的
- 线性得分函数 → `log p(z) ∝ -(z-μ)²` → 高斯分布

**意义：** 这与经典 ICA 的结论**完全相反**——在线性 ICA 中，高斯分布是唯一**失败**的情况；在 LeJEPA 的非线性设置中，高斯分布是唯一**成功**的情况。

---

### 定理 3：近似可识别性

> 当对齐目标和白化约束只近似满足时，恢复误差**优雅降级**：

```
E[‖h(z) - Qz‖²] ≤ D + (ε + D)²
```

其中：
- `D = δ / (2ρ(1-ρ))`：对齐间隙的归一化量
- `ε = ‖Cov(h(z)) - I‖_F`：白化误差

**实践含义：** 对齐质量是可识别性的主要瓶颈，白化误差影响较小。

---

### 定理 4：最优潜空间规划

> 若 `h(z) = Qz`（正交），则在**旋转不变代价函数**下，潜空间中的规划与真实世界中的规划**完全等价**：

```
V̂*(h(z₀)) = V*(z₀)   且   â*_{1:T}(h(z₀)) = a*_{1:T}(z₀)
```

**覆盖的控制问题：**
- 目标到达（goal-reaching）
- 线性二次调节（LQR）
- 任何依赖旋转不变量的代价函数

---

## 🔬 实验验证

### 实验 1：正向可识别性（验证定理 1）
- 2D 设置，4种非线性混合函数（见 [`mixing.py`](JEPA/lejepa-identifiability/experiments/lejepa_id/mixing.py)）：
  - `spiral`（螺旋，保测度旋转微分同胚 `g(z) = R(π‖z‖)z`）
  - `banana`（香蕉/抛物线弯曲，`x₁ = z₁ + z₀²`）
  - `sinusoid`（正弦剪切，`x₀ = z₀ + sin(1.5 z₁)`）
  - `nvp`（RealNVP 风格耦合层，`make_coupling_mixing`，任意偶数维）
- LeJEPA 在所有情况下恢复各向同性高斯结构（旋转等价）
- 扩展到 **1024 维**：SIGReg 和 VICReg 保持 `R² > 0.999`

### 实验 2：逆向验证（验证定理 2）
- 扫描广义正态分布族（形状参数 α）
- `R²` 在 **α=2（高斯）** 时达到峰值，非高斯分布线性可识别性下降

### 实验 3：近似界验证（验证定理 3）
- 所有运行的实际恢复误差均低于理论界
- 对齐损失是可识别性的最强预测指标

### 实验 4：潜空间规划（验证定理 4）
- DMC Reacher 环境（像素输入，2D 关节角度潜变量）
- 高斯编码器（OU 采样）：规划质量与 oracle 无统计显著差异
- 轨迹编码器（RL 策略采样，非高斯）：规划质量显著下降

---

## 🔑 关键洞见

### 1. 谱分解是核心工具
Hermite 多项式将任意函数分解为线性/非线性成分，OU 转移对高阶成分的衰减更强，这使得线性映射成为唯一最优解。

### 2. 数据分布决定可识别性
- **OU 采样（各向同性高斯）** → 满足理论假设 → 高可识别性
- **RL 策略轨迹（非高斯、各向异性）** → 违反假设 → 低可识别性

### 3. 探索策略的重要性
对于自监督预训练，**近似各向同性随机游走**的探索策略能保持数据在理论覆盖的范围内。

### 4. 三种方法的失效模式不同

| 方法 | 优势 | 失效场景 |
|------|------|----------|
| SIGReg | 对非高斯潜变量更鲁棒 | 高维时正交误差略增 |
| VICReg | 与 SIGReg 性能相当 | 非高斯潜变量时下降更快 |
| InfoNCE | 低维时表现好 | 高维时核宽度不匹配导致梯度消失 |

---

## 🔧 形式化验证（Lean 4）

所有定理均在 **Lean 4** 定理证明器中形式化验证（零 `sorry` 义务），使用 Mathlib v4.28.0。

**验证组件概览：**

| 文件 | 内容 | 状态 |
|------|------|------|
| `Hermite.lean` | 定理 1（Hermite 多项式路径） | ✅ 已验证 |
| `Uniqueness.lean` | 定理 2（高斯唯一性） | ✅ 已验证 |
| `Dirichlet.lean` | 附录 E（Dirichlet 能量路径） | ✅ 已验证 |
| `Approx.lean` | 定理 3（近似界） | ✅ 已验证 |
| `Planning.lean` | 定理 4（规划等价） | ✅ 已验证 |

---

## 📊 与慢特征分析（SFA）的关系

| 维度 | Sprekeler et al. (2014) | 本文 |
|------|------------------------|------|
| 可识别性类 | 置换等价 | 正交等价 |
| 潜变量分布 | 任意独立 | 高斯（或 i.i.d.） |
| 转移结构 | 需要不同速率 | 需要各向同性 |
| 提取方式 | 顺序（贪心） | 同时 |
| 函数空间 | 固定多项式核 | 学习（神经网络） |
| 近似界 | 无 | `D + (ε+D)²` |
| 实用算法 | xSFA（脆弱，≤6个潜变量） | LeJEPA/SIGReg（可扩展） |

---

## 💡 局限性与未来方向

1. **潜变量是否真的是高斯的？** 宏观任务相关变量可能因中心极限定理趋向高斯，但无法从观测中验证。
2. **维度不匹配问题（m ≠ n）：** 编码器输出维度与真实潜变量维度不同时的行为尚未理论化。
3. **有限样本与优化动态：** 定理 3 是总体层面的结论，样本复杂度和训练动态未涉及。
4. **动作条件转移的可识别性：** 本文只处理编码器侧，动作条件转移 `p̂(ẑ'|ẑ,a)` 的可识别性是下一步工作（与因果表示学习相关）。

---

## 🏆 核心贡献总结

> **LeJEPA 将经典 ICA 的叙事完全颠倒：** 在线性 ICA 中，高斯分布是源分离失败的唯一情况；在 LeJEPA 的非线性设置中，高斯分布恰恰是使线性可识别性成立的唯一分布。

**五大贡献：**
1. **首个 JEPA 可识别性结果**（定理 1）
2. **高斯分布唯一性的逆向定理**（定理 2）
3. **量化近似可识别性界**（定理 3）
4. **各向同性转移是同时提取的必要条件**（附录 F）
5. **线性可识别性与最优潜空间规划的等价性**（定理 4）

线性可识别性使学到的表示成为控制系统的可用状态，任何正交不变代价函数都可以直接在学到的潜空间中使用，无需修改——这是**可证明地学到世界模型**的含义。

---

## 📚 关键参考文献

- **LeJEPA：** Balestriero & LeCun, arXiv:2511.08544, 2025
- **LeWorldModel：** Maes et al., arXiv:2603.19312, 2026
- **V-JEPA 2：** Assran et al., arXiv:2506.09985, 2025
- **VICReg：** Bardes et al., arXiv:2105.04906, 2021
- **SFA 可识别性：** Sprekeler et al., JMLR 15:921-947, 2014
- **Causal-JEPA：** Nam et al., arXiv:2602.11389, 2026

---

## 🗂️ 代码仓库深度解析

> 本节基于本地 clone 的 [`JEPA/lejepa-identifiability/`](JEPA/lejepa-identifiability/) 仓库，对核心实现进行逐模块分析。

### 仓库结构

```
lejepa-identifiability/
├── lean/                    # Lean 4 形式化证明
│   └── LeJEPA/
│       ├── Hermite.lean     # 定理1（Hermite 多项式路径）
│       ├── Uniqueness.lean  # 定理2（高斯唯一性，Sturm-Liouville）
│       ├── Approx.lean      # 定理3（近似可识别性界）
│       ├── Dirichlet.lean   # 附录E（Dirichlet 能量替代证明）
│       └── Planning.lean    # 定理4（规划等价）
└── experiments/
    ├── lejepa_id/
    │   ├── mixing.py        # 非线性混合（spiral/banana/sinusoid/coupling）
    │   ├── losses.py        # SIGReg、白化损失、对齐损失、InfoNCE
    │   ├── models.py        # MLP 编码器、MatchedEncoder、CNN 编码器
    │   ├── data.py          # 潜变量采样、OU 增强
    │   ├── metrics.py       # R²、正交误差、近似界量化、Procrustes
    │   ├── reacher.py       # DMC Reacher 渲染与数据集
    │   └── engine.py        # 训练循环（warmup + cosine LR）
    ├── run.py               # 2D/scaling/gennorm/grid 统一入口
    ├── run_reacher.py       # Reacher 像素观测入口
    ├── prerender.py         # 渲染 Reacher OU/轨迹帧
    ├── analysis/            # 后处理绘图与表格
    └── configs/             # 实验超参数 YAML
```

---

### 核心实现：损失函数（[`losses.py`](JEPA/lejepa-identifiability/experiments/lejepa_id/losses.py)）

#### [`SIGReg`](JEPA/lejepa-identifiability/experiments/lejepa_id/losses.py:8)（Sliced characteristic-function Isotropic Gaussian Regularizer）

> 代码 docstring 标注为 *Sliced characteristic function regularizer*（Balestriero & LeCun 2025）。

```python
class SIGReg(nn.Module):
    def __init__(self, knots=17, n_slices=256, t_max=3.0):
        # 梯形积分节点 + 高斯加权
        t = torch.linspace(0, t_max, knots)
        dt = t_max / (knots - 1)
        w = torch.full((knots,), 2 * dt); w[[0, -1]] = dt   # 梯形权重
        self.phi = torch.exp(-t**2 / 2)                     # 标准高斯特征函数
        self.weights = w * torch.exp(-t**2 / 2)             # 积分权重×高斯加权

    def forward(self, h):
        # h: (V, B, N) -> scalar
        flat = h.flatten(0, 1)
        A = F.normalize(torch.randn(flat.size(-1), self.n_slices), dim=0)  # 随机切片方向
        xt = (flat @ A).unsqueeze(-1) * self.t
        err = (xt.cos().mean(0) - self.phi)**2 + xt.sin().mean(0)**2
        return (err @ self.weights).mean() * flat.size(0)
```

**关键设计：**
- 用**特征函数**（Fourier 变换）的实部/虚部偏差度量分布差异，而非矩匹配
- 随机切片（slicing）将高维问题降为一维投影，线性时间复杂度
- `knots=17` 个积分节点，`n_slices=256` 个随机方向，`t_max=3.0`
- 积分权重 `weights = 梯形权重 × exp(-t²/2)`：对低频段加权更高，与高斯特征函数的衰减一致

#### [`alignment_loss`](JEPA/lejepa-identifiability/experiments/lejepa_id/losses.py:39) 与 [`whitening_loss`](JEPA/lejepa-identifiability/experiments/lejepa_id/losses.py:31)

```python
def alignment_loss(h):
    """拉近正样本对。h: (V, B, N) -> scalar"""
    return (h.mean(0) - h).square().mean()

def whitening_loss(h):
    """||Cov(h) - I||²_F（VICReg 风格白化）"""
    cov = (flat.T @ flat) / (flat.shape[0] - 1)
    return (cov - torch.eye(...)).square().mean()
```

**训练目标：**
```python
# LeJEPA 模式
loss = lamb * sig + (1 - lamb) * align

# VICReg 模式（对比用）
loss = lamb * wht + (1 - lamb) * align

# InfoNCE 模式（对比用）
loss = infonce_loss(h, sigma)
```

---

### 核心实现：非线性混合（[`mixing.py`](JEPA/lejepa-identifiability/experiments/lejepa_id/mixing.py)）

> 混合函数 `g` 将独立潜变量 `z` 映射到"观测"空间 `x = g(z)`，模拟世界的非线性渲染。编码器的任务是反转它（恢复到正交等价）。

```python
def mix_spiral(z):
    """g(z) = R(π‖z‖) z —— 保测度螺旋微分同胚（旋转角随半径变化）"""

def mix_banana(z):
    """香蕉形：x₀ = z₀, x₁ = z₁ + z₀²"""

def mix_sinusoid(z):
    """正弦剪切：x₀ = z₀ + sin(1.5 z₁), x₁ = z₁"""

def make_coupling_mixing(N, n_layers=4, seed=1337):
    """RealNVP 风格耦合层，适用于任意偶数维 N（含 N=2 的 'nvp' 情形）
    交替更新：z2 += tanh(z1 @ W) / z1 += tanh(z2 @ W)，W 为正交矩阵×2"""
```

**设计要点：**
- `spiral` 保测度 → 不改变体积，是对编码器最严苛的"扭曲"测试
- `banana`/`sinusoid` 引入低阶多项式/三角非线性
- `coupling` 提供可扩展到高维的可逆混合，与 [`MatchedEncoder`](JEPA/lejepa-identifiability/experiments/lejepa_id/models.py:17) 结构对偶

---

### 核心实现：数据生成（[`data.py`](JEPA/lejepa-identifiability/experiments/lejepa_id/data.py)）

#### [`ou_augment`](JEPA/lejepa-identifiability/experiments/lejepa_id/data.py:29)（OU 过程增强）

```python
def ou_augment(z, rho, n_views=2, dist="gaussian", alpha=None):
    """z' = ρz + √(1-ρ²)η，η 与 z 同分布
    返回 (V, B, N) 形状的多视图张量"""
    fac = (1 - rho ** 2) ** 0.5
    eta = sample_latents(n_views * D, N, dist=dist, ...)
    return rho * z.unsqueeze(0) + fac * eta
```

**支持的分布：**
- `"gaussian"`：标准正态（理论保证成立）
- `"laplace"`：拉普拉斯（理论保证失效，用于消融）
- `"gennorm"`：广义正态（扫描形状参数 α，验证定理2）

---

### 核心实现：评估指标（[`metrics.py`](JEPA/lejepa-identifiability/experiments/lejepa_id/metrics.py)）

#### [`compute_all_metrics`](JEPA/lejepa-identifiability/experiments/lejepa_id/metrics.py:16)

```python
def compute_all_metrics(z, x, h, h_prime, rho, N):
    # 混合可逆性 R²（x↔z，作为上界参考）
    r2_zx, r2_xz = bidirectional_r2(z, x)
    # 双向 R²（z↔h，线性可识别性的主要指标）
    r2_zh, r2_hz = bidirectional_r2(z, h)

    # 正交误差（衡量 h = Qz 中 Q 的正交性）
    A = W[:N].T  # 线性回归系数
    orth_err = ||A^T A - I||_F
    orth_err_normalized = orth_err / √N   # 维度归一化，便于跨 N 比较

    # 近似界量化（验证定理3）
    delta = max(L_h - 2*(1-rho)*trace_cov, 0)
    D_bound = delta / (2*rho*(1-rho))          # spectral_gap = 2ρ(1-ρ)
    approx_bound = D_bound + (epsilon + D_bound)**2

    # Procrustes 距离（最优正交对齐后的误差）
    M = h^T z / n;  U, S, Vt = SVD(M);  Q = U @ Vt
    procrustes_mse = ||h - z @ Q^T||²
```

**辅助函数：** [`compute_recovery_metrics`](JEPA/lejepa-identifiability/experiments/lejepa_id/metrics.py:54) 用于 Reacher 等只需 `R²(z↔h)` + 正交误差的场景，支持 `suffix` 区分 OU/轨迹编码器的指标键名。

---

### 核心实现：编码器架构（[`models.py`](JEPA/lejepa-identifiability/experiments/lejepa_id/models.py)）

| 编码器 | 用途 | 结构 |
|--------|------|------|
| [`make_mlp_encoder`](JEPA/lejepa-identifiability/experiments/lejepa_id/models.py:8) | 2D 实验 | 4层 MLP + GELU |
| [`MatchedEncoder`](JEPA/lejepa-identifiability/experiments/lejepa_id/models.py:17) | 高维 Scaling | 逆 NVP 耦合层（与混合函数匹配） |
| [`make_cnn_encoder`](JEPA/lejepa-identifiability/experiments/lejepa_id/models.py:46) | Reacher 像素 | 4层 CNN + BN + AvgPool + 线性头 |

**MatchedEncoder 设计亮点：**
- 与 RealNVP 混合函数**结构对称**（逆耦合层）
- 理论上能精确反转混合，验证可识别性上界
- 参数：`z2 = z2 - tanh(z1 @ W)`（逆向耦合）

---

### 核心实现：训练引擎（[`engine.py`](JEPA/lejepa-identifiability/experiments/lejepa_id/engine.py)）

```python
def train_and_evaluate(encoder, mix_fn, *, N, rho, lamb, mode="lejepa", steps=20000, ...):
    # LR 调度：前半段恒定，后半段 cosine 衰减
    # 在线数据生成（无需预存数据集）
    # 每 log_every 步在固定 eval 集上评估所有指标
```

**训练流程：**
1. 采样潜变量 `z ~ N(0, I_N)`（或 laplace/gennorm，用于消融）
2. OU 增强得到正样本对 `(z, z')`
3. 混合函数 `g` 映射到观测空间 `(x, x') = (g(z), g(z'))`
4. 编码器 `h` 映射到嵌入空间
5. 按 `mode` 计算损失：
   - `lejepa`：`L = λ·SIGReg + (1-λ)·Alignment`
   - `whiten`（VICReg 风格对照）：`L = λ·Whitening + (1-λ)·Alignment`
   - `infonce`：`L = InfoNCE(h, σ)`
6. AdamW 优化（`lr=3e-3`，warmup 占前半段，后半段 cosine 衰减）
7. 每 `log_every` 步在固定 `z_eval` 集上评估全部指标

---

### 核心实现：Reacher 像素数据（[`reacher.py`](JEPA/lejepa-identifiability/experiments/lejepa_id/reacher.py)）

> 验证定理4的物理控制实验，基于 DeepMind Control Suite 的 `reacher / hard` 任务，通过 MuJoCo（EGL 后端）渲染 64×64 像素帧。

| 函数 | 作用 |
|------|------|
| [`render_at`](JEPA/lejepa-identifiability/experiments/lejepa_id/reacher.py:18) | 设定关节角 `qpos` 与目标位置，渲染单帧 `(3,64,64)` |
| [`generate_ou_image_pairs`](JEPA/lejepa-identifiability/experiments/lejepa_id/reacher.py:37) | 用 OU 过程采样关节角对 `(z_t, z_{t+1})` 并渲染为图像对 |
| [`solve_ik_grid`](JEPA/lejepa-identifiability/experiments/lejepa_id/reacher.py:66) | 200×200 网格搜索逆运动学，定位指尖到目标的关节角 |
| [`ReacherOUDataset`](JEPA/lejepa-identifiability/experiments/lejepa_id/reacher.py:82) | 预渲染 OU 图像对 + 真值潜变量（2D 关节角）的数据集 |

**关键点：** 潜变量是 **2D 关节角**，像素是高度非线性的"渲染混合"。OU 编码器恢复正交等价关节角 → 规划等价；RL 轨迹编码器因数据非各向同性而失效。

---

## 🔬 Lean 4 形式化证明深度解析

### 定理1证明链（[`Hermite.lean`](JEPA/lejepa-identifiability/lean/LeJEPA/Hermite.lean)）

**核心数据结构：**
```lean
structure SpectralWeights where
  w : ℕ → ℝ          -- Hermite 展开系数
  nonneg : ∀ d, 0 ≤ w d
  zero_degree : w 0 = 0   -- 零均值约束
  total_variance : ∑' d, w d = 1  -- 单位方差
```

**7步验证链：**

| 步骤 | 定理/引理 | 状态 |
|------|-----------|------|
| 1 | `mehler_summability`：Mehler 公式可求和性 | 公理化 |
| 2 | `correlation_le_rho`：相关性 ≤ ρ | ✅ 已验证 |
| 3 | `loss_lower_bound`：损失 ≥ 2(1-ρ)n | ✅ 已验证 |
| 4 | 最优性 → 每个 corr_i = ρ（`Finset.sum_lt_sum`） | ✅ 已验证 |
| 5 | `equality_forces_degree_one`：corr_i = ρ → w₁ = 1 | ✅ 已验证 |
| 6 | `linear_of_degree_one`：w₁ = 1 → h 线性 | 公理化 |
| 7 | `orthogonal_of_gaussian_linear`：线性 + 高斯 → 正交 | 公理化 |

**关键引理（已验证）：**
```lean
-- ρᵈ < ρ 对 d ≥ 2 严格成立（非线性成分被严格惩罚）
theorem pow_lt_self_of_ge_two (ρ : ℝ) (hρ0 : 0 < ρ) (hρ1 : ρ < 1)
    (d : ℕ) (hd : 2 ≤ d) : ρ ^ d < ρ

-- 等号成立 ⟺ 所有 d ≥ 2 的权重为零（即 h 是线性的）
theorem equality_forces_degree_one ...
    (heq : ∑' d, sw.w d * ρ ^ d = ρ) :
    ∀ d, 2 ≤ d → sw.w d = 0
```

---

### 定理2证明链（[`Uniqueness.lean`](JEPA/lejepa-identifiability/lean/LeJEPA/Uniqueness.lean)）

**Sturm-Liouville 框架：**
```lean
structure LatentComponent where
  K : ℝ          -- 扩散系数（K > 0）
  score : ℝ → ℝ  -- (log p)'，得分函数
  ev : ℝ         -- 第一非常数特征值 λ₁（ev > 0）
```

**核心代数步骤（已验证）：**
```lean
-- K·score(z)·a = −ev·(az + b)，a ≠ 0
-- ⟹ score(z) = (−ev/K)z + (−ev·b/(Ka))，斜率 < 0
theorem score_affine_of_eigenfunction ...
    ⟹ ∃ α β, α < 0 ∧ score z = α * z + β
```

**双条件定理（已验证）：**
```lean
theorem gaussian_uniqueness (lc : LatentComponent) :
    (IsGaussianScore → ∃ 仿射特征函数)  -- if 方向
    ∧
    (∀ 仿射特征函数 → IsGaussianScore)  -- only-if 方向
```

---

### 定理3证明链（[`Approx.lean`](JEPA/lejepa-identifiability/lean/LeJEPA/Approx.lean)，Proposition 4.3）

**核心装配定理（已验证）：**
```lean
theorem approximate_identifiability
    (ρ δ ε W_nl M_Q_norm total_error : ℝ) ...
    (hgap : δ ≥ 2 * ρ * (1 - ρ) * W_nl)        -- 谱间隙控制非线性能量
    (hpolar : M_Q_norm ≤ ε + W_nl)             -- 极分解界
    (hpythag : total_error = M_Q_norm ^ 2 + W_nl) :  -- 勾股分解
    total_error ≤ δ / (2*ρ*(1-ρ)) + (ε + δ/(2*ρ*(1-ρ))) ^ 2
```

**验证状态表：**

| 组件 | 状态 |
|------|------|
| 谱间隙正性 `2ρ(1-ρ) > 0` | ✅ 已验证 |
| 非线性能量界 `W_nl ≤ D` | ✅ 已验证 |
| 极分解 `‖M−Q‖ ≤ ε+W_nl` | 公理化 |
| 跨阶 Hermite 正交性 | 公理化 |
| 线性偏差平方界 | ✅ 已验证 |
| 勾股分解 | 公理化 |
| 单调性 `(ε+t)²+t` 递增 | ✅ 已验证 |
| 完整界装配 | ✅ 已验证 |
| 精确恢复 `δ=ε=0 ⟹ 误差=0`（退化为定理1） | ✅ 已验证 |

**附加结论（已验证）：** [`bound_small_perturbation`](JEPA/lejepa-identifiability/lean/LeJEPA/Approx.lean:181)——当 `ε+D ≤ 1` 时，二次项可被一阶项控制，界简化为 `≤ 2D + ε`。

---

### 定理4证明链（[`Planning.lean`](JEPA/lejepa-identifiability/lean/LeJEPA/Planning.lean)，Corollary）

**控制问题结构：**
```lean
structure ControlProblem (n : ℕ) (Action : Type*) where
  stage_cost : Latent n → Action → ℝ
  terminal_cost : Latent n → ℝ

-- O(n) 不变性：ℓ(Qz, a) = ℓ(z, a)
def IsOrthogonalInvariant cp Q : Prop :=
  (∀ z a, cp.stage_cost (Q z) a = cp.stage_cost z a) ∧
  (∀ z, cp.terminal_cost (Q z) = cp.terminal_cost z)
```

**规划等价定理（已验证）：**
```lean
-- 对任意动作序列，推前动力学下的总代价 = 原始动力学下的总代价
theorem planning_equivalence ... :
    totalCost cp E_hat a (Q z) = totalCost cp E a z

-- 最优动作序列在两个空间中完全相同
theorem minimizer_equivalence ... :
    (∀ a', cost_hat a (Q z) ≤ cost_hat a' (Q z)) ↔
    (∀ a', cost a z ≤ cost a' z)
```

---

## 🖼️ 官方网站图示解读

> 来源：https://klindtlab.github.io/lejepa-identifiability/（2026-05-27）

### 核心图示（三面板）

```
[左] 世界的潜变量          [中] 非线性混合           [右] LeJEPA 恢复
  z ~ N(0, I_n)    →→→   x = g(z)（未知）   →→→   h(x) = Qz（正交）
  独立高斯分量              螺旋/香蕉/剪切等           旋转等价恢复
```

**TL;DR（官网原文）：**
> LeJEPA linearly recovers the world's latent variables — up to rotation — **if and only if** those latents are Gaussian. The forward direction is a spectral argument on Hermite polynomials; the converse rules out every non-Gaussian alternative. All proofs are checked in Lean 4.

### 实验图示解读

**图(a)：近似界验证（定理3）**
- 横轴：理论界 `D + (ε+D)²`
- 纵轴：实际恢复误差
- 所有运行点均在对角线**下方**（界成立）

**图(b)：高斯唯一性（定理2）**
- 横轴：广义正态形状参数 α（α=2 为高斯）
- 纵轴：线性可识别性 R²
- R² 在 **α=2 处尖锐达到峰值**，两侧均下降

**图(c)：控制代价（定理4）**
- 高斯-OU 编码器：与 oracle 统计上无显著差异
- 轨迹编码器：代价显著偏高

**图(d)：代价随 R² 单调下降**
- 线性可识别性越高 → 规划代价越低
- 支持定理4的连续性推论

### Reacher 规划演示

```
[顶行] Oracle（关节空间直线）：平滑弧线轨迹
[中行] 高斯-OU 编码器：紧密跟随 oracle
[底行] RL 轨迹编码器：明显偏离（不可识别）
```

解码方式：在潜空间中线性插值，用**最近邻检索**解码到像素帧。

---

## 📊 完整实验结果表（官网版）

| N | 混合 R²(x→z) | SIGReg R²(h→z) | VICReg R²(h→z) | InfoNCE R²(h→z) |
|---|-------------|----------------|----------------|-----------------|
| 2 | 0.781±2.1e-3 | **0.999998**±3.4e-7 | 0.999996±8.4e-7 | 0.950961±1.6e-3 |
| 4 | 0.727±24e-3 | **0.999996**±12e-7 | 0.999987±54e-7 | 0.910871±8.2e-3 |
| 8 | 0.728±10e-3 | **0.999993**±9.0e-7 | 0.999988±4.8e-7 | 0.886818±42e-3 |
| 16 | 0.734±6.3e-3 | **0.999988**±4.9e-7 | 0.999987±4.6e-7 | 0.999880±0.01e-3 |
| 32 | 0.737±2.3e-3 | **0.999981**±7.2e-7 | 0.999981±9.4e-7 | 0.907809±26e-3 |
| 64 | 0.737±1.5e-3 | **0.999966**±7.4e-7 | 0.999968±8.1e-7 | 0.648496±3.1e-3 |
| 128 | 0.739±0.61e-3 | **0.999938**±3.2e-7 | 0.999942±7.2e-7 | 0.566955±6.6e-3 |
| 256 | 0.742±0.49e-3 | **0.999884**±7.9e-7 | 0.999889±7.2e-7 | 0.696587±0.49e-3 |
| 512 | 0.749±0.30e-3 | **0.999775**±6.7e-7 | 0.999785±6.9e-7 | 0.704393±0.26e-3 |
| 1024 | 0.763±0.17e-3 | **0.999561**±12e-7 | 0.999582±11e-7 | 0.720241±0.20e-3 |

> 5 个随机种子的均值±标准差。SIGReg 和 VICReg 在所有维度保持 R² > 0.999；InfoNCE 在高维（N ≥ 64）因固定核宽度退化。