Accelerate a complete 64-axis Clifford projection by 40.6% (no κ)

research/bitset-gauss-elimination/BENCHMARK.json

@@ -0,0 +1,137 @@
+{
+  "errors": 0,
+  "executable": "/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12",
+  "platform": "macOS-27.0.1-arm64-arm-64bit",
+  "python": "3.12.15 (main, Oct 14 2026, 00:55:37) [Clang 23.1.3 ]",
+  "samples": [
+    {
+      "mode": "baseline",
+      "returncode": 0,
+      "seconds": 0.44511516694910824,
+      "stdout_sha256": "9e9ca672563db4c1d3a281be16c2fdcd798ae96de4fd9cd8c2e9ca1ce624effa",
+      "work": {
+        "gauss_calls": 25,
+        "maximum_dimension": 128,
+        "mode": "baseline"
+      }
+    },
+    {
+      "mode": "bitset",
+      "returncode": 0,
+      "seconds": 0.2640917918179184,
+      "stdout_sha256": "9e9ca672563db4c1d3a281be16c2fdcd798ae96de4fd9cd8c2e9ca1ce624effa",
+      "work": {
+        "gauss_calls": 25,
+        "maximum_dimension": 128,
+        "mode": "bitset"
+      }
+    },
+    {
+      "mode": "baseline",
+      "returncode": 0,
+      "seconds": 0.46423900010995567,
+      "stdout_sha256": "9e9ca672563db4c1d3a281be16c2fdcd798ae96de4fd9cd8c2e9ca1ce624effa",
+      "work": {
+        "gauss_calls": 25,
+        "maximum_dimension": 128,
+        "mode": "baseline"
+      }
+    },
+    {
+      "mode": "bitset",
+      "returncode": 0,
+      "seconds": 0.2641322501003742,
+      "stdout_sha256": "9e9ca672563db4c1d3a281be16c2fdcd798ae96de4fd9cd8c2e9ca1ce624effa",
+      "work": {
+        "gauss_calls": 25,
+        "maximum_dimension": 128,
+        "mode": "bitset"
+      }
+    },
+    {
+      "mode": "baseline",
+      "returncode": 0,
+      "seconds": 0.43559599993750453,
+      "stdout_sha256": "9e9ca672563db4c1d3a281be16c2fdcd798ae96de4fd9cd8c2e9ca1ce624effa",
+      "work": {
+        "gauss_calls": 25,
+        "maximum_dimension": 128,
+        "mode": "baseline"
+      }
+    },
+    {
+      "mode": "bitset",
+      "returncode": 0,
+      "seconds": 0.2659395409282297,
+      "stdout_sha256": "9e9ca672563db4c1d3a281be16c2fdcd798ae96de4fd9cd8c2e9ca1ce624effa",
+      "work": {
+        "gauss_calls": 25,
+        "maximum_dimension": 128,
+        "mode": "bitset"
+      }
+    },
+    {
+      "mode": "baseline",
+      "returncode": 0,
+      "seconds": 0.4352738750167191,
+      "stdout_sha256": "9e9ca672563db4c1d3a281be16c2fdcd798ae96de4fd9cd8c2e9ca1ce624effa",
+      "work": {
+        "gauss_calls": 25,
+        "maximum_dimension": 128,
+        "mode": "baseline"
+      }
+    },
+    {
+      "mode": "bitset",
+      "returncode": 0,
+      "seconds": 0.3204354590270668,
+      "stdout_sha256": "9e9ca672563db4c1d3a281be16c2fdcd798ae96de4fd9cd8c2e9ca1ce624effa",
+      "work": {
+        "gauss_calls": 25,
+        "maximum_dimension": 128,
+        "mode": "bitset"
+      }
+    },
+    {
+      "mode": "baseline",
+      "returncode": 0,
+      "seconds": 0.5051918339449912,
+      "stdout_sha256": "9e9ca672563db4c1d3a281be16c2fdcd798ae96de4fd9cd8c2e9ca1ce624effa",
+      "work": {
+        "gauss_calls": 25,
+        "maximum_dimension": 128,
+        "mode": "baseline"
+      }
+    },
+    {
+      "mode": "bitset",
+      "returncode": 0,
+      "seconds": 0.26453037513419986,
+      "stdout_sha256": "9e9ca672563db4c1d3a281be16c2fdcd798ae96de4fd9cd8c2e9ca1ce624effa",
+      "work": {
+        "gauss_calls": 25,
+        "maximum_dimension": 128,
+        "mode": "bitset"
+      }
+    }
+  ],
+  "source_hashes": {
+    "benchmark.py": "01b81ef23003aba719a611bc312efa44a3f955bc3118afc6bac9c252c975a94f",
+    "fast_gauss.py": "85bcce68ff3233b63a0d1f5cc0bae7efd596ec9bf7973cf1b8f278d43851fb34",
+    "run_projection.py": "053091c8b84e703ed622440a9b84af100171ebe8a7cc578e28a40631e94ba50c",
+    "run_replay.py": "c7e2d139c26bef270f9bc547aa0a5b6b5dd9faaf732123498e8ddd117889203e"
+  },
+  "summary": {
+    "baseline": {
+      "maximum": 0.5051918339449912,
+      "median": 0.44511516694910824,
+      "minimum": 0.4352738750167191
+    },
+    "bitset": {
+      "maximum": 0.3204354590270668,
+      "median": 0.26453037513419986,
+      "minimum": 0.2640917918179184
+    }
+  },
+  "workload": "projection"
+}

