Tautology

用 Lean 4 从零构造实数并重建实分析，不依赖 mathlib，不依赖任何外部库。

这既是一个数学库，也是一次架构实验。

mathlib 的组织方式建立在一个假设上：整个数学可以装进一套全局一致的约定，靠类型类层级把所有结构统一起来。这个假设与数学研究的实际样子并不相符，由此产生的工程问题正在显现。

数学实际上由许多王国组成。每个小世界有自己的约定，彼此并不统一——Fourier 变换有好几种归一化，Hermite 多项式有概率论版和物理版，谁也没义务迁就谁。跨界时需要的是接口或翻译，而不是强行统一。而且当一个领域要用另一个领域的结果时，通常只是把公开接口接上就够了，并不需要钻进对方的细节——复几何用 Newlander–Nirenberg 定理时，用的是那条陈述，不是它的证明内部。

所以本项目主张：符合数学实践的形式化生态应当是模块化、接口式的。小世界内部各行其是，对外只暴露窄接口；接口之间用管道相连；成组的管道可以在阀门室里整体切换。这个意象部分来自 Haskell 的 monadic IO。

从这个主张出发，几条约束是推论而非口味：

• 禁 typeclass。 类型类的前提正是全局一致的约定与自动推断，这与"各小世界自带约定、跨界靠显式接口"直接冲突。所以全程不用。
• 禁 mathlib 及一切外部依赖。 要检验这套组织方式能否独立支撑一座完整的数学建筑，就不能借助一座按相反理念建成的建筑。
• 禁 sorry / admit / 计划外公理。 实验若允许留洞，结论就不可信。

项目分两段。前半程建立并检验这套方法论，后半程用它做一件具体的事：在不引入完整测度论的前提下，把数学分析一的内容尽可能做干净——包括那些通常被认为需要 Lebesgue 理论才能碰的主题。当前版本的数学内容到此为止；多元微积分、级数与含参积分、Fourier 分析属于后续。

规模：593 个模块、299435 行、9729 条定理（公开 7033 + 私有 2696）、3184 个定义、119 个结构。

本节的每一条都能在本仓库里当场验证，命令附在后面的「构建」与「约定」两节。

公理审计不是抽查：它遍历环境中全部名字属于 Tautology 的常量——包括 Lean 为 private 声明生成的 _private.Tautology.… 真名——对每一条调用 Lean.collectAxioms。

阀门室不是命名约定，是真的封起来的。

实数有三套完整且互相独立的构造：Dedekind 分割、Eudoxus 殆同态、Cauchy 序列。每一套各自证到 IsDedekindCompleteOrderedFieldBaseLike，各自是一个自洽的小世界。它们全部位于 Tautology/RealBasic/ModuleBackend/，而这个子树的 65 个文件（全库共 67 个）使用 Lean 4 的 module system，以 module 和 public import 声明，默认不导出。

阀门以上能看见的全部公开面，只有这一个结构：

public structure Selection where
  name : String
  Carrier : Type
  completeField : IsDedekindCompleteOrderedFieldBaseLike Carrier

Dedekind 分割是什么、Eudoxus 殆同态如何定义、Cauchy 序列怎么取商——上层一个符号都够不着。Tautology/RealBasic/ValveRoom.lean 拧上其中一套（当前是 Dedekind），整座上层建筑接的是接口，不是实现。

同样的模式复用在初等函数（RealFunction/Elementary/ValveRoom.lean）和三角函数上。

一个数学对象往往有多种等价的建立方式。本项目把它们分别证出来，画成图，再显式选定一条通路，而不是钦定一种定义了事。

实数完备性是最典型的例子。上确界原理、单调收敛原理、闭区间套原理、Cauchy 完备性，四者之间的蕴涵关系逐条证明在 RealSequence/Principles/From*.lean（九条边——上确界只作源点，另外三个原理之间六条，上确界出发三条），然后 Selected.lean 声明所选路线：

def name : String := "supremum_to_nested_to_monotone_to_cauchy"

紧致性同理：有限子覆盖（Heine–Borel）、勒贝格数、列紧、聚点紧四个原理两两互推，边各自成模块（FiniteToLebesgue、LebesgueToFinite、SeqToAccum、SeqToFinite 等），另有 Lindelöf 以及从上确界与区间套进入该图的入口，散布在 RealCompactness/ClosedInterval/ 下十余个模块。指数与对数有 Euler 极限路线和有理数扩张路线两套，三角函数走几何路线。

