|
| 1 | +# Independent review of open κ claims, 11 October 2026 |
| 2 | + |
| 3 | +This review checks the open CrocSwap pull requests that claim a conditional |
| 4 | +exponent above the reviewed gen4 result. It follows the verifier-first practice |
| 5 | +of Georgiev, Gómez-Serrano, Tao and Wagner, *Mathematical exploration and |
| 6 | +discovery at scale* (arXiv:2511.02864): assume a search may exploit its |
| 7 | +verifier, replay every claim from a fresh extract, and recompute the score by |
| 8 | +code that the claim does not ship. Negative results are recorded in |
| 9 | +[NEGATIVE-RESULTS.md](NEGATIVE-RESULTS.md). |
| 10 | + |
| 11 | +Scope: finite replay and exact arithmetic only. The original #109 framework, the |
| 12 | +all-size compiler, chart, routing, restored-row, prime-supply, precision/recovery |
| 13 | +and analytic interfaces, and every unmerged predecessor these PRs vendor, remain |
| 14 | +assumptions. Nothing here is a formal proof or a human peer review. PR replays |
| 15 | +for #355–#365 were performed by delegated Claude subagents in this session and |
| 16 | +spot-checked as noted; the gen4 and #366 replays and the independent #366 |
| 17 | +score were run directly. |
| 18 | + |
| 19 | +## Results |
| 20 | + |
| 21 | +All runs used Python 3.13, a fresh `git archive` extract of the PR head, and a new |
| 22 | +output directory. "Scorer" is [independent_bit_score.py](independent_bit_score.py): |
| 23 | +it recomputes every MOVE/COPY rank from frame dimensions, rejects a word whose |
| 24 | +rank fields disagree, and certifies the largest 10^-18 grid bit saving with its |
| 25 | +own exact rational log/exp enclosures. |
| 26 | + |
| 27 | +| PR | Head | Claimed κ | Replay | Scorer | Verdict | |
| 28 | +| --- | --- | --- | --- | --- | --- | |
| 29 | +| main (gen4) | `12a4934` | 90446448750933/1.25e17 ≈ 7.23572e-4 | PASS, 7m13s | — | reproduced | |
| 30 | +| #366 | `d3d8420` | 160987957846297/2e17 ≈ 8.04940e-4 | PASS, 8m42s | exact agreement | reproduced, caveats | |
| 31 | +| #364 | `f8c6a47` | 201219842699733/2.5e17 ≈ 8.04879e-4 | PASS, 6m21s | exact agreement | reproduced, caveats | |
| 32 | +| #362 | `f46ddb5` | 804849251275843/1e18 | PASS, 6m22s | exact agreement | reproduced, caveats | |
| 33 | +| #358 | `e76d7a9` | 80367971186626189473809/1e26 ≈ 8.03680e-4 | PASS, 744s | exact agreement | reproduced | |
| 34 | +| #356 | `c3d16f4` | 401580942485227026650141/5e26 ≈ 8.03162e-4 | PASS, 481s | exact agreement | reproduced | |
| 35 | +| #360 | `edef1a7` | 80351298055091/1e17 ≈ 8.03513e-4 | PASS after packaging fix | exact agreement | reproduced, packaging defect | |
| 36 | +| #355 | `e59117a` | 801967436473393/1e18 ≈ 8.01967e-4 | PASS after packaging fix | exact agreement | reproduced, packaging defect | |
| 37 | +| #365 | `a222705` | complex b = 876412559609473/1e18 | PASS, 2.7s | b reproduced | reproduced; κ unchanged | |
| 38 | +| #363 | `9df55da` | complex b = 932783231884153/1e18 | PASS, 9.9s | b reproduced | reproduced, new unproved layout; κ unchanged | |
| 39 | + |
| 40 | +Every bit-side claim is bound by the bit saving. The largest reproduced claim |
| 41 | +is #366, 11.25% above the reviewed gen4 result. |
| 42 | + |
| 43 | +## Findings |
| 44 | + |
| 45 | +**#366.** The final word's records hash, `b99fa242…`, equals the PR's |
| 46 | +`EXPECTED.json`. The scorer reproduces the bit saving 402794119831239/5e17, and |
| 47 | +the bit→κ map recomputed separately gives the claimed κ with the bit side binding |
| 48 | +(complex headroom ≈ 7.07e-5). Exact checks cover move/copy ranks against frames |
| 49 | +(`stagelib.check`), frame validity and `I-J/9` nondegeneracy, and rational moment |
| 50 | +enclosures with adjacent-grid rejection. Two scope points: |
| 51 | + |
| 52 | +- `price.py` uses a hard-coded default complex saving `b`; `complex_b.py` |
| 53 | + recomputes b from the E8 certificate but only prints it. We confirmed the |
| 54 | + printed value equals the default exactly. An assertion would close this. |
| 55 | +- `stagelib`'s column replay is over F2. Integer correctness of the signed lift |
| 56 | + rests on the columns checker's cancellation-free bound and inherited scalar |
| 57 | + evidence. |
| 58 | + |
| 59 | +The 47 outer inequalities are asserted by the PR's own `outer.py`; they were not |
| 60 | +recomputed independently. |
| 61 | + |
| 62 | +**#364 / #362.** `verify.sh` asserts the recomputed complex b. In this lineage |
| 63 | +`data/parity` is the PR's own regenerated base word, so "new frames" counts are |
| 64 | +relative to it, not to #325, and the README's "1,064 frames new relative to |
| 65 | +#325" is copied from #359. `stagelib.full_check` still checks every used frame |
| 66 | +of the final word, and nondegeneracy rechecked against the true #325 frames |
| 67 | +(8838 differing frames) found none degenerate. Several `cmd && echo` lines under |
| 68 | +`set -e` would not stop on failure; all printed in this replay. The producer |
| 69 | +regeneration scripts reference paths outside the package. |
| 70 | + |
| 71 | +**#358 / #356.** `legality.cpp` rejects a MOVE/COPY rank that differs from its |
| 72 | +frame dimension; the native 24-stage admission is actually executed. The audit's |
| 73 | +`assembly.py` reads its root from `REFINEMENT.json`; an independent 1e-27 root |
| 74 | +reproduced the claimed κ exactly. The exact integer operator check excludes |
| 75 | +MOVEs, which the native geometry check covers. |
| 76 | + |
| 77 | +**#360 / #355.** Both packages' `MANIFEST.json` pin a `.gitattributes` that is not |
| 78 | +committed, so the documented `verify.py` fails on a fresh checkout with |
| 79 | +"Package source missing, changed or unlisted". Replays used a copy with only |
| 80 | +that manifest entry removed. Integer correctness is checked over Z against the |
| 81 | +source word (int128 with overflow guards); the source words are compacted forms |
| 82 | +of unmerged #351/#354 words whose conversion is not replayed. |
| 83 | + |
| 84 | +**#365 / #363.** Both start from Sussman's identical `gcert1-e8-r783` certificate. |
| 85 | +Neither changes κ: running #366's `outer.assembly` with b equal to the old value, |
| 86 | +#365's or #363's gives the same κ, since the bit side binds. #363's seven-stage |
| 87 | +bridged layout B₃ has no written or Lean proof (Sussman's bridge certificate covers |
| 88 | +the five-stage layout) and inherits five-stage row constants. If admitted, it raises |
| 89 | +the complex cap to ≈ 9.33e-4, so bit-side gains up to that cap would count. |
| 90 | + |
| 91 | +## Reproduce |
| 92 | + |
| 93 | +```sh |
| 94 | +git fetch https://github.com/CrocSwap/integer-mult-bounds.git pull/366/head:pr366 |
| 95 | +git archive pr366 research/w3-design-t-mc-coupled-retiming | tar -x -C /tmp/pr366src |
| 96 | +python3 -B /tmp/pr366src/research/w3-design-t-mc-coupled-retiming/verify.py /tmp/pr366out |
| 97 | +python3 -I research/independent-review/independent_bit_score.py /tmp/pr366out/candidate \ |
| 98 | + 402794119831239/500000000000000000 |
| 99 | +``` |
| 100 | + |
| 101 | +Requires numpy, mpmath, a C++17 compiler and Boost headers. The receipt is |
| 102 | +[receipts/pr366.json](receipts/pr366.json). |
0 commit comments