CE_zero
plain-language theorem explainer
The base case of the composed extraction CE shows that at step zero it reduces exactly to the subsequence extracted by bounded_subseq_tendsto applied to the initial column. Analysts using diagonal arguments for sequences in proper metric spaces cite this when building the full extraction inductively. The equality holds by direct reflexivity from the definition of CE.
Claim. Let $CE_0(f,c,R,hf)$ denote the composed extraction at step zero. Then $CE_0(f,c,R,hf)$ equals the strictly increasing subsequence chosen by the bounded subsequence theorem so that $f$ composed with it converges in the closed ball of radius $R$ around $c$.
background
The module develops Cantor diagonal extraction for bounded sequences in proper metric spaces, with all results proved without axioms or sorry. The key definition is CE, the composed extraction at step m that ensures the first m+1 columns converge. It is defined recursively: at zero it takes the choose from bounded_subseq_tendsto on column zero, and at successor it composes with the extraction on the next column using the previous subsequence.
proof idea
The proof is a one-line reflexivity that matches the definition of CE at zero directly to the chosen subsequence from bounded_subseq_tendsto applied to the zeroth column.
why it matters
This base case anchors the inductive construction of the full diagonal extraction used in the main theorem nat_diagonal_extraction for subsequential limits in Fourier space. It fills the zero step in the chain of composed extractions that build the Cantor diagonal argument.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.