{"id":2476,"job_id":5226,"problem_id":1,"lane_id":null,"type":"explore","user_id":1,"model":"deepseek-v4-flash","provider":"deepseek","report_md":"# Job #5226 — route 210 first look: the pinned natural-interval residue count does not certify a route-173 covering witness as it stands\n\nRoute 210 asks whether the exact natural-interval residue theorem (openai/math pin\n`adc7f1241b42e322a6451854ab7e4b4c146bf78a`, `OAI.Problem337`: `ResidueIntervalCount.lean`,\n`PeriodicResidueCount.lean`) can certify one existing route-173 cyclic covering witness under the\nproject endpoint conventions. Read: route 173, return #2022 (+ its served certificate and checker),\nreturn #2464 and the source map. Ran the smallest test on the mapping, not the route's ladder.\n\n## Result (exact finite, independently checked)\n\n**A direct application over-counts: it counts killed *integers in the raw span*, not killed base\n*slots*.** At the served 23# witness the 21 killed slots are accompanied by **202** integers lying in\nthe assigned residue classes (over-count ≈ 9.6×). The pinned theorem is exact and useful, but it is\na statement about consecutive natural numbers; a route-173 window is a run of consecutive **tile\nindices** whose values are sparse integers. So the certificate is **not** a direct instantiation of\nthe contract — a bridge is required.\n\n## What was established (each number has a reproduction)\n\n1. **Contract verified and endpoints frozen.** The pin's `card_range_zmod_mem` is\n   `#{n<N : n mod d ∈ S} = (N/d)·|S| + |{r∈S : r.N < N%d}|`; `zmod_predicate_Ico_discrepancy` bounds\n   the error by `|S|`, uniformly in length and endpoints. The pin uses **only** `Finset.Ico`\n   (half-open `[a,a+N)`); an `Ioc` convention is the one-step shift\n   `#{n∈(a,a+N]} = #{n∈[a+1,a+1+N)}`, so the route's \"freeze Ico/Ioc\" reduces to one contract.\n   `fly_cz.py` contract block: 4000 random small cases, **0 mismatches** vs brute force; the 7\n   explicit endpoint controls (`N=0`, lower-inclusive, upper-exclusive for Ico; upper-inclusive,\n   lower-exclusive for Ioc; `d=1` all/none) all pass.\n2. **Mapping gap, quantified at small bases.** At base 7 (`D=15`, `Q=[11,13]`) the best window has\n   `K*=4` killed slots and **wraps** (`start=13`, `start+K=17>D`); the literal value-interval counts\n   are `11→5`, `13→6`, i.e. 11 integers for 4 slots. At base 11 (`D=135`, `Q=[13,17,19,23]`) the\n   best window has `K*=10`; value counts `24,18,16,13` = **71** integers for 10 slots. (The base-7\n   window confirms the cyclic-interval split is a real, exercisable case; my first draft gave\n   *negative* counts precisely because it ignored the wrap.)\n3. **Served witness #2022 re-verified independently** (integer arithmetic, no producer code): the\n   copy solves `c·W ≡ −r_q (mod q)` for every `q∈Q`; all 21 positions are killed; both neighbours\n   survive; the positions are twin-opener residues mod 23#; `st=2149740` and the neighbours are the\n   adjacent tile slots. Only **one** of the 21 slots is struck by more than one prime\n   (`sum strikes = 22`, `union = 21`).\n4. **What the interval count would say about the witness:** per prime `29,31,37,41,43,47` the\n   value-interval counts are `42,40,34,30,30,26` = **202**, against 21 killed slots — over-count\n   `181`, positive for every prime.\n\n## Why this is the right reading\n\nThe route's own caveat (\"Natural integer intervals are not consecutive ordered base slots… count\ndiscrepancy alone proves neither a witness nor all-start exhaustion\") is confirmed and sharpened:\nthe value-space count is not merely weak, it is **wrong by construction** for slot counts, because\nnon-tile integers (e.g. even n, or n with a small prime factor) satisfy `n mod q ∈ S` but are not\nbase slots. Two faithful repairs exist and are now specified: (a) apply the *periodic* half of the\npin to the **index-space** predicate `P_q(i) = [a_i mod q ∈ {r_q, r_q−2}]`, whose period is\n`D·q` (observed `165=15·11` at base 7, `1755=135·13` at base 11; it is **not** the order of `W mod q`\nbecause `S` is not translation-invariant); or (b) keep the value count and subtract the exact\nnon-tile killed integers (a second wheel count). Either still needs a **union layer** — the window\nis covered by the union over `Q`, not the sum (`202−21` and `71−10` show the gap; the served witness\nshows the collision is 1 at 23#).\n\n## What this changes, and what it does not\n\n* It **does not** certify the witness or all-start exhaustion, and no number of these rungs yields\n  a uniform-in-`s` bound on `K*` or `maxsum`. Nothing here bounds `G2`, `β₂` or twin-prime\n  infinitude.\n* It **does** locate the exact additional obligation the route listed as open, with executed\n  controls (wrap, `Ico`/`Ioc`, brute-force cross-check) and a bounded repair. That is the decision\n  a first look owes: the proposed adapter is well-posed only after the index/union bridge is added.\n\n## Reproduction\n\n`fly_cz.py` (stdlib+numpy) writes `fly_cz.json`; `check_cz.py` (stdlib, no producer import) rebuilds\nthe formula, the tile, the kill predicate and the value-interval application and passes **29/29**,\nexit 0; `check_cz.py --corrupt` detects both planted mutations. Cost: ~seconds, ≤0.3 GB (the 23# tile\nsieve). Served artifacts cached under `served/`; the two pinned Lean files fetched read-only at the\npin (see `prior_art_cz.md` for exact locators and the CRLF-hash trap on `certificate.json`).\n\nAttribution: original analysis by this run; upstream Apache-2.0 sources cited, not republished.\n48 of @Benjaminsen's returns wait for a verdict; nothing for the person to do.\n","patch":null,"cpu_hours":0.05,"hashes":{"sah.py":"21a1d3556191bf54458b13fa0ebe41b4550fb92a33ab9bee6518d82ef222c843","fly_cz.py":"03735b629f75eb1da99f5e777d01225657539ae7802086b38ab289bc4e97c8e5","fly_cz.out":"13355906deea18e7a073486dc3ce97737983de13fe34032f2fa27b48308e611f","check_cz.py":"b1ced64f050aea7e43a0eded0ef30db813f6a71020bc9d64ae2e1b40c1b70ba9","fly_cz.json":"32d775c06d05ecc843d59d21659814dce3792b48d55f9153b28a473e61e4a9ec","check_cz.out":"30bb5242caadfae13517b2bd37b23f8358957fe6c6dff2db6c97790fa0b12756","recipe_cz.md":"3887541a37dd36ae1f9bd7da97e58c450ac12bf3dc736711c9341d63f1f8ffef","report_cz.md":"d87a48ffe8392cbbff95c260d2d491eafefaf5933affef99763d541af4bdc8db","evidence_cz.md":"b36bc42577f44c89dc60161101c2fc8720eaa7b430fb912d47f41e7000e4f9e0","next_step.json":"1c2b5dbff59aa7d3b7d21d295229f8cc44beafcceaadc0dd8a2225646ce57cf2","prior_art_cz.md":"fed9940b4130cfe9aa0c592b81222d4eddcb82e053ff8fe708753de9c0ed4da8","certificate.json":"b013f504cae641ab686ecba49339681d28c884caa785185c837061caa685d00f","check_cz.control.out":"7d5be84a773f835b84b5fe18b21f3b7f3eeaca2dabe627e26ac8d91bb8c64260","source-map-2026-10-07.md":"9269972845423dd6de39b1a80266456c5424b1ad63f3ddd262d240e5f71b5694"},"author_rung":"measured","status":"recorded","final_rung":"recorded","created_at":"2026-10-07T15:40:07.921Z","repo_url":null,"commit":null,"cites":{"files":[],"handles":[],"returns":[2464,2022,2017,720],"messages":[]},"tokens":{"log":"custom","input":0,"models":{"deepseek-v4-flash":0},"output":0,"source":"none","entries":0,"cache_read":0,"cache_write":0,"observed_models":["deepseek-v4-flash"]},"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":{"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":210,"next_step":{"method":"Freeze the pinned contract (Ico only; Ioc = one-step shift) and its discrepancy bound. Build the bridge: (a) index-space periodic predicate P_q(i) = [a_i mod q in {r_q, r_q-2}] with period D*q, applying the periodic-count half of PeriodicResidueCount.lean on consecutive SLOT indices; and (b) the value-space count over [a_start, a_last+1) corrected by the exact non-tile killed integers. Add a union/inclusion-exclusion layer over Q for the window, and split a wrapping window into two natural intervals (seen at base 7). Validate: small bases against exhaustive slot enumeration; then the served #2022 witness at 23# (start 2149740, copy 1698935976) requiring union = 21, both neighbours survive, and the per-prime over-count reduced to 0 for the bridge counts. Report each endpoint/wrap case explicitly and keep witness and all-start exhaustion separate.","compute":{"ram_gb":2,"disk_gb":1,"cpu_hours":0},"failure":"Any base where the bridge count disagrees with exhaustive slot enumeration, or the 23# witness cannot be reproduced, is recorded with the exact finite witness as a defect of the proposed adapter; no counting reformulation is claimed and no larger ladder is run.","success":"Both bridge variants agree with exhaustive slot enumeration on the small bases and reproduce the served 23# witness exactly (21 killed slots, neighbours survive), with every Ico/Ioc and wrap control passing; the value-space over-count (181 at 23#) is removed by an explicit, checked correction term.","question":"Does a faithful index/union bridge around the pinned residue count reproduce a served route-173 covering witness (all m killed slots and the two surviving neighbours) at bases 7#, 11# and 23#, with the value-space over-count removed and every endpoint and wrap case checked?","budget_hours":1,"required_tools":[],"required_sources":[]},"depends_on":[2022],"evidence_md":"Direct application of the pinned natural-interval residue count to a route-173 covering witness\ncounts killed INTEGERS in the raw span, not killed base SLOTS, so it is wrong by construction for\nthe certificate it was proposed to certify.\n\nEstablished (exact, finite, all checked offline):\n(1) Contract: pin OAI.Problem337 `card_range_zmod_mem` = `#{n<N: n%d∈S} = (N/d)|S| +\n    |{r∈S: r.val<N%d}|`; `zmod_predicate_Ico_discrepancy` ≤ `|S|`, uniform. The pin supplies ONLY\n    `Finset.Ico` (half-open [a,a+N)); `Ioc` is the one-step shift. 4000 random small cases match\n    brute force (0 mismatches); 7 endpoint controls (N=0, lower/upper inclusion each way, d=1) pass.\n(2) Mapping gap: base 7 (D=15, Q=[11,13], best K*=4, window WRAPS) value counts 5+6=11 vs 4 slots;\n    base 11 (D=135, Q=[13,17,19,23], K*=10) value counts 24+18+16+13=71 vs 10 slots.\n(3) Served witness #2022 independently re-verified: c·W ≡ −r_q (mod q) for all q; 21 positions\n    killed; both neighbours survive; positions are twin-opener residues mod 23#; only 1 of 21 slots\n    is struck by >1 prime (sum of strikes 22, union 21). Value-interval counts at 23#:\n    42,40,34,30,30,26 = 202 integers vs 21 slots (over-count 181, positive per prime).\n\nWhat it changes: the proposed adapter is well-posed only after an explicit index/union bridge —\n(a) apply the periodic half of the pin to the index-space predicate P_q(i)=[a_i mod q ∈ {r_q,r_q−2}]\nwith period D·q (observed 165=15·11, 1755=135·13; NOT the order of W mod q, since S is not\ntranslation-invariant), or (b) subtract the exact non-tile killed integers from the value count —\nplus a union/inclusion-exclusion layer and a cyclic split for wrapping windows (base 7's window).\n\nScope: first look only. This certifies neither the witness nor all-start exhaustion; no uniform\nbound on K* or maxsum, and nothing on G2, β₂ or twin-prime infinitude. Reproduce via fly_cz.py /\ncheck_cz.py (29/29, exit 0; --corrupt detects 2 planted mutations).","prior_art_md":"Bounded online search (2026-10-07) plus the served prior-art records, then the exact remaining gap.\n\nSearched: \"exact count of residue classes in an interval, error bounded by the number of classes\";\n\"generalised Jacobsthal function paired progressions CRT covering base slots twin primes\". Sources\ninspected: Ziller & Morack, *Divisibility in paired progressions, Goldbach's conjecture, and the\ninfinitude of prime pairs*, arXiv:1706.00317 (they generalise Jacobsthal to progressions of\nconsecutive integer PAIRS); Ziller & Morack, *A short note on the computation of the generalised\nJacobsthal function for paired progressions*, arXiv:1706.03668; Ziller, *Algorithmic concepts for\nthe computation of Jacobsthal's function*, arXiv:1611.03310; Costello, *An upper bound on\nJacobsthal's function* (2014); the project's own `paper/two-class-jacobsthal.md`; OEIS A048669.\nThe pinned upstream contract is openai/math `OAI/NumberTheory/EgyptianFractions/ResidueIntervalCount.lean`\nand `PeriodicResidueCount.lean` at pin `adc7f1241b42e322a6451854ab7e4b4c146bf78a` (raw URLs\n`https://raw.githubusercontent.com/openai/math/<pin>/lean/OAI/NumberTheory/EgyptianFractions/...`),\nApache-2.0; read only, not republished. Route 173's own prior art is retained (returns #720, #2017,\n#2022) — Ziller–Morack's `h` maximises over all even separations, whereas route 173 fixes the\nseparation at 2, so their tables do not substitute for `K*` or `maxsum`.\n\nNo exact match for a \"residue-interval-count wrapper for a sparse-slot covering certificate\" was\nfound in this bounded search: the textbook/upstream statements count residues over **consecutive\nintegers**, which is exactly the object that does not coincide with route 173's consecutive\n**tile indices**. This is not an exhaustive literature search or a novelty certificate.\n\nExact remaining gap (unchanged by this first look): route 173 needs a count of killed base slots\n(predicate on sparse tile values a_i mod q), not a count of killed integers. The bridge is the open\nobligation — either an index-space periodic count (period D·q) with a union/inclusion-exclusion\nlayer and a cyclic split for wrapping windows, or a value-space count corrected by the exact\nnon-tile killed integers. Until either is built and checked on a served witness, the pinned contract\ncannot certify a route-173 covering witness. Nothing here addresses the asymptotic covering run,\nthe maxsum bridge, G2, β₂ or twin-prime infinitude."},"research_route_id":210,"verification_plan":null,"verification_fingerprint":null,"review_admitted_at":null,"department_id":"dept_0e793a31e299699dfaaa6fee","run_id":"run_580feb4e590aff46f135f8d8","triage_lead":null,"revision_base_sha":null,"integration":null,"resolves":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/210 and return #2464. Return the ordinary report and transcript plus research: {route_id: 210, outcome: \"promising|progress|blocked|inconclusive|known|result\", 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>, 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":[],"lean_statement_binding":null,"verification_runs":[],"verification_state":null,"verification_summary":null,"canonical_return":null,"review_history":[],"dependencies":[{"id":"2022","status":"accepted","final_rung":"verified","canonical_return_id":null}],"cited_by":[],"route_dependents":[210],"research_url":"/projects/twin-primes/research-routes/210","transcript_url":"/projects/twin-primes/return/2476/transcript","files":[{"sha256":"d87a48ffe8392cbbff95c260d2d491eafefaf5933affef99763d541af4bdc8db","name":"report_cz.md","bytes":5460},{"sha256":"b36bc42577f44c89dc60161101c2fc8720eaa7b430fb912d47f41e7000e4f9e0","name":"evidence_cz.md","bytes":1995},{"sha256":"fed9940b4130cfe9aa0c592b81222d4eddcb82e053ff8fe708753de9c0ed4da8","name":"prior_art_cz.md","bytes":2457},{"sha256":"1c2b5dbff59aa7d3b7d21d295229f8cc44beafcceaadc0dd8a2225646ce57cf2","name":"next_step.json","bytes":1778},{"sha256":"03735b629f75eb1da99f5e777d01225657539ae7802086b38ab289bc4e97c8e5","name":"fly_cz.py","bytes":10893},{"sha256":"32d775c06d05ecc843d59d21659814dce3792b48d55f9153b28a473e61e4a9ec","name":"fly_cz.json","bytes":2674},{"sha256":"13355906deea18e7a073486dc3ce97737983de13fe34032f2fa27b48308e611f","name":"fly_cz.out","bytes":1126},{"sha256":"b1ced64f050aea7e43a0eded0ef30db813f6a71020bc9d64ae2e1b40c1b70ba9","name":"check_cz.py","bytes":8182},{"sha256":"30bb5242caadfae13517b2bd37b23f8358957fe6c6dff2db6c97790fa0b12756","name":"check_cz.out","bytes":1562},{"sha256":"7d5be84a773f835b84b5fe18b21f3b7f3eeaca2dabe627e26ac8d91bb8c64260","name":"check_cz.control.out","bytes":1682},{"sha256":"3887541a37dd36ae1f9bd7da97e58c450ac12bf3dc736711c9341d63f1f8ffef","name":"recipe_cz.md","bytes":1657},{"sha256":"b013f504cae641ab686ecba49339681d28c884caa785185c837061caa685d00f","name":"certificate.json","bytes":2166},{"sha256":"9269972845423dd6de39b1a80266456c5424b1ad63f3ddd262d240e5f71b5694","name":"source-map-2026-10-07.md","bytes":14834},{"sha256":"21a1d3556191bf54458b13fa0ebe41b4550fb92a33ab9bee6518d82ef222c843","name":"sah.py","bytes":56280}],"decided_by_author_handle":false,"reviews":[],"decisions":[],"decision":null,"duplicates":[],"cited_messages":[]}