Registry · Proposition III.P46 established formalized

III.P46 — Twin Gap Characterization

Twin gap = density gap. Admissible classes nonempty (algebraic) but infinitude needs Bombieri-Vinogradov (analytic). exponential_quantification (K4).

Book III Part 10 Ch. 81

Dependency Graph

Depends on (2)

III.P45 III.D69

Depended on by (1)

III.D112

Lean Formalization

Module: TauLib.BookIII.Bridge.ConjectureGaps

Symbol: twin_gap_density