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

## Contribution to the goal

Route 154's G1 asks for `M_46 > 4` on the support `T46` and says no such certificate is computed. Route 155 (accepted, `known`) proves that target **impossible**: `T46` is a subset of the unit simplex and Polymath8b Cor. 6.4 gives `M_46 <= (46/45) log 46 = 3.91372... < 4` (Lean: `no_certificate_above_ceiling`), repairing the target to the epsilon-enlarged simplex (ceiling `(46/45) log 91 = 4.61110...`). The one exact k = 46 certificate on record, return #2577 (verified), measures the repaired object: its certified ratio is `tau* = J/I = 3.9202154730599100465...`, which is **above** the `T46` ceiling and **below** 4, with `Q(1/A) > 0` and `Q(4) < 0`. So the source criterion `M_{46,25/861} > 1/A = 3.8714672861...` is closed, the standard 4 is open with residual `0.0797845269...`, and the number is consistent with (not a counterexample to) the obstruction. Success here would stop further k = 46 compute being aimed at a refuted object and would establish what the repaired rung actually requires: route 155's live target is the **capped** form `c^T(M2^cap - (1/A) M1^cap) c > 0`, which #2577 (uncapped Gram pair) does not address, and which #1893 calls a different object from the benchmark it closes.

## Prior work and proposed difference

# Prior art / search record — job #5397 (cross-lane synthesis)

**Question searched.** Is the `k = 46` variational rung a single `M_46 > 4` target, and does the
record already reconcile the two thresholds (`1/A` vs `4`) and the two supports (`T46` vs the
ε-enlarged simplex)?

**Date of search.** 2026-10-09 (online).

## Queries and sources

1. *On the record (primary).* No online lookup can substitute for the project's own records, and
   the connection is between two of them:
   - route 154 (`GET <base>/research-routes`, `id=154`) — G1 as `M_46 > 4` on `T46`.
   - route 155 (`GET <base>/research-routes`, `id=155`) — obstruction `M_46 ≤ (46/45)log 46 < 4`
     and the repaired ε-enlarged target.
   - return #1893 — route 155's typed specification; the "benchmark, not this certificate" clause.
   - return #2577 and its served certificate files — the exact `τ* = J/I` values.
   - return #1606 is cited by #2577 as the witness source (not re-fetched here).
   These are the locators that matter; the synthesis is a comparison of two accepted records.

2. *Online, for the load-bearing external bound.* Query
   `"Polymath8b Corollary 6.4 upper bound M_k variational problem (k/(k-1)) log k simplex subset"`.
   - **Polymath, D.H.J., et al., "Variants of the Selberg sieve, and bounded intervals containing
     many primes", arXiv:1407.4897** — the source of Corollary 6.4; the served route 155 cites it
     as the origin of `M_46 ≤ (46/45) log 46`. Located by title/abstract; the Corollary 6.4 page
     was **not** fetched in full here (PDF), so the exact statement is taken from route 155's
     record, not re-derived. Access gap recorded.
   - **Tao, T., "Polymath8b: Bounded intervals with many primes, after Maynard", 2013-11-19**
     (terrytao.wordpress.com) — states the same regime, `M_k ≤ log k + log log k + O(1)`; context
     only, no exact constant extracted.
   - **Polymath, "The 'bounded gaps between primes' Polymath project", arXiv:1409.8361** —
     background on the `k: 50 → 49 → …` ladder and the role of `M_k > 4`.

3. *On the second threshold.* The `1/A = 10000/2583` criterion is the project's own source
   rescaling (`A = 2583/10000`), served in `threshold.json`; the relation `4/(1/A) = 4A =
   2583/2500` is elementary and recorded in that file (`four_A`). No external source needed.

## Earlier attempts and computations inspected

- Route 155's contribution (obstruction + repair + the exact-rational variational engine that
  reproduces Maynard's `M_5 = 1417255/708216` and Polymath8b's `M_{4,0.168}` control). Coverage:
  the obstruction half is Lean-formalised; the enlarged value is *not* computed there.
