Accelerate complete E7 classification replay 17.5x with exact bit lanes

research/e7-bitsliced-exhaustion/BENCHMARK.json

@@ -0,0 +1,52 @@
+{
+  "python": "3.12.14 (main, Aug 25 2026, 13:50:33) [Clang 22.1.3 ]",
+  "platform": "macOS-26.6.1-arm64-arm-64bit",
+  "command_flags": [
+    "-I",
+    "-B"
+  ],
+  "serial": true,
+  "records": [
+    {
+      "implementation": "old",
+      "seconds": 15.090498709003441,
+      "stdout_sha256": "2853012eeacb5e0354e938bc1a137fb4790db281967da8e454fa5f30366a15c4",
+      "stderr_sha256": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855"
+    },
+    {
+      "implementation": "new",
+      "seconds": 0.7883416670374572,
+      "stdout_sha256": "2853012eeacb5e0354e938bc1a137fb4790db281967da8e454fa5f30366a15c4",
+      "stderr_sha256": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855"
+    },
+    {
+      "implementation": "new",
+      "seconds": 0.8870171670569107,
+      "stdout_sha256": "2853012eeacb5e0354e938bc1a137fb4790db281967da8e454fa5f30366a15c4",
+      "stderr_sha256": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855"
+    },
+    {
+      "implementation": "old",
+      "seconds": 13.816090291016735,
+      "stdout_sha256": "2853012eeacb5e0354e938bc1a137fb4790db281967da8e454fa5f30366a15c4",
+      "stderr_sha256": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855"
+    },
+    {
+      "implementation": "old",
+      "seconds": 13.72491204191465,
+      "stdout_sha256": "2853012eeacb5e0354e938bc1a137fb4790db281967da8e454fa5f30366a15c4",
+      "stderr_sha256": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855"
+    },
+    {
+      "implementation": "new",
+      "seconds": 0.723674124921672,
+      "stdout_sha256": "2853012eeacb5e0354e938bc1a137fb4790db281967da8e454fa5f30366a15c4",
+      "stderr_sha256": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855"
+    }
+  ],
+  "median_seconds": {
+    "old": 13.816090291016735,
+    "new": 0.7883416670374572
+  },
+  "speed_ratio": 17.525510662067134
+}

research/e7-bitsliced-exhaustion/PROOF.md

