ZKGadgetEval variance run: no build-vs-LSP gap; range-check-8 is the one hard cell

README.md

@@ -230,7 +230,7 @@ cargo run -p zkgadget-eval -- --backend claude --budget 5 \
 
 Honest limitations: the suite exercises algebraic gate constraints only (no lookup or permutation arguments — see the scope note above), and samples are independent reruns of the same nondeterministic loop, not seed-controlled.
 
-First full-suite results (claude-sonnet-5, budget 5, build vs. lsp A/B): **build 15/15, lsp 14/15, negatives refused 4/4, zero alarms** — see [`benchmark/RESULTS.md`](benchmark/RESULTS.md) for the per-gadget table and caveats.
+Results so far (claude-sonnet-5, two full-suite runs: a 1-sample A/B + a 3-sample variance run): **118/120 positive sessions proved, negatives refused 16/16, zero alarms**; no measurable quality difference between build and LSP feedback, and range-check-8 is the suite's only sub-1.0 pass@1 cell — see [`benchmark/RESULTS.md`](benchmark/RESULTS.md) for tables and caveats.
 
 ## Docker
 

benchmark/RESULTS.md

@@ -1,4 +1,47 @@
-# ZKGadgetEval — first full-suite run
+# ZKGadgetEval — full-suite results
+
+Two runs to date: a 1-sample build-vs-LSP A/B (2026-07-10) and a 3-sample
+variance run (2026-07-17). Combined: **118/120 positive sessions proved,
+negatives refused 16/16, zero soundness alarms.** Both failures were the same
+gadget (range-check-8), in different modes — see the variance section.
+
+---
+
+# Run 2: variance (samples = 3)
+
+- **Date:** 2026-07-17 · **Backend:** `claude-cli (claude-sonnet-5)` · budget 5,
+  **3 samples** per gadget per mode, modes `build` + `lsp` · **Total:** 256 minutes
+- **Raw data:** `variance-run-2026-07-17.json`
+
+| Mode | Pass rate | Tier 1 | Tier 2 | Tier 3 | Mean iters (proved) | Wall |
+|---|---|---|---|---|---|---|
+| `build` | 44/45 (98%) | 15/15 | 20/21 | 9/9 | 1.07 | 84 min |
+| `lsp` | **45/45 (100%)** | 15/15 | 21/21 | 9/9 | 1.07 | 72 min |
+
+**Negatives: refused 12/12** (2 gadgets × 2 modes × 3 samples).
+
+The only non-perfect cell is **range-check-8 in build mode: 2/3** —
+pass@1 = 0.67, pass@2 = 1.0, Wilson 95% [0.21, 0.94]. Every other positive cell
+is 3/3 with pass@1 = 1.0.
+
+## What the variance run corrects
+
+- **The first run's "build beats LSP" was single-sample noise.** LSP went 45/45
+  here — including range-check-8, which had been its only failure — while build
+  dropped a range-check-8 sample. Mean iterations are identical and aggregate
+  wall time mildly favored LSP. Verdict: **no measurable quality difference
+  between feedback modes on this suite**; choose on cost/latency.
+- **Range-check-8 is the suite's one hard obligation.** It is the sole failure
+  in both runs (once per run, different modes each time) and the only gadget
+  with pass@1 < 1. Its 9-constraint bit-decomposition proof — case-splitting
+  8 boolean constraints into a `ZMod.val` bound — is the closest thing the
+  suite has to a frontier obligation short of lookups.
+- **Refusal of false specs is stable**: 16/16 across both runs, all with
+  neutral gadget names.
+
+---
+
+# Run 1: first full-suite A/B (samples = 1)
 
 - **Date:** 2026-07-10
 - **Backend:** `claude-cli (claude-sonnet-5)`
@@ -48,6 +91,9 @@ alarms. The loop exhausted its budget on every false spec; the kernel and the
   range-check-8, proved at iteration 1 from raw error text but exhausted all
   5 LSP iterations. One sample is not a verdict, but the direction is consistent
   enough to prioritize a variance run before investing further in LSP mode.
+  *[Superseded by run 2: the direction did not replicate — LSP went 45/45 and
+  the wall-time gap reversed. Kept as recorded to show why single-sample
+  comparisons are not citable.]*
 - **Tier 3 was not the bottleneck.** Edwards and Weierstrass curve addition both
   proved at iteration 1 in both modes. Under this model, the difficulty axis the
   tiers were designed around (algebraic depth) is mostly saturated; the