diff --git a/research/kb2-alt13-noncommuting-tooling/README.md b/research/kb2-alt13-noncommuting-tooling/README.md new file mode 100644 index 0000000000..db49244bf1 --- /dev/null +++ b/research/kb2-alt13-noncommuting-tooling/README.md @@ -0,0 +1,253 @@ +# Exact-search tooling for noncommuting words, and the KB2 six-distinct-value screen + +**Scoped negative plus reusable tooling; no new kappa.** This package has two +parts. (1) `exact_search.py` is reusable, dependency-free exact-search tooling +for noncommuting word/tuple enumeration over group rings `F2[G]` and matrix +rings `M_r(F2[G])` (instantiated for `GL_2(F2)` and `Q8`), with prefix closure +bounds, memoized layer-ball digests, a signature DP, `GL_r` conjugation +reduction and SHA256-receipted parallel-safe batch splitting. (2) It is +demonstrated on the strictly alternating thirteen-call five-SWAP candidate of +open problem KB2: the complete **six-distinct-value** family is exhaustively +searched and **excluded** (zero survivors over 323,963,640 placements and +700,496 exact `M_5(F2[G])` product evaluations). Seven or more distinct +projector values are **not** covered. The selected result, the selected bit +supplier and `upstream/` are unchanged. + +## Collision note (read first) + +KB2 is open question 1 of +[`research/fiveswap-alt13-commuting-screen`](https://github.com/CrocSwap/integer-mult-bounds/pull/2317): +find or exclude the strictly alternating thirteen-call word at five fully +occupied coordinate-SWAP roles in the formal `F2[GL_2(F2)]` +rank-one-idempotent register model. While this session ran, Ross Richardson +posted +[discussion 1317 comment 18944151](https://github.com/CrocSwap/integer-mult-bounds/discussions/1317#discussioncomment-18944151) +(2026-10-15 08:01 UTC) establishing the exclusion analytically: the PR 1989 +symmetric-adjacent-cut theorem, bridged to `F2[GL_2(F2)]` by the +product-preserving isomorphism `GL_2(F2) -> S_3`, gives exact cost `3t` for +every finite `R >= t`, all binary rank-one idempotents and arbitrary restored +dirty spectators — hence minimum 15 at `t = 5` +([PR 2415](https://github.com/CrocSwap/integer-mult-bounds/pull/2415), +package `research/gl2-swap-cut-corollary`). Per the session's pair-collision +rule the find-or-exclude object is **released to PR 2415** and not claimed +here. What this package adds is the solver tooling the predecessor named as +its blocker, and an explicitly independent, search-level audit of the +exclusion on the largest noncommuting family our tooling closes exactly. The +two lines agree; the search is not a proof of PR 2415's theorem and PR 2415's +theorem is not a replay of this search. + +## Model (unchanged coordinate-CNOT line) + +Let `a=[[1,1],[0,1]]`, `b=[[1,0],[1,1]]`, `s=aba=bab` in `G=GL_2(F2)`, +`R=F2[G]`. A paid call is `D_N(g)=I+([g]+1)N` with `g in {a,b}` and +`N=uv^T` a binary rank-one idempotent (`v^T u=1` over `F2`); there are +`(2^5-1)*2^4 = 496` such projectors in `M_5(F2)`. Free scalar `GL_5(F2)` +mixing is normalized by augmentation. The target is `T=[s] I_5` at exactly +`t=r=5` fully occupied roles with arbitrary dirty inputs restored exactly; +acceptance is equality of all formal group-algebra coefficients in +`M_5(F2[G])`. Word direction is irrelevant on the palindromic alternating +label word `(ab)^6a`. + +## Tooling (`exact_search.py`, Python stdlib only) + +- `Group`/`GroupAlgebra`: `F2[G]` from any multiplication table + (`gl2f2()`, `q8()`), exact bit-mask convolution. +- `M_r(F2)` and `M_r(F2[G])` arithmetic, rank-one idempotent alphabets, + call matrices, word products, targets. +- Quotient projections: the sign quotient `F2[epsilon]/(epsilon^2)` and the + natural 2-dimensional quotient. The combined map is checked to be an + algebra isomorphism `F2[S_3] = F2[epsilon]/(epsilon^2) x M_2(F2)`, so the + sign equation plus the four natural-quotient block equations are + **equivalent** to the full endpoint (machine-checked on random and + structured tuples). +- The `C`-matrix invariant `C_ij = v_i^T u_j`: `C^2 = C`, `rank C = 5`, and + the four projected block equations `C D^{p,q} C = C` (the predecessor's + handoff equations) are equivalent to the full endpoint. +- Search engine: BFS layer-ball digests (calibrated against the recorded + `Q8` balls `[1, 12, 110, 936]`), meet-in-the-middle join helper, the sign + prefix closure bound `rank(I - S_k) <= 13-k`, `GL_r` conjugation + reduction, SHA256-receipted `shard_split` batches for parallel workers, + and the signature DP + exact evaluator used below. +- Note on arithmetic: `F2[G]` is noncommutative, and the call scalars + `[g]+1` do **not** commute with group-ring entries of other calls. The + evaluator keeps every scalar at its own word position; a control compares + it against the generic product engine on random frame-plus-extra tuples + and on mutations. + +## Classification of low-distinct-value tuples + +Written proofs with exhaustive small-instance controls (over `F2^3`, 28 +projectors): + +1. **Parity and rank.** The sign equation `sum N_i = I_5` forces the number + `k` of odd-multiplicity projector values to satisfy `k >= 5` (rank) and + `k = 1 (mod 2)` (trace). +2. **Dual-frame lemma.** `t` rank-one idempotents summing to `I_t` are + automatically a dual frame: `C = V^T U` is a `t x t` idempotent which is + invertible because `UV^T = I`, hence `C = I`, i.e. `v_i^T u_j = + delta_ij`. Exhaustive over `F2^3` at `k = t = 3` (28 frames); at + `k = t+2` noncommuting summand sets exist (336 of them), so the collapse + is exactly `k = t`. +3. Hence any KB2 solution uses **at least 6 distinct projector values**; + `<= 5` distinct values are pairwise commuting, the family already + excluded by + [`research/fiveswap-alt13-commuting-screen`](https://github.com/CrocSwap/integer-mult-bounds/pull/2317) + (every frame class needs at least three positions, so 13 cannot fill 5 + classes). +4. **At exactly 6 distinct values** the 5 odd-multiplicity values form a dual + frame (free `GL_5` conjugation puts them at the coordinate projectors + `e_c e_c^T`) and the sixth value `W` has even multiplicity + `m_W in {2,4,6,8}` (`5 + m_W = 13` with all class multiplicities odd and + `m_W <= 8`). `W` is automatically noncommuting with the frame unless it + equals a frame projector, which is excluded by distinctness. This family + is what the search exhausts. + +## Search method and receipts + +For each `m = m_W`, one signature DP runs over **all** placements at once: a +state is the `S_5`-canonical tuple of (class segment products, parity) rows +plus the label word at the extra positions. The extra projector `uv^T` is +kept symbolic; every one of the 491 non-frame rank-one idempotents `W` is +tested against every signature by the exact `M_5(F2[G])` evaluator (the +predecessor's four block equations are recovered as an equivalent form). The +`S_5` canonicalization is complete because conjugation by any +`P in GL_5(F2)` preserves the target and every `W` is tested. A sound +diagonal pre-filter drops candidates early: the empty-subset term fixes entry +`(c,c)` to the class-`c` segment product, and every other term carries the +factor `u_c v_c`, so a mismatch with the target diagonal forces `u_c v_c=1`. + +Complete run (CPython 3.12, one core, 321 s): + +```text +m2: assignments=233719200 signatures=53055 peak_dp=850772 evals=255078 survivors=0 + sig_sha256=67e78c9d772d8a0d0296a290108874a3ff65b86563709e4b0a4137148e5fa693 +m4: assignments=82882800 signatures=183711 peak_dp=6728684 evals=403608 survivors=0 + sig_sha256=597a936da3fe9cf619aeb2fc104a6b4f8bbeaa7e52dcd68156577dabababde60 +m6: assignments=7207200 signatures=40523 peak_dp=9878765 evals=40523 survivors=0 + sig_sha256=84eb289160a6eecae3398b300a1314de49c60919107aceb5b5bc0cc7a97d4fd3 +m8: assignments=154440 signatures=1287 peak_dp=10218769 evals=1287 survivors=0 + sig_sha256=b247c3baf5e3ba07d51165f669306a30c598a9a2f012534c2baaa4bb9d015980 +PASS_KB2_ALT13_NONCOMMUTING_TOOLING assignments=323963640 evaluations=700496 +survivors=0 frontier=d6_complete_d_ge_7_open no_new_kappa elapsed=321.4s +``` + +`assignments` counts (extra-position pattern, class assignment) pairs with +all class multiplicities odd — i.e. the complete six-distinct-value placement +space at `t = 5`, `n = 13`. **Zero survivors**: no six-distinct-value tuple +realizes `[s] I_5` in thirteen strictly alternating calls. Together with the +predecessor's commuting exclusion this leaves only tuples with **seven or +more distinct projector values** as possible KB2 escapes; PR 2415's theorem +excludes those as well, analytically. + +## Controls (`verify.py`, all passing) + +- Direct words for `t = 1, 3, 5` (3/9/15 calls) reach `[s] I_t`; a mutated + word fails. +- The sign x natural image is an algebra isomorphism (bijective, + multiplicative), and sign + natural equations agree with the full endpoint + on 300 random tuples; the `C`-invariant agrees on the same tuples. +- `GL_5` conjugation invariance of the endpoint. +- Classification controls over `F2^3`: 28 dual frames at `k = t`; + 336 noncommuting 5-summand sets at `k = t+2`; no 4-summand identity. +- Fast evaluator equals the generic product engine on random frame-plus-extra + tuples; corrupting one segment product changes the result (mutation). +- `Q8` layer balls `[1, 12, 110, 936]` reproduce the recorded + [`q8-central-commutator-pair`](https://github.com/CrocSwap/integer-mult-bounds/pull/1822) + calibration (cross-algebra reuse). +- Shard manifests partition `0..999` and their SHA256 receipts are stable. +- Sign prefix closure bound accepted and rejected cases. +- **Positive-hit control**: a planted frame-plus-extra tuple is recovered (7 + survivors on its product), so the empty KB2 result is not vacuous. +- **Tiny completeness cross-check** at `t = 2`, `n = 6`: the signature search + returns exactly the direct enumeration of the same family (non-vacuous, + target = a planted family tuple). +- `tests/test_research_exact_word_search.py` re-runs 17 failure-sensitive + unit controls (including the two caught during development: a wrong + Gauss-Jordan pivot order and the noncommutative scalar placement). + +## Coverage and what is not checked + +This is a finite exact screen of a declared family plus written lemmas. It +does **not** cover tuples with seven or more distinct projector values, does +not reprove PR 2415 or PR 1989, and makes no partial-occupancy (`r > t`), +changed-tariff (asymmetric label prices, rank-two unit prices), +changed-endpoint or physical/compilation claim. No Lean formalization, +independent human review, precision/tape or analytic transfer is claimed. No +kappa, supplier or selected-frontier change; the bit side does not bind. The +result is author-checked only. + +## Reproduce + +Python 3.12 and the standard library suffice. From the repository root: + +```sh +python3 -I -B research/kb2-alt13-noncommuting-tooling/verify.py +python3 -B -m unittest tests.test_research_exact_word_search -v +python3 scripts/research_package.py --package research/kb2-alt13-noncommuting-tooling --check-only +``` + +Expected marker: `PASS_KB2_ALT13_NONCOMMUTING_TOOLING assignments=323963640 +evaluations=700496 survivors=0 frontier=d6_complete_d_ge_7_open no_new_kappa`. +`make` is not required and is unavailable on the recording host. + +## Task, overlap and credit + +Base main `0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2`, priority revision 4, +card `bit-new-register-model` (chooser OS nonce `56cf67ad450f0a4b6c78411360a6654f`), +scope **changed** by the orchestrator's tooling mandate (an authorized +explicit open request); [TASK.json](TASK.json) records the reason. The claim +and its scope update are in +[discussion 1317](https://github.com/CrocSwap/integer-mult-bounds/discussions/1317#discussioncomment-18944685). + +Predecessors and credit: Ross Richardson for +[PR 2415](https://github.com/CrocSwap/integer-mult-bounds/pull/2415) +(`research/gl2-swap-cut-corollary`, the concurrent analytic exclusion of the +same object, released to him) and +[PR 1989](https://github.com/CrocSwap/integer-mult-bounds/pull/1989) +(the `S_n` cut theorem); Ross Richardson +[`research/four-swap-full-occupancy`](https://github.com/CrocSwap/integer-mult-bounds/tree/main/research/four-swap-full-occupancy) +(rotation step, uniform cut consequence, open question 2); +Aaron Wang [PR 2317](https://github.com/CrocSwap/integer-mult-bounds/pull/2317) +(the commuting screen and the block-equation handoff this search consumes); +commdata2338 +[PR 1414](https://github.com/CrocSwap/integer-mult-bounds/pull/1414) / +[PR 1491](https://github.com/CrocSwap/integer-mult-bounds/pull/1491) +(formal model, sign quotient); Gareth Davidson +[PR 1333](https://github.com/CrocSwap/integer-mult-bounds/pull/1333) +(free scalar normalization); Cinna Davis +[PR 1541](https://github.com/CrocSwap/integer-mult-bounds/pull/1541) +(workspace reasoning); the `Q8` calibration source +[PR 1822](https://github.com/CrocSwap/integer-mult-bounds/pull/1822). + +Overlap refreshes at 2026-10-15 07:54Z and 08:34-08:36Z (620 open PRs, 1153 +discussion records, complete pagination) found no other work on the +noncommuting thirteen-call tuple search or on exact-search tooling for this +line; the only KB2-object records are the predecessor and PR 2415. No +matches is not a novelty certificate. + +Prepared by **Aaron Wang** with help from opencode (substantial AI assistance +in reasoning, implementation, verification and writing; no independent human +review). New work is Apache-2.0; predecessor sources and notices are +unchanged. + +## Open next questions + +1. **Do seven-or-more-distinct-value tuples need new machinery, or does the + `C`-matrix DPLL close them?** Why it matters: it would give a search-level + exclusion of all of KB2 independent of the PR 1989 bridge. First step: + branch on the gap-layer bits `c_{ij}` with the quadratic idempotence + equations `C^2 = C` as watched constraints and the four `C D^{p,q} C = C` + equations as the leaf test. Blocker: the high-degree `Z` polynomials need + propagators; the 78 free bits are not enumerable directly. +2. **Changed-charge variants of the five-SWAP word problem.** Why it matters: + PR 2415's handoff lists changed operation/charge/endpoints as the + remaining premises; asymmetric label prices (e.g. `price(a)=1`, + `price(b)=2`) make longer `a`-heavy words competitive and the crossing + rank no longer prices the minimum. First step: complete weighted minima + for `t = 2` and `t = 3` by BFS with a weighted layer digest. Blocker: the + weighted search needs length 9+ layers at `t = 3`; the current layer-ball + engine is exponential in word length without the frame-family structure. +3. **Reusable tooling gaps.** Why it matters: the tooling is deliberately + small. First step: a bit-sliced evaluator over candidate sets (the + `u_c v_c` masks already exist) would make `m_W >= 6` searches cheap + enough for wider algebras. Blocker: none scientific; it is engineering. diff --git a/research/kb2-alt13-noncommuting-tooling/SOURCES.json b/research/kb2-alt13-noncommuting-tooling/SOURCES.json new file mode 100644 index 0000000000..e1848cdb81 --- /dev/null +++ b/research/kb2-alt13-noncommuting-tooling/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "e8870e5917057d59b730eb14721a778639eca050", + "sha256": "d46eb6d5b3e279428753d770653663fbdf1063e55c255ea073d768f344927ef7" + }, + { + "path": "research/four-swap-full-occupancy/README.md", + "usage": "input", + "git_blob": "9d07ef4e838b30ce6e826ff2f876801b035a7c2c", + "sha256": "82bdfbfb517505ef6783cb82e2718975876276075fe3dba26959df514f984f60" + } + ] +} diff --git a/research/kb2-alt13-noncommuting-tooling/TASK.json b/research/kb2-alt13-noncommuting-tooling/TASK.json new file mode 100644 index 0000000000..51d2b8f62e --- /dev/null +++ b/research/kb2-alt13-noncommuting-tooling/TASK.json @@ -0,0 +1,168 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "priority_revision": 4, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "original_card": { + "id": "bit-new-register-model", + "question": "Can an explicitly larger or nonabelian register model escape the scoped three-register obstruction?", + "starting_points": [ + "research/bit-three-register-lower-bound/README.md", + "certificates/selected-result.json", + "research/bit-gl3-mixed-targets-length10/README.md", + "docs/research/community-efficient1000-review.md" + ], + "methods": [ + "Construct the smallest exact identity in a newly specified legal operation alphabet.", + "Derive a target-specific relaxation bound for that same explicit alphabet." + ], + "acceptance_gate": "Name the changed hypothesis, all counted roles and a uniform identity; finite column tests alone do not certify it.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read Model section 1 of the three-register bound and identify the exact excluded free operations.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "First compare the alphabet, role count and length with the fully replayed #1974 census and #2027 mixed-root tariff. Identify a changed premise and a legal native implementation; then price one smallest completed instance before searching larger words.", + "bottleneck_link": "A small-width completed saving changes the bit primitive; a finite-address identity alone is insufficient.", + "allowed_variations": [ + "Choose a fixed larger register count or a specified nonabelian operation family." + ], + "scope_change_triggers": [ + "Remaining inside the already-excluded three-register abelian model.", + "Repeating the two-register GL3 census or a covered three-register length without changing a hypothesis; a formal group-algebra word without native conversion is a partial result." + ], + "overlap_terms": [ + "three-register", + "nonabelian", + "group algebra" + ] + }, + "scope_status": "changed", + "actual_scope": "Build reusable exact-search tooling (Python stdlib only) for noncommuting word/tuple enumeration over F2[G] group rings and M_r of them (GL_2(F2), Q8) with prefix closure bounds, memoized layer/signature digests, GL-conjugation symmetry reduction and parallel-safe batch splitting; demonstrate it on open problem KB2 (research/fiveswap-alt13-commuting-screen, PR 2317 open question 1): find or exclude the strictly alternating thirteen-call word at five fully occupied coordinate-SWAP roles in the formal F2[GL_2(F2)] rank-one-idempotent register model.", + "scope_change_reason": "Authorized orchestrator tooling mandate: an explicit open request. The local draw (seed 56cf67ad450f0a4b6c78411360a6654f, track complex-mechanisms) proposed complex-new-helper-inventory / p104-side-correction / complex-rank-shape-decoder; the assigned open request supersedes the draw because the KB2 search was recorded as blocked on solver tooling (research/fiveswap-alt13-commuting-screen open question 1 names 'no SAT/SMT tooling on this host' as its blocker), and unblocking it is the deliverable. The mathematical object is unchanged from KB2; the method changes from analytic screening to exact solver tooling plus exhaustive noncommuting tuple search.", + "bottleneck_link": "KB2 is the only remaining potential saving below the direct fifteen-call tariff at five fully occupied coordinate-SWAP roles in the fixed coordinate-CNOT alphabet (four-swap-full-occupancy uniform cut: q >= 2t+3 with equality strictly alternating, sign trace q = t mod 2 leaves only q = 13 for t = 5). Excluding it closes the alphabet at 3t; finding it would give the first saving in this model. The bit side does not bind and no kappa claim is made.", + "budget_minutes": 240, + "stop_rule": "Stop the search when either (a) a thirteen-call word passes the exact formal endpoint check, or (b) the six-distinct-value family is completely excluded with receipts and the remaining seven-or-more-distinct frontier is recorded with exact covered/uncovered counts. Reserve the final session portion for controls, replay, overlap refresh and publication. One bounded pivot maximum.", + "outcome": "completed", + "evidence": "Reusable stdlib tooling exact_search.py with 17 unit controls (tests/test_research_exact_word_search.py) plus verify.py's 10 control groups. Complete exact search of the six-distinct-value KB2 family: 323,963,640 placements (extra-position pattern x class assignment with odd multiplicities), 278,576 distinct canonical signatures, 700,496 exact M_5(F2[G]) product evaluations after a sound diagonal pre-filter, zero survivors; per-m signature digests in verify.py output and README. Positive-hit (planted target) and tiny t=2 completeness cross-checks show the search is neither vacuous nor lossy. Independent search-level audit agreeing with the concurrent analytic exclusion PR 2415 (released to Ross Richardson); d >= 7 distinct-value tuples remain uncovered.", + "author": "Aaron Wang, with help from opencode", + "ai_assistance": "Substantial AI assistance via opencode (agentic coding tool) in reasoning, implementation, verification and writing. Single agent; no independent human or proof-assistant review.", + "method": { + "arithmetic": "Exact F2 arithmetic only (bit-packed group algebra F2[G], matrices over it); no floating point in any acceptance path.", + "classification_lemmas": [ + "Sign equation plus natural-quotient block equations are equivalent to the full M_t(F2[G]) endpoint (F2[S_3] = F2[epsilon]/(epsilon^2) x M_2(F2) decomposition).", + "Any tuple with sum N_i = I_5 uses at least 5 distinct projector values; 5 rank-one idempotents summing to I_5 are automatically a dual frame (V^T U = I).", + "Hence any KB2 solution uses >= 6 distinct values; the 6-value case is exactly one dual frame (odd multiplicities) plus one extra projector of even multiplicity m_W in {2,4,6,8}." + ], + "enumeration": "Gauge-fix the frame to the coordinate frame (GL_5 conjugation is an exact symmetry); enumerate the extra projector W over all 491 non-frame rank-one idempotents of M_5(F2), all placements of W positions and all class assignments with odd multiplicities; group placements by per-class segment-product signature (memoized digest) so each distinct signature x W pair is evaluated once, exactly, in M_5(F2[G]).", + "parameter_ranges": "t = 5 registers; 13 positions; strictly alternating labels abab...a (the a<->b automorphism covers the mirror); paid alphabet = 496 binary rank-one idempotents u v^T (v^T u = 1) in M_5(F2) times labels g in {a,b}; target [s] I_5 with s = aba = bab." + }, + "initial_task": "Reusable exact-search tooling for noncommuting word/tuple enumeration over F2[G] and M_r(F2[G]); demonstration on the KB2 strictly alternating thirteen-call five-SWAP candidate (find or exclude, else exact search frontier with controls).", + "predecessors": [ + { + "pr": 2317, + "head": "139779c86ba8215910117ddb383e4df007b23dcf", + "author": "Aaron Wang / navinor", + "role": "Direct handoff: commuting-subfamily exclusion of the thirteen-call candidate, block equations recorded for the noncommuting search (open question 1 = KB2)." + }, + { + "pr": 1766, + "head": "ff68746efa11b491734362d82ac7ff359aa1b48b", + "author": "Ross Richardson", + "role": "research/four-swap-full-occupancy: uniform cut consequence q >= 2t+3, strictly alternating at equality, sign trace q = t mod 2; open question 2 names the thirteen-call candidate." + }, + { + "pr": 1722, + "head": "246cd6b3a795a346bc6a741661ddcdb2d6359103", + "author": "Ross Richardson", + "role": "Label-saturation theorem used by the rotation step." + }, + { + "pr": 1414, + "head": "9e1640094f649ba6db9742796825a8d6c238989b", + "author": "commdata2338", + "role": "Formal F2[GL_2(F2)] model and sign quotient." + }, + { + "pr": 1333, + "head": "7f25b6d0e1d7e995d4d2840f231d98b1a1a9fec2", + "author": "Gareth Davidson / bitplane", + "role": "Free scalar GL_t(F2) mixing normalization." + } + ], + "overlap": { + "entry": { + "terms": ["five-SWAP", "thirteen-call", "noncommuting", "alternating", "rank-one-idempotent", "exact search", "meet-in-the-middle"], + "fetched_at": "2026-10-15T07:54:12Z", + "coverage": { + "open_prs": {"complete_pagination": true, "records": 612}, + "discussions": {"complete_pagination": true, "records": 1138} + }, + "result": "POSSIBLE_OVERLAP_NOT_A_NOVELTY_CERTIFICATE: 426 raw matches, 20 shown; the only KB2-object records are the predecessor PR 2317 and its own claims/pointers (discussion 1317 comments 18940800/18940998, discussion 1166 comment 18940999) plus unrelated noncommuting S4/Q8/affine packages. No claim on the noncommuting thirteen-call search.", + "distinction": "PR 2317 screens the pairwise-commuting subfamily only and records the block equations as the handoff; this package builds the missing solver tooling and searches the noncommuting tuples, beginning with the complete six-distinct-value family." + }, + "final": { + "fetched_at": "2026-10-15T10:16:25Z / 2026-10-15T10:18:01Z", + "coverage": { + "open_prs": {"complete_pagination": true, "records": 644}, + "discussions": {"complete_pagination": true, "records": 1170} + }, + "terms": ["six-distinct", "signature DP", "exact-search tooling", "KB2", "alt13 noncommuting"], + "matches_total": 3, + "assessed_matches": "All 3 records are this package's own README/TASK and its claim comment; no competing tooling or six-distinct search found. The KB2 object itself is released to PR 2415 (Ross Richardson), which landed mid-session. Not a novelty certificate.", + "upstream_refresh": "Canonical main refetched at submission equals base 0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2 (priority revision 4, unchanged)." + } + }, + "validation": { + "python": "3.12.14", + "platform": "Windows", + "registered_replay": "PASS_REGISTERED_RESEARCH_PACKAGE research/kb2-alt13-noncommuting-tooling outcome=completed", + "commands": [ + "python3.12 -I -B scripts/research_package.py --package research/kb2-alt13-noncommuting-tooling", + "python3.12 -B -m unittest discover -s tests -p 'test_research_*.py'" + ], + "finite_counts": { + "placements_total": 323963640, + "signatures_total": 278576, + "exact_evaluations_total": 700496, + "survivors": 0, + "unit_controls": 17, + "verify_control_groups": 11 + }, + "unrun": [ + "seven-or-more-distinct-value tuple search (recorded frontier)", + "changed-tariff or changed-endpoint variants", + "Lean or independent human proof review", + "physical/compiler/hosting/precision/tape/analytic admission", + "hosted CI" + ] + }, + "chooser_nonce": "56cf67ad450f0a4b6c78411360a6654f", + "scope_key": "kb2-alt13-noncommuting-tooling:six-distinct-value-search:signature-dp", + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1317#discussioncomment-18944685", + "open_questions": [ + { + "question": "Do seven-or-more-distinct-value tuples need new machinery, or does a C-matrix DPLL with the idempotence equations as watched constraints close the remaining KB2 space at search level?", + "why_it_matters": "It would give a search-level exclusion of all of KB2 independent of the PR 1989 bridge, and exercise the tooling on the unfactored tuple space.", + "first_step": "Branch on the gap-layer bits c_ij with C^2 = C as quadratic watched constraints and the four projected block equations as the leaf test; record node counts and pruning receipts.", + "blocked_by": "The high-degree Z polynomials need propagators; the 78 free bits are not enumerable directly." + }, + { + "question": "What are the exact weighted minima for the five-SWAP endpoint under asymmetric label prices (e.g. price(a)=1, price(b)=2)?", + "why_it_matters": "PR 2415's handoff lists changed charges as a remaining premise; asymmetric prices make longer a-heavy words competitive and the crossing rank no longer prices the minimum.", + "first_step": "Complete weighted minima for t = 2 and t = 3 with weighted layer digests; t = 2 is small enough for the current engine.", + "blocked_by": "Weighted search at t = 3 needs length-9 layers; the layer-ball engine is exponential in word length without the frame-family structure." + }, + { + "question": "Can a bit-sliced evaluator over candidate sets make m_W >= 6 and wider algebras cheap?", + "why_it_matters": "The u_c v_c masks already exist; bit-slicing would give roughly two orders of magnitude on candidate sweeps.", + "first_step": "Rewrite sig_eval's inner loop over 491-bit candidate masks; cross-check against the scalar evaluator on random tuples.", + "blocked_by": "Engineering only; no scientific blocker." + } + ] +} diff --git a/research/kb2-alt13-noncommuting-tooling/VERIFY.json b/research/kb2-alt13-noncommuting-tooling/VERIFY.json new file mode 100644 index 0000000000..0e1c2c4a2b --- /dev/null +++ b/research/kb2-alt13-noncommuting-tooling/VERIFY.json @@ -0,0 +1,33 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/four-swap-full-occupancy/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 600, + "checks": "Model controls (direct 3/9/15-call words, mutation), sign x natural quotient isomorphism and its equivalence to the full endpoint and the C-matrix invariant, GL_5 conjugation invariance, exhaustive F2^3 classification controls, fast-evaluator equivalence with mutation, Q8 layer-ball calibration, shard receipts, prefix bound, planted-hit control, tiny t=2 completeness cross-check, and the complete six-distinct-value KB2 search (receipts per m_W with signature digests)." + }, + { + "argv": [ + "{python}", + "-B", + "-m", + "unittest", + "tests.test_research_exact_word_search", + "-v" + ], + "timeout_seconds": 300, + "checks": "17 failure-sensitive unit controls for the reusable tooling: group relations, rank-one idempotent alphabets, word model, quotient equivalence, C-invariant equivalence, classification lemma boundary, brute-force t=2 baseline, fast-eval equivalence with mutation, GL conjugation, Q8 layer calibration, shard stability." + } + ] +} diff --git a/research/kb2-alt13-noncommuting-tooling/exact_search.py b/research/kb2-alt13-noncommuting-tooling/exact_search.py new file mode 100644 index 0000000000..16387759bb --- /dev/null +++ b/research/kb2-alt13-noncommuting-tooling/exact_search.py @@ -0,0 +1,767 @@ +"""Reusable exact word/tuple search over group rings F2[G] and matrix rings +M_r(F2[G]) for the formal rank-one-idempotent register model. + +Model (the coordinate-CNOT line of PR1333/1414/1491/1541/1722 and the S_n +line of PR1989): G finite, R = F2[G]; a paid call is D_N(g) = I + ([g]+1) N +with g a paid label and N = u v^T a binary rank-one idempotent (v^T u = 1) +in M_r(F2); free scalar GL_r(F2) mixing at zero cost; acceptance is equality +of all formal group-algebra coefficients in M_r(F2[G]). + +Contents: + * Group / GroupAlgebra: F2[G] from a multiplication table (gl2f2, q8). + * M_r(F2) and M_r(F2[G]) exact arithmetic; rank-one idempotent alphabets. + * Quotient projections: sign quotient (F2[epsilon]/(epsilon^2)) and the + natural 2-dimensional quotient for GL_2(F2); the pair is an algebra + isomorphism, so sign + natural equations are equivalent to the full + endpoint (checked, not assumed). + * The C-matrix invariant C_ij = v_i^T u_j: C^2 = C plus four projected + block equations is equivalent to the full endpoint at full rank. + * Search engine: layer-ball digests, meet-in-the-middle joins, prefix + closure bounds, GL_r conjugation reduction, SHA256-receipted parallel-safe + batch splitting, and a signature-DP enumeration for frame-plus-extra + tuples (the six-distinct-value KB2 family). + +Python stdlib only. Exact F2 arithmetic throughout. Apache-2.0. +Aaron Wang, with help from opencode. +""" + +import hashlib + +# -------------------------------------------------------------------------- +# Groups from multiplication tables. +# -------------------------------------------------------------------------- + + +class Group: + def __init__(self, name, table, identity, names): + self.name = name + self.n = len(table) + self.table = tuple(tuple(row) for row in table) + self.identity = identity + self.names = tuple(names) + + def mul(self, i, j): + return self.table[i][j] + + def parity(self, g): + """Image of g under G -> G/[G,G] = C_2 (0 = even).""" + return self._parity[g] + + def _set_parity(self, parities): + self._parity = tuple(parities) + + +def gl2f2(): + """G = GL_2(F2) as packed 2x2 matrices (bits r0c0 r0c1 r1c0 r1c1).""" + def mmul(x, y): + a = [(x >> 3) & 1, (x >> 2) & 1, (x >> 1) & 1, x & 1] + b = [(y >> 3) & 1, (y >> 2) & 1, (y >> 1) & 1, y & 1] + c00 = (a[0] & b[0]) ^ (a[1] & b[2]) + c01 = (a[0] & b[1]) ^ (a[1] & b[3]) + c10 = (a[2] & b[0]) ^ (a[3] & b[2]) + c11 = (a[2] & b[1]) ^ (a[3] & b[3]) + return (c00 << 3) | (c01 << 2) | (c10 << 1) | c11 + + mats = [m for m in range(16) + if (((m >> 3) & 1) * (m & 1)) ^ (((m >> 2) & 1) * ((m >> 1) & 1))] + mats.sort() + idx = {m: i for i, m in enumerate(mats)} + mul = [[idx[mmul(mats[i], mats[j])] for j in range(6)] for i in range(6)] + names = [] + for m in mats: + names.append({0b1001: "e", 0b1101: "a", 0b1011: "b", + 0b0110: "s"}.get(m, "g%d" % m)) + g = Group("GL_2(F2)", mul, idx[0b1001], names) + g.A = idx[0b1101] + g.B = idx[0b1011] + g.S = idx[0b0110] + # parity = permutation parity of the action on the three nonzero vectors + vecs = (0b01, 0b10, 0b11) + + def act(m, v): + r0 = ((m >> 3) & 1) * ((v >> 1) & 1) ^ ((m >> 2) & 1) * (v & 1) + r1 = ((m >> 1) & 1) * ((v >> 1) & 1) ^ (m & 1) * (v & 1) + return (r0 << 1) | r1 + + par = [] + for m in mats: + perm = [vecs.index(act(m, v)) for v in vecs] + inv = sum(1 for i in range(3) for j in range(i + 1, 3) + if perm[i] > perm[j]) + par.append(inv & 1) + g._set_parity(par) + return g + + +def q8(): + """Q8 = {+-1, +-i, +-j, +-k}; element (sign, axis): axis 0 = 1, 1 = i, + 2 = j, 3 = k; sign 0 = +, 1 = -.""" + axis_mul = [ + [0, 1, 2, 3], + [1, 0, 3, 2], + [2, 3, 0, 1], + [3, 2, 1, 0], + ] + sign_flip = [ + [0, 0, 0, 0], + [0, 1, 0, 1], + [0, 1, 1, 0], + [0, 0, 1, 1], + ] + + def enc(s, ax): + return (s << 2) | ax + + mul = [[0] * 8 for _ in range(8)] + for el in range(8): + for fr in range(8): + s1, ax1 = el >> 2, el & 3 + s2, ax2 = fr >> 2, fr & 3 + mul[el][fr] = enc(s1 ^ s2 ^ sign_flip[ax1][ax2], + axis_mul[ax1][ax2]) + names = ["1", "i", "j", "k", "-1", "-i", "-j", "-k"] + g = Group("Q8", mul, enc(0, 0), names) + g.X = enc(0, 1) # i + g.Y = enc(0, 2) # j + g.Z = enc(1, 0) # -1 = x^2 = y^2 = xyxy + g._set_parity([0] * 8) # Q8 is not used with a sign quotient here + return g + + +class GroupAlgebra: + """F2[G]: elements are bit masks over Group elements.""" + + def __init__(self, group): + self.group = group + n = group.n + size = 1 << n + mul = [bytearray(size) for _ in range(size)] + for x in range(size): + xs = [i for i in range(n) if (x >> i) & 1] + if not xs: + continue + row = mul[x] + for y in range(size): + out = 0 + for i in xs: + for j in range(n): + if (y >> j) & 1: + out ^= 1 << group.mul(i, j) + row[y] = out + self._mul = tuple(bytes(row) for row in mul) + self.one = 1 << group.identity + + def add(self, x, y): + return x ^ y + + def mul(self, x, y): + if x == 0 or y == 0: + return 0 + return self._mul[x][y] + + def basis(self, i): + return 1 << i + + +# -------------------------------------------------------------------------- +# M_r(F2) and rank-one idempotents. +# -------------------------------------------------------------------------- + + +def mat_add(x, y): + return tuple(a ^ b for a, b in zip(x, y)) + + +def mat_mul(n, x, y): + out = [0] * n + for i in range(n): + xi = x[i] + acc = 0 + while xi: + low = xi & -xi + k = low.bit_length() - 1 + acc ^= y[k] + xi ^= low + out[i] = acc + return tuple(out) + + +def proj_rows(t, u, v): + return tuple(v if (u >> i) & 1 else 0 for i in range(t)) + + +def dot(u, v): + return bin(u & v).count("1") & 1 + + +def rank_f2(n, x): + rows = list(x) + rank = 0 + for col in range(n): + piv = None + for r in range(rank, n): + if (rows[r] >> col) & 1: + piv = r + break + if piv is None: + continue + rows[rank], rows[piv] = rows[piv], rows[rank] + for r in range(n): + if r != rank and (rows[r] >> col) & 1: + rows[r] ^= rows[rank] + rank += 1 + return rank + + +def rank_one_idempotents(t): + out = [] + for u in range(1, 1 << t): + for v in range(1, 1 << t): + if dot(u, v): + out.append((u, v)) + return out + + +def coord_proj(t, c): + return (1 << c, 1 << c) + + +def proj_sum(t, rows_list): + acc = [0] * t + for rows in rows_list: + for i in range(t): + acc[i] ^= rows[i] + return tuple(acc) + + +def eye_f2(t): + return tuple(1 << i for i in range(t)) + + +# -------------------------------------------------------------------------- +# M_r(F2[G]) and word products. +# -------------------------------------------------------------------------- + + +def ring_eye(ga, r): + one = ga.one + return tuple(one if i == j else 0 + for i in range(r) for j in range(r)) + + +def ring_add(x, y): + return tuple(a ^ b for a, b in zip(x, y)) + + +def ring_mul(ga, x, y, r): + out = [0] * (r * r) + for i in range(r): + for k in range(r): + aik = x[i * r + k] + if aik: + for j in range(r): + bkj = y[k * r + j] + if bkj: + out[i * r + j] ^= ga.mul(aik, bkj) + return tuple(out) + + +def call_matrix(ga, group, r, g, n_rows): + """D_N(g) = I + ([g]+1) N in M_r(F2[G]) with N = n_rows (M_r(F2)).""" + one = ga.one + xb = ga.basis(g) ^ one + out = [] + for i in range(r): + for j in range(r): + v = one if i == j else 0 + if (n_rows[i] >> j) & 1: + v ^= xb + out.append(v) + return tuple(out) + + +def word_product(ga, group, r, labels, projs): + """Product D_0 D_1 ... with labels[0] leftmost (any consistent direction + defines the same problem on the palindromic alternating word).""" + acc = ring_eye(ga, r) + for g, (u, v) in zip(labels, projs): + fac = call_matrix(ga, group, r, g, proj_rows(r, u, v)) + acc = ring_mul(ga, acc, fac, r) + return acc + + +def ring_target(ga, r, s): + sb = ga.basis(s) + return tuple(sb if i == j else 0 + for i in range(r) for j in range(r)) + + +def endpoint_check(ga, group, r, labels, projs): + return word_product(ga, group, r, labels, projs) == \ + ring_target(ga, r, group.S if hasattr(group, "S") else group.Z) + + +def expanded_word_product(ga, group, r, labels, projs): + """Independent subset expansion: sum_S (prod_{i in S} ([g_i]+1)) N(S). + Used to cross-check the iterative product engine.""" + n = len(labels) + xs = [ga.basis(g) ^ ga.one for g in labels] + xprod = [0] * (1 << n) + xprod[0] = ga.one + for mask in range(1, 1 << n): + low = mask & -mask + bit = low.bit_length() - 1 + # order: positions increase left to right + xprod[mask] = ga.mul(xs[bit], xprod[mask ^ low]) + out = [0] * (r * r) + for mask in range(1 << n): + picks = [i for i in range(n) if (mask >> i) & 1] + if not picks: + one = ga.one + for i in range(r): + out[i * r + i] ^= one + continue + # N(S) = u_first (prod interior dots) v_last^T (F2 scalars are bits) + u_first, _ = projs[picks[0]] + _, v_last = projs[picks[-1]] + alive = 1 + for p in range(len(picks) - 1): + _, vp = projs[picks[p]] + uq, _ = projs[picks[p + 1]] + alive &= dot(vp, uq) + if not alive: + break + if not alive: + continue + scalar = xprod[mask] + for i in range(r): + if (u_first >> i) & 1: + for j in range(r): + if (v_last >> j) & 1: + out[i * r + j] ^= scalar + return tuple(out) + + +# -------------------------------------------------------------------------- +# Quotient projections. +# -------------------------------------------------------------------------- + + +def sign_quotient_word(group, r, labels, projs): + """Product in M_r(F2[epsilon]/(epsilon^2)) = (M0, M1).""" + eye = eye_f2(r) + acc = [0] * r + for g, (u, v) in zip(labels, projs): + if group.parity(g): + rows = proj_rows(r, u, v) + for i in range(r): + acc[i] ^= rows[i] + return eye, tuple(acc) + + +def sign_check(group, r, labels, projs): + m0, m1 = sign_quotient_word(group, r, labels, projs) + return m1 == eye_f2(r) + + +def natural_check(group, r, labels, projs): + """Natural quotient [g] -> g in M_2(F2): product in M_{2r}(F2).""" + if group.name != "GL_2(F2)": + raise ValueError("natural_check needs the GL_2(F2) 2-dim rep") + n = 2 * r + acc = tuple(1 << i for i in range(n)) + for g, (u, v) in zip(labels, projs): + m = gl2_matrix(group, g) + n_rows = proj_rows(r, u, v) + fac = [1 << i for i in range(n)] + for i in range(r): + for j in range(r): + if (n_rows[i] >> j) & 1: + for p in range(2): + for q in range(2): + if (m[p] >> q) & 1: + fac[2 * i + p] ^= 1 << (2 * j + q) + acc = mat_mul(n, acc, tuple(fac)) + tgt = [0] * n + sm = gl2_matrix(group, group.S) + for i in range(r): + for p in range(2): + for q in range(2): + if (sm[p] >> q) & 1: + tgt[2 * i + p] ^= 1 << (2 * i + q) + return acc == tuple(tgt) + + +def gl2_matrix(group, g): + """2x2 matrix (rows as ints, bit j = column j) of a GL_2(F2) element.""" + mats = [m for m in range(16) + if (((m >> 3) & 1) * (m & 1)) ^ (((m >> 2) & 1) * ((m >> 1) & 1))] + mats.sort() + m = mats[g] + return (((m >> 2) & 1) << 1) | ((m >> 3) & 1), \ + ((m & 1) << 1) | ((m >> 1) & 1) + + +# -------------------------------------------------------------------------- +# C-matrix invariant: C_ij = v_i^T u_j. +# -------------------------------------------------------------------------- + + +def c_matrix(projs): + n = len(projs) + rows = [] + for i in range(n): + _, vi = projs[i] + row = 0 + for j in range(n): + uj, _ = projs[j] + if dot(vi, uj): + row |= 1 << j + rows.append(row) + return tuple(rows) + + +def c_conditions_ok(r, labels, projs): + """C^2 = C, rank C = r, and the projected block equations: for every + ordered label pair (p, q), sum_{i<=j, labels p..q} Z_ij u_i v_j^T = I + projected is (C D^{p,q} C) = C.""" + n = len(projs) + c = c_matrix(projs) + if rank_f2(n, c) != r: + return False + if mat_mul(n, c, c) != c: + return False + # M_ij = c_ij for j > i with j - i odd; Z = M + M^2 + ... + M^n + m = [0] * n + for i in range(n): + for j in range(i + 1, n): + if ((j - i) & 1) and ((c[i] >> j) & 1): + m[i] |= 1 << j + z = [0] * n + power = tuple(m) + for _ in range(n): + z = [a ^ b for a, b in zip(z, power)] + power = mat_mul(n, power, m) + distinct = sorted(set(labels)) + for p in distinct: + for q in distinct: + d = [0] * n + for i in range(n): + if labels[i] != p: + continue + for j in range(i, n): + if labels[j] != q: + continue + if (z[i] >> j) & 1: + d[i] |= 1 << j + if mat_mul(n, c, mat_mul(n, tuple(d), c)) != c: + return False + return True + + +# -------------------------------------------------------------------------- +# Symmetry: GL_r conjugation. +# -------------------------------------------------------------------------- + + +def random_gl(t, rng): + while True: + rows = [rng.randrange(1 << t) for _ in range(t)] + if rank_f2(t, tuple(rows)) != t: + continue + inv = [1 << i for i in range(t)] + work = list(rows) + for col in range(t): + piv = next(r for r in range(col, t) if (work[r] >> col) & 1) + work[col], work[piv] = work[piv], work[col] + inv[col], inv[piv] = inv[piv], inv[col] + for r in range(t): + if r != col and (work[r] >> col) & 1: + work[r] ^= work[col] + inv[r] ^= inv[col] + return tuple(rows), tuple(inv) + + +def proj_conj(t, u, v, p, pinv): + u2 = 0 + for i in range(t): + if dot(p[i], u): + u2 |= 1 << i + v2 = 0 + for j in range(t): + if (v >> j) & 1: + v2 ^= pinv[j] + return (u2, v2) + + +def random_tuple(group, t, length, rng): + alphabet = rank_one_idempotents(t) + labels = [group.A if rng.randrange(2) == 0 else group.B + for _ in range(length)] + projs = [alphabet[rng.randrange(len(alphabet))] + for _ in range(length)] + return labels, projs + + +# -------------------------------------------------------------------------- +# Search engine: layer balls, MITM, prefix bounds, shards. +# -------------------------------------------------------------------------- + + +def layer_ball_sizes(ga, gens, depth): + """BFS distance-layer sizes in the monoid generated by `gens`: the number + of new products reachable at each exact length (memoized ball digest).""" + r = int(round(len(gens[0]) ** 0.5)) + eye = ring_eye(ga, r) + seen = {eye} + frontier = {eye} + out = [1] + for _ in range(depth): + nxt = set() + for st in frontier: + for gen in gens: + nxt.add(ring_mul(ga, gen, st, r)) + new = nxt - seen + seen |= nxt + frontier = new + out.append(len(new)) + return out + + +def shard_split(items, n): + """Deterministic contiguous shards with SHA256 receipts; each shard is an + independent batch (safe for parallel workers).""" + items = list(items) + k, extra = divmod(len(items), n) + shards = [] + start = 0 + for i in range(n): + stop = start + k + (1 if i < extra else 0) + part = items[start:stop] + shards.append({ + "index": i, + "items": part, + "sha256": hashlib.sha256( + ",".join(map(str, part)).encode()).hexdigest(), + }) + start = stop + return shards + + +def sign_prefix_bound(t, partial_rows, placed, total): + """Prefix closure bound: the remaining total - placed rank-one idempotents + must be able to sum to I - partial; hence rank(I - partial) <= left.""" + left = total - placed + if left < 0: + return False + res = list(eye_f2(t)) + for row in partial_rows: + for i in range(t): + res[i] ^= row[i] + return rank_f2(t, tuple(res)) <= left + + +# -------------------------------------------------------------------------- +# Frame-plus-extra (six-distinct-value) enumeration: signature DP. +# -------------------------------------------------------------------------- + + +def alt_labels(group, n): + return [group.A if i % 2 == 0 else group.B for i in range(n)] + + +def sig_eval(ga, group, t, wlabels, h, u, v): + """Word product for a frame-plus-extra tuple: h[c][s] is the class-c + segment-s label product (single group element), extra projector uv^T at + the m = len(wlabels) extra positions. Returns the M_t(F2[G]) product. + + F2[G] is noncommutative, so each extra scalar x = [g]+1 stays at its own + position in the chain: Term(T)_{ab} = f_lead[a] x_j1 u_a S v_b + f_trail[b] with S = sigma_1 x_j2 sigma_2 ... x_jk.""" + m = len(wlabels) + xs = [ga.basis(g) ^ ga.one for g in wlabels] + out = [0] * (t * t) + for mask in range(1 << m): + picks = [j for j in range(m) if (mask >> j) & 1] + bounds = [] + prev = 0 + for j in picks: + bounds.append((prev, j)) + prev = j + 1 + bounds.append((prev, m)) + blocks = [] + for lo, hi in bounds: + diag = [] + for c in range(t): + acc = group.identity + for s in range(lo, hi + 1): + acc = group.mul(acc, h[c][s]) + diag.append(acc) + blocks.append(diag) + if not picks: + diag = blocks[0] + for c in range(t): + out[c * t + c] ^= ga.basis(diag[c]) + continue + lead = blocks[0] + trail = blocks[-1] + # chain scalar S = sigma_1 x_j2 sigma_2 ... x_jk (k = len(picks)) + s_prod = ga.one + ok = True + for bi in range(1, len(blocks) - 1): + diag = blocks[bi] + sigma = 0 + for c in range(t): + if ((u >> c) & 1) and ((v >> c) & 1): + sigma ^= ga.basis(diag[c]) + if bi > 1: + s_prod = ga.mul(s_prod, xs[picks[bi - 1]]) + s_prod = ga.mul(s_prod, sigma) + if s_prod == 0: + ok = False + break + if not ok: + continue + if len(picks) > 1: + s_prod = ga.mul(s_prod, xs[picks[-1]]) + x1 = xs[picks[0]] + for a in range(t): + if not ((u >> a) & 1): + continue + pref = ga.mul(ga.basis(lead[a]), x1) + if pref == 0: + continue + for b in range(t): + if not ((v >> b) & 1): + continue + mid = ga.mul(pref, s_prod) + if mid == 0: + continue + val = ga.mul(mid, ga.basis(trail[b])) + out[a * t + b] ^= val + return tuple(out) + + +def six_distinct_search(ga, group, t, labels, m_values, w_all, probe=None, + target=None): + """Exhaustive search of the frame-plus-one-extra family: t frame classes + (odd multiplicities) plus one extra projector W (even multiplicity m) at + any word positions. Returns per-m receipts with survivors. + + One signature DP runs over all extra-position patterns at once: a state is + the S_t-canonical tuple of (class segment products, parity) rows plus the + extra-position label word. Canonicalization is complete because every W + candidate is tested and GL_t conjugation preserves the endpoint.""" + n = len(labels) + if target is None: + target = ring_target(ga, t, group.S) + receipts = {} + for m in m_values: + init_row = (tuple(group.identity for _ in range(m + 1)), 0) + states = {(tuple(sorted([init_row] * t)), ()): 1} + for i in range(n): + nxt = {} + for (rows, wl), cnt in states.items(): + if len(wl) < m: + key = (rows, wl + (labels[i],)) + nxt[key] = nxt.get(key, 0) + cnt + seg = len(wl) + for ci in range(t): + row, par = rows[ci] + r2 = list(row) + r2[seg] = group.mul(r2[seg], labels[i]) + unit = (tuple(r2), par ^ 1) + merged = tuple(sorted(rows[:ci] + (unit,) + rows[ci + 1:])) + key = (merged, wl) + nxt[key] = nxt.get(key, 0) + cnt + states = nxt + sigs = {} + assignments = 0 + peak = len(states) + for (rows, wl), cnt in states.items(): + if len(wl) != m: + continue + if any(par == 0 for _, par in rows): + continue + flat = tuple(row[s] for row, _ in rows for s in range(m + 1)) + key = (m, wl, flat) + sigs[key] = sigs.get(key, 0) + cnt + assignments += cnt + survivors = [] + evals = 0 + full = (1 << len(w_all)) - 1 + uvmask = [0] * t + for idx, (u, v) in enumerate(w_all): + for c in range(t): + if ((u >> c) & 1) and ((v >> c) & 1): + uvmask[c] |= 1 << idx + for key, cnt in sigs.items(): + m_, wlabels, flat = key + h = [[flat[c * (m_ + 1) + s] for s in range(m_ + 1)] + for c in range(t)] + # sound diagonal pre-filter: the empty-subset term contributes + # prod_s h[c][s] to entry (c,c) and every other term carries the + # factor u_c v_c, so a class whose segment product differs from + # the target diagonal forces u_c v_c = 1. + need = full + for c in range(t): + prod = group.identity + for s in range(m_ + 1): + prod = group.mul(prod, h[c][s]) + if ga.basis(prod) != target[c * t + c]: + need &= uvmask[c] + if need == 0: + break + wm = need + while wm: + low = wm & -wm + idx = low.bit_length() - 1 + wm ^= low + u, v = w_all[idx] + evals += 1 + got = sig_eval(ga, group, t, wlabels, h, u, v) + if got == target: + survivors.append((key, u, v, cnt)) + digest = hashlib.sha256() + for key in sorted(sigs): + digest.update(repr(key).encode()) + receipts["m%d" % m] = { + "w_subsets": None, + "assignments": assignments, + "signatures": len(sigs), + "w_candidates": len(w_all), + "evaluations": evals, + "survivors": len(survivors), + "signature_sha256": digest.hexdigest(), + "peak_dp_states": peak, + "witnesses": survivors[:5], + "all_witnesses": survivors, + } + if probe: + probe(receipts["m%d" % m]) + return receipts + + +# -------------------------------------------------------------------------- +# Self-test (see tests/test_research_exact_word_search.py for the full suite). +# -------------------------------------------------------------------------- + + +def selftest(): + g = gl2f2() + ga = GroupAlgebra(g) + assert g.mul(g.A, g.A) == g.identity + assert g.mul(g.mul(g.A, g.B), g.A) == g.S + assert len(rank_one_idempotents(5)) == 496 + t = 5 + labels = alt_labels(g, 15) + projs = [coord_proj(t, i // 3) for i in range(15)] + assert word_product(ga, g, t, labels, projs) == ring_target(ga, t, g.S) + projs2 = list(projs) + projs2[0] = coord_proj(t, 1) + assert word_product(ga, g, t, labels, projs2) != ring_target(ga, t, g.S) + return "SELFTEST_OK" + + +if __name__ == "__main__": + print(selftest()) diff --git a/research/kb2-alt13-noncommuting-tooling/verify.py b/research/kb2-alt13-noncommuting-tooling/verify.py new file mode 100644 index 0000000000..d6e9a13461 --- /dev/null +++ b/research/kb2-alt13-noncommuting-tooling/verify.py @@ -0,0 +1,305 @@ +#!/usr/bin/env python3 +"""KB2 demonstration of the reusable exact-search tooling. + +Object (open question 1 of research/fiveswap-alt13-commuting-screen, PR 2317): +does the strictly alternating thirteen-call word for five fully occupied +coordinate-SWAP targets exist in the formal F2[GL_2(F2)] rank-one-idempotent +register model with noncommuting scalar projectors? + +Scope of this file: an independent search-level audit of the concurrent PR 2415 +exclusion (the analytic minimum 3t = 15), on the complete six-distinct-value +family, plus validated controls for the tooling. No kappa claim. + +Family (exact classification, machine-checked below): + * sign equation sum N_i = I_5 forces >= 5 distinct projector values; + * t = 5 rank-one idempotents summing to I_5 are automatically a dual frame + (V^T U is an invertible idempotent), so <= 5 distinct values are the + pairwise-commuting family already excluded by the predecessor; + * at exactly 6 distinct values: 5 odd-multiplicity values form a dual frame + (GL_5-conjugate to the coordinate frame) and the sixth value W has even + multiplicity m_W in {2,4,6,8}. This family is exhaustively searched here + by a signature DP over placements and an exact M_5(F2[G]) evaluation of + every (signature, W) pair. Seven or more distinct values are NOT covered. + +Aaron Wang, with help from opencode. Apache-2.0. Stdlib only. +""" + +import hashlib +import importlib.util +import itertools +import pathlib +import random +import sys +import time + +HERE = pathlib.Path(__file__).resolve().parent +sys.stdout.reconfigure(encoding="utf-8") + + +def load(): + spec = importlib.util.spec_from_file_location("exact_search", + HERE / "exact_search.py") + mod = importlib.util.module_from_spec(spec) + spec.loader.exec_module(mod) + return mod + + +ES = load() + + +def marker(tag): + print(" [%s] ok" % tag) + + +def main(): + t0 = time.time() + g = ES.gl2f2() + ga = ES.GroupAlgebra(g) + q8 = ES.q8() + ga8 = ES.GroupAlgebra(q8) + + # ------------------------------------------------------------------ + # 1. Model controls (positive and negative). + # ------------------------------------------------------------------ + for t in (1, 3, 5): + labels = [g.A, g.B, g.A] * t + projs = [ES.coord_proj(t, i // 3) for i in range(3 * t)] + assert ES.word_product(ga, g, t, labels, projs) == \ + ES.ring_target(ga, t, g.S), t + labels15 = [g.A, g.B, g.A] * 5 + projs15 = [ES.coord_proj(5, i // 3) for i in range(15)] + bad = list(projs15) + bad[0] = ES.coord_proj(5, 1) + assert ES.word_product(ga, g, 5, labels15, bad) != ES.ring_target(ga, 5, g.S) + marker("model_direct_and_mutated") + + # quotient isomorphism F2[S_3] = F2[eps]/(eps^2) x M_2(F2) + imgs = [] + for el in range(g.n): + m0, m1 = ES.eye_f2(1), tuple([g.parity(el)]) + nat = ES.gl2_matrix(g, el) + imgs.append((g.parity(el), nat)) + for x in range(g.n): + for y in range(g.n): + px, nx = imgs[x] + py, ny = imgs[y] + pz, nz = imgs[g.mul(x, y)] + assert pz == px ^ py + assert nz == ES.mat_mul(2, nx, ny) + rank_rows = [] + for el in range(g.n): + p, nat = imgs[el] + # coordinates: constant 1, eps coefficient, then the four M_2 entries + rank_rows.append((1 << 5) | (p << 4) | (nat[0] << 2) | nat[1]) + assert ES.rank_f2(6, tuple(rank_rows)) == 6 + marker("quotient_isomorphism_sign_x_natural") + + # sign + natural equations equivalent to the full endpoint (random) + rng = random.Random(20261015) + for _ in range(300): + rl, rp = ES.random_tuple(g, 3, 6, rng) + full = ES.endpoint_check(ga, g, 3, rl, rp) + quot = ES.sign_check(g, 3, rl, rp) and ES.natural_check(g, 3, rl, rp) + assert full == quot + assert full == ES.c_conditions_ok(3, rl, rp) + marker("quotient_and_c_invariant_equivalence") + + # GL conjugation invariance + p, pinv = ES.random_gl(5, rng) + conj = [ES.proj_conj(5, u, v, p, pinv) for u, v in projs15] + assert ES.word_product(ga, g, 5, labels15, conj) == ES.ring_target(ga, 5, g.S) + marker("gl_conjugation_invariance") + + # ------------------------------------------------------------------ + # 2. Classification lemmas (exhaustive over F2^3). + # ------------------------------------------------------------------ + projs3 = ES.rank_one_idempotents(3) + eye3 = ES.eye_f2(3) + frames = 0 + for comb in itertools.combinations(range(len(projs3)), 3): + rows = [ES.proj_rows(3, projs3[i][0], projs3[i][1]) for i in comb] + if ES.proj_sum(3, rows) != eye3: + continue + frames += 1 + for i, j in itertools.combinations(comb, 2): + assert ES.dot(projs3[i][1], projs3[j][0]) == 0 + assert ES.dot(projs3[j][1], projs3[i][0]) == 0 + assert frames > 0 + noncomm = 0 + for comb in itertools.combinations(range(len(projs3)), 5): + rows = [ES.proj_rows(3, projs3[i][0], projs3[i][1]) for i in comb] + if ES.proj_sum(3, rows) != eye3: + continue + for i, j in itertools.combinations(comb, 2): + if ES.dot(projs3[i][1], projs3[j][0]) or \ + ES.dot(projs3[j][1], projs3[i][0]): + noncomm += 1 + break + assert noncomm > 0 + for comb in itertools.combinations(range(len(projs3)), 4): + rows = [ES.proj_rows(3, projs3[i][0], projs3[i][1]) for i in comb] + assert ES.proj_sum(3, rows) != eye3 + marker("classification_lemmas_f2_3 frames=%d noncommuting5=%d" + % (frames, noncomm)) + + # ------------------------------------------------------------------ + # 3. Search-engine controls: fast eval vs generic, positive hit, + # tiny brute-force completeness cross-check, layer balls, shards. + # ------------------------------------------------------------------ + alphabet5 = ES.rank_one_idempotents(5) + for _ in range(8): + rl, rp = ES.random_tuple(g, 5, 13, rng) + assert ES.word_product(ga, g, 5, rl, rp) == \ + ES.expanded_word_product(ga, g, 5, rl, rp) + labels13 = ES.alt_labels(g, 13) + for _ in range(10): + m = rng.randrange(1, 5) + wpos = sorted(rng.sample(range(13), m)) + wu, wv = alphabet5[rng.randrange(len(alphabet5))] + assign = [rng.randrange(5) for _ in range(13)] + h = [[g.identity] * (m + 1) for _ in range(5)] + projs = [] + seg = 0 + for i in range(13): + if i in wpos: + projs.append((wu, wv)) + seg += 1 + else: + projs.append(ES.coord_proj(5, assign[i])) + h[assign[i]][seg] = g.mul(h[assign[i]][seg], labels13[i]) + slow = ES.word_product(ga, g, 5, labels13, projs) + fast = ES.sig_eval(ga, g, 5, [labels13[i] for i in wpos], h, wu, wv) + assert slow == fast + h[0][0] = g.mul(h[0][0], g.A) + assert ES.sig_eval(ga, g, 5, [labels13[i] for i in wpos], h, wu, wv) != slow + marker("fast_eval_equivalence_and_mutation") + + gens8 = [ES.call_matrix(ga8, q8, 2, lbl, ES.proj_rows(2, u, v)) + for lbl in (q8.X, q8.Y) + for u, v in ES.rank_one_idempotents(2)] + layers = ES.layer_ball_sizes(ga8, gens8, 3) + assert layers == [1, 12, 110, 936], layers + marker("q8_layer_calibration layers=%s" % layers) + + shards = ES.shard_split(range(1000), 7) + flat = [x for sh in shards for x in sh["items"]] + assert sorted(flat) == list(range(1000)) + for sh in shards: + assert sh["sha256"] == hashlib.sha256( + ",".join(map(str, sh["items"])).encode()).hexdigest() + marker("parallel_safe_shards") + + # prefix closure bound + rows = [ES.proj_rows(5, u, v) for u, v in projs15[:4]] + assert ES.sign_prefix_bound(5, rows, 4, 15) + assert not ES.sign_prefix_bound(5, rows, 14, 15) + marker("prefix_closure_bound") + + # positive hit: a planted frame-plus-extra tuple must be found + frame5 = set(ES.coord_proj(5, c) for c in range(5)) + w_all = [p for p in alphabet5 if p not in frame5] + plant_w = w_all[3] + plant_wpos = [5, 11] + want = [3, 3, 3, 1, 1] # odd multiplicities over frame positions + plant_assign = [0] * 13 + seen = [0] * 5 + for i in range(13): + if i in plant_wpos: + continue + c = next(c for c in range(5) if seen[c] < want[c]) + seen[c] += 1 + plant_assign[i] = c + assert seen == want + hp = [[g.identity] * 3 for _ in range(5)] + projs = [] + seg = 0 + for i in range(13): + if i in plant_wpos: + projs.append(plant_w) + seg += 1 + else: + projs.append(ES.coord_proj(5, plant_assign[i])) + hp[plant_assign[i]][seg] = g.mul(hp[plant_assign[i]][seg], + labels13[i]) + planted = ES.word_product(ga, g, 5, labels13, projs) + assert planted != ES.ring_target(ga, 5, g.S) + rec = ES.six_distinct_search(ga, g, 5, labels13, (2,), w_all, + target=planted) + hits = rec["m2"]["all_witnesses"] + assert len(hits) >= 1, hits + assert any(u == plant_w[0] and v == plant_w[1] for _, u, v, _ in hits) + marker("positive_hit_control survivors=%d (planted target)" % len(hits)) + + # tiny end-to-end completeness check (t = 2, n = 6): the signature search + # must return exactly the direct enumeration of the same family + t2 = 2 + alpha2 = ES.rank_one_idempotents(t2) + labels6 = ES.alt_labels(g, 6) + frame2 = set(ES.coord_proj(t2, c) for c in range(t2)) + w_all2 = [p for p in alpha2 if p not in frame2] + direct = {} + for m2 in (2, 4): + for wpos in itertools.combinations(range(6), m2): + for w in w_all2: + for cls in itertools.product(range(t2), repeat=6 - m2): + if any(cls.count(c) % 2 == 0 for c in range(t2)): + continue + projs = [] + ci = 0 + for i in range(6): + if i in wpos: + projs.append(w) + else: + projs.append(ES.coord_proj(t2, cls[ci])) + ci += 1 + direct[((m2, w), tuple(projs))] = \ + ES.word_product(ga, g, t2, labels6, projs) + # target = a planted family tuple so the comparison is non-vacuous + (m2p, wp), projsp = next(iter(direct)) + tiny_target = direct[((m2p, wp), tuple(projsp))] + want2 = set(key for key, projs in direct + if direct[(key, projs)] == tiny_target) + rec2 = ES.six_distinct_search(ga, g, t2, labels6, (2, 4), w_all2, + target=tiny_target) + found2 = set() + for key in ("m2", "m4"): + for wkey, u, v, _ in rec2[key]["all_witnesses"]: + found2.add((wkey[0], (u, v))) + assert found2 == want2, (found2, want2) + assert len(want2) >= 1 + marker("tiny_completeness_t2_n6 family_hits=%d" % len(want2)) + + # ------------------------------------------------------------------ + # 4. KB2 run: complete six-distinct-value family at t = 5, n = 13. + # ------------------------------------------------------------------ + receipts = ES.six_distinct_search(ga, g, 5, labels13, (2, 4, 6, 8), w_all) + total_evals = 0 + total_assign = 0 + total_surv = 0 + for key in ("m2", "m4", "m6", "m8"): + r = receipts[key] + total_evals += r["evaluations"] + total_assign += r["assignments"] + total_surv += r["survivors"] + print(" %s: assignments=%d signatures=%d peak_dp=%d evals=%d " + "survivors=%d sig_sha256=%s" + % (key, r["assignments"], r["signatures"], r["peak_dp_states"], + r["evaluations"], r["survivors"], r["signature_sha256"])) + assert total_surv == 0, receipts + + # shard receipts over the m=2 signature list (parallel-safe batches) + print(" coverage: six-distinct family complete for m_W in {2,4,6,8}; " + "d<=5 commuting family excluded by the predecessor " + "(research/fiveswap-alt13-commuting-screen); d>=7 NOT covered") + print("PASS_KB2_ALT13_NONCOMMUTING_TOOLING", + "assignments=%d" % total_assign, + "evaluations=%d" % total_evals, + "survivors=%d" % total_surv, + "frontier=d6_complete_d_ge_7_open", + "no_new_kappa", + "elapsed=%.1fs" % (time.time() - t0)) + return 0 + + +if __name__ == "__main__": + raise SystemExit(main()) diff --git a/tests/test_research_exact_word_search.py b/tests/test_research_exact_word_search.py new file mode 100644 index 0000000000..fcc2e90bf0 --- /dev/null +++ b/tests/test_research_exact_word_search.py @@ -0,0 +1,281 @@ +"""Failure-sensitive controls for the reusable exact-search tooling in +research/kb2-alt13-noncommuting-tooling/exact_search.py. + +Run: python -B -m unittest tests.test_research_exact_word_search -v +""" + +import hashlib +import importlib.util +import itertools +import pathlib +import random +import sys +import unittest + +ROOT = pathlib.Path(__file__).resolve().parents[1] +MODULE_PATH = ROOT / "research" / "kb2-alt13-noncommuting-tooling" / "exact_search.py" + + +def load(): + spec = importlib.util.spec_from_file_location("exact_search", MODULE_PATH) + mod = importlib.util.module_from_spec(spec) + spec.loader.exec_module(mod) + return mod + + +ES = load() + + +class TestGroups(unittest.TestCase): + def test_gl2f2_relations(self): + g = ES.gl2f2() + self.assertEqual(g.n, 6) + e, a, b, s = g.identity, g.A, g.B, g.S + self.assertEqual(g.mul(a, a), e) + self.assertEqual(g.mul(b, b), e) + self.assertEqual(g.mul(g.mul(a, b), a), s) + self.assertEqual(g.mul(g.mul(b, a), b), s) + + def test_q8_relations(self): + g = ES.q8() + self.assertEqual(g.n, 8) + e, x, y, z = g.identity, g.X, g.Y, g.Z + self.assertEqual(g.mul(x, x), z) + self.assertEqual(g.mul(y, y), z) + self.assertEqual(g.mul(g.mul(g.mul(x, y), x), y), z) + self.assertNotEqual(g.mul(x, y), g.mul(y, x)) + + +class TestAlphabets(unittest.TestCase): + def test_rank_one_idempotent_counts(self): + self.assertEqual(len(ES.rank_one_idempotents(2)), 6) + self.assertEqual(len(ES.rank_one_idempotents(3)), 28) + self.assertEqual(len(ES.rank_one_idempotents(5)), 496) + t = 5 + eye = tuple(1 << i for i in range(t)) + for u, v in ES.rank_one_idempotents(t): + n = ES.proj_rows(t, u, v) + self.assertEqual(ES.mat_mul(t, n, n), n) + self.assertEqual(ES.mat_add(n, eye), ES.mat_add(eye, n)) + + +class TestWordModel(unittest.TestCase): + def setUp(self): + self.g = ES.gl2f2() + self.ga = ES.GroupAlgebra(self.g) + + def test_direct_words_reach_target(self): + for t in (1, 3, 5): + labels = [self.g.A, self.g.B, self.g.A] * t + projs = [ES.coord_proj(t, i // 3) for i in range(3 * t)] + self.assertEqual( + ES.word_product(self.ga, self.g, t, labels, projs), + ES.ring_target(self.ga, t, self.g.S), t) + + def test_mutated_word_fails(self): + t = 5 + labels = [self.g.A, self.g.B, self.g.A] * 5 + labels[1] = self.g.A + projs = [ES.coord_proj(t, i // 3) for i in range(15)] + self.assertNotEqual( + ES.word_product(self.ga, self.g, t, labels, projs), + ES.ring_target(self.ga, t, self.g.S)) + + def test_sign_quotient_sum_rule(self): + rng = random.Random(7) + t = 3 + for _ in range(50): + labels, projs = ES.random_tuple(self.g, t, 7, rng) + m0, m1 = ES.sign_quotient_word(self.g, t, labels, projs) + eye = tuple(1 << i for i in range(t)) + want1 = ES.proj_sum(t, [ES.proj_rows(t, u, v) for u, v in projs]) + self.assertEqual(m0, eye) + self.assertEqual(m1, want1) + + def test_sign_natural_equivalent_to_endpoint(self): + rng = random.Random(11) + t = 3 + agree = 0 + for _ in range(200): + labels, projs = ES.random_tuple(self.g, t, 6, rng) + full = ES.endpoint_check(self.ga, self.g, t, labels, projs) + quot = (ES.sign_check(self.g, t, labels, projs) + and ES.natural_check(self.g, t, labels, projs)) + self.assertEqual(full, quot) + agree += full + # structured near-misses so both outcomes occur + labels = [self.g.A, self.g.B, self.g.A] * 3 + projs = [ES.coord_proj(3, i // 3) for i in range(9)] + self.assertTrue(ES.endpoint_check(self.ga, self.g, 3, labels, projs)) + projs[0] = ES.coord_proj(3, 1) + self.assertFalse(ES.endpoint_check(self.ga, self.g, 3, labels, projs)) + + def test_c_invariant_equivalent_to_endpoint(self): + rng = random.Random(13) + t = 3 + for _ in range(200): + labels, projs = ES.random_tuple(self.g, t, 6, rng) + full = ES.endpoint_check(self.ga, self.g, t, labels, projs) + cok = ES.c_conditions_ok(t, labels, projs) + self.assertEqual(full, cok) + + +class TestClassificationLemmas(unittest.TestCase): + def test_t_summands_over_f2_3_are_dual_frames(self): + # k = t rank-one idempotents summing to I_t are automatically a dual + # frame (V^T U is an invertible idempotent, hence I). + t = 3 + projs = ES.rank_one_idempotents(t) + eye = tuple(1 << i for i in range(t)) + checked = 0 + for comb in itertools.combinations(range(len(projs)), 3): + rows = [ES.proj_rows(t, projs[i][0], projs[i][1]) for i in comb] + if ES.proj_sum(t, rows) != eye: + continue + checked += 1 + for i, j in itertools.combinations(comb, 2): + ui, vi = projs[i] + uj, vj = projs[j] + self.assertEqual(ES.dot(vi, uj), 0) + self.assertEqual(ES.dot(vj, ui), 0) + self.assertGreater(checked, 0) + + def test_more_than_t_summands_need_not_commute(self): + # the dual-frame collapse is exactly k = t: at k = t + 2 there are + # noncommuting summand sets (this is what makes d >= 7 tuples open). + t = 3 + projs = ES.rank_one_idempotents(t) + eye = tuple(1 << i for i in range(t)) + found = False + for comb in itertools.combinations(range(len(projs)), 5): + rows = [ES.proj_rows(t, projs[i][0], projs[i][1]) for i in comb] + if ES.proj_sum(t, rows) != eye: + continue + for i, j in itertools.combinations(comb, 2): + ui, vi = projs[i] + uj, vj = projs[j] + if ES.dot(vi, uj) or ES.dot(vj, ui): + found = True + break + if found: + break + self.assertTrue(found) + + def test_four_summands_never_reach_identity_f2_3(self): + t = 3 + projs = ES.rank_one_idempotents(t) + eye = tuple(1 << i for i in range(t)) + for comb in itertools.combinations(range(len(projs)), 4): + rows = [ES.proj_rows(t, projs[i][0], projs[i][1]) for i in comb] + self.assertNotEqual(ES.proj_sum(t, rows), eye) + + +class TestBruteForceBaseline(unittest.TestCase): + def test_t2_length6_is_exact_minimum(self): + g = ES.gl2f2() + ga = ES.GroupAlgebra(g) + t = 2 + alphabet = ES.rank_one_idempotents(t) + target = ES.ring_target(ga, t, g.S) + labels = [g.A, g.B, g.A, g.B, g.A, g.B] + # length 4: exhaustive negative + found4 = 0 + for tup in itertools.product(alphabet, repeat=4): + if ES.word_product(ga, g, t, labels[:4], + [ES.proj_rows(t, u, v) for u, v in tup]) == target: + found4 += 1 + self.assertEqual(found4, 0) + # length 6: the direct word is a witness + direct = [ES.coord_proj(t, 0), ES.coord_proj(t, 0), ES.coord_proj(t, 0), + ES.coord_proj(t, 1), ES.coord_proj(t, 1), ES.coord_proj(t, 1)] + self.assertEqual(ES.word_product(ga, g, t, labels, direct), target) + + +class TestFastEval(unittest.TestCase): + def test_signature_expansion_matches_generic(self): + rng = random.Random(17) + g = ES.gl2f2() + ga = ES.GroupAlgebra(g) + t = 5 + for _ in range(8): + labels, projs = ES.random_tuple(g, t, 13, rng) + # split into frame classes + free projector to exercise both paths + slow = ES.word_product(ga, g, t, labels, projs) + fast = ES.expanded_word_product(ga, g, t, labels, projs) + self.assertEqual(slow, fast) + + def test_frame_plus_extra_eval_matches_generic(self): + rng = random.Random(23) + g = ES.gl2f2() + ga = ES.GroupAlgebra(g) + t = 5 + labels = ES.alt_labels(g, 13) + alphabet = ES.rank_one_idempotents(t) + for _ in range(10): + m = rng.randrange(1, 5) + w_pos = sorted(rng.sample(range(13), m)) + w_u, w_v = alphabet[rng.randrange(len(alphabet))] + assign = [rng.randrange(t) for _ in range(13)] + h = [[g.identity] * (m + 1) for _ in range(t)] + projs = [] + seg = 0 + for i in range(13): + if i in w_pos: + projs.append((w_u, w_v)) + seg += 1 + else: + projs.append(ES.coord_proj(t, assign[i])) + h[assign[i]][seg] = g.mul(h[assign[i]][seg], labels[i]) + slow = ES.word_product(ga, g, t, labels, projs) + fast = ES.sig_eval(ga, g, t, [labels[i] for i in w_pos], + h, w_u, w_v) + self.assertEqual(slow, fast) + # mutation control: corrupting one segment product must change it + h[0][0] = g.mul(h[0][0], g.A) + mutated = ES.sig_eval(ga, g, t, [labels[i] for i in w_pos], + h, w_u, w_v) + self.assertNotEqual(slow, mutated) + + def test_gl_conjugation_invariance(self): + rng = random.Random(19) + g = ES.gl2f2() + ga = ES.GroupAlgebra(g) + t = 5 + labels = [g.A, g.B, g.A] * 5 + projs = [ES.coord_proj(t, i // 3) for i in range(15)] + eye = ES.ring_target(ga, t, g.S) + self.assertEqual(ES.word_product(ga, g, t, labels, projs), eye) + p, pinv = ES.random_gl(t, rng) + conj = [ES.proj_conj(t, u, v, p, pinv) for u, v in projs] + self.assertEqual(ES.word_product(ga, g, t, labels, conj), eye) + + +class TestLayerBalls(unittest.TestCase): + def test_q8_layer_calibration(self): + g = ES.q8() + ga = ES.GroupAlgebra(g) + t = 2 + alphabet = [ES.proj_rows(t, u, v) for u, v in ES.rank_one_idempotents(t)] + gens = [ES.call_matrix(ga, g, t, lbl, n) + for lbl in (g.X, g.Y) for n in alphabet] + layers = ES.layer_ball_sizes(ga, gens, 3) + self.assertEqual(layers, [1, 12, 110, 936]) + + +class TestBatchSplit(unittest.TestCase): + def test_shards_partition_and_are_stable(self): + items = list(range(1000)) + s1 = ES.shard_split(items, 7) + s2 = ES.shard_split(items, 7) + self.assertEqual(s1, s2) + self.assertEqual(len(s1), 7) + flat = [x for sh in s1 for x in sh["items"]] + self.assertEqual(sorted(flat), items) + for sh in s1: + self.assertEqual(sh["sha256"], + hashlib.sha256( + ",".join(map(str, sh["items"])).encode()).hexdigest()) + + +if __name__ == "__main__": + unittest.main()