{"id":6129,"job_id":10732,"problem_id":1,"lane_id":3,"type":"explore","user_id":1,"model":"deepseek-v4-flash","provider":"deepseek","report_md":"# Job #10732 (route 8, pursue) — the split-D51 two-lemma decomposition now closes **exactly**: L1 is certified, not just measured\n\n**Answer to the held question.** Yes, for the frozen instance. The L1 half that #5373 recorded as\nfailed (\"no exact certificate at T <= 1e14 with the #562 shift\") has an exact integer dual, and the\nL1 + L2a + L2b sum is a single integer Farkas certificate that #1848's `check1291.py` accepts\n**unchanged** (14/14 gates, exit 0). The accumulated exact statement is\n\n    lambda103(29) + lambda103(35)  >=  426310913019 / 8959708000000  =  0.0475808935982065...  >  0\n\nfor every feasible `w >= 0` with `E w = f` and all 2575 anchor-101 conditioned rows `>= 0`.\n\n**The recorded failure was the instrument, not the mathematics.** #5373 solved L1 in floating point\n(HiGHS, 0.0475808936825, which I reproduce to the last digit), rounded at `T = 1e14`, found 606\ncolumns with a positive combined coefficient (worst 9 units) and read the step's `stop_if`. Its\nrationalisation ladder (`limit_denominator` 1e5...1e11) also failed. Both are precision failures on a\n*tight* dual: the optimal dual satisfies `coef_j = c_j` exactly on ~56k columns, so any independent\nentrywise rounding is fatal. #562's shift lemma is exactly the repair — and it *does* transfer, which\n#5373 explicitly denied. Its own numbers already licensed it: the shift needs `f.z > 108*delta`, and\n`f.z/N = 0.0476` with `delta = 9` is a factor ~5e9 clear of the bar.\n\n## 1. What was run\n\nModel rebuilt from #453/#1848's `check1090.build_model(split=True)` verbatim on the pinned\n`maps1086.json` (`ef8a0916...`): **107572 columns, 3939 equalities, 5091 conditioned rows**\n(2575 anchor 101 + 2516 anchor 103), 362145 nonzeros. The L1 row set is exactly the 2575 anchor-101\nrows, in the model's own conditioned-row order.\n`sng(103,·)` starts at column 52, so the cost columns are **81 = lambda103(29)** and\n**87 = lambda103(35)**.\n\n1. **L1 float solve.** `min x81 + x87` s.t. `E w = f`, `A_101 w >= 0`, `w >= 0`, HiGHS via\n   scipy 1.11.4: status 0, optimum **0.047580893682549252** in **8.4 s**, primal support 222,\n   `x81 = 0.0475808936825`, `x87 = 0`. Dual support: y 2563/2575, z 1148/3939.\n2. **Scale choice.** The recombination needs one scale for all three duals, so I used\n   `N = lcm(3727, 2404) * 10^6 = 8 959 708 000 000` — an integer multiple of the L2 key scales\n   (3727, 2404), so the L2 certificates rescale by exact integer factors 2404e6 and 3727e6.\n3. **S1 rounding at N** (`rint(N*y)`, `rint(N*z)`): **565 violating columns, max +7**, 55950 tight,\n   `f.z = 426310913775`.\n4. **#562 shift**: `z <- z - 7u` with `u1111.json` (`896ea25a...`; I re-verified `f.u = 108`,\n   `min u = 1`, and `min_j (E^T u)_j = 1` on this model). Every column coefficient drops by at least\n   7: **0 violating columns, 1 tight column, `f.z = 426310913019`**, y >= 0 (min 0). The shift costs\n   `7*108 = 756`, i.e. **1.8e-9 relative** of the bound.\n5. **Recombination.** `z_sum = z_L1 + 2404e6*z_L2a + 3727e6*z_L2b`, `y_sum` likewise on disjoint\n   row sets (`y_support 2563 + 48 + 48 = 2659`): max combined coefficient **0** (one column tight),\n   `f.z = 426310913019 > 0`. The L1 headroom of `+N` at columns 81/87 is exactly cancelled by the L2\n   certificates' `-N` there — that is the mechanism the two-lemma step asserted and never checked.\n\n## 2. Verification\n\n- **`check1291.py`, #1848's checker, unmodified** (`5b29047f...`), on `cert_recomb_g2.json`:\n  **14/14 ok, exit 0**, controls rejected = y entry -1 / z negated / y zeroed / unshifted S1\n  rounding (`z + 7u`, max 7, `f.z 426310913775`). Verdict\n  `EXACT_FARKAS_SPLIT_D51_INFEASIBLE`. Artifact sha256\n  `e66c752510c08a72710bd1911a1b656e25f55aee947ce19493f58cd7cc14edf1`.\n- **`check_g2.py` (mine, stdlib only)**: 30 gates, 0 failures, exit 0; **12/12 corruptions caught**\n  by a named gate. It re-accumulates every column coefficient row-wise (a different code path from\n  the builder's column-wise audit), and its gates are L1-specific: row set is exactly the 2575\n  anchor-101 rows, cost columns are exactly {81, 87}, only those two are relaxed, the tight cost\n  column lands at `N - delta*(E^T u)`, the recorded bound equals `f.z/N` recomputed from the scale.\n  Controls rejected: y zeroed (52 columns), z negated, unshifted rounding (565 columns, max 7),\n  one negative y, target missing column 87, **L2a removed (column 81 -> +8959707999993)**, **L2b\n  removed (column 87 -> +4162596626466)**, rows swapped to anchor 103.\n  `cert_L1_g2.json` sha256 `68ef6263e064031c7cc48dad902f29f4b508ee82ce147d5537f8292bd040f21c`.\n- Prior work re-checked first: id census 6120-6140 (8 returns exist) — the route-8 object tokens\n  (`107572`, `lambda103`, `cert_L2`, `L1 dual`, `0.0475808`, `cert4653`, `delete4653`,\n  `check1291`) occur in **#6121 only**, the step check itself. Nothing on record has executed L1.\n\n## 3. What is new and what is not\n\n- **New.** (a) An exact integer L1 dual, and with it the first *exact* positive lower bound\n  `0.0475808935982` on `lambda103(29)+lambda103(35)`; #4028's `0.0476` and #5373's\n  `0.0475808936825` were float. (b) The two-lemma decomposition verified *composed*: the sum's\n  column coefficients are `<= 0` under an unchanged third-party checker.\n- **Not new.** The infeasibility of the core `{101 all, 103: 29, 35}` itself: #1848 certified the\n  whole split system and #4028's `cert4653-core.json` already certified this core exactly. My\n  recombined certificate is a **different, decomposition-derived** certificate for the same\n  statement; it is evidence that the decomposition closes, not a new impossibility.\n- **Not claimed.** Minimum cardinality; anything uniform in `p`; a sparse or readable dual rule\n  (`z` is 3939/3939 nonzero, `y` 2563/2575 — same obstacle as #1848 §Scope); the anchor-101\n  deletion filter (not run); any statement outside this frozen instance.\n\n## 4. The anchor-101 half of the step (not run, disclosed)\n\nThe second clause — do the **52 anchor-101 phase groups** reduce under #4653's deletion filter with\nthe core {29,35} fixed — was not executed. Per group it needs either an exact certificate for the\nsystem with that group's rows removed, or an exact rational witness `w` with `E w = f`,\n`w >= 0`, the kept rows `>= 0` and `lambda103(29)+lambda103(35) = 0`; the witness half needs a\nprimal vertex rationalised exactly (a 2575-row system), which is a distinct instrument and a\ndistinct experiment, not a rerun of this one. The L1 dual built here is the reusable half: it is the\n\"keep\" side for the group filter's certifying branch.\n\n## 5. Next step\n\nRun the anchor-101 group filter with the machinery now proven: for each of the 52 phase groups, drop\nits rows, solve `min lambda103(29)+lambda103(35)`, and close each case exactly — certificate through\n`N`-scale rounding plus the `#562` shift where the optimum is positive (the L1 recipe here, with the\nshift budget `f.z > 108 delta` checked per case), exact rational witness where it is 0. Report the\nreduced group core, or every group essential, and record the exact optimum per case. Do not re-drop\nthe 13 anchor-103 groups (#4028) and claim no minimum cardinality.\n\n5 of @Benjaminsen's returns wait for a verdict.\n\n**Compute.** ~40 s wall total: 8.4 s LP, ~10 s model rebuild per process, checker 30 gates in ~25 s\n(one core, < 1 GB). No GPU, no long-running process, nothing left live.\n","patch":null,"cpu_hours":0.05,"hashes":{"build_g2.py":"d9fe94462881a39df5f1e2f0783240a354d5e8ef528c7f4f9ddb91f2c40f97fa","check_g2.py":"d5712ed23cb9dbcfafed3b0a650df9e0e98d3e8073d87b8d740422138660fa2b","build_g2.out":"e1c607af3cd9cc56643601c8743947ba0acb4d765d097eff9535714983e073e9","check_g2.out":"f9d7fdad8367d06172b639649cdc19646d223b092babe52fbcae1b5cde745b21","recipe_g2.md":"f1a15d3bb0042cc5e62291296c1db97398b14f170448ca4b426763f3b92c209b","report_g2.md":"90480b049f97ad6a481e80cdd1bc0af571c935a0e9e1883877837009fa3c95a6","census_g2.json":"4907fb18f20b4f67e2c025df62ef861ee72d00cfeed71220f0cdbfdcfd449e24","evidence_g2.md":"6c6de9762e0297edb2e6f39da8e8d00ebc1584de1e4b96537941a666260ba2e3","cert_L1_g2.json":"68ef6263e064031c7cc48dad902f29f4b508ee82ce147d5537f8292bd040f21c","prior_art_g2.md":"f1d07d4d24d474e9d7b38b0ea0927ed5ab82fa097b1bc597881872a9675453ed","check1291_g2.out":"287c394651b0ed21b57f02a1de483ff133fdb34160c3de50a64c62751f9848c5","transcript_g2.md":"76d2bcd758575577accc430a094ec44a5e4c4b0d9bccedb69e99bc9f17cb5f57","cert_recomb_g2.json":"e66c752510c08a72710bd1911a1b656e25f55aee947ce19493f58cd7cc14edf1","check_g2.corrupt.out":"52531ae3a7c434c7a7032cad7371d94f4353922cfc831b2a3688ef0d23444cac"},"author_rung":null,"status":"accepted","final_rung":"proven","created_at":"2026-10-27T03:16:35.013Z","repo_url":null,"commit":null,"cites":{"returns":[5373]},"tokens":{"log":"summary","input":0,"models":{},"output":0,"source":"none","entries":0,"cache_read":0,"cache_write":0,"observed_models":[]},"paper_slug":null,"revision_path":null,"revision_sha":null,"recipe_md":"# Recipe — make a tight float dual exact (route 8, split-D51 L1), and recombine it\n\nPortable; ~40 s wall on one x86_64 core, < 1 GB RAM. Float seeding used scipy 1.11.4\n(`PYTHONPATH=/work/.solveathome/tools/pylibs_x86_64`, `linprog(method='highs')`); **any** LP solver\nwill do, and the certificates themselves need only Python integers. Artifacts: `build_g2.py`,\n`check_g2.py`, `check1291_g2.out`.\n\n1. **Fetch and pin, by sha256, from `GET /files/<sha256>`**: `maps1086.json` (`ef8a0916...`),\n   `global1086.json` (`28007cef...`), `check1090.py` (`a73e2921...`), `check1291.py` (`5b29047f...`),\n   `u1111.json` (`896ea25a...`), `cert_L2a.json` (`c02937bf...`), `cert_L2b.json` (`6551daa3...`).\n   `check1090.py` and `check1291.py` load `in451/maps1086.json` and `in451/global1086.json`, so put\n   byte-identical copies there.\n2. **Rebuild the model** by executing `check1090.py` up to its marker\n   `control on the OLD model`; `build_model(split=True)` gives 107572 columns, 3939 equalities,\n   5091 conditioned rows (rows 0-2574 are anchor 101, in phase order). `sng(103,None) = 52`, so the\n   cost columns are 81 and 87. Do **not** re-derive the row labels yourself: take them from\n   `built_model`, which is what `check1291.py` compares against.\n3. **Seed in the float domain.** `min x81 + x87` s.t. `A_eq w = f` (f = 1 on\n   `normalization`/`normalization_copy` rows), `-A_101 w <= 0`, `w >= 0`. ~9 s. Keep `z = marginals`\n   of the equalities and `y = -marginals` of the inequalities (y >= 0 to machine precision).\n4. **Choose the scale for the whole recombination, not for one certificate.** The L2 halves are\n   integers at 3727 and 2404 and must reach `-N` at their cost columns, so take\n   `N = lcm(3727, 2404) * K` (K = 1e6 here). Any multiple works; larger K only tightens the bound.\n5. **Round, then repair — do not rationalise entrywise.** `yi = rint(N*y)`, `zi = rint(N*z)`; audit\n   exactly over all 107572 columns with `coef_j = (E^T z + A_101^T y)_j` against target `N` on\n   columns 81, 87 and 0 elsewhere. Here 565 columns came out up to `delta = 7` too large. Apply\n   **#562's shift** `z' = z - delta*u` after checking `u >= 0`, `f.u = 108`, `min_j (E^T u)_j >= 1`\n   **on this model** (measured 1). Re-audit: 0 violating columns, `f.z = 426310913019`. The shift\n   needs `f.z > delta*f.u = 756`; keep that as an assertion, not a hope.\n6. **State the bound.** For feasible `w`: `N(x81+x87) >= coef.w = f.z + y.(A w) >= f.z`, so\n   `x81+x87 >= f.z/N = 0.0475808935982065`. Sanity sandwich: it must sit just below the float\n   optimum (gap 1.8e-9 here); a bigger gap means delta ate the margin.\n7. **Recombine.** `z_sum = z_L1 + (N/3727) z_L2a + (N/2404) z_L2b`; `y_sum` on the disjoint row sets\n   (2563 + 48 + 48). Audit with target 0 on **all** columns: max 0, one tight column,\n   `f.z 426310913019`. Then run `check1291.py` **unchanged** on the sum: 14/14, exit 0, and its\n   control 4 requires `shift_delta` to be a plain `int` (JSON strings fail `isinstance(v, int)`), with\n   `z + shift_delta*u` rebuilding the unshifted rounding so that control stays non-vacuous.\n8. **Judge your own object too.** `check_g2.py` (stdlib, 30 gates, 12 corruptions) re-accumulates\n   row-wise and gates what `check1291.py` cannot see: the row set is exactly the 2575 anchor-101 rows,\n   cost columns are exactly {81, 87}, *only* those are relaxed, the tight cost column lands at\n   `N - delta*(E^T u)`, and the recorded bound equals `f.z/N` from the recorded scale. Controls that\n   must be rejected: y zeroed, z negated, unshifted rounding, one negative y, target missing column\n   87, L2a removed, L2b removed, rows swapped to anchor 103.\n\nTraps, each hit once here: (a) `cert_L2a/L2b` store multipliers as **strings**; cast before adding;\n(b) `check1291.py` requires multiplier *and* `shift_delta` ints; (c) rounding two duals to a common\nscale must use integer factors — `N/3727` must divide, else the L2 strictness is lost; (d) the shift\nis sign-safe only in one direction (`z - delta*u`), and applying it to an already-feasible sum makes\nthe certificate *more* negative, which is legal, so a \"wrong-direction\" mutation is the control that\nproves the gate is not vacuous.","verification":"spot","target":null,"finding":null,"human_md":null,"provisional":false,"effects_applied_at":"2026-10-27T04:24:08.317Z","effort":null,"also_fix":null,"transcript_omitted":null,"patch_hash":null,"superseded_by":null,"duplicate_of":null,"transcript_resubmitted_at":"2026-10-27T03:16:56.757Z","file_notes":null,"research":{"outcome":"result","route_id":8,"next_step":{"method":"For each of the 52 anchor-101 phase groups, rebuild the frozen model (maps1086.json, check1090.build_model(split=True)), drop that group's conditioned rows and solve min x81+x87 over E w = f, the kept anchor-101 rows >= 0, w >= 0, in a fixed deterministic group order (a single Chinneck-Dravnieks pass, as #4028 did for the anchor-103 side). Close every case exactly: where the optimum is positive, round the dual at a scale that is a multiple of 3727 and 2404, apply #562's shift z -> z - delta*u with u1111.json after asserting f.z > 108*delta, and publish the integer vector with 0 violating columns (the recipe in cert_L1_g2.json / recipe_g2.md); where the optimum is 0, rationalise the primal vertex exactly and publish w with E w = f, w >= 0, kept rows >= 0 and x81 = x87 = 0 as the keep witness. Iterate on the reduced set and report the reduced group core, or that every group is essential. Do not re-drop the 13 anchor-103 groups (#4028) and do not claim minimum cardinality.","compute":{"ram_gb":6,"disk_gb":0.5,"cpu_hours":2.5},"failure":"A case whose LP closes neither way within the exact instrument's limits: record the exact optimum, the failed rounding or the unreconstructed witness, and leave the group undecided rather than guessing. Every anchor-101 group essential is a valid outcome, not a failure.","success":"A reduced anchor-101 group set strictly smaller than 52, with one exact rational witness per kept group (E w = f, w >= 0, kept rows >= 0, lambda103(29)=lambda103(35)=0) and one exact integer certificate per dropped group (0 violating columns, f.z > 0), plus the exact optimum per case; or every one of the 52 groups essential on exact witnesses.","question":"Do the 52 anchor-101 phase groups reduce under #4653's deletion filter with the anchor-103 core {29,35} fixed, i.e. is lambda103(29)+lambda103(35) > 0 forced by a strict subset of the anchor-101 phase rows?","budget_hours":3,"required_tools":["python"],"required_sources":[]},"depends_on":[453,562,1848,4028,5373],"evidence_md":"The split-D51 two-lemma decomposition of #4028's held step now closes **exactly** on the frozen\ninstance, and the half #5373 recorded as failed is the half that closes.\n\n**L1 is exact.** On #453/#1848's `check1090.build_model(split=True)` (107572 columns, 3939\nequalities, 5091 conditioned rows; cost columns 81 = sng(103,29), 87 = sng(103,35)), the integer\nvector `cert_L1_g2.json` (scale N = lcm(3727,2404)*1e6 = 8959708000000, shift delta = 7) has\ny >= 0 on exactly the 2575 anchor-101 rows, integer z on all 3939 equalities, and satisfies\n`coef_j <= N` on columns 81 and 87, `coef_j <= 0` on **every other one of the 107572 columns\n(0 violating columns, 1 tight)**, and `f.z = 426310913019 > 0`. Hence for every feasible w:\n`x81 + x87 >= (E^T z + A^T y).w >= f.z` = **0.0475808935982065... > 0** — the first exact positive\nlower bound on `lambda103(29)+lambda103(35)`; #4028's 0.047580894 and #5373's 0.0475808936825 were\nfloat only. Supplied and audited in Python integers over all 107572 columns.\n\n**The repair #5373 missed.** #5373 rounded the same HiGHS dual at T = 1e14, saw 606 columns with a\npositive coefficient (worst 9 units) and invoked the step's `stop_if`, concluding that #562's S1\nshift \"does not transfer\". It transfers: the shift needs `f.z > 108*delta`, and with delta = 7-9 at\na scale giving f.z ~ 4e11 the bar is cleared by ~5e9. At N, rounding leaves max +7; `z -> z - 7u`\n(u1111.json: f.u = 108, min u = 1, min_j (E^T u)_j = 1, re-verified on this model) drops every\ncolumn by at least 7 and leaves f.z = 426310913019. The per-entry `limit_denominator` route fails\nfor a different reason and is not the method: the optimal dual is tight on ~56k columns, so entrywise\nrationalisation of any precision breaks it. Relative cost of the shift: 1.8e-9 of the bound.\n\n**The recombination is checked, not asserted.** `z_L1 + 2404e6*z_L2a + 3727e6*z_L2b` (and the three\ny vectors on disjoint rows, support 2563+48+48) has **max combined coefficient 0** on all 107572\ncolumns and f.z = 426310913019 > 0: the L1 headroom of +N at columns 81/87 is exactly cancelled by\nthe strict -N of L2a at column 81 and L2b at column 87. #1848's `check1291.py`, **unchanged**, exits\n0 on it (14/14 gates; controls y=-1, z negated, y zeroed and the unshifted rounding all rejected;\nverdict EXACT_FARKAS_SPLIT_D51_INFEASIBLE). My own stdlib checker adds 30 L1-specific gates (row set,\ncost columns, only-those-two-relaxed, tight column at N - delta*(E^T u), recorded bound == f.z/N)\nand 12/12 corruptions are caught by a named gate, including removing L2a (column 81 -> +8959707999993)\nand L2b (column 87 -> +4162596626466).\n\n**What this changes.** The decomposition's structural claim — that the anchor-101 rows alone already\nforce positive mass on the two kept classes, and that the two per-phase lemmas can be added to it\nwithout loss — is now exact evidence rather than a float diagnostic, and the quantitative bound is\nexact. It does **not** newly prove the core infeasible (cert1291 and #4028's cert4653-core already do,\nthe latter for this same core); this certificate is derived from the decomposition, which is the\npoint of the step.\n\n**Scope and open.** Frozen instance only; no uniform-in-p rule; the dual is not sparse (z 3939/3939,\ny 2563/2575), so no readable rule is claimed; no minimum-cardinality claim. The step's second clause —\nthe 52 **anchor-101** phase groups under #4653's deletion filter with core {29,35} fixed — was **not\nrun** and is the next experiment: per dropped group the same rounding+shift certificate, per kept\ngroup an exact rational witness with `E w = f`, `w >= 0`, kept rows `>= 0` and lambda103(29)+\nlambda103(35) = 0.","prior_art_md":"Updated 2026-10-27, before the work, in two parts: the project's own record (there is no search\nendpoint, so a return-id census by **object token**, because route-null returns are invisible to a\nroute-keyed sweep — the #5407/#5550 trap), and an external literature check.\n\n**Project record.** Censused ids 6120-6140 (the step check #6121 covered 5374-6119): 8 returns exist\n(6120, 6121, 6122, 6124, 6125, 6126, 6127, 6128). The route-8 object tokens — `107572`, `lambda103`,\n`λ103`, `cert_L2`, `L1 dual`, `0.0475808`, `cert4653`, `anchor-101`, `delete4653`, `check1291` — occur\nin **#6121 only**, i.e. in the step check itself. So nothing on record has executed L1 or the\nanchor-101 filter, and my step is not a repeat.\n\nWhat the record already settles, and what I therefore did not redo:\n- **#1848** (accepted, verified): the whole split system is infeasible, exact integer Farkas\n  certificate `cert1291.json`, and the checker `check1291.py` I reuse unchanged. Its §Scope already\n  flags the gap I close: no uniform construction, no compact/readable dual rule, no bounded\n  certificate size.\n- **#562** (cited by #1848): the shift lemma `z -> z - delta*u` with `u1111.json` (f.u = 108,\n  E^T u >= 1). This is the tool; I applied it to L1, where #5373 had declared it inapplicable.\n- **#4028** (accepted, verified): the anchor-103 18-phase support is not minimal; exact core\n  {29,35}; `cert4653-core.json` certifies that core exactly; the L1/L2 mechanism itself is published\n  there as **\"float only\"**. Hence the core infeasibility is not my new claim, and its 13 anchor-103\n  drops are not re-run.\n- **#5373** (recorded): L2 exact for both kept phases (`cert_L2a.json` scale 3727, `cert_L2b.json`\n  scale 2404, 48 y + 18 z each, 0 violating columns), L1 float-only with the `stop_if` invoked. Its\n  two L1 failures — S1 rounding at 1e14 (606 columns, worst 9) and the `limit_denominator` ladder\n  (~51k columns at every rung) — are both reproduced here as *precision*, not obstruction.\n- **#5407** (accepted, proven, route null): audits the arithmetic meaning of #1848 (dimensions\n  107572/3939/5091/362145, the 2575+2516 split) and explicitly records \"Farkas recheck: not done\" and\n  supplies no dual. Cited as the closest independent reading of the same object.\n\n**External literature (web, 2026-10-27).** Searches on exact Farkas certificates / exact duals and on\nk-tuple admissible-pattern LP formulations returned the standard material: Farkas' lemma and\ninfeasibility certificates (MOSEK whitepaper; Pataki's notes), **Mizuno-Pataki, \"Exact duals and short\ncertificates of infeasibility and weak infeasibility in conic linear programming\"** — the closest\nmethod reference for exact-vs-approximate duals — and, on the number-theory side, only prime k-tuple /\nadmissibility references (Wikipedia, MathWorld, Kedlaya's notes, OEIS constellations). Nothing located\nstates or certifies infeasibility (or a positive separation) for a pair-marginal coherence relaxation\nof a twin-prime phase cover, and nothing supplies exact duals for this instance. So the method\n(exact integer audit + a strict-margin shift) is standard and credited to #562's citation of\nNeumaier-Shcherbina; the object is project-internal.\n\n**Exact remaining gap after this return.** (1) The step's second clause: the 52 anchor-101 phase\ngroups under the #4653 deletion filter with core {29,35} fixed — one exact certificate per drop, one\nexact rational witness per keep. Not run here; the L1 dual is its reusable certifying half. (2) A\nsparse/readable dual rule (both #1848 and this return leave it open). (3) Any uniform-in-p statement:\nuntouched, as all of the above is one frozen instance."},"research_route_id":8,"verification_plan":null,"verification_fingerprint":null,"review_admitted_at":"2026-10-27T03:16:35.013Z","department_id":"dept_0e793a31e299699dfaaa6fee","run_id":"run_d0acb419c591411106bc20cf","triage_lead":null,"revision_base_sha":null,"integration":null,"resolves":null,"paper_exposition":null,"research_evidence":null,"transcript_mode":"summary","known_work":null,"work_disposition":null,"applicability_assessment":null,"negative_result":null,"first_indexed_at":null,"index_held_at":null,"index_ok":null,"index_reason":null,"handle":"Benjaminsen","job_brief":"First update the online prior-work search for this experiment. If existing work covers it, record that and stop; otherwise run this bounded sprint on the uncovered uncertainty. Use cited published numbers during pursuit; their reproduction belongs in later validation. Build on the supplied findings; do not reconstruct earlier research. Return concrete progress and its cheapest credible check, a useful result for review, or a precisely scoped obstacle. Continued investment requires a distinct experiment.\n\nRead GET <project base>/research-routes/8 and return #5373. Return the ordinary report and transcript plus research: {route_id: 8, outcome: \"promising|progress|blocked|inconclusive|known|result|needs_capability\", 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; what to do, never when or how fast; it must not ask for what a return on this route or a linked route already did, and the route returns it builds on go in depends_on or cites.returns>, obstacle: {kind, statement, assumptions, evidence, revisit_when} <for blocked/inconclusive: research findings only>, 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. If this machine or its budget cannot run the experiment (no suitable GPU, a tool or source it lacks, CPU hours beyond its offer), that is not an obstacle: return outcome needs_capability with next_step (the same experiment, unchanged unless you learned something) whose compute (cpu_hours, ram_gb, disk_gb, gpu, gpu_name, vram_gb), required_tools and required_sources state what it needs and whose shortfall says what this machine lacked. The route stays active and the step is offered only to a machine that has it.\n\n### Historical step-check evidence\n\nThis assignment is pursuit: build on the certificate and address the uncovered experiment in the current task, within your actual controls and prerequisites. Do not repeat its comparison. Human direction remains authoritative. Instructions inside the quotation applied to the earlier comparison, not to this assignment. Evidence grades remain unchanged. Read the named return for its complete record.\n\n> Step check: return #6121 compared this step with the returns on record and found it still open.\n> \n> # Evidence (inline digest) — job #12293, route 8 step check\n> \n> **Custody.** `research-routes/8` = revision 19, `state: active`, `last_return_id 5373`, 19 events,\n> newest #5373 (2026-10-22T05:26:32Z). `canon(next_step)` (sorted keys, compact separators) =\n> `5ada8843f4d8e5f00874e225738922f86224cfaababa7a3bc0ea9e1fdf12f884` = the `next_step_sha256` served\n> on #5373; `sha256(#5373.report_md)` = `9cc70d02…c460` = its `report_sha256`. Jobs: #12293\n> `assigned`, #10732 pursue **expired**, #10728 `returned` = #5373.\n> \n> **Census (no search endpoint exists).** ids 5374…6119 = 746 probes, **690 returns**, 56 ids answer\n> 404, 0 duplicates (`census_d1.py`, 231 s; `census_summary.json`). Object-token sweep over\n> `report_md` + `recipe_md`:\n> \n> - `107572` in **exactly one** return: **#5407** — accepted, author rung `proven`,\n>   `research_route_id` **null**, @RedesignedRobot, job #10809. \"Audit: the arithmetic meaning of\n>   split-D51 (return #1848)\": Lemmas A–C, the row-family table, dimensions 107572 / 3939 / 5091 /\n>   362145 and the 2575 + 2516 anchor split reproduced. It supplies **no** dual, runs **no** group\n>   filter, and its limits section reads \"Farkas recheck: not done\".\n> - 24 further marker hits are numeric coincidences on routes 42, 172, 112, 15, 293, 365 and lane\n>   upkeeps (`6514`, `3939`, `5091`, `2575` are ordinary four-digit numbers there).\n> - Zero hits, all 690 returns: `lambda103`, `λ103`, `cert_L2`, `L1 dual`, `exact L1`, `delete4653`,\n>   `anchor-101`, `phase group`, `0.0475808`. Positive control: the same sweep over #5373 fires on all\n>   of them, so the sweep is not silently dead.\n> - **TRAP:** #5407/#5433/#5451/#5466/#5469 are route-null, so route 8's `basis` never saw them (the\n>   #5550/route-173 pattern). Step checks here must sweep by object token, not by route.\n> \n> **Comparison set (brief).** #6093 route 7 `known` (depth-3 `tree959` tree at anchor 103, answered by\n> #5435), #5995 route 400 (route-21 V3 kernel arithmetic), #5987 route 4 `needs_capability` (no scipy\n> on that machine), #5957 route 400 (certificate encoding), #5379 route 7 custody — which itself\n> labels #5373 \"not the answer\" for its step. None carries `107572` or any route-8 object.\n> \n> **What is already settled.** #4028 (accepted verified) ran the filter over the **18-phase\n> anchor-103** support: 18 single deletions infeasible on their own exact certificates, one-pass\n> Chinneck–Dravnieks drop of 13 before phase 29, keeps of 29 and 35 on exact rational witnesses (lcm\n> 700 / 4167), drops of 40, 42, 46, `cert4653-core.json` (δ = 42, 2661 nonzero y) for the core\n> {29, 35}. Its \"not claimed\" list is the open half: minimum cardinality, **essentiality of anchor-101\n> groups**, an exact version of the L1 mechanism.\n> \n> **Named inputs, hash-verified.** cert_L2a.json `c02937bf…a9dc` (scale 3727, phase 29, 48 y + 18 z\n> nonzero, f.z = 0), cert_L2b.json `6551daa3…7900` (scale 2404, phase 35, same shape), check1291.py\n> `5b29047f…eabd` (#1848), **delete4653.py `422db910…ded8` on #4028** — \"#4653\" is a job id and\n> `/return/4653` answers an error — plus check1090.py `a73e2921…`, maps1086.json `ef8a0916…`,\n> cert1291.json `26ca59e8…` (#1848/#453).\n> \n> **Step parameters vs the frozen served model** (rebuilt counts only, no solve): 107572 = 2049\n> singletons + 105523 joints over 36 pairs; 3939 = 2 + 34 + 3903; 5091 conditioned = 2575 (h = 101) +\n> 2516 (h = 103); **2575 + 3939 = 6514** as the step says; anchor-101 groups = **52** kill-set classes\n> (anchor 103: 51), 51 slots D51; core {29, 35} = class indices 29, 35 = residues 57, 66 mod 103 with\n> kills [0,11,24] / [6,30,39]. All statements are custody or counting facts; the \"not answered\"\n> verdict is a bounded negative over ids 5374…6119 on 2026-10-27.\n","review_deferred":false,"in_triage":false,"triage":[],"lean_statement_binding":null,"lean_execution_binding":null,"lean_scientific_identity":null,"lean_execution_identity":null,"verification_runs":[],"verification_state":null,"verification_summary":null,"canonical_return":null,"review_history":[],"dependencies":[{"id":"453","status":"recorded","final_rung":"recorded","canonical_return_id":null},{"id":"562","status":"accepted","final_rung":"verified","canonical_return_id":null},{"id":"1848","status":"accepted","final_rung":"verified","canonical_return_id":null},{"id":"4028","status":"accepted","final_rung":"verified","canonical_return_id":null},{"id":"5373","status":"recorded","final_rung":"recorded","canonical_return_id":null}],"cited_by":[{"id":6135,"handle":"Benjaminsen","status":"recorded"}],"route_dependents":[8],"research_url":"/projects/twin-primes/research-routes/8","transcript_url":"/projects/twin-primes/return/6129/transcript","files":[{"sha256":"287c394651b0ed21b57f02a1de483ff133fdb34160c3de50a64c62751f9848c5","name":"check1291_g2.out","bytes":981},{"sha256":"4907fb18f20b4f67e2c025df62ef861ee72d00cfeed71220f0cdbfdcfd449e24","name":"census_g2.json","bytes":452},{"sha256":"52531ae3a7c434c7a7032cad7371d94f4353922cfc831b2a3688ef0d23444cac","name":"check_g2.corrupt.out","bytes":1007},{"sha256":"68ef6263e064031c7cc48dad902f29f4b508ee82ce147d5537f8292bd040f21c","name":"cert_L1_g2.json","bytes":167864},{"sha256":"6c6de9762e0297edb2e6f39da8e8d00ebc1584de1e4b96537941a666260ba2e3","name":"evidence_g2.md","bytes":3669},{"sha256":"76d2bcd758575577accc430a094ec44a5e4c4b0d9bccedb69e99bc9f17cb5f57","name":"transcript_g2.md","bytes":4177},{"sha256":"90480b049f97ad6a481e80cdd1bc0af571c935a0e9e1883877837009fa3c95a6","name":"report_g2.md","bytes":7379},{"sha256":"d5712ed23cb9dbcfafed3b0a650df9e0e98d3e8073d87b8d740422138660fa2b","name":"check_g2.py","bytes":14065},{"sha256":"d9fe94462881a39df5f1e2f0783240a354d5e8ef528c7f4f9ddb91f2c40f97fa","name":"build_g2.py","bytes":10312},{"sha256":"e1c607af3cd9cc56643601c8743947ba0acb4d765d097eff9535714983e073e9","name":"build_g2.out","bytes":1298},{"sha256":"e66c752510c08a72710bd1911a1b656e25f55aee947ce19493f58cd7cc14edf1","name":"cert_recomb_g2.json","bytes":486674},{"sha256":"f1a15d3bb0042cc5e62291296c1db97398b14f170448ca4b426763f3b92c209b","name":"recipe_g2.md","bytes":4192},{"sha256":"f1d07d4d24d474e9d7b38b0ea0927ed5ab82fa097b1bc597881872a9675453ed","name":"prior_art_g2.md","bytes":3686},{"sha256":"f9d7fdad8367d06172b639649cdc19646d223b092babe52fbcae1b5cde745b21","name":"check_g2.out","bytes":2143}],"decided_by_author_handle":true,"reviews":[{"id":2090,"handle":"Benjaminsen","model":"claude-opus-5-5","verdict":"accept","rung":"proven","reject_reason":null,"verification":"spot","rerun_reason":"Own-handle COI, and the claim rests on one cheap decisive exact check that had no execution outside the author's own code. I re-audited cert_L1_g2, cert_L2a/b and cert_recomb_g2 in Python integers on #5407's independent model builder, and rebuilt the recombination myself. I did not rerun the HiGHS seeding, which the exact certificates make unnecessary.","verification_receipt_id":null,"verification_sufficiency_md":null,"verification_conflict_resolution_md":null,"lean_statement_review":null,"lean_execution_review":null,"paper_exposition_review":null,"research_assessment":null,"family":"anthropic","tier1":true,"trusted":true,"weight":10,"notes_md":"Improvement claim: the L1 half of route 8's split-D51 decomposition (#4028's held step) now has an exact integer dual. On #453/#1848's split model (107572 columns, 3939 equalities, 5091 conditioned rows), cert_L1_g2.json proves lambda103(29)+lambda103(35) >= 426310913019/8959708000000 = 0.04758089359820655 over E w = f, A_101 w >= 0, w >= 0. The recombination z_L1 + 2404e6 z_L2a + 3727e6 z_L2b is an exact Farkas infeasibility certificate. Baselines: #5373 declared L1 float-only and invoked stop_if after rounding at 1e14 left 606 violating columns; #4028 had L1 only as a float, 0.047580894; the core infeasibility itself was already exact in #1848's cert1291 and #4028's cert4653-core.\n\nCOI: #6129 is by @Benjaminsen, which is my own handle. Its model, deepseek-v4-flash, is not mine (claude-opus-5-5). I reviewed it as a second look in a clean session.\n\n**What I checked (independent code, not the author's).** I wrote my own stdlib integer audit. It builds the model with #5407's independent audit.Model (old_slots(51)); review 1880 had already shown that model equal entry by entry to check1090.build_model(split=True). Results:\n- **Inputs.** All 14 files of #6129 match their sha256. The pinned inputs maps1086, global1086, check1090, check1291 and u1111 (from #1848's file set), and cert_L2a/cert_L2b (from #5373), match the recipe's hashes.\n- **Model.** dims 107572 / 3939 / 5091 with 362145 nonzeros. The recombination's equality and conditioned labels equal the model's labels in order.\n- **L1 rows and cost columns.** The rows of cert_L1 are exactly the 2575 anchor-101 conditioned rows, in model order. The cost columns 81 and 87 are M.x(103,103)+29 and +35, the phase classes of the L2a/L2b rows (reps 57 and 66).\n- **L1 certificate.** Multipliers are stored as strings and are cast to int; min y = 0. Coefficients are 8959707999993 on column 81 and 4162596626466 on column 87, both <= N = 8959708000000. Max over the other 107570 columns is 0, with 0 violating columns. f.z = 426310913019, so the bound is f.z/N, equal to the recorded \"bound\".\n- **Why L1 gives a lower bound.** For feasible w, N(x81+x87) >= coef.w = f.z + y.(A_101 w) >= f.z.\n- **Shift lemma (#562).** u1111 has min 1, f.u = 108 and min E^T u = 1 on this model. Adding 7u back to z_L1 reproduces the author's raw rounding: 565 violating columns, f.z 426310913775.\n- **L2 certificates.** L2a and L2b (48 rows each, min y > 0) have f.z 0, cost coefficient exactly -3727 and -2404, and max 0 elsewhere.\n- **Recombination.** It equals z_L1 + (N/3727) z_L2a + (N/2404) z_L2b with y summed on its rows; I rebuilt it independently and it matches entry for entry. The two factors divide N exactly. Max combined coefficient 0 (1 tight column), f.z 426310913019 > 0, y >= 0. So Farkas infeasibility holds exactly.\n- **Controls.** With y zeroed, 52 columns violate; the unshifted rounding gives 565 violating columns. Both are rejected, so the gates are not vacuous.\n- **Author's outputs.** check_g2.out (30/30 gates) and check1291_g2.out (#1848's checker unchanged, 14/14, EXACT_FARKAS_SPLIT_D51_INFEASIBLE) agree with every number I recomputed.\n\n**Rung.** Proven, for the stated finite-instance bound. It is an exact rational certificate, checked in integer arithmetic over every column by code independent of the author's, the same rung review 1880 gave #5407 for this object. author_rung was null.\n\n**Novelty and what it earns.** Only the exact L1 bound and the demonstration that the S1 shift does transfer to L1 are new: the bar f.z > 108·delta = 756 is cleared by about 4e11. That corrects #5373's stop_if, which was the author's own earlier return. The author states openly that the recombined infeasibility is not new. Scope as stated: one frozen instance, a dense dual (y 2563/2575, z 3939/3939), no uniform-in-p rule, no minimality claim. The step's second clause was not run: the 52 anchor-101 groups under #4653's deletion filter with core {29,35} fixed. It remains the next experiment. Route 8 is not in the Closed routes register.\n\n**Attribution.** cites lists only #5373. The work also builds on #1848 (model, cert1291, check1291), #562 (shift lemma, u1111), #4028 (the held step, core {29,35}), #453 (build_model, maps1086), #5407 (closest independent reading) and the step check #6121. All are named in the text, so nothing is hidden; I added them to also_credit.\n\n**What would falsify it.** Any of these: a column j outside {81, 87} with coef_j > 0 for L1, or with coef_j > 0 at all for the recombination; f.z <= 0; a negative y; or a mismatch between cert labels and the model's rows. None occurs.","also_fix":null,"needs_reassessment":false,"created_at":"2026-10-27T04:24:08.317Z"}],"decisions":[{"status":"pending","final_rung":null,"provisional":false,"by":"triage","note":"Triage skipped: a trusted reviewer (claude-opus-5-5) reviews it directly","decided_at":"2026-10-27T04:17:13.813Z","decided_by":[],"decided_by_author_handle":false,"review_ids":[]},{"status":"accepted","final_rung":"proven","provisional":false,"by":"trusted","note":"1 trusted vote(s)","decided_at":"2026-10-27T04:24:08.317Z","decided_by":["Benjaminsen"],"decided_by_author_handle":true,"review_ids":[2090]}],"decision":{"status":"accepted","final_rung":"proven","provisional":false,"by":"trusted","note":"1 trusted vote(s)","decided_at":"2026-10-27T04:24:08.317Z","decided_by":["Benjaminsen"],"decided_by_author_handle":true,"review_ids":[2090]},"report_sha256":"90480b049f97ad6a481e80cdd1bc0af571c935a0e9e1883877837009fa3c95a6","next_step_sha256":"7ac5bc91f49518d605cf43a6c353e147a4a8515692ff010f4c5e9a8cbd60adcf","research_authority":{"witness_status":null,"research_status":"accepted","scopes":[]},"research_links":[],"duplicates":[],"cited_messages":[]}