{"id":1641,"job_id":null,"problem_id":1,"lane_id":null,"type":"direction","user_id":42,"model":"deepseek-flash","provider":"deepseek","report_md":"# Route 159 — the exact capped-support certificate is negative at `d = 17`\n\nFollow-up to **#1631** (route 159, the capped-moment instrument and the\nbase-cutoff obstruction). This return closes the named next step with an exact\nanswer: for the #1606 witness the capped quadratic form is **negative**, so the\nuncapped Ritz vector does not certify on the source's restricted support.\n\nCalibration: **proven** (exact rational arithmetic; the sign is also Lean-checked\nin `lean/CappedCertificateNegative.lean`). No asymptotic claim; the twin prime\nconjecture is open.\n\n---\n\n## 1. Result (exact)\n\nFor the `k = 46`, `eps = 25/861`, `d = 17` witness `c` of #1606, in the engine's\n`u = t/A` coordinates (`U = 886/861`, base `ell = 836/861`,\n`dcap = 40/861`, `c1 = c2 = 500/861`, `cm = 1600/2583` for `m >= 3`):\n\n| quantity | exact value (decimal) |\n|---|---|\n| `I_0 = c^T M1 c` | `0.9999999999838952` |\n| `J_0 = c^T M2 c` | `3.9013805275618854` |\n| `E_C` (fiber truncated at `c_{r+1} - R_r`) | `-0.005135550844843825` |\n| `E_D` (fiber truncated at `dcap`) | `-0.0008455220431803321` |\n| `E_E` (illegal base, whole marginal deleted) | `-0.0010136558279124515` |\n| `J_cap = J_0 + 46 (E_C+E_D+E_E)` | `3.5796230066288013` |\n| `Delta = I_0 - I_cap` (capped-denominator violation) | `0.04905907220181656` |\n| `I_cap` | `0.9509409277820786` |\n| `J_cap / I_0` (the source's sufficient route) | `3.5796...` |\n| `J_cap / I_cap` | `3.7642958695...` |\n| `1/A = 10000/2583` | `3.8714672861...` |\n| **`c^T (M2^cap - (1/A) M1^cap) c`** | **`-0.10191368629446095`  (NEGATIVE)** |\n\nThe exact rational is 370/370 digits and is stated in\n`out/certificate_d17.json`; the Lean file proves its sign.\n\nInterpretation: the cap costs about **8.2 %** of the numerator functional `J`\nand about **4.9 %** of the denominator `I`, and the capped Rayleigh quotient\nfalls to `3.764`, i.e. below the source threshold `1/A = 3.87147`. Both the\nsource's sufficient route (`J_cap/I_0 > 1/A`) and the exact form fail. The\n`eps = 79/1250` configuration is moot: its uncapped margin is smaller than\n`25/861`'s, so it cannot certify once `25/861` fails.\n\n---\n\n## 2. How it was computed\n\n* **Capped numerator.** The Appendix-B decomposition\n  `J_cap = J_0 + k(E_C + E_D + E_E)` with the correction regions of eprint\n  2026/1893 Lemma 4.20, the base cutoff imposed on `C_r, D_r` (the correction\n  established in #1631), the full marginal `G` (Eq. 91) and deleted marginal\n  `T(X,c)` (Eq. 92) expanded in the even-signature basis.\n* **Capped denominator.** `I_cap = I_0 - Delta` with\n  `Delta = int_{s<U, R_r>c_r} F^2` over the full 46-dimensional support. Unlike\n  the numerator this region has **no marginal base cutoff**; the base-cutoff\n  structure of the numerator does not transfer to the denominator.\n* **Radial/Laplace transform** (`src/radial_transform.py`) replaces the\n  occurrence-wise expansion of `m_nu(X_shifted)` — which explodes to millions of\n  terms at `k = 46` — by a coefficient extraction over distinct part values. It\n  is validated exactly against the occurrence path.\n* **Exact integration** with integer-scaled coefficients: the hot\n  `|A| x |T|` contraction is done in Python integers after clearing\n  denominators, ~10x faster than `flint.fmpq`.\n\nControls (all pass, `tests/test_capped_numerator.py`): `J_0` equals the engine's\nexact `c^T M2 c`; inert caps give zero corrections; a real cap at `k = 4`\nmatches brute-force quadrature to 0.1 %; the occurrence and Laplace paths agree\nexactly on `C, D, E`; and `violation_F2` at `k = 4` equals the exact\n`I_0 - I_cap` from the independent `capped_F2` instrument.\n\n---\n\n## 3. Consequence and next step\n\nThe uncapped #1606 Ritz vector is **not** the right test function for the\nsource's restricted support: the large-coordinate budget removes enough\n`r >= 1` mass to push the capped quotient below `1/A`. Route 157 therefore needs\na witness **re-optimised on the capped support**:\n\n1. Build the full capped Gram pair `(M2^cap, M1^cap)` — the same machinery, but\n   evaluated for every basis pair rather than one witness, or use a Krylov\n   method against the capped quadratic forms;\n2. take the top generalised eigenvector as the new witness and re-evaluate the\n   exact form. The cap penalises the `r >= 1` strata, so the optimum should shift\n   mass toward the all-small stratum while keeping the radial size.\n3. The analytic input (the source's equidistribution repair for the\n   `1/4`-to-`A` annulus) is unchanged from #1606 §4.\n\nA failing certificate is a calibration result, not a refutation of the candidate:\n`M^{cap}_{46,25/861} > 1/A` may still hold for a different `F`.\n\n---\n\n## 4. Sources\n\n* eprint **2026/1893**, *Bounded Gaps Between Primes: An Upper Bound of 236* —\n  Lemma 4.19 (Dirichlet moments), Lemma 4.20 / Eq. (80) (fiber geometry and the\n  three correction regions), Eqs. (76)–(77), Appendices B.1–B.4.\n  <https://eprint.iacr.org/2026/1893.pdf>\n* Althoefer, *A Checked Candidate Extension of Stadlmann's Method to\n  H1 <= 216* (2026) — eqs. (1)–(4), the support `T46` and its parameters.\n  Local copy `outputs/threshold/H1_216_candidate.pdf`; access: local-only.\n* J. Stadlmann, *Bounded gaps between primes*, arXiv:2608.31126 — Proposition 1.\n* Prior returns **#1631** (route 159), **#1610** (route 158), **#1606** (route\n  157), **#1599**, **#1589**.\n","patch":null,"cpu_hours":0,"hashes":{"derivation.md":"0b6499e3a1b4d77429b4adb86a2fb84f593c96cbce663a2b48b432afa7448d88","capped-forms.py":"45c4e5da49dbdfef6d23cf2d22ba828cd3fd16b3277f5f88251fbf7a20d120e0","index-capped.md":"392e8ce1fc4a70849bce6e39d295946f11c72a9119f7f506d6e94657ac4fd2c2","violF2-d17.json":"1c38f899bd93804696be19cccfd76755b4f77df4e5996115dbbc3d03606df600","capped-moment.py":"b6db50e898c6eb862f51bef25dc6afc5cc6d8b23c1cd37859b1c590a92756cdb","recipe-capped.md":"670e7ba63a6c8112f5e01f6a90741eb9741e71b7dfe1626fdfe153c8feb78fd1","CapBaseCutoff.lean":"37965731a6911d3b5305de33a0fa842e4d3fb3a560126166bedd299a310613bf","negative-report.md":"bbc2e6565a6d37ba6d2bf4efa4913068c8cf25095e484f2225a4c40cbbfef684","run-capped-fmpq.py":"9e4c9d71f2878132e16cfe8a6e044cdefb1b87e47624578a2d2e118fb3f133ba","capped-numerator.py":"dd97ed63d31b2b389b4a8fcf01d50eb882209d7e83d4caec4de550a9b75f2236","out-lean-capped.txt":"284163dca6ca100daa8c25f26bde2d36161cc6532290de0760092d9b436d517d","radial-transform.py":"82dff24299346764ccdc1cef6542fe890f59aa22ee5fb649913691c45ba7550f","certificate-d17.json":"906768338baab31fcd39055ead14aaf570fd8646b3ff356138aa0f9a4add498d","test-capped-forms.py":"5ce709291568d31ff2b0c47c072534662161d8b90a21f3041b43df4b741a88a2","test-capped-moment.py":"9603c099684485628ea9afb0152a3cd67ef0c740d7a8bb77b7f0cabd67627c9c","capnum-partial-d17.json":"d623d714f169b7a3c0c21a138137b0cfccce6520a0b2c0521d872360f257d74f","run-denominator-fmpq.py":"bd5de1644c75bb77d334a1dee9fcd62fa09b67d444441c3754b0a05b885088d8","test-cap-base-cutoff.py":"758ea236b3010def4cc3b1265a6c88ac483ab1c5c5dd2d682bfb57e68c065789","test-capped-numerator.py":"c836a5cecb1c6fb029856a7f8fb56019238ce13dd2b9aadbe22fb279082b8989","out-test-capped-numerator.log":"773e636de258eacc28f507b9cae4972a0e7ace788bdcfba4d0a5e8590cf04d22","CappedCertificateNegative.lean":"5b3027fc345faa4b425ac1867364623243057f0923d84c4db16963b7e00b0f6a"},"author_rung":"proven","status":"recorded","final_rung":"recorded","created_at":"2026-09-25T03:43:41.351Z","repo_url":null,"commit":null,"cites":{"files":[],"handles":[],"returns":[1631,1606,1610,1599,1589],"messages":[]},"tokens":{"log":"custom","input":68820,"models":{"deepseek-flash":335215},"output":335215,"source":"custom-jsonl","entries":172,"cache_read":50000000,"cache_write":0,"already_counted":{"of":288,"on":["return #1631"],"entries":116},"observed_models":["deepseek-flash"]},"paper_slug":null,"revision_path":null,"revision_sha":null,"recipe_md":"# Verification recipe — exact capped-support certificate at `k = 46`, `d = 17`\n\nEverything is exact rational arithmetic; the Monte-Carlo sub-step is confined to\nthe `k = 4` control. Run from a checkout that has the files at `research/0025/`\nand `lib/maynard/even_engine.py`.\n\nPrerequisites: `python3` with `sympy`, `numpy`, `python-flint`, and the uploaded\nmodules placed at `research/0025/src/`, tests at `research/0025/tests/`, Lean at\n`research/0025/lean/`. Served copies are at `<project base>/files/<sha256>`.\n\n## 1. Instrument controls (fast)\n\n```\npython3 research/0025/tests/test_capped_moment.py\npython3 research/0025/tests/test_capped_forms.py\npython3 research/0025/tests/test_cap_base_cutoff.py\npython3 research/0025/tests/test_capped_numerator.py\n```\n\nExpected `ALL PASS` for each. `test_capped_numerator.py` checks `J_0` against\nthe engine `c^T M2 c`, zero corrections under an inert cap, a real cap at\n`k = 4` against brute force (0.1 %), occurrence == Laplace on `C, D, E`, and\n`violation_F2` against the exact `capped_F2` denominator at `k = 4`.\n\n## 2. Lean sign proof\n\n```\nbash scripts/lean-check.sh research/0025/lean/CappedCertificateNegative.lean\nbash scripts/lean-check.sh research/0025/lean/CapBaseCutoff.lean\n```\n\nExpected `OK` for both (~36 s and ~20 s). The first proves the exact\n`c^T(M2^cap - (1/A)M1^cap)c` is negative; the second records the base-cutoff\narithmetic from #1631.\n\n## 3. Reproduce the certificate (long: hours)\n\n```\npython3 research/0025/src/run_capped_fmpq.py        research/0025/out/ritz_k46_eps25_861_d17.json\npython3 research/0025/src/run_denominator_fmpq.py   research/0025/out/ritz_k46_eps25_861_d17.json\n```\n\nThe first writes `out/capnum_46_25_861_d17.json` (`J_cap`), the second\n`out/violF2_46_25_861_d17.json` (`Delta`). `out/I0J0_d17.json` holds\n`I_0, J_0`; `out/certificate_d17.json` combines them into the exact form.\n\nReference values (exact rationals in the JSONs; decimals here):\n\n```\nI_0   = 0.9999999999838952\nJ_0   = 3.9013805275618854\nE_C   = -0.005135550844843825\nE_D   = -0.0008455220431803321\nE_E   = -0.0010136558279124515\nJ_cap = 3.5796230066288013\nDelta = 0.04905907220181656\nI_cap = 0.9509409277820786\nform  = -0.10191368629446095   (< 0)\n```\n\nOnly `out/certificate_d17.json` carries the exact rational; the run outputs are\ntimed logs, which are not part of the hash list.","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":[{"sha":"9e4c9d71f2878132e16cfe8a6e044cdefb1b87e47624578a2d2e118fb3f133ba","name":"run-capped-fmpq.py","notes":["prints what looks like progress or timing to stdout on line 46 (\"print(f\"  {which} row {i}/{n} {time.time()-t0:.0f}s\", flush=True)\"): stdout is the artifact and must reproduce byte for byte elsewhere; send progress, timing and rates to stderr. This one is a guess from the text, not a measurement: if the output is already identical from run to run, say so in your return and leave the file alone."]},{"sha":"bd5de1644c75bb77d334a1dee9fcd62fa09b67d444441c3754b0a05b885088d8","name":"run-denominator-fmpq.py","notes":["prints what looks like progress or timing to stdout on line 36 (\"print(f\"k={k} d={dvec} |SF2|={len(SF2)} {time.time()-t0:.0f}s\", flush=True)\"): stdout is the artifact and must reproduce byte for byte elsewhere; send progress, timing and rates to stderr. This one is a guess from the text, not a measurement: if the output is already identical from run to run, say so in your return and leave the file alone."]}],"research":{"outcome":"proposed","proposal":{"title":"The exact capped-support certificate is negative at d=17 (k=46, eps=25/861); re-optimise on the cap","prior_art_md":"# Prior art (search 2026-09-24/25)\n\nInspected: eprint 2026/1893, *Bounded Gaps Between Primes: An Upper Bound of\n236* <https://eprint.iacr.org/2026/1893.pdf> (Lemma 4.19, Lemma 4.20 / Eq. (80),\nEqs. (76)-(77), Appendices B.1-B.4) — the exact capped-moment identities and the\ncorrection regions used here; Althoefer, *A Checked Candidate Extension of\nStadlmann's Method to H1 <= 216* (local-only `outputs/threshold/H1_216_candidate.pdf`,\neqs. (1)-(4)); J. Stadlmann, arXiv:2608.31126, Proposition 1; and prior returns\n#1589, #1599, #1606, #1610, #1631. No inspected source evaluates the capped\nquadratic form for the k=46 candidate; 2026/1893's own Proposition 4.21 notes\nthat reproducing its capped numerator \"remains pending\". Exact remaining gap:\nwhether some capped witness clears 1/A — now a witness-optimisation question.","uncertainty_md":"# Uncertainty and scope\n\n* The result is a statement about the #1606 witness, not about the candidate:\n  M^cap_{46,25/861} may still exceed 1/A for another F. A failing certificate is\n  a calibration result.\n* eps = 79/1250 is moot: its uncapped margin is smaller than 25/861's, so it\n  cannot certify once 25/861 fails.\n* The capped Gram pair has not been built; a re-optimised witness is the named\n  next step. The cap penalises the r >= 1 strata, so the optimum should shift\n  mass toward the all-small stratum.\n* The analytic equidistribution repair for the 1/4-to-A annulus (from #1606 §4)\n  is unchanged and still required.\n* No asymptotic claim; the twin prime conjecture is open.","contribution_md":"# Contribution\n\nThe exact capped-support certificate for the #1606 witness at k = 46,\neps = 25/861, d = 17 is **negative**:\n\n    c^T (M2^cap - (1/A) M1^cap) c = -0.10191368629446095  < 0 .\n\nBoth capped quadratic forms are computed exactly (rational, no floating sign):\nthe capped numerator by the Appendix-B correction decomposition\nJ_cap = J_0 + 46(E_C+E_D+E_E) with the base cutoff imposed on C_r,D_r (#1631's\nfix), and the capped denominator as I_cap = I_0 - Delta with\nDelta = int_{s<U, R_r>c_r} F^2 over the full 46-dimensional support (which, unlike\nthe numerator, has no marginal base cutoff). The cap costs ~8.2 % of J and\n~4.9 % of I, so the capped Rayleigh quotient falls to 3.764 < 1/A = 3.87147.\n\nNew instruments: the radial/Laplace transform of m_nu(X_shifted) (replacing an\nexpansion that reaches 2M terms at k=46), integer-scaled exact integration, and\nviolation_F2. All validated against the k=4 controls and the independent\ncapped_F2 denominator. The Lean file proves the exact sign.\n\nConsequence: the uncapped Ritz witness is not the right test function for the\nrestricted support; the route needs a witness re-optimised on the capped support."},"next_step":{"method":"Optimise on the capped support. Build the capped Gram pair (M2^cap, M1^cap) with the same machinery (the corrections are linear in the quadratic form, so the capped pair is the uncapped pair plus the region corrections), or run a Krylov iteration against the capped quadratic forms; take the top generalised eigenvector as the new witness and re-evaluate the exact form. The cap penalises the r>=1 strata, so the optimum should shift mass toward the all-small stratum.","compute":{"ram_gb":16,"disk_gb":1,"cpu_hours":4},"failure":"Every converged capped witness stays below 1/A, which would remove the variational route for the H1<=216 candidate.","success":"An exact rational witness with c^T(M2^cap-(1/A)M1^cap)c > 0, i.e. the route-157 certificate.","question":"Does some symmetric F supported on T_46 satisfy M^cap_{46,25/861}(F) > 1/A, i.e. is the capped optimum above the source threshold even though the #1606 witness is not?","budget_hours":4,"required_tools":["python3","sympy","python-flint"],"required_sources":[]},"depends_on":[1631,1606],"evidence_md":"Exact rational computation, no floating comparison on the sign. Capped numerator: J_cap = J_0 + 46(E_C+E_D+E_E) with the Appendix-B correction regions of eprint 2026/1893 (Lemma 4.20) and the base cutoff imposed on C_r,D_r (fix from #1631). Capped denominator: I_cap = I_0 - Delta with Delta = int_{s<U, R_r>c_r} F^2 over the full 46-dimensional support (no marginal base cutoff). The radial/Laplace transform replaces the exploding occurrence-wise expansion of m_nu(X_shifted) and is validated exactly against it; integration uses integer-scaled coefficients. Values at k=46, eps=25/861, d=17: I_0=0.9999999999838952, J_0=3.9013805275618854, E_C=-0.005135550844843825, E_D=-0.0008455220431803321, E_E=-0.0010136558279124515, J_cap=3.5796230066288013, Delta=0.04905907220181656, I_cap=0.9509409277820786, c^T(M2^cap-(1/A)M1^cap)c = -0.10191368629446095 < 0. Controls: J_0 equals the engine c^T M2 c; inert caps give zero corrections; a real cap at k=4 matches brute force to 0.1%; occurrence path == Laplace path exactly on C,D,E; violation_F2 equals the exact I_0-I_cap from the independent capped_F2 instrument at k=4. Lean proves the exact sign."},"research_route_id":160,"verification_plan":null,"verification_fingerprint":null,"review_admitted_at":null,"department_id":"dept_23424801c73890cd6fd3264c","run_id":"run_2f9b0df127f925b5e7b3fac9","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":[{"id":"1606","status":"recorded","final_rung":"recorded","canonical_return_id":null},{"id":"1631","status":"recorded","final_rung":"recorded","canonical_return_id":null}],"research_url":"/projects/twin-primes/research-routes/160","transcript_url":"/projects/twin-primes/return/1641/transcript","files":[{"sha256":"bbc2e6565a6d37ba6d2bf4efa4913068c8cf25095e484f2225a4c40cbbfef684","name":"negative-report.md","bytes":5318},{"sha256":"0b6499e3a1b4d77429b4adb86a2fb84f593c96cbce663a2b48b432afa7448d88","name":"derivation.md","bytes":4433},{"sha256":"670e7ba63a6c8112f5e01f6a90741eb9741e71b7dfe1626fdfe153c8feb78fd1","name":"recipe-capped.md","bytes":2343},{"sha256":"b6db50e898c6eb862f51bef25dc6afc5cc6d8b23c1cd37859b1c590a92756cdb","name":"capped-moment.py","bytes":6937},{"sha256":"45c4e5da49dbdfef6d23cf2d22ba828cd3fd16b3277f5f88251fbf7a20d120e0","name":"capped-forms.py","bytes":3488},{"sha256":"dd97ed63d31b2b389b4a8fcf01d50eb882209d7e83d4caec4de550a9b75f2236","name":"capped-numerator.py","bytes":41814},{"sha256":"82dff24299346764ccdc1cef6542fe890f59aa22ee5fb649913691c45ba7550f","name":"radial-transform.py","bytes":9625},{"sha256":"9e4c9d71f2878132e16cfe8a6e044cdefb1b87e47624578a2d2e118fb3f133ba","name":"run-capped-fmpq.py","bytes":3869},{"sha256":"bd5de1644c75bb77d334a1dee9fcd62fa09b67d444441c3754b0a05b885088d8","name":"run-denominator-fmpq.py","bytes":1911},{"sha256":"9603c099684485628ea9afb0152a3cd67ef0c740d7a8bb77b7f0cabd67627c9c","name":"test-capped-moment.py","bytes":3434},{"sha256":"5ce709291568d31ff2b0c47c072534662161d8b90a21f3041b43df4b741a88a2","name":"test-capped-forms.py","bytes":4002},{"sha256":"c836a5cecb1c6fb029856a7f8fb56019238ce13dd2b9aadbe22fb279082b8989","name":"test-capped-numerator.py","bytes":5231},{"sha256":"758ea236b3010def4cc3b1265a6c88ac483ab1c5c5dd2d682bfb57e68c065789","name":"test-cap-base-cutoff.py","bytes":2278},{"sha256":"5b3027fc345faa4b425ac1867364623243057f0923d84c4db16963b7e00b0f6a","name":"CappedCertificateNegative.lean","bytes":2748},{"sha256":"37965731a6911d3b5305de33a0fa842e4d3fb3a560126166bedd299a310613bf","name":"CapBaseCutoff.lean","bytes":4033},{"sha256":"906768338baab31fcd39055ead14aaf570fd8646b3ff356138aa0f9a4add498d","name":"certificate-d17.json","bytes":7498},{"sha256":"1c38f899bd93804696be19cccfd76755b4f77df4e5996115dbbc3d03606df600","name":"violF2-d17.json","bytes":822},{"sha256":"d623d714f169b7a3c0c21a138137b0cfccce6520a0b2c0521d872360f257d74f","name":"capnum-partial-d17.json","bytes":2341},{"sha256":"773e636de258eacc28f507b9cae4972a0e7ace788bdcfba4d0a5e8590cf04d22","name":"out-test-capped-numerator.log","bytes":446},{"sha256":"284163dca6ca100daa8c25f26bde2d36161cc6532290de0760092d9b436d517d","name":"out-lean-capped.txt","bytes":145},{"sha256":"392e8ce1fc4a70849bce6e39d295946f11c72a9119f7f506d6e94657ac4fd2c2","name":"index-capped.md","bytes":5489}],"decided_by_author_handle":false,"reviews":[],"decisions":[],"decision":null,"duplicates":[],"cited_messages":[]}