CL
CL recursively builds the columnwise limit function g(m) for a bounded double-indexed sequence f in a proper metric space. Analysts formalizing diagonal arguments or Recognition Science researchers handling Fourier subsequences cite this construction. The definition proceeds by recursion on m, selecting at each step the limit point furnished by bounded_subseq_tendsto applied to the subsequence already extracted by CE for prior columns.
claimLet $f : ℕ → ℕ → X$ satisfy dist$(f(n,m),c) ≤ R$ for all $n,m$ in a proper metric space $X$. Define $CL : ℕ → X$ by recursion: $CL(0)$ is the limit point of a convergent subsequence of the zeroth column, and $CL(m+1)$ is the limit point of the $(m+1)$-th column extracted along the indices produced by the composed extraction $CE$ at step $m$.
background
The module proves Cantor diagonal extraction for bounded sequences in proper metric spaces. Its main theorem, nat_diagonal_extraction, asserts existence of a strictly increasing φ and a limit map g such that f(φ(n),m) tends to g(m) for every m. The auxiliary definition CE composes successive extractions so that the first m+1 columns converge simultaneously. The supporting theorem bounded_subseq_tendsto guarantees a convergent subsequence for any bounded sequence in a proper space by compactness of closed balls.
proof idea
CL is introduced by recursion on m. The base case m=0 selects the limit from the choose_spec of bounded_subseq_tendsto applied directly to column 0. The successor case applies bounded_subseq_tendsto to the sequence f(CE m n, m+1) and again selects the limit via choose_spec.
why it matters in Recognition Science
CL supplies the limit function g required by nat_diagonal_extraction, the central result of the module. It is invoked in D_converges to obtain convergence along the full diagonal extraction D, and in CE_conv_at and CE_conv_le to verify the columnwise limits. Within Recognition Science this extraction supports the Fourier analysis component of the Navier-Stokes development and feeds into downstream cosmological statements such as planckMeasurements.
scope and limits
- Does not construct explicit indices, only their existence via choice.
- Does not guarantee uniqueness of limits without further hypotheses on X.
- Does not apply to unbounded sequences or non-proper spaces.
- Does not yield computable values; remains noncomputable.
formal statement (Lean)
54private noncomputable def CL : ℕ → X
55 | 0 => (bounded_subseq_tendsto (fun n => f n 0) c R (fun n => hf n 0)).choose_spec.choose
56 | m + 1 =>
57 (bounded_subseq_tendsto (fun n => f (CE f c R hf m n) (m + 1)) c R
58 (fun n => hf (CE f c R hf m n) (m + 1))).choose_spec.choose
59
60/-- The "local" extraction at step m+1. -/