LE_strictMono
LE_strictMono asserts that the local extraction map LE at each fixed stage m is strictly increasing. Analysts building diagonal subsequences for double-indexed bounded sequences in proper metric spaces cite it to maintain monotonicity through the inductive construction of the composed extraction. The proof is a one-line wrapper that pulls the strict monotonicity witness directly from the choose_spec of bounded_subseq_tendsto applied to the shifted column sequence.
claimLet $f : ℕ → ℕ → X$ be bounded by radius $R$ around center $c$ in a proper metric space $X$. For each $m ∈ ℕ$, the map $LE(m) : ℕ → ℕ$ obtained by selecting a convergent subsequence for column $m+1$ after the indices of the composed extraction $CE(m)$ is strictly monotone.
background
The module constructs a Cantor diagonal extraction for a double sequence $f : ℕ → ℕ → X$ that remains bounded in a proper metric space. The composed extraction $CE(m)$ is built recursively so that the first $m+1$ columns converge simultaneously. The auxiliary map $LE(m)$ is the subsequence selector chosen specifically for column $m+1$ once the indices from $CE(m)$ are fixed; its definition invokes bounded_subseq_tendsto on the sequence $fun n => f (CE(m) n) (m+1)$ and retains the chosen index map.
proof idea
The proof is a one-line wrapper that extracts the first component of choose_spec.choose_spec from the application of bounded_subseq_tendsto to the column-$m+1$ sequence after $CE(m)$. No further tactics or reductions are required.
why it matters in Recognition Science
LE_strictMono supplies the inductive step for CE_strictMono, which in turn guarantees that the global extraction map remains strictly increasing at every stage. This monotonicity is required for the main nat_diagonal_extraction result to produce a single subsequence along which every column converges. The lemma therefore closes the deterministic, axiom-free construction of the diagonal argument used in the Fourier extraction layer.
scope and limits
- Does not establish convergence of any extracted subsequence.
- Does not apply to sequences that fail the uniform bound $dist(f n c) ≤ R$.
- Does not extend to metric spaces that are not proper.
- Does not supply an explicit closed-form expression for the extraction map.
formal statement (Lean)
70private theorem LE_strictMono (m : ℕ) : StrictMono (LE f c R hf m) :=
proof body
Term-mode proof.
71 (bounded_subseq_tendsto (fun n => f (CE f c R hf m n) (m + 1)) c R
72 (fun n => hf (CE f c R hf m n) (m + 1))).choose_spec.choose_spec.1
73