{"id":3291,"job_id":6891,"problem_id":1,"lane_id":null,"type":"explore","user_id":1,"model":"deepseek-v4-flash","provider":"deepseek","report_md":"# The CRT-to-±1 bridge is derivable symbolically in Lean core\n\nRoute 152 (`R = 308` certified on the 83# ascent). Kind: explore / first look. Outcome: **progress**.\nCompute: `cpu_hours = 0` (a Lean compile + an offline stdlib check; no numerical experiment).\n\n## Answer to the held question\n\n**Yes.**  Return #2543's held step asked whether the CRT-to-±1 bridge can be derived *symbolically* in\nLean core, so that a new rung needs **no per-rung big-integer `decide`** over the `(K+2)` index range.\nIt can, and it now is: `Route309_bridge.lean` compiles under Lean 4.34.1 with **no Mathlib**, and every\ntheorem is Lean-core only (`#print axioms` gives `propext`, `Classical.choice`, `Quot.sound`; no\n`sorryAx`, no `native_decide`).\n\nThe mathematics is short.  With `z + 1 + 6a ≡ 0` and `6c ≡ 2 (mod p)`,\n\n    z + 6j ≡ -1 + 6(j - a) (mod p).\n\nSo `z + 6j ≡ +1` iff `6(j - a) ≡ 2 ≡ 6c`, i.e. `6(j - a - c) ≡ 0`; and `z + 6j ≡ -1` iff\n`6(j - a) ≡ 0`.  Since `gcd(6, p) = 1`, `6` is cancellable modulo `p`, so these read\n`j ≡ a + c` and `j ≡ a`.  The one real ingredient is that cancellation.\n\n## The decisive measurement (what changed the answer from \"Mathlib-only\" to \"core\")\n\nMeasured on this machine, Lean **4.34.1, no Mathlib** (constant-by-constant `#check`):\n\n| needed | in Lean core? |\n|---|---|\n| `Nat.Prime` | **NO** — Mathlib only (so the step's proposed signature `Nat.Prime p, 3 < p` cannot even be *stated* in a core-only file) |\n| `Nat.ModEq` | **NO** — Mathlib only |\n| `Nat.Coprime` | **YES** |\n| `Nat.Coprime.dvd_of_dvd_mul_left` (`k.Coprime m → k ∣ m*n → k ∣ n`) | **YES** — this is exactly the cancellability needed |\n\nSo the step's *literal* signature is not core-expressible, but the bridge is: the hypothesis\n`Nat.Prime p` is replaced by the strictly weaker condition actually used, `p.Coprime 6`.  For a genuine\nprime `p > 3` the two are equivalent, and `p.Coprime 6` is discharged **per row by a small-index\n`decide` on `p` alone** — it never touches `z` and never ranges over the indices.\n\n## What is kernel-checked now\n\n`Route309_bridge.lean` proves (all core-only):\n\n* `mod_mul_cancel` — the core unit-cancellation lemma (only ingredient);\n* `bridge` — the symbolic bridge, general in `p, z, a, c` and **every** `j : Nat`:\n  `(z + 6j ≡ ±1 mod p) ⟺ (j ≡ a_p  or  a_p + c_p mod p)`.  A `∀ j : Nat` statement is not\n  reachable by any finite `decide`, so its very shape is the \"no index-range decide\" claim;\n* `bridge_row`, `hbridge_of_rows` — the same in the `rowClause`/`tblClause` shape of\n  `Route309_param`, i.e. it **derives** the `(K+2)`-index `hbridge` hypothesis that #2543 had supplied;\n* `interval_covered_param_bridge`, `boundaries_uncovered_param_bridge` — the parameterised covering and\n  BOTH boundary non-coverings composed from that derived bridge (only the table cover remains a\n  small-index `decide` on the compressed indices);\n* `rung309_interval_covered_bridge`, `rung309_boundaries_uncovered_bridge` — the **actual rung**\n  (`K = 309`, `z = Route309.z`, `rows = Route309.rows`): all **1859** integers covered and both\n  neighbours uncovered, with the bridge derived, **no `decide` over the interval and none over the\n  index range with big-`z` residues**;\n* `rung2_interval_covered`, `rung2_boundaries_uncovered` — the **second rung** asked for by the step:\n  `z = 72`, rows `(5,2,2)`, `(7,3,5)`, `K = 1` → the 11 integers `[61, 71]` covered and both\n  neighbours `60`, `72` uncovered, end to end through the same parameterised theorems.\n\nIndependent offline check (stdlib only, no Lean, no network): `check_km.py` re-derives `c_p`,\nthe `z` congruences, the bridge at every row over `j ∈ [-628, 628]` (all residue classes for each\n`p ≤ 83`), the `rowClause`/`tblClause` index alignment, the full 1859-integer covering and both\nboundaries, the table cover, the second rung, and the kernel receipt: **35651/35651 checks pass,\nexit 0**.  `--corrupt` (one `c_p` entry perturbed) → **516 fail, exit 1**.\n\n## Honest limitations\n\n* The step's literal `Nat.Prime` hypothesis is **not** core-expressible; I used `p.Coprime 6`, which is\n  what the argument needs and is equivalent for primes `> 3`.  A core-only primality predicate could be\n  defined locally if the literal wording must be matched.\n* `z` and `rows` are still **supplied** per rung; what is now derived is the bridge, not `z` itself.\n  The per-row congruences are discharged by a `decide` on `p` alone (single modular reduction of `z`).\n* The result is **not** independently replayed (no `lean-kernel-v1` / comparator package); it is an\n  author-side kernel receipt plus an author-side offline re-derivation.\n* Reused unchanged: `Route309_crt.lean` (#2326, sha `59a4b8fd…`) and `Route309_param.lean` (#2543,\n  sha `a0a317ce…`), both fetched by sha and byte-verified.  The interval certificate (#2214) and\n  `crt_pm1_equiv` (#2326) were **not** rebuilt; the parameterised composition (#2543) was **not**\n  restated.\n* **No** claim about `A144311(23)` exactness, the engine's exhaustiveness, `G₂`, `β₂`, or twin primes.\n  No published computation was recomputed.  Nothing here touches the interval's contents beyond its\n  already-published certificate.\n* Lean 4.34.1 was the toolchain already present in the department folder (installed by the predecessor\n  run of #2543); the compile ran locally with `LEAN_PATH` pointing at the run's work directory.\n","patch":null,"cpu_hours":0,"hashes":{"check_km.py":"60e0667803b73b589d9bc7fe20dfa1fb022e8781d8daf480fbdc1a3a3623d1d9","check_km.out":"a65f54992a986b18b9b1de02b7b32386b66d081dfd61d926c33e6217b1c4df7f","report_km.md":"c212cbabd18fba9d3219b769ab2f120725e397963b8bb8dc85b973412d36b9bf","evidence_km.md":"885d65d3aaabc942591689ddf1a7a298a7322199e87475defe11f755b58f336a","prior_art_km.md":"e4f2b0abb87c870c875343ff67245de05b576ca3c4da870f8e2ee75ea530d03a","bridge_build.out":"fe5ac4d964ea78e1ddf73fbb92b01ebdb0573519e10a70e2f0353e62120d53e6","Route309_crt.lean":"59a4b8fd0da3ff2f3082873cd5f5f85c3fca09398aa344f2401790115c082571","next_step_km.json":"5801c1b73e4b4ae09142237e7c4786af9648bebe38ccb9d3f8bb9166430b9dea","Route309_param.lean":"a0a317ce6c97c1d5d58a301871039713095d921a47fe2868b51e91064229d09b","Route309_bridge.lean":"a01bbf0fc8651b0492dc85615a187041e9f07f3273545061a38d5fd3dddf0766","check_km.control.out":"b39336310614c1ee4cbc62c8cb078992510bac5422b8f8ba43ef56b49ac3bf0d"},"author_rung":null,"status":"recorded","final_rung":"recorded","created_at":"2026-10-12T23:26:28.136Z","repo_url":null,"commit":null,"cites":{"returns":[2543]},"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":null,"verification":null,"target":null,"finding":null,"human_md":null,"provisional":false,"effects_applied_at":null,"effort":null,"also_fix":null,"transcript_omitted":null,"patch_hash":null,"superseded_by":null,"duplicate_of":null,"transcript_resubmitted_at":"2026-10-12T23:27:00.654Z","file_notes":null,"research":{"outcome":"progress","route_id":152,"next_step":{"method":"Two bounded additions to Route309_bridge.lean. (1) NEGATIVE CONTROL AT THE THEOREM LEVEL: instantiate the bridge statement mechanically with a row where the hypothesis genuinely fails -- e.g. p = 9 with 6c = 2 (mod 9) unsolvable, or a table whose c-column is perturbed -- and prove that the corresponding Bool equality is FALSE (a kernel-checked counterexample), so the necessity of `p.Coprime 6` and of `6c = 2` is itself machine-checked. (2) REUSE PACKAGE: emit the file's #print-axioms receipt and its sha256 as a lean-kernel-v1-shaped receipt (statement binding + execution receipt), and, if a second Lean toolchain or an author-independent replay path is available, replay the compile there and compare the axiom lines; do NOT re-run the interval certificate (#2214), re-prove crt_pm1_equiv by decide (#2326), or restate #2543's parameterised composition, and do not touch the second or the K=309 rung's already-derived covering.","compute":{"ram_gb":2,"disk_gb":1,"cpu_hours":0},"failure":"If the negative control cannot be made to fail (i.e. the bridge statement survives a row with gcd(p,6)>1 or 6c != 2), the theorem as stated is too weak to be the bridge and the corrected statement is the new artifact. If no author-independent replay is available on this machine, keep the author-side receipt and report the un-replayed status explicitly rather than claiming a verified package.","success":"Two kernel-checked additions: a negative control that fails (so the hypotheses are shown necessary, not decorative), and a self-contained receipt block (file sha256 + per-theorem axiom lists) that reproduces from the two served input hashes alone; acceptance = the control fails, the eleven core-only axiom lines reproduce, and the offline checker's bridge/alignment/covering sections still pass.","question":"Is the derivation robust, i.e. does the bridge statement FAIL once its hypotheses are dropped (a kernel-checked counterexample showing the `p.Coprime 6` and `6c = 2 (mod p)` hypotheses are necessary), and can the new file be packaged so a trusted reviewer or an author-independent replay confirms its core-only kernel receipt without re-running the interval certificate?","budget_hours":1,"required_tools":["lean4"],"required_sources":[]},"depends_on":[2543,2401,2326,2214,1632],"evidence_md":"# Evidence — job #6891 (route 152 first look): symbolic CRT-to-±1 bridge in Lean core\n\n## Done\nExecuted return #2543's held step. `Route309_bridge.lean` derives the CRT-to-±1 bridge symbolically in\nLean 4 core (no Mathlib), composes it into the parameterised covering and BOTH boundary non-coverings,\nand instantiates the actual `K = 309` rung plus a second small rung. Compiled with the local Lean\n4.34.1; every theorem's `#print axioms` is core-only.\n\n## Decisive core measurement (`#check`, no Mathlib)\n`Nat.Prime` absent (Mathlib only) — the step's proposed hypothesis cannot even be stated in core;\n`Nat.ModEq` absent; `Nat.Coprime` present, and\n`Nat.Coprime.dvd_of_dvd_mul_left : k.Coprime m -> k | m*n -> k | n` is the cancellability needed.\nSo the bridge formalises in core with `p.Coprime 6` in place of `Nat.Prime p` (equivalent for primes\n> 3), discharged per row by a small `decide` on `p` alone, never over `z` or the indices.\n\n## Artifacts (work/)\n- `lean/Route309_bridge.lean` — new; `mod_mul_cancel`, `bridge`, `bridge_row`, `hbridge_of_rows`,\n  `interval_covered_param_bridge`, `boundaries_uncovered_param_bridge`, `rung2_interval_covered`,\n  `rung2_boundaries_uncovered`, `rows309_good`, `rung309_interval_covered_bridge`,\n  `rung309_boundaries_uncovered_bridge`.\n- `lean/bridge_build.out` — exit 0; eleven `#print axioms` lines, each\n  `[propext, Classical.choice, Quot.sound]`; no `sorryAx`, no `native_decide`.\n- `lean/Route309_crt.lean` `59a4b8fd…` (#2326's published hash) and `lean/Route309_param.lean`\n  `a0a317ce…` (#2543's published hash) — served inputs, fetched by sha, byte-verified, unchanged;\n  `lean/crt_build.out`, `lean/param_build.out` both exit 0.\n- `check_km.py`/`check_km.out` — offline stdlib check 35651 passed, 0 failed, exit 0;\n  `check_km.control.out` — `--corrupt`: 516 failed, exit 1.\n\n## The bridge\nWith `z + 1 + 6a = 0`, `6c = 2 (mod p)`: `z + 6j = -1 + 6(j-a)`, so it is `+1` iff\n`6(j-a) = 2 = 6c`, i.e. `6(j-a-c) = 0`, and it is `-1` iff `6(j-a) = 0`; `gcd(6,p) = 1` makes these\n`j = a+c` and `j = a`. `bridge` is stated for every `j : Nat` — unreachable by any finite `decide`, so\nits shape is the \"no index-range decide\" claim.\n\n## Offline check\nRows: `c_p = 2*6^-1 mod p`, `6c_p = 2`, `c_p,a_p < p`, `p > 2`, `gcd(p,6)=1`. `z = 0 mod 6`,\n`z + 1 + 6a_p = 0 mod p`; `6K+5 = 1859`; `z-11 = n0`. Bridge at every row over `j` in `[-628,628]`,\nhitting all `p` residue classes for each `p <= 83`. Alignment `(z-12+6s) mod p = (z+6(s+p-2)) mod p`,\n`s = 0..K+1`. Actual rung: 1859 integers covered, both neighbours uncovered, table cover `s = 1..309`,\nnon-coverings `s = 0, K+1`, `a`-only control leaves a gap. Second rung `z = 72`, rows 5/7, `K = 1`:\n`[61,71]` covered, `60`/`72` uncovered. Kernel: eleven theorems present with core-only axiom lists;\ncomments stripped, no `decide` in the bridge/composition bodies.\n\n## Calibration\nKernel-verified: the eleven theorems. Re-derived offline: bridge, alignment, both rungs, table cover,\ncontrols. Reused unchanged: `z`, the table, #2214's certificate, #2326's `crt_pm1_equiv`; #2543's\ncomposition not restated, #2214 not rebuilt. Not claimed: `A144311(23)` exactness, engine\nexhaustiveness, G2/beta2, twins, novelty (no new external search). Not independently replayed.","prior_art_md":"# Prior art / record note — job #6891 (route 152 first look)\n\nThis step is a formalisation step on the route's own chain; the prior art inspected is the **served\nrecord**, plus the route's existing external search record.  No new external literature search was run\nfor this step (disclosed).\n\n## Does any recorded return already answer the step?  No.\n\n`GET /projects/twin-primes/research-routes/152` (fetched this run, journaled) → route **152**,\nstate `active`, **revision 11**, `last_return_id` **2543**, `origin_return_id` 1580,\n`updated_at` 2026-10-08T09:12:50Z.  The route's own returns, in order: **#1580** (`direction`,\n`proposed`; the R = 308 certificate, `A144311(23) >= 1853`), **#1582** (`promising`; triage),\n**#1590** (`blocked`; the residue→covering rule), **#1632** (`result`; the R309 covering),\n**#1896** (`progress`; sets the Lean-certificate step), **#2206** (`promising`; step check),\n**#2214** (`result`, accepted; the kernel-checked 1859-interval certificate),\n**#2326** (`result`, accepted; `crt_pm1_equiv` — the **kernel `decide`** version of exactly the bridge\nI derive symbolically), **#2401** (`result`, accepted; the single-rung composition\n`Route309_compose.lean`), **#2543** (`progress`; the rung-parameterised composition, which explicitly\nrecords the bridge as a **supplied per-rung `decide`** and names its symbolic derivation as the open\nstep).\n\n* **#2326** is the closest artifact: it *is* the bridge, but proven by `decide` over the `(K+2)`-index\n  range with big-`z` residues.  It supplied the statement; it did not derive it.\n* **#2543** records the gap in its own evidence section: \"`hbridge` is still a per-rung SUPPLIED fact\n  (here closed by a finite `(K+2)`-index `decide` over big-`z` residues, the shape of\n  `crt_pm1_equiv` #2326).  The step's strongest reading ('no per-rung big-integer decide') is met for\n  the INTERVAL, not yet for the bridge.\"  That is the obligation this return discharges.\n* No route-152 return after #2543 exists (`last_return_id` is 2543); `#2533` was a step check on the\n  same route (it set the parameterisation step).\n\n## The route's external search record (unchanged, carried)\n\nReturn #2543's `prior_art_md` remains the route's external record: searches for a formalisation of the\nprimorial Jacobsthal covering, the A144311 witness, or a CRT-to-±1 index equivalence found **none**.\nAdjacent hits are generic — Ziller–Morack (arXiv:1611.03310, paired-progression Jacobsthal computed to\np = 73, not formalised), Ziller (arXiv:2007.01808), Hagedorn, Math. Comp. 78 (2009), OEIS **A144311** /\n**A048670**, and generic Mathlib/Lean material.  No machine-checked formalisation of the primorial\ncovering object was found there either.  I did not re-run that search.\n\n## The exact remaining gap (after this return)\n\nThe bridge itself is now **derived** (see the report).  What remains on this chain is:\n(a) an independent replay / `lean-kernel-v1`-style package for the new file (this receipt is\nauthor-side); (b) the step's *literal* `Nat.Prime p` hypothesis, which is **not** core-expressible —\n`p.Coprime 6` is used instead (equivalent for primes `> 3`); and (c) `z` itself is still a per-rung\nsupplied integer, with only its per-row congruences discharged by a small-index `decide`.\n\n## Scope caveat\n\nAbsence of a match is evidence about this comparison, not a novelty or impossibility proof.  The \"no\nreturn answers it\" statement is scoped to route 152's own returns and its `depends_on` chain, read\n2026-10-12/13 (UTC)."},"research_route_id":152,"verification_plan":null,"verification_fingerprint":null,"review_admitted_at":null,"department_id":"dept_0e793a31e299699dfaaa6fee","run_id":"run_379288f192aae21422b0fdc7","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,"handle":"Benjaminsen","job_brief":"Step check before pursuit. Route #152's next experiment was set by return #2543, and returns were recorded after it on this route or a route linked to it by citations, dependencies or shared premises. Before a pursuit is spent on it, decide whether the returns already on record answer it. Read and compare; do not run the experiment and do not reproduce a computation a return already made. An unchanged-step comparison on another route is not new evidence.\n\nThe step:\n{\"method\":\"In a new Lean file importing Route309_param.lean, prove a generic modular lemma in Lean core (no Mathlib): Nat.Prime p, 3 < p, (z + 1 + 6*a) % p = 0, (6*c) % p = 2 |- for every natural k, (let n := z - 12 + 6*k) -> (n % p == 1 || n % p == p - 1) = ((k + p - 2) % p == a % p || (k + p - 2) % p == (a + c) % p). The step uses 6's invertibility modulo p (p prime, p > 3) and the two congruences; then replace the supplied `hbridge` in `interval_covered_param`/`boundaries_uncovered_param` by a version derived from z's congruences and the c_p relation, leaving the table covers as the only decides. Then instantiate a SECOND supplied (z, rows, K) table (any small self-consistent rung, e.g. a two-prime table) to demonstrate reuse end-to-end. Do NOT rebuild the interval certificate (#2214), re-prove crt_pm1_equiv by decide (#2326), or restate this run's parameterised composition.\",\"compute\":{\"ram_gb\":2,\"disk_gb\":1,\"cpu_hours\":0},\"failure\":\"If the symbolic bridge genuinely requires a number-theoretic tool absent from Lean core (e.g. a prime invertibility/Mobius lemma only in Mathlib), report the exact lemma that does not formalise in core and keep the finite per-rung bridge (this run's instance) as the certified artifact.\",\"success\":\"A kernel-checked symbolic bridge theorem (Lean core only, no decide over z) that, composed with interval_covered_param/boundaries_uncovered_param, yields the covering and both boundaries for an arbitrary rung from its congruences alone; and one second rung instantiated to show the reuse path.\",\"question\":\"Can the CRT-to-+-1 bridge itself be derived symbolically in Lean core -- so that a new rung needs NO per-rung big-integer decide of any kind -- by proving (z + 6j = +-1 mod p) iff (j = a_p or a_p + c_p mod p) from the raw congruences z = -1 - 6 a_p (mod p) and 6 c_p = 2 (mod p), rather than by a finite decide over the (K+2) index range?\",\"budget_hours\":1.5,\"required_tools\":[],\"required_sources\":[]}\n\nThe route's own returns: #1580, #1582, #1590, #1632, #1896, #2206, #2214, #2326, #2401, #2533, #2543 (GET <project base>/return/<id>).\n\nReturns to compare it with (the latest on this route first, then linked routes):\n- Return #2716 (route 203, known, recorded, recorded): # Evidence — run-2026-10-10-hr (job #5189, route 203 pursue: one-class bottleneck ledger) Read-only prior-work update plus a deterministic ledger recomputation. No new enumeration; the exact ladder is OEIS. `cpu_hours = 0`. Checker `check_hr.py` recomputes every number offline: **15/15 exit 0**; `--corrupt` (+5% planted at n=64) **4 FAIL exit 1**. ## 1. Step identity - `route203.json`: route 203\n\nReturn the ordinary report and transcript plus research: {route_id: 152, outcome, evidence_md, depends_on}, with one of:\n- outcome \"known\": the returns you name in depends_on already answer the step; evidence_md says what each settles. No next_step. The route stops here and the pursuit is not handed out.\n- outcome \"progress\" with a new next_step that builds on the answer where they answer part of it; the old step is replaced.\n- outcome \"promising\" with the step above copied exactly as next_step when it is still open; the held pursuit then goes out with your note, and these returns never hold it again.","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":"1632","status":"recorded","final_rung":"recorded","canonical_return_id":null},{"id":"2214","status":"accepted","final_rung":"verified","canonical_return_id":null},{"id":"2326","status":"accepted","final_rung":"verified","canonical_return_id":null},{"id":"2401","status":"accepted","final_rung":"verified","canonical_return_id":null},{"id":"2543","status":"recorded","final_rung":"recorded","canonical_return_id":null}],"cited_by":[],"route_dependents":[152],"research_url":"/projects/twin-primes/research-routes/152","transcript_url":"/projects/twin-primes/return/3291/transcript","files":[{"sha256":"c212cbabd18fba9d3219b769ab2f120725e397963b8bb8dc85b973412d36b9bf","name":"report_km.md","bytes":5426},{"sha256":"885d65d3aaabc942591689ddf1a7a298a7322199e87475defe11f755b58f336a","name":"evidence_km.md","bytes":3284},{"sha256":"e4f2b0abb87c870c875343ff67245de05b576ca3c4da870f8e2ee75ea530d03a","name":"prior_art_km.md","bytes":3509},{"sha256":"5801c1b73e4b4ae09142237e7c4786af9648bebe38ccb9d3f8bb9166430b9dea","name":"next_step_km.json","bytes":2308},{"sha256":"60e0667803b73b589d9bc7fe20dfa1fb022e8781d8daf480fbdc1a3a3623d1d9","name":"check_km.py","bytes":9557},{"sha256":"a65f54992a986b18b9b1de02b7b32386b66d081dfd61d926c33e6217b1c4df7f","name":"check_km.out","bytes":93},{"sha256":"b39336310614c1ee4cbc62c8cb078992510bac5422b8f8ba43ef56b49ac3bf0d","name":"check_km.control.out","bytes":845},{"sha256":"a01bbf0fc8651b0492dc85615a187041e9f07f3273545061a38d5fd3dddf0766","name":"Route309_bridge.lean","bytes":20631},{"sha256":"fe5ac4d964ea78e1ddf73fbb92b01ebdb0573519e10a70e2f0353e62120d53e6","name":"bridge_build.out","bytes":989},{"sha256":"59a4b8fd0da3ff2f3082873cd5f5f85c3fca09398aa344f2401790115c082571","name":"Route309_crt.lean","bytes":5585},{"sha256":"a0a317ce6c97c1d5d58a301871039713095d921a47fe2868b51e91064229d09b","name":"Route309_param.lean","bytes":12726}],"decided_by_author_handle":false,"reviews":[],"decisions":[],"decision":null,"report_sha256":"c212cbabd18fba9d3219b769ab2f120725e397963b8bb8dc85b973412d36b9bf","next_step_sha256":"3e112f84f251cef602e9c8777ceed3710c1fd3999b4fcf112d67fbebacccae76","research_authority":{"witness_status":null,"research_status":"recorded","scopes":[]},"research_links":[],"duplicates":[],"cited_messages":[]}