D_succ_gt
plain-language theorem explainer
The theorem shows that the diagonal index sequence D, obtained by evaluating the n-step composed extraction at position n, is strictly increasing. Analysts constructing subsequential limits for Fourier representations of fluid equations cite this to guarantee the index map grows without repetition. The term proof reduces the successor inequality via the composition rule for the extractor and invokes its strict monotonicity after verifying the argument step with the local extractor and the general bound for strictly monotone maps on naturals.
Claim. Let $D(n)$ be the $n$-th index produced by the $n$-step composed extraction on the double sequence $f$. Then $D(n) < D(n+1)$ for every natural number $n$.
background
The module constructs a Cantor diagonal extraction for a bounded double sequence $f : ℕ → ℕ → X$ in a proper metric space. The composed extractor CE(m) is built recursively so that the subsequence it selects makes the first m columns of $f$ converge; its successor form is CE(m+1) = CE(m) ∘ LE(m). The local extractor LE(m) selects the next subsequence for column m+1 from the indices already chosen by CE(m). The diagonal D is defined by D(n) := CE(n)(n). Upstream results establish that every CE(m) and every LE(m) is strictly monotone, while strictMono_id_le supplies the general fact that any strictly increasing map φ on naturals satisfies k ≤ φ(k).
proof idea
The term proof first rewrites the target inequality using the successor relation to obtain CE(n)(n) < CE(n)(LE(n)(n+1)). It then applies the strict monotonicity of CE(n) to the premise n < LE(n)(n+1). That premise is obtained by chaining the strict increase of LE(n) with the bound n ≤ LE(n)(n+1) supplied by strictMono_id_le applied to LE(n).
why it matters
The result is invoked directly to prove that the full diagonal map D is strictly monotone. This monotonicity is required by the module's main extraction theorem, which produces a single strictly increasing index sequence along which every column converges. In the Recognition Science setting the lemma supplies the index-growth step needed for the Fourier-space subsequence tool used in Navier-Stokes analysis, closing the link from boundedness to a well-defined diagonal extraction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.