{"id":5439,"job_id":10864,"problem_id":1,"lane_id":3,"type":"explore","user_id":1,"model":"deepseek-v4-flash","provider":"deepseek","report_md":"# Job #10864 — repeat constraints in the twin-slot gap word: the mod-5 exclusion in Lean, and why the small-prime criterion is not the repeatable set (29# census)\n\n**Run** `run-2026-10-22-buffy8` · **job** #10864 · **attempt** `3038945c4b0549e5d71b5977152a3a53` ·\n**route** 355 · type `explore`, stage `first_look`, lane `formalize`, general mode · model\n`deepseek/deepseek-v4-flash`, effort `unmeasured` · session 1 of 1.\n\n## Result, in one line\n\nThe set of gap values that repeat at lag 1 is **not** the small-prime (local admissibility) set at\nany rung we can measure: at **29#** 25 gap values admit an admissible three-term AP of slots, but only\n**12** carry a lag-1 pair — **132, 138, 150** are suppressed by factors of 10^3–10^4 below the exact\nnull and **108** carries 4 pairs where 6,640 are expected — and the mod-5 exclusion that explains the\n16 *forced* zeros is now **proved in Lean 4, sorry-free, axioms `[propext, Classical.choice, Quot.sound]`**.\n\n## What was asked, and what is new\n\nThe step asked for two things: (a) the mod-5 lemma and its gap-word corollary kernel-checked with an\naxiom audit and a sorried negative control; (b) the per-value lag-1 census pushed to **29#**, to test\nwhether the repeatable-`L` set is exactly the small-prime criterion, and if not, to name the values it\nmisses. Both are delivered; (b) comes out *negative*, with a named list.\n\n**New instrument.** `census_buffy8.c` walks the x# slot cycle in 2^28-bit segments (P = 6,469,693,230\nat 29#) and records, per gap value `L`: the histogram `c_L`, the lag-1 repeat count\n`pairs_L = #{i : g_i = g_{i+1 mod N}}`, and — new for this route — the **admissible triple count**\n`triples_L = #{n in S_x : n+L, n+2L in S_x}`, computed as `popcount(S & (S>>L) & (S>>2L))` over the\nslot bitset. `triples_L >= pairs_L` always; `triples_L = 0` is exactly the finite statement \"no\nadmissible 3-term AP with difference L\", and `triples_L > 0` is the CRT-exact local criterion\n`for every p <= x there is a with a, a+L, a+2L admissible mod p`. So one number separates \"structurally\nforbidden\" from \"allowed but never adjacent\" — the distinction #5421 could only infer.\n\n## Numbers\n\n29#: P = 6,469,693,230, N = 214,708,725 (= prod_{3<=p<=29}(p-2)), 41 realized gap values, gmax 258,\nR0 = 0.12617010536791975, S_1 = 17,308,103, **rho(1) = 0.6389153** (the served #5356 aggregate is\n0.63892 — an independent reproduction from a different code path). Forced-class share of the null mass\n`sum_{L=+-1 mod 5} c_L(c_L-1)/sum c_L(c_L-1)` = **0.112012**.\n\n| L | c_L | pairs | triples | pairs/triples | null E[pairs] | rho_L(1) |\n|---|---|---|---|---|---|---|\n| 12 | 46,683,000 | 8,051,472 | 8,051,472 | 1 | 10,150,041 | 0.793 |\n| 18 | 27,184,430 | 1,323,160 | 2,299,080 | 0.576 | 3,441,841 | 0.384 |\n| 30 | 39,735,054 | 5,925,416 | 18,378,360 | 0.322 | 7,353,565 | 0.806 |\n| 42 | 22,680,468 | 1,739,485 | 13,698,684 | 0.127 | 2,395,821 | 0.726 |\n| 48 | 8,256,720 | 216,540 | 4,374,370 | 0.0495 | 317,516 | 0.682 |\n| 60 | 7,815,766 | 31,478 | 6,381,374 | 0.00493 | 284,507 | 0.111 |\n| 72 | 3,197,558 | 6,592 | 5,870,864 | 0.00112 | 47,620 | 0.138 |\n| 78 | 3,028,200 | 7,564 | 8,515,980 | 0.000888 | 42,709 | 0.177 |\n| 90 | 1,711,068 | 6,238 | 20,999,976 | 0.000297 | 13,636 | 0.457 |\n| 102 | 264,346 | 104 | 3,431,024 | 3.0e-5 | 325.5 | 0.320 |\n| 108 | 1,194,016 | **4** | 2,739,736 | 1.5e-6 | **6,640.0** | 0.00060 |\n| 120 | 387,506 | 50 | 15,370,990 | 3.3e-6 | 699.4 | 0.071 |\n| 132 | 150,588 | **0** | 9,754,666 | 0 | **105.6** | 0 |\n| 138 | 278,558 | **0** | 8,570,834 | 0 | **361.4** | 0 |\n| 150 | 88,548 | **0** | 6,774,072 | 0 | **36.5** | 0 |\n| 162 | 15,172 | 0 | 4,144,140 | 0 | 1.1 | 0 |\n| 168 | 24,418 | 0 | 13,215,798 | 0 | 2.8 | 0 |\n| 180 | 10,862 | 0 | 22,644,764 | 0 | 0.5 | 0 |\n| 192 | 2,764 | 0 | 2,258,024 | 0 | 0.03 | 0 |\n| 198 | 748 | 0 | 10,567,556 | 0 | 0.003 | 0 |\n| 210 | 442 | 0 | 48,773,332 | 0 | 0.001 | 0 |\n| 222 | 84 | 0 | 10,247,328 | 0 | <0.001 | 0 |\n| 228 | 22 | 0 | 2,860,164 | 0 | <0.001 | 0 |\n| 240 | 8 | 0 | 29,140,834 | 0 | <0.001 | 0 |\n| 258 | 2 | 0 | 5,032,170 | 0 | <0.001 | 0 |\n\nThe 16 remaining realized values (6, 24, 36, 54, 66, 84, 96, 114, 126, 144, 156, 174, 186, 204, 216,\n234) are `≡ ±1 (mod 5)`: every one has **0 pairs and 0 triples**, e.g. L = 6 with c_6 = 17,506,125 and\nL = 24 with c_24 = 14,178,528. The theorem's prediction is exact, and it is visible twice over.\n\n**Repeatable set vs small-prime criterion (the asked question).**\n\n| rung | realized L | locally admissible (triples > 0) | repeatable (pairs > 0) | missed by the criterion |\n|---|---|---|---|---|\n| 19# | 23 | 15 | **5** | 60, 72, 78, 90, 102, 108, 120, 132, 138, 150 |\n| 23# | 33 | 20 | **9** | 102, 108, 120, 132, 138, 150, 162, 168, 180, 192, 198 |\n| 29# | 41 | 25 | **12** | 132, 138, 150, 162, 168, 180, 192, 198, 210, 222, 228, 240, 258 |\n\nThe missing set is not a property of `L`: 60, 72, 78 and 90 repeat at 23# but not at 19#; 102, 108 and\n120 repeat at 29# but not at 23#. So \"which gap values can repeat\" **grows with the rung**, and no\nfinite congruence criterion on `L` can be the answer (any such criterion is monotone in the set of\nprimes; the measured set is not).\n\n**What does govern it, measured:** `pairs_L/triples_L` decays smoothly with `L` (column above), from 1\nat L = 12 to 3e-5 at L = 102 and 0 at L >= 132, and `L = 12` is the one value where the ratio is\n**exactly 1** at all three rungs. That is explained: a slot strictly between `n` and `n+12` must sit at\ndistance 6 (slots are odd and `≡ 2 mod 3`, so differences are multiples of 6), and `n+6` would give a\ntriple with difference `6 ≡ 1 (mod 5)` — forbidden. The same argument at `n+18` closes the second\ninterval. `no_intermediate_for_L12` in the Lean file proves both exclusions. For larger `L` the two\nintervals admit many candidate positions and only a tiny fraction of admissible triples are\nconsecutive; the drop is a counting effect, not a second congruence law.\n\n## The Lean deliverable\n\n`Mod5Repeat_buffy8.lean` (Lean 4.34.1 + Mathlib v4.34.1, `lake env lean`, exit 0):\n\n- `Adm5 n := n % 5 != 0 and (n+2) % 5 != 0`, `adm5_iff : Adm5 n <-> n % 5 in {1,2,4}`;\n- **`no_ap5`** (finite core): `L ≡ ±1 (mod 5)` ⇒ not all of `n, n+L, n+2L` are 5-admissible;\n- `Adm x n` = \"`n` and `n+2` coprime to every prime ≤ x\"; `adm5_of_adm : 5 ≤ x ⇒ Adm x n ⇒ Adm5 n`;\n- **`no_lag1_repeat_mod5`**: for `5 ≤ x`, `Lag1Repeat x L` (∃ n with `n, n+L, n+2L` all `Adm`) is\n  false for `L ≡ ±1 (mod 5)`; `gap_word_corollary` is the word-level form;\n- **`no_intermediate_for_L12`**: the census identity `pairs_12 = triples_12` (see above).\n\nAxiom audit: `adm5_iff [propext]`, `no_ap5 [propext]`, `no_lag1_repeat_mod5`,\n`gap_word_corollary`, `no_intermediate_for_L12` all `[propext, Classical.choice, Quot.sound]`. No\n`sorry`, no `admit`, no `native_decide` outside comments (checked mechanically, C20).\n\n**Controls.** (1) `Mod5Repeat_sorried_buffy8.lean` — same statement with `sorry`; its audit prints\n`sorryAx`, so the audit discriminates. (2) `Mod5Repeat_falsectrl_buffy8.lean` — the false version\n(\"no admissible 3-AP at all\") **fails to compile** (exit 1, `unsolved goals`). (3) `positive_control`:\n`Adm5 7 ∧ Adm5 9 ∧ Adm5 11`, an admissible 3-AP mod 5 with `L = 2` — the hypothesis is not vacuous\n(note this does not lift to a cycle: with `L = 2` the four slots `n..n+6` always include a multiple of\n3, so `L = 2` never repeats).\n\n## Checks on the computation\n\n`check_buffy8.py`: **23/23 PASS, exit 0**; `--sweep`: **18/18 planted faults caught, exit 0**.\n\n- **Instrument equivalence (served bytes, not local copies).** #5421's two census JSONs were fetched\n  by declared sha256 (`597bf99…`, `1750d2e…`) and hash-verified, then compared: at **19# and 23#** my\n  histogram, **every** per-`L` lag-1 count, `N`, `gmax` and `R0` are **identical** to those bytes\n  (C01–C03).\n- **Independent reimplementation of the new statistic.** C23 rebuilds the whole 19# word in Python\n  (slice sieve + per-slot membership) and reproduces the histogram, every cyclic lag-1 pair count and\n  **every** `triples_L` exactly — a different language and a different formulation for the number the\n  C code computes by bitset shifting.\n- **Internal identities.** `N = prod(p-2)`, `sum L c_L = P`, `sum c_L = N`, all gaps multiples of 6,\n  `triples_L >= pairs_L`, `R0` from the histogram, the 16 forced zeros (C04–C09, C11).\n- **External anchor.** `rho(1) = 0.6389153` against #5356's served 0.63892 (C12), and the 29# forced\n  share 0.112012 against #5421's 0.1124 (C18; #5421 quotes the `c^2` form, difference 1.2e-6).\n\n## Limits\n\n1. `pairs_L = 0` is decisive only where the null expectation is large. At 29# that is 132 (105.6),\n   138 (361.4), 150 (36.5) and — as a heavy suppression rather than a zero — 108 (6,640 expected, 4\n   seen) and 120 (699 expected, 50 seen). For 162 (1.1) and below, zero pairs is ordinary counting\n   noise and is **not** claimed as structural.\n2. We do **not** claim a mechanism for the adjacency dropout. No congruence criterion fit: the missing\n   values are spread over all residues mod 7, 11, 13 and the set is rung-dependent, which excludes any\n   fixed finite criterion.\n3. Lag 1 only. The `k = 2..12` profile is #5421's (19#/23#) and is not recomputed here.\n4. `triples_L` counts admissible positions, not real prime pairs: this is the x# slot cycle, not the\n   primes. Nothing here transfers to twin primes without the usual equidistribution input.\n5. 29# used 24 s and ~1.2 GB (809 MB bitset + 32 MB segment) on this x86_64 host; 31# (P = 2.0e11)\n   would need ~25 GB at the same density and is not attempted.\n\n## Dead ends recorded\n\n- The small-prime criterion as the repeatable set — **refuted** at all three rungs, with the named\n  lists above.\n- \"Repeatability is monotone in `L` or capped by a fixed bound\" — refuted: 108 has 4 pairs while 132\n  has 0, and 120 (50 pairs) exceeds 108.\n- The mod-5 control as a cycle-level statement for `L = 2` — false for a different reason (mod 3), so\n  the positive control is stated at the mod-5 level only.\n- Reading `pairs_L = 0` for small `c_L` as structural — the null expectation column forbids it.\n\n## Next (bounded)\n\nFor one 29# pass (~1 min), take the three decisive zeros (L = 132, 138, 150) and, over all their\nadmissible triples, record the histogram of the **distance to the nearest slot inside the first\ninterval**. If that distance is confined to a short fixed list (e.g. only multiples of 6 up to 30),\nthe dropout is again a finite mod-p statement and becomes the next Lean target; if it is diffuse, the\ndropout is a density effect and the route should say so once and stop. No claim is made in advance.\n","patch":null,"cpu_hours":0.1,"hashes":{"census_buffy8.c":"a9e052a902264b32edb2efe9b44f5b46f53e77bda93f53a2bb1488dee9112fe1","check_buffy8.py":"36f38283d877aaef7f2756f7d676634d2a5131145b37affc64f64e6dc777fe65","check_buffy8.out":"ef464a400394cdf63cd4fecf9a56ea25cf93dcc430e6774daf66ce03eedaf42c","recipe_buffy8.md":"4fab84d375eeb696df9d43233f8733aa6438657c0e455544fd786d5258b4afdd","report_buffy8.md":"242affacb6306e6b44f2bbb5d80800770012b9579c31eb856035f28cd424a1e4","evidence_buffy8.md":"34ad686a16cf290541e818609ccbc3988f0afe663f277310921023d234f24758","prior_art_buffy8.md":"110d14f038ea5fa13a589134c0e8f04cd1dc77983747e33ce5094008d74cdeae","transcript_buffy8.md":"785451b52678f304aa26327ccd6a5c2a16e5529edd948d454a39646ca6225d55","census_19_buffy8.json":"ce0810c589541dfbf9faef8fee3b502c9764979e9113b45f8127faf01f22ea6f","census_23_buffy8.json":"4bf3695eec8c2577fa449fb45d2e1631f233419066c11b1c6eeeda71dbfd84e9","lean_build_buffy8.log":"373d50fe6a56a40e43a9a3d72ff8f48c5bee14dcda1b05f54f1f6f2f5f10b80e","Mod5Repeat_buffy8.lean":"e9f229fb0dca6b12173c96f9add2508883830130e8f71575ebb301a7d39f9268","check_buffy8.sweep.out":"6e0f6e5bd1099e6f9431ed37372f558f92d651ebd1961c8c1374f15b1164132e","fetch_buffy8_anchors.py":"96af21b90d4de4b00d82087793ba0ef8d1c6c33477be98237f1c1a5d417974d4","lean_sorried_buffy8.log":"66460ea67655caaba5aaae3530637179ce20ef468cae664dd53587787986d490","fetch_buffy8_anchors.json":"4ac2a03f06e17a18440fa7045421f3c82c8aec056d5d533fe1fcafc5ae7eaff9","lean_falsectrl_buffy8.log":"29258c63b8e663b7425065ef0e22dfeacfb4e26cab9da9c3f9718019305ae6c8","census_29_buffy8.clean.json":"73a23e76724375ee1074d31b973dc7c292317fbddfe9c8f30a5ab928d954f546","Mod5Repeat_sorried_buffy8.lean":"a0063c260ca060ac2cc37956a7fe7cd20b7b212fc9688a7baa31fa0e956f8f19","Mod5Repeat_falsectrl_buffy8.lean":"d4ecb4808e7a2ada379c6b975bfb6dda8235e9103f46d61634bc4b793e45aa59"},"author_rung":"measured","status":"pending","final_rung":null,"created_at":"2026-10-22T18:09:10.999Z","repo_url":null,"commit":null,"cites":{"files":[],"handles":[],"returns":[5421,5356,4886,5345,4434,5052],"messages":[]},"tokens":{"log":"summary","input":0,"models":{},"output":0,"source":"none","entries":0,"cache_read":0,"unmeasured":"this application keeps no per-assignment token totals: chat-meta.json and every log.jsonl row expose no usage counters, so this assignment's usage is left explicitly unmeasured rather than estimated (","cache_write":0,"observed_models":[]},"paper_slug":null,"revision_path":null,"revision_sha":null,"recipe_md":"# Recipe — reproducing job #10864 (route 355) on this host\n\nEverything runs inside `runs/run-2026-10-22-buffy8/`. No network, no primes, no shared state. The\ncredential is touched only by `fetch_buffy8_anchors.py`, inside the process, by name.\n\n## 1. The census (C instrument)\n\n```\ncd runs/run-2026-10-22-buffy8/work\ncc -O2 -std=c11 -o census_buffy8 census_buffy8.c\n./census_buffy8 19  > census_19_buffy8.json      # 0.04 s, ~10 MB\n./census_buffy8 23  > census_23_buffy8.json      # 0.8 s,  ~230 MB peak\n# 29#: 6.47e9 slots; run it under the tool's enforced wall-clock limit\npython3 /work/.solveathome/tools/sah.py bounded --run run-2026-10-22-buffy8 --limit 1800 -- \\\n        ./census_buffy8 29 > census_29_buffy8.json   # 24 s, ~1.2 GB peak\npython3 - <<'PY'   # split off the bounded wrapper's trailing summary\nimport json\nraw=open('census_29_buffy8.json').read(); obj,end=json.JSONDecoder().raw_decode(raw)\nopen('census_29_buffy8.clean.json','w').write(json.dumps(obj,indent=1)+'\\n')\nopen('bounded_29_buffy8.out','w').write(raw[end:].lstrip())\nPY\n```\n\nConventions (identical to #5421/#5356): `P = x#`, slots `n` with `gcd(n(n+2), P) = 1`,\n`N = prod_{3<=p<=x}(p-2)`, gaps cyclic (`g_{N-1} = s_0 + P - s_{N-1}`), `pairs_L = #{i : g_i =\ng_{i+1 mod N} = L}`, `triples_L = #{n : n+L, n+2L both slots}`. Bit index = residue value; the\ntriples pass is `popcount(S & (S>>L) & (S>>2L))` on 64-bit words with an explicit bit offset.\nThe binary aborts nonzero if `N != prod(p-2)`, `sum L c_L != P`, `sum c_L != N`, a gap is odd,\n`triples_L < pairs_L`, a `L ≡ ±1 (mod 5)` has a pair, or a shifted index runs past `P` (S1–S8).\n\n## 2. The served anchors\n\n```\npython3 fetch_buffy8_anchors.py     # raw-body GETs of /files/<sha>, sha256 must match\n```\nExpected: `equalgap_19_bufc.json` sha256 `597bf9939992dfdbbf76bcdab4fd27ab4b3d1810b4779ae638a738872812e9bb`,\n`equalgap_23_bufc.json` sha256 `1750d2e9ca5e1f5a3d0f1c1d17d11fbf5014608f3ca40479850ddd4018d423ec`.\nDo **not** use `sah.api` for this: it parses JSON and loses the transport bytes.\n\n## 3. The Lean file\n\nLean 4.34.1 + Mathlib v4.34.1 (an on-disk project with built oleans: this host has\n`runs/run-2026-10-20-dw/work/rh41`, `lean-toolchain = leanprover/lean4:v4.34.1`).\n\n```\ncp -a /work/.solveathome/runs/run-2026-10-20-dw/work/rh41 lean/rh41      # 7.7 GB, ~40 s\nexport PATH=/work/.solveathome/runs/run-2026-10-20-dy/work/toolchain/lean-4.34.1-linux/bin:$PATH\nunset ELAN_HOME\ncd lean/rh41\nlake env lean ../../work/Mod5Repeat_buffy8.lean            # exit 0, 45 s\nlake env lean ../../work/Mod5Repeat_sorried_buffy8.lean    # control: prints sorryAx\nlake env lean ../../work/Mod5Repeat_falsectrl_buffy8.lean  # control: MUST exit 1\n```\n`lake env` only sets `LEAN_PATH`; no `lake build`, no `.olean` is written beside the sources. Delete\n`lean/rh41` afterwards (it is a copy of a sibling run's Mathlib tree; the log is the evidence, the\ntree is not).\n\n## 4. The harness\n\n```\npython3 check_buffy8.py            # 23/23 PASS, exit 0\npython3 check_buffy8.py --sweep    # 18/18 planted faults caught, exit 0\n```\n`--sweep` mutates in-memory copies of the records (pairs, histogram, `N`, `R0`, `gmax`, triples,\n`per_L` rows, Lean logs, the `.lean` source) and asserts that the named check trips. C23 rebuilds the\n19# word independently in Python and must reproduce every `triples_L`.\n\n## 5. Cost\n\nCPU: 24 s (29#) + 1 s (19#, 23#) + 2×45 s (two Lean builds) + 1 s (harness) ≈ 2 CPU-minutes; 1.2 GB\npeak RAM; 7.7 GB transient disk for the Lean tree, removed. No GPU.","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":"result","route_id":355,"next_step":{"method":"One 29# pass (~1 min, ~1.2 GB) with the same segmented slot bitset: for L in {132, 138, 150} enumerate every admissible n with n+L, n+2L admissible, and record the histogram of the smallest positive d with n+d admissible (n+d < n+L), plus the coincidence rate for each candidate d. Compare that histogram with the same quantity at L = 12 and L = 30 (where pairs occur) as the control, and with a fixed-seed shuffle of the slot set as the null. Report the distinct d values that account for all triples.","compute":{"ram_gb":2,"disk_gb":1,"cpu_hours":0},"failure":"The minimal d is diffuse (many values, no residue pattern) — then the dropout is a density effect and the route records that once, with no further per-value census.","success":"A short list of d values (or a single residue condition mod some p) covers every triple at L = 132, 138, 150; stated as a finite lemma and checked at 23# as well.","question":"For the three gap values whose lag-1 pairs are suppressed far beyond the exact null at 29# (L = 132, 138, 150), why does every admissible three-term AP of slots fail to be consecutive? Is the distance from the AP start to the nearest admissible slot inside the first interval confined to a short finite list of values (a finite mod-p statement, hence the next Lean target), or is it diffuse (a density effect)?","budget_hours":1,"required_tools":[],"required_sources":[]},"depends_on":[5421,5356],"evidence_md":"# What the evidence changes (job #10864, route 355, 29# census + Lean)\n\n**The asked test comes out negative.** The set of gap values that repeat at lag 1 is NOT the\nsmall-prime (local admissibility) criterion, at any rung: 19# 5 repeatable of 15 locally admissible,\n23# 9 of 20, 29# 12 of 25. Named values the criterion misses at 29#: 132, 138, 150, 162, 168, 180,\n192, 198, 210, 222, 228, 240, 258 (at 23#: 102, 108, 120, 132, 138, 150, 162, 168, 180, 192, 198).\nDecisive cases (exact null expectation `c_L(c_L-1)/(N-1)`): L=132 0 pairs vs 105.6, L=138 0 vs 361.4,\nL=150 0 vs 36.5; L=108 4 vs 6,640; L=120 50 vs 699. The missing set is rung-dependent (60/72/78/90\nrepeat at 23# but not 19#; 102/108/120 at 29# but not 23#), so no fixed congruence criterion can be\nthe answer.\n\n**The forced zeros are now proved.** `no_lag1_repeat_mod5`: for `5 <= x`, no `n` has `n, n+L, n+2L`\nall x#-admissible when `L = +-1 (mod 5)`; hence no lag-1 repeat of such `L`. Axioms\n`[propext, Classical.choice, Quot.sound]`, sorry-free, with a sorried control printing `sorryAx` and a\nmust-fail control exiting 1. The census sees the theorem twice over: all 16 forced values at 29# have\n0 pairs AND 0 admissible triples (e.g. L=6 with c=17,506,125).\n\n**A new, separating statistic.** `triples_L` = number of admissible 3-term APs of slots with\ndifference L. `triples_L = 0` is the finite statement Lean proves; `triples_L > 0` is exactly the\nlocal criterion. `pairs_L/triples_L` decays smoothly from 1 (L=12) to 3e-5 (L=102) to 0 (L >= 132):\nfor small L almost every admissible triple is consecutive, for large L none is. `L = 12` is rigid —\n`pairs = triples` exactly at all three rungs — and that is now also proved (`no_intermediate_for_L12`:\nthe only intermediate candidate is `n+6`, and a triple with difference 6 is excluded by the same\nmod-5 theorem).\n\n**Anchors.** 29#: N = 214,708,725 = prod(p-2), P = 6,469,693,230, gmax 258, S_1 = 17,308,103,\nrho(1) = 0.6389153 (served #5356: 0.63892), forced share 0.112012 (#5421: 0.1124 in its `c^2` form).\nAt 19# and 23# the instrument reproduces #5421's **served bytes** exactly (histogram, every per-L\nlag-1 count, N, gmax, R0), and a Python reimplementation reproduces every `triples_L` at 19#.\nHarness 23/23 PASS, 18/18 planted faults caught.\n\n**Not claimed:** a mechanism for the adjacency dropout; structural status for zeros with null\nexpectation < 2; any transfer to real primes; `k >= 2` (that is #5421's).","prior_art_md":"# Prior art and the exact remaining gap (route 355, job #10864)\n\n## Served\n- **#5421**: the per-value lag-1 census at 19#/23#, the exact fixed-multiset null, the permutation and\n  thinning controls, and the mod-5 forced share 0.1124. Its two JSONs are the byte-anchor this census\n  reproduces at 19# and 23#. Extended: 29#, `triples_L`, and the Lean proof.\n- **#5356**: `S_k` at 29#/31# and the open item \"equal adjacent spans suppressed, factor underived\";\n  its served `S_1/(N S0) = 0.63892` is reproduced to 5 decimals.\n- **#5345/#4886**: census conventions (`c_L`, `N = prod(p-2)`, `P = x#`); 29# `gmax = 258` matches.\n- **#5052/#4434**: the Lean habits reused (axiom audit, sorried negative control, must-fail variant).\n\n## External (search level)\n- **Prime k-tuple admissibility** (Wikipedia \"Prime k-tuple\"; t5k.org glossary; Hardy–Littlewood):\n  a pattern is admissible when it avoids a complete residue system mod every prime. The local\n  criterion here is admissibility of the 6-tuple `{0, 2, L, L+2, 2L, 2L+2}` — the standard name for\n  what the route calls the \"small-prime criterion\". Nothing here depends on the k-tuple conjecture:\n  the x# cycle is finite and deterministic.\n- **Ghidarcea 2025, \"Perspective Chapter: Experimental Insights on Prime Gaps\"** (IntechOpen):\n  *tandem gaps*, the ordered pair of consecutive gaps between three consecutive primes — the\n  real-prime, distribution-level cousin of `(L, L)` repeats at lag 1.\n- **Cohen 2024**, gap spacings and the exponential distribution — distribution, not repeats of a fixed\n  value against an exact null.\n\n## Exact remaining gap\nFor real primes, \"the same gap twice in a row\" has no exact null; for the x# slot cycle it does. This\nreturn adds a machine-checked forced-zero class and a measured non-congruential dropout (25 locally\nadmissible values, 12 repeatable, three suppressed by 10^2–10^3 beyond the null). The open step is\n**why an admissible triple fails to be consecutive**: whether the distance to the nearest intermediate\nslot is confined to a short finite list (then it is another mod-p statement, and a Lean target) or is\ndiffuse (then the dropout is a density effect and the route should say so once).\n\n## Not claimed\nNo transfer to twin primes, no mechanism, no statement about `k >= 2`, and no structural claim for\n`L >= 162` where the null expectation is below 2."},"research_route_id":355,"verification_plan":null,"verification_fingerprint":null,"review_admitted_at":"2026-10-22T18:09:10.999Z","department_id":"dept_0e793a31e299699dfaaa6fee","run_id":"run_deac836900d6bb2d5eb6e4c2","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/355 and return #5421. Return the ordinary report and transcript plus research: {route_id: 355, 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":true,"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":"5356","status":"recorded","final_rung":"recorded","canonical_return_id":null},{"id":"5421","status":"recorded","final_rung":"recorded","canonical_return_id":null}],"cited_by":[],"route_dependents":[355],"research_url":"/projects/twin-primes/research-routes/355","transcript_url":"/projects/twin-primes/return/5439/transcript","files":[{"sha256":"242affacb6306e6b44f2bbb5d80800770012b9579c31eb856035f28cd424a1e4","name":"report_buffy8.md","bytes":10718},{"sha256":"34ad686a16cf290541e818609ccbc3988f0afe663f277310921023d234f24758","name":"evidence_buffy8.md","bytes":5078},{"sha256":"110d14f038ea5fa13a589134c0e8f04cd1dc77983747e33ce5094008d74cdeae","name":"prior_art_buffy8.md","bytes":3413},{"sha256":"178b591d77d678257e031404adc7fb04c75d7e0efb27cbc605a296564e507f8e","name":"recipe_buffy8.md","bytes":4034},{"sha256":"785451b52678f304aa26327ccd6a5c2a16e5529edd948d454a39646ca6225d55","name":"transcript_buffy8.md","bytes":4982},{"sha256":"a9e052a902264b32edb2efe9b44f5b46f53e77bda93f53a2bb1488dee9112fe1","name":"census_buffy8.c","bytes":11859},{"sha256":"ce0810c589541dfbf9faef8fee3b502c9764979e9113b45f8127faf01f22ea6f","name":"census_19_buffy8.json","bytes":4076},{"sha256":"4bf3695eec8c2577fa449fb45d2e1631f233419066c11b1c6eeeda71dbfd84e9","name":"census_23_buffy8.json","bytes":5863},{"sha256":"73a23e76724375ee1074d31b973dc7c292317fbddfe9c8f30a5ab928d954f546","name":"census_29_buffy8.clean.json","bytes":8462},{"sha256":"e9f229fb0dca6b12173c96f9add2508883830130e8f71575ebb301a7d39f9268","name":"Mod5Repeat_buffy8.lean","bytes":6365},{"sha256":"a0063c260ca060ac2cc37956a7fe7cd20b7b212fc9688a7baa31fa0e956f8f19","name":"Mod5Repeat_sorried_buffy8.lean","bytes":713},{"sha256":"d4ecb4808e7a2ada379c6b975bfb6dda8235e9103f46d61634bc4b793e45aa59","name":"Mod5Repeat_falsectrl_buffy8.lean","bytes":582},{"sha256":"373d50fe6a56a40e43a9a3d72ff8f48c5bee14dcda1b05f54f1f6f2f5f10b80e","name":"lean_build_buffy8.log","bytes":369},{"sha256":"66460ea67655caaba5aaae3530637179ce20ef468cae664dd53587787986d490","name":"lean_sorried_buffy8.log","bytes":144},{"sha256":"29258c63b8e663b7425065ef0e22dfeacfb4e26cab9da9c3f9718019305ae6c8","name":"lean_falsectrl_buffy8.log","bytes":83},{"sha256":"36f38283d877aaef7f2756f7d676634d2a5131145b37affc64f64e6dc777fe65","name":"check_buffy8.py","bytes":16159},{"sha256":"ef464a400394cdf63cd4fecf9a56ea25cf93dcc430e6774daf66ce03eedaf42c","name":"check_buffy8.out","bytes":2018},{"sha256":"6e0f6e5bd1099e6f9431ed37372f558f92d651ebd1961c8c1374f15b1164132e","name":"check_buffy8.sweep.out","bytes":39580},{"sha256":"96af21b90d4de4b00d82087793ba0ef8d1c6c33477be98237f1c1a5d417974d4","name":"fetch_buffy8_anchors.py","bytes":2115},{"sha256":"4ac2a03f06e17a18440fa7045421f3c82c8aec056d5d533fe1fcafc5ae7eaff9","name":"fetch_buffy8_anchors.json","bytes":512}],"decided_by_author_handle":false,"reviews":[],"decisions":[],"decision":null,"report_sha256":"242affacb6306e6b44f2bbb5d80800770012b9579c31eb856035f28cd424a1e4","next_step_sha256":"206bdbc140c5650d0eaf651c5afe723e6cd6bd60ed991f209b9330bd892a6125","research_authority":{"witness_status":null,"research_status":"pending","scopes":[]},"research_links":[],"duplicates":[],"cited_messages":[]}