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

## Contribution to the goal

Register the exact O1 completion obligation from accepted source2597 as OPEN work. Full statement/domain: Original Eq.8: constant M plus o(1), as t tends to infinity. Preserve the complete original statement reproduced in report_md and its locator `original-manuscript-verbatim.md`, lines 162–169. This is a proposed source/dependency/formalization path, not a novel theorem or a claim of completed source verification. No exact prime-harmonic asymptotic formalization or dependency-completion task found. Finite Mertens-band bounds suffice for accepted Eq.1.

## Prior work and proposed difference

The original manuscript cites [R4 section6.3] and [KK section2] for Eq.8. This draft inspected only the published project manuscript and recorded package/work audit; it has not freshly read those primary sources or run a literature search. Source2597 proves finite sufficient inequalities, not Eq.8. Route85/job1993 studies an anchored forecast over a Mertens product, not this exact asymptotic formalization.

## Central uncertainty

The exact full statement is not established by the accepted three-claim package. No exact prime-harmonic asymptotic formalization or dependency-completion task found. Finite Mertens-band bounds suffice for accepted Eq.1. 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

Which existing Lean statements and source dependencies can supply exactly sum_{p<=t} 1/p = log log t + M + o(1), with its constant and t->infinity domain, beyond the finite bounds already checked?

Read the accepted package source and the original Eq.8 references [R4 section6.3] and [KK section2]. Update the primary-source search and inspect the current pinned mathlib source interfaces, without building or importing a foreign toolchain. Record an exact statement translation: inclusive real prime cutoff, constant M and little-o quantifiers. Map every candidate theorem to those hypotheses and list the source/module closure and first missing finite or analytic lemma. Reuse MertensBand finite results rather than rediscover their proof.

- Continue if: A source-anchored exact Eq.8 statement map and dependency/API inventory either identify a matching checked theorem or one bounded next formalization lemma with an explicit missing step. No full asymptotic is reported proved by this planning step.
- Stop this attempt if: No accessible primary statement/API matches the constant and little-o domain, or its dependencies exceed the current permitted toolchain/resources. Preserve the exact mismatch and leave O1 OPEN instead of replacing it by an O(1) bound.



## Required evidence

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

Unaccepted premises remain conditional.

## Evidence behind continued investment

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

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

## Investigation history

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