{"id":2656,"job_id":5415,"problem_id":1,"lane_id":null,"type":"explore","user_id":1,"model":"deepseek-v4-flash","provider":"deepseek","report_md":"# First look, route #239: the O5 \"context-and-sieve\" obligation is two located external statements plus one missing general-κ interface\n\n**Verdict: promising.** Prior work does not cover the route's contribution; the full O5 obligations\nare now separately located with exact assumptions and ranges, mapped onto reusable results, and one\nbounded missing interface/lemma is named. Nothing found contradicts the mapping. This is a\nsource/interface/dependency inventory only: it proves no external theorem, reads no printed page\nbeyond the arXiv v2 primary text already cited by the project, and does not reopen the Eq.(4) task\nowned by route #217.\n\n## What the assignment asks\n\nJob #5415 (`explore`, research stage `first_look`) on route **#239**, *\"O5 OPEN: full FGKMT\ncomparison and general quoted sieve completion plan\"*. The route registers the obligation that the\naccepted three-claim package (return #2597) leaves as statement-bundle `unmapped_claims` entry\n`context-and-sieve: External one-class comparison and the general quoted sieve (original Eqs. 5–7,\n11)`. Central question, verbatim from the brief:\n\n> Which exact external FGKMT one-class theorem and arbitrary-kappa sieve statements remain missing\n> after the checked Eq.4 cover bridge and the finite dimension-four sieve?\n\nThe brief also fixes the boundaries: do **not** duplicate route #217/job5257 (Eq.4 convention/\npackaging) and do **not** reprove the finite cover identity.\n\n## What was read (hash-pinned)\n\n- Manuscript `kk-lower-bound.md`, SHA-256 `6c287c180b331318a19b3fb0a0e571147e01d785c4efa4341cf3bba5bd1c8e80`\n  (served at `/projects/twin-primes/docs/paper/kk-lower-bound.md`; equals return #2603's cited hash).\n  Its §9 states the exact O5 asymmetry: *\"The full external Ford–Green–Konyagin–Maynard–Tao\n  one-class theorem and the quoted arbitrary-kappa/multiplicative-g/nonnegative-weight sieve are\n  not established here as those statements. Actual incidence/CRT moments, the residue-set\n  interpretation, and the required finite dimension-four sieve are proved.\"*\n- `kk-lower-bound.revised.md`, SHA-256 `50a60a0344a8a32d025499caf26983534df363d9d0c9988e41adbdc2d416b521`\n  (served with return #2597): §2 Eq.(4)–(5), §3 Input S, §10 claim map and the [KK]/[HT]/[HR]/[FI]\n  reference list.\n- Retained Lean: `statement-bundle.json` (unmapped-claims list), `SieveInterface.lean`,\n  `SieveParameters.lean`, `SieveCoarse.lean` (raw-fetched from return #2597, sha-verified).\n- Route records: route #239, return #2603 (origin proposal), route #217, return #2484 (the Eq.4\n  boundary), return #1826 (historical interface repairs).\n- External primary text: Kalmynin–Konyagin arXiv:2302.00459**v2** full text and abstract\n  (SHA-256 `63bc250b…`, `01bff059…`); Ford–Green–Konyagin–Maynard–Tao arXiv:1412.5029 abstract\n  (SHA-256 `120591d4…`). Saved under `work/ext/`.\n\n## The O5 statement/dependency table\n\n| item | exact statement / object | exact source | status after this look |\n|---|---|---|---|\n| **O5-a** | One-class Jacobsthal lower bound: for `y ≥ 19`, `P(y)=∏_{p≤y}p`, `j(P(y)) ≫ y·(ln y)(ln ln ln y)/(ln ln y)`; equivalently `max_{p_{n+1}≤X}(p_{n+1}−p_n) ≫ ln X·(ln ln X)(ln ln ln ln X)/(ln ln ln X)` for large `X` | **FGKMT**, *Long gaps between primes*, J. Amer. Math. Soc. **31**:1 (2018), 65–105 (arXiv:1412.5029) = KK arXiv:2302.00459v2 reference **[1]** = KK `Theorem ([1])` | **Located exactly.** Deep external theorem; no Mathlib/Lean formalization exists; must stay external (named hypothesis), not a package axiom. This is manuscript Eq.(5)'s input. |\n| **O5-b** | Elementary comparison `G_2(P(y)) ≥ g(P(y))` (original Eq.(4)) | manuscript §2 | **Owned by route #217** (`Integration.lean`, `oneClassCover_le_G2`); not touched here. |\n| **O5-c** | **Input S** (general quoted sieve / fundamental lemma): `κ>0`, `z≥2`; multiplicative `g` with `0 ≤ g(p) ≤ κ`, `g(p) < p`; nonnegative weights `a_n` with, for every squarefree `d | P(z)`, `Σ_{n≡0 (d)} a_n = g(d)X/d + r_d`, `|r_d| ≤ g(d)`; `z ≪ X` ⟹ `S(a,z) = Σ_{(n,P(z))=1} a_n ≪_κ X·V(z)`, `V(z)=∏_{p≤z}(1−g(p)/p)` | **KK Lemma 1**, p.4 (self-contained restatement; proof: *\"a version of the fundamental lemma of sieve theory. See, for example, [5, Theorem 2.2]\"*), where [5] = **Halberstam–Richert, *Sieve methods*, Academic Press (1974)**, Thm 2.2; project names pp.68–69. Second carrier: **Friedlander–Iwaniec, *Opera de Cribro*, Thm 6.9 + Cor 6.10** | **Statement located exactly** (KK's own Lemma 1 is self-contained, so the statement is not an unread-page dependency). **Provenance sub-gap:** HR pp.68–69 and FI pp.68–69 were never read as page images in the project (OCR custody only, return #158). **Interface gap:** the accepted package has **no general-κ statement at all** (only the concrete κ=4 instance). |\n| **O5-d** | Case-1 reduction: sets `Ω_p ⊂ ℤ/pℤ` with `|Ω_p|=g(p)` ⟹ `S(X,Ω) ≪ X·V(z)` (KK Corollary 1, p.4) = original Eq.(11) / manuscript Lemma 2 | KK Corollary 1 | Located; the manuscript itself calls Lemma 2 elementary. The accepted package proves the **concrete κ=4 analogue** (`SieveCoarse.actual_survivor_le`, `SieveParameters.actual_uniform_survivor`). |\n| **O5-e** | The actual finite **dimension-four** sieve for the manuscript's own `Ω_p` (`g(2)=1`, `g(3)=2`, `g(p)≤4`, `g(p)/p≤4/5`) | accepted package: `ActualBoundingSieve.lean`, `SieveCoarse.lean`, `SieveParameters.lean` | **PROVED** (Selberg, self-contained; it does not invoke Input S). Distinct from the general-κ statement; do not duplicate. |\n\n## Reading of the boundary (what is *not* missing)\n\nThe manifest's two sources do not require Input S at all. `SieveCoarse.actual_survivor_le` proves the\nmanuscript's own sieve with an explicit Selberg denominator and a coarse polynomial error `4L⁵`, and\n`SieveParameters.actual_uniform_survivor` turns it into `uniformConstant·X·fullV + y/(12 log y)` on\nthe proved domain. So the general quoted sieve (O5-c) is retained for the *general* statements and the\nweaker bound (manuscript §8, eq.(27)), not for Eq.(1). That is consistent with the manuscript's own\nclaim map, which marks bound (1) as DERIVED/INFERRED and (11) as elementarily reduced.\n\n## The one bounded missing interface/lemma\n\n**Name:** a general-κ upper-sieve *statement interface* — call it `SieveUpperBound` — mirroring KK\nLemma 1 exactly, introduced into the pinned toolchain as an **explicit conditional hypothesis**\n(no axiom, no `sorry`), together with the observation that the accepted concrete κ=4 development is\nits instance.\n\nWhat it changes: today `context-and-sieve` is an opaque `unmapped_claims` string. A named interface\nturns the *general* obligation into a single reusable object whose hypotheses (arbitrary `κ`, `z≥2`,\nmultiplicative `g`, `0≤g(p)≤κ`, `g(p)<p`, nonnegative weights, the divisor-sum identity with\n`|r_d|≤g(d)`, and the level restriction `z ≪ X`) are explicit and checkable, while O5-a (the FGKMT\nvalue) and the HR/FI provenance stay declared external. Nothing in the accepted three-claim package\nis weakened: the interface is a parameter, so any theorem proved under it is conditional.\n\n**Smallest adequate acceptance check (falsifiable):** the interface file elaborates at the package's\npinned toolchain, `#print axioms` for the interface and any bridge lemma returns exactly\n`[propext, Classical.choice, Quot.sound]` (no `sorryAx`), and a snapshot diff of the declared\nhypothesis set against KK Lemma 1 shows all six conditions present. Falsified if any hypothesis is\ndropped (in particular `g(p)<p` or `z≪X`) or if `sorryAx` appears.\n\n**Not** proposed here: proving O5-a or O5-c (deep external mathematics, forbidden as a Lean axiom),\nreading the printed HR/FI pages (a separate documentary provenance obligation), or re-doing O5-b/O5-e.\n\n## What each outcome would change\n\n- If the interface is accepted: the general quoted sieve becomes a named, reusable premise; the\n  formulation work in route #217's package can cite it instead of restating a prose gap, and the\n  `context-and-sieve` unmapped item splits cleanly into \"external value (FGKMT)\" + \"named hypothesis\n  (Input S)\" + \"checked dimension-four instance\".\n- If the interface cannot be stated at the pins: record the exact definitional obstruction (which\n  hypothesis resists the package vocabulary) as a scoped obstacle on route #239, keep O5 OPEN, and\n  leave the FGKMT/HR/FI inputs explicitly external.\n\n## Limits\n\nNo printed HR/FI page was read; no external theorem was proved; no Lean was executed in this return;\nno published number was recomputed. Byte-level structure claims are decided by the attached\n`check_gt.py` (python3 stdlib, no network, no Lean). The mathematical mapping is author-side and\nstays heuristic pending the proposed formalization. Transcript scrubbed of credentials, private\nownership identifiers and unrelated pre-assignment history; research reads of this project's served\ndocuments retained.\n\n## Sources\n\n- Manuscript `kk-lower-bound.md` SHA-256 `6c287c18…c8e80`; https://solveathome.org/projects/twin-primes/docs/paper/kk-lower-bound.md\n- `kk-lower-bound.revised.md` SHA-256 `50a60a03…b521`; route #239; return #2603; route #217; return #2484; return #1826\n- K. Ford, B. Green, S. Konyagin, J. Maynard, T. Tao, *Long gaps between primes*, JAMS **31**:1 (2018) 65–105; arXiv:1412.5029\n- A. B. Kalmynin, S. V. Konyagin, *A polynomial analogue of Jacobsthal function*, arXiv:2302.00459v2 (Lemma 1, Corollary 1, p.4; Theorem ([1]))\n- H. Halberstam, H.-E. Richert, *Sieve methods*, Academic Press (1974), Thm 2.2; J. B. Friedlander, H. Iwaniec, *Opera de Cribro*, AMS Colloq. Publ. 57 (2010), Thm 6.9 + Cor 6.10\n","patch":null,"cpu_hours":0,"hashes":{"sah.py":"21a1d3556191bf54458b13fa0ebe41b4550fb92a33ab9bee6518d82ef222c843","check_gt.py":"e9b5ad1869c19f179e26cf74b1a002991f24cb3a0b4b9fd8f3f304bc3466ef14","fetch_gt.py":"d90ee33cd71eb0202e36038cd356bb8de5760fad2a05eb10193c6c44321539df","check_gt.out":"951271143f720ed630de8db03372c517ab5081e41b4c070891d20fb70fe64742","recipe_gt.md":"6fb5feabb072d7278d78044de2402299dea9c56a7858dd386bc13ee5c0e61b67","redact_gt.py":"2dc4de62118205a289687e6fcbe78a5d15fbe043be1e10987bbba9b67f7617c6","report_gt.md":"9ba73fa5b962e7c80499b8c4d3ebb7b42b315ce19d031091e1d77d4c06c749b0","upload_gt.py":"1e4dd8705f6156a2b2a69ab3a9a0b0439e19f3877d37c9cb7c9e8927f14f2d1c","manuscript.md":"6c287c180b331318a19b3fb0a0e571147e01d785c4efa4341cf3bba5bd1c8e80","next_step.json":"daba739f82ef995f4511cca436480c7333652f15ec12916d5b3cc3efda18a456","route_239.json":"8c639cc329e4561832506fc62e2b3860632eddc7528fe68fea4b6285cde1af6a","ext_report.json":"27dcb675cfd1f5d47a329641f13663f3c78268c545055b5e9e9ab12570c2c326","SieveCoarse.lean":"8bc57801384e29fc3b6d53e4bec64cea1fb4f77865fdb36fb5b834e457ac5d03","return_2484.json":"8efdc2f2dcd1669fe8748be5ecd41791bfff60c40ec65d97bb98d6dee8d2a27c","return_2603.json":"d953e755fd438d450da9e9d84d0c00c20b0b90d3541ab4e1e90b2d99b10748ad","fetch_arxiv_gt.py":"1d85039840297ccdbd4cb99b061ff9bd27b7476abc36e2fee49ff1df360ea688","fetch_files_gt.py":"aa0bf9f6d6b2256c556b6a9bf4015a3f393ace4096f1ab96511a14b586879819","files_report.json":"af7b6c27adc72e7638d6db6493f123e20461e2b2f5a94c2e923e92125c4de757","SieveInterface.lean":"ea07fcd56eb2688d70125f4b0ed11080554dc56821fd73489ab5683882384d73","build_payload_gt.py":"89b57482fb51b898d871797c497f68b288790f0a74fb9ae60f9f7ab94b246343","SieveParameters.lean":"f7d83b195e5748ef941f5d7a1c9fcd9b11ad99893bac45b9342e1d558939007b","check_gt.control.out":"c21dfe6649ecaec0b78a988a30df61c3708de8ff876e8e48af80ef7fbd987112","export_transcript.py":"029efc05e4b791b297f3cb254a24887e3d23b98b1ab4a6639d1f6dc7b69cc82f","kk-2302.00459v2.html":"63bc250b513b82735c0f4cc7aaae7d49d036703ed7ab67845c4e0605d5619a2d","statement-bundle.json":"1f3f0a4bc27f24de44aef5a53389f70e0797a9883687b54e695db5257dd50ad6","research_evidence_gt.md":"6b7b23f161bae7ff87e7c082c72ab27aade98a91d51a089d28746a3d46eb03f7","ActualBoundingSieve.lean":"594b6695d429f3f3afd144925eb7567b613ca6ba4c9ee56a2de6d260f5f32782","fgkmt-1412.5029.abs.html":"120591d462fa839ca8924ffff9e5b526d133c7c3f8d1340e3115857a612ed43f","research_prior_art_gt.md":"cc006b9f0f5c8b1bc802c98b79e487c51e24904f81806b89a2f6364d0279dfd5","kk-lower-bound.revised.md":"50a60a0344a8a32d025499caf26983534df363d9d0c9988e41adbdc2d416b521"},"author_rung":null,"status":"recorded","final_rung":"recorded","created_at":"2026-10-10T00:19:21.009Z","repo_url":null,"commit":null,"cites":{"returns":[2603]},"tokens":{"log":"custom","input":0,"models":{"deepseek-v4-flash":0},"output":0,"source":"none","entries":0,"cache_read":0,"cache_write":0,"observed_models":["deepseek-v4-flash"]},"paper_slug":null,"revision_path":null,"revision_sha":null,"recipe_md":"# Reproduction recipe for the route-239 first-look byte claims\n\nThis first look is documentary: no Lean is executed, no published number is recomputed, and no\nexternal theorem is proved. The decisive claims are byte-level structure claims over retained\ninputs, decided by `check_gt.py` (python3 >= 3.10, standard library only, no network, no Lean, no\nrandomness, no timing).\n\n## Inputs (all content-addressed; fetch each by SHA-256 and verify)\n\nFrom the accepted package / served docs (raw-bytes fetch, then SHA-256):\n\n- `manuscript.md`  <- served `/projects/twin-primes/docs/paper/kk-lower-bound.md`, SHA-256\n  `6c287c180b331318a19b3fb0a0e571147e01d785c4efa4341cf3bba5bd1c8e80`\n- `kk-lower-bound.revised.md` SHA-256 `50a60a0344a8a32d025499caf26983534df363d9d0c9988e41adbdc2d416b521`\n- `statement-bundle.json`, `SieveInterface.lean`, `SieveParameters.lean`, `SieveCoarse.lean`,\n  `ActualBoundingSieve.lean`, `SelbergFinite.lean`, `FiniteCoreTargets.lean`,\n  `IncidenceMoments.lean`, `CRTMoments.lean`, `DivisorMoments.lean` (return #2597, each matched\n  against its served `sha256` in `files_report.json`)\n\nExternal primary sources (raw HTML snapshots, SHA-256 in `ext_report.json`):\n\n- `ext/kk-2302.00459v2.html` (Kalmynin-Konyagin full text; contains Lemma 1, Corollary 1,\n  `j(P(y))`, `V(z)`, and the references with `[1]` FGKMT and `[5]` Halberstam-Richert)\n- `ext/kk-2302.00459.abs.html`, `ext/fgkmt-1412.5029.abs.html`\n\nRecords: `route_239.json`, `return_2603.json`, `return_2597.json`, `return_2484.json`,\n`route_217.json`, `return_1826.json`.\n\n## Command\n\n```\npython3 check_gt.py\n```\n\nExpected: stdout exactly equal to `check_gt.out` (50 `PASS` lines ending `checks=50 fails=0`) and\nexit code 0.\n\nNegative control:\n\n```\npython3 check_gt.py --corrupt\n```\n\nExpected: every check FAILs (50 `FAIL` lines, ending `checks=50 fails=0` is not printed; the run\nends with `checks=50 fails=50`) and exit code 1.\n\n## Coverage\n\nThe checker decides only byte-level structure: the served manuscript hash; the manuscript's O5\nasymmetry sentence, Eq.(4) sentence, Eq.(5) LaTeX shape and the `[KK, Theorem A and reference 1]`\nlocator; the revised manuscript's Input S heading, its HR Theorem 2.2 provenance line, the FI\nsecond-carrier line and the recorded HR page-read gap; the statement bundle's `context-and-sieve`\nunmapped entry; route/return boundary ids (parent 217, origin 2603, job 5415, `oneClassCover_le_G2`);\nand the presence in the KK/FGKMT snapshots of the exact external statements. It does **not** establish\nstatement correctness, does not read the printed Halberstam-Richert or Friedlander-Iwaniec pages,\ndoes not compile Lean, and does not certify that Eq.(5)'s meaning is captured — that mapping and the\nproposed general-kappa interface are the next step's job.","verification":null,"target":null,"finding":null,"human_md":null,"provisional":false,"effects_applied_at":null,"effort":null,"also_fix":null,"transcript_omitted":{"share":0,"omitted":0,"outputs":0},"patch_hash":null,"superseded_by":null,"duplicate_of":null,"transcript_resubmitted_at":null,"file_notes":null,"research":{"outcome":"promising","route_id":239,"next_step":{"method":"Add one Lean file to the accepted package (no new imports beyond the pinned Mathlib) declaring a structure/Prop 'SieveUpperBound' that mirrors KK Lemma 1 exactly: parameters kappa>0, z>=2; fields g : Nat -> Real multiplicative with 0 <= g p <= kappa and g p < p; a : Nat -> Real with 0 <= a n; for every squarefree d with d | P(z) a field giving sum_{n : d | n} a n = g d * X / d + r d together with |r d| <= g d; a level field encoding z << X; and the conclusion siftedSum a (P z) <= C * X * V z for a constant C depending only on kappa. Keep it a hypothesis (never an axiom, never sorry). Add a short bridge remark/lemma showing the concrete kappa=4 data of SieveCoarse.actual_survivor_le / SieveParameters.actual_uniform_survivor satisfies those hypotheses (g = ActualBoundingSieve.density (omegaSet z0 z1), weights = the manuscript incidence weights), by #check/specialization only, no new analytic proof. Do not attempt to prove the interface, do not reopen O5-b (route #217) or O5-e (the proved dimension-four sieve), and leave the FGKMT value and the Halberstam-Richert/Friedlander-Iwaniec page reads as declared external inputs. Also write the source/dependency table as a served markdown file.","compute":{"ram_gb":2,"disk_gb":1,"cpu_hours":0},"failure":"The interface cannot be stated at the pins without dropping or weakening a KK Lemma 1 hypothesis (most likely g(p)<p, the nonnegative-weight condition, or the z<<X level restriction), or any hypothesis is only expressible as an axiom/sorry. Record the exact definitional obstruction as a scoped obstacle on route #239, keep O5 OPEN, and leave the FGKMT and Halberstam-Richert/Friedlander-Iwaniec inputs explicitly external rather than assumed Lean premises.","success":"The interface file elaborates at the package's pinned toolchain; #print axioms for the interface and the bridge returns exactly [propext, Classical.choice, Quot.sound] with no sorryAx; and a snapshot diff of the declared hypothesis set against Kalmynin-Konyagin Lemma 1 shows all six conditions present (kappa>0 and z>=2; multiplicativity; 0<=g(p)<=kappa; g(p)<p; nonnegative weights; the divisor-sum identity with |r_d|<=g(d); the z<<X level restriction). The 'context-and-sieve' unmapped item can then be annotated as external-value + named-hypothesis + checked-instance.","question":"Can the general quoted sieve 'Input S' (Kalmynin-Konyagin Lemma 1 = Halberstam-Richert, Sieve methods (1974), Theorem 2.2) be captured as a single named, axiom-free general-kappa statement interface in the pinned toolchain, recognized as the general form of the accepted concrete kappa=4 dimension-four development, so that the statement-bundle 'context-and-sieve' unmapped item splits into an external value (the FGKMT one-class theorem) plus a named reusable hypothesis (Input S) plus a checked concrete instance?","budget_hours":0.5,"required_tools":[],"required_sources":[]},"depends_on":[2597,2603],"evidence_md":"First look on route #239 (O5 \"context-and-sieve\"). The obligation is not one missing lemma but two\nlocated external statements plus an absent interface, and the split is now decisive.\n\n(1) The one-class input behind manuscript Eq.(5) is exactly K. Ford, B. Green, S. Konyagin,\nJ. Maynard, T. Tao, \"Long gaps between primes\", J. Amer. Math. Soc. 31:1 (2018) 65-105\n(arXiv:1412.5029). This is not inference: the project's own cited paper, Kalmynin-Konyagin\narXiv:2302.00459v2, lists it as reference [1] and restates it as its \"Theorem ([1])\":\nj(P(y)) >> y (ln y)(ln ln ln y)/(ln ln y) for y >= 19, P(y)=prod_{p<=y} p; equivalently\nmax_{p_{n+1}<=X}(p_{n+1}-p_n) >> ln X (ln ln X)(ln ln ln ln X)/(ln ln ln X), which is verbatim the\nFGKMT abstract bound. So Eq.(5)'s external theorem is fully located with its range; no Mathlib/Lean\nformalization of it exists, so it must remain a named external input, never a package axiom.\n\n(2) Input S (the general quoted sieve) is KK Lemma 1 on p.4, and KK's Lemma 1 is a self-contained\nrestatement: kappa>0, z>=2, multiplicative g with 0 <= g(p) <= kappa and g(p) < p, nonnegative\nweights a_n with sum_{n=0 mod d} a_n = g(d)X/d + r_d and |r_d| <= g(d) for all d|P(z), z << X, giving\nS(a,z) <<_kappa X V(z), V(z)=prod_{p<=z}(1-g(p)/p). KK's proof cites \"[5, Theorem 2.2]\", where its\nreference [5] is H. Halberstam and H.-E. Richert, \"Sieve methods\", Academic Press (1974). So the\nexact statement is located from a primary source already read at page 4 by the manuscript; the\nresidual is provenance (HR pages 68-69, and the FI second carrier Thm 6.9 + Cor 6.10, were never\nread as page images) plus the absence of any general-kappa object in the accepted package.\nKK Corollary 1 (S(X,Omega) << X V(z) for sets Omega_p with |Omega_p|=g(p)) is the manuscript's\nLemma 2 / original Eq.(11).\n\n(3) The accepted package does not need Input S at all. SieveCoarse.actual_survivor_le proves the\nactual manuscript sieve for its own Omega_p (g(2)=1, g(3)=2, g(p)<=4) with an explicit Selberg\ndenominator and coarse error 4L^5, and SieveParameters.actual_uniform_survivor turns it into\nuniformConstant * X * fullV + y/(12 log y) on the proved domain. The documented reason Input S is\nretained is the general statements and the weaker bound (manuscript eq.(27)), not Eq.(1). This\nmatches the manuscript's own claim map.\n\n(4) Boundary with route #217: the elementary comparison G2 >= g (original Eq.(4)) is route #217's\nIntegration.lean (oneClassCover_le_G2) and is untouched here. O5 is complementary, not duplicate.\n\nNamed single bounded missing interface/lemma: a general-kappa upper-sieve statement interface\n(\"SieveUpperBound\") mirroring KK Lemma 1 exactly, added as an explicit conditional hypothesis (no\naxiom), plus the observation that the accepted concrete kappa=4 development is its instance. This\nconverts the opaque \"context-and-sieve\" unmapped claim into a checkable object with all six\nhypotheses explicit, while the FGKMT value and HR/FI provenance stay declared external.\n\nAcceptance: the interface elaborates at the pinned toolchain, #print axioms is exactly\n[propext, Classical.choice, Quot.sound] with no sorryAx, and a snapshot diff shows all six KK Lemma 1\nhypotheses declared; falsified if any is dropped (notably g(p)<p or z<<X) or sorryAx appears.\n\nLimits: no external theorem proved, no printed HR/FI page read, no Lean executed, no number\nrecomputed; byte claims are decided by the attached checker; the mathematical mapping is heuristic.","prior_art_md":"Search date 2026-10-10 (this session). The route record claimed no fresh primary reading; this look\nadds one. Queries: author names + identifier 2302.00459; \"Jacobsthal function lower bound primorial\ng(P(y))\"; \"Kalmynin Konyagin Theorem A reference 1 one-class lower bound\"; \"Ford Green Konyagin\nMaynard Tao Long gaps between primes JAMS 2018\". Reused the project's recorded searches\n(route #217's 2026-10-07 run: no Lean/mathlib Jacobsthal formalization; no published two-class lower\nbound) and did not re-run the broad dedup audit already recorded in return #2603 (234 routes, 205\njobs). Sources inspected: arXiv:2302.00459v2 full text (HTML, SHA-256 63bc250b...) and abstract\n(01bff059...); arXiv:1412.5029 abstract (120591d4...); the served manuscript and the route-217/239\nrecords.\n\nDecisive new findings:\n1. KK reference [1] = K. Ford, B. Green, S. Konyagin, J. Maynard, T. Tao, \"Long gaps between primes\",\n   J. Amer. Math. Soc. 31:1 (2018) 65-105. KK restates its one-class content as \"Theorem ([1])\"\n   with j(P(y)) >> y (ln y)(ln ln ln y)/(ln ln y), y>=19. This is the exact external theorem behind\n   manuscript Eq.(5) and it is named, ranged and reachable from a primary source.\n2. KK reference [5] = H. Halberstam, H.-E. Richert, \"Sieve methods\", Academic Press (1974), cited by\n   KK Lemma 1's proof as \"[5, Theorem 2.2]\". KK Lemma 1's statement is self-contained.\n3. KK Corollary 1 = S(X,Omega) << X V(z) = manuscript Lemma 2 / original Eq.(11).\n\nExact remaining gap (distinct from route #217): (a) no general-kappa upper-sieve interface exists in\nthe accepted package (SieveCoarse/SieveParameters give only the concrete kappa=4 instance and\nActualBoundingSieve only the actual residue sets); (b) the Halberstam-Richert printed pages 68-69 and\nthe Friedlander-Iwaniec second carrier (Opera de Cribro, Thm 6.9 + Cor 6.10, pp.68-69) were never\nread at page image in the project - documentary provenance, not statement availability; (c) the FGKMT\nvalue is deep external mathematics with no Lean formalization anywhere (Mathlib has no Jacobsthal\ncovering function; confirmed in route #217's recorded search), so it cannot become a package theorem\nand must stay a named external hypothesis. Route #217/job5257 owns only Eq.4 convention/packaging and\nexplicitly leaves FGKMT external; the finite cover identity and the dimension-four sieve are proved\n(return #2597) and are not re-proved here. No prior return builds the general quoted sieve as a named\ninterface, so the proposed bounded step is distinct and unclaimed.\n\nUnchanged carry-forward (not re-investigated): the 2026 computational preprint on covering residue\nsystems (researchgate.net/publication/415098139) remains an access gap in the project record."},"research_route_id":239,"verification_plan":null,"verification_fingerprint":null,"review_admitted_at":null,"department_id":"dept_0e793a31e299699dfaaa6fee","run_id":"run_88a0a7d1ca714c9ec341f3ca","triage_lead":null,"revision_base_sha":null,"integration":null,"resolves":null,"paper_exposition":null,"handle":"Benjaminsen","job_brief":"Search online for existing attempts, results, tables and datasets before testing feasibility. Reuse the recorded search and inspect the closest sources and weakest assumption. Use published numbers with citations; do not reproduce them in a first look. Seek the smallest experiment on the uncovered step. Recommend promising only with specific evidence and a bounded next step; do not claim the route is proved. Map the assumptions of any borrowed method onto this problem.\n\nRead GET <project base>/research-routes/239 and return #2603. Return the ordinary report and transcript plus research: {route_id: 239, outcome: \"promising|progress|blocked|inconclusive|known|result\", evidence_md: \"what the evidence changes, <=4000 chars\", prior_art_md: \"updated online search record, sources and exact remaining gap, <=4000\", next_step: {question, method, success, failure, budget_hours} <only for continued pursuit; what to do, never when or how fast; it must not ask for what a return on this route or a linked route already did, and the route returns it builds on go in depends_on or cites.returns>, obstacle: {kind, statement, assumptions, evidence, revisit_when} <for blocked/inconclusive>, depends_on: [<return ids actually required>]}. A result with a distinct next_step requests review and continues pursuit concurrently; omit next_step when no further experiment is warranted. Use known with prior_art_md and no next_step or obstacle when cited prior work already covers the proposed contribution; it stops automatic investigation without requesting review. The evidence grade is separate. Do not close a broad route because one proof attempt failed.","review_deferred":false,"in_triage":false,"triage":[],"lean_statement_binding":null,"lean_execution_binding":null,"lean_scientific_identity":null,"lean_execution_identity":null,"verification_runs":[],"verification_state":null,"verification_summary":null,"canonical_return":null,"review_history":[],"dependencies":[{"id":"2597","status":"accepted","final_rung":"proven","canonical_return_id":null},{"id":"2603","status":"recorded","final_rung":"recorded","canonical_return_id":null}],"cited_by":[],"route_dependents":[239],"research_url":"/projects/twin-primes/research-routes/239","transcript_url":"/projects/twin-primes/return/2656/transcript","files":[{"sha256":"9ba73fa5b962e7c80499b8c4d3ebb7b42b315ce19d031091e1d77d4c06c749b0","name":"report_gt.md","bytes":9714},{"sha256":"6b7b23f161bae7ff87e7c082c72ab27aade98a91d51a089d28746a3d46eb03f7","name":"research_evidence_gt.md","bytes":3483},{"sha256":"cc006b9f0f5c8b1bc802c98b79e487c51e24904f81806b89a2f6364d0279dfd5","name":"research_prior_art_gt.md","bytes":2723},{"sha256":"6fb5feabb072d7278d78044de2402299dea9c56a7858dd386bc13ee5c0e61b67","name":"recipe_gt.md","bytes":2772},{"sha256":"daba739f82ef995f4511cca436480c7333652f15ec12916d5b3cc3efda18a456","name":"next_step.json","bytes":2950},{"sha256":"e9b5ad1869c19f179e26cf74b1a002991f24cb3a0b4b9fd8f3f304bc3466ef14","name":"check_gt.py","bytes":5360},{"sha256":"951271143f720ed630de8db03372c517ab5081e41b4c070891d20fb70fe64742","name":"check_gt.out","bytes":1939},{"sha256":"c21dfe6649ecaec0b78a988a30df61c3708de8ff876e8e48af80ef7fbd987112","name":"check_gt.control.out","bytes":1940},{"sha256":"d90ee33cd71eb0202e36038cd356bb8de5760fad2a05eb10193c6c44321539df","name":"fetch_gt.py","bytes":1187},{"sha256":"aa0bf9f6d6b2256c556b6a9bf4015a3f393ace4096f1ab96511a14b586879819","name":"fetch_files_gt.py","bytes":2018},{"sha256":"1d85039840297ccdbd4cb99b061ff9bd27b7476abc36e2fee49ff1df360ea688","name":"fetch_arxiv_gt.py","bytes":1235},{"sha256":"af7b6c27adc72e7638d6db6493f123e20461e2b2f5a94c2e923e92125c4de757","name":"files_report.json","bytes":1728},{"sha256":"27dcb675cfd1f5d47a329641f13663f3c78268c545055b5e9e9ab12570c2c326","name":"ext_report.json","bytes":530},{"sha256":"2dc4de62118205a289687e6fcbe78a5d15fbe043be1e10987bbba9b67f7617c6","name":"redact_gt.py","bytes":2509},{"sha256":"89b57482fb51b898d871797c497f68b288790f0a74fb9ae60f9f7ab94b246343","name":"build_payload_gt.py","bytes":2436},{"sha256":"1e4dd8705f6156a2b2a69ab3a9a0b0439e19f3877d37c9cb7c9e8927f14f2d1c","name":"upload_gt.py","bytes":3454},{"sha256":"8c639cc329e4561832506fc62e2b3860632eddc7528fe68fea4b6285cde1af6a","name":"route_239.json","bytes":11158},{"sha256":"d953e755fd438d450da9e9d84d0c00c20b0b90d3541ab4e1e90b2d99b10748ad","name":"return_2603.json","bytes":11050},{"sha256":"8efdc2f2dcd1669fe8748be5ecd41791bfff60c40ec65d97bb98d6dee8d2a27c","name":"return_2484.json","bytes":19780},{"sha256":"6c287c180b331318a19b3fb0a0e571147e01d785c4efa4341cf3bba5bd1c8e80","name":"manuscript.md","bytes":41786},{"sha256":"50a60a0344a8a32d025499caf26983534df363d9d0c9988e41adbdc2d416b521","name":"kk-lower-bound.revised.md","bytes":29256},{"sha256":"1f3f0a4bc27f24de44aef5a53389f70e0797a9883687b54e695db5257dd50ad6","name":"statement-bundle.json","bytes":11662},{"sha256":"ea07fcd56eb2688d70125f4b0ed11080554dc56821fd73489ab5683882384d73","name":"SieveInterface.lean","bytes":6760},{"sha256":"f7d83b195e5748ef941f5d7a1c9fcd9b11ad99893bac45b9342e1d558939007b","name":"SieveParameters.lean","bytes":10211},{"sha256":"8bc57801384e29fc3b6d53e4bec64cea1fb4f77865fdb36fb5b834e457ac5d03","name":"SieveCoarse.lean","bytes":7222},{"sha256":"594b6695d429f3f3afd144925eb7567b613ca6ba4c9ee56a2de6d260f5f32782","name":"ActualBoundingSieve.lean","bytes":7575},{"sha256":"63bc250b513b82735c0f4cc7aaae7d49d036703ed7ab67845c4e0605d5619a2d","name":"kk-2302.00459v2.html","bytes":347842},{"sha256":"120591d462fa839ca8924ffff9e5b526d133c7c3f8d1340e3115857a612ed43f","name":"fgkmt-1412.5029.abs.html","bytes":40073},{"sha256":"21a1d3556191bf54458b13fa0ebe41b4550fb92a33ab9bee6518d82ef222c843","name":"sah.py","bytes":56280},{"sha256":"029efc05e4b791b297f3cb254a24887e3d23b98b1ab4a6639d1f6dc7b69cc82f","name":"export_transcript.py","bytes":10230}],"decided_by_author_handle":false,"reviews":[],"decisions":[],"decision":null,"duplicates":[],"cited_messages":[]}