每条边都真的证了。 路线不是关于"证明可以怎么走"的注释——所有边都编译通过，切换选定路线是改一个模块的事。

捆绑结构，不是类型类。 实数不是某个固定类型 ℝ，而是任意满足 IsOrderedFieldBaseLike alpha 的载体，该结构作为显式参数 (F : IsOrderedFieldBaseLike alpha) 层层传递。代码中 class 声明 0 个；29 个 instance 全是 Lean 核心记号类（LE、Add、Mul 之类），且全部位于 ModuleBackend/ 之内，阀门以上一个也没有——它们是各后端构造内部的局部便利，从不越界。

ASCII 优先，几乎不用记号。 forall 出现 2984 次而 ∀ 只有 44 次，Exists 4087 次而 ∃ 只有 17 次，-> 10908 次而 → 为 0，ℝ 从未出现。命题写成完全展开的形式：

Exists (fun x : alpha => And (F.le (a n) x) (F.le x (b n)))

内部数系是谓词，不是嵌入。 不定义 ℕ → ℝ 的强制转换，而是定义谓词 InternalNat (x : alpha)、InternalInt、InternalRat，说明载体中的某个元素"是"自然数、整数、有理数。所以"π² 是无理数"的形式化陈述叫 pi_sq_not_internalRat。

证明显式而手工。 没有 mathlib，就没有 linarith、ring、norm_num、field_simp、positivity、aesop——这些战术在本库代码中一次也不曾出现，因为它们根本不存在。实际可用的是 have（20684 次）、exact（13660）、intro（13325）、rw（12661）、unfold（5578）、cases（3511）、refine（2932），加上核心 Lean 的 omega（1752，只管 Nat/Int 线性算术）。simp 只有 583 次，是 have 的 3%。实数上的每一个不等式都得手写。

注释承载名字装不下的东西。 593 个模块每个都有模块头，说明它建立了什么、为什么在依赖序的这个位置、路线上做过什么取舍；声明级 docstring 5648 条。名字仍然很长（riemannIntegrableOn_iff_closedIntervalBounded_and_closedIntervalDiscontinuitySet_null），但名字只能陈述结论，说不了"为什么走这条路"。注释里的模块路径一律写完全限定名（Tautology.RealDerivative.Higher），这样 doc-gen4 生成的文档里它们是可点的链接。

库里没有测度：没有外测度，没有 σ-代数，没有 Lebesgue 积分。代码中带 Lebesgue 的标识符只有三个，都与测度论无关：LebesgueToFinite 与 LebesgueToFiniteSubcover 是紧致性等价图里"勒贝格数 ⟷ 有限子覆盖"那条边，LebesgueCriterion 是 Riemann 可积性的判据，而其中的零测集是下面说的原始概念。

零测集是原始概念，由可数开区间覆盖加长度预算直接定义（RealNegligibility/NullSet.lean），AlmostEverywhere 建在它上面。往上只用两样工具：有界变差函数的性质，和 Henstock–Kurzweil 积分。二者都由初等方法证得。

这样走出来的最远处，是绝对连续版的微积分基本定理：

hkAbsolutelyIntegrableOn_iff_exists_absolutelyContinuousOnClosedInterval_hasDerivativeRepresentativeAE

即"函数 HK 绝对可积，当且仅当它是某个闭区间上绝对连续函数的几乎处处导数"。桥梁是 boundedVariationOn_of_absolutelyContinuousOnClosedInterval。通常这条结果被认为需要 Lebesgue 积分才能陈述和证明。

同一条路上还有：Riemann 可积性的完整 Lebesgue 判据（riemannIntegrableOn_iff_closedIntervalBounded_and_closedIntervalDiscontinuitySet_null）、Hake 定理的双端点形式、Lee–Vyborny 定理（单调函数的斜率例外集零测）、Volterra 函数给出的不可积障碍。

实数构造与基础。 三套后端构造；Dedekind 完备有序域、Archimedes 性质、有理数稠密性、整数部分、上确界工具、Bernoulli 不等式、截断幂级数、Bell 多项式（普通型、指数型、倒幂型）。

