Indeed, every \(n\in(X+H_X,2X]\) is counted for exactly \(H_X\) values of

\(t\), so

Insert the global asymptotic and use \(H_X=o(X)\). In particular, every

large dyadic block contains at least one good starting point. Since

\(H_X\le C\sqrt t(\log t)^2\) for \(t\in[X,2X]\), this produces arbitrarily

large good \(t\) at the live-page scale.

This argument supplies no information about a sparse set of bad \(t\), which

is exactly the quantifier in the question.

3. Exact semiprime reduction

Let \(S_2(x;H)\) be the contribution from semiprimes alone. Unique

factorisation gives the exact identity

Here \(q\) is the larger prime factor. This is (a).

Restrict further to \(p\le q\le2p\), and call the resulting sum \(B(x;H)\).

Then

Every term in (2) is a term of the composite-only sum, so

This isolates a clean sufficient lemma:

> Uniform balanced-pair lemma needed. Find fixed \(C,\kappa>0\) such

> that, for every sufficiently large \(x\),

> \[ > \#\{(p,q)\in\mathbb P^2:p\le q\le2p,\ > x\le pq\le x+C\sqrt x(\log x)^2\}\ge\kappa\sqrt x. \tag{4} > \]

For large \(x\), all \(q\) in (4) are at most \(2\sqrt x\). Thus (4) would

give \(B(x;H)\ge\kappa/2\), proving even the composite-only version.

For \(q\asymp\sqrt x\), each inner prime interval in (1) or (2) has length

A lane-by-lane prime number theorem would therefore demand uniform prime

control in polylogarithmic intervals, far beyond known all-\(y\) results.

Such lane-by-lane control is stronger than necessary: (4) only asks for an

aggregate Type-II lower bound across the hyperbolic strip. But no checked

source supplies that aggregate lower bound either.

For comparison, applying the Guth–Maynard all-\(y\) exponent

\(\theta>17/30\) at factor scale \(y=\sqrt x\) naturally produces product

intervals of size

polynomially longer than \(x^{1/2}\log^2x\).

A prime-number-theorem heuristic, not a proof, predicts

This follows by replacing each prime measure by \(dt/\log t\) in (2).

The full semiprime heuristic similarly predicts \(4C\). Both statements are

(c) only.

4. Exhaustive finite theorem

4.1 A wholly integer inner window

For integer \(m\ge3\), set

and

The exact positive-term expansion

certifies the decimal inequality; the last cross-product differs by \(5\):

\(842000-693\cdot1215=5\).

Since \(m-1\ge2^{k_m}\), (6) gives

Now take any real \(x\) and \(m=\lceil x\rceil\).

• If \(x\notin\mathbb Z\), then \(x>m-1\), and monotonicity of

\(u+\sqrt u\log^2u\), together with (7), gives

\[ m+h_-(m)

• If \(x=m\), the same containment is immediate from (7).

Therefore

This proves that checking the integer window (6) for every integer \(m\) also

checks every real \(x\). This part is (a).

4.2 Exact lower weights and the event scan

Generate every event

that can occur in the windows. Its genuine contribution is \(1/q\). The

checker instead adds

All comparisons and running sums use the integer numerator

\(\lfloor10^{12}/q\rfloor\).

Let

Both \(h_-(m)\) and \(m+h_-(m)\) are nondecreasing. If \(m\) is not an

event product, moving from \(m\) to \(m+1\) removes no event and may only add

events on the right. Hence a new minimum can occur only

1. at the first integer of a reported block, or

2. at \(m=n+1\) immediately after an event \(n=pq\) leaves.

The program scans exactly these candidates with two monotone pointers.

This is the reason 3.56 million candidates certify roughly one billion

integer starts.

Completeness of prime generation is also elementary: if

\(p\le q\le2p\) and \(pq\le N\), then \(p\le\sqrt N\) and

\(q^2\le2pq\le2N\). A sieve through \(\lfloor\sqrt{2N}\rfloor+2\) therefore

contains every possible factor.

4.3 Certified table

The table blocks are blocks of the integer \(m=\lceil x\rceil\).

“Minimum” is the exact minimum of the fixed-point lower sum (9), not a

floating estimate.

| integer \(m\) block | certified minimum | attaining \(m\) | \(h_-(m)\) | balanced terms |

|---:|---:|---:|---:|---:|

| \(10^6\)–\(9{,}999{,}999\) | 0.961228141898 | 1,021,338 | 174,729 | 1,189 |

| \(10^7\)–\(99{,}999{,}999\) | 1.022100901595 | 16,113,170 | 1,019,555 | 4,913 |

| \(10^8\)–\(10^9\) | 1.066514980610 | 516,150,462 | 8,541,967 | 28,703 |

The global fixed-point minimum is

By (8), (9), and (3), this proves the boxed finite theorem for every real

\(x\in[10^6,10^9]\). The finite conclusion is (d), backed by the

elementary proof of what the computation certifies.

4.4 Reproduction and independent checks

Run:

python runs/erdos462_wave5x_reverify.py

Observed output on this VM:

exact log(2) certificate: 842/1215 > 693/1000
least-factor vs prime-pair identity cross-check: PASS
small candidate-scan vs every-x cross-check: PASS
parameters: real_x=[1000000,1000000000] terminal=1012743665 q_limit=45007 primes=4676 events=3602274 candidates=3561287 scale=1000000000000
block=[1000000,9999999] scaled_min=961228141898 lower=0.961228141898 at_m=1021338 h_minus=174729 right=1196067 terms=1189 direct_sum≈0.961228142459 direct_recount=PASS
block=[10000000,99999999] scaled_min=1022100901595 lower=1.022100901595 at_m=16113170 h_minus=1019555 right=17132725 terms=4913 direct_sum≈1.022100903973 direct_recount=PASS
block=[100000000,1000000000] scaled_min=1066514980610 lower=1.066514980610 at_m=516150462 h_minus=8541967 right=524692429 terms=28703 direct_sum≈1.066514994833 direct_recount=PASS
CERTIFIED: for every real x in [10^6,10^9], the balanced-semiprime contribution in the live-page window is > 0.961

Measured cost was 10.87 seconds wall time and 160,864 KiB peak resident memory.

The script contains four independent safeguards:

1. an exact rational certificate for \(0.693<\log2\);

2. a complete least-prime-factor factorisation check against prime-pair

generation through \(10^5\);

3. a candidate-only scan compared with an every-integer prefix scan on

\(1000\le m\le50000\);

4. a fresh factor-pair enumeration at each of the three reported minima,

independent of the event array and two-pointer scan.

The displayed direct_sum≈ values are diagnostics only. Certification uses

the smaller exact integer scaled_min values.

5. Exact wall

The finite computation rules out small or moderately large counterexamples

for \(C=1\), even for the stronger composite-only sum, but it cannot settle an

eventual statement. No finite extension changes that quantifier.

The precise missing analytic input is (4), or an alternative lower bound of

comparable strength for the rough-number integral/full weighted sum. Existing

tools checked here fall short for distinct reasons:

• global RSA-integer asymptotics have errors much larger than the

\(\asymp\sqrt x\) target increment;

• all-\(y\) prime-number theorems reach polynomial, not polylogarithmic,

factor intervals;

• almost-all results do not exclude a sparse sequence of bad \(x\);
• existence of one \(E_2\)-number is inadequate, because a balanced one has

weight only \(\asymp x^{-1/2}\), while the desired sum needs

\(\gg\sqrt x\) such weighted events in aggregate.

Thus the honest endpoint is a verified finite theorem, an exact balanced

bilinear reduction, and a named uniform Type-II lower-bound barrier—not a

solution of the asymptotic problem.

PARTIAL: The stronger composite-only inequality with C=1 is certified (>0.961) for every real x in [10^6,10^9], and the remaining all-x asymptotic step is the stated uniform balanced-semiprime Type-II lower bound.