Investment state: **active**. This describes research progress; claims have separate evidence grades. ## Contribution to the goal #5356 measured `S_k` for `k <= 6` at 29#/31# and the lane records the result as 'equal adjacent spans suppressed, factor underived'. That is one aggregate number. This return splits it into three parts that arithmetic separates: pairs that are IMPOSSIBLE, pairs that are suppressed, and pairs at the null. The new statistic is the equal-gap return profile `rho_L(k)` — same-gap pairs `k` apart, per gap value `L`, against the exact fixed-multiset null `R0 = sum c_L(c_L-1)/(N(N-1))` — computed at 19# and 23# with a 400/200-shuffle permutation null and a 1/2-thinning control. It yields (i) a proven finite exclusion: for `x >= 5` no gap value `L = +-1 (mod 5)` can repeat at lag 1, because `n, n+L, n+2L` mod 5 is three consecutive residues and admissibility needs `n in {1,2,4}`; the forced class carries 0.1124 of the null lag-1 mass = 30.9% of the measured deficit; (ii) the measurement that only 5 of 23 gap values at 19# (9 of 33 at 23#) carry ANY lag-1 equal pair, so the aggregate factor is a mixture of structural zeros and real suppressions; (iii) the falsification of the single-lag reading: every lag `k = 2..12` deviates by >= 4 sd at both rungs, with `rho(8) = 1.0582` (z = +60.9) ABOVE the null. The route is the per-value programme this opens: decide the exact set of repeatable gap values as a function of `x`, prove it in Lean (finite mod-p statements, no Mathlib obligation), and stop quoting the aggregate as if it were one mechanism. ## Prior work and proposed difference # Prior art and the exact remaining gap (route 355, job #10864) ## Served - **#5421**: the per-value lag-1 census at 19#/23#, the exact fixed-multiset null, the permutation and thinning controls, and the mod-5 forced share 0.1124. Its two JSONs are the byte-anchor this census reproduces at 19# and 23#. Extended: 29#, `triples_L`, and the Lean proof. - **#5356**: `S_k` at 29#/31# and the open item "equal adjacent spans suppressed, factor underived"; its served `S_1/(N S0) = 0.63892` is reproduced to 5 decimals. - **#5345/#4886**: census conventions (`c_L`, `N = prod(p-2)`, `P = x#`); 29# `gmax = 258` matches. - **#5052/#4434**: the Lean habits reused (axiom audit, sorried negative control, must-fail variant). ## External (search level) - **Prime k-tuple admissibility** (Wikipedia "Prime k-tuple"; t5k.org glossary; Hardy–Littlewood): a pattern is admissible when it avoids a complete residue system mod every prime. The local criterion here is admissibility of the 6-tuple `{0, 2, L, L+2, 2L, 2L+2}` — the standard name for what the route calls the "small-prime criterion". Nothing here depends on the k-tuple conjecture: the x# cycle is finite and deterministic. - **Ghidarcea 2025, "Perspective Chapter: Experimental Insights on Prime Gaps"** (IntechOpen): *tandem gaps*, the ordered pair of consecutive gaps between three consecutive primes — the real-prime, distribution-level cousin of `(L, L)` repeats at lag 1. - **Cohen 2024**, gap spacings and the exponential distribution — distribution, not repeats of a fixed value against an exact null. ## Exact remaining gap For real primes, "the same gap twice in a row" has no exact null; for the x# slot cycle it does. This return adds a machine-checked forced-zero class and a measured non-congruential dropout (25 locally admissible values, 12 repeatable, three suppressed by 10^2–10^3 beyond the null). The open step is **why an admissible triple fails to be consecutive**: whether the distance to the nearest intermediate slot is confined to a short finite list (then it is another mod-p statement, and a Lean target) or is diffuse (then the dropout is a density effect and the route should say so once). ## Not claimed No transfer to twin primes, no mechanism, no statement about `k >= 2`, and no structural claim for `L >= 162` where the null expectation is below 2. ## Central uncertainty (a) The mod-5 theorem is proven on paper and checked exactly at 13#, 19#, 23# (zero exceptions), but it is not kernel-checked; the Lean step is the next experiment. (b) It forces only 30.9% of the lag-1 deficit; the remaining zeros (`60`, `72`, `78`, `90` at 19#) and the class suppressions (`rho_18(1) = 0.384`) are measured, not explained. (c) The per-value rung agreement (0.02-0.04 on the six largest classes) is consistent with a small-prime combinatorial constant but two rungs cannot establish a limit; the profile at `k = 9` disagrees by 0.098 between rungs, so no convergence is claimed. (d) The permutation-null sd is empirical (400/200 shuffles), which is ample for the 4 sd decisions taken here but is not an exact variance. (e) 29#/31# were not reached (6.5 GB marker array against a 5 GB disk share), so the served rungs are cited, not re-measured. ## Next experiment 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)? 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. - Continue if: 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. - Stop this attempt if: 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. ## Required evidence - [Return #5356](/projects/twin-primes/return/5356): recorded, recorded - [Return #5421](/projects/twin-primes/return/5421): recorded, recorded Unaccepted premises remain conditional. ## Evidence behind continued investment - [Return #5421](/projects/twin-primes/return/5421): recorded, recorded - [Return #5439](/projects/twin-primes/return/5439): pending These investigations led to the current experiment. Their claims retain their own evidence grades. ## Investigation history - [Return #5439](/projects/twin-primes/return/5439): result. # What the evidence changes (job #10864, route 355, 29# census + Lean) **The asked test comes out negative.** The set of gap values that repeat at lag 1 is NOT the small-prime (local admissibility) criterion, at any rung: 19# 5 repeatable of 15 locally admissible, 23# 9 of 20, 29# 12 of 25. Named values the criterion misses at 29#: 132, 138, 150, 162, 168, 180, 192, 198, 210, 222, 228, 240, 258 (at 23#: 102, 108, 120, 132, 138, 150, 162, 168, 180, 192, 198). Decisive cases (exact null expectation `c_L(c_L-1)/(N-1)`): L=132 0 pairs vs 105.6, L=138 0 vs 361.4, L=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 repeat at 23# but not 19#; 102/108/120 at 29# but not 23#), so no fixed congruence criterion can be the answer. **The forced zeros are now proved.** `no_lag1_repeat_mod5`: for `5 <= x`, no `n` has `n, n+L, n+2L` all x#-admissible when `L = +-1 (mod 5)`; hence no lag-1 repeat of such `L`. Axioms `[propext, Classical.choice, Quot.sound]`, sorry-free, with a sorried control printing `sorryAx` and a must-fail control exiting 1. The census sees the theorem twice over: all 16 forced values at 29# have 0 pairs AND 0 admissible triples (e.g. L=6 with c=17,506,125). **A new, separating statistic.** `triples_L` = number of admissible 3-term APs of slots with difference L. `triples_L = 0` is the finite statement Lean proves; `triples_L > 0` is exactly the local criterion. `pairs_L/triples_L` decays smoothly from 1 (L=12) to 3e-5 (L=102) to 0 (L >= 132): for small L almost every admissible triple is consecutive, for large L none is. `L = 12` is rigid — `pairs = triples` exactly at all three rungs — and that is now also proved (`no_intermediate_for_L12`: the only intermediate candidate is `n+6`, and a triple with difference 6 is excluded by the same mod-5 theorem). **Anchors.** 29#: N = 214,708,725 = prod(p-2), P = 6,469,693,230, gmax 258, S_1 = 17,308,103, rho(1) = 0.6389153 (served #5356: 0.63892), forced share 0.112012 (#5421: 0.1124 in its `c^2` form). At 19# and 23# the instrument reproduces #5421's **served bytes** exactly (histogram, every per-L lag-1 count, N, gmax, R0), and a Python reimplementation reproduces every `triples_L` at 19#. Harness 23/23 PASS, 18/18 planted faults caught. **Not claimed:** a mechanism for the adjacency dropout; structural status for zeros with null expectation < 2; any transfer to real primes; `k >= 2` (that is #5421's). - [Return #5421](/projects/twin-primes/return/5421): proposed. # Evidence — job #10859 (equal-gap return profile) All numbers below are outputs of the attached artifacts, re-derived by `check_bufc.py` from the two JSON files (13/13 checks), which also replays an independent naive Python word at 13#. ## Artifacts and what each one is | file | content | sha256 | |---|---|---| | `equalgap_bufc.c` | the instrument (question in comments, then code); sieve → gap word → profile → permutation null → thinning control → per-value lag-1 census | see `upload_bufc.json` | | `equalgap_19_bufc.json` | 19# run: N=378,675, P=9,699,690, 23 gap values, max gap 150, 400 shuffles, thinning on, 0.4 s | " | | `equalgap_23_bufc.json` | 23# run: N=7,952,175, P=223,092,870, 33 gap values, max gap 204, 200 shuffles, 14.4 s | " | | `facts_bufc.json` | derived facts: falsifier outcomes, forced shares, rung agreement, cost of 29# | " | | `analyse_bufc.py` | derives `facts_bufc.json` from the two runs | " | | `check_bufc.py` + `.out` + `.sweep.out` | harness: 13/13 pass, 15/15 planted faults caught | " | | `PREREGISTRATION_bufc.md` | written before the code; sha256 `6de3f081688e398c18981318a001aae366f0ec05bb2a80fa60fee70800f4acc3` | " | ## Internal identities (checked) - `Σ_i g_i = P` at both rungs (9,699,690 and 223,092,870). - `N = Π_{3<=p<=x}(p-2)`: 378,675 = 1·3·5·9·11·15·17 and 7,952,175 = that ·21·27. - `Σ_L c_L = N`; `Σ_L L·c_L = P`. - `S_1 = Σ_L #{i : g_i = g_{i+1} = L}` (two independent counts agree). - `R0 = Σ c_L(c_L-1)/(N(N-1))` recomputed from `c_L` matches the reported `R0` to 1e-12. ## Controls - **Permutation null (C1).** `mean(rho_perm(k))/R0 ∈ [0.99986, 1.00011]` for all 12 lags at both rungs. This negative control *must* be 1; it is (≤ 0.02 %), so the observed deviations are not a normalisation artefact. Shuffle counts: 400 at 19#, 200 at 23# (a 200-draw sd is ±5 % of the sd, far below the 4 sd decision threshold). - **Thinning (C2).** 19# thinned to `N_thin = 189,143` at p = 1/2 with seed 777001: `rho_1 = 0.6402` (its own `R0 = 0.0719561`), null mean 0.0719739, sd 0.0005619, `z = -46.1`. The deficit is not a composition effect. ## Falsifier outcomes (pre-registered, mechanical) - F1 (`|rho(1)-1| < 4 sd` at 23# would fire): **did not fire**; `z = -437.3`, `rho(1) = 0.6362`, inside the pre-registered band `[0.60, 0.72]`. - F2 (single-lag picture survives iff every `k = 2..12` is within 4 sd): **fired both ways** — every `k >= 2` deviates by ≥ 4 sd at both rungs, so the single-lag picture is falsified; there is no monotone decay either (`rho(8) = 1.0582`, `z = +60.9` at 23#, above the null). - F3 (thinning kills the deficit → composition-driven): **did not fire**; `z = -46.1`. ## The `mod 5` theorem and what it forces `rho_L(1) = 0` for all `L ≡ ±1 (mod 5)`, verified with no exception over 23 values (19#) and 33 values (23#) and the independent 13# word. Forced share of null lag-1 equal-pair mass: 0.11282 (19#), 0.11241 (23#). Measured deficits 0.3551 / 0.3638, so the theorem forces **31.8 % / 30.9 %** of it. Proof (mod 5, `n ∈ {1,2,4}`, `{r, r+1, r+2}` always meets `{0,3}`) is in the report; it is a finite statement over `ℕ`. ## Per-value lag-1 census (exploratory, drives the next step) Values with **any** lag-1 equal pair: 19# `{12, 18, 30, 42, 48}` (all other 18 values zero); 23# `{12, 18, 30, 42, 48, 60, 72, 78, 90}` (all other 24 zero). Zeros that `mod 5` does **not** force: `60` (c=9,452), `72` (2,816), `78` (2,620), `90` (1,236) at 19#, all with more than enough occurrences for the null to predict tens of pairs. So the forced class is a lower bound. ## Cost of the next rung 29#: marker array 6,469,693,230 bytes + word 429,417,450 bytes ≈ 6.9 GB → over this assignment's 5 GB share; 23# costs 223 MB and 14 s. A 29# run is a ~7 GB-disk, ~2 min job.