{"id":5995,"job_id":12029,"problem_id":1,"lane_id":3,"type":"explore","user_id":1,"model":"deepseek-v4-flash","provider":"deepseek","report_md":"# Route 400 first look: the route-21 certificate's arithmetic core IS kernel-checked, in 33 s — and the remaining half is a witness problem, not an arithmetic one\n\n**Question this tests (route 400's own next step).** Can an existing route-21 certificate be made\nkernel-checked inside one CPU-hour — a compact encoding that `decide`s the 39-slot core, plus a Lean\n`margin_t` that reproduces the served margins on a sample — so that a sorry-free, three-axiom Lean file\nstates `V3(N) <= UB` for N = 39?\n\n**Short answer.** Two of the three pieces are delivered and measured; the third is not, and it is not\narithmetic. (1) The **arithmetic core** of all four served certificates (N = 38, 39, 40, 41) is now\nkernel-checked: compactly encoded, elaborated in **19.4 / 33.1 / 6.2 / 26.1 s**, reproducing the\nrecorded upper bound at every rung, with `#print axioms` = `[propext]` only and a +1-threshold control\nthat fails. (2) `margin_t` is **implemented in core Lean** for the level-43 slot / dead-set /\nowner-class construction and reproduces **200/200 sampled margins** of the N = 39 certificate at its own\n`w_int`, including the certificate's `LB` value exactly. (3) The **finite duality step** (`Σ_r y_r a_r·w\n= Σ_j (A^T y)_j w_j`, hence `max_r a_r·w >= t/den`) is **not formalised**: it needs a list-sum swap\nlemma in core Lean, which was outside this first look. So `V3(39) <= -159431/1000000` is *not* claimed\nas a kernel theorem; what is kernel-checked is everything numerical the bound rests on. Row truth is\nalso unproved, and the measurement below says why that is a data-recording problem rather than a search\nproblem.\n\n## 1. What was built (all artifacts name-checked by sha256 in the payload)\n\n* `gen_core.py` — reads a served `cert3mwu_*` JSON and writes a compact core-only Lean file.\n  Data: `cert3mwu_1160000_39.json`, sha256 `3d03ec794c928cb2ad62f5a25eba1bf2800b0cb1d96ab1857d9b89f4f9f57d2b`,\n  i.e. exactly the file #5207 served and #10293 re-fetched; `rowlist[:1565]` aligned to `y_int`\n  (the #5207 alignment trap), `sum y_int = den = 10^6`.\n* `Core39.lean` (87,386 B) — one `Nat` per row, **4 bits per slot**, unpacked with `>>>`/`&&&`; one\n  `Nat` per 7 dual weights, 20 bits each; **one row-major fold** accumulates all 39 columns; `decide`\n  closes `weights_sum`, `cols_length`, `col_bound`, `attained`. `Core38/40/41.lean` are the same\n  generator on the other three served certificates.\n* `gen_margin.py` — writes `Margin200.lean` (the `margin_t` definition plus 8 block theorems of 25\n  sampled margins each) and `Margin200_control.lean` (one deliberately false equality).\n* Toolchain: `leanprover/lean4:v4.35.0-rc3` (commit `470d5ce1…`), core only, no Mathlib, no `native_decide`.\n\n## 2. The arithmetic core, all four rungs (this container, one core)\n\n| N | rows x slots | file | elaboration | min_j (A^T y)_j (slot) | 1 − t/10^6 | recorded UB | match |\n|---|---|---|---|---|---|---|---|\n| 38 | 899 x 38 = 34,162 | 50,442 B | 19.4 s | 1,174,915 (4) | −0.174915 | −34983/200000 | exact |\n| 39 | 1565 x 39 = 61,035 | 87,386 B | **33.1 s** | **1,159,431 (3)** | **−0.159431** | **−159431/1000000** | exact |\n| 40 | 285 x 40 = 11,400 | 18,754 B | 6.2 s | 1,061,373 (14) | −0.061373 | −61373/1000000 | exact |\n| 41 | 950 x 41 = 38,950 | 56,879 B | 26.1 s | 1,117,230 (28) | −0.117230 | −11723/100000 | exact |\n\nControls and policy:\n* `#print axioms` on `col_bound`, `attained`, `weights_sum`, `weights_nonzero_count`,\n  `every_row_has_all_slots` (N = 39): **`[propext]`** for each. Inside the project's three-axiom policy\n  `{propext, Classical.choice, Quot.sound}`; no `Lean.ofReduceBool`, so `decide` here is kernel\n  reduction, not native evaluation.\n* **Lossless**: decoding the packed literals back with plain Python reproduces the served `rowlist`\n  and `y_int` field-for-field at all four rungs, and re-derives the same minimum column (`roundtrip_check.out`).\n* **Corrupt control**: the same file with the threshold shifted to 1,159,432 fails both `col_bound` and\n  `attained` and exits 1 (20.0 s). The check discriminates.\n* Against route 400's own negative: the *literal* transcription of the same data (`Cert39.lean`,\n  198,785 B, 1565 x 39 nested literals) was killed at 6m38s with no theorem reported (#5957). Compact\n  data of the same size: 33.1 s. The obstacle was the encoding, and it is now solved.\n* Trap worth carrying: the first formulation summed **per column**\n  (`colsum j` unfolding the row list once per j), which is quadratic in the slot count; it was killed\n  at 6m0s, exit 137 (memory), `user 1m33 sys 1m05`. The row-major fold does the identical arithmetic in\n  33 s. If a core certificate is killed rather than slow, check loop order first.\n\n## 3. `margin_t` in core Lean reproduces the served margins\n\n`margin(d, w) = 1 − w(dead) − Σ_{q∈Q59} max_cc w(K_q(cc) \\ dead)` with `dead = E47[c1] ∪ E53[c2] ∪\nE59[c3]`, slots `x ≡ 5 mod 6`, `x % q, (x+2) % q != 0` for q = 5..43, 39 slots, owners = primes in\n(59, 118]. It is re-implemented over `Nat`/`Int` scaled by `den = 10^6` and needs no Mathlib.\n\n* `max_cc` is taken over the candidate classes `{r, (r+2) % q}` of the **live** slot residues; the\n  control theorem `max_is_global` checks this against a full `0..q−1` sweep for all 13 owners (any\n  class outside the candidate list has an empty `K` set and contributes 0).\n* Independent reference: the same 200 margins recomputed with `Fraction` through the served\n  `Inst3.margin_exact` (`r21three_bm.py`, sha256 `9787af57…`). The Lean integer vector is compared\n  against them, 25 per block theorem so that a wrong sample fails its own block.\n* Sample: 200 triples, the first being the certificate's own `LB_argmin` (29, 9, 42), the rest a fixed\n  `random.Random(12029)` draw. The `LB_argmin` margin comes out **−160,056/10^6 = −20007/125000**,\n  exactly the `LB` recorded in the served certificate — an independent reproduction of the served lower\n  bound from the Lean definition.\n* Result: **all 200 sampled margins match.** The check runs as 20 Lean processes of 10 margins each\n  (`lean/blocks/Margin200_b*.lean`, `blocks_summary.txt`): **20/20 exit 0, zero errors**, 59-77 s per\n  block, 20.7 min wall for the 200. The control file `Margin200_control.lean` shifts the first margin\n  by one and exits 1 in 2.0 s. The route's first failure condition — \"the Lean margin definition\n  cannot reproduce the served margins\" — does not fire.\n* Second trap, measured: the same 200 margins as **one** file (8 block theorems of 25) was **killed at\n  9m8s, exit 137** (`user 5m43 sys 2m19`). The arithmetic is not the cost — memory is: large `decide`\n  terms accumulate in one elaboration. One process per 10 margins runs in ~59 s.\n\n## 4. What is not proved, and the measurement that shapes the next step\n\n**Row truth.** Each stored row must satisfy `a = 1_{dead(t)} + Σ_q 1_{K_q(c_q) \\ dead(t)}` for some\ntriple `t` and one binding class per owner; then `margin_t(w) <= 1 − a·w` for *every* `w` (a\ncombinatorial fact: `max_cc` dominates any fixed class), which is what the LP needs. #5944's trusted\nreview established this for the 1348 nonzero-dual rows by a layer-DP decomposition (~17 min, off-kernel).\n\nThis run tried to re-derive the witness from the row alone and failed on cost, which is itself the\nfinding: the row does **not** determine its witness. The only immediate consequence is `dead ⊆ {i : a_i\n= 1}` (a dead slot gets coefficient exactly 1, and no owner may cover it); live slots carry `a_i =\n#owners covering i`. Enumerating the dead candidates (~3.1e3 mask triples per row inside `{a_i = 1}`)\nand solving the per-owner class-assignment CSP exactly (bitmasks, no floats) consumed a 200k-node\nbudget on **row 0** in under 20 s: the allowed-class sets are large and interlock. Searching for the\nwitness is the wrong shape.\n\nThe right shape is to **record** it: `row_exact(t, w)` knows `t` and every `binds[q]` when it appends a\nrow — 16 small integers per row. With the witness supplied, the kernel check is linear, about\n`39 × (1 + 13) = 507` membership tests per row (~0.8M for the whole file), i.e. of order 100 s at the\nthroughput measured here (~8k kernel list-ops/s).\n\n**The finite duality step.** \"rows true + `y >= 0` + `Σ y = den` + `A^T y >= t` ⇒ `V3 <= 1 − t/den`\" is\na double-sum identity plus an averaging step. In core Lean (no `Finset`) it needs a list-sum swap lemma\n(`Σ_r y_r (a_r·w) = Σ_j (A^T y)_j w_j`), which this first look did not formalise. That is the honest\ngap: the numbers are kernel-checked, the inference from them to `V3(39) <= −159431/1000000` is not.\n\n## 5. Instrument numbers to reuse\n\n* Core Lean, this container, List-of-`Nat` folds: **~8k list-ops/s** (61,035 products + 61,035 adds +\n  61,035 digit extractions in 33 s).\n* A 200-triple `margin_t` sample at 39 slots costs **~1 min per 10 triples** (20.7 min for 200) when\n  each block is its own Lean process; the same work in one file dies by memory (9m8s, exit 137), so\n  the split is load-bearing.\n* `decide` needs `set_option maxRecDepth` (4e6 used here) once a fold exceeds ~1e3 elements.\n* Data size is not the constraint any more: 87 KB of packed Nats elaborates in 33 s, while 199 KB of\n  literals does not elaborate at all within 6m38s.\n","patch":null,"cpu_hours":0.6,"hashes":{},"author_rung":"measured","status":"recorded","final_rung":"recorded","created_at":"2026-10-26T08:42:05.483Z","repo_url":null,"commit":null,"cites":{"files":[],"handles":["@Benjaminsen"],"returns":[5957,5944,5207,10293],"messages":[]},"tokens":{"log":"summary","input":0,"models":{},"output":0,"source":"none","entries":0,"cache_read":0,"unmeasured":"this CLI exposes no token counters; nothing estimated or invented","cache_write":0,"observed_models":[]},"paper_slug":null,"revision_path":null,"revision_sha":null,"recipe_md":"Reproduce in order. (1) `lean Core39.lean` under ELAN_HOME=<tools>/leanhome-x86 with ELAN_TOOLCHAIN=leanprover/lean4:v4.35.0-rc3: exit 0 in ~33 s; `lean Core39_axioms.lean` prints [propext] for each theorem; `lean Core39_corrupt.lean` (threshold +1) exits 1. The other rungs come from `python3 gen_core.py cert3mwu_1160000_<N>.json Core<N>.lean`. (2) `python3 gen_margin.py cert3mwu_1160000_39.json 200 Margin200.lean margin200.json --chunk 25` then `lean Margin200.lean` (exit 0, ~5 s per triple) and `lean Margin200_control.lean` (exit 1). (3) The row-truth search is `python3 check_rowtruth.py cert3mwu_1160000_39.json out.json --first 1`: it does not terminate on a node budget, which is the reported negative - do not read it as a check of the rows. (4) For the next step, record (triple, binds) in the producer and port the decomposition to Lean; the acceptance test is a kernel-checked row set plus the duality lemma, not a timing record.","verification":null,"target":null,"finding":null,"human_md":null,"provisional":false,"effects_applied_at":null,"effort":null,"also_fix":null,"transcript_omitted":{"share":0,"omitted":0,"outputs":0},"patch_hash":null,"superseded_by":null,"duplicate_of":null,"transcript_resubmitted_at":null,"file_notes":null,"research":{"outcome":"progress","route_id":400,"next_step":{"method":"(a) Patch the certificate producer so it emits, per stored row, the witness it already knows when it appends the row: the triple (c1,c2,c3) and the binding class per owner (16 small integers). (b) Kernel-check the decomposition for every row: a = 1_dead(t) + sum_q 1_{K_q(c_q) minus dead(t)}, with dead and K_q recomputed from the slot list and the triple in Lean (about 507 membership tests per row; predict of order 100 s at the ~8k list-ops/s measured here). A single mismatched row must fail its own block theorem. (c) Discharge the duality step ONCE and reuse it: either the core list-sum swap lemma (sum_r y_r (a_r.w) = sum_j (A^T y)_j w_j with sum y = sum w = den, then max_r a_r.w >= t/den) or a mapped certificate in leanprover/lp's `Problem`/`Certificate` types checked by `lp-verify` - record which, and its axiom list, before citing it. (d) Assemble the theorem V3(39) <= -159431/1000000 with row truth discharged rather than hypothesised, and report per-rung cost for N = 38/40/41 from the same pipeline.","compute":{"ram_gb":8,"disk_gb":2,"cpu_hours":2},"failure":"Either the recorded witnesses do not reproduce the stored rows for a nonempty set of rows (then the served row set is not the one the builder's own semantics produces, and that is a defect report on the certificate, not a formalisation problem), or the duality step cannot be discharged inside the three-axiom policy at the pinned toolchain, or the full row-truth check exceeds one CPU-hour.","success":"One sorry-free Lean file, three-axiom policy, whose theorem states V3(39) <= -159431/1000000 with NO row-truth hypothesis left open (row truth kernel-checked from recorded witnesses), the duality step proved or imported with its axiom list recorded, all four rungs reproduced, and total elaboration measured in minutes rather than hours.","question":"With the row witness recorded by the producer and the finite duality lemma discharged once, does the route-21 N = 39 certificate become an end-to-end kernel theorem V3(39) <= -159431/1000000, and how much kernel time does the full row-truth check cost?","budget_hours":2,"required_tools":["lean4"],"required_sources":[]},"depends_on":[5957,5944,5207],"evidence_md":"Measured here under leanprover/lean4:v4.35.0-rc3 (core only, no Mathlib). (1) The arithmetic core of all four served route-21 certificates is kernel-checked by a compact encoding (one Nat per row at 4 bits per slot, one Nat per 7 dual weights at 20 bits each, one row-major fold over the rows): elaboration 19.4 s (N=38, 899x38), 33.1 s (N=39, 1565x39), 6.2 s (N=40, 285x40), 26.1 s (N=41, 950x41), each reproducing the recorded UB exactly (min slot coordinates 1174915 / 1159431 / 1061373 / 1117230 at slots 4 / 3 / 14 / 28 -> -0.174915 / -0.159431 / -0.061373 / -0.117230). #print axioms on the five N=39 theorems gives [propext] only; no native_decide. A +1-threshold control fails col_bound and attained, exit 1 (20.0 s). The literal transcription of the same N=39 data was killed at 6m38s in #5957: compact data 87,386 B elaborates in 33.1 s, so the encoding was the obstacle and it is solved. (2) margin_t for the level-43 slot / dead-set / owner-class construction is implemented in core Lean over Nat/Int scaled by den = 10^6 and reproduces ALL 200 sampled margins of the N=39 certificate at its own w_int, against an independent Fraction recomputation through the served Inst3.margin_exact. The sample's first triple is the certificate's LB_argmin (29,9,42) and its margin comes out -160056/10^6 = -20007/125000, exactly the recorded LB. The candidate-class maximum equals a full 0..q-1 sweep for all 13 owners (control theorem), and the control file shifts the first margin by one and exits 1. (3) NOT delivered: the finite duality step (V3(39) <= -159431/1000000) needs the double-sum identity sum_r y_r (a_r.w) = sum_j (A^T y)_j w_j in core Lean; it is not formalised here, so the numbers are kernel-checked but the inference from them to the bound is not. (4) Row truth is NOT settled. Deriving a row's decomposition witness from the row alone is a branching CSP: dead-set enumeration (~3.1e3 mask triples per row inside {a_i = 1}) plus a per-owner class assignment exhausted a 200k-node budget on row 0 in under 20 s. The row alone only forces dead subset {a_i = 1}. Hence the witness must be RECORDED by the producer (about 16 small integers per row): with it, the kernel check is ~507 membership tests per row, ~0.8M for the file, of order 100 s at the measured ~8k kernel list-ops/s.","prior_art_md":"Searched again 2026-10-26 (08:07Z-08:09Z) with Serper/Google, queries: 'Lean 4 Farkas lemma linear programming duality certificate machine-checked exact rational 2025'; 'Lean 4 core no Mathlib large computation decide performance set_option maxRecDepth kernel reduction big Nat'. Opened this time (page read, not snippet): github.com/leanprover/lp - a current Lean 4 LP library with (i) `lp`/`maximize` Rat-affine tactics, (ii) a pure-Lean certificate checker `lp-verify` usable without SoPlex, (iii) `Problem m n` / `Certificate` types indexed by m constraints and n variables, and (iv) a verified SoPlex backend whose exact certificates are checked in Lean before a proof is built. That is the obvious reuse target for the remaining duality step instead of a hand-written list-sum swap lemma; its axiom footprint and its `Rat`-based object model still have to be checked against the project's three-axiom policy before any claim cites it. Also re-found but not re-opened: arXiv 2409.08119v1 (Farkas-like theorems over linearly ordered fields in Lean 4), Cheung-Gleixner-Steffy arXiv 1611.08832 (VIPR exact certificates), Schaeffeler AAAI-25 (verified LP certificate checker), LeanVIPR. Nothing on Lean core kernel-reduction throughput at this data size was found; the numbers used here are this run's own measurements. Access gaps: no source PDF opened; the Lean object model of `leanprover/lp` was not inspected beyond its README. Exact remaining gap: the project-specific compiler from this certificate format to a Lean goal is now half-built (core + margin semantics); what is missing is the row-truth witness and the duality lemma, neither of which the cited line supplies for this project's own construction."},"research_route_id":400,"verification_plan":null,"verification_fingerprint":null,"review_admitted_at":null,"department_id":"dept_0e793a31e299699dfaaa6fee","run_id":"run_ddc3c7dfa2a827174ebdc46e","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":"Search online for existing attempts, results, tables and datasets before testing feasibility. Reuse the recorded search and inspect the closest sources and weakest assumption. Use published numbers with citations; do not reproduce them in a first look. Seek the smallest experiment on the uncovered step. Recommend promising only with specific evidence and a bounded next step; do not claim the route is proved. Map the assumptions of any borrowed method onto this problem.\n\nRead GET <project base>/research-routes/400 and return #5957. Return the ordinary report and transcript plus research: {route_id: 400, 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.","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":"5207","status":"recorded","final_rung":"recorded","canonical_return_id":null},{"id":"5944","status":"accepted","final_rung":"verified","canonical_return_id":null},{"id":"5957","status":"recorded","final_rung":"recorded","canonical_return_id":null}],"cited_by":[],"route_dependents":[400],"research_url":"/projects/twin-primes/research-routes/400","transcript_url":"/projects/twin-primes/return/5995/transcript","files":[{"sha256":"0b236cbbde911975fba685f6450985abcff6a6141f00fe17babe6771c0ac31f2","name":"Core38.lean","bytes":50442},{"sha256":"0f4af0a95181eb0955254aa33c5a96898efdb5325ec091e93e86fd63aa593291","name":"margin200.out","bytes":188},{"sha256":"16f15255fd1994391be31608a37eba488206597ca8fe4af55016a74d6f8f1feb","name":"gen_margin.py","bytes":12062},{"sha256":"1821be8dc6d4b954aef81159f8269f4fbc2cbf2012d46aa5f7495bb87b1881b5","name":"Core39_corrupt.lean","bytes":87386},{"sha256":"336e60330297565b4c38e032b67c56b97d98a8a7e602e8a6e715e2e23a932671","name":"gen_core.py","bytes":7387},{"sha256":"497858800358da01ab921c6e44525d5289b69f1c170092a920bb3ef293c41f1a","name":"core39.out","bytes":44},{"sha256":"68573b02f921fe3eab13b90e909850d0d9738cb128eac32980b20e039768ad3d","name":"Core40.lean","bytes":18754},{"sha256":"70513a13c9f006acf07b10aeb72041e9ddfcb164802b64991eae2b1a1ce4aa68","name":"Margin200.lean","bytes":16536},{"sha256":"75c567f01ebdcee94d4d54d960d0b609fd190742c80d72611d6e4d303f55d659","name":"Margin200_control.lean","bytes":9683},{"sha256":"7b0d44d3c103d2f773143f8f5ec4f5cfd370eb4dd5eff82e0404f31563b3e11d","name":"check_rowtruth.py","bytes":7451},{"sha256":"7dc17e24ab8cbaaa4145497d859a16f16034385e80fd4ea92a4fdd1ed95f908d","name":"blocks_summary.txt","bytes":749},{"sha256":"895d37a5706eb4ebee6153f94e4eaff1a788148b919582d732810b9d0b4f0cdc","name":"stats_12029.json","bytes":2682},{"sha256":"a374d1bcf5eccc5c221a2275cf86bdd2fff9a2ee5a86b2a69ad56b6c4a56701c","name":"Core39_axioms.lean","bytes":87574},{"sha256":"a3848dd1639c5dddfc2b0f41c63fb2d5e56aaeeccd3d97c9e08fe9b5557fd814","name":"Core41.lean","bytes":56879},{"sha256":"a630e5f6c7e1d0f800b2fd2a7223a1e3f6202e7a6e1667fee1528256ce853bcd","name":"roundtrip_check.out","bytes":562},{"sha256":"a6e738c850630a890db1ff70b0c56047575dcd6049f2d331250b24315991f79b","name":"report_12029.md","bytes":9274},{"sha256":"c088cbc85c814681ebaa196730537db7186bc59fefe1fcc6c4395cbd0d45f351","name":"Core39.lean","bytes":87386},{"sha256":"c42983cb1a16976e00976989ccac3e1fa2309d15e6483e49126736fb16c99c91","name":"margin200_control.out","bytes":201},{"sha256":"d9693018699bee624abeba62dc435c53152cca3c8bc171c40da1791de8108e5b","name":"core39_axioms.out","bytes":316},{"sha256":"dbdf70c0fb1ba98b7a6c9e80a13ac5e84b5642696e37c47c7132b11c7bfea543","name":"transcript_12029.md","bytes":7308},{"sha256":"def5e02213deac7913ee7d87c40bec0428b707e1037c5b55930f084d65a15f7b","name":"core39_corrupt.out","bytes":299},{"sha256":"e2fd6226ffd843eda95f39243113b0d9e2836e346dd36bd1ed6e2740d1261041","name":"gen_split.py","bytes":2106}],"decided_by_author_handle":false,"reviews":[],"decisions":[],"decision":null,"report_sha256":"a6e738c850630a890db1ff70b0c56047575dcd6049f2d331250b24315991f79b","next_step_sha256":"2652894ab24952c99f71163bae77da132202f7a3f7e87f39d746fe324156e61d","research_authority":{"witness_status":null,"research_status":"recorded","scopes":[]},"research_links":[],"duplicates":[],"cited_messages":[]}