harmonic_sum_diverges
plain-language theorem explainer
The partial sums of the harmonic series diverge to positive infinity. Researchers on annular cost bounds in Recognition Science cite this to establish that nonzero topological charge forces unbounded J-cost on expanding meshes. The proof sandwiches the sum below the logarithm via a standard inequality and lifts the known divergence of log via monotonicity at infinity.
Claim. The limit as $N$ tends to infinity of the sum from $n=0$ to $N-1$ of $1/(n+1)$ equals positive infinity.
background
The Annular J-Cost Framework defines phiCost u as cosh((log φ)·u) − 1, equivalently J(φ^u). AnnularSample collects phase increments on concentric rings, and Jensen-based coercivity shows nonzero winding forces Θ(m² log N) cost. The module certifies harmonic divergence as part of the annular topological floor and excess decomposition, with the remaining conditional part being concrete trace families for analytic carriers.
proof idea
The tactic proof first obtains tendsto of log((n:ℝ)+1) to infinity by composing the natural-number cast limit with the logarithm. It then establishes the pointwise lower bound log((N:ℝ)+1) ≤ harmonic sum up to N via the imported log_add_one_le_harmonic inequality, rewriting the range sum to a Fin sum. Finally it applies Filter.tendsto_atTop_mono to transfer the divergence.
why it matters
This result feeds the defect_cost_unbounded theorem, the key contradiction lemma showing that a zero of ζ with Re > 1/2 produces a defect whose annular cost is unbounded, violating cost-covering. It supplies the harmonic divergence step required for the annular topological floor in the RS framework, linking directly to the phi-ladder and the eight-tick octave. It touches the open construction of matching excess bounds for holomorphic carriers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.