@@ -0,0 +1,118 @@
+# Exact binary-code exhaustion in bit lanes
+
+Ali Romman, with substantial OpenAI Codex assistance. Apache-2.0.
+
+## Claim and consumer
+
+Let g_0,...,g_(d-1) be independent vectors in F2^n. Encode each vector as a
+nonnegative integer with at most n bits. For 0 <= w <= n, `low_weight_words`
+returns every word of their span with Hamming weight at most w, exactly once.
+It includes zero. There is no assumption about the code, its minimum distance,
+the generator order, or the relation between n and a machine word width.
+The input check rejects dependent generators and malformed bounds.
+
+The complete E7 classifier from PR5669 uses this function with n=63, d=27,
+and w=12. It checks that zero and exactly 1,638 weight-twelve words remain.
+Thus every nonzero word has weight at least twelve and all equality supports
+are retained. The bound, equality theorem and all geometric conclusions are
+the predecessor's results. This package changes their exact replay method.
+
+## Coefficient partition
+
+Set k=min(batch_bits,d) and L=2^k. Number lanes by integers a in [0,L).
+The integer mask has a one at each of those L positions. For each j<k, the
+coefficient pattern has bit a equal to bit j of a. The geometric-series
+formula in the implementation repeats a block of 2^j zero bits followed by
+2^j one bits. Its period divides L. Integer multiplication concatenates
+these disjoint blocks; it cannot create a carry between them.
+
+For each coordinate i, XOR the coefficient patterns whose generator g_j
+has coordinate i equal to one. Lane a now holds coordinate i of the low
+coefficient sum. Gray traversal enumerates every coefficient vector on
+g_k,...,g_(d-1) exactly once. At step t>0 it changes the generator indexed
+by the least significant one bit of t. Induction gives the usual Gray word
+t XOR floor(t/2), a bijection on all high coefficients.
+
+For a fixed high sum h, XOR the full lane mask at coordinate i precisely
+when h_i=1. Each lane is now one complete codeword. Every coefficient vector
+appears in exactly one batch and lane. Independence makes their images
+distinct. No pruning or sampling occurs.
+
+## Weight addition and comparison
+
+For three one-bit operands a,b,c in one lane, set
+
+```text
+s = a XOR b
+sum_bit = s XOR c
+carry_bit = (a AND b) OR (s AND c).
+```
+
+The integer identity a+b+c=sum_bit+2*carry_bit holds in each of the eight
+cases. Every operation is bitwise, so the same identity holds separately
+in every lane. The program keeps carry bits in a separate plane of twice
+the weight; it never shifts them into another lane. Two operands use the
+same half-adder identity. At each level, these steps reduce the operand
+list and send carries to the next level. They terminate with the exact
+binary expansion of each lane's Hamming weight.
+
+The comparator scans those planes from high to low. `equal` contains the
+lanes whose prefix equals the bound prefix; `less` contains those already
+strictly smaller. If the next bound bit is one, zero lanes leave `equal`
+and enter `less`. If it is zero, one lanes leave `equal` without entering
+`less`. This invariant proves that `less OR equal` contains exactly weights
+at most w. The final mask removes all positions outside the finite lane set.
+If the bound exceeds the largest representable value, every lane qualifies.
+
+For each retained lane, the program reconstructs the literal XOR of the
+chosen low generators and h. This is its exact input word. Zero dimension,
+zero width, zero weight, and a bound equal to n follow from the same rules.
+
+## Resource bound and scope
+
+The public batch parameter is an integer in 1..20, with default 16. Input
+dimension and width have no fixed cap. The plane storage is O(n*2^k) bits,
+in addition to O(nd) bits for generators and elimination. Outputs are yielded
+one at a time. The E7 default uses 2,048 batches of 65,536 lanes; it does not
+store a 134-million-entry word table.
+
+Each batch uses O(n) Boolean adder operations and O(log(n+1)) comparison
+operations on L-bit integers. Input planes require O(nk) such operations.
+Literal output reconstruction costs at most d vector XORs per output.
+The coefficient space is still exponential in d. This is an exact arithmetic
+implementation improvement, not a polynomial algorithm for minimum distance.
+Python object overhead and integer operations remain positive costs.
+
+## Full replay boundary
+
+The source archive is retained byte for byte. The derived `classify.py`
+differs from the source verifier at only `HERE` and `minimum_supports`.
+The first locates the retained archive; the second calls the new engine.
+The registered check compares every other Python syntax node exactly.
+It then runs the complete derived check and compares every field of the
+source receipt. All 63 reflection maps, all 135 frames, rational lift and
+quadratic ranks, all 120 ambient slices, omission controls and rejection
+controls remain active. There is no runtime replacement of a function and
+no cache of source results.
+
+The independent small oracle constructs spans by literal list doubling and
+uses integer Hamming weights. It covers all 1,381 independent unordered
+generator sets in F2^4, all five weight bounds, and five batch sizes: 34,525
+comparisons. Separate tests cover widths through 127, malformed domains,
+changed bases, changed bounds and a full changed basis for the E7 code.
+These finite checks corroborate the general lane argument above.
+
+## Relevance and attribution
+
+E7 support exhaustion is used in the E8 deletion and quadratic-extension
+work. Faster exact replays reduce the cost of checking those certificates
+and permit larger bounded code searches. The implementation does not alter
+the physical multiplication word, its paid profile or any selected bound.
+Complete kappa is unchanged.
+
+Credit Nick Petalas's PR5238 for the geometry, support theorem and binary
+code; Ali Romman's PR5669 for the equality classification and complete
+consumer; and the source's JoyboyBrian, Josie Elliston, Andrey Mas, Aaron
+Wang, Brett Halligan, themilkman216 and DreamingOfClouds lineage. All source
+notices remain in the retained archive. Boolean adders and bit-parallel
+enumeration are established methods; no literature-priority claim is made.

