port(curve-velocity-mfderiv): 曲线速度 + mfderiv 设施

[LehengChen]

port(curve-velocity-mfderiv): 曲线速度 + mfderiv 函子性设施

Port of Lee, Introduction to Smooth Manifolds, §3: the velocity of a
parametrized curve (global and within-set) and basic functoriality of the
manifold differential mfderiv — the chain rule, the differential of a
diffeomorphism / its inverse, and invertibility of the differential of an
open-subset inclusion. Independent sub-chain root for tangent-bundle
localization.

Source → landing

Three source files split across two new modules under
OpenGALib/Manifold/Tangent/:

Source (import/smooth-manifolds-lee @ a5f308c)	Landing	Contributes
Chap03/Sec03_17/Definition_3_17_extra_1.lean	CurveVelocity.lean	unitTangentVector (private helper), curve_velocity, curve_velocityWithin, curve_velocityWithin_eq_curve_velocity
Chap03/Sec03_14/Proposition_3_6.lean	MFDeriv.lean	mfderiv_comp_of_smooth, diffeomorph_mfderiv_symm_eq_symm
Chap03/Sec03_14/Proposition_3_9.lean	MFDeriv.lean	mfderiv_open_subset_inclusion_isInvertible

Core objects (new)

• Manifold.curve_velocity I γ t — velocity γ'(t) ∈ T_{γ t} M of a curve
  γ : ℝ → M at parameter t, = mfderiv 𝓘(ℝ) I γ t applied to the unit
  tangent vector d/dt.
• Manifold.curve_velocityWithin I γ s t — within-set (one-sided) velocity
  relative to a domain subset s ⊆ ℝ, using mfderivWithin (for boundary
  arguments).

Supporting results: curve_velocityWithin_eq_curve_velocity (within-set and
ordinary velocity agree at a differentiability point of a uniquely
differentiable parameter set); mfderiv_comp_of_smooth (chain rule for smooth
maps); diffeomorph_mfderiv_symm_eq_symm (inverse of dΦ is d(Φ⁻¹) for a
C^n diffeomorphism, n ≠ 0); mfderiv_open_subset_inclusion_isInvertible
(differential of Subtype.val : U → M for an open U is invertible).

设计中立声明 (design-neutral)

• No second packaging class introduced. Everything is stated directly on
  Mathlib's tangent-bundle / differential API: mfderiv / mfderivWithin,
  TangentSpace, ModelWithCorners (incl. 𝓘(ℝ)), ContMDiff,
  MDifferentiableAt, Diffeomorph (M ≃ₘ^n⟮I, I'⟯ N), PartialDiffeomorph,
  IsLocalDiffeomorphAt, ContinuousLinearMap.IsInvertible. No OpenGA
  SmoothManifold packaging and no Lee TopologicalManifold are touched.
• No restate transform in this ticket (transforms: []); none applied.
• Proofs are unchanged from source modulo namespace placement and an added
  omit (see Deviations).

Deviations / namespacing

• Namespace. Source declarations were bare top-level (inside source
  sections, no enclosing namespace). Per the namespace policy all were moved
  under namespace Manifold (namespace_root) with their names preserved:
  curve_velocity, curve_velocityWithin, curve_velocityWithin_eq_curve_velocity,
  mfderiv_comp_of_smooth, diffeomorph_mfderiv_symm_eq_symm,
  mfderiv_open_subset_inclusion_isInvertible. No declaration renamed to dodge
  the gate. The curve_velocity / curve_velocityWithin names are kept verbatim
  to match the ticket core_objects (they use _ only as a math-name connector,
  not snake_case identifiers).
• "Two mfderiv lemmas" → three theorems. The ticket note phrases the
  MFDeriv.lean content as "the two mfderiv lemmas", but lists three source
  files. Definition_3_17_extra_1 supplies the curve-velocity content
  (→ CurveVelocity.lean); the remaining two source files
  (Proposition_3_6, Proposition_3_9) together contain three real
  theorems. To avoid dropping a listed source file, all three landed in
  MFDeriv.lean (Prop 3.6 contributes two; Prop 3.9 one). Flagging the count
  mismatch for review.
• #check-only items not ported. Proposition_3_6.lean also contained three
  #check stubs (mfderiv typed as a CLM, mfderiv_id,
  Diffeomorph.mfderivToContinuousLinearEquiv[_coe]). These are not
  declarations and exist verbatim in Mathlib; not carried over.
• omit added. mfderiv_comp_of_smooth does not use the [IsManifold …]
  section instances; an omit [IsManifold I ∞ M] [IsManifold I' ∞ N] [IsManifold I'' ∞ P] in was added to silence the unusedSectionVars linter
  (in the source these instances were "used" only via sibling #checks in the
  same section). No effect on the statement.
• Overlap with existing OpenGA code. None. Grep over OpenGALib/ shows no
  pre-existing curve_velocity* or these three mfderiv theorem names.
• Mathlib API. No renames or inlined dependencies. All referenced lemmas
  exist verbatim on the current toolchain: mfderiv_comp,
  mfderivWithin_eq_mfderiv, Diffeomorph.isLocalDiffeomorph,
  IsLocalDiffeomorphAt.localInverse[_*],
  IsLocalDiffeomorphAt.mfderivToContinuousLinearEquiv[_coe],
  Diffeomorph.mfderivToContinuousLinearEquiv,
  TopologicalSpace.Opens.openPartialHomeomorphSubtypeCoe,
  ChartedSpace.liftPropWithinAt_subtypeVal_comp_iff, contMDiff_subtype_val,
  ContinuousLinearMap.isInvertible_equiv.
• Imports. Dropped the source import Mathlib (Proposition_3_9) and the
  per-item Mathlib.* imports in favor of targeted imports; no
  SmoothManifoldsLee.* imports were present.

出处 (provenance)

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

• Chap03/Sec03_17/Definition_3_17_extra_1.lean
• Chap03/Sec03_14/Proposition_3_6.lean
• Chap03/Sec03_14/Proposition_3_9.lean

Per-module provenance lines are embedded in each landing file's module docstring.

Index wiring

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

Branch

port/curve-velocity-mfderiv, cut from the stacked batch tip
port/exhaustion-cutoff (not origin/develop). Files:

• new: OpenGALib/Manifold/Tangent/CurveVelocity.lean
• new: OpenGALib/Manifold/Tangent/MFDeriv.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/ticket05-20260614T044252Z.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.curve_velocity ≙ γ'(t) = dγ_t(d/dt); curve_velocityWithin its
  within-set variant;
• mfderiv_comp_of_smooth ≙ chain rule d(G∘F)_p = dG_{F p} ∘ dF_p;
• diffeomorph_mfderiv_symm_eq_symm ≙ d(Φ⁻¹)_{Φ p} = (dΦ_p)⁻¹;
• mfderiv_open_subset_inclusion_isInvertible ≙ the inclusion of an open
  submanifold has invertible differential at each point.

[Xinze-Li-Moqian]

感谢 #69（曲线速度 + mfderiv）。现在 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 额外一项：curve_velocity、curve_velocityWithin 是 snake_case，按 NAMING_CONVENTION.md 第 42 行 def 须 lowerCamelCase → curveVelocity、curveVelocityWithin。