SmoothManifoldsLee 大分支整合：方案讨论（流程 / 自动化流水线 / 评审分配）

[Xinze-Li-Moqian]

背景

@LehengChen 推送的 import/smooth-manifolds-lee（a5f308c）包含 Lee《Introduction to Smooth Manifolds》第 1–5 章的形式化：346 个文件、约 6.2 万行，自包含、仅依赖 Mathlib，与 OpenGALib 现有代码零依赖、零重复。

核心问题：如何把以教材为顺序的形式化，转化为可复用性、可维护性、可延伸性极高的软件，并把转化过程本身做成可重复的流程。

全量重叠审计结论（2026-06-12）

• 分类：187 全新 / 95 Mathlib 重复（教材编号式包装，跳过）/ 57 部分重复
• 价值：52 个高价值文件（子流形、切片图卡、浸没、覆盖映射、带边流形为主）
• 与 OpenGALib 现有代码零重复——我们从黎曼度量层起步，Lee 覆盖的子流形/浸入/坐标球层正是库里缺的中间层

方案文档（请先读这两份）

在分支 docs/sml-integration-plan 的 docs/log/2026-06-12-smooth-manifolds-lee/ 下：

1. PLAN.md — 事件与问题定义、分支与移植流程（import/* 冻结快照永不 merge、一单一 port/* 分支、质量门）、自动化流水线设想（两条常驻约束：通用层优先、语义符合）、人工评审分配（最小可信基 + 核心节点 CODEOWNERS）
2. WORKLIST.md — 逐章审计结果、五个共用设施层、9 张施工单台账（首单 port/manifold-typeclass-core）

讨论定稿后这两份文档随小 PR 合入 develop，本 issue 作为整合工作的总追踪点。

待讨论 / 待决定

• 施工单粒度与依赖排序是否合理（特别是首单先定打包类约定）
• TopologicalManifold n M（显式维数）收编进 SmoothManifold M 谱系时，维数参数去留
• 带边流形支持的优先级（它是 GMT 散度定理的前提）
• @LehengChen：上游后续快照推 import/smooth-manifolds-lee-v2、不 force-push，是否可行
• Chap04 秩理论（rankAt/HasConstantRank）陈述层含 sorry：整段推迟还是优先补证明
• 三个新 linter（Math./Eng. docstring 对、命名空间白名单、出处行）是否进 OpenGALib/Util/Linter/
• 核心节点入度阈值（建议内部被引 ≥ 5 入选，首版清单随首单提交）
• CODEOWNERS 专家映射：流形地基 / 子流形与切片 / 带边与 GMT 接口各归谁
• 人审时限（建议核心节点 PR 三个工作日内响应）

关联：import/smooth-manifolds-lee（a5f308c）