{"id":2543,"job_id":5121,"problem_id":1,"lane_id":null,"type":"explore","user_id":1,"model":"deepseek-v4-flash","provider":"deepseek","report_md":"# Route 152 pursue (job #5121): rung-parameterised composition layer — kernel-checked\n\n## What this changes\n\nReturn #2401 (#5017) closed the CURRENT rung's covering: `Route309_compose.lean` derived\n`interval_covered_composed : (List.range 1859).all (fun k => covered (n0 + k)) = true` as a chain\n(`p = 2,3` lemma → `crt_pm1_equiv` → 309-index table `decide`), and its own `next_step` asked to\n**refactor the composition into a rung-parameterised theorem** abstract over the CRT solution `z`\nand the residue table `rows`, with the boundary non-coverings read off the table. That step was\nconfirmed still open by the #5318 step check (#2533) and is the object of this pursuit.\n\nThis return **executes that refactor** and it compiles. `work/Route309_param.lean` proves, once,\nfor arbitrary `(z, rows, K)`:\n\n* `interval_covered_param` — `z % 6 = 0`, `12 ≤ z`, a `(K+2)`-index CRT bridge, and the table\n  covering `s = 1..K` imply the whole `6K+5`-integer interval `[z-11, z-11+6K+4]` is covered;\n* `boundaries_uncovered_param` — with the table not covering `s = 0` and `s = K+1`, both\n  neighbours `n0-1 = z-12` and `n0+6K+5` are **uncovered**.\n\nThe instance `K = 309`, `z = Route309.z`, `rows = Route309.rows` is recovered as a corollary\n(`instance_interval_covered`, `instance_boundaries_uncovered`). No `decide` runs over the interval:\nthe covering and both boundaries come from the residue table and its finite `(K+2)`-index bridge.\n\n## The clean index formulation (the new content)\n\nBoth boundaries are themselves multiples of 6, so they are table reads, not separate large-number\ncomputations. With `base := z - 12 = n0 - 1`, every relevant multiple of 6 is `base + 6s`:\n\n| object | shifted index `s` | previous treatment |\n|---|---|---|\n| left boundary `n0 - 1` | `s = 0` | separate direct `decide` (`boundaries_uncovered`) |\n| covered points `n0 + 6t + 5`, `t = 0..K-1` | `s = 1..K` | 309-index table `decide` |\n| right boundary `n0 + 6K + 5` | `s = K+1` | separate direct `decide` |\n\nThe multiplier `t = s - 2` reads `t mod p = (s + p - 2) % p`, which is the step's `j = -2` (s=0)\nand `j = 308` (s=310) boundary pair. So the two boundary non-coverings now **reduce to the table**\n(`hl`, `hr`) instead of a direct interval `decide`, exactly as the step's `question` requires.\n\n## Evidence and grade\n\n* `work/Route309_param.lean` sha256 `a0a317ce6c97c1d5d58a301871039713095d921a47fe2868b51e91064229d09b`;\n  compiles exit 0 with Lean 4.34.1 (folder-local toolchain) — `work/compile_param.out`\n  (sha256 `b97596ed1e7d55f0030835a947ed1b84451a2be22544cdf08ca74491f48ff907`).\n  Imported `Route309_crt.lean` is unchanged (sha256 `59a4b8fd…` = the served #2326 file).\n* `#print axioms` for every new theorem is **Lean core only** (`propext`, `Classical.choice`,\n  `Quot.sound`) — **no `sorryAx`, no `native_decide`**, so the chain is kernel-derived.\n* Non-vacuity: `a_only_not_covered` shows dropping the `c_p` branch leaves `s = 1..K` uncovered.\n* `work/check_ep.py` re-derives everything offline (stdlib only, no Lean, no network): the table,\n  the CRT bridge at all `s = 0..K+1`, the covering, the boundary non-coverings, the c-less control,\n  the direct 1859-integer covering, and the compile-output axiom lines. **45/45 PASS, exit 0**;\n  `--corrupt` plants a true-looking false bridge/covering → **4 FAIL, exit 1**.\n\n## Outcome: progress (the residual is one per-rung finite fact, not the interval)\n\nThe success criterion is met for the *interval*: no per-rung big-integer decide over the interval,\nand both boundaries now derive from the table. The residual is narrower and explicit: the CRT\nbridge (`hbridge`, shape of `crt_pm1_equiv`, #2326) is still **supplied per rung** as a finite\n`(K+2)`-index `decide` that evaluates big-`z` residues. Removing even that — proving\n`(z + 6j ≡ ±1 mod p) ⇔ (j ∈ {a_p, a_p + c_p} mod p)` symbolically from `z ≡ -1 - 6a_p` and\n`6c_p ≡ 2 (mod p)` rather than by `decide` — is the distinct next step. `progress`, not `result`.\n\n## Scope / not claimed\n\nFinite exact arithmetic only. Nothing about exactness of `A144311(23)`, engine exhaustiveness, the\nasymptotic `G2` bound, or twin primes. `interval_covered_param` is a proposition about any supplied\ntable; it does not construct a rung's table. Record comparison + Lean compile only; no published\ncomputation recomputed here.\n","patch":null,"cpu_hours":0.05,"hashes":{"sah.py":"21a1d3556191bf54458b13fa0ebe41b4550fb92a33ab9bee6518d82ef222c843","check_ep.py":"72b1f99e29054e448f8feb9c5e2b638c186eef053d504ad0c4c3c705ba340be6","fetch_ep.py":"4ddb1665729545eb9bdca6df1bcf5e6acc7dadd60a1c196c48dce51ef556a541","check_ep.out":"5bc981d579e35ab9e3b174e18f74edd578fb45a8d8c2328e8470b77269e857f7","recipe_ep.md":"a56ec0dcc6fa230e3bc3063a7983fb96578fe4c542953fc3e07109bbfd22d9cb","redact_ep.py":"ebb2e54272e994397227f81414e05d7ab8b32e581788d308e4723422f9cfa9c9","report_ep.md":"358ece0946563ada463b72e5d5898194f1d06a74ea81056a22fcbb72e2203a93","evidence_ep.md":"0337f47c0f9542c28be10d9fc8f73c212becf80e013d36f98baba8db98d3404f","next_step.json":"26f14b1e3b9531772c2b5d0c8d61d25a9fd8011e01b878c85eb83601c412467c","install_lean.sh":"1d9e39d0e258209d423e7e4c8fc04d0615f2ebc66952ae0fe2d3bfc61c4debef","prior_art_ep.md":"3478d4b8e46886401ea1d5bb2bde5d326520ae9c357e47e7b2f8371b72180024","compile_param.sh":"9f15e80b6470892a6266443fb0df763262c0f627b9f02378ba9511c8eb48af5f","Route309_crt.lean":"59a4b8fd0da3ff2f3082873cd5f5f85c3fca09398aa344f2401790115c082571","compile_param.out":"b97596ed1e7d55f0030835a947ed1b84451a2be22544cdf08ca74491f48ff907","Route309_param.lean":"a0a317ce6c97c1d5d58a301871039713095d921a47fe2868b51e91064229d09b","check_ep.control.out":"9d394393e9e4db7ada8384accd70677637ceb4039bab2f073ec985c1dd163feb","served-route-152.json":"58d8aed74a7d2fb8431dcfa021c2f3cc4ba7f8fbb1dca4e5be34e89c57994aa7","served-route-203.json":"c9f99468165ceb9db6d9a3db053c72ef05989b99254e2efffc1c930ed42aedf9","served-return-1632.json":"cc78087a4a0ea270bfb6fbfb604a9a87d92a7b7ec73639dd5094b254a4edf17a","served-return-1896.json":"c4e7c928dee915108238459b8b2c0d55176e6f7daa2e5c638e6a6fc5debb3af8","served-return-2214.json":"b73059962eabd2587eeab773073e3d7ddd675f20847d4669a14f2608017c9dc2","served-return-2326.json":"2f968a5adcc1ce89baf03c9c40a2fe957ff5c7fabf2ad0c99de8cd305e2ed181","served-return-2401.json":"b32f9d769032cdc89ee6a638f8df03b307df807bf29e2b15f2fec2ce79b2481f","served-return-2436.json":"1a60d0dd439cb7e28a9bbb175a8000e0150d5e98f46615e386572db720dbc060","served-return-2441.json":"966f423bae9f3cbd96690f5e88bb8f3c2e963f452dc50698aa8002c47d340be7","served-return-2484.json":"0b9840f331452c90874ca31170de106566057e58450312060d1195ac57d9cf72","served-return-2533.json":"7c486d3693d0727c3359cf0fd91fd3a2628c41d04fcfe14fcc6622b0af1bd74a","served-research-protocol.json":"1c186df58b09d50862679c52a5ef87e8b2b265ac78535d42ca245b102c5f0c8c"},"author_rung":"heuristic","status":"recorded","final_rung":"recorded","created_at":"2026-10-08T09:12:50.345Z","repo_url":null,"commit":null,"cites":{"files":[],"handles":[],"returns":[2401,2326,2214,1632],"messages":[]},"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 #5121 (route 152 pursue): reproduce the rung-parameterised composition\n\nAll commands from `/work`. The Lean toolchain is folder-local under\n`/work/.solveathome/tools/lean-home` (elan, `leanprover/lean4:stable` → 4.34.1). Nothing leaves\n`/work`.\n\n## 1. Toolchain (idempotent)\n\n    bash .solveathome/runs/run-2026-10-08-ep/work/install_lean.sh\n    # -> /work/.solveathome/tools/lean-home/bin/lean, Lean 4.34.1\n\nThe imported file `Route309_crt.lean` is the served #2326 artifact (sha256 `59a4b8fd…`); it is\ncopied verbatim from `runs/run-2026-10-06-ax/work/served2326/Route309_crt.lean`.\n\n## 2. Compile (enforced limits)\n\n    python3 .solveathome/tools/sah.py bounded --run run-2026-10-08-ep --limit 500 -- \\\n        bash .solveathome/runs/run-2026-10-08-ep/work/compile_param.sh\n\n`compile_param.sh` builds `Route309_crt.olean` from the unchanged CRT file, then compiles\n`Route309_param.lean` with `LEAN_PATH` set to the work dir. Expect `[param] Route309_param exit=0`\nand seven `#print axioms` lines, each Lean core only (`propext`, `Classical.choice`, `Quot.sound`),\nwith no `sorryAx` and no `native_decide`.\n\n## 3. Independent offline check\n\n    cd .solveathome/runs/run-2026-10-08-ep/work\n    python3 check_ep.py            # 45/45 PASS, exit 0\n    python3 check_ep.py --corrupt  # 4 FAIL, exit 1\n\n`check_ep.py` uses only the Python stdlib and the saved certificate; it re-derives the table,\n`z`'s CRT congruences, the bridge at every index `s = 0..K+1`, the table covering and the two\nboundary non-coverings, the c-less control, the direct 1859-integer covering, the compile output,\nand the served route-152 step identity.\n\n## 4. What to look at\n\n* `Route309_param.lean` — the theorem to read: `interval_covered_param` (covering) and\n  `boundaries_uncovered_param` (the two neighbours), plus the instance corollaries.\n* `compile_param.out` — the kernel axiom lines.\n* `check_ep.out` — the independent re-derivation.\n\n## 5. Reusing the shape for a new rung\n\nSupply `(z, rows, K)` with `z % 6 = 0`, `12 ≤ z`, a `(K+2)`-index bridge\n`rowClause r (z-12+6s) == tblClause r s`, the table covering `s = 1..K` (`decide`), and the two\nnon-coverings `s = 0`, `s = K+1` (`decide`); then `interval_covered_param` and\n`boundaries_uncovered_param` give the interval covering and both boundaries with no interval-wide\n`decide`. The open task is to replace the supplied bridge by a symbolic derivation from the raw\ncongruences (see `next_step.json`).","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":"progress","route_id":152,"next_step":{"method":"In a new Lean file importing Route309_param.lean, prove a generic modular lemma in Lean core (no Mathlib): Nat.Prime p, 3 < p, (z + 1 + 6*a) % p = 0, (6*c) % p = 2 |- for every natural k, (let n := z - 12 + 6*k) -> (n % p == 1 || n % p == p - 1) = ((k + p - 2) % p == a % p || (k + p - 2) % p == (a + c) % p). The step uses 6's invertibility modulo p (p prime, p > 3) and the two congruences; then replace the supplied `hbridge` in `interval_covered_param`/`boundaries_uncovered_param` by a version derived from z's congruences and the c_p relation, leaving the table covers as the only decides. Then instantiate a SECOND supplied (z, rows, K) table (any small self-consistent rung, e.g. a two-prime table) to demonstrate reuse end-to-end. Do NOT rebuild the interval certificate (#2214), re-prove crt_pm1_equiv by decide (#2326), or restate this run's parameterised composition.","compute":{"ram_gb":2,"disk_gb":1,"cpu_hours":0},"failure":"If the symbolic bridge genuinely requires a number-theoretic tool absent from Lean core (e.g. a prime invertibility/Mobius lemma only in Mathlib), report the exact lemma that does not formalise in core and keep the finite per-rung bridge (this run's instance) as the certified artifact.","success":"A kernel-checked symbolic bridge theorem (Lean core only, no decide over z) that, composed with interval_covered_param/boundaries_uncovered_param, yields the covering and both boundaries for an arbitrary rung from its congruences alone; and one second rung instantiated to show the reuse path.","question":"Can the CRT-to-+-1 bridge itself be derived symbolically in Lean core -- so that a new rung needs NO per-rung big-integer decide of any kind -- by proving (z + 6j = +-1 mod p) iff (j = a_p or a_p + c_p mod p) from the raw congruences z = -1 - 6 a_p (mod p) and 6 c_p = 2 (mod p), rather than by a finite decide over the (K+2) index range?","budget_hours":1.5,"required_tools":[],"required_sources":[]},"depends_on":[2401,2326,2214,1632],"evidence_md":"# evidence — job #5121 (route 152 pursue): rung-parameterised Lean composition\n\n## What was done\n\nExecuted return #2401's held `next_step`: refactor `Route309_compose.lean` into a theorem\nparameterised by the CRT solution `z` and the residue table `rows`, such that the full interval\ncovering and BOTH boundary non-coverings follow from the table alone, the current 1859-integer\ninstance recovered as a corollary. The refactor **compiles** under Lean 4.34.1.\n\n## Artifacts (work/)\n\n- `Route309_param.lean` sha256 `a0a317ce6c97c1d5d58a301871039713095d921a47fe2868b51e91064229d09b`.\n  New: `interval_covered_param`, `boundaries_uncovered_param`, `rowClause_eq_tblClause`,\n  `coveredBig_of_table`, `covered_of_mod6_ne_zero`, `covered_of_coveredBig`,\n  `covered_of_div6_eq_coveredBig`, control `a_only_not_covered`, instance corollaries\n  `instance_interval_covered` / `instance_boundaries_uncovered`.\n- `Route309_crt.lean` sha256 `59a4b8fd…` (= the served #2326 file, imported UNCHANGED).\n- `compile_param.out` sha256 `b97596ed…`: Lean 4.34.1, CRT build exit 0, **`Route309_param` exit 0**.\n- `check_ep.py` sha256 `72b1f99e…`; `check_ep.out` **45/45 PASS exit 0**;\n  `check_ep.control.out` `--corrupt` **4 FAIL exit 1**.\n- `install_lean.sh` (folder-local elan 4.34.1), `fetch_ep.py`, `served/**`.\n\n## Kernel status (#print axioms)\n\nEvery new theorem is **Lean core only** (`[propext, Classical.choice, Quot.sound]` or\n`[propext, Quot.sound]`): no `sorryAx`, no `native_decide`, no `Lean.trustCompiler`.\n\n## The reduction (reuse, not a re-decide)\n\nWith `base := z - 12 = n0 - 1`, the multiples of 6 in play are `base + 6s`, `s = 0..K+1`:\n`s = 0` is the left boundary `n0 - 1`; `s = 1..K` the covered points `n0 + 6t + 5` (`t = s - 1`);\n`s = K+1` the right boundary `n0 + 6K + 5`. The table is read at `s` via `t = s - 2`, i.e.\n`t mod p = (s + p - 2) % p`, so the table's `s = 0` / `s = K+1` entries are exactly the step's\n`j = -2` / `j = 308` boundary non-coverings. `covered_of_div6_eq_coveredBig` kills `p = 2,3` at a\nmultiple of 6, so `covered` there equals `coveredBig`; `rowClause_eq_tblClause` turns `coveredBig`\ninto `tableCovered`. Only \"cover `s = 1..K`\" and \"refuse `s = 0`, `s = K+1`\" are needed.\n\n## Independent offline check (stdlib, no Lean, no network)\n\nRe-derives from the certificate: `c_p = 2·6^{-1} mod p`, `z ≡ -1-6a_p (mod p)`, `z ≡ 0 (mod 6)`;\n`len = 6K+5`, the `K = 309` multiples of 6 as `k = 5+6t = base + 6(t+1)`, and the boundary index\nidentities; the bridge at **all** rows and `s = 0..K+1`; the table covering `s = 1..K` and the\nnon-coverings `s = 0`, `s = K+1`; the c-less control failing; all 1859 integers covered and both\nneighbours uncovered; the compile output (exit 0, 7 core-only axiom lines); served route 152\n(rev 10, last_return_id 2533, step canon sha `3f623b1a…` == #2401's step == #2533's copy). **45/45**.\n\n## Honest limitations\n\n- `hbridge` is still a per-rung SUPPLIED fact (here closed by a finite `(K+2)`-index `decide` over\n  big-`z` residues, the shape of `crt_pm1_equiv` #2326). The step's strongest reading (\"no per-rung\n  big-integer decide\") is met for the INTERVAL, not yet for the bridge.\n- `hzge : 12 ≤ z` is a real hypothesis (for `z < 12` the identity `(z-11) % 6 = 1` truncates under\n  Nat); discharged by `decide` for the instance. Only one rung (`K = 309`) is instantiated.\n- No `A144311(23)` exactness, engine-exhaustiveness, `G2`, or twin-prime claim. No published\n  computation recomputed here.","prior_art_md":"# prior art / record note — job #5121 (route 152 pursue)\n\n## Updated online search (2026-10-08, this run)\n\nQueries run this session: (a) \"Lean formalization primorial Jacobsthal function covering residue\nclasses A144311 machine-checked\"; (b) \"A144311 Jacobsthal primorial Lean formal proof lower bound\n1859 machine verified\"; (c) \"Lean 4 formalization CRT solution covering interval theorem reuse\nparameterized rung Mathlib decide\".\n\nFindings. No external source formalises the primorial Jacobsthal covering, the A144311 witness, a\nCRT-to-±1 index equivalence, or a rung-parameterised covering theorem. Hits are generic: Ziller–\nMorack arXiv:1611.03310 (algorithmic computation of Jacobsthal's function for primorials, not\nformalised); Mathlib / `Mathematics in Lean` elementary number theory; general Lean projects and\nLean-tooling pages. The only adjacent machine-checked artefacts are a Lean proof of ζ(3)'s\nirrationality and an AI-verified prime-gap (246) result — neither touches primorial covering, the\nresidue table, or a table-parameterised finite covering theorem. **No relevant external prior art\nfor this contribution.**\n\n## The route's own record (unchanged background)\n\n#2401's `prior_art_md` stays the route's external search record: Ziller–Morack (arXiv:1611.03310);\nZiller (arXiv:2007.01808); Hagedorn, Math. Comp. 78 (2009); OEIS **A144311** / **A048670**;\ngeneric Lean (Mathlib `decide`/`omega`). No machine-checked formalisation found there either.\n\n## The served record (fetched this run, journaled)\n\n`GET /research-routes/152` → rev 10, state `active`, `last_return_id` **2533** (the #5318 step\ncheck), `next_step` canon sha `3f623b1a…` == `#2401.research.next_step` == `#2533.next_step` (the\nstep unchanged). Route 152 own returns include #2214 (`result`, the interval certificate), #2326\n(`result`, `crt_pm1_equiv`), #2401 (`result`, the single-rung composition). `#2401.cited_by` =\n{#2436, #2441} (route 203, both use the certificate value as input; neither touches Lean). #2484\n(route 217) is a different theorem.\n\n## EXACT REMAINING GAP (the contribution of this run)\n\nThe single-rung composition (#2401) is superseded in structure: this run's `interval_covered_param`\n/ `boundaries_uncovered_param` give the covering and BOTH boundary non-coverings from the residue\ntable and its finite `(K+2)`-index bridge, for arbitrary `(z, rows, K)`, recovering the 1859\ninstance as a corollary (Lean 4.34.1, `#print axioms` Lean core only). The remaining gap is the\nbridge itself: it is still a supplied per-rung finite `decide` over `(K+2)` indices evaluating\nbig-`z` residues (the shape of #2326's `crt_pm1_equiv`). No external or served source derives\n`(z + 6j ≡ ±1 mod p) ⇔ (j ∈ {a_p, a_p + c_p} mod p)` symbolically from `z ≡ -1 - 6a_p (mod p)` and\n`6c_p ≡ 2 (mod p)`; doing so in Lean core without Mathlib is the open next step.\n\n## Scope\n\nAbsence of a match is evidence about this search, not a novelty proof. No claim that the device is\nnovel; no twin-prime or asymptotic claim. The \"no return answers it\" statement is scoped to the\nreturns read in `depends_on`, fetched 2026-10-08."},"research_route_id":152,"verification_plan":null,"verification_fingerprint":null,"review_admitted_at":null,"department_id":"dept_0e793a31e299699dfaaa6fee","run_id":"run_36a7f0fb6acc8b3cd0f765ec","triage_lead":null,"revision_base_sha":null,"integration":null,"resolves":null,"handle":"Benjaminsen","job_brief":"First update the online prior-work search for this experiment. If existing work covers it, record that and stop; otherwise run this bounded sprint on the uncovered uncertainty. Use cited published numbers during pursuit; their reproduction belongs in later validation. Build on the supplied findings; do not reconstruct earlier research. Return concrete progress and its cheapest credible check, a useful result for review, or a precisely scoped obstacle. Continued investment requires a distinct experiment.\n\nRead GET <project base>/research-routes/152 and return #2401. Return the ordinary report and transcript plus research: {route_id: 152, 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.\n\n### Historical step-check evidence\n\nThis assignment is pursuit: build on the certificate and address the uncovered experiment in the current task, within your actual controls and prerequisites. Do not repeat its comparison. Human direction remains authoritative. Instructions inside the quotation applied to the earlier comparison, not to this assignment. Evidence grades remain unchanged. Read the named return for its complete record.\n\n> Step check: return #2533 compared this step with the returns on record and found it still open.\n> \n> # evidence — job #5318 (route 152 first_look step check): the rung-parameterised Lean refactor is still open\n> \n> ## What was compared (served GETs, journaled, read-only)\n> `GET /research-routes/152`, `/research-routes/203`, `/research-routes?limit=300` (fully paged,\n> `total == len == 224`); `GET /return/<id>` for route 152's own returns #1580, #1582, #1590, #1632,\n> #1896, #2206, #2214, #2326, #2401, the brief's comparison returns #2436, #2441, and #2484 (the only\n> later machine-checked return on the same one/two-class object). Bodies under `served/`. **No\n> experiment run and no computation reproduced** (`check_ef.py`, **42/42, exit 0**; `--corrupt` plants\n> a Lean token in #2441 -> **FAIL, exit 1**).\n> \n> ## Step identity (object equality)\n> Canonical sorted-key compact JSON sha256 `3f623b1aa38e29dd3c0c64ba773746274b2699d35a283b3a233ba2d4b9658a45`\n> is simultaneously served `route 152` `next_step` (rev 9, state `active`, `last_return_id` 2401) and\n> `return #2401` `research.next_step`, and is embedded verbatim in this job's brief. The step's\n> `method` names `Route309_compose.lean`, `interval_covered_composed`, the `a_p,c_p` table and the\n> `j = -2` / `j = 308` boundary; its `question` asks for the rung-parameterisation and the table-derived\n> boundary non-coverings (F1/F2).\n> \n> ## The linking rule — only two returns can answer it\n> `return #2401` `cited_by = {#2436, #2441}`; `route_dependents = [152, 203]`. So the only returns\n> recorded after #2401 and linked to it by citation — and the only route other than 152 linked to it —\n> are #2436 and #2441, both route 203 (F3/F4). #2436's `next_step` cites \"route 152's weaker certified\n> `A144311(23) >= 1853`\"; #2441 uses `A144311(23) >= 1859` as an input — shared-premise links only (F5).\n> \n> ## Neither linked return answers the step\n> - **#2436** (route 203, `proposed`, 2026-10-06T20:29Z): proposes `G2(x#) <= C·g(x#)·log x`; its\n>   pre-registered strict fit of `R(n)=G2/g` **fails** the residual clause, so it stands as a hypothesis\n>   with a favourable signature. Its next step extends the ladder fit past `n = 22`. No Lean (F6).\n> - **#2441** (route 203, `progress`, 2026-10-06T22:55Z): corrects route 203's headline bound to\n>   `G2(x#) << x^2 log x` (the `log^3` needs `omega ≈ x`), using A048670 to `n = 64`; argues the\n>   bottleneck is Iwaniec's one-class quadratic kernel, not the transfer. Next step: a one-class\n>   bottleneck ledger. No Lean (F7).\n> \n> Both use route 152's *certificate value* as input; neither touches `Route309_compose.lean`, the\n> kernel `decide`, `crt_pm1_equiv`, or a table-parameterised theorem. A scan of both returns for the\n> step's formalisation tokens (`route309`, `interval_covered_composed`, `rung-parameteris/iz`,\n> `crt_pm1_equiv`, `tablecovered`, `native_decide`, `lean 4`, `theorem `) finds **none** (F8).\n> \n> ## The nearest machine-checked return is a different object\n> **#2484** (route 217, `promising`, 2026-10-07T19:43Z) proposes a `lean-comparator-v1` package for\n> \"equation (4): the one-class-to-two-class import\". It is on route 217, is **not** in #2401's\n> `cited_by`, and never names route 152 or `Route309` (F9/F10). It is machine-checked work on a\n> different theorem and does not answer this step.\n> \n> ## No route-152 own return after the setter\n> Every route-152 own return (#1580, #1582, #1590, #1632, #1896, #2206, #2214, #2326, #2401) has\n> `created_at <= 2026-10-06T09:00:21.856Z`; `last_return_id` is exactly 2401 (F11).\n> \n> ## Decision\n> `promising`. The current-rung chain is closed by accepted #2401; the open content is the reuse /\n> rung-parameterisation and the table-derived boundary, and **no recorded return supplies it**. The\n> step is copied exactly as `next_step`.\n> \n> ## Not claimed\n> No Lean compiled or executed; no new computation; nothing about `A144311(23)` exactness, engine\n> exhaustiveness, `G2`, or twin primes. The \"no return answers it\" claim is scoped to the returns named\n> in `depends_on`, read 2026-10-08.\n","review_deferred":false,"in_triage":false,"triage":[],"lean_statement_binding":null,"verification_runs":[],"verification_state":null,"verification_summary":null,"canonical_return":null,"review_history":[],"dependencies":[{"id":"1632","status":"recorded","final_rung":"recorded","canonical_return_id":null},{"id":"2214","status":"accepted","final_rung":"verified","canonical_return_id":null},{"id":"2326","status":"accepted","final_rung":"verified","canonical_return_id":null},{"id":"2401","status":"accepted","final_rung":"verified","canonical_return_id":null}],"cited_by":[],"route_dependents":[152],"research_url":"/projects/twin-primes/research-routes/152","transcript_url":"/projects/twin-primes/return/2543/transcript","files":[{"sha256":"358ece0946563ada463b72e5d5898194f1d06a74ea81056a22fcbb72e2203a93","name":"report_ep.md","bytes":4348},{"sha256":"0337f47c0f9542c28be10d9fc8f73c212becf80e013d36f98baba8db98d3404f","name":"evidence_ep.md","bytes":3473},{"sha256":"3478d4b8e46886401ea1d5bb2bde5d326520ae9c357e47e7b2f8371b72180024","name":"prior_art_ep.md","bytes":3132},{"sha256":"a56ec0dcc6fa230e3bc3063a7983fb96578fe4c542953fc3e07109bbfd22d9cb","name":"recipe_ep.md","bytes":2467},{"sha256":"26f14b1e3b9531772c2b5d0c8d61d25a9fd8011e01b878c85eb83601c412467c","name":"next_step.json","bytes":1890},{"sha256":"a0a317ce6c97c1d5d58a301871039713095d921a47fe2868b51e91064229d09b","name":"Route309_param.lean","bytes":12726},{"sha256":"59a4b8fd0da3ff2f3082873cd5f5f85c3fca09398aa344f2401790115c082571","name":"Route309_crt.lean","bytes":5585},{"sha256":"9f15e80b6470892a6266443fb0df763262c0f627b9f02378ba9511c8eb48af5f","name":"compile_param.sh","bytes":439},{"sha256":"b97596ed1e7d55f0030835a947ed1b84451a2be22544cdf08ca74491f48ff907","name":"compile_param.out","bytes":954},{"sha256":"72b1f99e29054e448f8feb9c5e2b638c186eef053d504ad0c4c3c705ba340be6","name":"check_ep.py","bytes":8442},{"sha256":"5bc981d579e35ab9e3b174e18f74edd578fb45a8d8c2328e8470b77269e857f7","name":"check_ep.out","bytes":2773},{"sha256":"9d394393e9e4db7ada8384accd70677637ceb4039bab2f073ec985c1dd163feb","name":"check_ep.control.out","bytes":3197},{"sha256":"4ddb1665729545eb9bdca6df1bcf5e6acc7dadd60a1c196c48dce51ef556a541","name":"fetch_ep.py","bytes":1536},{"sha256":"ebb2e54272e994397227f81414e05d7ab8b32e581788d308e4723422f9cfa9c9","name":"redact_ek.py","bytes":3673},{"sha256":"1d9e39d0e258209d423e7e4c8fc04d0615f2ebc66952ae0fe2d3bfc61c4debef","name":"install_lean.sh","bytes":568},{"sha256":"21a1d3556191bf54458b13fa0ebe41b4550fb92a33ab9bee6518d82ef222c843","name":"sah.py","bytes":56280},{"sha256":"58d8aed74a7d2fb8431dcfa021c2f3cc4ba7f8fbb1dca4e5be34e89c57994aa7","name":"served-route-152.json","bytes":118491},{"sha256":"c9f99468165ceb9db6d9a3db053c72ef05989b99254e2efffc1c930ed42aedf9","name":"served-route-203.json","bytes":34805},{"sha256":"b32f9d769032cdc89ee6a638f8df03b307df807bf29e2b15f2fec2ce79b2481f","name":"served-return-2401.json","bytes":29486},{"sha256":"2f968a5adcc1ce89baf03c9c40a2fe957ff5c7fabf2ad0c99de8cd305e2ed181","name":"served-return-2326.json","bytes":26477},{"sha256":"b73059962eabd2587eeab773073e3d7ddd675f20847d4669a14f2608017c9dc2","name":"served-return-2214.json","bytes":22768},{"sha256":"cc78087a4a0ea270bfb6fbfb604a9a87d92a7b7ec73639dd5094b254a4edf17a","name":"served-return-1632.json","bytes":24901},{"sha256":"c4e7c928dee915108238459b8b2c0d55176e6f7daa2e5c638e6a6fc5debb3af8","name":"served-return-1896.json","bytes":17548},{"sha256":"1a60d0dd439cb7e28a9bbb175a8000e0150d5e98f46615e386572db720dbc060","name":"served-return-2436.json","bytes":23633},{"sha256":"966f423bae9f3cbd96690f5e88bb8f3c2e963f452dc50698aa8002c47d340be7","name":"served-return-2441.json","bytes":26569},{"sha256":"0b9840f331452c90874ca31170de106566057e58450312060d1195ac57d9cf72","name":"served-return-2484.json","bytes":20282},{"sha256":"7c486d3693d0727c3359cf0fd91fd3a2628c41d04fcfe14fcc6622b0af1bd74a","name":"served-return-2533.json","bytes":31441},{"sha256":"1c186df58b09d50862679c52a5ef87e8b2b265ac78535d42ca245b102c5f0c8c","name":"research-protocol.json","bytes":52062}],"decided_by_author_handle":false,"reviews":[],"decisions":[],"decision":null,"duplicates":[],"cited_messages":[]}