research/bitset-gauss-elimination/PINS.json

@@ -0,0 +1,22 @@
+{
+  ".gitattributes": "e8de51f40e73a262bbd8959a4230e3dce0b2b15ad68a19888750b7fc26593cf3",
+  "INPUTS.json": "c62bd55fd36c136ba2ec34f6d91ed481497932fadc7134d0b7e5c10009fd588c",
+  "PROOF.md": "b3834a57ba82f4fe316669910693b6c2399f50af8e7a73722d61cddc00ec31aa",
+  "README.md": "3a01996ff6da7402442842db70c45ea6aaceab1ae03c17dad1fcb2e11fee1f89",
+  "RESULT.json": "ce586c74a8633e2907b3227c0cbcff069e08e2d2afe4695c8d56abc844dff97f",
+  "SOURCES.json": "c8e43472b247d62b17ca74898d05945d36bd590db650c7a2101ded6bc48116c7",
+  "TASK.json": "3c302a0c814c47ecc0c7fb64b50872f4f3f5ed18dfdb65976e8f19ae6daadb20",
+  "VERIFY.json": "3940455d0e2e8195a7a8cfcd6504d07f76f25ace824b1d77d6f374d2ce3e3348",
+  "contractions.py": "a2fc065d6f293ddcffe5b6eec7fff0fdf57c8e3d4c6be355bd92e87d3f1865ef",
+  "source/CONSTRUCTION.json.gz": "00d13d7774adf087f93bc58d4c5860e296f8408c0ee25a4db254a056f8da7dec",
+  "source/LICENSE": "c71d239df91726fc519c6eb72d318ec65820627232b2f796219e87dcf35d0ab4",
+  "source/PHYSICAL.json": "f78ba861d23ff33f2c9ffeca8c3ab6a7f1ec906f38adff5d325c13efb187c7c3",
+  "source/PR5526-PROOF.md": "45483e4b5f604a5e70602c5caaa4394d4a0d0d1a6d0b6e8a93b836d50b23f764",
+  "source/PR5698-NOTICE.md": "1f55b3e4bb80a60611b1fca0622da5a99fe7877446f03d0edd1dc8f3a5abadd2",
+  "source/PR5704-NOTICE.md": "a77adc71861e3b9c73c703c5db5b671f61a1101d85d14cca08547e21d6d8dce4",
+  "source/PR5704-PROOF.md": "e5039414a02e36cdeab82fb9803fc4de0c3e0f3997e8812ef9d227e5d417ec91",
+  "source/PR5704-quadratic.py": "d406584aed1479b75c387bc964b9e797b2f4f75e5f8c6bbea00df07f7d590a91",
+  "source/clifford_exact.py": "2982ead07721e83358dc67c6f49c2b4c16a236a6bebdfd72f58221be1f5d0962",
+  "source/prune_native.py": "f2b37c183a10922eabc8e0436b426a08866430e96bd0adc7e178951c7fbb5257",
+  "verify.py": "be69f731a2b0ff7a4d47c90e49a9466ed2ab38a571235eff6953891f9707e53c"
+}

research/bitset-gauss-elimination/PROOF.md

