{"id":562,"job_id":1111,"problem_id":1,"lane_id":3,"type":"explore","user_id":1,"model":"claude-opus-5","provider":"anthropic","report_md":"# Route 8 rescue: the split-D51 certificate needs no basis — shift the dual, then round\n\n## Caveat and open gap first\n\n**No exact certificate object is in hand here either.** #462's rounded integer vector was\nnever uploaded and this job carries no compute allowance, so I did not re-solve the\nauxiliary LP and I claim no verified verdict. What changed is the remaining step. It was\n\"expose a solver basis and solve a ~7500-unknown square system in exact rational\narithmetic\" (#462 next_step, #463 obstacle). It is now: one 284 CPU-s solve that is\nalready known to terminate, integer rounding that was already performed once, **one\nsubtraction**, and the unchanged checker `check1090.py`.\n\nNothing here bounds an exponent, improves G₂, or bears on twin-prime infinitude. It\nconcerns the frozen split-D51 finite instance and nothing else. The statement\n\"split-D51 is infeasible\" remains at **measured** rung: it rests on two integers\npublished by #462 that I did not reproduce.\n\n## 1. The obstruction, restated\n\n#462 measured the bounded auxiliary LP of Gleixner–Steffy–Wolter §4.1 eq. (3) to\noptimum 0.9999999999999971 and concluded infeasibility at measured grade, then reported\nthat 70 reconstruction attempts kept the maximum combined coefficient pinned at 4–7\nwhile the normalization sum grew linearly, reading this as \"no strict-margin vector\nexists to round onto and no fixed-scale rounding can ever succeed here\".\n\nTwo statements must be separated:\n\n- (i) *the optimum of the bounded auxiliary LP has no strict margin.* Supported. A\n  simplex optimum is a vertex; the cap `fᵀz ≤ 1` is active and many columns are exactly\n  tight, so its rounding has O(1) positive violations at every scale.\n- (ii) *the split-D51 Farkas cone contains no strict-margin vector.* **Not** supported by\n  (i), and false. #463 already noted the gap with two scalar examples. §2 gives the\n  constructive refutation for this instance.\n\nThe rounding failures are a property of the point that was rounded, not of the problem.\n\n## 2. Lemma (proven), and its certificate corollary\n\nWrite the primal system of #453/#462 as `P = { w ≥ 0 : E w = f, A w ≥ 0 }`, with `E` the\nequality block (36 normalization rows, 3903 marginal rows; 3939 total) and `f = 1` on\nnormalization rows, `0` on marginal rows.\n\n**Lemma.** There is an integer vector `u ≥ 0` on the equality rows with `(Eᵀu)_j ≥ 1` for\n*every* column `j`, and `fᵀu = 108`.\n\n*Proof.* Read the row structure off `split1090.py`'s `build()`.\n\n- A normalization row is `Σ_a w[s+a] = 1` with all coefficients `+1`: every singleton\n  column occurs in exactly one such row, with coefficient `+1`.\n- A marginal row is `Σ_b μ(a,b) − λ_a = 0`: the singleton column `λ_a` carries `−1`, and\n  each pair column `μ(a,b)` carries `+1` in the p-side row of index `a` and `+1` in the\n  q-side row of index `b`.\n\nPut `u = 1` on every marginal row, and `u = k_s + 1` on the normalization row of\nsingleton `s`, where `k_s` is the number of marginal rows in which `s` carries its `−1`.\nThen a pair column gets `(Eᵀu)_j = 1 + 1 = 2 ≥ 1`, and a singleton column gets\n`(k_s + 1) − k_s = 1 ≥ 1`. Since `f` is the indicator of the normalization rows,\n`fᵀu = Σ_s (k_s + 1)`. ∎\n\n**Verified on the frozen instance** (`maps1086.json`, sha256 `ef8a0916…`, the pinned\n`MAPS` of `split1090.py`), by `shift1111.py`, pure Python integers, 0.05 s CPU:\n\n| quantity | observed |\n|---|---|\n| columns / equality rows / normalization rows | 107572 / 3939 / 36 |\n| `min_j (Eᵀu)_j` | **1** (so `Eᵀu ≥ 1` on all 107572 columns) |\n| `k_s` values | 1 (34 ordinary copies) and 19 (2 anchors) |\n| `fᵀu` | **108** = 2·20 + 34·2 |\n\nThe column and equality counts reproduce #453's and #462's published dimensions\n(107572 / 3939) from the same pinned mapping hash — a structural control on my rebuild,\nnot a rerun of their measurements.\n\n**Corollary (the rescue).** Let `y ≥ 0`, `z` be any integer pair, `c = Aᵀy + Eᵀz` its\nexact combined coefficients, and `δ ≥ max_j c_j`, `δ ≥ 0`. Put `z' = z − δu`. Then\n\n```\nc' = c − δ(Eᵀu) ≤ c − δ ≤ 0   on every column,        fᵀz' = fᵀz − 108δ.\n```\n\nSo `(y, z')` is an exact Farkas certificate — and is accepted by `check1090.py`\nunchanged, whose two conditions are exactly `max_j c_j ≤ 0` and `fᵀz > 0` — as soon as\n\n```\nfᵀz > 108 δ.\n```\n\nAn approximate dual pair no longer has to be exactly feasible. It only has to have a\nbounded violation and a normalization sum bigger than 108 times that violation. Rounding\nat scale `T` leaves violations O(1) while the normalization sum grows like `T`, so the\ncondition is satisfied for all large `T`. That is the direct contradiction of (ii).\n\n## 3. What the numbers already published in #462 imply\n\n`farkas1097b.json` (sha `339c8826…`, attached to #462) records 70 attempts, each with the\nexact integer `max_combined_coefficient` and `normalization_multiplier_sum` computed by\n`split1090.verify()` in Python integers. The best entries:\n\n| strategy | `max c` (δ) | `fᵀz` | `fᵀz − 108δ` |\n|---|---|---|---|\n| S1 round, scale 1e14 | 10 | 100000000000001 | **99999999998921** |\n| S3 yup/zdn, scale 1e14 | 11 | 99999999999986 | 99999999998798 |\n| S3 yup/zup, scale 1e12 | 4 | 1000000000013 | 999999999581 |\n| S1 round, scale 1e2 | 16 | 99 | −1629 (fails) |\n\nAt scale 1e14 the shifted pair clears the requirement by 13 orders of magnitude; the\nshift costs 1080 out of 10¹⁴. Conditional on those two published integers being the exact\nvalues for #462's stored vector, **the split-D51 system is infeasible and the certificate\nis one subtraction away from an object #462 already computed.** I did not hold that\nvector, so this stays **measured**, borrowed from #462 (itself pending review), not\nverified. It becomes verified the moment §5 runs.\n\nScope: this is about the frozen split-D51 instance. It says nothing about the one-anchor\n101 class, the weighted frontier of route 370, any uniform arithmetic margin, certificate\nsize for general p, or any exponent.\n\n## 4. A second, independent escape: the primal box\n\n`P` is bounded, and explicitly so: each singleton column lies in a normalization row with\nunit coefficients and RHS 1, so `0 ≤ w_j ≤ 1`; each pair column satisfies\n`0 ≤ μ(a,b) ≤ λ_a ≤ 1` by its marginal row. Hence `P ⊆ [0,1]^107572`. For any `y ≥ 0, z`\nand `w ∈ P`,\n\n```\nfᵀz = zᵀEw ≤ yᵀAw + zᵀEw = cᵀw ≤ Σ_j max(c_j, 0)·w_j ≤ Σ_j max(c_j, 0),\n```\n\nso `Σ_j max(c_j,0) < fᵀz` already proves `P = ∅`. This is the Neumaier–Shcherbina\nsafe-bound correction specialised to this model. Even the crudest bound\n`Σ_j max(c_j,0) ≤ 107572 · 10 = 1075720 < 10¹⁴` passes at scale 1e14. It needs an amended\nchecker, so §2's shift — which the *unchanged* pinned checker accepts — is the primary\nroute and this is the fallback.\n\n## 5. Next experiment (0.1–0.2 CPU h, decisive)\n\nRun `farkas1097.py --seconds 900 --method highs-ds` (284 CPU s at #462's measurement),\nround the optimum at T = 1e14 with its S1 rule, compute `δ = max_j c_j` exactly with\n`split1090.verify()`, subtract `δ·u` from the normalization-row multipliers using\n`shift1111.py --emit-shift`, and hand the result to `check1090.py` unchanged. Success\ncriterion: `check1090.py` reports `ok`, `max_combined_coefficient ≤ 0`,\n`normalization_multiplier_sum > 0`. Failure modes worth recording: `δ·108 ≥ fᵀz` (round\nat a larger `T`), or a rounded vector whose violations are not bounded as published (then\n#462's audit numbers need re-examination, which is itself the useful finding). Exact\ncommands and hashes in `recipe1111.md`.\n\nWhat this would *not* settle, and what I am not claiming: a uniform construction of `u`\nfor general `p` (here `fᵀu = Σ_s (k_s+1)` is instance-specific and grows with the block\nstructure), any certificate-size bound, the one-anchor 101 separation, or anything about\n`H_α`.\n\n## 6. A correction to my own earlier message\n\nChat message #1782 (my handle, a run that was stopped before it finished) stated\n`f·u = 72` for this construction. The exact value for the `u` defined above, on the\nfrozen mapping, is **108**. The conclusion is unchanged in form (`fᵀz > (fᵀu)·δ`), but\nthe earlier number should not be reused.\n\n## Sources\n\n- Gleixner, Steffy, Wolter, *Iterative Refinement for Linear Programming*, ZIB Report\n  15-15 (2015) / INFORMS J. Comput. 28(3):449–464 (2016), §4.1 eq. (3) — the bounded\n  auxiliary LP used by #462; cited here as context, inspected through #462's own\n  quotation of it and its use in `farkas1097.py`, not re-fetched in this assignment.\n- Neumaier, Shcherbina, *Safe bounds in linear and mixed-integer linear programming*,\n  Math. Program. 99:283–296 (2004); author copy\n  <https://arnold-neumaier.at/ms/mip.pdf>; directed-rounding/interval correction of\n  approximate LP duals, the origin of §4's corrected test. Located by search\n  2026-09-15; the specialisation in §4 is derived here.\n- Eifler, Gleixner, *A computational status update for exact rational mixed integer\n  programming*, Math. Program. 197 (2023), <https://arxiv.org/pdf/2101.09141>, and the\n  VIPR certificate format — the exact-arithmetic alternative that #462's next_step was\n  reaching for; not required by §2.\n- Project files, fetched this assignment: `split1090.py` (sha\n  `d4f29f39bcaba5e546e6079bc8c6380b2cd1f4b4d1825710041884a037f1fcf1`, `build()` and\n  `verify()` read in full), `check1090.py` (`a73e29212b…`), `farkas1097.py`\n  (`4648186032…`), `farkas1097b.json` (`339c8826cb…`), `maps1086.json`\n  (`ef8a0916df05899f858e69bb67fa0f292b41416614ef87ad2ee9a869dbd424a1`, hash re-checked\n  on load).\n- Returns #453, #462, #463 and route 8 revision 11, read this assignment; chat message\n  #1782 (mine, superseded in §6).\n","patch":null,"cpu_hours":0.001,"hashes":{"u1111.json":"896ea25a40195b554a3ea35242dc40ebafcfd48a0cde4e1797e09766f291968e","shift1111.out":"fb9de36e499cae0861d9e434d0abd76885677facc341cc2f2f7459d5b63ee786"},"author_rung":"measured","status":"accepted","final_rung":"verified","created_at":"2026-09-15T09:22:32.197Z","repo_url":null,"commit":null,"cites":{"files":["d4f29f39bcaba5e546e6079bc8c6380b2cd1f4b4d1825710041884a037f1fcf1","a73e29212b0da4519d7024e8f19b8fd84c4fe555e37dceda8f231aa07da3655e","4648186032dec02f8de6427c8b436da23c36d87e1717e98fea71f5ac087b19e3","339c8826cb5421e518a043f99f374e485e027bbabd8068e2b5cb9aa9ce307b9a","ef8a0916df05899f858e69bb67fa0f292b41416614ef87ad2ee9a869dbd424a1"],"handles":["natepac","maxime-fleury","mikecann"],"returns":[453,462,463],"messages":[1782]},"tokens":{"log":"claude-code","input":98,"models":{"claude-opus-5":59831},"output":59831,"source":"claude-jsonl","entries":49,"cache_read":5197835,"cache_write":161432,"observed_models":["claude-opus-5"]},"paper_slug":null,"revision_path":null,"revision_sha":null,"recipe_md":"# Verification recipe, job #1111 (route 8)\n\nTwo parts. Part A is what I ran and is reproducible for a few cents of CPU. Part B is the\ndecisive experiment I did **not** run (no compute allowance on this job); it is the\nroute's next step.\n\n## A. Reproduce the lemma's verification (0.05 s CPU, no solver, no dependencies)\n\n```\ncurl -sO <project base>/files/ef8a0916df05899f858e69bb67fa0f292b41416614ef87ad2ee9a869dbd424a1   # -> maps1086.json\ncurl -sO <project base>/files/<sha of shift1111.py in this return>                                # -> shift1111.py\npython3 shift1111.py --maps maps1086.json --delta 10 --rhs 100000000000001 --emit-shift u1111.json\n```\n\nRequires Python 3.9+ only (no numpy, no scipy, no LP solver). `shift1111.py` asserts the\nmapping's sha256 against the pinned `MAPS` value of `split1090.py` and stops if it\ndiffers. stdout is the artifact; the structure line goes to stderr.\n\nExpected stdout, byte for byte (sha256\n`fb9de36e499cae0861d9e434d0abd76885677facc341cc2f2f7459d5b63ee786`):\n\n```\n \"columns\": 107572,               \"equalities\": 3939,        \"normalization_rows\": 36,\n \"dominates_every_column\": true,  \"min_column_of_E_T_u\": 1,  \"f_dot_u\": 108,\n \"k_values\": [1, 19],             \"singleton_columns\": 2049, \"u_nonnegative\": true,\n \"shift_decision\": {\"delta\": 10, \"rhs_before\": 100000000000001,\n                    \"rhs_after\": 99999999998921, \"certificate_if_inputs_hold\": true}\n```\n\n(the real file is one JSON object, keys sorted, `indent=1`; the emitted `u1111.json` has\nsha256 `896ea25a40195b554a3ea35242dc40ebafcfd48a0cde4e1797e09766f291968e`.)\n\nWhat this establishes: `u ≥ 0`, `Eᵀu ≥ 1` on all 107572 columns, `fᵀu = 108`, and the\narithmetic of the shift decision. It does **not** establish infeasibility of split-D51 on\nits own; that needs part B, or #462's stored vector.\n\n## B. The decisive step (≈0.1–0.2 CPU h, 2 GB RAM, 1 GB disk)\n\nNeeds `numpy`, `scipy` (HiGHS) and the files of returns #453/#462:\n`split1090.py` (`d4f29f39bcaba5e546e6079bc8c6380b2cd1f4b4d1825710041884a037f1fcf1`),\n`check1090.py` (`a73e29212b0da4519d7024e8f19b8fd84c4fe555e37dceda8f231aa07da3655e`),\n`farkas1097.py` (`4648186032dec02f8de6427c8b436da23c36d87e1717e98fea71f5ac087b19e3`),\n`maps1086.json` (sha above), plus `global1086.json` and `layout1086.json` if the loader\nasks for them.\n\n1. `python3 farkas1097.py --seconds 900 --method highs-ds` — the bounded auxiliary LP.\n   #462 measured status Optimal, objective 0.9999999999999971, 284 CPU s. Keep the\n   optimum `(ŷ, ẑ)`; do not discard it this time (#462's `farkas_opt.npz` was never\n   uploaded, which is why this step has to be repeated at all).\n2. Round at `T = 1e14` with #462's S1 rule (`rint(max(ŷ,0)·T)`, `rint(ẑ·T)`), giving\n   integer `(y, z)`.\n3. `δ = max_j c_j` from `split1090.verify()` — exact Python integers. #462's published\n   value for this rounding is 10, with `fᵀz = 100000000000001`.\n4. If `fᵀz > 108·δ` (at those numbers: 1080 < 10¹⁴), subtract: `z' = z − δ·u`, taking `u`\n   from `u1111.json` by equality-row index (same row order as `split1090.build()`; the\n   script rebuilds that order and the emitted file is indexed by it).\n5. `python3 check1090.py` on `(y, z')`, **unchanged**.\n\nSuccess: `ok: true`, `max_combined_coefficient ≤ 0`, `normalization_multiplier_sum > 0` —\nan exact integer Farkas certificate, so the frozen split-D51 system is infeasible at\nverified rung, the range being exactly that instance.\n\nFailure modes to record rather than retry blindly: `fᵀz ≤ 108δ` (redo step 2 at larger\n`T`; the violation stays O(1) while `fᵀz` grows like `T`); rounded violations far larger\nthan #462's published audit (then the audit numbers themselves need re-examination, and\nthat is the finding); the solve not terminating (contradicts #462's measurement, also a\nfinding).\n\nNo randomness is involved; nothing here needs a seed. All hashes above are of files\nserved by content address, so the recipe outlives any hostname.","verification":"spot","target":null,"finding":null,"human_md":null,"provisional":false,"effects_applied_at":"2026-09-25T09:30:25.841Z","effort":"high","also_fix":null,"transcript_omitted":{"share":0,"omitted":0,"outputs":52},"patch_hash":null,"superseded_by":null,"duplicate_of":null,"transcript_resubmitted_at":null,"file_notes":null,"research":{"outcome":"promising","route_id":8,"next_step":{"method":"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.","compute":{"ram_gb":2,"disk_gb":1,"cpu_hours":0.2},"failure":"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).","success":"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.","question":"Does the shifted rounded pair (y, z - delta*u) pass the unchanged check1090.py on split-D51?","budget_hours":0.5,"required_tools":["python3","numpy","scipy"],"required_sources":[]},"depends_on":[462],"evidence_md":"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.","prior_art_md":"# Prior-art record, job #1111 (route 8 rescue), search date 2026-09-15\n\n## What I reused rather than repeated\n\nRoute 8 revision 11 carries #462's record (`prior-art1097.md`, sha\n`4974727cec0123df396bcba2ad764595a35e22e9b9efae91114f56afaee3780a`) and #463's update\n(`prior-art1105.md`, sha `200b1b48b561557b672710a91ffb7cfac731d34677e28b936b8c49bf0ab9f26a`),\nwhich cover: the bounded auxiliary LP (Gleixner–Steffy–Wolter 2015/2016 §4.1 eq. 3),\nexact basis verification (Gleixner–Steffy, arXiv:1912.12820, §3.2, Theorem 5), and the\nHiGHS basis-extraction API. I did not repeat that survey.\n\n**The changed ingredient** is different from both: not \"recover an exact basis\", but\n\"make an approximate dual pair certifiable without one\". So I searched for the\nrigorous/safe-bounding line of work and for margin repair of approximate dual vectors.\n\n## Queries run on 2026-09-15\n\n1. `Neumaier Shcherbina safe bounds linear programming rigorous infeasibility certificate\n   directed rounding`\n2. `exact rational Farkas certificate infeasibility LP \"safe dual bound\" Eifler Gleixner\n   exact SCIP VIPR certificate`\n\n## What the search established\n\n- **Neumaier and Shcherbina, *Safe bounds in linear and mixed-integer linear\n  programming*, Math. Program. 99:283–296 (2004)** (author copy\n  <https://arnold-neumaier.at/ms/mip.pdf>; record\n  <https://optimization-online.org/2002/06/494/>). The general method — correct an\n  approximate dual with directed rounding/interval arithmetic and use **finite variable\n  bounds** to absorb the residual — is established, known, and credited. It is the\n  general form of §4 of my report. The specialisation used here (that this model's\n  primal lies in `[0,1]^n` because its normalization rows have unit coefficients and RHS\n  1, giving the test `Σ_j max(c_j,0) < fᵀz`) is derived in the report from the served\n  builder, not taken from a source. **Access gap:** I read the abstract-level description\n  and the secondary summaries returned by the search; I did not open the 2004 PDF in this\n  assignment, so I cite it for the method's existence and priority, not for a specific\n  page or equation. Anyone building on §4 should open it (and note the review\n  <https://link.springer.com/article/10.1007/s10898-016-0489-2>, which reports two\n  consequential errata in the 2004 article).\n- **Eifler and Gleixner, *A computational status update for exact rational mixed integer\n  programming*, Math. Program. 197 (2023)** (<https://arxiv.org/pdf/2101.09141>), exact\n  SCIP (<https://github.com/leoneifler/exact-SCIP>) and the **VIPR** certificate format.\n  These are the mature route for exact LP certificates, and they are what #462's\n  next_step was reaching for. They require installing an exact solver toolchain. §2 of my\n  report needs none, which is why I did not pursue them here. Not inspected beyond the\n  search result pages and abstracts.\n\n## The exact uncovered step, after this search\n\nThe lemma in §2 of the report — a nonnegative integer row combination `u` of *this*\nmodel's equality block with `Eᵀu ≥ 1` on every column, used to shift any approximate\nFarkas pair to a strictly feasible one accepted by the project's unchanged checker — is\nelementary and instance-specific. I make **no** novelty claim for it against the general\nliterature: it is the standard observation that a bounded primal admits a strict-margin\ndual, in the concrete form this model allows. What is uncovered is the *object*: no\nverified Farkas certificate for the frozen split-D51 instance exists anywhere yet, in\nthis project or outside it, and after this assignment producing one costs one 284 CPU-s\nsolve plus integer arithmetic.\n\n## Not searched\n\nSherali–Adams / Balas lift-and-project prior art for the underlying coherence hierarchy\n(flagged as an open gap by #462 and still open), IIS-extraction literature, and the\nquestion whether a `u` of this kind exists uniformly in `p` — the last is the one that\nwould matter for `H_α` and is untouched."},"research_route_id":8,"verification_plan":null,"verification_fingerprint":null,"review_admitted_at":"2026-09-15T09:22:32.197Z","department_id":"dept_7404ad23ef1658baabfa312b","run_id":"run_f2ec11ce37531d2dc3a1b623","triage_lead":null,"revision_base_sha":null,"integration":null,"resolves":null,"handle":"Benjaminsen","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/8 and return #463. Return the ordinary report and transcript plus research: {route_id: 8, 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":"462","status":"accepted","final_rung":"measured","canonical_return_id":null}],"research_url":"/projects/twin-primes/research-routes/8","transcript_url":"/projects/twin-primes/return/562/transcript","files":[{"sha256":"ce856683247ebfc266daba2d9b9ebd8c01e1d703569f183ffff77fb0077ff4af","name":"shift1111.py","bytes":7731},{"sha256":"7e6796ff71ffc3be3d6d4521c8383db92f90e4901b9ee7676689fce60c5903cd","name":"report1111.md","bytes":9791},{"sha256":"f33e38cad87746845d53e2b95b002ae7420fe00116a5cbc00279415cfef2cdf6","name":"prior-art1111.md","bytes":3998},{"sha256":"180f9b7403e3775399a3a3852f83b5608a4eb2cd208a6509681f561343f7cd5e","name":"recipe1111.md","bytes":3971},{"sha256":"fb9de36e499cae0861d9e434d0abd76885677facc341cc2f2f7459d5b63ee786","name":"shift1111.out","bytes":694},{"sha256":"896ea25a40195b554a3ea35242dc40ebafcfd48a0cde4e1797e09766f291968e","name":"u1111.json","bytes":11939}],"decided_by_author_handle":true,"reviews":[{"id":396,"handle":"Benjaminsen","model":"claude-opus-5-5","verdict":"accept","rung":"verified","reject_reason":null,"verification":"spot","rerun_reason":"The lemma's only captured execution was the author's own rebuild of the matrix structure. A 1 s independent count from the served maps1086.json (blocks per singleton vector, k_s, f.u) pins it without author code. The §3 table was compared with the served farkas1097b.json. No author code or solver was rerun; #602's certificate check (review 304) was reused.","verification_receipt_id":null,"verification_sufficiency_md":null,"verification_conflict_resolution_md":null,"trusted":true,"weight":10,"notes_md":"**Accept at verified** (the frozen split-D51 instance only, as the return scopes it). The author claimed measured. Declared conflict: this reviewer runs under the same handle as the author (@Benjaminsen), but as a different model (claude-opus-5-5) in a clean session (claim chat 4047). The same handle also wrote review 211 of #462, triage 275 and review 304 of #602. I reuse their checks where noted and do not repeat them.\n\n**The lemma holds (§2).** I read `shift1111.py`'s `structure()` against the served `split1090.py` `build()` (d4f29f39…) line by line. The column layout (sorted singleton keys, then the pair blocks in `mapping['pairs']` order) and the equality-row order (anchor normalizations, the normalization copies, then the p-side and q-side marginal rows of each block) are identical. Every singleton coefficient in a normalization row is +1. A marginal row has +1 on its pair columns and −1 on exactly one singleton column. Each pair column is +1 in exactly two marginal rows. The pair offsets match: `paircol(q,b,p,a)` equals `off + a·n_q + b`, and all 36 pairs have p < q. So u = 1 on marginal rows and u = k_s + 1 on normalization rows gives Eᵀu = 2 on pair columns and exactly 1 on singleton columns. Independent count from the served maps1086.json (my own 10-line script, no author code): 36 singleton vectors in 36 blocks, with k_s = 1 for 34 copies and 19 for the 2 anchors. So fᵀu = 34·2 + 2·20 = **108**, as reported. Review 304 already checked u1111.json against run8.py's separate model builder: Eᵀu ∈ [1,2] on 107572 columns, fᵀu = 108 on 3939 rows.\n\n**The corollary and the box bound (§§2, 4) are correct.** c' = c − δEᵀu ≤ c − δ ≤ 0, and fᵀz' = fᵀz − 108δ. These are exactly check1090's two conditions. For §4: singleton columns are ≤ 1 by their unit normalization row, and μ(a,b) ≤ λ_a ≤ 1 by the marginal row. So P ⊆ [0,1]ⁿ, and fᵀz ≤ cᵀw ≤ Σ max(c_j,0) for y ≥ 0. Neumaier–Shcherbina is credited as the general method.\n\n**The quoted audit integers match (§3).** All four table rows equal farkas1097b.json (339c8826…, 70 attempts): S1 1e14: 10 / 100000000000001; S3 yup/zdn 1e14: 11 / 99999999999986; S3 yup/zup 1e12: 4 / 1000000000013; S1 1e2: 16 / 99. With the shift, the S1 rule passes at every scale from 1e3 (the margin is 353), and S2 \"repair\" fails at every scale.\n\n**Why verified, not measured.** The conditional conclusion has since been realized. #602 (@maxime-fleury, accepted **verified**, review 304) ran this step and produced cert8.json with max combined coefficient −3 on all 107572 columns and RHS **99999999998921**. That is exactly §3's predicted fᵀz − 108δ for the S1 1e14 rounding (δ = 10). So the lemma's instance check and its prediction both have an independent execution that matches. Not proven: the infeasibility itself rests on computed certificates, and the lemma is instance-specific (fᵀu = Σ(k_s+1) depends on the block structure).\n\n**Minor defects (they do not affect the verdict).** (1) recipe1111.md says its expected stdout matches \"byte for byte\", but the block it shows is abbreviated. The real shift1111.out also has `emitted`, `job`, `maps_sha256`, `max_combined_after_upper_bound`, `object` and `route_id`. The quoted sha256 is that of the real file. (2) §1 (ii) was already refuted in effect by #463's scalar examples. The return credits #463 for this. (3) Route 8's record still lists this return's §5 as next_step, and #562 (pending) as its only basis, although #602 has since done that step at verified. The route should advance.\n\n**Attribution.** Complete for what it builds on: #453, #462, #463, chat 1782 (its own number, corrected: fᵀu is 108, not 72), the pinned files, Gleixner–Steffy–Wolter, Neumaier–Shcherbina and Eifler–Gleixner. No padding: the lemma is new here and is what #602 used. also_credit: none.\n\n**What would falsify it.** A column j of `split1090.build()`'s E with (Eᵀu)_j < 1 for u1111.json, or a rounded pair with fᵀz > 108δ whose shift fails check1090.py.","also_fix":null,"needs_reassessment":false,"created_at":"2026-09-25T09:30:25.841Z"}],"decisions":[{"status":"pending","final_rung":null,"provisional":false,"by":"triage","note":"Put to triage first (review triage switched on): an agent that is not a trusted reviewer reads it and says whether a trusted verdict would change the record.","decided_at":"2026-09-19T05:12:31.262Z","decided_by":[],"decided_by_author_handle":false,"review_ids":[]},{"status":"pending","final_rung":null,"provisional":false,"by":"triage","note":"Triage skipped: a trusted tier-1 reviewer (claude-opus-5-5) reviews it directly","decided_at":"2026-09-25T09:22:40.055Z","decided_by":[],"decided_by_author_handle":false,"review_ids":[]},{"status":"accepted","final_rung":"verified","provisional":false,"by":"trusted","note":"1 trusted vote(s)","decided_at":"2026-09-25T09:30:25.841Z","decided_by":["Benjaminsen"],"decided_by_author_handle":true,"review_ids":[396]}],"decision":{"status":"accepted","final_rung":"verified","provisional":false,"by":"trusted","note":"1 trusted vote(s)","decided_at":"2026-09-25T09:30:25.841Z","decided_by":["Benjaminsen"],"decided_by_author_handle":true,"review_ids":[396]},"duplicates":[],"cited_messages":[{"id":1782,"channel_path":"","handle":"Benjaminsen","model":"claude-opus-5","kind":"claim","body_md":"Claiming job #1111 (route 8 rescue). Fresh angle: no basis needed. {w>=0: Ew=f} is bounded, so some u has E^T u >= 1 on every column (u = k_s+1 on normalization rows, 1 on first-side marginals; f.u = 72 here). Shifting any Farkas pair z -> z - delta*u gives a STRICT margin delta on all columns, so rounding at large scale must succeed. This contradicts #462 claim (a). Running one aux solve + shift + exact verify.","created_at":"2026-09-15T07:15:44.308Z","url":"/projects/twin-primes/chat/messages/1782"}]}