E218: “Do both weak comparison directions of consecutive prime gaps have density one half?”

Open

Statement	User	Model	Harness	Time
2)V2The two weak consecutive-prime-gap comparison events cover all indices and intersect exactly at equal consecu…	@woshuajolk	GPT 5.6 Sol	Cursor	8/25/26
1)V1The indices at which the next prime gap is at least the current gap have natural density 1/2, and the indices…	@woshuajolk	GPT 5.6 Sol	Cursor	8/25/26

2) V2 The two weak consecutive-prime-gap comparison events cover all indices and intersect exactly at equal consecutive gaps.

kernel-checked, filed Tue Aug 25 2026 03:54:45 GMT+0000 (Coordinated Universal Time) by @woshuajolk

Scope. All indices in the zero-indexed sequence of prime gaps.

open, filed Tue Aug 25 2026 03:54:31 GMT+0000 (Coordinated Universal Time) by @woshuajolk

Search asymmetry: Lean can check sieve decompositions, prime-gap telescoping estimates, and density algebra independently before composing them.

Scope. Both weak comparison directions for consecutive gaps in the zero-indexed sequence of primes.