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

## Contribution to the goal

Register the exact O5 completion obligation from accepted source2597 as OPEN work. Full statement/domain: Original Eqs.5-7,11: full external FGKMT one-class theorem, arbitrary-kappa/multiplicative-g/nonnegative-weight sieve and stated ranges. Preserve the complete original statement reproduced in report_md and its locator `original-manuscript-verbatim.md`: lines 116–131 (one-class comparison), lines 138–160 (Input S and its source-scope note), and lines 196–228 (Lemma 2 and its proof). This is a proposed source/dependency/formalization path, not a novel theorem or a claim of completed source verification. Route217/job5257 covers Eq.4 convention/packaging only and explicitly leaves FGKMT external. No exact task for the complete external theorem plus general sieve found. Do not duplicate the Eq.4 task or reprove the finite cover identity.

## Prior work and proposed difference

The original statement block cites the external one-class result and general sieve. No fresh primary reading/literature search is claimed here. Route217/job5257 is queued for Eq.4 binding/packaging and explicitly leaves FGKMT external; its recorded return2484 is reused. Route78/return1826 contains historical sieve-interface corrections, not a checked arbitrary-kappa theorem. The actual cover identity is already proved and excluded from O5.

## Central uncertainty

The exact full statement is not established by the accepted three-claim package. Route217/job5257 covers Eq.4 convention/packaging only and explicitly leaves FGKMT external. No exact task for the complete external theorem plus general sieve found. Do not duplicate the Eq.4 task or reprove the finite cover identity. 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 exact external FGKMT one-class theorem and arbitrary-kappa sieve statements remain missing after the checked Eq.4 cover bridge and the finite dimension-four sieve?

Read all retained Eq.5-7/11 domains and cited primary references, updating the source search before choosing a proof task. Create a statement/dependency table for the full one-class comparison and the quoted arbitrary-kappa, multiplicative-g, nonnegative-weight sieve, including support, density, error, constant and level restrictions. Compare with actual finite incidence/CRT and dimension-four statements. Read route217/job5257 and route78 historical interface repairs; leave Eq.4 packaging on its existing route and reuse the checked cover equivalence. This new route addresses the complementary complete external/general statements. Select one exact missing source-interface or finite lemma; no unbounded proof/build commitment.

- Continue if: The full O5 obligations are separately located with exact assumptions and mapped to reusable results, and one bounded missing interface/lemma is named. Any incomplete external theorem remains explicitly external rather than an assumed Lean premise.
- Stop this attempt if: The sources only prove a special dimension, different weights or a convention outside the printed statement; or the supposed task duplicates Eq.4 already owned by route217. Preserve the distinction, link existing work and keep O5 OPEN.



## Required evidence

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

Unaccepted premises remain conditional.

## Evidence behind continued investment

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

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

## Investigation history

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