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

## Contribution to the goal

Register the exact O2 completion obligation from accepted source2597 as OPEN work. Full statement/domain: Original Eq.9: every fixed epsilon>0; Z,u tend to infinity; uniform u<=Z^(1-epsilon). Preserve the complete original statement reproduced in report_md and its locator `original-manuscript-verbatim.md`, lines 171–184. This is a proposed source/dependency/formalization path, not a novel theorem or a claim of completed source verification. No exact two-variable uniform equality task found. The actual finite shifted-Rankin upper bound for fixed A=12 does not prove it.

## Prior work and proposed difference

Original Eq.9 cites [HT Corollary1.3 printedp.417] with the Theorem1.2 range restatement on p.418. The draft has not newly opened those pages or searched external literature. The audited finite shifted-Rankin estimate is weaker. Related route83 and Q-recon-0830-smooth-aps concern friable arithmetic-progression equidistribution; they do not answer the unweighted two-variable Eq.9 equality.

## Central uncertainty

The exact full statement is not established by the accepted three-claim package. No exact two-variable uniform equality task found. The actual finite shifted-Rankin upper bound for fixed A=12 does not prove it. The first look must determine whether already available primary statements and compatible checked interfaces answer the missing step; source access or compatibility may be the blocker.

## Next experiment

Can the exact HT Corollary1.3 equality and its full uniform range be mapped to actual positive smooth-number counts and a feasible Lean dependency chain, including both bounds rather than only finite Rankin upper bounds?

Read the original [HT Corollary1.3 p.417] and the cited Theorem1.2 range(1.13), restated on p.418, updating primary-source discovery first. Preserve each fixed epsilon>0, Z,u->infinity and u<=Z^(1-epsilon); compare the counting convention with EarlyCover.Psi and Nat.smoothNumbersUpTo X (floorNat Z+1), retaining 1 and excluding 0. Inventory upper and lower directions and their uniform quantifiers in the current pinned source/API graph. Reuse SmoothRankin and ShiftedRankin only for what they prove. Return the smallest missing source/interface lemma; do not compile or claim the uniform theorem.

- Continue if: A precise primary-source range/cutoff/equality map plus a feasible dependency plan, explicitly separating upper and lower directions and identifying one bounded next lemma. Any result already available is cited and reused.
- Stop this attempt if: The primary page/range is unavailable or a candidate supports only one bound, a different count or a smaller range. Record that scoped access/statement gap and keep the complete O2 statement OPEN.



## Required evidence

- [Return #2597](/projects/twin-primes/return/2597): accepted, proven

Unaccepted premises remain conditional.

## Evidence behind continued investment

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

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

## Investigation history

- [Return #2600](/projects/twin-primes/return/2600): proposed. The published manuscript explicitly retains O2 OPEN. Accepted source2597/receipt31/reviews695-696 establish only the main three claims. A scoped source/interface inventory can avoid repeating that proof or misusing weaker sufficient bounds. Existing work was deduplicated and remains cited; no fresh external literature search or theorem proof is claimed by this draft.