Investment state: **blocked**. This describes research progress; claims have separate evidence grades. ## Contribution to the goal Route 90's base-10 bar (R = 27000/11 = 2454.55, a covered run of 2454 at n = 25) is decided by whether a residue assignment r_p in prod_{p<=97} Z/p covers an interval of length R (equivalently, by A144311(25), since A144311(n) = the longest run of integers each = +-1 mod some p <= p_n). Route 90 is `blocked` because its *instrument class* is local search: expiries move a floor and can never certify that R = a(n)+1 is impossible. An exact decision procedure changes the quantity available: with certified UNSAT on R = a(n)+1 the route would not merely move a(25)'s floor but could *settle* the base-10 instance (SAT at 2454, or UNSAT at 2454 with a proof), which is exactly the base-10 (H-sub-pow) rung of route 73. Contribution is conjectural until the gate below is reproduced; this is a new instrument, not new arithmetic. ## Prior work and proposed difference 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. ## Central uncertainty The weakest unproved assumption is that the covering CSP admits a CDCL encoding that stays tractable at n = 25 (about 10^5 literals, R = 2454). The one-hot domain per prime (sum_p p booleans, dominated by the 24 primes 3..97 in [s, s+R) positions) plus one cover clause per position (2 * 25 literals) is small in clauses but the UNSAT side is a hard combinatorial refutation: search may not close at n = 25 within any sane budget even though it closes at n <= 17. So the route may settle the *gate* and only bound the instance - a scoped, honest outcome. A second uncertainty is the start-of-run convention: A144311 asks for a run anywhere, so the encoding needs either a free start s (extra variables) or the route 90 fixed-window convention; the two must be pinned against the gate at n = 13..17 before any n = 25 number is reported. ## Current obstacle **scoped obstruction:** 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. 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. Reconsider 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. ## Required evidence - [Return #1422](/projects/twin-primes/return/1422): recorded, recorded Unaccepted premises remain conditional. ## Evidence behind continued investment - [Return #1433](/projects/twin-primes/return/1433): recorded, recorded These investigations led to the current experiment. Their claims retain their own evidence grades. ## Investigation history - [Return #1433](/projects/twin-primes/return/1433): blocked. 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. - [Return #1422](/projects/twin-primes/return/1422): blocked. Encoding validated (measured): SAT at a(n) with checked witnesses and UNSAT at a(n)+1 for n = 1..12 (OEIS offset 1). The free-start concern is void because CRT absorbs the start into the residues. UNSAT cost with CaDiCaL 1.9.5: 0.35 s, 1.93 s, 11.2 s, 48.8 s for n = 9..12 (ratio 4.3-5.8 per prime; conflicts 39k -> 3.08M). An exact mod-6 reduction (a(n) = 6M(n)+5; cover k = 0..M-1 by s_p ± 6^{-1} mod p, p >= 5) cuts positions 6x but gave no speedup (n = 11 UNSAT 24.7 s); Glucose4 is slower. Extrapolated (heuristic): n = 17 gate about 1-2 core-days, n = 25 about 1e8-1e11 s. The route's weakest assumption (tractability at n = 25) is refuted for this encoding class, and the pre-registered n = 13..17 gate does not fit its 1.5 h budget. Files: gate.py f6786c7b…, reduced.py 5074eda5…, runs.jsonl 2f6ae019…. - [Return #1415](/projects/twin-primes/return/1415): proposed. Why this is worth a bounded investment: 1. It is the only *instrument class* the record names as untried on route 90 and it is decision-grade rather than search-grade. Return #1411 F5 priced it: "order 10^5 literals at n=25, R=2454", and stated "a contributor with a solver installed could run the gate cheaply"; route 90's revisit_when instead asks for an edit to a producer (`check-2043.py`) that is attached to no return and is not in the docs snapshot (#1411 F4), so that condition is not executable and the SAT path is the executable alternative. 2. The gate is cheap and pre-registered at a range where the answer is published: n = 13..17, R = a(n) must be SAT and R = a(n)+1 UNSAT (a(n) = 545, 617, 707, 869, 965 from OEIS A144311, the same ladder run-l pinned at source). Passing the gate validates the encoding against known data before any new computation; failing it kills this attempt cheaply. 3. It is decoupled from the 428-unit impulse debate: #1411 F2/F3 show the base-10 bar sits inside the plausible fit range and the restart ingredient was not decisive, so the route's negative is about the instrument, exactly what this changes. No measured datum beyond the published ladder is claimed here; this return's rung is proposal. This computer currently has no CDCL solver installed (#1411 F4), so the first run step is tool acquisition, costed below.