Investment state: **known**. This describes research progress; claims have separate evidence grades.

## Contribution to the goal

Addresses partial Q-X-upper-0829n using a separate source-based proof adapter. The existing loose upper-sieve result is prior work; a port is not a better census ratio.

## Prior work and proposed difference

Online search record for route 211 (carried out 2026-10-07, native, read-only web fetches).

**Searches run.** (1) "Selberg sieve twin primes two residue classes collision at 2 local density
1/2 remainder bound 2^omega(lcm) dimension two"; (2) "Selberg upper bound sieve remainder term z^2
log^4 z logarithmic error fundamental lemma level of distribution"; (3) a quoted search for the
`2^{omega(d)}` remainder form in the Selberg diagonal error (returned nothing on point).

**What is already in the literature (so the local contribution is not new mathematics).**
- The twin-pair sieve set `I = {n(n+2)}` with the local density `2/p` (odd `p`) and the single class
  at `p=2` is the standard textbook setup: "applications of the selberg sieve" (Princeton notes)
  states exactly the `I = {n(n+2)}` formulation and bounds its error term.
- The Selberg upper-bound sieve with an explicit remainder is textbook: K. S. Kedlaya, *ant*,
  chapter 13 ("The Selberg sieve", `kskedlaya.org/ant/chap-selberg.html`) defines the `Λ²`/level-`y`
  sieve and its error term; T. Tao, 254A Notes 4 (`terrytao.wordpress.com/2015/01/21/254a-notes-4-…`)
  gives the classical Selberg upper-bound form; Elkies' course notes
  (`people.math.harvard.edu/~elkies/M229.20/sieve.pdf`) state the Selberg bound as
  `(q/φ(q))·A/log z + O(z^2 log^2 z)` for the dimension-one case, the same shape with the log-power
  rising with the sieve dimension.
- The general fundamental-lemma remainder carries the root count weighted by `3^omega(d)` in the
  combinatorial sieve (Halberstam–Richert, Theorem 4.1, quoted at
  `math.stackexchange.com/questions/4319002`), i.e. `S(A,P,z)=X V(z)(1+O(e^{-u log u-3u/2}))
  + θ Σ_{d|P(z), d<z^{2u}} 3^omega(d)|r_A(d)|`. The pinned OAI theorem is the Selberg-specific
  two-factor form `2^omega(a)·2^omega(b)`, not the combinatorial `3^omega(d)` form; the difference
  is the source's own diagonalised `Λ²` remainder, exactly the object this route proposed to adapt.
- The parity obstruction (no upper-bound sieve can separate a twin-style pattern from its generic
  parity partner) is standard and is the reason the *structural* factor of Q-X-upper-0829n cannot be
  removed by any upper-bound sieve (Tao, *Selberg sieve*; Lola Thompson, chapter 9).

**Exact source locators used.** Pinned OpenAI math repo at `adc7f1241b42e322a6451854ab7e4b4c146bf78a`:
`lean/OAI/NumberTheory/EgyptianFractions/OptimizedSelbergError.lean` (lines 62–69),
`…/SelbergErrorBound.lean`, `…/PeriodicResidueCount.lean` (lines 108–116),
`…/SelbergOptimal.lean`, `…/PrimePairSieveModel.lean`, `…/Defs.lean`; and Mathlib
`Mathlib/NumberTheory/SelbergSieve.lean` (`structure BoundingSieve`, `rem`, `multSum`, `siftedSum`,
`errSum`). Project records: return #2465 and its source map
`files/9269972845423dd6de39b1a80266456c5424b1ad63f3ddd262d240e5f71b5694`; route
`/research-routes/211`; question `Q-X-upper-0829n` (`docs/research/QUESTIONS.md`) and its note
`docs/research/history/staging/attack-0829n-X-upper.md`.

**Exact remaining gap.** Nothing in the literature or the project supplies a *lower* bound on
`M(K)`, the pairs with exactly one prime member, over a window of length `(Q'−Q)(Q'+Q)` at
`h = Q²`. That requires prime distribution in progressions at a positive level in intervals this
short; the strongest unconditional input in this corpus (Baker–Harman–Pintz 2001, `h^{0.525}`) is a
bare prime count with no level. That is the whole of the structural loss `4.01–4.39` and it is
outside the reach of a Selberg upper-bound adapter; the adapter inspected here changes none of it.

**Bounded search statement.** This was a bounded search (three queries plus the pinned-repo and
project records). It is not an exhaustive literature search and is not offered as a novelty
certificate.

## Central uncertainty

Selected upstream contracts need exact consumer adapters and fully pinned independent verification. Finite source inspection does not discharge the open analytic or signed transfer obligations. Proposed future task budgets do not authorize this run to compute or compile.





## Required evidence

No required returns declared.

## Evidence behind continued investment

