Main Theorem

theorem KrafftSieve.mu_min_lt_one_implies_tpc : {n : ℕ | muMin n < 1}.Infinite → {p : ℕ | Prime p ∧ Prime (p + 2)}.Infinite

Theorem: If there are infinitely many intervals where the optimal multidimensional weight achieves a ratio strictly less than 1, then there are infinitely many twin primes.