6. The finite-difference proof🔗

This is the argument formalized in Lean. The exact unconditional theorem is HardyZeta.hardy, in HardyZeta/Hardy.lean. Every analytic input below is proved for the actual mathlib zeta function.

1. 6.1. Required analytic input
2. 6.2. Finite algebra
3. 6.3. Limits only on bounded intervals
4. 6.4. Contradiction from an eventual sign
5. 6.5. Scope of the change