worldmodel/JEPA/lejepa-identifiability/lean/HOWTO_PROOF.md

LeJEPA Lean 4 证明过程 How-To

本文档面向想要理解、修改或扩展 LeJEPA 形式化证明的读者。 从"为什么用 Lean"到"如何写一个新定理"，逐步讲解。

---

目录

1. 为什么用 Lean 4 做数学证明
2. 项目结构速览
3. 核心概念：axiom vs theorem
4. 定理 4.1 证明走读（Hermite.lean）
5. 定理 4.2 证明走读（Uniqueness.lean）
6. 命题 4.3 证明走读（Approx.lean）
7. 附录 C 证明走读（Dirichlet.lean）
8. 推论 4.5 证明走读（Planning.lean）
9. 常用 Lean 4 证明策略速查
10. 如何添加新定理
11. 调试技巧

---

1. 为什么用 Lean 4 做数学证明

传统数学证明的问题

论文中的数学证明依赖人类读者的直觉填补细节。例如"由 Mehler 公式显然有…"这类表述，实际上隐藏了大量步骤。

Lean 4 的优势

人类直觉证明                    Lean 4 形式化证明
─────────────────               ─────────────────────────────
"显然 ρᵈ ≤ ρ"                  pow_le_self_of_pos_lt_one ρ hρ0 hρ1 d hd
"由求和不等式"                  Summable.tsum_le_tsum (fun d => ...) ...
"等号成立当且仅当线性"           equality_forces_degree_one sw ρ hρ0 hρ1 ...

Lean 4 强制你填补每一个逻辑跳跃，编译通过即意味着证明无误。

Mathlib 的作用

Mathlib 是 Lean 4 的数学库，包含：

• 实分析（Mathlib.Analysis.*）
• 内积空间（Mathlib.Analysis.InnerProductSpace.*）
• 无穷级数（Mathlib.Topology.Algebra.InfiniteSum.*）
• 线性代数（Mathlib.LinearAlgebra.*）

LeJEPA 的证明大量复用 Mathlib 中已有的定理。

---

2. 项目结构速览

lean/
├── lakefile.lean          # 构建配置，声明 Mathlib 依赖
├── lean-toolchain         # 固定 Lean 版本：v4.28.0
├── lake-manifest.json     # 锁定所有依赖的精确 commit
├── LeJEPA.lean            # 顶层入口，import 所有子模块
└── LeJEPA/
    ├── Hermite.lean       # 定理 4.1：线性可识别性（主路径）
    ├── Uniqueness.lean    # 定理 4.2：高斯唯一性
    ├── Approx.lean        # 命题 4.3：近似可识别性界
    ├── Dirichlet.lean     # 附录 C：Dirichlet 能量替代证明
    ├── Planning.lean      # 推论 4.5：规划等价
    ├── PropApprox.lean    # 命题 4.3 辅助引理
    ├── ThmHermite.lean    # 定理 4.1 辅助引理
    └── ThmDirichlet.lean  # 附录 C 辅助引理

依赖关系

Hermite.lean ──────────────────────────────► 定理 4.1
     │
     ▼
Uniqueness.lean ───────────────────────────► 定理 4.2
     │
     ▼
Approx.lean ───────────────────────────────► 命题 4.3
     │
     ▼
Dirichlet.lean ────────────────────────────► 附录 C（独立路径）
Planning.lean ─────────────────────────────► 推论 4.5

---

3. 核心概念：axiom vs theorem

theorem（已验证）

theorem pow_le_self_of_pos_lt_one (ρ : ℝ) (hρ0 : 0 < ρ) (hρ1 : ρ ≤ 1)
    (d : ℕ) (hd : 1 ≤ d) : ρ ^ d ≤ ρ := by
  calc ρ ^ d ≤ ρ ^ 1 := pow_le_pow_of_le_one (le_of_lt hρ0) hρ1 hd
       _ = ρ := pow_one ρ

theorem 后面跟着 := by 和完整的证明策略。Lean 会机械地验证每一步。

axiom（公理化）

