Research: verified T74 residue concentration (superseded by #2863)

research/shared-kernel-pair-concentration/.gitattributes

@@ -0,0 +1 @@
+* -text

research/shared-kernel-pair-concentration/CLAIM.json

@@ -0,0 +1,23 @@
+{
+  "status": "PASS_COMPLETE_CONDITIONAL_FINITE_RELEASE",
+  "baseline_head": "0b2e2537b368a0cade07ce3f71452ea018ebe394",
+  "baseline_kappa": "17200966286848326009719999999999999999999998999999999999999999999999/10000000000000000000000000000000000000000000000000000000000000000000000",
+  "kappa": "17200974023397817160599999999999999999999998999999999999999999999999/10000000000000000000000000000000000000000000000000000000000000000000000",
+  "kappa_decimal": "0.0017200974023397817160599999999999999999999998999999999999999999999999",
+  "gain": "48353434319693/62500000000000000000000",
+  "gain_decimal": "7.73654949115088E-10",
+  "complex_lower": "86004870116989085803/50000000000000000000000",
+  "profile": {
+    "1": 1611720,
+    "2": 427573,
+    "3": 183550,
+    "4": 85248,
+    "5": 26196,
+    "8": 5328,
+    "16": 1,
+    "48": 26758
+  },
+  "scope": "Conditional finite supplier and outer release. Not a formal complete multiplication theorem or measured runtime speedup.",
+  "release_receipt_sha256": "b0bd7d115bf2753f786870887bc14a2a3f42459761412f350a4802efa336ba71",
+  "supplier_manifest_sha256": "34ef9abf9ef04ccaaf79dbd84b964bb704a448b95629ffd2a8200f709c8b0505"
+}

research/shared-kernel-pair-concentration/CONSTRUCTION.json

@@ -0,0 +1 @@
+{"source_head":"0b2e2537b368a0cade07ce3f71452ea018ebe394","source_sha256":{"FILL.json.gz":"82218aaaf08825bd4a3cca676815c7e9c00d06d0da123b1c5ad234c8c91cb501","ORDER.json":"84f030a59dde4fa4635988ef0931ebae66964b3a202df79d38247fbe8a5592dc","DISPATCH.json":"5513481a70c83767b5836b15fb7ff204d2a8f8fca83c6bcaee90a20b3d1ec6c4"},"copies":2,"replica_offset":37,"time_map":"2*t+k","transfer":{"call":658,"helper":297,"width":7,"before":[35,16,37,0],"after":[72,16,37,7]},"profile_delta_from_double":{"2":1,"9":-2,"16":1},"status":"GENERATED_NOT_ADMITTED"}

research/shared-kernel-pair-concentration/DISPATCH.json

@@ -0,0 +1 @@
+[[0,0,"extra"],[0,37,"extra"],[0,1,"extra"],[0,38,"extra"],[0,2,"extra"],[0,39,"extra"],[0,3,"extra"],[0,40,"extra"],[0,4,"extra"],[0,41,"extra"],[1,0,"extra"],[1,37,"extra"],[0,5,"extra"],[0,42,"extra"],[1,1,"extra"],[1,38,"extra"],[0,6,"extra"],[0,43,"extra"],[1,2,"extra"],[1,39,"extra"],[0,7,"extra"],[0,44,"extra"],[1,3,"extra"],[1,40,"extra"],[0,8,"extra"],[0,45,"extra"],[1,4,"extra"],[1,41,"extra"],[0,9,"extra"],[0,46,"extra"],[2,0,"extra"],[2,37,"extra"],[1,5,"extra"],[1,42,"extra"],[0,10,"extra"],[0,47,"extra"],[2,1,"extra"],[2,38,"extra"],[1,6,"extra"],[1,43,"extra"],[0,11,"extra"],[0,48,"extra"],[2,2,"extra"],[2,39,"extra"],[1,7,"extra"],[1,44,"extra"],[0,12,"extra"],[0,49,"extra"],[2,3,"extra"],[2,40,"extra"],[1,8,"extra"],[1,45,"extra"],[0,13,"extra"],[0,50,"extra"],[2,4,"extra"],[2,41,"extra"],[1,9,"extra"],[1,46,"extra"],[3,0,"extra"],[3,37,"extra"],[0,14,"extra"],[0,51,"extra"],[2,5,"extra"],[2,42,"extra"],[1,10,"extra"],[1,47,"extra"],[3,1,"extra"],[3,38,"extra"],[0,15,"extra"],[0,52,"extra"],[2,6,"extra"],[2,43,"extra"],[1,11,"extra"],[1,48,"extra"],[3,2,"extra"],[3,39,"extra"],[0,16,"extra"],[0,53,"extra"],[2,7,"extra"],[2,44,"extra"],[1,12,"extra"],[1,49,"extra"],[3,3,"extra"],[3,40,"extra"],[0,17,"extra"],[0,54,"extra"],[2,8,"extra"],[2,45,"extra"],[1,13,"extra"],[1,50,"extra"],[3,4,"extra"],[3,41,"extra"],[0,18,"extra"],[0,55,"extra"],[2,9,"extra"],[2,46,"extra"],[4,0,"extra"],[4,37,"extra"],[1,14,"extra"],[1,51,"extra"],[3,5,"extra"],[3,42,"extra"],[0,19,"extra"],[0,56,"extra"],[2,10,"extra"],[2,47,"extra"],[4,1,"extra"],[4,38,"extra"],[1,15,"extra"],[1,52,"extra"],[3,6,"extra"],[3,43,"extra"],[0,20,"extra"],[0,57,"extra"],[2,11,"extra"],[2,48,"extra"],[4,2,"extra"],[4,39,"extra"],[1,16,"extra"],[1,53,"extra"],[3,7,"extra"],[3,44,"extra"],[0,21,"extra"],[0,58,"extra"],[2,12,"extra"],[2,49,"extra"],[4,3,"extra"],[4,40,"extra"],[1,17,"extra"],[1,54,"extra"],[3,8,"extra"],[3,45,"extra"],[0,22,"extra"],[0,59,"extra"],[2,13,"extra"],[2,50,"extra"],[4,4,"extra"],[4,41,"extra"],[1,18,"extra"],[1,55,"extra"],[3,9,"extra"],[3,46,"extra"],[0,23,"extra"],[0,60,"extra"],[5,0,"extra"],[5,37,"extra"],[2,14,"extra"],[2,51,"extra"],[4,5,"extra"],[4,42,"extra"],[1,19,"extra"],[1,56,"extra"],[3,10,"extra"],[3,47,"extra"],[0,24,"extra"],[0,61,"extra"],[5,1,"extra"],[5,38,"extra"],[2,15,"extra"],[2,52,"extra"],[4,6,"extra"],[4,43,"extra"],[1,20,"extra"],[1,57,"extra"],[3,11,"extra"],[3,48,"extra"],[0,25,"extra"],[0,62,"extra"],[5,2,"extra"],[5,39,"extra"],[2,16,"extra"],[2,53,"extra"],[4,7,"extra"],[4,44,"extra"],[1,21,"extra"],[1,58,"extra"],[3,12,"extra"],[3,49,"extra"],[0,26,"extra"],[0,63,"extra"],[5,3,"extra"],[5,40,"extra"],[2,17,"extra"],[2,54,"extra"],[4,8,"extra"],[4,45,"extra"],[1,22,"extra"],[1,59,"extra"],[3,13,"extra"],[3,50,"extra"],[0,27,"extra"],[0,64,"extra"],[5,4,"extra"],[5,41,"extra"],[2,18,"extra"],[2,55,"extra"],[4,9,"extra"],[4,46,"extra"],[1,23,"extra"],[1,60,"extra"],[6,0,"extra"],[6,37,"extra"],[3,14,"extra"],[3,51,"extra"],[0,28,"extra"],[0,65,"extra"],[5,5,"extra"],[5,42,"extra"],[2,19,"extra"],[2,56,"extra"],[4,10,"extra"],[4,47,"extra"],[1,24,"extra"],[1,61,"extra"],[6,1,"extra"],[6,38,"extra"],[3,15,"extra"],[3,52,"extra"],[0,29,"extra"],[0,66,"extra"],[5,6,"extra"],[5,43,"extra"],[2,20,"extra"],[2,57,"extra"],[4,11,"extra"],[4,48,"extra"],[1,25,"extra"],[1,62,"extra"],[6,2,"extra"],[6,39,"extra"],[3,16,"extra"],[3,53,"extra"],[0,30,"extra"],[0,67,"extra"],[5,7,"extra"],[5,44,"extra"],[2,21,"extra"],[2,58,"extra"],[4,12,"extra"],[4,49,"extra"],[1,26,"extra"],[1,63,"extra"],[6,3,"extra"],[6,40,"extra"],[3,17,"extra"],[3,54,"extra"],[0,31,"extra"],[0,68,"extra"],[5,8,"extra"],[5,45,"extra"],[2,22,"extra"],[2,59,"extra"],[4,13,"extra"],[4,50,"extra"],[1,27,"extra"],[1,64,"extra"],[6,4,"extra"],[6,41,"extra"],[3,18,"extra"],[3,55,"extra"],[0,32,"extra"],[0,69,"extra"],[5,9,"extra"],[5,46,"extra"],[2,23,"extra"],[2,60,"extra"],[7,0,"extra"],[7,37,"extra"],[4,14,"extra"],[4,51,"extra"],[1,28,"extra"],[1,65,"extra"],[6,5,"extra"],[6,42,"extra"],[3,19,"extra"],[3,56,"extra"],[0,33,"extra"],[0,70,"extra"],[5,10,"extra"],[5,47,"extra"],[2,24,"extra"],[2,61,"extra"],[7,1,"extra"],[7,38,"extra"],[4,15,"extra"],[4,52,"extra"],[1,29,"extra"],[1,66,"extra"],[6,6,"extra"],[6,43,"extra"],[3,20,"extra"],[3,57,"extra"],[0,34,"extra"],[0,71,"extra"],[5,11,"extra"],[5,48,"extra"],[2,25,"extra"],[2,62,"extra"],[7,2,"extra"],[7,39,"extra"],[4,16,"extra"],[4,53,"extra"],[1,30,"extra"],[1,67,"extra"],[6,7,"extra"],[6,44,"extra"],[3,21,"extra"],[3,58,"extra"],[0,35,"extra"],[0,72,"extra"],[5,12,"extra"],[5,49,"extra"],[2,26,"extra"],[2,63,"extra"],[7,3,"extra"],[7,40,"extra"],[4,17,"extra"],[4,54,"extra"],[1,31,"extra"],[1,68,"extra"],[6,8,"extra"],[6,45,"extra"],[3,22,"extra"],[3,59,"extra"],[0,36,"extra"],[0,73,"extra"],[5,13,"extra"],[5,50,"extra"],[2,27,"extra"],[2,64,"extra"],[7,4,"extra"],[7,41,"extra"],[4,18,"extra"],[4,55,"extra"],[1,32,"extra"],[1,69,"extra"],[6,9,"extra"],[6,46,"extra"],[3,23,"extra"],[3,60,"extra"],[8,0,"extra"],[8,37,"extra"],[5,14,"extra"],[5,51,"extra"],[2,28,"extra"],[2,65,"extra"],[7,5,"extra"],[7,42,"extra"],[4,19,"extra"],[4,56,"extra"],[1,33,"extra"],[1,70,"extra"],[6,10,"extra"],[6,47,"extra"],[3,24,"extra"],[3,61,"extra"],[8,1,"extra"],[8,38,"extra"],[5,15,"extra"],[5,52,"extra"],[2,29,"extra"],[2,66,"extra"],[7,6,"extra"],[7,43,"extra"],[4,20,"extra"],[4,57,"extra"],[1,34,"extra"],[1,71,"extra"],[6,11,"extra"],[6,48,"extra"],[3,25,"extra"],[3,62,"extra"],[8,2,"extra"],[8,39,"extra"],[5,16,"extra"],[5,53,"extra"],[2,30,"extra"],[2,67,"extra"],[7,7,"extra"],[7,44,"extra"],[4,21,"extra"],[4,58,"extra"],[1,35,"extra"],[1,72,"extra"],[6,12,"extra"],[6,49,"extra"],[3,26,"extra"],[3,63,"extra"],[8,3,"extra"],[8,40,"extra"],[5,17,"extra"],[5,54,"extra"],[2,31,"extra"],[2,68,"extra"],[7,8,"extra"],[7,45,"extra"],[4,22,"extra"],[4,59,"extra"],[1,36,"extra"],[1,73,"extra"],[6,13,"extra"],[6,50,"extra"],[3,27,"extra"],[3,64,"extra"],[8,4,"extra"],[8,41,"extra"],[5,18,"extra"],[5,55,"extra"],[2,32,"extra"],[2,69,"extra"],[7,9,"extra"],[7,46,"extra"],[4,23,"extra"],[4,60,"extra"],[6,14,"extra"],[6,51,"extra"],[3,28,"gauge44"],[3,65,"gauge44"],[8,5,"gauge44"],[8,42,"gauge44"],[5,19,"gauge44"],[5,56,"gauge44"],[2,33,"gauge44"],[2,70,"gauge44"],[7,10,"gauge44"],[7,47,"gauge44"],[4,24,"gauge44"],[4,61,"gauge44"],[6,15,"gauge44"],[6,52,"gauge44"],[3,29,"gauge44"],[3,66,"gauge44"],[8,6,"gauge44"],[8,43,"gauge44"],[5,20,"gauge44"],[5,57,"gauge44"],[2,34,"gauge44"],[2,71,"gauge44"],[7,11,"gauge44"],[7,48,"gauge44"],[4,25,"gauge44"],[4,62,"gauge44"],[6,16,"gauge44"],[6,53,"gauge44"],[3,30,"gauge44"],[3,67,"gauge44"],[8,7,"gauge44"],[8,44,"gauge44"],[5,21,"gauge44"],[5,58,"gauge44"],[2,35,"gauge44"],[2,72,"gauge44"],[7,12,"gauge44"],[7,49,"gauge44"],[4,26,"gauge44"],[4,63,"gauge44"],[6,17,"gauge44"],[6,54,"gauge44"],[3,31,"gauge44"],[3,68,"gauge44"],[8,8,"gauge44"],[8,45,"gauge44"],[5,22,"gauge44"],[5,59,"gauge44"],[2,36,"gauge44"],[2,73,"gauge44"],[7,13,"gauge44"],[7,50,"gauge44"],[4,27,"gauge44"],[4,64,"gauge44"],[6,18,"gauge44"],[6,55,"gauge44"],[3,32,"gauge44"],[3,69,"gauge44"],[8,9,"gauge44"],[8,46,"gauge44"],[5,23,"gauge44"],[5,60,"gauge44"],[7,14,"gauge44"],[7,51,"gauge44"],[4,28,"gauge44"],[4,65,"gauge44"],[6,19,"gauge44"],[6,56,"gauge44"],[3,33,"gauge44"],[3,70,"gauge44"],[8,10,"gauge44"],[8,47,"gauge44"],[5,24,"gauge44"],[5,61,"gauge44"],[7,15,"gauge44"],[7,52,"gauge44"],[4,29,"gauge44"],[4,66,"gauge44"],[6,20,"gauge44"],[6,57,"gauge44"],[3,34,"gauge44"],[3,71,"gauge44"],[8,11,"gauge44"],[8,48,"gauge44"],[5,25,"gauge44"],[5,62,"gauge44"],[7,16,"gauge44"],[7,53,"gauge44"],[4,30,"gauge44"],[4,67,"gauge44"],[6,21,"gauge44"],[6,58,"gauge44"],[3,35,"gauge44"],[3,72,"gauge44"],[8,12,"gauge44"],[8,49,"gauge44"],[5,26,"gauge44"],[5,63,"gauge44"],[7,17,"gauge44"],[7,54,"gauge44"],[4,31,"gauge44"],[4,68,"gauge44"],[6,22,"gauge44"],[6,59,"gauge44"],[3,36,"gauge44"],[3,73,"gauge44"],[8,13,"gauge44"],[8,50,"gauge44"],[5,27,"gauge44"],[5,64,"gauge44"],[7,18,"gauge44"],[7,55,"gauge44"],[4,32,"gauge44"],[4,69,"gauge44"],[6,23,"gauge44"],[6,60,"gauge44"],[8,14,"gauge44"],[8,51,"gauge44"],[5,28,"gauge44"],[5,65,"gauge44"],[7,19,"gauge44"],[7,56,"gauge44"],[4,33,"gauge44"],[4,70,"gauge44"],[6,24,"gauge44"],[6,61,"gauge44"],[8,15,"gauge44"],[8,52,"gauge44"],[5,29,"gauge44"],[5,66,"gauge44"],[7,20,"gauge44"],[7,57,"gauge44"],[4,34,"gauge44"],[4,71,"gauge44"],[6,25,"gauge44"],[6,62,"gauge44"],[8,16,"gauge44"],[8,53,"gauge44"],[5,30,"gauge44"],[5,67,"gauge44"],[7,21,"gauge44"],[7,58,"gauge44"],[4,35,"gauge44"],[4,72,"gauge44"],[6,26,"gauge44"],[6,63,"gauge44"],[8,17,"gauge44"],[8,54,"gauge44"],[5,31,"gauge44"],[5,68,"gauge44"],[7,22,"gauge44"],[7,59,"gauge44"],[4,36,"gauge44"],[4,73,"gauge44"],[6,27,"gauge44"],[6,64,"gauge44"],[8,18,"gauge44"],[8,55,"gauge44"],[5,32,"gauge44"],[5,69,"gauge44"],[7,23,"gauge44"],[7,60,"gauge44"],[6,28,"gauge44"],[6,65,"gauge44"],[8,19,"gauge44"],[8,56,"gauge44"],[5,33,"gauge44"],[5,70,"gauge44"],[7,24,"gauge44"],[7,61,"gauge44"],[6,29,"gauge44"],[6,66,"gauge44"],[8,20,"gauge44"],[8,57,"gauge44"],[5,34,"gauge44"],[5,71,"gauge44"],[7,25,"gauge44"],[7,62,"gauge44"],[6,30,"gauge44"],[6,67,"gauge44"],[8,21,"gauge44"],[8,58,"gauge44"],[5,35,"gauge44"],[5,72,"gauge44"],[7,26,"gauge44"],[7,63,"gauge44"],[6,31,"gauge44"],[6,68,"gauge44"],[8,22,"gauge44"],[8,59,"gauge44"],[5,36,"gauge44"],[5,73,"gauge44"],[7,27,"gauge44"],[7,64,"gauge44"],[6,32,"gauge44"],[6,69,"gauge44"],[8,23,"gauge44"],[8,60,"gauge44"],[7,28,"gauge44"],[7,65,"gauge44"],[6,33,"gauge44"],[6,70,"gauge44"],[8,24,"gauge44"],[8,61,"gauge44"],[7,29,"gauge44"],[7,66,"gauge44"],[6,34,"gauge44"],[6,71,"gauge44"],[8,25,"gauge44"],[8,62,"gauge44"],[7,30,"gauge44"],[7,67,"gauge44"],[6,35,"gauge44"],[6,72,"gauge44"],[8,26,"gauge44"],[8,63,"gauge44"],[7,31,"gauge44"],[7,68,"gauge44"],[6,36,"gauge44"],[6,73,"gauge44"],[8,27,"gauge44"],[8,64,"gauge44"],[7,32,"gauge44"],[7,69,"gauge44"],[8,28,"gauge44"],[8,65,"gauge44"],[7,33,"gauge44"],[7,70,"gauge44"],[8,29,"gauge44"],[8,66,"gauge44"],[7,34,"gauge44"],[7,71,"gauge44"],[8,30,"gauge44"],[8,67,"gauge44"],[7,35,"gauge44"],[7,72,"gauge44"],[8,31,"gauge44"],[8,68,"gauge44"],[7,36,"gauge44"],[7,73,"gauge44"],[8,32,"gauge44"],[8,69,"gauge44"],[8,33,"gauge44"],[8,70,"gauge44"],[8,34,"gauge44"],[8,71,"gauge44"],[8,35,"gauge44"],[8,72,"gauge44"],[8,36,"gauge44"],[8,73,"gauge44"]]

research/shared-kernel-pair-concentration/EXACT-MOMENT.json

@@ -0,0 +1,28 @@
+{
+  "status": "PASS_INDEPENDENT_EXACT_PAIR_MOMENT",
+  "complex_lower": "86004870116989085803/50000000000000000000000",
+  "root_bracket_30": [
+    "1720097402339781716060441963/1000000000000000000000000000000",
+    "430024350584945429015110491/250000000000000000000000000000"
+  ],
+  "kappa_rational": "17200974023397817160599999999999999999999998999999999999999999999999/10000000000000000000000000000000000000000000000000000000000000000000000",
+  "kappa_decimal_90": "0.0017200974023397817160599999999999999999999998999999999999999999999999",
+  "baseline_rational": "17200966286848326009719999999999999999999998999999999999999999999999/10000000000000000000000000000000000000000000000000000000000000000000000",
+  "gain_rational": "48353434319693/62500000000000000000000",
+  "gain_decimal_90": "7.73654949115088E-10",
+  "controls": {
+    "old_doubled_profile_rejected_at_candidate_endpoint": true,
+    "next_endpoint_grid_point_rejected": true
+  },
+  "profile": {
+    "1": 1611720,
+    "2": 427573,
+    "3": 183550,
+    "4": 85248,
+    "5": 26196,
+    "8": 5328,
+    "16": 1,
+    "48": 26758
+  },
+  "scope": "Directed integer atanh and exp enclosures; no floating point. Complete hosting and outer release required separately."
+}

research/shared-kernel-pair-concentration/EXPERIMENTS.md

@@ -0,0 +1,37 @@
+# Experiment log
+
+Session: 2026-10-16, approximately 03:37–04:30 UTC. Default repository budget:
+about 60 minutes, no paid external compute, at most two native audit shards per
+replay. Source snapshots and command records include exact argv, exit codes,
+environment, elapsed time and log SHA256. Search seed: 20261016.
+
+| Step | Hypothesis / action | Result and decision |
+| --- | --- | --- |
+| Baseline | Paginated live PR census; reproduce PR2853 d01045df after distinguishing multiplication kappa from local/Fourier caps | Complete release passed in 838.88 s with four fresh native chains. |
+| H1a | Remaining 12 helpers in the four dirty-A quartets might admit extra dirty entrance lines | All 12 failed the inherited exact D-in-span census with climb and raise enabled. |
+| H1b | A coupled invertible raw-dirt transform within each fixed quartet could make two compensation columns vanish | Independent exact rational propagation: rank 3 and nullity 1 in every quartet, both providers. At most one zero column under an invertible 4x4 change at the fixed boundary. This does not exclude interleaved gates, changed receiving helpers or new frames. Controls raise rank to four / erase it to zero. |
+| H2 | Same-call distinct-width exchanges in PR2853's changed inventory may lower the idle bill | 66,685,248 pairs across two passes; two legal swaps, exact delta H3-H4-H6+H7. Independent full owner and 3000-digit moment checks passed. Complete release passed in 520.38 s. Kappa 0.00171937773626898616…; gain 7.75713995049e-11 over PR2853. Superseded by new PR2856/2857. |
+| H3 | Re-derive T248 composition for PR2853 | Not pursued after the new frontier appeared. No compatibility or summed-gain claim. |
+| Refresh | PR2857 0b2e2537 appears with cheaper staged kernels and a T37 fill | Its full documented reproduction passed twice. The second used its exact pinned dependencies; 499.15 s. Two current native chains fresh, older parent/native evidence explicitly authenticated and reused. |
+| H4 | The same exact pair-exchange method might improve PR2857 | 16,671,312 distinct-width same-call pairs; zero improving moves. This does not prove global allocation optimality. |
+| H5 | Two interleaved T37 copies permit a cross-copy transfer unavailable to a same-call swap | One width-7 transfer replaces 2H9 by H2+H16. Independent event/owner checks, exact moments and complete strict release pass. Final gain 7.73654949115088e-10 over exact PR2857. |
+
+The complete command stream is in `evidence/run-logs/`. `generate.py` reproduces
+H5 without a solver. The previous search/checker programs and receipts are in
+the saved session handoff bundle; relevant negative scripts are in `experiments/`.
+
+Development failures are retained: the first high-precision endpoint command
+used a nonexistent profile filename; the first paired-owner checker used the
+uncompressed name of a compressed pinned plan; the first paired-moment binary
+search began outside its deliberately narrow exponential-domain guard. These
+were corrected by supplying the actual filename and a certified initial root
+bracket. No mathematical predicate, guard or expected result was weakened.
+The complete inherited candidate verifier passed on its first run.
+
+The earlier PR2853 candidate's frozen CLAIM metadata says admission was pending
+when frozen. Its later PASS_RELEASE receipt is the authority for the completed
+run; frozen source was not edited after verification. It remains superseded.
+
+No further large fixed-inventory search was started. PR2857's reported tight
+fractional cap leaves only about 4.18e-9 above its original witness; this result
+uses about 0.774e-9 of that. A remaining relaxation gap is not a feasible witness.