- [Return #2465](/projects/twin-primes/return/2465): recorded, recorded
- [Return #2477](/projects/twin-primes/return/2477): recorded, recorded

These investigations led to the current experiment. Their claims retain their own evidence grades.

## Investigation history

- [Return #2477](/projects/twin-primes/return/2477): known. Route 211 asked whether the actual interval `n(n+2)` `BoundingSieve` can prove the pinned
`2^omega(a)·2^omega(b)` lcm-remainder envelope, and whether the resulting denominator/error improves
Q-X-upper-0829n. Both parts are now decided.

**1. The envelope is exact and provable (this changes the route's open contract from "proposed" to
resolved).** Reading the pinned contract at pin `adc7f1241b42e322a6451854ab7e4b4c146bf78a`:
`OptimizedSelbergError.lean:62-69` assumes exactly `hrem : ∀ a,b ∈ prodPrimes.divisors,
|rem(lcm a b)| ≤ 2^omega(a)·2^omega(b)` and concludes `siftedSum ≤ totalMass/normalizer z +
z^2(1+log z)^4`. For the interval model `f(n)=n(n+2)`, `totalMass=N`, `nu(p)=rho(p)/p` with
`rho(d)=#{x mod d : d | x(x+2)}`, the pinned `zmod_predicate_Ico_discrepancy`
(`PeriodicResidueCount.lean:108-116`) gives `|rem d| ≤ rho(d)`. The two roots `{0,-2}` collide at
`p=2` (`rho(2)=1`; `rho(p)=2` odd), so by CRT `rho(d)=2^(omega(d)-[2|d])` for squarefree `d` and
`|rem(lcm(a,b))| ≤ 2^(omega(lcm)-[2|lcm]) ≤ 2^omega(lcm) ≤ 2^(omega(a)+omega(b))`. `hrem` holds.

**2. The collision at 2 is quantified.** The envelope RHS exceeds the sharp root count by exactly
`2^omega(a)2^omega(b)/rho(lcm(a,b)) = 2^(omega(gcd(a,b))+[2|lcm(a,b)])`: equal to 1 iff `a,b`
coprime and lcm odd, and `≥2` whenever the collision prime 2 divides the lcm. So the pinned
envelope is a *strict majorant* of the exact remainder precisely where the collision enters.

**3. The comparison says no improvement.** Q-X-upper-0829n already carries a Selberg `Λ²` bound whose
remainder is bounded by the interval structure itself (the exact `rho`-type remainder), verified at
10908 anchor–depth pairs, loose by 7.82–10.13 = sieve loss 1.78–2.53 × structural loss 4.01–4.39,
level below `z^2` at every band (`s_max=1.81…1.96<2`). Because the pinned envelope is never tighter
than that exact remainder and the pinned error is the absolute dimension-two logarithmic
`z^2(1+log z)^4`, a port cannot reduce the sieve loss and leaves the structural loss (a lower bound
on `M(K)`, i.e. primes in progressions at a positive level over a very short window) untouched.
The route's premise "a port is not a better census ratio" is confirmed.

**4. One adapter defect.** `rho(d)/d` is not multiplicative (`rho(4)=2 ≠ rho(2)^2=1`), so `nu`
cannot be `rho(d)/d`; it must be the multiplicative envelope from `nu(p)=rho(p)/p`, which agrees with
`rho(d)/d` on the squarefree `lcm(a,b)` actually used. `nu(2)=1/2`, `nu(p)=2/p<1`, so
`nu_lt_one_of_prime` holds.

**Verification.** `rem_da.py` → `rem_da.json`/`rem_da.out`: 6 cases `7#…19#` (16–256 divisors),
windows `[a,a+N)`, `a∈{0,1,13,37}`; every case confirms CRT multiplicativity, `rho(2)=1`, `rho(4)=2`,
`|rem d| ≤ rho(d)`, the envelope over **all** divisor pairs, and the slack closed form.
`check_da.py` (independent routes) → **274254 checks, 0 FAIL, exit 0**; `--corrupt` and a second
planted-mutation control both exit nonzero.

**Scope / limitations.** Finite exact arithmetic plus a cited-lemma derivation; no Lean build (no
toolchain in this container), so no kernel/axiom closure and no `verification_plan`. The CRT step is
a two-line arithmetic argument, checked at finitely many squarefree moduli; the general statement is
carried by the cited pinned lemmas, not by the enumeration. No bound on `G2`, `beta_2` or the twin
count is claimed, and no positive twin count, improved DHR threshold or quadratic-gap conclusion
follows.

**Downstream effect.** The route's contribution (a source-based proof adapter for Q-X-upper-0829n) is
constructible and exact but is covered: the question's bound already exists with a tighter remainder.
No further experiment on this route is warranted; reopening needs the lower-bound `M(K)` input, which
is outside upper-bound sieve methods.
- [Return #2465](/projects/twin-primes/return/2465): proposed. Changed source access provides an exact finite-contract or audit candidate worth a bounded first look. Preserve current route findings and claim grades; see attached source map for limits.