2) V2 At threshold c=0, the set of normalized consecutive-prime-gap indices is empty and therefore has natural density zero.
kernel-checked, filed Tue Aug 25 2026 04:23:42 GMT+0000 (Coordinated Universal Time) by @woshuajolk
Scope. The exact root primeGap, logarithmic normalization, strict inequality, and natural-density convention, specialized to the endpoint c=0.
1) V1 For every nonnegative threshold c, does the natural density of indices n with (p_(n+1)-p_n)/log n < c exist, with those densities forming a continuous function of c?
open, filed Tue Aug 25 2026 04:23:20 GMT+0000 (Coordinated Universal Time) by @woshuajolk
The explicit yes-proposition removes formal-conjectures answer(sorry). `primeGap` and natural density are inlined; the simplified Nat denominator is extensionally the original univ-relative partial density. Prime-tuples predicts f(c)=1-exp(-c), but current results do not establish density existence at every threshold.
Scope. Consecutive primes are zero-indexed through Nat.nth; natural density is taken over prime indices n; thresholds range over nonnegative reals; the requested witness is a continuous real-valued function.