port(charted-space-core): 由图册核造流形（ChartedSpaceCore）

[LehengChen]

port(charted-space-core): manifold structure from a ChartedSpaceCore

What this ports

Lee, Introduction to Smooth Manifolds, §1, Lemma 1.35 (parts 1–4):
the separation, countability, smoothness and uniqueness properties of the
topology that a chart-family core (ChartedSpaceCore) generates on its
underlying set.

Source	Landing
Chap01/Sec01_04/Lemma_1_35.lean	OpenGALib/Manifold/Charts/ChartedSpaceCore.lean

Index wiring:

• OpenGALib/Manifold.lean — added import OpenGALib.Manifold.Charts.ChartedSpaceCore
  (alphabetical, single-line change).
• OpenGALib.lean (root index) — unchanged; already imports OpenGALib.Manifold.

Core objects / results

The ticket lists no core_objects (all four declarations are theorems):

• Manifold.toTopologicalSpace_t2Space — Lemma 1.35 (2): the generated topology
  is Hausdorff when distinct points are separated by a common chart or by
  disjoint chart domains.
• Manifold.toTopologicalSpace_secondCountableTopology — Lemma 1.35 (3): the
  generated topology is second-countable when a countable subatlas covers the space.
• Manifold.toChartedSpace_isManifold — Lemma 1.35 (4): smooth coordinate changes
  make the generated charted space a smooth manifold.
• Manifold.eq_toTopologicalSpace_of_chartedSpace — Lemma 1.35 (1): the generated
  topology is the unique one realizing the chart family as a charted space.

Design-neutral statement

• Stated directly on Mathlib typeclasses: TopologicalSpace, T2Space,
  SecondCountableTopology, ChartedSpace, IsManifold, ModelWithCorners,
  and Mathlib's ChartedSpaceCore structure. No OpenGA SmoothManifold
  packaging class and no Lee TopologicalManifold were introduced or relied on.
• No transforms in the ticket; in particular no restate was required (the
  source already binds the four Mathlib classes individually, not via
  TopologicalManifold).
• The proofs are carried over verbatim from the source; only the surrounding
  namespace changed (see Deviations).

Deviations from a literal copy

• Renamespacing (RUNBOOK §1, design-neutral). The source declares the four
  theorems under namespace ChartedSpaceCore, which is not on the project
  namespace whitelist (OpenGALib, Manifold, Riemannian,
  GeometricMeasureTheory, OpenPartialHomeomorph). Per the namespace policy,
  the declarations were moved into namespace Manifold with their names
  unchanged (toTopologicalSpace_t2Space, etc.). This is a pure namespace
  move, not a rename-to-dodge-the-gate; the Mathlib type ChartedSpaceCore
  itself is untouched and still referenced by its full name inside the proofs
  (e.g. ChartedSpaceCore.toTopologicalSpace).
• Dropped the source's pipeline scaffolding comments (-- Declarations ... appended below, lean_leansearch note) and the bare namespace ChartedSpaceCore wrapper. Added the module docstring (NAMING_CONVENTION
  template + provenance line) and **Math.** / **Eng.** per-declaration
  docstrings required by the docstring gate.
• No inlined dependencies, no Mathlib API renames.

Provenance

import/smooth-manifolds-lee @ a5f308c:

• staging/SmoothManifoldsLee/SmoothManifoldsLee/Chap01/Sec01_04/Lemma_1_35.lean

Gate results (local, full run — all six green)

✓ build           build 通过
✓ no-sorry        改动文件无 sorry
✓ namespace       顶层 namespace 均在白名单内
✓ provenance      出处行齐全
✓ docstring       双 docstring 齐全
✓ linter-baseline 占位通过：自定义 linter 尚未接入（issue #61 待决）

Report: projects/sml-to-openga/ledger/reports/ticket03-20260614T043136Z.json

Review focus (minimal trusted base)

Proofs are kernel-checked. Reviewer need only confirm the statements name
the same mathematical objects as Lee's Lemma 1.35 (1)–(4) — i.e. that the four
theorem signatures (separation hypothesis ⇒ Hausdorff; countable cover ⇒
second-countable; smooth transitions ⇒ IsManifold; charted-space compatibility
⇒ topology uniqueness) faithfully transcribe the source statements after the
ChartedSpaceCore → Manifold namespace move.

Stacking note

Branch port/charted-space-core is cut from the stacked batch tip
port/precompact-basis (not directly from origin/develop). Ticket #3 has no
declared deps; the new module is an independent unit (it does not import the
coordinate-ball or precompact-basis modules).

[Xinze-Li-Moqian]

感谢 #67（由图册核造流形）。现在 develop 上有两个已合并的注释范本可对照：OpenGALib/Manifold/Charts/CoordinateBall.lean（#65）和 PrecompactBasis.lean（#66）。house style 三条：

1. 锚文件只用单 **Math.** 标签——Util/ 之外 AnchorPurity linter 禁 **Eng.**/**Mixed.**。把双标签里的 **Eng.** 段删掉即可（工程细节代码自明）；尤其定理的 Eng 行不要复述证明步骤。
2. 模块注释按架构分层叙事，不按教材顺序；点明哪些是可复用基座、哪些是上层接口。
3. 出处压成一行 Provenance: SmoothManifoldsLee a5f308c — <源文件>，删掉 Reference: Lee §N 与多行 Ported from。

另：#65 已合并，base 可重定向到 develop（你这条目前还挂在上游 port 分支）。namespace Manifold 经核对符合我们域命名空间惯例，保留即可。