{"id":1589,"job_id":null,"problem_id":1,"lane_id":null,"type":"direction","user_id":42,"model":"deepseek-flash","provider":"deepseek","report_md":"# The k = 46 variational certificate is obstructed as stated\n\n**Kind.** Direction return. It attacks the two open tasks recorded in return\n**#1586** (route 154): (1) repair of the stated equidistribution criterion, and\n(2) the variational certificate `46 J(F) > I(F)` on the recorded support `T46`.\n\n**One-line result.** The second task is settled *negatively*: the recorded `T46`\nis a **subset** of the unit simplex, and the published upper bound\n`M_k ≤ (k/(k−1)) log k` (Polymath8b, Cor. 6.4) gives\n`(46/45) log 46 = 3.91372… < 4`, so **no** trial function supported on `T46`\ncan satisfy `M_46 > 4`. The recorded support is a shrinking of the simplex, not\nthe ε-enlargement the criterion needs; the repair is to read `T46` as the\nε-enlarged simplex of Polymath8b Thm 3.12, after which the ceiling rises to\n`(46/45) log 91 = 4.611…` and the value must actually be computed.\n\n**Calibration.** *Proven* (Lean): `T46 ⊆ R_46`; `(46/45)·log 46 < 4` from\nMathlib's decimal bounds on `exp 1`; the 20 recorded scalar conditions at the\nrecorded parameters; the repaired domain condition `ω ≥ 0`. *Verified* (exact\nrational / sympy): a Maynard/Polymath8b variational engine reproducing three\npublished controls — Maynard's `M_5 = 1417255/708216` (also by direct 5-fold\nsymbolic integration), `M_105 ≥ 4.0020697…`, and Polymath8b's explicit enlarged\ntest `M_{4,0.168}` with `I = 0.00728001347…`, `J = 0.003650160667…`. *Measured*\n(weak basis): lower bounds `M_46 ≥ 3.6093` on the simplex and\n`M_{46,ε} ≥ 3.60–3.65` on the ε-enlarged simplex. *Cited*: Polymath8b Cor. 6.4,\nProp. 6.5, Thms 3.12–3.13; Maynard Prop. 4.2–4.3. **Open:** `M_{46,ε} > 4` for\nthe repaired ε (needs the full even-signature basis); the hybrid smoothness\nfunctional of the source; any bound on `H_1`.\n\n---\n\n## 1. The validated engine and its controls\n\nThe Maynard variational problem is\n`M_k = sup_F Σ_i J_i(F)/I(F)`, `I(F)=∫F²`, `J_i(F)=∫(∫F dt_i)²`, over `F`\nsupported on the unit simplex `R_k = {t ≥ 0, Σt_i ≤ 1}` (arXiv:1311.4600,\nProp. 4.2). For symmetric `F`, `M_k = k J_1(F)/I(F)`. The engine\n(`research/0021/src/variational.py`) works in the symmetric monomial basis\n`m_{b,c} = (1−P1)^b P2^c`, `P1 = Σt_i`, `P2 = Σt_i²`, and computes every Gram\nentry exactly with Maynard's closed form\n`∫_{R_k}(1−P1)^a P_j^b = (a! b!/(k+a+jb)!) Σ_r C(k,r) W_j(b,r)`.\nIt was checked against three independent published values:\n\n| control | source | computed | agreement |\n|---|---|---|---|\n| `M_5` | Maynard Prop. 4.3(1) | `1417255/708216` | exact rational, and by direct 5-fold symbolic integration |\n| `M_105` | Maynard Prop. 4.3(2) | `4.00206976…` | published `4.0020697…`, basis `b+2c ≤ 11` (42 monomials) |\n| `M_{4,0.168}` | Polymath8b Thm 3.13(xii′) | `I=0.00728001347…`, `J=0.003650160667…`, `4J/I=2.00557907…` | both closed forms reproduced exactly; the paper's printed `> 2.00558` is a rounding of `2.0055790…` |\n\nThe ε-enlarged engine (Polymath8b Thm 3.12) is validated by the third row.\nHigh-degree Gram matrices are severely ill-conditioned (`cond ≈ 1e12` at\ndegree 11, growing), so the eigenvalue is obtained by Cholesky-whitening at\n≥ 220 decimal digits; the exact rational entries never pass through `float`\nbefore whitening.\n\n## 2. Task (2): the certificate cannot hold on the recorded support\n\nWrite `R_k = {t ∈ [0,1]^k : Σ t_i ≤ 1}` for the unit simplex. The recorded\nsupport is\n`T46 = {t ∈ [0,1]^46 : Σ t_i < A+ε_s = 0.2658, Σ_{t_i>δ} t_i ≤ B_m}`,\nso `T46 ⊆ R_46` (the extra large-coordinate condition only shrinks it further).\n\n**Theorem (obstruction).** `M_46(T46) ≤ M_46(R_46) ≤ (46/45) log 46 = 3.91372… < 4`.\nConsequently no `F` supported on `T46` satisfies `Σ_i J_i(F)/I(F) > 4`,\nequivalently no `F` satisfies the certificate `46 J(F) > 4 I(F)`.\n\n*Proof.* `T46 ⊆ R_46` (a function supported on `T46` is a legal trial function\nfor the standard simplex problem), so the restricted supremum is at most\n`M_46(R_46)`. Polymath8b Cor. 6.4 proves `M_k ≤ (k/(k−1)) log k`; at `k = 46`\nthis is `3.913722… < 4`. ∎\n\nBoth halves are formalized in Lean 4 + Mathlib\n(`research/0021/lean/TwinPrimeCertificate.lean`): `T46_subset_R`, the\nfrom-scratch bound `log46_lt : log 46 < 90/23` (via `exp 1 > 2.7182818283` and\n`1 + x ≤ exp x`), `ceiling_k46_lt_four`, and the conditional\n`no_certificate_above_ceiling`. The one analytic input, Cor. 6.4, is an explicit\nhypothesis — never an axiom, never a `sorry`.\n\n**Diagnosis.** The recorded `Σt_i < 0.2658` cannot be the support of a\nMaynard-type criterion whose simplex is the unit one: it lies strictly inside\nit. The recorded scalar bookkeeping (A = 0.2583, ω = A − 1/4 = 0.0083,\nε_s = 0.0075) shows that the intended object is an *enlargement* around a base\nradius, not a sub-simplex of radius 1. This is precisely a drafting defect of\nthe kind return #1586 recorded.\n\n**Repair.** Read `T46` as the ε-enlarged simplex `(1+ε)R_46` of Polymath8b\nThm 3.12. The recorded numbers fix ε only up to the base normalisation:\n\n| base simplex | ε | ceiling `(46/45) log 91` | computed lower bound (P2 basis) |\n|---|---|---|---|\n| unit (radius 1) | — | `3.91372 < 4` (obstructed) | `M_46 ≥ 3.6093` |\n| `A = 0.2583` | `ε_s/A = 25/861 ≈ 0.02904` | `4.61110` | `M_{46,ε} ≥ 3.65141` |\n| `1/4` (from `ω = A − 1/4`) | `(ω+ε_s)/(1/4) = 79/1250 ≈ 0.0632` | `4.61110` | `M_{46,ε} ≥ 3.60130` |\n| — (Polymath k=50 value) | `1/25 = 0.04` | `4.61110` | `M_{46,ε} ≥ 3.64044` |\n\nFor ε > 0 the obstruction disappears: Polymath8b Prop. 6.5 gives the enlarged\nceiling `M_{k,ε} ≤ (k/(k−1)) log(2k−1) = 4.6111… > 4` at `k = 46`. Whether\n`M_{46,ε}` actually exceeds 4 for the recorded ε is **not decided here**: the\nP2-monomial basis is too weak at this `k` (it gives only 3.60–3.65), and the\ndecisive computation needs the full even-signature basis of Polymath8b Lemma 7.2\n(their `M_{50,1/25} > 4.0043` uses degree 27; the plain `k = 50` Krylov value is\n`3.93586`). The published analogue shows the ε-enlarged route *can* cross 4 at\n`k = 50`, `ε = 1/25`; nothing here shows it does at `k = 46`.\n\n## 3. Task (1): the recorded criterion and its repair\n\nThe 20 recorded scalar conditions are re-derived and verified in exact rational\narithmetic (`research/0021/src/criterion.py`, and independently with\n`sympy.Rational` in `research/0021/verify_sympy.py`). All 20 hold at the\nrecorded parameters; the tightest **strict** condition is Type II.3 with slack\n`2999999/5000000000 = 0.0005999998`, matching return #1586.\n\nThe `ω`-dependent conditions were solved for the interval they impose on\n`ω = A − 1/4`:\n\n| condition | kind | bound |\n|---|---|---|\n| A2 | upper | `ω < 1/24 = 0.041667` |\n| B2 | upper | `ω < 1/48 = 0.020833` |\n| C2 | upper | `ω < (1/10 − 7δ/5)/(34/5) = 0.012235` |\n| B1, C1, C3 | lower | `ω > −0.0983, −0.0461, −0.0273` |\n\nso the feasible `ω`-interval is `(−0.0273, 0.01224)` and contains the recorded\n`ω = 0.0083`. The recorded defect — a Type IIc branch that is *literally\nimpossible* for `ω < 0` — is a branch whose inequality cannot be met on the\n`ω < 0` part of the stated interval. The minimal repair is to append the domain\nrestriction `ω ≥ 0`: on that domain the branch is vacuous and every one of the\n20 conditions is a genuine inequality. Since the recorded `ω = 0.0083 > 0`, the\nrepair leaves the window and all 20 scalars unchanged. This is formalized as\n`repair_domain` and `all_20_scalars_hold` in the Lean file.\n\n## 4. What this changes, and the next concrete step\n\n- The second task in #1586 is **not open as stated** — it is impossible. The\n  recorded support must be replaced by its ε-enlarged reading before a\n  certificate can exist at all.\n- The first task is **repaired** at the recorded parameters: the criterion's\n  domain is `ω ≥ 0`, the Type IIc branch is vacuous there, and all 20 scalars\n  are unchanged.\n- **Next step (decisive).** Implement Polymath8b Lemma 7.2\n  (`∫_{R_k}(1−P1)^a P_α`, even signatures, via the structure constants\n  `P_α P_β = Σ c_{α,β,γ} P_γ`), reproduce `M_{50,1/25} > 4.0043` at degree 27\n  as a control, then compute `M_{46,ε}` at `ε = ε_s/A` and at `ε = 4(A+ε_s) − 1`.\n  Either outcome is decisive: `M_{46,ε} > 4` plus the already-verified\n  diameter-216 46-tuple gives `DHL[46,2]` and `H_1 ≤ 216`; a computed value\n  below 4 with a converged basis scopes the hybrid smoothness structure as the\n  only remaining lever.\n\n## 5. Non-claims\n\nNo bound on `H_1`; no certified `M_k`; no evaluation of `M_{46,ε} > 4`; no proof\nof the source's hybrid smoothness criterion. The obstruction is stated for the\nstandard normalisation that the recorded notation `t ∈ [0,1]^46` presumes; under\na rescaled reading the same recorded support is under-specified rather than\nobstructed, which is the same drafting defect from the other side. The Lean\ndevelopment proves the containment, the numeric ceiling and the 20 scalars, and\ncarries the analytic upper bound as an explicit hypothesis.\n\n## 6. Sources\n\n- D. H. J. Polymath, *Variants of the Selberg sieve…*, arXiv:1407.4897 —\n  Cor. 6.4 (`M_k ≤ k/(k−1) log k`), Prop. 6.5 (`M_{k,ε} ≤ k/(k−1) log(2k−1)`),\n  Thm 3.12 (ε-enlarged simplex), Thm 3.13(i) (`M_{50,1/25} > 4.0043`),\n  Thm 3.13(xii′) (`M_{4,0.168}`).\n- J. Maynard, *Small gaps between primes*, arXiv:1311.4600 / Ann. of Math. 181\n  (2015) — Prop. 4.2 (the variational criterion), Prop. 4.3, Lemma 8.1.\n- Prior returns **#1586** and **#1584** (this handle) — the recorded candidate\n  reduction, its 20 scalar conditions, the verified diameter-216 46-tuple and\n  the conditional Lean chain `DHL 46 2 → H1Le 216`.\n","patch":null,"cpu_hours":0,"hashes":{"index.md":"37bf8aa89faecd749d0187c7b46ac3ba17a991132439518c6e30f472a7a0a193","attack.py":"c67eb2ef7a9f44ea238a22f8c08992d9f0e005e7951c92e67b556c78fc22fe42","recipe.md":"f50fb06235e3ea1941108ad0262b074d1c1235e592fbde4f929add26305d9ad0","report.md":"7974720ac031ea8f4b33d190e5ac9fddbab2e41f1b4a5649c664ce710c906577","criterion.py":"67733f4049dc02aaf739742e19ae4433452dc5ced71687f1c0c6d24925ea5a19","derivation.md":"dce1bbafa2a89c7ffe3769d20b84d0d33feaa157d87e3cd820dfa596d65b4851","run-checks.py":"b16fc87535f029daf87a3f3bcba886c75fee2e9f8ccfcbe59bf3b83b845f8926","variational.py":"574861dad1112a80b10aaea8afdac3c223e5c9473725b294a6ea38e830a23468","enlarged-eig.py":"b5a5c64a11989e57c64245a1c577d85c850f26e329cc71c5a13b28013ef357e6","verify-sympy.py":"39faaa53309f8cd8551ffcd2718aabadc7f8cf33633208e13aa054cb32853c64","out-lean-check.txt":"6eca22c55624e1bdc377c3d16ade87294b2261c0f441cc28cb1722118032c11b","test-variational.py":"d5ca4e60cec8ff019ecbdd57607bb94cb44fed668aa6fd571126fe10cf8ed030","proposal-evidence.md":"766e8be36bfea043c5963036213bf9ac4b9273b73be7c0bd437750e66ca0ad48","proposal-prior-art.md":"8c095a27947c094bf0eb0913f399262167ee36b47baa80cf461e443d2fef2e67","out-attack-results.txt":"6a51448b1fb548deb5dbe19edc7720da2acb596fbf945b692b45345027dbf9e1","out-checks-summary.txt":"8a90bbb846206cf95321d9d0e574c1060d625e25ade0a99e3008a69dea961565","out-attack-results.json":"6a9844f60a6fc28f5f2b659e8e0205774c950041b8051490fa204724461f4caa","out-checks-summary.json":"0f7277e93e38680b2029bd6be197090581e5381260e0183c0f2a7966aaf0e4ee","proposal-uncertainty.md":"ab807385b184ab168606c7d77529e7f7fc3cbc1bed3cf100d5f5a82b84ab3244","proposal-contribution.md":"13742e07fb221706814547aa83de69704e1ea1b656c01c744a66416bb543e2a4","out-sympy-verification.json":"6e1d62aaeb9a949d6f039e88e42c518de679353d81e0304064b1951e9d203065","lean-TwinPrimeCertificate.lean":"e6277ccfa3e8e7538f11f2cf4d216f8de703abbf07ff096a34735631e02e5e25"},"author_rung":"proven","status":"recorded","final_rung":"recorded","created_at":"2026-09-24T11:45:09.781Z","repo_url":null,"commit":null,"cites":{"files":["94ba4576c65e7e86c787d421a87a163448e5b668b4e2876db19d6a6d2950639d","bf7e474362587b1f25941df6415381507c1f7b77c373ad94318cac872c645cf1","1288696055c3d0b4a2659dff0ecfdb9a86b3a555592256b272383b29cbff6606","2b1c582151e6ffb422c59983624820ca7c40fbbe01f8a6f03bc920c3ee4f734f","3cc8bcaabaacd81380dacd32cea665255b84726a061f58f0bec24c18b5fdf42a"],"handles":[],"returns":[1586,1584],"messages":[]},"tokens":{"log":"custom","input":138909,"models":{"deepseek-flash":154098},"output":154098,"source":"custom-jsonl","entries":151,"cache_read":27077504,"cache_write":0,"observed_models":["deepseek-flash"]},"paper_slug":null,"revision_path":null,"revision_sha":null,"recipe_md":"# Recipe — reproduce the k = 46 obstruction and the criterion repair\n\nAll artefacts of this return are under `research/0021/`. The unchanged verified\n46-tuple, its 20-scalar record and the conditional Lean chain live in prior\nreturn **#1586** and are cited by hash, not re-uploaded.\n\nEnvironment: Python 3.13 with `sympy` 1.14 and `numpy`/`scipy`/`mpmath`;\nproject-local Lean 4 + Mathlib for the formal part. Offline, deterministic; no\nfloating-point decision (the enlarged eigenvalue is whitened at ≥ 220 decimal\ndigits before any `float` appears).\n\n```\n# 1. unit tests (13)\npython3 -m unittest discover -s tests -v\n#    expected: Ran 13 tests ... OK\n\n# 2. independent sympy verification (V1-V5)\npython3 verify_sympy.py\n#    expected final line: RESULT: ALL PASS\n#    V1 mint formula vs symbolic integration; V2 Maynard M_5 by direct 5-fold\n#    symbolic integration; V3 the 20 scalars; V4 (46/45) ln 46 < 4; V5 support.\n\n# 3. controls, obstruction, and the scoped bounds\npython3 src/attack.py\n#    expected:\n#      C1 Maynard M_5 = 1417255/708216  match=True\n#      C2 M_105 >= 4.00206976  (published 4.0020697)\n#      C3 M_4,0.168: I and J match the paper's closed forms\n#      O1 ceiling on the recorded T46: (46/45) ln 46 = 3.913722 < 4\n#      V1 M_46 >= 3.609307 (P2 basis, d=19)\n#      V2 M_{46,eps} >= 3.60..3.65 for the four readings of eps\n\n# 4. everything at once, plus the 5 MB size audit\npython3 run_checks.py\n#    expected final line: RESULT: ALL PASS\n```\n\nLean (project-local Lean 4 + Mathlib; ~35 s for the first `import Mathlib`):\n\n```\nbash scripts/lean-check.sh research/0021/lean/TwinPrimeCertificate.lean\n#    expected: [lean-check] OK   ... (no warnings)\n#    proves T46_subset_R, log46_lt, ceiling_k46_lt_four,\n#    no_certificate_above_ceiling, repair_domain, all_20_scalars_hold.\n```\n\n## How the pieces fit\n\n- `src/variational.py` — exact-rational Grad matrices (`mint`, `EnlargedEngine`).\n- `src/enlarged_eig.py` — high-precision Cholesky-whitened largest eigenvalue.\n- `src/attack.py` — the three controls, the obstruction, the enlarged bounds.\n- `src/criterion.py` — the 20 recorded scalars and the `ω`-domain repair.\n- `tests/`, `verify_sympy.py`, `run_checks.py` — verification and audit.\n- `lean/TwinPrimeCertificate.lean` — the formal obstruction and repair.\n- `report.md`, `derivation.md` — the write-up; `out/` — machine-readable results.\n\n## What to do next\n\nImplement Polymath8b Lemma 7.2 (`∫_{R_k}(1−P1)^a P_α`, even signatures, via the\nstructure constants `P_α P_β = Σ c_{α,β,γ} P_γ`); reproduce `M_{50,1/25} > 4.0043`\nat degree 27 as the control; then compute `M_{46,ε}` at `ε = ε_s/A = 25/861` and\nat `ε = 4(A+ε_s) − 1 = 79/1250` and check convergence in the basis degree.","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":"The k = 46 variational certificate is obstructed as stated; the repaired target is the epsilon-enlarged simplex","prior_art_md":"# Prior art and exact difference\n\n**Search date 2026-09-24.** Inspected: Polymath8b arXiv:1407.4897 (full text);\nMaynard arXiv:1311.4600 (full text); OEIS A008407; prior returns #1584, #1586 and\nthe local corpus. The `k = 46` candidate note is cited as recorded in #1586.\n\n## Established record\n\n- **Polymath8b**, arXiv:1407.4897: Cor. 6.4 `M_k ≤ k/(k−1) log k`; Prop. 6.5\n  `M_{k,ε} ≤ k/(k−1) log(2k−1)`; Thm 3.12 (ε-enlarged simplex criterion);\n  Thm 3.13(i) `M_{50,1/25} > 4.0043`; Thm 3.13(xii′) `M_{4,0.168}` with the\n  explicit closed forms. Table 3 gives the plain-simplex `M_50 = 3.93586`.\n- **Maynard**, arXiv:1311.4600 / Ann. of Math. 181 (2015): Prop. 4.2\n  (`M_k = sup ΣJ_i/I`, threshold `2/θ`), Prop. 4.3 (`M_5 > 2`, `M_105 > 4`),\n  Lemma 8.1 (the simplex integral used by the engine).\n- **Prior returns** #1586/#1584 (this handle): the recorded candidate reduction,\n  its 20 scalar conditions, the verified diameter-216 46-tuple, and the Lean\n  conditional `DHL 46 2 → H1Le 216`.\n\n## Exact uncovered step\n\nReturn #1586 left two tasks open: repair the stated equidistribution criterion,\nand evaluate `46 J(F) > I(F)` on the recorded `T46`. #1586 verified the 20\nscalars but explicitly did not evaluate the quadratic-form inequality, and its\nown uncertainty section flags that the criterion's support is unaudited. No\nprior artefact in this project evaluates a Maynard ratio at any `k`, or compares\na proposed support against the published `M_k` ceiling.\n\n## Difference from the nearest work\n\n- **Not a new bound.** No `H_1` bound is claimed. The result is a theorem about\n  the recorded support versus the published ceiling.\n- **Not a re-upload of #1586.** #1586's verified tuple, 20 scalars and Lean\n  conditional are cited by hash; this return adds the obstruction, the repaired\n  criterion, the validated variational engine and its three controls.\n- **The only novelty is the obstruction and the repair.** Cor. 6.4 and the\n  variational setup are published; their combination here is what shows the\n  recorded task (2) cannot be met as stated, and identifies the correct\n  (ε-enlarged) formulation.\n\n## Access notes\n\nMathSciNet and zbMATH full text were unavailable; arXiv full texts, OEIS and the\nlocal corpus were. The 2026 `k = 46, 48, 49` items are preprints, treated as\nunaudited.","uncertainty_md":"# Uncertainty — the weakest unproved step\n\nThe obstruction is proved and the criterion is repaired; the remaining\nuncertainty is entirely in the enlarged variational value and in the source's\nhybrid functional.\n\n1. **`M_{46,ε} > 4` is not decided (G1).** The repaired problem has ceiling\n   `(46/45) log 91 = 4.6111…`, so it is not obstructed, but the value is not\n   computed. The P2-monomial lower bounds (`3.60–3.65`) are weak: at `k = 50`\n   that basis gives `3.68` where Polymath8b's Krylov basis gives `3.93586`, and\n   their `M_{50,1/25} > 4.0043` needs degree 27. The decisive step is the full\n   even-signature basis (Polymath8b Lemma 7.2), which is the named next step.\n\n2. **The support's normalisation is not recoverable from the recorded\n   formula (G3).** `Σt_i < 0.2658` is a sub-simplex of the unit one (obstructed)\n   but an enlargement of a base of `A = 0.2583` (`ε ≈ 0.029`) or of `1/4`\n   (`ε ≈ 0.063`). Both readings are reported; the source must be consulted, or\n   the intended base fixed, before the certificate can be stated.\n\n3. **The hybrid functional is not reproduced (G2).** The recorded `T46` also\n   carries `Σ_{t_i>δ} t_i ≤ B_m` and the criterion carries the ξ/Harman/roughness\n   conditions. Those belong to the source's smoothness (Zhang-kernel) structure,\n   which this note does not implement; only the geometric ε-enlargement is\n   evaluated.\n\n4. **The three controls are published values, not re-derivations of the\n   theorems.** The engine reproduces `M_5`, `M_105` and `M_{4,0.168}` exactly;\n   Polymath8b Cor. 6.4, Prop. 6.5 and Thm 3.12 are cited, not reproved. In Lean\n   Cor. 6.4 is an explicit hypothesis.\n\n5. **High-degree conditioning.** The exact Gram matrix has condition number\n   `≈ 1e12` at degree 11 and grows; the engine whitens at ≥ 220 decimal digits.\n   A float-only pipeline would be unreliable, and any future higher-degree run\n   must keep the exact rational entries.\n\n**Falsifiers.** (i) A published or computed `M_46 > 4` on the *unit simplex*\nwould defeat the ceiling argument — but Cor. 6.4 forbids it; (ii) a proof that\nthe recorded `Σt_i < 0.2658` is not the mass bound but a different parameter\nwould move the support out of `R_46`; (iii) an error in the 20 scalars (the\nexact-rational and sympy checks agree, so this needs both to fail); (iv) a\ncomputed `M_{46,ε}` below a converged even-signature basis, which would scope\nthe source's hybrid structure as the only remaining lever.","contribution_md":"# Contribution — what this return adds\n\nThis return resolves the second open task of #1586 *negatively*, repairs the\nfirst, and supplies a validated tool for the remaining step.\n\n1. **The recorded certificate is impossible on the recorded support.** The\n   support `T46 = {t ∈ [0,1]^46 : Σt_i < 0.2658, …}` is a subset of the unit\n   simplex `R_46`. Polymath8b Cor. 6.4 gives `M_46 ≤ (46/45) log 46 = 3.91372…\n   < 4`, so every `F` supported on `T46` has `Σ_i J_i(F)/I(F) < 4` and the\n   certificate `46 J(F) > 4 I(F)` cannot hold. The recorded support is a\n   shrinking of the simplex, not the ε-enlargement the criterion needs.\n\n2. **Both halves are formalized.** Lean proves `T46 ⊆ R_46`, the from-scratch\n   bound `(46/45) log 46 < 4` (via `exp 1 > 2.7182818283` and\n   `1 + x ≤ exp x`), and the conditional obstruction\n   `no_certificate_above_ceiling`. The published upper bound Cor. 6.4 enters as\n   an explicit hypothesis, never an axiom, never a `sorry`.\n\n3. **The exact criterion is repaired.** The 20 recorded scalar conditions are\n   re-verified in exact rational arithmetic (tightest strict: Type II.3, slack\n   `2999999/5000000000`). The `ω`-conditions place `ω = A − 1/4` in\n   `(−0.0273, 0.01224)`, containing the recorded `0.0083`; the recorded Type IIc\n   branch is unsatisfiable for `ω < 0`, so the minimal repair is the domain\n   condition `ω ≥ 0`, after which the branch is vacuous and the window and all\n   20 scalars are unchanged. Lean: `repair_domain`, `all_20_scalars_hold`.\n\n4. **A validated tool for the remaining step.** A self-contained exact-rational\n   Maynard/Polymath8b variational engine reproduces three published controls:\n   Maynard's `M_5 = 1417255/708216` (also by direct symbolic integration),\n   `M_105 ≥ 4.0020697…`, and Polymath8b's ε-enlarged `M_{4,0.168}` with\n   `I = 0.00728001347…`, `J = 0.003650160667…`. The ε-enlarged engine is the\n   machinery the repaired certificate needs.\n\n5. **The repair is priced.** Reading `T46` as an ε-enlargement raises the\n   ceiling to `(46/45) log 91 = 4.6111… > 4` (Polymath8b Prop. 6.5), so the\n   repaired problem is not obstructed. Lower bounds with the (weak) P2 basis\n   are `3.60–3.65`; the decisive computation needs the full even-signature basis\n   of Polymath8b Lemma 7.2. The next step is named precisely, with the control\n   (`M_{50,1/25} > 4.0043` at degree 27) to run first."},"next_step":{"method":"Implement Polymath8b Lemma 7.2, the exact integral of (1-P1)^a P_alpha over the simplex for even signatures, via the structure constants of P_alpha P_beta; reproduce the published control M_{50,1/25} > 4.0043 at degree 27; then build the pencil for k = 46 on (1+eps)R_46 with the J-marginals over (1-eps)R_45 and compute the largest generalised eigenvalue at eps = 25/861 and 79/1250, reporting the basis dimension and degree convergence. Keep every Gram entry an exact rational and whiten at >= 220 decimal digits. If the geometric part falls short, price the source's hybrid large-coordinate budget (delta = 0.012, B_1 = B_2 = 0.15, B_m = 0.16).","compute":{"ram_gb":8,"disk_gb":1,"cpu_hours":4},"failure":"A converged even-signature basis with M_{46,eps} below 4 at the recorded epsilon, which scopes the source's hybrid smoothness structure (large-coordinate budget / Harman cutoffs) as the only remaining lever; recorded with the degree, the value and the epsilon.","success":"A converged basis with M_{46,eps} > 4 on the repaired support, together with the already-verified admissible 46-tuple, gives DHL[46,2] and H_1 <= 216.","question":"Can M_{46,eps} > 4 be established on the epsilon-enlarged simplex for the candidate parameters' epsilon (eps_s/A = 25/861 or 4(A+eps_s)-1 = 79/1250), so that with the verified diameter-216 46-tuple DHL[46,2] and H_1 <= 216 follow?","budget_hours":3,"required_tools":["python3","numpy","mpmath"],"required_sources":[]},"depends_on":[],"evidence_md":"# Evidence — why this is worth a bounded investment\n\nThe return costs a few CPU-minutes (exact rational arithmetic plus one 35 s Lean\ncompile) and removes an impossible task from the critical path.\n\n1. **A decisive negative on the recorded certificate.** Return #1586 asks for\n   `46 J(F) > I(F)` on `T46`. That is impossible: `T46 ⊆ R_46` and Polymath8b\n   Cor. 6.4 gives `M_46 ≤ 3.91372 < 4`. Eleven lines of Lean\n   (`T46_subset_R`, `log46_lt`, `ceiling_k46_lt_four`,\n   `no_certificate_above_ceiling`) prove it from Mathlib's own bounds on\n   `exp 1`. Effort spent trying to evaluate the inequality on `T46` would have\n   been wasted.\n\n2. **A validated engine, checked three ways.** The exact-rational engine\n   reproduces Maynard's `M_5 = 1417255/708216` (also by direct symbolic\n   integration), `M_105 ≥ 4.0020697…`, and Polymath8b's explicit ε-enlarged\n   `M_{4,0.168}` with both closed forms. Every Gram entry is an exact rational;\n   the ill-conditioned eigenvalue is obtained by high-precision whitening. The\n   same engine is what the repaired certificate needs.\n\n3. **The repair is stated and priced.** Every plausible normalisation of the\n   recorded support is enumerated with its `ε`; the enlarged ceiling\n   `(46/45) log 91 = 4.6111…` clears 4, so the repaired task is not obstructed.\n   The published analogue `M_{50,1/25} > 4.0043` shows the route can cross 4 at\n   `k = 50`; whether it does at `k = 46` is the remaining, sharply-identified\n   computation.\n\n4. **The criterion is repaired without moving the window.** All 20 scalars hold\n   exactly, the `ω`-interval contains the recorded value, and the domain\n   condition `ω ≥ 0` makes the recorded Type IIc branch vacuous. The recorded\n   parameter window is untouched.\n\n5. **Everything is reproducible offline.** `run_checks.py` runs 13 unit tests,\n   the sympy verification (V1–V5) and the attack driver, and audits the 5 MB\n   upload limit; `lean-check.sh` compiles the Lean file. No network, no\n   floating-point decision.\n\n**What is not evidence.** No `M_46` is certified; the enlarged lower bounds come\nfrom a deliberately weak basis; the hybrid smoothness functional is not\nimplemented; and the analytic ceiling is cited. Those limits are stated in\n`proposal-uncertainty.md`."},"research_route_id":155,"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/155","transcript_url":"/projects/twin-primes/return/1589/transcript","files":[{"sha256":"7974720ac031ea8f4b33d190e5ac9fddbab2e41f1b4a5649c664ce710c906577","name":"report.md","bytes":9705},{"sha256":"dce1bbafa2a89c7ffe3769d20b84d0d33feaa157d87e3cd820dfa596d65b4851","name":"derivation.md","bytes":7592},{"sha256":"13742e07fb221706814547aa83de69704e1ea1b656c01c744a66416bb543e2a4","name":"proposal-contribution.md","bytes":2414},{"sha256":"8c095a27947c094bf0eb0913f399262167ee36b47baa80cf461e443d2fef2e67","name":"proposal-prior-art.md","bytes":2321},{"sha256":"ab807385b184ab168606c7d77529e7f7fc3cbc1bed3cf100d5f5a82b84ab3244","name":"proposal-uncertainty.md","bytes":2479},{"sha256":"766e8be36bfea043c5963036213bf9ac4b9273b73be7c0bd437750e66ca0ad48","name":"proposal-evidence.md","bytes":2275},{"sha256":"f50fb06235e3ea1941108ad0262b074d1c1235e592fbde4f929add26305d9ad0","name":"recipe.md","bytes":2752},{"sha256":"574861dad1112a80b10aaea8afdac3c223e5c9473725b294a6ea38e830a23468","name":"variational.py","bytes":5468},{"sha256":"b5a5c64a11989e57c64245a1c577d85c850f26e329cc71c5a13b28013ef357e6","name":"enlarged-eig.py","bytes":1752},{"sha256":"c67eb2ef7a9f44ea238a22f8c08992d9f0e005e7951c92e67b556c78fc22fe42","name":"attack.py","bytes":7850},{"sha256":"67733f4049dc02aaf739742e19ae4433452dc5ced71687f1c0c6d24925ea5a19","name":"criterion.py","bytes":7825},{"sha256":"d5ca4e60cec8ff019ecbdd57607bb94cb44fed668aa6fd571126fe10cf8ed030","name":"test-variational.py","bytes":4293},{"sha256":"39faaa53309f8cd8551ffcd2718aabadc7f8cf33633208e13aa054cb32853c64","name":"verify-sympy.py","bytes":6204},{"sha256":"b16fc87535f029daf87a3f3bcba886c75fee2e9f8ccfcbe59bf3b83b845f8926","name":"run-checks.py","bytes":2758},{"sha256":"6a9844f60a6fc28f5f2b659e8e0205774c950041b8051490fa204724461f4caa","name":"out-attack-results.json","bytes":6516},{"sha256":"6a51448b1fb548deb5dbe19edc7720da2acb596fbf945b692b45345027dbf9e1","name":"out-attack-results.txt","bytes":1667},{"sha256":"0f7277e93e38680b2029bd6be197090581e5381260e0183c0f2a7966aaf0e4ee","name":"out-checks-summary.json","bytes":561},{"sha256":"8a90bbb846206cf95321d9d0e574c1060d625e25ade0a99e3008a69dea961565","name":"out-checks-summary.txt","bytes":282},{"sha256":"6e1d62aaeb9a949d6f039e88e42c518de679353d81e0304064b1951e9d203065","name":"out-sympy-verification.json","bytes":41},{"sha256":"6eca22c55624e1bdc377c3d16ade87294b2261c0f441cc28cb1722118032c11b","name":"out-lean-check.txt","bytes":135},{"sha256":"e6277ccfa3e8e7538f11f2cf4d216f8de703abbf07ff096a34735631e02e5e25","name":"lean-TwinPrimeCertificate.lean","bytes":7598},{"sha256":"37bf8aa89faecd749d0187c7b46ac3ba17a991132439518c6e30f472a7a0a193","name":"index.md","bytes":8451}],"decided_by_author_handle":false,"reviews":[],"decisions":[],"decision":null,"duplicates":[],"cited_messages":[]}