axiom mehler_summability
    (sw : SpectralWeights) (ρ : ℝ) (hρ0 : 0 < ρ) (hρ1 : ρ < 1) :
    Summable (fun d => sw.w d * ρ ^ d)

axiom 是无证明的假设，用于：

1. Mathlib 中存在但接口不匹配的结论（如 Mehler 公式）
2. 需要测度论/概率论框架才能严格表述的结论

⚠️ axiom 不影响已验证定理的正确性，但意味着这些结论的严格性依赖于公理的正确性。

structure（数据结构）

structure SpectralWeights where
  w : ℕ → ℝ           -- 权重函数
  nonneg : ∀ d, 0 ≤ w d
  zero_degree : w 0 = 0
  summable : Summable w
  total_variance : ∑' d, w d = 1

structure 将相关数据和约束打包，类似于数学中的"设 w 满足以下条件"。

---

4. 定理 4.1 证明走读（Hermite.lean）

数学陈述

若 h : ℝⁿ → ℝⁿ 满足 h(z) ~ N(0,Iₙ) 且最小化对齐损失，则 h(z) = Uz，U ∈ O(n)。

证明链

Mehler 公式（axiom）
    ↓
corr_i = Σ_d w_d ρᵈ（axiom: correlation_eq_spectral_sum）
    ↓
corr_i ≤ ρ（VERIFIED: correlation_le_rho）
    ↓
𝓛(h) ≥ 2(1-ρ)n（VERIFIED: loss_lower_bound）
    ↓
𝓛(h) = 2(1-ρ)n → 每个 corr_i = ρ（VERIFIED: Finset.sum_lt_sum）
    ↓
corr_i = ρ → w_d = 0 for d ≥ 2（VERIFIED: equality_forces_degree_one）
    ↓
h 是线性的（axiom: linear_of_degree_one）
    ↓
h 是正交的（axiom: orthogonal_of_gaussian_linear）

关键引理逐行解析

correlation_le_rho（相关性上界）

theorem correlation_le_rho (sw : SpectralWeights) (ρ : ℝ)
    (hρ0 : 0 < ρ) (hρ1 : ρ < 1)
    (hsum : Summable (fun d => sw.w d * ρ ^ d)) :
    ∑' d, sw.w d * ρ ^ d ≤ ρ := by
  calc ∑' d, sw.w d * ρ ^ d
      ≤ ∑' d, sw.w d * ρ :=          -- 逐项 w_d·ρᵈ ≤ w_d·ρ
        hsum.tsum_le_tsum
          (fun d => spectral_term_le sw ρ hρ0 (le_of_lt hρ1) d)
          (summable_spectral_upper sw ρ)
    _ = ρ := tsum_spectral_upper sw ρ  -- Σ w_d·ρ = ρ（因为 Σ w_d = 1）

关键 Mathlib 定理：

• Summable.tsum_le_tsum：若逐项 f(d) ≤ g(d) 且两者可求和，则 Σf ≤ Σg
• tsum_mul_right：Σ(a_d · c) = (Σ a_d) · c

equality_forces_degree_one（等号强制线性）

-- 反证法：假设存在 d₀ ≥ 2 使得 w_{d₀} > 0
by_contra h
push_neg at h
obtain ⟨d₀, hd₀_ge, hd₀_ne⟩ := h
-- 在 d₀ 处有严格不等式：w_{d₀}·ρ^{d₀} < w_{d₀}·ρ
have hstrict : sw.w d₀ * ρ ^ d₀ < sw.w d₀ * ρ := ...
-- 由 tsum_lt_tsum：Σ w_d·ρᵈ < Σ w_d·ρ = ρ
-- 但假设 Σ w_d·ρᵈ = ρ，矛盾

关键 Mathlib 定理：

• Summable.tsum_lt_tsum：若存在一项严格小且其余项 ≤，则 tsum 严格小

hermite_identifiability（主定理组装）

