实证复现与 Lean 考证

技术栈、路线图与落地方案

本文是《Hansen计量评注》的方法页，不是 Lean 子工程，也不是教材正文。当前不建立 Lean 仓库；先把双轨目标、参照项目、技术栈与验收标准写清楚，再按章推进。面向教师的系统教程（范式差异、历史、类型论、技术栈、工作流、结果解释、计量路径）在栏目 Lean 形式化，源稿目录 block-lean/。

1 为何放在 hansenpeer

问题 结论
这份 qmd 写在哪？ 本仓库 block-ext/stack-roadmap.qmd，挂在「思考扩展」
为何不放 hansenEM？ hansenEM 是 Hansen (2022年) 双语源稿站点；路线图属于评注方法，不应混入 chapters_eng/ / chapters_chn/
教材侧如何看见？ hansenEM 的「开发声明」只保留一条指向本页的入口，避免两份正文

双仓库分工不变：定理与表图的原文在 hansenEM（chapters_eng/、hansen-programs/、hansen-data/）；复现脚本、逐步证明、本章清单写在本仓库。跨仓库用章节号对齐。日后若做 Lean，另开独立 git，不要写进 _book/ 或 hansenEM/_site/。

2 双轨目标

flowchart TB
  src["hansenEM 原文<br/>定理 / 表图 / 随书脚本"]
  src --> emp["实证轨<br/>R / Stata 复现"]
  src --> l1["理论 L1<br/>教学展开"]
  l1 --> l2["理论 L2<br/>计算核对"]
  l1 -.-> l3["理论 L3<br/>Lean 证书<br/>尚未开工"]

  • 实证轨：用可编程脚本复现书中表、图与系数；先跑通作者公开程序，再独立实现并对照数字。
  • 理论轨：把教材省略的推导展开，使师生能逐步核验。默认交付是 L1（Quarto 证明笔记）；L2 是 R 可算的代数/模拟；L3 才是 Lean。未做 L3 时，不写「已形式化证明」。

3 两个参照仓库

3.1 lean-hansen-econometrics

社区项目 mostlyharmfuleconometrics/lean-hansen-econometrics 按章形式化 Hansen 的数学结果，目标是可复用 API（Application Programming Interface，可调用的程序接口）与原文对照表，而不是逐句翻译教材。

公开状态（以该仓库 README 为准）：第 2–13 章有 Lean 模块并被根库导入；第 1、14–29 章多为 inventory（定理清单）；没有任何一章被标成「整章完成」。工具链钉在 Lean 4.29.0 与 Mathlib（Lean 的数学库）v4.29.0。

