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

## Contribution to the goal

Register the exact O4 completion obligation from accepted source2597 as OPEN work. Full statement/domain: Original Eq.10: pi(y)-pi(y/2)~y/(2 log y). Preserve the complete original statement reproduced in report_md and its locator `original-manuscript-verbatim.md`, lines 186–192. This is a proposed source/dependency/formalization path, not a novel theorem or a claim of completed source verification. No exact dyadic count asymptotic task found. The checked eventual cardinality lower bound y/(3 log y) does not imply this asymptotic.

## Prior work and proposed difference

Original InputP is the dyadic count asymptotic. Accepted source2597 supplies an elementary eventual lower budget sufficient for Eq.1, not a PNT asymptotic. The current audit found no exact queued O4 task. No new primary-source or PNT library inspection has been performed for this draft.

## Central uncertainty

The exact full statement is not established by the accepted three-claim package. No exact dyadic count asymptotic task found. The checked eventual cardinality lower bound y/(3 log y) does not imply this asymptotic. 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

What source-compatible Lean chain proves pi(y)-pi(y/2)~y/(2 log y) with the literal real endpoints, beyond the checked reserved-prime lower budget?

Read retained InputP/Eq.10 and PrimeReserveBound. Update primary-source discovery for the exact asymptotic and inspect compatible pinned Lean source interfaces. Translate pi at real inclusive cutoffs and the strict dyadic difference before considering Nat floors; record the floor/end-point error and all eventual quantifiers. Map a candidate prime-number theorem or equivalent input to the ratio limit using genuine checked dependencies. Reuse the actual y/(3log y) reserve proof; do not infer an asymptotic from it, migrate toolchains or start a large source build. Return a minimal exact interface/dependency plan.

- Continue if: A pinned-source plan for the exact dyadic asymptotic and cutoff conversion identifies matching APIs or a first bounded missing lemma, with compatibility/import/resource requirements explicit.
- Stop this attempt if: Only a Chebyshev lower bound, foreign incompatible library, unchecked PNT premise or differently scoped interval is available. Keep O4 OPEN and record the precise statement or compatibility blocker.



## Required evidence

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

Unaccepted premises remain conditional.

## Evidence behind continued investment

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

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

## Investigation history

- [Return #2602](/projects/twin-primes/return/2602): proposed. The published manuscript explicitly retains O4 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.