igneum-network/igneum
1
0
Fork 0
Code Issues Pull requests Releases Activity

mhpow B4: name the open rows of the loss table by their section 6 items

Browse source 
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
This commit is contained in:
igneum-labs 2026-10-09 09:28:55 +00:00
parent add70b655e
commit 7eaaa9f257
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
docs/analysis/mhpow/b4/README.md
View file

@ -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