The prime-gap dyadic series

What is checked in Lean

• The finite summation-by-parts identity relating the prime dyadic partial sums to the prime-gap dyadic partial sums, with an exact endpoint term and no convergence premise.
• The factor-of-two normalisation between the two displayed indexings, at every finite horizon.
• Conditional on summability of the prime dyadic series, the exact infinite prime-gap identity and the equivalence of irrationality of the prime and prime-gap series.
• For an abstract integer-digit dyadic tail recurrence: the exact block identity, and that a shift of fixed length is integral exactly when an explicit scaled state is.
• That one integral shift propagates to every later index.
• That repeated doubling removes the power-of-two denominator, so every rational-valued dyadic recurrence has one fixed positive shift integral at all sufficiently late indices.
• For a real-valued dyadic recurrence, cofinal non-integrality of every fixed positive shift implies irrationality of the initial state.
• That the actual consecutive-prime-gap sequence is unbounded, by the factorial prime-free-interval construction, and therefore is not eventually periodic with any positive period.
• For any integer-digit dyadic tail recurrence, two adjacent fixed-length shifts lying strictly between -1 and 1 cannot both be integral when the corresponding digits differ.
• For the actual prime gaps, a cofinal supply of adjacent small-shift pairs with a mismatching gap excludes eventual integrality of that fixed shift.
• The generic distance-to-integers core of the finite-truncation criterion: an approximation farther than its error bound from every integer certifies non-integrality.

Main results

Statements and boundaries are copied from the corpus record. Registry status: not_registered; the claim registry does not carry these declarations and kernel checking them does not promote them into reviewed public claims

What is not checked

• The target irrationality.
• The definition and recurrence of the concrete prime-gap tail as Lean infinite sums; the note supplies these at paper level. Summability of the concrete prime series is Lean-checked unconditionally via an elementary polynomial prime bound.
• A theorem supplying cofinally many adjacent actual-prime-gap tail shifts in the open unit interval with the required gap mismatch.
• Any theorem forcing periodicity or automaticity of the prime gaps from rationality; the free-carry identity disconfirms that route.

Open obligations

Prove any one of these and the corresponding reduction above becomes unconditional.

• prime_gap_cofinal_shift_escape For every fixed h >= 1 and every N0, find N >= N0 for which sum_{j>=1} (g_{N+h+j}-g_{N+j})/2^j is not an integer.
• cofinal_adjacent_small_mismatch For every fixed h >= 1 and every N0, find N >= N0 such that both adjacent full tail shifts have absolute value less than 1 and g_{N+h+1} != g_{N+1}. The checked local consumer then excludes eventual integrality of the h-shift.
• actual_prime_gap_tail_formal_bridge Formalise summability of the actual prime and prime-gap dyadic series and identify the concrete infinite prime-gap tail with the checked real/rational dyadic recurrence, so the local consumer reaches the target series without a paper-only analytic bridge.

Lean modules

Comparator review

The Comparator replays selected exact interfaces against a pinned toolchain. It never widens what Lean proved.

The paper