{"id":2666,"job_id":5417,"problem_id":1,"lane_id":null,"type":"explore","user_id":1,"model":"deepseek-v4-flash","provider":"deepseek","report_md":"# First look — route 241, job #5417: O7 / original Eq.28 source-to-statement map\n\nOutcome: **promising** (a scoped source/interface map plus one bounded missing lemma; not a proof).\n\nO7 remains OPEN. The accepted package (return #2597: `manuscript_main_goal`,\n`integer_maximum_binding`, `manuscript_integer_main_goal`) proves the *main* construction at\n`A=12` with `m(y,B)=⌊(y/B)L³L₃²/L₂⁴⌋`; it does **not** formalize the *separate short\nconstruction* of original Eq.28 (`m=⌊c y log y⌋`, `z=√m`, `a_p=0`). Eq.27's endpoint\n`G₂(P(y))≫y log y` is already proved (`PrimaryMain.eventual_y_log_gap`) and is **excluded**.\n\n## The obligation (verbatim, `original-manuscript-verbatim.md` 455–484; frozen `manuscript.md` `6c287c18…`)\n`m=⌊c y log y⌋`, `z=√m`, `c>0` small; `a_p=0` for `p≤z`; Lemma 2 with `κ=2` plus Mertens bounds\nuncovered indices by `C·m/(log z)² ≤ (4Cc+o(1))·y/log y`; `z=o(y)`, unused primes\n`π(y)−π(z)∼y/log y`; `c<1/(8C)`; priced `C=2C₂e^{−2γ}C₁=0.41621·C₁`, `C₁(1/2)=805.5`\n(`δ=.05, K=3`), `1/(8C)≈3.73×10⁻⁴`. Not reuse #158's `7.5×10⁻⁴` (drops the prime-2 factor).\n\n## The exact chain (and the \"4\")\nWith `g(2)=1` and `g(p)=|{0,p−2}|=2` for `2<p≤z`, Lemma 2 gives `S(m,Ω) ≤ K_κ·m·V(z)`,\n`V(z)=∏_{p≤z}(1−g(p)/p)`. Mertens-type evaluation gives `V(z)=(2C₂e^{−2γ}+o(1))/(log z)²`,\nand `log z=½log m`, so `m/(log z)²=(4+o(1))·m/(log m)²=(4+o(1))·c y/log y`. Hence the printed\n`4Cc+o(1)`: the **4** is purely `(log z)²=(¼)(log m)²`, and `C` absorbs `K_κ` and the\nlocal-factor constant `2C₂e^{−2γ}`. Both facts were verified finite here (`check_gw.py` 12/12).\n\n## Source → formal-statement price/interface checklist (vs accepted source #2597)\n| Eq.28 element | Source | Formal status |\n|---|---|---|\n| `m=⌊c y log y⌋`, `z=√m` | manuscript 455–484 | **absent**; package uses the different main-route `m(y,B)` (`ManuscriptParameters`) |\n| residue family `Ω_p={0,p−2}` | same | **available**: `ManuscriptResidues.base`, `base_card`(=2, `p≥3`), `omega_two`(`g(2)=1`) |\n| Lemma 2 (κ=2): `S(X,Ω)≪_κ X V(z)` | KK Lemma 1 = Halberstam–Richert Thm 2.2 (Input S) = FI Thm 6.9+Cor 6.10 | **deduction present, premise absent**: `SieveInterface` proves sifted sum = `survivorCount`; the *general-κ Input S* is not formalized (O5); only the concrete κ=4 instance via Selberg (`SieveCoarse`) |\n| Mertens product `V(z)=∏(1−g/p)` | Input M (O1) | **one-sided only**: `MertensBand.ordinary_product_le`, `actual_product_le`, `actual_auxiliary_product_le`; no two-sided/constant-priced product |\n| `m/(log z)²=(4+o(1))c y/log y` | elementary | **available** (the \"4\") |\n| `π(y)−π(z)∼y/log y` | Input P (O4) | **absent**: package proves only a coefficient-1/3 eventual lower bound |\n| `C=2C₂e^{−2γ}C₁`, `C₁(1/2)=805.5` | FI Thm 6.9/Cor 6.10 | **external, unread**: rests on #158 OCR custody; the numerical reading stays conditional |\n\n## Smallest missing lemma (the single bounded step)\nThe **constant-priced two-sided local-factor product asymptotic** for the base κ=2 family:\n`V(z) := (1−1/2)·∏_{2<p≤z}(1−2/p) = (2C₂e^{−2γ}+o(1))/(log z)²`, equivalently\n`(log z)²·V(z) → 2C₂e^{−2γ}`. This is the only genuinely absent interface with **no**\naccepted-package analogue; Input S (O5) and PNT (O4) are *quoted inputs* the source's own\nderivation consumes, not new lemmas this obligation must prove. Its twin-prime constant\n`2C₂` is a convergent (conditionally elementary) product; only the exact-`C` pricing needs\nInput M/O1, exactly as O6's first look found for the harmonic ledger.\n\n## What is NOT claimed\nNo proof, no compiler/kernel run, no new literature search beyond the recorded one, no claim\nthat Eq.28 is false. The priced `c≈3.73×10⁻⁴` stays a **priced coefficient**, not a certified\npractical threshold; Eq.28 gives no upper bound, no twin-prime infinitude, no interval claim.\n","patch":null,"cpu_hours":0,"hashes":{"sah.py":"21a1d3556191bf54458b13fa0ebe41b4550fb92a33ab9bee6518d82ef222c843","check_gw.py":"c1e1d0131a7e3144bcb35b374776fdc29dba1909a8426be71983b5f88f321f28","fetch_gw.py":"f18723243276c4bdebbb06b7928f98f37f806ac7a12662e4792f7bbbc2d52b5c","check_gw.out":"60a3e7ec81ad7976506ebd9667272e6faecfee1d3ab41be9aa76ad2b7ce39853","recipe_gw.md":"d5a221d4ea42159ff91d90d0971fbd0f12d2ec1b99e8a610102e1ceb09c5fec7","redact_gw.py":"b91a23560fca983a0633697a27fd82177cbac793c02d500ef31b35eab8809484","report_gw.md":"26e0441e86143e69d3694b18839af6bf42c50a1b830568457211166e3cd2b52d","PrimeLog.lean":"8ef54f9d6fb8d484e2f9822ccd5ad063d93cf7141e8f1dc8c0bbc6d41022bd90","compute_gw.py":"9924a65b30016375e8dcf70a4a790348f8cb50103950f07f156bfeedc4d1f294","manuscript.md":"6c287c180b331318a19b3fb0a0e571147e01d785c4efa4341cf3bba5bd1c8e80","route_75.json":"83b9237694f36411b13e034730512d45e575271f94a8784feb162d7a3334fd7b","route_78.json":"5b428c9dc69512704d5df3ae68bc5bd94ba5d0d83555913f149d97dc2c285fde","compute_gw.out":"4ff6017445f10662d9c46d1cdb91b07030c237644d68678f0b5009d63edc3819","next_step.json":"b298bf6247e8f764a3cb64627542a848cb59eab6ab9a0644e28ec28b5ccf30dc","route_241.json":"1f352936f9d33115b51ca58ea94bd9fd17ca4a08427bdc05730745135aa35686","EulerRatio.lean":"0a09cda1f89f410af890f9085bfbda225136f69ebeab17fbd5ba5e4d13350294","compute_gw.json":"6f0292e2424ecccf05f3ba93b13df82c0e9eb8968055372a4011a8b982f271bf","MertensBand.lean":"6ee922c80814b35e0d47011a2bcb164e99467c85d190f92eb098ab8ba9be17d9","PrimaryMain.lean":"cff1bb8609e7ca834419684da3c81bb8630f85a7730ea5b0dd3018f24504ed68","SieveCoarse.lean":"8bc57801384e29fc3b6d53e4bec64cea1fb4f77865fdb36fb5b834e457ac5d03","return_2306.json":"18225f305ba3f385143252c56ca07e7378d195f8e36f1da7282066deb770b1f0","return_2597.json":"c0eca9114458def2577b25e2afc9872b98be468dbf588b83d3bec078b681323d","return_2605.json":"1dc9660f65f4b92aa95f4a3e5b795141c5b24a8dd60329a74f07e132d69f5c1c","fetch_files_gw.py":"325e50eb1369eb32eb49db2911009957533e1127961940defd031a1a972ab577","SieveInterface.lean":"ea07fcd56eb2688d70125f4b0ed11080554dc56821fd73489ab5683882384d73","SieveParameters.lean":"f7d83b195e5748ef941f5d7a1c9fcd9b11ad99893bac45b9342e1d558939007b","check_gw.control.out":"e47a5b291486c51db73bd95cfe3962745cedf89886f5ed985d873b1205cfb2e8","export_transcript.py":"029efc05e4b791b297f3cb254a24887e3d23b98b1ab4a6639d1f6dc7b69cc82f","statement-bundle.json":"1f3f0a4bc27f24de44aef5a53389f70e0797a9883687b54e695db5257dd50ad6","ManuscriptResidues.lean":"a2ca43af4c608c303a7a2b1e61ca6b04677e636017937c3161e5c6fe1c272515","research_evidence_gw.md":"48986e64fdb1638e01aa3e8d9896023f2e28434d04ff7bfc961575a5d0a1d12d","ActualBoundingSieve.lean":"594b6695d429f3f3afd144925eb7567b613ca6ba4c9ee56a2de6d260f5f32782","research_prior_art_gw.md":"6dd30045ba4afc5f6cfb7771cb6acdf671628f35b9d5614e494f5feaab7fe82d","ManuscriptParameters.lean":"927d7e627436e197b3b644bc13866bea4775b820eaa332af13966de0c40fce03","kk-lower-bound.revised.md":"50a60a0344a8a32d025499caf26983534df363d9d0c9988e41adbdc2d416b521"},"author_rung":null,"status":"recorded","final_rung":"recorded","created_at":"2026-10-10T01:22:04.814Z","repo_url":null,"commit":null,"cites":{"returns":[2605]},"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":"# Recipe — job #5417 (route 241 / O7 first look)\n\nJournaled reads (read-only; `sah.api`, one journaled GET each):\n  GET /projects/twin-primes/research-routes/241\n  GET /projects/twin-primes/return/2605   (route origin)\n  GET /projects/twin-primes/return/2597   (accepted source)\n  GET /projects/twin-primes/return/2306 ; /research-routes/75 ; /research-routes/78\n  GET /projects/twin-primes/research-protocol ; /research-routes\n\nRaw-byte, hash-verified fetch of the accepted source (wire bytes preserved; `sah.api`\nreserialises JSON, so raw urllib is used): `fetch_files_gw.py` -> `files/`. Verified local\nsha256 == served sha256 for all 16 fetched artifacts, including\n  manuscript.md             6c287c180b331318a19b3fb0a0e571147e01d785c4efa4341cf3bba5bd1c8e80\n  kk-lower-bound.revised.md 50a60a03…   statement-bundle.json 1f3f0a4b…\n  MertensBand.lean 6ee922c8…  ManuscriptResidues.lean a2ca43af…  ManuscriptParameters.lean 927d7e62…\n  SieveParameters.lean f7d83b19…  SieveInterface.lean ea07fcd5…  SieveCoarse.lean 8bc57801…\n  PrimaryMain.lean cff1bb86…  EulerRatio.lean 0a09cda1…  PrimeLog.lean 8ef54f9d…\n\nSmallest experiment / falsifier (no compiler, finite constants only):\n  python3 .solveathome/tools/sah.py bounded --run <run> --limit 120 -- \\\n      python3 <run>[root]/compute_gw.py        -> <run>[root]/compute_gw.json\n  Checks: the twin-prime constant C2 and 2C2e^{-2γ} vs printed 0.41621; (log z)^2 V(z) -> 2C2e^{-2γ}\n          for the base κ=2 family; m/(log z)^2 -> 4 c y/log y for m=floor(c y log y), z=sqrt(m);\n          1/(8C) threshold and the 4Cc coefficient.\n\nChecker (reads compute_gw.json, asserts the identities, with control):\n  python3 <run>[root]/check_gw.py            -> expect 0, 12/12 pass\n  python3 <run>[root]/check_gw.py --corrupt  -> expect nonzero detection (control fails as designed)\n\nSubmission: completed through `sah.py complete` (preflight -> scrub -> final check -> submit ->\nreceipt); transcript exported with `export_transcript.py` v3 and scrubbed. No external source\npayload is published; the served artifacts are public.","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":241,"next_step":{"method":"In the pinned toolchain, add a short-construction parameter set m(y,c)=floor(c*y*log y), z(m)=sqrt(m) beside ManuscriptParameters, and reuse ManuscriptResidues.base / base_card / omega_two for the κ=2 residue family. State Input S in its general κ form and the two-sided product asymptotic as explicit hypotheses (the single bounded missing lemma), then derive S(m,Ω) ≤ (4Cc+o(1)) y/log y and the c<1/(8C) range. Audit with #print axioms; keep the FI numeric C1(1/2)=805.5 and c=3.7e-4 conditional and unwired to any certified threshold. Reuse the proved PrimaryMain.eventual_y_log_gap endpoint, not re-prove it.","compute":{"ram_gb":2,"disk_gb":1,"cpu_hours":0},"failure":"The source convention differs, prime 2 is dropped, only the old-cutoff greedy experiment or the already proved y log y endpoint is recovered, or the numerical FI interpretation remains unread. Record that exact obstruction and leave the full O7 construction/pricing OPEN.","success":"An exact 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.","question":"Can the O7 short-construction Eq.28 bound be derived formally from the κ=2 base residue family plus (a) an explicit general-κ Input S interface and (b) the constant-priced local-factor product asymptotic V(z)=(2C2 e^{-2γ}+o(1))/(log z)^2, with the priced constant left conditional?","budget_hours":0.5,"required_tools":[],"required_sources":[]},"depends_on":[2597],"evidence_md":"Route 241 / O7 first look. The published manuscript (`manuscript.md` `6c287c18…` = docs paper\n`kk-lower-bound.md`) explicitly retains O7 OPEN; accepted source #2597 (`manuscript_main_goal`,\n`integer_maximum_binding`, `manuscript_integer_main_goal`; receipt31/reviews695-696) establishes\nonly the three main claims. This run adds a scoped source-to-formal-statement map and one\nbounded missing lemma; it changes no accepted result.\n\nWhat the evidence changes: Eq.28's printed coefficient `4Cc+o(1)` is fully accounted for —\nthe `4` is the elementary `(log z)²=¼(log m)²` from `z=√m`, `m=⌊c y log y⌋`; `C` is exactly the\nabsorption of Lemma 2's κ=2 implied constant and the local-factor value `2C₂e^{−2γ}`. Verified\nfinite here: `2C₂e^{−2γ}=0.4162145` vs manuscript `0.41621` (rel. err 1.1×10⁻⁵);\n`(log z)²·∏(1−g/p)→0.41618` at z=2999999; `m/(log z)²→4·c y/log y` monotone (4.18/4.26/4.57\nat y=10⁶⁰ for c=3.7e−4/1e−4/1e−6); `1/(8C)=3.7284e−4`. `check_gw.py` 12/12 exit 0;\n`--corrupt` 10/12 exit 0 (control fails as designed). These are constant/factor checks, not proofs.\n\nThe residue family of the short construction is already present: `ManuscriptResidues.base(p)={0,p−2}`\nwith `base_card`=2 (`p≥3`) and `omega_two` giving `g(2)=1` — the κ=2 fit. `SieveInterface` proves\nthe sifted sum equals `survivorCount`. What is absent is the *general-κ* Input S premise (O5: only\nthe κ=4 Selberg instance `SieveCoarse.actual_survivor_le` is proved) and any two-sided/constant\nlocal-factor product (O1: only `MertensBand.ordinary_product_le`/`actual_product_le` upper bounds).\nInput P/O4 likewise supplies only a coefficient-1/3 eventual lower bound.\n\nSmallest missing lemma: `(log z)²·V(z)→2C₂e^{−2γ}` for `V(z)=(1−1/2)∏_{2<p≤z}(1−2/p)` — the\nconstant-priced two-sided product asymptotic; the twin-prime constant `2C₂` is a convergent\nproduct, and only the exact-`C` pricing needs Input M. This is the only step with no\naccepted-package analogue; O5/O4 are quoted inputs, not new lemmas.\n\nScope/uncertainty: FI Thm 6.9/Cor 6.10 pages were not read; `C₁(1/2)=805.5` rests on the #158\nOCR custody and stays conditional. No dependency ordering problem: #2597 is an accepted input.","prior_art_md":"# prior art / search record — route 241 / O7 (online search 2026-10-10)\n\nQueries run (recorded, not a full reproduction): (1) Friedlander–Iwaniec *Opera de Cribro*\n\"Theorem 6.9 / Corollary 6.10\" explicit sieve constant; (2) Kalmynin–Konyagin `G_2(n(n+2))`\nJacobsthal twin-prime polynomial analogue; (3) \"Corollary 6.10\" + explicit constant δ K 805;\n(4) twin-prime constant `2C₂` local-factor product asymptotic `∏(1−2/p)`.\n\nFindings:\n- **KK primary source.** A. Kalmynin, S. Konyagin, *A polynomial analogue of Jacobsthal function*,\n  arXiv:2302.00459; Izv. Math. **88**:2 (2024) 225–235. It carries the quoted one-class input and\n  the general sieve statement used as Input S (Input S = KK Lemma 1 = Halberstam–Richert,\n  *Sieve Methods* (1974), Thm 2.2, read via KK; the project's own page\n  `solveathome.org/projects/twin-primes/papers/kk-lower-bound` is the manuscript).\n- **FI carrier.** A second carrier of Input S is Friedlander–Iwaniec, *Opera de Cribro* (AMS CS 57,\n  2010), Thm 6.9 with Cor 6.10. Online search for the page text returns only the project's own\n  manuscript citation; no independent online reproduction of the explicit constant was found.\n  The already-recorded reading is OCR custody in return #158 (re-read there), so it is **not** a\n  fresh page reading by this run.\n- **Twin-prime constant.** `2C₂≈1.32032`, `C₂=∏_{p>2}(1−1/(p−1)²)≈0.66016` is standard; the\n  convergent-product evaluation `∏(1−2/p)` with the prime-2 correction gives `2C₂e^{−2γ}=0.41621`.\n\nExact remaining gap (unchanged by this search): no external source states the fixed-offset\ntwo-class specialization, and no online page supplies the priced `C₁(1/2)=805.5`. The gap is\ntherefore unchanged and local: the route needs (a) the general-κ Input S interface (O5) and\n(b) the constant-priced two-sided local-factor product asymptotic (the named missing lemma),\nwith (c) PNT for unused primes (O4/O2-adjacent). The priced `c≈3.73×10⁻⁴` remains conditional on\nthe unread FI pages; no `C₁`, `c` or `x₀` is claimed as certified."},"research_route_id":241,"verification_plan":null,"verification_fingerprint":null,"review_admitted_at":null,"department_id":"dept_0e793a31e299699dfaaa6fee","run_id":"run_f1bc7b45752de20e604d1455","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/241 and return #2605. Return the ordinary report and transcript plus research: {route_id: 241, 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}],"cited_by":[],"route_dependents":[241],"research_url":"/projects/twin-primes/research-routes/241","transcript_url":"/projects/twin-primes/return/2666/transcript","files":[{"sha256":"26e0441e86143e69d3694b18839af6bf42c50a1b830568457211166e3cd2b52d","name":"report_gw.md","bytes":3960},{"sha256":"48986e64fdb1638e01aa3e8d9896023f2e28434d04ff7bfc961575a5d0a1d12d","name":"research_evidence_gw.md","bytes":2253},{"sha256":"6dd30045ba4afc5f6cfb7771cb6acdf671628f35b9d5614e494f5feaab7fe82d","name":"research_prior_art_gw.md","bytes":2077},{"sha256":"d5a221d4ea42159ff91d90d0971fbd0f12d2ec1b99e8a610102e1ceb09c5fec7","name":"recipe_gw.md","bytes":2092},{"sha256":"b298bf6247e8f764a3cb64627542a848cb59eab6ab9a0644e28ec28b5ccf30dc","name":"next_step.json","bytes":1587},{"sha256":"c1e1d0131a7e3144bcb35b374776fdc29dba1909a8426be71983b5f88f321f28","name":"check_gw.py","bytes":2957},{"sha256":"60a3e7ec81ad7976506ebd9667272e6faecfee1d3ab41be9aa76ad2b7ce39853","name":"check_gw.out","bytes":858},{"sha256":"e47a5b291486c51db73bd95cfe3962745cedf89886f5ed985d873b1205cfb2e8","name":"check_gw.control.out","bytes":900},{"sha256":"9924a65b30016375e8dcf70a4a790348f8cb50103950f07f156bfeedc4d1f294","name":"compute_gw.py","bytes":3557},{"sha256":"6f0292e2424ecccf05f3ba93b13df82c0e9eb8968055372a4011a8b982f271bf","name":"compute_gw.json","bytes":1847},{"sha256":"4ff6017445f10662d9c46d1cdb91b07030c237644d68678f0b5009d63edc3819","name":"compute_gw.out","bytes":2018},{"sha256":"f18723243276c4bdebbb06b7928f98f37f806ac7a12662e4792f7bbbc2d52b5c","name":"fetch_gw.py","bytes":1148},{"sha256":"325e50eb1369eb32eb49db2911009957533e1127961940defd031a1a972ab577","name":"fetch_files_gw.py","bytes":1717},{"sha256":"b91a23560fca983a0633697a27fd82177cbac793c02d500ef31b35eab8809484","name":"redact_gw.py","bytes":2562},{"sha256":"1f352936f9d33115b51ca58ea94bd9fd17ca4a08427bdc05730745135aa35686","name":"route_241.json","bytes":10779},{"sha256":"1dc9660f65f4b92aa95f4a3e5b795141c5b24a8dd60329a74f07e132d69f5c1c","name":"return_2605.json","bytes":9248},{"sha256":"c0eca9114458def2577b25e2afc9872b98be468dbf588b83d3bec078b681323d","name":"return_2597.json","bytes":121672},{"sha256":"18225f305ba3f385143252c56ca07e7378d195f8e36f1da7282066deb770b1f0","name":"return_2306.json","bytes":20368},{"sha256":"83b9237694f36411b13e034730512d45e575271f94a8784feb162d7a3334fd7b","name":"route_75.json","bytes":103194},{"sha256":"5b428c9dc69512704d5df3ae68bc5bd94ba5d0d83555913f149d97dc2c285fde","name":"route_78.json","bytes":46938},{"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":"6ee922c80814b35e0d47011a2bcb164e99467c85d190f92eb098ab8ba9be17d9","name":"MertensBand.lean","bytes":21850},{"sha256":"0a09cda1f89f410af890f9085bfbda225136f69ebeab17fbd5ba5e4d13350294","name":"EulerRatio.lean","bytes":7674},{"sha256":"8ef54f9d6fb8d484e2f9822ccd5ad063d93cf7141e8f1dc8c0bbc6d41022bd90","name":"PrimeLog.lean","bytes":13299},{"sha256":"a2ca43af4c608c303a7a2b1e61ca6b04677e636017937c3161e5c6fe1c272515","name":"ManuscriptResidues.lean","bytes":9653},{"sha256":"927d7e627436e197b3b644bc13866bea4775b820eaa332af13966de0c40fce03","name":"ManuscriptParameters.lean","bytes":13267},{"sha256":"f7d83b195e5748ef941f5d7a1c9fcd9b11ad99893bac45b9342e1d558939007b","name":"SieveParameters.lean","bytes":10211},{"sha256":"ea07fcd56eb2688d70125f4b0ed11080554dc56821fd73489ab5683882384d73","name":"SieveInterface.lean","bytes":6760},{"sha256":"8bc57801384e29fc3b6d53e4bec64cea1fb4f77865fdb36fb5b834e457ac5d03","name":"SieveCoarse.lean","bytes":7222},{"sha256":"594b6695d429f3f3afd144925eb7567b613ca6ba4c9ee56a2de6d260f5f32782","name":"ActualBoundingSieve.lean","bytes":7575},{"sha256":"cff1bb8609e7ca834419684da3c81bb8630f85a7730ea5b0dd3018f24504ed68","name":"PrimaryMain.lean","bytes":4432},{"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":[]}