Reduce complete E7 replay time by 21.55% (no new κ)

research/e7-intersection-counters/BENCHMARK.json

@@ -0,0 +1,112 @@
+{
+  "python": "3.12.15 (main, Oct 14 2026, 00:55:37) [Clang 23.1.3 ]",
+  "executable": "/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12",
+  "platform": "macOS-27.0.1-arm64-arm-64bit",
+  "cpu_count": 18,
+  "load_average": [
+    3.92578125,
+    3.45361328125,
+    2.77392578125
+  ],
+  "errors": 0,
+  "serial": true,
+  "command_flags": [
+    "-I",
+    "-W",
+    "error",
+    "-B"
+  ],
+  "records": [
+    {
+      "engine": "original",
+      "seconds": 0.37083045789040625,
+      "returncode": 0,
+      "stdout_sha256": "2853012eeacb5e0354e938bc1a137fb4790db281967da8e454fa5f30366a15c4",
+      "stderr_bytes": 0
+    },
+    {
+      "engine": "intersection",
+      "seconds": 0.29308387520723045,
+      "returncode": 0,
+      "stdout_sha256": "2853012eeacb5e0354e938bc1a137fb4790db281967da8e454fa5f30366a15c4",
+      "stderr_bytes": 0
+    },
+    {
+      "engine": "original",
+      "seconds": 0.3668871249537915,
+      "returncode": 0,
+      "stdout_sha256": "2853012eeacb5e0354e938bc1a137fb4790db281967da8e454fa5f30366a15c4",
+      "stderr_bytes": 0
+    },
+    {
+      "engine": "intersection",
+      "seconds": 0.2906480410601944,
+      "returncode": 0,
+      "stdout_sha256": "2853012eeacb5e0354e938bc1a137fb4790db281967da8e454fa5f30366a15c4",
+      "stderr_bytes": 0
+    },
+    {
+      "engine": "original",
+      "seconds": 0.3726658751256764,
+      "returncode": 0,
+      "stdout_sha256": "2853012eeacb5e0354e938bc1a137fb4790db281967da8e454fa5f30366a15c4",
+      "stderr_bytes": 0
+    },
+    {
+      "engine": "intersection",
+      "seconds": 0.29022570815868676,
+      "returncode": 0,
+      "stdout_sha256": "2853012eeacb5e0354e938bc1a137fb4790db281967da8e454fa5f30366a15c4",
+      "stderr_bytes": 0
+    },
+    {
+      "engine": "original",
+      "seconds": 0.3703519580885768,
+      "returncode": 0,
+      "stdout_sha256": "2853012eeacb5e0354e938bc1a137fb4790db281967da8e454fa5f30366a15c4",
+      "stderr_bytes": 0
+    },
+    {
+      "engine": "intersection",
+      "seconds": 0.291430874960497,
+      "returncode": 0,
+      "stdout_sha256": "2853012eeacb5e0354e938bc1a137fb4790db281967da8e454fa5f30366a15c4",
+      "stderr_bytes": 0
+    },
+    {
+      "engine": "original",
+      "seconds": 0.3705076249316335,
+      "returncode": 0,
+      "stdout_sha256": "2853012eeacb5e0354e938bc1a137fb4790db281967da8e454fa5f30366a15c4",
+      "stderr_bytes": 0
+    },
+    {
+      "engine": "intersection",
+      "seconds": 0.2877717078663409,
+      "returncode": 0,
+      "stdout_sha256": "2853012eeacb5e0354e938bc1a137fb4790db281967da8e454fa5f30366a15c4",
+      "stderr_bytes": 0
+    }
+  ],
+  "median_seconds": {
+    "original": 0.3705076249316335,
+    "intersection": 0.2906480410601944
+  },
+  "range_seconds": {
+    "original": [
+      0.3668871249537915,
+      0.3726658751256764
+    ],
+    "intersection": [
+      0.2877717078663409,
+      0.29308387520723045
+    ]
+  },
+  "reduction": 0.21554099969244866,
+  "implementation_sha256": {
+    "engine.py": "882d0177e990b0534bb16ec188a622b6167051505bdb5a7b19b4462499a72e47",
+    "replay.py": "8cae6e46cc8ceddc9b1a714191750f00c39acca92a1b435ccea9accfcae4e1e8",
+    "benchmark.py": "ec0d4dbfe8231330af8b10378bce8d6e6f9a64c6ca6e2c503711d5bad921e24f",
+    "SOURCES.json": "1a7991ac02dcdd08338ff0d308a101b9aefd87dc2ab8cebc6d9d5dcb2d4a3fab"
+  }
+}

