From 7eaaa9f257d9bd1699cb39387fa2bd0feb7d3e63 Mon Sep 17 00:00:00 2001 From: igneum-labs <337424239+igneum-labs@users.noreply.github.com> Date: Fri, 9 Oct 2026 09:28:55 +0000 Subject: [PATCH] mhpow B4: name the open rows of the loss table by their section 6 items Co-Authored-By: Claude Opus 5.5 --- docs/analysis/mhpow/b4/README.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/docs/analysis/mhpow/b4/README.md b/docs/analysis/mhpow/b4/README.md index b8d4f65b3..91beca37a 100644 --- a/docs/analysis/mhpow/b4/README.md +++ b/docs/analysis/mhpow/b4/README.md @@ -230,8 +230,8 @@ rbcost(G, 20 delta m) - eps m c_b/2, for q <= 2^(n/(10 delta)) and |V| <= 2^(n/( | L7 | DRSample red-blue bound | (1 - rho)/16 of N c_b for m <= C' N^rho; nothing for m >= C N / log N | R2 Lemma 5.5, Thm 5.2, sec. 5.4 | constants not shown tight; the cut-off is a real pebbling | | L8 | combined L6 x L7 | >= 256/(1 - rho): 341x at rho = 0.25, 512x at 0.5 | params.txt sec. 5 | needs new theorems | | L9 | RO instantiated by a permutation (only if used) | eps/(40 delta), cache 20 delta m | R16 Thm 1 | B1's choice | -| L10 | MTP certificate instead of full evaluation | unknown | none (open) | B4 obligation O1, O2 | -| L11 | amortisation across instances | unknown for terms 2 and 3; none for term 1 | none (open) | B4 obligation O6 | +| L10 | MTP certificate instead of full evaluation | unknown | none (open) | section 6, NEW items 1 and 2 (row B4-B04) | +| L11 | amortisation across instances | unknown for terms 2 and 3; none for term 1 | none (open) | section 6, NEW item 6 | | L12 | technology coefficients | each must be a lower bound over the permitted set; an estimate is not a bound | plan sec. 8 | evidence work, not proof | The arithmetic consequence (params.txt sec. 7): if the composed theorem proves only L = E_honest / loss, a 1.5x certificate needs