|
| 1 | +# Faster exact balanced-Fano replay |
| 2 | + |
| 3 | +This tooling change accelerates the existing exhaustive check of the historical |
| 4 | +10-role, 14-gate balanced-Fano model. It preserves the negative result and its |
| 5 | +complete ordered enumeration. It does not extend the search domain or claim a |
| 6 | +new κ. The selected conditional result remains #626 with #543, exactly |
| 7 | +`51110230636731/31250000000000000`, at the base commit below. |
| 8 | + |
| 9 | +The production change is confined to |
| 10 | +[`balanced_fano.py`](../../scripts/experiments/balanced_fano.py). Each local |
| 11 | +binary operation now acts on a packed column representation, avoiding a fresh |
| 12 | +10-by-10 transpose at every leaf. The matching table retains each first prefix |
| 13 | +word; its matrix is reconstructed only when recovering a witness. |
| 14 | + |
| 15 | +## Reproduce |
| 16 | + |
| 17 | +From the repository root, using Python 3.11 or later and no third-party packages: |
| 18 | + |
| 19 | +```sh |
| 20 | +python3 -B research/balanced-fano-performance/benchmark.py --rounds 5 |
| 21 | +``` |
| 22 | + |
| 23 | +Expected: `PASS_IDENTICAL_COMPLETE_RESULTS`, with **279,936 prefixes**, |
| 24 | +**258,156 distinct prefix keys**, **279,936 inverse suffixes**, no witness, |
| 25 | +and these unchanged stream hashes: |
| 26 | + |
| 27 | +```text |
| 28 | +prefix b34379c5feeb67216fb7531294f13da5f67ce4a22f92b94ff8ea2b26f3aa21ec |
| 29 | +suffix a19c1f14c463451e7bdd0900a2aeae701d98bcee790e9145d70e05c316555c38 |
| 30 | +``` |
| 31 | + |
| 32 | +Each sample runs in a fresh process. The two implementations run sequentially |
| 33 | +in alternating order, fixed by assignment seed 91, on identical inputs. Every |
| 34 | +sample must match **every result field** in the original certificate, including |
| 35 | +counts, both hashes, witness and scope. The benchmark fails on a changed source |
| 36 | +pin, unequal result, or subprocess failure. It has no noisy timing threshold. |
| 37 | +The benchmark's RSS measurement supports macOS and Linux; the checker itself |
| 38 | +uses portable Python integers. Use `--output /path/to/new-result.json` to retain |
| 39 | +a new measurement without overwriting the shipped receipt. |
| 40 | + |
| 41 | +[`RESULT.json`](RESULT.json) records all local samples, medians, environment and |
| 42 | +exact implementation hashes. The measurement is for this fixed search, not the |
| 43 | +complete research suite, selected supplier replay, or multiplication runtime. |
| 44 | +OS caches were not flushed and no CPU affinity was imposed. |
| 45 | + |
| 46 | +The contributor name was corrected after measurement. `RESULT.json` records |
| 47 | +both the measured and updated hashes for the benchmark's attribution-only |
| 48 | +module-docstring edit. Its executable AST was checked unchanged after removing |
| 49 | +that docstring; all timing samples and mathematical results are retained. |
| 50 | + |
| 51 | +On CPython 3.13.2 / macOS arm64, five sequential pairs give median search time |
| 52 | +**5.969 → 2.051 seconds (2.91×)** and median peak process RSS |
| 53 | +**162,381,824 → 113,180,672 bytes (30.3% lower)**. These are measured local |
| 54 | +results, not guaranteed performance on other environments. |
| 55 | + |
| 56 | +Additional checks: |
| 57 | + |
| 58 | +```sh |
| 59 | +python3 -B -m unittest discover -s tests -p 'test_balanced_fano_performance.py' -v |
| 60 | +python3 -B -m unittest discover -s tests -p 'test_stronger_screens.py' -v |
| 61 | +python3 -B -S scripts/audit_stronger_screens.py |
| 62 | +make selected-record-check |
| 63 | +``` |
| 64 | + |
| 65 | +The audit regenerates only `certificates/stronger-rank-screens.json`. Its sole |
| 66 | +change is the SHA256 binding for the optimized source. A test restores that one |
| 67 | +old binding and requires the entire serialized certificate to match its |
| 68 | +original SHA256, so other certificate differences cannot pass unnoticed. |
| 69 | + |
| 70 | +Local validation also passed `PYTHONDONTWRITEBYTECODE=1 make verify-tests`: |
| 71 | +555 tests in 85 isolated modules and the existing patch-application checks. |
| 72 | +The six added tests also pass under `python3 -B -O`. See |
| 73 | +[`VALIDATION.json`](VALIDATION.json) for the precise coverage. Full `make verify` |
| 74 | +and the selected supplier cold replay were not rerun for this historical-checker |
| 75 | +change; unrelated artifacts were not regenerated. Remote CI is separate from |
| 76 | +this local evidence. |
| 77 | + |
| 78 | +## Why the enumeration is identical |
| 79 | + |
| 80 | +For a binary matrix `M` with `W` rows, encode its columns as |
| 81 | + |
| 82 | +```text |
| 83 | +S = sum(M[i,j] * 2**(W*j+i) for i,j in range(W)). |
| 84 | +U = sum(2**(W*j) for j in range(W)). |
| 85 | +``` |
| 86 | + |
| 87 | +The masks `(S >> a) & U` and `(S >> b) & U` extract rows `a` and `b` |
| 88 | +into the same column-start positions. XOR therefore adds those two rows over |
| 89 | +F2 simultaneously in every column. Clearing only `U << a` and `U << b` and |
| 90 | +placing the two selected linear combinations in those positions gives exactly |
| 91 | +the old local row operation. The positions are disjoint because `a != b` and |
| 92 | +both are in `[0,W)`. Python integers have arbitrary precision; this uses no |
| 93 | +fixed-width truncation or approximate arithmetic. |
| 94 | + |
| 95 | +The identity uses bits `i*(W+1)`. Induction on the unchanged depth-first GL2 |
| 96 | +choice order shows that each leaf has the same word and matrix as before. |
| 97 | +Reading each W-bit block yields the old `columns(rows)` tuple. Thus prescribed |
| 98 | +columns, sorted free columns, packed keys, first-prefix selection, stream |
| 99 | +order and both hashes remain identical. There is no pruning, orbit reduction, |
| 100 | +sampling, memoized result reuse, or changed stopping rule. |
| 101 | + |
| 102 | +When keys match, replaying the retained first prefix word reconstructs its |
| 103 | +original columns exactly. The suffix inversion and full recovered-permutation |
| 104 | +checks are unchanged. Half-enumeration budgets and invalid-terminal/port |
| 105 | +rejections run before enumeration as before. |
| 106 | + |
| 107 | +The existing meet-in-the-middle argument still covers all `6**14 = 78,364,164,096` |
| 108 | +complete local assignments via the two `6**7` streams. The absence of a match |
| 109 | +excludes only this fixed balanced topology, with its three prescribed |
| 110 | +terminals and free permutation of the other seven roles. It does not exclude |
| 111 | +other Fano completions, larger gates, or different terminal obligations. |
| 112 | + |
| 113 | +## Evidence and provenance |
| 114 | + |
| 115 | +- Exact base: `66849e1475c930fd7732b1a0067ffee7e1e95f60`. |
| 116 | +- The reference is the byte-for-byte original `balanced_fano.py`, last changed |
| 117 | + by `d55bcd62ceb8f322bcf311a5a66e94c3ac7724f0`; its SHA256 and shared dependencies |
| 118 | + are pinned in [`SOURCE.json`](SOURCE.json). No pending PR code is required. |
| 119 | +- Tests compare every `(columns, word)` pair in both full historical streams, |
| 120 | + not only their final hashes. Independent dense matrix controls cover widths |
| 121 | + 2, 3, 5, 9, 16, 33 and 65, including integer limb and byte boundaries. |
| 122 | +- Seeded small-model comparisons cover complete result dictionaries, positive |
| 123 | + witnesses, first matching suffixes, empty words, repeated/reversed ports, |
| 124 | + fixed/free terminals and negative cases. Existing tests independently exhaust |
| 125 | + 9,294 complete dense assignments. |
| 126 | +- A missing-leaf mutation still reports no completion, but changes both counts |
| 127 | + and hashes and is rejected by the receipt comparison. Invalid inputs and an |
| 128 | + exhausted half budget retain the original exceptions; budget exhaustion is |
| 129 | + never reported as a negative mathematical result. |
| 130 | + |
| 131 | +[`CLAIM.json`](CLAIM.json) records assignment seed 91, candidate selection and |
| 132 | +overlap review. No pinned sprint coordination issue existed. Nearby PRs #367, |
| 133 | +#452, #662, #667, #672, #707, #709 and #721 address other algebra, producer, |
| 134 | +geometry, arithmetic or archive checks. This contribution replays the already |
| 135 | +closed Fano model more efficiently; it is not a renewed search. |
| 136 | + |
| 137 | +No selected construction, `upstream/`, theorem claim or inherited compiler, |
| 138 | +hosting, precision, tape, or analytic assumption changes. These are exact |
| 139 | +finite checks and an implementation equivalence argument, not a formal proof |
| 140 | +of the full multiplication theorem. Attribution and AI disclosure are in |
| 141 | +[`NOTICE.md`](NOTICE.md). |
0 commit comments