research/e7-intersection-counters/PROOF.md

@@ -0,0 +1,90 @@
+# Exact intersection counters for translated bit lanes
+
+This implementation proof was produced by Nick Petalas. Apache-2.0.
+
+## Model and reused machinery
+
+Ali Romman's PR5729 represents independent binary generators as integer
+bitsets. The first b generators define 2^b parallel lanes. For coordinate j,
+integer C_j has bit l equal to coordinate j of the low-generator word u_l.
+The remaining generators are traversed in binary reflected Gray order,
+producing an offset v. Lane l represents exactly u_l xor v.
+
+The new implementation retains that representation, assignment order,
+source population-plane adder, threshold selector and final word extraction
+order. It changes how the weight planes for one translated batch are formed.
+The statement here concerns this changed computation, not a new proof of
+the E7 classification or its geometry.
+
+## Weight identity
+
+For binary words u,v, count separately the coordinates where both are one.
+Their contribution is two to wt(u)+wt(v) and zero to wt(u xor v). A coordinate
+with just one set bit contributes one to both sides. Thus
+
+```text
+wt(u xor v) = wt(u) + wt(v) - 2 wt(u and v).
+```
+
+Compute the population planes for all u_l once, before the offset loop.
+For offset v, pass only the coordinate columns C_j with v_j=1 to the
+retained population-plane adder. In every lane this gives wt(u_l and v).
+The scalar wt(v) is obtained by ordinary integer popcount.
+
+`translated_planes` adds that scalar to the fixed wt(u_l) planes and
+subtracts twice the intersection count. The adder uses the usual full-adder
+parity/carry identity. The subtractor uses the ordinary full-subtractor
+borrow identity
+
+```text
+borrow_out = (not a and (b or borrow_in)) or (b and borrow_in).
+```
+
+All Boolean operations act independently on corresponding bits of the
+integer operands. Carries and borrows move to the next weight plane, never
+to another coefficient lane.
+
+Let k=bit_length(width). The implementation keeps the low k weight planes,
+so its arithmetic is modulo 2^k. Intermediate addition or subtraction can
+wrap. The final true weight is between zero and width, and width<2^k for
+positive width. Therefore its residue identifies the true weight uniquely.
+Width zero is a separate valid empty-word case: the threshold accepts the
+sole zero lane, with no weight plane needed.
+
+The retained `at_most` predicate consequently selects exactly the same
+lanes as the original translated-column population count. The high offset
+sequence and low-lane extraction order are identical. Independent generators
+make the assignment-to-word map injective, so every qualifying word is
+returned once, in the same order. No cached support set or classification
+result participates in this computation.
+
+## Complete caller preservation
+
+`replay.py` authenticates six source files and loads the unchanged PR5729
+`classify.py`. Its private `run_path` dispatch substitutes only the
+`low_weight_words` binding returned for that consumer's exact `binary.py`
+path. Every other load follows the original function. Both comparator
+modes use the same dispatch and authentication boundary.
+
+The source `main` still executes its complete `check`, including root/frame
+construction, ambient slices, support enumeration, reflections, rational
+ranks, orbit partition, all retained controls and comparison of the complete
+result dictionary with the pinned RESULT.json. Its two output lines are
+compared byte for byte between fresh original/intersection processes.
+No production source or predecessor certificate is modified.
+
+## Finite evidence and limits
+
+The verifier compares every independent unordered generator set in F2^4
+under every bound 0..4 and batch size 1..5. Its literal subset-XOR oracle
+checks contents; comparison with the source iterator also checks ordering.
+There are 1,381 sets and 34,525 complete comparisons, all enumerated.
+Another 108 fixed wide-code cases reach width 127. An independent scalar
+popcount check covers all 87,381 ordered pairs u,v over widths 0..8,
+including arithmetic wraparound. Sixteen rejected inputs and three changed
+input/bound histories exercise validation and absence of result caching.
+
+These tests corroborate the implementation proof. The complete caller
+checks preserve the predecessor computation rather than strengthen its
+scientific conclusion. Timings describe this host, not every environment.
+There is no new support bound, supplier, physical algorithm or kappa claim.

research/e7-intersection-counters/README.md

