strictMono_id_le
plain-language theorem explainer
Strictly increasing maps φ from naturals to naturals are bounded below by the identity. Analysts building diagonal subsequences for Fourier coefficients in Navier-Stokes cite the bound to guarantee that index shifts remain non-decreasing. The argument is a direct induction on n that invokes the zero lower bound at the base and applies the strict increase to the successor step.
Claim. If $φ:ℕ→ℕ$ is strictly increasing, then $n≤φ(n)$ for every natural number $n$.
background
The module constructs Cantor diagonal extraction for bounded sequences in proper metric spaces, producing a strictly increasing index map φ together with a pointwise limit g. This lemma supplies the lower bound n ≤ φ n that is required when the extraction operator CE is factored across multiple steps. Upstream, zero_le from the arithmetic foundation supplies the base inequality for natural numbers, while the successor operation encodes the inductive generator in the underlying Peano structure.
proof idea
The proof proceeds by induction on n. The zero case is discharged directly by the zero lower bound theorem. For the successor case the inductive hypothesis k ≤ φ k is combined with the strict increase applied to k < k+1, then the successor inequality is recovered by the transitivity lemma Nat.succ_le_of_lt.
why it matters
The result is invoked inside CE_factor to construct the strictly increasing ρ satisfying ρ(k) ≥ k when the extraction index is advanced by p steps; it likewise supports D_succ_gt which establishes that the diagonal sequence itself is strictly increasing. In the Recognition framework it closes the elementary arithmetic fact needed for subsequence extraction that underpins the Fourier-space treatment of the Navier-Stokes equations, consistent with the eight-tick octave and the dimensional reduction derived in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.