Montel compactness of restrictCLM (finiteness-and-chi)

Unit: finiteness-and-chi (docs/design/finiteness-and-chi.md §4.4, proof plan §6.3).

• isCompactOperator_restrictCLM: for S' ⋐ S inside a single chart source, the restriction restrictCLM : BddHoloOn S →L[ℂ] BddHoloOn S' is a compact operator (Montel's theorem, quoted from Jacobian/Forms/Montel.lean).

Placement note (deviation from the design doc's §3 file plan, flagged honestly): the design's §4.4 header also lists the cocycle-level assembly (isCompactOperator_resZ_UV, isCompactOperator_tradeCompact), but those need ShrinkChain/NZ1/tradeCompact, which are defined in Chain.lean — built after this file per the same file plan's build order. To keep this file gate-free and self-contained (no forward reference to a not-yet-written file), the single-chart lemma lives here; the cocycle-level assembly is proved in Chain.lean immediately after the relevant definitions, by IsCompactOperator.comp_clm/.clm_comp composed with this lemma (per §6.3 step 5) — no mathematical content moves, only the file boundary.

theorem RS.Finiteness.isCompactOperator_of_isCompactOperator_val {E : Type u_2} {N : Type u_3} [NormedAddCommGroup E] [NormedSpace ℂ E] [NormedAddCommGroup N] [NormedSpace ℂ N] {S : Submodule ℂ N} (hS : IsClosed ↑S) (f : E →L[ℂ] ↥S) (hf : IsCompactOperator fun (e : E) => ↑(f e)) : IsCompactOperator ⇑f

Compat: a CLM into a closed submodule is a compact operator as soon as its composite with the ambient inclusion is (the closedness lets a compact "witness set" for the ambient map be trimmed, via Subtype.isCompact_iff, to a compact witness set inside the submodule itself).

theorem RS.Finiteness.isCompactOperator_restrictCLM {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [CompactSpace X] {S' S : TopologicalSpace.Opens X} {x₀ : X} (hsrc : ↑S ⊆ (chartAt ℂ x₀).source) (hc : closure ↑S' ⊆ ↑S) : IsCompactOperator ⇑(restrictCLM ⋯)

Montel compactness of the restriction: for S' ⋐ S ⊆ source (chartAt ℂ x₀), the restriction BddHoloOn S → BddHoloOn S' is a compact operator.