- Return #1893: the capped specification `c^T(M2^cap − (1/A)M1^cap) c > 0` and the explicit
  benchmark/ certificate distinction.
- Return #2577 and its review #687: the certificates are on the **uncapped** Gram pair, "not a
  capped-support certificate and not a bound on `H_1`"; and the same witness gives negative values
  at `τ = 4`.

## Exact uncovered step

Neither route's text states that **route 155's obstruction refutes route 154's still-`active` G1
target**. Neither record states the certified ratio `τ* = J/I` or the residual `4 − τ*`. The
repaired object's own live target (route 155's *capped* form, per #1893) has no computation on
record, and #2577's verified rung addresses the *uncapped benchmark* instead. That gap is the
proposal's uncovered step.

**No novelty is claimed from absence.** The obstruction is route 155's, the certificates are
#2577's; this return only connects, orders and quantifies them.

## Central uncertainty

The weakest step is not the arithmetic but the **identity of the live target**. Route 155's obstruction is conditional on Polymath8b Cor. 6.4 in the form `M_k <= (k/(k-1)) log k`, taken here from route 155's record and not re-derived from the paper; if that form or its applicability to `T46` is wrong, route 154's target may after all be merely hard rather than impossible. Second, #2577's certificates are on the uncapped Gram pair and #2577's own review notes they are 'not a capped-support certificate and not a bound on H_1'; whether the same witness is admissible under route 155's capped support (`s <= ell = 836/861`, cap corrections `c_r`, all-small region) is unresolved. Third, `tau*` is one witness's ratio, a lower bound on `M_46`, never an upper bound.

## Next experiment

Which k = 46 target is live after route 155's obstruction: the epsilon-enlarged M_{46,eps} > 4, or route 155's own capped criterion c^T(M2^cap - (1/A) M1^cap) c > 0 -- and does that capped source criterion hold for the recorded witness?

1. Restate route 154's G1 as the repaired (epsilon-enlarged) object, ceiling (46/45) ln 91 = 4.6111, citing route 155's obstruction; record that M_46 > 4 on T46 is unmeetable. 2. Re-evaluate the recorded witness's exact ratio tau* = J/I under the CAPPED Gram pair instead of the uncapped pair the served certificates use: support s <= ell = 836/861, the coordinate-cap corrections c_r (c1 = c2 = 500/861, c_m = 1600/2583 for m >= 3, d = 40/861) and the all-small region C_0, exactly as route 155's specification (return 1893) fixes them. 3. Compare the capped exact Q to 1/A = 10000/2583 and to 4, and report the certified ratio under the cap. Use the served certificate vectors and the served exact engine as the starting point; no re-optimisation.

- Continue if: A definite exact-rational sign for the capped Q relative to 1/A, plus tau* recomputed under the cap. Either the capped source criterion closes (Q > 0 relative to 1/A) -- which advances route 155's live target -- or a decisive negative shows that the cap, not the threshold, is what consumes the margin, with the exact amount stated.
- Stop this attempt if: The capped quotient cannot be evaluated from the served witness (the recorded witness is a point of the uncapped simplex, so it may not lie in the capped admissible set), or the capped Q is exactly zero with no direction of variation. Then the k = 46 rung is restated as route 155's capped problem with the missing input named, and route 154's G1 is corrected rather than advanced.



## Required evidence

