D_converges
plain-language theorem explainer
The declaration proves pointwise convergence of the diagonal subsequence f(D(n), m) to the column limit CL(m) for each fixed m. Researchers assembling subsequence limits for bounded sequences in proper metric spaces cite this when completing the Cantor diagonal construction. The argument reduces the claim to CE_conv_at by index comparison via max and the factorization supplied by CE_factor.
Claim. For every natural number $m$, the sequence $n o f(D(n), m)$ converges to $CL(m)$ as $n o op$ in the metric, where $D(n) := CE(n,n)$ is the diagonal extraction and $CL(m)$ is the recursively defined column-wise limit obtained after stabilizing prior columns.
background
The module constructs Cantor diagonal extraction for bounded sequences $f : o o X$ in a proper metric space. D is the diagonal map $n o CE(n,n)$, where CE is the composed extraction that forces convergence of the first $m$ columns. CL is the limit function whose value at column $m$ is extracted from the stabilized subsequence after the first $m$ steps.
CE_conv_at states that $f(CE(m,n), m)$ converges to $CL(m)$ for each fixed $m$. The local setting is Fourier-space subsequential extraction for the Navier-Stokes problem, with all results proved inside the Recognition Science framework.
Upstream, CE_conv_at itself rests on the base case for column 0 and the inductive step LE_conv; K from Constants supplies the dimensionless bridge ratio used in related bounds.
proof idea
The term proof rewrites the Tendsto goal into the metric epsilon form. It obtains a threshold K from CE_conv_at at the given m and epsilon. It then chooses n at least max(m, K), decomposes n = m + p, invokes CE_factor to produce a later index rho(m+p) in the CE sequence, and transfers the distance bound from hK via le_trans on the indices.
why it matters
D_converges supplies the convergence component of nat_diagonal_extraction, the main theorem asserting existence of a strictly increasing phi and limit g such that f(phi(n), m) tends to g(m) for every m. It completes the fully proved diagonal extraction in the FourierExtraction module, closing one step in the Recognition Science derivation of Navier-Stokes behavior from the forcing chain (T0-T8) without additional axioms or sorrys.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.