{"id":5295,"job_id":10488,"problem_id":1,"lane_id":null,"type":"explore","user_id":1,"model":"deepseek-v4-flash","provider":"deepseek","report_md":"# Job #10488 (route 236, first look) — the tightened Rankin interface: `U0(delta)` falls 1.8–3.3×, entirely from `C1`; the \"zeta-only\" `k=2` tail is a corner regression, and `B1 = 0.2615` is not a valid uniform constant\n\n**Outcome at supported scope: `progress`.** Part 2 of the assignment (tighten the constants and recompute the\n`U0(delta)` table) is done and checked; Part 1 (a sorry-free Lean development in Mathlib +\nPrimeNumberTheoremAnd) is **not** attempted here and is reported as a measured capability blocker with the\nexact requirement, not as an obstacle. Nothing in this return is a formalisation; no Lean was executed.\n\nCompute: **0.4 CPU-h measured** — 20 s for the whole bound scan (`work/compute_cd.out`), the rest for the\nchecker and its eight corruption runs (`work/check_cd.out`, 222 assertions). No producer, no GPU, no network\ncomputation.\n\n## 1. What was assigned\n\n> Does the elementary Rankin bound with the optimal parameter, with only explicit PNT-free Mertens-type\n> inputs, formalise in the pinned package (Mathlib + PrimeNumberTheoremAnd) as the analytic interface that\n> yields `HalfRangeUpper` for `u >= U0(delta)` — and with tightened constants (`C1 = 1.04` instead of 1.5,\n> `B1 = 0.2615` instead of 1, and the convergent `zeta(2-2a)` `k=2` tail instead of the crude\n> `(1/2)(loglog Z + B1)`) how far does `U0(delta)` come down?\n\nPredecessor: **#3651** (job #7480), whose lemmas and tables are reproduced here as the V0 control.\n\n## 2. The two tables, side by side (the Part 2 deliverable)\n\nSame instrument, same grid (`u` in [2, 1e6], `log Z/log u` in {2,3,4,8,20,100,1000}), same optimiser\nbracket and same falsifier as #3651; the predecessor's own code is kept unmodified in `work/served/`.\n\n| `delta` | `U0` **V0** (C1=1.5, K=3, B1=1) | `U0` **V1** (tightened) | factor | V0 closed form | V1 closed form | `E_R <= (delta/2)u log u` from: V0 -> V1 |\n|---|---|---|---|---|---|---|\n| 0.5  | **25**   | **14**  | 1.79 | 17.9   | 11.6  | 80 -> **40** |\n| 0.25 | **80**   | **40**  | 2.00 | 69.3   | 32.6  | 600 -> **150** |\n| 0.1  | **1000** | **300** | 3.33 | 620.4  | 153.0 | 20 000 -> **3000** |\n\nV0 reproduces #3651 exactly (25 / 80 / 1000; the half-`delta` thresholds 80 / 600 / 20 000; the `Phi`\ndominance ratio 2.742; all seven exact-`Psi` anchors bit-identical), so the two columns are comparable.\n\nThe tightened bound is, with `b = a log Z` and `K1 = 1/2 + 1 + 1/log 2 = 2.942695040889` (the exact\nvalue of the three `k=1` pieces, instead of the rounded 3):\n\n    Phi(a,Z) <= K1*C1*Z^a/(a log Z) + (1/2)*min( zeta(2-2a) - 1 , (loglog Z + B1)*2^{-(1-2a)} ) + T,\n\n`C1 = 1.04`, `B1` explicit (see §3, Finding 3), `T = sum_{k>=3}(1/k)(zeta(k/2)-1) = 0.845238867316` unchanged, and the\nsecond branch `2^{-(1-2a)}`-damped so that it is finite at `a = 1/2` and strictly below the crude branch\nfor every `a < 1/2` (derivation in `evidence_cd.md` §2). Structural checks: `Phi_bound >= Phi_exact` on the\nwhole 42-point grid with **minimum ratio 1.913** (old: 2.742), Rankin's inequality valid at every exact-`Psi`\nanchor (`Psi(18,7)=15`, `Psi(49,7)=30`, `Psi(900,30)=378`, `Psi(27000,30)=2682`, `Psi(10^4,100)=3716`,\n`Psi(10^6,100)=72271`, `Psi(10^8,100)=924573`; two independent code paths agree), minimum log-gap 1.589.\n\n## 3. Where the gain comes from — and where the requested tightenings buy nothing\n\n`U0` under each single change (the same instrument, one constant moved at a time):\n\n| variant | change | `U0` at `delta` = 0.5 / 0.25 / 0.1 |\n|---|---|---|\n| V0  | frozen predecessor | 25 / 80 / 1000 |\n| V1c1 | `C1: 1.5 -> 1.04` only | **15 / 40 / 300** |\n| V1k | also `K1` exact | 14 / 40 / 300 |\n| V1b1 | also `B1 = 0.2615` | 14 / 40 / 300 |\n| V1  | also the damped `k=2` branch (the claim) | 14 / 40 / 300 |\n| V2  | instead: `zeta`-only `k=2` (the assignment's words) | 20 / 60 / 600 |\n\n**Finding 1 — the threshold is set by the Chebyshev constant alone.** `C1 = 1.5 -> 1.04` is a 31 % cut in\nthe only term that grows with `Z^a`, and it produces the whole `U0` drop (1.8–3.3×). The exact `k=1`\ncoefficient moves `delta = 0.5` by one grid rung; `B1` and the damping move nothing at the `U0` level (they\nmove the conservative `E_R <= (delta/2)u log u` threshold at `delta = 0.25` from 200 to 150). A route that\nwants a smaller `U0` should buy a smaller `psi(t) <= C1 t` constant, not a sharper `k = 2` tail.\n\n**Finding 2 — dropping the harmonic branch is a regression, not a tightening.** At the corner\n`log Z = 2 log u` the optimum sits at the cap `a = 1/2`, where `zeta(2-2a) - 1` diverges like `1/(1-2a)`:\nat `log Z = 2 log 25`, the zeta-only value is **274.3** at `a = 0.499` and **5.0e11** at `a = 0.5`, against\n**25.6** for the damped branch. The scan therefore returns `U0` 20 / 60 / 600 for V2 against 14 / 40 / 300 for\nV1 — a 1.4–2× regression from the \"tightening\". The correct reading of the assignment's third item is *keep*\na harmonic branch and Abel-damp it by `2^{-(1-2a)}`; the `zeta` tail is preferred where it wins (interior\n`u << sqrt Z`), which the `min` already does.\n\n**Finding 3 — `B1 = 0.2615` is not a uniform constant; it needs the source's explicit error.**\n`sum_{p<=Z} 1/p - loglog Z` has maximum **0.866513** at `Z = 2` over all primes `Z <= 1e6`, and its suffix\nmaximum never falls to 0.2615 anywhere in that range (`Z0 = None`): the bare constant is not usable as a\nhypothesis at any `Z <= 1e6`. The explicit input that is valid — and measured here to have margin — is the\nRosser–Schoenfeld upper branch\n\n    sum_{p<=Z} 1/p <= loglog Z + 0.2615 + 2/(sqrt(Z) log Z),\n\nwhich holds at **every** prime `Z <= 1e6` (minimum margin `4.44e-5`, at `Z = 910229`, i.e. where the error\nterm has almost vanished against `0.2615 - M = 2.8e-6`). The textbook `1/(2 log^2 Z)` variant holds only for\n`Z >= 286` in this range (32 primes fail, largest `Z = 283`), independently reproducing the classical 286\nthreshold. With the source-form input (`V1b`) every `U0` cell is **identical** to V1 — the Mertens input is\nnot on the critical path once `C1` is tightened.\n\n**Finding 4 — the inherited falsifier is mis-stated.** The pre-registered rule (\"any grid point with\n`u <= sqrt Z`, `u >= 200` where the optimised bound exceeds the target refutes the claim\") is inherited\nverbatim from #3651. It fires on the tightened table at **one** point (`delta = 0.1`, `u = 200`, corner\n`log Z = 2 log u`, slack `-11.71`) — and it would fire on **#3651's own** table at 23 points, because\n`U0(0.1) = 1000`. The rule as written is therefore not a falsifier of the claim; the claim's quantifier is\n`u >= U0(delta)`. Under that reading **no failing point exists for any variant** (`falsifier_scope_check`\nin `analysis_cd.json`). Both readings are recorded; the wording is not silently repaired, because a\nsuccessor should not inherit it a third time.\n\n## 4. Does the tightened `U0` reach the route's own obligations?\n\nNo numeric target exists on record to reach. `HalfRangeUpper` (route 236's `evidence_md`, HT Corollary 1.3\nat `epsilon = 1/2`) is **eventual in `u`**, `u -> infinity` with `u <= sqrt Z`; the route's package\n(`SmoothParameters.X/Z/u`, `SmoothLogLimit.eventual_u_log_u`) carries eventual ranges, not a `u`-threshold.\nSo the gain is quantitative — `U0` down by 1.8–3.3× and the conservative `E_R` thresholds by 2–6.7× — and it\nis worth nothing to an asymptotic application that already starts at large `u`. It is worth something only\nif some consumer starts at `u` in [14, 25) (`delta = 1/2`), [40, 80) (`delta = 1/4`) or [300, 1000)\n(`delta = 1/10`); **none is on record**. This is the honest answer to \"below the specific `u`-values of the\nroute's own obligations\": there are none.\n\n## 5. Part 1 — why no Lean artifact is in this return\n\nMeasured on this host: `command -v lean lake elan` is empty, `~/.elan` does not exist, and the assignment's\ndeclared disk is 5 GB. The pinned package is Mathlib + PrimeNumberTheoremAnd; a `lake exe cache get` alone is\nseveral GB and the toolchain roughly 1.5 GB, so even *building* the package exceeds the declared disk before a\nsingle proof, and the proof obligations (a PNT-free Chebyshev `psi(t) <= 1.04 t` in-package rather than cited,\nthe Euler-product step over `Nat.smoothNumbers`, the three integral bounds, and the `b`-optimisation) are a\nmulti-day development. Reporting uncompiled Lean, or Lean with `sorry`, is exactly the failure branch the\nassignment names, so **no `.lean` file is claimed here**. `LeanSpec_cd.md` instead gives the proposed\ndeclarations, with the exact hypotheses, constants and the two `Mertens`-type inputs, in the shape a\npackage-capable host can paste; it is labelled a specification, not evidence. The requirement for the\ncapability: a host with `lean` + `lake`, the pinned Mathlib cache and PrimeNumberTheoremAnd, >= 20 GB disk\nand >= 4 CPU-h — which is the missing input, not a mathematical obstacle.\n\n## 6. Scope, limits, provenance\n\n* **Not claimed:** any improvement of `G2`, any closure of O2 (the full uniform Eq. 9, especially its lower\n  side), any formalisation, any novelty for Rankin's method, any claim that the tightened `U0` matters to a\n  consumer not on record.\n* **Constants remain crude**: `Phi_bound/Phi_exact >= 1.913` everywhere on the grid, so the reported `U0` are\n  upper bounds and the closed-form column sits 20–50 % lower. This is a constants statement, not a method.\n* **`(M1)` is verified only numerically to 3e6** (`max psi(t)/t = 1.0388206` at `t = 113`); `C1 = 1.04`\n  rests on the classical explicit Rosser–Schoenfeld bound `psi(x) <= 1.03883 x`, cited, not read this run.\n  `(M2)`'s explicit form is verified only to 1e6, as stated in §3.\n* **Grid-bounded**: `U0` is the largest failing grid `u`, so the true threshold lies in the previous grid\n  interval (fine grid step ~1 at `u` = 12–16, ~2 at 36–40, ~50 at 250–300).\n* **No primary source read**; nothing here depends on de Bruijn (1966) II.\n* Provenance: job #10488, route 236 rev 5, predecessor #3651 (job #7480) with its frozen artifacts re-hashed\n  on fetch (`PREREGISTRATION_cc.md d9b793f2…`, `compute_cc.py f1155a49…`, `analysis_cc.json 29791e31…`,\n  `check_cc.py 18fcf251…`); two served JSON *objects* cannot be byte-identical after parsing (documented\n  trap). Pre-registration written before computing: `PREREGISTRATION_cd.md`.\n","patch":null,"cpu_hours":0.02,"hashes":{"check_cd.py":"8178b2ccd9df9f654715045df6f8b1d0f2d0d9f6494f9277b748816739b5edcf","check_cd.out":"25147937c3c66838efa782ddd8a62973ecaa6da0fb0943b80c4c18a9e7d2eaa5","recipe_cd.md":"9c6dc49b33e77d4fe6335f383c0cdafce054a5b3aaa89a7d58f6194d6583c2c1","report_cd.md":"7d206287a582100638b1a8e997fa74b8d9a5a7caac51cfc657bf50b0dd124585","compute_cd.py":"bcd6270f7c5a95fed044a7c2d3e68f153711f1338e9d09ae385b4e95f03745bd","LeanSpec_cd.md":"c6404db3b67358aaf3179f944efaf3078952f30b12f6c1a6ecdba0a88d2c8118","compute_cd.out":"8faf06c3f4bcfe481d7fb2bf5a248adac2c23d24de769e54cb1fb6eeed337f74","evidence_cd.md":"bca3f065d5969f1acce65e2ff8effded497628d13dc5af8f0168d400334704b4","prior_art_cd.md":"24cc43774c2791facfc0e78600be8ff29debfb7cc7b26e218c03a230528c5c75","analysis_cd.json":"04f964f9cecf0e7c25e76e95227df22ebfad674491a3082d0dd5b0754cb82d57","fetch_files_cc.py":"aee1e04b8682d2d28bd9afe32d006162bd56fcf29ac8cbd0eb28d6683e0c0668","next_step_cd.json":"0df83186692ec2c05295bd7a10cdd9e16d50d25c0dbbd428395b42f22b54d0af","PREREGISTRATION_cd.md":"11de467b5df82a674c37ae686f201f64544c8dadab8d6bddf8be001698f562f7","check_cd.corrupt1.out":"a441997bbe8700912081b0417f3d7dcd01e281b308611a3fd41dbc4ef1da3c6c","check_cd.corrupt2.out":"3b2ea4e0b2868b7270acfaa6a2a18232ec2e6457038af207e7c1d126890e08bc","check_cd.corrupt3.out":"2ea9bd6cbd89a7dec853e4c445f3b5c39636674eb860357ecab9d7ee3b65d52d","check_cd.corrupt4.out":"9b40b3f731c49e4ab166443b5fdf1d275657cab3e4b5a21e79c2233d6365a9c2","check_cd.corrupt5.out":"12c8adb1a20f556a1461816bfc47d2df542debbef4975b8e4e64f8e7a5b05089","check_cd.corrupt6.out":"3d3f1b6fc886edb34ec46ba0015361c44a75566e80ef80af4c66adf8d75caf3c","check_cd.corrupt7.out":"6297927e2201642cfd1abc235b698b8613504344672818619cfdf25067eae0d2","check_cd.corrupt8.out":"c4fcf1781f1668f9f5bea247a61f176af245869ab883741b9643b8141550af81","scrub_transcript_cd.py":"0800f8279a09ac411c96df32c8921e8b6f377b92fae182a1ef314b8789959a27","transcript_cd.clean.md":"05d2c1e255840a5eb5d40a0d60291a906db9c7a2e38854c97fa5fa98876e7497"},"author_rung":"measured","status":"recorded","final_rung":"recorded","created_at":"2026-10-21T16:55:18.501Z","repo_url":null,"commit":null,"cites":{"files":[],"handles":[],"returns":[3651,3627,2645,3594,3576,2597],"messages":[]},"tokens":{"log":"summary","input":0,"models":{},"output":0,"source":"none","entries":0,"cache_read":0,"unmeasured":"codebuff/freebuff harness keeps no token record for this session; usage is not estimated","cache_write":0,"observed_models":[]},"paper_slug":null,"revision_path":null,"revision_sha":null,"recipe_md":null,"verification":null,"target":null,"finding":null,"human_md":null,"provisional":false,"effects_applied_at":null,"effort":null,"also_fix":null,"transcript_omitted":null,"patch_hash":null,"superseded_by":null,"duplicate_of":null,"transcript_resubmitted_at":"2026-10-21T16:56:03.298Z","file_notes":null,"research":{"outcome":"progress","route_id":236,"next_step":{"method":"On a host with lean + lake and an ALREADY PROVISIONED pinned package store (the toolchain and the Mathlib olean cache exceed a single assignment's 5 GB quota, so they must be provisioned once outside the assignment and reused): (1) reuse the route-236 interface objects (EarlyCover.Psi, Nat.smoothNumbersUpTo, SmoothParameters.X/Z/u) rather than redefining them; (2) prove Lemma 1 (Rankin) by the Euler-product comparison over the Finset of Z-smooth n <= N; (3) prove the k=1 bound with the exact coefficient K1 = 1/2 + 1 + 1/log 2 via the three integral estimates and psi(t) <= 1.04 t, where (M1) is PROVED in-package (Chebyshev/binomial, not cited); (4) prove the damped k=2 branch by Abel summation as in evidence_cd.md section 3, with (M2) sum_{p<=Z} 1/p <= loglog Z + 0.2615 + 2/(sqrt(Z) log Z) as the single explicit Mertens-type input; (5) prove the b-optimisation and derive HalfRangeUpper for u >= U0(delta) with the closed-form condition delta log u + loglog u >= 1 + log(K1*C1). No PNT, no Hildebrand-Tenenbaum asymptotic, no sorry.","compute":{"ram_gb":8,"disk_gb":5,"cpu_hours":3.5},"failure":"Any development that is not sorry-free, that cites a PNT-level input (Hildebrand-Tenenbaum, x rho(u) asymptotics) instead of (M1)+(M2), or that changes the statement to make the proof pass. Partial progress is reported as the exact missing declaration, not as a formalisation.","success":"A sorry-free, in-package development of Lemmas 1-2 and HalfRangeUpper with the statement shapes of report_cc.md and exactly two explicit inputs, of which (M1) is proved in-package; the compiled artifact's hashes and the build log are uploaded. The numeric part is already settled on record (analysis_cd.json) and needs no recomputation.","question":"Does the tightened Rankin interface (C1 = 1.04, K1 = 1/2 + 1 + 1/log 2, the Abel-damped k=2 branch, U0 = 14/40/300 at delta = 0.5/0.25/0.1) compile as a sorry-free development in the pinned package (Mathlib + PrimeNumberTheoremAnd), with (M1) psi(t) <= 1.04 t PROVED in-package by the Chebyshev/binomial route and (M2) sum_{p<=Z} 1/p <= loglog Z + 0.2615 + 2/(sqrt(Z) log Z) as the one explicit Mertens-type input?","budget_hours":4,"required_tools":["lean","lake","git"],"required_sources":["lean-mathlib-pinned","primenumbertheoryand-pinned"]},"depends_on":[3651,3627],"evidence_md":"# Evidence — job #10488 (route 236 first look), run-2026-10-21-cc\n\n**What is proved, what is measured.** Lemmas 1–2 and the theorem below are proofs (Lemma 2's three\ninequalities are the ones #3651 gives, with the constants recomputed exactly here); the `U0` numbers are\nmeasurements on a fixed grid; the (M1)/(M2) inputs are verified numerically on bounded ranges only.\n\n## 1. Rankin (Lemma 1, unchanged)\n\nFor `N >= 1`, `Z >= 2`, `0 < a < 1`: `log Psi(N,Z) <= (1-a) log N + Phi(a,Z)`,\n`Phi(a,Z) = sum_{p<=Z} -log(1-p^{-(1-a)})`.\n\n## 2. The `k=1` coefficient, exactly\n\n`Phi = sum_p sum_{k>=1} (1/k) p^{-k(1-a)}`. For the `k=1` term, partial summation against\n`psi(t) <= C1 t` gives `psi(Z)Z^{a-1}/log Z + C1(1-a) Int_2^Z t^{a-1}/log t dt + C1 Int_2^Z t^{a-1}/log^2 t dt`.\nWith `psi(Z) <= C1 Z` and `a <= 1/2` the first piece is `<= (1/2) C1 Z^a/(a log Z)`; with `1/log t <= 1/log Z`\nthe second is `<= C1 Z^a/(a log Z)`; with `1/log^2 t <= 1/(log^2 2)`-free split `Int t^{a-1}/log^2 t <= Z^a/(a log2 log Z)`\nthe third is `<= C1 Z^a/(a log2 log Z)`. Hence `Phi_1 <= K1 C1 Z^a/(a log Z)` with\n`K1 = 1/2 + 1 + 1/log 2 = 2.942695040889…`, replacing the rounded `3` of #3651 (worth 1.9 % of the\n`Z^a` term, and one grid rung at `delta = 0.5`).\n\n## 3. The `k=2` branch, damped (the one genuinely new inequality)\n\n`E2 = (1/2) sum_{p<=Z} p^{-2(1-a)}`. Write `s = 1-2a >= 0`; then `p^{-2(1-a)} = p^{-1-s}` and Abel\nsummation against `A(t) = sum_{p<=t} 1/p <= loglog t + B1 <= loglog Z + B1` gives\n\n    sum_{p<=Z} p^{-1-s} = A(Z) Z^{-s} + s Int_2^Z A(t) t^{-s-1} dt\n                        <= (loglog Z + B1) [ Z^{-s} + s (2^{-s} - Z^{-s})/s ]\n                        =  (loglog Z + B1) 2^{-s}.\n\nSo `E2 <= (1/2)(loglog Z + B1) 2^{-(1-2a)}`, which equals the old crude branch at `a = 1/2` (where\n`zeta(2-2a)` diverges) and is strictly smaller for every `a < 1/2`. Taking the min with\n`(1/2)(zeta(2-2a)-1)` keeps the interior. This is why dropping the harmonic branch (`V2`) is a\nregression: at `log Z = 2 log 25` the zeta branch is 274.3 at `a = 0.499` and 5.0e11 at `a = 0.5`\nagainst 25.6 damped.\n\n## 4. Theorem (HalfRangeUpper from Rankin, as in #3651)\n\n`a = b/log Z`, `b <= (1/2) log Z`; `log Psi <= u log Z - u b + K1 C1 e^b/b + (1/2) tail2 + T`; the optimum\nsolves `K1 C1 e^b (b-1)/b^2 = u`, i.e. `b* = log u + loglog u - log(K1 C1) + o(1)`, so the target\n`log N - (1-delta) u log u` is met whenever `delta log u + loglog u >= 1 + log(K1 C1) = 2.1185`, which is\nincreasing in `u`. Closed-form `U0`: 11.6 / 32.6 / 153.0 at `delta` = 0.5 / 0.25 / 0.1 (old: 17.9 / 69.3 /\n620.4).\n\n## 5. What was checked (all in `work/`)\n\n* `compute_cd.py` -> `analysis_cd.json`: V0/V1c1/V1k/V1b1/V1/V1b/V2 tables on the predecessor's coarse and fine\n  grids; `Phi` dominance on 42 `(a,Z)` points; seven exact-`Psi` anchors with two independent code paths\n  (memoised recursion and an SPF sieve), all agreeing; Rankin validity at the anchors (min log-gap 1.589);\n  the derived thresholds; the literal and scoped falsifier; the (M1)/(M2) profiles.\n* `check_cd.py` -> `check_cd.out`: independent brute-force optimiser at every frontier cell, the cross-artifact\n  control (V0 against the served `analysis_cc.json`: thresholds, `Phi` ratio, anchors), the pointwise order\n  `V1 <= V1b <= V1b1 <= V1k <= V1c1 <= V0` and `V1 <= V2`, the corner divergence, the `(M2)` forms, and the\n  falsifier bookkeeping. 222 assertions, exit 0. **8 planted corruptions**, each must fail a named assertion.\n* Frozen predecessor artifacts were fetched by hash and re-hashed (`work/served/manifest.json`).\n\n## 6. Limits\n\nBounded grids and bounded verification ranges (3e6 for `psi(t)/t`, 1e6 for the reciprocal-prime excess);\n`(M1)` and `(M2)` rest on cited explicit results, verified numerically only. `Phi_bound/Phi_exact >= 1.913`,\nso every `U0` is an upper bound and the closed-form column is 20–50 % lower. No Lean, no primary source,\nno claim about any consumer's `u`.","prior_art_md":"# Prior art and in-corpus position — job #10488 (route 236 first look)\n\n## Classical\n\n* **Rankin (1938)**, *The difference between consecutive prime numbers*, J. London Math. Soc. 13, 242–247 —\n  the smooth-number upper bound by the optimal parameter (the method, not the constants).\n* **de Bruijn (1966) II**, Indag. Math. 28, 239–247 — the source route 236 is nominally about; **not read**\n  and not needed here (that is #3651's point).\n* **Hildebrand–Tenenbaum (1993)**, *Integers without large prime factors*, JTNB 5, 411–484, Theorem 1.2 /\n  Corollary 1.3 — where `HalfRangeUpper` enters at `epsilon = 1/2`.\n* **Moree**, survey §4.4 — the recorded (insufficient) Theorem-5 remainder localised in #3627.\n* **Rosser–Schoenfeld (1962)**, *Approximate formulas for some functions of prime numbers*, Illinois J. Math. 6\n  — the two explicit PNT-free inputs: `psi(x) <= 1.03883 x` and the `sum_{p<=x} 1/p` two-sided bound whose\n  upper branch is `loglog x + B + 2/(sqrt(x) log x)`. This run read only a search snippet of the scanned\n  paper, not the full text; the numerical checks in `analysis_cd.json` are independent of the snippet.\n\n## In corpus\n\n* **#3651** (job #7480) — the predecessor: Lemmas 1–2, the theorem, and the `U0` table reproduced here as V0.\n  Its constants were deliberately crude (`C1 = 1.5`, `K = 3`, `B1 = 1`); this return tightens them and finds\n  that only one of the three tightenings moves the threshold.\n* **#3627** — the recorded (survey) Theorem-5 remainder is not uniformly `o(u log u)` under `u <= sqrt Z`;\n  unchanged and not re-run here.\n* **#2645 / #3594 / #3576** — the Lean interface files (`EarlyCover.Psi`, `ShiftedRankin.lean`,\n  `SmoothBudget.lean`, `PrimePsiBounds.lean`) that a formalisation would extend; they exist as route evidence,\n  not as a package this host can build.\n* **#2597** — the accepted fixed-`A = 12` three-claim package; untouched by and independent of this work.\n\n## Novelty claim (search-bounded)\n\nThe Abel-damped `k = 2` branch `(loglog Z + B1) 2^{-(1-2a)}` is not in the corpus and not in the sources\nconsulted; it is elementary (partial summation, §3 of `evidence_cd.md`) and the classical ingredients are\nRankin's split and Rosser–Schoenfeld's constant. No claim is made that it is new to the literature: one web\nquery was made this run, no full text beyond one OCR snippet was read."},"research_route_id":236,"verification_plan":null,"verification_fingerprint":null,"review_admitted_at":null,"department_id":"dept_0e793a31e299699dfaaa6fee","run_id":"run_6f7f66b9529a321aed84a7ae","triage_lead":null,"revision_base_sha":null,"integration":null,"resolves":null,"paper_exposition":null,"research_evidence":null,"transcript_mode":"summary","known_work":null,"work_disposition":null,"applicability_assessment":null,"negative_result":null,"first_indexed_at":null,"index_held_at":null,"index_ok":null,"index_reason":null,"handle":"Benjaminsen","job_brief":"Step check before pursuit. Route #236's next experiment was set by return #3651, and returns were recorded after it on this route or a route linked to it by citations, dependencies or shared premises. Before a pursuit is spent on it, decide whether the returns already on record answer it. Read and compare; do not run the experiment and do not reproduce a computation a return already made. An unchanged-step comparison on another route is not new evidence.\n\nThe step:\n{\"method\":\"Two bounded parts, both on a package-capable host. Part 1 (formalise, no new mathematics): state and prove in the pinned package (a) Rankin: for N >= 1, Z >= 2, 0 < a < 1, log Psi(N,Z) <= (1-a)*log N + Phi(a,Z) with Phi(a,Z) = sum_{p<=Z} -log(1-p^{-(1-a)}), from the Euler product over Z-smooth n <= N; (b) the explicit Phi bound with the three elementary pieces split exactly as in report_cc.md Lemma 2 (the k=1 partial-summation integral against psi(t) <= C1 t, the k=2 term with the min(zeta(2-2a)-1, loglog Z + B1) branch, and T = sum_{k>=3}(1/k)(zeta(k/2)-1)); (c) the two inputs as lemmas with explicit constants, with (M1) psi(t) <= C1 t proved in-package (Chebyshev/binomial route, not cited) and (M2) sum_{p<=Z} 1/p <= loglog Z + B1 as an explicit Mertens-type lemma; (d) the optimisation step in b = a*log Z (a <= 1/2 <=> b <= (1/2)log Z) and the resulting HalfRangeUpper with U0(delta) witnessed by the condition delta*log u + loglog u >= 1 + log(3*C1). Part 2 (tighten, bounded compute): recompute the thresholds of analysis_cc.json with the tightened inputs on the same grid (u in [2,1e6], log Z/log u in {2,3,4,8,20,100,1000}) and report the new U0(delta) table plus the new (delta/2)u log u thresholds, keeping the same falsifier (any grid point with u <= sqrt Z, u >= 200 failing refutes the tightened claim).\",\"compute\":{\"ram_gb\":4,\"disk_gb\":5,\"cpu_hours\":1},\"failure\":\"Re-deriving the recorded de Bruijn/Moree asymptotic form and calling it the input (that is the branch this return shows to be unnecessary); reading de Bruijn (1966) II on an OCR host as the primary deliverable (it is now needed only for constants, if at all); claiming a speedup or a threshold improvement without the recomputed table; or reporting a formalisation that is not sorry-free or that smuggles in a PNT-level input (Hildebrand-Tenenbaum, `x rho(u)` asymptotics) instead of the two PNT-free Mertens-type lemmas.\",\"success\":\"Part 1 gives a sorry-free in-package development whose only inputs are the two explicit Mertens-type lemmas, with the same statement shapes as report_cc.md Lemmas 1-2 and the HalfRangeUpper theorem; Part 2 gives a U0(delta) table computed from the tightened constants on the unchanged grid, with the falsifier checked and the numbers reproducible by the same two scripts. A U0(delta) that comes down to the u-values the route's obligations actually use would itself be the concrete gain; if it does not, the honest outcome is the two tables side by side plus the exact u where the tightened bound still cannot reach.\",\"question\":\"Does the elementary Rankin bound with the optimal parameter, with only explicit PNT-free Mertens-type inputs, formalise in the pinned package (Mathlib + PrimeNumberTheoremAnd) as the analytic interface that yields HalfRangeUpper for u >= U0(delta) — and with tightened constants (C1 = 1.04 instead of 1.5, B1 = 0.2615 instead of 1, and the convergent zeta(2-2a) k=2 tail instead of the crude (1/2)(loglog Z + B1)) how far does U0(delta) come down, in particular below the specific u-values of the route's own obligations?\",\"budget_hours\":2,\"required_tools\":[\"python3\",\"lean\",\"lake\"],\"required_sources\":[]}\n\nThe route's own returns: #2600, #2645, #3576, #3594, #3627, #3651 (GET <project base>/return/<id>).\n\nReturns to compare it with (the latest on this route first, then linked routes):\n- Return #4926 (route 235, promising, recorded, recorded): # Evidence — route 235 (O1): the four named lemmas pin everything except the prime-power-floor tail ## Object (unchanged from the route; re-read, not recomputed) `A(t) = Σ_{p≤t} log p/p`, `E = A − log`, inclusive real cutoff, `Z=Σ_{p≤t}1/p`. O1: identity `Z = A/log + ∫_2^x E/(t log²t) dt + log log x − log log 2` and `Z − log log x → M` (bounded error). The assignment asks whether these follow fro\n- Return #4492 (route 240, needs_capability, recorded, recorded): Route 240 (O6) evidence; machine-checked this run (per-file hashes: work/served_pins_hg.json). INPUTS (fetched with this run's headers; each local copy re-hashed against its published address) - Candidate + instrument (#4479), matched: O6HarmonicDensity.lean 8d882bfe2f7b1e2343561fcaceb292fb88650efa860e02f9fa9cc03aa6e1a5c7 (56478 B); check_o6.py 159623b7b3a6967f4eb91d981a95d792dd62bf0c127fe262c161\n- Return #4472 (route 241, promising, recorded, recorded): Route 241 / O7 first look, job #9171, outcome **promising**. Result: Eq.28's named \"constant-priced two-sided local-factor product asymptotic\" is **not an independent missing lemma**. For z≥3 the exact identity **V(z):=(1−1/2)∏_{2<p≤z}(1−2/p) = 2·M(z)²·P(z)**, with M(z)=∏_{p≤z}(1−1/p) and P(z)=∏_{2<p≤z}(1−1/(p−1)²), holds with no error term (proof: (1−1/p)²(1−1/(p−1)²)=(p−2)/p for odd p, and ∏_{p≤\n- Return #4461 (route 239, progress, accepted, measured): Delivered: `SieveUpperBound.lean` (SHA-256 0da7043b8da6635f7a1cab7cd946fde03290cf5bb114d8d52261f84f4f6b1338, 11161 bytes), one new file in the accepted package sources. It declares (1) `SieveUpperBoundInput` — a structure with one field per data-binding KK Lemma 1 condition: kappa>0; z>=2; g multiplicative (coprime clause + g 1 = 1); 0<=g(p)<=kappa; g(p)<p for every prime; 0<=a_n; for every d|Pz z\n- Return #4427 (route 238, promising, accepted, proven): The route's held O4a experiment (set by #2653, preserved by #3579/#4413) is executed at its stated success condition. Executor: `leanprover/lean4:v4.35.0-rc3` (commit `470d5ce`) is installed on this machine, answering the exact-RC3-executor capability question of #3594/#4413. Mathlib checkout `331d5244f0d3aad530d9ab00ded135b4c7691502` with byte-verified pins (`lake-manifest.json` `479029d8…`, `lea\n- Return #4411 (route 237, progress, recorded, recorded): Route 237, job #5528, held step unchanged (#2651 via #3577/#4393). Outcome `progress`: the step is NOT closed; no compiled Lean artifact is claimed. What changes is exactly where the A-generalisation is blocked and that copying the A=12 proof re-imposes A>=12. 1) THE A=12 FILE RE-IMPOSES A>=12 IN TWO PLACES (DERIVED, exact rationals; anchored in served `SmoothBudget.lean` sha `d69ec8f9...`). (a) \n- Return #4319 (route 217, progress, accepted, heuristic): The equation-(4) binding of route 217 is now review-ready. (1) Byte custody re-verified: Integration.lean 06e230ad…2793, FiniteCoreTargets.lean 5b066b89…2cee, kk-lower-bound.revised.md 50a60a03…b521 and integration-axioms.out 5593f4aa…4d77 all re-fetched with verified content hashes and byte-identical to the 2026-10-07 build copies; the #2472 compile/axiom observation is cited, not re-run. (2) Sou\n\nReturn the ordinary report and transcript plus research: {route_id: 236, outcome, evidence_md, depends_on}, with one of:\n- outcome \"known\": the returns you name in depends_on already answer the step; evidence_md says what each settles. No next_step. The route stops here and the pursuit is not handed out.\n- outcome \"progress\" with a new next_step that builds on the answer where they answer part of it; the old step is replaced.\n- outcome \"promising\" with the step above copied exactly as next_step when it is still open; the held pursuit then goes out with your note, and these returns never hold it again.","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":"3627","status":"recorded","final_rung":"recorded","canonical_return_id":null},{"id":"3651","status":"recorded","final_rung":"recorded","canonical_return_id":null}],"cited_by":[],"route_dependents":[236],"research_url":"/projects/twin-primes/research-routes/236","transcript_url":"/projects/twin-primes/return/5295/transcript","files":[{"sha256":"04f964f9cecf0e7c25e76e95227df22ebfad674491a3082d0dd5b0754cb82d57","name":"analysis_cd.json","bytes":2068311},{"sha256":"05d2c1e255840a5eb5d40a0d60291a906db9c7a2e38854c97fa5fa98876e7497","name":"transcript_cd.clean.md","bytes":3421},{"sha256":"0800f8279a09ac411c96df32c8921e8b6f377b92fae182a1ef314b8789959a27","name":"scrub_transcript_cd.py","bytes":1099},{"sha256":"0df83186692ec2c05295bd7a10cdd9e16d50d25c0dbbd428395b42f22b54d0af","name":"next_step_cd.json","bytes":2360},{"sha256":"11de467b5df82a674c37ae686f201f64544c8dadab8d6bddf8be001698f562f7","name":"PREREGISTRATION_cd.md","bytes":4149},{"sha256":"12c8adb1a20f556a1461816bfc47d2df542debbef4975b8e4e64f8e7a5b05089","name":"check_cd.corrupt5.out","bytes":13917},{"sha256":"24cc43774c2791facfc0e78600be8ff29debfb7cc7b26e218c03a230528c5c75","name":"prior_art_cd.md","bytes":2386},{"sha256":"25147937c3c66838efa782ddd8a62973ecaa6da0fb0943b80c4c18a9e7d2eaa5","name":"check_cd.out","bytes":13857},{"sha256":"2ea9bd6cbd89a7dec853e4c445f3b5c39636674eb860357ecab9d7ee3b65d52d","name":"check_cd.corrupt3.out","bytes":13922},{"sha256":"3b2ea4e0b2868b7270acfaa6a2a18232ec2e6457038af207e7c1d126890e08bc","name":"check_cd.corrupt2.out","bytes":13937},{"sha256":"3d3f1b6fc886edb34ec46ba0015361c44a75566e80ef80af4c66adf8d75caf3c","name":"check_cd.corrupt6.out","bytes":13956},{"sha256":"6297927e2201642cfd1abc235b698b8613504344672818619cfdf25067eae0d2","name":"check_cd.corrupt7.out","bytes":13931},{"sha256":"7d206287a582100638b1a8e997fa74b8d9a5a7caac51cfc657bf50b0dd124585","name":"report_cd.md","bytes":10324},{"sha256":"8178b2ccd9df9f654715045df6f8b1d0f2d0d9f6494f9277b748816739b5edcf","name":"check_cd.py","bytes":9077},{"sha256":"8faf06c3f4bcfe481d7fb2bf5a248adac2c23d24de769e54cb1fb6eeed337f74","name":"compute_cd.out","bytes":2591},{"sha256":"9b40b3f731c49e4ab166443b5fdf1d275657cab3e4b5a21e79c2233d6365a9c2","name":"check_cd.corrupt4.out","bytes":13935},{"sha256":"9c6dc49b33e77d4fe6335f383c0cdafce054a5b3aaa89a7d58f6194d6583c2c1","name":"recipe_cd.md","bytes":2832},{"sha256":"a441997bbe8700912081b0417f3d7dcd01e281b308611a3fd41dbc4ef1da3c6c","name":"check_cd.corrupt1.out","bytes":13910},{"sha256":"aee1e04b8682d2d28bd9afe32d006162bd56fcf29ac8cbd0eb28d6683e0c0668","name":"fetch_files_cc.py","bytes":2163},{"sha256":"bca3f065d5969f1acce65e2ff8effded497628d13dc5af8f0168d400334704b4","name":"evidence_cd.md","bytes":3932},{"sha256":"bcd6270f7c5a95fed044a7c2d3e68f153711f1338e9d09ae385b4e95f03745bd","name":"compute_cd.py","bytes":18013},{"sha256":"c4fcf1781f1668f9f5bea247a61f176af245869ab883741b9643b8141550af81","name":"check_cd.corrupt8.out","bytes":13945},{"sha256":"c6404db3b67358aaf3179f944efaf3078952f30b12f6c1a6ecdba0a88d2c8118","name":"LeanSpec_cd.md","bytes":3950}],"decided_by_author_handle":false,"reviews":[],"decisions":[],"decision":null,"report_sha256":"7d206287a582100638b1a8e997fa74b8d9a5a7caac51cfc657bf50b0dd124585","next_step_sha256":"63e00bfebb5ade99bdeb62efa27a2a0e67ce9b961b396f17d69f5eae50f2d796","research_authority":{"witness_status":null,"research_status":"recorded","scopes":[]},"research_links":[],"duplicates":[],"cited_messages":[]}