The Schwartz cospan lemma (finiteness-and-chi, Banach half)

Unit: finiteness-and-chi (docs/design/finiteness-and-chi.md §0 (D-b), §4.3, §6.1–6.2).

Pure Banach-space material, zero project dependencies (D6: no manifold variables at all). This file is the make-or-break analytic core of the unit: it replaces Forster's §14.3/14.5/14.7 (finite-codimensional ε-contraction subspaces, iterated with Hilbert-space orthogonal complements) by one abstract statement, the classical L. Schwartz perturbation lemma specialized to the cospan form we need:

• schwartz_finite_cospan: if u v : E →L[ℂ] F are continuous linear maps between Banach spaces, u surjective and v compact, then there is a finite-dimensional S ≤ F with F = range (u - v) + S (span form — we never need closedness of range (u - v), only dimensions of quotients of it, so the harder half of Schwartz's theorem is not proved here).
• finiteDimensional_of_cospan: the consumer form used by Chain.lean/TradeBounded.lean: any P linearly hit by F and killed on range (u - v) is finite-dimensional.
• FiniteDimensional.of_linearMap_ker_range: the "extension" helper (finite kernel + finite codomain ⇒ finite domain) reused by both all-D finiteness steps and the χ ledger.

The proof of schwartz_finite_cospan mirrors mathlib's own proof of ContinuousLinearMap.exists_preimage_norm_le (Analysis/Normed/Operator/Banach.lean) in texture: Function.iterate, Summable.of_norm, summable_geometric_of_lt_one, telescoping, tendsto_nhds_unique — with an extra finite-dimensional "escape" term s ∈ S carried in parallel with the approximate-preimage term e, since we only get a compact (not surjective) perturbation v to correct for. Forster's open-mapping step 14.6(b) survives as the first line (u.exists_preimage_norm_le hu); Montel-compactness of v enters only via IsCompactOperator.isCompact_closure_image_closedBall (the forward form — the iff-lemma isCompactOperator_iff_isCompact_closure_image_closedBall hits a deterministic isDefEq timeout at E →L[ℂ] F, per the spike scratch_finiteness.lean §11).

theorem RS.schwartz_finite_cospan {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] (u v : E →L[ℂ] F) (hu : Function.Surjective ⇑u) (hv : IsCompactOperator ⇑v) : ∃ (S : Submodule ℂ F), FiniteDimensional ℂ ↥S ∧ ∀ (f : F), ∃ (e : E), f - (u e - v e) ∈ S

Schwartz's perturbation lemma, cospan/span form: a compact perturbation v of a surjective continuous linear map u between Banach spaces has finite-codimensional range — every f : F is u e - v e up to a finite-dimensional correction S, independent of f.

theorem RS.finiteDimensional_of_cospan {E : Type u_3} {F : Type u_4} {P : Type u_5} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] [AddCommGroup P] [Module ℂ P] (u v : E →L[ℂ] F) (hu : Function.Surjective ⇑u) (hv : IsCompactOperator ⇑v) (χ : F →ₗ[ℂ] P) (hker : ∀ (e : E), χ (u e - v e) = 0) (hχ : Function.Surjective ⇑χ) : FiniteDimensional ℂ P

Consumer form: any linear target P that is (a) killed by u − v and (b) hit by all of F, is finite-dimensional — the direct Schwartz-consumer shape needed for H1Cover.

theorem RS.FiniteDimensional.of_linearMap_ker_range {M : Type u_3} {N : Type u_4} [AddCommGroup M] [Module ℂ M] [AddCommGroup N] [Module ℂ N] (f : M →ₗ[ℂ] N) [FiniteDimensional ℂ ↥f.ker] [FiniteDimensional ℂ N] : FiniteDimensional ℂ M

The extension helper: a linear map with finite-dimensional kernel and finite-dimensional codomain has finite-dimensional domain (used by both all-D finiteness steps and the χ ledger's finiteDimensional_linSys).