@@ -0,0 +1,137 @@
+# Faster complete E7 replay using intersection counters
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+Claim type: measured verifier improvement with a scoped equivalence proof
+and exact finite conformance. No new kappa is claimed.
+
+The complete current E7 classification replay has median time 0.290648 s
+with intersection counters, versus 0.370508 s with Ali Romman's PR5729
+bit-lane engine. That is a 21.55% reduction on this host. Five alternating
+fresh processes per engine have ranges 0.287772..0.293084 s and
+0.366887..0.372666 s, respectively. All ten outputs are byte-identical,
+with zero failures. [BENCHMARK.json](BENCHMARK.json) is the generated receipt
+with raw samples, interpreter/environment and implementation hashes.
+
+The new step uses
+
+```text
+wt(u xor v) = wt(u) + wt(v) - 2 wt(u and v).
+```
+
+It computes fixed lane weights once, then counts only columns selected by
+the changing offset. Exact bit-plane addition and subtraction recover every
+translated weight. [PROOF.md](PROOF.md) covers modular wraparound, every
+coefficient assignment and iterator order. All complete classification
+checks still run in the unchanged consumer.
+
+## Reproduce
+
+From the repository root, use CPython 3.12 and its standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/e7-intersection-counters/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -O -B research/e7-intersection-counters/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/e7-intersection-counters
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/e7-intersection-counters --check-source-history
+```
+
+Another CPython 3.12 path can replace this host's path. Expected markers are
+`PASS_E7_INTERSECTION_COUNTERS` and `PASS_REGISTERED_RESEARCH_PACKAGE`.
+Default replay writes no files and prints a generated receipt bound to all
+ten package files. The registered commands exercise normal and optimized
+Python, including two complete fresh scientific callers in each mode.
+
+For the opt-in accelerated complete replay:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/e7-intersection-counters/replay.py
+```
+
+Add `--engine original` for the current PR5729 comparator. To generate new
+local timings, run `benchmark.py --output /absolute/path/outside/package.json`
+with the same interpreter and flags. Timing includes process startup,
+source authentication, imports, complete code enumeration, all downstream
+classification checks, receipt comparison and output. The additional generic
+conformance suite is outside that performance comparison.
+
+The verifier enumerates 34,525 complete small-code comparisons on 1,381
+independent generator sets, 108 wide-code cases and 87,381 scalar word pairs
+for the new arithmetic. It rejects sixteen malformed or over-capacity inputs
+and checks three changed-input histories. Outputs retain the original
+iterator order. The complete E7 consumer compares its entire internal result
+with the retained receipt, then emits identical output with both engines.
+
+## Measurement and scope
+
+The unreported baseline profile puts 0.236 of 0.623 instrumented seconds in
+population-plane counting. Reflection transport and rational elimination
+remain substantial unchanged costs, limiting the complete speedup. This
+profile is diagnostic and is not one of the ten timing samples. Both timed
+engines use the current default batch size sixteen. No stale original Gray
+iterator is used as the comparator.
+
+Measurements used CPython 3.12.15, macOS arm64 and eighteen logical CPUs.
+The entry load averages were 1.46, 2.83 and 2.48; other work can share the
+host. Alternating serial processes give both engines the same exposure to
+that noise. This is a local observation, not a hardware-independent speed
+promise, a multiplication runtime benchmark or a CI timing certificate.
+
+The adapter accepts widths 0..127, at most 27 independent generators,
+batch sizes 1..20 and at most 65,536 high-offset batches. These explicit
+capacities include the complete E7 caller. They restrict the generic helper
+interface, not the scientific replay's coefficient coverage. A generator
+outside those capacities is rejected, rather than partially enumerated.
+This is an opt-in standalone consumer substitution; production adoption,
+concurrent shared-process use and other codes are outside the claim.
+
+## Provenance and credit
+
+Base main is `2485805a6d47f36ea83ddde6327d453ac82d44dc`, priority revision 8.
+SOURCES.json pins all six live inputs. The selected-binding first example
+passes at conditional kappa .003125804; no selected cold replay is run.
+The `replay-runtime` card is refined to this originally posed counter
+implementation question. It changes no scientific support theorem.
+
+Credit Ali Romman's [PR5729](https://github.com/CrocSwap/integer-mult-bounds/pull/5729)
+for the bit-lane representation, Boolean population/threshold routines and
+complete consumer, and his [PR5669](https://github.com/CrocSwap/integer-mult-bounds/pull/5669)
+for the classification and retained checks. Nick Petalas's PR5238 supplies
+the inherited geometry. Their source files and credit lines stay unchanged.
+The weight identity and binary arithmetic are classical; the new contribution
+is their intersection-count implementation and complete-command evidence.
+No general literature-priority claim is made.
+
+Live claims, open PRs, recent account work, main READMEs and merged formula
+searches were checked. Sparse local coverage is incomplete. The canonical
+[claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19294736)
+records the corrected target. No predecessor audit is the deliverable.
+Independent human and formal proof-kernel review are unclaimed. There is no
+new native/physical caller, compiler, precision/tape, BIT or outer admission;
+Lean, Docker and the selected scientific replay were not run.
+
+## Open next questions
+
+Can this opt-in engine replace the production iterator at a named caller
+boundary, with regenerated dependent source pins? Begin with one explicit
+installation and source-bound compatibility check. This package preserves
+frozen sources and supplies the complete opt-in comparison; production
+integration is separate. TASK.json records relevance, first step and blockers.
+No further optimization or mathematical search is reserved.
+
+## Verifier constraints
+
+New functions are below sixty physical lines. There is no recursion. Explicit
+capacities bound rows, bit lanes, widths, batches, subprocesses and timeouts.
+The largest bit-lane table has 127 columns of at most 2^20 bits. The fixed
+verification fixtures use smaller tables and at most 1,024 literal words.
+Every complete child process has a sixty-second timeout and its exit status,
+stderr and exact output are checked.
+
+Power of Ten rules 3 and 9 require managed-runtime deviations. Python allocates
+bounded integers, tuples and lists during checking. `run_path` dispatches
+only to named local source/adapter files, after authenticating external
+inputs. The partial iterator has exactly the retained population/threshold
+helpers as injected call targets. Each standalone process owns its temporary
+consumer binding. Warnings are errors in both registered modes; no shared
+source, diagnostics configuration or repository-wide suite changes.

research/e7-intersection-counters/SOURCES.json

@@ -0,0 +1,54 @@
+{
+  "schema_version": 1,
+  "base_commit": "2485805a6d47f36ea83ddde6327d453ac82d44dc",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a",
+      "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "research/e7-bitsliced-exhaustion/binary.py",
+      "usage": "input",
+      "git_blob": "cad9fc43ec0244bce415a76bc61b6445ffbd7519",
+      "sha256": "e79ad4d1d4be1748cf09aacc4274a316000d4b5922f13495778892b9309dc56e"
+    },
+    {
+      "path": "research/e7-bitsliced-exhaustion/classify.py",
+      "usage": "input",
+      "git_blob": "3c14a223aebb5b05562c2db4f37eacc87148f9a3",
+      "sha256": "9fbdf0d4ad5c7a5feddfda2bfda7fbfedcdbc1361543b6ec7ef0f8ecc6bfb6c1"
+    },
+    {
+      "path": "research/e7-bitsliced-exhaustion/source/RESULT.json",
+      "usage": "input",
+      "git_blob": "d32035693b23f114723c953c94370b349aa13cad",
+      "sha256": "2742bd01c85c988cb4b8c13359839ce9e10672bde1a40c8bf668aae70b12c98d"
+    },
+    {
+      "path": "research/e7-bitsliced-exhaustion/source/SOURCES.json",
+      "usage": "input",
+      "git_blob": "195cf52a31ad494b2a4444beaa2bf66f0c8942e8",
+      "sha256": "6281c850b2827c2d10624822c9fa2aed4f7ecf50e1c615777e72214aa568ecc6"
+    },
+    {
+      "path": "research/e7-bitsliced-exhaustion/source/vendor/PR5238.py",
+      "usage": "input",
+      "git_blob": "781a074d45126b1a84b92ee2393dc95790c0cb1b",
+      "sha256": "95502bb9e551302cbb0483097250441e96e5f858a5624745678875e3cedba9d2"
+    },
+    {
+      "path": "research/e7-bitsliced-exhaustion/source/vendor/PR5238.md",
+      "usage": "input",
+      "git_blob": "5dc802961147c41af039e899d8baa3c8bb9e3909",
+      "sha256": "36e2263d28280043d6861caa4c81270be4800246e17647ec09da7cb4c2826085"
+    }
+  ]
+}