对我们可直接搬用的方法：

  1. 先 inventory，再证明。 每章一份 inventory/chN-inventory.md：印刷陈述、假设、Lean 目标、缺口。空单元格表示未做，不要虚构定理名。
  2. 分层 API。 LinearAlgebraUtils / ProbabilityUtils / AsymptoticUtils 为可复用层；章文件给出 Hansen 记号的薄包装。
  3. 印刷陈述可能过强或有误。 该库在第 11、12、13 章显式区分字面陈述、修正陈述与诊断性反例。我们的 L1 笔记同样必须标出「原文 vs 采用的条件」。
  4. 有限样本普通最小二乘（OLS, Ordinary Least Squares）的三种全函数化。 Base（要求 \(X'X\) 可逆）、Star（奇异时走 nonsingInv）、OrZero（教材对外包装）。渐近证明用 Star，章末可引用的陈述用 OrZero。
  5. 对照表 + 门禁。 定理编号 ↔︎ Lean 声明；lake build 与 Mathlib 风格检查进 CI（Continuous Integration，持续集成）；另有 redundancy / hygiene / faithfulness / proof-quality 四维审阅（冗余、卫生、保真、证明质量）。

不要整库 fork 进本仓库。我们的差异化是中文教学展开、实证数字复现，以及 Cursor 双仓库协同。该库是对照与借鉴对象。

3.2 NavierStokesAndEuler

OpenAI 仓库 openai/NavierStokesAndEuler 为分析论文提供 Lean 4 证书。工具链为 Lean 4.34.0-rc2 + Mathlib 同标签；sorry_count: 0。根目录 formalization.yaml 把论文定理、Lean 声明、文件路径、公理（propext 命题外延、Classical.choice 选择公理、Quot.sound 商类型）写成机器可读元数据。Comparator（对照检查器）挑战把陈述接到独立参考（DeepMind Formal Conjectures 中的 Navier–Stokes 表述），用第二套检查器跑 lake exe comparator。

公告中的工作顺序是：多智能体先写分析证明，再用另一模型编成 Lean。公开结果对应 Clay 表述中带光滑外力的 C/D，不是无外力的 A/B。内核只保证「这个形式陈述可从给定公理推出」，不保证「这个陈述就是原问题」。

对计量评注的迁移：

他们 我们
分析 PDF + Lean 证书拆开 L1 笔记 +（将来）L3 lake build
formalization.yaml 对齐论文定理 章 inventory 对齐 Hansen 定理号
Comparator 对照独立问题陈述 对照 hansenEM/chapters_eng 原文
不申领超范围结论 不把 L1/L2 说成形式化证明
上万并发智能体 不模仿；用 Cursor 读原文、跑脚本、一次钉一条定理

4 技术栈

4.1 共同层

  • 源稿与发布：Quarto Website；本仓库产物 _book/，教材侧 _site/。只改 .qmd 源稿。
  • 协同：同一 Cursor workspace，两套独立 git；章节号对齐；Agent 先打开 hansenEM 再写本仓库。
  • 文献：本仓库 hansenpeer.bib；教材侧 hansenEM/bib/。不要把一侧 renv 拷到另一侧。

4.2 实证轨

组件 用途
R（≥ 4.2）+ renv 主实现与可重复环境
Stata 对照作者 .do，不是默认主实现
Quarto / knitr 把估计结果写进 .qmd
作者数据与程序 hansenEM/hansen-data/、hansenEM/hansen-programs/，或 Hansen 官网 zip
教材侧轻量复现 hansenEM/replication/（贴近书中表图）
评注侧独立实现 本仓库 part*/、Rscript/、code/

验收：同一表号下并列「教材数字 | 作者脚本 | 本仓库脚本」，差异必须解释（异方差一致（HC, heteroskedasticity-consistent）标准误公式、自由度、软件默认值、样本筛选）。只改作者脚本却声称独立复现，不算通过。

4.3 理论轨

层 栈 现在做不做
L1 教学展开 Quarto + LaTeX；假设清单与引理拆分 做
L2 计算核对 R 矩阵恒等式、有限样本模拟 命题可算时做
L3 逻辑证书 日后：elan（工具链管理器）+ Lean 4 + Mathlib + Lake（Lean + Make，包与构建）；lean-toolchain 与 Mathlib 同标签钉死；lake exe cache get && lake build 暂不做子工程

L3 若开工，版本跟当时的 Mathlib 稳定标签走，不必绑定参照仓库的 4.29.0 或 4.34.0-rc2。Mathlib 与 Lean 必须锁在一起。社区安装见 Lean projects。

L3 目录原则（预告，不是现在创建）：独立 git；根库 import 表面；inventory/ 为对照真相源；Lean 源与 Quarto 评注分开放。不要把 .lean 塞进本仓库 _book/ 或教材章节。

5 路线图

阶段可以并行，但依赖关系不要反着走。

5.1 阶段 0：方法冻结（本页）

  • 双仓库职责、三层证书、两个参照项目的可迁移点写进本页与 .cursor 规则。
  • 不初始化 Lean 工程，不把 Mathlib 源码拷进仓库（vendor）。

5.2 阶段 1：章清单（仍无 Lean）

对准备动手的章，在本仓库写 Markdown inventory（建议 inventory/chNN.md，需要时再加）：

  • Hansen 定理/定义/假设编号
  • hansenEM 对应 .qmd 路径
  • L1 笔记路径、实证脚本路径
  • 印刷陈述是否过强；Lean 目标列先留空

优先第 2–4 章（条件期望、OLS 代数、有限样本）和第 4、12 章实证（工资例、Card 工具变量（IV, Instrumental Variables））。

5.3 阶段 2：实证独立化

  1. 打开教材表/图与假设。
  2. 跑通 hansen-programs。
  3. 在本仓库重写 R 实现。
  4. 填对照表。
  5. 扩展（别的标准误、别的样本）与「书中结论」分开写。

近期样本：part01-reg/chpt04-empirical-example.qmd 与教材第 12 章 IV（hansenEM/replication/chpt12-iv/ 已有轻量复现，评注侧补独立实现与讨论）。

5.4 阶段 3：L1 证明展开

按「先代数、后渐近」：

  1. 第 3 章：正规方程、投影 \(P\) 与歼灭子 \(M\)、Frisch–Waugh–Lovell（FWL）定理、leave-one-out（逐一剔除；本仓库已有记号与 leave-one-out 笔记，可升格为定理级展开）。
  2. 第 2 章：塔性质、正交性、最佳预测、线性投影。
  3. 第 4 章：无偏性与方差（写清独立同分布（i.i.d.）与满秩）。
  4. 更晚：第 6–7 章渐近、第 10 章 bootstrap（自助法）、第 12–13 章 IV / 广义矩方法（GMM, Generalized Method of Moments）。

每条定理一篇（或一节），不要整章空泛综述。模板见 节 6.2。

5.5 阶段 4：可选 L3（需另行决定）

仅当明确要求建立 Lean 子工程时：钉死工具链 → 先移植或重证第 3 章 FWL 一条链 → lake build 全绿 → 更新 inventory 对照表。可继续对照 lean-hansen-econometrics，但对外定理名与中文评注以我们的 inventory 为准。Comparator 式第二通道属于更后期。

6 落地方案

6.1 目录约定

hansenEM/                     # 教材源稿（只读对齐，除非改译文/纠错）
  chapters_eng/chptNN-*.qmd
  hansen-programs/  hansen-data/
  replication/                # 教材侧轻量表图

hansenpeer/                   # 评注（本页所在仓库）
  part01-reg/  part04-panel/  # 章评注与实证
  block-matrix/               # 矩阵预备
  block-ext/stack-roadmap.qmd # 本页
  block-lean/                 # Lean 形式化学习教程（无 lakefile）
  inventory/                  # 阶段 1 起：章清单（可后建）

Lean 子工程若出现，使用第三仓库或本仓库平行目录，独立 lakefile.toml / lean-toolchain，与 Quarto 站点构建解耦。

6.2 L1 笔记模板

## 对象
Hansen 定理 X.Y（章 NN）：[一句转述，不改条件]
原文：hansenEM/chapters_eng/chptNN-….qmd

## 维持假设
- Assumption A.B：…
- 教材未写明但证明用到：…

## 引理
1. …
2. …

## 逐步推导
（补「于是 / 显然」中的代数或极限交换）

## 对照
- 与教材一致
- 印刷陈述过强、记号冲突、或我们改用的条件

6.3 实证笔记最低字段

  • 教材表/图编号与章节
  • 数据文件、样本筛选、估计量
  • 作者脚本路径、本仓库脚本路径
  • 对照表与差异说明
  • 随机种子（模拟时）

6.4 验收

  • 实证：第三者能按 .qmd 复现对照表；数字对不上时有书面原因。
  • L1：假设与定理号能在 hansenEM 原文中定位；省略步骤已补；若修正陈述，不得静默改写。
  • L2：脚本对同一恒等式给出可重复的数值/符号核对。
  • L3（未来）：sorry 为 0（或 inventory 诚实记录剩余 sorry）；对照表指向具体声明；lake build 在钉死工具链下通过。内核通过 ≠ 已证明 Hansen 印刷原句。

6.5 与 Cursor Agent

  • 改教材正文：hansenEM 技能 hansen-textbook-qmd。
  • 写复现：hansen-empirical-replication。
  • 写证明：hansen-theory-proof（Lean 细节见该技能下 lean-stack.md）。
  • 一次只钉一条定理或一张表。

7 明确不做

  • 现在不创建 Lean 子工程、不提交 lakefile.toml。学习讲义放 block-lean/，与 Quarto 站点一起渲染，但不编译 Mathlib。
  • 不把 lean-hansen-econometrics 或 Mathlib 拷进本仓库。
  • 不把评注长证明写进 hansenEM/chapters_*。
  • 不用上万智能体规模衡量进度。
  • 不以 L1 文采或 L2 模拟代替逻辑证书。

参考文献

Hansen, Bruce. 2022年. Econometrics. Princeton University Press.