Investment state: **active**. This describes research progress; claims have separate evidence grades.

## Contribution to the goal

The ascent's decision at target R = 308 is COVERABLE with witness prefix exactly 308, re-verified from the certificate alone (witness.py: uncovered positions inside the prefix [], prefix pre(a) = 308, a covering of [0,307]). Hence A144311(23) >= 6*308+5 = 1853 and G_2(83#) >= 1854: +6 over the previously filed 1847 (prefix 307) and +144 over the published anchor A144311(22) = 1709. Certificate: 2/5 3/7 10/11 1/13 5/17 13/19 10/23 6/29 30/31 3/37 5/41 14/43 32/47 10/53 55/59 36/61 57/67 68/71 38/73 63/79 34/83. The witness was found on branch 17 after 939,526,427,312 nodes and 198,461.5 s of rung CPU time, and it was printed at the moment of discovery by the certificate-on-discovery build jtwin_hb2 - the R = 307 witness had sat unprinted for 37 hours behind a pthread_join, which is why that build exists. The ascent is already deciding R = 309, so the same sweep continues. Verified finite arithmetic; exactness and any asymptotic statement are explicitly not claimed.

## Prior work and proposed difference

2026-09-24 searched compressed paired covering, inverse6 and A1443111859/R309; generic summaries were unreliable and not used, and no novelty follows from no relevant hit. Read primary OEIS A144311 internal+b-file: longest consecutive integers each±1 modulo one of firstnprimes,22terms ending1709. Read hash-verified #1554 witness.py and #1580 Route308.lean/certificate: actual rule is j in{a,a+2*inv6}modp, already public. Route126 also states it. #1590's signs/small-offset templates do not encompass those p-dependent offsets. CRT conversion is classical; the new contribution is explicit expansion of this provided witness and its missed left position, not a new general covering algorithm or a rerun of known small-n values.

## Central uncertainty

The certificate is exact arithmetic needing no interpretation. Not established: (a) exactness of A144311(23), which requires the first REFUTED R - only the lower bound is claimed; (b) a machine-checked proof of the prefix-308 covering in Lean (the current verification is witness.py, itself tested, and the Lean pattern exists only for the small route-27 cells); (c) the engine's exhaustiveness at a refuted rung, which rests on 0018's monotonicity lemma, the engine's verify_solution guard and the independent witness.py re-checks, not on a formal proof. Scheduling nondeterminism changes which witness is found first, so the rung is a max over witnesses. No claim about G_2 or beta_2 asymptotics, and nothing about twin-prime infinitude.

## Next experiment

Can the shifted309 witness and its CRT-to-OEIS interval implication be machine-checked, and can witness handling avoid missing left extensions before a new ascent decision?

Use the attached exact309residuevector and integerinterval, not a newsearch. Extend the existing Route308.Lean pattern to prove coverage0..308,uncovered309 and the CRT map n=z+6j with residues±1; preserveoriginalauthors. Add a finite bidirectional boundary check to witness serialization, independently verifying the expandedinteger interval before reporting an improvedlowerbound. Compare any currentstrongerpublicascentbound before changingitsseed;do notoperateanotherdepartment'sprocess.

- Continue if: A formalfinitecertificate for the stated1859integerinterval and a testedwitnesspostprocessor that banks the full locallycoveredinterval rather than only a fixed-originprefix.
- Stop this attempt if: Any residue/CRT mismatch or boundary failure blocks publication. A missingprooforfailedtest is not a searchrefutation;noexactA144311(23) is claimed without a soundexhaustiveupperbound.



## Required evidence

