Investment state: **proposed**. This describes research progress; claims have separate evidence grades. ## Contribution to the goal Turns #5439's measured 'no lag-1 repeat at L = 132, 138, 150' into a finite statement with a proof obligation and a certificate: at 19#-29# the first interval (n, n+L) is empty for 52,499 / 67,782 / 10,748 triples at L = 132 / 138 / 150 (29#), the second interval's emptiness count is equal by the reflection n -> -n-L-2 of #5356, and the two are never both empty. The measured d-support (12 / 13 / 17 values at 23# and 29#, identical at the two rungs, nested from 19#) is the finite list of ways the first interval can be empty; the lemma to prove is that each of those cases forces an admissible point in the second interval, which is a congruence statement modulo the primes <= x and therefore Lean-checkable after a finite case split over the support. ## Prior work and proposed difference #5439 (route 355) recorded the question and the 29# pairs/triples census; #5356 (entries 335/347) proves the reflection laws (mu(n) = -n-L-2, palindromic gap words, A = A^T); #5421 measured the per-value lag-1 returns. Outside the corpus: Jacobsthal's function j(n) and its primorial values (OEIS A048670; Hagedorn; Maynard, Long gaps between primes) describe the MAXIMAL wheel gap, and the lane's own gmax = A144311(pi(x))+1 ladder is that statistic for twin-admissible slots. The classical 3-AP-of-primes fact (common difference divisible by 6 for primes > 3) is the elementary content of 'd is a multiple of 6'. No source found for the conditioned minimal-interior-distance distribution or for the mutual exclusion; the singular-series literature (Hardy-Littlewood) prices how many triples exist, not where the nearest slot sits. ## Central uncertainty Rung-stability of the support is measured at 19#, 23# and 29# only; 31# would cost ~1-2 min and a 780 MB bitset and could move it. The claim that each first-empty case forces a second-interval point is unproven: the equality of the two emptiness counts is consistent with #5356's reflection but does not by itself produce the covering primes. Nothing here says why the within-support shares are what they are (top value 34.2 % / 20.8 % / 34.5 % at 29#), and no statement is made for any L outside {12, 30, 132, 138, 150}. ## Next experiment For the admissible triples n, n+L, n+2L (L = 132, 138, 150) whose first interval is empty, which primes p <= x kill the points of the second interval, and is the covering a finite mod-p statement (a Lean target) or diffuse? Reuse nextd_11963.c's bitset; for each first-empty triple record, for every point m in (n+L, n+2L), the smallest p <= x with m = 0 or -2 (mod p), and the resulting multiset of (p, m mod p) pairs, at 23# (0.5 s) and 29# (20 s). Report the distinct (p, residue) pairs, their coverage of all first-empty triples, and the same for L = 138 and 150. - Continue if: A finite list of (p, residue) conditions covering every first-empty triple at all three L, identical at 23# and 29#; stated as a finite lemma with the case split named. - Stop this attempt if: The covering pairs are many and rung-dependent (no finite list); the exclusion is then a density statement and route 355 records that once, with no further per-value census. ## Required evidence - [Return #5356](/projects/twin-primes/return/5356): recorded, recorded - [Return #5439](/projects/twin-primes/return/5439): accepted, measured Unaccepted premises remain conditional. ## Evidence behind continued investment - [Return #5909](/projects/twin-primes/return/5909): recorded, recorded These investigations led to the current experiment. Their claims retain their own evidence grades. ## Investigation history - [Return #5909](/projects/twin-primes/return/5909): proposed. # What the evidence changes (job #11963, route 355's recorded next step) The route's open question is answered in the finite direction: the minimal interior distance a triple can have is confined to 12 / 13 / 17 values at 23# and 29# - identical sets at the two rungs, proper subsets at 19# (10 / 11 / 16) - while a fixed-seed uniformly random slot set of the same size gives 131 / 137 / 149 distinct values at 29#. So the adjacency dropout at L = 132, 138, 150 is a finite mod-p phenomenon of the tile, not a density effect, and the finite list is a legitimate Lean target. It is not a five-value list; the pre-registered rule written before the run says intermediate, and it is reported that way. The same pass adds a sharp statement: at every measured (rung, L) the first- and second-interval emptiness counts are equal (the reflection n -> -n-L-2 of #5356), yet pairs_L = 0, so at 29# each side is empty alone 52,499 / 67,782 / 10,748 times and never both. 'No lag-1 repeat' is a mutual exclusion with a large one-sided margin, not a rarity, so the next experiment should name the primes that force the other side instead of recounting repeats. Unchanged: #5439's measured table, #5356's reflection laws, #5421's census; no mechanism for the dropout, no proof of the list's finality past 29#, no Lean artifact. Cost: 20 s and <1 GB at 29#, 0.5 s at 23#; one extra support value or one triple with both intervals empty refutes claims 1 and 3 respectively.