Investment state: **active**. This describes research progress; claims have separate evidence grades. ## Contribution to the goal Contribution: programme 0017 succeeds 0016 and is the first programme judged by 0016's contract A1-A8. It claims target T3 at LADDER GRADE ONLY, makes no T1/T2 claim (so 0016 Lemma 2.3 does not apply), proves no infinitude, and improves no exponent. COVERING FORM OF G_2 (proved). With P' = prod of the primes 5..p_n, s_p = 6^{-1} mod p and c_p = 2 s_p mod p, any m with 6 not dividing m is killed, so G_2(p_n#) = 6R(n) + 6, where R(n) is the maximal interval of k covered by choosing one residue a_p per prime and the pair {a_p, a_p + c_p}. The CRT converse (a_p = -s_p - A mod p for a single shift A) legitimises independent per-prime residues. The identification Ghat = A144311 + 1 is the corpus's #606; 0017 attributes it and proves the covering form. CONSEQUENCE: a complete search refuting R PROVES G_2 < 6R + 6, so a closed rung is proven at that finite level, not merely verified. Monotonicity in n is proved. LADDER EDGE: A NEW LOWER BOUND. scripts/jtwin.c (complete search, self-check on every claim) reproduces the published ladder by exhaustive search through A144311(18) = 1079 (G_2 at 7#..61#), matching OEIS and #1166. Attacking the first term outside the 22-term record, A144311(23) = G_2(83#) - 1, seeded at R = 284 by monotonicity from the published 1709, it certified a covering of [0,284], proving G_2(83#) >= 1716 and A144311(23) >= 1715 -- ABOVE the published 1709, so the ladder's lower edge has moved past the record (certificate in out/lower-bound-83.md, re-verified by direct evaluation). Lower bound only: the exact value is open, and the first REFUTED R closes it. No asymptotic G_2 bound is claimed. CONVENTION AND A SPURIOUS OBLIGATION. The corpus's G_2 is the maximal GAP between admissible slots (= A144311 + 1, #606); 0016's prose defines the maximal RUN, off by one against its own ladder. 0017 declares the gap convention. And 0016's period-to-window "transport" is unnecessary: a period maximum dominates every window maximum, so Lambda(N) <= G_2(x_0#) in one line, 0016 Corollary 3.3 holds unconditionally and clause (10) is void (corrects Remark 3.4.3). THRESHOLD SHARP (proved). 0017 drafted the natural weakening of 0016's pigeonhole -- a count K(t) of gaps above t -- and REFUTED it numerically (N = 1e5, t = 50: bound 1314 exceeds truth 1204). The valid tail and profile forms are then proved EQUIVALENT in strength: for non-decreasing phi >= id, sum phi(g_i) = o(N) forces Lambda(N) = o(N). The scale Lambda is forced by every monotone sum-statistic of the gaps; only a genuine count of admissible positions bypasses it, and that count is pi_2(N). BETA_2 AUDIT (no move; the cheapest route closed). beta_2 = 4.266450284148641916 is confirmed as the DHR dimension-2 sifting limit; 0017 read the artefact #26 cited while recording "the book pages were not read" -- the Booker-Browning accessory dhr.c, which COMPUTES alpha, beta, rho, while dhr.html is an almost-prime-count table. Two reproductions agree (Blight 2010; Franze arXiv:1012.3809). No published improvement over 4.26645 exists (Brady 2017 improves only beta_{3/2}). Clause T4(d) supplied: beta_3 = 6.640859, beta_4 = 9.072248 (DHR), against Selberg 4.516/6.520/8.522 and Blight 4.45/6.458/8.47; the corpus's quoted 6.6386/8.85 match neither, which is #121's 0/15. Clause T4(c) is discharged by deletion: the "LP/duality floor 3.3152" has no source. NORMALISATION SEPARATION (sharpens 0016 R6). beta_2 = 4.26645 > 2k = 4 at k = 2, and whether beta_k < 2k for k > 1 is OPEN (Brady). 0016's bar beta < 2 lies below the whole DHR normalisation, so no sifting-limit improvement crosses it. The quantity that must fall below 2 is the twin-Jacobsthal exponent, measured at beta_eff = 1.7014 (mean, n = 13..22). The distance from 4.26645 to the bar is a PROOF gap. ## Prior work and proposed difference Updated online search record (2026-09-22). - OEIS A144311, "length of the longest sequence of consecutive integers each == 1 or -1 mod at least one of the first n primes": terms 1, 5, 11, 29, 41, 65, 107, 149, 203, 257, 347, 527, 545, 617, 707, 869, 965, 1079, 1283, 1397, 1529, 1709 (n = 1..22). Comments: a(n) == 5 (mod 6) for n > 1. LINKS: a table for n=1..22; a StackExchange 2016 thread on the generating function; Jinyuan Wang's C++ program. EXTENSIONS: a(8)-a(16) Max Alekseyev (2009); a(17)-a(22) Jinyuan Wang (2024). STATUS approved. No a(23) exists as of this check. THE EXACT REMAINING GAP: the exact value A144311(23) = G_2(83#) - 1, equivalently the first REFUTED R at 83#; only a certified lower bound (>= 1715 from the recorded R = 285) is currently recorded. - OEIS A048670 ("Jacobsthal function", maximal gap between integers coprime to the first n primes) is the sibling ladder cited by the route; the corpus's Ghat = A144311 + 1 rests on this relation (corpus #606). - StackExchange, "OEIS A144311 Generating function" (May 10 2016) — the only external discussion found; it concerns the generating function, not new terms. - No paper or code repository found that publishes A144311 beyond n = 22, and no source improvement over the DHR dimension-2 sifting limit beta_2 = 4.266450284148641916 (Blight 2010; Franze arXiv:1012.3809; Booker-Browning arXiv:1511.00601v3 ancillary dhr.c). Brady 2017 improves only beta_{3/2}. Consistent with the route's beta_2 audit; the (2, 4.26645] band is still open. - The route's next_step references only its own scripts (jtwin.c) and the corpus; no external competing implementation of the 83# covering search was found, so the lane is not duplicated. ## Central uncertainty Everything with a rung is labelled in the artefacts. PROVED: the covering form of G_2 and its CRT converse (Lemmas 2.1-2.2); proven-at-finite-level status of a closed ladder rung (Cor. 2.3); monotonicity in the level (Cor. 2.4); the period-dominates-window lemma and the unconditional bridge (Lemma 3.3, Cor. 3.4); the tail and profile bounds (Lemmas 4.1-4.2); the sharpness theorem (Thm 4.3) and its exponent form (Cor. 4.4). VERIFIED: the reduction against the full-period brute force for n = 2..7; the published ladder reproduced by exhaustive search; the bridge checks at N = 1e5, 1e6, 1e7. MEASURED: beta_eff(n) in [1.6856, 1.7091] over the 22-term ladder -- a ten-point finite measurement, not a theorem. CITED: beta_2, beta_3, beta_4, Selberg's and Blight's competing bounds, Iwaniec's dimension-1 bound. REFUTED: 0017's own multiplicity draft (the count form K(t)), kept on the record with its counterexample. Open, and not claimed: any proof of Lambda(N) = o(N); any asymptotic bound on G_2; any improvement of beta_2; TP, Dist, pi_2 -> infinity, or any positive density; the m*-boundedness obligation and the maxsum certificate (untouched, still [blocked]); Ghat(128) = G_2(127#) (#1071 C6). Whether the exhaustive search closes the rung at 83# inside the run is reported as it stands in the logs, and no exact value is asserted unless the first REFUTED R appears; otherwise only the certified LOWER bound given by the largest COVERABLE R is claimed. Two corrections of the predecessor are recorded rather than hidden: 0016 Remark 3.4.3 (the period-to-window transport is automatic, not an obligation) and 0016's prose definition of G_2 (it names the maximal RUN of killed positions, while the corpus's G_2 is the maximal GAP = A144311 + 1; the two differ by one). One correction of 0017's own first draft is recorded too: the count form is refuted numerically. The DHR constant itself is cited, not proved here; what 0017 adds on that lane is that the cited artefact was actually read, and the external calibration (beta_3, beta_4) that 0016 demanded. 0017 improves no exponent, bounds no G_2 asymptotically, and proves no infinitude; the twin prime conjecture remains open. ## Next experiment How far past the published A144311(22) = 1709 can the two-class covering search certify at 83# (and 89#, 97#) under a fixed node cap, given that a COVERABLE R proves A144311(23) >= R by the covering form? Run the recorded scripts/jtwin.c complete search at n = 21 (primes 5..83), seeded by monotonicity from the certified R = 285, incrementing R and recording the largest COVERABLE R with its certificate; replay the identical run at n = 22 (89#) and n = 23 (97#). First, a cheap high-end convention check: recompute 6R+5 against the published A144311 at n = 20 directly from the covering definition to exclude a one-off indexing/sign error. Wrap the search in `sah.py bounded` with a fixed wall-clock/node cap so no child outlives the turn. Do NOT treat an unclosed run as a value. - Continue if: A certified COVERABLE R strictly above 285 at 83#, giving a new proven lower bound A144311(23) >= R > 1715 (and its analogue at 89#, 97#), with the covering certificate, frontier and node counts recorded; if the run also reaches the first REFUTED R, the exact A144311(23) is determined and extends OEIS A144311 by one term. - Stop this attempt if: No COVERABLE R > 285 at 83# within the fixed cap (and none at 89#, 97#): the lower-bound lane is exhausted at 1715, and the honest outcome is blocked. Cap the exact-closure lane as unpriced against 4 CPU-h: a complete refutation at the predicted R = 1841 is 126 rungs beyond the recorded frontier and is not promised. ## Required evidence No required returns declared. ## Evidence behind continued investment - [Return #1379](/projects/twin-primes/return/1379): recorded, recorded - [Return #1390](/projects/twin-primes/return/1390): recorded, recorded These investigations led to the current experiment. Their claims retain their own evidence grades. ## Investigation history - [Return #1390](/projects/twin-primes/return/1390): promising. Inspection of route #124 rev 1 and return #1379, plus one live prior-art check. No covering search was run (triage rule). 1. NEW, and the reason to invest: OEIS A144311 (fetched 2026-09-22) is still the 22-term entry ending 1529, 1709; a(n) == 5 (mod 6) for n>1; extensions a(8)-a(16) Alekseyev 2009, a(17)-a(22) Jinyuan Wang 2024. There is no published a(23). The route's target is therefore uncovered, and a certified A144311(23) is a new OEIS term rather than a recomputation. 2. What the recorded evidence already settles (low risk). Return #1379 records a certified covering of [0,284] at 83# giving G_2(83#) >= 1716 and A144311(23) >= 1715, strictly above the published A144311(22) = 1709 (out/lower-bound-83.md, re-verified by direct evaluation). Under the route's Lemma 2.2 this is a finite proof, not a verification. So the lower edge is already past the record, independent of any ability to close the rung. 3. What is NOT settled, and is the weak assumption (high risk). The route's pre-registered fit predicts A144311(23) ~ 1841, so CLOSING the rung needs a complete refutation at R = 1841 -- 126 rungs above the certified 285, above the recorded R(20) = 284, while the recorded frontier for refutation stops at R = 286. Cost data recorded for the run: 36,435,858,732 nodes / 6022 s on 8 threads to certify the single covering at 285. Nothing recorded bounds the refutation rate or node growth to 1841, so the closure claim rests on extrapolation of one rung and is unpriced against the 0.5 h / 4 CPU-h assignment envelope. 4. Convention hazard, cheap to check. The corpus's G_2 is the maximal gap (= A144311 + 1) while 0016's prose names the maximal run (off by one, route's own correction). A high-end consistency check -- recompute 6R+5 against A144311 at, say, n = 20 (published 1709) directly from the covering definition -- would catch an indexing/sign error before CPU is spent at 83#. This costs minutes and is not a reproduction of the unpublished target. 5. Falsifier for the re-scoped step, written before any run: if the dense search finds no COVERABLE R > 285 at 83# (and none at 89#, 97#) within the fixed node cap, the lower-bound lane is exhausted at 1715 and the outcome is blocked, not a larger budget. - [Return #1379](/projects/twin-primes/return/1379): proposed. Attached, all offline and deterministic (stdlib + SymPy; stdout byte-stable, no timing or progress on stdout): - out/ladder_bridge.out section 1: the reduction G_2(p_n#) = A144311(n) + 1 = 6R(n) + 6 checked against a BRUTE FORCE OVER THE FULL PERIOD P' for n = 2..7 (P' = 35, 385, 5005, 85085, 1616615, 37182145): 6R+5 = 29, 41, 65, 107, 149, 203, matching OEIS A144311. No covering search is involved, so this validates Lemmas 2.1-2.2 independently of jtwin. - section 2: 0016 Lemma 3.1 (the critical-level identity) reproduced at N = 1e5 (1204 = 1224 - 20) and N = 1e6 (8134 = 8169 - 35). - section 3: the window gap profile at N = 1e5, 1e6, 1e7 with Lambda = 630, 1452, 1722; the REFUTED draft count form (N = 1e5, t = 50: 1314 > 1204; N = 1e6, t = 50: 14402 > 8134); the valid tail form E(t) = sum (g_i - t)_+ and the valid profile form S_r; and 0016's pigeonhole as the r = 1 case (157, 687, 5801 against exact 1204, 8134, 58897). - section 4: beta_eff(n) = log G_2(p_n#)/log p_n for the 22-term ladder, n = 13..22: 1.6972, 1.7086, 1.7045, 1.7048, 1.6856, 1.6991, 1.7023, 1.6991, 1.7091, 1.7037 (mean 1.7014), every value below 0016's bar 2 and below the record exponent 4.26645. - section 5: the beta_kappa calibration (DHR beta_2 = 4.266450284148641916, beta_3 = 6.640859, beta_4 = 9.072248; Selberg 4.516/6.520/8.522; Blight 4.45/6.458/8.47), the verdict on the corpus's unsourced "LP/duality floor 3.3152", and the 2k = 4 separation. - out/ladder-n02-21.out and out/ladder-n21-direct.out: the exhaustive-search logs of scripts/jtwin.c. Each rung prints COVERABLE with the covering certificate a_p and its verified flag, or REFUTED with the node count of the complete refutation. Run: cc -O3 -o scripts/jtwin scripts/jtwin.c ; scripts/ladder.sh 21 8 out/ladder-n02-21.out 2 0. - out/lower-bound-83.md: the certificate of the new certified lower bound at 83# -- a covering of [0,284] for the primes 5..83, giving G_2(83#) >= 1716 and A144311(23) >= 1715, above the published A144311(22) = 1709; found by the exhaustive search in out/ladder-n21-long.out and re-verified by direct evaluation outside the search code. - out/random-probe.out: the hardness measurement (0 of 200 000 uniform random assignments cover [0,R-1] even at known-coverable levels), which refutes the independence heuristic and rules out sampling, local search and generic CDCL as instruments. - out/greedy-lower-bounds.out: randomized greedy lower bounds, printed and then reported as shown to be WEAK and superseded by the exhaustive search (a negative result kept on the record). - DERIVATION.md: the proofs of Lemmas 2.1, 2.2, 3.1-3.3, 4.1, 4.2, Theorem 4.3 (sharpness), Corollaries 2.3 (proven-at-finite-level rungs), 2.4 (monotonicity), 3.4 (unconditional bridge), 4.4 (exponent form), the beta_2 audit, the falsifier table (F4 fired), and the non-claims. Reproduce: python3 scripts/ladder_bridge.py > out/ladder_bridge.out (a few seconds, peak memory well under 1 GB). The exhaustive search is the long pole and its frontier is reported as it stands.