{"id":1847,"job_id":1290,"problem_id":1,"lane_id":5,"type":"explore","user_id":1,"model":"claude-opus-5-5","provider":"anthropic","report_md":"# Job #1290 (pursue route 18): the D51 owner instance is UNSAT, and its small checked refutation is already on record (#1844); CDCL on the owner CNF does not find it\n\n**Caveats first.** This concerns one frozen instance (p = 97, a = 9409, first 51 slots, L = 3131, Q = 101..193). Nothing here touches H_alpha, uniformity or twin-prime infinitude. The step's decisive object was already published by this department on route 7 (#1844, anchored on #1840's method). This return connects it to route 18 and adds the owner CNF, its census, and a CDCL measurement. Outcome `known`.\n\n## What the step asked, and where it is answered\n\nThe step asked for (0) a published D51 owner census and CNF, (1)-(3) a CDCL decision with a witness or a refutation whose size is compared with 1,494,560, and (4) the LP relaxation on the same census.\n\n- **Witness: none exists (proven, prior work).** #1840 (job 959) certified the frozen 48-slot prefix (L = 2831) non-coverable with a 3,507-leaf branch tree of integer-checked LP certificates. Any cover of D51 covers its 48-slot prefix, so D51 has no phase cover. By #472's Helly lemma (q > 3), the owner CNF is SAT iff a phase cover exists, so the owner CNF is UNSAT.\n- **Small checked refutation of D51 itself (proven, prior work).** #1844 (job 975) published `tree975-51-109.cert.jsonl` (sha256 94d5de9a...5d, 40,536 bytes). It branches once on q = 109, and each of its 109 phases is closed by an integer weight vector w with sum_{q != 109} max_b W(q,b) < W(residual). That is 110 records and 5,457 integers, checked by the stdlib `checkcert959.py` in 0.06 s here. Rerunning `tree959.py 9409 51 8` today reproduced the file byte for byte (5 s, 473 LPs). Measured against the route's figure: 110 records vs 1,494,560 tree nodes. The node-cap framing is retired, but by a counting (cutting-planes-type) certificate on the phase formulation, not by the owner representation.\n- **Negative controls on that certificate (this run):** dropping one leaf, lowering one weight, and applying it at n = 52 or n = 47 were all rejected by the checker.\n- **LP relaxation (prior work plus a derivation).**\n  - The pairwise owner LP (0 <= x <= 1, coverage >= 1, x(s,q) + x(t,q) <= 1 per conflict) is feasible at x = 1/19 for any instance with >= 2 colours, so it carries no information.\n  - The configuration LP (one column per colour-q independent set) is, by the Helly lemma, exactly #1840's phase LP. Its value v(51) = 1.0141051060 is SILENT, with an integer fractional cover of slack 14105102/10^9. This is already in #1840's `frozen959.out`, reproduced here by `lp1290.py`, and the n = 52 value 1.00753135 matches.\n  - So no Farkas certificate exists at depth 0. One branching level is necessary and sufficient in this family: #1844 found no single anchor closes at n <= 50, and 109 is the only one that closes at 51.\n\n## New in this return\n\n1. **The instance is now pinned** (step 0). `census1290.py` checks the input arithmetic and writes the owner CNFs:\n   - `owner1290-D51.cnf`: 969 variables, 23,831 clauses (51 coverage + 23,780 conflict), sha256 d35923f6...629f.\n   - `owner1290-D51-amo.cnf`: 32,552 clauses with at-most-one, sha256 62ff4b82...36bb.\n   - Both are uploaded as `.cnf.txt` (same bytes; `.cnf` is not an accepted file type).\n   - The input check confirms the 51 slots are exactly the 97#-admissible twin starts in [9409, 12540) (coherence974-input.json, sha256 b173e69b...62c1), with common residue 5 mod 6 and diameter + 2 = 3122 < 9409.\n2. **Census (measured, exact).** Of the 1,275 pairs, 880 have NO compatible prime, 345 have one and 50 have two; no pair has three. Compatible pairs per colour range over 13..42. The exact per-colour capacity max_b |K_q(b) ∩ D| is 3 at most primes (4 at 103 and 107, 2 at 157 and 179), summing to 57 against n = 51. So even the exact alpha (not a clique-cover bound) leaves the per-colour capacity prune silent by 6. #561's revisit condition (lists concentrated so that some colour becomes tight) is checked and not met.\n3. **Encoding control.** `encode1290.py` maps #1840's verified n = 47 cover to owners (smallest killing prime per slot). It satisfies all 20,214 clauses of the D51 CNF on those slots, 0 violated.\n4. **CDCL on the owner CNF (measured).** CaDiCaL 1.9.5 via python-sat 1.9.dev15, DRAT proof logging on, conflict budget in 10^6 chunks, bounded by run-limited (1500 CPU s each, one thread):\n   - base CNF: undecided; last completed chunk 31,000,038 conflicts at 1490 CPU s, stopped by the 1500 CPU-s limit (status None)\n   - AMO CNF: undecided; last completed chunk 29,000,039 conflicts at 1475 CPU s, stopped by the 1500 CPU-s limit (status None)\n   - A positive control, the owner CNF of the COVERABLE 47-slot prefix, found no witness within 300 CPU s either.\n\n   Compare #1840: CaDiCaL on #357's phase CNF at n = 48, no answer in 600 s. On this instance, clause learning on the owner representation neither finds witnesses nor refutes, while the arithmetic weight certificate is 110 records. This matches the colouring/pigeonhole analogy on the route: resolution-based systems pay for the counting that one weighted inequality does directly.\n\n## Consequence for the route\n\nThe central uncertainty (\"does the owner representation give a useful smaller independently checked proof on D51?\") has a measured answer on this instance. The smallest checked proof on record is the phase-side depth-1 weight tree (#1844), and the owner CNF gives CDCL no foothold within about 25 CPU minutes. I propose no next step on route 18. A future owner-specific experiment would need an ingredient the owner view adds and the weight certificate lacks. I found none: the per-colour capacity in the owner view is exactly the depth-0 weight bound with unit weights (57 >= 51), which the LP already dominates.\n\n## Sources\n\n- Returns #472 (owner equivalence, Helly lemma), #473 (1,494,560 count), #561 (capacity-prune bound), #386 (coherence974-input.json), #1840 (tree959.py sha256 ad236e22...f106, checkcert959.py 53879d8b...1765, sprint959.py c656054c...162a, frozen959.out, n = 47 cover in cover959.out), #1844 (tree975-51-109.cert.jsonl 94d5de9a...5d); #370's r370-route4-weighted.py (76d7f18e...487b) is imported by the job-959 scripts.\n- Prior-art search: see research.prior_art_md.\n\n45 of @Benjaminsen's returns wait for a verdict.\n\nTranscript: scrubbed by sah-py-1.0.5 (credentials, account/session identifiers, local paths outside the working folder, third-party payload markers); nothing else removed.\n","patch":null,"cpu_hours":0.92,"hashes":{"census1290.out":"42f8b8ae4aadf656599135c0ca9e57fd0430886ae29da1330aa170488ed847f4","encode1290.out":"9263e4da9e0479f1b79652d62163a9c4e6605b105ce2feecf21cdd0e2a281ee5","owner1290-D51.cnf.txt":"d35923f6b2d89dc3ddcf637fc833c64125a17c4b4de591e37ed8a0fd6479629f","owner1290-D51-amo.cnf.txt":"62ff4b82d2e0552a6d95849ac94a40712b03fec7137aca046bd587b6b7e136bb"},"author_rung":"proven","status":"recorded","final_rung":"recorded","created_at":"2026-09-26T17:25:56.671Z","repo_url":null,"commit":null,"cites":{"files":["b173e69b99916a9562cfab59223359984c629f5845a68a265d4ef3dbc3f162c1","53879d8b75638f258732a20f2dc96219f4c988cafa109f858a0bc13e882f1765","94d5de9afa0e5dce9ae350f592c6e18be859f650fda9b0da6146e97f35c71d5b","ad236e224d91200b0c27bff8eeae94316e62d0faf22c16e5901442642ee2f106","c656054c6e0cddf371f87064062eef779fda202cf8604c54f30e15774455162a"],"handles":[],"returns":[386,472,473,561,1840,1844],"messages":[]},"tokens":{"log":"claude-code","input":152,"models":{"claude-opus-5-5":54216},"output":54216,"source":"claude-jsonl","entries":76,"cache_read":9276024,"cache_write":162218,"observed_models":["claude-opus-5-5"]},"paper_slug":null,"revision_path":null,"revision_sha":null,"recipe_md":"# Recipe - job #1290 (route 18)\n\nInputs (fetch from `<project base>/../files/<sha256>`, i.e. the host-root /files path):\ncoherence974-input.json (b173e69b99916a9562cfab59223359984c629f5845a68a265d4ef3dbc3f162c1, return #386);\ncheckcert959.py (53879d8b75638f258732a20f2dc96219f4c988cafa109f858a0bc13e882f1765, #1840);\ntree975-51-109.cert.jsonl (94d5de9afa0e5dce9ae350f592c6e18be859f650fda9b0da6146e97f35c71d5b, #1844).\n\n1. **Decisive check (stdlib, < 1 s):** `python3 checkcert959.py 9409 51 tree975-51-109.cert.jsonl` prints\n   `PASS: a=9409 n=51 L=3131 has no phase cover by Q=101..193 (19 primes); 1 branch nodes, 109 leaves, max depth 1`.\n   Negative controls: the same certificate at n = 52 or n = 47 must fail, as must any copy with one leaf removed or one weight lowered.\n2. **Owner CNF and census (stdlib, ~2 s):** `python3 census1290.py coherence974-input.json > census1290.out`.\n   Expected: census1290.out sha256 42f8b8ae4aadf656599135c0ca9e57fd0430886ae29da1330aa170488ed847f4; owner1290-D51.cnf d35923f6b2d89dc3ddcf637fc833c64125a17c4b4de591e37ed8a0fd6479629f; owner1290-D51-amo.cnf 62ff4b82d2e0552a6d95849ac94a40712b03fec7137aca046bd587b6b7e136bb.\n3. **Encoding control (stdlib, < 1 s):** `python3 encode1290.py coherence974-input.json owner1290-D51.cnf > encode1290.out`, expected sha256 9263e4da9e0479f1b79652d62163a9c4e6605b105ce2feecf21cdd0e2a281ee5 (`ENCODING CONTROL PASS`, 0 violated of 20214).\n4. **LP values (numpy + scipy/HiGHS, ~3 s):** place lp1290.py next to a directory `../959/` holding sprint959.py (c656054c...162a, #1840) and r370-route4-weighted.py (76d7f18e...487b, #370); run `python lp1290.py coherence974-input.json`. Expected lines: n=51 `v = 1.0141051060 SILENT exact check 14105102`; n=52 `1.0075313501 SILENT`; n=53 `0.9956680146 DEFICIT`. The file hash 59cb98c3...e208 was observed with scipy 1.13.1. Compare the printed values if your version differs.\n5. **CDCL measurement (optional, python-sat, 2 x 25 CPU min):** `python solve1290.py owner1290-D51.cnf 200000000 owner1290-D51.drat` under a 1500 CPU-second limit, and the same for the -amo file. Observed: undecided at the cap (conflict counts in the report). This is a measurement of one solver at one budget, not a lower bound. Timing and conflicts depend on the host and version and are not hashed.\n\nScope: step 1 proves that the single frozen instance D51 has no phase cover, and hence (by #472's Helly lemma) that its owner CNF is UNSAT. Nothing uniform follows.","verification":null,"target":null,"finding":null,"human_md":null,"provisional":false,"effects_applied_at":null,"effort":"high","also_fix":null,"transcript_omitted":{"share":0.022988505747126436,"omitted":2,"outputs":87},"patch_hash":null,"superseded_by":null,"duplicate_of":null,"transcript_resubmitted_at":"2026-09-26T17:27:20.402Z","file_notes":null,"research":{"outcome":"known","route_id":18,"depends_on":[472,1840,1844],"evidence_md":"Known (prior work #1840, #1844), connected to route 18 here:\n- D51 has no phase cover (#1840: its 48-slot prefix is already non-coverable), so by #472's Helly lemma the owner CNF is UNSAT; the SAT branch of the step is closed.\n- The decisive checked refutation of D51 itself is #1844's tree975-51-109.cert.jsonl: 1 branch (q = 109) + 109 weight leaves, 110 records, 40,536 bytes, stdlib check 0.06 s. Reproduced byte for byte by tree959.py today; four negative controls rejected. That is 110 records against the route's 1,494,560-node figure. It is a phase-side counting certificate, not an owner-representation proof.\n- LP: the pairwise owner LP is trivially feasible (x = 1/19). The configuration LP equals #1840's phase LP, v(51) = 1.0141051060 SILENT, so depth 0 cannot close; depth 1 closes only at anchor 109 (#1844 frontier975.out).\nNew measurements: owner CNF published (969 vars, 23,831 clauses, sha256 d35923f6...629f; AMO variant 32,552, 62ff4b82...36bb); pair lists: 880/345/50 pairs with 0/1/2 compatible primes, none with 3; exact per-colour capacity sum 57 >= 51, so the capacity prune stays silent even with exact alpha (#561's revisit condition not met); encoding control 0 of 20,214 clauses violated by #1840's n = 47 cover. CaDiCaL 1.9.5 on the owner CNF: base undecided; last completed chunk 31,000,038 conflicts at 1490 CPU s, stopped by the 1500 CPU-s limit (status None); AMO undecided; last completed chunk 29,000,039 conflicts at 1475 CPU s, stopped by the 1500 CPU-s limit (status None); the coverable n = 47 owner CNF was also unsolved in 300 CPU s. So on this instance the owner representation gives CDCL no foothold, while one weighted inequality per leaf does the work.","prior_art_md":"Search 2026-09-26 (this assignment), updating the route ledger (#472's prior-art1118.md, #561's record); reused without re-reading: Ziller-Morack arXiv 1611.03310 and 1706.03668 (section and page locators in #472), Buss-Pitassi CSL'97, Beyersdorff-Galesi-Lauria IPL 2010, Samaras-Stergiou JAIR 2005.\nQueries: (1) \"Jacobsthal function computation SAT solver covering residue classes primes\"; (2) \"twin prime admissible interval covering by residue classes one per prime SAT integer programming Jacobsthal twin\"; (3) \"SAT solver DRAT proof covering congruences residue classes prime sieve unsatisfiable certificate\"; (4) \"resolution complexity graph k-colorability lower bound Beame Culberson Mitchell Moore CDCL proof size colouring pigeonhole\".\nInspected (abstract level, via export.arxiv.org API / Zenodo records API): Ziller-Morack 1611.03310v2 and 1706.03668v1 (ILP/enumeration for Jacobsthal and paired-progression Jacobsthal values up to 251 and 73; no proof-size data for residual instances; already on the ledger). D. C. Tucker, \"The Atlas of Maximal Gaps: Exact Covering Enumeration for Primorial Sieves\", Zenodo record 22919682 (2026-09-23): twin-desert widths W(p) certified for 13 <= p <= 31 and a \"capacity pre-sieve\"; it concerns maximal deserts over the whole primorial period, not certificates for a fixed residual window with primes above p. Full text not read. M. Raso, D. Venturi, arXiv 2609.08528 (survivor-set counting): not relevant to certificates.\nSeen in search results only, NOT inspected: Beame-Culberson-Mitchell-Moore, \"The resolution complexity of random graph k-colorability\", Discrete Appl. Math. 153 (2005) 25-47 (linear-exponential resolution lower bounds for random sparse k-colourability); generic DRAT/LRAT certificate literature (SAT Competition certificate track). No located source applies CDCL/DRAT to residue-class covering of prime-sieve windows.\nDepartment record (decisive): #1840 (job 959) certifies the frozen prefix n = 48 non-coverable and tabulates v(n), including v(51) = 1.0141051060; #1844 (job 975) publishes the depth-1 anchor-109 certificate for n = 51 (tree975-51-109.cert.jsonl) and the one-anchor frontier table. These cover the step's success object (witness or small checked refutation plus the LP on the same census).\nExact remaining gap: none for the D51 question. Open and not addressed here: whether any owner-specific proof system beats the phase-side weight tree on larger windows, and H_alpha (uniform noncoverability), which remains TPC-strength."},"research_route_id":18,"verification_plan":null,"verification_fingerprint":null,"review_admitted_at":null,"department_id":"dept_cc0a0b6ba2bdfadd5f9c50be","run_id":"run_c4e949bb3e59c524c49eef80","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/18 and return #561. Return the ordinary report and transcript plus research: {route_id: 18, 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":null,"verification_summary":null,"canonical_return":null,"review_history":[],"dependencies":[{"id":"472","status":"recorded","final_rung":"recorded","canonical_return_id":null},{"id":"1840","status":"pending","final_rung":null,"canonical_return_id":null},{"id":"1844","status":"pending","final_rung":null,"canonical_return_id":null}],"research_url":"/projects/twin-primes/research-routes/18","transcript_url":"/projects/twin-primes/return/1847/transcript","files":[{"sha256":"42f8b8ae4aadf656599135c0ca9e57fd0430886ae29da1330aa170488ed847f4","name":"census1290.out","bytes":1050},{"sha256":"eca54df84793947e08a21ed517f053550e55b921a7288a7388e7b92cf5f3bb51","name":"census1290.py","bytes":4061},{"sha256":"f25d501bd4bef4125b1fe203064816612ebeb4f2116d85488f34b23d4f7c6f65","name":"ctl1290.py","bytes":1805},{"sha256":"9263e4da9e0479f1b79652d62163a9c4e6605b105ce2feecf21cdd0e2a281ee5","name":"encode1290.out","bytes":152},{"sha256":"c9847a9bc3643fcf5b9d9952525532026d824de1a4abaca85b1ec304673bf14f","name":"encode1290.py","bytes":1580},{"sha256":"59cb98c3b5ccbbbd083acc42c132bed8569ec2afe13c8d8c18ba5131c433e208","name":"lp1290.out","bytes":467},{"sha256":"1053a2bc8a10927e391667388a8f14c3e849631cfabdd1d1c1a30d589e098d43","name":"lp1290.py","bytes":1799},{"sha256":"62ff4b82d2e0552a6d95849ac94a40712b03fec7137aca046bd587b6b7e136bb","name":"owner1290-D51-amo.cnf.txt","bytes":386741},{"sha256":"d35923f6b2d89dc3ddcf637fc833c64125a17c4b4de591e37ed8a0fd6479629f","name":"owner1290-D51.cnf.txt","bytes":284029},{"sha256":"9f42f5fbdeb8937cb733e4969a7dda301353b582aec03d85584d8a96054fe6f8","name":"solve1290-amo.log","bytes":1100},{"sha256":"1023b1a954aac421a9bb701cc45c9570e400dab32baa33fac63a9294b6d08e4d","name":"solve1290-base.log","bytes":1176},{"sha256":"ac962b46cd9c1c41a2ec25d2cc29f08ffc6de3ba6852bef40266d5cb91dcd120","name":"solve1290.py","bytes":2274}],"decided_by_author_handle":false,"reviews":[],"decisions":[],"decision":null,"duplicates":[],"cited_messages":[]}