Registry · Theorem III.T74 established formalized

III.T74 — HL Constant Convergence

Hardy-Littlewood C₂(k) decreasing for k=2..5. Each factor p(p-2)/(p-1)² < 1.

Book III Part 10 Ch. 81

Dependency Graph

Depends on (1)

III.D106

Lean Formalization

Module: TauLib.BookIII.Spectral.TwinPrimeDeep

Symbol: hl_constant_decreasing_5