Gauss–Kuzmin with explicit geometric rate in Lean: Lipschitz contraction, no spectral theory

To formalize |λ{Tⁿx ≤ t} − log₂(1+t)| ≤ qⁿ·log(1+t) for the Gauss map, track gₙ = (density of Tⁿ₊λ)·(1+y). Then gₙ₊₁(y) = Σₖ wₖ(y) gₙ(1/(k+1+y)) with wₖ = (1+y)/((k+1+y)(k+2+y)), which telescopes to Σ wₖ = 1. Split Ug(x)−Ug(y) = Σ wₖ(x)(g(bₖx)−g(bₖy)) + Σ (wₖ(x)−wₖ(y))(g(bₖy)−g(0)). The second sum works because Σ(wₖ(x)−wₖ(y))·g(0) = 0. With wₖ(x)−wₖ(y) = (y−x)(1−k−k²+x+y+xy)/Π, crude per-k rational bounds give Lip(Ug) ≤ (311/320)·Lip(g). Treat k=0,1 by hand and bound the tail by a telescoping 11/20·(1/((k+2)(k+3)) − …). In Mathlib, tsum_of_norm_bounded (HasSum of the majorant ⇒ ‖Σ'‖ ≤ a) closes the contraction step in one line. ∫₀¹ gₙ/(1+y) = 1 forces gₙ to cross 1/log 2; argue by contradiction with intervalIntegral.intervalIntegral_pos_of_pos_on, which avoids the IVT. Polynomial side goals: rw [div_le_iff₀]; field_simp; ring_nf; nlinarith [pow_nonneg hk i …] worked, but div_le_div_iff₀ after field_simp often fails to match.