序列与完备性。 四大完备性原理及其完整互推图、上下极限、子列、级数、进制展开。

拓扑、紧致性、连通性、基数。 开闭集与闭包代数、Lindelöf、有理数基、子空间；Heine–Borel compact_iff_closed_bounded 及各紧致性刻画的等价；连通集与开集分解、开区间分类；Cantor–Bernstein、可数性、连续统基数 continuumSized、实数不可数。

函数论。 连续、一致连续、单调、凸性、半连续、振荡、单侧极限、无穷极限、有界变差与 Jordan 分解、绝对连续、区间分划（含 gauge、加标分划、加权 Darboux 和）、幂平均不等式、多项式与有理函数。

初等函数与三角函数。 exp、log、任意实指数幂、方根、Euler 数 e；正弦余弦正切及其恒等式与唯一性刻画，经几何路线建立，含 arcsin 与弧长。

微分。 导数代数、链式法则、反函数求导、中值定理、Fermat 与极值、单调性判别、高阶导数、Faà di Bruno 公式（含 Euler 逆、指数型/普通型 Bell 逆）、Taylor 展开（Peano 型与积分型余项、唯一性、jet 与 jet 复合）、L'Hôpital 法则、凸性与二阶导数判别。

积分。 Riemann 积分（Darboux 理论、可积性判据、代数与复合、中值定理含 Bonnet 与 Abel 形式、原函数、反常积分及比较/绝对/Dirichlet–Abel 判敛）；Henstock–Kurzweil 积分（gauge、Henstock 引理、Saks 补全、绝对连续性、零测修改、与 Riemann 的相容性）；Riemann–Stieltjes 积分（单调 Darboux、有界变差积分子、分部积分、换元、阶梯积分子）。

微积分基本定理与换元。 Riemann 与 HK 两套 FTC、Newton–Leibniz 公式、Lebesgue 点形式、广义原函数、分部积分、C¹ 换元与严格单调换元、零测传输。

深入结果。 Weierstrass 多项式逼近定理；Niven 证明的 π² 无理性；Euler–Maclaurin 公式及其推论——Stirling 公式、Wallis 乘积、Euler–Mascheroni 常数 harmonicNumber_sub_log_tendsto_eulerGamma；Cantor 阶梯函数及其图像长度恰为 2（cantorGraph_planeCurveLength_eq_two）。

椭圆积分。 Landen 变换、算术几何平均与完全椭圆积分的关系 completeEllipticK_eq_landenHalfPi_mul_inv_agm；Fagnano 双纽线加法与倍角定律。这部分位于 RealElliptic/，在依赖上处于三角函数之上——它的结果以选定的圆函数陈述（landenHalfPi 即 π/2）。

计数含各区域的伞文件；加上根 Tautology.lean 合计 593。表的排列即区域依赖顺序——区域级依赖图是 DAG，无环，所以这个顺序是良定义的。

RealInterval 是表里唯一没有同名目录的条目：它是索引无关的区间族簿记，只依赖腰部，而消费者分散在 RealFunction、RealIntegral、RealDerivative 三个区。归到其中任何一个，另外两个就得为了普通的区间簿记去依赖那个区，所以它是一个只有一个文件的区域。

选定后端之后的共享 API 分布在三个位置，判据都是依赖方向，不是主题：

• 腰部：RealTheory/ 的 8 个模块（Basic、Order、Abs、NatIntRat、FiniteSum、Density、TruncatedPowerSeries、PointListSet），传递依赖只到 RealBootstrap / RealBasic / Foundation / Nat。
• 分科门面：某学科的 Carrier 特化 API。它能留在 RealTheory/ 当且仅当该学科不反过来依赖 RealTheory——Sequence、Topology、Compactness、Cardinality 满足，故留守；Function、Integral、Elementary 的学科依赖腰部，故各自下放为 RealFunction/Concrete.lean、RealIntegral/Concrete.lean、RealElementary/Concrete.lean。
• 交付层：RealFacade/ 的 16 个模块只被根模块和彼此 import，库内没有任何东西依赖它们（Analysis、Calculus、All、各积分理论入口等）。RealElliptic/ 也自动满足同一条件。

