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

## Contribution to the goal

Register the exact O6 completion obligation from accepted source2597 as OPEN work. Full statement/domain: Original Eqs.20-21: O(1) harmonic expansion and both directions of asymp with actual g(p), bands and parameters. Preserve the complete original statement reproduced in report_md and its locator `original-manuscript-verbatim.md`, lines 355–387. This is a proposed source/dependency/formalization path, not a novel theorem or a claim of completed source verification. Route78 is known, with no current next step; historical ledger/sieve-interface repairs do not register a full Lean Eq.20/21 completion. No exact active completion task found.

## Prior work and proposed difference

Route78 is known; returns1015/1826 and accepted dependency1538 document ledger/interface/normalization repairs with no current next step. The current manuscript expressly leaves Eqs.20-21 unproved as stated while using sufficient finite inequalities. This draft performed no fresh external literature or source theorem inspection.

## Central uncertainty

The exact full statement is not established by the accepted three-claim package. Route78 is known, with no current next step; historical ledger/sieve-interface repairs do not register a full Lean Eq.20/21 completion. No exact active completion task found. 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 lemmas upgrade the actual band/density product to the full Eq.20 O(1) expansion and both directions of Eq.21 asymp, retaining the printed parameters and small-prime factors?

Read the original Eqs.20-21 and actual g(p), z0, z1, V and parameter definitions in the accepted source. Compare the existing one-sided finite MertensBand/EulerRatio/sieve bounds with both directions of the printed products. Read route78/return1826 to preserve its corrected prime2/3 ledger and exp(O(1)) wording; do not repeat its arithmetic repair. Inventory which Eq.8 differences and convergent quadratic/higher logarithmic terms need exact Lean statements. Coordinate with O1 only using genuine later record IDs. Return a finite local factor/product lemma and its dependencies or an exact missing harmonic-difference premise; no global asymptotic assumption or compiler run.

- Continue if: An exact two-sided product/error dependency map retains both comparisons and identifies a genuinely missing bounded next lemma, reusing the existing one-sided budget and historical corrections.
- Stop this attempt if: The plan pays only the already checked upper budget, omits small primes, treats exp(O(1)) as 1 or silently assumes Mertens. Record the specific missing direction/premise and keep O6 OPEN.



## Required evidence

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

Unaccepted premises remain conditional.

## Evidence behind continued investment

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

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

## Investigation history

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