{"id":1848,"job_id":1291,"problem_id":1,"lane_id":3,"type":"explore","user_id":1,"model":"claude-opus-5-5","provider":"anthropic","report_md":"# Job #1291 (pursue route 8): split-D51 is infeasible, with an exact integer Farkas certificate\n\n**Outcome: result.** #562's step was run as prescribed and succeeded. The frozen split-D51 system (#453's model: 107572 columns, 3939 equalities, 5091 conditioned rows; anchors 101/103 common, 17 ordinary singleton vectors split into per-star copies, #1086's 36 blocks) has an exact integer Farkas certificate `cert1291.json` (sha256 `26ca59e8...970a`). A stdlib checker verifies it in 0.4 s. Range: that one frozen instance. It does not give an exponent, a uniform-in-p rule or any statement about H_alpha or twin-prime infinitude.\n\n## What was run\n\n1. **Bounded Farkas search LP.** GSW 2016 §4.1 eq. (3), assembled and optioned exactly as #462's `farkas1097b.py`, via scipy 1.13.1 `linprog(method='highs-ds')`, 1 thread. Result: status 0 (HiGHS Optimal), objective 1.0000000000000004, **165 CPU s**. #462 measured 284 CPU s. The optimum was kept this time (`farkas_opt1291.npz`, local; not needed to check anything below). The first run stopped after step 2 on a Python 3.9 `write_text(newline=)` incompatibility in my driver. Steps 2-4 were redone from the kept optimum (`--reuse`, 0.6 CPU s). `solvelog1291.txt` is the solve's own log.\n2. **S1 rounding at T = 1e14** (`rint(max(y,0)T)`, `rint(zT)`). Exact `split1090.verify()` gives δ = max_j c_j = **13** and f·z = 100000000000001. #462's audit had δ = 10 at the same scale. The difference comes from a different optimal vertex on a different scipy/HiGHS. It is O(1), as #562 predicted, not \"far larger\", so the failure mode did not fire.\n3. **Shift (#562's lemma).** u = `u1111.json` (sha `896ea25a...`, f·u = 108, E^T u >= 1 on every column). Since f·z = 1e14+1 > 108·13 = 1404, set z' = z − 13u.\n4. **Result:** max combined coefficient **0** (107571 columns strictly negative, 1 at exactly 0), f·z' = **99999999998597 > 0**, y >= 0. That is `verify()['ok'] = true`.\n\nWhy this is a proof: for any w >= 0 with Ew = f and Aw >= 0, f·z' = z'^T E w <= −y^T A w <= 0, since (A^T y + E^T z')_j <= 0 and y >= 0. This contradicts f·z' > 0.\n\n## Independent check (cheapest credible check)\n\n`check1291.py` is stdlib only (no numpy, scipy or solver). Correction to #562's recipe: **`check1090.py` cannot be run \"unchanged\" on a new certificate.** It has no input for one. It verifies only #451's control certificate, the failed transport and `ds1090.json`. So `check1291.py` executes `check1090.py` (sha256 pinned `a73e2921...`) verbatim up to its own `control on the OLD model` marker. That prefix contains its sha-pinned loaders, `build_model()` and `combined()`. The checker then calls `build_model(split=True)` and `combined()` on the certificate. The model and the arithmetic therefore come from #453's reviewed checker, not from the solver-side builder that produced the certificate. The two builders agree on every row label (checked).\n\nChecks, 14/14 ok:\n- dimensions 107572 / 3939 / 5091\n- row labels equal the certificate's order\n- integer multipliers\n- y >= 0\n- max combined coefficient 0\n- f·z' > 0\n\nControls, all rejected as required:\n- a y entry set to −1\n- z negated\n- y zeroed (max 5.5e16)\n- **the unshifted S1 rounding z' + 13u: max 13, f·z = 1e14+1.** So the shift is what turns #462's rounding into a certificate.\n\n`check1090.py` itself was also rerun on its own artifact: 14 checks, 0 failures.\n\n## What this changes on the route\n\n#462 read split-D51 as infeasible at measured grade (solver objective). #562 made the certificate conditional on #462's two borrowed audit integers. The system is now **exactly infeasible**: a served integer object and a stdlib checker, with no borrowed numbers. #462's conclusion follows: with ordinary-prime singletons split per star and only the anchor singletons shared, the shared-anchor coherence alone already conflicts on N51. #562's general point is also confirmed on a fresh solve: rounding the vertex optimum always leaves an O(1) violation on tight columns (13 here), and one integer shift by a dominating row combination removes it.\n\n## Scope and what stays open\n\n- Finite: the frozen split-D51 instance built from `maps1086.json` (sha `ef8a0916...`).\n- No uniform construction of u or of the certificate in p, no compact dual rule, and no bound on certificate size (4207 nonzero y, all 3939 z nonzero, max |multiplier| 3.5e15). This is not a readable rule. The next step asks whether a sparse one exists.\n- Dependencies: #453 (builder and checker; status recorded, not accepted; its builder is anchored by reproducing #451's accepted certificate), #462 (auxiliary LP), #562 (shift lemma and u).\n\n## Prior art\n\nUpdated 2026-09-26 (`prior-art1291.md`). No located source certifies or states infeasibility of this or any pair-marginal coherence relaxation of a twin-prime phase cover. Tucker's Zenodo atlas (2026-09-23) is exact covering enumeration over primorial periods, not this LP. The shift method is the standard strict-margin correction (credited to Neumaier-Shcherbina 2004 in #562). No method novelty is claimed.\n\nCompute: 165 CPU s solve + ~3 s rounding and verification + 0.4 s check, about 0.05 CPU h against a 0.2 h hint. The tools the step named (python3, numpy, scipy) came from an existing department venv (numpy 2.0.2, scipy 1.13.1, CPython 3.9). All of #453/#462/#562's scripts were fetched by sha256 and used unmodified; only the driver `solve1291.py` and the checker `check1291.py` are new.\n\n45 of @Benjaminsen's returns wait for a verdict.\n","patch":null,"cpu_hours":0.05,"hashes":{"check1291.out":"718c20c3e4daa713f01a54879270ec83154740189bb1b468adbe9a73d6006b43"},"author_rung":"verified","status":"pending","final_rung":null,"created_at":"2026-09-26T17:35:26.474Z","repo_url":null,"commit":null,"cites":{"files":["28007cef45a1a1fc5642b207ca4c19c3325808add1a05684626e851091a40836","896ea25a40195b554a3ea35242dc40ebafcfd48a0cde4e1797e09766f291968e","a73e29212b0da4519d7024e8f19b8fd84c4fe555e37dceda8f231aa07da3655e","d4f29f39bcaba5e546e6079bc8c6380b2cd1f4b4d1825710041884a037f1fcf1","ef8a0916df05899f858e69bb67fa0f292b41416614ef87ad2ee9a869dbd424a1"],"handles":[],"returns":[451,453,462,562],"messages":[]},"tokens":{"log":"claude-code","input":134,"models":{"claude-opus-5-5":39515},"output":39515,"source":"claude-jsonl","entries":67,"cache_read":6434459,"cache_write":127794,"observed_models":["claude-opus-5-5"]},"paper_slug":null,"revision_path":null,"revision_sha":null,"recipe_md":"# Recipe: job #1291 (route 8)\n\nFetch every input from host-root `/files/<sha256>` into one directory. Put maps1086, global1086 and layout1086 in `in451/` as well.\n\n| file | sha256 | from |\n|---|---|---|\n| maps1086.json | ef8a0916df05899f858e69bb67fa0f292b41416614ef87ad2ee9a869dbd424a1 | #451 |\n| global1086.json | 28007cef45a1a1fc5642b207ca4c19c3325808add1a05684626e851091a40836 | #451 |\n| layout1086.json | b71ca9427970a1187f2178e5a58669a856bbca95c45a1d7cb1da719f27a731ab | #451 |\n| split1090.py | d4f29f39bcaba5e546e6079bc8c6380b2cd1f4b4d1825710041884a037f1fcf1 | #453 |\n| check1090.py | a73e29212b0da4519d7024e8f19b8fd84c4fe555e37dceda8f231aa07da3655e | #453 |\n| u1111.json | 896ea25a40195b554a3ea35242dc40ebafcfd48a0cde4e1797e09766f291968e | #562 |\n| cert1291.json, check1291.py, solve1291.py | this return | #1291 |\n\n## A. Check the certificate (decisive; stdlib only, ~0.4 s)\n\n```\npython3 check1291.py cert1291.json\n```\n\nExit 0. The last line has `\"verdict\": \"EXACT_FARKAS_SPLIT_D51_INFEASIBLE\"`, `\"max_combined_coefficient\": 0` and `\"normalization_multiplier_sum\": 99999999998597`, with 14 `ok` lines and no `FAIL`. Expected stdout is `check1291.out` in this return. The checker runs `check1090.py`'s own prefix (loaders, `build_model`, `combined`) verbatim, sha-pinned, so the model is #453's reviewed builder. Coverage: decisive for the frozen instance.\n\n## B. Regenerate the certificate (needs numpy + scipy; ~165-285 CPU s)\n\n```\npython3 solve1291.py --seconds 900 --method highs-ds > solve1291.out\npython3 check1291.py cert1291.json\n```\n\nHiGHS may return a different optimal vertex on another numpy/scipy version. Then δ (13 here, 10 in #462) and the certificate bytes differ, but `check1291.py` should still pass. Byte-for-byte reproduction of `cert1291.json` is not claimed across versions. Part A is the decisive check. Measured here: CPython 3.9, numpy 2.0.2, scipy 1.13.1, 1 thread, 165 CPU s. `--reuse farkas_opt1291.npz` redoes only the rounding and shift from a kept optimum.\n\nNo randomness; no seeds.","verification":null,"target":null,"finding":null,"human_md":null,"provisional":false,"effects_applied_at":null,"effort":"high","also_fix":null,"transcript_omitted":{"share":0.028985507246376812,"omitted":2,"outputs":69},"patch_hash":null,"superseded_by":null,"duplicate_of":null,"transcript_resubmitted_at":"2026-09-26T17:36:51.809Z","file_notes":null,"research":{"outcome":"result","route_id":8,"next_step":{"method":"On the same GSW auxiliary LP (solve1291.py assembly), fix f.z = 1 and minimise sum(y) (L1 on conditioned-row multipliers), then iteratively reweight (1/(y_r+eps)) 3-5 times. Record, per slot i and anchor phase a, how many conditioned rows [h,a,i] carry y > 0. Round, shift by u1111.json and certify each sparse candidate with check1291.py unchanged. Report the smallest certified support and its slot/phase distribution, and whether the same slots recur for both anchors.","compute":{"ram_gb":4,"disk_gb":1,"cpu_hours":0.5},"failure":"Every certified certificate needs more than 2000 conditioned rows spread over most of the 51 slots: then no compact rule is visible at this size and the route should not seek one at N51.","success":"A certified certificate with at most 500 nonzero y (from 4207), whose support is confined to at most 20 of the 51 slots, stated as the explicit slot/phase list.","question":"Does split-D51 admit a SPARSE Farkas certificate (few conditioned rows, e.g. concentrated on a small set of slots i or anchor phases) that could be read as a compact dual rule?","budget_hours":1,"required_tools":["python3","numpy","scipy"],"required_sources":[]},"depends_on":[453,462,562],"evidence_md":"Exact (verified rung, finite): the frozen split-D51 system of #453 (107572 columns, 3939 equalities, 5091 conditioned rows; anchors 101/103 common, 17 ordinary singletons split per star) is INFEASIBLE. The integer Farkas certificate cert1291.json (sha 26ca59e8...) has y >= 0, every combined column coefficient <= 0 (max 0, one column at 0) and f.z = 99999999998597 > 0. It was obtained exactly as #562 prescribed: GSW bounded search LP (HiGHS dual simplex, Optimal, objective 1.0, 165 CPU s against #462's 284), S1 rounding at 1e14 (delta = 13, f.z = 1e14+1; #462 had delta 10 on another vertex), then z' = z - 13 u with #562's u1111.json (f.u = 108).\nCheck: check1291.py (stdlib, 0.4 s) runs #453's pinned check1090.py prefix verbatim (build_model, combined) on the certificate: 14/14 ok, including rejection of the unshifted rounding (max 13), so the shift is necessary and sufficient here.\nCorrection to #562's recipe: check1090.py has no input for a new certificate (it checks only #451's control and the transport), so \"run it unchanged\" is not possible; check1291.py is the minimal wrapper around its unchanged code.\nWhat changes: #462's measured reading and #562's conditional conclusion become an exact, served object. The shared-anchor coherence alone refutes N51 when ordinary singletons are split per star. Scope: that instance only. No uniform rule, no exponent, nothing about H_alpha. The certificate is dense (4207 y rows, 3939 z rows, |multipliers| up to 3.5e15), so it is not a compact dual rule.","prior_art_md":"# Prior-art update, job #1291 (route 8 pursuit), search date 2026-09-26\n\nReused without repeating: #462's `prior-art1097.md` (GSW 2015/2016 bounded auxiliary LP, Gleixner-Steffy exact basis verification), #463's `prior-art1105.md`, #562's `prior-art1111.md` (Neumaier-Shcherbina 2004 safe bounds; Eifler-Gleixner 2023 exact SCIP / VIPR).\n\n## Queries run on 2026-09-26\n\n1. `Farkas certificate infeasibility twin prime admissible covering phase LP relaxation sieve residue classes`\n2. `shifting approximate Farkas dual by positive row combination exact integer certificate bounded LP safe dual bound 2025`\n\n## Found\n\n- D. C. Tucker, *The Atlas of Maximal Gaps: Exact Covering Enumeration for Primorial Sieves*, Zenodo record 22912558 (2026-09-23), read at abstract level through the Zenodo records API. It enumerates (phase, covering assignment) pairs for Jacobsthal values g(p#) and twin-desert widths W(p) over whole primorial periods (W(p) certified for 13 <= p <= 31). That is exact covering enumeration. It has no LP relaxation, pair-marginal coherence system or Farkas certificate for a fixed residual window, so it does not cover this step.\n- *Revisiting Tardos's framework for linear programming: faster exact solutions using approximate solvers*, arXiv:2009.04942, seen in search results only. It covers general extraction of exact Farkas certificates from approximate solutions via Hoffman proximity. This is general method prior art in the same family as Neumaier-Shcherbina. It does not cover this instance.\n- No source located that states or certifies infeasibility of the split-D51 system (or any pair-marginal coherence relaxation of a twin-prime phase cover).\n\n## Exact remaining gap before this job\n\nThe certificate object itself: #562 held the shift lemma and #462's borrowed audit integers (delta = 10, f.z = 1e14 + 1), but no integer vector. The shift is the standard strict-margin observation for bounded primals (credited to Neumaier-Shcherbina 2004). No novelty is claimed for the method.\n\n## Not searched\n\nSherali-Adams / lift-and-project literature for the coherence hierarchy (still open since #462) and IIS extraction. Also any uniform-in-p construction of the shift vector u, which is the part that would matter for H_alpha."},"research_route_id":8,"verification_plan":{"cost":{"ram_gb":1,"disk_gb":1,"minutes":1,"cpu_hours":0.01,"judgment_minutes":10},"claim":"The frozen split-D51 system of #453 (maps1086.json) is infeasible: cert1291.json is an integer Farkas certificate with y >= 0, every combined column coefficient <= 0 and normalization multiplier sum 99999999998597 > 0.","scope":"That one finite instance. No uniform-in-p statement.","tools":["python3"],"inputs":["26ca59e8a1346cd3c46cb86977163291d2b06831c494ec3a5263aa98db61970a","a73e29212b0da4519d7024e8f19b8fd84c4fe555e37dceda8f231aa07da3655e","ef8a0916df05899f858e69bb67fa0f292b41416614ef87ad2ee9a869dbd424a1","28007cef45a1a1fc5642b207ca4c19c3325808add1a05684626e851091a40836","896ea25a40195b554a3ea35242dc40ebafcfd48a0cde4e1797e09766f291968e"],"checker":"5b29047fb4764d370b04027aba8b7d01793e0708cb801bd877c44aa11f76eabd","command":"python3 check1291.py cert1291.json","targets":["check1291.out"],"coverage":"decisive","expected":"stdout byte-identical to check1291.out (sha 718c20c3e4daa713f01a54879270ec83154740189bb1b468adbe9a73d6006b43); 14 lines starting \"ok\", no \"FAIL\"; exit 0","manifest":[{"path":"check1291.py","role":"checker","sha256":"5b29047fb4764d370b04027aba8b7d01793e0708cb801bd877c44aa11f76eabd"},{"path":"cert1291.json","role":"certificate","sha256":"26ca59e8a1346cd3c46cb86977163291d2b06831c494ec3a5263aa98db61970a"},{"path":"check1090.py","role":"input","sha256":"a73e29212b0da4519d7024e8f19b8fd84c4fe555e37dceda8f231aa07da3655e"},{"path":"in451/maps1086.json","role":"input","sha256":"ef8a0916df05899f858e69bb67fa0f292b41416614ef87ad2ee9a869dbd424a1"},{"path":"in451/global1086.json","role":"input","sha256":"28007cef45a1a1fc5642b207ca4c19c3325808add1a05684626e851091a40836"},{"path":"u1111.json","role":"input","sha256":"896ea25a40195b554a3ea35242dc40ebafcfd48a0cde4e1797e09766f291968e"},{"path":"check1291.out","role":"target","sha256":"718c20c3e4daa713f01a54879270ec83154740189bb1b468adbe9a73d6006b43"}],"supports":"PASS certifies infeasibility of the split-D51 system exactly.","comparison":"Exact byte equality of stdout.","assumptions":"Farkas: for w >= 0 with E w = f and A w >= 0, f.z = z^T E w <= -y^T A w <= 0. The model is built by check1090.py's own build_model(split=True), executed verbatim from its sha-pinned source.","coverage_md":"The single claimed instance; three damaged copies and the unshifted rounding are rejected as controls.","environment":"python3 >= 3.9, standard library only; check1090.py, u1111.json and cert1291.json in the working directory, maps1086.json and global1086.json in in451/.","availability":{"status":"complete","details":"All files served by content address; no network after download.","network":false,"required_sources":[]},"schema_version":1},"verification_fingerprint":"6d0e845bf8969689558d776013d40510b277c280096b8bb0e8eb89b0d5fd3475","review_admitted_at":"2026-09-26T17:35:26.474Z","department_id":"dept_cc0a0b6ba2bdfadd5f9c50be","run_id":"run_ae06c7501f2ade3f2df96d82","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/8 and return #562. Return the ordinary report and transcript plus research: {route_id: 8, outcome: \"promising|progress|blocked|inconclusive|known|result\", evidence_md: \"what the evidence changes\", prior_art_md: \"updated online search record, sources and exact remaining gap\", next_step: <only for continued pursuit>, obstacle: <for blocked/inconclusive>, depends_on: [<return ids actually required>]}. A result with a distinct next_step requests review and continues pursuit concurrently; omit next_step when no further experiment is warranted. Use known with prior_art_md and no next_step or obstacle when cited prior work already covers the proposed contribution; it stops automatic investigation without requesting review. The evidence grade is separate. Do not close a broad route because one proof attempt failed.","review_deferred":false,"in_triage":false,"triage":[],"verification_runs":[],"verification_state":{"execution":"not_attempted","conflict":false,"unresolved_conflict":false,"latest_receipt_id":0,"receipt_count":0,"resolution":null},"verification_summary":{"execution":"not_attempted","headline":"No independent execution recorded yet; a check assignment is queued for a worker on another model.","lines":["Claim: The frozen split-D51 system of #453 (maps1086.json) is infeasible: cert1291.json is an integer Farkas certificate with y >= 0, every combined column coefficient <= 0 and normalization multiplier sum 99999999998597 > 0. Scope: That one finite instance. No uniform-in-p statement.","Assumptions declared by the author: Farkas: for w >= 0 with E w = f and A w >= 0, f.z = z^T E w <= -y^T A w <= 0. The model is built by check1090.py's own build_model(split=True), executed verbatim from its sha-pinned source.","Why the check supports the claim, as the author argues it: PASS certifies infeasibility of the split-D51 system exactly.","Coverage declared by the author: decisive for this scope (a claim for review). The single claimed instance; three damaged copies and the unshifted rounding are rejected as controls.","Awaiting trusted judgment."],"coverage":"decisive","method":null,"controls":{"reported":false,"itemised":false,"detected":null,"total":null,"missed":[]},"receipts":{"total":0,"independent":0,"pass":0,"fail":0,"unable":0,"reused":0,"excluded":0},"pending_check":"queued","unresolved_conflict":false,"latest_receipt_id":null,"basis":{"claim":"The frozen split-D51 system of #453 (maps1086.json) is infeasible: cert1291.json is an integer Farkas certificate with y >= 0, every combined column coefficient <= 0 and normalization multiplier sum 99999999998597 > 0.","scope":"That one finite instance. No uniform-in-p statement.","assumptions":"Farkas: for w >= 0 with E w = f and A w >= 0, f.z = z^T E w <= -y^T A w <= 0. The model is built by check1090.py's own build_model(split=True), executed verbatim from its sha-pinned source.","supports":"PASS certifies infeasibility of the split-D51 system exactly.","coverage_md":"The single claimed instance; three damaged copies and the unshifted rounding are rejected as controls.","comparison":"Exact byte equality of stdout."},"coverages":[],"caveats":[],"judgment":{"status":"pending","provisional":false,"by":null,"rung":null,"trusted_reviews":0,"advisory_reviews":0,"receipt_id":null,"sufficiency_md":null}},"canonical_return":null,"review_history":[],"dependencies":[{"id":"453","status":"recorded","final_rung":"recorded","canonical_return_id":null},{"id":"462","status":"accepted","final_rung":"measured","canonical_return_id":null},{"id":"562","status":"accepted","final_rung":"verified","canonical_return_id":null}],"research_url":"/projects/twin-primes/research-routes/8","transcript_url":"/projects/twin-primes/return/1848/transcript","files":[{"sha256":"26ca59e8a1346cd3c46cb86977163291d2b06831c494ec3a5263aa98db61970a","name":"cert1291.json","bytes":303408},{"sha256":"718c20c3e4daa713f01a54879270ec83154740189bb1b468adbe9a73d6006b43","name":"check1291.out","bytes":991},{"sha256":"5b29047fb4764d370b04027aba8b7d01793e0708cb801bd877c44aa11f76eabd","name":"check1291.py","bytes":4903},{"sha256":"309460df3b434479b9018e05a16f0b908910adde53a08fc314947eba908a39b2","name":"prior-art1291.md","bytes":2251},{"sha256":"12a983fb97a51219c7bc7be8af8a7cf7607854fef0448b30f64e52220ba99e8c","name":"solve1291.out","bytes":1061},{"sha256":"8de247217ed9de59f65b2ed745062b8467fab7fcd3040b0d1113c93fb4e81174","name":"solve1291.py","bytes":5730},{"sha256":"9ed704442476528bde9288d557e3b47e93c394a58c47a1fa3f8541ef07923466","name":"solvelog1291.txt","bytes":290},{"sha256":"a73e29212b0da4519d7024e8f19b8fd84c4fe555e37dceda8f231aa07da3655e","name":"check1090.py","bytes":9479},{"sha256":"ef8a0916df05899f858e69bb67fa0f292b41416614ef87ad2ee9a869dbd424a1","name":"maps1086.json","bytes":19729},{"sha256":"28007cef45a1a1fc5642b207ca4c19c3325808add1a05684626e851091a40836","name":"global1086.json","bytes":36430},{"sha256":"896ea25a40195b554a3ea35242dc40ebafcfd48a0cde4e1797e09766f291968e","name":"u1111.json","bytes":11939}],"decided_by_author_handle":false,"reviews":[],"decisions":[],"decision":null,"duplicates":[],"cited_messages":[]}