research/e7-bitsliced-exhaustion/README.md

@@ -0,0 +1,73 @@
+# Exact E7 exhaustion in bit lanes
+
+The complete E7 minimum-support classifier runs 17.53 times faster in the
+recorded local comparison: median 13.816 seconds becomes 0.788 seconds.
+All six fresh-process outputs are byte-identical. All 134,217,727 nonzero
+codewords remain covered. Complete kappa is unchanged.
+
+The [proof](PROOF.md) establishes the exact iterator for arbitrary independent
+binary generators. [binary.py](binary.py) computes Hamming weights in parallel
+integer bit lanes. [classify.py](classify.py) is the complete derived consumer.
+Only its source-root path and minimum-support function differ from the frozen
+verifier; the registered check compares every other syntax node.
+
+[RESULT.json](RESULT.json) records all scientific checks.
+[BENCHMARK.json](BENCHMARK.json) records alternating fresh-process timings on
+Python 3.12.14, macOS arm64. [VALIDATION.md](VALIDATION.md) states the limits.
+[SOURCES.json](SOURCES.json) binds all eleven retained input files.
+
+## Reproduce
+
+From the repository root, with Python 3.12 and its standard library:
+
+```sh
+python3.12 -B scripts/research_package.py --package research/e7-bitsliced-exhaustion
+```
+
+Expected markers:
+
+```text
+PASS_E7_BITSLICED_EXHAUSTION
+PASS_REGISTERED_RESEARCH_PACKAGE
+```
+
+The registered verifier covers all 1,381 independent unordered generator sets
+in F2^4, all five weight bounds and five batch sizes: 34,525 comparisons.
+It also checks 108 wide-code cases, sixteen domain and invalidation controls,
+the full original classification result, and a second full E7 basis.
+The full classification retains all reflection, frame, rational-rank,
+ambient-pivot and corruption controls from the predecessor.
+
+For a separate timing run, use an output path outside the package:
+
+```sh
+python3.12 -I -B research/e7-bitsliced-exhaustion/benchmark.py --output /tmp/e7-timings.json
+```
+
+The timing command alternates three complete old and three complete new
+fresh-process replays on the same interpreter. It checks exact output equality.
+Runtime ratios are local measurements, not a universal hardware guarantee or
+a physical multiplication speedup. The iterator still exhausts an exponential
+coefficient space. Its bounded bit-lane storage avoids a full word table.
+
+## Credit and scope
+
+[PR #5669](https://github.com/CrocSwap/integer-mult-bounds/pull/5669), exact head
+700efb538a3d919409c9506d117846b7895b02ea, supplies the complete classification,
+consumer and receipt. Its retained [PR #5238](https://github.com/CrocSwap/integer-mult-bounds/pull/5238)
+source supplies Nick Petalas's frame-code geometry and minimum-support proof.
+The complete predecessor notices and attribution remain unchanged in `source/`.
+The new bit-lane implementation, proof and independent small-code oracle are
+by Ali Romman with substantial OpenAI Codex assistance. No subagents.
+Apache-2.0. The consumer uses the same assistant family as its predecessor;
+no independent human or proof-kernel acceptance is claimed.
+
+No new geometry bound, physical supplier, selected-frontier change or complete
+kappa gain is inferred. The value is faster exact verification for the E7/E8
+deletion and decoder work. No other consumer is silently changed.
+
+## Open next questions
+
+- Bind another actual deletion or decoder code to the iterator. Compare all
+  old checks and outputs, then measure its full replay. No other installation
+  or speed claim is included here.