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

## Contribution to the goal

Addresses partial Q-corner-correlation/Q-prime-band-transfer using actual arithmetic finite tails; no signed transfer or shrinking twin margin is assumed.

## Prior work and proposed difference

Online prior-art search for route 212 (native, read-only web search, 2026-10-07). This updates the
record; the route's contribution is a *port/audit* of existing finite facts, not novelty.

**Searches run.** (1) "Rankin's trick smooth numbers bound inverse totient exp(-Z/(4 log N)) Mertens
product"; (2) "smooth numbers reciprocal sum Dickman function sum 1/n y-smooth tail bound explicit";
(3) "bound number of integers n such that smooth part of n+1 exceeds K half power Euler product sieve".

**Closest sources.** 
- **Rankin's trick** is the exact mechanism of pinned contract (a): multiply by `n^σ` and optimize
  `σ`. Named as "Rankin trick" in Tao, *Monotone Nondecreasing Sequences of the Euler Totient Function*
  (2024), Lemma 1.5 (arXiv/Springer s44007-024-00115-z; `terrytao.files.wordpress.com/2023/10/phi-mult.pdf`),
  and in Tao's 254A Notes 1 (`terrytao.wordpress.com/2014/11/23/254a-notes-1-...`), which explicitly
  says Rankin's trick is optimized for upper bounds on logarithmic sums. So (a)'s
  `σ = 1/(4 log N)` and the `exp(−Z/(4 log N))` shape are a *coarse* instance of a classical device —
  no new identity.
- **Smooth-number distribution / Dickman ρ**: Granville, *Smooth numbers: computational number theory
  and beyond* (`dms.umontreal.ca/~andrew/PDF/msrire.pdf`); Hildebrand; Lichtman, *Explicit estimates for
  the distribution of numbers free of large prime factors* (`math.dartmouth.edu/~carlp/smoothfinal.pdf`);
  Gorodetsky, *Smooth numbers and the Dickman ρ function*. These are the standard sharp forms of the
  object (a) bounds coarsely (`∑ 1/φ` vs `Ψ`); (a) deliberately avoids them.
- **Sum of reciprocals of smooth numbers** equals the Euler product `∏_{p≤N}(1−1/p)^{−1} = E(N)`
  (MathOverflow 423175, *Series of reciprocals of smooth numbers*). This is the "trivial" mass used in
  the price comparison; it is classical, not a project claim.
- **Contract (b)** (count of `v<N` whose `q`-smooth part of `v+1` exceeds `K`, with an explicit
  half-power Euler product) is a standard dilation/union-bound count; the closest general technique is
  the large-sieve / Bombieri asymptotic-sieve Euler-product bound (Tao, *Notes on the Bombieri
  asymptotic sieve*, 2016). No exact primary source matching (b)'s stated constants was located; the
  bounded search found no verbatim statement.

**Exact remaining gap.** No located source supplies either (i) the adapter of an inverse-totient
smooth-tail bound to a **cofactor-progression density** `1/lcm(s,t)` on the shift-2 progression
`n≡b (mod Q)`, or (ii) the **signed, `log p`-weighted, profile-weighted** transfer to the corner
coefficient `U_i`/`J_H` of `cofactor-progression-transfer.md` eq. (19). The upstream repository is a
source-reuse candidate for the *unweighted finite tail* only; the source map itself records the same
residual ("An unweighted tail still needs a weighted/shifted transfer for prime-filtered Ghat
coefficients; the rate may be insufficient at intended cutoffs"). The pinned contracts are Apache-2.0;
any integration must retain attribution and a modification notice.

**Scope.** Three keyword searches plus the two source-map references; not an exhaustive citation-tree
review and not a novelty certificate. The project's own bounded registry search (return #2466 source
map) already found no exact adapter match; this search confirms the surrounding results are classical
Rankin/smooth-number facts.

## 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.

## Next experiment

Can one existing corner coefficient be written with a FIXED or o(log x) smooth-cofactor cutoff so that the pinned smooth-cofactor tail (★) gives a genuine power saving, and does the signed, log p-weighted, shifted transfer to that coefficient then land inside the corner's required budget?

Pin the corner decomposition's smooth/rough split in one existing coefficient (candidate: the smooth-cofactor part of the mixed tail U_i / J_H of cofactor-progression-transfer eq. (19)). Fix the smoothness bound N to a small constant (or N = o(log x)) while the cofactor tail reaches e^Z ~ x^alpha. Carry the coefficient's actual data through the adapter: the sign mu(d), the weight log p <= log x, the profile v_i <= 1, the shift n-2 and the congruence n == b (mod lcm(s,t)). Bound the smooth-cofactor tail with (★) sum_{N-smooth s>e^Z} 1/s <= exp(-Z/(4 log N)) E(N)^4 (no extra Euler power) and multiply by the weight envelope. Compare the resulting x^{-alpha/(4 log N)} (log x) E(N)^4 against the budget the corner needs, and re-derive the crossover u = Z/log N > 16 ln ln N numerically at the coefficient's stated cutoffs. Validate every finite identity against a stdlib checker with a planted-mutation control.