theorem hermite_identifiability ... := by
  -- Step 1: 每个相关性 ≤ ρ
  have hcorr_le : ∀ i, enc.correlation i ≤ ρ := ...
  -- Step 2: 最优时每个相关性 = ρ（反证：若某个 < ρ，则损失 > 2(1-ρ)n）
  have hcorr_eq_rho : ∀ i, enc.correlation i = ρ := by
    by_contra hne; push_neg at hne
    obtain ⟨i₀, hi₀⟩ := hne
    -- Finset.sum_lt_sum：一项严格小 → 总和严格小 → 损失严格大
    have hsum_lt : ∑ i, enc.correlation i < ∑ _i, ρ :=
      Finset.sum_lt_sum (fun i _ => hcorr_le i) ⟨i₀, ..., hi₀_lt⟩
    ...
  -- Step 3: 相关性 = ρ → 度数集中在 1
  have hdeg : ∀ i d, 2 ≤ d → (enc.spectrum i).w d = 0 := ...
  -- Step 4-5: 线性 + 正交（axiom）
  obtain ⟨M, hM⟩ := linear_of_degree_one enc hdeg
  obtain ⟨U, hU⟩ := orthogonal_of_gaussian_linear M hnorm_M
  exact ⟨U, fun z => by rw [hM z, hU z]⟩

---

5. 定理 4.2 证明走读（Uniqueness.lean）

数学陈述

转移算子的第一个非常数特征函数是仿射的，当且仅当 p 是高斯分布。

核心代数步骤

-- SL 特征方程：K · score(z) · a = −ev·(az + b)
-- 目标：推出 score(z) = αz + β，其中 α < 0

theorem score_affine_of_eigenfunction
    (lc : LatentComponent) (a b : ℝ) (ha : a ≠ 0)
    (heigen : ∀ z, lc.K * lc.score z * a = -(lc.ev * (a * z + b))) :
    ∃ (α β : ℝ), α < 0 ∧ (∀ z, lc.score z = α * z + β) := by
  refine ⟨-(lc.ev / lc.K), -(lc.ev * b / (lc.K * a)), ?_, ?_⟩
  · -- α = −ev/K < 0（因为 ev > 0, K > 0）
    have := div_pos lc.hev lc.hK; linarith
  · -- 代数化简：从特征方程解出 score(z)
    intro z
    have hKa_ne : lc.K * a ≠ 0 := mul_ne_zero (ne_of_gt lc.hK) ha
    have h1 : lc.score z = -(lc.ev * (a * z + b)) / (lc.K * a) := by
      field_simp at h ⊢; linarith
    rw [h1]; field_simp; ring

关键策略：

• field_simp：自动化简含除法的等式（需要非零条件）
• ring：纯代数恒等式验证
• linarith：线性算术推理

---

6. 命题 4.3 证明走读（Approx.lean）

数学陈述

𝔼[‖h(z) − Qz‖²] ≤ D + (ε + D)²，其中 D = δ/(2ρ(1−ρ))

四步证明结构

Step 1: 谱间隙控制非线性能量
  δ ≥ 2ρ(1−ρ)·W_nl  →  W_nl ≤ D

Step 2: 极分解给出线性偏差
  ‖M−Q‖ ≤ ε + W_nl  →  ‖M−Q‖² ≤ (ε+W_nl)²

Step 3: Pythagorean 分解（axiom）
  total_error = ‖M−Q‖² + W_nl

Step 4: 单调性
  W_nl ≤ D  →  (ε+W_nl)²+W_nl ≤ (ε+D)²+D

nonlinear_energy_le_D（Step 1）

theorem nonlinear_energy_le_D
    (ρ δ W_nl : ℝ) (hρ0 : 0 < ρ) (hρ1 : ρ < 1)
    (hgap : δ ≥ 2 * ρ * (1 - ρ) * W_nl) :
    W_nl ≤ δ / (2 * ρ * (1 - ρ)) := by
  have hsgap : (0 : ℝ) < 2 * ρ * (1 - ρ) := two_spectral_gap_pos ρ hρ0 hρ1
  rw [le_div_iff₀ hsgap]  -- W_nl ≤ δ/c ↔ W_nl·c ≤ δ（c > 0）
  linarith

bound_monotone（Step 4）

