CL
plain-language theorem explainer
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.
Claim. Let $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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.