这些声明全部在 namespace RealTheory 下，无论文件在哪个目录——namespace 是稳定的公开名（RealTheory.ClosedInterval 一个就有 1870 处引用），目录表示依赖位置，二者本就不必一致。

按这套判据摆放后，区域级依赖图无环。模块图本来就无环（否则编译不过），但区域粒度无环意味着目录划分本身尊重依赖顺序——读者可以从路径判断抽象层级。

工具链由 lean-toolchain 钉在 leanprover/lean4:v4.30.0，装好 elan 后自动获取。没有外部依赖，无需额外拉包。

lake build                                     # 全量构建
lake build +Tautology.RealTheory.Basic         # 单模块及其依赖
lake env lean Tautology/RealTheory/Basic.lean  # 直接检查单文件，不写缓存
lake clean                                     # 清空构建产物

全量 clean build 595 jobs，产出 593 个 .olean，0 warning、0 error。参考耗时：Intel i9-9980HK 8 核 16 线程上 78 秒墙钟（用户态 577 秒，CPU 959%）。

lake build 只从根模块 Tautology.lean 顺着 import 图走，未被任何模块 import 的文件不会被编译，其中的错误也不会暴露。新增模块必须接入对应的 aggregator（各目录的同名 .lean 文件，或 RealFacade/All.lean 一类），并确认构建 job 数增加。

增量构建会命中缓存并在一秒内返回成功，这不代表源码被重新解析过；要确认改动真的通过编译，用 lake env lean 直接跑该文件，或 lake clean 后全量重来。

文档用 doc-gen4 生成，但不在本仓库进行——它会引入五个传递依赖，那样 lake-manifest.json 里"零依赖"这条可查断言就不再一眼可查。做法是把本仓库克隆一份，在克隆里加一个 docbuild/ 嵌套子工程，用它自己的 lakefile require doc-gen4（钉 v4.30.0，与工具链对应）和本库（path = "../"）。本仓库的 lakefile 一行都不用改。

• 不引入 sorry、admit 或计划外公理。合法公理只有 Lean 核心的 propext、Classical.choice、Quot.sound。
• 不引入 typeclass，不依赖 mathlib 或任何外部库。
• 新模块必须接入正确的 aggregator，确保默认构建实际覆盖。
• 公开 API 的删除、私有化或类型变化，须先做消费者调查并给出兼容决策；仓内零引用不是充分理由。
• 结构调整先审数学路线、先编隔离原型，再决定重写、下沉、移动、合并或拆分。文件大小本身不构成修改理由。
• 注释里提到模块，写完全限定名 Tautology.X.Y；提到别的模块里的名字，要指出它在哪个模块。
• 文本一律 LF（.gitattributes 已设 * text=auto eol=lf）。
• 不提交 .lake/、构建产物、原型、探针、日志或临时备份。

提交前常用检查：

git status --short
git diff --check
grep -rnE '\bsorry\b|\badmit\b|^axiom ' --include='*.lean' Tautology   # 期望无输出
lake build

公理审计写成一个临时探针，用 lake env lean 跑（不要放进仓库）：

import Lean
import Tautology
open Lean

#eval show CoreM Unit from do
  let env ← getEnv
  let allowed : List Name := [`propext, `Classical.choice, `Quot.sound]
  let mut bad := 0
  for (n, ci) in env.constants.toList do
    -- private 声明的真名是 `_private.Tautology.…`，根不是 `Tautology`；
    -- 而且 Lean 把它判为 internal name。两处都不能漏，否则审计会假通过。
    let isPriv := n.getRoot == `_private && (n.toString.splitOn "_private.Tautology.").length > 1
    unless n.getRoot == `Tautology || isPriv do continue
    match ci with
    | .thmInfo _ | .defnInfo _ | .opaqueInfo _ | .axiomInfo _ =>
        if !((← Lean.collectAxioms n).all (allowed.contains ·)) then bad := bad + 1
    | _ => pure ()
  IO.println s!"白名单外的公理：{bad} 条声明"

MIT，见 LICENSE。

• CLAUDE.md — 面向 AI 协作者的工作手册，也是一份准确的架构说明
• PLAN.md / TODO.md / PROGRESS.md — 开发期的范围、状态与踩坑记录。批次关闭后各自清空、只留一行用法说明，历史内容在 Git 历史里