{"id":1464,"job_id":2847,"problem_id":1,"lane_id":null,"type":"explore","user_id":1,"model":"claude-opus-5-5","provider":"anthropic","report_md":"# Route 144 triage: deterministic cube-and-conquer with LP closure. Outcome: known.\nRung: **measured** (single-threaded HiGHS 1.15.1, one machine with 4 CPUs, aarch64). Everything below is in runs file bb58fcbb63b2.\n\n## 1. The proposed split order cannot close a cube (proof)\nThe next step splits on the r = 1, 2, 3 **largest** primes. Take any cube that leaves a set U of primes unfixed. Put x_{q,r} = 1/q for q in U and set the fixed primes as fixed. Every exactly-one row holds. Every cover row gets at least S(U) = [2 in U]/2 + sum_{odd q in U} 2/q from the free primes. With 2 and 3 free, S(U) >= 1/2 + 2/3 = 7/6 > 1, so **the cube LP is feasible for every residue choice of the fixed primes**. This holds at every n and every depth up to n-2 in largest-first order. The #1459 depth curve fixed random prime subsets, which include 2 and 3, so it does not transfer to this order. Sampled check: 0/50 infeasible at depths 1, 2 and 3 (n = 13, R = 546), and 0/40 at n = 9. The route's success clause \"LP-closed fraction at each depth at least the depth curve\" cannot hold in this order.\n\n## 2. The reverse order works and is deterministic (measured)\nSplit on the **smallest** primes first (2, 3, 5, 7, ...), close each cube by the pure LP (presolve off), and run DFS in lexicographic order. This is `cc.py` on the served `ilp132.py` encoding. Every UNSAT instance R = a(n)+1 closes:\n\n| n | R | LP solves | wall s | closing depths |\n|---|---|---|---|---|\n| 9 | 204 | 315 | 0.35 | 4-5 |\n| 10 | 258 | 645 | 0.89 | 4-5 |\n| 11 | 348 | 3,195 | 4.85 | 4-6 |\n| 12 | 528 | 3,183 | 17.9 | 5-6 |\n| 13 | 546 | 35,505 | 138.9 | 5-10 |\n| 14 | 618 | 70,809 | 326.1 | 6-8 |\n\nWith random_seed 7 instead of 0, n = 12 and n = 13 give identical per-depth counts (3,183 and 35,505). On the **same machine**, the MIP (ilp132.py, seed 0) needs 247.1 s and 70,718 nodes at n = 13. So the cube search is 1.78x faster there, just short of the route's 2x bar. Against #1459's cross-machine targets it clears both (138.9 < 162 s; 326.1 < 332 s). The LP-solve counts give per-prime factors of 2.0, 5.0, 1.0, 11.2 and 2.0: deterministic, but not smooth.\n\n## 3. Prior art already covers the contribution\nOEIS A144311 lists a(1..22) (a(22) = 1709) and links a C++ program by Jinyuan Wang. It is a deterministic DFS over residues, smallest primes first (2 and 3 are absorbed by the mod-6 reduction). It prunes a node when the sum over the remaining primes of their best residue's coverage is below the number of uncovered positions. That bound is the aggregated form of this LP: summing the cover rows shows that LP feasibility implies the bound passes. So LP closure prunes at least as much per node but costs about 4 ms per node. A seed-independent exact instrument with a measurable cost per prime therefore already exists, and it has decided the covering question well past n = 14. No compiler is installed here, so it was not timed.\n\n## Consequence\nThe route's contribution is known. Its specific method (largest-first split) is provably vacuous, and the working variant is the published smallest-first DFS with a stronger bound. What remains is route 132's own gap (n = 23..25, beyond the OEIS table). The instrument question there is whether the LP bound's extra pruning pays for its cost against the OEIS program. That is route 132's next step, not this route's.\n\nCost: about 0.26 CPU-h, all under `sah run-limited`. 48 returns wait for a verdict.\n","patch":null,"cpu_hours":0.26,"hashes":{"cc.py":"99dee652d4908200f5560c3368db2e16cd7f312c1f0c70cd5d1f721ad4bb8555","ilp132.py":"e87e8bbbe69235923a58ec5af4ee1dc78cd708ef89abfca17d427ed1ab9a7e16","runs.jsonl":"bb58fcbb63b252d5b5cc0935527f8686781da20e73ac8deab916774744e92766"},"author_rung":"measured","status":"recorded","final_rung":"recorded","created_at":"2026-09-23T00:28:59.168Z","repo_url":null,"commit":null,"cites":{"files":["99dee652d4908200f5560c3368db2e16cd7f312c1f0c70cd5d1f721ad4bb8555","bb58fcbb63b252d5b5cc0935527f8686781da20e73ac8deab916774744e92766","e87e8bbbe69235923a58ec5af4ee1dc78cd708ef89abfca17d427ed1ab9a7e16"],"handles":[],"returns":[1459,1422,1433],"messages":[]},"tokens":{"log":"claude-code","input":72,"models":{"claude-opus-5-5":27282},"output":27282,"source":"claude-jsonl","entries":36,"cache_read":2438199,"cache_write":98382,"observed_models":["claude-opus-5-5"]},"paper_slug":null,"revision_path":null,"revision_sha":null,"recipe_md":"# Recipe (job 2847): CPython 3.13 + numpy + highspy 1.15.1, < 1 GB RAM\n1. Fetch the served `ilp132.py` (file e87e8bbbe69235923a58ec5af4ee1dc78cd708ef89abfca17d427ed1ab9a7e16) and `cc.py` (file 99dee652d4908200f5560c3368db2e16cd7f312c1f0c70cd5d1f721ad4bb8555) into one directory.\n2. `python3 cc.py dfs --n N --order small [--seed S] --cap 600` for N = 9..14: one JSON line with verdict, lp_solves, per-depth created/closed counts and wall seconds.\n3. `python3 cc.py sample --n 13 --order large --depth d --k 50` for d = 1, 2, 3: counts of LP-infeasible random cubes (expected 0 by the proof in the report).\n4. Same-machine MIP baseline: `python3 ilp132.py --n 13 13 --only 546 --sym none --seed 0 --cap 600`.\nAll outputs are collected in file bb58fcbb63b252d5b5cc0935527f8686781da20e73ac8deab916774744e92766 (runs.jsonl).","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":36},"patch_hash":null,"superseded_by":null,"duplicate_of":null,"transcript_resubmitted_at":null,"file_notes":null,"research":{"outcome":"known","route_id":144,"depends_on":[1459],"evidence_md":"(1) Proof: in the route's largest-first order, every cube LP is feasible while primes 2 and 3 are free. x_{q,r} = 1/q on the free set U gives each cover row >= S(U) >= 1/2 + 2/3 > 1. So r = 1..3 (indeed any depth <= n-2) closes 0 cubes at every n. Sample check: 0/50 at n = 13, depths 1-3. The #1459 depth curve fixed random subsets that include 2 and 3, so it does not apply to this order.\n(2) Measured: smallest-first LP-closure DFS (cc.py on the served ilp132.py encoding, pure LP, lexicographic) closes UNSAT at R = a(n)+1 for n = 9..14 with 315 / 645 / 3,195 / 3,183 / 35,505 / 70,809 LP solves in 0.35 / 0.89 / 4.85 / 17.9 / 138.9 / 326.1 s. Seeds 0 and 7 give identical counts at n = 12 and 13. The same-machine MIP at n = 13 takes 247.1 s and 70,718 nodes, a 1.78x speed-up (short of the 2x bar). #1459's cross-machine targets are met (138.9 < 162 s; 326.1 < 332 s). Per-prime LP-count factors are 2.0, 5.0, 1.0, 11.2 and 2.0.\n(3) This variant is the published OEIS A144311 algorithm (deterministic smallest-first residue DFS) with the LP replacing its aggregated coverage bound, which the LP dominates. So the route's contribution, a seed-independent exact instrument with measurable per-prime cost, is prior art. The open item is route 132's n = 23..25.","prior_art_md":"Search 2026-09-23. OEIS A144311 (https://oeis.org/A144311): data a(1..22) = 1, 5, 11, ..., 1529, 1709. Comment: a(n) = 5 mod 6 for n > 1. Link: Jinyuan Wang, C++ program (https://oeis.org/A144311/a144311.cpp.txt, read in full). Method: it reduces mod 6 (x = 1 mod 6, so 2 and 3 are fixed) and then runs a DFS over the residues of 5, 7, 11, ... in increasing order. It keeps per-prime residue coverage counts of the still-uncovered positions, prunes when the sum over the remaining primes of the maximum count is below the number of uncovered positions, and grows the record window. That is exactly a deterministic smallest-first cube-and-conquer with a relaxation closure. Its bound is the aggregate of the covering LP: summing the LP's cover rows gives sum_q sum_r x_{q,r} cov_{q,r} >= #uncovered, with LHS <= sum_q max_r cov_{q,r}, so the LP prunes a superset. Also related: Hagedorn (2009, Math. Comp.) and Ziller & Morack (arXiv 1611.03310) compute Jacobsthal's h(n) by exact residue-enumeration searches with counting bounds (cited from memory, not re-read this turn), and the route's cited sources are Heule's cube-and-conquer (IJCAI 2017), proof-prefix partitioning (SAT 2025) and CP-SAT LP workers. Exact remaining gap: a(23..25) are not in OEIS and are route 132's target. This return did not time the OEIS program against LP closure (no compiler here). The OEIS values carry no proof log, so an independent certificate for n = 15..22 would be a verification contribution, not an instrument one."},"research_route_id":144,"verification_plan":null,"verification_fingerprint":null,"review_admitted_at":null,"department_id":"dept_da55f23c995cabb5136f4e91","run_id":"run_723587eda9a5cb782822861f","triage_lead":null,"revision_base_sha":null,"integration":null,"resolves":null,"handle":"Benjaminsen","job_brief":"Search online for existing attempts, results, tables and datasets before testing feasibility. Reuse the recorded search and inspect the closest sources and weakest assumption. Use published numbers with citations; do not reproduce them in triage. Seek the smallest experiment on the uncovered step. Recommend promising only with specific evidence and a bounded next step; do not claim the route is proved. Map the assumptions of any borrowed method onto this problem.\n\nRead GET <project base>/research-routes/144 and return #1459. Return the ordinary report and transcript plus research: {route_id: 144, 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>, 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.","review_deferred":false,"in_triage":false,"triage":[],"verification_runs":[],"verification_state":null,"verification_summary":null,"canonical_return":null,"review_history":[],"dependencies":[{"id":"1459","status":"recorded","final_rung":"recorded","canonical_return_id":null}],"research_url":"/projects/twin-primes/research-routes/144","transcript_url":"/projects/twin-primes/return/1464/transcript","files":[{"sha256":"99dee652d4908200f5560c3368db2e16cd7f312c1f0c70cd5d1f721ad4bb8555","name":"cc.py","bytes":4280},{"sha256":"bb58fcbb63b252d5b5cc0935527f8686781da20e73ac8deab916774744e92766","name":"runs.jsonl","bytes":4014},{"sha256":"e87e8bbbe69235923a58ec5af4ee1dc78cd708ef89abfca17d427ed1ab9a7e16","name":"ilp132.py","bytes":7444}],"decided_by_author_handle":false,"reviews":[],"decisions":[],"decision":null,"duplicates":[],"cited_messages":[]}