theorem bound_monotone (ε W_nl D : ℝ)
    (hle : W_nl ≤ D) :
    (ε + W_nl) ^ 2 + W_nl ≤ (ε + D) ^ 2 + D := by
  have h1 : ε + W_nl ≤ ε + D := by linarith
  nlinarith [sq_nonneg (ε + D - ε - W_nl)]
  -- nlinarith 处理非线性算术：(ε+D)²-(ε+W_nl)² = (D-W_nl)(2ε+D+W_nl) ≥ 0

关键策略：

• le_div_iff₀：将 a ≤ b/c（c > 0）转化为 a*c ≤ b
• nlinarith：非线性算术推理，可处理平方项

---

7. 附录 C 证明走读（Dirichlet.lean）

数学陈述

C¹ 微分同胚 + 保高斯测度 + 正交 Jacobian → h(z) = Uz

证明链（Step 3-6 已验证）

正交 Jacobian（假设）
    ↓
h 是 1-Lipschitz（MVT，VERIFIED）
    ↓
h⁻¹ 也是 1-Lipschitz（IFT + MVT，VERIFIED）
    ↓
双 Lipschitz → 全局等距（VERIFIED）
    ↓
Mazur–Ulam（axiom）→ h(z) = Az + b
    ↓
h(0) = 0 → b = 0（VERIFIED）
    ↓
A 保范数 → A 是线性等距（VERIFIED）

lipschitz_of_orthogonal_jacobian（MVT 应用）

theorem lipschitz_of_orthogonal_jacobian
    (h : GaussianDiffeo n)
    (horth : ∀ z v, ‖h.jacobian z v‖ = ‖v‖) :
    LipschitzWith 1 h.toFun := by
  apply lipschitzWith_of_nnnorm_fderiv_le (𝕜 := ℝ)
  · intro x; exact (h.hasFDeriv x).differentiableAt
  · intro x
    have hfderiv : fderiv ℝ h.toFun x = h.jacobian x :=
      (h.hasFDeriv x).fderiv
    rw [hfderiv, ContinuousLinearMap.opNNNorm_le_iff]
    intro y; simp only [one_mul]
    exact_mod_cast le_of_eq (horth x y)

关键 Mathlib 定理：

• lipschitzWith_of_nnnorm_fderiv_le：MVT 的 Lipschitz 版本
• ContinuousLinearMap.opNNNorm_le_iff：算子范数的等价刻画

isometry_of_bilipschitz（双 Lipschitz → 等距）

theorem isometry_of_bilipschitz ... := by
  rw [isometry_iff_dist_eq]
  intro x y
  apply le_antisymm
  · -- dist(hx,hy) ≤ dist(x,y)：正向 Lipschitz
    have hfwd := hlip.dist_le_mul x y
    simp only [NNReal.coe_one, one_mul] at hfwd; exact hfwd
  · -- dist(x,y) ≤ dist(hx,hy)：对 h⁻¹ 用 Lipschitz
    have hbwd := hinvlip.dist_le_mul (h.toFun x) (h.toFun y)
    -- h⁻¹(h(x)) = x，h⁻¹(h(y)) = y
    rw [hx, hy] at hbwd; exact hbwd

---

8. 推论 4.5 证明走读（Planning.lean）

数学陈述

对任意 O(n)-不变代价函数，在学习潜空间和真实潜空间中的最优值和最优计划完全一致。

核心定理：planning_equivalence

theorem planning_equivalence ... := by
  unfold totalCost
  -- 阶段代价等价：对每个时间步 t
  have hstage :
      (∑ t, E_hat.stage_exp a (Q z) t cp.stage_cost)
        = ∑ t, E.stage_exp a z t cp.stage_cost := by
    apply Finset.sum_congr rfl
    intro t _
    exact stage_cost_equiv cp Q E_hat E hinv a z t
  -- 终端代价等价
  have hterm := terminal_cost_equiv cp Q E_hat E hinv a z
  rw [hstage, hterm]

stage_cost_equiv（阶段代价等价）

