CE_strictMono
The composed extraction map at each finite stage m is strictly monotone. Researchers constructing diagonal subsequences for bounded double-indexed sequences in proper metric spaces cite this lemma inside the Cantor extraction argument. The proof is by induction on m, with the base case taken from the subsequence choice and the successor case obtained by rewriting via the successor lemma and composing with the next-layer strict monotonicity.
claimLet $f : ℕ → ℕ → X$ be a double sequence bounded by radius $R$ around center $c$ in a proper metric space. For each natural number $m$, the composed extraction map $φ_m : ℕ → ℕ$ (built by iteratively selecting convergent subsequences for the first $m+1$ columns) is strictly increasing.
background
The module develops a Cantor diagonal extraction for bounded sequences $f : ℕ → ℕ → X$ in proper metric spaces, with the goal of producing a single strictly increasing index map $φ$ along which every column converges. CE is the recursive construction that, at stage $m$, yields an extraction map making the first $m+1$ columns converge simultaneously. It is defined by choosing a convergent subsequence for column 0 at the base and, at each successor, composing the previous map with a fresh subsequence extraction for the next column along the prior indices.
proof idea
Proof by induction on $m$. The zero case extracts strict monotonicity directly from the choose_spec of bounded_subseq_tendsto applied to the first column. The successor case rewrites CE (m+1) via the CE_succ lemma as the composition of CE m with the next-layer map, then applies the inductive hypothesis composed with the strict monotonicity of that layer given by LE_strictMono.
why it matters in Recognition Science
This lemma is invoked in D_succ_gt to establish that the diagonal index sequence is strictly increasing. It therefore supports the main module result nat_diagonal_extraction, which asserts the existence of a strictly increasing $φ$ and a limit function $g$ such that $f(φ(n), m)$ converges for every column $m$. In the Recognition Science setting the construction supplies the strictly monotone index maps required for the forcing-chain steps that isolate J-uniqueness and the eight-tick octave structure.
scope and limits
- Does not establish convergence of the original double sequence, only along the extracted subsequence.
- Does not apply when the ambient space fails to be proper or the sequence is unbounded.
- Does not produce a unique extraction map; different choices of subsequences may yield different $φ_m$.
- Does not supply quantitative rates or moduli of convergence.
Lean usage
rw [CE_succ]; exact (CE_strictMono f c R hf k).comp (LE_strictMono f c R hf k)formal statement (Lean)
74private theorem CE_strictMono : ∀ m, StrictMono (CE f c R hf m) := by
proof body
Term-mode proof.
75 intro m; induction m with
76 | zero =>
77 exact (bounded_subseq_tendsto (fun n => f n 0) c R (fun n => hf n 0)).choose_spec.choose_spec.1
78 | succ k ih =>
79 rw [CE_succ]; exact ih.comp (LE_strictMono f c R hf k)
80