Route Boolean-sector query families with O(n log n) ordinary work

research/sector-routing-butterfly/.gitattributes

@@ -0,0 +1 @@
+inputs/** -text

research/sector-routing-butterfly/NOTICE.md

@@ -0,0 +1,5 @@
+# Attribution
+
+Ali Romman with substantial OpenAI Codex assistance wrote `routing.py`, `verify.py`, and the new proof and prose. No independent human review is claimed.
+
+The frozen source files retain their text. They come from PR5626 at `380591a21cad88c03a05a8e8177ed0eede85c492` and PR5578 as present at `df0137efd35e11b4445734bf612bdd4c7ebc330c`. See PINS.json for hashes and paths. PR5626 credits Dugongue PR5578 T6, Ali Romman PR5615, and their retained source authors. The present route does not reimplement or claim authorship of their query-rank theorem.

research/sector-routing-butterfly/PINS.json

@@ -0,0 +1,34 @@
+[
+  {
+    "file": "inputs/SECTOR-PROOF.md",
+    "sha256": "16c2e4a41591727944089e0b84233d376d4822dfb224cf087a6d9151a01cbb80",
+    "commit": "380591a21cad88c03a05a8e8177ed0eede85c492",
+    "path": "research/optimal-sector-query-compiler/PROOF.md",
+    "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/5626",
+    "git_blob": "ee7035ca6d052fe7ba39d5d8a055fd2aa02480cf"
+  },
+  {
+    "file": "inputs/SECTOR-RESULT.json",
+    "sha256": "a9cc4c6e6b97118a0b9fc02f0af6113fcd42d45cadf2c5714c9a5f4ae0a9deb8",
+    "commit": "380591a21cad88c03a05a8e8177ed0eede85c492",
+    "path": "research/optimal-sector-query-compiler/RESULT.json",
+    "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/5626",
+    "git_blob": "61c14d779cc9747a808ea35ec11b23761ea60ca3"
+  },
+  {
+    "file": "inputs/packing.py",
+    "sha256": "c7b7acdd7aa71e48a1d7447316400bb3213eaabbbe1e42c59e67dfcb0a83258d",
+    "commit": "380591a21cad88c03a05a8e8177ed0eede85c492",
+    "path": "research/optimal-sector-query-compiler/packing.py",
+    "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/5626",
+    "git_blob": "6925652078a36c2cc5d1c91f5315d23ebf7e178b"
+  },
+  {
+    "file": "inputs/TYPED-PROVIDER.md",
+    "sha256": "dc1a21489807dc3553e4225b56534c4372ebafd72598eb673ef7c675f55fec21",
+    "commit": "df0137efd35e11b4445734bf612bdd4c7ebc330c",
+    "path": "research/characteristic-gaussian-provider/typed-provider.md",
+    "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/5578",
+    "git_blob": "cc190c322d944eabd2a8fb36ad8d11923cb5c5ec"
+  }
+]

research/sector-routing-butterfly/PROOF.md

@@ -0,0 +1,72 @@
+# Exact routing, cost, and storage proofs
+
+## 1. Scope and algebra
+
+Work over a ring in which 2 is a unit. The ordinary maps `J_j` commute and square to `I`. The query `Q` commutes with all of them and has square `J_0`. For `a in F2^s`, set
+
+`E_a = 2^(-s) sum_m (-1)^(a dot m) J^m`.
+
+The `E_a` are pairwise orthogonal idempotents and sum to `I`. No positivity or numerical approximation is used. There are `r` independent blocks, each with `n=2^s` data fields. Define `F_a=I+Q E_a/2` and `G_a=I+(Q-I)E_a`.
+
+## 2. Controlled swap from legal instructions
+
+For bit `k`, put `P=(I-J_k)/2`. On two distinct fields `(a,b)`, execute:
+
+```
+a += P b
+b -= P a
+a += P b
+b  = J_k b
+```
+
+Each of the first three lines is two separate ADDs, with coefficients `+/-1/2` and shifts `I,J_k`. Thus this macro has six ADDs and one pure SHIFT. Since `P^2=P`, the final fields are
+
+`((I-P)a + P b, P a + (I-P)b)`.
+
+It swaps the fields on the negative `J_k` sector and leaves them in place on the positive sector. This identity also follows by direct expansion in `Z[1/2][J_k]/(J_k^2-1)`. The verifier checks all input columns and every cut of the seven-instruction macro. Both the coefficient prefix norm and suffix norm have maximum 2.
+
+For each bit `k`, apply the macro to all `n/2` role pairs that differ in bit `k`. Do this for all bits. Call the result `R`. On sector `sigma`, the role action is `a -> a xor sigma`. Hence `R^2=I`, and its output at role zero is `sum_a E_a x_a`. The bit stages commute as complete maps. Using the same stage order a second time is therefore a valid inverse; it is not necessary to reverse the individual shears.
+
+## 3. The two middle operations
+
+Route each block, act at role zero, then route again.
+
+For `F`, use one extra field `z`. Clear it once at entry. In each block, copy the routed role zero to `z` with one ADD, query `z`, add half of `z` to role zero, then clear `z`. The next block can use the same field. On sector `sigma`, only original role `sigma` receives `Q/2` of itself. All other roles are unchanged. This is precisely `diag(F_a)`. The full map is independent of the initial value of `z`, and the final value of `z` is zero.
+
+For `G`, query routed role zero in place. There is no extra field. Sector `sigma` applies `Q` only to original role `sigma`, which is precisely `diag(G_a)`.
+
+The two routes use `ns` controlled swaps per block. This proves the in-place tariff table. To keep inputs, first clear `rn` separate output fields and copy each input to its output with one ADD. Apply the in-place circuit to these outputs. This gives `rn` further ADDs and CLEARs. The original input fields are unchanged. The input-preserving comparison is thus a comparison of the same retained-input contract as PR5626, not a storage saving obtained by dropping its inputs.
+
+For one block, PR5626 has `2n^2+n` ADDs, `n+2` CLEARs and `n+1` owned fields including outputs. The new retained-input circuit has `6ns+n+2` ADDs, `ns` pure shifts and the same query, CLEAR and field counts. It uses fewer ADDs for `s>=4`. Its ordinary instruction count is `O(n log n)` for this entire family. A universal lower bound on ADD count is not claimed.
+
+## 4. Query lower bound
+
+On every nonempty sector, the coefficient of `Q` in `diag(F_a)` has rank `r`: there is one nonzero entry `1/2` per block. The same rank is `r` for `G`. The sector-rank lower bound of PR5626 therefore requires at least `r` single-field queries, even with linear feedback and extra fields. Our circuits attain this bound.
+
+This lower bound requires `I` and `Q` to be linearly independent on every sector used. The native central Gaussian family has this property for `f>=3`, as specified in the source proof. The construction works for smaller `f`, but the same minimality claim is not made there. The construction needs no Smith factorization or odd division.
+
+## 5. Sharp workspace and CLEAR counts in a declared alphabet
+
+This section has a narrower instruction model than the query lower bound. Allow distinct-role ADDs with dyadic coefficients and ordinary `J` shifts; pure ordinary shifts; `Q` or `Q^-1` on one field; multiplication of a field by a dyadic unit `+/-2^k`; and CLEAR. Extra borrowed fields may start arbitrarily, but must be restored. Each owned workspace field also starts arbitrarily and must finish zero. Do not allow a nonunit scalar overwrite, an arbitrary destructive address map, or a free initial zero field.
+
+Specialize `Q=1` and every `J_j=1`, then reduce the dyadic coefficients modulo 3. Each block of `F` has one factor `3/2`, which becomes zero, and all other factors are one. If there are `m` owned fields, the final map has nullity `r+m`: `r` data directions and `m` owned directions. All allowed instructions except CLEAR are invertible modulo 3. One CLEAR can reduce rank by at most one. Thus at least `r+m` CLEARs are required.
+
+There must also be at least one owned field. If `m=0`, the desired map on all data and restored borrowed fields is invertible over the rationals at the same specialization. A CLEAR would make the full square map singular, so no CLEAR could occur. Every remaining instruction has determinant a dyadic unit. Their product cannot have determinant `(3/2)^r`. This is a contradiction. With `m=1`, our circuit attains both the minimum workspace and the lower bound `r+1` CLEARs. For the gauge map, zero workspace and zero CLEARs are attained, so those counts are minimal.
+
+These statements do not concern the additional retained outputs of the input-preserving wrapper. They do not apply to a model that admits `SCALE 3/2`: that instruction is singular modulo 3 and defeats the key invertibility premise. The verifier checks this scope control. In particular, the argument is not a universal memory lower bound for arbitrary scalar algorithms.
+
+## 6. Prefix and suffix bounds
+
+Use the maximum absolute row-sum norm on all fields and addresses. At a complete bit stage, each role interacts with only one other role. Every partial prefix and suffix within that stage has norm at most 2, from the exact local seven-instruction check. A full route has `s` stages. Thus every route prefix and suffix has norm at most `2^s=n`.
+
+Let `M>=1` bound the query, all its prefixes, and all its suffixes. Each middle prefix and suffix in the perturbation circuit has norm at most `2(1+M)`, including a cut with arbitrary residual `z`. This follows by the triangle inequality on the copy, query, half-ADD and CLEAR. The gauge middle uses at most `M`. Composition gives the common bound `2 n^2 (1+M)` for every prefix and suffix in either in-place block.
+
+The full `F` block has norm at most `1+M/2`; the full `G` block has norm at most `2+M`. Different completed blocks act on disjoint data. A prefix starts with the workspace clear. In a suffix, arbitrary workspace at the cut can affect at most the first remaining middle operation; its next CLEAR removes it before later blocks. Thus the same common bound holds for any number of sequential blocks, with no factor exponential in `r`. The input-preserving wrapper adds a copy stage of norm at most 2, so twice the common bound suffices for its prefixes and suffixes.
+
+At native instruction boundaries, `||Q_f||_infinity = 2^(f/2)`, and `M=2^f` is a rational upper bound. This substitution does not bound an unexamined arithmetic implementation inside QUERY. A caller must provide those internal bounds and pay for the actual shifts and shifted ADDs. No complete tape, precision, or multiplication budget follows from the field circuit alone.
+
+## 7. Checks and proof boundaries
+
+The symbolic interpreter uses the regular group algebra `Q[C4 x C2^(s-1)]`. The low two bits give the power of `Q`; the other bits give spectator involutions. Its final matrix is compared with a direct expansion of each `E_a`. It includes every initial data and workspace column. A separate reverse-order adjoint interpreter swaps ADD source and destination roles and checks the transposed final map. This is a role transpose over a commutative coefficient ring, not the native address adjoint.
+
+The native interpreter instead uses exact pairs of rational numbers at each address. It applies the Gaussian two-point map on each central bit and literal XOR shifts on the spectator bits. Its expected result expands the projectors directly from the original inputs. The tests cover one orbit of the spectator translations; all such address orbits have the same action. Five deleted or changed instructions fail against the full-column target. These finite checks do not replace the all-parameter proof above or the missing complete caller.

research/sector-routing-butterfly/README.md

@@ -0,0 +1,44 @@
+# Boolean-sector routing with one query per block
+
+This package replaces the quadratic ordinary work in the published T7 family with an in-place routing network. It gives an exact construction for every sector count `n = 2^s`, `s >= 1`, and every number `r >= 1` of disjoint blocks. It does not install a complete multiplication caller.
+
+Let `J_0,...,J_(s-1)` be commuting involutions. Let `Q` commute with them and satisfy `Q^2 = J_0`. Put `E_a = product_j (I + (-1)^a_j J_j)/2`. The perturbation map is `x_(b,a) -> x_(b,a) + Q E_a x_(b,a)/2`. The gauge map replaces this expression with `(I + (Q-I)E_a)x_(b,a)`.
+
+| Contract | QUERY | ADD | Pure SHIFT | CLEAR | Extra fields |
+|---|---:|---:|---:|---:|---:|
+| Perturbation, in place | r | 6rns+2r | rns | r+1 | 1 |
+| Gauge, in place | r | 6rns | rns | 0 | 0 |
+| Perturbation, inputs retained | r | 6rns+rn+2r | rns | rn+r+1 | rn+1, with outputs |
+
+Each ADD has different source and destination fields. Every coefficient is `1`, `1/2`, or `-1/2`. There is no sector-dependent overwrite primitive. The pure shifts and the shifted ADDs are explicit instructions.
+
+For 32 sectors and one block, the input-preserving version uses **994 ADDs and 160 pure shifts**, instead of the **2,080 ADDs** in PR5626. Both use one query, 34 CLEARs, and 33 extra fields including outputs. If each ADD and pure shift has unit cost, the total falls from 2,080 to 1,154. A physical caller can price these operations differently. The in-place version uses 962 ADDs, 160 shifts, two CLEARs, and one extra field. Its storage comparison has a different input-retention contract.
+
+The query count is minimal in the faithful-sector model of PR5626. The perturbation workspace and CLEAR counts are also minimal in the narrower alphabet specified in [PROOF.md](PROOF.md). The proof does not allow a nonunit scalar overwrite. It counts an owned field as arbitrary on entry and zero on exit. The gauge version needs no owned field.
+
+The proof gives a bound `2 n^2 (1+M)` for every prefix and suffix of an in-place block, if `M >= 1` bounds the query and its internal prefixes and suffixes. The same bound holds for sequential disjoint blocks. Instruction-boundary checks do not certify the arithmetic inside a native query.
+
+## Evidence
+
+Run with Python 3.12 and the standard library:
+
+```sh
+python3.12 -I -W error -B research/sector-routing-butterfly/verify.py
+python3.12 -I -O -W error -B research/sector-routing-butterfly/verify.py
+```
+
+The verifier checks 28 full-column maps in `Q[C4 x C2^(s-1)]`, with `s <= 5` and up to four blocks. A separate reverse-adjoint replay checks each suffix and final transpose. Five further full-column cases retain the inputs. It also checks 48 exact native Gaussian address cases with `1 <= f <= 4`, `1 <= s <= 3`, and one or two blocks. Arbitrary initial workspace columns are included. Five changed words must fail. A nonunit-scale control marks the limit of the storage proof. [RESULT.json](RESULT.json) stores the exact counts and coefficient norms.
+
+The general statement follows from the proof. The finite checks support that proof; they are not an exhaustive native caller certificate. The source files in `inputs/` are evidence, not executable dependencies. Their bytes and commits are pinned in [PINS.json](PINS.json). Source history is not available in the shallow export; byte checks and the committed-file check are separate.
+
+## Attribution and limits
+
+Ali Romman with substantial OpenAI Codex assistance wrote this package. The model derived and implemented the route, proofs and checks. No independent human review is claimed. Retain credit to Dugongue for PR5578 T6/T7 and PR5586 C8; PR5626 supplies the sector-rank lower bound and the comparison compiler. PR5615 supplies its dyadic rank-factor lineage. Retain Nick Petalas, Cao, DaysSky, Cinna, Ryanson, zxv and Jacob in that source lineage. The frozen files retain their original text.
+
+The selected result at base `df0137efd35e11b4445734bf612bdd4c7ebc330c` is unchanged. This result has no new kappa. A complete supplier, a profitable native B/C demand, physical routing, precision, and a complete outer bill remain open. The existing whole-caller and role-gauge obstructions retain their scope.
+
+## Open next questions
+
+- Find an actual caller whose required map has these disjoint sector supports. Price the full input and return protocol before claiming a gain.
+- Price the ordinary shifts and shifted ADDs at that caller's actual address layout. A count of field instructions is not a tape cost.
+- Test whether a broader scalar-overwrite alphabet can use less workspace without a larger arithmetic or precision bill. The present storage proof does not cover that alphabet.