port(exhaustion-cutoff): 穷竭函数 + 局部光滑谓词 + 单位分解⇒仿紧

[LehengChen]

port(exhaustion-cutoff): 穷竭函数 + 局部光滑谓词 + 单位分解 ⇒ 仿紧

Port of Lee, Introduction to Smooth Manifolds, §2 (Sec 2.11 / Sec 2.12):
exhaustion functions, the local-extension smoothness predicate, the existence of
a positive smooth exhaustion function on a manifold, and paracompactness from
subordinate partitions of unity. Underpins non-compact L²/Bochner/GMT work.

Source → landing

All four source files land in a single new module
OpenGALib/Manifold/Cutoff/Exhaustion.lean:

Source (import/smooth-manifolds-lee @ a5f308c)	Contributes
Chap02/Sec02_11/Definition_2_11_extra_2.lean	IsSmoothOn, isSmoothOn_iff_exists_local_extension
Chap02/Sec02_11/Definition_2_11_extra_3.lean	IsExhaustionFunction (class), .tendsto_atTop, .isProperMap, the two instances, Continuous.isExhaustionFunction
Chap02/Sec02_11/Proposition_2_28.lean	exists_positive_smooth_exhaustion_function
Chap02/Sec02_12/Problem_2_13.lean	paracompactSpace_of_hasSubordinatePartitionOfUnity

Core objects (new)

• Manifold.IsSmoothOn (f : A → N) I I' — a map on a subset of a smooth
  manifold is smooth iff every point of A has an open neighborhood on which f
  extends to a bundled smooth map C^∞⟮I, U; I', N⟯.
• Manifold.IsExhaustionFunction (f : M → ℝ) — Prop-valued class: f
  continuous with every closed sublevel set f ⁻¹' Iic c compact
  (@[mk_iff isExhaustionFunction_iff]).

Supporting results: tendsto_atTop (→ +∞ off compact sets), isProperMap
(+ two convenience instances), Continuous.isExhaustionFunction (compact-space
case), exists_positive_smooth_exhaustion_function (positive smooth exhaustion
on a Hausdorff σ-compact smooth manifold via a compact exhaustion + the
partition-of-unity gluing lemma), paracompactSpace_of_hasSubordinatePartitionOfUnity.

设计中立声明 (design-neutral)

• No second packaging class introduced. Everything is stated directly on Mathlib
  typeclasses: TopologicalSpace, T2Space, CompactSpace,
  SigmaCompactSpace, ChartedSpace, IsManifold, ModelWithCorners,
  FiniteDimensional. Smooth maps use Mathlib's ContMDiff* / C^∞⟮·,·;·,·⟯
  owner and PartitionOfUnity.
• No restate transform in this ticket (transforms: []); none applied.
• No bump function ported. The ticket deliberately excludes Proposition_2_25
  (bump) and the sorry-bearing Lemma_2_26 because OpenGA already has
  OpenGALib/Riemannian/Manifold/BumpFunction.lean. The four ported source
  files did not require bump — exists_positive_smooth_exhaustion_function
  uses CompactExhaustion + exists_contMDiffMap_forall_mem_convex_of_local_const,
  not a bump partition, so no duplication was needed.

Deviations / namespacing

• Namespace. Source declarations lived in non-whitelisted Mathlib namespaces
  (namespace Function for IsSmoothOn / IsExhaustionFunction; bare top-level
  for exists_positive_smooth_exhaustion_function and
  paracompactSpace_of_hasSubordinatePartitionOfUnity). Per the namespace
  policy, all declarations were moved under namespace Manifold with their
  names preserved. Two consequences, flagged for review:
  • IsSmoothOn / IsExhaustionFunction are now Manifold.IsSmoothOn /
    Manifold.IsExhaustionFunction, so the source's f.IsSmoothOn /
    f.IsExhaustionFunction dot-notation (on f : M → ℝ, a Function) no
    longer applies; uses were rewritten to prefix form IsSmoothOn f … /
    IsExhaustionFunction f. Projection dot-notation on a class hypothesis
    (hf.continuous, hf.tendsto_atTop, hf.isProperMap) is unaffected.
  • Continuous.isExhaustionFunction is now
    Manifold.Continuous.isExhaustionFunction (name kept verbatim), so it no
    longer provides hf.isExhaustionFunction dot-notation on a Continuous
    hypothesis. Kept the name rather than renaming to dodge the gate; flagging in
    case a reviewer prefers a Manifold-native name or whitelisting.
• Overlap with existing OpenGA code. None. IsSmoothOn,
  IsExhaustionFunction, and both existence theorems do not currently exist
  anywhere in OpenGALib/ (grep clean). No conflict with BumpFunction.lean.
• Mathlib API. No renames needed; all referenced lemmas
  (isProperMap_iff_tendsto_cocompact, atTop_le_cocompact,
  compl_mem_cocompact, CompactExhaustion.find family,
  exists_contMDiffMap_forall_mem_convex_of_local_const,
  contMDiffAt_subtype_iff, …) exist verbatim on toolchain
  leanprover/lean4:v4.30.0-rc2. No inlined dependencies.
• Imports. Dropped the source import Mathlib (Definition_2_11_extra_3) and
  the SmoothManifoldsLee.* import (Proposition_2_28) in favor of targeted
  Mathlib imports.

出处 (provenance)

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

• Chap02/Sec02_11/Definition_2_11_extra_2.lean
• Chap02/Sec02_11/Definition_2_11_extra_3.lean
• Chap02/Sec02_11/Proposition_2_28.lean
• Chap02/Sec02_12/Problem_2_13.lean

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

Index wiring

• OpenGALib/Manifold.lean — added import OpenGALib.Manifold.Cutoff.Exhaustion
  (alphabetical, after the Charts.* lines).
• OpenGALib.lean already imports OpenGALib.Manifold; no change needed.

Branch

port/exhaustion-cutoff, cut from the stacked batch tip
port/charted-space-core (not origin/develop). Files:

• new: OpenGALib/Manifold/Cutoff/Exhaustion.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/ticket04-20260614T043725Z.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 §2:

• Manifold.IsExhaustionFunction ≙ continuous with compact closed sublevel sets;
• Manifold.IsSmoothOn ≙ locally smoothly extendable on a subset;
• exists_positive_smooth_exhaustion_function ≙ positive smooth exhaustion
  function existence on a Hausdorff σ-compact smooth manifold;
• paracompactSpace_of_hasSubordinatePartitionOfUnity ≙ subordinate POU for all
  open covers ⇒ paracompact.

[Xinze-Li-Moqian]

感谢 #68（穷竭函数 + 局部光滑 + 单位分解⇒仿紧）。现在 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 经核对符合我们域命名空间惯例，保留即可。

[LehengChen]

已更新:house style 修订 + 去教材编号(同 #67)。陈述/证明未改,七门全绿。本 PR stacked 于 #67——#67 合入 develop 后本 PR 的 base 会自动改投 develop。