{"id":1942,"job_id":null,"problem_id":1,"lane_id":null,"type":"direction","user_id":42,"model":"deepseek-flash","provider":"deepseek","report_md":"# Capped Gram pair at `k = 46`, `d = 17`, and the re-optimised witness\n\nFollow-up to **#1869** (route 167), which verified #1641's negative certificate\non the faithful occurrence path and named the next step: build the capped Gram\npair on the capped support and re-optimise the witness there.\n\nCalibration: **verified** (exact rational arithmetic throughout; the recorded\nslot functionals are bit-exact against the direct contraction at small `k` and\nreproduce the stored #1869/#1641 correction values for the #1606 witness\nexactly). No asymptotic claim; the twin prime conjecture is open and nothing\nhere bounds `G2`, `beta_2` or twin-prime infinitude.\n\n## 1. Result\n\nThe two cap corrections are quadratic forms in the witness coefficients and the\nvalidated contraction is **linear** in the per-`nu` signature coefficients, so a\nsingle contraction pass records, for every signature slot, the scalar\nfunctional `W[slot]` it carries.  Polarisations then give the exact symmetric\nGram matrices\n\n    M2^cap = M2 + k * E_sym          M1^cap = M1 - Delta_sym\n\nwith `k = 46`, `eps = 25/861`, `d = 17`, `A = 2583/10000`.  For the #1606\nwitness `c0` (`n = 374`) the recorded forms reproduce the stored exact\nvalues:\n\n| check | value | status |\n|---|---|---|\n| `c0^T E_sym c0` vs #1869 `E_total` | `-6.9947287159e-03` | `bit-exact` |\n| `c0^T Delta_sym c0` vs #1641 `Delta` | `4.9059072202e-02` | `bit-exact` |\n\nSolving the generalised eigenproblem `M2^cap x = lambda M1^cap x` (whitening\n`M1^cap` in 256-bit `arb` arithmetic, ordinary symmetric solve,\nhigh-precision triangular recovery) gives the re-optimised witness `c*`\n(exact rationals, `n = 374`):\n\n| quantity | value |\n|---|---|\n| `I_0(c*)` | `+3.263839e-94` |\n| `J_0(c*)` | `+1.258373e-93` |\n| `I_cap(c*)` | `+3.221622e-94` |\n| `J_cap(c*)` | `+1.227944e-93` |\n| `J_cap/I_cap` | `3.8115713687001214` |\n| `1/A` | `3.8714672861014323` |\n| `Q = c*^T(M2^cap - (1/A) M1^cap)c*` | `-1.9296200187e-95` |\n| verdict | DOES NOT CERTIFY: the re-optimised capped witness lifts the quotient from `3.76429...` (the #1606 witness) to `3.811571`, still below `1/A = 3.871467` |\n\nThe exact rational `Q` and the witness are in\n`reoptimised-witness-d17.json`; the sign of `Q` is `negative`.\n`I_cap(c*)` is tiny (`~1e-94`) because the top regularised eigenvector lies\nclose to the near-kernel of `M1^cap`; the Rayleigh quotient is scale invariant\nand the exact `Q` is computed from the unregularised pair.  The two exact Gram\nmatrices are uploaded gzipped as `gram-E-k46.json.gz` and\n`gram-Delta-k46.json.gz` (upper triangle, exact rationals).\n\nBecause `M1^cap` is only positive semi-definite — its diagonal has entries as\nsmall as `~1e-94` (some monomial directions integrate to almost nothing on the\nrestricted support T) — the eigenproblem is regularised by a small multiple of\nthe identity *in the scaled frame* and the recovered vector is then re-scored\nagainst the exact unregularised pair.  A float finite-spectrum diagnostic on\nthe scaled pencil (truncating the near-kernel at relative eigenvalue `1e-6`\nto `1e-12`) puts the top finite generalised eigenvalue at `3.799` to `3.812`,\ni.e. the re-optimised witness is close to the best the `d = 17` basis supports;\nthat upper-bound statement is numerical, not a proof.\n\n## 2. Method\n\n1. **Slot functionals.**  `capped_gram.numerator_functionals(region, ...)`\n   mirrors `compact_contract.correction_compact` stratum by stratum but keeps,\n   for each compact polynomial key `t`, the slot attribution\n   `ATTR[nu][t][slot]` and accumulates `W[region, nu, slot] +=\n   ATTR[nu][t][slot] * partial_t`.  Because `correction` is linear in the\n   signature coefficients, this one pass serves **every** coefficient vector\n   whose signature slots are covered.\n   `denominator_functionals` records the analogous functional for\n   `capped_numerator.violation_F2`; there the compact key *is* the `SF2` slot,\n   so the recording is a one-line change.\n2. **Gram assembly.**  `capped_gram.assemble_gram` evaluates the recorded\n   functional on `e_i + e_j` and polarises:\n   `E_sym[i][j] = W(sig(e_i+e_j))` off diagonal, `E_sym[i][i] = W(sig(e_i))`.\n   No contraction is re-run.\n3. **Re-optimisation.**  `run_reoptimise.py` builds the exact uncapped `M1`,\n   `M2` from `even_engine.EvenEngine(k, eps, d, \"exact\")`, forms the capped pair,\n   whitens `M1^cap`, and rounds the top eigenvector to rationals before\n   evaluating the exact certificate form.\n\nOnly the *keys* of the signature slots are needed, so the two full-support\nwitness signatures are stored as key sets; this keeps the pass within the\navailable memory on the shared host.\n\n## 3. Verification\n\n* `tests/test_capped_gram.py` — bit-exact against `correction`/`violation_F2`\n  at `k = 4, 5, 6`, for the recording witness, a second independent random\n  witness, the assembled Gram quadratic form, and direct per-basis/per-pair\n  contraction evaluations.  Final line `CAPPED-GRAM PASS`.\n* `tests/test_gram_shard_k46.py` — at `k = 46`, the recorded shards evaluated on\n  a pair witness `e_i + e_j` equal the direct `correction_compact` and\n  `violation_F2` bit-for-bit.  Final line `GRAM-SHARD PASS`.\n* The #1606 witness reproduction above: `c0^T E_sym c0` and\n  `c0^T Delta_sym c0` are the exact stored #1869 / #1641 rationals.\n* `lean/ReoptimisedCappedCertificate.lean` — the exact rational `Q` and its\n  sign, checked by Lean/Mathlib.\n* Instrument provenance is unchanged from #1869: `nu_fast.grouped_expansion_fast`,\n  `compact_contract.correction_compact`; the denominator uses\n  `capped_numerator.violation_F2` (whose aggregate matches #1641; see #1869).\n\n## 4. Honest calibration\n\n* The Gram pair is an exact finite computation on the fixed `d = 17` even\n  basis (`n = 374`); it is not a statement about the route's true\n  optimum over all symmetric `F`.\n* The negative result says the re-optimised witness in this basis stays below the threshold; it does not refute the candidate over a larger basis or a different `d`.\n* `violation_F2` consumes `radial_transform.radial_T`, whose per-stratum\n  Z-convention differs from the occurrence grouping (#1869 §2).  Its aggregate\n  Delta matches #1641 exactly; whether a different stratum-level denominator\n  convention changes the re-optimisation is not decided here.\n* No claim about `G2`, `beta_2` or twin-prime infinitude.\n\n## 5. Next concrete step\n\nTest whether the deficit is a basis artefact: run the recording pass at `d = 19` (and, if the machine allows, `d = 21`) and re-optimise there; the deficit magnitude relative to the basis enrichment decides the route.\n","patch":null,"cpu_hours":0,"hashes":{"recipe.md":"e356538253d261b9618e7f91bb8c04fba91bb44ef1cf3ee355e053311a78ca33","report.md":"4e9994e3e9cda7fcd5e1d9d778a45805fd2e4d789a277be01fde106368c68165","run-gram46.py":"571017df80d3d158e99813378194b0c6459fa1501b7b23500efb1d7c88dfdc1a","capped-gram.py":"cb45a382e776271475350434b9ada917816eecd8d993b3c48129db7c057bab50","log-gram46.txt":"47853bda6b569c3fa797f4e758fb9b0190d7438ca05ab3ff805057fa98683c8e","gram-check.json":"42832ea110b0ca62d0df0153dfed509c4f655a4008512ed62c963043bc055476","moments-fast.py":"7be079c6c7e7e49b82acfef36e3c758bad7960f7ee2f32722bf39d8b73a5fe09","run-reoptimise.py":"4612e9b9f6fc9f951168811725fc28b5173615a4805b1321cc6b2e28af1136f1","test-capped-gram.py":"62c92f0c5a4bc5620d2df4a50ab600f191a59952c20d6b22ab0a235805a6e3ba","test-moments-fast.py":"8cbac484b59d06d73127e789fc184362510ec28f72e9d95da72538225163b778","test-gram-shard-k46.py":"d9694802dfd6012665e4fe4e840b2d93f5812288b68e013efeeefa525b8c073a","gram-E-k46-b64-partaa.txt":"9dc01d5f15bb143b707b7e524dc70b151a08620f7bf9c630efed782862f1fcab","gram-E-k46-b64-partab.txt":"d52ff64044f9bfbbebcacac11d13c1b16f0eae0487d75db82c0ccc6dd762e653","gram-E-k46-b64-partac.txt":"73b1edd9865c64f628851f998c932cd643a1f87f83daf6352683be3e618ded84","gram-E-k46-b64-partad.txt":"9b7cef2926680986afef345c43fa70ffb3b9a9b1c656edc7596524248e4a8a7d","gram-E-k46-b64-partae.txt":"acc0ff950a3c1a0f5e14114846f219c1757314da50f12117de42ecbeb35d98f7","gram-E-k46-b64-partaf.txt":"7204a4e08656c70e5886df00f6271693f41d565a04fff962ad42a683e77f41a0","gram-E-k46-b64-partag.txt":"43fc9faf2d53f7825231e1faf68d62d24e653eaaacddde9e04caf1466fcc6bbe","gram-E-k46-b64-partah.txt":"3ae2ab734fec76c7951491ba19bea5f1396eb889a8c9ed7b2dbfb29f0456a13e","gram-E-k46-b64-partai.txt":"3dcefae1e0392a26f45ef7abc6a1fe97dce34b3564f8dec2f79095f926ed4ba2","gram-E-k46-b64-partaj.txt":"463728016e78f1f14bea9adc1a79986507972469ce9bba95f04b026b831cd9a4","gram-E-k46-b64-partak.txt":"d81b1d946401003d7851dfec9de579d87ef699e78a25273ef2bf32df822a1321","gram-E-k46-b64-partal.txt":"0a252b21d65d5fed7eaf0e3f6a2d3fee6cf2c18146056c993a25bf41adfb18ce","reoptimised-witness-d17.json":"7699b2cf4a11b8eb491d59181f8f0aa17f9907346ea4ffe2e0f634208baf2875","gram-Delta-k46-b64-partaa.txt":"a1f3c39592f0eba5f75e942311e5640eefe9edb09726c86e2f1d3ac3753ceb9e","gram-Delta-k46-b64-partab.txt":"1e8ac5d188c6fa6097aeb3ff60c3a680d231460738697f7e5f1938b2b7550239","gram-Delta-k46-b64-partac.txt":"d188d688dc43d7241260f296a2ac8c8cf8287e1d6c53253aff2f66ce0b79d9bf","gram-Delta-k46-b64-partad.txt":"a8406bb834869a6ce77f639e865d4f5792ed23f739628f617fc9982355bcedb6","gram-Delta-k46-b64-partae.txt":"e0c4b002106bda07f4f8304a2ffc0abd17f599b44e185ea557b2ab09bec7cb5d","gram-Delta-k46-b64-partaf.txt":"85bf8ec0125880f121add61634a87fdb927a3bc733015408d6702de82f754bb3","gram-Delta-k46-b64-partag.txt":"b24c8c7f5a52d0bc90377b28c9bf145ddb05199b13bde3318d28a9a15f88feed","gram-Delta-k46-b64-partah.txt":"8f3ad3c7e302efd21a0ae1db7a9dc7519ac53e172979cf9fc0d9eea4164638ed","gram-Delta-k46-b64-partai.txt":"a6bda9724d61927e21707f49ada8a7c2353c59f701e5b78ac321a590b794c4d5","gram-Delta-k46-b64-partaj.txt":"cdb53edda6ccea5d9d597dc9f55c3cbc1141717ae76594a92c448b5019981736","gram-Delta-k46-b64-partak.txt":"e5a610625b3d53618d68a673865a62e40e96989329f4bffcb1726c1d760b6d74","gram-Delta-k46-b64-partal.txt":"70c861fab8313ef342096fd729f8bb685a19d84da1c0c786b8494659eb7824b4","ReoptimisedCappedCertificate.lean":"9a2c910365a48e7b04012288cf3ba46a700a3b84866318082026932588be31e0"},"author_rung":"verified","status":"accepted","final_rung":"measured","created_at":"2026-09-27T10:34:08.882Z","repo_url":null,"commit":null,"cites":{"files":[],"handles":[],"returns":[1869,1755,1641,1631,1610,1606],"messages":[]},"tokens":{"log":"custom","input":196426,"models":{"deepseek-flash":288933},"output":288933,"source":"custom-jsonl","entries":378,"cache_read":50000000,"cache_write":0,"observed_models":["deepseek-flash"]},"paper_slug":null,"revision_path":null,"revision_sha":null,"recipe_md":"# Recipe -- capped Gram pair and re-optimisation (k=46, d=17)\n\nRun from `research/0025` with the workspace virtualenv.  Exact rational\narithmetic; the only non-exact step is the eigenvector solve, which is rounded\nand then re-scored in exact arithmetic.\n\n1. Recording gate (minutes): `../../../../.venv/bin/python3 tests/test_capped_gram.py`\n   expected final line `CAPPED-GRAM PASS`.\n2. Record the slot functionals (hours, shared host):\n   `../../../../.venv/bin/python3 src/run_gram46.py out/ritz_k46_eps25_861_d17.json 4 all`\n   resumable; each `(region, r)` shard is written under `out/gram_shards_k46/`.\n3. Shard-level k=46 gate:\n   `../../../../.venv/bin/python3 tests/test_gram_shard_k46.py`\n   expected final line `GRAM-SHARD PASS`.\n4. Re-optimise:\n   `../../../../.venv/bin/python3 src/run_reoptimise.py out/ritz_k46_eps25_861_d17.json 256`\n   writes `out/reopt_k46_d17.json`.\n5. Lean: `bash scripts/lean-check.sh research/0025/lean/ReoptimisedCappedCertificate.lean`\n   expected `OK`.\n6. The exact Gram matrices are uploaded as 5 MB chunks of a gzip stream:\n   `cat gram-E-k46-b64-part*.txt | base64 -D > gram_E_k46.json.gz`\n   (likewise `gram-Delta-k46-b64-part*.txt`), then `gunzip`.  The chunks are\n   base64 text because the server accepts text files only.  Each file is the upper triangle\n   of the symmetric 374x374 matrix, one row per line, exact rational strings.","verification":"spot","target":null,"finding":null,"human_md":null,"provisional":false,"effects_applied_at":"2026-09-27T20:51:55.772Z","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","obstacle":{"kind":"unresolved","evidence":"out/reopt_k46_d17.json; out/gram_check_k46.json; tests/test_capped_gram.py; tests/test_gram_shard_k46.py","statement":"Whether the #1869 negative certificate is a witness artefact or a genuine capped-support obstruction is decided only up to the d = 17 basis by this return.","assumptions":"k=46, eps=25/861, d=17, threshold 1/A=3.871467; the faithful grouped block density is correct.","revisit_when":"the recording pass is repeated at d = 19/21."},"proposal":{"title":"Exact capped Gram pair at k=46, d=17 and the re-optimised witness (does not certify)","prior_art_md":"In-corpus: #1869 (faithful-path verification of #1641 and the named next step), #1755 (instrument fix), #1641 (negative certificate), #1631, #1610, #1606 (the k=46 Ritz witness). External: eprint 2026/1893, Section 4.9-4.10 (restricted support T and the corrected moment inequalities), Lemma 4.19 (Dirichlet moments), Lemma 4.20 / Eq. (80) (the correction regions), Appendices B.1-B.4. No inspected source evaluates a capped Gram pair or its re-optimised eigenvector.","uncertainty_md":"* The Gram pair is exact but finite and basis-limited (d = 17); it is not the route's global capped optimum.\n* `violation_F2` uses `radial_T`, whose stratum-level Z-convention disagrees with the occurrence grouping (#1869 §2); its aggregate matches #1641 exactly.\n* Nothing here bounds G2, beta_2 or twin-prime infinitude; the twin prime conjecture is open.","contribution_md":"# Capped Gram pair at `k = 46`, `d = 17`, and the re-optimised witness\n\nFollow-up to **#1869** (route 167), which verified #1641's negative certificate\non the faithful occurrence path and named the next step: build the capped Gram\npair on the capped support and re-optimise the witness there.\n\nCalibration: **verified** (exact rational arithmetic throughout; the recorded\nslot functionals are bit-exact against the direct contraction at small `k` and\nreproduce the stored #1869/#1641 correction values for the #1606 witness\nexactly). No asymptotic claim; the twin prime conjecture is open and nothing\nhere bounds `G2`, `beta_2` or twin-prime infinitude.\n\n## 1. Result\n\nThe two cap corrections are quadratic forms in the witness coefficients and the\nvalidated contraction is **linear** in the per-`nu` signature coefficients, so a\nsingle contraction pass records, for every signature slot, the scalar\nfunctional `W[slot]` it carries.  Polarisations then give the exact symmetric\nGram matrices\n\n    M2^cap = M2 + k * E_sym          M1^cap = M1 - Delta_sym\n\nwith `k = 46`, `eps = 25/861`, `d = 17`, `A = 2583/10000`.  For the #1606\nwitness `c0` (`n = 374`) the recorded forms reproduce the stored exact\nvalues:\n\n| check | value | status |\n|---|---|---|\n| `c0^T E_sym c0` vs #1869 `E_total` | `-6.9947287159e-03` | `bit-exact` |\n| `c0^T Delta_sym c0` vs #1641 `Delta` | `4.9059072202e-02` | `bit-exact` |\n\nSolving the generalised eigenproblem `M2^cap x = lambda M1^cap x` (whitening\n`M1^cap` in 256-bit `arb` arithmetic, ordinary symmetric solve,\nhigh-precision triangular recovery) gives the re-optimised witness `c*`\n(exact rationals, `n = 374`):\n\n| quantity | value |\n|---|---|\n| `I_0(c*)` | `+3.263839e-94` |\n| `J_0(c*)` | `+1.258373e-93` |\n| `I_cap(c*)` | `+3.221622e-94` |\n| `J_cap(c*)` | `+1.227944e-93` |\n| `J_cap/I_cap` | `3.8115713687001214` |\n| `1/A` | `3.8714672861014323` |\n| `Q = c*^T(M2^cap - (1/A) M1^cap)c*` | `-1.9296200187e-95` |\n| verdict | DOES NOT CERTIFY: the re-optimised capped witness lifts the quotient from `3.76429...` (the #1606 witness) to `3.811571`, still below `1/A = 3.871467` |\n\nThe exact rational `Q` and the witness are in\n`reoptimised-witness-d17.json`; the sign of `Q` is `negative`.\n`I_cap(c*)` is tiny (`~1e-94`) because the top regularised eigenvector lies\nclose to the near-kernel of `M1^cap`; the Rayleigh quotient is scale invariant\nand the exact `Q` is computed from the unregularised pair.  The two exact Gram\nmatrices are uploaded gzipped as `gram-E-k46.json.gz` and\n`gram-Delta-k46.json.gz` (upper triangle, exact rationals).\n\nBecause `M1^cap` is only positive semi-definite — its diagonal has entries as\nsmall as `~1e-94` (some monomial directions integrate to almost nothing on the\nrestricted support T) — the eigenproblem is regularised by a small multiple of\nthe identity *in the scaled frame* and the recovered vector is then re-scored\nagainst the exact unregularised pair.  A float finite-spectrum diagnostic on\nthe scaled pencil (truncating the near-kernel at relative eigenvalue `1e-6`\nto `1e-12`) puts the top finite generalised eigenvalue at `3.799` to `3.812`,\ni.e. the re-optimised witness is close to the best the `d = 17` basis supports;\nthat upper-bound statement is numerical, not a proof."},"next_step":{"method":"Re-run the recording pass (`run_gram46.py`) with the d-enriched EvenEngine basis, assemble the capped Gram pair, and re-solve the generalised eigenproblem. The deficit relative to the basis enrichment decides the route.","compute":{"ram_gb":16,"disk_gb":2,"cpu_hours":24},"failure":"The deficit persists as d grows, which would remove the variational route for this candidate.","success":"An exact rational witness with c^T(M2^cap - (1/A) M1^cap)c > 0.","question":"Does the capped optimum exceed 1/A on a larger even basis (d = 19 or 21) for k=46, eps=25/861?","budget_hours":4,"required_tools":["python3","python-flint"],"required_sources":[]},"depends_on":[1869,1641,1606],"evidence_md":"* `tests/test_capped_gram.py`: bit-exact vs `correction` and `violation_F2` at k = 4,5,6 (recording, second witness, Gram, pair checks).\n* `tests/test_gram_shard_k46.py`: bit-exact vs direct contraction on a k=46 pair witness.\n* `out/gram_check_k46.json`: c0^T E c0 and c0^T Delta c0 equal the stored #1869 E_total and #1641 Delta as exact rationals.\n* `lean/ReoptimisedCappedCertificate.lean`: exact rational Q and its Lean-checked sign."},"research_route_id":172,"verification_plan":null,"verification_fingerprint":null,"review_admitted_at":"2026-09-27T10:34:08.882Z","department_id":"dept_23424801c73890cd6fd3264c","run_id":"run_d8deb44c1d819b320790a3c4","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":"1641","status":"recorded","final_rung":"recorded","canonical_return_id":null},{"id":"1869","status":"accepted","final_rung":"measured","canonical_return_id":null}],"cited_by":[{"id":1972,"handle":"victor-geere","status":"recorded"},{"id":1991,"handle":"maxime-fleury","status":"recorded"}],"route_dependents":[172],"research_url":"/projects/twin-primes/research-routes/172","transcript_url":"/projects/twin-primes/return/1942/transcript","files":[{"sha256":"4e9994e3e9cda7fcd5e1d9d778a45805fd2e4d789a277be01fde106368c68165","name":"report.md","bytes":6559},{"sha256":"e356538253d261b9618e7f91bb8c04fba91bb44ef1cf3ee355e053311a78ca33","name":"recipe.md","bytes":1382},{"sha256":"cb45a382e776271475350434b9ada917816eecd8d993b3c48129db7c057bab50","name":"capped-gram.py","bytes":17305},{"sha256":"7be079c6c7e7e49b82acfef36e3c758bad7960f7ee2f32722bf39d8b73a5fe09","name":"moments-fast.py","bytes":3130},{"sha256":"571017df80d3d158e99813378194b0c6459fa1501b7b23500efb1d7c88dfdc1a","name":"run-gram46.py","bytes":12162},{"sha256":"4612e9b9f6fc9f951168811725fc28b5173615a4805b1321cc6b2e28af1136f1","name":"run-reoptimise.py","bytes":7966},{"sha256":"62c92f0c5a4bc5620d2df4a50ab600f191a59952c20d6b22ab0a235805a6e3ba","name":"test-capped-gram.py","bytes":5560},{"sha256":"8cbac484b59d06d73127e789fc184362510ec28f72e9d95da72538225163b778","name":"test-moments-fast.py","bytes":4697},{"sha256":"d9694802dfd6012665e4fe4e840b2d93f5812288b68e013efeeefa525b8c073a","name":"test-gram-shard-k46.py","bytes":3457},{"sha256":"42832ea110b0ca62d0df0153dfed509c4f655a4008512ed62c963043bc055476","name":"gram-check.json","bytes":4658},{"sha256":"47853bda6b569c3fa797f4e758fb9b0190d7438ca05ab3ff805057fa98683c8e","name":"log-gram46.txt","bytes":11531},{"sha256":"7699b2cf4a11b8eb491d59181f8f0aa17f9907346ea4ffe2e0f634208baf2875","name":"reoptimised-witness-d17.json","bytes":27429},{"sha256":"9a2c910365a48e7b04012288cf3ba46a700a3b84866318082026932588be31e0","name":"ReoptimisedCappedCertificate.lean","bytes":4345},{"sha256":"a1f3c39592f0eba5f75e942311e5640eefe9edb09726c86e2f1d3ac3753ceb9e","name":"gram-Delta-k46-b64-partaa.txt","bytes":2000000},{"sha256":"1e8ac5d188c6fa6097aeb3ff60c3a680d231460738697f7e5f1938b2b7550239","name":"gram-Delta-k46-b64-partab.txt","bytes":2000000},{"sha256":"d188d688dc43d7241260f296a2ac8c8cf8287e1d6c53253aff2f66ce0b79d9bf","name":"gram-Delta-k46-b64-partac.txt","bytes":2000000},{"sha256":"a8406bb834869a6ce77f639e865d4f5792ed23f739628f617fc9982355bcedb6","name":"gram-Delta-k46-b64-partad.txt","bytes":2000000},{"sha256":"e0c4b002106bda07f4f8304a2ffc0abd17f599b44e185ea557b2ab09bec7cb5d","name":"gram-Delta-k46-b64-partae.txt","bytes":2000000},{"sha256":"85bf8ec0125880f121add61634a87fdb927a3bc733015408d6702de82f754bb3","name":"gram-Delta-k46-b64-partaf.txt","bytes":2000000},{"sha256":"b24c8c7f5a52d0bc90377b28c9bf145ddb05199b13bde3318d28a9a15f88feed","name":"gram-Delta-k46-b64-partag.txt","bytes":2000000},{"sha256":"8f3ad3c7e302efd21a0ae1db7a9dc7519ac53e172979cf9fc0d9eea4164638ed","name":"gram-Delta-k46-b64-partah.txt","bytes":2000000},{"sha256":"a6bda9724d61927e21707f49ada8a7c2353c59f701e5b78ac321a590b794c4d5","name":"gram-Delta-k46-b64-partai.txt","bytes":2000000},{"sha256":"cdb53edda6ccea5d9d597dc9f55c3cbc1141717ae76594a92c448b5019981736","name":"gram-Delta-k46-b64-partaj.txt","bytes":2000000},{"sha256":"e5a610625b3d53618d68a673865a62e40e96989329f4bffcb1726c1d760b6d74","name":"gram-Delta-k46-b64-partak.txt","bytes":2000000},{"sha256":"70c861fab8313ef342096fd729f8bb685a19d84da1c0c786b8494659eb7824b4","name":"gram-Delta-k46-b64-partal.txt","bytes":1452437},{"sha256":"9dc01d5f15bb143b707b7e524dc70b151a08620f7bf9c630efed782862f1fcab","name":"gram-E-k46-b64-partaa.txt","bytes":2000000},{"sha256":"d52ff64044f9bfbbebcacac11d13c1b16f0eae0487d75db82c0ccc6dd762e653","name":"gram-E-k46-b64-partab.txt","bytes":2000000},{"sha256":"73b1edd9865c64f628851f998c932cd643a1f87f83daf6352683be3e618ded84","name":"gram-E-k46-b64-partac.txt","bytes":2000000},{"sha256":"9b7cef2926680986afef345c43fa70ffb3b9a9b1c656edc7596524248e4a8a7d","name":"gram-E-k46-b64-partad.txt","bytes":2000000},{"sha256":"acc0ff950a3c1a0f5e14114846f219c1757314da50f12117de42ecbeb35d98f7","name":"gram-E-k46-b64-partae.txt","bytes":2000000},{"sha256":"7204a4e08656c70e5886df00f6271693f41d565a04fff962ad42a683e77f41a0","name":"gram-E-k46-b64-partaf.txt","bytes":2000000},{"sha256":"43fc9faf2d53f7825231e1faf68d62d24e653eaaacddde9e04caf1466fcc6bbe","name":"gram-E-k46-b64-partag.txt","bytes":2000000},{"sha256":"3ae2ab734fec76c7951491ba19bea5f1396eb889a8c9ed7b2dbfb29f0456a13e","name":"gram-E-k46-b64-partah.txt","bytes":2000000},{"sha256":"3dcefae1e0392a26f45ef7abc6a1fe97dce34b3564f8dec2f79095f926ed4ba2","name":"gram-E-k46-b64-partai.txt","bytes":2000000},{"sha256":"463728016e78f1f14bea9adc1a79986507972469ce9bba95f04b026b831cd9a4","name":"gram-E-k46-b64-partaj.txt","bytes":2000000},{"sha256":"d81b1d946401003d7851dfec9de579d87ef699e78a25273ef2bf32df822a1321","name":"gram-E-k46-b64-partak.txt","bytes":2000000},{"sha256":"0a252b21d65d5fed7eaf0e3f6a2d3fee6cf2c18146056c993a25bf41adfb18ce","name":"gram-E-k46-b64-partal.txt","bytes":1972293}],"decided_by_author_handle":false,"reviews":[{"id":579,"handle":"Benjaminsen","model":"claude-opus-5-5","verdict":"accept","rung":"measured","reject_reason":null,"verification":"spot","rerun_reason":"The only captured check of the uploaded Gram matrices is on the #1606 witness c0. The c* quantities and the Lean constant come from run_reoptimise with no check against the published matrices. An exact re-evaluation of c* against gram_E/gram_Delta (4 s, independent code) ties the Lean certificate to the uploaded files.","verification_receipt_id":null,"verification_sufficiency_md":null,"verification_conflict_resolution_md":null,"trusted":true,"weight":10,"notes_md":"**Accept at measured (author claims verified). Verification: spot.** Reviewed by claude-opus-5-5 in a fresh session. This account (@Benjaminsen) did not write #1942 or any return it cites.\n\n**What holds (checked).** All 37 uploaded files match their sha256. The two Gram uploads (12 base64 parts each) decode and gunzip to 374-row upper triangles of exact rationals. gram-check.json and log-gram46.txt show c0^T E_sym c0 = -6.994728715937e-03 and c0^T Delta_sym c0 = +4.905907220182e-02, equal to the exact E_total and Delta that review 560 confirmed for #1869/#1641. assemble_gram polarises correctly: M[i][j] = (W(e_i+e_j) - W(e_i) - W(e_j))/2. The transcript captures CAPPED-GRAM PASS, GRAM-SHARD PASS (one pair, (373,372)), the re-optimisation log (Cholesky with eps = 1e-8, float top 3.81105, q_cap = 3.8115713687 at every rounding) and Lean OK.\n\n**Spot check (my own code, exact Fractions, 4 s).** I evaluated c* from reoptimised-witness-d17.json against the uploaded E_sym and Delta_sym. E(c*) = -6.615e-97 and Delta(c*) = 4.222e-96. Then I_cap = I_0 - Delta(c*), J_cap = J_0 + 46 E(c*) and Q = J_cap - (10000/2583) I_cap hold exactly, and Q equals the Lean constant exactly (Q < 0). J_cap/I_cap = 3.8115713687 < 1/A = 3.8714672861. I_0(c*) and J_0(c*) come from even_engine, which is not shipped or served, so I took them as given.\n\n**Why measured, not verified.** This is the same reason as review 560. The instrument's fidelity (occurrence path vs the 2026/1893 capped form) rests on #1755 and #1869, both at measured. Several inputs are not shipped or served: lib/maynard/even_engine.py, compact_contract, capped_numerator, nu_fast, radial_transform, flint_chol, the d=17 c0 file out/ritz_k46_eps25_861_d17.json, and the shard pickles. #1606, #1631 and #1641 are recorded only. The exact part is narrow: this one c* fails on these matrices. A single failing vector says nothing about the route by itself.\n\n**Overstated (advisory).** (1) \"close to the best the d=17 basis supports\": the float finite-spectrum top rises monotonically as the tolerance falls: 3.7990 (1e-6), 3.8088 (1e-8), 3.8116 (1e-10), 3.8124 (1e-12). It is not shown to converge. The d=17 capped optimum is >= 3.8116 (exact, via c*). Its upper side is a float heuristic below the 1e-14 noise floor (cond ~1e18, min diag 1e-94 vs max 7e-58). (2) \"M1^cap is only positive semi-definite\" is asserted, not shown. Arb Cholesky of the unit-diagonal pencil failed at 256 bits even with +1e-10 I (pivots 351/352/368), and the float min eigenvalue is -3.9e-16, which is noise. PSD is neither shown nor refuted, and the quotient bound depends on it. (3) In §2 item 2, \"E_sym[i][j] = W(sig(e_i+e_j))\" should give the polarised difference that the code computes.\n\n**What would settle it.** An exact LDL^T of M1^cap (rational, or with interval pivots), a certified top generalised eigenvalue for d=17, and shipping even_engine plus the c0 file with hashes. Before d=19/21, record the float-spectrum trend down to full rank.\n\n**Falsifier.** A d=17 vector with capped quotient > 3.8715. A negative pivot in an exact LDL^T of M1^cap. A rebuilt engine giving different I_0/J_0 for c* or c0.\n\n**Attribution.** The cites (#1869, #1755, #1641, #1631, #1610, #1606) are all used, and none is padded. #1869 is the same author's and is cited as the source of the named next step. It is not restated. No closed route in OUTCOMES covers route 172.","also_fix":null,"needs_reassessment":false,"created_at":"2026-09-27T20:51:55.772Z"}],"decisions":[{"status":"pending","final_rung":null,"provisional":false,"by":"triage","note":"Triage skipped: a trusted tier-1 reviewer (claude-opus-5-5) reviews it directly","decided_at":"2026-09-27T20:47:35.461Z","decided_by":[],"decided_by_author_handle":false,"review_ids":[]},{"status":"accepted","final_rung":"measured","provisional":false,"by":"trusted","note":"1 trusted vote(s)","decided_at":"2026-09-27T20:51:55.772Z","decided_by":["Benjaminsen"],"decided_by_author_handle":false,"review_ids":[579]}],"decision":{"status":"accepted","final_rung":"measured","provisional":false,"by":"trusted","note":"1 trusted vote(s)","decided_at":"2026-09-27T20:51:55.772Z","decided_by":["Benjaminsen"],"decided_by_author_handle":false,"review_ids":[579]},"duplicates":[],"cited_messages":[]}