From 96278e8cdfe2aadb16024e6ee2c7deaebd4ed484 Mon Sep 17 00:00:00 2001 From: Ali Romman <226877337+aliromman@users.noreply.github.com> Date: Sun, 25 Oct 2026 22:22:34 -0500 Subject: [PATCH] Compile Boolean-sector families with in-place butterfly routing --- .../sector-routing-butterfly/.gitattributes | 1 + research/sector-routing-butterfly/NOTICE.md | 5 + research/sector-routing-butterfly/PINS.json | 34 ++ research/sector-routing-butterfly/PROOF.md | 72 ++++ research/sector-routing-butterfly/README.md | 44 ++ research/sector-routing-butterfly/RESULT.json | 406 ++++++++++++++++++ .../sector-routing-butterfly/SOURCES.json | 45 ++ research/sector-routing-butterfly/TASK.json | 96 +++++ research/sector-routing-butterfly/VERIFY.json | 34 ++ .../inputs/SECTOR-PROOF.md | 177 ++++++++ .../inputs/SECTOR-RESULT.json | 50 +++ .../inputs/TYPED-PROVIDER.md | 164 +++++++ .../inputs/packing.py | 159 +++++++ research/sector-routing-butterfly/routing.py | 56 +++ research/sector-routing-butterfly/verify.py | 242 +++++++++++ 15 files changed, 1585 insertions(+) create mode 100644 research/sector-routing-butterfly/.gitattributes create mode 100644 research/sector-routing-butterfly/NOTICE.md create mode 100644 research/sector-routing-butterfly/PINS.json create mode 100644 research/sector-routing-butterfly/PROOF.md create mode 100644 research/sector-routing-butterfly/README.md create mode 100644 research/sector-routing-butterfly/RESULT.json create mode 100644 research/sector-routing-butterfly/SOURCES.json create mode 100644 research/sector-routing-butterfly/TASK.json create mode 100644 research/sector-routing-butterfly/VERIFY.json create mode 100644 research/sector-routing-butterfly/inputs/SECTOR-PROOF.md create mode 100644 research/sector-routing-butterfly/inputs/SECTOR-RESULT.json create mode 100644 research/sector-routing-butterfly/inputs/TYPED-PROVIDER.md create mode 100644 research/sector-routing-butterfly/inputs/packing.py create mode 100644 research/sector-routing-butterfly/routing.py create mode 100644 research/sector-routing-butterfly/verify.py diff --git a/research/sector-routing-butterfly/.gitattributes b/research/sector-routing-butterfly/.gitattributes new file mode 100644 index 0000000000..8abeb4295b --- /dev/null +++ b/research/sector-routing-butterfly/.gitattributes @@ -0,0 +1 @@ +inputs/** -text diff --git a/research/sector-routing-butterfly/NOTICE.md b/research/sector-routing-butterfly/NOTICE.md new file mode 100644 index 0000000000..d348e382a3 --- /dev/null +++ b/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. diff --git a/research/sector-routing-butterfly/PINS.json b/research/sector-routing-butterfly/PINS.json new file mode 100644 index 0000000000..84e4f3adbd --- /dev/null +++ b/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" + } +] diff --git a/research/sector-routing-butterfly/PROOF.md b/research/sector-routing-butterfly/PROOF.md new file mode 100644 index 0000000000..1e29da0927 --- /dev/null +++ b/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. diff --git a/research/sector-routing-butterfly/README.md b/research/sector-routing-butterfly/README.md new file mode 100644 index 0000000000..c5f618d370 --- /dev/null +++ b/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. diff --git a/research/sector-routing-butterfly/RESULT.json b/research/sector-routing-butterfly/RESULT.json new file mode 100644 index 0000000000..822b80f24a --- /dev/null +++ b/research/sector-routing-butterfly/RESULT.json @@ -0,0 +1,406 @@ +{ + "formal_cases": [ + { + "ADD": 14, + "CLEAR": 2, + "QUERY": 1, + "SHIFT": 2, + "mode": "perturbation", + "owned": 1, + "prefix": "3", + "r": 1, + "s": 1, + "suffix": "7/2" + }, + { + "ADD": 12, + "CLEAR": 0, + "QUERY": 1, + "SHIFT": 2, + "mode": "gauge", + "owned": 0, + "prefix": "3", + "r": 1, + "s": 1, + "suffix": "3" + }, + { + "ADD": 28, + "CLEAR": 3, + "QUERY": 2, + "SHIFT": 4, + "mode": "perturbation", + "owned": 1, + "prefix": "3", + "r": 2, + "s": 1, + "suffix": "7/2" + }, + { + "ADD": 24, + "CLEAR": 0, + "QUERY": 2, + "SHIFT": 4, + "mode": "gauge", + "owned": 0, + "prefix": "3", + "r": 2, + "s": 1, + "suffix": "3" + }, + { + "ADD": 42, + "CLEAR": 4, + "QUERY": 3, + "SHIFT": 6, + "mode": "perturbation", + "owned": 1, + "prefix": "3", + "r": 3, + "s": 1, + "suffix": "7/2" + }, + { + "ADD": 36, + "CLEAR": 0, + "QUERY": 3, + "SHIFT": 6, + "mode": "gauge", + "owned": 0, + "prefix": "3", + "r": 3, + "s": 1, + "suffix": "3" + }, + { + "ADD": 56, + "CLEAR": 5, + "QUERY": 4, + "SHIFT": 8, + "mode": "perturbation", + "owned": 1, + "prefix": "3", + "r": 4, + "s": 1, + "suffix": "7/2" + }, + { + "ADD": 48, + "CLEAR": 0, + "QUERY": 4, + "SHIFT": 8, + "mode": "gauge", + "owned": 0, + "prefix": "3", + "r": 4, + "s": 1, + "suffix": "3" + }, + { + "ADD": 50, + "CLEAR": 2, + "QUERY": 1, + "SHIFT": 8, + "mode": "perturbation", + "owned": 1, + "prefix": "6", + "r": 1, + "s": 2, + "suffix": "5" + }, + { + "ADD": 48, + "CLEAR": 0, + "QUERY": 1, + "SHIFT": 8, + "mode": "gauge", + "owned": 0, + "prefix": "6", + "r": 1, + "s": 2, + "suffix": "9/2" + }, + { + "ADD": 100, + "CLEAR": 3, + "QUERY": 2, + "SHIFT": 16, + "mode": "perturbation", + "owned": 1, + "prefix": "6", + "r": 2, + "s": 2, + "suffix": "5" + }, + { + "ADD": 96, + "CLEAR": 0, + "QUERY": 2, + "SHIFT": 16, + "mode": "gauge", + "owned": 0, + "prefix": "6", + "r": 2, + "s": 2, + "suffix": "9/2" + }, + { + "ADD": 150, + "CLEAR": 4, + "QUERY": 3, + "SHIFT": 24, + "mode": "perturbation", + "owned": 1, + "prefix": "6", + "r": 3, + "s": 2, + "suffix": "5" + }, + { + "ADD": 144, + "CLEAR": 0, + "QUERY": 3, + "SHIFT": 24, + "mode": "gauge", + "owned": 0, + "prefix": "6", + "r": 3, + "s": 2, + "suffix": "9/2" + }, + { + "ADD": 200, + "CLEAR": 5, + "QUERY": 4, + "SHIFT": 32, + "mode": "perturbation", + "owned": 1, + "prefix": "6", + "r": 4, + "s": 2, + "suffix": "5" + }, + { + "ADD": 192, + "CLEAR": 0, + "QUERY": 4, + "SHIFT": 32, + "mode": "gauge", + "owned": 0, + "prefix": "6", + "r": 4, + "s": 2, + "suffix": "9/2" + }, + { + "ADD": 146, + "CLEAR": 2, + "QUERY": 1, + "SHIFT": 24, + "mode": "perturbation", + "owned": 1, + "prefix": "12", + "r": 1, + "s": 3, + "suffix": "9" + }, + { + "ADD": 144, + "CLEAR": 0, + "QUERY": 1, + "SHIFT": 24, + "mode": "gauge", + "owned": 0, + "prefix": "12", + "r": 1, + "s": 3, + "suffix": "8" + }, + { + "ADD": 292, + "CLEAR": 3, + "QUERY": 2, + "SHIFT": 48, + "mode": "perturbation", + "owned": 1, + "prefix": "12", + "r": 2, + "s": 3, + "suffix": "9" + }, + { + "ADD": 288, + "CLEAR": 0, + "QUERY": 2, + "SHIFT": 48, + "mode": "gauge", + "owned": 0, + "prefix": "12", + "r": 2, + "s": 3, + "suffix": "8" + }, + { + "ADD": 438, + "CLEAR": 4, + "QUERY": 3, + "SHIFT": 72, + "mode": "perturbation", + "owned": 1, + "prefix": "12", + "r": 3, + "s": 3, + "suffix": "9" + }, + { + "ADD": 432, + "CLEAR": 0, + "QUERY": 3, + "SHIFT": 72, + "mode": "gauge", + "owned": 0, + "prefix": "12", + "r": 3, + "s": 3, + "suffix": "8" + }, + { + "ADD": 584, + "CLEAR": 5, + "QUERY": 4, + "SHIFT": 96, + "mode": "perturbation", + "owned": 1, + "prefix": "12", + "r": 4, + "s": 3, + "suffix": "9" + }, + { + "ADD": 576, + "CLEAR": 0, + "QUERY": 4, + "SHIFT": 96, + "mode": "gauge", + "owned": 0, + "prefix": "12", + "r": 4, + "s": 3, + "suffix": "8" + }, + { + "ADD": 386, + "CLEAR": 2, + "QUERY": 1, + "SHIFT": 64, + "mode": "perturbation", + "owned": 1, + "prefix": "24", + "r": 1, + "s": 4, + "suffix": "17" + }, + { + "ADD": 384, + "CLEAR": 0, + "QUERY": 1, + "SHIFT": 64, + "mode": "gauge", + "owned": 0, + "prefix": "24", + "r": 1, + "s": 4, + "suffix": "16" + }, + { + "ADD": 962, + "CLEAR": 2, + "QUERY": 1, + "SHIFT": 160, + "mode": "perturbation", + "owned": 1, + "prefix": "48", + "r": 1, + "s": 5, + "suffix": "33" + }, + { + "ADD": 960, + "CLEAR": 0, + "QUERY": 1, + "SHIFT": 160, + "mode": "gauge", + "owned": 0, + "prefix": "48", + "r": 1, + "s": 5, + "suffix": "32" + } + ], + "local_controlled_swap_prefix": "2", + "local_controlled_swap_suffix": "2", + "native_cases": 48, + "new_kappa_claim": false, + "preserving_cases": [ + { + "ADD": 16, + "CLEAR": 4, + "QUERY": 1, + "SHIFT": 2, + "owned_including_outputs": 3, + "prefix": "3", + "s": 1, + "suffix": "7/2" + }, + { + "ADD": 54, + "CLEAR": 6, + "QUERY": 1, + "SHIFT": 8, + "owned_including_outputs": 5, + "prefix": "6", + "s": 2, + "suffix": "5" + }, + { + "ADD": 154, + "CLEAR": 10, + "QUERY": 1, + "SHIFT": 24, + "owned_including_outputs": 9, + "prefix": "12", + "s": 3, + "suffix": "9" + }, + { + "ADD": 402, + "CLEAR": 18, + "QUERY": 1, + "SHIFT": 64, + "owned_including_outputs": 17, + "prefix": "24", + "s": 4, + "suffix": "17" + }, + { + "ADD": 994, + "CLEAR": 34, + "QUERY": 1, + "SHIFT": 160, + "owned_including_outputs": 33, + "prefix": "48", + "s": 5, + "suffix": "33" + } + ], + "rejected_controls": [ + "missing_query", + "missing_shift", + "missing_entry_clear", + "missing_final_clear", + "wrong_involution", + "nonunit_scale_not_invertible_mod_3" + ], + "selected_frontier_changed": false, + "status": "PASS_SECTOR_ROUTING_BUTTERFLY" +} diff --git a/research/sector-routing-butterfly/SOURCES.json b/research/sector-routing-butterfly/SOURCES.json new file mode 100644 index 0000000000..74e46c64a4 --- /dev/null +++ b/research/sector-routing-butterfly/SOURCES.json @@ -0,0 +1,45 @@ +{ + "schema_version": 1, + "base_commit": "df0137efd35e11b4445734bf612bdd4c7ebc330c", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8", + "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/characteristic-gaussian-provider/typed-provider.md", + "usage": "provenance", + "git_blob": "cc190c322d944eabd2a8fb36ad8d11923cb5c5ec", + "sha256": "dc1a21489807dc3553e4225b56534c4372ebafd72598eb673ef7c675f55fec21" + }, + { + "path": "research/optimal-sector-query-compiler/PROOF.md", + "usage": "provenance", + "pin": "head:380591a21cad88c03a05a8e8177ed0eede85c492:research/optimal-sector-query-compiler/PROOF.md", + "git_blob": "ee7035ca6d052fe7ba39d5d8a055fd2aa02480cf", + "sha256": "16c2e4a41591727944089e0b84233d376d4822dfb224cf087a6d9151a01cbb80" + }, + { + "path": "research/optimal-sector-query-compiler/RESULT.json", + "usage": "provenance", + "pin": "head:380591a21cad88c03a05a8e8177ed0eede85c492:research/optimal-sector-query-compiler/RESULT.json", + "git_blob": "61c14d779cc9747a808ea35ec11b23761ea60ca3", + "sha256": "a9cc4c6e6b97118a0b9fc02f0af6113fcd42d45cadf2c5714c9a5f4ae0a9deb8" + }, + { + "path": "research/optimal-sector-query-compiler/packing.py", + "usage": "provenance", + "pin": "head:380591a21cad88c03a05a8e8177ed0eede85c492:research/optimal-sector-query-compiler/packing.py", + "git_blob": "6925652078a36c2cc5d1c91f5315d23ebf7e178b", + "sha256": "c7b7acdd7aa71e48a1d7447316400bb3213eaabbbe1e42c59e67dfcb0a83258d" + } + ] +} diff --git a/research/sector-routing-butterfly/TASK.json b/research/sector-routing-butterfly/TASK.json new file mode 100644 index 0000000000..bab39b7482 --- /dev/null +++ b/research/sector-routing-butterfly/TASK.json @@ -0,0 +1,96 @@ +{ + "schema_version": 1, + "task_id": "joint-query-controller", + "priority_revision": 7, + "base_commit": "df0137efd35e11b4445734bf612bdd4c7ebc330c", + "original_card": { + "id": "joint-query-controller", + "question": "Can the installed QQ16 caller win a complete matched protocol bill, or can a changed demand eliminate actual paid work?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/qq16-caller-install/README.md" + ], + "methods": [ + "Derive the matched whole-caller physical bill for installed and baseline protocols.", + "Change the actual demanded observations and prove a cheaper legal producer/consumer contract." + ], + "acceptance_gate": "Name the changed premise of the fixed F0/B1 observation obstruction. Show exactly which query is recovered, legal native reads and restoration, and a full favorable budget including cover maps, helpers and endpoints. Local inverse identities alone do not close the global controller. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read #4166 COST.md and ADMISSION.json. An actual caller connection is now proposed. Its native-component profile loses; parent park/restore versus external-call costs remain unresolved. Retain the producer and recovery lineage rather than rebuild it.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "At the actual installed cut, compare matched complete parent park/restore and external input/return protocols at the same bank/packet geometry, including every later root call and service cost. Alternatively pin both bridge observations and derive a genuinely smaller source-compatible demand. Stop if the complete necessary inequality fails or an essential cost is unknown; no larger decoder scan from a local tape-action saving.", + "bottleneck_link": "The native local words exist; retained query information and its physical access are the missing link to a composed recursive interface.", + "allowed_variations": [ + "One paid query, one changed first pair, or one precisely specified affine helper state.", + "A counterexample or lower bound for that exact proposed repair.", + "One unresolved obligation of a newer local decoder, with exact source heads and a distinct claim/domain." + ], + "scope_change_triggers": [ + "Retaining the fixed first pair and ordinary schedule while allowing only homogeneous selected-only control, already excluded by the witness.", + "Treating cover-map counts as zero-cost physical address operations.", + "Recreating the pending complete local decoder or early-record/output-bank coalescing already under investigation without a distinct audit or changed premise.", + "Treating a completed-output defect inequality as a producer-interior, dirty-range or physical-cost certificate.", + "Recreating completed-output recovery or caller wiring already supplied by #4166 without new independent coverage.", + "Dropping retained later root calls or claiming native-profile dominance from the isolated publication saving." + ], + "overlap_terms": [ + "QQ16", + "joint-query", + "changing-chart controller", + "selected observation", + "1969", + "2540", + "early record", + "output-bank retention", + "complete native decoder", + "2965", + "producer defect", + "dirty-helper range", + "F17 consumer", + "4166", + "qq16-caller-install" + ], + "existing_checks": [ + { + "scope": "PR #4166: author-checked installed producer/service/return/bridge connection; native-component comparison loses.", + "evidence": "research/qq16-caller-install/README.md", + "remaining": "Complete matched physical protocol bill, or changed source-compatible demand/circuit; no affordable supplier yet.", + "status": "author-checked", + "source_commit": "0b082d22a0e9a442d264ab0633e35ef26c790630", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "refined", + "actual_scope": "Construct an in-place Boolean-sector butterfly for the published T7 family, with exact all-parameter tariffs, matched retained-input comparison, and scoped query/storage/CLEAR lower bounds.", + "scope_change_reason": "PR5626 closes the exact query count but its generic ordinary emitter is quadratic in the sector count and uses separate outputs. This scope reduces that ordinary cost for the full published family and states both input contracts.", + "bottleneck_link": "Reduce charged ordinary work and temporary storage in an exact native query service; an actual profitable complete caller is still required.", + "budget_minutes": 120, + "stop_rule": "Stop after the family construction, matched comparison, exact replay and scoped lower bounds. Do not expand into a native caller without a complete bill.", + "outcome": "completed", + "evidence": "PROOF.md; RESULT.json; verify.py; PINS.json", + "author": "Ali Romman with substantial OpenAI Codex assistance", + "ai_assistance": "Substantial OpenAI Codex assistance for algebra, implementation, verification and writing. No independent human review.", + "open_questions": [ + { + "question": "Which actual caller has this sector-supported demand?", + "why_it_matters": "A field compiler alone does not improve kappa.", + "first_step": "Pin a required native map and compare full matched caller bills.", + "blocked_by": "No such profitable caller is supplied." + }, + { + "question": "What is the actual tape cost of the shifts?", + "why_it_matters": "Field pass counts do not determine physical cost.", + "first_step": "Compile both contracts at the same address layout and precision.", + "blocked_by": "A concrete caller and physical layout are required." + } + ] +} diff --git a/research/sector-routing-butterfly/VERIFY.json b/research/sector-routing-butterfly/VERIFY.json new file mode 100644 index 0000000000..a6ff071340 --- /dev/null +++ b/research/sector-routing-butterfly/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 570, + "checks": "All-column group-ring identities, reverse oracle, retained-input contract, exact native actions, source hashes and rejection controls" + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 570, + "checks": "All-column group-ring identities, reverse oracle, retained-input contract, exact native actions, source hashes and rejection controls" + } + ] +} diff --git a/research/sector-routing-butterfly/inputs/SECTOR-PROOF.md b/research/sector-routing-butterfly/inputs/SECTOR-PROOF.md new file mode 100644 index 0000000000..ee7035ca6d --- /dev/null +++ b/research/sector-routing-butterfly/inputs/SECTOR-PROOF.md @@ -0,0 +1,177 @@ +# Exact query count over ordinary involution sectors + +Ali Romman with substantial OpenAI Codex assistance. Apache-2.0. + +## 1. Model and result + +Let J_0,...,J_(s-1) be commuting ordinary involutions, with s >= 1. +Let Q commute with them and satisfy Q squared = J_0. Write J_mask for +the product selected by the binary mask. A scalar coefficient acts on role +indices and is applied once, not once per address column. + +Consider the prescribed linear map from n input fields to m output fields + + F = A(J) + B(J) Q, + A(J) = sum_mask A_mask J_mask, + B(J) = sum_mask B_mask J_mask. + +A program can use arbitrary scalar combinations of the J_mask, zero owned +storage, COPY, CLEAR, and Q or Q inverse on one whole field per paid query. +Queries can be interleaved with ordinary operations, and later queries can +use earlier results. The program is a fixed linear program. It does not +branch on runtime data. Other address maps and higher-rank Gaussian queries +are not in this lower-bound alphabet. + +For a sign vector sigma, let + + E_sigma = product_j (I + sigma_j J_j)/2, + B_sigma = sum_mask product_(j in mask) sigma_j B_mask. + +Assume each sector is nonzero and Q is not a scalar on that sector. Equivalently, +I and Q are linearly independent there. Then the exact minimum paid count is + + q_min = max_sigma rank(B_sigma). + +The same upper bound holds without the independence assumption. In that case +it need not be minimal. The compiler uses the full formal Boolean algebra, +so it does not silently discard a sector that is empty in a particular model. + +This generalizes the sufficient two-sector construction in PR5578 T6. The +new results are the matching lower bound for interleaved queries, the exact +dyadic emitter, the extension to any finite Boolean family, and the sharp +role-gauge consequence in Section 5. No complete caller or kappa is supplied. + +## 2. Lower bound with arbitrary feedback and storage + +Fix one sector. Every ordinary operation is now scalar on address space. +Represent each live wire, as a function of the original independent inputs, +by an even coefficient row plus an odd coefficient row times Q. The relation +Q squared = sigma_0 keeps this form after every query. The representation is +unique because I and Q are independent on the sector. + +At entry every odd row is zero. Ordinary scalar operations, copies and clears +cannot increase the dimension of the span of all available odd rows. A query +on a wire with coefficients (a,b) changes them to (sigma_0 b,a). Thus it adds +at most one new row a to the total odd-row span. Keeping the old wire or extra +copies does not increase this limit. A Q inverse query differs by the ordinary +scalar sigma_0 and has the same bound. + +After q queries, every odd output row lies in a space of dimension at most q. +The required odd output matrix is B_sigma. Hence q >= rank(B_sigma) for every +sector. This proves the lower bound without a one-layer, no-reuse or no-feedback +assumption. Arbitrary initial owned dirt cannot improve it: set that independent +dirt to zero and obtain the same required map on the main inputs. + +## 3. Attainment with exact dyadic coefficients + +Take rank factorizations B_sigma = U_sigma V_sigma. Pad their inner dimensions +to q = max rank(B_sigma), and put + + U = sum_sigma U_sigma E_sigma, + V = sum_sigma V_sigma E_sigma. + +Complementary sectors satisfy E_sigma E_tau = 0 for sigma != tau and their +sum is I. Consequently UV=B(J). Since every factor commutes with Q, the word + + gather z = Vx; query Q on each of the q z fields; + output y = A(J)x + UQz; clear z + +has endpoint F on every input. The symbol Qz in the scatter means the queried +version of z; the word contains exactly q queries in total. All inputs remain +unchanged during the gather and scatter. Output and work buffers are cleared +before their first read, so their arbitrary initial dirt has no effect. + +Dyadic B_sigma admit rank factorizations over the dyadic ring Z[1/2]. To obtain +one, multiply by a common power-of-two denominator d and use integer Smith +form U0(d B_sigma)V0=S. Both U0 and V0 are unimodular, so their inverses have +integer entries. The first r columns of U0 inverse, multiplied by the nonzero +diagonal entries of S/d, and the first r rows of V0 inverse give the required +factorization. There is no division by a nonunit odd pivot. + +The inverse Walsh transform divides only by 2^s. Thus every emitted gather, +scatter and direct coefficient is dyadic. The retained PR5615 Smith utility +supplies the factorization step. Each use is checked by exact multiplication +and by the integrality of both inverse basis matrices. The replay computes +the rank again by a separate rational elimination with opposite pivot order. + +The compiler emits only CLEAR, shifted scalar ADD and QUERY. It uses m+q +owned fields, including the m output fields. It emits m+2q CLEARs, and at most +2^s(mn+qn+mq) shifted ADDs. Zero coefficients are omitted. A shifted ADD reads +J_mask applied to its source. That address action, coefficient implementation, +movement and field pass all have real nonrecursive costs. The emitted counts +and coefficient bit sizes are component data, not a machine compiler bill. + +## 4. Actual lifted Gaussians and a larger sharp example + +For the usual lifted central Gaussian Q_f, its square is the ordinary +translation that flips that axis in every digit column. Take this as J_0. +Additional independent spectator-axis translations supply J_1,...,J_(s-1). +They commute with Q_f and with one another. In the Fourier basis the possible +central eigenvalues are i^k for 0 <= k <= f. For f >= 3, both square roots of +each sign occur. Independent spectator signs leave each Boolean sector +nonempty. The hypotheses of Section 1 therefore hold for every f >= 3. +The construction remains valid for f=1,2, but the minimum claim is not made +there because one or more sectors can make Q scalar. + +For each of the 2^s sectors give one independent field x_sigma the map + + x_sigma -> x_sigma + (1/2) Q E_sigma x_sigma. + +Every B_sigma has rank one. Separate sector queries use 2^s requests; the +compiler uses exactly one. The map is invertible: each diagonal perturbation +has norm at most 1/2, so its inverse norm is at most 2. These outputs are not +canonical Gaussian targets and earn no such credit. The compiler emits the +forward map only; a dyadic exact inverse is not assumed. + +The verified examples include 2,4,8,16 and 32 sectors. The 32-sector example +uses one query, 2080 shifted ADDs, 34 CLEARs and 33 owned fields including +outputs. This exposes the ordinary-work tradeoff rather than treating sector +selection as free. The two-sector case is exactly the credited PR5578 T7 map. +Its literal tensor Gaussian matrices are checked at widths 1 through 4. + +## 5. Scalar role-gauge boundaries already attain the minimum + +Let P and R be scalar role projectors and M an invertible scalar matrix. +The boundary G_R(Q) M G_P(Q) inverse, where G_P(Q)=I+(Q-I)P, has + + A = (I-R) M (I-P) + R M P, + B(J_0) = R M (I-P) + J_0 (I-R) M P. + +Choose bases that split each projector's image and kernel. The two summands +of B_sigma occupy disjoint input and output blocks, for either sign of J_0. +Their total rank is + + rank(R M - M P). + +This is the tariff already supplied as an upper bound by PR5578 T3. Sections +1-3 prove that it is exact in the present query alphabet, even with interleaved +queries, extra ordinary spectator sectors and feedback. Thus this form of +sector packing cannot lower an already factored scalar role-gauge boundary. +A lower complete cost must change the boundary defect or the permitted maps. +The statement does not cover noncommuting address-valued role matrices. + +## 6. Evidence and limits + +The exact replay covers every ordered pair of 2 by 2 sector matrices with +entries -1,0,1, plus rectangular dyadic cases, noncoordinate role projectors, +and interleaved feedback words. It compares complete polynomial actions on +all original inputs and arbitrary initial owned values. A separate literal +tensor-matrix check covers the source two-field example. Corrupt query, sector +mask and cleanup words reject, as does a nondyadic input. + +The lower bound is a written proof for the stated algebra. Finite checks are +corroboration, not a formal kernel or independent human review. No actual +selected-caller section has been replaced. Native addresses outside the +specified involution algebra, higher-rank queries, precision, tape movement, +compiler reserves and the full supplier/outer join remain separate obligations. + +## 7. Attribution + +Dugongue PR5578 T6/T7 supplies two-sector packing and the two-field example; +T3 supplies the role-gauge upper bound. PR5586 C8 names the completed-caller +target. Retain Cao Yifan, DaysSky, Cinna Davis, Nick Petalas, Ryanson Jonathan, +zxv, Jacob Alan Sussman and all source authors named in the pinned notes. +Ali Romman PR5615 supplies the unchanged Smith routine, following the classical +Smith method and the earlier dyadic Euclidean work of Nick Petalas. Boolean +Fourier decomposition and rank factorization are standard methods. The input +files retain their original credit and AI disclosures. diff --git a/research/sector-routing-butterfly/inputs/SECTOR-RESULT.json b/research/sector-routing-butterfly/inputs/SECTOR-RESULT.json new file mode 100644 index 0000000000..61c14d779c --- /dev/null +++ b/research/sector-routing-butterfly/inputs/SECTOR-RESULT.json @@ -0,0 +1,50 @@ +{ + "complete_two_by_two_sector_pairs": 6561, + "strict_sharing_pairs": 6400, + "rectangular_cases": 72, + "role_gauge_cases": 72, + "feedback_words": 160, + "feedback_queries_removed": 558, + "rejection_controls": 4, + "physical_basis_cases": 60, + "examples": [ + { + "generators": 1, + "query_count": 1, + "ordinary_adds": 10, + "ordinary_clears": 4, + "owned_fields_including_outputs": 3 + }, + { + "generators": 2, + "query_count": 1, + "ordinary_adds": 36, + "ordinary_clears": 6, + "owned_fields_including_outputs": 5 + }, + { + "generators": 3, + "query_count": 1, + "ordinary_adds": 136, + "ordinary_clears": 10, + "owned_fields_including_outputs": 9 + }, + { + "generators": 4, + "query_count": 1, + "ordinary_adds": 528, + "ordinary_clears": 18, + "owned_fields_including_outputs": 17 + }, + { + "generators": 5, + "query_count": 1, + "ordinary_adds": 2080, + "ordinary_clears": 34, + "owned_fields_including_outputs": 33 + } + ], + "example_word_sha256": "668b6303a9526fe613b154aeae45e5082fa39be3431c1aeb57c96d3488d89891", + "lower_bound_scope": "Faithful sectors; scalar combinations of the declared involutions; Q or inverse Q on one field", + "no_new_kappa": true +} diff --git a/research/sector-routing-butterfly/inputs/TYPED-PROVIDER.md b/research/sector-routing-butterfly/inputs/TYPED-PROVIDER.md new file mode 100644 index 0000000000..cc190c322d --- /dev/null +++ b/research/sector-routing-butterfly/inputs/TYPED-PROVIDER.md @@ -0,0 +1,164 @@ +# Typed Gaussian providers, subspace gauges and sector-multiplexed queries + +Dugongue, with substantial OpenAI Codex assistance. Informal mathematics based only on local source and proof-tree scans. No numerical experiment, solver, web search or Lean check was used. The constructions below have complete all-input operator proofs on their stated domains; they do not assert an unproved profitable provider or a larger numerical κ. + +## Sources and actual starting contract + +The actual local sources are `research/native-dual-suppliers/HETEROGENEOUS-CONTROLLER.md`, `FREE-ENDPOINT-GAUGES.md`, `DUAL-PROVIDER.md` and `ROUND3-IMPROVEMENT.md`; the scalar event definition in `research/kappa-rebuild/bit/complex_controller_factor.py` was read as text and was not executed. The preceding mathematical continuation supplies `boundary.md` and `consumer.md`. The linked symplectic balanced-coevaluation and mode-support notes motivate reciprocal-dual and invariant-subspace bookkeeping; no fresh formal verification is inferred from those sources. + +The admitted B and C local words have 112 independent main pairs, 408 independent helper fields, and respectively 56 A plus 56 B or C ports. Their exact main types are + + A = D [[1,0],[Q^(-1),1]], + B = D [[1,0],[1,Q]], + C = D [[Q,0],[1,1]], + +where D acts on seven fresh axes and Q on the common central axis. Helpers and paid Gaussian jobs retain their individually stated profiles. Arbitrary main-pair permutations place the exceptional ports but do not identify helper inputs. Backward calls use the actual inverse-transpose endpoints with their even-power monomial corrections. + +Credit Cao Yifan for the retained native round-three word, DaysSky for the quotient construction, Cinna Davis and the controller lineage, Nick Petalas and Ryanson Jonathan for endpoint analysis, Dugongue for transported/repaired interfaces, zxv and Jacob Alan Sussman for compiler foundations, and all retained Gaussian/Clifford/source08 contributors. Ordinary rank factorization, projector decomposition, nullity and elementary matrix identities are classical. The new applications here are the precisely stated fusion, projection-gauge and sector-query interfaces. + +## T1. Complete exceptional-port extraction and two-call fusion + +Let S_y(t)=[[1,0],[t,1]], and suppress the common commuting D factor for a moment. + +**Theorem.** Exceptional B and C ports have the exact ordinary-boundary extractions + + S_y(−1) B = D diag(1,Q), + C S_y(−1) = D diag(Q,1). + +For two calls on the same pair, with arbitrary commuting fresh factors D_1,D_2, + + C_2 B_1 = D_2 D_1 Q S_y(2Q^(-1)), + S_y(−1) B_2 C_1 = D_2 D_1 Q S_y(Q^(-1)). + +**Proof.** In the first identity subtract the first output row of B from its second. In the second replace the first input contribution in C's second row by its difference with the second input. Both are the stated elementary shear and give the displayed diagonals on arbitrary independent inputs. + +For the two-call products multiply the two explicit matrices: + + [[Q,0],[1,1]] [[1,0],[1,Q]] = [[Q,0],[2,Q]], + [[1,0],[1,Q]] [[Q,0],[1,1]] = [[Q,0],[1+Q,Q]]. + +Factor out the common Q; in the second product the remaining shear is S_y(1+Q^(-1)), whose ordinary S_y(1) factor is removed on the left. Restore the commuting D factors. ∎ + +The direct B extraction is inherited predecessor work, including the PR4660 extraction discussion; it is not claimed anew. The combined formulas supply explicit homogeneous-shear fusion rules. The ordinary A-A pair is D_2D_1 S_y(2Q^(-1)), and scalar diagonal conjugation normalizes its factor 2 without Gaussian work. + +The common Q in the exceptional two-call formula is the existing central coordinate. Repeating the construction produces powers of that same Q, whose even powers are ordinary monomials. It does not create one fresh Gaussian rank per fused block. Likewise the free extraction on 56 ports does not diagonalize the other 56 A ports. A full caller must retain these exact facts when adding targets and costs. + +## T2. A Gaussian gauge on an ordinary role subspace + +Work over a field K of characteristic not 2 and let V be the data space. A scalar role projector P is an idempotent n by n matrix over K. It acts only on the n role indices, and therefore commutes with a common Gaussian Q on V. Define + + G_P(Q) = I + (Q−I)P. + +**Theorem.** G_P(Q) is invertible, with inverse G_P(Q^(-1)). It is ordinary-conjugate to Q on rank(P) role fields and identity on the other fields. It can be applied with rank(P) charged Gaussian jobs and explicit ordinary boundaries. + +**Proof.** The role space is the direct sum im(P) ⊕ ker(P): x=Px+(I−P)x, and the intersection is zero. Choose a basis in each summand and combine them into an ordinary scalar basis matrix U. In that basis P is diag(I_r,0), so G_P(Q) is diag(QI_r,I). The asserted inverse and construction follow. Alternatively, multiply the two displayed polynomial expressions in P and use P²=P. ∎ + +This is a changed gauge representation, not a claim that Q on an arbitrary role subspace is free. The basis maps and all Gaussian requests are specified. For a fixed finite template the ordinary maps have fixed coefficient data and actual finite field-pass cost. + +## T3. Coordinate-free rank tariff for an ordinary boundary + +Let M be an invertible scalar role matrix, with an input projector P and output projector R. Put + + F = G_R(Q) M G_P(Q)^(-1), + E = R M − M P. + +**Theorem.** There is an explicit all-input boundary construction for F using rank(E) charged Q or Q^(-1) jobs, ordinary linear operations and O(n) owned field buffers returned to zero. If E=0, F=M and no Gaussian correction is needed. + +**Proof.** Choose ordinary bases diagonalizing P on inputs and R on outputs. In those bases write M in four blocks M_00,M_01,M_10,M_11, according to the zero/one projector sectors. The physical boundary has ordinary diagonal blocks and crossed blocks M_01Q^(-1),M_10Q. The transformed E has crossed blocks −M_01 and M_10 and zero diagonal blocks; their input and output supports are disjoint, so + + rank(E)=rank(M_01)+rank(M_10). + +Rank-factor each crossed scalar block. Form its inner scalar combinations in owned temporary fields from one unchanged input snapshot, query each combination once, and distribute through the outer rank factor. Accumulate both direct and crossed terms in an owned output bank, swap it into the main bank after the last read, and clear the old bank and temporaries. This produces exactly F on every independent input and preserves unrelated fields. All Gaussian calls are counted. If E=0 the intertwining identity RM=MP gives G_R M=M G_P, hence F=M. ∎ + +This extends the row-bit boundary tariff to arbitrary scalar role subspaces. It does not extend it to an arbitrary matrix whose entries are noncommuting address operators. + +## T4. Composition and reciprocal-dual compatibility + +**Theorem.** For scalar M_1,M_2 and projectors P_0,P_1,P_2, define + + E_1=P_1M_1−M_1P_0, + E_2=P_2M_2−M_2P_1. + +Then the whole-boundary defect obeys + + P_2M_2M_1−M_2M_1P_0 = E_2M_1+M_2E_1, + +so its rank is at most rank(E_1)+rank(E_2). For invertible M, the reciprocal-dual defect is + + R^T M^(-T) − M^(-T) P^T + = M^(-T) (RM−MP)^T M^(-T), + +and has exactly the same rank. + +**Proof.** Expand the first identity; the two terms containing M_2P_1M_1 cancel. Rank is subadditive and cannot increase under multiplication. For the second identity transpose RM−MP and multiply by M^(-T) on both sides. Invertible left/right factors preserve rank. The dual gauge is G_(P^T)(Q^(-T)), so T3 applies to the actual reciprocal-dual operator at that same tariff. ∎ + +The global defect can have lower rank than the sum of local defects, including exact cancellation. This justifies compressing a completed ordinary boundary as one matrix rather than pricing a chosen ADD factorization as though its separate corrections could never share. + +## T5. Zero-correction endpoint gauges inside actual multiplicity spaces + +Assume a complete reference word satisfies + + L M R_0 = T, + +where L and R_0 are ordinary invertible scalar boundaries and T is the actual independent-output operator. Assume each target block of T commutes with the common Q. Suppose the internal entrance and exit gauges are G_A(Q) and G_B(Q), and there is a projector P such that + + R_0^(-1) A R_0 = P = L B L^(-1), + PT=TP. + +**Theorem.** The gauged interior has the exact same independent target under the same ordinary boundary maps: + + L G_B(Q) M G_A(Q)^(-1) R_0 = T. + +No Gaussian correction at those two boundaries is needed. + +**Proof.** The first projector identity gives G_A(Q)^(-1)R_0=R_0G_P(Q)^(-1). The second gives L G_B(Q)=G_P(Q)L. Therefore the left side is G_P(Q) T G_P(Q)^(-1). Since P commutes with T and the actual target blocks commute with the common Q, this equals T. All input fields remain arbitrary and independent because the complete endpoint is exactly the original T. ∎ + +For a scalar projector and T=diag(T_i), its commutator has entries P_ij(T_j−T_i). Thus a sufficient source of such projectors is an actual multiplicity block where the operators T_i are exactly identical. Equal Gaussian rank alone is not equality of these operators. Address-dependent normalizers must be included explicitly before applying the scalar statement. + +The theorem is a constructive admission criterion. This note has not supplied A,B satisfying it for a profitable complementary-provider schedule, so no free boundary in the current provider is asserted merely from the existence of this criterion. + +## T6. Sector-multiplexed Gaussian queries + +Suppose Q²=J and J is an ordinary involution, J²=I. Define E_+=(I+J)/2 and E_-=(I−J)/2. These are complementary ordinary projectors commuting with Q. Let A_+,A_- be scalar role matrices, with ranks r_+,r_-, and let + + A=A_+E_+ + A_-E_-. + +**Theorem.** The vector contribution A Q x can be computed using + + max(r_+,r_-) + +charged Gaussian jobs, explicit ordinary operations and cleared owned storage. + +**Proof.** Choose rank factorizations A_σ=U_σV_σ. Pad each inner dimension with zero rows/columns to r=max(r_+,r_-). Put + + U=U_+E_+ +U_-E_-, + V=V_+E_+ +V_-E_-. + +Scalar role matrices commute with the sector projectors. Since E_+E_-=0 and E_++E_-=I, UV=A. Form the r temporary fields Vx, apply Q once to each, and spread by U. Because Q commutes with all entries of U,V, the result is A Q x. Each temporary packs disjoint projected components, whose dimensions sum to the original data-space dimension; it does not pack two independent full data fields into one without accounting for information. Clear the owned storage after accumulation. ∎ + +For the actual lifted central Gaussian Q_f, Q_f² is the explicit translation that flips the selected bit in every digit column. E_± are therefore finite combinations of two ordinary monomial maps, uniformly in the lift width. The theorem has a concrete ordinary implementation and does not require a width-dependent spectral decomposition. + +## T7. A complete strict query-sharing example + +**Theorem.** Let Q be unitary with Q²=J as above. The invertible two-field map + + x ↦ x + (1/4)(Q+Q^(-1))x, + y ↦ y + (1/4)(Q−Q^(-1))y + +has an implementation using one Q job, plus ordinary operations and cleared owned storage. Its inverse norm is at most 2 in Euclidean norm. + +**Proof.** Since Q^(-1)=QJ, + + Q+Q^(-1)=2QE_+, + Q−Q^(-1)=2QE_-. + +Form z=E_+x+E_-y in an owned temporary, query Qz once, and return x+(1/2)E_+Qz and y+(1/2)E_-Qz. Orthogonality of the complementary sectors proves the two displayed outputs. The block-diagonal perturbation of identity has norm at most 1/2, so its Neumann inverse has norm at most 2. This norm argument establishes invertibility, not an unpriced inverse algorithm. The one-query forward construction is already explicit. ∎ + +The literal four-term implementation uses four Q or Q^(-1) calls; merely factoring the two odd expressions separately uses two. Sector multiplexing reduces that explicit tariff to one while preserving the full stated all-input map. These outputs are not declared canonical independent Gaussian targets. To improve κ this pattern must occur inside a completed provider whose original independent endpoint remains unchanged. + +## Exact contribution and κ status + +T1 supplies exact fusion normal forms for the actual typed B/C operators. T2–T5 provide role-subspace gauge admission and complete boundary tariffs, including duals. T6–T7 give a concrete way to share Gaussian queries across ordinary involution sectors, with a strict full-map example. + +A higher κ still requires a particular complete supplier whose actual paid profile is decreased by one of these replacements while preserving its independent target operators and uniform compiler premises. No such profitable B/C instance was established in this note. The constructions are positive, fully stated tools for that task; they are not a claim that the complex-only quotient headline has already satisfied the missing controller contract. + diff --git a/research/sector-routing-butterfly/inputs/packing.py b/research/sector-routing-butterfly/inputs/packing.py new file mode 100644 index 0000000000..6925652078 --- /dev/null +++ b/research/sector-routing-butterfly/inputs/packing.py @@ -0,0 +1,159 @@ +#!/usr/bin/env python3 +"""Compile exact dyadic Gaussian queries over ordinary Boolean sectors. + +Ali Romman with substantial OpenAI Codex assistance. Apache-2.0. +Sector packing follows Dugongue PR5578 T6. The Smith routine is retained +from Ali Romman PR5615 with its original header. +""" +from fractions import Fraction as Q +from hashlib import sha256 +from pathlib import Path +import argparse +import importlib.util +import json + +HERE = Path(__file__).resolve().parent + + +def need(test, message): + if not test: + raise ValueError(message) + + +def load_smith(): + path = HERE / 'vendor/capacity.py' + need(sha256(path.read_bytes()).hexdigest() + == '1cd82b0beab7983d955cfc1d1e562af490f90bcaad6e3ec7d07e0c5a33608834', + 'Smith source bytes') + spec = importlib.util.spec_from_file_location('retained_smith', path) + module = importlib.util.module_from_spec(spec) + spec.loader.exec_module(module) + return module.smith + + +smith = load_smith() + + +def eye(n): + return [[Q(i == j) for j in range(n)] for i in range(n)] + + +def inverse(matrix): + n = len(matrix) + data = [list(map(Q, row)) + identity for row, identity in zip(matrix, eye(n))] + for j in range(n): + pivot = next((i for i in range(j, n) if data[i][j]), None) + need(pivot is not None, 'Invertible Smith factor') + data[pivot], data[j] = data[j], data[pivot] + value = data[j][j] + data[j] = [x / value for x in data[j]] + for i in range(n): + if i != j: + value = data[i][j] + data[i] = [x - value * y for x, y in zip(data[i], data[j])] + return [row[n:] for row in data] + + +def rank_factor(matrix): + m, n = len(matrix), len(matrix[0]) + denominator = max(x.denominator for row in matrix for x in row) + integer = [[int(denominator * x) for x in row] for row in matrix] + left, diagonal, right = smith(integer) + li, ri = inverse(left), inverse(right) + need(all(x.denominator == 1 for z in (li, ri) for row in z for x in row), + 'Unimodular Smith factors') + rank = sum(diagonal[i][i] != 0 for i in range(min(m, n))) + u = [[li[i][k] * Q(diagonal[k][k], denominator) for k in range(rank)] + for i in range(m)] + v = ri[:rank] + need(all(sum(u[i][k] * v[k][j] for k in range(rank)) == matrix[i][j] + for i in range(m) for j in range(n)), 'Exact factorization') + return u, v, rank + + +def sign(mask, sector): + return -1 if (mask & sector).bit_count() % 2 else 1 + + +def validate(even, odd): + count = len(even) + need(count >= 2 and count & (count - 1) == 0 and len(odd) == count, + 'Power-of-two sector count, at least two') + m, n = len(even[0]), len(even[0][0]) if even[0] else 0 + need(m > 0 and n > 0, 'Nonempty matrix') + result = [] + for parts in (even, odd): + converted = [] + for matrix in parts: + need(len(matrix) == m and all(len(row) == n for row in matrix), 'Matrix shape') + values = [[Q(x) for x in row] for row in matrix] + need(all(x.denominator & (x.denominator - 1) == 0 + for row in values for x in row), 'Dyadic coefficients') + converted.append(values) + result.append(converted) + return result[0], result[1], count, m, n + + +def compile_map(even, odd): + """Return a word for sum_mask (A_mask + B_mask Q) J_mask.""" + even, odd, count, m, n = validate(even, odd) + factors = [] + for sector in range(count): + matrix = [[sum(sign(mask, sector) * odd[mask][i][j] + for mask in range(count)) for j in range(n)] for i in range(m)] + factors.append(rank_factor(matrix)) + queries = max(r for _, _, r in factors) + u_parts, v_parts = [], [] + for mask in range(count): + u_parts.append([[sum(sign(mask, sector) * + (factors[sector][0][i][k] if k < factors[sector][2] else 0) + for sector in range(count)) / Q(count) + for k in range(queries)] for i in range(m)]) + v_parts.append([[sum(sign(mask, sector) * + (factors[sector][1][k][j] if k < factors[sector][2] else 0) + for sector in range(count)) / Q(count) + for j in range(n)] for k in range(queries)]) + outputs = list(range(n, n + m)) + work = list(range(n + m, n + m + queries)) + program = [['CLEAR', r] for r in outputs + work] + + def add_matrix(parts, destinations, sources): + for mask, matrix in enumerate(parts): + for i, row in enumerate(matrix): + for j, coefficient in enumerate(row): + if coefficient: + program.append(['ADD', destinations[i], sources[j], str(coefficient), mask]) + + add_matrix(even, outputs, list(range(n))) + add_matrix(v_parts, work, list(range(n))) + program.extend(['QUERY', r] for r in work) + add_matrix(u_parts, outputs, work) + program.extend(['CLEAR', r] for r in work) + coefficients = [Q(event[3]) for event in program if event[0] == 'ADD'] + need(all(x.denominator & (x.denominator - 1) == 0 for x in coefficients), + 'Emitted dyadic coefficients') + return {'schema': 'boolean-sector-query-word/v1', 'generators': count.bit_length() - 1, + 'input_fields': n, 'output_fields': m, 'query_count': queries, + 'sector_ranks': [r for _, _, r in factors], + 'owned_fields_including_outputs': m + queries, + 'ordinary_adds': len(coefficients), 'ordinary_clears': m + 2 * queries, + 'max_coefficient_numerator_bits': max((abs(x.numerator).bit_length() for x in coefficients), default=0), + 'max_coefficient_denominator_bits': max((x.denominator.bit_length() - 1 for x in coefficients), default=0), + 'output_registers': outputs, 'work_registers': work, 'program': program} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('input', type=Path) + parser.add_argument('--output', type=Path, required=True) + args = parser.parse_args() + source = json.loads(args.input.read_text()) + word = compile_map(source['even'], source['odd']) + with args.output.open('x') as stream: + json.dump(word, stream, indent=2) + stream.write('\n') + print('EMITTED_SECTOR_QUERY_WORD', word['query_count'], word['ordinary_adds']) + + +if __name__ == '__main__': + main() diff --git a/research/sector-routing-butterfly/routing.py b/research/sector-routing-butterfly/routing.py new file mode 100644 index 0000000000..c6d9e910c5 --- /dev/null +++ b/research/sector-routing-butterfly/routing.py @@ -0,0 +1,56 @@ +"""Compile sector maps with distinct-role ADDs and ordinary shifts.""" +from fractions import Fraction as F + + +def emit(s, r=1, mode="perturbation"): + if s < 1 or r < 1 or mode not in ("perturbation", "gauge"): + raise ValueError("invalid circuit parameters") + n = 1 << s + word = [] + def add(dst, src, c, mask=0): + word.append(("ADD", dst, src, F(c), mask)) + def route(offset): + for k in range(s): + for a in range(n): + if a & (1 << k): + continue + x, y = offset+a, offset+a+(1 << k) + for dst, src, sign in ((x,y,1),(y,x,-1),(x,y,1)): + add(dst,src,F(sign,2)) + add(dst,src,F(-sign,2),1 << k) + word.append(("SHIFT",y,1 << k)) + if mode == "perturbation": + word.append(("CLEAR", r*n)) + for b in range(r): + x = b*n + route(x) + if mode == "perturbation": + add(r*n,x,1) + word.append(("QUERY",r*n)) + add(x,r*n,F(1,2)) + word.append(("CLEAR",r*n)) + else: + word.append(("QUERY",x)) + route(x) + return word + + +def tariff(s, r, mode): + n = 1 << s + return dict(QUERY=r, ADD=6*r*n*s+(2*r if mode=="perturbation" else 0), + SHIFT=r*n*s, CLEAR=r+1 if mode=="perturbation" else 0, + owned=1 if mode=="perturbation" else 0) + + +def emit_preserving(s, r=1, mode="perturbation"): + """Keep the inputs and put the result in separate output fields.""" + size = r*(1 << s) + word = [] + for i in range(size): + word.extend([("CLEAR",size+i),("ADD",size+i,i,F(1),0)]) + for op in emit(s,r,mode): + if op[0]=="ADD": + word.append((op[0],op[1]+size,op[2]+size,*op[3:])) + else: + word.append((op[0],op[1]+size,*op[2:])) + return word diff --git a/research/sector-routing-butterfly/verify.py b/research/sector-routing-butterfly/verify.py new file mode 100644 index 0000000000..614981a8dd --- /dev/null +++ b/research/sector-routing-butterfly/verify.py @@ -0,0 +1,242 @@ +"""Check all columns in the group ring and exact native address actions.""" +import hashlib +import json +from collections import Counter +from fractions import Fraction as F +from pathlib import Path +import sys +sys.path.insert(0, str(Path(__file__).resolve().parent)) +from routing import emit, emit_preserving, tariff +P = Path(__file__).resolve().parent + + +def require(ok, why): + if not ok: + raise RuntimeError(why) + + +def shift(g, mask): + return g ^ ((mask & 1)*2) ^ ((mask >> 1) << 2) + + +def query(g): + return (g & ~3) | ((g+1) & 3) + + +def transform(row, fn): + return {(a,fn(g)):c for (a,g),c in row.items()} + + +def plus(a,b,c=F(1)): + out = a.copy() + for key, value in b.items(): + out[key] = out.get(key,F(0)) + c*value + if not out[key]: + del out[key] + return out + + +def run_ring(word, width, adjoint=False): + rows = [{(i,0):F(1)} for i in range(width)] + colnorm = [F(1)]*width + rownorm = [F(1)]*width + maximum = F(1) + for op in reversed(word) if adjoint else word: + dst = op[1] + if op[0] == "ADD": + _,dst,src,c,mask = op + if adjoint: + dst,src = src,dst + require(dst != src, "same-role ADD") + row = plus(rows[dst],transform(rows[src],lambda g:shift(g,mask)),c) + elif op[0] == "SHIFT": + row = transform(rows[dst],lambda g:shift(g,op[2])) + elif op[0] == "QUERY": + row = transform(rows[dst],query) + elif op[0] == "CLEAR": + row = {} + else: + raise RuntimeError("unknown instruction") + for (a,_),c in rows[dst].items(): + colnorm[a] -= abs(c) + for (a,_),c in row.items(): + colnorm[a] += abs(c) + rows[dst] = row + rownorm[dst] = sum(map(abs,row.values()),F(0)) + maximum = max(maximum, max(colnorm if adjoint else rownorm)) + return rows, maximum + + +def expected(s,r,mode): + n = 1 << s + width = r*n + (mode=="perturbation") + out = [{} for _ in range(width)] + for i in range(r*n): + a = i % n + out[i] = {(i,0):F(1)} + for mask in range(n): + c = F((-1)**((a & mask).bit_count()),n) + g = shift(0,mask) + out[i] = plus(out[i],{(i,query(g)):c},F(1,2) if mode=="perturbation" else F(1)) + if mode=="gauge": + out[i] = plus(out[i],{(i,g):-c}) + return out + + +def transpose(rows): + out = [{} for _ in rows] + for i,row in enumerate(rows): + for (j,g),c in row.items(): + out[j][i,g] = c + return out + + +def zadd(a,b): + return (a[0]+b[0],a[1]+b[1]) + + +def zscale(c,a): + return (c*a[0],c*a[1]) + + +def native_q(v,f): + out = v[:] + for k in range(f): + for a in range(len(v)): + if a & (1 << k): + continue + b = a | (1 << k) + x,y = out[a],out[b] + sm = zadd(x,y) + df = zadd(x,zscale(-1,y)) + idf = (-df[1],df[0]) + out[a] = zscale(F(1,2),zadd(sm,idf)) + out[b] = zscale(F(1,2),zadd(sm,zscale(-1,idf))) + return out + + +def native_shift(v,mask,f): + address_mask = (((1 << f)-1) if mask & 1 else 0) | ((mask >> 1) << f) + return [v[a ^ address_mask] for a in range(len(v))] + + +def native_run(word, values, f): + rows = [v[:] for v in values] + for op in word: + dst = op[1] + if op[0]=="ADD": + src,c,mask = op[2:] + v = native_shift(rows[src],mask,f) + rows[dst] = [zadd(a,zscale(c,b)) for a,b in zip(rows[dst],v)] + elif op[0]=="QUERY": + rows[dst] = native_q(rows[dst],f) + elif op[0]=="SHIFT": + rows[dst] = native_shift(rows[dst],op[2],f) + else: + rows[dst] = [(F(0),F(0))]*len(rows[dst]) + return rows + + +def native_expected(values,s,r,f,mode): + n = 1 << s + out = [] + for i in range(r*n): + v = values[i] + e = [(F(0),F(0))]*len(v) + for mask in range(n): + c = F((-1)**(((i % n)&mask).bit_count()),n) + e = [zadd(a,zscale(c,b)) for a,b in zip(e,native_shift(v,mask,f))] + q = native_q(e,f) + out.append([zadd(a,zscale(F(1,2),b)) for a,b in zip(v,q)] if mode=="perturbation" else + [zadd(a,zadd(b,zscale(-1,c))) for a,b,c in zip(v,q,e)]) + if mode=="perturbation": + out.append([(F(0),F(0))]*len(values[0])) + return out + + +def local_norms(): + word = emit(1,1,"gauge")[:7] + rows,prefix = run_ring(word,2) + _,suffix = run_ring(word,2,True) + want = [{(0,0):F(1,2),(0,2):F(1,2),(1,0):F(1,2),(1,2):F(-1,2)}, + {(1,0):F(1,2),(1,2):F(1,2),(0,0):F(1,2),(0,2):F(-1,2)}] + require(rows==want, "controlled swap identity") + return prefix,suffix + + +def main(): + sources = json.loads((P/"PINS.json").read_text()) + for pin in sources: + require(hashlib.sha256((P/pin["file"]).read_bytes()).hexdigest()==pin["sha256"],"source hash") + local = local_norms() + require(max(local)<=2, "local norm") + cases = sorted({(s,1) for s in range(1,6)} | {(s,r) for s in range(1,4) for r in range(1,5)}) + records = [] + for s,r in cases: + for mode in ("perturbation","gauge"): + word = emit(s,r,mode) + expected_map = expected(s,r,mode) + rows,pre = run_ring(word,len(expected_map)) + rev,suf = run_ring(word,len(expected_map),True) + require(rows==expected_map, "all-column forward map") + require(transpose(rev)==expected_map, "reverse oracle") + count = Counter(op[0] for op in word) + bill = tariff(s,r,mode) + require(all(count[k]==v for k,v in bill.items() if k!="owned"), "exact tariff") + records.append(dict(s=s,r=r,mode=mode,**bill,prefix=str(pre),suffix=str(suf))) + preserving = [] + for s in range(1,6): + n = 1 << s + word = emit_preserving(s) + want = [{(i,0):F(1)} for i in range(n)] + expected(s,1,"perturbation") + rows,pre = run_ring(word,2*n+1) + rev,suf = run_ring(word,2*n+1,True) + require(rows==want and transpose(rev)==want,"input-preserving map") + count = Counter(op[0] for op in word) + require(count==Counter(ADD=6*n*s+n+2,SHIFT=n*s,QUERY=1,CLEAR=n+2),"preserving tariff") + preserving.append(dict(s=s,**dict(count),owned_including_outputs=n+1,prefix=str(pre),suffix=str(suf))) + baseline = json.loads((P/"inputs/SECTOR-RESULT.json").read_text())["examples"] + require(all(x["ordinary_adds"]==2*(1 << (2*x["generators"]))+(1 << x["generators"]) + and x["owned_fields_including_outputs"]==(1 << x["generators"])+1 + for x in baseline),"source comparison") + physical = 0 + for s in range(1,4): + for r in (1,2): + for f in range(1,5): + for mode in ("perturbation","gauge"): + width = r*(1 << s)+(mode=="perturbation") + values = [[(F(((i+3)*(a+2))%13-6,4),F((i+2*a)%7-3,2)) + for a in range(1 << (f+s-1))] for i in range(width)] + require(native_run(emit(s,r,mode),values,f)==native_expected(values,s,r,f,mode),"native map") + q2 = native_q(native_q(values[0],f),f) + require(q2==native_shift(values[0],1,f),"native Q square") + physical += 1 + word = emit(2,1,"perturbation") + want = expected(2,1,"perturbation") + mutants = {} + for name,kind in (("missing_query","QUERY"),("missing_shift","SHIFT"),("missing_entry_clear","CLEAR")): + idx = next(i for i,op in enumerate(word) if op[0]==kind) + mutants[name] = word[:idx]+word[idx+1:] + idx = max(i for i,op in enumerate(word) if op[0]=="CLEAR") + mutants["missing_final_clear"] = word[:idx]+word[idx+1:] + idx = next(i for i,op in enumerate(word) if op[0]=="ADD" and op[-1]) + bad = word[:] + bad[idx] = (*bad[idx][:-1],2) + mutants["wrong_involution"] = bad + for name,bad in mutants.items(): + require(run_ring(bad,len(want))[0]!=want,"undetected mutant: "+name) + require((F(3,2).numerator % 3)==0, "nonunit scale scope control") + result = dict(status="PASS_SECTOR_ROUTING_BUTTERFLY",formal_cases=records,preserving_cases=preserving,native_cases=physical, + local_controlled_swap_prefix=str(local[0]),local_controlled_swap_suffix=str(local[1]), + rejected_controls=list(mutants)+["nonunit_scale_not_invertible_mod_3"], + selected_frontier_changed=False,new_kappa_claim=False) + raw = json.dumps(result,indent=2,sort_keys=True)+"\n" + if "--write" in sys.argv: + (P/"RESULT.json").write_text(raw) + else: + require((P/"RESULT.json").read_text()==raw,"result mismatch") + print(result["status"],len(records),"formal cases",physical,"native cases",flush=True) + + +if __name__=="__main__": + main()