CE_factor
plain-language theorem explainer
The theorem shows that the composed extraction CE at depth m+p equals the depth-m extraction composed with a strictly increasing ρ that satisfies ρ(k) ≥ k for every k. Analysts working on diagonal subsequence extraction for Fourier coefficients in the Navier-Stokes setting would cite this to reduce multi-column convergence statements to single-column ones. The argument runs by induction on p, using the identity for the base case and composing with the LE operator plus CE_succ in the successor step.
Claim. Let $CE_m$ denote the composed extraction at depth $m$ that forces convergence of the first $m$ columns of the bounded sequence $f$. For natural numbers $m$ and $p$ there exists a strictly increasing map $ρ:ℕ→ℕ$ with $ρ(k)≥k$ for all $k$ such that $CE_{m+p}(k)=CE_m(ρ(k))$ for every $k$.
background
The module implements Cantor diagonal extraction for bounded sequences in proper metric spaces, with the goal of producing a single subsequence along which every column of $f$ converges. The operator CE is defined recursively: CE 0 selects a subsequence making column 0 converge, while CE (m+1) composes the prior extraction with a fresh subsequence chosen to make column m+1 converge. This yields a map that simultaneously stabilizes the first m columns.
proof idea
Proof by induction on p. The base case p=0 takes ρ to be the identity, which is strictly monotone and satisfies the lower bound by reflexivity together with equality by definition. For the successor step, the inductive hypothesis supplies ρ for q; the new map is ρ composed with LE at level m+q. Strict monotonicity follows from composition of strict mono maps, the inequality ρ(k)≥k follows by transitivity using the lower bound property of LE, and the functional equality is obtained by rewriting the depth, applying CE_succ, and invoking the inductive hypothesis after simplification.
why it matters
The result is invoked by D_converges to pass from column-wise convergence of CE to convergence of the diagonal subsequence D at every fixed column. It supplies the inductive step that lets extraction depth increase while preserving earlier limits, which is required to complete the full diagonal argument in the module. Within the Recognition Science framework this step supports the passage from discrete recognition steps to continuum limits via the composition law and the arithmetic structure underlying the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.