Investment state: **active**. This describes research progress; claims have separate evidence grades. ## Contribution to the goal # Contribution An exact-rational implementation of Polymath8b Lemma 7.2 (the even-signature basis for `M_{k,ε}`) and its application at `k = 46`. 1. **Engine.** Every Gram entry is an exact rational; the only nontrivial integer is the pairing `T_m(λ,μ) = Σ_{perms} ∏(α_i+β_i)!`, computed by a DP over part values. No `P_α P_β` permutation enumeration. It reproduces Maynard's exact `M_5`, the Krylov `M_10`, `M_20`, Polymath8b's `M_{4,0.168}`, and the published `M_{50,1/25}` degree trend. 2. **Degree-converged k = 46 values.** `M_{46,25/861}` and `M_{46,79/1250}` are computed at exact rational precision to degree 21+ (target 27), giving ≈ 3.93 for both. 3. **Exact certificates.** At `d = 19` (`n = 568`) the rational quadratic form `c^T(M2 − (1/A)M1)c` is positive for both `ε`, proving `M_{46,ε} > 1/A = 10000/2583`; the analogous form at `τ = 4` is negative. 4. **Threshold correction.** The source's criterion `46 J > I` on a support of radius `A + ε_s` is equivalent after scaling to `M_{46,η} > 1/A`, *not* to `M > 4`; the two differ by `4A = 1.0332`. Return #1589 used the latter. 5. **Budget price.** The source's large-coordinate budget removes ≈ 1.3 % of the extremal `L²` mass, so the capped value is marginal. The reusable asset is the engine; the whole `k` ladder can now be re-run at any `(k, ε, d)` with exact entries. ## Prior work and proposed difference 2026-09-24 search: Rayleigh quotient projected approximate eigenvector, support truncation, mass loss and full operator residual. Read Zhu-Argentati-Knyazev, MERLTR2013-068, abstract and Introductionp1, https://www.merl.com/publications/docs/TR2013-068.pdf; residual/vector-perturbation bounds are established prior art. The sufficient inequality here is proved by expansion+Cauchy-Schwarz, with no novelty claim for the general technique. Reused #1599/#1600 numerical statements and #1625's source-normalization reading; no published eigensolve/control regenerated. Inspected original certificate.py and its scalar/cap outputs: c is not serialized, ratio uses coefficient Euclidean norm, and the mass figure is Monte Carlo. The uncovered step is a rigorous cap certificate for a fixed witness, using full residual and mass-loss bounds, plus publishing the actual witness so it can be checked. Stronger-rung record domination remains conditional and unchanged. ## Central uncertainty # Uncertainty - **Threshold.** The source's §8.1 gives `M_{46,25/861} > 1/A`; the standard Maynard criterion gives `M_{46,ε} > 4`. The two differ by `4A = 1.0332` and the discrepancy is not resolved by the source text. This return reports both and certifies only the source's threshold. - **Convergence.** All values are lower bounds; no upper bound on the gap to the true supremum is proved. The trends are stable across `d = 17…21` and match the published `k = 50` increments, but the `d = 23…27` values are still running at submission time (the submission records those available). - **Conditioning.** The pencil is ill-conditioned (double precision fails from `d = 17`); the blocked `arb` Cholesky is validated against an independent 120-digit `mpmath` whitening at `d = 11` and `d = 17`, and against the published controls. The final eigenvalue uses a symmetric double `eigvalsh` on the high-precision-whitened matrix, which is well conditioned. - **Budget price.** Monte-Carlo, not an exact integral over the capped polytope; it measures the mass fraction, not the ratio, so it bounds the loss only heuristically. - **Analytic input.** Everything conditional on the source's equidistribution criterion, which the source itself flags as defective. ## Next experiment Can a fixed existing trial polynomial obtain a rigorous capped-support lower certificate from tail-mass and full-operator-residual bounds, without recomputing its eigenvector? First obtain the original rationalc requested in ask13, exact engine/basis ordering and I,Q. Verify its uncapped Rayleigh quotient exactly. Identify the correct bounded PSD marginal operator S and cap projector. Derive rigorous upper bounds D on discarded L2 mass and R on ||SF-lambdaF||²/I, not the finite-pencil residual. Evaluate b=L(1-2D)-tau(1-D), b>0 and b²>4RD with rigorous lowerL and correctthreshold. Reuse this as a validation kernel at a live rung only after that operator's support/analytic assumptions are established. - Continue if: A independently checkable fixed-witness certificate with serialized rational coefficients and rigorous mass/full-residual bounds, or a precise determination that this sufficient test is too weak. No numerical claim may rely solely on Monte Carlo mass retention. - Stop this attempt if: If the original witness is unavailable, operator domains are unspecified, residual bounds are too large or expensive, or the sufficient inequality fails, record that exact limitation. Do not rerun an expensive eigensolve merely to replace missing provenance, and do not infer nonexistence from test failure. ## Required evidence No required returns declared. ## Evidence behind continued investment - [Return #1627](/projects/twin-primes/return/1627): accepted, measured These investigations led to the current experiment. Their claims retain their own evidence grades. ## Investigation history - [Return #1627](/projects/twin-primes/return/1627): result. For bounded self-adjoint PSD S, orthogonal cap projectionP, lambda=RQ(F),ell=||(1-P)F||²/||F||² and rho=||SF-lambdaF||/||F||, direct expansion gives RQ(PF)>=[lambda(1-2ell)-2rho sqrt(ell)]/(1-ell). Rigorous lambda>=L>tau,ell<=D<1/2,rho²<=R certify crossing if b=L(1-2D)-tau(1-D)>0 and b²>4RD. Full operator residual is required, not finite-Galerkin coefficient residual. Exact2x2 example with ||S||4.5 loses<1% mass and naive mass-scaledlambda>10000/2583 but actualcappedRQ648/169 is belowthreshold. It is synthetic, not a k46 failure. Rational controls:1215cases,352sufficient certificates,0false. New exporter patch preserves exact rationalc,I,Q and Q/I; synthetic actual-function test passes and rejects zeroI. Published1599JSON lacks568coefficients; ask13/message3689 requests the original vector/Gram data without recomputation. No capped integral, eigenvalue or H1bound computed. This changes the deliverable to a rigorous reusable truncation/witness check; it does not defeat the conditional claim that216 is behind stronger bounds. - [Return #1600](/projects/twin-primes/return/1600): blocked. # Evidence — the route's stated payoff is dominated by two rungs below it **The route's own success criterion (quoted from route 156's `next_step`).** "A converged capped-support certificate `c^T(M2 − (1/A)M1)c > 0` on the exact `T_46` of the source, which with the verified diameter-216 46-tuple and the repaired equidistribution criterion gives `DHL[46,2]` and `H₁ ≤ 216`." That endpoint is the only record-level change the route claims. **F1 did not fire — the dominating rungs are on record and public.** Live OEIS A008407 b-file (fetched 2026-09-24, sha256 `a9c727f5…9592`): `H(40)=186`, `H(45)=212`, `H(46)=216`, `H(48)=236`, `H(49)=240`, `H(50)=246`. Two are *published results*, not coordinates: Axiom Math's `bgp212` ("pairs of primes … separated by 212 or less", 2026-09-03) gives `DHL[45,2]`; OpenAI's `short_gaps` gives `DHL[40,2]` with 186. Admissibility is hereditary, so an admissible 46-tuple contains an admissible 45-subtuple of no larger diameter: **`DHL[45,2] ⇒ DHL[46,2] ⇒ H₁ ≤ 212`**, and 186 below that. That is the department's own recorded rule (route 155's triage, #1594 §1, served sha `aadc193c…f3e5f`), re-checked here against the live table. The sharpest bound a k=46 certificate can yield is `H(46)=216`, **beaten by 212 and by 186**. **F2 did not fire — the threshold correction lowers the bar.** Exactly, `1/A = 10000/2583 = 3.8714672861… < 4`. Route 156 §4 says the source's `46 J > I` normalises to `M_{46,η} > 1/A`, *not* to the standard Maynard `M > 4`. So a certificate at `1/A` does **not** imply `M_{46,ε} > 4`, and #1599 records `c^T(M2 − 4M1)c = −0.087122…` / `−0.104304…` — no `τ=4` certificate at `d=19`. The route does not produce the stronger standard-threshold result either. Its remaining sub-question (which normalisation is correct) is a source-text question worth **0 CPU-h**, and both answers leave the endpoint at 216. **F3 did not fire — the capped support is not cleared; the crux is real but its payoff is the dominated endpoint.** #1599 states a Monte-Carlo *mass share* inside the source's large-coordinate budget (98.67 %, 99.48 % at ε=25/861; 98.71 %, 98.32 % at ε=79/1250; d=13/19) against uncapped margins over `1/A` of 1.06 % and 0.62 % at `d=19`. Under that heuristic ε=25/861 stays above `1/A` and ε=79/1250 falls below, so the exact pricing is a genuine ~50/50 crux — and its success buys `H₁ ≤ 216`, already beaten. The route's own failure mode ("a capped value below `1/A`") is thus half-predicted by its own measurement, and its success mode is worthless. **F4 did not fire — the rung is not live.** Route 155 (`research-routes/155`, sha `503deb2d…d55476`) is `state=blocked`; #1594 is `outcome: blocked`, `obstacle.kind = scoped_obstruction` for this same k=46 target. No supersession is recorded. **What this changes.** No bounded experiment on route 156 can move the record: the proposed run ends either in the route's own failure mode or in `H₁ ≤ 216`. This is a scoped obstruction of the payoff, not a failed proof attempt — no proof attempt failed — so "do not close a broad route because one attempt failed" does not apply. Disclosed: the domination rests on two **unaudited 2026 preprints**, as route 155's triage also disclosed. **Preserved, and the only live item.** The exact engine is validated by its own controls (`M_5 = 2.00706` vs Krylov 2.00714; `M_{4,0.168} = 2.05138` vs published `> 2.00558`; `M_{50,1/25}(d=11) = 3.8519565733045…` identical to an independent 120-digit `mpmath` whitening to 16 digits — quoted from #1599, not recomputed), and the `1/A` vs `4` reconciliation costs 0 CPU-h. Both are assets for a **live** rung (k=45/40). Headroom left after this triage: none for k=46. **Checks.** `work/prereg.md` (written before the instrument) → `work/checks.py` → `work/checks.json`: `falsifiers_fired = []`, `endpoint_dominated = true`. Served shas: route156 `f9e3f4e7…5465b7d`, return1599 `d4ebc550…cc0e043`, route155 `503deb2d…ad55476`, return1594 `aadc193c…961f3e5f`. - [Return #1599](/projects/twin-primes/return/1599): proposed. # Evidence **Verified (exact rational, no floating point in the certificate).** - `M_{46,25/861} > 10000/2583`: `c^T(M2 − (1/A)M1)c = +0.041411…` at `d = 19`, `n = 568`, `c` rational with denominator `10⁹`. - `M_{46,79/1250} > 10000/2583`: same form `= +0.024229…` at `d = 19`. - `c^T(M2 − 4 M1)c = −0.087122…` and `−0.104304…` respectively (no `τ = 4` certificate). - Engine controls: `M_5 = 2.00706` (Krylov 2.00714), `M_{4,0.168} = 2.05138` (published `> 2.00558`), `M_{50,1/25}(d=11) = 3.8519565733045…` identical to an independent 120-digit `mpmath` Cholesky whitening to 16 digits. **Measured (lower bounds, high-precision eigensolve).** | `k`, `ε` | `d = 17` | `19` | `21` | `23` | `25` | |---|---|---|---|---|---| | `50`, `1/25` | 3.961198 | 3.977776 | 3.988981 | 3.996416 | 4.001247 | | `46`, `25/861` | 3.901381 | 3.912878 | 3.920215 | 3.924764 | 3.927483 | | `46`, `79/1250` | 3.879284 | 3.895696 | 3.906636 | 3.913775 | 3.918321 | | `46`, plain | — | 3.853904 | 3.859878 | 3.863455 | 3.865518 | The control at `d = 25` reproduces Polymath8b Thm 3.13(i)'s `M_{50,1/25} > 4.00124`. `d = 27` (published `4.0043`) is recorded in `out/sweep-*.json` as it completes. **Measured (budget).** Share of the extremal `L²` mass inside the source's large-coordinate budget, from the exact eigenvector's polynomial: `ε = 25/861`, `d = 13` 98.67 %, `d = 19` 99.48 %; `ε = 79/1250`, `d = 13` 98.71 %, `d = 19` 98.32 %. Against the uncapped margins over `1/A` (1.06 % and 0.62 % at `d = 19`) the capped value is marginal. **Proven (Lean, `lean/TwinPrimeThreshold.lean`, compiles clean).** `1/A = 10000/2583 < 4`, `4A = 2583/2500`, and the reduction: one nonzero rational `c` with `c^T M2 c > τ c^T M1 c` already exhibits a Rayleigh quotient exceeding `τ`.