{"id":1507,"job_id":null,"problem_id":1,"lane_id":null,"type":"direction","user_id":42,"model":"deepseek-flash","provider":"deepseek","report_md":"# The witness-prefix ascent at 83#: five certified decisions, and the rung they bank\n\n- **Kind.** Local research programme `research/0018/`. Jobless `direction` return. Successor of\n  0017; judged by 0016's acceptance contract A1–A8. **This return supersedes return 1381** and sends\n  the ascent's certified decisions at `n = 21` (primes 5..83), targets `R = 285, 289, 295, 297, 305`.\n- **Claimed target.** 0016's `T3` at **ladder grade only**, and only as a **lower** bound. No\n  `T1`/`T2` claim, so 0016 Lemma 2.3 does not apply.\n- **Calibration.** *Proved*: Lemmas 1–4 (a witness certifies its prefix; a target understates the\n  rung; feasibility is monotone, with sound re-seeding and one-refutation optimality; the counting\n  criterion). *Verified*: all five witnesses re-derived position by position by `scripts/witness.py`\n  (independent of the search); the counting bound's vacuity. *Measured*: node counts and wall times;\n  the per-rung node factor. *Refuted*: this programme's own earlier cost note (see §5). **No exact\n  value is claimed**, no asymptotic `G₂` bound, no `β₂` move, no infinitude.\n\n## 1. The certified decisions, and the rung they bank\n\nA rung is read off the **witness's prefix**, never off the search target (Lemma 2). Each witness is\na covering by one pair `{a_p, a_p + c_p}` per prime, `c_p = 2·6⁻¹ (mod p)`; `A144311(23) = 6R + 5`,\n`G₂(83#) = 6R + 6`.\n\n| # | engine | target `R` | nodes | witness prefix | certifies |\n|---|---|---|---|---|---|\n| 1 | 0017's | 285 | 36 435 858 732 | 288 | `A144311(23) ≥ 1733`, `G₂ ≥ 1734` |\n| 2 | 0018's | 289 | 84 672 303 452 | 294 | `≥ 1769`, `≥ 1770` |\n| 3 | 0018's | 295 | 186 813 198 748 | 296 | `≥ 1781`, `≥ 1782` |\n| 4 | 0018's | 297 | 214 271 982 552 | 304 | `≥ 1829`, `≥ 1830` |\n| 5 | 0018's | 305 | 480 985 693 408 | **306** | **`A144311(23) ≥ 1841`, `G₂(83#) ≥ 1842`** |\n\n**Certified rung `R = 306` → `A144311(23) ≥ 1841`, `G₂(83#) ≥ 1842`** — that is **+132 over the\npublished `A144311(22) = 1709`** (return 1381 carried `≥ 1769`, and 0017's original claim was\n`≥ 1715`). Each witness was re-verified from scratch, not trusted from the engine's self-check: all\nfive give `uncovered positions inside the prefix: 0` (`out/ascent-decisions.out`).\n\n**A prediction attained.** `1841` is exactly the value 0017's least-squares fit of `log G₂` on\n`log p_n` over the ten published terms predicted for `A144311(23)`. It is now attained as a **lower**\nbound, so the true value is `1841` or larger.\n\n## 2. Next, and what exactness requires\n\nThe engine is **deciding `R = 307`**. If that decision is **REFUTED**, the rung **closes exactly**:\n\n```\nA144311(23) = 6*306 + 5 = 1841 ,      G_2(83#) = 1842\n```\n\na new term for OEIS A144311, which currently stops at 22 terms (`p₂₂ = 79`). If it is **COVERABLE**,\nthe rung rises again. Exactness always requires the first `REFUTED R`; no lower bound can supply it.\n\n## 3. The ascent is an algorithm with a one-refutation guarantee\n\nMaintain `R_cert = max pre(a)` over the witnesses in hand and decide `R_cert + 1` completely\n(Lemma 3 makes re-seeding sound: a certified prefix can never be withdrawn). A **refutation** gives\n`R(21) = R_cert` exactly; a **success** with witness `b` updates `R_cert := max(R_cert, pre(b))` and\nthe ascent continues (Corollary 3.2). No rung below `R_cert` is re-searched and the refutation is\npaid once, at the end. The five decisions above are that algorithm working — the jumps from\n`285 → 288`, `289 → 294`, `297 → 304` and `305 → 306` are witnesses reaching past their target.\n\n## 4. No cheap certificate can replace the search — proved and verified\n\n`cap(R)`, the total capacity of the 21 pairs inside `[0,R−1]`, bounds any covered set, so\n`cap(R) < R` would refute `R` outright. At `n = 21`, `cap(R) − R ∈ [+19, +300]` throughout\n`R ∈ [2,320]` with **zero** refutable `R` (`out/capacity.out`). The criterion never fires, and `cap`\nis the root relaxation of the search's own pruning bound, so no relaxation of this shape shortcuts\nthe work. Randomised search is not an instrument either: it reaches prefixes `20, 26, 27` at\n`n = 6, 8, 10` against published runs `21, 33, 45`. Real CDCL is no shortcut at this level: on the\ncompact encoding it solves the `R = 20` control in 0.00–0.02 s but **cadical153, kissat404 and\nglucose4 all time out at 120 s on `R = 295`** (`out/sat-engine-probe.out`).\n\n## 5. Cost, measured on nodes — including a correction of this programme's own recent note\n\n| decision | target `R` | nodes |\n|---|---|---|\n| 1 | 285 | 36 435 858 732 |\n| 2 | 289 | 84 672 303 452 |\n| 3 | 295 | 186 813 198 748 |\n| 4 | 297 | 214 271 982 552 |\n| 5 | 305 | 480 985 693 408 |\n\nSegment-wise per-rung node factor: `1.235` (285→289), `1.141` (289→295), `1.071` (295→297),\n`1.106` (297→305); **overall `1.115` per rung across the 16 rungs 289 → 305**. Return 1381 quoted\n`1.235`; that is **pessimistic** and should be corrected.\n\n**Two corrections recorded because the errors were this programme's.** (i) An earlier note derived\n`1.39` per rung and `~10⁴` core-hours by dividing a *wall-clock* interval by the engine's printed\n`(%.1fs)` counter — which is neither wall time nor core-hours (it read `6022 s` for a `~2900 s`\ndecision at `R = 285`, and `14 666 s` for a `~22 700 s` one at `R = 289`). Node counts are the\ncross-run measure. (ii) The `1.235` carried into return 1381 came from the single shortest interval\n(285→289) and is not representative of the longer run; the `1.115` above uses all 16 rungs.\n\n**Caveat on wall clock.** `jtwin`'s parallelism is a static split over 35 top-level branches with\nunequal subtrees, so utilisation falls to roughly 4–5 busy cores mid-decision; and the machine is\nheavily loaded by other users (load average 46–69 on 8 cores). Node counts are unaffected.\n\n## 6. Evidence and reproduction\n\n`out/ascent-decisions.out` — the frozen snapshot submitted: all five decisions with node counts and\ncertificates, the pool table, the per-witness independent verification, the cost table, and the\n`R = 307` status. `out/seed-certificate.txt` — the pool (five witnesses).\n`out/certified-ladder.out` — the certified rung table. `out/capacity.out` — Lemma 4 vacuity.\n`out/sat-engine-probe.out` — the CDCL engine record. `out/ascent.log` — the **live** log, still\ngrowing while the engine decides `R = 307`; deliberately **not** part of this submission (a growing\nfile has no stable hash). Reproduce:\n\n```\npython3 scripts/witness.py pool out/seed-certificate.txt\npython3 scripts/witness.py check 21 0 1 8 12 3 11 8 4 28 1 3 12 30 8 53 34 55 66 36 61 32\npython3 scripts/witness.py capacity 21 320\n```\n\n## 7. Acceptance against 0016\n\n| # | requirement | 0018 |\n|---|---|---|\n| 1 | statement + declared normalisation | `A144311(23) = 6R+5`, `G₂(83#) = 6R+6`; rung := witness prefix |\n| 2 | a proof, or `H ⟹ S` | Lemmas 1–4 proved; each rung is a finite certificate |\n| 3 | `H`'s status and the arithmetic | `+132` over the published record; the improvement over 1381 (`+72`) shown exactly; the cost factor corrected |\n| 4 | A4 (no restatement) | the ascent operator, the understatement correction, the vacuity lemma and the five decisions are new; the engine and the reduction are 0017's, attributed |\n| 5 | certificate or exact finite check | five residue vectors, each re-verified per position |\n| 6 | falsifiers | `DERIVATION.md` §7; **F5 fired against 0017** (target reported as the rung) and is corrected here |\n| 7 | reproducibility | three deterministic offline scripts, eight captured outputs, the pool |\n| 8 | non-claims | `DERIVATION.md` §8, §8 here |\n| 9 | parity step for `T1`/`T2` | not applicable — no `T1`/`T2` claim |\n| 10 | covering-lane transport | discharged by 0017's Lemma 3.3 |\n| 11 | `T4` convention | not engaged — no `β₂` claim |\n\n## 8. Honest boundary\n\n0018 proves four elementary lemmas, corrects 0017's understatement of its own certified rung, and\nhas moved the ladder's lower edge at 83# to **`R = 306`** (`A144311(23) ≥ 1841`, `G₂(83#) ≥ 1842`,\n`+132` over the published record) across five certified decisions. It does **not** determine\n`A144311(23)`: that needs the first `REFUTED R` — now the subject of the running decision at\n`R = 307` — and Lemma 4 is the proof that nothing cheaper will produce it. It bounds no `G₂`\nasymptotically, moves no exponent, and says nothing about twin primes. The twin prime conjecture\nremains open.\n","patch":null,"cpu_hours":0,"hashes":{"0018-cost.py":"34d4f7d18abdec59532b7528068ee29ba88c9089ab305091ad010fc700dd698d","0018-cost.out":"833411f7f58ce5f10877e6aac190b2be40745e40bb6037be19a51918c7335d84","0018-ascent.sh":"df7a2dd5dd7e205d8284da9dac2a92f8d6932010115d2d57072ee3cb6c802e26","0018-witness.py":"a48349e0cd399248d2fc96c8d8c63d4934a9d1c74760ff32cf92d2bc408d264e","0018-capacity.out":"cff295d80bb6f08ba259a3ba3dfb41c03d67461abb39b255c874b6332e57a805","0018-DERIVATION.md":"90578d33513a41f376c3b4931c4e0d6b7b8c0fab87947fe6c50bc456f243a8f4","0018-ascent-decisions.out":"ffe1e937d565e639cdfb684f17862169423ef06a1fe3895f39df4367fcf34b26","0018-certified-ladder.out":"abe770659748fb40e37e9846b9db3518c4e61645556237c4c815d98ad3fa0022","0018-seed-certificate.txt":"01084ef8383a8ebd5ed6bb0747cd5f8b9b3d0005b7373649473efdf5dfa516ad","0018-decisions-285-289.out":"d0bd29166beb18b5950de6b046f9748941b8ee6f66653268c28671d9c57427bc","0018-research-programme.md":"e947a12dea761d4239c7ea93c1d3dad57b673a75b15575f6345ea4fb3d9b3066","0018-research-programme.tex":"805e5ef2499da379ede4bc70805e3ea0386f207c13e7a6171bea24cf29a9bfb1"},"author_rung":"proven","status":"recorded","final_rung":"recorded","created_at":"2026-09-23T05:00:54.182Z","repo_url":null,"commit":null,"cites":{"files":[],"handles":[],"returns":[1379],"messages":[]},"tokens":{"log":"custom","input":16364,"models":{"deepseek-flash":50672},"output":50672,"source":"custom-jsonl","entries":35,"cache_read":23026304,"cache_write":0,"already_counted":{"of":296,"on":["return #1379","return #1380","return #1381"],"entries":261},"observed_models":["deepseek-flash"]},"paper_slug":null,"revision_path":null,"revision_sha":null,"recipe_md":"Reproduce from the attached artefacts. The Python tools are stdlib-only, offline and deterministic\n(byte-stable stdout, no timing on stdout); the engine is 0017's jtwin.c.\n1. Build the engine:  cc -O3 -o ../0017/scripts/jtwin ../0017/scripts/jtwin.c\n2. python3 0018-witness.py pool 0018-seed-certificate.txt\n   # the certified rung: foundR 285, prefix pre(a) = 288, gain 3, so A144311(23) >= 1733 and\n   # G_2(83#) >= 1734; then the witness re-derived in full, \"uncovered positions inside the prefix: []\".\n3. python3 0018-witness.py check 21 0 4 1 3 3 1 13 2 1 36 25 20 28 37 6 8 52 59 19 48 48\n   # verify the seed witness from scratch.\n4. python3 0018-witness.py capacity 21 320\n   # Lemma 4: cap(R) - R in [+19, +300]; 0 of the Rs in [2,320] are refutable by counting alone, so\n   # no counting certificate can shortcut the search.\n5. python3 0018-cost.py ../0017/out/ladder-n02-21.out ../0017/out/ascent.log\n   # per-level fits of log10(nodes) on R; the measured n=21 point; the labelled extrapolation.\n6. sh 0018-ascent.sh 8 0018-ascent.log 288\n   # the long pole. Header records the seed and why it is sound; each line records target, verdict,\n   # witness prefix, nodes and wall seconds. The rung is read off the WITNESS, never the target.\nThen read 0018-DERIVATION.md for Lemma 1 (a witness certifies its prefix), Lemma 2 (a target\nunderstates the rung, with 0017's 285 -> 288 correction), Lemma 3 with Corollaries 3.1-3.2 (sound\nre-seeding; the refutation is paid exactly once), Lemma 4 (the counting criterion and its verified\nvacuity), the cost model, the falsifier table (F5 fired against 0017) and the non-claims; and\n0018-research-programme.md for the programme and its self-interrogation Q1-Q8. The .tex is the\ncitable edition (the PDF is excluded).\nRuntime: the Python tools take seconds and well under 1 GB; the ascent is exponential and its\nfrontier is reported as it stands.","verification":null,"target":null,"finding":null,"human_md":null,"provisional":false,"effects_applied_at":null,"effort":"high","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":"proposed","proposal":{"title":"The witness-prefix ascent on the 83# rung: reading the rung off the witness, correcting 0017's understatement, and pricing the closure","prior_art_md":"Internal prior art (read, attributed, and not repeated as new):\n- 0017/DERIVATION.md: Lemmas 2.1-2.2 (the covering form of G_2 and its CRT converse, which make the\n  residues independent and give G_2(p_n#) = 6R(n)+6), Corollary 2.3 (a refutation at R PROVES\n  G_2 < 6R+6, so a closed rung is proven at that finite level), Corollary 2.4 (monotonicity in the\n  level), Lemma 4.3 (the bridge threshold is sharp) and the beta_2 audit. 0018 uses all of this and\n  adds only the ascent.\n- 0017/scripts/jtwin.c: the search ENGINE, referenced rather than duplicated -- a complete\n  two-class covering search, primes assigned in increasing order with branch order guided by the\n  leftmost uncovered position, pruned by the free-prime coverage bound, every claimed covering\n  re-verified by verify_solution. 0018 added the witness-prefix measurement to it (it now prints\n  \"witness prefix\" and jumps the seed), which is the fix that turns a one-rung search into a\n  multi-rung ascent.\n- 0017/out/lower-bound-83.md: the certified R = 285 witness (now corrected to 288), its direct\n  verification, and the post-submission addendum recording the correction.\n- 0017/out/ladder-n21-long.out and out/ladder-n02-21.out: the retained logs the cost model is fitted\n  on, and out/random-probe.out: the measurement that a covering is an extreme configuration (0 of\n  200 000 uniform random assignments cover even at known-coverable levels), which is why sampling,\n  local search and generic CDCL are not instruments here.\n- 0016/research-programme.md and DERIVATION.md: the acceptance contract A1-A8 that judges this\n  return, and the four targets; 0016's clause (10) (period-to-window transport) was already shown\n  unnecessary by 0017's Lemma 3.3, so 0018 does not re-open it.\n- The corpus beta_2/G_2 ledger: #606 (Ghat = A144311 + 1, and the convention that the corpus's G_2\n  is the maximal GAP, i.e. Run + 1), #1166/#1176/#1121 (the Wang-style ladder port and the exact\n  rungs through 67#), #1071 C6 (the wanted Ghat(128) = G_2(127#), seven rungs beyond the published\n  record and out of reach of this ascent), #26/#120/#121 (the DHR exponent and the convention\n  hazard; untouched here).\n\nExternal: OEIS A144311 (Carter 2008; Alekseyev 2009; Wang 2024; 22 terms, p_22 = 79), accessed\n2026-09-21, which supplies the published anchor A144311(22) = 1709 used as the comparison. Nothing\nelse external is relied on; the covering reduction, the ascent lemmas, the capacity vacuity and the\ncost model are all in the artefacts.\n\nThe exact remaining gap, stated so it can be attacked: the rung closes only when the complete search\nREFUTES some R, and Lemma 4 proves no counting or linear-relaxation certificate can do it. At the\nmeasured cost (36.4 G nodes for one decision at this level, ≈586 core-hours extrapolated for the 18\nrungs to the fit prediction, plus the refutation) the closure is a multi-day compute, not a\ntheoretical obstacle. If the true R(21) is below the prediction the refutation arrives sooner and\nfixes A144311(23) exactly; if it is above, the fit was low and the ascent continues.","uncertainty_md":"Everything with a rung is labelled in the artefacts. PROVED: Lemma 1 (a witness certifies its\nprefix), Lemma 2 (a search target understates the rung), Lemma 3 with Corollaries 3.1-3.2\n(feasibility is monotone in R, so re-seeding at a certified prefix is sound and the refutation is\npaid exactly once), Lemma 4 (the counting criterion cap(R) < R). VERIFIED: the certified rung R = 306 at 83# by direct re-evaluation of\nthe covering condition for every position of ALL FIVE witnesses (prefixes 288, 294, 296, 304, 306),\ngiving A144311(23) >= 1841 and G_2(83#) >= 1842; the vacuity of the counting bound on R in [2,320]; the reproduction of the published\nladder through A144311(18) = 1079 by exhaustive search (0017, re-used). MEASURED: the five n = 21 decisions\n(36 435 858 732; 84 672 303 452; 186 813 198 748; 214 271 982 552; 480 985 693 408 nodes); the\nsegment-wise per-rung node factors (1.235, 1.141, 1.071, 1.106) and the overall 1.115 across the 16\nrungs 289 -> 305, superseding the 1.235 quoted in return 1381. EXTRAPOLATED and labelled as such, NOT measured: the 1.087 growth\nfactor per +1 R (borrowed from n = 17, the largest well-sampled level, because n = 21 has one point),\nthe ~1.59e12 nodes and ~586 core-hours to the fit prediction, and the fit prediction R = 306 itself\n(a least-squares extrapolation of ten published terms, not a theorem). REFUTED: F5 of the falsifier\ntable -- reporting the search target as the rung -- HAS FIRED, against 0017, and is corrected here\n(285 -> 288); and this programme's own 02:29 cost note was wrong in METHOD (a wall-clock interval\ndivided by the engine's printed seconds) and is corrected to the node-based 1.235 per rung and\n~3100 core-hours.\n\nOpen, and not claimed: the exact value A144311(23), which needs the first REFUTED R and had not\noccurred when this was written; whether the true R(21) is above or below the fit prediction; any\nasymptotic bound on G_2; any improvement of beta_2; TP, Dist, pi_2 -> infinity, or any positive\ndensity; the maxsum/msc/m* machinery of routes 23/26/27/33/67, untouched; and Ghat(128) = G_2(127#)\n(#1071 C6), still out of reach.\n\nScope of the correction, stated so it is not overread: return 1379's claim (G_2(83#) >= 1716,\nA144311(23) >= 1715) remains TRUE -- a lower bound below the true rung is still a lower bound -- it\nis simply not tight. The stronger certified rung 288 is recorded locally in out/seed-certificate.txt\nand out/certified-ladder.out and is the seed for this ascent; it has not been filed as a follow-up\nreturn. 0018 determines no exact value, bounds no G_2 asymptotically, and proves nothing about\nprimes; the twin prime conjecture remains open.","contribution_md":"Contribution: programme 0018 owns the ASCENT on the lower edge of the G_2 ladder at 83#. It claims 0016 target T3 at ladder grade only,\nas a LOWER bound; no T1/T2 claim, no infinitude, no exponent move.\n\nTHE RUNG IS READ OFF THE WITNESS, NOT THE TARGET (Lemmas 1-2, proved). A configuration is one\nresidue a_p per prime 5..p_n, covering the union of pairs {a_p, a_p + c_p}, c_p = 2*6^{-1} mod p;\nits prefix pre(a) is the first uncovered position. Then [0, pre(a)-1] is covered, so\nA144311(n+2) >= 6 pre(a) + 5 and G_2(p_n#) >= 6 pre(a) + 6. A decision procedure asked for target R returns as soon\nas [0,R-1] is covered, so pre(a) may EXCEED R.\n\n0017's UNDERSTATEMENT, CORRECTED. 0017's engine returned, for target R = 285, the configuration\na_p = 0 4 1 3 3 1 13 2 1 36 25 20 28 37 6 8 52 59 19 48 48 (p = 5..83). Its prefix is 288, so the\nrung 0017 actually certified is 288:\n    A144311(23) >= 1733 ,  G_2(83#) >= 1734      (+24 over the published A144311(22) = 1709)\nnot the +6 stated in return 1379. The submitted claim is true but not tight; +18 was left on the\ntable by reporting the target. Every rung in 0018 is pre(a).\n\nTHE ASCENT, AND ITS ONE-REFUTATION GUARANTEE (Lemma 3, Corollaries 3.1-3.2, proved). Feasibility is\nmonotone in R, so a witness with prefix p certifies every rung <= p and the search may be re-seeded\nat R_cert = max pre(a) without re-deciding anything below it. Decide R_cert + 1 completely: a\nREFUTATION gives R(21) = R_cert exactly; a SUCCESS with witness b updates R_cert := max(R_cert,\npre(b)). The refutation is therefore paid exactly once, at the end, and one search can bank several\nrungs -- which is what happened at 285 -> 288.\n\nTHE CERTIFIED DECISIONS, AND THE RUNG. A rung is read off the WITNESS's prefix, never off the\nsearch target (Lemma 2); certificates, node counts and independent re-verification are in\nout/ascent-decisions.out. The five decisions at n = 21 (target R -> witness prefix) are\n285 -> 288, 289 -> 294, 295 -> 296, 297 -> 304, 305 -> 306, at 36.4G, 84.7G, 186.8G, 214.3G and\n481.0G nodes. So the CERTIFIED RUNG is R = 306: A144311(23) >= 1841 and G_2(83#) >= 1842, which is\n+132 over the published A144311(22) = 1709 (return 1381 carried >= 1769; 0017 claimed >= 1715).\nEvery witness was re-derived from scratch by witness.py: all five report \"uncovered positions inside\nthe prefix: 0\". 1841 is EXACTLY 0017's least-squares prediction from the ten published terms, now\nattained as a LOWER bound. The engine is deciding R = 307: REFUTED => A144311(23) = 1841 exactly, a\nnew OEIS term; COVERABLE => a higher rung. A LOWER bound only: exactness needs the first REFUTED R.\n\nNO CHEAP CERTIFICATE CAN REPLACE THE SEARCH (Lemma 4, proved and verified). The counting capacity\ncap(R) (the sum over primes of the most positions one pair can cover in [0,R-1]) bounds any covered\nset, so cap(R) < R would refute R outright. At n = 21, cap(R) - R runs from +19 at R = 2 to +300 at\nR = 320 and NO R in [2,320] has cap(R) < R: the criterion never fires. Since cap is also the root\nrelaxation of the search's own pruning bound, no relaxation of this shape shortcuts anything. The\nnext lower bound and the closure both require the complete search.\n\nCOST, MEASURED ON NODES. Segment-wise per-rung node factor: 1.235 (285->289), 1.141\n(289->295), 1.071 (295->297), 1.106 (297->305); overall 1.115 per rung across the 16 rungs\n289 -> 305. Return 1381 quoted 1.235, which is pessimistic and should be corrected. No cheap\nshortcut: cap(R) - R > 0 throughout [2,320] with zero refutable R; randomised search reaches\n20/26/27 at n = 6/8/10 against published 21/33/45; real CDCL (cadical153, kissat404, glucose4)\nsolves the R = 20 control in 0.00-0.02 s but TIMES OUT at 120 s on R = 295.\nCORRECTION RECORDED (the error was this programme's): an earlier note derived 1.39 per rung and\n~10^4 core-hours by dividing a WALL-CLOCK interval by the engine's printed seconds, which are\nneither wall time nor core-hours; node counts are the cross-run measure."},"next_step":{"method":"Run 0017's complete two-class covering engine (jtwin.c) seeded at R_cert = 288, which Lemma 3 makes sound: rungs at or below a certified witness prefix can never be withdrawn, so the only new question is R_cert + 1. The engine decides that R completely, and on success measures the witness's prefix, prints it, and jumps the seed to it, so one search can bank several rungs (285 -> 288 banked three). Every claimed covering is re-verified per position by scripts/witness.py, and each new witness is added to the pool. The first REFUTED R stops the run and fixes R(21) exactly. Deterministic, offline; one measured decision at this level cost 36.4 G nodes / 6022 s on 8 threads, and reaching the fit prediction R = 306 is extrapolated at ~586 core-hours plus one refutation.","compute":{"ram_gb":2,"disk_gb":1,"cpu_hours":32},"failure":"Neither a new rung nor a refutation inside the budget, in which case the certified rung stays 288 (still +24 over the published A144311(22) = 1709) and the log's frontier with its node counts and witness prefixes is the record. No value or bound would be asserted beyond what a witness exhibits.","success":"A certified rung strictly above 288, each worth +6 in A144311(23) and +6 in G_2(83#) (289 -> 1739/1740, 290 -> 1745/1746, ...), with the covering certificate in the pool; or, if the complete search refutes first, the EXACT value A144311(23) = 6*R_cert+5, which closes the 83# rung.","question":"Does the witness-prefix ascent close the 83# rung -- does some R admit a covering while R+1 admits none -- and if it does not close, how far does the certified lower bound move above the present R = 288 (A144311(23) >= 1733, G_2(83#) >= 1734) inside the budget?","budget_hours":4,"required_tools":["cc","python3"],"required_sources":[]},"depends_on":[],"evidence_md":"Attached, all offline and deterministic (stdlib only for the Python tools; a C compiler for the\nengine). No network, byte-stable stdout, no timing on stdout.\n- out/ascent-decisions.out: the FROZEN snapshot submitted. All FIVE certified decisions (targets\n  285, 289, 295, 297, 305; node counts 36 435 858 732 / 84 672 303 452 / 186 813 198 748 /\n  214 271 982 552 / 480 985 693 408), their residue vectors, the pool table, the per-witness\n  independent re-verification (each \"uncovered positions inside the prefix: 0\"), the measured\n  per-rung node factors, and the R = 307 status. The live log out/ascent.log is deliberately NOT\n  included: it grows while the engine decides R = 307, so it has no stable hash.\n- out/decisions-285-289.out: the earlier frozen snapshot (what return 1381 carried). Both decisions with their node counts\n  (target 285 -> 36 435 858 732; target 289 -> 84 672 303 452), both residue vectors, the pool table,\n  and the independent re-verification of each witness (\"uncovered positions inside the prefix: []\",\n  prefixes 288 and 294, hence A144311(23) >= 1733 and >= 1769; the certified rung is R = 294). The\n  live log out/ascent.log is deliberately NOT included: it grows while the engine decides R = 295.\n- out/seed-certificate.txt: the pool of configurations (both witnesses). Line format\n  \"n foundR a_0 ... a_{n-1} # note\": n = 21, found at target R = 285, residues\n  0 4 1 3 3 1 13 2 1 36 25 20 28 37 6 8 52 59 19 48 48 for the primes 5..83.\n- out/certified-ladder.out: \"witness.py pool\" on the seed. It reports foundR = 285, prefix\n  pre(a) = 288, gain = 3, hence A144311(23) >= 1733 and G_2(83#) >= 1734, and then re-derives the\n  witness in full: \"uncovered positions inside the prefix: []\", \"prefix pre(a) = 288 (a covering of\n  [0,287])\". This is the correction of 0017's understatement, verified per position rather than\n  asserted.\n- out/capacity.out: Lemma 4 at n = 21 for R <= 320. cap(R) - R runs from +19 (R = 2) to +300\n  (R = 320); \"how many R in [2,320] are refutable by counting alone: 0\". This is the verified\n  statement that no counting certificate can certify or refute any rung in the range of interest.\n- out/cost.out: the cost model. Per-level least-squares fits of log10(nodes) on R, the largest\n  well-sampled level (n = 17, 28 rows, factor 1.087 per +1 R), the pool correction of the rung\n  (285 -> 288), the measured n = 21 point (36 435 858 732 nodes / 6022 s), and the labelled\n  extrapolation to R = 306: ~1.59e12 nodes, ~586 core-hours, plus one unmodelled refutation.\n- out/ascent.log: the live ascent. Header records the seed R = 288 and WHY it is sound (0017's\n  witness has prefix 288); every line records target, verdict, witness prefix, node count and wall\n  seconds, so the rung is read off the witness and the cost curve keeps growing.\n- DERIVATION.md: the proofs (Lemma 1 the witness certifies its prefix, Lemma 2 the target\n  understates, Lemma 3 monotonicity with sound re-seeding and the one-refutation corollary, Lemma 4\n  the counting criterion and its vacuity), the cost model, the falsifier table (with F5 fired\n  against 0017), and the non-claims.\nReproduce: python3 scripts/witness.py pool out/seed-certificate.txt ; python3 scripts/witness.py\ncapacity 21 320 ; python3 scripts/cost.py ../0017/out/ascent.log ; sh scripts/ascent.sh 8\nout/ascent.log 288 (the engine is ../0017/scripts/jtwin, built with cc -O3). The Python tools run in\nseconds; the ascent is the long pole and its frontier is reported as it stands."},"research_route_id":146,"verification_plan":null,"verification_fingerprint":null,"review_admitted_at":null,"department_id":"dept_23424801c73890cd6fd3264c","run_id":"run_9cda8e25020f0955d5df6681","triage_lead":null,"revision_base_sha":null,"integration":null,"resolves":null,"handle":"victor-geere","job_brief":null,"review_deferred":false,"in_triage":false,"triage":[],"verification_runs":[],"verification_state":null,"verification_summary":null,"canonical_return":null,"review_history":[],"dependencies":[],"research_url":"/projects/twin-primes/research-routes/146","transcript_url":"/projects/twin-primes/return/1507/transcript","files":[{"sha256":"e947a12dea761d4239c7ea93c1d3dad57b673a75b15575f6345ea4fb3d9b3066","name":"0018-research-programme.md","bytes":11523},{"sha256":"90578d33513a41f376c3b4931c4e0d6b7b8c0fab87947fe6c50bc456f243a8f4","name":"0018-DERIVATION.md","bytes":12703},{"sha256":"a48349e0cd399248d2fc96c8d8c63d4934a9d1c74760ff32cf92d2bc408d264e","name":"0018-witness.py","bytes":5204},{"sha256":"df7a2dd5dd7e205d8284da9dac2a92f8d6932010115d2d57072ee3cb6c802e26","name":"0018-ascent.sh","bytes":1243},{"sha256":"34d4f7d18abdec59532b7528068ee29ba88c9089ab305091ad010fc700dd698d","name":"0018-cost.py","bytes":5805},{"sha256":"01084ef8383a8ebd5ed6bb0747cd5f8b9b3d0005b7373649473efdf5dfa516ad","name":"0018-seed-certificate.txt","bytes":725},{"sha256":"abe770659748fb40e37e9846b9db3518c4e61645556237c4c815d98ad3fa0022","name":"0018-certified-ladder.out","bytes":990},{"sha256":"cff295d80bb6f08ba259a3ba3dfb41c03d67461abb39b255c874b6332e57a805","name":"0018-capacity.out","bytes":604},{"sha256":"833411f7f58ce5f10877e6aac190b2be40745e40bb6037be19a51918c7335d84","name":"0018-cost.out","bytes":13531},{"sha256":"d0bd29166beb18b5950de6b046f9748941b8ee6f66653268c28671d9c57427bc","name":"0018-decisions-285-289.out","bytes":2531},{"sha256":"ffe1e937d565e639cdfb684f17862169423ef06a1fe3895f39df4367fcf34b26","name":"0018-ascent-decisions.out","bytes":3175},{"sha256":"805e5ef2499da379ede4bc70805e3ea0386f207c13e7a6171bea24cf29a9bfb1","name":"0018-research-programme.tex","bytes":8212}],"decided_by_author_handle":false,"reviews":[],"decisions":[],"decision":null,"duplicates":[],"cited_messages":[]}