port(coordinate-components): 坐标切向量分量

[LehengChen]

port(coordinate-components): 坐标切向量分量 + 图卡坐标基

Port of Lee, Introduction to Smooth Manifolds, §3: the coordinate-component
view of tangent vectors. A smooth chart containing p identifies T_p M with
the model space, yielding (a) the chart-induced coordinate basis of T_p M
(Prop. 3.15(2)), and (b) the coordinate components of a tangent vector in each
preferred chart, which transform by tangentCoordChange on overlaps. The bundled
compatible-family realization CoordinateTangentVector is shown to be canonically
equivalent to T_p M — the same tangent space in a different presentation, not a
second owner type. Conceptually continues #5 (tangent-bundle localization).

Source → landing

Two source files (plus one inlined wrapper) into one new module under
OpenGALib/Manifold/Tangent/:

Source (import/smooth-manifolds-lee @ a5f308c)	Landing	Contributes
Chap03/Sec03_15/Proposition_3_15.lean	CoordinateComponents.lean	chart_mdifferentiable_of_mem_maximalAtlas, chart_coordinate_vectors_basis
Chap03/Sec03_18/Definition_3_18_extra_4.lean	CoordinateComponents.lean	IsCoordinateTangentVector, CoordinateTangentVector (+ component_apply, compatible_apply, ext, CoeFun), coordinateComponent, coordinateComponent_isCoordinateTangentVector, toCoordinateTangentVector, CoordinateTangentVector.{toTangentSpace, coordinateComponent_toTangentSpace, toTangentSpace_toCoordinateTangentVector, toCoordinateTangentVector_toTangentSpace, equivTangentSpace}
Chap03/Sec03_15/Remark_3_15_extra_4.lean (inlined wrapper)	CoordinateComponents.lean	tangent_coordinates_change

Core objects (new)

• Manifold.IsCoordinateTangentVector I p component — compatibility predicate: a
  choice of model-space component in every preferred chart containing p,
  matched by the tangent coordinate-change maps tangentCoordChange I x y p on
  overlaps.
• Manifold.CoordinateTangentVector I p — bundled compatible family of
  preferred-chart components at p (the coordinate-family realization of
  T_p M).
