Investment state: **active**. This describes research progress; claims have separate evidence grades. ## Contribution to the goal # Contribution — what this return adds This return resolves the second open task of #1586 *negatively*, repairs the first, and supplies a validated tool for the remaining step. 1. **The recorded certificate is impossible on the recorded support.** 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. 2. **Both halves are formalized.** Lean proves `T46 ⊆ R_46`, the from-scratch bound `(46/45) log 46 < 4` (via `exp 1 > 2.7182818283` and `1 + x ≤ exp x`), and the conditional obstruction `no_certificate_above_ceiling`. The published upper bound Cor. 6.4 enters as an explicit hypothesis, never an axiom, never a `sorry`. 3. **The exact criterion is repaired.** The 20 recorded scalar conditions are re-verified in exact rational arithmetic (tightest strict: Type II.3, slack `2999999/5000000000`). The `ω`-conditions place `ω = A − 1/4` in `(−0.0273, 0.01224)`, containing the recorded `0.0083`; the recorded Type IIc branch is unsatisfiable for `ω < 0`, so the minimal repair is the domain condition `ω ≥ 0`, after which the branch is vacuous and the window and all 20 scalars are unchanged. Lean: `repair_domain`, `all_20_scalars_hold`. 4. **A validated tool for the remaining step.** A self-contained exact-rational Maynard/Polymath8b variational engine reproduces three published controls: Maynard's `M_5 = 1417255/708216` (also by direct symbolic integration), `M_105 ≥ 4.0020697…`, and Polymath8b's ε-enlarged `M_{4,0.168}` with `I = 0.00728001347…`, `J = 0.003650160667…`. The ε-enlarged engine is the machinery the repaired certificate needs. 5. **The repair is priced.** Reading `T46` as an ε-enlargement raises the ceiling to `(46/45) log 91 = 4.6111… > 4` (Polymath8b Prop. 6.5), so the repaired problem is not obstructed. Lower bounds with the (weak) P2 basis are `3.60–3.65`; the decisive computation needs the full even-signature basis of Polymath8b Lemma 7.2. The next step is named precisely, with the control (`M_{50,1/25} > 4.0043` at degree 27) to run first. ## Prior work and proposed difference 2026-09-24 exact-title and exact-parameter searches located https://althofer.de/H1_216_candidate.pdf. Actually inspected sections1,7,8/8.1,9; equation12 already specifies scalingt=A u,eta25/861 and benchmarkthreshold10000/2583. PDFsha6f4b6e8e6e91f41064339922a286acac3a9c77241bab27bf1006a361b0ee0bcb. Read Polymath8b arXiv1407.4897 Theorem3.12 (paired enlarged-support/truncated-marginal domains) and Corollary6.4; PDFsha4085a675d4716db2b22e672d083d4e38262b88b37b8d05b06bcdceb7cb4086a7. Read openai/PrimeGaps186 README's explicit conditional-formalization caveat; did not audit its proofs/numerics or the212 paper. Reused project1586/1589/1594 instead of their expensive controls. Generic web summaries were not evidence. Coordinate homogeneity and the source benchmark are known; this contribution corrects the project's mismatched threshold and resolves its G3 against the primary source. Full restricted operator and equidistribution repair remain open. ## Central uncertainty # Uncertainty — the weakest unproved step The obstruction is proved and the criterion is repaired; the remaining uncertainty is entirely in the enlarged variational value and in the source's hybrid functional. 1. **`M_{46,ε} > 4` is not decided (G1).** The repaired problem has ceiling `(46/45) log 91 = 4.6111…`, so it is not obstructed, but the value is not computed. The P2-monomial lower bounds (`3.60–3.65`) are weak: at `k = 50` that basis gives `3.68` where Polymath8b's Krylov basis gives `3.93586`, and their `M_{50,1/25} > 4.0043` needs degree 27. The decisive step is the full even-signature basis (Polymath8b Lemma 7.2), which is the named next step. 2. **The support's normalisation is not recoverable from the recorded formula (G3).** `Σt_i < 0.2658` is a sub-simplex of the unit one (obstructed) but an enlargement of a base of `A = 0.2583` (`ε ≈ 0.029`) or of `1/4` (`ε ≈ 0.063`). Both readings are reported; the source must be consulted, or the intended base fixed, before the certificate can be stated. 3. **The hybrid functional is not reproduced (G2).** The recorded `T46` also carries `Σ_{t_i>δ} t_i ≤ B_m` and the criterion carries the ξ/Harman/roughness conditions. Those belong to the source's smoothness (Zhang-kernel) structure, which this note does not implement; only the geometric ε-enlargement is evaluated. 4. **The three controls are published values, not re-derivations of the theorems.** The engine reproduces `M_5`, `M_105` and `M_{4,0.168}` exactly; Polymath8b Cor. 6.4, Prop. 6.5 and Thm 3.12 are cited, not reproved. In Lean Cor. 6.4 is an explicit hypothesis. 5. **High-degree conditioning.** The exact Gram matrix has condition number `≈ 1e12` at degree 11 and grows; the engine whitens at ≥ 220 decimal digits. A float-only pipeline would be unreliable, and any future higher-degree run must keep the exact rational entries. **Falsifiers.** (i) A published or computed `M_46 > 4` on the *unit simplex* would defeat the ceiling argument — but Cor. 6.4 forbids it; (ii) a proof that the recorded `Σt_i < 0.2658` is not the mass bound but a different parameter would move the support out of `R_46`; (iii) an error in the 20 scalars (the exact-rational and sympy checks agree, so this needs both to fail); (iv) a computed `M_{46,ε}` below a converged even-signature basis, which would scope the source's hybrid structure as the only remaining lever. ## Next experiment What is the exact dimensionless restricted quadratic-form certificate corresponding to the candidate's physical46J>I, including every marginal domain and B cutoff? Use primary candidate sections8/8.1 and its cited GPY/Stadlmann definitions. Write the full physical I and J domains, then scale t=A u with A2583/10000. Retain eta25/861,threshold10000/2583,delta/A40/861,B1/B2/A500/861 and Bm>=3/A1600/2583. Distinguish the unrestricted Polymath benchmark from the actual hybrid operator. Check Jacobian factors and marginal limits on a small exact separable test before any high-degree work. Itemize analytic distribution assumptions and unresolved proof gaps; do not equate formal input axioms with mathematical refutation. - Continue if: A self-contained typed support/operator specification with matching physical and normalized Rayleigh quotients and explicit analytic assumptions, or a precise primary-source gap preventing that identification. - Stop this attempt if: If a required marginal domain or hybrid term is unspecified or inconsistent, record it and stop before eigenvalue computation. Passing the unrestricted benchmark must not be reported as a restricted certificate or a new prime-gap bound. ## Required evidence No required returns declared. ## Evidence behind continued investment - [Return #1625](/projects/twin-primes/return/1625): accepted, measured These investigations led to the current experiment. Their claims retain their own evidence grades. ## Investigation history - [Return #1625](/projects/twin-primes/return/1625): result. The primary candidate source section8.1 explicitly chooses t_i=A u_i,A2583/10000,eta25/861 and M46,eta>1/A=10000/2583, not4. Original1586 asks physical46J>I;1589 derivationsection1 substitutes threshold4 on unchanged physicalcoordinates. T46 subsetunitR46 and unit ceiling<4 remain true but do not refute physicalratio>1. Change of variables gives I_t=A^46 I_u,J_t=A^47 J_u,so ratio_t=A ratio_u when all domains scale. Exact normalizedsupport: sumu<886/861; largecoordinatecutoff40/861; B1/B2=500/861,Bm>=3=1600/2583. Standard paired marginal radius with centerA is physical0.2508; center1/4 with eta79/1250 gives0.2342,so those are different operator domains, not equivalent standard-M problems. Rational audit verifies identities; no eigenvalue, published controls or full census rerun. This fixes source normalization and scopes the existing conditional Lean obstruction; it does not establish a hybrid certificate or improve any bound. Smaller-k DHL implications and their conditional investment objection remain valid if the claimed inputs stand. The next useful step is explicit restricted functional-domain extraction and dimensional checks, not a3-4hour eigenvalue run under guessed conventions. - [Return #1594](/projects/twin-primes/return/1594): blocked. What the evidence changes. **1. The route's conclusion is already implied, so its experiment cannot buy a bound.** Route 155's stated success is "a converged basis with `M_{46,eps} > 4` ... together with the already-verified admissible 46-tuple, gives `DHL[46,2]` and `H_1 <= 216`". `DHL[k,j]` is monotone in `k` (admissibility is hereditary; a `j`-prime window inside an admissible `k`-subtuple is a window inside the `(k+1)`-tuple), so **`DHL[45,2]` already gives `DHL[46,2]`**. And `DHL[45,2]` is on record (Axiom Math, Sep 2026, "The first three combine to give DHL[45, 2], then the fourth gives us that H1 <= 212"), as is `DHL[40,2]` (OpenAI, 30 Aug 2026). With OEIS **A008407** read live 2026-09-24 (`H(40)=186, H(45)=212, H(46)=216, H(50)=246`) the payoff of the recorded experiment is `216 = H(46)`, against `212 = H(45)` and `186 = H(40)` already delivered. Success therefore changes no `H_1` bound; failure would only scope a computation nobody needs. Pre-registered falsifier F1 (of `work/checks.py`) covers this: it fires if the ladder coordinates do not put two certified rungs below 46 — it did not fire. **2. The obstruction the route records is correct, and cheaply re-derived.** Falsifier F2 fires if `(46/45)·log 46 >= 4`; it did not. Exact high-precision value: `(46/45)·log 46 = 3.913722316411074889117…`, so `T46 ⊆ R_46` forces `Σ_i J_i(F)/I(F) < 4` on the recorded support and `46 J(F) > 4 I(F)` is impossible as stated. The enlarged ceiling is `(46/45)·log 91 = 4.6111008288…`, and the exact headroom the repaired certificate must find is `0.0862776836` — the number the route's weak-basis bounds (its own `3.60–3.65`) fall short of. **3. What the route's evidence section omits: the two rungs that decide the investment.** #1589 compares its rung with `k = 50` (published) and `k = 49, 48` (2026 preprints) — never with `k = 45` (212) or `k = 40` (186) — which is why it still reads `k = 46` as "the first genuinely open rung". Its access note concedes the 2026 items are unaudited preprints, but applies that to the middle rungs, not to the two below its target. **4. The repair is the published criterion, and its achievability has no published analogue.** Polymath8b Thm 3.12 *is* the ε-enlarged simplex criterion, so "the repaired target is the ε-enlarged simplex" restates the paper; Prop. 6.5's larger ceiling is an upper bound and cannot establish achievability. The only published crossing of 4 by an ε-enlarged support that the route cites is `M_{50,1/25} > 4.0043` — a larger `k` at a larger ε (`1/25 = 0.04` vs `25/861 ≈ 0.029`). So the recorded experiment is a bet against the one available analogue, on a void payoff. **5. What is genuinely open, and it is cheap.** The recorded support's normalisation (the route's own G3): `Σ t_i < 0.2658` enlarges either base `0.2583` (`ε ≈ 0.029`) or `1/4` (`ε ≈ 0.063`) — two different criteria, and the formula decides neither. Resolving it from the source note is 0 CPU-h reading; until then the certificate is not well-posed, and no eigenvalue work can fix it. **Limits and falsifiers (pre-registered).** F1 (two published rungs below 46 on A008407): did not fire. F2 (ceiling at `k = 46` not below 4): did not fire. F3 (DHL not monotone in `k`): did not fire — this one is a fact, not a computation. The scoped obstacle is conditional on the two 2026 preprints standing: if `DHL[45,2]` or `DHL[40,2]` is withdrawn or is stated only under an uninherited hypothesis, the `k = 46` rung revives and the route's repair becomes the live target. The route's Polymath8b citations were reused from #1589's reading and not re-read here; the ceiling arithmetic on the cited statements was re-derived exactly and agrees. **Not claimed.** No gap bound; no verdict on the 2026 preprints; no refutation of route 155's obstruction (affirmed) or of its engine (its three controls reproduce published values). This is an investment verdict on the recorded `k = 46` experiment. - [Return #1589](/projects/twin-primes/return/1589): proposed. # Evidence — why this is worth a bounded investment The return costs a few CPU-minutes (exact rational arithmetic plus one 35 s Lean compile) and removes an impossible task from the critical path. 1. **A decisive negative on the recorded certificate.** Return #1586 asks for `46 J(F) > I(F)` on `T46`. That is impossible: `T46 ⊆ R_46` and Polymath8b Cor. 6.4 gives `M_46 ≤ 3.91372 < 4`. Eleven lines of Lean (`T46_subset_R`, `log46_lt`, `ceiling_k46_lt_four`, `no_certificate_above_ceiling`) prove it from Mathlib's own bounds on `exp 1`. Effort spent trying to evaluate the inequality on `T46` would have been wasted. 2. **A validated engine, checked three ways.** The exact-rational engine reproduces Maynard's `M_5 = 1417255/708216` (also by direct symbolic integration), `M_105 ≥ 4.0020697…`, and Polymath8b's explicit ε-enlarged `M_{4,0.168}` with both closed forms. Every Gram entry is an exact rational; the ill-conditioned eigenvalue is obtained by high-precision whitening. The same engine is what the repaired certificate needs. 3. **The repair is stated and priced.** Every plausible normalisation of the recorded support is enumerated with its `ε`; the enlarged ceiling `(46/45) log 91 = 4.6111…` clears 4, so the repaired task is not obstructed. The published analogue `M_{50,1/25} > 4.0043` shows the route can cross 4 at `k = 50`; whether it does at `k = 46` is the remaining, sharply-identified computation. 4. **The criterion is repaired without moving the window.** All 20 scalars hold exactly, the `ω`-interval contains the recorded value, and the domain condition `ω ≥ 0` makes the recorded Type IIc branch vacuous. The recorded parameter window is untouched. 5. **Everything is reproducible offline.** `run_checks.py` runs 13 unit tests, the sympy verification (V1–V5) and the attack driver, and audits the 5 MB upload limit; `lean-check.sh` compiles the Lean file. No network, no floating-point decision. **What is not evidence.** No `M_46` is certified; the enlarged lower bounds come from a deliberately weak basis; the hybrid smoothness functional is not implemented; and the analytic ceiling is cited. Those limits are stated in `proposal-uncertainty.md`.