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

## Contribution to the goal

Register the exact O7 completion obligation from accepted source2597 as OPEN work. Full statement/domain: Original Eq.28: m=floor(c*y*log y), z=sqrt m, coefficient 4Cc+o(1), quoted C/c pricing and hypotheses. Eq.27 endpoint is already proved and excluded from this gap. Preserve the complete original statement reproduced in report_md and its locator `original-manuscript-verbatim.md`, lines 455–484. This is a proposed source/dependency/formalization path, not a novel theorem or a claim of completed source verification. Route75/job4981 pursues finite phase-independent Bonferroni certificates. It does not prove the complete Eq.28 asymptotic/pricing. No exact completion task found; do not repeat the already proved y*log y endpoint.

## Prior work and proposed difference

Original Eq.28 cites FI Theorem6.9/Corollary6.10 conditionally on the stated reading. The draft has not newly inspected these references or reproduced pricing. Route75/job4981 concerns finite phase-independent certificate bounds, not the full asymptotic/priced construction; return2306 is reused. The y*log y endpoint is already proved in accepted source2597 and is not an O7 gap.

## Central uncertainty

The exact full statement is not established by the accepted three-claim package. Route75/job4981 pursues finite phase-independent Bonferroni certificates. It does not prove the complete Eq.28 asymptotic/pricing. No exact completion task found; do not repeat the already proved y*log y endpoint. 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 source and formal dependencies establish the original m=floor(c*y*log y), z=sqrt(m) Eq.28 estimate, local-factor pricing and c range, beyond the already proved y*log y endpoint?

Read Eq.28 and [FI Theorem6.9/Corollary6.10] with the original kappa2/InputS interpretation; update primary-source discovery before relying on the numerical reading. Bind the exact m, z and residue family, the coefficient4Cc+o(1), z=o(y), unused-prime asymptotic, c<1/(8C), prime2 factor, and quoted delta=.05/K=3/C1(1/2)=805.5 pricing. Compare with route75/job4981 finite phase-independent certificate work and route78 normalization history without rerunning either. The proved PrimaryMain.eventual_y_log_gap endpoint is reused and not proposed as new. Return an exact source-to-formal-statement price/interface checklist and one bounded missing lemma; keep the printed numerical reading conditional until actually supported.

- Continue if: A complete Eq.28 statement/domain/constant map identifies the precise general-sieve/prime inputs and the smallest missing lemma. It preserves the distinction between a priced coefficient and a certified practical threshold.
- Stop this attempt if: The source convention differs, prime2 is dropped, only the old-cutoff greedy experiment or already proved endpoint is recovered, or the numerical FI interpretation remains unread. Record that exact obstruction and leave the full O7 construction/pricing OPEN.



## Required evidence

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

Unaccepted premises remain conditional.

## Evidence behind continued investment

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

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

## Investigation history

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