From 1997a2a6852915e765eceb39f88da6907daec00d Mon Sep 17 00:00:00 2001 From: Xinze-Li-Moqian <70414198+Xinze-Li-Moqian@users.noreply.github.com> Date: Sun, 14 Jun 2026 14:53:37 -0400 Subject: [PATCH 1/2] docs: land SmoothManifoldsLee integration ledger on develop PLAN.md (integration workflow, automation pipeline, review allocation) and WORKLIST.md (audit results + live construction ledger) move onto the trunk so the ledger sits with the work. Content from the closed PR #60 docs branch, re-based onto current develop to avoid the stale-base deletions (that branch predated the #65 merge). --- .../2026-06-12-smooth-manifolds-lee/PLAN.md | 67 +++ .../WORKLIST.md | 550 ++++++++++++++++++ 2 files changed, 617 insertions(+) create mode 100644 docs/log/2026-06-12-smooth-manifolds-lee/PLAN.md create mode 100644 docs/log/2026-06-12-smooth-manifolds-lee/WORKLIST.md diff --git a/docs/log/2026-06-12-smooth-manifolds-lee/PLAN.md b/docs/log/2026-06-12-smooth-manifolds-lee/PLAN.md new file mode 100644 index 0000000..4db4bb6 --- /dev/null +++ b/docs/log/2026-06-12-smooth-manifolds-lee/PLAN.md @@ -0,0 +1,67 @@ +# 2026-06-12 · SmoothManifoldsLee 大分支整合方案 + +**事件**：LehengChen 推送 `import/smooth-manifolds-lee`（`a5f308c`）：Lee《Introduction to Smooth Manifolds》Ch1–5 的形式化，346 文件 / 6.2 万行，仅依赖 Mathlib，与 OpenGALib 零依赖零重复。当日全量审计：**187 全新 / 95 Mathlib 重复 / 57 部分重复；52 个高价值文件**。明细与施工台账见同目录 `WORKLIST.md`。 + +## 问题 + +这批材料是**教材序的形式化**：一个编号一个文件、import 图与章节耦合、设施代码（图卡操作、截断函数、实例打包）散落在各章定理脚下随用随造。我们要的是**高复用、可维护、可延伸的软件**：声明按数学对象组织、设施沉淀为共用层、上层只 import 设施而不知道教材的存在。 + +所以要回答的是：**教材序形式化 → 软件库的转化怎么做，并且做成可重复的流程**——这不会是最后一次有人带着一整本书的形式化来敲门。 + +## 分支与流程 + +``` +import/ 冻结参考快照（只读，永不 merge，staging/ 不进主干） + ↓ 人工/AI 移植，非 git merge +port/<工单> 短命施工分支，一单一支，从 develop 切出 + ↓ PR + CI + review +develop → main 现有惯例不变 +``` + +- import 分支永不合并：外来约定不进历史，且审计结论只对锚定的快照 commit 有效。上游再有新货推 `import/-v2`，diff 出增量、只重审增量，不 force-push。 +- 每个 port PR 的质量门：命名空间已换、落点符合布局、**零 sorry**、提交前**全量 `lake build`**、模块 docstring 带出处行（`Ported from ()`）、linter 基线无新增违例。 +- 领单即在 `WORKLIST.md` 台账改状态，台账改动随移植 PR 同行；不碰别人 in-progress 的单。 +- 全部移植完：参考分支打 tag 归档后删除，台账存档作为出处记录。 + +## 自动化流水线（设想，待试点） + +9 张施工单是同构单元，每单走同一循环，自动化程度由试点数据决定： + +``` +领单 → ① 通用层判定（AI 输出 复用/扩展/新建 决策表，必须附 grep 证据） + → ② 移植（AI：换命名空间、重组、每条声明补 Math./Eng. 双 docstring） + → ③ 机器门（CI：全量构建、零 sorry、linter、命名与出处检查） + → ④ 自动开 PR（附决策表与台账 diff） + → ⑤ 人审（只审两项，见下节） +``` + +两条**常驻约束**写进 AI 任务模板，不靠口头提醒： + +1. **通用层优先**：未回答"主分支是否已有同型设施"之前不许写代码。本次审计已验证必要性——两边各写了同一组设施的一半（图卡演算、截断函数、打包类）。 +2. **语义符合**：每条声明带 Math./Eng. 双 docstring（范例 `Riemannian/TangentBundle/TangentSmooth.lean`）。存在性 linter 把守，忠实性人审把守。 + +自动化终点是 PR，不是 develop。人始终是合并守门员。 + +## 人的部分：评审怎么分配 + +依据最小可信基（minimal trusted base）：Lean 内核已检查全部证明，**证明不用人审**；但定义错了，内核会让我们证明几千行关于错误对象的真命题。人审对象收缩为**定义与陈述**，其中定义错误废整个下游依赖锥，定理陈述错误只废自己。 + +1. **核心节点清单**：依赖图入度高的 `def`/`class`/`structure` 入选（实测承重墙：`IsEmbeddedSubmanifold` 被引 18 次、`TopologicalManifold` 17 次），人工增补语义微妙者；`theorem` 一般不入选。 +2. **CODEOWNERS**：核心节点文件映射到数学专家，无 owner 批准不能合并（GitHub 机制强制）。 +3. **专家只审两件事**：Math. docstring 与陈述是否同一数学对象；核心定义的实例化测试是否非空洞（example 进 `Tests/`，如"球面是 `IsEmbeddedSubmanifold`"，堵"假设不可满足、空洞为真"）。 +4. 非核心节点：AI 审 + 抽查。 + +一句话：内核消灭了证明审查，剩余负担集中在可信基，可信基里承重的是依赖图枢纽——枢纽钉给专家，用最少的专家时间买全局正确性。 + +## 待团队决定 + +- [ ] 三个新 linter（docstring 对、命名空间白名单、出处行）进 `OpenGALib/Util/Linter/`？ +- [ ] 核心节点入度阈值（建议 ≥ 5，首版清单随工单 #1 提交） +- [ ] CODEOWNERS 映射：流形地基 / 子流形与切片 / 带边与几何测度论接口各归谁 +- [ ] 自动开 PR 触发方式：本地脚本 / GitHub Action / 定时 agent +- [ ] 人审时限（建议核心节点 PR 三个工作日内响应） + +**试点**：工单 #1（`port/manifold-typeclass-core`）半手工走完整循环，校准模板与 linter；按返工率和人审发现数决定 #2–9 的自动化深度。 + +--- +关联：PR #60 · `import/smooth-manifolds-lee`（`a5f308c`） diff --git a/docs/log/2026-06-12-smooth-manifolds-lee/WORKLIST.md b/docs/log/2026-06-12-smooth-manifolds-lee/WORKLIST.md new file mode 100644 index 0000000..e61fa90 --- /dev/null +++ b/docs/log/2026-06-12-smooth-manifolds-lee/WORKLIST.md @@ -0,0 +1,550 @@ +# SmoothManifoldsLee 整合工单 + +来源：分支 `import/smooth-manifolds-lee`（commit `a5f308c`，LehengChen，2026-06-12），内容为 Lee《Introduction to Smooth Manifolds》第 1–5 章的 Lean 4 形式化，自包含、仅依赖 Mathlib（v4.30.0），与 OpenGALib 现状零依赖关系。 + +本工单由 2026-06-12 的全量重叠审计产出：40+ 个并行 agent 逐文件对照 Mathlib（`.lake/packages/mathlib`）与 OpenGALib 判重、定级、给出落点建议。审计覆盖全部 346 个章节文件（339 个批量审计 + 7 个深层子目录文件补审）。 + +## 总体统计 + +| 维度 | 分布 | +|---|---| +| 重叠分类 | new 187 · mathlib-dup 95 · partial-dup 57 | +| 移植价值 | high 52 · medium 101 · low 186 | +| 含 sorry 文件 | 106 | + +约 28% 的文件实质重复 Mathlib（多为带教材编号的包装/复述），直接跳过；187 个全新文件是移植主体。 + +## 整合原则 + +1. **按目标模块移植，不按章节顺序**。教材组织（`ChapNN/SecNN_MM/`）不进主库；声明按数学对象重组进领域模块。 +2. **声明名基本可保留**（已是 Mathlib 风格描述性命名），命名空间按我们的**域命名空间惯例**（域名=目录名，对照 `Riemannian`/`Tensor`/`GeometricMeasureTheory`）——对流形域这恰好就是 `namespace Manifold`，与 Mathlib 共享根命名空间和我们扩展 `TangentBundle`/`ContinuousLinearMap` 一致，**不需另起**。文件结构按 `../../NAMING_CONVENTION.md` 重排。 + - **注释 house style（合并 #65 时确立）**：锚文件（`Util/` 之外）只用单 `**Math.**` 标签——`AnchorPurity` linter 禁 `**Eng.**`/`**Mixed.**`，工程细节省掉或挪进 `Util/`；模块注释按架构分层叙事（非教材顺序）；出处压成一行 `Provenance:` 脚注。范本见 develop 上 `OpenGALib/Manifold/Charts/CoordinateBall.lean`（db767b1）。PLAN 早先写的"Math./Eng. 双 docstring"是误读，已废。 + - **def 命名仍须 lowerCamelCase**（`NAMING_CONVENTION.md` 第 42 行）：staged 源的 snake_case（如 `curve_velocity`、`chart_coordinate_vectors_basis`）移植时要改名。 +3. **打包类收编进现有体系**：`TopologicalManifold n M` 等类只是 Mathlib 实例（T2 + 第二可数 + `ChartedSpace`）的打包，与我们已有的 `SmoothManifold M` 打包类（`Riemannian/Manifold/SmoothManifold.lean`）是同一设计模式。移植时统一收编进我们的打包类体系，不引入第二套；维数显式化（`n` 参数）是否保留在收编时定夺。 + - 与 OpenGALib 的重叠：全量审计为 0 个 `opengalib-dup`——我们库直接踩在 Mathlib 流形机器上做度量层以上的内容，Lee 覆盖的子流形/浸入/坐标球层我们完全没有。唯一接口接触点：`GeometricMeasureTheory/Varifold.lean` 的 `LocalSmoothEmbeddingWitness` 临时证人结构，嵌入子流形理论移植后应垫到其下并替换之。 +4. **sorry 不进主干**：含 sorry 的文件要么先补证明，要么陈述层有 sorry 的（如 Chap04 的 `rankAt`/`HasConstantRank`）整段推迟。 +5. **落点归一化**：下文 agent 建议的 targetModule 路径风格不一（`Riemannian/Manifold/…`、`Riemannian/Submanifold/…` 等），施工时统一收敛到一个顶层流形域（待定名，候选 `OpenGALib/SmoothManifold/`），垫在 `Riemannian` 与 `GeometricMeasureTheory` 之下。 +6. 工具链先升级：staged 代码用 Lean v4.30.0 正式版，我们在 rc2，第一批移植前对齐。 + +## 共用抽象设施层 + +两边各自实现了同一组设施的两半（我们：度量/测度面向；他们：拓扑/嵌入面向）。合并时以下五层作为共用模块进主分支，两边上层各自 import： + +| 设施层 | OpenGALib 已有 | staged 分支提供 | 备注 | +|---|---|---|---| +| 流形打包类 | `SmoothManifold M`、`RiemannianManifold M` | `TopologicalManifold n M`、`SmoothManifoldWithBoundary n M` | 收编为一条谱系；**带边支持是我们的空白，且是 GMT 散度定理的前提** | +| 图卡演算 | `Riemannian/Volume/Util/ChartOverlap.lean`、`ChartTransition.lean` | 坐标球、居中图卡、预紧坐标球、欧氏切片坐标 | 同源设施各写一半，应独立成共用 `Charts` 模块，从 `Volume/Util/` 迁出 | +| 截断/单位分解 | `Riemannian/Manifold/BumpFunction.lean` | 环形截断、单位分解存在性、穷竭函数 | 都在包装同批 Mathlib 原语，合并为一个平滑化模块 | +| 切丛局部化 | `Riemannian/TangentBundle/TangentSmooth.lean`（`trivAt` 判据） | 切丛平凡化、点导子、曲线速度 | 跟施工顺序第 4 站走 | +| 子流形抽象 | `Varifold.lean` 的 `LocalSmoothEmbeddingWitness`（临时证人） | `IsEmbeddedSubmanifold` + 切片图卡理论 | 跟施工顺序第 2 站走，移植后替换证人结构 | + +设施层 1–3 小、基本无 sorry、两边消费者均已存在，适合作为第一批合并内容，priority 高于按章节移植。 + +## 施工台账 + +流程见 `PLAN.md`（领单改状态、一单一 `port/` 分支、质量门、销单）。施工单按依赖序排列；标注"可并行"的单之间无依赖。 + +| # | 施工单 | 内容 | 依赖 | 状态 | +|---|---|---|---|---| +| 1 | `port/manifold-typeclass-core` | 设施层 1：打包类谱系合并（`TopologicalManifold n M`、带边流形类收编进 `SmoothManifold M` 谱系；Chap01 Sec01/Sec01_06） | — | todo | +| 2 | `port/charts` | 设施层 2：图卡演算共用模块（坐标球、居中图卡 + 现有 `ChartOverlap`/`ChartTransition` 迁出合并） | #1 | todo | +| 3 | `port/cutoffs` | 设施层 3：截断/单位分解/穷竭函数并入 `BumpFunction` 体系（Chap02 Sec02_10/11 高价值条目） | #1 | todo（与 #2 可并行） | +| 4 | `port/embedded-submanifold` | 设施层 5 上半：`IsEmbeddedSubmanifold` + 图论式子流形 API（Chap05 Sec05_28） | #2 | todo | +| 5 | `port/slice-charts` | 设施层 5 下半：切片定理基础设施（`Theorem_5_8/` 全家 + Sec05_29） | #4 | todo | +| 6 | `port/submersion-covering` | 浸没/浸入/覆盖映射（Chap04 Sec04_25/26 高价值簇） | #2 | todo（与 #4–5 可并行） | +| 7 | `port/tangent-localization` | 设施层 4：切丛局部化（平凡化、点导子、曲线速度；Chap03 高价值条目） | #1 | todo（与 #2–6 可并行） | +| 8 | `port/varifold-witness-swap` | `LocalSmoothEmbeddingWitness` 替换为子流形理论 | #5 | todo | +| 9 | （按需）medium 条目 | 见各章节"可考虑"表 | 视条目 | backlog | + +前置事项（不占施工单）：工具链对齐 v4.30.0 正式版。 + +### 实际 PR 波次（2026-06-14，LehengChen） + +LehengChen 自行做了更细的分解（栈式 PR，不完全对应上表）。实际状态以此为准： + +| PR | 分支 | 内容 | 状态 | +|---|---|---|---| +| #65 | `port/coordinate-ball` | 坐标球图卡谓词 | **已合并 develop**（注释经 house-style 修订 db767b1，作为范本） | +| #66 | `port/precompact-basis` | 预紧坐标球可数基 + 局部有限加细 | open，待反馈：base 改 develop、注释回炉 | +| #67 | `port/charted-space-core` | 由图册核造流形 | open，同上 | +| #68 | `port/exhaustion-cutoff` | 穷竭函数 + 局部光滑 + 单位分解⇒仿紧 | open，同上 | +| #69 | `port/curve-velocity-mfderiv` | 曲线速度 + mfderiv（含 snake_case def 待改名） | open，同上 | +| #70 | `port/coordinate-components` | 坐标切向量分量（含 snake_case def；内联了 `tangent_coordinates_change`） | open，同上 | + +反馈共性（指向已合并的 #65 为范本）：①注释 house style（单 Math 标签 / 架构叙事 / 出处脚注）；②定理的 Eng 行勿复述证明；③snake_case def 改 lowerCamelCase；④#65 合并后 base 重定向 develop。 + +## 补审：深层子目录文件（批量审计遗漏，已补） + +| 文件 | 主要声明 | 分类 | 价值 | sorry | 理由 | +|------|----------|------|------|-------|------| +| Chap05/Sec05_29/Theorem_5_8/Common.lean | euclidean_slice_projection 等 27 条 | new | high | 否 | 欧氏切片几何与图卡居中基础设施 | +| Chap05/Sec05_29/Theorem_5_8/Index.lean | 重导出 | new | medium | 否 | 索引文件 | +| Chap05/Sec05_29/Theorem_5_8/LocalNormalFormAPI.lean | rank_normal_form 等 | partial-dup | medium | 否 | 包装 Mathlib 浸入正规形式，桥接第 4 章秩形式 | +| Chap05/Sec05_29/Theorem_5_8/LocalSliceAtlas.lean | slice_condition_chartAt 等 30+ 条 | new | high | 否 | 切片条件图册构造核心 | +| Chap05/Sec05_29/Theorem_5_8/LocalSliceImmersion.lean | local_slice_condition_has_embedded_submanifold_structure 等 11 条 | new | high | 否 | 切片上嵌入子流形结构的完成步 | +| Chap05/Sec05_36/Theorem_5_51/EuclideanHalfSlice.lean | euclidean_half_slice_projection_partial_homeomorph | new | medium | 是 | 半切片边界图卡的半成品 | +| Chap05/Sec05_36/Theorem_5_51/Index.lean | 重导出 | new | low | 是 | 下游未实现 | + +--- + +# Chap01 + +## 移植优先（high，10 项） + +| 文件 | 声明 | 分类 | 落点 | sorry | 理由 | +|---|---|---|---|---|---| +| Sec01/Definition_1_extra_2.lean | IsCoordinateBall, centerAt 等 | new | Manifold/Charts | 否 | 坐标球/盒卡形谓词，Mathlib 缺，坐标球栈基础 | +| Sec01/Example_1_5.lean | RealProjectiveSpace, realProjectiveChart 等 | new | Instances/ProjectiveSpace | 否 | RP^n 商拓扑与标准仿射卡，Mathlib 完全缺失 | +| Sec01/Example_1_8.lean | contDiffGroupoid_pi, instIsManifoldPi 等 | new | Instances/Pi | 否 | 有限乘积 IsManifold 实例，补 Mathlib 已注明缺口 | +| Sec01/Lemma_1_10.lean | isTopologicalBasis_isPrecompactCoordinateBall 等 | new | Manifold/Charts | 否 | 预紧坐标球可数基，单位分解/穷竭列底层 | +| Sec01_03/Definition_1_3_extra_1.lean | IsSmoothCoordinateBall, IsRegularCoordinateBall 等 | new | Manifold/CoordinateBall | 否 | 光滑/正则坐标球谓词全证，需脱离项目内依赖 | +| Sec01_04/Example_1_32.lean | regular_level_set_smooth_structure 等 | new | Manifold/RegularLevelSet | 否 | 正则水平集定理 1750 行全证，Mathlib 无正则值定理 | +| Sec01_04/Lemma_1_35.lean | ChartedSpaceCore.toTopologicalSpace_t2Space, toChartedSpace_isManifold 等 | new | Manifold/ChartedSpaceCore | 否 | 由图册造流形的 T2/二可数/光滑判据，Mathlib 缺 | +| Sec01_06/Exercise_1_42.lean | IsRegularCoordinateHalfBall 等 | new | Manifold/CoordinateBalls | 是 | 正则坐标(半)球可数基，三定理全 sorry | +| Sec01_07/Problem_1_9.lean | ComplexProjectiveSpace, complexProjectiveSpaceIsManifold 等 | new | Instances/ComplexProjectiveSpace | 否 | CP^n 完整流形结构无 sorry，Fubini-Study 宿主 | +| Sec01_05/Proposition_1_40.lean | IsBoundaryModelCoordinateBall, countable_fundamentalGroup 等 | partial-dup | Manifold/CoordinateBall | 是 | 半球基与可数基本群为缺口，拓扑推论 Mathlib 已有，全 sorry | + +
可考虑（medium，21 项） + +| 文件 | 声明 | 分类 | 落点 | sorry | 理由 | +|---|---|---|---|---|---| +| Sec01/Exercise_1_1.lean | HasCoordinateBallCharts 等 | new | Manifold/Charts | 否 | 卡收缩/拉直引理完整，存在式陈述需重构 | +| Sec01/Exercise_1_6.lean | realProjectiveSpace_t2Space 等 | new | Instances/ProjectiveSpace | 是 | 补 Example_1_5 所需 T2/二可数，四条全 sorry | +| Sec01/Exercise_1_7.lean | realProjectiveSpaceCompactSpace | new | Instances/ProjectiveSpace | 否 | RP^n 紧性全证，宜随 Example_1_5 一并移植 | +| Sec01_03/Proposition_1_19.lean | exists_countable_regular_coordinate_ball_basis 等 | new | Manifold/CoordinateBall | 是 | 正则坐标球可数基有用，证明 sorry 且打包需重构 | +| Sec01_04/Example_1_30.lean | graph_coordinate_chart, graph_charted_space 等 | new | Manifold/GraphChart | 是 | 光滑映射图卡空间为缺口，关键引理 sorry | +| Sec01_04/Example_1_33.lean | realProjectiveSpaceIsManifold, realProjectiveChartTransitionDiffeomorph 等 | new | Instances/RealProjectiveSpace | 否 | ℝPⁿ 光滑结构全证，需先移上游 Example_1_5 | +| Sec01_06/Definition_1_6_extra_1.lean | contMDiffOn_halfSpace_iff_forall_exists_smoothAmbientExtension 等 | new | Manifold/HalfSpaceExtension | 是 | 半空间环境延拓光滑判据，关键边界引理 sorry | +| Sec01_06/Definition_1_6_extra_3.lean | IsSmoothCoordinateHalfBall 等 | new | Manifold/CoordinateBalls | 是 | 与 Exercise_1_42 定义重叠，需先合并 API | +| Sec01_07/Problem_1_10.lean | problem_1_10_chart_matrix, block_column_subspace 等 | new | GeometricMeasureTheory/Grassmannian/Charts | 是 | Grassmann 矩阵坐标可喂 varifold，主定理全 sorry | +| Sec01_07/Problem_1_11.lean | closed_unit_ball_smoothManifoldWithBoundary 等 | new | SmoothManifold/ClosedBall | 是 | 闭球带边流形补缺口，关键定理 sorry，图册取自 Problem_2_4 | +| Sec01_07/Problem_1_5.lean | sigmaCompactSpace_of_connected_paracompact_locallyCompact_t2 等 | new | Manifold/Paracompactness | 否 | 仿紧⇒σ紧逆向及二可数刻画，Mathlib 仅有正向 | +| Sec01_07/Problem_1_6.lean | supportedRadialTwistHomeomorph, exists_uncountably_many_distinct_smooth_structures 等 | new | Manifold/SmoothStructures | 否 | 不可数多光滑结构全证，多为单定理脚手架 | +| Sec01/Definition_1_extra_1.lean | TopologicalManifold, dimension_eq 等 | partial-dup | Manifold/TopologicalManifold | 是 | C⁰流形打包类，多为包装且维数不变 sorry | +| Sec01/Example_1_3.lean | graphMap, graph_coordinates 等 | partial-dup | Manifold/Charts | 否 | 打包同胚 graphOn≃ₜU 为 Mathlib 缺，GMT 图参数化常用 | +| Sec01/Theorem_1_15.lean | exists_countable_locallyFinite_refinement_of_isTopologicalBasis 等 | partial-dup | Manifold/Charts | 否 | 预紧坐标球可数局部有限加细，喂单位分解 | +| Sec01_02/Definition_1_2_extra_3.lean | IsSmoothAtlas 等 | partial-dup | SmoothManifold/Atlas | 否 | 不依实例的图册谓词为新，属小众脚手架 | +| Sec01_02/Proposition_1_17.lean | same_smooth_structure_iff_union_is_smooth_atlas 等 | partial-dup | SmoothManifold/Atlas | 否 | 并集判同光滑结构为新，letI 陈述需重构 | +| Sec01_04/Example_1_36.lean | grassmannian, grassmannian.chart_equiv 等 | partial-dup | Instances/Grassmannian | 是 | Grassmann 卡双射缺口，非平凡引理全 sorry | +| Sec01_05/Proposition_1_38.lean | boundaryChart, boundaryTopologicalManifold 等 | partial-dup | Manifold/InteriorBoundary | 是 | 边界作(n-1)流形构造，近全 sorry 且绑定专有模型 | +| Sec01_06/Exercise_1_44.lean | ModelWithCorners.interiorOpens 等 | partial-dup | Manifold/InteriorBoundary | 否 | 内部为无边开子流形等小引理，补全边界设施 | +| Sec01_06/Theorem_1_46.lean | isInteriorPoint_iff_of_mem_maximalAtlas 等 | partial-dup | Manifold/InteriorBoundary | 否 | 边界检测推广到极大图册卡，全证 | + +
+ +
跳过（44 项，绝大多数为 Mathlib 包装/recall 文件） + +- Sec01/Definition_1_extra_3.lean — mathlib-dup — 纯 recall 类型类 +- Sec01/Definition_1_extra_4.lean — mathlib-dup — recall 加薄包装 +- Sec01/Example_1_4.lean — mathlib-dup — 球面实例一行复包 +- Sec01/Example_1_9.lean — new — 平凡 abbrev +- Sec01/Exercise_1_14.lean — mathlib-dup — 纯 recall +- Sec01/Lemma_1_13.lean — mathlib-dup — 与 Exercise_1_14 重复 +- Sec01/Proposition_1_11.lean — partial-dup — recall 加实例装配 +- Sec01/Proposition_1_12.lean — mathlib-dup — 纯 recall 包装 +- Sec01/Proposition_1_16.lean — new — 一行 simpa 引 1.40 +- Sec01/Theorem_1_2.lean — new — recall 项目 sorry 定理 +- Sec01_02/Definition_1_2_extra_1.lean — mathlib-dup — #check 指针 +- Sec01_02/Definition_1_2_extra_2.lean — partial-dup — 两行包装 +- Sec01_02/Definition_1_2_extra_4.lean — mathlib-dup — recall 指针 +- Sec01_02/Definition_1_2_extra_5.lean — mathlib-dup — rfl 即得且 sorry +- Sec01_02/Exercise_1_18.lean — mathlib-dup — 零声明指针 +- Sec01_02/Remark_1_2_extra_6.lean — mathlib-dup — recall 指针 +- Sec01_03/Exercise_1_20.lean — new — 复述 1.19 无新声明 +- Sec01_03/Notation_1_3_extra_2.lean — mathlib-dup — extChartAt recall +- Sec01_04/Example_1_21.lean — partial-dup — 离散流形薄装配 +- Sec01_04/Example_1_22.lean — mathlib-dup — sorry 复述实例 +- Sec01_04/Example_1_23.lean — new — 一次性反例无 API +- Sec01_04/Example_1_24.lean — mathlib-dup — 薄组合/#check +- Sec01_04/Example_1_25.lean — mathlib-dup — 一行推论加 #check +- Sec01_04/Example_1_26.lean — mathlib-dup — 纯 #check +- Sec01_04/Example_1_27.lean — mathlib-dup — #check 加 sorry 辅理 +- Sec01_04/Example_1_28.lean — partial-dup — 关键开性 sorry +- Sec01_04/Example_1_29.lean — mathlib-dup — 两步推论 +- Sec01_04/Example_1_31.lean — mathlib-dup — 球面实例 #check +- Sec01_04/Example_1_34.lean — mathlib-dup — 复述乘积实例 +- Sec01_04/Notation_1_4_extra_1.lean — mathlib-dup — 记号对照 #check +- Sec01_05/Definition_1_5_extra_1.lean — partial-dup — 半空间模型笨拙打包 +- Sec01_05/Exercise_1_39.lean — mathlib-dup — 零声明 #check +- Sec01_05/Exercise_1_41.lean — partial-dup — 纯指针文件 +- Sec01_05/Theorem_1_37.lean — mathlib-dup — 单条 recall +- Sec01_06/Definition_1_6_extra_2.lean — mathlib-dup — 类复包 Mathlib +- Sec01_06/Exercise_1_43.lean — mathlib-dup — 零声明 #check +- Sec01_06/Proposition_1_45.lean — mathlib-dup — 纯 recall +- Sec01_07/Problem_1_1.lean — new — 双原点反例无 API +- Sec01_07/Problem_1_12.lean — mathlib-dup — infer_instance 直调 +- Sec01_07/Problem_1_2.lean — partial-dup — 习题级薄组合 +- Sec01_07/Problem_1_3.lean — mathlib-dup — 双向薄包装 +- Sec01_07/Problem_1_4.lean — new — 近平凡引理加反例 +- Sec01_07/Problem_1_7.lean — mathlib-dup — 重造球极图册多 sorry +- Sec01_07/Problem_1_8.lean — partial-dup — 圆专用习题 + +
+ +## 小结 + +第一章共审计 75 个文件，约六成是对 Mathlib 既有结果的 recall、#check 或薄封装，可直接跳过。真正值得移植的核心资产集中在两条线：一是坐标球/覆盖基础设施（坐标球谓词、预紧坐标球可数基、正则坐标(半)球），它们是单位分解、穷竭列与 GMT 覆盖论证的底层；二是实例级缺口（RP^n、CP^n 的完整流形结构、有限乘积 IsManifold 实例、正则水平集定理、ChartedSpaceCore 构造引理），均为 Mathlib 公认空白且大多 sorry-free。中等价值条目多数受 sorry 残留或项目内部依赖（TopologicalManifold 类、LeeBoundaryModelSpace）牵制，移植前需先做 API 重构与依赖消解。 + +--- + +# Chap02 + +## 移植优先（high，4 项） + +| 文件 | 声明 | 分类 | 落点 | sorry | 理由 | +|---|---|---|---|---|---| +| Sec02_12/Problem_2_4.lean | closed_unit_ball_fixed_atlas, split_at_coordinate 等 | new | Instances/ClosedBall | 否 | 闭球带边流形 2600 行无 sorry，直撑 GMT 散度定理 | +| Sec02_11/Proposition_2_28.lean | exists_positive_smooth_exhaustion_function | new | Manifold/Exhaustion | 否 | 正光滑穷竭函数全证，非紧 L²/Bochner/GMT 所需 | +| Sec02_09/Example_2_14.lean | unitOpenBallDiffeomorph, smoothChartDiffeomorph 等 | partial-dup | Manifold/Diffeomorph | 否 | 打包单位球≃ℝⁿ与卡微分同胚，Mathlib 仅散装引理 | +| Sec02_09/Proposition_2_15.lean | Diffeomorph.pi, Diffeomorph.restrictOpen 等 | partial-dup | Manifold/Diffeomorph | 是 | 乘积与开子流形限制 API 为缺口，六条辅理 sorry | + +
可考虑（medium，14 项） + +| 文件 | 声明 | 分类 | 落点 | sorry | 理由 | +|---|---|---|---|---|---| +| Sec02_09/Theorem_2_17.lean | Diffeomorph.dimension_eq 等 | new | Manifold/Diffeomorph | 否 | 微分同胚维数不变全证，Mathlib 缺此通用引理 | +| Sec02_11/Definition_2_11_extra_2.lean | Function.IsSmoothOn 等 | new | Manifold/SmoothExtension | 否 | 子类型域局部延拓光滑谓词，需对齐 ContMDiffOn | +| Sec02_11/Definition_2_11_extra_3.lean | Function.IsExhaustionFunction 等 | new | Manifold/Exhaustion | 否 | 穷竭函数类与 proper 引理，2.28 的 API 基础 | +| Sec02_11/Lemma_2_26.lean | exists_supported_contMDiffMap_extension_of_isClosed | new | Manifold/SmoothExtension | 是 | 闭集光滑延拓为真缺口，仅有陈述需从头证 | +| Sec02_12/Problem_2_10.lean | smooth_iff_pullback_preserves_smooth_real_functions 等 | new | Manifold/SmoothFunctionCriterion | 是 | 回拉保光滑函数判据有用，定理全 sorry | +| Sec02_12/Problem_2_11.lean | Projectivization.basisMap, BasisCompatible 等 | new | Instances/Projectivization | 是 | Projectivization 结构搬运层，关键证明 sorry 且依赖一章 | +| Sec02_12/Problem_2_13.lean | paracompactSpace_of_hasSubordinatePartitionOfUnity | new | Manifold/PartitionOfUnity | 否 | 单位分解⇒仿紧逆向全证，Mathlib 仅有正向 | +| Sec02_12/Problem_2_6.lean | projectivizationMap, contMDiff_projectivizationMap 等 | new | Manifolds/ProjectiveSpace | 否 | 齐次映射下降到 ℝPⁿ 为新，需先移项目图册 | +| Sec02_12/Problem_2_7.lean | smooth_functions_not_finiteDimensional 等 | new | Util/SmoothFunctionSpace | 否 | C^∞(M,ℝ) 无限维全证，于本库方向偏小众 | +| Sec02_08/Corollary_2_8.lean | gluing_lemma_for_smooth_maps | partial-dup | Manifold/SmoothManifold | 否 | 光滑层粘合解包为 ContMDiff 级可用陈述 | +| Sec02_08/Exercise_2_2.lean | contMDiff_open_submanifold_halfspace_iff_forall_exists_smoothAmbientExtension 等 | partial-dup | Manifold/Boundary | 否 | 半空间延拓判据真缺，需连带一章依赖文件 | +| Sec02_09/Theorem_2_18.lean | Diffeomorph.restrictInterior 等 | partial-dup | Manifold/Diffeomorph | 是 | 限制到流形内部为新，依项目内设施且 simp 引理 sorry | +| Sec02_11/Proposition_2_25.lean | exists_smooth_bump_function_for | partial-dup | Manifold/BumpFunction | 否 | 严格 tsupport⊆U 闭集 bump，可扩展本库模块 | +| Sec02_12/Problem_2_3.lean | hopf_map, hopf_map_smooth 等 | partial-dup | Instances/HopfFibration | 是 | Hopf 映射 S³→S² 为新典型例，五条证明全 sorry | + +
+ +
跳过（40 项，绝大多数为 Mathlib 包装/recall 文件） + +- Sec02_08/Definition_2_8_extra_2.lean — mathlib-dup — 纯 #check 复述 +- Sec02_08/Definition_2_8_extra_4.lean — mathlib-dup — 薄逐点推论 +- Sec02_08/Definition_2_8_extra_5.lean — mathlib-dup — recall 编号对照 +- Sec02_08/Definition_2_8_extra_6.lean — partial-dup — 既有 API 已覆盖 +- Sec02_08/Exercise_2_1.lean — mathlib-dup — 仅 #check 环结构 +- Sec02_08/Exercise_2_11.lean — mathlib-dup — 三条 recall +- Sec02_08/Exercise_2_3.lean — mathlib-dup — 两行包装 +- Sec02_08/Exercise_2_7.lean — mathlib-dup — 纯 recall 交叉引用 +- Sec02_08/Exercise_2_9.lean — mathlib-dup — 四行包装 +- Sec02_08/Notation_2_8_extra_3.lean — mathlib-dup — 记号对照 #check +- Sec02_08/Proposition_2_10.lean — mathlib-dup — 四条 #check +- Sec02_08/Proposition_2_4.lean — mathlib-dup — 单条 #check +- Sec02_08/Proposition_2_5.lean — mathlib-dup — 单条 #check +- Sec02_08/Proposition_2_6.lean — mathlib-dup — 两条 #check +- Sec02_08/Remark_2_8_extra_1.lean — new — 术语谓词无数学内容 +- Sec02_08/Remark_2_8_extra_7.lean — mathlib-dup — 零声明词汇复述 +- Sec02_09/Definition_2_9_extra_1.lean — mathlib-dup — 纯 #check +- Sec02_09/Exercise_2_16.lean — partial-dup — recall 脚手架 +- Sec02_09/Exercise_2_19.lean — partial-dup — recall 脚手架 +- Sec02_10/Definition_2_10_extra_1.lean — mathlib-dup — 文档加单 #check +- Sec02_10/Definition_2_10_extra_2.lean — mathlib-dup — 本库已有包装 +- Sec02_10/Definition_2_10_extra_3.lean — mathlib-dup — 定义 recall +- Sec02_10/Definition_2_10_extra_4.lean — mathlib-dup — 定义 recall +- Sec02_10/Exercise_2_24.lean — mathlib-dup — #check 特化 +- Sec02_10/Lemma_2_20.lean — mathlib-dup — recall 指针 +- Sec02_10/Lemma_2_21.lean — partial-dup — smoothStep 已覆盖 +- Sec02_10/Lemma_2_22.lean — partial-dup — ContDiffBump 已供 +- Sec02_10/Theorem_2_23.lean — mathlib-dup — sorry 复述 +- Sec02_11/Definition_2_11_extra_1.lean — new — 平凡常函数检查 +- Sec02_11/Exercise_2_27.lean — new — 教学反例 +- Sec02_11/Theorem_2_29.lean — mathlib-dup — 六行特化包装 +- Sec02_12/Problem_2_1.lean — new — 教学反例无 API +- Sec02_12/Problem_2_12.lean — new — 主定理单 sorry +- Sec02_12/Problem_2_14.lean — mathlib-dup — 字面 recall +- Sec02_12/Problem_2_5.lean — new — 教材特定含两 sorry +- Sec02_12/Problem_2_8.lean — new — 依赖未移植图册 +- Sec02_12/Problem_2_9.lean — new — 教材特定大量辅件 +- Sec02_12/Problem_2_9_corecheck.lean — new — 流水线快照 +- Sec02_12/Problem_2_9_pre_north.lean — new — 流水线快照 +- Sec02_12/Problem_2_9_prefixcheck.lean — new — 流水线快照 + +
+ +## 小结 + +第二章共审计 55 个文件，其中大部分（约 40 个）是对 Mathlib 既有 ContMDiff / 光滑函数 / 单位分解 API 的 #check 或 recall 式复述，可直接跳过。真正值得移植的核心资产集中在两条线：一是 Diffeomorph 基础设施（乘积、开子流形限制、维数不变性、单位球与图卡的打包微分同胚），二是闭球带边流形构造（Problem 2.4，2600 行无 sorry）与正光滑穷竭函数（Proposition 2.28），后两者直接支撑 GMT 散度定理与非紧 L²/Bochner 方向的缺口。中等价值项多数围绕光滑延拓、投影空间结构与回拉判据，部分仍含 sorry，宜在对应目标模块成型后按依赖顺序择机引入。 + +--- + +# Chap03 + +## 移植优先（high，4 项） + +| 文件 | 声明 | 分类 | 落点 | sorry | 理由 | +|---|---|---|---|---|---| +| Sec03_14/Proposition_3_9.lean | mfderiv_open_subset_inclusion_isInvertible | new | Util/Tangent | 否 | 开子集包含微分可逆全证，Mathlib 缺此切空间识别 API | +| Sec03_17/Proposition_3_23.lean | exists_smooth_curve_with_velocity, exists_smooth_curve_with_velocity_boundaryless 等 | new | CurveVelocity | 否 | 曲线速度满射切空间含边界情形，Mathlib 全缺 | +| Sec03_16/Proposition_3_20.lean | tangent_bundle_opens_trivializationAt_eq_toProd, globalChartDiffeomorph 等 | partial-dup | TangentBundle/Trivialization | 否 | 单图卡切丛平凡化全证，主 def 依赖含 sorry 的 3.22 | +| Sec03_20/Problem_3_7.lean | TangentSpace.toPointDerivation, smooth_germ_derivation_existsUnique_tangentVector 等 | partial-dup | TangentBundle/PointDerivation | 是 | 切向量≃芽导子等价，Mathlib 著名缺口，余两条 sorry | + +
可考虑（medium，11 项） + +| 文件 | 声明 | 分类 | 落点 | sorry | 理由 | +|---|---|---|---|---|---| +| Sec03_13/Proposition_3_2.lean | directional_point_derivation, geometric_to_point_derivation_linear_equiv 等 | new | Util/Tangent/PointDerivation | 是 | 几何切向量↔导子等价是真缺口，但仅欧氏且关键步全 sorry | +| Sec03_14/Lemma_3_11.lean | mfderiv_half_space_inclusion_isInvertible_of_boundary_eq_zero | new | Manifold/Boundary | 是 | 半空间包含边界点微分可逆，仅语句无证明可移 | +| Sec03_14/Proposition_3_8.lean | PointDerivation.congr_of_eqOn_nhds | new | Manifold/Derivation | 否 | 导子局部性 bump 函数完整证明，但本库不用导子模型 | +| Sec03_17/Definition_3_17_extra_1.lean | curve_velocity, curve_velocityWithin 等 | new | CurveVelocity | 否 | 命名曲线速度薄封装，是移植 3.23 的基础 | +| Sec03_18/Definition_3_18_extra_3.lean | SmoothCurveAt, CurveVelocityClass 等 | new | TangentBundle/CurveVelocity | 是 | 曲线速度实现切空间，两核心定理 sorry 需重设计 | +| Sec03_18/Definition_3_18_extra_4.lean | IsCoordinateTangentVector, TangentSpace.coordinateComponent 等 | new | TangentBundle/CoordinateComponents | 否 | 坐标分量 API 全证，Mathlib 缺，偏教学起源 | +| Sec03_20/Problem_3_4.lean | tangentBundle_circle_diffeomorph_prodLie, circleTangentFiberDiffeomorph 等 | new | TangentBundle/LieGroupTrivialization | 否 | 李群平凡化 TG≃G×Lie(G) 全证，硬编码圆需泛化 | +| Sec03_14/Proposition_3_6.lean | mfderiv_comp_of_smooth, diffeomorph_mfderiv_symm_eq_symm | partial-dup | Util/Tangent | 否 | 微分同胚逆的微分等于微分之逆，Mathlib 缺的小胶水 | +| Sec03_15/Proposition_3_15.lean | chart_mdifferentiable_of_mem_maximalAtlas, chart_coordinate_vectors_basis | partial-dup | Util/Chart/CoordinateBasis | 否 | 图卡 mfderiv 打包成 Basis，小型可复用坐标 API | +| Sec03_16/Corollary_3_22.lean | tangentMap_diffeomorph, tangentMap_comp_of_smooth 等 | partial-dup | TangentBundle/Diffeomorph | 是 | Diffeomorph 诱导切丛微分同胚，五条辅助引理 sorry | +| Sec03_20/Problem_3_1.lean | isLocallyConstant_of_mfderiv_eq_zero, mfderiv_eq_zero_iff_isLocallyConstant 等 | partial-dup | TangentBundle/MFDerivLocallyConstant | 是 | mfderiv≡0 当且仅当局部常值，正向 sorry 受阻 | + +
+ +
跳过（42 项，绝大多数为 Mathlib 包装/recall 文件） + +- Sec03_13/Corollary_3_3.lean — new — 欧氏限定全 sorry +- Sec03_13/Definition_3_13_extra_1.lean — mathlib-dup — 薄包装加记号 +- Sec03_13/Definition_3_13_extra_2.lean — mathlib-dup — 仅 #check 复述 +- Sec03_13/Definition_3_13_extra_3.lean — mathlib-dup — rfl 级复述 +- Sec03_13/Exercise_3_5.lean — mathlib-dup — 纯 #check 回顾 +- Sec03_13/Lemma_3_1.lean — mathlib-dup — 欧氏一行推论 +- Sec03_13/Lemma_3_4.lean — mathlib-dup — 一行包装 +- Sec03_14/Definition_3_14_extra_1.lean — mathlib-dup — 复述 mfderiv 签名 +- Sec03_14/Definition_3_14_extra_2.lean — mathlib-dup — 单个 #check +- Sec03_14/Exercise_3_7.lean — mathlib-dup — 纯 #check 复述 +- Sec03_14/Proposition_3_10.lean — mathlib-dup — 一行 defeq +- Sec03_14/Proposition_3_12.lean — mathlib-dup — sorry 复述维数 +- Sec03_14/Proposition_3_13.lean — mathlib-dup — 一行包装附 sorry +- Sec03_15/Definition_3_15_extra_1.lean — partial-dup — 已被现有 API 覆盖 +- Sec03_15/Definition_3_15_extra_2.lean — partial-dup — 一行 .repr 包装 +- Sec03_15/Example_3_16.lean — new — 教科书数值例 +- Sec03_15/Exercise_3_17.lean — new — 教学专用示例 +- Sec03_15/Remark_3_15_extra_3.lean — mathlib-dup — 纯回顾 +- Sec03_15/Remark_3_15_extra_4.lean — partial-dup — 两行胶水已有 +- Sec03_15/Remark_3_15_extra_5.lean — mathlib-dup — 回顾复述 +- Sec03_16/Definition_3_16_extra_1.lean — mathlib-dup — 回顾 TangentBundle +- Sec03_16/Definition_3_16_extra_3.lean — mathlib-dup — 仅 #check +- Sec03_16/Exercise_3_19.lean — new — 单个 rfl 定理 +- Sec03_16/Notation_3_16_extra_2.lean — mathlib-dup — 仅记号加 #check +- Sec03_16/Notation_3_16_extra_4.lean — mathlib-dup — 回顾桥引理 +- Sec03_16/Proposition_3_18.lean — mathlib-dup — 特化 contMDiff_proj +- Sec03_16/Proposition_3_21.lean — mathlib-dup — 单个 #check 特化 +- Sec03_17/Proposition_3_24.lean — mathlib-dup — 链规则一行求值 +- Sec03_17/Corollary_3_25.lean — mathlib-dup — 复述 3.24 +- Sec03_18/Definition_3_18_extra_1.lean — mathlib-dup — 记号加一行实例 +- Sec03_18/Definition_3_18_extra_2.lean — partial-dup — 平凡 abbrev 加 sorry +- Sec03_19/Definition_3_19_extra_1.lean — mathlib-dup — 回顾 Category +- Sec03_19/Definition_3_19_extra_2.lean — mathlib-dup — 回顾 IsIso +- Sec03_19/Definition_3_19_extra_3.lean — mathlib-dup — 回顾小范畴概念 +- Sec03_19/Definition_3_19_extra_4.lean — mathlib-dup — 仅 #check 函子 +- Sec03_19/Definition_3_19_extra_5.lean — mathlib-dup — 仅 #check 反变函子 +- Sec03_19/Example_3_26.lean — partial-dup — 教学示例 +- Sec03_19/Exercise_3_27.lean — mathlib-dup — 回顾无新证明 +- Sec03_20/Problem_3_3.lean — mathlib-dup — 纯回顾复述 +- Sec03_20/Problem_3_5.lean — new — 教科书专用习题 +- Sec03_20/Problem_3_6.lean — new — 具体例几乎全 sorry +- Sec03_20/Problem_3_8.lean — new — 纯回顾桥文件 + +
+ +## 小结 + +第三章共审计 53 个文件，其中约四分之三为 Mathlib 重复（recall/#check 复述或一行包装），可直接跳过。真正值得移植的高价值条目集中在切空间基础设施：开子集包含映射微分可逆性（Proposition 3.9）、曲线速度满射（Proposition 3.23）、单图卡切丛平凡化（Proposition 3.20）以及切向量-导子等价（Problem 3.7），前三者中两个已完全无 sorry。中价值条目多围绕导子模型与坐标基 API，但普遍含 sorry 或需要设计返工，建议在 CurveVelocity 与 Tangent 工具模块落地高价值条目后再酌情跟进。 + +--- + +# Chap04 + +## 移植优先（high，16 项） + +| 文件 | 声明 | 分类 | 落点 | sorry | 理由 | +|---|---|---|---|---|---| +| Sec04_21/Exercise_4_3.lean | prod_fst_isSmoothSubmersion, prod_mk_right_isImmersion 等 | new | Manifold/ImmersionSubmersion | 否 | 积投影淹没/切片浸入全证，含可复用图卡群胚基建 | +| Sec04_21/Exercise_4_4.lean | IsSmoothSubmersion.comp, IsImmersion.comp 等 | new | Manifold/ImmersionSubmersion | 是 | 淹没复合与秩 API，攻 Mathlib TODO，一辅助引理 3 sorry | +| Sec04_22/Proposition_4_8.lean | IsLocalDiffeomorph.isImmersion, is_local_diffeomorph_iff_is_immersion_and_is_smooth_submersion 等 | new | Manifold/Submersion | 否 | 局部微分同胚↔浸入+淹没全证，上游谓词含 sorry | +| Sec04_22/Theorem_4_5.lean | isLocalDiffeomorphAt_of_contMDiffAt_mfderiv_isInvertible, model_partialDiffeomorph_of_inverse_function_theorem 等 | new | Manifold/InverseFunctionTheorem | 否 | 流形版反函数定理完整证明，Mathlib 明确 TODO | +| Sec04_24/Exercise_4_16.lean | IsImmersion.ex416_comp, IsSmoothEmbedding.comp 等 | new | SmoothManifold/Immersion | 是 | 浸入/光滑嵌入复合，Mathlib proof_wanted，余一 sorry | +| Sec04_25/Definition_4_25_extra_2.lean | Topology.IsTopologicalSubmersion, IsTopologicalSubmersion.isQuotientMap 等 | new | Manifold/Submersion | 否 | 拓扑淹没 API 全证（开/商映射），Mathlib 缺 | +| Sec04_25/Proposition_4_28.lean | Manifold.IsSmoothSubmersion, IsSmoothSubmersion.isOpenMap 等 | new | Manifold/Submersion | 否 | 定义 Mathlib 缺失的光滑淹没结构，依赖含 sorry 的 4.26 | +| Sec04_25/Theorem_4_26.lean | Manifold.IsSmoothLocalSection, smooth_submersion_iff_exists_smooth_local_section_through_every_point 等 | new | Manifold/Submersion | 是 | 局部截面定理刻画淹没，主定理 sorry 需秩定理级工作 | +| Sec04_25/Theorem_4_29.lean | Manifold.contMDiff_iff_comp_of_surjective_smooth_submersion | new | Manifold/Submersion | 是 | 满淹没特征性质是商流形主力引理，仅语句含 sorry | +| Sec04_25/Theorem_4_30.lean | Manifold.existsUnique_contMDiff_lift_of_surjective_smooth_submersion | new | Manifold/Submersion | 是 | 商流形光滑提升存在唯一性核心基建，证明为 sorry | +| Sec04_26/Definition_4_26_extra_1.lean | Manifold.IsSmoothCoveringMap, IsUniversalSmoothCoveringMap 等 | new | Manifold/CoveringMap | 否 | 光滑覆盖映射核心定义层，Mathlib 仅有拓扑版 | +| Sec04_26/Exercise_4_37.lean | IsLocalDiffeomorph.isSmoothLocalSection, IsSmoothCoveringMap.isSmoothLocalSection 等 | new | Manifold/CoveringMap | 否 | 连续局部截面自动光滑，全证通用升级引理 | +| Sec04_26/Proposition_4_36.lean | IsCoveringMap.exists_localSectionOn, IsSmoothCoveringMap.localSection_eq 等 | new | Manifold/CoveringMap | 否 | 光滑局部截面存在与预连通集上唯一性，完整 API | +| Sec04_26/Proposition_4_40.lean | exists_unique_smooth_covering_structure, lifted_covering_chartedSpace 等 | new | Manifold/CoveringMap | 否 | 拓扑覆盖唯一光滑结构，700 行无 sorry 大定理 | +| Sec04_26/Proposition_4_46.lean | isSmoothCoveringMap_of_proper_localDiffeomorph, fiber_finite_of_proper_local_diffeomorph 等 | new | Manifold/CoveringMap | 否 | 真局部微分同胚⇒覆盖映射判据全证，移植需并回正式定义 | +| Sec04_27/Problem_4_5.lean | complexProjectiveQuotientMap_isSmoothSubmersion, complexProjectiveLine_diffeomorphic_sphere 等 | new | Instances/ComplexProjectiveSpace | 否 | CP^n 商淹没全证，含 CP^1≅S^2 压轴构造 | + +
可考虑（medium，22 项） + +| 文件 | 声明 | 分类 | 落点 | sorry | 理由 | +|---|---|---|---|---|---| +| Sec04_21/Definition_4_21_extra_1.lean | rank_at_eq_finrank_range_mfderiv, is_immersion_iff_forall_injective_mfderiv 等 | new | Manifold/Rank | 是 | 秩 API 填 Mathlib 缺口，但定理全 sorry 仅语句可移 | +| Sec04_21/Proposition_4_1.lean | exists_open_restriction_isSmoothSubmersion_of_surjective_mfderiv, exists_open_restriction_isImmersion_of_injective_mfderiv | new | Manifold/ImmersionSubmersion | 是 | 点态满/单 mfderiv 给局部淹没/浸入，证明全 sorry | +| Sec04_22/Exercise_4_10.lean | smooth_iff_comp_left_of_isLocalDiffeomorph, smooth_iff_comp_right_of_surjective_isLocalDiffeomorph | new | Manifold/LocalDiffeomorph | 否 | 经局部微分同胚前后复合检测光滑性，全证 iff 引理 | +| Sec04_23/Theorem_4_14.lean | constant_rank_surjective_is_smooth_submersion, constant_rank_injective_is_immersion 等 | new | Manifold/RankTheorem | 是 | 全局秩定理是真缺口，但三证明全 sorry 仅语句 | +| Sec04_23/Theorem_4_15.lean | boundary_immersion_normal_form, BoundaryLocalCoordinateNormalFormAt 等 | new | Manifold/Boundary | 是 | 带边流形浸入边界标准形，与 GMT 相关但主定理 sorry | +| Sec04_24/Definition_4_24_extra_2.lean | Topology.IsTopologicalImmersion, IsEmbedding.isTopologicalImmersion 等 | new | SmoothManifold/Immersion | 否 | 局部嵌入谓词小型全证拓扑 API，单独价值有限 | +| Sec04_24/Proposition_4_22.lean | smooth_embedding_of_injective_isImmersion_isOpenMap, smooth_embedding_of_compact_source_injective_isImmersion 等 | new | SmoothManifold/Embedding | 是 | 单浸入成嵌入的充分条件骨架，五证明全 sorry | +| Sec04_24/Theorem_4_25.lean | Manifold.isImmersion_iff_forall_exists_open_restriction_isSmoothEmbedding | new | SmoothManifold/Embedding | 是 | 局部嵌入定理是真缺口，但仅单条 sorry 存根 | +| Sec04_25/Definition_4_25_extra_1.lean | ContinuousMap.IsLocalSection, Function.RightInverse.isLocalSection_restrict_top 等 | new | Manifold/Submersion | 否 | 连续映射局部截面谓词，小而全证的基础层 | +| Sec04_25/Theorem_4_31.lean | Manifold.existsUnique_diffeomorph_of_surjective_smooth_submersions_constant_on_each_others_fibers | new | Manifold/Submersion | 是 | 光滑商唯一性，4.29/4.30 的推论，仅语句 sorry | +| Sec04_26/Exercise_4_38.lean | Manifold.IsSmoothCoveringMap.pi, isCoveringMap_pi 等 | new | Manifold/CoveringMap | 否 | 覆盖映射有限积定理无 sorry，移植前需精简同胚管线 | +| Sec04_26/Exercise_4_39.lean | Bundle.Trivialization.sheet_coordinate_eq_on_component, component_bijOn_baseSet 等 | new | Manifold/CoveringMap | 否 | 叶分解引理全证，Mathlib 缺的 Trivialization API，略偏门 | +| Sec04_26/Proposition_4_33.lean | IsSmoothCoveringMap.isSmoothSubmersion, diffeomorphOfInjective 等 | new | Manifold/CoveringMap | 是 | 覆盖映射基本性质接口正确，但五条中四条 sorry | +| Sec04_27/Problem_4_11.lean | isProperMap_iff_finite_fibers_of_isCoveringMap, exists_smoothCoveringMap_not_isProperMap | new | MetricGeometry/Covering/ProperMap | 是 | 覆盖真当且仅当纤维有限是真缺口，仅语句需从头证 | +| Sec04_27/Problem_4_12.lean | torus_of_revolution_map_isSmoothEmbedding, torus_product_isManifold 等 | new | Instances/Torus | 否 | 平坦环面嵌入 R^3 全证，含 pi 群胚/积流形助手 | +| Sec04_27/Problem_4_3.lean | boundary_rank_normal_form, constant_rank_boundary_local_coordinate_normal_form | new | Manifold/RankTheorem | 是 | 边界点常秩标准形是真缺口，但 sorry 语句且形式别扭 | +| Sec04_27/Problem_4_6.lean | not_exists_smooth_submersion_to_euclideanSpace | new | Manifold/Submersion | 否 | 紧流形无淹没到 R^k 经典结果全证，依赖项目谓词 | +| Sec04_27/Problem_4_7.lean | contMDiff_iff_comp_equiv_of_submersion_characteristic_property, exists_diffeomorph_of_submersion_characteristic_property | new | Manifold/Submersion | 是 | 商光滑结构唯一性有价值，但两定理皆 sorry | +| Sec04_22/Proposition_4_6.lean | isLocalDiffeomorph_comp, isLocalDiffeomorph_pi 等 | partial-dup | Manifold/LocalDiffeomorph | 是 | 缺失的复合/积/坐标判据引理全 sorry，余为回顾 | +| Sec04_23/Theorem_4_12.lean | rank_normal_form, constant_rank_local_coordinate_normal_form 等 | partial-dup | Manifold/RankTheorem | 是 | 常秩定理是真缺口，但五证明全 sorry 且欧氏结构需重构 | +| Sec04_24/Example_4_20.lean | denseTorusCurve, circle_exp_isLocalDiffeomorph_from_angle_branch 等 | partial-dup | SmoothManifold/CircleExp | 否 | 无理缠绕属反例，Circle.exp 局部微分同胚助手可复用 | +| Sec04_26/Example_4_35.lean | circle_exp_isSmoothCoveringMap, sphere_to_realProjectiveSpace_isCoveringMap 等 | partial-dup | Instances/CoveringExamples | 否 | 光滑覆盖实例全证，RP^n 覆盖为新内容好例证 | + +
+ +
跳过（26 项，绝大多数为 Mathlib 包装/recall 文件） + +- Sec04_21/Example_4_2.lean — new — 全 sorry 教学例 +- Sec04_22/Definition_4_22_extra_1.lean — mathlib-dup — 纯 abbrev 复述 +- Sec04_22/Exercise_4_7.lean — mathlib-dup — 仅 #check 回顾 +- Sec04_22/Exercise_4_9.lean — new — 欧氏硬编码加 sorry +- Sec04_23/Corollary_4_13.lean — new — 单条 sorry 复述 +- Sec04_24/Definition_4_24_extra_1.lean — mathlib-dup — 八行仅 #check +- Sec04_24/Example_4_17.lean — partial-dup — of_opens 加 sorry 存根 +- Sec04_24/Example_4_18.lean — new — 单个具体反例 +- Sec04_24/Example_4_19.lean — new — 教学八字曲线反例 +- Sec04_24/Exercise_4_24.lean — new — 一次性反例机件 +- Sec04_24/Lemma_4_21.lean — mathlib-dup — 重证 Dirichlet 逼近 +- Sec04_25/Exercise_4_27.lean — new — x^3 教学反例 +- Sec04_25/Exercise_4_32.lean — new — 纯回顾 4.31 +- Sec04_26/Corollary_4_43.lean — new — sorry 存根 +- Sec04_26/Exercise_4_34.lean — new — 纯回顾脚手架 +- Sec04_26/Exercise_4_42.lean — new — 纯回顾 4.41 +- Sec04_26/Exercise_4_44.lean — new — 纯回顾 4.43 +- Sec04_26/Exercise_4_45.lean — new — 边界框架 sorry 存根 +- Sec04_26/Proposition_4_41.lean — new — 边界版主结果全 sorry +- Sec04_27/Problem_4_1.lean — new — 薄包装单反例 +- Sec04_27/Problem_4_10.lean — new — 单条 sorry 语句 +- Sec04_27/Problem_4_13.lean — new — 语句依赖未证基建 +- Sec04_27/Problem_4_2.lean — mathlib-dup — 一行特化 +- Sec04_27/Problem_4_4.lean — new — 纯记账回顾 +- Sec04_27/Problem_4_8.lean — new — 全 sorry 反例 +- Sec04_27/Problem_4_9.lean — new — 纯回顾视图 + +
+ +## 小结 + +第四章（浸入、淹没、嵌入与覆盖映射）是整个审计中移植价值最高的章节之一：16 个高价值文件中多数完全无 sorry，包括流形版反函数定理（Mathlib 明确 TODO）、光滑淹没与光滑覆盖映射的完整定义层 API、拓扑覆盖提升唯一光滑结构的 700 行大定理，以及 CP^n 商淹没与 CP^1 ≅ S^2 的完整构造。中价值条目主要是设计良好但证明缺失的语句骨架（秩定理、全局秩定理、商流形特征性质），移植它们等于承诺补全秩定理级别的证明工作。建议优先按 Submersion → CoveringMap → InverseFunctionTheorem 的依赖顺序成块移植无 sorry 文件，再以其为基础逐步补证 IsSmoothSubmersion 上游的局部截面定理。 + +--- + +# Chap05 + +## 移植优先（high，18 项） + +| 文件 | 声明 | 分类 | 落点 | sorry | 理由 | +|---|---|---|---|---|---| +| Sec05_28/Definition_5_28_extra_1.lean | IsEmbeddedSubmanifold、IsEmbeddedSubmanifold.codimension 等 | new | Manifold/Submanifold/Embedded | 否 | 嵌入子流形类填 Mathlib 空白，需 Sec05_31 浸入结构 | +| Sec05_28/Proposition_5_4.lean | graphMap、graphMap_isSmoothEmbedding 等 | new | Manifold/Submanifold/Graph | 是 | 光滑映射的图作光滑嵌入，Mathlib 缺，GMT 基础 | +| Sec05_29/Definition_5_29_extra_1.lean | Set.euclideanSlice、Set.IsSliceInChart 等 | new | Manifold/SliceCharts | 否 | 切片图卡/局部切片条件 API，子流形理论根基 | +| Sec05_29/Theorem_5_8.lean | local_slice_criterion_for_embedded_submanifold 等 | new | Manifold/SliceCharts | 否 | 局部 k-切片判据无 sorry 全证，Mathlib 空白 | +| Sec05_30/Proposition_5_16.lean | euclidean_tail_projection、embedded_submanifold_iff_locally_level_set_of_smooth_submersion 等 | new | Manifold/Submanifold/LocalDefining | 是 | 浸没水平集局部判据，投影引理已证，主 iff 仍 sorry | +| Sec05_31/Definition_5_31_extra_1.lean | Manifold.ImmersedSubmanifold、IsImmersion.toImmersedSubmanifold 等 | new | Manifold/Submanifold/Immersed | 否 | 无 sorry 捆绑浸入子流形结构，varifold 代码直接受益 | +| Sec05_32/Corollary_5_30.lean | IsSmoothEmbedding.contMDiff_toSubtype、contMDiffAt_toSubtype 等 | new | Manifold/Submanifold | 否 | 一般余域限制定理已证，Mathlib 仅有球面特例 | +| Sec05_35/Corollary_5_39.lean | tangent_iff_mfderiv_eq_zero_of_isDefiningFunction 等 | new | Submanifold/LevelSet | 否 | 正则值切空间刻画已证，但依赖含 sorry 的命题 5.38 | +| Sec05_35/Definition_5_35_extra_2.lean | IsInwardPointing、IsBoundaryTangentVector 等 | new | Boundary/PointingVectors | 否 | 内外指向向量 API 填散度定理缺口，定义需重设计 | +| Sec05_35/Notation_5_35_extra_1.lean | Manifold.submanifoldTangentSpace、T[J; p] 记号 | new | Submanifold/TangentSpace | 否 | 子流形切空间核心定义，全节定理之基石 | +| Sec05_35/Proposition_5_35.lean | tangentVector_mem_submanifold_iff_exists_curve 等 | new | Submanifold/TangentSpace | 否 | 切向量即曲线速度，全证，需 Chap03 曲线基建 | +| Sec05_35/Proposition_5_38.lean | IsLocalDefiningMapOn、tangentSpace_eq_ker_mfderiv_of_isLocalDefiningMapOn | new | Submanifold/LevelSet | 是 | 局部定义映射核心 API，5.39/5.40 依赖，主定理 sorry | +| Sec05_36/Definition_5_36_extra_4.lean | Set.euclideanHalfSlice、OpenPartialHomeomorph.IsBoundarySliceChart 等 | new | Manifold/SliceCharts | 否 | 带边界半切片图卡 API 无 sorry，需 Sec05_29 配套 | +| Sec05_36/Theorem_5_51.lean | local_slice_criterion_for_embedded_submanifold_with_boundary 等 | new | Manifold/SubmanifoldWithBoundary | 是 | 带边界 k-切片判据约 2000 行，核心三处 sorry 待补 | +| Sec05_37/Problem_5_18.lean | immersed_submanifold_isEmbeddedSubmanifold_iff_smoothFunctions_isSmoothOn 等 | new | Manifold/Submanifold/SmoothExtension | 否 | 嵌入 iff 光滑函数可延拓，无 sorry 可复用 API | +| Sec05_37/Problem_5_23.lean | IsBoundaryRegularValue、regular_preimage_has_embedded_submanifold_with_boundary_structure 等 | new | Manifold/Submanifold/RegularValue | 是 | 带边界正则值原像定理大部已证，余两引理 sorry | +| Sec05_37/Problem_5_8.lean | basis_model_diffeomorph、regularCoordinateBall_compl_boundary_diffeomorph_sphere 等 | new | Manifold/CoordinateBall | 是 | 正则坐标球/正则域基建近完成，仅余一处 sorry | +| Sec05_36/Proposition_5_49.lean | isSmoothEmbedding_of_le、immersed_submanifold_has_embedded_neighborhood 等 | partial-dup | Manifold/Submanifold | 否 | 嵌入像诱导结构已证，超出 Mathlib SmoothEmbedding | + +
可考虑（medium，33 项） + +| 文件 | 声明 | 分类 | 落点 | sorry | 理由 | +|---|---|---|---|---|---| +| Sec05_28/Proposition_5_2.lean | IsInducedImageManifoldStructure、smooth_embedding_range_has_induced_manifold_structure 等 | new | Manifold/Submanifold/InducedStructure | 是 | 像上诱导结构是基石，但定理全 sorry 且 API 需重做 | +| Sec05_28/Proposition_5_3.lean | productSliceMap、productSliceMap_isSmoothEmbedding 等 | new | Manifold/Submanifold/Product | 是 | 切片嵌入 x↦(x,p) 小引理可用，主定理全 sorry | +| Sec05_28/Proposition_5_7.lean | smooth_map_graph_isProperlyEmbedded | new | Manifold/Submanifold/Graph | 是 | 全局图真嵌入，单条 sorry，应与命题 5.4 同移植 | +| Sec05_29/Exercise_5_10.lean | sphericalCoordinates、sphericalCoordinates_mem_maximalAtlas 等 | new | Instances/SphericalCoordinates | 否 | 三维球坐标图卡全证，但属具体图卡非通用基建 | +| Sec05_30/Corollary_5_13.lean | smooth_submersion_level_set_has_embedded_submanifold_structure 等 | new | Manifold/Submanifold/LevelSet | 否 | 浸没水平集推论为薄包装，依赖含 sorry 定理 5.12 | +| Sec05_30/Corollary_5_14.lean | regular_level_set_has_embedded_submanifold_structure 等 | new | Manifold/Submanifold/LevelSet | 是 | 正则水平集定理填空白，但全 sorry 需从头证 | +| Sec05_30/Definition_5_30_extra_2.lean | Manifold.IsRegularPoint、Manifold.IsCriticalValue 等 | new | Manifold/Submanifold/RegularValue | 是 | 正则/临界点词汇缺失，但支撑引理全 sorry | +| Sec05_30/Definition_5_30_extra_3.lean | Set.IsDefiningMap、Set.IsLocalDefiningMapOn 等 | new | Manifold/Submanifold/DefiningMap | 是 | 定义映射 API 空白，但类设计需大幅重做 | +| Sec05_30/Theorem_5_12.lean | constant_rank_level_set_has_embedded_submanifold_structure 等 | new | Manifold/Submanifold/LevelSet | 是 | 常秩水平集定理为关键空白，全 sorry 仅语句可移 | +| Sec05_31/Definition_5_31_extra_2.lean | ImmersedSubmanifold.IsLocalParametrization、IsGlobalParametrization 等 | new | Manifold/Submanifold/Parametrization | 是 | 参数化谓词新颖，但硬编码 Fin k，API 需重做 | +| Sec05_31/Exercise_5_20.lean | ImmersedSubmanifold.continuous_inclusion、subspaceTopology_le_givenTopology_iff_isEmbedding 等 | new | Manifold/Submanifold/Immersed | 否 | 已证核心 API，应与 Definition_5_31_extra_1 同移植 | +| Sec05_31/Proposition_5_18.lean | injective_immersion_range_has_immersed_submanifold_structure 等 | new | Manifold/Submanifold/Immersed | 是 | 单射浸入像结构存在唯一性，仅语句无证明 | +| Sec05_31/Proposition_5_22.lean | ImmersedSubmanifold.exists_open_neighborhood_isSmoothEmbedding | new | Manifold/Submanifold/Immersed | 是 | 浸入子流形局部嵌入有用，但全文单条 sorry 语句 | +| Sec05_31/Proposition_5_23.lean | IsImmersion.isSmoothLocalParametrization_of_mem_maximalAtlas 等 | new | Manifold/Submanifold/Parametrization | 否 | 图卡给局部参数化已证，但绑定待重做的定义 | +| Sec05_32/Remark_5_32_extra_1.lean | IsWeaklyEmbeddedSubmanifold 实例 | new | Manifold/Submanifold | 否 | 嵌入蕴含弱嵌入的胶水实例，须随子流形类同移 | +| Sec05_32/Theorem_5_29.lean | contMDiff_toSubtype_of_isImmersedSubmanifold | new | Manifold/Submanifold | 是 | 推广推论 5.30 的余域限制，仅语句需从头证 | +| Sec05_33/Theorem_5_31.lean | immersed_submanifold_structure_unique_of_same_carrier | new | Manifold/Submanifold | 是 | 子流形结构唯一性 sorry 语句，需全套 API 加真证明 | +| Sec05_35/Definition_5_35_extra_3.lean | BoundaryDefiningFunction、CoeFun 实例 | new | Boundary/DefiningFunction | 否 | 捆绑边界定义函数，硬编码半空间且与 5.43 重复 | +| Sec05_35/Exercise_5_40.lean | tangentSpace_eq_ker_mfderiv_of_level_set_of_hasConstantRank 等 | new | Submanifold/LevelSet | 是 | 常秩水平集切空间，关键引理 sorry 且与 5.39 重复 | +| Sec05_35/Exercise_5_44.lean | boundary_defining_derivative、inwardPointing_iff_boundaryDefiningDerivative_pos 等 | new | Boundary/DefiningFunction | 是 | 导数符号刻画内外向是对的 API，四定理全 sorry | +| Sec05_35/Proposition_5_37.lean | tangentVector_mem_submanifold_iff_forall_smooth_eq_zero | new | Submanifold/TangentSpace | 是 | 函数式切向刻画，单条 sorry，证明需延拓引理 | +| Sec05_35/Proposition_5_41.lean | boundary_coordinate_component、boundary_vector_trichotomy 等 | new | Boundary/PointingVectors | 是 | 边界向量坐标三分法配套定理，八条全 sorry | +| Sec05_35/Proposition_5_43.lean | IsBoundaryDefiningFunction、exists_boundary_defining_function | new | Boundary/DefiningFunction | 是 | 全局边界定义函数存在性 sorry，与 extra_3 重复 | +| Sec05_36/Definition_5_36_extra_2.lean | Set.IsRegularDomain、instIsRegularDomainEmpty | new | Manifold/RegularDomain | 否 | 正则域即散度定理积分域，依项目脚手架需重建 | +| Sec05_36/Definition_5_36_extra_3.lean | Manifold.IsRegularValue、IsRegularSublevelSet 等 | new | Manifold/RegularValue | 是 | 正则值概念填空白，iff 引理 sorry，设计需改 | +| Sec05_36/Proposition_5_46.lean | regular_domain_manifoldInterior_image_eq_interior 等 | new | Manifold/RegularDomain | 是 | 正则域内部/边界对应拓扑内部/边缘，证明全 sorry | +| Sec05_37/Problem_5_15.lean | transported_subset_chartedSpace、transported_subset_isManifold_top 等 | new | Manifold/StructureTransport | 否 | 结构沿同胚移植引理族已证可复用，反例部分教材性 | +| Sec05_37/Problem_5_19.lean | curve_velocity_mem_embedded_submanifold_tangent 等 | new | Manifold/Submanifold/Tangent | 否 | 曲线速度落入切子空间已证，半个文件是反例 | +| Sec05_37/Problem_5_4.lean | continuous_injective_interval_to_curve_manifold_isEmbedding 等 | new | Manifold/CurveEmbedding | 否 | 一维区域不变性辅助引理无 sorry，Mathlib 缺 | +| Sec05_37/Problem_5_5.lean | continuous_injective_real_to_curve_manifold_isEmbedding 等 | new | Manifold/CurveEmbedding | 否 | 实线入一维流形嵌入引理已证，宜与 5.4 并为一模块 | +| Sec05_37/Problem_5_6.lean | unitTangentBundle、unitTangentBundle_exists_isSmoothEmbedding 等 | new | TangentBundle/UnitTangentBundle | 是 | 单位切丛各处皆无，但主定理全 sorry，仅 API 种子 | +| Sec05_28/Proposition_5_1.lean | open_submanifold_isEmbeddedSubmanifold 等 | partial-dup | Manifold/Submanifold/Open | 是 | 部分重复 Mathlib of_opens，逆命题全 sorry 需推广 | +| Sec05_32/Definition_5_32_extra_2.lean | IsImmersedSubmanifold、IsWeaklyEmbeddedSubmanifold 等 | partial-dup | Manifold/Submanifold | 否 | 子流形谓词类填空白，API 需重做且一辅助重复 Mathlib | + +
+ +
跳过（34 项，绝大多数为 Mathlib 包装/recall 文件） + +- Sec05_28/Corollary_5_6.lean — mathlib-dup — 一行复合既有引理 +- Sec05_28/Definition_5_28_extra_2.lean — partial-dup — 薄命名缩写 +- Sec05_28/Proposition_5_5.lean — mathlib-dup — 仅 #check 包装 +- Sec05_29/Example_5_9.lean — partial-dup — 球面 API 重包装 +- Sec05_29/Remark_5_29_extra_2.lean — new — 仅 sorry 语句备注 +- Sec05_29/Remark_5_29_extra_3.lean — new — recall 交叉引用 +- Sec05_30/Definition_5_30_extra_1.lean — mathlib-dup — recall 原像概念 +- Sec05_30/Example_5_15.lean — mathlib-dup — 球面教学复述 +- Sec05_30/Example_5_17.lean — new — 环面例全 sorry +- Sec05_31/Example_5_19.lean — new — 八字反例无 API +- Sec05_31/Example_5_25.lean — new — #check 加平凡推论 +- Sec05_31/Example_5_26.lean — new — 八字脚手架含 sorry +- Sec05_31/Exercise_5_24.lean — new — 仅 recall/#check +- Sec05_32/Example_5_28.lean — new — 八字反例关键 sorry +- Sec05_32/Theorem_5_27.lean — mathlib-dup — recall 加一行特化 +- Sec05_34/Notation_5_34_extra_1.lean — mathlib-dup — 纯记号引用 +- Sec05_35/Definition_5_35_extra_4.lean — new — R² 专用脚手架 +- Sec05_35/Example_5_45.lean — new — 单条平面曲线例 +- Sec05_35/Exercise_5_36.lean — new — 纯 recall 复述 +- Sec05_35/Exercise_5_42.lean — new — recall sorry 语句 +- Sec05_36/Definition_5_36_extra_1.lean — mathlib-dup — #check 复述谓词 +- Sec05_36/Exercise_5_50.lean — partial-dup — recall 重证组合 +- Sec05_36/Exercise_5_52.lean — partial-dup — recall 再导出 +- Sec05_36/Exercise_5_54.lean — partial-dup — recall 指针 +- Sec05_36/Remark_5_36_extra_5.lean — partial-dup — 无声明备注 +- Sec05_36/Theorem_5_53.lean — partial-dup — 一行包装且 sorry +- Sec05_37/Problem_5_1.lean — new — 具体习题无 API +- Sec05_37/Problem_5_10.lean — new — 三次曲线 17 sorry +- Sec05_37/Problem_5_11.lean — new — 具体零集全 sorry +- Sec05_37/Problem_5_12.lean — partial-dup — 新部分全 sorry +- Sec05_37/Problem_5_13.lean — new — 一次性反例含 sorry +- Sec05_37/Problem_5_20.lean — new — 八字反例无 API +- Sec05_37/Problem_5_7.lean — new — 单例分类含 sorry +- Sec05_37/Problem_5_9.lean — new — 单条 sorry 语句 + +
+ +## 小结 + +本章（第五章：子流形理论）是整个审计中移植价值最高的一章：嵌入/浸入子流形类、切片图卡判据、子流形切空间、局部定义映射与边界向量 API 共 18 个高价值文件，几乎全部为 Mathlib 空白且半数以上 sorry-free，可直接支撑 OpenGALib 的 GMT 与散度定理缺口。建议以 SliceCharts、Submanifold/Immersed+Embedded、Submanifold/TangentSpace 三条主线为骨架先移植无 sorry 文件，再用 medium 表中的 level-set 与 boundary 系列补全语句层。低价值条目以教材具体反例与 recall 脚手架为主，可整体跳过。 From 2cc2713ca0e15776e41a35f4d8c3aa4734cda490 Mon Sep 17 00:00:00 2001 From: Xinze-Li-Moqian <70414198+Xinze-Li-Moqian@users.noreply.github.com> Date: Sun, 14 Jun 2026 15:01:02 -0400 Subject: [PATCH 2/2] docs: translate integration ledger to English MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit PLAN.md and WORKLIST.md → English to match the public repo's language (CONVENTIONS / NAMING_CONVENTION / REFACTOR_PLAYBOOK are English). Folds in the corrections established since: single **Math.** anchor docstrings (not Math./Eng. dual), namespace Manifold per domain-namespace convention, issue #61 as the discussion venue. Audit tables and item counts unchanged (high 52 / medium 101 / skip 186). --- .../2026-06-12-smooth-manifolds-lee/PLAN.md | 157 ++- .../WORKLIST.md | 962 ++++++++++-------- 2 files changed, 618 insertions(+), 501 deletions(-) diff --git a/docs/log/2026-06-12-smooth-manifolds-lee/PLAN.md b/docs/log/2026-06-12-smooth-manifolds-lee/PLAN.md index 4db4bb6..736fc8c 100644 --- a/docs/log/2026-06-12-smooth-manifolds-lee/PLAN.md +++ b/docs/log/2026-06-12-smooth-manifolds-lee/PLAN.md @@ -1,67 +1,122 @@ -# 2026-06-12 · SmoothManifoldsLee 大分支整合方案 +# 2026-06-12 · SmoothManifoldsLee integration plan -**事件**：LehengChen 推送 `import/smooth-manifolds-lee`（`a5f308c`）：Lee《Introduction to Smooth Manifolds》Ch1–5 的形式化，346 文件 / 6.2 万行，仅依赖 Mathlib，与 OpenGALib 零依赖零重复。当日全量审计：**187 全新 / 95 Mathlib 重复 / 57 部分重复；52 个高价值文件**。明细与施工台账见同目录 `WORKLIST.md`。 +**Event.** LehengChen pushed `import/smooth-manifolds-lee` (`a5f308c`): a Lean +formalization of Lee's *Introduction to Smooth Manifolds* Ch1–5 — 346 files / +62k lines, Mathlib-only deps, zero dependency on and zero overlap with +OpenGALib. Same-day full audit: **187 new / 95 Mathlib-dup / 57 partial-dup; +52 high-value files**. Per-file detail and the construction ledger are in +`WORKLIST.md` (same folder). -## 问题 +## Problem -这批材料是**教材序的形式化**：一个编号一个文件、import 图与章节耦合、设施代码（图卡操作、截断函数、实例打包）散落在各章定理脚下随用随造。我们要的是**高复用、可维护、可延伸的软件**：声明按数学对象组织、设施沉淀为共用层、上层只 import 设施而不知道教材的存在。 +This material is a **textbook-ordered formalization**: one file per numbered +item, an import graph coupled to chapter numbering, and infrastructure code +(chart operations, cutoff functions, instance packaging) scattered ad hoc under +each chapter's theorems. We want **reusable, maintainable, extensible +software**: declarations organized by mathematical object, infrastructure +settled into shared layers, upper layers importing the infrastructure without +knowing the textbook exists. -所以要回答的是：**教材序形式化 → 软件库的转化怎么做，并且做成可重复的流程**——这不会是最后一次有人带着一整本书的形式化来敲门。 +So the question to answer is: **how to turn a textbook-ordered formalization +into a software library, and make that conversion a repeatable process** — this +will not be the last time someone shows up with a whole book's worth of +formalization. -## 分支与流程 +## Branches and process ``` -import/ 冻结参考快照（只读，永不 merge，staging/ 不进主干） - ↓ 人工/AI 移植，非 git merge -port/<工单> 短命施工分支，一单一支，从 develop 切出 +import/ frozen reference snapshot (read-only, never merged, staging/ stays out of trunk) + ↓ manual/AI port, not a git merge +port/ short-lived work branch, one item each, cut from develop ↓ PR + CI + review -develop → main 现有惯例不变 +develop → main existing practice unchanged ``` -- import 分支永不合并：外来约定不进历史，且审计结论只对锚定的快照 commit 有效。上游再有新货推 `import/-v2`，diff 出增量、只重审增量，不 force-push。 -- 每个 port PR 的质量门：命名空间已换、落点符合布局、**零 sorry**、提交前**全量 `lake build`**、模块 docstring 带出处行（`Ported from ()`）、linter 基线无新增违例。 -- 领单即在 `WORKLIST.md` 台账改状态，台账改动随移植 PR 同行；不碰别人 in-progress 的单。 -- 全部移植完：参考分支打 tag 归档后删除，台账存档作为出处记录。 - -## 自动化流水线（设想，待试点） - -9 张施工单是同构单元，每单走同一循环，自动化程度由试点数据决定： +- Import branches are never merged: foreign conventions stay out of history, and + audit conclusions are valid only for the pinned snapshot commit. New upstream + material goes to `import/-v2`; diff the delta, re-audit only the delta, + no force-push. +- Quality gates per port PR: house-style namespace, correct module placement, + **zero sorry**, **full `lake build`** before pushing, a one-line provenance + footer in the module docstring (`Provenance: — `), no + new linter-baseline violations. +- Claiming an item updates its status in the `WORKLIST.md` ledger; the ledger + change travels with the port PR. Don't touch an item someone else has marked + in-progress. +- When all items are ported: tag the reference branch for archive, then delete + it; the ledger remains as the provenance record. + +## Automation pipeline (proposed, to be piloted) + +The work items are isomorphic units; each runs the same loop, with automation +depth decided by pilot data: ``` -领单 → ① 通用层判定（AI 输出 复用/扩展/新建 决策表，必须附 grep 证据） - → ② 移植（AI：换命名空间、重组、每条声明补 Math./Eng. 双 docstring） - → ③ 机器门（CI：全量构建、零 sorry、linter、命名与出处检查） - → ④ 自动开 PR（附决策表与台账 diff） - → ⑤ 人审（只审两项，见下节） +claim → ① shared-layer check (AI emits a reuse/extend/new decision table, grep evidence required) + → ② port (AI: house-style namespace, restructure, single **Math.** docstrings) + → ③ machine gate (CI: full build, zero sorry, linters, naming + provenance checks) + → ④ auto-open PR (with decision table and ledger diff) + → ⑤ human review (two things only — see next section) ``` -两条**常驻约束**写进 AI 任务模板，不靠口头提醒： - -1. **通用层优先**：未回答"主分支是否已有同型设施"之前不许写代码。本次审计已验证必要性——两边各写了同一组设施的一半（图卡演算、截断函数、打包类）。 -2. **语义符合**：每条声明带 Math./Eng. 双 docstring（范例 `Riemannian/TangentBundle/TangentSmooth.lean`）。存在性 linter 把守，忠实性人审把守。 - -自动化终点是 PR，不是 develop。人始终是合并守门员。 - -## 人的部分：评审怎么分配 - -依据最小可信基（minimal trusted base）：Lean 内核已检查全部证明，**证明不用人审**；但定义错了，内核会让我们证明几千行关于错误对象的真命题。人审对象收缩为**定义与陈述**，其中定义错误废整个下游依赖锥，定理陈述错误只废自己。 - -1. **核心节点清单**：依赖图入度高的 `def`/`class`/`structure` 入选（实测承重墙：`IsEmbeddedSubmanifold` 被引 18 次、`TopologicalManifold` 17 次），人工增补语义微妙者；`theorem` 一般不入选。 -2. **CODEOWNERS**：核心节点文件映射到数学专家，无 owner 批准不能合并（GitHub 机制强制）。 -3. **专家只审两件事**：Math. docstring 与陈述是否同一数学对象；核心定义的实例化测试是否非空洞（example 进 `Tests/`，如"球面是 `IsEmbeddedSubmanifold`"，堵"假设不可满足、空洞为真"）。 -4. 非核心节点：AI 审 + 抽查。 - -一句话：内核消灭了证明审查，剩余负担集中在可信基，可信基里承重的是依赖图枢纽——枢纽钉给专家，用最少的专家时间买全局正确性。 - -## 待团队决定 - -- [ ] 三个新 linter（docstring 对、命名空间白名单、出处行）进 `OpenGALib/Util/Linter/`？ -- [ ] 核心节点入度阈值（建议 ≥ 5，首版清单随工单 #1 提交） -- [ ] CODEOWNERS 映射：流形地基 / 子流形与切片 / 带边与几何测度论接口各归谁 -- [ ] 自动开 PR 触发方式：本地脚本 / GitHub Action / 定时 agent -- [ ] 人审时限（建议核心节点 PR 三个工作日内响应） - -**试点**：工单 #1（`port/manifold-typeclass-core`）半手工走完整循环，校准模板与 linter；按返工率和人审发现数决定 #2–9 的自动化深度。 +Two **standing constraints** are written into the AI task template, not relied +on as verbal reminders: + +1. **Shared-layer-first**: no code until the question "does the trunk already + have an equivalent facility?" is answered. The audit confirmed the need — + both sides had written half of the same facilities (chart calculus, cutoff + functions, bundled classes). +2. **Semantic faithfulness**: each declaration carries a single docstring tag. + Anchor files (outside `Util/`) use `**Math.**` only — the `AnchorPurity` + linter forbids `**Eng.**`/`**Mixed.**` there; engineering detail is dropped + (the code is self-evident) or moved to a `Util/` submodule. Tag *presence* is + linter-enforced; *faithfulness* is human-reviewed. (Note: an earlier draft of + this plan called for "Math./Eng. dual docstrings" — that was a misreading of + the house style, now corrected.) + +The pipeline terminates at a PR, never at develop. A human is always the merge +gatekeeper. + +## The human part: how review is allocated + +Grounded in the minimal-trusted-base argument: the Lean kernel has checked every +proof, so **proofs need no human review**; but a wrong definition lets the +kernel happily certify thousands of lines of true theorems about the wrong +object. Human review collapses to **definitions and statements**, and within +that, a wrong definition kills the entire downstream dependency cone while a +wrong theorem statement only kills itself. + +1. **Core-node list**: high in-degree `def`/`class`/`structure` declarations are + selected (measured load-bearing walls: `IsEmbeddedSubmanifold` referenced 18×, + `TopologicalManifold` 17×), plus hand-added semantically-subtle definitions; + `theorem`s generally don't qualify. +2. **CODEOWNERS**: core-node files map to math experts; no merge without owner + approval (enforced by GitHub). +3. **Experts review only two things**: whether the `**Math.**` docstring and the + statement describe the same mathematical object; and whether the definition's + instantiation test is non-vacuous (an example in `Tests/`, e.g. "the sphere is + an `IsEmbeddedSubmanifold`", to block "hypotheses unsatisfiable, vacuously + true"). +4. Non-core nodes: AI review + spot checks. + +In one line: the kernel eliminated proof review, the remaining burden concentrates +on the trusted base, and the load-bearing part of the trusted base is the +dependency-graph hubs — pin the hubs to experts via CODEOWNERS, buying global +correctness with the least expert time. + +## For the team to decide + +- [ ] Add three linters (docstring tag, namespace whitelist, provenance line) to + `OpenGALib/Util/Linter/`? +- [ ] Core-node in-degree threshold (suggest ≥ 5; first list ships with item #1). +- [ ] CODEOWNERS mapping: manifold foundations / submanifolds & slices / boundary + & geometric-measure-theory interface — who owns each. +- [ ] Auto-PR trigger: local script / GitHub Action / scheduled agent. +- [ ] Human-review SLA (suggest core-node PRs answered within three working days). + +**Pilot**: item #1 runs the full loop semi-manually to calibrate the template and +linters; rework rate and human-review findings decide the automation depth for +#2–9. --- -关联：PR #60 · `import/smooth-manifolds-lee`（`a5f308c`） +Related: issue #61 · `import/smooth-manifolds-lee` (`a5f308c`) diff --git a/docs/log/2026-06-12-smooth-manifolds-lee/WORKLIST.md b/docs/log/2026-06-12-smooth-manifolds-lee/WORKLIST.md index e61fa90..80624dc 100644 --- a/docs/log/2026-06-12-smooth-manifolds-lee/WORKLIST.md +++ b/docs/log/2026-06-12-smooth-manifolds-lee/WORKLIST.md @@ -1,550 +1,612 @@ -# SmoothManifoldsLee 整合工单 +# SmoothManifoldsLee integration worklist -来源：分支 `import/smooth-manifolds-lee`（commit `a5f308c`，LehengChen，2026-06-12），内容为 Lee《Introduction to Smooth Manifolds》第 1–5 章的 Lean 4 形式化，自包含、仅依赖 Mathlib（v4.30.0），与 OpenGALib 现状零依赖关系。 +Source: branch `import/smooth-manifolds-lee` (commit `a5f308c`, LehengChen, +2026-06-12) — a Lean 4 formalization of Lee's *Introduction to Smooth Manifolds* +Ch1–5, self-contained, Mathlib-only deps (v4.30.0), zero dependency on the +current OpenGALib. -本工单由 2026-06-12 的全量重叠审计产出：40+ 个并行 agent 逐文件对照 Mathlib（`.lake/packages/mathlib`）与 OpenGALib 判重、定级、给出落点建议。审计覆盖全部 346 个章节文件（339 个批量审计 + 7 个深层子目录文件补审）。 +This worklist is the output of the 2026-06-12 full overlap audit: 40+ parallel +agents classified each file against Mathlib (`.lake/packages/mathlib`) and +OpenGALib for duplication, rated it, and proposed a landing module. The audit +covers all 346 chapter files (339 batch-audited + 7 deep-subdirectory files +audited in a follow-up). -## 总体统计 +## Overall stats -| 维度 | 分布 | +| Dimension | Distribution | |---|---| -| 重叠分类 | new 187 · mathlib-dup 95 · partial-dup 57 | -| 移植价值 | high 52 · medium 101 · low 186 | -| 含 sorry 文件 | 106 | - -约 28% 的文件实质重复 Mathlib（多为带教材编号的包装/复述），直接跳过；187 个全新文件是移植主体。 - -## 整合原则 - -1. **按目标模块移植，不按章节顺序**。教材组织（`ChapNN/SecNN_MM/`）不进主库；声明按数学对象重组进领域模块。 -2. **声明名基本可保留**（已是 Mathlib 风格描述性命名），命名空间按我们的**域命名空间惯例**（域名=目录名，对照 `Riemannian`/`Tensor`/`GeometricMeasureTheory`）——对流形域这恰好就是 `namespace Manifold`，与 Mathlib 共享根命名空间和我们扩展 `TangentBundle`/`ContinuousLinearMap` 一致，**不需另起**。文件结构按 `../../NAMING_CONVENTION.md` 重排。 - - **注释 house style（合并 #65 时确立）**：锚文件（`Util/` 之外）只用单 `**Math.**` 标签——`AnchorPurity` linter 禁 `**Eng.**`/`**Mixed.**`，工程细节省掉或挪进 `Util/`；模块注释按架构分层叙事（非教材顺序）；出处压成一行 `Provenance:` 脚注。范本见 develop 上 `OpenGALib/Manifold/Charts/CoordinateBall.lean`（db767b1）。PLAN 早先写的"Math./Eng. 双 docstring"是误读，已废。 - - **def 命名仍须 lowerCamelCase**（`NAMING_CONVENTION.md` 第 42 行）：staged 源的 snake_case（如 `curve_velocity`、`chart_coordinate_vectors_basis`）移植时要改名。 -3. **打包类收编进现有体系**：`TopologicalManifold n M` 等类只是 Mathlib 实例（T2 + 第二可数 + `ChartedSpace`）的打包，与我们已有的 `SmoothManifold M` 打包类（`Riemannian/Manifold/SmoothManifold.lean`）是同一设计模式。移植时统一收编进我们的打包类体系，不引入第二套；维数显式化（`n` 参数）是否保留在收编时定夺。 - - 与 OpenGALib 的重叠：全量审计为 0 个 `opengalib-dup`——我们库直接踩在 Mathlib 流形机器上做度量层以上的内容，Lee 覆盖的子流形/浸入/坐标球层我们完全没有。唯一接口接触点：`GeometricMeasureTheory/Varifold.lean` 的 `LocalSmoothEmbeddingWitness` 临时证人结构，嵌入子流形理论移植后应垫到其下并替换之。 -4. **sorry 不进主干**：含 sorry 的文件要么先补证明，要么陈述层有 sorry 的（如 Chap04 的 `rankAt`/`HasConstantRank`）整段推迟。 -5. **落点归一化**：下文 agent 建议的 targetModule 路径风格不一（`Riemannian/Manifold/…`、`Riemannian/Submanifold/…` 等），施工时统一收敛到一个顶层流形域（待定名，候选 `OpenGALib/SmoothManifold/`），垫在 `Riemannian` 与 `GeometricMeasureTheory` 之下。 -6. 工具链先升级：staged 代码用 Lean v4.30.0 正式版，我们在 rc2，第一批移植前对齐。 - -## 共用抽象设施层 - -两边各自实现了同一组设施的两半（我们：度量/测度面向；他们：拓扑/嵌入面向）。合并时以下五层作为共用模块进主分支，两边上层各自 import： - -| 设施层 | OpenGALib 已有 | staged 分支提供 | 备注 | +| Overlap class | new 187 · mathlib-dup 95 · partial-dup 57 | +| Port value | high 52 · medium 101 · low 186 | +| Files with sorry | 106 | + +About 28% of files substantially duplicate Mathlib (mostly textbook-numbered +wrappers / recall) and are skipped; the 187 new files are the porting body. + +## Integration principles + +1. **Port by target module, not chapter order.** The textbook layout + (`ChapNN/SecNN_MM/`) does not enter the trunk; declarations are regrouped by + mathematical object into domain modules. +2. **Declaration names mostly survive** (already Mathlib-style descriptive + naming); namespaces follow our **domain-namespace convention** (namespace = + directory name, cf. `Riemannian`/`Tensor`/`GeometricMeasureTheory`) — for the + manifold domain that happens to be `namespace Manifold`, and sharing a root + namespace with Mathlib is consistent with how we extend + `TangentBundle`/`ContinuousLinearMap`, so **no new namespace is needed**. File + structure is reorganized per `../../NAMING_CONVENTION.md`. + - **Docstring house style (established merging #65):** anchor files (outside + `Util/`) use single `**Math.**` tags only — the `AnchorPurity` linter + forbids `**Eng.**`/`**Mixed.**`, so engineering detail is dropped or moved + into `Util/`; module docstrings use architecture-layered narrative (not + textbook order); provenance is demoted to a one-line `Provenance:` footer. + Exemplar on develop: `OpenGALib/Manifold/Charts/CoordinateBall.lean` + (db767b1). The earlier PLAN wording "Math./Eng. dual docstring" was a + misread and is retired. + - **defs still require lowerCamelCase** (`NAMING_CONVENTION.md` line 42): the + staged source's snake_case (e.g. `curve_velocity`, + `chart_coordinate_vectors_basis`) must be renamed when ported. +3. **Fold bundled classes into the existing system.** Classes like + `TopologicalManifold n M` are just packaging of Mathlib instances (T2 + + second-countable + `ChartedSpace`), the same design pattern as our existing + `SmoothManifold M` (`Riemannian/Manifold/SmoothManifold.lean`). Port them into + our packaging lineage rather than introducing a second set; whether to keep + the explicit dimension (`n`) parameter is decided at fold-in time. + - Overlap with OpenGALib: the audit found 0 `opengalib-dup` — our library sits + directly on Mathlib's manifold machinery doing metric-layer-and-up content; + the submanifold/immersion/coordinate-ball layer Lee covers, we lack entirely. + The one interface contact point: `GeometricMeasureTheory/Varifold.lean`'s + `LocalSmoothEmbeddingWitness` placeholder structure, which the embedded- + submanifold theory should sit under and replace once ported. +4. **No sorry in the trunk.** Files with sorry either get proved first, or, if + the statement layer itself contains sorry (e.g. Chap04's + `rankAt`/`HasConstantRank`), the whole block is deferred. +5. **Normalize landing targets.** The per-agent `targetModule` suggestions below + vary in path style (`Riemannian/Manifold/…`, `Riemannian/Submanifold/…`, + etc.); in practice they converge into one top-level manifold domain + (`OpenGALib/Manifold/`, established by #65), sitting below `Riemannian` and + `GeometricMeasureTheory`. +6. Toolchain first: the staged code used Lean v4.30.0 stable, we were on rc2 — + align before the first wave. (Resolved: both now on v4.30.0-rc2.) + +## Shared abstraction layers + +The two sides each implemented half of the same facilities (us: +metric/measure-facing; them: topology/embedding-facing). On merge the following +five layers become shared modules in the trunk, with each side's upper layers +importing them: + +| Facility layer | OpenGALib has | Staged branch provides | Notes | |---|---|---|---| -| 流形打包类 | `SmoothManifold M`、`RiemannianManifold M` | `TopologicalManifold n M`、`SmoothManifoldWithBoundary n M` | 收编为一条谱系；**带边支持是我们的空白，且是 GMT 散度定理的前提** | -| 图卡演算 | `Riemannian/Volume/Util/ChartOverlap.lean`、`ChartTransition.lean` | 坐标球、居中图卡、预紧坐标球、欧氏切片坐标 | 同源设施各写一半，应独立成共用 `Charts` 模块，从 `Volume/Util/` 迁出 | -| 截断/单位分解 | `Riemannian/Manifold/BumpFunction.lean` | 环形截断、单位分解存在性、穷竭函数 | 都在包装同批 Mathlib 原语，合并为一个平滑化模块 | -| 切丛局部化 | `Riemannian/TangentBundle/TangentSmooth.lean`（`trivAt` 判据） | 切丛平凡化、点导子、曲线速度 | 跟施工顺序第 4 站走 | -| 子流形抽象 | `Varifold.lean` 的 `LocalSmoothEmbeddingWitness`（临时证人） | `IsEmbeddedSubmanifold` + 切片图卡理论 | 跟施工顺序第 2 站走，移植后替换证人结构 | +| Manifold bundled classes | `SmoothManifold M`, `RiemannianManifold M` | `TopologicalManifold n M`, `SmoothManifoldWithBoundary n M` | fold into one lineage; **boundary support is a gap of ours, and a prerequisite for the GMT divergence theorem** | +| Chart calculus | `Riemannian/Volume/Util/ChartOverlap.lean`, `ChartTransition.lean` | coordinate balls, centered charts, precompact coordinate balls, Euclidean slice coordinates | same-origin facilities, half each; should become a shared `Charts` module, moved out of `Volume/Util/` | +| Cutoff / partition of unity | `Riemannian/Manifold/BumpFunction.lean` | annular cutoff, partition-of-unity existence, exhaustion functions | both wrap the same batch of Mathlib primitives; merge into one smoothing module | +| Tangent-bundle localization | `Riemannian/TangentBundle/TangentSmooth.lean` (`trivAt` criterion) | tangent-bundle trivialization, point derivations, curve velocity | follows construction-order stop 4 | +| Submanifold abstraction | `Varifold.lean`'s `LocalSmoothEmbeddingWitness` (placeholder) | `IsEmbeddedSubmanifold` + slice-chart theory | follows construction-order stop 2; replaces the witness structure once ported | -设施层 1–3 小、基本无 sorry、两边消费者均已存在，适合作为第一批合并内容，priority 高于按章节移植。 +Layers 1–3 are small, mostly sorry-free, and have consumers on both sides +already — good as the first merge batch, higher priority than chapter-ordered +porting. -## 施工台账 +## Construction ledger -流程见 `PLAN.md`（领单改状态、一单一 `port/` 分支、质量门、销单）。施工单按依赖序排列；标注"可并行"的单之间无依赖。 +Process: see `PLAN.md` (claim → update status, one branch per `port/` item, +quality gates, sign-off). Items are listed in dependency order; "parallel-OK" +items have no dependency between them. -| # | 施工单 | 内容 | 依赖 | 状态 | +| # | Item | Content | Deps | Status | |---|---|---|---|---| -| 1 | `port/manifold-typeclass-core` | 设施层 1：打包类谱系合并（`TopologicalManifold n M`、带边流形类收编进 `SmoothManifold M` 谱系；Chap01 Sec01/Sec01_06） | — | todo | -| 2 | `port/charts` | 设施层 2：图卡演算共用模块（坐标球、居中图卡 + 现有 `ChartOverlap`/`ChartTransition` 迁出合并） | #1 | todo | -| 3 | `port/cutoffs` | 设施层 3：截断/单位分解/穷竭函数并入 `BumpFunction` 体系（Chap02 Sec02_10/11 高价值条目） | #1 | todo（与 #2 可并行） | -| 4 | `port/embedded-submanifold` | 设施层 5 上半：`IsEmbeddedSubmanifold` + 图论式子流形 API（Chap05 Sec05_28） | #2 | todo | -| 5 | `port/slice-charts` | 设施层 5 下半：切片定理基础设施（`Theorem_5_8/` 全家 + Sec05_29） | #4 | todo | -| 6 | `port/submersion-covering` | 浸没/浸入/覆盖映射（Chap04 Sec04_25/26 高价值簇） | #2 | todo（与 #4–5 可并行） | -| 7 | `port/tangent-localization` | 设施层 4：切丛局部化（平凡化、点导子、曲线速度；Chap03 高价值条目） | #1 | todo（与 #2–6 可并行） | -| 8 | `port/varifold-witness-swap` | `LocalSmoothEmbeddingWitness` 替换为子流形理论 | #5 | todo | -| 9 | （按需）medium 条目 | 见各章节"可考虑"表 | 视条目 | backlog | +| 1 | `port/manifold-typeclass-core` | Layer 1: bundled-class lineage merge (`TopologicalManifold n M`, boundary-manifold class into the `SmoothManifold M` lineage; Chap01 Sec01/Sec01_06) | — | todo | +| 2 | `port/charts` | Layer 2: chart-calculus shared module (coordinate balls, centered charts + existing `ChartOverlap`/`ChartTransition` moved out and merged) | #1 | todo | +| 3 | `port/cutoffs` | Layer 3: cutoff / partition of unity / exhaustion into the `BumpFunction` system (Chap02 Sec02_10/11 high-value items) | #1 | todo (parallel with #2) | +| 4 | `port/embedded-submanifold` | Layer 5 upper half: `IsEmbeddedSubmanifold` + graph-style submanifold API (Chap05 Sec05_28) | #2 | todo | +| 5 | `port/slice-charts` | Layer 5 lower half: slice-theorem infrastructure (`Theorem_5_8/` family + Sec05_29) | #4 | todo | +| 6 | `port/submersion-covering` | submersion / immersion / covering maps (Chap04 Sec04_25/26 high-value cluster) | #2 | todo (parallel with #4–5) | +| 7 | `port/tangent-localization` | Layer 4: tangent-bundle localization (trivialization, point derivations, curve velocity; Chap03 high-value items) | #1 | todo (parallel with #2–6) | +| 8 | `port/varifold-witness-swap` | replace `LocalSmoothEmbeddingWitness` with the submanifold theory | #5 | todo | +| 9 | (on demand) medium items | see each chapter's "Consider" table | per item | backlog | -前置事项（不占施工单）：工具链对齐 v4.30.0 正式版。 +Prerequisite (not a work item): align toolchain to v4.30.0. -### 实际 PR 波次（2026-06-14，LehengChen） +### Actual PR wave (2026-06-14, LehengChen) -LehengChen 自行做了更细的分解（栈式 PR，不完全对应上表）。实际状态以此为准： +LehengChen made his own finer-grained decomposition (a stacked PR chain, not a +strict match to the table above). Actual status takes precedence: -| PR | 分支 | 内容 | 状态 | +| PR | Branch | Content | Status | |---|---|---|---| -| #65 | `port/coordinate-ball` | 坐标球图卡谓词 | **已合并 develop**（注释经 house-style 修订 db767b1，作为范本） | -| #66 | `port/precompact-basis` | 预紧坐标球可数基 + 局部有限加细 | open，待反馈：base 改 develop、注释回炉 | -| #67 | `port/charted-space-core` | 由图册核造流形 | open，同上 | -| #68 | `port/exhaustion-cutoff` | 穷竭函数 + 局部光滑 + 单位分解⇒仿紧 | open，同上 | -| #69 | `port/curve-velocity-mfderiv` | 曲线速度 + mfderiv（含 snake_case def 待改名） | open，同上 | -| #70 | `port/coordinate-components` | 坐标切向量分量（含 snake_case def；内联了 `tangent_coordinates_change`） | open，同上 | +| #65 | `port/coordinate-ball` | coordinate-ball chart predicates | **merged to develop** (docstrings house-style-revised in db767b1, serves as the exemplar) | +| #66 | `port/precompact-basis` | precompact coordinate-ball countable basis + locally-finite refinement | open, pending feedback: retarget base to develop, revise docstrings | +| #67 | `port/charted-space-core` | manifold from a chart-family core | open, same | +| #68 | `port/exhaustion-cutoff` | exhaustion functions + local smoothness + partition-of-unity ⇒ paracompact | open, same | +| #69 | `port/curve-velocity-mfderiv` | curve velocity + mfderiv (has snake_case defs to rename) | open, same | +| #70 | `port/coordinate-components` | coordinate tangent components (has snake_case defs; inlines `tangent_coordinates_change`) | open, same | -反馈共性（指向已合并的 #65 为范本）：①注释 house style（单 Math 标签 / 架构叙事 / 出处脚注）；②定理的 Eng 行勿复述证明；③snake_case def 改 lowerCamelCase；④#65 合并后 base 重定向 develop。 +Common feedback (pointing at merged #65 as the exemplar): ① docstring house +style (single Math tags / architecture narrative / provenance footer); ② +theorem Eng-lines must not narrate proofs; ③ snake_case defs → lowerCamelCase; +④ retarget base to develop now that #65 is merged. -## 补审：深层子目录文件（批量审计遗漏，已补） +## Follow-up audit: deep-subdirectory files (missed by the batch audit, now added) -| 文件 | 主要声明 | 分类 | 价值 | sorry | 理由 | +| File | Main declarations | Class | Value | sorry | Rationale | |------|----------|------|------|-------|------| -| Chap05/Sec05_29/Theorem_5_8/Common.lean | euclidean_slice_projection 等 27 条 | new | high | 否 | 欧氏切片几何与图卡居中基础设施 | -| Chap05/Sec05_29/Theorem_5_8/Index.lean | 重导出 | new | medium | 否 | 索引文件 | -| Chap05/Sec05_29/Theorem_5_8/LocalNormalFormAPI.lean | rank_normal_form 等 | partial-dup | medium | 否 | 包装 Mathlib 浸入正规形式，桥接第 4 章秩形式 | -| Chap05/Sec05_29/Theorem_5_8/LocalSliceAtlas.lean | slice_condition_chartAt 等 30+ 条 | new | high | 否 | 切片条件图册构造核心 | -| Chap05/Sec05_29/Theorem_5_8/LocalSliceImmersion.lean | local_slice_condition_has_embedded_submanifold_structure 等 11 条 | new | high | 否 | 切片上嵌入子流形结构的完成步 | -| Chap05/Sec05_36/Theorem_5_51/EuclideanHalfSlice.lean | euclidean_half_slice_projection_partial_homeomorph | new | medium | 是 | 半切片边界图卡的半成品 | -| Chap05/Sec05_36/Theorem_5_51/Index.lean | 重导出 | new | low | 是 | 下游未实现 | +| Chap05/Sec05_29/Theorem_5_8/Common.lean | euclidean_slice_projection etc., 27 decls | new | high | no | Euclidean slice geometry and chart-centering infrastructure | +| Chap05/Sec05_29/Theorem_5_8/Index.lean | re-exports | new | medium | no | index file | +| Chap05/Sec05_29/Theorem_5_8/LocalNormalFormAPI.lean | rank_normal_form etc. | partial-dup | medium | no | wraps Mathlib immersion normal form, bridges Ch4 rank form | +| Chap05/Sec05_29/Theorem_5_8/LocalSliceAtlas.lean | slice_condition_chartAt etc., 30+ decls | new | high | no | core of the slice-condition atlas construction | +| Chap05/Sec05_29/Theorem_5_8/LocalSliceImmersion.lean | local_slice_condition_has_embedded_submanifold_structure etc., 11 decls | new | high | no | completion step for the embedded-submanifold structure on slices | +| Chap05/Sec05_36/Theorem_5_51/EuclideanHalfSlice.lean | euclidean_half_slice_projection_partial_homeomorph | new | medium | yes | half-slice boundary chart, half-finished | +| Chap05/Sec05_36/Theorem_5_51/Index.lean | re-exports | new | low | yes | downstream unimplemented | --- # Chap01 -## 移植优先（high，10 项） +## Port priority (high, 10 items) -| 文件 | 声明 | 分类 | 落点 | sorry | 理由 | +| File | Declarations | Class | Target | sorry | Rationale | |---|---|---|---|---|---| -| Sec01/Definition_1_extra_2.lean | IsCoordinateBall, centerAt 等 | new | Manifold/Charts | 否 | 坐标球/盒卡形谓词，Mathlib 缺，坐标球栈基础 | -| Sec01/Example_1_5.lean | RealProjectiveSpace, realProjectiveChart 等 | new | Instances/ProjectiveSpace | 否 | RP^n 商拓扑与标准仿射卡，Mathlib 完全缺失 | -| Sec01/Example_1_8.lean | contDiffGroupoid_pi, instIsManifoldPi 等 | new | Instances/Pi | 否 | 有限乘积 IsManifold 实例，补 Mathlib 已注明缺口 | -| Sec01/Lemma_1_10.lean | isTopologicalBasis_isPrecompactCoordinateBall 等 | new | Manifold/Charts | 否 | 预紧坐标球可数基，单位分解/穷竭列底层 | -| Sec01_03/Definition_1_3_extra_1.lean | IsSmoothCoordinateBall, IsRegularCoordinateBall 等 | new | Manifold/CoordinateBall | 否 | 光滑/正则坐标球谓词全证，需脱离项目内依赖 | -| Sec01_04/Example_1_32.lean | regular_level_set_smooth_structure 等 | new | Manifold/RegularLevelSet | 否 | 正则水平集定理 1750 行全证，Mathlib 无正则值定理 | -| Sec01_04/Lemma_1_35.lean | ChartedSpaceCore.toTopologicalSpace_t2Space, toChartedSpace_isManifold 等 | new | Manifold/ChartedSpaceCore | 否 | 由图册造流形的 T2/二可数/光滑判据，Mathlib 缺 | -| Sec01_06/Exercise_1_42.lean | IsRegularCoordinateHalfBall 等 | new | Manifold/CoordinateBalls | 是 | 正则坐标(半)球可数基，三定理全 sorry | -| Sec01_07/Problem_1_9.lean | ComplexProjectiveSpace, complexProjectiveSpaceIsManifold 等 | new | Instances/ComplexProjectiveSpace | 否 | CP^n 完整流形结构无 sorry，Fubini-Study 宿主 | -| Sec01_05/Proposition_1_40.lean | IsBoundaryModelCoordinateBall, countable_fundamentalGroup 等 | partial-dup | Manifold/CoordinateBall | 是 | 半球基与可数基本群为缺口，拓扑推论 Mathlib 已有，全 sorry | - -
可考虑（medium，21 项） - -| 文件 | 声明 | 分类 | 落点 | sorry | 理由 | +| Sec01/Definition_1_extra_2.lean | IsCoordinateBall, centerAt, etc. | new | Manifold/Charts | no | Coordinate-ball/box-chart predicates, missing in Mathlib, foundation of the coordinate-ball stack | +| Sec01/Example_1_5.lean | RealProjectiveSpace, realProjectiveChart, etc. | new | Instances/ProjectiveSpace | no | RP^n quotient topology and standard affine charts, completely absent from Mathlib | +| Sec01/Example_1_8.lean | contDiffGroupoid_pi, instIsManifoldPi, etc. | new | Instances/Pi | no | Finite-product IsManifold instance, fills a gap Mathlib already flags | +| Sec01/Lemma_1_10.lean | isTopologicalBasis_isPrecompactCoordinateBall, etc. | new | Manifold/Charts | no | Countable basis of precompact coordinate balls, underpins partitions of unity / exhaustion sequences | +| Sec01_03/Definition_1_3_extra_1.lean | IsSmoothCoordinateBall, IsRegularCoordinateBall, etc. | new | Manifold/CoordinateBall | no | Smooth/regular coordinate-ball predicates, fully proved, needs decoupling from in-project dependencies | +| Sec01_04/Example_1_32.lean | regular_level_set_smooth_structure, etc. | new | Manifold/RegularLevelSet | no | Regular-level-set theorem, 1750 lines fully proved, Mathlib has no regular value theorem | +| Sec01_04/Lemma_1_35.lean | ChartedSpaceCore.toTopologicalSpace_t2Space, toChartedSpace_isManifold, etc. | new | Manifold/ChartedSpaceCore | no | T2/second-countable/smooth criteria for building a manifold from an atlas, missing in Mathlib | +| Sec01_06/Exercise_1_42.lean | IsRegularCoordinateHalfBall, etc. | new | Manifold/CoordinateBalls | yes | Countable basis of regular coordinate (half-)balls, all three theorems sorry | +| Sec01_07/Problem_1_9.lean | ComplexProjectiveSpace, complexProjectiveSpaceIsManifold, etc. | new | Instances/ComplexProjectiveSpace | no | Complete CP^n manifold structure with no sorry, host for Fubini-Study | +| Sec01_05/Proposition_1_40.lean | IsBoundaryModelCoordinateBall, countable_fundamentalGroup, etc. | partial-dup | Manifold/CoordinateBall | yes | Half-ball basis and countable fundamental group are the gaps, topological corollaries already in Mathlib, all sorry | + +
Consider (medium, 21 items) + +| File | Declarations | Class | Target | sorry | Rationale | |---|---|---|---|---|---| -| Sec01/Exercise_1_1.lean | HasCoordinateBallCharts 等 | new | Manifold/Charts | 否 | 卡收缩/拉直引理完整，存在式陈述需重构 | -| Sec01/Exercise_1_6.lean | realProjectiveSpace_t2Space 等 | new | Instances/ProjectiveSpace | 是 | 补 Example_1_5 所需 T2/二可数，四条全 sorry | -| Sec01/Exercise_1_7.lean | realProjectiveSpaceCompactSpace | new | Instances/ProjectiveSpace | 否 | RP^n 紧性全证，宜随 Example_1_5 一并移植 | -| Sec01_03/Proposition_1_19.lean | exists_countable_regular_coordinate_ball_basis 等 | new | Manifold/CoordinateBall | 是 | 正则坐标球可数基有用，证明 sorry 且打包需重构 | -| Sec01_04/Example_1_30.lean | graph_coordinate_chart, graph_charted_space 等 | new | Manifold/GraphChart | 是 | 光滑映射图卡空间为缺口，关键引理 sorry | -| Sec01_04/Example_1_33.lean | realProjectiveSpaceIsManifold, realProjectiveChartTransitionDiffeomorph 等 | new | Instances/RealProjectiveSpace | 否 | ℝPⁿ 光滑结构全证，需先移上游 Example_1_5 | -| Sec01_06/Definition_1_6_extra_1.lean | contMDiffOn_halfSpace_iff_forall_exists_smoothAmbientExtension 等 | new | Manifold/HalfSpaceExtension | 是 | 半空间环境延拓光滑判据，关键边界引理 sorry | -| Sec01_06/Definition_1_6_extra_3.lean | IsSmoothCoordinateHalfBall 等 | new | Manifold/CoordinateBalls | 是 | 与 Exercise_1_42 定义重叠，需先合并 API | -| Sec01_07/Problem_1_10.lean | problem_1_10_chart_matrix, block_column_subspace 等 | new | GeometricMeasureTheory/Grassmannian/Charts | 是 | Grassmann 矩阵坐标可喂 varifold，主定理全 sorry | -| Sec01_07/Problem_1_11.lean | closed_unit_ball_smoothManifoldWithBoundary 等 | new | SmoothManifold/ClosedBall | 是 | 闭球带边流形补缺口，关键定理 sorry，图册取自 Problem_2_4 | -| Sec01_07/Problem_1_5.lean | sigmaCompactSpace_of_connected_paracompact_locallyCompact_t2 等 | new | Manifold/Paracompactness | 否 | 仿紧⇒σ紧逆向及二可数刻画，Mathlib 仅有正向 | -| Sec01_07/Problem_1_6.lean | supportedRadialTwistHomeomorph, exists_uncountably_many_distinct_smooth_structures 等 | new | Manifold/SmoothStructures | 否 | 不可数多光滑结构全证，多为单定理脚手架 | -| Sec01/Definition_1_extra_1.lean | TopologicalManifold, dimension_eq 等 | partial-dup | Manifold/TopologicalManifold | 是 | C⁰流形打包类，多为包装且维数不变 sorry | -| Sec01/Example_1_3.lean | graphMap, graph_coordinates 等 | partial-dup | Manifold/Charts | 否 | 打包同胚 graphOn≃ₜU 为 Mathlib 缺，GMT 图参数化常用 | -| Sec01/Theorem_1_15.lean | exists_countable_locallyFinite_refinement_of_isTopologicalBasis 等 | partial-dup | Manifold/Charts | 否 | 预紧坐标球可数局部有限加细，喂单位分解 | -| Sec01_02/Definition_1_2_extra_3.lean | IsSmoothAtlas 等 | partial-dup | SmoothManifold/Atlas | 否 | 不依实例的图册谓词为新，属小众脚手架 | -| Sec01_02/Proposition_1_17.lean | same_smooth_structure_iff_union_is_smooth_atlas 等 | partial-dup | SmoothManifold/Atlas | 否 | 并集判同光滑结构为新，letI 陈述需重构 | -| Sec01_04/Example_1_36.lean | grassmannian, grassmannian.chart_equiv 等 | partial-dup | Instances/Grassmannian | 是 | Grassmann 卡双射缺口，非平凡引理全 sorry | -| Sec01_05/Proposition_1_38.lean | boundaryChart, boundaryTopologicalManifold 等 | partial-dup | Manifold/InteriorBoundary | 是 | 边界作(n-1)流形构造，近全 sorry 且绑定专有模型 | -| Sec01_06/Exercise_1_44.lean | ModelWithCorners.interiorOpens 等 | partial-dup | Manifold/InteriorBoundary | 否 | 内部为无边开子流形等小引理，补全边界设施 | -| Sec01_06/Theorem_1_46.lean | isInteriorPoint_iff_of_mem_maximalAtlas 等 | partial-dup | Manifold/InteriorBoundary | 否 | 边界检测推广到极大图册卡，全证 | +| Sec01/Exercise_1_1.lean | HasCoordinateBallCharts, etc. | new | Manifold/Charts | no | Chart-shrinking/straightening lemmas complete, existential statements need restructuring | +| Sec01/Exercise_1_6.lean | realProjectiveSpace_t2Space, etc. | new | Instances/ProjectiveSpace | yes | Supplies the T2/second-countability needed by Example_1_5, all four sorry | +| Sec01/Exercise_1_7.lean | realProjectiveSpaceCompactSpace | new | Instances/ProjectiveSpace | no | RP^n compactness fully proved, best ported together with Example_1_5 | +| Sec01_03/Proposition_1_19.lean | exists_countable_regular_coordinate_ball_basis, etc. | new | Manifold/CoordinateBall | yes | Countable basis of regular coordinate balls is useful, proof has sorry and packaging needs restructuring | +| Sec01_04/Example_1_30.lean | graph_coordinate_chart, graph_charted_space, etc. | new | Manifold/GraphChart | yes | Graph chart space of a smooth map is the gap, key lemma sorry | +| Sec01_04/Example_1_33.lean | realProjectiveSpaceIsManifold, realProjectiveChartTransitionDiffeomorph, etc. | new | Instances/RealProjectiveSpace | no | ℝPⁿ smooth structure fully proved, requires porting upstream Example_1_5 first | +| Sec01_06/Definition_1_6_extra_1.lean | contMDiffOn_halfSpace_iff_forall_exists_smoothAmbientExtension, etc. | new | Manifold/HalfSpaceExtension | yes | Half-space ambient-extension smoothness criterion, key boundary lemma sorry | +| Sec01_06/Definition_1_6_extra_3.lean | IsSmoothCoordinateHalfBall, etc. | new | Manifold/CoordinateBalls | yes | Definition overlaps with Exercise_1_42, API must be merged first | +| Sec01_07/Problem_1_10.lean | problem_1_10_chart_matrix, block_column_subspace, etc. | new | GeometricMeasureTheory/Grassmannian/Charts | yes | Grassmann matrix coordinates can feed varifolds, main theorem all sorry | +| Sec01_07/Problem_1_11.lean | closed_unit_ball_smoothManifoldWithBoundary, etc. | new | SmoothManifold/ClosedBall | yes | Closed-ball manifold-with-boundary fills a gap, key theorem sorry, atlas taken from Problem_2_4 | +| Sec01_07/Problem_1_5.lean | sigmaCompactSpace_of_connected_paracompact_locallyCompact_t2, etc. | new | Manifold/Paracompactness | no | Paracompact⇒σ-compact converse and second-countability characterization, Mathlib only has the forward direction | +| Sec01_07/Problem_1_6.lean | supportedRadialTwistHomeomorph, exists_uncountably_many_distinct_smooth_structures, etc. | new | Manifold/SmoothStructures | no | Uncountably many smooth structures fully proved, mostly single-theorem scaffolding | +| Sec01/Definition_1_extra_1.lean | TopologicalManifold, dimension_eq, etc. | partial-dup | Manifold/TopologicalManifold | yes | C⁰-manifold packaging class, mostly wrappers and dimension invariance sorry | +| Sec01/Example_1_3.lean | graphMap, graph_coordinates, etc. | partial-dup | Manifold/Charts | no | Packaged homeomorphism graphOn≃ₜU missing in Mathlib, commonly used for GMT graph parametrization | +| Sec01/Theorem_1_15.lean | exists_countable_locallyFinite_refinement_of_isTopologicalBasis, etc. | partial-dup | Manifold/Charts | no | Countable locally-finite refinement of precompact coordinate balls, feeds partitions of unity | +| Sec01_02/Definition_1_2_extra_3.lean | IsSmoothAtlas, etc. | partial-dup | SmoothManifold/Atlas | no | Instance-free atlas predicate is new, niche scaffolding | +| Sec01_02/Proposition_1_17.lean | same_smooth_structure_iff_union_is_smooth_atlas, etc. | partial-dup | SmoothManifold/Atlas | no | Union criterion for same smooth structure is new, letI statement needs restructuring | +| Sec01_04/Example_1_36.lean | grassmannian, grassmannian.chart_equiv, etc. | partial-dup | Instances/Grassmannian | yes | Grassmann chart bijection is the gap, nontrivial lemma all sorry | +| Sec01_05/Proposition_1_38.lean | boundaryChart, boundaryTopologicalManifold, etc. | partial-dup | Manifold/InteriorBoundary | yes | Construction of the boundary as an (n-1)-manifold, nearly all sorry and bound to a proprietary model | +| Sec01_06/Exercise_1_44.lean | ModelWithCorners.interiorOpens, etc. | partial-dup | Manifold/InteriorBoundary | no | Small lemma that the interior is a boundaryless open submanifold, fills out boundary infrastructure | +| Sec01_06/Theorem_1_46.lean | isInteriorPoint_iff_of_mem_maximalAtlas, etc. | partial-dup | Manifold/InteriorBoundary | no | Boundary detection generalized to maximal-atlas charts, fully proved |
-
跳过（44 项，绝大多数为 Mathlib 包装/recall 文件） - -- Sec01/Definition_1_extra_3.lean — mathlib-dup — 纯 recall 类型类 -- Sec01/Definition_1_extra_4.lean — mathlib-dup — recall 加薄包装 -- Sec01/Example_1_4.lean — mathlib-dup — 球面实例一行复包 -- Sec01/Example_1_9.lean — new — 平凡 abbrev -- Sec01/Exercise_1_14.lean — mathlib-dup — 纯 recall -- Sec01/Lemma_1_13.lean — mathlib-dup — 与 Exercise_1_14 重复 -- Sec01/Proposition_1_11.lean — partial-dup — recall 加实例装配 -- Sec01/Proposition_1_12.lean — mathlib-dup — 纯 recall 包装 -- Sec01/Proposition_1_16.lean — new — 一行 simpa 引 1.40 -- Sec01/Theorem_1_2.lean — new — recall 项目 sorry 定理 -- Sec01_02/Definition_1_2_extra_1.lean — mathlib-dup — #check 指针 -- Sec01_02/Definition_1_2_extra_2.lean — partial-dup — 两行包装 -- Sec01_02/Definition_1_2_extra_4.lean — mathlib-dup — recall 指针 -- Sec01_02/Definition_1_2_extra_5.lean — mathlib-dup — rfl 即得且 sorry -- Sec01_02/Exercise_1_18.lean — mathlib-dup — 零声明指针 -- Sec01_02/Remark_1_2_extra_6.lean — mathlib-dup — recall 指针 -- Sec01_03/Exercise_1_20.lean — new — 复述 1.19 无新声明 +
Skip (44 items — mostly Mathlib wrappers / recall files) + +- Sec01/Definition_1_extra_3.lean — mathlib-dup — pure recall typeclass +- Sec01/Definition_1_extra_4.lean — mathlib-dup — recall plus thin wrapper +- Sec01/Example_1_4.lean — mathlib-dup — one-line re-wrap of the sphere instance +- Sec01/Example_1_9.lean — new — trivial abbrev +- Sec01/Exercise_1_14.lean — mathlib-dup — pure recall +- Sec01/Lemma_1_13.lean — mathlib-dup — duplicates Exercise_1_14 +- Sec01/Proposition_1_11.lean — partial-dup — recall plus instance assembly +- Sec01/Proposition_1_12.lean — mathlib-dup — pure recall wrapper +- Sec01/Proposition_1_16.lean — new — one-line simpa citing 1.40 +- Sec01/Theorem_1_2.lean — new — recall of an in-project sorry theorem +- Sec01_02/Definition_1_2_extra_1.lean — mathlib-dup — #check pointer +- Sec01_02/Definition_1_2_extra_2.lean — partial-dup — two-line wrapper +- Sec01_02/Definition_1_2_extra_4.lean — mathlib-dup — recall pointer +- Sec01_02/Definition_1_2_extra_5.lean — mathlib-dup — rfl-provable and sorry +- Sec01_02/Exercise_1_18.lean — mathlib-dup — zero-declaration pointer +- Sec01_02/Remark_1_2_extra_6.lean — mathlib-dup — recall pointer +- Sec01_03/Exercise_1_20.lean — new — restates 1.19 with no new declarations - Sec01_03/Notation_1_3_extra_2.lean — mathlib-dup — extChartAt recall -- Sec01_04/Example_1_21.lean — partial-dup — 离散流形薄装配 -- Sec01_04/Example_1_22.lean — mathlib-dup — sorry 复述实例 -- Sec01_04/Example_1_23.lean — new — 一次性反例无 API -- Sec01_04/Example_1_24.lean — mathlib-dup — 薄组合/#check -- Sec01_04/Example_1_25.lean — mathlib-dup — 一行推论加 #check -- Sec01_04/Example_1_26.lean — mathlib-dup — 纯 #check -- Sec01_04/Example_1_27.lean — mathlib-dup — #check 加 sorry 辅理 -- Sec01_04/Example_1_28.lean — partial-dup — 关键开性 sorry -- Sec01_04/Example_1_29.lean — mathlib-dup — 两步推论 -- Sec01_04/Example_1_31.lean — mathlib-dup — 球面实例 #check -- Sec01_04/Example_1_34.lean — mathlib-dup — 复述乘积实例 -- Sec01_04/Notation_1_4_extra_1.lean — mathlib-dup — 记号对照 #check -- Sec01_05/Definition_1_5_extra_1.lean — partial-dup — 半空间模型笨拙打包 -- Sec01_05/Exercise_1_39.lean — mathlib-dup — 零声明 #check -- Sec01_05/Exercise_1_41.lean — partial-dup — 纯指针文件 -- Sec01_05/Theorem_1_37.lean — mathlib-dup — 单条 recall -- Sec01_06/Definition_1_6_extra_2.lean — mathlib-dup — 类复包 Mathlib -- Sec01_06/Exercise_1_43.lean — mathlib-dup — 零声明 #check -- Sec01_06/Proposition_1_45.lean — mathlib-dup — 纯 recall -- Sec01_07/Problem_1_1.lean — new — 双原点反例无 API -- Sec01_07/Problem_1_12.lean — mathlib-dup — infer_instance 直调 -- Sec01_07/Problem_1_2.lean — partial-dup — 习题级薄组合 -- Sec01_07/Problem_1_3.lean — mathlib-dup — 双向薄包装 -- Sec01_07/Problem_1_4.lean — new — 近平凡引理加反例 -- Sec01_07/Problem_1_7.lean — mathlib-dup — 重造球极图册多 sorry -- Sec01_07/Problem_1_8.lean — partial-dup — 圆专用习题 +- Sec01_04/Example_1_21.lean — partial-dup — thin assembly of a discrete manifold +- Sec01_04/Example_1_22.lean — mathlib-dup — sorry restatement of an instance +- Sec01_04/Example_1_23.lean — new — one-off counterexample with no API +- Sec01_04/Example_1_24.lean — mathlib-dup — thin combination / #check +- Sec01_04/Example_1_25.lean — mathlib-dup — one-line corollary plus #check +- Sec01_04/Example_1_26.lean — mathlib-dup — pure #check +- Sec01_04/Example_1_27.lean — mathlib-dup — #check plus sorry helper lemma +- Sec01_04/Example_1_28.lean — partial-dup — key openness sorry +- Sec01_04/Example_1_29.lean — mathlib-dup — two-step corollary +- Sec01_04/Example_1_31.lean — mathlib-dup — #check on the sphere instance +- Sec01_04/Example_1_34.lean — mathlib-dup — restatement of the product instance +- Sec01_04/Notation_1_4_extra_1.lean — mathlib-dup — notation cross-reference #check +- Sec01_05/Definition_1_5_extra_1.lean — partial-dup — clumsy packaging of the half-space model +- Sec01_05/Exercise_1_39.lean — mathlib-dup — zero-declaration #check +- Sec01_05/Exercise_1_41.lean — partial-dup — pure pointer file +- Sec01_05/Theorem_1_37.lean — mathlib-dup — single recall +- Sec01_06/Definition_1_6_extra_2.lean — mathlib-dup — class-style re-wrap of Mathlib +- Sec01_06/Exercise_1_43.lean — mathlib-dup — zero-declaration #check +- Sec01_06/Proposition_1_45.lean — mathlib-dup — pure recall +- Sec01_07/Problem_1_1.lean — new — line-with-two-origins counterexample with no API +- Sec01_07/Problem_1_12.lean — mathlib-dup — direct infer_instance call +- Sec01_07/Problem_1_2.lean — partial-dup — exercise-level thin combination +- Sec01_07/Problem_1_3.lean — mathlib-dup — bidirectional thin wrapper +- Sec01_07/Problem_1_4.lean — new — near-trivial lemma plus counterexample +- Sec01_07/Problem_1_7.lean — mathlib-dup — rebuilds the stereographic atlas, many sorry +- Sec01_07/Problem_1_8.lean — partial-dup — circle-specific exercise
-## 小结 +## Summary -第一章共审计 75 个文件，约六成是对 Mathlib 既有结果的 recall、#check 或薄封装，可直接跳过。真正值得移植的核心资产集中在两条线：一是坐标球/覆盖基础设施（坐标球谓词、预紧坐标球可数基、正则坐标(半)球），它们是单位分解、穷竭列与 GMT 覆盖论证的底层；二是实例级缺口（RP^n、CP^n 的完整流形结构、有限乘积 IsManifold 实例、正则水平集定理、ChartedSpaceCore 构造引理），均为 Mathlib 公认空白且大多 sorry-free。中等价值条目多数受 sorry 残留或项目内部依赖（TopologicalManifold 类、LeeBoundaryModelSpace）牵制，移植前需先做 API 重构与依赖消解。 +Chapter 1 audits 75 files in total; about sixty percent are recall, #check, or thin wrappers around existing Mathlib results and can be skipped outright. The assets genuinely worth porting cluster along two lines: first, the coordinate-ball / covering infrastructure (coordinate-ball predicates, countable basis of precompact coordinate balls, regular coordinate (half-)balls), which underpins partitions of unity, exhaustion sequences, and GMT covering arguments; second, instance-level gaps (complete manifold structures for RP^n and CP^n, the finite-product IsManifold instance, the regular-level-set theorem, the ChartedSpaceCore construction lemmas), all acknowledged Mathlib blanks and mostly sorry-free. Most medium-value entries are held back by residual sorry or in-project dependencies (the TopologicalManifold class, LeeBoundaryModelSpace) and require API restructuring and dependency resolution before porting. + +--- --- # Chap02 -## 移植优先（high，4 项） +## Port priority (high, 4 items) -| 文件 | 声明 | 分类 | 落点 | sorry | 理由 | +| File | Declarations | Class | Target | sorry | Rationale | |---|---|---|---|---|---| -| Sec02_12/Problem_2_4.lean | closed_unit_ball_fixed_atlas, split_at_coordinate 等 | new | Instances/ClosedBall | 否 | 闭球带边流形 2600 行无 sorry，直撑 GMT 散度定理 | -| Sec02_11/Proposition_2_28.lean | exists_positive_smooth_exhaustion_function | new | Manifold/Exhaustion | 否 | 正光滑穷竭函数全证，非紧 L²/Bochner/GMT 所需 | -| Sec02_09/Example_2_14.lean | unitOpenBallDiffeomorph, smoothChartDiffeomorph 等 | partial-dup | Manifold/Diffeomorph | 否 | 打包单位球≃ℝⁿ与卡微分同胚，Mathlib 仅散装引理 | -| Sec02_09/Proposition_2_15.lean | Diffeomorph.pi, Diffeomorph.restrictOpen 等 | partial-dup | Manifold/Diffeomorph | 是 | 乘积与开子流形限制 API 为缺口，六条辅理 sorry | +| Sec02_12/Problem_2_4.lean | closed_unit_ball_fixed_atlas, split_at_coordinate, etc. | new | Instances/ClosedBall | no | Closed-ball manifold-with-boundary, 2600 lines sorry-free, directly supports the GMT divergence theorem | +| Sec02_11/Proposition_2_28.lean | exists_positive_smooth_exhaustion_function | new | Manifold/Exhaustion | no | Positive smooth exhaustion function fully proved, required by the noncompact L²/Bochner/GMT directions | +| Sec02_09/Example_2_14.lean | unitOpenBallDiffeomorph, smoothChartDiffeomorph, etc. | partial-dup | Manifold/Diffeomorph | no | Packages unit-ball≃ℝⁿ and chart diffeomorphisms; Mathlib only has scattered lemmas | +| Sec02_09/Proposition_2_15.lean | Diffeomorph.pi, Diffeomorph.restrictOpen, etc. | partial-dup | Manifold/Diffeomorph | yes | Product and open-submanifold restriction API is a gap; six auxiliary lemmas have sorry | -
可考虑（medium，14 项） +
Consider (medium, 14 items) -| 文件 | 声明 | 分类 | 落点 | sorry | 理由 | +| File | Declarations | Class | Target | sorry | Rationale | |---|---|---|---|---|---| -| Sec02_09/Theorem_2_17.lean | Diffeomorph.dimension_eq 等 | new | Manifold/Diffeomorph | 否 | 微分同胚维数不变全证，Mathlib 缺此通用引理 | -| Sec02_11/Definition_2_11_extra_2.lean | Function.IsSmoothOn 等 | new | Manifold/SmoothExtension | 否 | 子类型域局部延拓光滑谓词，需对齐 ContMDiffOn | -| Sec02_11/Definition_2_11_extra_3.lean | Function.IsExhaustionFunction 等 | new | Manifold/Exhaustion | 否 | 穷竭函数类与 proper 引理，2.28 的 API 基础 | -| Sec02_11/Lemma_2_26.lean | exists_supported_contMDiffMap_extension_of_isClosed | new | Manifold/SmoothExtension | 是 | 闭集光滑延拓为真缺口，仅有陈述需从头证 | -| Sec02_12/Problem_2_10.lean | smooth_iff_pullback_preserves_smooth_real_functions 等 | new | Manifold/SmoothFunctionCriterion | 是 | 回拉保光滑函数判据有用，定理全 sorry | -| Sec02_12/Problem_2_11.lean | Projectivization.basisMap, BasisCompatible 等 | new | Instances/Projectivization | 是 | Projectivization 结构搬运层，关键证明 sorry 且依赖一章 | -| Sec02_12/Problem_2_13.lean | paracompactSpace_of_hasSubordinatePartitionOfUnity | new | Manifold/PartitionOfUnity | 否 | 单位分解⇒仿紧逆向全证，Mathlib 仅有正向 | -| Sec02_12/Problem_2_6.lean | projectivizationMap, contMDiff_projectivizationMap 等 | new | Manifolds/ProjectiveSpace | 否 | 齐次映射下降到 ℝPⁿ 为新，需先移项目图册 | -| Sec02_12/Problem_2_7.lean | smooth_functions_not_finiteDimensional 等 | new | Util/SmoothFunctionSpace | 否 | C^∞(M,ℝ) 无限维全证，于本库方向偏小众 | -| Sec02_08/Corollary_2_8.lean | gluing_lemma_for_smooth_maps | partial-dup | Manifold/SmoothManifold | 否 | 光滑层粘合解包为 ContMDiff 级可用陈述 | -| Sec02_08/Exercise_2_2.lean | contMDiff_open_submanifold_halfspace_iff_forall_exists_smoothAmbientExtension 等 | partial-dup | Manifold/Boundary | 否 | 半空间延拓判据真缺，需连带一章依赖文件 | -| Sec02_09/Theorem_2_18.lean | Diffeomorph.restrictInterior 等 | partial-dup | Manifold/Diffeomorph | 是 | 限制到流形内部为新，依项目内设施且 simp 引理 sorry | -| Sec02_11/Proposition_2_25.lean | exists_smooth_bump_function_for | partial-dup | Manifold/BumpFunction | 否 | 严格 tsupport⊆U 闭集 bump，可扩展本库模块 | -| Sec02_12/Problem_2_3.lean | hopf_map, hopf_map_smooth 等 | partial-dup | Instances/HopfFibration | 是 | Hopf 映射 S³→S² 为新典型例，五条证明全 sorry | +| Sec02_09/Theorem_2_17.lean | Diffeomorph.dimension_eq, etc. | new | Manifold/Diffeomorph | no | Dimension invariance under diffeomorphism fully proved; Mathlib lacks this general lemma | +| Sec02_11/Definition_2_11_extra_2.lean | Function.IsSmoothOn, etc. | new | Manifold/SmoothExtension | no | Local-extension smoothness predicate over a subtype domain; needs alignment with ContMDiffOn | +| Sec02_11/Definition_2_11_extra_3.lean | Function.IsExhaustionFunction, etc. | new | Manifold/Exhaustion | no | Exhaustion-function class plus proper lemma; the API foundation for 2.28 | +| Sec02_11/Lemma_2_26.lean | exists_supported_contMDiffMap_extension_of_isClosed | new | Manifold/SmoothExtension | yes | Smooth extension from a closed set is a genuine gap; only the statement exists, proof needed from scratch | +| Sec02_12/Problem_2_10.lean | smooth_iff_pullback_preserves_smooth_real_functions, etc. | new | Manifold/SmoothFunctionCriterion | yes | Useful criterion: pullback preserves smooth functions; theorem entirely sorry | +| Sec02_12/Problem_2_11.lean | Projectivization.basisMap, BasisCompatible, etc. | new | Instances/Projectivization | yes | Projectivization structure-transport layer; key proofs sorry and depend on Chapter 1 | +| Sec02_12/Problem_2_13.lean | paracompactSpace_of_hasSubordinatePartitionOfUnity | new | Manifold/PartitionOfUnity | no | Partition of unity ⇒ paracompact (converse) fully proved; Mathlib only has the forward direction | +| Sec02_12/Problem_2_6.lean | projectivizationMap, contMDiff_projectivizationMap, etc. | new | Manifolds/ProjectiveSpace | no | Homogeneous map descending to ℝPⁿ is new; needs the projective atlas ported first | +| Sec02_12/Problem_2_7.lean | smooth_functions_not_finiteDimensional, etc. | new | Util/SmoothFunctionSpace | no | C^∞(M,ℝ) infinite-dimensional fully proved; fairly niche for this library's direction | +| Sec02_08/Corollary_2_8.lean | gluing_lemma_for_smooth_maps | partial-dup | Manifold/SmoothManifold | no | Smooth-sheaf gluing unpacked into a usable ContMDiff-level statement | +| Sec02_08/Exercise_2_2.lean | contMDiff_open_submanifold_halfspace_iff_forall_exists_smoothAmbientExtension, etc. | partial-dup | Manifold/Boundary | no | Half-space extension criterion is a genuine gap; needs accompanying Chapter 1 dependency files | +| Sec02_09/Theorem_2_18.lean | Diffeomorph.restrictInterior, etc. | partial-dup | Manifold/Diffeomorph | yes | Restriction to manifold interior is new; depends on in-project facilities, simp lemmas sorry | +| Sec02_11/Proposition_2_25.lean | exists_smooth_bump_function_for | partial-dup | Manifold/BumpFunction | no | Bump with strict tsupport⊆U closed set; can extend this library's module | +| Sec02_12/Problem_2_3.lean | hopf_map, hopf_map_smooth, etc. | partial-dup | Instances/HopfFibration | yes | Hopf map S³→S² is a new canonical example; five proofs entirely sorry |
-
跳过（40 项，绝大多数为 Mathlib 包装/recall 文件） - -- Sec02_08/Definition_2_8_extra_2.lean — mathlib-dup — 纯 #check 复述 -- Sec02_08/Definition_2_8_extra_4.lean — mathlib-dup — 薄逐点推论 -- Sec02_08/Definition_2_8_extra_5.lean — mathlib-dup — recall 编号对照 -- Sec02_08/Definition_2_8_extra_6.lean — partial-dup — 既有 API 已覆盖 -- Sec02_08/Exercise_2_1.lean — mathlib-dup — 仅 #check 环结构 -- Sec02_08/Exercise_2_11.lean — mathlib-dup — 三条 recall -- Sec02_08/Exercise_2_3.lean — mathlib-dup — 两行包装 -- Sec02_08/Exercise_2_7.lean — mathlib-dup — 纯 recall 交叉引用 -- Sec02_08/Exercise_2_9.lean — mathlib-dup — 四行包装 -- Sec02_08/Notation_2_8_extra_3.lean — mathlib-dup — 记号对照 #check -- Sec02_08/Proposition_2_10.lean — mathlib-dup — 四条 #check -- Sec02_08/Proposition_2_4.lean — mathlib-dup — 单条 #check -- Sec02_08/Proposition_2_5.lean — mathlib-dup — 单条 #check -- Sec02_08/Proposition_2_6.lean — mathlib-dup — 两条 #check -- Sec02_08/Remark_2_8_extra_1.lean — new — 术语谓词无数学内容 -- Sec02_08/Remark_2_8_extra_7.lean — mathlib-dup — 零声明词汇复述 -- Sec02_09/Definition_2_9_extra_1.lean — mathlib-dup — 纯 #check -- Sec02_09/Exercise_2_16.lean — partial-dup — recall 脚手架 -- Sec02_09/Exercise_2_19.lean — partial-dup — recall 脚手架 -- Sec02_10/Definition_2_10_extra_1.lean — mathlib-dup — 文档加单 #check -- Sec02_10/Definition_2_10_extra_2.lean — mathlib-dup — 本库已有包装 -- Sec02_10/Definition_2_10_extra_3.lean — mathlib-dup — 定义 recall -- Sec02_10/Definition_2_10_extra_4.lean — mathlib-dup — 定义 recall -- Sec02_10/Exercise_2_24.lean — mathlib-dup — #check 特化 -- Sec02_10/Lemma_2_20.lean — mathlib-dup — recall 指针 -- Sec02_10/Lemma_2_21.lean — partial-dup — smoothStep 已覆盖 -- Sec02_10/Lemma_2_22.lean — partial-dup — ContDiffBump 已供 -- Sec02_10/Theorem_2_23.lean — mathlib-dup — sorry 复述 -- Sec02_11/Definition_2_11_extra_1.lean — new — 平凡常函数检查 -- Sec02_11/Exercise_2_27.lean — new — 教学反例 -- Sec02_11/Theorem_2_29.lean — mathlib-dup — 六行特化包装 -- Sec02_12/Problem_2_1.lean — new — 教学反例无 API -- Sec02_12/Problem_2_12.lean — new — 主定理单 sorry -- Sec02_12/Problem_2_14.lean — mathlib-dup — 字面 recall -- Sec02_12/Problem_2_5.lean — new — 教材特定含两 sorry -- Sec02_12/Problem_2_8.lean — new — 依赖未移植图册 -- Sec02_12/Problem_2_9.lean — new — 教材特定大量辅件 -- Sec02_12/Problem_2_9_corecheck.lean — new — 流水线快照 -- Sec02_12/Problem_2_9_pre_north.lean — new — 流水线快照 -- Sec02_12/Problem_2_9_prefixcheck.lean — new — 流水线快照 +
Skip (40 items — mostly Mathlib wrappers / recall files) + +- Sec02_08/Definition_2_8_extra_2.lean — mathlib-dup — pure #check restatement +- Sec02_08/Definition_2_8_extra_4.lean — mathlib-dup — thin pointwise corollary +- Sec02_08/Definition_2_8_extra_5.lean — mathlib-dup — recall numbering cross-reference +- Sec02_08/Definition_2_8_extra_6.lean — partial-dup — existing API already covers it +- Sec02_08/Exercise_2_1.lean — mathlib-dup — only #check of the ring structure +- Sec02_08/Exercise_2_11.lean — mathlib-dup — three recalls +- Sec02_08/Exercise_2_3.lean — mathlib-dup — two-line wrapper +- Sec02_08/Exercise_2_7.lean — mathlib-dup — pure recall cross-reference +- Sec02_08/Exercise_2_9.lean — mathlib-dup — four-line wrapper +- Sec02_08/Notation_2_8_extra_3.lean — mathlib-dup — notation cross-reference #check +- Sec02_08/Proposition_2_10.lean — mathlib-dup — four #checks +- Sec02_08/Proposition_2_4.lean — mathlib-dup — single #check +- Sec02_08/Proposition_2_5.lean — mathlib-dup — single #check +- Sec02_08/Proposition_2_6.lean — mathlib-dup — two #checks +- Sec02_08/Remark_2_8_extra_1.lean — new — terminology predicate with no mathematical content +- Sec02_08/Remark_2_8_extra_7.lean — mathlib-dup — zero-declaration vocabulary restatement +- Sec02_09/Definition_2_9_extra_1.lean — mathlib-dup — pure #check +- Sec02_09/Exercise_2_16.lean — partial-dup — recall scaffolding +- Sec02_09/Exercise_2_19.lean — partial-dup — recall scaffolding +- Sec02_10/Definition_2_10_extra_1.lean — mathlib-dup — docs plus a single #check +- Sec02_10/Definition_2_10_extra_2.lean — mathlib-dup — wrapper already in this library +- Sec02_10/Definition_2_10_extra_3.lean — mathlib-dup — definition recall +- Sec02_10/Definition_2_10_extra_4.lean — mathlib-dup — definition recall +- Sec02_10/Exercise_2_24.lean — mathlib-dup — #check specialization +- Sec02_10/Lemma_2_20.lean — mathlib-dup — recall pointer +- Sec02_10/Lemma_2_21.lean — partial-dup — smoothStep already covers it +- Sec02_10/Lemma_2_22.lean — partial-dup — ContDiffBump already provides it +- Sec02_10/Theorem_2_23.lean — mathlib-dup — sorry restatement +- Sec02_11/Definition_2_11_extra_1.lean — new — trivial constant-function check +- Sec02_11/Exercise_2_27.lean — new — pedagogical counterexample +- Sec02_11/Theorem_2_29.lean — mathlib-dup — six-line specialization wrapper +- Sec02_12/Problem_2_1.lean — new — pedagogical counterexample, no API +- Sec02_12/Problem_2_12.lean — new — single-sorry main theorem +- Sec02_12/Problem_2_14.lean — mathlib-dup — literal recall +- Sec02_12/Problem_2_5.lean — new — textbook-specific, contains two sorry +- Sec02_12/Problem_2_8.lean — new — depends on an unported atlas +- Sec02_12/Problem_2_9.lean — new — textbook-specific, heavy auxiliary machinery +- Sec02_12/Problem_2_9_corecheck.lean — new — pipeline snapshot +- Sec02_12/Problem_2_9_pre_north.lean — new — pipeline snapshot +- Sec02_12/Problem_2_9_prefixcheck.lean — new — pipeline snapshot
-## 小结 +## Summary -第二章共审计 55 个文件，其中大部分（约 40 个）是对 Mathlib 既有 ContMDiff / 光滑函数 / 单位分解 API 的 #check 或 recall 式复述，可直接跳过。真正值得移植的核心资产集中在两条线：一是 Diffeomorph 基础设施（乘积、开子流形限制、维数不变性、单位球与图卡的打包微分同胚），二是闭球带边流形构造（Problem 2.4，2600 行无 sorry）与正光滑穷竭函数（Proposition 2.28），后两者直接支撑 GMT 散度定理与非紧 L²/Bochner 方向的缺口。中等价值项多数围绕光滑延拓、投影空间结构与回拉判据，部分仍含 sorry，宜在对应目标模块成型后按依赖顺序择机引入。 +Chapter 2 audited 55 files in total, most of which (about 40) are #check- or recall-style restatements of Mathlib's existing ContMDiff / smooth-function / partition-of-unity API and can be skipped outright. The core assets genuinely worth porting cluster along two lines: first, the Diffeomorph infrastructure (products, open-submanifold restriction, dimension invariance, the packaged unit-ball and chart diffeomorphisms); second, the closed-ball manifold-with-boundary construction (Problem 2.4, 2600 lines sorry-free) and the positive smooth exhaustion function (Proposition 2.28), the latter two directly supporting the gaps in the GMT divergence theorem and the noncompact L²/Bochner directions. The medium-value items mostly revolve around smooth extension, projective-space structure, and pullback criteria; some still contain sorry, and they are best introduced in dependency order once their target modules have taken shape. + +--- --- # Chap03 -## 移植优先（high，4 项） +## Port priority (high, 4 items) -| 文件 | 声明 | 分类 | 落点 | sorry | 理由 | +| File | Declarations | Class | Target | sorry | Rationale | |---|---|---|---|---|---| -| Sec03_14/Proposition_3_9.lean | mfderiv_open_subset_inclusion_isInvertible | new | Util/Tangent | 否 | 开子集包含微分可逆全证，Mathlib 缺此切空间识别 API | -| Sec03_17/Proposition_3_23.lean | exists_smooth_curve_with_velocity, exists_smooth_curve_with_velocity_boundaryless 等 | new | CurveVelocity | 否 | 曲线速度满射切空间含边界情形，Mathlib 全缺 | -| Sec03_16/Proposition_3_20.lean | tangent_bundle_opens_trivializationAt_eq_toProd, globalChartDiffeomorph 等 | partial-dup | TangentBundle/Trivialization | 否 | 单图卡切丛平凡化全证，主 def 依赖含 sorry 的 3.22 | -| Sec03_20/Problem_3_7.lean | TangentSpace.toPointDerivation, smooth_germ_derivation_existsUnique_tangentVector 等 | partial-dup | TangentBundle/PointDerivation | 是 | 切向量≃芽导子等价，Mathlib 著名缺口，余两条 sorry | +| Sec03_14/Proposition_3_9.lean | mfderiv_open_subset_inclusion_isInvertible | new | Util/Tangent | no | Full proof that the differential of an open-subset inclusion is invertible; Mathlib lacks this tangent-space identification API | +| Sec03_17/Proposition_3_23.lean | exists_smooth_curve_with_velocity, exists_smooth_curve_with_velocity_boundaryless, etc. | new | CurveVelocity | no | Surjectivity of curve velocity onto the tangent space including the boundary case; entirely missing from Mathlib | +| Sec03_16/Proposition_3_20.lean | tangent_bundle_opens_trivializationAt_eq_toProd, globalChartDiffeomorph, etc. | partial-dup | TangentBundle/Trivialization | no | Full proof of single-chart tangent-bundle trivialization; the main def depends on 3.22 which contains sorry | +| Sec03_20/Problem_3_7.lean | TangentSpace.toPointDerivation, smooth_germ_derivation_existsUnique_tangentVector, etc. | partial-dup | TangentBundle/PointDerivation | yes | Equivalence tangent vector ≃ germ derivation; a well-known Mathlib gap, with two remaining sorrys | -
可考虑（medium，11 项） +
Consider (medium, 11 items) -| 文件 | 声明 | 分类 | 落点 | sorry | 理由 | +| File | Declarations | Class | Target | sorry | Rationale | |---|---|---|---|---|---| -| Sec03_13/Proposition_3_2.lean | directional_point_derivation, geometric_to_point_derivation_linear_equiv 等 | new | Util/Tangent/PointDerivation | 是 | 几何切向量↔导子等价是真缺口，但仅欧氏且关键步全 sorry | -| Sec03_14/Lemma_3_11.lean | mfderiv_half_space_inclusion_isInvertible_of_boundary_eq_zero | new | Manifold/Boundary | 是 | 半空间包含边界点微分可逆，仅语句无证明可移 | -| Sec03_14/Proposition_3_8.lean | PointDerivation.congr_of_eqOn_nhds | new | Manifold/Derivation | 否 | 导子局部性 bump 函数完整证明，但本库不用导子模型 | -| Sec03_17/Definition_3_17_extra_1.lean | curve_velocity, curve_velocityWithin 等 | new | CurveVelocity | 否 | 命名曲线速度薄封装，是移植 3.23 的基础 | -| Sec03_18/Definition_3_18_extra_3.lean | SmoothCurveAt, CurveVelocityClass 等 | new | TangentBundle/CurveVelocity | 是 | 曲线速度实现切空间，两核心定理 sorry 需重设计 | -| Sec03_18/Definition_3_18_extra_4.lean | IsCoordinateTangentVector, TangentSpace.coordinateComponent 等 | new | TangentBundle/CoordinateComponents | 否 | 坐标分量 API 全证，Mathlib 缺，偏教学起源 | -| Sec03_20/Problem_3_4.lean | tangentBundle_circle_diffeomorph_prodLie, circleTangentFiberDiffeomorph 等 | new | TangentBundle/LieGroupTrivialization | 否 | 李群平凡化 TG≃G×Lie(G) 全证，硬编码圆需泛化 | -| Sec03_14/Proposition_3_6.lean | mfderiv_comp_of_smooth, diffeomorph_mfderiv_symm_eq_symm | partial-dup | Util/Tangent | 否 | 微分同胚逆的微分等于微分之逆，Mathlib 缺的小胶水 | -| Sec03_15/Proposition_3_15.lean | chart_mdifferentiable_of_mem_maximalAtlas, chart_coordinate_vectors_basis | partial-dup | Util/Chart/CoordinateBasis | 否 | 图卡 mfderiv 打包成 Basis，小型可复用坐标 API | -| Sec03_16/Corollary_3_22.lean | tangentMap_diffeomorph, tangentMap_comp_of_smooth 等 | partial-dup | TangentBundle/Diffeomorph | 是 | Diffeomorph 诱导切丛微分同胚，五条辅助引理 sorry | -| Sec03_20/Problem_3_1.lean | isLocallyConstant_of_mfderiv_eq_zero, mfderiv_eq_zero_iff_isLocallyConstant 等 | partial-dup | TangentBundle/MFDerivLocallyConstant | 是 | mfderiv≡0 当且仅当局部常值，正向 sorry 受阻 | +| Sec03_13/Proposition_3_2.lean | directional_point_derivation, geometric_to_point_derivation_linear_equiv, etc. | new | Util/Tangent/PointDerivation | yes | Geometric tangent vector ↔ derivation equivalence is a genuine gap, but Euclidean-only with the key step entirely sorry | +| Sec03_14/Lemma_3_11.lean | mfderiv_half_space_inclusion_isInvertible_of_boundary_eq_zero | new | Manifold/Boundary | yes | Differential of half-space inclusion at a boundary point is invertible; statement only, no proof to port | +| Sec03_14/Proposition_3_8.lean | PointDerivation.congr_of_eqOn_nhds | new | Manifold/Derivation | no | Complete bump-function proof of derivation locality, but this library does not use the derivation model | +| Sec03_17/Definition_3_17_extra_1.lean | curve_velocity, curve_velocityWithin, etc. | new | CurveVelocity | no | Thin wrapper naming curve velocity; the basis for porting 3.23 | +| Sec03_18/Definition_3_18_extra_3.lean | SmoothCurveAt, CurveVelocityClass, etc. | new | TangentBundle/CurveVelocity | yes | Curve velocity realizing the tangent space; two core theorems sorry, needs redesign | +| Sec03_18/Definition_3_18_extra_4.lean | IsCoordinateTangentVector, TangentSpace.coordinateComponent, etc. | new | TangentBundle/CoordinateComponents | no | Fully proved coordinate-component API; missing from Mathlib, pedagogically oriented | +| Sec03_20/Problem_3_4.lean | tangentBundle_circle_diffeomorph_prodLie, circleTangentFiberDiffeomorph, etc. | new | TangentBundle/LieGroupTrivialization | no | Full proof of Lie-group trivialization TG ≃ G × Lie(G); hardcoded circle needs generalization | +| Sec03_14/Proposition_3_6.lean | mfderiv_comp_of_smooth, diffeomorph_mfderiv_symm_eq_symm | partial-dup | Util/Tangent | no | Differential of a diffeomorphism's inverse equals the inverse of the differential; small glue missing from Mathlib | +| Sec03_15/Proposition_3_15.lean | chart_mdifferentiable_of_mem_maximalAtlas, chart_coordinate_vectors_basis | partial-dup | Util/Chart/CoordinateBasis | no | Packages chart mfderiv into a Basis; small reusable coordinate API | +| Sec03_16/Corollary_3_22.lean | tangentMap_diffeomorph, tangentMap_comp_of_smooth, etc. | partial-dup | TangentBundle/Diffeomorph | yes | Diffeomorph induces a tangent-bundle diffeomorphism; five auxiliary lemmas sorry | +| Sec03_20/Problem_3_1.lean | isLocallyConstant_of_mfderiv_eq_zero, mfderiv_eq_zero_iff_isLocallyConstant, etc. | partial-dup | TangentBundle/MFDerivLocallyConstant | yes | mfderiv ≡ 0 iff locally constant; the forward direction is sorry-blocked |
-
跳过（42 项，绝大多数为 Mathlib 包装/recall 文件） - -- Sec03_13/Corollary_3_3.lean — new — 欧氏限定全 sorry -- Sec03_13/Definition_3_13_extra_1.lean — mathlib-dup — 薄包装加记号 -- Sec03_13/Definition_3_13_extra_2.lean — mathlib-dup — 仅 #check 复述 -- Sec03_13/Definition_3_13_extra_3.lean — mathlib-dup — rfl 级复述 -- Sec03_13/Exercise_3_5.lean — mathlib-dup — 纯 #check 回顾 -- Sec03_13/Lemma_3_1.lean — mathlib-dup — 欧氏一行推论 -- Sec03_13/Lemma_3_4.lean — mathlib-dup — 一行包装 -- Sec03_14/Definition_3_14_extra_1.lean — mathlib-dup — 复述 mfderiv 签名 -- Sec03_14/Definition_3_14_extra_2.lean — mathlib-dup — 单个 #check -- Sec03_14/Exercise_3_7.lean — mathlib-dup — 纯 #check 复述 -- Sec03_14/Proposition_3_10.lean — mathlib-dup — 一行 defeq -- Sec03_14/Proposition_3_12.lean — mathlib-dup — sorry 复述维数 -- Sec03_14/Proposition_3_13.lean — mathlib-dup — 一行包装附 sorry -- Sec03_15/Definition_3_15_extra_1.lean — partial-dup — 已被现有 API 覆盖 -- Sec03_15/Definition_3_15_extra_2.lean — partial-dup — 一行 .repr 包装 -- Sec03_15/Example_3_16.lean — new — 教科书数值例 -- Sec03_15/Exercise_3_17.lean — new — 教学专用示例 -- Sec03_15/Remark_3_15_extra_3.lean — mathlib-dup — 纯回顾 -- Sec03_15/Remark_3_15_extra_4.lean — partial-dup — 两行胶水已有 -- Sec03_15/Remark_3_15_extra_5.lean — mathlib-dup — 回顾复述 -- Sec03_16/Definition_3_16_extra_1.lean — mathlib-dup — 回顾 TangentBundle -- Sec03_16/Definition_3_16_extra_3.lean — mathlib-dup — 仅 #check -- Sec03_16/Exercise_3_19.lean — new — 单个 rfl 定理 -- Sec03_16/Notation_3_16_extra_2.lean — mathlib-dup — 仅记号加 #check -- Sec03_16/Notation_3_16_extra_4.lean — mathlib-dup — 回顾桥引理 -- Sec03_16/Proposition_3_18.lean — mathlib-dup — 特化 contMDiff_proj -- Sec03_16/Proposition_3_21.lean — mathlib-dup — 单个 #check 特化 -- Sec03_17/Proposition_3_24.lean — mathlib-dup — 链规则一行求值 -- Sec03_17/Corollary_3_25.lean — mathlib-dup — 复述 3.24 -- Sec03_18/Definition_3_18_extra_1.lean — mathlib-dup — 记号加一行实例 -- Sec03_18/Definition_3_18_extra_2.lean — partial-dup — 平凡 abbrev 加 sorry -- Sec03_19/Definition_3_19_extra_1.lean — mathlib-dup — 回顾 Category -- Sec03_19/Definition_3_19_extra_2.lean — mathlib-dup — 回顾 IsIso -- Sec03_19/Definition_3_19_extra_3.lean — mathlib-dup — 回顾小范畴概念 -- Sec03_19/Definition_3_19_extra_4.lean — mathlib-dup — 仅 #check 函子 -- Sec03_19/Definition_3_19_extra_5.lean — mathlib-dup — 仅 #check 反变函子 -- Sec03_19/Example_3_26.lean — partial-dup — 教学示例 -- Sec03_19/Exercise_3_27.lean — mathlib-dup — 回顾无新证明 -- Sec03_20/Problem_3_3.lean — mathlib-dup — 纯回顾复述 -- Sec03_20/Problem_3_5.lean — new — 教科书专用习题 -- Sec03_20/Problem_3_6.lean — new — 具体例几乎全 sorry -- Sec03_20/Problem_3_8.lean — new — 纯回顾桥文件 +
Skip (42 items — mostly Mathlib wrappers / recall files) + +- Sec03_13/Corollary_3_3.lean — new — Euclidean-restricted, entirely sorry +- Sec03_13/Definition_3_13_extra_1.lean — mathlib-dup — thin wrapper plus notation +- Sec03_13/Definition_3_13_extra_2.lean — mathlib-dup — #check restatement only +- Sec03_13/Definition_3_13_extra_3.lean — mathlib-dup — rfl-level restatement +- Sec03_13/Exercise_3_5.lean — mathlib-dup — pure #check recall +- Sec03_13/Lemma_3_1.lean — mathlib-dup — one-line Euclidean corollary +- Sec03_13/Lemma_3_4.lean — mathlib-dup — one-line wrapper +- Sec03_14/Definition_3_14_extra_1.lean — mathlib-dup — restates the mfderiv signature +- Sec03_14/Definition_3_14_extra_2.lean — mathlib-dup — single #check +- Sec03_14/Exercise_3_7.lean — mathlib-dup — pure #check restatement +- Sec03_14/Proposition_3_10.lean — mathlib-dup — one-line defeq +- Sec03_14/Proposition_3_12.lean — mathlib-dup — sorry restatement of dimension +- Sec03_14/Proposition_3_13.lean — mathlib-dup — one-line wrapper with sorry +- Sec03_15/Definition_3_15_extra_1.lean — partial-dup — already covered by existing API +- Sec03_15/Definition_3_15_extra_2.lean — partial-dup — one-line .repr wrapper +- Sec03_15/Example_3_16.lean — new — textbook numerical example +- Sec03_15/Exercise_3_17.lean — new — pedagogy-only example +- Sec03_15/Remark_3_15_extra_3.lean — mathlib-dup — pure recall +- Sec03_15/Remark_3_15_extra_4.lean — partial-dup — two-line glue already present +- Sec03_15/Remark_3_15_extra_5.lean — mathlib-dup — recall restatement +- Sec03_16/Definition_3_16_extra_1.lean — mathlib-dup — recalls TangentBundle +- Sec03_16/Definition_3_16_extra_3.lean — mathlib-dup — #check only +- Sec03_16/Exercise_3_19.lean — new — single rfl theorem +- Sec03_16/Notation_3_16_extra_2.lean — mathlib-dup — notation plus #check only +- Sec03_16/Notation_3_16_extra_4.lean — mathlib-dup — recalls bridge lemma +- Sec03_16/Proposition_3_18.lean — mathlib-dup — specializes contMDiff_proj +- Sec03_16/Proposition_3_21.lean — mathlib-dup — single #check specialization +- Sec03_17/Proposition_3_24.lean — mathlib-dup — one-line evaluation of the chain rule +- Sec03_17/Corollary_3_25.lean — mathlib-dup — restates 3.24 +- Sec03_18/Definition_3_18_extra_1.lean — mathlib-dup — notation plus one-line instance +- Sec03_18/Definition_3_18_extra_2.lean — partial-dup — trivial abbrev plus sorry +- Sec03_19/Definition_3_19_extra_1.lean — mathlib-dup — recalls Category +- Sec03_19/Definition_3_19_extra_2.lean — mathlib-dup — recalls IsIso +- Sec03_19/Definition_3_19_extra_3.lean — mathlib-dup — recalls the small-category concept +- Sec03_19/Definition_3_19_extra_4.lean — mathlib-dup — #check functor only +- Sec03_19/Definition_3_19_extra_5.lean — mathlib-dup — #check contravariant functor only +- Sec03_19/Example_3_26.lean — partial-dup — pedagogical example +- Sec03_19/Exercise_3_27.lean — mathlib-dup — recall, no new proof +- Sec03_20/Problem_3_3.lean — mathlib-dup — pure recall restatement +- Sec03_20/Problem_3_5.lean — new — textbook-only exercise +- Sec03_20/Problem_3_6.lean — new — concrete example, almost entirely sorry +- Sec03_20/Problem_3_8.lean — new — pure recall bridge file
-## 小结 +## Summary -第三章共审计 53 个文件，其中约四分之三为 Mathlib 重复（recall/#check 复述或一行包装），可直接跳过。真正值得移植的高价值条目集中在切空间基础设施：开子集包含映射微分可逆性（Proposition 3.9）、曲线速度满射（Proposition 3.23）、单图卡切丛平凡化（Proposition 3.20）以及切向量-导子等价（Problem 3.7），前三者中两个已完全无 sorry。中价值条目多围绕导子模型与坐标基 API，但普遍含 sorry 或需要设计返工，建议在 CurveVelocity 与 Tangent 工具模块落地高价值条目后再酌情跟进。 +Chapter 3 audited 53 files in total, roughly three-quarters of which are Mathlib duplicates (recall/#check restatements or one-line wrappers) and can be skipped outright. The high-value items genuinely worth porting cluster around tangent-space infrastructure: invertibility of the differential of an open-subset inclusion (Proposition 3.9), surjectivity of curve velocity (Proposition 3.23), single-chart tangent-bundle trivialization (Proposition 3.20), and the tangent-vector–derivation equivalence (Problem 3.7); two of the first three are already entirely sorry-free. The medium-value items mostly revolve around the derivation model and the coordinate-basis API, but generally contain sorrys or need design rework, so it is advisable to follow up on them only after the high-value items have landed in the CurveVelocity and Tangent utility modules. + +--- --- # Chap04 -## 移植优先（high，16 项） +## Port priority (high, 16 items) -| 文件 | 声明 | 分类 | 落点 | sorry | 理由 | +| File | Declarations | Class | Target | sorry | Rationale | |---|---|---|---|---|---| -| Sec04_21/Exercise_4_3.lean | prod_fst_isSmoothSubmersion, prod_mk_right_isImmersion 等 | new | Manifold/ImmersionSubmersion | 否 | 积投影淹没/切片浸入全证，含可复用图卡群胚基建 | -| Sec04_21/Exercise_4_4.lean | IsSmoothSubmersion.comp, IsImmersion.comp 等 | new | Manifold/ImmersionSubmersion | 是 | 淹没复合与秩 API，攻 Mathlib TODO，一辅助引理 3 sorry | -| Sec04_22/Proposition_4_8.lean | IsLocalDiffeomorph.isImmersion, is_local_diffeomorph_iff_is_immersion_and_is_smooth_submersion 等 | new | Manifold/Submersion | 否 | 局部微分同胚↔浸入+淹没全证，上游谓词含 sorry | -| Sec04_22/Theorem_4_5.lean | isLocalDiffeomorphAt_of_contMDiffAt_mfderiv_isInvertible, model_partialDiffeomorph_of_inverse_function_theorem 等 | new | Manifold/InverseFunctionTheorem | 否 | 流形版反函数定理完整证明，Mathlib 明确 TODO | -| Sec04_24/Exercise_4_16.lean | IsImmersion.ex416_comp, IsSmoothEmbedding.comp 等 | new | SmoothManifold/Immersion | 是 | 浸入/光滑嵌入复合，Mathlib proof_wanted，余一 sorry | -| Sec04_25/Definition_4_25_extra_2.lean | Topology.IsTopologicalSubmersion, IsTopologicalSubmersion.isQuotientMap 等 | new | Manifold/Submersion | 否 | 拓扑淹没 API 全证（开/商映射），Mathlib 缺 | -| Sec04_25/Proposition_4_28.lean | Manifold.IsSmoothSubmersion, IsSmoothSubmersion.isOpenMap 等 | new | Manifold/Submersion | 否 | 定义 Mathlib 缺失的光滑淹没结构，依赖含 sorry 的 4.26 | -| Sec04_25/Theorem_4_26.lean | Manifold.IsSmoothLocalSection, smooth_submersion_iff_exists_smooth_local_section_through_every_point 等 | new | Manifold/Submersion | 是 | 局部截面定理刻画淹没，主定理 sorry 需秩定理级工作 | -| Sec04_25/Theorem_4_29.lean | Manifold.contMDiff_iff_comp_of_surjective_smooth_submersion | new | Manifold/Submersion | 是 | 满淹没特征性质是商流形主力引理，仅语句含 sorry | -| Sec04_25/Theorem_4_30.lean | Manifold.existsUnique_contMDiff_lift_of_surjective_smooth_submersion | new | Manifold/Submersion | 是 | 商流形光滑提升存在唯一性核心基建，证明为 sorry | -| Sec04_26/Definition_4_26_extra_1.lean | Manifold.IsSmoothCoveringMap, IsUniversalSmoothCoveringMap 等 | new | Manifold/CoveringMap | 否 | 光滑覆盖映射核心定义层，Mathlib 仅有拓扑版 | -| Sec04_26/Exercise_4_37.lean | IsLocalDiffeomorph.isSmoothLocalSection, IsSmoothCoveringMap.isSmoothLocalSection 等 | new | Manifold/CoveringMap | 否 | 连续局部截面自动光滑，全证通用升级引理 | -| Sec04_26/Proposition_4_36.lean | IsCoveringMap.exists_localSectionOn, IsSmoothCoveringMap.localSection_eq 等 | new | Manifold/CoveringMap | 否 | 光滑局部截面存在与预连通集上唯一性，完整 API | -| Sec04_26/Proposition_4_40.lean | exists_unique_smooth_covering_structure, lifted_covering_chartedSpace 等 | new | Manifold/CoveringMap | 否 | 拓扑覆盖唯一光滑结构，700 行无 sorry 大定理 | -| Sec04_26/Proposition_4_46.lean | isSmoothCoveringMap_of_proper_localDiffeomorph, fiber_finite_of_proper_local_diffeomorph 等 | new | Manifold/CoveringMap | 否 | 真局部微分同胚⇒覆盖映射判据全证，移植需并回正式定义 | -| Sec04_27/Problem_4_5.lean | complexProjectiveQuotientMap_isSmoothSubmersion, complexProjectiveLine_diffeomorphic_sphere 等 | new | Instances/ComplexProjectiveSpace | 否 | CP^n 商淹没全证，含 CP^1≅S^2 压轴构造 | - -
可考虑（medium，22 项） - -| 文件 | 声明 | 分类 | 落点 | sorry | 理由 | +| Sec04_21/Exercise_4_3.lean | prod_fst_isSmoothSubmersion, prod_mk_right_isImmersion, etc. | new | Manifold/ImmersionSubmersion | no | Product-projection submersion / slice immersion fully proved, includes reusable chart groupoid infrastructure | +| Sec04_21/Exercise_4_4.lean | IsSmoothSubmersion.comp, IsImmersion.comp, etc. | new | Manifold/ImmersionSubmersion | yes | Submersion composition and rank API, tackles a Mathlib TODO, one helper lemma has 3 sorry | +| Sec04_22/Proposition_4_8.lean | IsLocalDiffeomorph.isImmersion, is_local_diffeomorph_iff_is_immersion_and_is_smooth_submersion, etc. | new | Manifold/Submersion | no | Local diffeomorphism ↔ immersion + submersion fully proved, upstream predicate has sorry | +| Sec04_22/Theorem_4_5.lean | isLocalDiffeomorphAt_of_contMDiffAt_mfderiv_isInvertible, model_partialDiffeomorph_of_inverse_function_theorem, etc. | new | Manifold/InverseFunctionTheorem | no | Manifold-version inverse function theorem fully proved, an explicit Mathlib TODO | +| Sec04_24/Exercise_4_16.lean | IsImmersion.ex416_comp, IsSmoothEmbedding.comp, etc. | new | SmoothManifold/Immersion | yes | Immersion / smooth-embedding composition, Mathlib proof_wanted, one remaining sorry | +| Sec04_25/Definition_4_25_extra_2.lean | Topology.IsTopologicalSubmersion, IsTopologicalSubmersion.isQuotientMap, etc. | new | Manifold/Submersion | no | Topological-submersion API fully proved (open / quotient maps), missing from Mathlib | +| Sec04_25/Proposition_4_28.lean | Manifold.IsSmoothSubmersion, IsSmoothSubmersion.isOpenMap, etc. | new | Manifold/Submersion | no | Defines the smooth-submersion structure Mathlib lacks, depends on 4.26 which has sorry | +| Sec04_25/Theorem_4_26.lean | Manifold.IsSmoothLocalSection, smooth_submersion_iff_exists_smooth_local_section_through_every_point, etc. | new | Manifold/Submersion | yes | Local-section theorem characterizing submersions, main-theorem sorry needs rank-theorem-level work | +| Sec04_25/Theorem_4_29.lean | Manifold.contMDiff_iff_comp_of_surjective_smooth_submersion | new | Manifold/Submersion | yes | Surjective-submersion characteristic property is the workhorse lemma for quotient manifolds, only the statement has sorry | +| Sec04_25/Theorem_4_30.lean | Manifold.existsUnique_contMDiff_lift_of_surjective_smooth_submersion | new | Manifold/Submersion | yes | Existence-uniqueness of smooth lifts for quotient manifolds, core infrastructure, proof is sorry | +| Sec04_26/Definition_4_26_extra_1.lean | Manifold.IsSmoothCoveringMap, IsUniversalSmoothCoveringMap, etc. | new | Manifold/CoveringMap | no | Core definition layer for smooth covering maps, Mathlib only has the topological version | +| Sec04_26/Exercise_4_37.lean | IsLocalDiffeomorph.isSmoothLocalSection, IsSmoothCoveringMap.isSmoothLocalSection, etc. | new | Manifold/CoveringMap | no | Continuous local sections are automatically smooth, fully proved general upgrade lemma | +| Sec04_26/Proposition_4_36.lean | IsCoveringMap.exists_localSectionOn, IsSmoothCoveringMap.localSection_eq, etc. | new | Manifold/CoveringMap | no | Existence of smooth local sections and uniqueness on preconnected sets, complete API | +| Sec04_26/Proposition_4_40.lean | exists_unique_smooth_covering_structure, lifted_covering_chartedSpace, etc. | new | Manifold/CoveringMap | no | Unique smooth structure on a topological cover, 700-line sorry-free major theorem | +| Sec04_26/Proposition_4_46.lean | isSmoothCoveringMap_of_proper_localDiffeomorph, fiber_finite_of_proper_local_diffeomorph, etc. | new | Manifold/CoveringMap | no | Proper local diffeomorphism ⇒ covering map criterion fully proved, port requires merging back into the formal definition | +| Sec04_27/Problem_4_5.lean | complexProjectiveQuotientMap_isSmoothSubmersion, complexProjectiveLine_diffeomorphic_sphere, etc. | new | Instances/ComplexProjectiveSpace | no | CP^n quotient submersion fully proved, includes the capstone CP^1 ≅ S^2 construction | + +
Consider (medium, 22 items) + +| File | Declarations | Class | Target | sorry | Rationale | |---|---|---|---|---|---| -| Sec04_21/Definition_4_21_extra_1.lean | rank_at_eq_finrank_range_mfderiv, is_immersion_iff_forall_injective_mfderiv 等 | new | Manifold/Rank | 是 | 秩 API 填 Mathlib 缺口，但定理全 sorry 仅语句可移 | -| Sec04_21/Proposition_4_1.lean | exists_open_restriction_isSmoothSubmersion_of_surjective_mfderiv, exists_open_restriction_isImmersion_of_injective_mfderiv | new | Manifold/ImmersionSubmersion | 是 | 点态满/单 mfderiv 给局部淹没/浸入，证明全 sorry | -| Sec04_22/Exercise_4_10.lean | smooth_iff_comp_left_of_isLocalDiffeomorph, smooth_iff_comp_right_of_surjective_isLocalDiffeomorph | new | Manifold/LocalDiffeomorph | 否 | 经局部微分同胚前后复合检测光滑性，全证 iff 引理 | -| Sec04_23/Theorem_4_14.lean | constant_rank_surjective_is_smooth_submersion, constant_rank_injective_is_immersion 等 | new | Manifold/RankTheorem | 是 | 全局秩定理是真缺口，但三证明全 sorry 仅语句 | -| Sec04_23/Theorem_4_15.lean | boundary_immersion_normal_form, BoundaryLocalCoordinateNormalFormAt 等 | new | Manifold/Boundary | 是 | 带边流形浸入边界标准形，与 GMT 相关但主定理 sorry | -| Sec04_24/Definition_4_24_extra_2.lean | Topology.IsTopologicalImmersion, IsEmbedding.isTopologicalImmersion 等 | new | SmoothManifold/Immersion | 否 | 局部嵌入谓词小型全证拓扑 API，单独价值有限 | -| Sec04_24/Proposition_4_22.lean | smooth_embedding_of_injective_isImmersion_isOpenMap, smooth_embedding_of_compact_source_injective_isImmersion 等 | new | SmoothManifold/Embedding | 是 | 单浸入成嵌入的充分条件骨架，五证明全 sorry | -| Sec04_24/Theorem_4_25.lean | Manifold.isImmersion_iff_forall_exists_open_restriction_isSmoothEmbedding | new | SmoothManifold/Embedding | 是 | 局部嵌入定理是真缺口，但仅单条 sorry 存根 | -| Sec04_25/Definition_4_25_extra_1.lean | ContinuousMap.IsLocalSection, Function.RightInverse.isLocalSection_restrict_top 等 | new | Manifold/Submersion | 否 | 连续映射局部截面谓词，小而全证的基础层 | -| Sec04_25/Theorem_4_31.lean | Manifold.existsUnique_diffeomorph_of_surjective_smooth_submersions_constant_on_each_others_fibers | new | Manifold/Submersion | 是 | 光滑商唯一性，4.29/4.30 的推论，仅语句 sorry | -| Sec04_26/Exercise_4_38.lean | Manifold.IsSmoothCoveringMap.pi, isCoveringMap_pi 等 | new | Manifold/CoveringMap | 否 | 覆盖映射有限积定理无 sorry，移植前需精简同胚管线 | -| Sec04_26/Exercise_4_39.lean | Bundle.Trivialization.sheet_coordinate_eq_on_component, component_bijOn_baseSet 等 | new | Manifold/CoveringMap | 否 | 叶分解引理全证，Mathlib 缺的 Trivialization API，略偏门 | -| Sec04_26/Proposition_4_33.lean | IsSmoothCoveringMap.isSmoothSubmersion, diffeomorphOfInjective 等 | new | Manifold/CoveringMap | 是 | 覆盖映射基本性质接口正确，但五条中四条 sorry | -| Sec04_27/Problem_4_11.lean | isProperMap_iff_finite_fibers_of_isCoveringMap, exists_smoothCoveringMap_not_isProperMap | new | MetricGeometry/Covering/ProperMap | 是 | 覆盖真当且仅当纤维有限是真缺口，仅语句需从头证 | -| Sec04_27/Problem_4_12.lean | torus_of_revolution_map_isSmoothEmbedding, torus_product_isManifold 等 | new | Instances/Torus | 否 | 平坦环面嵌入 R^3 全证，含 pi 群胚/积流形助手 | -| Sec04_27/Problem_4_3.lean | boundary_rank_normal_form, constant_rank_boundary_local_coordinate_normal_form | new | Manifold/RankTheorem | 是 | 边界点常秩标准形是真缺口，但 sorry 语句且形式别扭 | -| Sec04_27/Problem_4_6.lean | not_exists_smooth_submersion_to_euclideanSpace | new | Manifold/Submersion | 否 | 紧流形无淹没到 R^k 经典结果全证，依赖项目谓词 | -| Sec04_27/Problem_4_7.lean | contMDiff_iff_comp_equiv_of_submersion_characteristic_property, exists_diffeomorph_of_submersion_characteristic_property | new | Manifold/Submersion | 是 | 商光滑结构唯一性有价值，但两定理皆 sorry | -| Sec04_22/Proposition_4_6.lean | isLocalDiffeomorph_comp, isLocalDiffeomorph_pi 等 | partial-dup | Manifold/LocalDiffeomorph | 是 | 缺失的复合/积/坐标判据引理全 sorry，余为回顾 | -| Sec04_23/Theorem_4_12.lean | rank_normal_form, constant_rank_local_coordinate_normal_form 等 | partial-dup | Manifold/RankTheorem | 是 | 常秩定理是真缺口，但五证明全 sorry 且欧氏结构需重构 | -| Sec04_24/Example_4_20.lean | denseTorusCurve, circle_exp_isLocalDiffeomorph_from_angle_branch 等 | partial-dup | SmoothManifold/CircleExp | 否 | 无理缠绕属反例，Circle.exp 局部微分同胚助手可复用 | -| Sec04_26/Example_4_35.lean | circle_exp_isSmoothCoveringMap, sphere_to_realProjectiveSpace_isCoveringMap 等 | partial-dup | Instances/CoveringExamples | 否 | 光滑覆盖实例全证，RP^n 覆盖为新内容好例证 | +| Sec04_21/Definition_4_21_extra_1.lean | rank_at_eq_finrank_range_mfderiv, is_immersion_iff_forall_injective_mfderiv, etc. | new | Manifold/Rank | yes | Rank API fills a Mathlib gap, but theorems are all sorry, only statements portable | +| Sec04_21/Proposition_4_1.lean | exists_open_restriction_isSmoothSubmersion_of_surjective_mfderiv, exists_open_restriction_isImmersion_of_injective_mfderiv | new | Manifold/ImmersionSubmersion | yes | Pointwise surjective/injective mfderiv gives a local submersion/immersion, proofs all sorry | +| Sec04_22/Exercise_4_10.lean | smooth_iff_comp_left_of_isLocalDiffeomorph, smooth_iff_comp_right_of_surjective_isLocalDiffeomorph | new | Manifold/LocalDiffeomorph | no | Detecting smoothness via pre/post composition with a local diffeomorphism, fully proved iff lemmas | +| Sec04_23/Theorem_4_14.lean | constant_rank_surjective_is_smooth_submersion, constant_rank_injective_is_immersion, etc. | new | Manifold/RankTheorem | yes | Global rank theorem is a genuine gap, but all three proofs are sorry, statements only | +| Sec04_23/Theorem_4_15.lean | boundary_immersion_normal_form, BoundaryLocalCoordinateNormalFormAt, etc. | new | Manifold/Boundary | yes | Boundary normal form for immersions of manifolds-with-boundary, GMT-relevant but main theorem sorry | +| Sec04_24/Definition_4_24_extra_2.lean | Topology.IsTopologicalImmersion, IsEmbedding.isTopologicalImmersion, etc. | new | SmoothManifold/Immersion | no | Small fully-proved topological API for the local-embedding predicate, limited standalone value | +| Sec04_24/Proposition_4_22.lean | smooth_embedding_of_injective_isImmersion_isOpenMap, smooth_embedding_of_compact_source_injective_isImmersion, etc. | new | SmoothManifold/Embedding | yes | Skeleton of sufficient conditions for an injective immersion to be an embedding, all five proofs sorry | +| Sec04_24/Theorem_4_25.lean | Manifold.isImmersion_iff_forall_exists_open_restriction_isSmoothEmbedding | new | SmoothManifold/Embedding | yes | Local-embedding theorem is a genuine gap, but only a single sorry stub | +| Sec04_25/Definition_4_25_extra_1.lean | ContinuousMap.IsLocalSection, Function.RightInverse.isLocalSection_restrict_top, etc. | new | Manifold/Submersion | no | Local-section predicate for continuous maps, small fully-proved foundation layer | +| Sec04_25/Theorem_4_31.lean | Manifold.existsUnique_diffeomorph_of_surjective_smooth_submersions_constant_on_each_others_fibers | new | Manifold/Submersion | yes | Uniqueness of smooth quotients, a corollary of 4.29/4.30, statement-only sorry | +| Sec04_26/Exercise_4_38.lean | Manifold.IsSmoothCoveringMap.pi, isCoveringMap_pi, etc. | new | Manifold/CoveringMap | no | Finite-product theorem for covering maps, no sorry, port needs streamlining the diffeomorphism pipeline first | +| Sec04_26/Exercise_4_39.lean | Bundle.Trivialization.sheet_coordinate_eq_on_component, component_bijOn_baseSet, etc. | new | Manifold/CoveringMap | no | Sheet-decomposition lemmas fully proved, Trivialization API missing from Mathlib, somewhat niche | +| Sec04_26/Proposition_4_33.lean | IsSmoothCoveringMap.isSmoothSubmersion, diffeomorphOfInjective, etc. | new | Manifold/CoveringMap | yes | Basic-property interface for covering maps is correct, but four of five are sorry | +| Sec04_27/Problem_4_11.lean | isProperMap_iff_finite_fibers_of_isCoveringMap, exists_smoothCoveringMap_not_isProperMap | new | MetricGeometry/Covering/ProperMap | yes | Cover-is-proper iff fibers finite is a genuine gap, statements only, needs proving from scratch | +| Sec04_27/Problem_4_12.lean | torus_of_revolution_map_isSmoothEmbedding, torus_product_isManifold, etc. | new | Instances/Torus | no | Flat-torus embedding into R^3 fully proved, includes pi-groupoid / product-manifold helpers | +| Sec04_27/Problem_4_3.lean | boundary_rank_normal_form, constant_rank_boundary_local_coordinate_normal_form | new | Manifold/RankTheorem | yes | Constant-rank normal form at boundary points is a genuine gap, but sorry statements and awkward form | +| Sec04_27/Problem_4_6.lean | not_exists_smooth_submersion_to_euclideanSpace | new | Manifold/Submersion | no | Classical result that a compact manifold admits no submersion to R^k fully proved, depends on project predicates | +| Sec04_27/Problem_4_7.lean | contMDiff_iff_comp_equiv_of_submersion_characteristic_property, exists_diffeomorph_of_submersion_characteristic_property | new | Manifold/Submersion | yes | Uniqueness of smooth quotient structure is valuable, but both theorems are sorry | +| Sec04_22/Proposition_4_6.lean | isLocalDiffeomorph_comp, isLocalDiffeomorph_pi, etc. | partial-dup | Manifold/LocalDiffeomorph | yes | Missing composition/product/coordinate-criterion lemmas all sorry, rest is recall | +| Sec04_23/Theorem_4_12.lean | rank_normal_form, constant_rank_local_coordinate_normal_form, etc. | partial-dup | Manifold/RankTheorem | yes | Constant-rank theorem is a genuine gap, but all five proofs sorry and the Euclidean structure needs reworking | +| Sec04_24/Example_4_20.lean | denseTorusCurve, circle_exp_isLocalDiffeomorph_from_angle_branch, etc. | partial-dup | SmoothManifold/CircleExp | no | Irrational-winding counterexample, Circle.exp local-diffeomorphism helper is reusable | +| Sec04_26/Example_4_35.lean | circle_exp_isSmoothCoveringMap, sphere_to_realProjectiveSpace_isCoveringMap, etc. | partial-dup | Instances/CoveringExamples | no | Smooth-covering instances fully proved, RP^n cover is new content and a good example |
-
跳过（26 项，绝大多数为 Mathlib 包装/recall 文件） - -- Sec04_21/Example_4_2.lean — new — 全 sorry 教学例 -- Sec04_22/Definition_4_22_extra_1.lean — mathlib-dup — 纯 abbrev 复述 -- Sec04_22/Exercise_4_7.lean — mathlib-dup — 仅 #check 回顾 -- Sec04_22/Exercise_4_9.lean — new — 欧氏硬编码加 sorry -- Sec04_23/Corollary_4_13.lean — new — 单条 sorry 复述 -- Sec04_24/Definition_4_24_extra_1.lean — mathlib-dup — 八行仅 #check -- Sec04_24/Example_4_17.lean — partial-dup — of_opens 加 sorry 存根 -- Sec04_24/Example_4_18.lean — new — 单个具体反例 -- Sec04_24/Example_4_19.lean — new — 教学八字曲线反例 -- Sec04_24/Exercise_4_24.lean — new — 一次性反例机件 -- Sec04_24/Lemma_4_21.lean — mathlib-dup — 重证 Dirichlet 逼近 -- Sec04_25/Exercise_4_27.lean — new — x^3 教学反例 -- Sec04_25/Exercise_4_32.lean — new — 纯回顾 4.31 -- Sec04_26/Corollary_4_43.lean — new — sorry 存根 -- Sec04_26/Exercise_4_34.lean — new — 纯回顾脚手架 -- Sec04_26/Exercise_4_42.lean — new — 纯回顾 4.41 -- Sec04_26/Exercise_4_44.lean — new — 纯回顾 4.43 -- Sec04_26/Exercise_4_45.lean — new — 边界框架 sorry 存根 -- Sec04_26/Proposition_4_41.lean — new — 边界版主结果全 sorry -- Sec04_27/Problem_4_1.lean — new — 薄包装单反例 -- Sec04_27/Problem_4_10.lean — new — 单条 sorry 语句 -- Sec04_27/Problem_4_13.lean — new — 语句依赖未证基建 -- Sec04_27/Problem_4_2.lean — mathlib-dup — 一行特化 -- Sec04_27/Problem_4_4.lean — new — 纯记账回顾 -- Sec04_27/Problem_4_8.lean — new — 全 sorry 反例 -- Sec04_27/Problem_4_9.lean — new — 纯回顾视图 +
Skip (26 items — mostly Mathlib wrappers / recall files) + +- Sec04_21/Example_4_2.lean — new — all-sorry teaching example +- Sec04_22/Definition_4_22_extra_1.lean — mathlib-dup — pure abbrev restatement +- Sec04_22/Exercise_4_7.lean — mathlib-dup — #check recall only +- Sec04_22/Exercise_4_9.lean — new — Euclidean hardcoded plus sorry +- Sec04_23/Corollary_4_13.lean — new — single-sorry restatement +- Sec04_24/Definition_4_24_extra_1.lean — mathlib-dup — eight lines of #check only +- Sec04_24/Example_4_17.lean — partial-dup — of_opens plus sorry stub +- Sec04_24/Example_4_18.lean — new — single concrete counterexample +- Sec04_24/Example_4_19.lean — new — teaching figure-eight curve counterexample +- Sec04_24/Exercise_4_24.lean — new — one-off counterexample machinery +- Sec04_24/Lemma_4_21.lean — mathlib-dup — re-proves Dirichlet approximation +- Sec04_25/Exercise_4_27.lean — new — x^3 teaching counterexample +- Sec04_25/Exercise_4_32.lean — new — pure recall of 4.31 +- Sec04_26/Corollary_4_43.lean — new — sorry stub +- Sec04_26/Exercise_4_34.lean — new — pure recall scaffolding +- Sec04_26/Exercise_4_42.lean — new — pure recall of 4.41 +- Sec04_26/Exercise_4_44.lean — new — pure recall of 4.43 +- Sec04_26/Exercise_4_45.lean — new — boundary-framework sorry stub +- Sec04_26/Proposition_4_41.lean — new — all-sorry boundary-version main result +- Sec04_27/Problem_4_1.lean — new — thin-wrapper single counterexample +- Sec04_27/Problem_4_10.lean — new — single-sorry statement +- Sec04_27/Problem_4_13.lean — new — statement depends on unproved infrastructure +- Sec04_27/Problem_4_2.lean — mathlib-dup — one-line specialization +- Sec04_27/Problem_4_4.lean — new — pure bookkeeping recall +- Sec04_27/Problem_4_8.lean — new — all-sorry counterexample +- Sec04_27/Problem_4_9.lean — new — pure recall view
-## 小结 +## Summary -第四章（浸入、淹没、嵌入与覆盖映射）是整个审计中移植价值最高的章节之一：16 个高价值文件中多数完全无 sorry，包括流形版反函数定理（Mathlib 明确 TODO）、光滑淹没与光滑覆盖映射的完整定义层 API、拓扑覆盖提升唯一光滑结构的 700 行大定理，以及 CP^n 商淹没与 CP^1 ≅ S^2 的完整构造。中价值条目主要是设计良好但证明缺失的语句骨架（秩定理、全局秩定理、商流形特征性质），移植它们等于承诺补全秩定理级别的证明工作。建议优先按 Submersion → CoveringMap → InverseFunctionTheorem 的依赖顺序成块移植无 sorry 文件，再以其为基础逐步补证 IsSmoothSubmersion 上游的局部截面定理。 +Chapter 4 (immersions, submersions, embeddings, and covering maps) is one of the highest port-value chapters in the whole audit: most of the 16 high-value files are completely sorry-free, including the manifold-version inverse function theorem (an explicit Mathlib TODO), the complete definition-layer API for smooth submersions and smooth covering maps, the 700-line major theorem on unique smooth structure lifted along a topological cover, and the full construction of the CP^n quotient submersion together with CP^1 ≅ S^2. The medium-value entries are mostly well-designed but proof-missing statement skeletons (rank theorem, global rank theorem, quotient-manifold characteristic property); porting them amounts to committing to rank-theorem-level proof work. Recommendation: prioritize porting the sorry-free files in blocks following the dependency order Submersion → CoveringMap → InverseFunctionTheorem, then build on them to gradually complete the local-section theorem upstream of IsSmoothSubmersion. + +--- --- # Chap05 -## 移植优先（high，18 项） +## Port priority (high, 18 items) -| 文件 | 声明 | 分类 | 落点 | sorry | 理由 | +| File | Declarations | Class | Target | sorry | Rationale | |---|---|---|---|---|---| -| Sec05_28/Definition_5_28_extra_1.lean | IsEmbeddedSubmanifold、IsEmbeddedSubmanifold.codimension 等 | new | Manifold/Submanifold/Embedded | 否 | 嵌入子流形类填 Mathlib 空白，需 Sec05_31 浸入结构 | -| Sec05_28/Proposition_5_4.lean | graphMap、graphMap_isSmoothEmbedding 等 | new | Manifold/Submanifold/Graph | 是 | 光滑映射的图作光滑嵌入，Mathlib 缺，GMT 基础 | -| Sec05_29/Definition_5_29_extra_1.lean | Set.euclideanSlice、Set.IsSliceInChart 等 | new | Manifold/SliceCharts | 否 | 切片图卡/局部切片条件 API，子流形理论根基 | -| Sec05_29/Theorem_5_8.lean | local_slice_criterion_for_embedded_submanifold 等 | new | Manifold/SliceCharts | 否 | 局部 k-切片判据无 sorry 全证，Mathlib 空白 | -| Sec05_30/Proposition_5_16.lean | euclidean_tail_projection、embedded_submanifold_iff_locally_level_set_of_smooth_submersion 等 | new | Manifold/Submanifold/LocalDefining | 是 | 浸没水平集局部判据，投影引理已证，主 iff 仍 sorry | -| Sec05_31/Definition_5_31_extra_1.lean | Manifold.ImmersedSubmanifold、IsImmersion.toImmersedSubmanifold 等 | new | Manifold/Submanifold/Immersed | 否 | 无 sorry 捆绑浸入子流形结构，varifold 代码直接受益 | -| Sec05_32/Corollary_5_30.lean | IsSmoothEmbedding.contMDiff_toSubtype、contMDiffAt_toSubtype 等 | new | Manifold/Submanifold | 否 | 一般余域限制定理已证，Mathlib 仅有球面特例 | -| Sec05_35/Corollary_5_39.lean | tangent_iff_mfderiv_eq_zero_of_isDefiningFunction 等 | new | Submanifold/LevelSet | 否 | 正则值切空间刻画已证，但依赖含 sorry 的命题 5.38 | -| Sec05_35/Definition_5_35_extra_2.lean | IsInwardPointing、IsBoundaryTangentVector 等 | new | Boundary/PointingVectors | 否 | 内外指向向量 API 填散度定理缺口，定义需重设计 | -| Sec05_35/Notation_5_35_extra_1.lean | Manifold.submanifoldTangentSpace、T[J; p] 记号 | new | Submanifold/TangentSpace | 否 | 子流形切空间核心定义，全节定理之基石 | -| Sec05_35/Proposition_5_35.lean | tangentVector_mem_submanifold_iff_exists_curve 等 | new | Submanifold/TangentSpace | 否 | 切向量即曲线速度，全证，需 Chap03 曲线基建 | -| Sec05_35/Proposition_5_38.lean | IsLocalDefiningMapOn、tangentSpace_eq_ker_mfderiv_of_isLocalDefiningMapOn | new | Submanifold/LevelSet | 是 | 局部定义映射核心 API，5.39/5.40 依赖，主定理 sorry | -| Sec05_36/Definition_5_36_extra_4.lean | Set.euclideanHalfSlice、OpenPartialHomeomorph.IsBoundarySliceChart 等 | new | Manifold/SliceCharts | 否 | 带边界半切片图卡 API 无 sorry，需 Sec05_29 配套 | -| Sec05_36/Theorem_5_51.lean | local_slice_criterion_for_embedded_submanifold_with_boundary 等 | new | Manifold/SubmanifoldWithBoundary | 是 | 带边界 k-切片判据约 2000 行，核心三处 sorry 待补 | -| Sec05_37/Problem_5_18.lean | immersed_submanifold_isEmbeddedSubmanifold_iff_smoothFunctions_isSmoothOn 等 | new | Manifold/Submanifold/SmoothExtension | 否 | 嵌入 iff 光滑函数可延拓，无 sorry 可复用 API | -| Sec05_37/Problem_5_23.lean | IsBoundaryRegularValue、regular_preimage_has_embedded_submanifold_with_boundary_structure 等 | new | Manifold/Submanifold/RegularValue | 是 | 带边界正则值原像定理大部已证，余两引理 sorry | -| Sec05_37/Problem_5_8.lean | basis_model_diffeomorph、regularCoordinateBall_compl_boundary_diffeomorph_sphere 等 | new | Manifold/CoordinateBall | 是 | 正则坐标球/正则域基建近完成，仅余一处 sorry | -| Sec05_36/Proposition_5_49.lean | isSmoothEmbedding_of_le、immersed_submanifold_has_embedded_neighborhood 等 | partial-dup | Manifold/Submanifold | 否 | 嵌入像诱导结构已证，超出 Mathlib SmoothEmbedding | - -
可考虑（medium，33 项） - -| 文件 | 声明 | 分类 | 落点 | sorry | 理由 | +| Sec05_28/Definition_5_28_extra_1.lean | IsEmbeddedSubmanifold, IsEmbeddedSubmanifold.codimension, etc. | new | Manifold/Submanifold/Embedded | no | Embedded submanifold class fills a Mathlib gap; needs the Sec05_31 immersion structure | +| Sec05_28/Proposition_5_4.lean | graphMap, graphMap_isSmoothEmbedding, etc. | new | Manifold/Submanifold/Graph | yes | Graph of a smooth map as a smooth embedding; missing from Mathlib, GMT foundation | +| Sec05_29/Definition_5_29_extra_1.lean | Set.euclideanSlice, Set.IsSliceInChart, etc. | new | Manifold/SliceCharts | no | Slice-chart / local-slice-condition API, the bedrock of submanifold theory | +| Sec05_29/Theorem_5_8.lean | local_slice_criterion_for_embedded_submanifold, etc. | new | Manifold/SliceCharts | no | Local k-slice criterion fully proved sorry-free, a Mathlib gap | +| Sec05_30/Proposition_5_16.lean | euclidean_tail_projection, embedded_submanifold_iff_locally_level_set_of_smooth_submersion, etc. | new | Manifold/Submanifold/LocalDefining | yes | Local criterion for submersion level sets; projection lemma proved, main iff still sorry | +| Sec05_31/Definition_5_31_extra_1.lean | Manifold.ImmersedSubmanifold, IsImmersion.toImmersedSubmanifold, etc. | new | Manifold/Submanifold/Immersed | no | Sorry-free bundled immersed-submanifold structure; varifold code benefits directly | +| Sec05_32/Corollary_5_30.lean | IsSmoothEmbedding.contMDiff_toSubtype, contMDiffAt_toSubtype, etc. | new | Manifold/Submanifold | no | General codomain-restriction theorem proved; Mathlib has only the sphere special case | +| Sec05_35/Corollary_5_39.lean | tangent_iff_mfderiv_eq_zero_of_isDefiningFunction, etc. | new | Submanifold/LevelSet | no | Regular-value tangent-space characterization proved, but depends on Proposition 5.38 which contains sorry | +| Sec05_35/Definition_5_35_extra_2.lean | IsInwardPointing, IsBoundaryTangentVector, etc. | new | Boundary/PointingVectors | no | Inward/outward-pointing vector API fills the divergence-theorem gap; definitions need redesign | +| Sec05_35/Notation_5_35_extra_1.lean | Manifold.submanifoldTangentSpace, T[J; p] notation | new | Submanifold/TangentSpace | no | Core definition of the submanifold tangent space, cornerstone of the whole section's theorems | +| Sec05_35/Proposition_5_35.lean | tangentVector_mem_submanifold_iff_exists_curve, etc. | new | Submanifold/TangentSpace | no | Tangent vector as curve velocity, fully proved; needs the Chap03 curve infrastructure | +| Sec05_35/Proposition_5_38.lean | IsLocalDefiningMapOn, tangentSpace_eq_ker_mfderiv_of_isLocalDefiningMapOn | new | Submanifold/LevelSet | yes | Core local-defining-map API on which 5.39/5.40 depend; main theorem sorry | +| Sec05_36/Definition_5_36_extra_4.lean | Set.euclideanHalfSlice, OpenPartialHomeomorph.IsBoundarySliceChart, etc. | new | Manifold/SliceCharts | no | Boundary half-slice-chart API, sorry-free; needs the Sec05_29 counterpart | +| Sec05_36/Theorem_5_51.lean | local_slice_criterion_for_embedded_submanifold_with_boundary, etc. | new | Manifold/SubmanifoldWithBoundary | yes | Boundary k-slice criterion, ~2000 lines, three core sorries to fill | +| Sec05_37/Problem_5_18.lean | immersed_submanifold_isEmbeddedSubmanifold_iff_smoothFunctions_isSmoothOn, etc. | new | Manifold/Submanifold/SmoothExtension | no | Embedded iff smooth functions extend; sorry-free, reusable API | +| Sec05_37/Problem_5_23.lean | IsBoundaryRegularValue, regular_preimage_has_embedded_submanifold_with_boundary_structure, etc. | new | Manifold/Submanifold/RegularValue | yes | Boundary regular-value preimage theorem mostly proved, two lemmas remain sorry | +| Sec05_37/Problem_5_8.lean | basis_model_diffeomorph, regularCoordinateBall_compl_boundary_diffeomorph_sphere, etc. | new | Manifold/CoordinateBall | yes | Regular-coordinate-ball / regular-domain infrastructure nearly complete, only one sorry left | +| Sec05_36/Proposition_5_49.lean | isSmoothEmbedding_of_le, immersed_submanifold_has_embedded_neighborhood, etc. | partial-dup | Manifold/Submanifold | no | Embedded-image induced structure proved, goes beyond Mathlib's SmoothEmbedding | + +
Consider (medium, 33 items) + +| File | Declarations | Class | Target | sorry | Rationale | |---|---|---|---|---|---| -| Sec05_28/Proposition_5_2.lean | IsInducedImageManifoldStructure、smooth_embedding_range_has_induced_manifold_structure 等 | new | Manifold/Submanifold/InducedStructure | 是 | 像上诱导结构是基石，但定理全 sorry 且 API 需重做 | -| Sec05_28/Proposition_5_3.lean | productSliceMap、productSliceMap_isSmoothEmbedding 等 | new | Manifold/Submanifold/Product | 是 | 切片嵌入 x↦(x,p) 小引理可用，主定理全 sorry | -| Sec05_28/Proposition_5_7.lean | smooth_map_graph_isProperlyEmbedded | new | Manifold/Submanifold/Graph | 是 | 全局图真嵌入，单条 sorry，应与命题 5.4 同移植 | -| Sec05_29/Exercise_5_10.lean | sphericalCoordinates、sphericalCoordinates_mem_maximalAtlas 等 | new | Instances/SphericalCoordinates | 否 | 三维球坐标图卡全证，但属具体图卡非通用基建 | -| Sec05_30/Corollary_5_13.lean | smooth_submersion_level_set_has_embedded_submanifold_structure 等 | new | Manifold/Submanifold/LevelSet | 否 | 浸没水平集推论为薄包装，依赖含 sorry 定理 5.12 | -| Sec05_30/Corollary_5_14.lean | regular_level_set_has_embedded_submanifold_structure 等 | new | Manifold/Submanifold/LevelSet | 是 | 正则水平集定理填空白，但全 sorry 需从头证 | -| Sec05_30/Definition_5_30_extra_2.lean | Manifold.IsRegularPoint、Manifold.IsCriticalValue 等 | new | Manifold/Submanifold/RegularValue | 是 | 正则/临界点词汇缺失，但支撑引理全 sorry | -| Sec05_30/Definition_5_30_extra_3.lean | Set.IsDefiningMap、Set.IsLocalDefiningMapOn 等 | new | Manifold/Submanifold/DefiningMap | 是 | 定义映射 API 空白，但类设计需大幅重做 | -| Sec05_30/Theorem_5_12.lean | constant_rank_level_set_has_embedded_submanifold_structure 等 | new | Manifold/Submanifold/LevelSet | 是 | 常秩水平集定理为关键空白，全 sorry 仅语句可移 | -| Sec05_31/Definition_5_31_extra_2.lean | ImmersedSubmanifold.IsLocalParametrization、IsGlobalParametrization 等 | new | Manifold/Submanifold/Parametrization | 是 | 参数化谓词新颖，但硬编码 Fin k，API 需重做 | -| Sec05_31/Exercise_5_20.lean | ImmersedSubmanifold.continuous_inclusion、subspaceTopology_le_givenTopology_iff_isEmbedding 等 | new | Manifold/Submanifold/Immersed | 否 | 已证核心 API，应与 Definition_5_31_extra_1 同移植 | -| Sec05_31/Proposition_5_18.lean | injective_immersion_range_has_immersed_submanifold_structure 等 | new | Manifold/Submanifold/Immersed | 是 | 单射浸入像结构存在唯一性，仅语句无证明 | -| Sec05_31/Proposition_5_22.lean | ImmersedSubmanifold.exists_open_neighborhood_isSmoothEmbedding | new | Manifold/Submanifold/Immersed | 是 | 浸入子流形局部嵌入有用，但全文单条 sorry 语句 | -| Sec05_31/Proposition_5_23.lean | IsImmersion.isSmoothLocalParametrization_of_mem_maximalAtlas 等 | new | Manifold/Submanifold/Parametrization | 否 | 图卡给局部参数化已证，但绑定待重做的定义 | -| Sec05_32/Remark_5_32_extra_1.lean | IsWeaklyEmbeddedSubmanifold 实例 | new | Manifold/Submanifold | 否 | 嵌入蕴含弱嵌入的胶水实例，须随子流形类同移 | -| Sec05_32/Theorem_5_29.lean | contMDiff_toSubtype_of_isImmersedSubmanifold | new | Manifold/Submanifold | 是 | 推广推论 5.30 的余域限制，仅语句需从头证 | -| Sec05_33/Theorem_5_31.lean | immersed_submanifold_structure_unique_of_same_carrier | new | Manifold/Submanifold | 是 | 子流形结构唯一性 sorry 语句，需全套 API 加真证明 | -| Sec05_35/Definition_5_35_extra_3.lean | BoundaryDefiningFunction、CoeFun 实例 | new | Boundary/DefiningFunction | 否 | 捆绑边界定义函数，硬编码半空间且与 5.43 重复 | -| Sec05_35/Exercise_5_40.lean | tangentSpace_eq_ker_mfderiv_of_level_set_of_hasConstantRank 等 | new | Submanifold/LevelSet | 是 | 常秩水平集切空间，关键引理 sorry 且与 5.39 重复 | -| Sec05_35/Exercise_5_44.lean | boundary_defining_derivative、inwardPointing_iff_boundaryDefiningDerivative_pos 等 | new | Boundary/DefiningFunction | 是 | 导数符号刻画内外向是对的 API，四定理全 sorry | -| Sec05_35/Proposition_5_37.lean | tangentVector_mem_submanifold_iff_forall_smooth_eq_zero | new | Submanifold/TangentSpace | 是 | 函数式切向刻画，单条 sorry，证明需延拓引理 | -| Sec05_35/Proposition_5_41.lean | boundary_coordinate_component、boundary_vector_trichotomy 等 | new | Boundary/PointingVectors | 是 | 边界向量坐标三分法配套定理，八条全 sorry | -| Sec05_35/Proposition_5_43.lean | IsBoundaryDefiningFunction、exists_boundary_defining_function | new | Boundary/DefiningFunction | 是 | 全局边界定义函数存在性 sorry，与 extra_3 重复 | -| Sec05_36/Definition_5_36_extra_2.lean | Set.IsRegularDomain、instIsRegularDomainEmpty | new | Manifold/RegularDomain | 否 | 正则域即散度定理积分域，依项目脚手架需重建 | -| Sec05_36/Definition_5_36_extra_3.lean | Manifold.IsRegularValue、IsRegularSublevelSet 等 | new | Manifold/RegularValue | 是 | 正则值概念填空白，iff 引理 sorry，设计需改 | -| Sec05_36/Proposition_5_46.lean | regular_domain_manifoldInterior_image_eq_interior 等 | new | Manifold/RegularDomain | 是 | 正则域内部/边界对应拓扑内部/边缘，证明全 sorry | -| Sec05_37/Problem_5_15.lean | transported_subset_chartedSpace、transported_subset_isManifold_top 等 | new | Manifold/StructureTransport | 否 | 结构沿同胚移植引理族已证可复用，反例部分教材性 | -| Sec05_37/Problem_5_19.lean | curve_velocity_mem_embedded_submanifold_tangent 等 | new | Manifold/Submanifold/Tangent | 否 | 曲线速度落入切子空间已证，半个文件是反例 | -| Sec05_37/Problem_5_4.lean | continuous_injective_interval_to_curve_manifold_isEmbedding 等 | new | Manifold/CurveEmbedding | 否 | 一维区域不变性辅助引理无 sorry，Mathlib 缺 | -| Sec05_37/Problem_5_5.lean | continuous_injective_real_to_curve_manifold_isEmbedding 等 | new | Manifold/CurveEmbedding | 否 | 实线入一维流形嵌入引理已证，宜与 5.4 并为一模块 | -| Sec05_37/Problem_5_6.lean | unitTangentBundle、unitTangentBundle_exists_isSmoothEmbedding 等 | new | TangentBundle/UnitTangentBundle | 是 | 单位切丛各处皆无，但主定理全 sorry，仅 API 种子 | -| Sec05_28/Proposition_5_1.lean | open_submanifold_isEmbeddedSubmanifold 等 | partial-dup | Manifold/Submanifold/Open | 是 | 部分重复 Mathlib of_opens，逆命题全 sorry 需推广 | -| Sec05_32/Definition_5_32_extra_2.lean | IsImmersedSubmanifold、IsWeaklyEmbeddedSubmanifold 等 | partial-dup | Manifold/Submanifold | 否 | 子流形谓词类填空白，API 需重做且一辅助重复 Mathlib | +| Sec05_28/Proposition_5_2.lean | IsInducedImageManifoldStructure, smooth_embedding_range_has_induced_manifold_structure, etc. | new | Manifold/Submanifold/InducedStructure | yes | Induced structure on the image is foundational, but the theorem is all sorry and the API needs reworking | +| Sec05_28/Proposition_5_3.lean | productSliceMap, productSliceMap_isSmoothEmbedding, etc. | new | Manifold/Submanifold/Product | yes | Slice-embedding x↦(x,p) small lemma usable, main theorem all sorry | +| Sec05_28/Proposition_5_7.lean | smooth_map_graph_isProperlyEmbedded | new | Manifold/Submanifold/Graph | yes | Global graph proper embedding, single sorry, should be ported together with Proposition 5.4 | +| Sec05_29/Exercise_5_10.lean | sphericalCoordinates, sphericalCoordinates_mem_maximalAtlas, etc. | new | Instances/SphericalCoordinates | no | 3D spherical-coordinate chart fully proved, but a concrete chart rather than general infrastructure | +| Sec05_30/Corollary_5_13.lean | smooth_submersion_level_set_has_embedded_submanifold_structure, etc. | new | Manifold/Submanifold/LevelSet | no | Submersion level-set corollary is a thin wrapper, depends on Theorem 5.12 which contains sorry | +| Sec05_30/Corollary_5_14.lean | regular_level_set_has_embedded_submanifold_structure, etc. | new | Manifold/Submanifold/LevelSet | yes | Regular level-set theorem fills a gap, but is all sorry and needs proving from scratch | +| Sec05_30/Definition_5_30_extra_2.lean | Manifold.IsRegularPoint, Manifold.IsCriticalValue, etc. | new | Manifold/Submanifold/RegularValue | yes | Regular/critical-point vocabulary missing, but supporting lemmas all sorry | +| Sec05_30/Definition_5_30_extra_3.lean | Set.IsDefiningMap, Set.IsLocalDefiningMapOn, etc. | new | Manifold/Submanifold/DefiningMap | yes | Defining-map API is a gap, but the class design needs major reworking | +| Sec05_30/Theorem_5_12.lean | constant_rank_level_set_has_embedded_submanifold_structure, etc. | new | Manifold/Submanifold/LevelSet | yes | Constant-rank level-set theorem is a key gap, all sorry, only the statement is portable | +| Sec05_31/Definition_5_31_extra_2.lean | ImmersedSubmanifold.IsLocalParametrization, IsGlobalParametrization, etc. | new | Manifold/Submanifold/Parametrization | yes | Parametrization predicates are novel, but hard-code Fin k, API needs reworking | +| Sec05_31/Exercise_5_20.lean | ImmersedSubmanifold.continuous_inclusion, subspaceTopology_le_givenTopology_iff_isEmbedding, etc. | new | Manifold/Submanifold/Immersed | no | Core API proved, should be ported together with Definition_5_31_extra_1 | +| Sec05_31/Proposition_5_18.lean | injective_immersion_range_has_immersed_submanifold_structure, etc. | new | Manifold/Submanifold/Immersed | yes | Existence-uniqueness of the injective-immersion image structure, statement only, no proof | +| Sec05_31/Proposition_5_22.lean | ImmersedSubmanifold.exists_open_neighborhood_isSmoothEmbedding | new | Manifold/Submanifold/Immersed | yes | Local embedding of immersed submanifolds is useful, but the whole file is a single sorry statement | +| Sec05_31/Proposition_5_23.lean | IsImmersion.isSmoothLocalParametrization_of_mem_maximalAtlas, etc. | new | Manifold/Submanifold/Parametrization | no | Chart gives local parametrization, proved, but bound to definitions awaiting rework | +| Sec05_32/Remark_5_32_extra_1.lean | IsWeaklyEmbeddedSubmanifold instance | new | Manifold/Submanifold | no | Glue instance for embedded implies weakly embedded, must move with the submanifold class | +| Sec05_32/Theorem_5_29.lean | contMDiff_toSubtype_of_isImmersedSubmanifold | new | Manifold/Submanifold | yes | Codomain restriction generalizing Corollary 5.30, statement only, needs proving from scratch | +| Sec05_33/Theorem_5_31.lean | immersed_submanifold_structure_unique_of_same_carrier | new | Manifold/Submanifold | yes | Uniqueness of submanifold structure, sorry statement, needs the full API plus a real proof | +| Sec05_35/Definition_5_35_extra_3.lean | BoundaryDefiningFunction, CoeFun instance | new | Boundary/DefiningFunction | no | Bundled boundary defining function, hard-codes the half-space and duplicates 5.43 | +| Sec05_35/Exercise_5_40.lean | tangentSpace_eq_ker_mfderiv_of_level_set_of_hasConstantRank, etc. | new | Submanifold/LevelSet | yes | Constant-rank level-set tangent space, key lemma sorry and duplicates 5.39 | +| Sec05_35/Exercise_5_44.lean | boundary_defining_derivative, inwardPointing_iff_boundaryDefiningDerivative_pos, etc. | new | Boundary/DefiningFunction | yes | Derivative-sign characterization of inward/outward is the right API, all four theorems sorry | +| Sec05_35/Proposition_5_37.lean | tangentVector_mem_submanifold_iff_forall_smooth_eq_zero | new | Submanifold/TangentSpace | yes | Functional tangent-vector characterization, single sorry, proof needs the extension lemma | +| Sec05_35/Proposition_5_41.lean | boundary_coordinate_component, boundary_vector_trichotomy, etc. | new | Boundary/PointingVectors | yes | Companion theorems for the boundary-vector coordinate trichotomy, all eight sorry | +| Sec05_35/Proposition_5_43.lean | IsBoundaryDefiningFunction, exists_boundary_defining_function | new | Boundary/DefiningFunction | yes | Existence of a global boundary defining function, sorry, duplicates extra_3 | +| Sec05_36/Definition_5_36_extra_2.lean | Set.IsRegularDomain, instIsRegularDomainEmpty | new | Manifold/RegularDomain | no | Regular domain is the divergence-theorem integration domain, needs rebuilding per project scaffolding | +| Sec05_36/Definition_5_36_extra_3.lean | Manifold.IsRegularValue, IsRegularSublevelSet, etc. | new | Manifold/RegularValue | yes | Regular-value concept fills a gap, iff lemma sorry, design needs changing | +| Sec05_36/Proposition_5_46.lean | regular_domain_manifoldInterior_image_eq_interior, etc. | new | Manifold/RegularDomain | yes | Regular-domain interior/boundary correspond to topological interior/frontier, proof all sorry | +| Sec05_37/Problem_5_15.lean | transported_subset_chartedSpace, transported_subset_isManifold_top, etc. | new | Manifold/StructureTransport | no | Family of structure-transport-along-homeomorphism lemmas proved and reusable, counterexample part is textbook-ish | +| Sec05_37/Problem_5_19.lean | curve_velocity_mem_embedded_submanifold_tangent, etc. | new | Manifold/Submanifold/Tangent | no | Curve velocity lands in the tangent subspace, proved; half the file is a counterexample | +| Sec05_37/Problem_5_4.lean | continuous_injective_interval_to_curve_manifold_isEmbedding, etc. | new | Manifold/CurveEmbedding | no | 1D invariance-of-domain auxiliary lemma, sorry-free, missing from Mathlib | +| Sec05_37/Problem_5_5.lean | continuous_injective_real_to_curve_manifold_isEmbedding, etc. | new | Manifold/CurveEmbedding | no | Real line into a 1-manifold embedding lemma proved, should be combined with 5.4 into one module | +| Sec05_37/Problem_5_6.lean | unitTangentBundle, unitTangentBundle_exists_isSmoothEmbedding, etc. | new | TangentBundle/UnitTangentBundle | yes | Unit tangent bundle absent everywhere, but main theorem all sorry, only an API seed | +| Sec05_28/Proposition_5_1.lean | open_submanifold_isEmbeddedSubmanifold, etc. | partial-dup | Manifold/Submanifold/Open | yes | Partly duplicates Mathlib of_opens, converse all sorry and needs generalizing | +| Sec05_32/Definition_5_32_extra_2.lean | IsImmersedSubmanifold, IsWeaklyEmbeddedSubmanifold, etc. | partial-dup | Manifold/Submanifold | no | Submanifold predicate classes fill a gap, API needs reworking and one helper duplicates Mathlib |
-
跳过（34 项，绝大多数为 Mathlib 包装/recall 文件） - -- Sec05_28/Corollary_5_6.lean — mathlib-dup — 一行复合既有引理 -- Sec05_28/Definition_5_28_extra_2.lean — partial-dup — 薄命名缩写 -- Sec05_28/Proposition_5_5.lean — mathlib-dup — 仅 #check 包装 -- Sec05_29/Example_5_9.lean — partial-dup — 球面 API 重包装 -- Sec05_29/Remark_5_29_extra_2.lean — new — 仅 sorry 语句备注 -- Sec05_29/Remark_5_29_extra_3.lean — new — recall 交叉引用 -- Sec05_30/Definition_5_30_extra_1.lean — mathlib-dup — recall 原像概念 -- Sec05_30/Example_5_15.lean — mathlib-dup — 球面教学复述 -- Sec05_30/Example_5_17.lean — new — 环面例全 sorry -- Sec05_31/Example_5_19.lean — new — 八字反例无 API -- Sec05_31/Example_5_25.lean — new — #check 加平凡推论 -- Sec05_31/Example_5_26.lean — new — 八字脚手架含 sorry -- Sec05_31/Exercise_5_24.lean — new — 仅 recall/#check -- Sec05_32/Example_5_28.lean — new — 八字反例关键 sorry -- Sec05_32/Theorem_5_27.lean — mathlib-dup — recall 加一行特化 -- Sec05_34/Notation_5_34_extra_1.lean — mathlib-dup — 纯记号引用 -- Sec05_35/Definition_5_35_extra_4.lean — new — R² 专用脚手架 -- Sec05_35/Example_5_45.lean — new — 单条平面曲线例 -- Sec05_35/Exercise_5_36.lean — new — 纯 recall 复述 -- Sec05_35/Exercise_5_42.lean — new — recall sorry 语句 -- Sec05_36/Definition_5_36_extra_1.lean — mathlib-dup — #check 复述谓词 -- Sec05_36/Exercise_5_50.lean — partial-dup — recall 重证组合 -- Sec05_36/Exercise_5_52.lean — partial-dup — recall 再导出 -- Sec05_36/Exercise_5_54.lean — partial-dup — recall 指针 -- Sec05_36/Remark_5_36_extra_5.lean — partial-dup — 无声明备注 -- Sec05_36/Theorem_5_53.lean — partial-dup — 一行包装且 sorry -- Sec05_37/Problem_5_1.lean — new — 具体习题无 API -- Sec05_37/Problem_5_10.lean — new — 三次曲线 17 sorry -- Sec05_37/Problem_5_11.lean — new — 具体零集全 sorry -- Sec05_37/Problem_5_12.lean — partial-dup — 新部分全 sorry -- Sec05_37/Problem_5_13.lean — new — 一次性反例含 sorry -- Sec05_37/Problem_5_20.lean — new — 八字反例无 API -- Sec05_37/Problem_5_7.lean — new — 单例分类含 sorry -- Sec05_37/Problem_5_9.lean — new — 单条 sorry 语句 +
Skip (34 items — mostly Mathlib wrappers / recall files) + +- Sec05_28/Corollary_5_6.lean — mathlib-dup — one-line composition of an existing lemma +- Sec05_28/Definition_5_28_extra_2.lean — partial-dup — thin naming abbreviation +- Sec05_28/Proposition_5_5.lean — mathlib-dup — only a #check wrapper +- Sec05_29/Example_5_9.lean — partial-dup — sphere API rewrapped +- Sec05_29/Remark_5_29_extra_2.lean — new — only a sorry-statement remark +- Sec05_29/Remark_5_29_extra_3.lean — new — recall cross-reference +- Sec05_30/Definition_5_30_extra_1.lean — mathlib-dup — recall of the preimage concept +- Sec05_30/Example_5_15.lean — mathlib-dup — pedagogical sphere restatement +- Sec05_30/Example_5_17.lean — new — torus example all sorry +- Sec05_31/Example_5_19.lean — new — figure-eight counterexample, no API +- Sec05_31/Example_5_25.lean — new — #check plus trivial corollary +- Sec05_31/Example_5_26.lean — new — figure-eight scaffolding with sorry +- Sec05_31/Exercise_5_24.lean — new — only recall/#check +- Sec05_32/Example_5_28.lean — new — figure-eight counterexample, key sorry +- Sec05_32/Theorem_5_27.lean — mathlib-dup — recall plus a one-line specialization +- Sec05_34/Notation_5_34_extra_1.lean — mathlib-dup — pure notation reference +- Sec05_35/Definition_5_35_extra_4.lean — new — R²-specific scaffolding +- Sec05_35/Example_5_45.lean — new — single plane-curve example +- Sec05_35/Exercise_5_36.lean — new — pure recall restatement +- Sec05_35/Exercise_5_42.lean — new — recall sorry statement +- Sec05_36/Definition_5_36_extra_1.lean — mathlib-dup — #check predicate restatement +- Sec05_36/Exercise_5_50.lean — partial-dup — recall reproof combination +- Sec05_36/Exercise_5_52.lean — partial-dup — recall re-derivation +- Sec05_36/Exercise_5_54.lean — partial-dup — recall pointer +- Sec05_36/Remark_5_36_extra_5.lean — partial-dup — remark with no declarations +- Sec05_36/Theorem_5_53.lean — partial-dup — one-line wrapper with sorry +- Sec05_37/Problem_5_1.lean — new — concrete exercise, no API +- Sec05_37/Problem_5_10.lean — new — cubic curve, 17 sorries +- Sec05_37/Problem_5_11.lean — new — concrete zero set all sorry +- Sec05_37/Problem_5_12.lean — partial-dup — new part all sorry +- Sec05_37/Problem_5_13.lean — new — one-off counterexample with sorry +- Sec05_37/Problem_5_20.lean — new — figure-eight counterexample, no API +- Sec05_37/Problem_5_7.lean — new — single-example classification with sorry +- Sec05_37/Problem_5_9.lean — new — single sorry statement
-## 小结 +## Summary + +This chapter (Chapter 5: submanifold theory) is the highest-value chapter to port in the entire audit: embedded/immersed submanifold classes, slice-chart criteria, submanifold tangent spaces, local defining maps, and boundary-vector APIs — 18 high-value files in total, almost all Mathlib gaps and more than half sorry-free, directly able to support OpenGALib's GMT and divergence-theorem gaps. The recommendation is to use the three main lines SliceCharts, Submanifold/Immersed+Embedded, and Submanifold/TangentSpace as the skeleton, porting the sorry-free files first, then using the level-set and boundary series from the medium table to fill in the statement layer. The low-value entries are mostly concrete textbook counterexamples and recall scaffolding, and can be skipped wholesale. -本章（第五章：子流形理论）是整个审计中移植价值最高的一章：嵌入/浸入子流形类、切片图卡判据、子流形切空间、局部定义映射与边界向量 API 共 18 个高价值文件，几乎全部为 Mathlib 空白且半数以上 sorry-free，可直接支撑 OpenGALib 的 GMT 与散度定理缺口。建议以 SliceCharts、Submanifold/Immersed+Embedded、Submanifold/TangentSpace 三条主线为骨架先移植无 sorry 文件，再用 medium 表中的 level-set 与 boundary 系列补全语句层。低价值条目以教材具体反例与 recall 脚手架为主，可整体跳过。