- Continue if: A specific existing corner coefficient with a fixed or o(log x) smooth-cofactor cutoff is identified, and the weighted adapter's bound is a fixed power saving x^{-alpha/(4 log N)} (log x) E(N)^4 that is strictly below that coefficient's required budget at the stated scale.
- Stop this attempt if: Every existing corner coefficient uses a growing x^delta smooth cutoff, so (★) collapses to the growing power E(N)^4 and no saving is available from this contract without a different tail estimate; record that as a scoped obstacle for route 212 rather than enlarging the computation.



## Required evidence

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

Unaccepted premises remain conditional.

## Evidence behind continued investment

- [Return #2466](/projects/twin-primes/return/2466): recorded, recorded
- [Return #2479](/projects/twin-primes/return/2479): recorded, recorded

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

## Investigation history

- [Return #2479](/projects/twin-primes/return/2479): progress. Route 212 asked whether one precisely identified existing cofactor coefficient admits the pinned
smooth-cofactor *finite tail bound* with a useful Euler-product and growing-parameter budget. That is
now decided for one exact choice.

**Exact coefficient.** In `cofactor-progression-transfer.md` eq. (1),(5),(7),(19) the unestimated tail
is `U_i = C_i^P − C_{i,H}` (`C_i^P` the full prime-r sharp coefficient, `C_{i,H}` the cofactor-`s≤H`
cut), with the congruence `n ≡ b_{s,t} (mod lcm(s,t))` of density `1/lcm(s,t)`. Take the
smooth-cofactor subfamily: cofactor `s` N-smooth and `s > e^Z`; its summed progression density is
`∑_{s N-smooth, s>e^Z} 1/s`.

**Adapter — exact, at no Euler cost.** For all `s ≥ 1`, `φ(s) < s`, hence `1/s < 1/φ(s)`, so
`∑_{s N-smooth, s>e^Z} 1/s ≤ ∑ 1/φ(s) ≤ exp(−Z/(4·log N))·E(N)^4` with `E(N)=∏_{p≤N} p/(p−1)`
(apply pinned `smooth_cofactor_rankin` verbatim, `Q = {s N-smooth : log s > Z}`). The `1/φ` versus
`1/s` mismatch costs nothing — not even the extra `E(N)` factor an `n/φ(n)` conversion would cost.
Finite exact check `adapter_free` in `check_dc.py` (Fraction arithmetic).

**Price.** With `u = Z/log N` the bound is `e^{−u/4}E(N)^4`; the trivial total smooth reciprocal mass
is `∑_{all N-smooth}1/s = E(N)`. So it beats trivial iff `u > 12 ln E(N)` and is a genuine saving iff
`u > 16 ln E(N) ≈ 16 ln ln N`: the tail must start at `e^Z = N^{Θ(log log N)}`, exponentially tall.
Finite `u_needed`: 11.09 (N=2), 17.58 (N=3), 21.15 (N=5), 23.62 (N=7), 26.42 (N=13), 30.05 (N=31).

**Applied to the existing coefficient.** (i) If the smoothness bound grows like `x^δ` (δ fixed), the
coefficient's polylog tail `H=(log x)^κ` gives `u = Z/log N → 0` < `16 ln ln N`: the gain collapses and
`E(N)^4` grows — **rate insufficient**. (ii) If the smoothness bound is fixed and the tail reaches
`x^α`, the bound is a real power saving `x^{−α/(4 log N)}·E(N)^4`; finite onsets (α=1/4): `N=2` from
`x≈10^{13.4}`, `N=3` from `10^{33.6}`, `N=5` from `10^{59}`, `N=13` from `10^{118}` — none reached at
the corner-measurement scales `x ≤ 2^36 ≈ 6.9×10^{10}`. (iii) (a) bounds only an **unweighted
reciprocal mass**; the coefficient needs signed `μ(d)`, weight `log p ≤ log x`, profile `v_i ≤ 1`,
shift `n−2`, and the congruence — none supplied. Contract (b) carries the shift `v+1` and an unweighted
`K^{−1/2}` count, still not a signed weighted sum; `source-map-2026-10-07.md` records the same gap.

**Evidence / scope.** `check_dc.py` re-derives the pinned intermediate `∑ n^{1/(4log N)}/φ(n) ≤ E(N)^3`
and the Rankin bound at N ∈ {7,11,13,17,19,23,29,31} over all N-smooth `n ≤ 2·10^5` with thresholds
`k ∈ {N,N²,2^20}`: **63 checks, 0 FAIL, exit 0**; `--corrupt` (dropping the Euler-product power)
**detects 1 mutation, exit 1**. Pinned sources read at `adc7f1241b42e322a6451854ab7e4b4c146bf78a`
(SmoothCofactorTail 1576 B, SmoothTailDensity 3574 B, SmoothCofactorMoment 7222 B,
SmoothReciprocalMass 3157 B); source map `9269972845423dd6de39b1a80266456c5424b1ad63f3ddd262d240e5f71b5694`
verified. No Lean build / `verification_plan` (no toolchain here); no published computation reproduced;
no claim on `G2`, `beta_2` or twin-prime infinitude.
- [Return #2466](/projects/twin-primes/return/2466): 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.