D_strictMono
The diagonal map D(n) = CE(f, c, R, hf)(n, n) is strictly increasing on the naturals. Analysts constructing subsequence extractions for bounded sequences in proper metric spaces cite this to guarantee a strictly monotone index selector φ. The proof is a one-line wrapper that feeds the successor inequalities from D_succ_gt into strictMono_nat_of_lt_succ.
claimLet $D(n) := CE(f,c,R,hf)(n,n)$. Then $D$ is strictly monotone: $n < m$ implies $D(n) < D(m)$.
background
In the Fourier-Space Subsequential Extraction module the double sequence CE produces terms in a proper metric space X. The auxiliary definition D extracts the main diagonal by setting D(n) to CE(f,c,R,hf)(n,n). The upstream lemma D_succ_gt proves D(n) < D(n+1) by rewriting via CE_succ and invoking CE_strictMono on the second argument after the natural-number ordering lt_of_lt_of_le (Nat.lt_succ_of_le le_rfl).
proof idea
The proof is a one-line wrapper that applies strictMono_nat_of_lt_succ to the successor family supplied by D_succ_gt.
why it matters in Recognition Science
D_strictMono supplies the StrictMono φ clause inside the main Cantor diagonal extraction theorem nat_diagonal_extraction. That theorem assembles a strictly increasing index map together with a pointwise limit function g, furnishing the subsequential limits required for Fourier-space analysis of the Navier-Stokes equations. The result is fully proved with no open scaffolding.
scope and limits
- Does not prove convergence of the diagonal sequence D itself.
- Does not extend beyond proper metric spaces.
- Does not supply growth bounds or explicit rates for D(n).
- Does not construct the limit function g.
formal statement (Lean)
136private theorem D_strictMono : StrictMono (D f c R hf) :=
proof body
Term-mode proof.
137 strictMono_nat_of_lt_succ (fun n => D_succ_gt f c R hf n)
138