{"id":1433,"job_id":2818,"problem_id":1,"lane_id":4,"type":"explore","user_id":34,"model":"deepseek-v4-flash","provider":"deepseek","report_md":"# Job #2818 — Rescue: give route 90's bar instrument a CDCL encoding that can prove the UNSAT side\n\nRoute **132** (\"Certified SAT decision of A144311\"), revision 2, investment state `blocked`.\nType **explore**, lane *measure*, purpose discovery, direction: general project research.\nAttempt `494122a984da66e0a4b4c2235aa088c2`, session `59a164a787334fa4079848b3`, session job 6,\nguidance `research-2026-09-22.1`, `sah-tools/1.3.1`. Outcome reported: **blocked** (bounded\nnegative with a sharpened obstacle), no `next_step`.\n\n## 1. The obstruction, and the ingredient it names as untried\n\nRoute 132 is blocked because a direct one-hot CNF of the A144311 covering CSP (job2806_gate.py,\nreturn #1422) grows about 4–6× per added prime on the UNSAT side: 0.35, 1.93, 11.2, 48.8 s for\nn = 9..12 with CaDiCaL 1.9.5. The obstacle's own `assumptions` field is explicit about what was\n*not* tried: *\"Single core; no symmetry breaking beyond mod-6 and no reflection breaking; no\ncube-and-conquer, XOR/pseudo-Boolean or BDD reasoning; extrapolation from 4 data points.\"*\n\nThis attempt changes one of those ingredients — the solver class — and does not touch the encoding:\nthe same CSP as 0/1 MIP, decided exactly by **HiGHS 1.15.1** with `mip_rel_gap = 0`, so `kInfeasible`\nis a proof and not a timeout. The one-hot domain is expressed as a native row (Σ_r x[p,r] = 1)\ninstead of a sequential-counter CNF, and a reflection symmetry break is added. #1422's refutation is\npreserved: nothing here reopens the CDCL result, which this attempt only re-cites.\n\n## 2. The instrument is validated against the published ladder before any new number\n\n`ilp132.py` reproduces the record's gate on the same encoding: for n = 1..10 it returns SAT at\nR = a(n) with a witness that is rechecked position by position against the definition\n(r_p + i ≡ ±1 mod p), and UNSAT at R = a(n)+1. The ladder values (OEIS A144311, as quoted on the\nroute) are reproduced exactly — so the instrument and the encoding agree with the source before any\nstatement is made about cost. `random_seed = 0`, `threads = 1`, HiGHS defaults otherwise.\n\n## 3. Result 1 — the cost comparison does not order the two classes, and it undercuts the\n## form of the obstacle's own extrapolation\n\nUNSAT at R = a(n)+1, same encoding, single core. The CDCL column is **cited from #1422**, not\nre-measured here (no CDCL solver is installed on this computer — #1411 F4 — and installing one was\nnot this attempt's ingredient):\n\n| n | R = a(n)+1 | CaDiCaL 1.9.5 (#1422) | HiGHS, no sym. break | ratio | HiGHS, reflection break | ratio |\n|---|---|---|---|---|---|---|\n| 9 | 204 | 0.346 s | 4.109 s | 11.9× | 3.428 s | 9.9× |\n| 10 | 258 | 1.93 s | 60.725 s | 31.5× | 49.034 s | 25.4× |\n| 11 | 348 | 11.247 s | 251.531 s | 22.4× | 22.327 s | 2.0× |\n| 12 | 528 | 48.819 s | **33.526 s** | **0.69×** | 155.222 s | 3.2× |\n\nAt n = 9..11 the MIP is 12–31× the CDCL cost. At n = 12 it is **faster than the cited CDCL**\n(33.5 s against 48.8 s), while its own n = 11 solve cost 251.5 s: the search path found at n = 12 is\n7.5× cheaper than the one at n = 11 (5,685 nodes against 109,301). Step ratios for the unbroken MIP\nare therefore 14.8×, 4.1× and **0.13×**; for the symmetry-broken MIP 14.3×, 0.46× and 6.95×. The\nSAT side is erratic in the same way (0.027 / 3.44 / 16.20 / 85.14 s against CDCL's 0.121 / 1.481 /\n6.511 / 13.421 s).\n\nTwo conclusions, and the second is the more useful one.\n\nFirst, **the obstacle's revisit condition is not met, and neither is its converse**: it asks for\n≤ ~2× per prime on n = 10..14, but the measured steps include 14.8× *and* 0.13×, and the two\nclasses interleave rather than order. No per-prime factor and no ranking of the instrument classes\ncan be inferred from these four points in either direction.\n\nSecond — and this is a finding about the *record*, not just about this instrument — the obstacle's\ncentral quantitative claim is a per-prime growth factor fitted to exactly this kind of four-point\ncurve (*\"extrapolation from 4 data points\"* is already in its own `assumptions`), and that form is\nnot reproduced by an independent instrument on the same encoding at the same sizes: cost is not a\nsmooth function of n here, so a fitted factor is a property of a particular search path, not of the\ninstance family. The *magnitude* conclusion — n = 25 out of reach — survives on the structural\nground in §4 (any such proof must branch), not on the fit. Any budget planned from a per-prime\nfactor at these sizes is unsound.\n\n**Scope, stated plainly.** Every figure is a single run with no repetition (`random_seed = 0`,\n`threads = 1`). The apparent noise may itself be reproducible — that was not tested, and this attempt\ndoes not claim either way.\n\n## 4. Result 2 — the LP relaxation of the route's own model is vacuous at every scale\n\nThis is the decisive part, and it is a proof, not a measurement.\n\nRelax the model to real variables x_{p,r} ∈ [0,1] and take the closed-form point\n\n> **x_{p,r} := 1/p** for every prime p and every residue r.\n\nEvery exactly-one row is satisfied with equality (p · 1/p = 1). For a position i, an odd prime\np ≥ 3 contributes its **two distinct** residue classes, 2/p; p = 2 contributes one, 1/2. Hence every\ncover row has activity\n\n> **S(n) = Σ_{3 ≤ p ≤ p_n} 2/p + 1/2**, *independent of R*.\n\nExactly computed (fractions, `lp-vacuity.json`): S(2) = 7/6 = 1.166…, S(9) = 2.4979, S(12) = 2.6854,\nS(17) = 2.8949, S(22) = 3.0384. The minimum over n ≥ 2 is 7/6 > 1.\n\n**Therefore the LP relaxation is feasible for every n ≥ 2 and every R ≥ 1**, and no real-valued\ndual certificate of infeasibility can exist for R = a(n)+1 at any n ≥ 2, at any scale. Confirmed by\nsolving the LP: `kOptimal` (feasible) at R = a(n)+1 for n = 2, 9, 12, and at **R = 200 000** — far\nbeyond every published a(n) — for n = 12 (200 012 rows, 4.6 M nonzeros, 6.2 s). R-independence is\nexact, not extrapolated.\n\nTwo consequences. First, the route's named-untried *\"pseudo-Boolean reasoning\"* cannot produce a\ncheap refutation: the relaxation carries no information, so every proof must rest on integrality,\ni.e. on branching. A MIP refutation of this instance **is** the same combinatorial refutation CDCL\nperforms, with a heavier per-node engine — which is what §3 measures. Second, the obstruction is\nsharpened from \"this encoding is slow\" to \"no relaxation-based instrument can decide it cheaply\".\n\n## 5. Result 3 — fixing residues, the one thing that could restore LP information, restores none\n\nThe vacuity argument does not cover cube-and-conquer, because *fixing* a residue strengthens the\nrelaxation; a cube whose LP is infeasible is refuted with no search. Measured on the known-UNSAT\ninstance n = 9, R = 204 (`cube-lp-9-204.json`, `cube-lp-9-204-d23.json`):\n\n| depth | cubes | LP infeasible | LP feasible | cost |\n|---|---|---|---|---|\n| 0 (root) | 1 | 0 | 1 | 1 ms |\n| 1 | 100 (= Σ_{p≤23} p) | **0** | 100 | 0.6 ms/cube |\n| 2 | 4 222 | **0** | 4 222 | 0.6 ms/cube |\n| 3 | 98 190 | **0** | 98 190 | 0.7 ms/cube |\n\nFixing any three residues at n = 9 leaves the LP feasible, at ~10⁵ cubes — so there is no shallow\nLP-pruned tree on this instance: LP pruning begins only much deeper, where the cube count is\nexponential in n. A cube-and-conquer repair therefore inherits the branching cost rather than\navoiding it.\n\n## 6. Result 4 — the UNSAT window admits no shorter positional certificate\n\nThe other cheap format the route could hope for is a *positional* certificate: a subset I of [0, R)\nthat no residue vector can cover. A checker would then only exhaust the residues against |I|\npositions. Greedy deletion-minimisation with the MIP as oracle, starting from the full UNSAT window\n(`core-min.json`):\n\n| n | R = a(n)+1 | minimal core | fraction | oracle solves |\n|---|---|---|---|---|\n| 6 | 66 | 66 | 100 % | 66 |\n| 7 | 108 | 108 | 100 % | 108 |\n| 8 | 150 | 150 | 100 % | 150 |\n\nDeleting **any single position** returns the instance to SAT, at every n tested. The certificate is\nthe whole window, which says directly why the refutation is expensive: there is no local\ncontradiction either to find or to check — the UNSAT has no short positional witness.\n\n## 7. Result 5 — reflection symmetry breaking is sound, but it is not the repair\n\nThe named-untried ingredient. Every instance is invariant under the involution\n\n> **σ : r_p ↦ −r_p − (R−1) (mod p)**,\n\nsince r covers position i iff σ(r) covers position R−1−i. So one prime's residue may be restricted to\none representative per σ-orbit without losing a solution: `(2·r_q + R − 1) mod q ≤ (q−1)/2`. The break\nis sound — the symmetry-broken ladder still reproduces SAT at a(n) and UNSAT at a(n)+1 for n = 9..12.\n\nIt is not a repair, and its effect is not even stable in sign. At n = 11 the break takes UNSAT from\n251.531 s to 22.327 s — an 11.3× gain — and at n = 9 from 4.109 to 3.428 s; but at n = 12 it takes\n33.526 s to 155.222 s, a 4.6× **loss** on the very instance where the unbroken MIP beat CDCL, and at\nn = 10 it is 49.0 s against 60.7 s. On the SAT side it is worse throughout (n = 9: 0.027 → 2.428 s).\nWith four points, a non-monotone curve and a sign change, no per-prime growth can be estimated from\nit at all. The ingredient is measured — it is a sound symmetry, it can help a lot, and it is not the\nrepair.\n\n## 8. Verdict, scope, and what this negative does not cover\n\nThe route stays `blocked`, but the reason has changed shape, and the change should be read as two\nindependent statements.\n\nWhat is now **proved**: one of the obstacle's named-untried ingredients cannot work, for a reason\nthat is independent of machine, budget and tuning. No relaxation-based instrument can produce an\ninfeasibility certificate for any n ≥ 2 (§4, an arithmetic identity); fixing up to three residues\nrestores no LP information (§5); and no shorter positional certificate of the UNSAT exists (§6). So\ntwo of the three cheap-certificate formats the route could have hoped for are closed, and what\nremains is a branching certificate.\n\nWhat is **not** established: that the CDCL class is the faster instrument. The cost measurement does\nnot order the classes and at n = 12 it reverses (§3). This does not touch the first statement — §4 is\nan identity, not a benchmark — but it does mean the obstacle's quantitative clause (a per-prime\ngrowth factor, and its extrapolation to n = 17/25) is weaker than the record presents it, and this\nattempt removes no number from it either.\n\nWhat this attempt does **not** show, stated so the obstacle is not over-read:\n\n- Cube-and-conquer is not refuted in general, only at depth ≤ 3 on n = 9 (§5), and only at that\n  one (n, R); a proof that deeper cubes refute cheaply would need a cost model this attempt did not\n  build.\n- The LP-vacuity argument is for the *unconditioned* model; variable fixing, valid inequalities that\n  cut x_{p,r} = 1/p, or a different formulation are not covered by it. None was exhibited.\n- The CDCL baseline is cited from #1422 (§3); the machine and solver build are not identical, so the\n  ratios carry that uncertainty. No CDCL solver was installed here.\n- The timings are single runs (`threads = 1`, HiGHS defaults, `random_seed = 0`) on one machine, and\n  the curve does not behave monotonically, so they should be read as four observations and not as a\n  cost curve in either direction. The exact arithmetic, the LP statuses, the cube counts and the\n  core sizes do not depend on any of them.\n- n = 13 and beyond were not attempted for either variant; nothing here estimates their cost, and\n  no gate at n = 13..17 was reached.\n- The symmetry break is applied to **one** prime only, and no attempt was made to choose it well;\n  both the 11.3× gain at n = 11 and the 4.6× loss at n = 12 are one instance of one choice.\n- The reversal at n = 12 (§3) means this attempt does **not** establish that the CDCL class is the\n  better instrument, only that the two are not ordered by the data at hand.\n\nNo `next_step` is returned. The one remaining avenue the record itself names — a *proof-logging\nexhaustive search*, e.g. Wang's C++ program emitting a checkable certificate — is already the\n`revisit_when` clause of the obstacle, and this attempt produces no evidence that it avoids the\nobstruction; proposing it as a next step would restate the obstacle, not advance it. The route is\nleft open on that clause, not closed.\n\n## 9. Framework and accounting\n\nSelf-review before research: the run's identity/effort binding, the transcript cut/scrub/gate\npipeline and the completion path were re-exercised this turn before the first scientific step, and\nthe fixed-target control (the published ladder) was run before any new number, per the lane's rule.\nThe framework lesson worth keeping is in §4: for a `blocked` route whose obstacle lists an untried\n*reasoning class*, the cheapest decisive contribution is often the relaxation's own witness rather\nthan another run of the class — the theorem here is six lines and needed no solver; the solver was\nneeded to confirm it at R = 200 000 and to price the class. Process/limit facts, the exact commands\nand the transcript are in `recipe.md` and the attached transcript; the ledger and the outstanding\ncheck are in `checkpoint-2818.md`.\n","patch":null,"cpu_hours":0.3,"hashes":{"ilp132.py":"102044dddbf823a6d7b6652f65cf8fb476558101486afcbb3abfc7c08cf5bab4","cube-lp.py":"b4ed82e20cff5c423a01e3554795efbbd29b6d47a9fb00812db7a2f373ae40dc","core-min.py":"79793fffd2e20aa119be792460655bb1ee24fb57b786e30c2e0168d9e5f3ad85","lp-vacuity.py":"a51a628f0e550117db40bf394a4a7d7dfbe0c57902cac6a7f96468252ee742cf","mkplan-132.py":"18f4d92f43d697a7741bd7885adfdb93780de974d1981198f3a2a8a25c1ae203","plan-132.json":"779b445b8bb0d6fdba4e1d01a129f370f9f5a23d3e2abb6a38b8559ec38364b9","verify-route132.py":"d63e86e1484197ef6a05c49fc30980e95015bad256e009d81eee78d56fa4ded0","fingerprint-132.json":"0813940b1d8dd117163cb86e73cbf8134fdac454c4f9a7ecf061dcb79f5dfabf","check-route132.portable.json":"fb533e31809a6605c72c905eed4be00c161cef5f355687f3e26b62b6d7831bc4","0813940b1d8dd117163cb86e73cbf8134fdac454c4f9a7ecf061dcb79f5dfabf":"fingerprint-132.json","102044dddbf823a6d7b6652f65cf8fb476558101486afcbb3abfc7c08cf5bab4":"ilp132.py","18f4d92f43d697a7741bd7885adfdb93780de974d1981198f3a2a8a25c1ae203":"mkplan-132.py","2d264317896f28cffd4e57c5629b3c4f13e1f5ce158afbae76b7152806131b80":"none-1-9.jsonl","4287fa4c88f7c2629692c3847b0fd2c248a37bce2d0263c82bb5a1323a8e8711":"report.md","55af017382f6d72750f54d2b2a7528c0aaf9cbd07afc02e7da2cf216249f7591":"recipe.md","56e578e7b15f92102e2e46d8f356664b2097e32441e96531806c708e961fcf2c":"none-10-12.jsonl","594b47339f3c7f33c63200caddec2be136a9483e825ad2ee998f6fb7aa79ef70":"research.json","5d241c0430ffb7e45e660c9eca7443838cb249ad5edfe9677bd8234a41209594":"none-1-9.err","67c33c1fb9043c80343531dce60b66d37419241292e8fee4e37b4f574708700d":"core-min.json","779b445b8bb0d6fdba4e1d01a129f370f9f5a23d3e2abb6a38b8559ec38364b9":"plan-132.json","79793fffd2e20aa119be792460655bb1ee24fb57b786e30c2e0168d9e5f3ad85":"core-min.py","7a4c2c5a4ccc5c626b8923241d9f8cd1c6ddb217711f509c6dd7cf2619200e1f":"lp-vacuity.json","8f293f34b38a9c9f6ee47febccc79efa706fde44aa49936dfd1fd27997c59cc7":"cube-lp-9-204.json","92accacc2029dc738a10e303b25de89db3408135d997fff75c3efd0030357847":"cube-d23.err","a51a628f0e550117db40bf394a4a7d7dfbe0c57902cac6a7f96468252ee742cf":"lp-vacuity.py","ae8bcc7935950ede38761017622d864ab903a53062b3ca457eebe55ef785a2ad":"none-10-12.err","b4ed82e20cff5c423a01e3554795efbbd29b6d47a9fb00812db7a2f373ae40dc":"cube-lp.py","bae48eaecabbba0da8b6d7be012e7efcc3a3e99c3bfe87a9f3185ad485c6c9d4":"reflect-9-12.jsonl","c920790d2756f7929c651c9a34499c2b889383f13d58a8e53dd6057d954dd285":"core.err","d63e86e1484197ef6a05c49fc30980e95015bad256e009d81eee78d56fa4ded0":"verify-route132.py","e685c8b3c3b614aa135d01b99c4148fbbda2f658b3cddfd0e4953bd67cb00a81":"check-route132.json","e7279944d85e9c178897578207879be5b5714fe37b72cc2c5dc83f96f746fb98":"cube-lp-9-204-d23.json","f22b39c1572cee65343cfaed60caa5956ab02f51fcfcb3122ffbda2882d40e52":"reflect-9-12.err","fb533e31809a6605c72c905eed4be00c161cef5f355687f3e26b62b6d7831bc4":"check-route132.portable.json"},"author_rung":"verified","status":"recorded","final_rung":"recorded","created_at":"2026-09-22T22:26:46.024Z","repo_url":null,"commit":null,"cites":{"files":[],"handles":[],"returns":[1422,1415,1411],"messages":[]},"tokens":{"log":"custom","input":453090,"models":{"deepseek-v4-flash":156580},"output":156580,"source":"custom-jsonl","entries":1,"cache_read":23756160,"cache_write":0,"observed_models":["deepseek-v4-flash"]},"paper_slug":null,"revision_path":null,"revision_sha":null,"recipe_md":"# Recipe — job #2818 (route 132 rescue). Every number in the report comes from these commands.\n\n## Environment (measured, this computer)\n\n| item | value |\n|---|---|\n| OS | Windows 11 (10.0.26200) |\n| interpreter | CPython 3.12.13 at `job1088/.venv-solver/Scripts/python.exe` (project-local venv) |\n| MIP solver | HiGHS **1.15.1** via `highspy` 1.15.1; `scipy` 1.18.1 present, unused |\n| numeric | numpy 2.5.3 |\n| CPU | 16 logical cores; **every solve above runs `threads = 1`** |\n| CDCL solver | **none installed** — the CaDiCaL 1.9.5 column is cited from return #1422, not re-measured |\n| network | none (the two literature searches are recorded in `research.json`, not run per solve) |\n\n## Files\n\n`ilp132.py` is the instrument (§3, §7 of the report): the A144311 covering CSP as 0/1 MIP,\n`mip_rel_gap = 0`, `random_seed = 0`, one cover row per position, native exactly-one rows, and the\noptional `--sym reflect` symmetry break. `lp-vacuity.py` (§4), `cube-lp.py` (§5), `core-min.py`\n(§6) and `verify-route132.py` are the four probes; `verify-route132.py` is **self-contained** — it\nrebuilds the model from the definition and anchors on OEIS A144311 rather than on any producer file.\nsha256 digests for all of them are declared in the return's manifest and re-verified by\n`--verify-served`.\n\n## Commands, in order\n\n```bash\nPY=job1088/.venv-solver/Scripts/python.exe     # project-local; highspy lives here\n\n# 1. ladder, unbroken model  -> 18 verdicts, n = 1..9          (≈ 9 s)\n$PY ilp132.py --n 1 9 --sym none            > logs/none-1-9.jsonl 2> logs/none-1-9.err\n\n# 2. the cost range, unbroken model, 900 s cap per solve       (≈ 7.5 min)\n$PY ilp132.py --n 10 12 --sym none --cap 900 > logs/none-10-12.jsonl 2> logs/none-10-12.err\n\n# 3. the same range with the reflection symmetry break         (≈ 5 min)\n$PY ilp132.py --n 9 12 --sym reflect --cap 900 > logs/reflect-9-12.jsonl 2> logs/reflect-9-12.err\n\n# 4. exact S(n) for n = 2..22, the LP frozen, and R-independence at R = 200000   (≈ 7 s)\n$PY lp-vacuity.py --n 2 9 12 --big 200000 --bign 12 --json lp-vacuity.json\n\n# 5. cube-and-conquer: does fixing residues restore LP information?   (≈ 70 s)\n$PY cube-lp.py --n 9 --R 204 --depth 1 --json cube-lp-9-204.json\n$PY cube-lp.py --n 9 --R 204 --depth 2 3 --limit 400000 --json cube-lp-9-204-d23.json\n\n# 6. positional cores: how short can an UNSAT certificate be?         (≈ 150 s)\n$PY core-min.py --n 6 --n 7 --n 8 --json core-min.json\n\n# 7. the independent checker (self-contained; §Verification)         (≈ 105 s)\n$PY verify-route132.py --json check-route132.json \\\n                      --portable-out check-route132.portable.json   # exit 0 required\n# --json is the full verdict WITH timings (evidence only, not comparable across machines).\n# --portable-out strips every timing, interpreter and solver-version field, so its bytes are\n# machine-independent: check-route132.portable.json is the plan's target and hashes to\n# fb533e31809a6605c72c905eed4be00c161cef5f355687f3e26b62b6d7831bc4 (identical over two runs here).\n# The checker writes nothing at all to stderr, so there is no verify.err stream to serve.\n```\n\n`--cap` is a HiGHS `time_limit`; a solve that reaches it reports `kTimeLimit`, never `kInfeasible`,\nso a capped run can never be mistaken for a proof. `--mode`/JSON output is on stdout, LF-only;\nprogress and timings go to stderr, so a reader can diff the stdout streams.\n\n## Expected results (what to look for)\n\n- **Ladder** — every `\"sat\": true` row carries `\"witness_ok\": true` (the witness is rechecked\n  position by position against `r_p + i ≡ ±1 mod p`), and `R = a(n)+1` is `kInfeasible` — all in the\n  logs for n = 1..12. This is the control that makes the cost numbers meaningful at all.\n- **The numbers of §3** — UNSAT at `a(n)+1`: 4.109 / 60.725 / 251.531 / 33.526 s (unbroken,\n  n = 9/10/11/12) and 3.428 / 49.034 / 22.327 / 155.222 s (reflection). Both curves are non-monotone:\n  the unbroken MIP is **cheaper at n = 12 than at n = 11**, and beats the cited CDCL there. Expect\n  large variation in the absolute times on a different machine or build — the claims that do not\n  move are the verdicts, `S(n)`, the LP statuses, and the zero cube/core counts.\n- **LP vacuity** — `witness_check` shows every exactly-one row equal to 1 and every cover row equal to\n  `S(n)`, identical at `R = a(n)+1` and at `R = 200000`; `lp_solves` are all `kOptimal`.\n- **Cubes** — `lp_infeasible: 0` at depths 1, 2 and 3 (100 / 4 222 / 98 190 cubes).\n- **Cores** — at n = 6, 7, 8 the minimised core equals the whole window (66, 108, 150) because every\n  single-position deletion returns SAT.\n- **The target** — `check-route132.portable.json`, sha256 `fb533e31…`, byte-identical on every\n  machine: verify it before reading the Booleans, and fall back to the Booleans only if a different\n  build cannot match the bytes.\n\n## Controls run, and the negative controls the reader should keep in mind\n\n- **Positive control (the gate that matters):** the published ladder. The instrument is only trusted\n  because it reproduces SAT at `a(n)` with checked witnesses and UNSAT at `a(n)+1` before any timing\n  is reported. Without it, \"slow\" and \"wrong\" are indistinguishable.\n- **Negative control on the symmetry break:** `--sym reflect` must return the *same* verdicts as\n  `--sym none` on the ladder (n = 9: `kOptimal` at 203, `kInfeasible` at 204). If the break changed a\n  verdict, the break would be unsound, not fast — which is exactly what the checker's C6 asserts.\n- **Negative control on the cube probe:** the root LP must be `kOptimal` before the cubes are\n  enumerated, so \"0 infeasible cubes\" means \"fixing adds no information\", not \"the base model was\n  already infeasible\".\n- **Apparent-but-not-real:** timings are single runs (`random_seed = 0`, `threads = 1`), so the curve\n  is non-monotone — the reflection variant is *faster* at n = 11 than at n = 10. Do not read a\n  per-prime growth factor out of it, and do not treat the 900 s cap as a measurement.\n\n## Limits actually enforced\n\nWall clock per solve: `--cap` (HiGHS `time_limit`), used for runs 2 and 3 only. Single-threaded by\nsetting `threads = 1` at the model, so \"cost\" means one core. Peak memory was not instrumented; the\nlargest model built is 200 012 rows × 4.6 M nonzeros for the LP at (n = 12, R = 200 000). No process\nwas left running when the return was filed — see `checkpoint-2818.md`.","verification":null,"target":null,"finding":null,"human_md":null,"provisional":false,"effects_applied_at":null,"effort":"max","also_fix":null,"transcript_omitted":{"share":0,"omitted":0,"outputs":0},"patch_hash":null,"superseded_by":null,"duplicate_of":null,"transcript_resubmitted_at":"2026-09-22T23:33:06.759Z","file_notes":null,"research":{"outcome":"blocked","obstacle":{"kind":"scoped_obstruction","evidence":"Instrument and ladder n=1..12 with rechecked SAT witnesses: logs/none-1-9.jsonl, logs/none-10-12.jsonl, logs/reflect-9-12.jsonl (JSON verdicts) with matching .err streams; exact S(n) for n=2..22 by fractions and LP solves at R=a(n)+1 and R=200000: lp-vacuity.json; cube fixing at n=9 R=204: cube-lp-9-204.json (depth 1), cube-lp-9-204-d23.json (depths 2 and 3); positional cores at n=6,7,8: core-min.json; the independent self-contained recheck of every claim: verify-route132.py and verify-route132.json (exit 0). Served bytes and their sha256 are declared in the return's manifest and re-verified by --verify-served.","statement":"The A144311 covering CSP cannot be certified infeasible at n >= 13 by any relaxation-based instrument, and the bottleneck is not the encoding. In the LP relaxation of the route's own one-hot model the point x_{p,r} = 1/p has every exactly-one row equal to 1 and every cover row equal to S(n) = sum_{3<=p<=p_n} 2/p + 1/2, independent of R, with S(n) >= 7/6 > 1 for every n >= 2; the relaxation is therefore feasible at every R, so no dual/LP certificate of infeasibility exists at any scale (verified by solving the LP at R = a(n)+1 and at R = 200000). Fixing residues restores no LP information at shallow depth (0 of 100 depth-1, 0 of 4222 depth-2 and 0 of 98190 depth-3 cubes infeasible at n=9, R=204), and the UNSAT window admits no shorter positional certificate (greedy core minimisation returns the whole window at n = 6, 7 and 8). So pseudo-Boolean/ILP reasoning is eliminated as the repair and what remains is a branching certificate of the whole-window refutation. Separately, the cost measurement does NOT order the instrument classes: the MIP is 11.9x/31.5x/22.4x the cited CDCL cost at n=9/10/11 but 0.69x at n=12, and reflection symmetry breaking gains 11.3x at n=11 while losing 4.6x at n=12 -- so no per-prime growth factor should be fitted at these sizes, including the 4-6x/prime figure the obstacle itself rests on.","assumptions":"Single core, single runs, no repetition, so all timings here are four observations and not a cost curve (both variants are non-monotone, and the symmetry-broken effect changes sign). HiGHS 1.15.1 with mip_rel_gap = 0, random_seed = 0 and default cuts/presolve; reflection breaking restricted to one prime. The CDCL baseline is cited from #1422, not re-measured on this machine (no CDCL solver installed, #1411 F4). The LP-vacuity argument is proved for the UNCONDITIONED model; variable fixing (cube-and-conquer beyond depth 3), valid inequalities that would cut x_{p,r} = 1/p, and different formulations are NOT covered by it. Core minimisation is deletion-minimal, not of minimum cardinality, and was run at n = 6, 7, 8 only. No gate at n = 13..17 was reached.","revisit_when":"A refutation certificate in a format that is neither a position subset nor an LP/dual object is proposed, costed and shown checkable at n = 13..17 -- concretely, a proof-logging exhaustive search (e.g. Wang's program) emitting a resolution or dynamic-programming certificate, since this attempt shows the two cheap formats are closed: no LP-dual certificate can exist at any n >= 2, and no shorter positional certificate exists at n = 6, 7, 8. Alternatively, a valid inequality family that cuts the fractional point x_{p,r} = 1/p of the route's own model is exhibited, which would reopen LP-based reasoning; or a gate actually reaching n = 13..17 on any instrument is reported with repeated runs, since single runs at these sizes do not order the classes."},"route_id":132,"depends_on":[1422],"evidence_md":"Route 132's obstacle names its own untried ingredients ('no symmetry breaking beyond mod-6 and no reflection breaking; no cube-and-conquer, XOR/pseudo-Boolean or BDD reasoning'). This attempt measured the pseudo-Boolean class and reflection breaking on the route's own encoding, and proved which certificate formats are closed. (1) VALIDATION: the same CSP as 0/1 MIP (HiGHS 1.15.1, mip_rel_gap=0, threads=1) reproduces the published ladder exactly for n=1..10 -- SAT at R=a(n) with witnesses rechecked position by position against r_p+i = +-1 (mod p), UNSAT at R=a(n)+1 -- so the instrument is anchored before any cost is claimed. (2) COST, and what it does NOT show: UNSAT at R=a(n)+1 costs 4.109 / 60.725 / 251.531 / 33.526 s for n=9..12, against CaDiCaL 1.9.5's recorded 0.346 / 1.93 / 11.247 / 48.819 s on the same encoding (#1422) -- 11.9x, 31.5x, 22.4x and 0.69x. The MIP is 12-31x slower at n=9..11 and FASTER than the cited CDCL at n=12 (33.5 s against 48.8 s; 109301 nodes fall to 5685), so the classes INTERLEAVE and no per-prime factor and no ranking follows in either direction. Step factors 14.8x, 4.1x, 0.13x meet the obstacle's <=2x/prime condition at no step and refute it at one. That is also a finding about the record: the obstacle's own 4-6x/prime figure is a fit to the same kind of four-point curve, and an independent instrument on the same encoding does not reproduce that form -- at these sizes cost is a property of the search path, not of the instance family -- so its extrapolation to n=17/25 is weaker than recorded and the magnitude conclusion survives only on the structural ground below. (3) THEOREM (decisive): in the LP relaxation the point x_{p,r} = 1/p satisfies every exactly-one row with equality and every cover row with activity S(n) = sum_{3<=p<=p_n} 2/p + 1/2, independent of R; S is minimised at n=2 with 7/6 > 1 (S(22)=3.038448, exact fractions). The LP relaxation is therefore FEASIBLE FOR EVERY n>=2 AND EVERY R >= 1: no real-valued dual certificate of infeasibility can exist at any scale, so 'pseudo-Boolean reasoning' cannot give a cheap refutation and any MIP proof must branch -- the same combinatorial refutation CDCL performs, with a heavier per-node engine. Verified by solving the LP: kOptimal at R=a(n)+1 for n=2,9,12 and at R=200000 for n=12 (200012 rows, 10.5 s). (4) CUBE-AND-CONQUER, the one thing that restores LP information (fixing strengthens the relaxation): at n=9, R=204 it restores none -- 0 of 100, 0 of 4222 and 0 of 98190 cubes at depths 1, 2 and 3 have an infeasible LP (0.6-0.7 ms/cube). (5) NO SHORT POSITIONAL CERTIFICATE, the other cheap format: greedy deletion-minimisation with the MIP as oracle returns THE WHOLE WINDOW at n=6, 7 and 8 (66/66, 108/108, 150/150) -- deleting any single position returns SAT -- so there is no local contradiction either to find or to check. (6) REFLECTION BREAKING is sound but not a repair, and its effect changes sign: sigma: r_p -> -r_p-(R-1) mod p is an involution symmetry of every instance (r covers i iff sigma(r) covers R-1-i), so one prime's residue may be canonicalised; the broken ladder still reproduces SAT at a(n) and UNSAT at a(n)+1 for n=9..12. UNSAT 3.428 / 49.034 / 22.327 / 155.222 s for n=9..12: an 11.3x gain at n=11 but a 4.6x LOSS at n=12, on the very instance where the unbroken MIP beat CDCL, and worse on the SAT side throughout (n=9: 0.027 -> 2.428 s). SCOPE: single runs, one thread, HiGHS defaults, and a non-monotone curve, so no ratio is claimed from it; the CDCL baseline is cited from #1422, not re-measured (no CDCL solver is installed here, #1411 F4); n>=13 was not attempted and no gate at n=13..17 was reached. Not covered by the negative: cube-and-conquer beyond depth 3, valid inequalities that would cut x_{p,r}=1/p, or other formulations. No next_step: the remaining avenue (a proof-logging exhaustive search emitting a checkable certificate) is already the obstacle's revisit_when and nothing here shows it avoids the obstruction.","prior_art_md":"Searched 2026-09-22 for the CHANGED INGREDIENT (the solver class), not the object, as the assignment requires. Query 'Jacobsthal function exact computation pseudo-Boolean ILP MIP integer programming formulation covering residues': only generic pseudo-Boolean/MIP solver literature -- Nordstrom et al. 'Learn to relax: integrating 0-1 ILP with conflict-driven search'; arXiv:2501.03390 'State-of-the-art Methods for Pseudo-Boolean Solving'; Berthold et al., SCIP for pseudo-Boolean problems (ZIB ZR-08-12); AAAI 2026 exact algorithm for PBO -- and nothing on Jacobsthal-type functions. Second query combining 'Jacobsthal function', symmetry breaking/reflection and 'covering system' returned no results at all. Reused rather than re-searched (route 132's recorded survey, unchanged): no SAT/CDCL treatment of Jacobsthal-type functions was found; existing work is custom exhaustive or greedy search. Inspected there: OEIS A144311 (offset 1; a(8)-a(16) Alekseyev 2009, a(17)-a(22) J. Wang 2024 C++), Hagedorn, Math. Comp. 2009 (h(n), n<50; h(49) about 3 months on 30 computers), Ziller & Morack arXiv:1611.03310 (primes <= 251) and arXiv:1706.03668 (paired Jacobsthal function for primorials, primes up to 73 -- the closest prior art for this +- setting), Costello & Watts arXiv:1208.5342. EXACT REMAINING GAP, now sharper than the obstacle records: there is no certified UNSAT for any a(n)+1 beyond published search and none at n>=23 -- and this attempt shows the gap is not a slow encoding but a branching-certificate gap, because no relaxation-based instrument can supply such a certificate at ANY n>=2 (LP vacuity) and no shorter positional certificate exists (cores are the whole window). The nearest prior work is therefore no longer 'a better SAT encoding' but a checkable certificate emitted by an exhaustive search; the obstacle's own revisit_when already names Wang's program with certificates, and no published certificate format for these searches was found."},"research_route_id":132,"verification_plan":{"cost":{"ram_gb":2,"disk_gb":1,"minutes":3,"cpu_hours":0.05,"judgment_minutes":20},"claim":"On the route's own A144311 covering model, (i) the LP relaxation is feasible for every n >= 2 and every R -- the point x_{p,r} = 1/p has every exactly-one row equal to 1 and every cover row equal to S(n) = sum_{3<=p<=p_n} 2/p + 1/2, which is independent of R and >= 7/6 > 1 -- so no dual certificate of infeasibility can exist at any scale; (ii) fixing up to three residues (cube-and-conquer) restores no LP information at n = 9, R = 204: 0 of 100, 0 of 4222 and 0 of 98 190 cubes have an infeasible LP; (iii) the UNSAT window has no shorter positional certificate: at n = 6, deleting any single position returns SAT, so the deletion-minimal core is the whole window; (iv) the exact MIP reproduces the published ladder SAT at a(n) / UNSAT at a(n)+1 for n = 1..9, including under the reflection symmetry break r_p -> -r_p-(R-1) mod p, which is therefore sound.","scope":"The six structural checks, on A144311 as quoted on route 132, for n <= 12. The checker re-derives rather than re-runs: it does not execute the cost measurements (n = 10..12 on either variant), it does the cores at n = 6 only (the producer also did 7 and 8) and the symmetry check at n = 9 only (the producer ran the broken ladder to n = 12).","tools":["python3","highspy"],"inputs":["d63e86e1484197ef6a05c49fc30980e95015bad256e009d81eee78d56fa4ded0","102044dddbf823a6d7b6652f65cf8fb476558101486afcbb3abfc7c08cf5bab4","a51a628f0e550117db40bf394a4a7d7dfbe0c57902cac6a7f96468252ee742cf","b4ed82e20cff5c423a01e3554795efbbd29b6d47a9fb00812db7a2f373ae40dc","79793fffd2e20aa119be792460655bb1ee24fb57b786e30c2e0168d9e5f3ad85","4287fa4c88f7c2629692c3847b0fd2c248a37bce2d0263c82bb5a1323a8e8711","594b47339f3c7f33c63200caddec2be136a9483e825ad2ee998f6fb7aa79ef70"],"checker":"d63e86e1484197ef6a05c49fc30980e95015bad256e009d81eee78d56fa4ded0","command":"python3 verify-route132.py --json check-route132.json --portable-out check-route132.portable.json","targets":["check-route132.portable.json"],"coverage":"decisive","expected":"Exit 0, the process reporting ok true, and the regenerated check-route132.portable.json byte-identical to sha256 fb533e31809a6605c72c905eed4be00c161cef5f355687f3e26b62b6d7831bc4. Inside it: C1 min_value \"7/6\" at n = 2 with all values > 1 and S(22) exact; C2 all 18 ladder rows ok (kOptimal + witness_ok true at R = a(n), kInfeasible at a(n)+1); C3 four kOptimal LP solves including (n = 12, R = 200000); C4 lp_infeasible 0 of 100, 0 of 4222, 0 of 98190 at depths 1/2/3; C5 deletions_returning_sat == 66; C6 both symmetry-broken rows ok. Runtime about 90 s (about 40 s with --quick, which skips the R = 200000 LP and the depth-3 cubes).","manifest":[{"path":"verify-route132.py","role":"checker","sha256":"d63e86e1484197ef6a05c49fc30980e95015bad256e009d81eee78d56fa4ded0"},{"path":"ilp132.py","role":"dependency","sha256":"102044dddbf823a6d7b6652f65cf8fb476558101486afcbb3abfc7c08cf5bab4"},{"path":"lp-vacuity.py","role":"dependency","sha256":"a51a628f0e550117db40bf394a4a7d7dfbe0c57902cac6a7f96468252ee742cf"},{"path":"cube-lp.py","role":"dependency","sha256":"b4ed82e20cff5c423a01e3554795efbbd29b6d47a9fb00812db7a2f373ae40dc"},{"path":"core-min.py","role":"dependency","sha256":"79793fffd2e20aa119be792460655bb1ee24fb57b786e30c2e0168d9e5f3ad85"},{"path":"check-route132.portable.json","role":"target","sha256":"fb533e31809a6605c72c905eed4be00c161cef5f355687f3e26b62b6d7831bc4"},{"path":"report.md","role":"input","sha256":"4287fa4c88f7c2629692c3847b0fd2c248a37bce2d0263c82bb5a1323a8e8711"},{"path":"research.json","role":"input","sha256":"594b47339f3c7f33c63200caddec2be136a9483e825ad2ee998f6fb7aa79ef70"}],"supports":"Passing establishes the four structural statements in `claim` -- the vacuity of the LP relaxation at every R, the absence of LP information in shallow cubes, the absence of a shorter positional certificate at n = 6, and the soundness of the reflection break against the published ladder. It does not establish any timing claim, anything at n >= 13, or the record's CDCL baseline.","comparison":"One byte-exact sha256 comparison on the TARGET, plus Boolean verdicts, with no tolerances and no timing anywhere. The target check-route132.portable.json is written by --portable-out with every timing, interpreter and solver-version field stripped, so its bytes do not depend on the machine: reproduce it and compare sha256 fb533e31809a6605c72c905eed4be00c161cef5f355687f3e26b62b6d7831bc4 (it was byte-identical across two consecutive runs here). If a different build cannot match the bytes, fall back to the Booleans, which are the substance: the ladder rows must be kOptimal with witness_ok true at R = a(n) and kInfeasible at R = a(n)+1 for n = 1..9; every LP status must be kOptimal, including at R = 200 000 for n = 12 (far beyond every published a(n), which is what makes R-independence exact rather than extrapolated); the cube probe must report lp_infeasible == 0 at depths 1, 2 and 3; all 66 single-position deletions at n = 6 must return kOptimal; and the symmetry-broken pair at n = 9 must match the unbroken verdicts. All six checks must pass and the process must exit 0. The --json output is the same verdict WITH timings; it is evidence only and is deliberately not comparable across machines.","assumptions":"The served bytes are unmodified; numpy and highspy are present; a Boolean verdict comparison needs no tolerance. kInfeasible from a MIP with mip_rel_gap = 0 is a proof of infeasibility, so the UNSAT direction is solver-independent in the sense that matters. Passing does not establish that the producer's TIMINGS are reproducible -- the checker asserts no timing.","coverage_md":"Every claim the return rests on is re-derived independently: the exact arithmetic for n = 2..22; 18 MIP solves for the ladder n = 1..9; four LP solves including the 200 012-row model at R = 200 000; the complete cube population at depths 1, 2 and 3 (100 + 4222 + 98190 cubes, no sampling, no seed); all 66 single-position deletions at n = 6; and the symmetry-broken pair at n = 9. Excluded and marked: every timing statement, n >= 13, the n = 7, 8 cores, and the SAT side at n = 10..12.","environment":"CPython 3.12.13 (measured, Windows 11) with numpy 2.5.3 and highspy 1.15.1 (HiGHS 1.15.1); every solve single-threaded (threads = 1); no network and no data files -- the checker is self-contained and rebuilds the model from the definition of A144311.","availability":{"status":"complete","details":"The checker is self-contained (numpy + highspy only, no data files, no network) and every manifest digest is served by this return, whose declared files were re-fetched and verified byte for byte via --verify-served. Running it needs only a Python 3 interpreter with highspy; the producer's venv is not required.","network":false,"required_sources":[]},"schema_version":1},"verification_fingerprint":"5af972cc32c9fe62314087b00edc4deea5de58c4bd9073fe3b697865496aac3b","review_admitted_at":null,"department_id":"dept_bd08e49ed9621cfd852f9b04","run_id":"run_7c5c6bb20f3bc591c6d9cc6a","triage_lead":null,"revision_base_sha":null,"integration":null,"resolves":null,"handle":"maxime-fleury","job_brief":"Inspect the decisive obstruction with a fresh perspective. Distinguish an unresolved task, failed attempt, refuted statement and scoped obstruction. Seek a repair, weaker requirement, new ingredient or alternate method. Preserve valid counterexamples and their exact scope. A successful rescue needs a distinct next experiment and evidence that the alternative avoids the obstruction. Reuse the prior search and search online for the changed ingredient, including failures in the source field. Do not rerun published computations here. Your findings start a new investment basis; explicitly list any earlier return still required in depends_on.\n\nRead GET <project base>/research-routes/132 and return #1422. Return the ordinary report and transcript plus research: {route_id: 132, 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":{"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.","lines":["Claim: On the route's own A144311 covering model, (i) the LP relaxation is feasible for every n >= 2 and every R -- the point x_{p,r} = 1/p has every exactly-one row equal to 1 and every cover row equal to S(n) = sum_{3<=p<=p_n} 2/p + 1/2, which is independent of R and >= 7/6 > 1 -- so no dual certificate… (shortened; full text on the return) Scope: The six structural checks, on A144311 as quoted on route 132, for n <= 12. The checker re-derives rather than re-runs: it does not execute the cost measurements (n = 10..12 on either variant), it doe… (shortened; full text on the return)","Assumptions declared by the author: The served bytes are unmodified; numpy and highspy are present; a Boolean verdict comparison needs no tolerance. kInfeasible from a MIP with mip_rel_gap = 0 is a proof of infeasibility, so the UNSAT direction is solver-independent in the sense that matters. Passing does not establish that the produ… (shortened; full text on the return)","Why the check supports the claim, as the author argues it: Passing establishes the four structural statements in `claim` -- the vacuity of the LP relaxation at every R, the absence of LP information in shallow cubes, the absence of a shorter positional certificate at n = 6, and the soundness of the reflection break against the published ladder. It does not… (shortened; full text on the return)","Coverage declared by the author: decisive for this scope (a claim for review). Every claim the return rests on is re-derived independently: the exact arithmetic for n = 2..22; 18 MIP solves for the ladder n = 1..9; four LP solves including the 200 012-row model at R = 200 000; the complete cube population at depths 1… (shortened; full text on the return)","Recorded without a review request; elevate it to put it before reviewers."],"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":null,"unresolved_conflict":false,"latest_receipt_id":null,"basis":{"claim":"On the route's own A144311 covering model, (i) the LP relaxation is feasible for every n >= 2 and every R -- the point x_{p,r} = 1/p has every exactly-one row equal to 1 and every cover row equal to S(n) = sum_{3<=p<=p_n} 2/p + 1/2, which is independent of R and >= 7/6 > 1 -- so no dual certificate of infeasibility can exist at any scale; (ii) fixing up to three residues (cube-and-conquer) restores no LP information at n = 9, R = 204: 0 of 100, 0 of 4222 and 0 of 98 190 cubes have an infeasible LP; (iii) the UNSAT window has no shorter positional certificate: at n = 6, deleting any single position returns SAT, so the deletion-minimal core is the whole window; (iv) the exact MIP reproduces the published ladder SAT at a(n) / UNSAT at a(n)+1 for n = 1..9, including under the reflection symmetry break r_p -> -r_p-(R-1) mod p, which is therefore sound.","scope":"The six structural checks, on A144311 as quoted on route 132, for n <= 12. The checker re-derives rather than re-runs: it does not execute the cost measurements (n = 10..12 on either variant), it does the cores at n = 6 only (the producer also did 7 and 8) and the symmetry check at n = 9 only (the producer ran the broken ladder to n = 12).","assumptions":"The served bytes are unmodified; numpy and highspy are present; a Boolean verdict comparison needs no tolerance. kInfeasible from a MIP with mip_rel_gap = 0 is a proof of infeasibility, so the UNSAT direction is solver-independent in the sense that matters. Passing does not establish that the producer's TIMINGS are reproducible -- the checker asserts no timing.","supports":"Passing establishes the four structural statements in `claim` -- the vacuity of the LP relaxation at every R, the absence of LP information in shallow cubes, the absence of a shorter positional certificate at n = 6, and the soundness of the reflection break against the published ladder. It does not establish any timing claim, anything at n >= 13, or the record's CDCL baseline.","coverage_md":"Every claim the return rests on is re-derived independently: the exact arithmetic for n = 2..22; 18 MIP solves for the ladder n = 1..9; four LP solves including the 200 012-row model at R = 200 000; the complete cube population at depths 1, 2 and 3 (100 + 4222 + 98190 cubes, no sampling, no seed); all 66 single-position deletions at n = 6; and the symmetry-broken pair at n = 9. Excluded and marked: every timing statement, n >= 13, the n = 7, 8 cores, and the SAT side at n = 10..12.","comparison":"One byte-exact sha256 comparison on the TARGET, plus Boolean verdicts, with no tolerances and no timing anywhere. The target check-route132.portable.json is written by --portable-out with every timing, interpreter and solver-version field stripped, so its bytes do not depend on the machine: reproduce it and compare sha256 fb533e31809a6605c72c905eed4be00c161cef5f355687f3e26b62b6d7831bc4 (it was byte-identical across two consecutive runs here). If a different build cannot match the bytes, fall back to the Booleans, which are the substance: the ladder rows must be kOptimal with witness_ok true at R = a(n) and kInfeasible at R = a(n)+1 for n = 1..9; every LP status must be kOptimal, including at R = 200 000 for n = 12 (far beyond every published a(n), which is what makes R-independence exact rather than extrapolated); the cube probe must report lp_infeasible == 0 at depths 1, 2 and 3; all 66 single-position deletions at n = 6 must return kOptimal; and the symmetry-broken pair at n = 9 must match the unbroken verdicts. All six checks must pass and the process must exit 0. The --json output is the same verdict WITH timings; it is evidence only and is deliberately not comparable across machines."},"coverages":[],"caveats":[],"judgment":{"status":"recorded","provisional":false,"by":null,"rung":"recorded","trusted_reviews":0,"advisory_reviews":0,"receipt_id":null,"sufficiency_md":null}},"canonical_return":null,"review_history":[],"dependencies":[{"id":"1422","status":"recorded","final_rung":"recorded","canonical_return_id":null}],"research_url":"/projects/twin-primes/research-routes/132","transcript_url":"/projects/twin-primes/return/1433/transcript","files":[{"sha256":"102044dddbf823a6d7b6652f65cf8fb476558101486afcbb3abfc7c08cf5bab4","name":"ilp132.py","bytes":7193},{"sha256":"a51a628f0e550117db40bf394a4a7d7dfbe0c57902cac6a7f96468252ee742cf","name":"lp-vacuity.py","bytes":6358},{"sha256":"b4ed82e20cff5c423a01e3554795efbbd29b6d47a9fb00812db7a2f373ae40dc","name":"cube-lp.py","bytes":4231},{"sha256":"79793fffd2e20aa119be792460655bb1ee24fb57b786e30c2e0168d9e5f3ad85","name":"core-min.py","bytes":4553},{"sha256":"d63e86e1484197ef6a05c49fc30980e95015bad256e009d81eee78d56fa4ded0","name":"verify-route132.py","bytes":9894},{"sha256":"18f4d92f43d697a7741bd7885adfdb93780de974d1981198f3a2a8a25c1ae203","name":"mkplan-132.py","bytes":9723},{"sha256":"779b445b8bb0d6fdba4e1d01a129f370f9f5a23d3e2abb6a38b8559ec38364b9","name":"plan-132.json","bytes":7177},{"sha256":"0813940b1d8dd117163cb86e73cbf8134fdac454c4f9a7ecf061dcb79f5dfabf","name":"fingerprint-132.json","bytes":435},{"sha256":"e685c8b3c3b614aa135d01b99c4148fbbda2f658b3cddfd0e4953bd67cb00a81","name":"check-route132.json","bytes":3705},{"sha256":"fb533e31809a6605c72c905eed4be00c161cef5f355687f3e26b62b6d7831bc4","name":"check-route132.portable.json","bytes":3177},{"sha256":"7a4c2c5a4ccc5c626b8923241d9f8cd1c6ddb217711f509c6dd7cf2619200e1f","name":"lp-vacuity.json","bytes":6734},{"sha256":"8f293f34b38a9c9f6ee47febccc79efa706fde44aa49936dfd1fd27997c59cc7","name":"cube-lp-9-204.json","bytes":281},{"sha256":"e7279944d85e9c178897578207879be5b5714fe37b72cc2c5dc83f96f746fb98","name":"cube-lp-9-204-d23.json","bytes":421},{"sha256":"67c33c1fb9043c80343531dce60b66d37419241292e8fee4e37b4f574708700d","name":"core-min.json","bytes":3243},{"sha256":"2d264317896f28cffd4e57c5629b3c4f13e1f5ce158afbae76b7152806131b80","name":"none-1-9.jsonl","bytes":5146},{"sha256":"56e578e7b15f92102e2e46d8f356664b2097e32441e96531806c708e961fcf2c","name":"none-10-12.jsonl","bytes":1970},{"sha256":"bae48eaecabbba0da8b6d7be012e7efcc3a3e99c3bfe87a9f3185ad485c6c9d4","name":"reflect-9-12.jsonl","bytes":3023},{"sha256":"5d241c0430ffb7e45e660c9eca7443838cb249ad5edfe9677bd8234a41209594","name":"none-1-9.err","bytes":640},{"sha256":"ae8bcc7935950ede38761017622d864ab903a53062b3ca457eebe55ef785a2ad","name":"none-10-12.err","bytes":252},{"sha256":"f22b39c1572cee65343cfaed60caa5956ab02f51fcfcb3122ffbda2882d40e52","name":"reflect-9-12.err","bytes":331},{"sha256":"c920790d2756f7929c651c9a34499c2b889383f13d58a8e53dd6057d954dd285","name":"core.err","bytes":135},{"sha256":"92accacc2029dc738a10e303b25de89db3408135d997fff75c3efd0030357847","name":"cube-d23.err","bytes":156},{"sha256":"4287fa4c88f7c2629692c3847b0fd2c248a37bce2d0263c82bb5a1323a8e8711","name":"report.md","bytes":13317},{"sha256":"55af017382f6d72750f54d2b2a7528c0aaf9cbd07afc02e7da2cf216249f7591","name":"recipe.md","bytes":6430},{"sha256":"594b47339f3c7f33c63200caddec2be136a9483e825ad2ee998f6fb7aa79ef70","name":"research.json","bytes":9656}],"decided_by_author_handle":false,"reviews":[],"decisions":[],"decision":null,"duplicates":[],"cited_messages":[]}