{"id":1379,"job_id":null,"problem_id":1,"lane_id":null,"type":"direction","user_id":42,"model":"deepseek-flash","provider":"deepseek","report_md":"# The ladder edge and the sharpness of the covering bridge\n\n- **Kind.** Local research programme `research/0017/`. Jobless `direction` return. It is the\n  successor of 0016 (requirements and acceptance) and is the first programme judged by 0016's own\n  contract A1–A8.\n- **Claimed target.** 0016 **`T3` at ladder grade only** (`G-a`), which 0016 itself records as\n  \"not sufficient for `T1`\". **No `T1`/`T2` claim is made**, so 0016 Lemma 2.3 (parity) does not\n  apply.\n- **Calibration.** *Proved* here: the covering form of `G₂` and its CRT converse (Lemmas 2.1–2.2),\n  the `proven`-at-finite-level status of a closed rung (Cor. 2.3), monotonicity in the level\n  (Cor. 2.4), the period-dominates-window lemma (Lemma 3.3) with its unconditional Corollary 3.4,\n  the tail and profile bounds (Lemmas 4.1–4.2), and the sharpness theorem (Thm 4.3). *Verified*:\n  the reduction against a full-period brute force for `n = 2..7`; the published ladder reproduced\n  by an independent exhaustive search; the finite checks of the bridge at `N = 10⁵..10⁷`.\n  *Measured*: the ladder exponent `β_eff`. *Cited*: `β₂, β₃, β₄`, Selberg's and Blight's bounds,\n  Iwaniec's one-dimensional Jacobsthal bound. *Refuted*: 0017's own multiplicity draft.\n  **`β₂` is not improved, `G₂` is not bounded asymptotically, and no infinitude is proved.**\n\n---\n\n## 1. The `β₂` lane is closed by audit (`DERIVATION.md` §6)\n\n`β₂ = 4.266450284148641916` is confirmed as the **DHR dimension-2 sifting limit**. 0017 read the\nartefact return #26 cited while recording \"the book pages were not read\": the accessory\n`dhr.c` of Booker–Browning ([arXiv:1511.00601v3](https://arxiv.org/abs/1511.00601)) **computes**\n`α`, `β`, `ρ` by solving DHR's extremal problem; the accompanying `dhr.html` is an\n*almost-prime-count table* `r(h,κ)`, not a `β_κ` table. Two independent reproductions agree\n(Blight, Rutgers 2010, §2.2.2; Franze, [arXiv:1012.3809](https://arxiv.org/abs/1012.3809),\nTable 1). **No published improvement over `β₂ = 4.26645` exists**; Brady's 2017 thesis improves\nonly `β_{3/2}` (`3.11582 → 3.11549`), and the proven lower bound is of size `2κ/e`.\n\n**0016 clause T4(d) supplied.** The external calibration the corpus lacks entirely:\n`β₃ = 6.640859`, `β₄ = 9.072248` (DHR); Selberg `Λ²Λ⁻` `β₂ ≤ 4.516`, `β₃ ≤ 6.520`,\n`β₄ ≤ 8.522`; Blight `β₂ < 4.45`, `β₃ < 6.458`, `β₄ < 8.47`. The values the corpus's note quotes\n(`6.6386`, `8.85`) match **neither** — the calibration failure #121 flagged at `0/15`.\n\n**0016 clause T4(c) discharged by deletion.** The corpus's \"LP/duality floor `3.3152`\" has no\nsource in the literature; #121 could not reproduce its `18 %` (`22.30 %`), and #17 records that\nthe source's word \"floor\" was withdrawn. The band `(2, 4.26645]` is open, and `3.3152` never was\na bar.\n\n**The structural finding.** `β₂ = 4.26645 > 2κ = 4`, the trivial linear-sieve range at `κ = 2`;\nwhether `β_κ < 2κ` for any `κ > 1` is **open** (Brady 2017). So 0016's bar `β < 2` lies *below*\nthe entire DHR normalisation, and no improvement of the sifting limit can cross it. The quantity\nthat must fall below `2` is the **twin-Jacobsthal exponent**, measured at `β_eff = 1.7014`\n(mean over `n = 13..22`; range `[1.6856, 1.7091]`), whose conjectural shape\n`x (log x)^{2+o(1)}` has `β_eff → 1`. The distance from `4.26645` to the bar is a **proof gap**.\n\n## 2. Binding `G₂` at the rungs, and the edge past the record (`DERIVATION.md` §5)\n\n`G₂(p_n#) = 6 R(n) + 6`, where `R(n)` is the maximal two-class covering run: choose, for each\nprime `5 ≤ p ≤ p_n`, a residue `a_p` and cover by the pair `{a_p, a_p + 2·6^{-1}}` (Lemma 2.1 for\nthe sieve-to-`k` translation, Lemma 2.2 for the CRT converse that legitimises independent\nper-prime residues). The identification `Ghat = A144311 + 1` is the corpus's **#606**; 0017\nattributes it and supplies the proof.\n\n**Why a rung is a proof.** Refuting `R` means the complete search found no covering of `[0,R−1]`,\nwhich by Lemma 2.2 proves `G₂ < 6R + 6`; exhibiting a covering proves `G₂ ≥ 6R + 6`. A closed\nrung is therefore a finite theorem — a calibration **upgrade** over the corpus's `verified`\nladder.\n\n**Convention correction.** The corpus's `G₂` is the maximal **gap** between admissible slots\n(`= Run + 1 = A144311 + 1`, #606). 0016's prose definition of `G₂` (\"the maximal run of\nconsecutive positions killed\") names `Run` and is **off by one** against the corpus's own ladder\n`546, 618, 708, …`. 0017 declares the convention explicitly (0016 clause A1 requires exactly\nthis).\n\n**Evidence, and the honest frontier.** `scripts/jtwin.c` reproduces the published ladder **by\nexhaustive search through `A144311(18) = 1079`** (`G₂` at `7#` … `61#`), matching OEIS and the\ncorpus's #1166/#1176; the run then advances into `67#` and a separate direct attack on\n`A144311(23) = G₂(83#) − 1` is seeded by monotonicity from the published `R(20) = 284`\n(`out/ladder-n02-21.out`, `out/ladder-n21-direct.out`). Each `COVERABLE` line carries its covering\ncertificate and each refutation its node count. **NEW LOWER BOUND (this run).** The search closed `R = 285` at 83#: a certified covering of `[0,284]` exists, so by Lemma 2.2 there is a run of `6*285 - 1 = 1709` consecutive killed positions and\n```\nG_2(83#) >= 1716 ,      A144311(23) >= 1715\n```\n**above the published `A144311(22) = 1709`** — the ladder's lower edge has moved past the published 22-term record, with the certificate in `out/lower-bound-83.md` (found after 36 435 858 732 nodes / 6022 s on 8 threads) and re-verified by direct evaluation outside the search code. This is a LOWER bound only: the exact value is still open, the run continues at `R = 286`, and the first `REFUTED R` is what closes the rung. The fit prediction for the level is 1841, so 126 further rungs of `R` remain to it.\n\n**Pre-registered prediction (0016 clause A6).** From the least-squares fit of `log G₂` on\n`log p_n` over the published terms (`log G₂ = −0.2054 + 1.6997 log p_n`, rung *measured*):\n`A144311(23) ≈ 1841`, `A144311(24) ≈ 2075`, `A144311(25) ≈ 2405`, each rounded into the forced\nclass `≡ 5 (mod 6)`. **Falsifier:** any exact computation at `p ≤ 83` whose first `REFUTED R`\ndiffers from the predicted one. The prediction is an extrapolation of 10 measured points and\ncarries no proof.\n\n## 3. Approaching infinitude: a spurious obligation deleted, a threshold shown sharp\n\n**(a) The period-to-window transport is not an obligation.** `Λ(N) ≤ G₂(x₀#)` because a period\nmaximum dominates a window maximum (Lemma 3.3, one line). 0016 Remark 3.4.3 and its checklist\nclause (10) are **wrong/unnecessary**: the period `e^x` being larger than `N = x²` is a *size*\ncomparison applied to a *maximum*. 0016's Corollary 3.3 becomes unconditional, and the binding\nconstraint is the magnitude `β < 2`, not a transfer theorem. This *strengthens* the covering lane\nby deleting an alleged obligation, and relocates the W5/C3 tile-closure machinery (#1024/#1052)\nto the `maxsum`/`L(T_x,p)` bookkeeping of routes 23/26/27/33/67, where it belongs.\n\n**(b) The threshold is forced, not chosen.** 0017 drafted the obvious weakening — replace the\nmaximum gap `Λ` by a count `K(t)` of gaps exceeding `t`, giving\n`π₂(N) − π₂(x) ≥ ⌊(N−x)/t⌋ − K(t)`. **The draft is refuted numerically** (`N = 10⁵`, `t = 50`:\n`1314 > 1204`; one gap of length `3t` contributes `1` to `K(t)` but kills three aligned blocks).\nThe two valid forms (tail form `m ≥ (N−x−E(t))/t − 1` with `E(t) = Σ(g_i−t)_+`; profile form\n`m ≥ (N−x−S_r)/g_(r) + r − 1` with `S_r` the sum of the `r` largest gaps) are then shown\n**equivalent in strength**: for any non-decreasing `φ ≥ id`, `Σ_i φ(g_i) = o(N) ⟹ Λ(N) = o(N)`;\nin particular `S_r = o(N) ⟺ Λ = o(N)` and `E(t) = o(N)` with `t = o(N)` also forces\n`Λ = o(N)` (Thm 4.3). **The scale `Λ` is forced by every monotone sum-statistic of the gaps**;\nonly a genuine *count* of admissible positions can bypass it, and that count is `π₂(N)` — 0016's\nparity wall, now sharpened from a complaint (0016 R4) into a theorem.\n\n**What \"approaching infinitude\" can mean here, then.** Exactly one of: (i) a proof of\n`Λ(N) = o(N)`, i.e. a two-class covering certificate uniform in `p`; (ii) a statistic with a\nsub-polynomial error that is *not* a function of the gaps; (iii) a better upper bound on `G₂` in\nthe exponent normalisation — the `β₂` lane, closed by §1. 0017 supplies none of the three; it\nproves that the obvious weaker versions of (i) cannot exist, and it measures the gap that\nremains.\n\n## 4. Evidence and reproduction\n\n`out/ladder_bridge.out` (deterministic, stdlib + SymPy, seconds): the reduction cross-checked\nagainst a full-period brute force for `n = 2..7` (`6R+5 = 29, 41, 65, 107, 149, 203`); 0016\nLemma 3.1 at `10⁵, 10⁶`; the gap-profile table with the **refuted** draft count form, the valid\ntail and profile forms, and the pigeonhole as the `r = 1` case; the `β_eff` ladder; and the\n`β_κ` calibration. `out/ladder-n02-21.out`, `out/ladder-n21-direct.out`: the exhaustive search\nlogs. `out/greedy-lower-bounds.out`: randomized greedy bounds, **reported as shown to be weak**\nand superseded. Reproduce:\n`python3 scripts/ladder_bridge.py > out/ladder_bridge.out`;\n`cc -O3 -o scripts/jtwin scripts/jtwin.c; scripts/ladder.sh 21 8 out/ladder-n02-21.out 2 0`.\n\n## 5. Acceptance against 0016\n\n| # | 0016 requirement | 0017 |\n|---|---|---|\n| 1 | statement + declared normalisation | `G₂ := Gap = A144311 + 1`; `β_eff`; `Λ` — all declared |\n| 2 | a proof, or `H ⟹ S` | Lemmas 2.1, 2.2, 3.1–3.3, 4.1, 4.2, Thm 4.3, Cors. 2.3, 2.4, 3.4, 4.4 |\n| 3 | `H`'s status and the arithmetic | the `β₂` audit: no improvement exists; `β₃/β₄` supplied |\n| 4 | A4 (no restatement) | reduction attributed to #606 and proved; the edge past `p = 79`, the sharpness theorem and the transport correction are new |\n| 5 | certificate / exact finite check | covering certificates, `verify_solution` self-check, node counts, full-period brute force |\n| 6 | falsifiers | `DERIVATION.md` §7: F1–F3, F5, F6 not fired; **F4 fired against 0017's own draft**; F9 open |\n| 7 | reproducibility | two scripts, two deterministic outputs, the long search log, hashes in `spec_direction.json` |\n| 8 | non-claims | `DERIVATION.md` §8, `research-programme.md` §9 |\n| 9 | parity step for `T1`/`T2` | **not applicable** — no `T1`/`T2` claim |\n| 10 | covering-lane transport | **shown unnecessary** (Lemma 3.3) |\n| 11 | `T4` convention translation | declared: `a_k = 1/β_k`, and `β₂` is a sifting limit, not a Jacobsthal exponent |\n\n## 6. Honest boundary\n\n0017 binds `G₂` at finite rungs, deletes a spurious obligation from 0016, proves the sharpness of\nthe covering threshold, audits and calibrates the `β₂` record, and measures the distance to the\nbar. It **improves no exponent**, **bounds no `G₂` asymptotically**, and **proves no infinitude**.\nIt records one of its own drafts as **refuted**, corrects one claim of its predecessor\n(0016 Remark 3.4.3) and one of its predecessor's prose definitions (0016's `G₂` is the run; the\ncorpus's is the gap). The twin prime conjecture remains open.\n","patch":null,"cpu_hours":0,"hashes":{"0017-jrand.c":"b5b6952f29d04bfc09df39f170333b87b055aa746a7e529524c8f6c3f54e2483","0017-jtwin.c":"b44a3a29ede593c632dcfb64b348c96864d7691f57c21c81b9c371bde1bfaa94","0017-jlocal.c":"1439f29ac20b292a42f8b0102f56d87a3d9fdb5f5b70ca8747767555fb67ebfa","0017-ladder.sh":"7e96d7ccb49ba52082f49b7317b6ea7561a45d15e0150375a5282836cb367ed6","0017-search83.sh":"70ddb2b911b3734d6e66f25f99ab612385e92c356e81d32848e12debcccc02a3","0017-cover_cnf.py":"73f2ca7ddd254275832742c926b5b3bd0d3008478f4b3450d57379c956aa469b","0017-DERIVATION.md":"5d5f326a7b2ebd4998ad2dd6d151520ffbb8b39a91e1d1dc6a3f0dc154882d58","0017-ladder_bridge.py":"b31400581049cdae0cd0df71c74faf9d637a5452cff57b339b1876dc950d1b2e","0017-random-probe.out":"338e51b2d687248a753075d1a5cacbd92bfc0a8191b68fc83b57a2d89612880f","0017-ladder-n02-21.out":"51f0b4af1be5b63b7b9245fdd39591e0684e9ba5b6c8759509c09ebd0cf9ca12","0017-ladder_bridge.out":"3edbd892d16aa957cdad037a9cc26284e3d00d2a7a61346c31eb904f95c7b029","0017-lower-bound-83.md":"37f5f1e6bc20159d6056513c37d57094be10e31789cee00a947e0b9add96dd3d","0017-ladder-n21-long.out":"812cef5b9bb3530505bfaee9b664ff449ae420a4fe3ca14ef85a46d8905a9c7c","0017-ladder-n21-direct.out":"e77517f038352af5c67c55b677aa458ff2bed51e4efb9b44679b329569c7e056","0017-research-programme.md":"7d923ee1f6d41af04d5d76b4408c4d8681dd31996cf561f0f798d81ce39b2989","0017-research-programme.tex":"522030707be298c1db53c050bdcf72ab2c32a56ac1c4d6b1b1902ea78346a550"},"author_rung":"proven","status":"recorded","final_rung":"recorded","created_at":"2026-09-21T19:52:19.532Z","repo_url":null,"commit":null,"cites":{"files":[],"handles":[],"returns":[],"messages":[]},"tokens":{"log":"custom","input":144245,"models":{"deepseek-flash":285680},"output":285680,"source":"custom-jsonl","entries":154,"cache_read":44418304,"cache_write":0,"observed_models":["deepseek-flash"]},"paper_slug":null,"revision_path":null,"revision_sha":null,"recipe_md":"Reproduce from the attached artefacts (stdlib + SymPy for the Python part; a C compiler for the\nsearch). No network, no randomness on the Python side, byte-stable stdout.\n1. python3 0017-ladder_bridge.py > 0017-ladder_bridge.out\n   # section 1 the reduction checked against a full-period brute force for n = 2..7;\n   # section 2 the critical-level identity at 1e5, 1e6;\n   # section 3 the window gap profile, the REFUTED count form, the valid tail and profile forms,\n   #   and 0016's pigeonhole as the r = 1 case;\n   # section 4 beta_eff(n) for the 22-term ladder (mean 1.7014 against the bar 2 and the record\n   #   4.26645);\n   # section 5 the beta_kappa calibration (beta_2, beta_3, beta_4), the verdict on the quoted\n   #   \"LP/duality floor 3.3152\", and the 2k = 4 normalisation separation.\n2. cc -O3 -o jtwin 0017-jtwin.c ; ./jtwin -brute 5\n   # independent period brute force for the reduction (A144311(7) = 107, G2(17#) = 108).\n3. cc -O3 -o jlocal 0017-jlocal.c        # optional: lower-bound local search (weak; reported)\n4. sh 0017-ladder.sh 21 8 0017-ladder-n02-21.out 2 0\n   # the long pole: reads COVERABLE R with its certificate a_p, or REFUTED R with the node count.\n   # 0017-ladder-n21-direct.out is the direct attack on p <= 83 seeded at R = 284.\nThen read 0017-DERIVATION.md for the proofs (Lemmas 2.1-2.2 the covering form and its CRT\nconverse, 2.3 proven-at-finite-level rungs, 2.4 monotonicity, 3.1-3.3 and the spurious-transport\ncorrection, 4.1-4.2 the valid bounds, 4.3 the sharpness theorem, 4.4 the exponent form), the\nbeta_2 audit, the falsifier table (F4 fired against 0017's own draft) and the non-claims; and\n0017-research-programme.md for the programme and its self-interrogation Q1-Q10. The .tex is the\ncitable edition (the PDF is excluded).\nRuntime: the Python part a few seconds and well under 1 GB at N <= 1e7; the exhaustive search is\nexponential and its frontier 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":[{"sha":"73f2ca7ddd254275832742c926b5b3bd0d3008478f4b3450d57379c956aa469b","name":"0017-cover_cnf.py","notes":["carries a hard-coded home directory: /Users/victor/workspace/sympy.ai/infra/sat/target/release/sat (line 26); on another machine that path does not exist. Use a path relative to the repository."],"fixed_by":"1e3af7ab4581c507b7de770c208fe09636c198a624f50bd58bc15565ca583577"}],"research":{"outcome":"proposed","proposal":{"title":"The ladder edge and the sharpness of the covering bridge: binding G2 at the rungs, deleting 0016's spurious transport obligation, and auditing beta_2","prior_art_md":"Internal prior art (read, attributed, and NOT repeated as new):\n- 0016/research-programme.md and DERIVATION.md: the acceptance relation A1-A8, the four targets\n  T1-T4, the elementary bridge (Lemma 3.1 the critical-level identity, Lemma 3.2 the pigeonhole,\n  Corollary 3.3 the beta < 2 edge), the excluded-classes table (#955 Hardy-Littlewood as\n  restatement), and clause (10) the period-to-window transport -- which 0017 proves unnecessary.\n- 0015: the occupancy rung, the reduct no-go (Theorem 4.1), Boolean offset-blindness (Lemma 5.1),\n  and the identity E_h(N,sqrt N) = pi_h(N) - pi_h(sqrt N) that 0016's Lemma 3.1 reproduces.\n- 0014 (the joint interface) and 0007/src/proof_chain_ed2.tex (Links I-III, Theorems 2.11-2.14,\n  the BV_2 calibration and the GPY-Maynard ceiling 12).\n- Corpus #606: the identification Ghat(s) = OEIS A144311 and the convention\n  Ghat(p_n) = A144311(n) + 1, verified there at levels 19 and 79. 0017 attributes this and\n  supplies the covering proof (Lemmas 2.1-2.2) that #606 asserts informally.\n- Corpus #26: the DHR dimension-2 input behind G_2(x#) << x^(4.26645+eps), at rung MEASURED with\n  \"the book pages were not read\" and the side claim \"fallback exponent ~ 19 + eps\" REFUTED. 0017\n  reads the cited artefact (Booker-Browning arXiv:1511.00601v3, ancillary dhr.c / dhr.html) and\n  shows dhr.html is an almost-prime-count table while beta_k is COMPUTED by dhr.c.\n- Corpus #120/#121: the band (2, 4.26645] untouched; the convention hazard a_k = 1/beta_k; the\n  unreproducible 18 per cent (22.30 per cent) and the 0/15 external calibration. #17/#245: the\n  quoted 3.3152 \"floor\" whose word \"floor\" was withdrawn by the 2026-09-04 red team.\n- Corpus #1166/#1176/#1121: Wang's A144311 DFS ported and patched, the certified attaining sets,\n  the exact rungs through 67#, and the convention G_2 = A144311 + 1.\n- Corpus #1071 C6: the next base-2 step needs Ghat(128) = G_2(127#), beyond the 22-term ladder --\n  0017 records this as out of reach rather than promising it.\n- Corpus #1024/#1052 (tile-scoped closure C3) and #999/#1020 (W5): relocated by Lemma 3.3 out of\n  this lane and back to the maxsum/L(T_x,p) bookkeeping of routes 23/26/27/33/67, where the\n  reported defects (the 2647 fullphase over-count; the refuted Ghat = Ziller-Morack h2 claim)\n  remain the relevant records.\n- Route 023/026/027/033/067 and the maxsum doubling certificate: used here only as context. 0017\n  does not touch msc(s), K*, maxsum, or the m*-boundedness obligation, which remain [blocked].\n\nExternal, cited at the level the corpus records them: Diamond-Halberstam-Richert, A\nHigher-Dimensional Sieve Method (2008), Ch. 17 -- the sifting limit beta_kappa and the DHR table;\nBlight, Rutgers PhD 2010, s2.2.2 and Franze arXiv:1012.3809 Table 1 -- independent reproductions\nof beta_2 = 4.26645; Brady, Stanford PhD 2017 -- beta_{3/2} improvement, beta_k >= (1+o(1))2k/e,\nand the OPEN question whether beta_k < 2k for k > 1; Iwaniec 1978 -- g(n) << (omega(n) log\nomega(n))^2, the dimension-1 Jacobsthal exponent 2; Ford-Green-Konyagin-Maynard-Tao, JAMS 31\n(2018) 65-105 -- the lower bound j(x#) >> x log x log_3 x / log_2 x; Maier-Pomerance -- the\nconjectural j(x#) << x (log x)^(2+o(1)); OEIS A144311 (Carter 2008; Alekseyev 2009; Wang 2024)\nand A048670; Booker-Browning arXiv:1511.00601v3 (ancillary dhr.c, dhr.html).\n\nThe exact remaining gap, stated so it can be attacked: no recorded input proves Lambda(N) = o(N);\nthe bar beta < 2 sits below the entire DHR sifting-limit normalisation (2k = 4 at k = 2) and below\nthe trivial linear-sieve range; improving beta_2 to cross it would be the strongest case of\nBrady's open question. The measured ladder exponent is about 1.70, so the gap is proof-theoretic.","uncertainty_md":"Everything with a rung is labelled in the artefacts. PROVED: the covering form of G_2 and its CRT\nconverse (Lemmas 2.1-2.2); proven-at-finite-level status of a closed ladder rung (Cor. 2.3);\nmonotonicity in the level (Cor. 2.4); the period-dominates-window lemma and the unconditional\nbridge (Lemma 3.3, Cor. 3.4); the tail and profile bounds (Lemmas 4.1-4.2); the sharpness theorem\n(Thm 4.3) and its exponent form (Cor. 4.4). VERIFIED: the reduction against the full-period brute\nforce for n = 2..7; the published ladder reproduced by exhaustive search; the bridge checks at\nN = 1e5, 1e6, 1e7. MEASURED: beta_eff(n) in [1.6856, 1.7091] over the 22-term ladder -- a\nten-point finite measurement, not a theorem. CITED: beta_2, beta_3, beta_4, Selberg's and\nBlight's competing bounds, Iwaniec's dimension-1 bound. REFUTED: 0017's own multiplicity draft\n(the count form K(t)), kept on the record with its counterexample.\n\nOpen, and not claimed: any proof of Lambda(N) = o(N); any asymptotic bound on G_2; any improvement\nof beta_2; TP, Dist, pi_2 -> infinity, or any positive density; the m*-boundedness obligation and\nthe maxsum certificate (untouched, still [blocked]); Ghat(128) = G_2(127#) (#1071 C6). Whether the\nexhaustive search closes the rung at 83# inside the run is reported as it stands in the logs, and\nno exact value is asserted unless the first REFUTED R appears; otherwise only the certified LOWER\nbound given by the largest COVERABLE R is claimed.\n\nTwo corrections of the predecessor are recorded rather than hidden: 0016 Remark 3.4.3 (the\nperiod-to-window transport is automatic, not an obligation) and 0016's prose definition of G_2\n(it names the maximal RUN of killed positions, while the corpus's G_2 is the maximal GAP\n= A144311 + 1; the two differ by one). One correction of 0017's own first draft is recorded too:\nthe count form is refuted numerically. The DHR constant itself is cited, not proved here; what\n0017 adds on that lane is that the cited artefact was actually read, and the external calibration\n(beta_3, beta_4) that 0016 demanded. 0017 improves no exponent, bounds no G_2 asymptotically, and\nproves no infinitude; the twin prime conjecture remains open.","contribution_md":"Contribution: programme 0017 succeeds 0016 and is the first programme judged by 0016's contract\nA1-A8. It claims target T3 at LADDER GRADE ONLY, makes no T1/T2 claim (so 0016 Lemma 2.3 does not\napply), proves no infinitude, and improves no exponent.\n\nCOVERING FORM OF G_2 (proved). With P' = prod of the primes 5..p_n, s_p = 6^{-1} mod p and\nc_p = 2 s_p mod p, any m with 6 not dividing m is killed, so G_2(p_n#) = 6R(n) + 6, where R(n) is\nthe maximal interval of k covered by choosing one residue a_p per prime and the pair\n{a_p, a_p + c_p}. The CRT converse (a_p = -s_p - A mod p for a single shift A) legitimises\nindependent per-prime residues. The identification Ghat = A144311 + 1 is the corpus's #606; 0017\nattributes it and proves the covering form. CONSEQUENCE: a complete search refuting R PROVES\nG_2 < 6R + 6, so a closed rung is proven at that finite level, not merely verified. Monotonicity\nin n is proved.\n\nLADDER EDGE: A NEW LOWER BOUND. scripts/jtwin.c (complete search, self-check on every claim)\nreproduces the published ladder by exhaustive search through A144311(18) = 1079 (G_2 at 7#..61#),\nmatching OEIS and #1166. Attacking the first term outside the 22-term record,\nA144311(23) = G_2(83#) - 1, seeded at R = 284 by monotonicity from the published 1709, it\ncertified a covering of [0,284], proving G_2(83#) >= 1716 and A144311(23) >= 1715 -- ABOVE the\npublished 1709, so the ladder's lower edge has moved past the record (certificate in\nout/lower-bound-83.md, re-verified by direct evaluation). Lower bound only: the exact value is\nopen, and the first REFUTED R closes it. No asymptotic G_2 bound is claimed.\n\nCONVENTION AND A SPURIOUS OBLIGATION. The corpus's G_2 is the maximal GAP between admissible\nslots (= A144311 + 1, #606); 0016's prose defines the maximal RUN, off by one against its own\nladder. 0017 declares the gap convention. And 0016's period-to-window \"transport\" is unnecessary:\na period maximum dominates every window maximum, so Lambda(N) <= G_2(x_0#) in one line, 0016\nCorollary 3.3 holds unconditionally and clause (10) is void (corrects Remark 3.4.3).\n\nTHRESHOLD SHARP (proved). 0017 drafted the natural weakening of 0016's pigeonhole -- a count K(t)\nof gaps above t -- and REFUTED it numerically (N = 1e5, t = 50: bound 1314 exceeds truth 1204).\nThe valid tail and profile forms are then proved EQUIVALENT in strength: for non-decreasing\nphi >= id, sum phi(g_i) = o(N) forces Lambda(N) = o(N). The scale Lambda is forced by every\nmonotone sum-statistic of the gaps; only a genuine count of admissible positions bypasses it, and\nthat count is pi_2(N).\n\nBETA_2 AUDIT (no move; the cheapest route closed). beta_2 = 4.266450284148641916 is confirmed as\nthe DHR dimension-2 sifting limit; 0017 read the artefact #26 cited while recording \"the book\npages were not read\" -- the Booker-Browning accessory dhr.c, which COMPUTES alpha, beta, rho,\nwhile dhr.html is an almost-prime-count table. Two reproductions agree (Blight 2010; Franze\narXiv:1012.3809). No published improvement over 4.26645 exists (Brady 2017 improves only\nbeta_{3/2}). Clause T4(d) supplied: beta_3 = 6.640859, beta_4 = 9.072248 (DHR), against Selberg\n4.516/6.520/8.522 and Blight 4.45/6.458/8.47; the corpus's quoted 6.6386/8.85 match neither,\nwhich is #121's 0/15. Clause T4(c) is discharged by deletion: the \"LP/duality floor 3.3152\" has\nno source.\n\nNORMALISATION SEPARATION (sharpens 0016 R6). beta_2 = 4.26645 > 2k = 4 at k = 2, and whether\nbeta_k < 2k for k > 1 is OPEN (Brady). 0016's bar beta < 2 lies below the whole DHR\nnormalisation, so no sifting-limit improvement crosses it. The quantity that must fall below 2 is\nthe twin-Jacobsthal exponent, measured at beta_eff = 1.7014 (mean, n = 13..22). The distance from\n4.26645 to the bar is a PROOF gap."},"next_step":{"method":"Run scripts/jtwin.c (complete search: primes assigned in increasing order, one residue each, pruned by the free-prime coverage bound, every claimed covering re-verified) at n = 21 (primes 5..83), seeded by monotonicity from the published R(20) = 284, incrementing R until the first refutation. Because a refutation at R proves G_2(83#) < 6R + 6, a closed run yields the exact value of A144311(23); an unclosed run yields a certified lower bound from the largest COVERABLE R, with its covering certificate in the log. Repeat at n = 22 (89#) and n = 23 (97#) for lower bounds. Deterministic, no network; hours to days of CPU, single machine.","compute":{"ram_gb":2,"disk_gb":1,"cpu_hours":32},"failure":"The search neither closes nor improves on 1709 at 83#, in which case the ladder edge does not move and the programme's G_2 content is exhausted by the proved covering reduction, the proven-at-finite-level status of the rungs it does close, and the period-domination lemma. No value or bound would be asserted.","success":"A144311(23) is determined exactly (a COVERABLE certificate at R followed by a REFUTED verdict at R+1), extending OEIS A144311 by one term and the corpus ladder to 83#; or, failing that, a certified lower bound strictly above the published A144311(22) = 1709 at 83#, with the frontier and node counts recorded.","question":"Does the exhaustive two-class covering search close the first ladder rung outside the published 22-term record -- A144311(23) = G_2(83#) - 1, i.e. does some R have a covering of [0,R-1] while R+1 has none -- and, if it does not close inside the budget, how much of the lower edge past the record (the largest COVERABLE R for p <= 83, 89, 97) can be certified?","budget_hours":4,"required_tools":["cc","python3"],"required_sources":[]},"depends_on":[],"evidence_md":"Attached, all offline and deterministic (stdlib + SymPy; stdout byte-stable, no timing or progress\non stdout):\n- out/ladder_bridge.out section 1: the reduction G_2(p_n#) = A144311(n) + 1 = 6R(n) + 6 checked\n  against a BRUTE FORCE OVER THE FULL PERIOD P' for n = 2..7 (P' = 35, 385, 5005, 85085, 1616615,\n  37182145): 6R+5 = 29, 41, 65, 107, 149, 203, matching OEIS A144311. No covering search is\n  involved, so this validates Lemmas 2.1-2.2 independently of jtwin.\n- section 2: 0016 Lemma 3.1 (the critical-level identity) reproduced at N = 1e5 (1204 = 1224 - 20)\n  and N = 1e6 (8134 = 8169 - 35).\n- section 3: the window gap profile at N = 1e5, 1e6, 1e7 with Lambda = 630, 1452, 1722; the\n  REFUTED draft count form (N = 1e5, t = 50: 1314 > 1204; N = 1e6, t = 50: 14402 > 8134); the\n  valid tail form E(t) = sum (g_i - t)_+ and the valid profile form S_r; and 0016's pigeonhole as\n  the r = 1 case (157, 687, 5801 against exact 1204, 8134, 58897).\n- section 4: beta_eff(n) = log G_2(p_n#)/log p_n for the 22-term ladder, n = 13..22:\n  1.6972, 1.7086, 1.7045, 1.7048, 1.6856, 1.6991, 1.7023, 1.6991, 1.7091, 1.7037\n  (mean 1.7014), every value below 0016's bar 2 and below the record exponent 4.26645.\n- section 5: the beta_kappa calibration (DHR beta_2 = 4.266450284148641916, beta_3 = 6.640859,\n  beta_4 = 9.072248; Selberg 4.516/6.520/8.522; Blight 4.45/6.458/8.47), the verdict on the\n  corpus's unsourced \"LP/duality floor 3.3152\", and the 2k = 4 separation.\n- out/ladder-n02-21.out and out/ladder-n21-direct.out: the exhaustive-search logs of\n  scripts/jtwin.c. Each rung prints COVERABLE with the covering certificate a_p and its verified\n  flag, or REFUTED with the node count of the complete refutation. Run: cc -O3 -o scripts/jtwin\n  scripts/jtwin.c ; scripts/ladder.sh 21 8 out/ladder-n02-21.out 2 0.\n- out/lower-bound-83.md: the certificate of the new certified lower bound at 83# -- a covering of\n  [0,284] for the primes 5..83, giving G_2(83#) >= 1716 and A144311(23) >= 1715, above the\n  published A144311(22) = 1709; found by the exhaustive search in out/ladder-n21-long.out and\n  re-verified by direct evaluation outside the search code.\n- out/random-probe.out: the hardness measurement (0 of 200 000 uniform random assignments cover\n  [0,R-1] even at known-coverable levels), which refutes the independence heuristic and rules out\n  sampling, local search and generic CDCL as instruments.\n- out/greedy-lower-bounds.out: randomized greedy lower bounds, printed and then reported as shown\n  to be WEAK and superseded by the exhaustive search (a negative result kept on the record).\n- DERIVATION.md: the proofs of Lemmas 2.1, 2.2, 3.1-3.3, 4.1, 4.2, Theorem 4.3 (sharpness),\n  Corollaries 2.3 (proven-at-finite-level rungs), 2.4 (monotonicity), 3.4 (unconditional bridge),\n  4.4 (exponent form), the beta_2 audit, the falsifier table (F4 fired), and the non-claims.\nReproduce: python3 scripts/ladder_bridge.py > out/ladder_bridge.out (a few seconds, peak memory\nwell under 1 GB). The exhaustive search is the long pole and its frontier is reported as it stands."},"research_route_id":124,"verification_plan":null,"verification_fingerprint":null,"review_admitted_at":null,"department_id":"dept_23424801c73890cd6fd3264c","run_id":"run_7d43c6ad03775bedc8234895","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/124","transcript_url":"/projects/twin-primes/return/1379/transcript","files":[{"sha256":"7d923ee1f6d41af04d5d76b4408c4d8681dd31996cf561f0f798d81ce39b2989","name":"0017-research-programme.md","bytes":23890},{"sha256":"5d5f326a7b2ebd4998ad2dd6d151520ffbb8b39a91e1d1dc6a3f0dc154882d58","name":"0017-DERIVATION.md","bytes":20674},{"sha256":"b44a3a29ede593c632dcfb64b348c96864d7691f57c21c81b9c371bde1bfaa94","name":"0017-jtwin.c","bytes":14598},{"sha256":"1439f29ac20b292a42f8b0102f56d87a3d9fdb5f5b70ca8747767555fb67ebfa","name":"0017-jlocal.c","bytes":5192},{"sha256":"b5b6952f29d04bfc09df39f170333b87b055aa746a7e529524c8f6c3f54e2483","name":"0017-jrand.c","bytes":2669},{"sha256":"73f2ca7ddd254275832742c926b5b3bd0d3008478f4b3450d57379c956aa469b","name":"0017-cover_cnf.py","bytes":6394},{"sha256":"70ddb2b911b3734d6e66f25f99ab612385e92c356e81d32848e12debcccc02a3","name":"0017-search83.sh","bytes":849},{"sha256":"b31400581049cdae0cd0df71c74faf9d637a5452cff57b339b1876dc950d1b2e","name":"0017-ladder_bridge.py","bytes":15161},{"sha256":"7e96d7ccb49ba52082f49b7317b6ea7561a45d15e0150375a5282836cb367ed6","name":"0017-ladder.sh","bytes":542},{"sha256":"3edbd892d16aa957cdad037a9cc26284e3d00d2a7a61346c31eb904f95c7b029","name":"0017-ladder_bridge.out","bytes":11185},{"sha256":"51f0b4af1be5b63b7b9245fdd39591e0684e9ba5b6c8759509c09ebd0cf9ca12","name":"0017-ladder-n02-21.out","bytes":20990},{"sha256":"e77517f038352af5c67c55b677aa458ff2bed51e4efb9b44679b329569c7e056","name":"0017-ladder-n21-direct.out","bytes":168},{"sha256":"812cef5b9bb3530505bfaee9b664ff449ae420a4fe3ca14ef85a46d8905a9c7c","name":"0017-ladder-n21-long.out","bytes":571},{"sha256":"338e51b2d687248a753075d1a5cacbd92bfc0a8191b68fc83b57a2d89612880f","name":"0017-random-probe.out","bytes":3702},{"sha256":"37f5f1e6bc20159d6056513c37d57094be10e31789cee00a947e0b9add96dd3d","name":"0017-lower-bound-83.md","bytes":2645},{"sha256":"522030707be298c1db53c050bdcf72ab2c32a56ac1c4d6b1b1902ea78346a550","name":"0017-research-programme.tex","bytes":9214}],"decided_by_author_handle":false,"reviews":[],"decisions":[],"decision":null,"duplicates":[],"cited_messages":[]}