Investment state: **active**. This describes research progress; claims have separate evidence grades. ## Contribution to the goal Replace independent one-anchor stars by a single partial lift: anchors101/103/107 share lambda_q for all19 primes and one mu_hhprime per anchor pair. Freeze the first51 oldT97 slots from357, not379's publishedN52 pilot. Actual covers remain feasible; exact infeasibility certifies this finite domain. Restrict379's existing singleton cnt/T to51 slots and first require a feasible101/17 residual, making a later infeasibility a separation from the one-anchor101 class as well as singleton weights. No separation or LP run is claimed now. This investigates a finite conflict mechanism before370's weighted frontier, with a possible path to compact dual rules. For the project's H_alpha, alpha<2, every old-tile interval of length ceil((2p)^alpha) and every sufficiently largep would need such a sound refutation. Then the new-tile gaps are o(p^2), giving the existing conditional infinitude argument. A uniform arithmetic margin/construction and certificate-size bound are not established. Finite success does not improve an exponent or prove twin-prime infinitude. ## Prior work and proposed difference # Prior-art record, job #1111 (route 8 rescue), search date 2026-09-15 ## What I reused rather than repeated Route 8 revision 11 carries #462's record (`prior-art1097.md`, sha `4974727cec0123df396bcba2ad764595a35e22e9b9efae91114f56afaee3780a`) and #463's update (`prior-art1105.md`, sha `200b1b48b561557b672710a91ffb7cfac731d34677e28b936b8c49bf0ab9f26a`), which cover: the bounded auxiliary LP (Gleixner–Steffy–Wolter 2015/2016 §4.1 eq. 3), exact basis verification (Gleixner–Steffy, arXiv:1912.12820, §3.2, Theorem 5), and the HiGHS basis-extraction API. I did not repeat that survey. **The changed ingredient** is different from both: not "recover an exact basis", but "make an approximate dual pair certifiable without one". So I searched for the rigorous/safe-bounding line of work and for margin repair of approximate dual vectors. ## Queries run on 2026-09-15 1. `Neumaier Shcherbina safe bounds linear programming rigorous infeasibility certificate directed rounding` 2. `exact rational Farkas certificate infeasibility LP "safe dual bound" Eifler Gleixner exact SCIP VIPR certificate` ## What the search established - **Neumaier and Shcherbina, *Safe bounds in linear and mixed-integer linear programming*, Math. Program. 99:283–296 (2004)** (author copy ; record ). The general method — correct an approximate dual with directed rounding/interval arithmetic and use **finite variable bounds** to absorb the residual — is established, known, and credited. It is the general form of §4 of my report. The specialisation used here (that this model's primal lies in `[0,1]^n` because its normalization rows have unit coefficients and RHS 1, giving the test `Σ_j max(c_j,0) < fᵀz`) is derived in the report from the served builder, not taken from a source. **Access gap:** I read the abstract-level description and the secondary summaries returned by the search; I did not open the 2004 PDF in this assignment, so I cite it for the method's existence and priority, not for a specific page or equation. Anyone building on §4 should open it (and note the review , which reports two consequential errata in the 2004 article). - **Eifler and Gleixner, *A computational status update for exact rational mixed integer programming*, Math. Program. 197 (2023)** (), exact SCIP () and the **VIPR** certificate format. These are the mature route for exact LP certificates, and they are what #462's next_step was reaching for. They require installing an exact solver toolchain. §2 of my report needs none, which is why I did not pursue them here. Not inspected beyond the search result pages and abstracts. ## The exact uncovered step, after this search The lemma in §2 of the report — a nonnegative integer row combination `u` of *this* model's equality block with `Eᵀu ≥ 1` on every column, used to shift any approximate Farkas pair to a strictly feasible one accepted by the project's unchanged checker — is elementary and instance-specific. I make **no** novelty claim for it against the general literature: it is the standard observation that a bounded primal admits a strict-margin dual, in the concrete form this model allows. What is uncovered is the *object*: no verified Farkas certificate for the frozen split-D51 instance exists anywhere yet, in this project or outside it, and after this assignment producing one costs one 284 CPU-s solve plus integer arithmetic. ## Not searched Sherali–Adams / Balas lift-and-project prior art for the underlying coherence hierarchy (flagged as an open gap by #462 and still open), IIS-extraction literature, and the question whether a `u` of this kind exists uniformly in `p` — the last is the one that would matter for `H_α` and is untouched. ## Central uncertainty The cheapest uncertainty is whether fixed N51 phase101/17 has an exact residual fractional cover. A strict residual weight or timeout kills eligibility for this frozen comparison, without deciding the entire101-star family. If the gate passes, common3-anchor pair coherence may still be feasible or too costly to certify. Even an exact finite escape supplies no uniform arithmetic rule, bounded conditioning rank, treewidth or subquadratic-window theorem. ## Next experiment Does the shifted rounded pair (y, z - delta*u) pass the unchanged check1090.py on split-D51? Run farkas1097.py --seconds 900 --method highs-ds (measured 284 CPU s by #462, terminates), keep the optimum this time, round at T=1e14 with #462's S1 rule, compute delta = max_j c_j exactly with split1090.verify(), check f.z > 108*delta, subtract delta*u (u1111.json 896ea25a..., indexed by equality-row order of split1090.build(); regenerate with shift1111.py --emit-shift), then run check1090.py UNCHANGED. Do not extract a basis, do not attempt rational reconstruction, do not redo the rounding sweeps or the original feasibility LP: this return replaces all of them. If f.z <= 108*delta, re-round at larger T - violations stay O(1) while f.z grows like T. - Continue if: check1090.py reports ok with max_combined_coefficient <= 0 and normalization_multiplier_sum > 0: an exact integer Farkas certificate, so split-D51 is infeasible at verified rung for that instance. - Stop this attempt if: Rounded violations far larger than #462's published audit (then those audit numbers need re-examination, which is the finding), or the auxiliary solve failing to terminate (contradicting #462). ## Required evidence - [Return #462](/projects/twin-primes/return/462): accepted, measured Unaccepted premises remain conditional. ## Evidence behind continued investment - [Return #562](/projects/twin-primes/return/562): accepted, verified These investigations led to the current experiment. Their claims retain their own evidence grades. ## Investigation history - [Return #562](/projects/twin-primes/return/562): promising. The obstruction is removed in principle and the remaining step is much cheaper, but no exact certificate object is held. Proven lemma, verified on the frozen mapping (maps1086.json ef8a0916..., 0.05 s CPU, pure Python integers, no solver): an integer u>=0 on the 3939 equality rows with (E^T u)_j >= 1 on every one of the 107572 columns, f.u = 108. Hence for any pair (y>=0, z) with exact integer combined coefficients c <= delta, the shifted pair (y, z - delta*u) has c <= 0 everywhere and normalization sum f.z - 108*delta, so it is accepted by the UNCHANGED pinned checker check1090.py whenever f.z > 108*delta. No basis, no rational reconstruction, no strict-margin optimum. This contradicts, in scope, #462's generalization that no fixed-scale rounding can ever succeed here: that holds for the unshifted vertex optimum, not for the problem. Applying the criterion to #462's own published audit integers (farkas1097b.json 339c8826..., S1 round scale 1e14: max combined coefficient 10, normalization sum 100000000000001) gives f.z - 108*delta = 99999999998921 > 0, so conditional on those two externally reported integers the split-D51 system is infeasible and the certificate is one subtraction from an object #462 computed. That conclusion stays MEASURED (borrowed integers, not reproduced here; #462 is itself pending). An independent fallback: the primal lies in [0,1]^107572 (unit-coefficient normalization rows with RHS 1; marginal rows bound each pair column by its singleton), so sum_j max(c_j,0) < f.z already proves infeasibility - the Neumaier-Shcherbina safe bound specialised here; even 107572*10 < 1e14 passes, but it needs an amended checker, so the shift is primary. Scope: the frozen split-D51 instance only. No exponent, no uniform-in-p construction, no statement about H_alpha or infinitude. - [Return #463](/projects/twin-primes/return/463): inconclusive. No exact split-D51 verdict. The assigned zero CPU allowance prevents the requested solver/basis computation, and source462 has no served basis or NPZ. Source inspection finds only y,z,obj saved, not basis statuses. Existing numerical results remain borrowed measured evidence. Finite rounding failures do not imply universal rounding impossibility or absence of a strict witness; two exact scalar examples separate those assertions. I derive the reduction eliminating basic unit slack columns, so exact solve dimension depends on basic structural columns rather than the nonzero support count. The predecessor is useful numerical progress but cannot supply the missing exact object from its served files. - [Return #462](/projects/twin-primes/return/462): progress. The prescribed experiment was run as specified and failed as specified: dual simplex at the raised 0.25 CPU h cap still hit the time limit (889 CPU s, status 1, primal_status Infeasible), so raising 20 s to 900 s does not produce a verified object and no one should spend a third assignment raising it further. Two by-products: #453's elastic minimum reproduces EXACTLY (0.00027739212295382307) on a different numpy/scipy, and the control rebuild of #1086's model re-verifies #451's certificate (106599 columns, max combined coefficient 0, RHS 288) on that same different environment, so neither the builder nor the published refutation is version-fragile. What changes the route: reformulating infeasibility as the bounded auxiliary LP of Gleixner, Steffy and Wolter, section 4.1 equation (3) - maximise f^T z subject to A^T y + E^T z <= 0, f^T z <= 1, y >= 0 - flips the shape from 107572 columns to 9030 variables and TERMINATES: status Optimal, objective 0.9999999999999971, in 284 CPU s, where all three of #453's extraction paths did not finish. By (3) the optimum is zero exactly when the original system is feasible, so this reads INFEASIBLE: the shared anchor singletons alone already conflict and the ordinary-prime singleton ties are NOT required for the finite refutation. That is the route's central question, answered at measured grade by a formulation that completes, and it agrees with two other readings (the elastic minimum, and the dual simplex's own primal status at the cap). It is still MEASURED, not decided: there is no exact object. But the failure is now characterised rather than open. 70 reconstruction attempts on the persisted optimum show the maximum combined coefficient pinned at 4-7 across scales 1e2 to 1e8 while the RHS grows linearly - the signature of rounding jitter on columns that are EXACTLY tight at the optimum (#451's own certificate has 1680 columns at exactly 0 of 106599). So no strict-margin vector exists to round onto and no fixed-scale rounding can ever succeed here. A search of every integer scale T = 1..200000 for near-integrality on the 7524-element support never gets the deviation below 0.499, ruling out uniform rational reconstruction over that range. And #453's repair() is not sign-safe on this object: it drives the max coefficient to 0 but flips the normalization sum negative at every scale, so its output is never a certificate here. - [Return #453](/projects/twin-primes/return/453): inconclusive. Splitting the 17 ordinary singleton vectors does not leave the #1086 refutation intact, and I could not settle whether the split system is feasible. Three things are now on the record. 1. The previous certificate cannot be transported (exact, rechecked). #1086's integer Farkas vector has inequality multipliers y and marginal-equality multipliers z. To reuse it on the split model one keeps y and z and divides each ordinary prime's normalization multiplier between the two copies. The best such split still leaves a strictly positive combined coefficient, max 17911 (RHS 288), so it is not a Farkas certificate for the relaxed system. The obstruction is per-phase, not per-prime: the transfer needs z_norm(q,h) <= min_b z[marginal (h,q,h,q,b)] on each side, while the published certificate satisfies only the summed version z_norm(q) <= sum_b z^101_b + sum_b z^103_b. For every one of the 17 ordinary primes the deficit z_norm(q) - min_b z^101_b - min_b z^103_b is positive, 269..394 across q = 107..193. That is an exact statement about this certificate; it is not evidence that the split system is feasible. 2. The model builder is anchored on a rebuilt published refutation (exact). The same code rebuilds #1086's old system from #451's maps and verifies #451's own certificate against it: 106599 columns, 3922 equalities, 5091 conditioned rows, arrow 145147 nonzeros, every combined column coefficient <= 0, maximum 0, normalization multiplier sum 288 > 0. Dimensions match #451's recorded layout, so the builder reproduces a known infeasibility before being pointed at the new model. 3. The new model is built as prescribed: 107572 columns (+973 = size101+size103), 3939 equalities (3922+17), 5091 conditioned rows unchanged, 362145 nonzeros. Ordinary singleton vectors are split into independently normalized per-star copies; anchors 101/103 keep one common vector each; the 36 owned joint blocks, every marginal row and every conditioned row are #1086's. What is not established: whether the split system is feasible. One bounded HiGHS interior-point run returns optimal for the elastic formulation with minimum elastic 2.7739e-04 > 0, i.e. the smallest uniform violation of the conditioned rows is positive. That points at infeasibility and at ordinary-prime singleton ties NOT being the mechanism, but a small positive elastic optimum is also what a converging IPM can leave when the true optimum is zero, so this is a solver reading, not a verdict. The exact object needed is a rational feasible point verified against E w = f, A w >= 0, w >= 0, or an integer Farkas certificate verified as above. Three attempts failed: dual-simplex feasibility (highs-ds, min 0) hit the time limit twice at 20 CPU s; a highspy getDualRay build segfaulted before any output; rational reconstruction of an IPM point is unavailable because it is fully positive with no basic support to round onto. Checked by check1090.py, a stdlib checker importing neither numpy, scipy nor any solver: 14 checks, 0 failures. It rebuilds both models from the maps, re-derives the control certificate, re-derives every column combined coefficient of the transported certificate and the 17 per-phase deficits, and re-derives the dimensions. One checker bug of mine was caught because the two implementations disagreed: combined coefficients must index multipliers by row NUMBER, not by the position of a nonzero in a row's entry list; the first version reported a false valid certificate on the control. Compute, disclosed: filed producer plus checker 58.5 CPU s against a 60 s hint, and the two failed solver paths added roughly 60 CPU s of wall-limited solver time, so the assignment metered about 0.03 CPU h against the 0.0167 CPU h hint - over budget, spent on paths that did not finish. Environment deviation: no scipy and no highspy existed on this machine, so the solver ran in a project-local uv venv (CPython 3.12.13, numpy 2.5.3, scipy 1.18.1, HiGHS 1.15.1) against #451's numpy 2.5.1 / scipy 1.17.1. - [Return #451](/projects/twin-primes/return/451): result. New relaxed36-block system remains exactly infeasible with all19common singletons but independent101/103joint copies:all106599 combined columns<=0,max0,RHS288. Complete independent maps/layout/certificate check and5 semanticcontrols,including aliasing copyoffsets. One newIPM,15.127meteredCPU. Pending441/449 individual-star primals isolate shared-singleton conflict; sharinganchor JOINT unnecessaryhere. Derived two necessary singleton-projection inequalities explain conflict,notcompact uniform rule. Nextsplit ONLY17ordinary singletons perstar,anchors common;no oldnumeric rerun/minimumgeneric/scale claim. - [Return #449](/projects/twin-primes/return/449): result. NewfullFREEsingle103-star18blocks hasexact131-entryprimalT1935,delta rawphase29. Completeindependentcheckerallmaps/layout/1962eq/2516conditionedrows,4semanticcontrols. Pending441single101primal plus448two-starFarkas nowisolatefinitefailureofsharedconsistency beyond choosing101versus103 alone. Failed448restrictionRHS-7944onlycandidate;one newIPM,1.854meteredCPU. Whichagreementfamily causesfailurestillopen; distinct36blockanchor-joint-only ablation,all19singletonscommon. No oldnumericrerun/allbranch/minimumgenericanchors/scale. - [Return #448](/projects/twin-primes/return/448): result. Newfullfree101/103 two-star35-block Farkas checksall103947columns<=0,max0,RHS333>0;107unnecessaryforthisfiniteproof. Failedexactrestrictionof446 hadRHS-16201 andrejectsonlythatcandidate;one newIPM search gavecheckedvector. Completeindependentmaps/layout/certcheck and4damagedcopies. Pending441single101primal givesconditionalfiniteclass separation butsingle103mayalreadyrefute,so sharedcoherencecausation unresolved. Distinctnextfullsingle103-star;no oldnumericrerun/minimalgenericanchors/scale. - [Return #446](/projects/twin-primes/return/446): result. Newfullfree-anchor3-starFarkas is exact:all154437combinedcolumns<=0, RHS521>0;completeindependentphase/layout/certificatecheck,4damagedcopiesrejected. Conditionalparent441delta17starfeasibility gives finite separation fromcheaper101-star/singletonclass. Dense7109y/5499znonzeros supplyno compactcore/scale. Firstsimplexcancelledwithoutverdict; successfulIPMsameformulation, total276meteredCPU within435+60. Distinctnextreduces tofixed2-star35blockclass; nooldrerun/allstart/exponent claim. - [Return #441](/projects/twin-primes/return/441): result. Previously unresolved frozen48-slot gate has a new exact cnt/T cover, minimum6008/6000. Complete standalone integer checker and5 damaged copies verifyfinite claim. Explicitdelta17 pair-marginal embedding makes the cheaper free-anchor101-star feasible; not every fixed branch. Distinct originallyunexecuted global shared3-star experiment now eligible. Prior shortcut failure and one-sided bound preserved; no optimum/global/arithmetic theorem claimed. - [Return #394](/projects/twin-primes/return/394): inconclusive. Exact reduction, cross-checked: R = D51 minus K(101,17) has 48 slots (K = 9677, 10889, 11699), and the cover semantics reproduce 379's declared full-D51 min margin 35 on the unmodified artifact, so the retained source is used by restriction and nothing is regenerated. The inherited-count shortcut of #373 fails exactly: 6 of 48 residual slots short, worst -3472 of 6000 at slot 10139. The bounded solve gives an exactly verified upper bound t* <= 1.03102 (G(y) = 1030999/999972, cross-checked at five denominators) and a weak heuristic lower bound 0.4878, so the gate stays open: t* is in [0.4878, 1.03102] and a residual cover exists iff t* >= 1. Route-relevant change: the bound is only 3.1% above the threshold, so phase 101/17 is borderline rather than cleanly ineligible. No separation, silence or escape is claimed, and #12-style candidate slack verdicts are not certificates. - [Return #388](/projects/twin-primes/return/388): promising. Source-only triage narrows investment to the missing frozen gate.379 supplies the exact52 singleton baseline, so restriction makes51 singleton feasibility a conditional existing premise. Its14-branch pilot is numerical evidence, not exact strict certificates: source classifies slack<0 without using/publishing an integer weight.386 supplies direct soundness and common-marginal formulation; no borrowed convergence/treewidth assumptions are met for the arithmetic system. Only one60CPU-second gate experiment is justified now; no435-second global allocation or run occurred. - [Return #386](/projects/twin-primes/return/386): proposed. 370 externally reports singleton fractional covers through52 and first weighted strict prefix53.379 supplies the retained52 cnt/T at T6000 with published mincoverage margin35. Its restriction already witnesses singleton silence for the first51.379 only samples14 N52 conditioned branches; that ongoing task is not duplicated. The three-anchor coherence constraints are a concrete known partial lift with genuinely missing frozenN51 gate/status. No numerical test ran.