-- 关键步骤：O(n)-不变性 + 轨迹推前 → 代价相等
theorem stage_cost_equiv ... := by
  rw [stage_pushforward E_hat E Q a z t cp.stage_cost]
  -- 推前后：E_hat.stage_exp a (Qz) t c = E.stage_exp a z t (c ∘ Q)
  -- 由 O(n)-不变性：c(Q z', act) = c(z', act)
  have hfun : (fun z' act => cp.stage_cost (Q z') act) = cp.stage_cost := by
    funext z'; funext act
    exact hinv.1 z' act  -- IsOrthogonalInvariant 的第一个分量
  rw [hfun]

---

9. 常用 Lean 4 证明策略速查

策略	用途	示例
linarith	线性算术（加减乘常数）	linarith [h1, h2]
nlinarith	非线性算术（含平方）	nlinarith [sq_nonneg x]
ring	纯代数恒等式	ring
field_simp	化简含除法的等式	field_simp [hne]
simp	自动化简	simp [lemma1, lemma2]
exact	精确匹配	exact h
exact_mod_cast	带类型转换的精确匹配	exact_mod_cast h
apply	应用定理（留下子目标）	apply mul_pos
rw	重写（等式替换）	rw [h1, h2]
calc	链式计算	calc a ≤ b := ... _ = c := ...
by_contra	反证法	by_contra h; push_neg at h
push_neg	将否定推入量词	push_neg at h
obtain	解构存在量词	obtain ⟨x, hx⟩ := h
intro	引入假设/变量	intro x hx
funext	函数外延性	funext x
constructor	分解 And/Iff	constructor
refine	部分填充目标	refine ⟨_, _, ?_, ?_⟩
set	引入局部定义	set D := δ / (2*ρ*(1-ρ)) with hD_def

---

10. 如何添加新定理

步骤 1：确定数学内容

例如，想证明"当 n=1 时，相关性上界是紧的"。

步骤 2：在合适的文件中添加

-- 在 Hermite.lean 末尾添加
/-- 当 n=1 且 w₁=1 时，相关性恰好等于 ρ。 -/
theorem correlation_tight_when_linear
    (sw : SpectralWeights)
    (hlin : ∀ d, 2 ≤ d → sw.w d = 0)
    (ρ : ℝ) (hρ0 : 0 < ρ) (hρ1 : ρ < 1)
    (hsum : Summable (fun d => sw.w d * ρ ^ d)) :
    ∑' d, sw.w d * ρ ^ d = ρ := by
  -- 由 hlin，所有 d ≥ 2 的项为 0
  -- 由 w₀ = 0（zero_degree），只剩 d=1 项
  -- w₁ = 1（由 total_variance 和其他项为 0）
  sorry -- 待完成

步骤 3：填写证明

  -- 将 tsum 分解为 d=0, d=1, d≥2 三部分
  have h_ge2 : ∀ d, 2 ≤ d → sw.w d * ρ ^ d = 0 := by
    intro d hd; simp [hlin d hd]
  have h0 : sw.w 0 * ρ ^ 0 = 0 := by simp [sw.zero_degree]
  -- 利用 tsum_eq_single 或手动计算
  ...

步骤 4：编译验证

cd lean
lake build LeJEPA.Hermite

步骤 5：检查无 sorry

grep -n "sorry" LeJEPA/Hermite.lean

---

11. 调试技巧

查看当前目标

在证明中插入 ? 或使用 #check 查看类型：

theorem my_thm ... := by
  intro h
  -- 此时在 VS Code 中将鼠标悬停在下一行可看到当前目标
  exact?  -- 让 Lean 搜索可用的定理

使用 #check 查看定理类型

#check Summable.tsum_le_tsum
-- Summable.tsum_le_tsum : Summable g → (∀ b, f b ≤ g b) → Summable f → tsum f ≤ tsum g

使用 example 快速测试

-- 不需要命名，快速验证一个小引理
example (a b : ℝ) (ha : 0 < a) (hb : 0 < b) : 0 < a * b :=
  mul_pos ha hb

常见错误及解决

错误	原因	解决
unknown identifier 'xxx'	引理名拼写错误	用 exact? 搜索
type mismatch	类型不匹配	检查隐式参数，用 exact_mod_cast
failed to synthesize instance	缺少类型类实例	检查 import，添加 [...] 实例
maximum recursion depth	证明太复杂	增加 set_option maxHeartbeats
tactic 'exact' failed