• Manifold.coordinateComponent v x — the component of v : TangentSpace I p in
  the preferred chart centered at x, written in the model vector space E
  (via the tangent-bundle trivialization's fiberwise linear equivalence).

Supporting: chart_coordinate_vectors_basis (Prop. 3.15(2) coordinate basis of
T_p M from a chart); coordinateComponent_isCoordinateTangentVector (chart
components transform correctly); CoordinateTangentVector.equivTangentSpace
(CoordinateTangentVector I p ≃ TangentSpace I p).

设计中立声明 (design-neutral)

• No second packaging class introduced. Everything is stated directly on
  Mathlib's tangent-bundle / chart API: TangentSpace, tangentCoordChange,
  tangentBundleCore, trivializationAt / Bundle.Trivialization.*,
  ModelWithCorners, ChartedSpace, IsManifold, IsManifold.maximalAtlas,
  OpenPartialHomeomorph.MDifferentiable, EuclideanSpace.basisFun,
  Module.Basis. No OpenGA SmoothManifold packaging and no Lee
  TopologicalManifold are touched. CoordinateTangentVector is explicitly a
  re-presentation of TangentSpace I p (equivalence proved), not a rival type.
• No restate transform in this ticket (transforms: []); none applied.
• Proofs are unchanged from source modulo namespace placement (see Deviations).

Deviations / namespacing

• Inlined wrapper tangent_coordinates_change (per ticket note). The source
  Definition_3_18_extra_4.lean imports Remark_3_15_extra_4, a Mathlib-only
  thin wrapper providing tangent_coordinates_change (identifies the
  tangent-bundle trivialization coordChangeL with tangentCoordChange via
  tangentBundleCore.trivializationAt_coordChange_eq). Per the ticket note and
  RUNBOOK policy (do not add a new SmoothManifoldsLee.* import to a
  non-ported source module), the wrapper was inlined verbatim into the
  landing file rather than imported. Its non-declaration #check tangentCoordChange_def
  was dropped. Flagging the inline for review.
• Namespace (renamespacing of Mathlib-type namespaces). Source declarations
  lived under bare namespace TangentSpace (a Mathlib type — non-whitelisted)
  and namespace CoordinateTangentVector (the new type). Per the namespace
  policy all were moved under namespace Manifold (namespace_root) with
  their names preserved. To keep the dot-notation API (v.toTangentSpace,
  v.component, Manifold.CoordinateTangentVector.equivTangentSpace, etc.)
  while passing the lexical namespace gate, the inner CoordinateTangentVector
  declarations use qualified declaration names (CoordinateTangentVector.foo)
  directly inside namespace Manifold instead of a nested
  namespace CoordinateTangentVector block. Resulting fully-qualified names are
  unchanged (Manifold.CoordinateTangentVector.*). The former
  TangentSpace.{coordinateComponent, coordinateComponent_isCoordinateTangentVector, toCoordinateTangentVector} are now Manifold.{coordinateComponent, coordinateComponent_isCoordinateTangentVector, toCoordinateTangentVector}
  (dropped the TangentSpace. prefix; names otherwise verbatim). No
  declaration was renamed to dodge the gate.
• #check-only item not ported (would not compile here).
  Proposition_3_15.lean contained #check tangentSpace_finrank_eq_of_n_dimensional_manifold,
  whose target is an SML-only declaration from Chap03/Sec03_14/Proposition_3_10.lean
  (Prop. 3.10) — not in this ticket's scope and not in Mathlib. The #check
  is a sanity stub, not a declaration; it was dropped (carrying it would break
  the build by referencing an unported symbol). The two real declarations of
  Prop. 3.15 (chart_mdifferentiable_of_mem_maximalAtlas,
  chart_coordinate_vectors_basis) are pure-Mathlib and ported unchanged.
• Added docstring on the CoeFun instance. The source CoeFun instance had no
  docstring; a Math./Eng. docstring was added to satisfy the docstring gate
  (no change to the instance).
• Imports. Added Mathlib.Analysis.InnerProductSpace.PiL2 (for
  EuclideanSpace / EuclideanSpace.basisFun, reached transitively in the
  source via Proposition_3_10) and Mathlib.Geometry.Manifold.VectorBundle.Tangent
  (for tangentBundleCore / tangentCoordChange, from the inlined wrapper)
  alongside the source imports …ContMDiff.Atlas, …MFDeriv.Atlas. Dropped the
  source import SmoothManifoldsLee.* lines.
• Overlap with existing OpenGA code. None. Grep over OpenGALib/ shows no
  pre-existing IsCoordinateTangentVector, CoordinateTangentVector,
  coordinateComponent, or the chart-basis theorem names.
• Mathlib API. No renames. All referenced lemmas exist verbatim on the
  current toolchain: contMDiffOn_of_mem_maximalAtlas,
  contMDiffOn_symm_of_mem_maximalAtlas, ContMDiffOn.mdifferentiableOn,
  OpenPartialHomeomorph.MDifferentiable.mfderiv, EuclideanSpace.basisFun,
  Module.Basis.map, Bundle.Trivialization.{linearEquivAt, coordChangeL_apply, symm_apply_apply_mk}, TangentBundleCore.trivializationAt_coordChange_eq,
  mem_chart_source.

出处 (provenance)

import/smooth-manifolds-lee @ a5f308c, subpath
staging/SmoothManifoldsLee/SmoothManifoldsLee:

• Chap03/Sec03_15/Proposition_3_15.lean
• Chap03/Sec03_18/Definition_3_18_extra_4.lean
• Chap03/Sec03_15/Remark_3_15_extra_4.lean (inlined wrapper)

The three provenance lines are embedded in the landing file's module docstring.

Index wiring

• OpenGALib/Manifold.lean — added
  import OpenGALib.Manifold.Tangent.CoordinateComponents (alphabetical, after
  the Cutoff.Exhaustion line, before Tangent.CurveVelocity).
• OpenGALib.lean already imports OpenGALib.Manifold; no change needed.

Branch

port/coordinate-components, cut from the stacked stack tip
port/curve-velocity-mfderiv (ticket #5, not origin/develop). Files:

• new: OpenGALib/Manifold/Tangent/CoordinateComponents.lean
• modified: OpenGALib/Manifold.lean

Gate 结果 (all six green)

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

Report: projects/sml-to-openga/ledger/reports/ticket06-20260614T045001Z.json
(full lake build, cache warm; 0 sorry).

评审重点 (minimal trusted base)

Proofs are kernel-checked; please focus review on whether the definitions and
statements name the same mathematical objects as Lee §3:

• Manifold.coordinateComponent v x ≙ the component of v ∈ T_p M in the chart
  centered at x;
• Manifold.IsCoordinateTangentVector / CoordinateTangentVector ≙ a tangent
  vector presented as a coordinate-compatible family
  (transformation rule via tangentCoordChange);
• CoordinateTangentVector.equivTangentSpace : CoordinateTangentVector I p ≃ TangentSpace I p
  ≙ this family realization is the same object as T_p M;
• chart_coordinate_vectors_basis ≙ Prop. 3.15(2) coordinate basis of T_p M
  from a smooth chart;
• the inlined tangent_coordinates_change ≙ Remark 3.15-extra-4 (trivialization
  coordChange = tangentCoordChange).

[Xinze-Li-Moqian]

感谢 #70（坐标切向量分量）。现在 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 经核对符合我们域命名空间惯例，保留即可。

本 PR 额外两项：

• chart_coordinate_vectors_basis 是 snake_case → chartCoordinateVectorsBasis（def 须 lowerCamelCase）。
• 你内联了 tangent_coordinates_change（源自尚未移植的 Remark_3_15_extra_4）。已在 WORKLIST 记一笔，避免将来重复移植；保持内联即可，等那条正式移植时再抽出。

[LehengChen]

已更新:house style 修订 + 去教材编号;并把 def 改为 camelCase(chartCoordinateVectorsBasis)。陈述/证明未改,七门全绿。stacked 于 #69。