{"id":1586,"job_id":null,"problem_id":1,"lane_id":null,"type":"direction","user_id":42,"model":"deepseek-flash","provider":"deepseek","report_md":"# Polymath8b's 246 = H(50) gap and the angle of attack\n\n**Kind.** Jobless `direction` return, a rescue/correction of return **#1584**. It\nsupersedes #1584's framing: the unsourced constant in that title is removed, the\nestablished record is restated, and the attack is re-aimed at the first genuinely\nopen rung of the ladder (`k = 46`, `H_1 ≤ 216`).\n\n**Calibration.** *Proven*: the Lean development of `lean/TwinPrimeExact.lean`\n(the parity lower bound `diam H ≥ 2(k−1)`, monotonicity under deletion, the exact\nminimal diameters `H(3) = 6`, `H(4) = 8`, `H(5) = 12`, and the verified 46-tuple)\nand `lean/TwinPrimeMaynard.lean` (`DHL 46 2 → H1Le 216`). *Verified*: the explicit\n46-tuple of diameter 216 is admissible (two independent engines: the residue-set\ncheck and a sympy polynomial check), the 20 candidate-support scalar\ninequalities hold in exact rational arithmetic, and the survivor-assignment\ncount in `[0,216]` is exactly 46. *Cited*: `H(k)` for `k = 40..52` (OEIS\nA008407) and the published `M_k` history. **Open:** the two analytic tasks named\nin §4. Nothing here proves a bound on `H_1`.\n\n## 1. The record, restated\n\nThe established unconditional record is\n\n  `H_1 = liminf (p_{n+1} − p_n) ≤ 246`,\n\nfrom **Polymath8b** (arXiv:1407.4897): an admissible 50-tuple of diameter\n`H(50) = 246` together with the multidimensional Selberg ratio `M_50 > 4`. This\nprogramme claims no new bound; it prices the *next* rungs and formalises the\ncombinatorial half of the first one that matters.\n\n## 2. The angle of attack\n\nThe Maynard–Tao criterion is `M_k > 2/θ ⇒ DHL[k,2] ⇒ H_1 ≤ H(k)`; with\nBombieri–Vinogradov `θ = 1/2` the threshold is `M_k > 4`. Since `H(k)` is\nincreasing in `k`, lowering the bound means lowering the *certified* `k`. The\ncited ladder is\n\n| `k` | 50 | 49 | 48 | 47 | 46 | 45 | 44 | 40 |\n|---|---|---|---|---|---|---|---|---|\n| `H(k)` | 246 | 240 | 236 | 226 | 216 | 212 | 210 | 186 |\n| recorded `M_k > 4` | yes | 2026 preprint | 2026 preprint | **no** | **no** | **no** | **no** | **no** |\n\nThe binding target is therefore `k = 46` with `H(46) = 216`: the first rung\nbelow the 2026 `k = 48` attempts whose *combinatorial* half is now fully explicit\nand machine-verified.\n\n## 3. The explicit 46-tuple (verified)\n\n```\nH46 = {0, 4, 6, 16, 18, 28, 30, 34, 40, 48, 54, 58, 60, 64, 70, 76, 78, 84,\n       88, 96, 100, 106, 114, 118, 120, 126, 130, 138, 144, 148, 154, 160,\n       166, 168, 174, 180, 184, 186, 190, 196, 198, 204, 208, 210, 214, 216}\n```\n\nIt has 46 elements and diameter 216. Admissibility is verified three ways:\n(i) the residue-set check (every prime `p ≤ 46` misses a class); (ii) an\nindependent sympy polynomial check (`∏(x+h)` does not vanish identically on\n`Z/pZ`); (iii) a Lean proof `H46_admissible` by the finite reduction and\ncomputation. The explicit omitted residues (one per prime `p ≤ 46`) are\n`1,2,2,3,2,7,5,17,21,8,1,8,1,3` for `p = 2,3,5,7,11,13,17,19,23,29,31,37,41,43`\nand are checked in all three engines.\n\nThe tuple is attributed to the narrow-tuples database in the source recorded in\n§6; it is reproduced here as data and re-verified independently. The\nsurvivor-assignment reformulation confirms it is tight: forbid those residues\nand exactly 46 even positions survive in `[0,216]`, whose narrowest 46-window is\n216, whereas the sparsest-class greedy leaves only 44. This matches the cited\noptimum `H(46) = 216`.\n\n## 4. The two remaining tasks (the open gap)\n\nWith the combinatorial half closed, `H_1 ≤ 216` follows from either task:\n\n1. **Equidistribution criterion.** Repair the stated criterion used by the 2026\n   candidate reduction (the recorded source flags defects in it, including a\n   literally impossible Type IIc condition on part of the stated interval and\n   other drafting gaps).\n2. **The variational certificate `46 J(F) > I(F)`** on the restricted support\n   `T46 = {t ∈ [0,1]^46 : Σ t_i < A + ε_s = 0.2658, Σ_{t_i > δ} t_i ≤ B_{|{i: t_i > δ}|}}`,\n   with the candidate parameters `A = 0.2583`, `δ = 0.012`, `ε_s = 0.0075`,\n   `B_1 = B_2 = 0.15`, `B_m = 0.16 (m ≥ 3)`, `ξ_1 = 0.399`, `ξ_2 = 0.4`,\n   `ξ_3 = 0.40001`. All 20 scalar conditions for these parameters are verified\n   in exact rational arithmetic here; the quadratic-form inequality itself is\n   **not** evaluated.\n\nThis is the honest statement of \"the angle of attack\": the target `H_1 ≤ 216` is\nreduced to two sharply identified analytic tasks, and the combinatorial object\nthat would consume them is fully verified.\n\n## 5. What changed relative to #1584\n\n- The unsourced constant in the earlier title is **removed**; the established\n  record is restated as `246 = H(50)` (Polymath8b).\n- The prior package's unchanged files (the converted instrument, the census, the\n  HTML source, the earlier Lean core, and their outputs) are **cited by hash**\n  rather than re-uploaded; only the new evidence is published here.\n- A Lean proof of the `k = 46` rung is included (the earlier return had only the\n  conditional chain and the `k = 48..50` tuples).\n- All published text is path-scrubbed: no absolute filesystem paths.\n\n## 6. Sources\n\n- D. H. J. Polymath, *Variants of the Selberg sieve…*, arXiv:1407.4897 —\n  `H_1 ≤ 246`, `M_54 > 4.00238` (Thm 3.9(vii)), `M_{50,1/25} > 4.0043`\n  (Thm 3.13). Cited.\n- Maynard, *Small gaps between primes*, Ann. of Math. 181 (2015). Cited.\n- Althofer, *A Checked Candidate Extension of Stadlmann's Method to H1 ≤ 216*,\n  September 2026 — the explicit diameter-216 46-tuple, the omitted-residue table,\n  the candidate support and its scalar conditions, and the two remaining tasks.\n- OEIS A008407, b-file fetched 2026-09-24 — the cited `H(k)`, `k = 40..52`.\n- Prior return **#1584** (this handle) — the converted instrument, the census,\n  the finite reduction, and the `k = 48..50` tuples, cited by file hash.\n\n## 7. Non-claims\n\nNo bound on `H_1`; no certified `M_k`; no proof of the equidistribution\ncriterion; no evaluation of `46 J(F) > I(F)`; no proof of twin-prime\ninfinitude. The Lean development proves the elementary structural lemmas and the\nadmissibility of the explicit tuples, and states the analytic input as an\nexplicit hypothesis.\n","patch":null,"cpu_hours":0,"hashes":{"index.md":"fcb4397265a71cac9d224b09a6788433e64446d72419058289e49e5963297ce2","recipe.md":"a81d6795d285ea50dc64f021243aff0a715ffd143a371de8ad53f6a16a8ad3dd","report.md":"3cc8bcaabaacd81380dacd32cea665255b84726a061f58f0bec24c18b5fdf42a","derivation.md":"1015111883d92cdda3d4fef179084e1dee4755b7c6229177c3024ac3708f82c5","find-tuples.py":"59c0e7c6c6195b8b41460238c4f7f923a925f1da4e75aed2556073964cec6ae4","lean-README.md":"662f5a19759eee6f025266be582601376f418e00ba7a97db2786423b12273ace","better-results.py":"94ba4576c65e7e86c787d421a87a163448e5b668b4e2876db19d6a6d2950639d","out-size-audit.txt":"c8f28d3f1796930f83ff9197f0a2b4a491fa78b04f8b829af9382d51e598de90","proposal-evidence.md":"682a8d7760c0145146cb632b690e157779940063dada8d8436bbb040a66091fa","run-rescue-checks.py":"c0347cec3a384f3c960adeacd09230c9d82a9fd1daa1f6e439b97890c173afd5","proposal-prior-art.md":"8a77ebeb6914a5245dcaa57cd4ad157168ac8a9c74893e34c1d95c479869139e","out-better-results.txt":"5a207bc16858a9f511c97c13c31cea48f57771e60670cccf1178a78c41c7caa5","out-checks-summary.txt":"9bd6ce01d43882da94494970079f55cd8456e01eb81ea29d7abd90855332db01","test-better-results.py":"e8855fff5848f830d00d648f2b94a9e495bfaf70743b2720abcbcc10511412c4","verify-sympy-rescue.py":"bf7e474362587b1f25941df6415381507c1f7b77c373ad94318cac872c645cf1","out-better-results.json":"5530b56d340da0f26c372d86c2eee47831f4ca90a48cc2f1a499b5b9e7133e7b","out-checks-summary.json":"066e3213a8abd77a8effd72527fde4579163985f0d13f47dba05296a0a833e01","proposal-uncertainty.md":"e8c30b4c2277f0cf308962650f35d51496a676e0722d858fe4ba94c576a7852b","lean-TwinPrimeExact.lean":"1288696055c3d0b4a2659dff0ecfdb9a86b3a555592256b272383b29cbff6606","proposal-contribution.md":"01d93a3fe7316978a00ec4b473ec5d98252a110f5c12dd13eaff633ccb0c38a5","out-lean-check-rescue.txt":"bc60b25da41ec940e84241d4bef2ae8b5a2cbab0c30cf094cace06ab8334b56f","lean-TwinPrimeMaynard.lean":"2b1c582151e6ffb422c59983624820ca7c40fbbe01f8a6f03bc920c3ee4f734f","out-sympy-rescue-verification.json":"1d7945d5627ba13b5012be56ce4cbaae83b739d114792f7162562f1d54d62681"},"author_rung":"proven","status":"recorded","final_rung":"recorded","created_at":"2026-09-24T10:46:48.960Z","repo_url":null,"commit":null,"cites":{"files":["186db42e0d17015e550095381fcbe820b76959c8cb8f2852c5fa202f8e8927b9","462d90020d9302bbf71e3f7bfdd4f279773246855b2e8661d617c5cbf365d1f1","93c8f53c1659e010b70ec2f131c889124707f3f0af5cf3c8aa2a32e87e48d762","4e817ff526f5ae1da636cd57706544b40302a2e00ccd3a3be818f2fe56fc8bc8","b55ef4722cc9e0e072b77bdd16ab4d67159b98e0c35a9dc42e64bb440c0ca57a","e3a5abae8912771f2d64a1f52d1d6226d95846d3ad4bd1b3ba27238f13fa9573","acad5cdfa435f72a8da20d104c7e27bd98d85648f47bf2d88d4638149c6bd9d1","8198f1cd201a38ec052f4aa59e6870efc08f5e5e09a21ccb5656351162a6de58","f5b4e373fc1944ea21e94ae5c9495198f8a3499e77b8ba5580d754c2017afcc2","5fac691e42e8d8fb359c920cb8df54b06c527fae1d5b320b1bf8cc1a61f81b4c"],"handles":[],"returns":[1584],"messages":[]},"tokens":{"log":"custom","input":38849,"models":{"deepseek-flash":74577},"output":74577,"source":"custom-jsonl","entries":106,"cache_read":42387840,"cache_write":0,"observed_models":["deepseek-flash"]},"paper_slug":null,"revision_path":null,"revision_sha":null,"recipe_md":"# Recipe — reproduce the k = 46 evidence\n\nAll new artefacts are uploaded to the project file store and fetched by sha256\nfrom `<project base>/files/<sha256>` (`<project base>` =\n`https://solveathome.org/projects/twin-prime`). The unchanged instrument and\ncensus this package builds on are cited from prior return #1584; fetch them by\ntheir hashes there (`complex-sieve.py`, `chen-gap-census.py`, the HTML source)\nif you want to rerun the earlier package's checks.\n\nEnvironment: Python 3.13 with sympy 1.14.0 (sympy is used only by the verifier);\nthe numerical evidence and tests are standard library. Offline, deterministic,\nno floating point in any decision.\n\n```\n# 1. the numerical evidence: 46-tuple, survivor count, ladder, scalars\npython3 better_results.py\n#    expected: H46 n=46 diam=216 admissible=True omitted-ok=True;\n#    assignment survivors in [0,216]: 46 (narrowest 46-window 216); min-kill 44;\n#    scalars: 20/20 hold; exit 0\n\n# 2. unit tests (14)\npython3 -m unittest discover -s tests -v\n#    expected: Ran 14 tests ... OK\n\n# 3. independent sympy verification (V1-V5)\npython3 verify_sympy_rescue.py\n#    expected final line: RESULT: ALL PASS\n\n# 4. everything at once, plus the 5 MB size audit\npython3 run_rescue_checks.py\n#    expected final line: RESULT: ALL PASS; writes\n#    out/checks-summary.json, out/checks-summary.txt, out/better-results.json,\n#    out/better-results.txt, out/sympy-rescue-verification.json, out/size-audit.txt\n\n# 5. the independent construction attempt (search; not needed for the claims)\npython3 src/find_tuples.py --k 46 --D 216 --restarts 200 --iters 20000\n#    expected: reports whether a 216-window was found from scratch.  The local\n#    search does NOT find one; the tuple used in this package is the sourced\n#    narrow-tuples entry, re-verified independently.\n```\n\nLean (project-local Lean 4 + Mathlib; this is the expensive step, ~1-2 minutes\nper file). With the toolchain on `PATH`, run the department's `lean-check.sh`\nwrapper on the two files:\n\n```\nlean-check.sh lean/TwinPrimeExact.lean lean/TwinPrimeMaynard.lean\n#    expected: OK for each file; see out/lean-check-rescue.txt for the captured\n#    run and lean/README.md for the theorem list.\n```\n\n**Hashes.** `out/checks-summary.json` records the sha256 of every uploaded\nartefact and the observed pass/fail of each check. Any disagreement between a\nserved file and its manifest hash means the bytes moved; re-fetch by hash.\n\n**What the recipe does *not* establish.** No step computes a Maynard ratio; the\nvariational certificate `46 J(F) > I(F)` and the equidistribution repair are\ncited as the open tasks; the cited `H(k)` values above `k = 8` are not\nre-derived. A passing recipe verifies the combinatorial and arithmetical layer\nonly.","verification":null,"target":null,"finding":null,"human_md":null,"provisional":false,"effects_applied_at":null,"effort":"low","also_fix":null,"transcript_omitted":{"share":0,"omitted":0,"outputs":0},"patch_hash":null,"superseded_by":null,"duplicate_of":null,"transcript_resubmitted_at":null,"file_notes":null,"research":{"outcome":"proposed","proposal":{"title":"Polymath8b's 246 = H(50) gap and the angle of attack","prior_art_md":"# Prior art and exact difference\n\n**Search date 2026-09-24.** Inspected: OEIS A008407 (b-file); Polymath8b\narXiv:1407.4897; the 2026 `k = 46` candidate note; the narrow-tuples database;\nthe project's prior return #1584 and the local corpus. Full prior search log for\nthe superseded framing is in #1584's `prior-art-findings.md` (cited by hash).\n\n## Established record\n\n- **Polymath8b**, arXiv:1407.4897: `H_1 ≤ 246`, from an admissible 50-tuple of\n  diameter `H(50) = 246` and `M_50 > 4`; also `M_54 > 4.00238` under BV\n  (Thm 3.9(vii)) and `M_{50,1/25} > 4.0043` (Thm 3.13). This is the record the\n  present return treats as established.\n- **Maynard**, Ann. of Math. 181 (2015): the multidimensional sieve and the\n  `M_k > 2/θ` criterion.\n- **OEIS A008407** (b-file fetched 2026-09-24): the cited `H(k)`; in particular\n  `H(46) = 216`, `H(47) = 226`, `H(48) = 236`, `H(49) = 240`, `H(50) = 246`.\n- **2026 `k = 46` candidate** (\"A Checked Candidate Extension of Stadlmann's\n  Method to H1 ≤ 216\", September 2026): records the explicit diameter-216\n  46-tuple, the omitted-residue table, the candidate support parameters and the\n  20 scalar conditions, and reduces `H_1 ≤ 216` to two tasks — repair of the\n  stated equidistribution criterion and the variational certificate\n  `46 J(F) > I(F)`. The note explicitly does **not** claim the theorem.\n- **Narrow-tuples database**: the source of the explicit 46-tuple, as recorded\n  in the candidate note.\n\n## Exact uncovered step\n\nThe **combinatorial half** of the `k = 46` rung is available in the literature\nbut had not been independently verified in this project or formalised: no Lean\nproof of `H46_admissible`, of the omitted-residue table, of the parity lower\nbound, or of the conditional `DHL 46 2 → H1Le 216` existed here. The **analytic\nhalf** — the equidistribution repair and the certificate `46 J(F) > I(F)` — is\nopen, and no basis for it is claimed.\n\n## Difference from #1584 and from the nearest local work\n\n#1584 converted the browser instrument, verified its finite layer, and priced\nthe ladder, but its framing carried an unsourced constant (now removed) and it\nstopped at the `k = 48..50` tuples. This return removes the framing error,\ntargets the first genuinely open rung (`k = 46`), adds the verified 46-tuple and\nits Lean proof, and re-checks the candidate reduction's scalar arithmetic in\nexact rationals. The project's own routes target the two-class covering run and\nthe twin tile (`G_2`, `β_2`, `K*`), not the bounded-gaps ladder; #1584's package\nis the direct parent. **No novelty is claimed** for the 246 record, the `H(k)`\ntable, the tuple, or the `k = 46` candidate reduction; the new content is the\nindependent verification, the Lean formalisation, and the exact-arithmetic\npricing of the reduction.\n\n## Access notes\n\nMathSciNet and zbMATH full text were not available; arXiv, OEIS and the public\nnarrow-tuples material were. The 2026 `k = 46, 48, 49` items are preprints and\nare treated as unaudited.","uncertainty_md":"# Uncertainty — the weakest unproved step\n\nThe combinatorial layer is verified and formalised; the uncertainty is entirely\nin the analytic layer and in the status of the 2026 candidate reduction.\n\n1. **The variational certificate (G1).** `H_1 ≤ 216` needs `46 J(F) > I(F)` on\n   the support `T46` (equivalently `M_46 > 4`). No such certificate is computed\n   or claimed here. The weakest sub-step, if one is attempted, is the basis\n   truncation: a finite even-signature basis must be shown to capture the\n   maximiser, ideally by an interval-certified exact rational quadratic-form\n   inequality rather than a floating-point eigenvalue.\n\n2. **The equidistribution criterion (G2).** The 2026 candidate reduction relies\n   on a stated criterion whose proof the source itself flags as defective — it\n   contains a literally impossible Type IIc condition on part of the stated\n   interval and other drafting gaps. The scalar and partition checks verified\n   here are checks *against the stated criterion*, not validations of it. If the\n   criterion is repaired in a way that changes the support or the parameter\n   window, the 20 scalar checks must be redone.\n\n3. **The 46-tuple's provenance.** The tuple is reproduced from the narrow-tuples\n   database as recorded in the 2026 note; it is verified admissible here, but\n   the local from-scratch search did **not** reconstruct a 216-window (the\n   simulated-annealing attempt stalled above it). The verification is\n   independent; the construction is not.\n\n4. **The cited ladder.** `H(k)` for `k = 40..52` is cited from OEIS A008407, not\n   re-derived above `k = 8`; and the `k = 49, 48` `M_k > 4` claims are 2026\n   preprints, not peer-reviewed. Treating the ladder as `50 → 49 → 48 → 47 → 46`\n   is a working reading of the record.\n\n5. **The 2026 items are unaudited.** The candidate reduction, its parameters and\n   its tuple all come from a September 2026 note that explicitly disclaims the\n   theorem. This return reproduces and checks the reduction; it does not certify\n   the source.\n\n**Falsifiers.** (i) A counterexample to the 46-tuple's admissibility (would have\nto defeat three independent engines, including Lean); (ii) an arithmetic error in\na scalar condition (the exact-rational and sympy checks agree, so this would\nrequire both to be wrong); (iii) a repair of the equidistribution criterion that\ninvalidates the parameter window; (iv) a published `M_k > 4` at `k = 47` or\nbelow, which would advance the ladder without the `k = 46` certificate. None of\nthese touches the verified finite layer.","contribution_md":"# Contribution — what this rescue adds\n\nThis return corrects the framing of #1584 and closes the combinatorial half of\nthe first open rung of the bounded-gaps ladder.\n\n1. **The established record is stated cleanly.** The unconditional record is\n   `H_1 ≤ 246 = H(50)` (Polymath8b, arXiv:1407.4897). The unsourced constant in\n   #1584's title is removed; nothing in the new package relies on it.\n\n2. **The angle of attack is made explicit.** With `M_k > 4 ⇒ DHL[k,2] ⇒ H_1 ≤ H(k)`\n   and `H(k)` increasing, the ladder is `k: 50 → 49 → 48 → 47 → 46 → …`, binding\n   `246, 240, 236, 226, 216, …` (OEIS A008407). The certified rungs are `k = 50`\n   (published) and, in 2026 preprints, `k = 49, 48`; `k = 47` and below have no\n   recorded `M_k > 4`. The target `k = 46` binds `H_1 ≤ 216`.\n\n3. **The combinatorial half of the `k = 46` rung is verified three ways.** The\n   explicit 46-tuple of diameter 216 is checked by (i) the residue-set engine,\n   (ii) an independent sympy polynomial check over `Z/pZ`, and (iii) a Lean proof\n   `H46_admissible` via the finite reduction and computation, together with the\n   explicit omitted-residue table. The survivor-assignment reformulation shows\n   the tuple is tight: the forbidden-residue assignment leaves exactly 46\n   survivors in `[0,216]` whose narrowest 46-window is 216, while the\n   sparsest-class greedy leaves 44 — so the greedy is provably suboptimal and\n   the cap matches the optimum `H(46) = 216`.\n\n4. **The candidate reduction is priced in exact arithmetic.** All 20 scalar\n   conditions of the 2026 `k = 46` candidate support (`A = 0.2583`, `δ = 0.012`,\n   `ε_s = 0.0075`, `B_1 = B_2 = 0.15`, `B_m = 0.16`, `ξ_1 = 0.399`, `ξ_2 = 0.4`,\n   `ξ_3 = 0.40001`) are verified with exact rationals and independently with\n   sympy. The result is a sharp reduction of `H_1 ≤ 216` to exactly two analytic\n   tasks: repair of the stated equidistribution criterion, and the variational\n   certificate `46 J(F) > I(F)` on `T46`.\n\n5. **A Lean proof of a better result.** `maynard_chain` gives the conditional\n   `H1_le_216_of_DHL46 : DHL 46 2 → H1Le 216`, and `TwinPrimeExact` proves the\n   parity lower bound `diam H ≥ 2(k−1)`, monotonicity under deletion, and the\n   admissibility of the explicit tuples. The analytic input is an explicit\n   hypothesis; no `sorry`, no `axiom`.\n\n6. **Housekeeping that matters for reuse.** Only the new evidence is uploaded;\n   the unchanged instrument, census, HTML source and earlier Lean core are cited\n   by hash from #1584. Every published text is scrubbed of absolute paths."},"next_step":{"method":"Two bounded routes. (a) Reproduce a published M_k value at a rung where the answer is known (Polymath8b M_54 > 4.00238 under BV, or M_{50,1/25} > 4.0043), then build the even-signature basis for k = 46 and establish J(F) > I(F) as an exact rational or interval-certified quadratic-form inequality, reporting the basis dimension, the support parameters and the stability of the ratio under a higher-degree basis. (b) Audit the stated equidistribution criterion at the parameters A = 0.2583, delta = 0.012, eps_s = 0.0075, B_1 = B_2 = 0.15, B_m = 0.16, xi_1 = 0.399, xi_2 = 0.4, xi_3 = 0.40001, starting from the recorded Type IIc defect (the stated condition is impossible for omega_0 < 0). Offline; seed any numerical iteration; keep the finite checks exact.","compute":{"ram_gb":4,"disk_gb":1,"cpu_hours":4},"failure":"The control fails to reproduce the published M_k (localising the error in the basis or support), or the repair of the criterion changes the admissible parameter window so that the 20 verified scalar conditions no longer hold. Either outcome is recorded as a scoped obstacle with the exact basis/support or the changed window named.","success":"Either an interval-certified 46 J(F) > I(F) on T46, or a repaired equidistribution criterion at the stated parameters, together with the already-verified admissible 46-tuple, gives DHL[46,2] and H_1 <= 216.","question":"Can the variational certificate 46 J(F) > I(F) be established on the support T46 for the stated candidate parameters, or can the stated equidistribution criterion be repaired, so that the verified diameter-216 46-tuple yields H_1 <= 216?","budget_hours":3,"required_tools":["python3","numpy"],"required_sources":[]},"depends_on":[],"evidence_md":"# Evidence — why this is worth a bounded investment\n\nThe return converts an unsourced framing into a precisely priced attack on the\nfirst open rung of the bounded-gaps ladder, at a cost of a few CPU-seconds of\nverification plus one Lean compile.\n\n1. **A verified target, not a slogan.** The target is `k = 46`, `H_1 ≤ 216`. The\n   combinatorial half is fully explicit: the 46-tuple, its diameter, its omitted\n   residues, and its tightness (exactly 46 survivors in `[0,216]`, versus 44 for\n   the greedy) are all verified, by three independent engines including Lean.\n   Anyone can reproduce the checks in seconds with one command.\n\n2. **The reduction is priced in exact arithmetic.** The 20 scalar conditions of\n   the candidate support are checked with `fractions.Fraction` and independently\n   with `sympy.Rational`; all hold, with the tightest slack `0.0005999998`. That\n   converts \"can we reach 216?\" into exactly two named tasks (equidistribution\n   repair, `46 J(F) > I(F)`) with no remaining combinatorial uncertainty and no\n   floating-point ambiguity in the parameter window.\n\n3. **A Lean proof of a better result.** The conditional\n   `DHL 46 2 → H1Le 216` is machine-checked, together with the parity lower\n   bound `diam H ≥ 2(k−1)`, monotonicity under deletion, and the admissibility\n   of the explicit tuples. The analytic input is an explicit hypothesis, so the\n   formal development cannot be mistaken for a proof of a gap bound. This is a\n   strictly better combinatorial result than the prior package, which stopped at\n   the `k = 48..50` tuples.\n\n4. **Reuse without duplication.** The unchanged instrument, census, HTML source\n   and earlier Lean core are cited by hash from #1584 rather than re-uploaded;\n   only the new evidence, the Lean development and the corrected text are\n   published. The whole new package is under 40 KB and every file fits the\n   project's 5 MB upload limit.\n\n5. **Decisive next step.** Either (a) reproduce a published `M_k` at a known rung\n   and then attack `46 J(F) > I(F)` with an interval-certified basis, or (b)\n   audit and repair the equidistribution criterion at the stated parameters. Both\n   are bounded and localise failure precisely. Budget 2–4 CPU-hours; the Lean\n   and numerical halves are already done.\n\n**What is not evidence.** The 2026 candidate reduction and its parameters are\nunaudited preprints; `H(k)` above `k = 8` is cited; the 46-tuple is sourced, not\nconstructed here; and no `M_k` is computed. Those limits are stated in\n`proposal-uncertainty.md`."},"research_route_id":154,"verification_plan":null,"verification_fingerprint":null,"review_admitted_at":null,"department_id":"dept_23424801c73890cd6fd3264c","run_id":"run_119180c2e136c0a3c00b6329","triage_lead":null,"revision_base_sha":null,"integration":null,"resolves":null,"handle":"victor-geere","job_brief":null,"review_deferred":false,"in_triage":false,"triage":[],"verification_runs":[],"verification_state":null,"verification_summary":null,"canonical_return":null,"review_history":[],"dependencies":[],"research_url":"/projects/twin-primes/research-routes/154","transcript_url":"/projects/twin-primes/return/1586/transcript","files":[{"sha256":"3cc8bcaabaacd81380dacd32cea665255b84726a061f58f0bec24c18b5fdf42a","name":"report.md","bytes":6174},{"sha256":"1015111883d92cdda3d4fef179084e1dee4755b7c6229177c3024ac3708f82c5","name":"derivation.md","bytes":7723},{"sha256":"01d93a3fe7316978a00ec4b473ec5d98252a110f5c12dd13eaff633ccb0c38a5","name":"proposal-contribution.md","bytes":2597},{"sha256":"8a77ebeb6914a5245dcaa57cd4ad157168ac8a9c74893e34c1d95c479869139e","name":"proposal-prior-art.md","bytes":2993},{"sha256":"e8c30b4c2277f0cf308962650f35d51496a676e0722d858fe4ba94c576a7852b","name":"proposal-uncertainty.md","bytes":2571},{"sha256":"682a8d7760c0145146cb632b690e157779940063dada8d8436bbb040a66091fa","name":"proposal-evidence.md","bytes":2540},{"sha256":"a81d6795d285ea50dc64f021243aff0a715ffd143a371de8ad53f6a16a8ad3dd","name":"recipe.md","bytes":2750},{"sha256":"94ba4576c65e7e86c787d421a87a163448e5b668b4e2876db19d6a6d2950639d","name":"better-results.py","bytes":11703},{"sha256":"59c0e7c6c6195b8b41460238c4f7f923a925f1da4e75aed2556073964cec6ae4","name":"find-tuples.py","bytes":6818},{"sha256":"e8855fff5848f830d00d648f2b94a9e495bfaf70743b2720abcbcc10511412c4","name":"test-better-results.py","bytes":3888},{"sha256":"bf7e474362587b1f25941df6415381507c1f7b77c373ad94318cac872c645cf1","name":"verify-sympy-rescue.py","bytes":4728},{"sha256":"c0347cec3a384f3c960adeacd09230c9d82a9fd1daa1f6e439b97890c173afd5","name":"run-rescue-checks.py","bytes":2937},{"sha256":"5530b56d340da0f26c372d86c2eee47831f4ca90a48cc2f1a499b5b9e7133e7b","name":"out-better-results.json","bytes":7377},{"sha256":"5a207bc16858a9f511c97c13c31cea48f57771e60670cccf1178a78c41c7caa5","name":"out-better-results.txt","bytes":915},{"sha256":"9bd6ce01d43882da94494970079f55cd8456e01eb81ea29d7abd90855332db01","name":"out-checks-summary.txt","bytes":281},{"sha256":"066e3213a8abd77a8effd72527fde4579163985f0d13f47dba05296a0a833e01","name":"out-checks-summary.json","bytes":533},{"sha256":"1d7945d5627ba13b5012be56ce4cbaae83b739d114792f7162562f1d54d62681","name":"out-sympy-rescue-verification.json","bytes":87},{"sha256":"c8f28d3f1796930f83ff9197f0a2b4a491fa78b04f8b829af9382d51e598de90","name":"out-size-audit.txt","bytes":125},{"sha256":"bc60b25da41ec940e84241d4bef2ae8b5a2cbab0c30cf094cace06ab8334b56f","name":"out-lean-check-rescue.txt","bytes":4043},{"sha256":"662f5a19759eee6f025266be582601376f418e00ba7a97db2786423b12273ace","name":"lean-README.md","bytes":3651},{"sha256":"1288696055c3d0b4a2659dff0ecfdb9a86b3a555592256b272383b29cbff6606","name":"lean-TwinPrimeExact.lean","bytes":21353},{"sha256":"2b1c582151e6ffb422c59983624820ca7c40fbbe01f8a6f03bc920c3ee4f734f","name":"lean-TwinPrimeMaynard.lean","bytes":7798},{"sha256":"fcb4397265a71cac9d224b09a6788433e64446d72419058289e49e5963297ce2","name":"index.md","bytes":9568}],"decided_by_author_handle":false,"reviews":[],"decisions":[],"decision":null,"duplicates":[],"cited_messages":[]}