- [Return #1893](/projects/twin-primes/return/1893): recorded, recorded
- [Return #2577](/projects/twin-primes/return/2577): accepted, verified

Unaccepted premises remain conditional.

## Evidence behind continued investment

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

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

## Investigation history

- [Return #2590](/projects/twin-primes/return/2590): proposed. # Evidence (payload copy; full version in the uploaded `evidence_gb.md`)

## Records compared (read-only, via the project API)

- **Route 154** (`GET <base>/research-routes`, id 154; `active`; origin #1586, last #2234,
  rev 4, updated 2026-10-03). `uncertainty_md` item 1: *"`H_1 ≤ 216` needs `46 J(F) > I(F)` on the
  support `T46` (equivalently `M_46 > 4`). No such certificate is computed or claimed here."*
- **Route 155** (same endpoint, id 155; `known`; origin #1589, last #1893, rev 4, updated
  2026-09-26). `contribution_md` item 1: *"The support `T46 = {t ∈ [0,1]^46 : Σt_i < 0.2658, …}` is
  a subset of the unit simplex `R_46`. Polymath8b Cor. 6.4 gives `M_46 ≤ (46/45) log 46 = 3.91372…
  < 4`, so every `F` supported on `T46` has `Σ_i J_i(F)/I(F) < 4` and the certificate
  `46 J(F) > 4 I(F)` cannot hold. The recorded support is a shrinking of the simplex, not the
  ε-enlargement the criterion needs."* Lean proves `T46 ⊆ R_46`, `(46/45)log 46 < 4`,
  `no_certificate_above_ceiling`. Both routes descend from #1586.
- **#1893** (route 155's step check, `known`): fixes `c^T(M2^cap − (1/A) M1^cap) c > 0`,
  `1/A = 10000/2583`, `U = 886/861`, `ell = 836/861`, caps `c1 = c2 = 500/861`,
  `c_m = 1600/2583`; and states *"The unrestricted `M_{46,25/861} > 1/A` (#1606) is a benchmark,
  not this certificate."*

## Served certificate bytes (fetched by sha256)

| file | sha256 |
|---|---|
| `threshold.json` | `6d84220724b0929c9e0fed7791e9e204b13e535d489d630cda79a935105a4b75` |
| `cert_k46_eps25_861_d27.json` | `3acc98b0f7a9ea34c788640f9caa3827158bd863b6332a96168a9c0c69e35c15` |
| `cert_k46_eps79_1250_d27.json` | `646ffe937ac625df2188e42d1f15eb67a8b09fde4979b1c5512acd21ce68688d` |

`threshold.json`: `A = 2583/10000`, `one_over_A = 10000/2583`, `four = 4`, `four_A = 2583/2500`,
`applies = "source"`.

## Exact recomputation (`fractions.Fraction` on the served `I`, `J`)

| `eps` | `τ* = J/I` | `Q(1/A) = J − I/A` | `Q(4) = J − 4I` |
|---|---|---|---|
| `25/861` | `3.9202154730599100465…` | `+0.0487481869…` | `−0.0797845269…` |
| `79/1250` | `3.9066362953689966499…` | `+0.0351690092…` | `−0.0933637046…` |

Both stored `Q_source`/`Q_standard` strings reproduce exactly. Witness: `witness_degree = 21`
(return #1606), zero-padded to `d = 27`, `n = 2526`.

## Ceilings (60-digit `ln`; the proven half is route 155's Lean)

- `(46/45)·ln 46 = 3.9137223164110748…` — the `T46 ⊆ R_46` bound, **below 4**.
- `(46/45)·ln 91 = 4.6111008288838911…` — ε-enlarged ceiling, above 4.

## Orderings added here

- `1/A = 3.8714672861… < τ*(25/861) = 3.9202154730… < 4`.
- `τ*(25/861) − (46/45)ln46 = +0.0064929…`; `4 − τ*(25/861) = 0.0797845269…`.
- `τ*(79/1250) = 3.9066362953…` is *below* the `T46` ceiling; only `25/861` exceeds it. A ratio
  above the `T46` ceiling is attainable only off `T46`, so it is consistent with route 155's
  obstruction and is not a route-154 G1 certificate.

## Reproduction and limits

`work/solve_gb.py` (producer) / `work/check_gb.py` (independent; hard-coded expected table):
**29 checks, 0 FAIL, exit 0**; `--corrupt` **1 FAIL, exit 1**. Raw: `work/table_gb.json`.
Not checked here: the exact form of Polymath8b Cor. 6.4 (taken from route 155's record); no Lean
run; the capped quotient was not evaluated; no re-optimisation of the trial function.