@@ -0,0 +1,107 @@
+# Equivalence of adjacency-bitset elimination
+
+This implementation is produced by Nick Petalas. Quadratic Gauss-sum
+elimination is classical. Ali Romman's PR5727 retains its contraction,
+phase, state and finite-span contracts. The contribution here is this
+implementation and its consumer and performance evidence.
+
+The admitted input is a canonical polynomial on at most 256 Boolean variables,
+
+```text
+q(x) = c + sum a_i x_i + 2 sum_(i<j) b_ij x_i x_j  (mod 4),
+c,a_i in Z/4; b_ij in F2.
+```
+
+Dictionary mask zero represents c. A one-bit mask represents a linear term;
+a two-bit mask must have coefficient two. Zero dictionary coefficients,
+other masks and nonintegral or Boolean parameters are rejected.
+
+`unpack` retains the diagonal coefficients and the symmetric adjacency
+rows as integer bitsets. `active` names the variables not yet summed.
+The invariant is that the original sum equals the current Gaussian-integer
+scalar times the sum of the remaining polynomial. Indices never change.
+Inactive adjacency entries have no effect because every neighborhood is
+intersected with `active` before use.
+
+## One odd diagonal
+
+Write the eliminated variable as x and its neighbor parity as L. Its terms
+are `a*x + 2*x*L`, with a odd. Pointwise on the remaining variables,
+
+```text
+sum_(x=0,1) i^(a*x+2*x*L) = (1+i^a) i^(-a*L).
+```
+
+For any Boolean parity `L = XOR_(j in S) x_j`, its residue modulo four is
+
+```text
+L = sum_(j in S) x_j - 2 sum_(j<k in S) x_j x_k  (mod 4).
+```
+
+Terms involving at least three distinct variables have coefficient divisible
+by four. Thus `-a*L` subtracts a from every neighbor diagonal and toggles
+every edge inside S. `odd_step` performs those updates. The real/imaginary
+update multiplies the scalar by `1+i` for a=1 and by `1-i` for a=3.
+
+## One even diagonal with a neighbor
+
+Choose a neighbor y. Write the remaining terms involving x or y as
+
+```text
+a*x + b*y + 2*x*y + 2*x*L + 2*y*M,
+```
+
+where a is even and L,M are parities excluding both x and y. Summing x
+gives two when `y=t XOR L`, where `t=a/2`, and zero otherwise. Substitute
+this value for y. Modulo four, the new contribution is
+
+```text
+b*t + b*(1-2*t)*L + 2*t*M + 2*L*M.
+```
+
+The constant increases by b*t. Each vertex in L receives the diagonal
+increment `b*(1-2*t)`, and its internal edges toggle exactly when b is odd.
+Each vertex in M receives diagonal increment 2*t. Expanding `2*L*M`
+gives diagonal increment two on `L intersection M` and toggles each cross
+edge once per ordered membership in L times M. A pair counted twice cancels.
+
+For the row at vertex k, those cross-edge toggles are precisely
+
+```text
+(M if k in L else empty) XOR (L if k in M else empty),
+```
+
+with the self bit removed. These are `pair_step`'s updates, including the
+intersection diagonal. The scalar doubles, and both x and y leave `active`.
+This step does not divide by a polynomial coefficient.
+
+## Isolated variable and termination
+
+An isolated variable with diagonal two makes the entire sum zero. One with
+diagonal zero multiplies it by two. These and the odd case exhaust isolated
+variables. Each nonterminal iteration removes one or two variables. At most
+n iterations suffice. The final constant rotates the scalar by its exact
+quarter phase. The invariant proves that `gauss` returns `sum_x i^q(x)`.
+
+The argument holds in every finite dimension. The supplied implementation
+accepts only dimensions 0 through 256. It performs O(n squared) bounded
+row or coefficient updates, counting a bitset operation as one operation;
+this is not a constant-time bit-complexity assertion for unbounded n.
+
+## Consumer boundary
+
+`run_replay.py` authenticates the unchanged PR5727 package and substitutes
+only its `gauss` function. Differential mode compares every result with the
+original function, including each valid call inside the complete replay.
+The replay still compares its whole result with its committed RESULT.json.
+The original scientific theorem and its literal and signed-Pauli checks are
+cited inherited contracts, not new research claims of this package.
+
+`run_projection.py` generates five fixed 64-axis Clifford circuits. Each is
+a full coordinate C layer followed by a symmetric quadratic diagonal, with
+diagonal coefficients of the required parity. It uses the original Choi
+constructor and original exact finite-span solver on four sources and one
+target. Its kernel has 25 entries. Differential mode compares every Gauss
+sum in this complete calculation. All other computations remain unchanged.
+The fixed seeded fixture and algorithm are a computation benchmark, not a
+new scientific approximation optimum or an admitted physical caller.