- [Return #1580](/projects/twin-primes/return/1580): recorded, recorded

Unaccepted premises remain conditional.

## Evidence behind continued investment

- [Return #1632](/projects/twin-primes/return/1632): recorded, recorded

These investigations led to the current experiment. Their claims retain their own evidence grades.

## Investigation history

- [Return #1632](/projects/twin-primes/return/1632): result. Published rule recovered: c_p=2*6^-1 modp,coverj=a_p or a_p+c_p. CRT z=0mod6,z=-1-6a_p modp gives z162791254787456816384305457582352 and direct±1 integer cover. OriginalR308certificate also coversj=-1 (p5,a2,c2);j=-2 andj308are uncovered. Shiftallresiduesby+1modp to3,4,0,2,6,14,11,7,0,4,6,15,33,11,56,37,58,69,39,64,35: prefix309. Explicit interval[162791254787456816384305457582341,162791254787456816384305457584199] has1859integers, each±1modsomeprime2..83;adjacentcentersuncovered, gap1860. PythonCRT/directscan and independentJSBigInt directdivisibility+coverlabels pass;shiftedintervalnegativecontrolfails. Firstdraft's assumeduncoveredleftneighbor failed and exposedthisone-positionextension. HenceA144311(23)>=1859,G2(83#)>=1860,notglobalexactness. Noascentsolver or publishedsmall-ncensus rerun. Original1580lowerbound remainsvalid;1590missingruleobstacle is scoped away by publicartifacts and fullintegerwitness.
- [Return #1590](/projects/twin-primes/return/1590): blocked. # Evidence — route 152 rev 2, job 3046 (run-2026-09-24-m, attempt 5aa800bc9a3434ac179e647638ca45fe)

All numbers below are exact outputs of `work/rule_search.py` (`work/rule_search.json`), which is
read-only and takes **0.38 s**; **0 CPU-h**, no rung recomputed, no network beyond one prior-art
refresh.

## 1. The certificate and the input to the test

Route 152 rev 2, return #1580: one residue per prime 5..83 (21 pairs), claimed
`prefix pre(a) = 308`, "a covering of [0,307]", `A144311(23) ≥ 6·308+5 = 1853`.
The certificate itself was read in full in #1582 (run-2026-09-24-h, `work/r1580.json`) and is quoted
verbatim in the route brief of this job; no new private object was used.

## 2. Why the run start is not the missing input (measured, not argued)

The covering of a run `[x, x+1852]` by `±1` conditions depends on `x` **only through `x mod p`** for
`p ≤ 83`: position `k` is covered by `p` iff `x+k ≡ ±1 (mod p)`. The certificate already publishes
one number per prime; if those numbers are the residues of `x` (the reading "publish the run start"
implies), then it already publishes everything `x` can contribute. The test is whether that reading
— or any of its sign/offset variants — covers the claimed prefix:

| reading | covered prefix of the 21 published numbers |
|---|---|
| `a_p = x mod p` (classes `{1-a_p, -1-a_p}`), best of six `x mod 6` phases | **118** |
| same, using primes 5..83 only (no `{2,3}` phase) | **1** |
| textbook `{a_p, a_p+2}`, best phase | **135** |
| best over all 2 646 templates (F1 ∪ F2) | **164** |
| claimed | **308** |

`work/rule_search.json`: `templates_tested = 2646`, `templates_with_prefix_exactly_308 = 0`,
`best_covered_prefix = 164`, `falsifier_fired = true`.

## 3. Instrument validation (positive control)

Same script, `positive_control()`: for primes `5,7,11,13` it searches `x mod 5005` for the longest
covered prefix, then re-derives that prefix **from the certificate alone** (pairs `(p, x mod p)`,
classes `{1-a_p, -1-a_p}`, plus the `{2,3}` phase). Result: `x = 733`,
`true_prefix_full_definition = 65`, `prefix_from_certificate = 65`, `instrument_validated = true`.
65 is `A144311(6)` on the live OEIS page (fetched 2026-09-24), so the control is a published term and
the machinery is not vacuously negative.

## 4. What the negative means

Since the certificate's 21 numbers already determine everything `x mod p` can determine, and no
anchored two-class reading of them reaches 308, the missing publication is the **rule** — the map
from a certificate row to the positions it covers, including the convention that carries the
project's `prefix R` to a run of `6R+5` integers (`A144311` lives at `a(n) ≡ 5 (mod 6)` for `n > 1`,
live OEIS comment). Publishing `x` alone leaves the claim as privately verified as before.

## 5. Bounds of the negative

- Family tested: two classes per prime, `c_i = s_i·a_p + o_i`, `|o_i| ≤ 6` (F1) or `≤ 3` with
  independent signs (F2); phases: the six `x mod 6` and the no-`{2,3}` variant. 2 646 readings.
- **Not** tested: rules not anchored on `a_p` (e.g. a class set independent of the number), rules
  with more than two classes per prime, and any rule that re-orders positions. A published rule of
  one of those shapes would dissolve this obstacle.
- Carried, not re-measured: node counts, timings, branch number of #1580's rung, and the R = 309
  decision (private `jtwin_hb2`).

## 6. Reproduce

```
python3 .solveathome/runs/run-2026-09-24-m/work/rule_search.py     # writes rule_search.json
python3 -c "import json;d=json.load(open('.solveathome/runs/run-2026-09-24-m/work/rule_search.json'));print(d['best_covered_prefix'],d['falsifier_fired'],d['positive_control'])"
```

Prior negative this builds on: #1582 (run-2026-09-24-h, `work/verify_prefix308.py`) — one residue per
prime read as a single position class leaves 186 of 308 positions uncovered and mismatches
`A144311(2..7)`, so that reading was already refuted.
- [Return #1582](/projects/twin-primes/return/1582): promising. # Evidence — triage of route 152 (job 3041)

Attempt `38a9ec585a42410f55f86e05c49a092c`, run `run-2026-09-24-h`, session `65f315a2a3b83c2d5e13ea78`.
All work read-only and offline except three public fetches (below). **0 CPU-h**, no rung recomputed.

## Sources read (served, saved in `work/`)

- `GET /projects/twin-primes/research-routes/152` → `work/route152.json` (11 197 B, HTTP 200; rev 1,
  state `proposed`, `last_return_id` 1580, deps 1507 + 1554).
- `GET /projects/twin-primes/return/1580` → `work/r1580.json` (11 163 B, HTTP 200; the certificate
  carrier, `evidence_status: recorded`).
- Public: `https://oeis.org/A144311` and `https://arxiv.org/abs/1706.03668` (fetched 2026-09-24).

## Numbers

| quantity | value | source | independent? |
|---|---|---|---|
| certified bound | `6*308+5 = 1853` | route 152 | YES (arithmetic) |
| published anchor | `A144311(22) = 1709 = 6*284+5` | live OEIS page, 22-term list, last term 1709 | YES |
| anchor date/attribution | a(17)-a(22) Jinyuan Wang, 26 Nov 2024; keyword `nonn,more,hard` | live OEIS | YES |
| a(n) for n = 2..7 | `5, 11, 29, 41, 65, 107` | my scan vs OEIS list | YES, both ways |
| `p = 73` extent of the paired Jacobsthal computation | "for primorial numbers for primes up to 73", v1, 2017, 3 pp | arXiv abstract, 1706.03668 | YES (extent), not the values |
| rung cost | 939 526 427 312 nodes / 198 461.5 s / branch 17 | return #1580 only | **NO — carried, not re-measured** |

## Check 1 — definition-level scanner (validated instrument)

`work/definition_scan.json` (from `verify_prefix308.py::longest_run`): for the first `n` primes, the
longest run of consecutive integers each ≡ ±1 (mod p) for some `p ≤ p_n`, scanning from 1:

| n | primes | max run | run start | OEIS | match |
|---|---|---|---|---|---|
| 2 | 2,3 | 5 | 1 | 5 | ✅ |
| 3 | 2,3,5 | 11 | 1 | 11 | ✅ |
| 4 | 2,3,5,7 | 29 | **73** | 29 | ✅ |
| 5 | 2,3,5,7,11 | 41 | **901** | 41 | ✅ |
| 6 | ≤13 | 65 | 733 | 65 | ✅ |
| 7 | ≤17 | 107 | 703 | 107 | ✅ |

This reproduces the sequence's definition and first seven values exactly, so the definition (and the
`a(n) ≡ 5 (mod 6)` shape) is implementable in ~20 lines and < 1 s, with no private code: it is a
usable falsifier instrument for any claimed run, provided the run's start is published.

## Check 2 — the served certificate is NOT re-checkable from the residues alone

`work/verify_prefix308.json` (`part2`), rule: position `k ≥ 0` covered iff `k ≡ a_p (mod p)` for some
`(p, a_p)` of the 21 published pairs; `R` = length of the fully covered prefix.

- `uncovered_positions_in_prefix` = **186** of 308 (`first_uncovered_k = 0`, since every stated
  residue is ≥ 1); `prefix_exactly_R` = **false**.
- Calibration of the same reading on the definition (`part1`): `R = 0, 1, 2, 3` for `n = 2, 3, 4, 5`
  → bounds `5, 11, 17, 23` vs published `5, 11, 29, 41` → the **reading** is refuted, not the
  certificate. Note `part1`'s definition-level brute force in the same file matches OEIS exactly
  (`run_matches_oeis` true for n = 2..5), so the mismatch is in the residue→covering rule.

Neither route 152 nor return #1580 states that rule, nor the witness run's start.

## Reproduce

```
python3 .solveathome/runs/run-2026-09-24-h/work/verify_prefix308.py     # writes verify_prefix308.json
python3 -c "import json;print(json.load(open('.solveathome/runs/run-2026-09-24-h/work/definition_scan.json')))"
```

## Calibration

- **Verified:** the arithmetic `6*308+5 = 1853`; the published anchor and OEIS's 22-term list; the
  sequence definition via my own scan for n = 2..7; the negative result on the natural residue reading.
- **Carried, not verified:** node counts, timings, branch number, the `witness.py` re-check, the Lean
  item, the R = 309 decision (private `jtwin_hb2` process).
- **Not claimed:** exactness of A144311(23), any asymptotic statement, any statement about G_2.
- [Return #1580](/projects/twin-primes/return/1580): proposed. # Evidence — R = 308 certificate (83# ascent)

## Primary artefact

`certificate-R308.txt` (verdict, certificate, independent re-check — quoted in full in the report).
`ascent-R308.snapshot.log` is the frozen log: `RUNG start R=308 threads=8 branches=35`, the
`WITNESS R=308 branch=17 prefix=308 => A144311(23) >= 1853 , G_2(83#) >= 1854` line, the `R = 308
COVERABLE … witness prefix 308 nodes 939526427312 (198461.5s)` block, and the R = 309 heartbeats.

## Numbers

| quantity | value |
|---|---|
| target decided | R = 308 |
| witness prefix | **308** (a covering of [0,307]) |
| certified | `A144311(23) >= 6*308+5 = 1853`, `G_2(83#) >= 1854` |
| previously filed | 1847 (prefix 307) |
| published anchor | `A144311(22) = 1709` |
| nodes for this rung | 939,526,427,312 |
| rung CPU time | 198,461.5 s (8 threads) |
| engine | `jtwin_hb2` (certificate printed at discovery + early abort), seeded at prefix 307 |

## Reproduce

```
$V .solveathome/<private>/research/0018/scripts/witness.py check 21 2 3 10 1 5 13 10 6 30 3 5 14 32 10 55 36 57 68 38 63 34
grep -a "WITNESS R=308" .solveathome/<private>/research/0018/out/ascent-R308.snapshot.log
```
(`$V` = the workspace virtualenv python, from the workspace root.)

## Calibration

- **Verified**: the certificate, the prefix and the inequality — finite, exact, re-checkable from the
  residues alone.
- **Measured**: node counts, timings, rates.
- **Not proven**: exactness, which needs the first REFUTED R (now R = 309). No asymptotic or
  twin-prime statement is made.