From 14ff05d9b88c97ad09dec835dc89154d34a98464 Mon Sep 17 00:00:00 2001
From: gaojie <gaojie@plantshero.com>
Date: Tue, 2 Jun 2026 04:41:13 +0800
Subject: [PATCH] Refactor code structure for improved readability and
 maintainability

---
 JEPA/{ =>  achieve}/lejepa_resources.md       |   0
 .../lejepa_world_model_notes.md               |   0
 JEPA/README.md                                | 891 ++++++++++++++++++
 .../sprekeler14a_sfa_identifiability.pdf      | Bin
 4 files changed, 891 insertions(+)
 rename JEPA/{ =>  achieve}/lejepa_resources.md (100%)
 rename JEPA/{ =>  achieve}/lejepa_world_model_notes.md (100%)
 create mode 100644 JEPA/README.md
 rename JEPA/{ => papers}/sprekeler14a_sfa_identifiability.pdf (100%)

diff --git a/JEPA/lejepa_resources.md b/JEPA/ achieve/lejepa_resources.md
similarity index 100%
rename from JEPA/lejepa_resources.md
rename to JEPA/ achieve/lejepa_resources.md
diff --git a/JEPA/lejepa_world_model_notes.md b/JEPA/ achieve/lejepa_world_model_notes.md
similarity index 100%
rename from JEPA/lejepa_world_model_notes.md
rename to JEPA/ achieve/lejepa_world_model_notes.md
diff --git a/JEPA/README.md b/JEPA/README.md
new file mode 100644
index 0000000..a4f4cc2
--- /dev/null
+++ b/JEPA/README.md
@@ -0,0 +1,891 @@
+# LeJEPA 世界模型可识别性 — 综合笔记
+
+> 本文档合并自 [`lejepa_world_model_notes.md`](JEPA/lejepa_world_model_notes.md)（论文与代码深度笔记）和 [`lejepa_resources.md`](JEPA/lejepa_resources.md)（资源汇总）。
+>
+> **论文：** *When Does LeJEPA Learn a World Model?*
+
+---
+
+## 📑 目录
+
+- [第一部分：论文阅读笔记](#第一部分论文阅读笔记)
+  - [核心问题](#-核心问题)
+  - [背景与动机](#-背景与动机)
+  - [世界模型的数学框架](#-世界模型的数学框架)
+  - [四大定理](#-四大定理)
+  - [实验验证](#-实验验证)
+  - [关键洞见](#-关键洞见)
+  - [形式化验证（Lean 4）](#-形式化验证lean-4)
+  - [与慢特征分析（SFA）的关系](#-与慢特征分析sfa的关系)
+  - [局限性与未来方向](#-局限性与未来方向)
+  - [核心贡献总结](#-核心贡献总结)
+- [第二部分：代码仓库深度解析](#第二部分代码仓库深度解析)
+- [第三部分：Lean 4 形式化证明深度解析](#第三部分lean-4-形式化证明深度解析)
+- [第四部分：官方网站图示与实验结果](#第四部分官方网站图示与实验结果)
+- [第五部分：资源汇总](#第五部分资源汇总)
+
+---
+
+# 第一部分：论文阅读笔记
+
+**作者：** 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）因固定核宽度退化。
+
+---
+
+# 第五部分：资源汇总
+
+> 通过互联网搜索整理，收录时间：2026-06-01
+
+## 🎬 视频资源
+
+### 官方演示视频
+| 标题 | 链接 | 频道 | 时间 | 说明 |
+|------|------|------|------|------|
+| **world model video**（官方） | https://youtu.be/EioGDo67ZDs | AI and the Brain | 2026-05-09 | 论文官方配套视频，291次观看，由作者团队发布 |
+
+> 📌 该视频由 GitHub README 直接链接，是论文的官方配套演示视频。
+
+---
+
+## 📄 论文资源
+
+### 核心论文
+
+| 论文 | arXiv | 发表时间 | 说明 |
+|------|-------|----------|------|
+| **When Does LeJEPA Learn a World Model?** | [2605.26379](https://arxiv.org/abs/2605.26379) | 2026-05-25 | 本文，可识别性理论 |
+| **LeJEPA: Provable and Scalable Self-Supervised Learning Without the Heuristics** | [2511.08544](https://arxiv.org/abs/2511.08544) | 2025-11-11 | LeJEPA 原始论文，提出 SIGReg |
+| **LeWorldModel: Stable End-to-End JEPA from Pixels** | [2603.19312](https://arxiv.org/abs/2603.19312) | 2026-03-13 | LeJEPA 扩展到动作条件控制 |
+| **V-JEPA 2: Self-Supervised Video Models** | [2506.09985](https://arxiv.org/abs/2506.09985) | 2025 | Meta 的视频 JEPA，理解/预测/规划 |
+| **Causal-JEPA** | [2602.11389](https://arxiv.org/abs/2602.11389) | 2026 | 通过对象级干预学习世界模型 |
+
+### LeJEPA 原始论文摘要（arXiv:2511.08544）
+> Learning manipulable representations of the world and its dynamics is central to AI. Joint-Embedding Predictive Architectures (JEPAs) offer a promising blueprint, but lack of practical guidance and theory has led to ad-hoc R&D. We present a comprehensive theory of JEPAs and instantiate it in **LeJEPA**, a lean, scalable, and theoretically grounded training objective.
+>
+> **核心贡献：**
+> - 识别各向同性高斯分布为 JEPA 嵌入的最优分布
+> - 提出 SIGReg（Sketched Isotropic Gaussian Regularization）
+> - 单一超参数、线性时间/内存复杂度、无启发式技巧
+> - ~50 行代码实现，ViT-H/14 在 ImageNet-1k 达到 79%
+
+### LeWorldModel 摘要（arXiv:2603.19312）
+> LeWorldModel (LeWM) 是首个仅用两个损失项（下一嵌入预测 + 高斯正则化）从原始像素端到端稳定训练的 JEPA。
+>
+> **亮点：**
+> - ~15M 参数，单 GPU 数小时可训
+> - 规划速度比基础模型快 48 倍
+> - 潜空间编码有意义的物理结构
+> - 可可靠检测物理上不合理的事件
+
+---
+
+## 🌐 官方网站与代码
+
+### 项目主页
+- **官方网站：** https://klindtlab.github.io/lejepa-identifiability/
+  - 包含完整摘要、定理说明、实验结果图表
+  - 发布时间：2026-05-27
+
+### 代码仓库
+- **可识别性论文代码：** https://github.com/klindtlab/lejepa-identifiability
+  - Lean 4 形式化证明（`lean/` 目录）
+  - 实验代码（`experiments/` 目录）
+  - 支持 2D、Scaling、Gennorm、Grid、Reacher 五类实验
+
+- **LeJEPA 原始代码：** https://github.com/rbalestr-lab/lejepa
+  - GitHub Stars: 1,170+
+  - 包含完整训练代码
+
+### 交互演示
+- **Google Colab Demo（~30秒，T4 GPU）：**
+  https://colab.research.google.com/drive/1ozjRk3FfUIDX7WBqlOKvhNcIamy0JxCH?usp=sharing
+
+---
+
+## 🤗 HuggingFace 资源
+
+### 论文页面
+- **可识别性论文：** https://huggingface.co/papers/2605.26379
+  - AI 生成摘要：LeJEPA demonstrates linear identifiability of latent variables from nonlinear observations under Gaussian distributions, enabling reliable world modeling and planning.
+
+- **LeJEPA 原始论文：** https://huggingface.co/papers/2511.08544
+
+### 相关模型（基于 LeJEPA 训练）
+| 模型 | 说明 |
+|------|------|
+| [gajeshladhar/core-jepa](https://huggingface.co/gajeshladhar/core-jepa) | 图像特征提取，25次下载 |
+| [falafel-hockey/lejepa-vit-small-patch8-256-sentinel2-5band](https://huggingface.co/falafel-hockey/lejepa-vit-small-patch8-256-sentinel2-5band) | 遥感图像（Sentinel-2）特征提取 |
+| [adipanda/lejepa](https://huggingface.co/adipanda/lejepa) | LeJEPA 模型 |
+| [caiovicentino1/lejepa-v1-tinyimagenet](https://huggingface.co/caiovicentino1/lejepa-v1-tinyimagenet) | TinyImageNet 训练版本 |
+
+### 相关数据集
+| 数据集 | 说明 |
+|--------|------|
+| [falafel-hockey/sentinel2-lejepa-global-diverse-256](https://huggingface.co/datasets/falafel-hockey/sentinel2-lejepa-global-diverse-256) | Sentinel-2 遥感数据，5k 样本 |
+
+---
+
+## 📚 相关背景论文
+
+### JEPA 系列
+| 论文 | 说明 |
+|------|------|
+| LeCun, *A Path Towards Autonomous Machine Intelligence* (2022) | JEPA 原始提案 |
+| I-JEPA (Assran et al., CVPR 2023) | 图像 JEPA |
+| V-JEPA (Bardes et al., 2024) | 视频 JEPA |
+| V-JEPA 2 (Assran et al., 2025) | 视频理解/预测/规划 |
+
+### 可识别性理论背景
+| 论文 | 说明 |
+|------|------|
+| Hyvärinen & Pajunen (1999) | 非线性 ICA 不可识别性 |
+| Hyvärinen & Morioka (2016, 2017) | 时间对比学习 + 非线性 ICA |
+| Khemakhem et al. (2020) | VAE + 非线性 ICA 统一框架 |
+| Sprekeler et al. (2014) | SFA 非线性盲源分离理论 |
+| Sobal et al. (2022) | JEPA 关注慢特征 |
+
+### 自监督学习对比
+| 方法 | 论文 | 与 LeJEPA 关系 |
+|------|------|----------------|
+| VICReg | Bardes et al. (2021) | 二阶矩白化，理论上等价 |
+| InfoNCE | van den Oord et al. (2018) | 隐式高斯化，高维退化 |
+| BYOL | Grill et al. (2020) | stop-gradient，无理论保证 |
+| SimSiam | Chen & He (2021) | stop-gradient，无理论保证 |
+| DINO/DINOv3 | Caron et al. (2021) / 2025 | 自蒸馏 + 特征聚类 |
+
+---
+
+## 🔬 技术要点速查
+
+### LeJEPA 训练目标
+```
+L(h) = λ · L_SIG + (1-λ) · L_inv
+
+L_inv = E[‖h(z') - h(z)‖²]          # 对齐损失（正样本对）
+L_SIG = SIGReg(h(z), N(0,I))         # 高斯正则化（防坍塌）
+```
+
+### SIGReg 实现原理
+- 通过随机切片（sliced/sketching）将嵌入投影到 `n_slices=256` 个一维方向
+- 在 `knots=17` 个积分节点上估计投影的**特征函数**（实部 `cos` + 虚部 `sin`）
+- 与标准高斯特征函数 `φ(t)=exp(-t²/2)` 对比，按梯形权重×高斯权重加权积分
+- 线性时间复杂度，~50 行代码（见 [`losses.py:SIGReg`](JEPA/lejepa-identifiability/experiments/lejepa_id/losses.py:8)）
+
+### 关键超参数
+| 参数 | 推荐范围 | 说明 |
+|------|----------|------|
+| `λ`（正则化权重） | `1e-3` ~ `1e-2` | 太大→坍塌，太小→不可识别 |
+| `ρ`（OU 相关性） | `0.8` ~ `0.95` | 控制正样本对的相似度 |
+
+### 实验结果摘要
+| 维度 N | SIGReg R² | VICReg R² | InfoNCE R² |
+|--------|-----------|-----------|------------|
+| 2 | 0.999998 | 0.999996 | 0.950961 |
+| 64 | 0.999966 | 0.999968 | 0.648496 |
+| 256 | 0.999884 | 0.999889 | 0.696587 |
+| 1024 | 0.999561 | 0.999582 | 0.720241 |
+
+---
+
+## 📋 BibTeX 引用
+
+```bibtex
+@article{klindt2026lejepa,
+  author    = {Klindt, David and LeCun, Yann and Balestriero, Randall},
+  title     = {When Does LeJEPA Learn a World Model?},
+  year      = {2026},
+  journal   = {arXiv preprint arXiv:2605.26379},
+}
+
+@article{balestriero2025lejepa,
+  author    = {Balestriero, Randall and LeCun, Yann},
+  title     = {LeJEPA: Provable and Scalable Self-Supervised Learning Without the Heuristics},
+  year      = {2025},
+  journal   = {arXiv preprint arXiv:2511.08544},
+}
+
+@article{maes2026leworldmodel,
+  author    = {Maes, Lucas and Le Lidec, Quentin and Scieur, Damien and LeCun, Yann and Balestriero, Randall},
+  title     = {LeWorldModel: Stable End-to-End Joint-Embedding Predictive Architecture from Pixels},
+  year      = {2026},
+  journal   = {arXiv preprint arXiv:2603.19312},
+}
+```
+
+---
+
+## 🗺️ 资源地图
+
+```
+LeJEPA 生态系统
+├── 理论基础
+│   ├── arXiv:2511.08544 (LeJEPA 原始论文)
+│   └── arXiv:2605.26379 (可识别性理论，本文)
+├── 应用扩展
+│   ├── arXiv:2603.19312 (LeWorldModel，像素控制)
+│   └── arXiv:2602.11389 (Causal-JEPA，因果干预)
+├── 代码
+│   ├── github.com/rbalestr-lab/lejepa (LeJEPA 训练)
+│   └── github.com/klindtlab/lejepa-identifiability (可识别性实验)
+├── 演示
+│   ├── YouTube: youtu.be/EioGDo67ZDs (官方视频)
+│   ├── 官网: klindtlab.github.io/lejepa-identifiability
+│   └── Colab: 交互式 2D 演示
+└── 社区
+    ├── HuggingFace: huggingface.co/papers/2605.26379
+    └── HuggingFace: huggingface.co/papers/2511.08544 (1170+ Stars)
+```
+
+---
+
+## 📖 相关文件
+
+- [数学证明分解导航](JEPA/math/README.md) — 6 个 topic 拆解四大定理
+- [代码仓库](JEPA/lejepa-identifiability/) — 本地 clone 的官方实现
+- [论文笔记原文](JEPA/lejepa_world_model_notes.md) ｜ [资源汇总原文](JEPA/lejepa_resources.md)
\ No newline at end of file
diff --git a/JEPA/sprekeler14a_sfa_identifiability.pdf b/JEPA/papers/sprekeler14a_sfa_identifiability.pdf
similarity index 100%
rename from JEPA/sprekeler14a_sfa_identifiability.pdf
rename to JEPA/papers/sprekeler14a_sfa_identifiability.pdf