D
plain-language theorem explainer
D defines the diagonal extraction map by evaluating the composed extraction CE at matching level n, yielding a single index sequence for simultaneous convergence of all columns in a bounded double sequence. Analysts working on subsequential limits for Navier-Stokes or Fourier-mode extractions would cite this auxiliary construction. The definition is a direct one-line application of the recursive CE builder.
Claim. Define $D : ℕ → ℕ$ by $D(n) := CE_n(n)$, where $CE_m$ is the composed extraction that forces convergence of the first $m$ columns of the bounded sequence $f$ under the given bound $c$ and radius $R$.
background
The module develops Cantor diagonal extraction for bounded sequences in proper metric spaces, with all results proved without axioms or sorry. CE is the composed extraction at step m: it makes columns 0..m converge by recursively selecting bounded subsequences, starting from the base case at column 0 and composing the chosen index maps at each successor step. The local setting is the Fourier-space extraction needed for Navier-Stokes analysis, where the main theorem guarantees a strictly increasing φ and a limit function g such that the extracted subsequence converges columnwise.
proof idea
This is a one-line wrapper that applies the composed extraction CE at level n to produce the diagonal index D(n).
why it matters
D supplies the diagonal map required to complete the simultaneous column convergence in the module's main extraction result. It directly supports the Recognition Science treatment of bounded sequences arising in Navier-Stokes Fourier modes, closing the construction that feeds the overall forcing chain and phi-ladder mass formulas. No open scaffolding remains in this definition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.