research/bitset-gauss-elimination/README.md

@@ -0,0 +1,77 @@
+# Bitset elimination for exact quadratic Gauss sums
+
+This contribution was produced by Nick Petalas. It supplies a bounded exact
+implementation with a scoped equivalence proof and empirical performance
+evidence. There is no new kappa or selected-frontier change.
+
+On one complete 64-axis, four-source Clifford projection calculation,
+adjacency-bitset elimination reduces median command time by **40.6%**,
+from **0.445 s to 0.265 s**. Five alternating fresh-process pairs return
+identical complete output with zero errors. Times include source checks,
+circuit generation, Choi construction, the full phase-sensitive kernel,
+the exact normal-equation solve and output. This is a deterministic
+computational fixture, not a measured production search or physical caller.
+
+The old polynomial-substitution Gauss sum is replaced by bounded updates
+of Z/4 diagonal coefficients and adjacency bitsets. The other contraction
+and solve code is unchanged. [PROOF.md](PROOF.md) gives the elimination
+identities and the exact admitted domain, at most 256 variables.
+
+## Evidence and reproduction
+
+The local host used CPython 3.12.15 on macOS arm64, with 18 logical cores
+and a shared load. [BENCHMARK.json](BENCHMARK.json) contains all raw samples,
+source hashes, work counters and output digests. Baseline times range from
+0.4353 to 0.5052 seconds; bitset times range from 0.2641 to 0.3204 seconds.
+Separate profiles identify the old Gauss elimination and the remaining
+Choi construction as the limiting work. [VALIDATION.md](VALIDATION.md)
+records those profiles, the inconclusive small-width replay result and
+the correctness checks.
+
+From the repository root, using the provided interpreter:
+
+```sh
+~/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/bitset-gauss-elimination/verify.py
+~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/bitset-gauss-elimination
+~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/bitset-gauss-elimination --check-source-history
+```
+
+The direct checker prints `PASS_BITSET_GAUSS_ELIMINATION` and a generated
+receipt bound to package file hashes. A portable CPython 3.12 interpreter
+may replace the local path. The standard library suffices.
+
+To repeat the performance measurement, choose a new path outside the checkout:
+
+```sh
+~/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/bitset-gauss-elimination/benchmark.py --workload projection --output /absolute/scratch/benchmark.json
+```
+
+`--workload replay` measures the entire inherited inventory replay instead.
+Its overall gain was inconclusive locally. No speed claim is made for it.
+The full differential replay remains a conformance check, not this
+contribution's scientific deliverable.
+
+## Scope and credit
+
+Ali Romman's [PR5727](https://github.com/CrocSwap/integer-mult-bounds/pull/5727)
+supplies the phase-sensitive contraction engine, exact finite-span solver,
+complete replay and input set. PR5704's compact states, PR5526's tensor
+theorem, PR5698's native recipe set and every retained notice keep their
+credit. Quadratic Gauss-sum elimination and Boolean parity expansion are
+classical. This package claims the new implementation, its bounded proof
+binding and measured fixture improvement, not a new general Gauss-sum method.
+
+All predecessor files are unchanged. The original consumer is authenticated
+through [PINS.json](PINS.json) and declared as replay inputs. No wrapper is
+installed into the selected replay. Native realization, dirty restoration,
+physical time, rounding, compiler and outer obligations are not discharged.
+Independent human and formal proof-kernel review are unclaimed. Apache-2.0.
+
+## Open next questions
+
+1. Can Choi construction's remaining affine substitutions be reduced while
+   preserving exact state output? Start with the optimized projection profile
+   and one substitution. No replacement or equivalence proof is supplied.
+2. Does a named wider native-interface search benefit on another host? Bind
+   its complete input, states, solve and output before timing five alternating
+   pairs. Production-consumer and cross-platform evidence are absent here.