From 139779c86ba8215910117ddb383e4df007b23dcf Mon Sep 17 00:00:00 2001 From: Aaron Wang Date: Thu, 15 Oct 2026 00:54:50 -0400 Subject: [PATCH] Screen: no thirteen-call five-SWAP word with commuting projectors (scoped negative) Adds research/fiveswap-alt13-commuting-screen: a complete exact screen of the pairwise-commuting projector subfamily for the strictly alternating 13-call candidate at t=5 fully occupied coordinate-SWAP roles in the formal F2[GL_2(F2)] rank-one-idempotent register model. Every frame class needs at least three word positions, so q >= 3t in this family and the direct 3t tariff is exact there; in particular no 5-class partition of 13 positions exists. Any 13-call escape must use noncommuting scalar projectors. No new kappa. Aaron Wang, with help from opencode. --- .../fiveswap-alt13-commuting-screen/README.md | 153 ++++++++ .../SOURCES.json | 24 ++ .../fiveswap-alt13-commuting-screen/TASK.json | 69 ++++ .../VERIFY.json | 21 ++ .../fiveswap-alt13-commuting-screen/verify.py | 333 ++++++++++++++++++ 5 files changed, 600 insertions(+) create mode 100644 research/fiveswap-alt13-commuting-screen/README.md create mode 100644 research/fiveswap-alt13-commuting-screen/SOURCES.json create mode 100644 research/fiveswap-alt13-commuting-screen/TASK.json create mode 100644 research/fiveswap-alt13-commuting-screen/VERIFY.json create mode 100644 research/fiveswap-alt13-commuting-screen/verify.py diff --git a/research/fiveswap-alt13-commuting-screen/README.md b/research/fiveswap-alt13-commuting-screen/README.md new file mode 100644 index 0000000000..d29ed69847 --- /dev/null +++ b/research/fiveswap-alt13-commuting-screen/README.md @@ -0,0 +1,153 @@ +# Five fully occupied SWAP targets: no thirteen-call word with commuting projectors + +**Scoped negative screen; no new kappa.** In the formal `F2[GL_2(F2)]` +coordinate-CNOT register model, this package screens the strictly alternating +thirteen-call candidate for five fully occupied coordinate-SWAP targets inside +the **pairwise-commuting projector subfamily**. The screen is complete and +excludes that family: every frame class needs at least three word positions, so +no partition of thirteen positions into five classes exists. In fact the same +argument shows `q >= 3t` for commuting projectors at any fully occupied target +count `t`, so the direct `3t` tariff is exact inside this family. Any +thirteen-call escape for five targets must use noncommuting scalar projectors. +The selected result, the selected bit supplier and `upstream/` are unchanged; +the bit side does not bind. + +## Model (unchanged coordinate-CNOT line) + +Let `a=[[1,1],[0,1]]`, `b=[[1,0],[1,1]]`, and `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`). Every call, including an undo, costs +one. Free scalar `GL_t(F2)` mixing is normalized by augmentation (credit: +PR1333). The target is `T=[s] I_t` at exactly `r=t` fully occupied roles with +arbitrary dirty inputs restored exactly. Equality is equality of all formal +group-algebra coefficients. + +## Why thirteen calls, why alternating + +`research/four-swap-full-occupancy` proves that any fully occupied `t`-target +word saving over `3t` has `q >= 2t+3` (every rotated cut carries both label +counts at least `t+1`), and that at equality the labels strictly alternate +(credit: Ross Richardson's rotation step and the PR1722 saturation lemma). +For `t=5` the sign trace `q = t mod 2` then leaves exactly one candidate below +the direct fifteen: `q=13`, strictly alternating. That package's open question +2 asks whether rank-one idempotent unknowns can realize it and names +noncommuting scalar-projector interactions as the blocker. This package closes +the commuting part of that question. + +## Necessary conditions and the commuting reduction + +Work in the natural quotient `R -> M_2(F2)` (`[g] -> g`). A call maps to +`I + (g+I) tensor N`; expanding the product, a subsequence of calls survives +exactly when consecutive picked labels differ, and contributes +`(N-product) tensor E(row of last label, col of first label)`. Comparing with +the target `I_t tensor (E12+E21)` gives, for every frame class position set +`S`, four mod-2 conditions on the label-alternating nonempty subsequences of +`S`: each of the four `(first label, last label)` counts `(a,a)`, `(a,b)`, +`(b,a)`, `(b,b)` must be **odd** (the empty subsequence cancels the `E11` and +`E22` identity terms). + +**Commuting reduction.** The sign quotient (`[g] -> 1+epsilon` over +`F2[epsilon]/(epsilon^2)`) gives `sum N_i = I_t`. Pairwise-commuting distinct +rank-one idempotents are equal or mutually orthogonal (`phi_i v_j = 0`), and an +orthogonal distinct sum equal to `I_t` uses exactly `t` projectors forming a +frame with odd multiplicities (any extra even-multiplicity projector would +need `v=0`). Up to `GL_t` conjugation the word is therefore a coordinate-frame +word, and each of the `t` classes must satisfy the four conditions above. + +**Size floor.** A class of size one or two fails the conditions for every +label word: one subsequence contributes to exactly one category; two positions +contribute to at most three. Hence every class has at least three positions and +`q >= 3t` in the commuting family. The direct word `aba` on each coordinate +attains `3t`, so the tariff is exact there. For `t=5`, thirteen positions +cannot fill five classes of size at least three. + +## Checked results (`verify.py`, exact, stdlib only) + +```text +PASS_FIVESWAP_ALT13_COMMUTING_SCREEN min_class=3 admissible_sets=1365 size_hist=3:91,5:455,7:546,9:247,11:26 partitions5=0 direct15_partitions=608 small_pairs=2046 commuting_pairs=196 frames3=28 no_new_kappa +``` + +- Formal product controls: the direct words for `t=1` (3 calls), `t=3` (9 + calls) and `t=5` (15 calls) reach `[s] I_t` exactly in `M_t(R)`. +- Complete screen of all 8,191 nonempty position sets of the strictly + alternating thirteen-label word: 1,365 sets are admissible, the minimum + admissible size is 3, and an exact-cover DP finds **zero** partitions of the + thirteen positions into five admissible classes. All admissible sizes are + odd, matching the sign equation's odd-multiplicity deduction. +- Positive structural control: the direct fifteen-call partition passes the + conditions (608 five-class partitions pass in total). +- Failure controls: a mutated direct word fails the formal product; a + size-one class is rejected; the universal size floor is checked + exhaustively for every label word through length six (2,046 cases); an + explicit noncommuting idempotent pair witnesses that the excluded family is + strict. +- Reduction-lemma support: exhaustive over `F2^3` (28 rank-one idempotents): + every commuting pair is equal or orthogonal (196 commuting pairs), and 28 + orthogonal triples sum to `I_3`. + +## Scope and what is not checked + +This is a finite exact screen of a declared subfamily plus a written reduction, +not a general exclusion of thirteen-call words. No noncommuting tuple search is +attempted; the general block equations above are recorded as the handoff for +that search. No partial-occupancy (restored dirty extras, `r > t`) claim is +made: at partial targets the rotation and the block comparison change shape +(see the workspace boundary in `research/four-swap-full-occupancy`). No Lean +formalization, independent human review, physical compilation, hosting, +precision/tape, analytic transfer or selected-supplier cold replay is claimed. +The result is author-checked only. + +## Reproduce + +Python 3.12 and the standard library suffice. From the repository root: + +```sh +python3 -I -B research/fiveswap-alt13-commuting-screen/verify.py +python3 scripts/research_package.py --package research/fiveswap-alt13-commuting-screen --check-only +``` + +Expected marker: `PASS_FIVESWAP_ALT13_COMMUTING_SCREEN ... partitions5=0 ... +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 `c91910338314e7e3bba60391fdf5bb54` +(track `bit-mechanisms`). [TASK.json](TASK.json) records the refined scope. +The claim is in +[discussion 1317](https://github.com/CrocSwap/integer-mult-bounds/discussions/1317#discussioncomment-18940800). + +Predecessors and credit: commdata2338 (PR1414/PR1491) for the formal model, +sign invariant and swap results; Gareth Davidson (PR1333) for scalar +normalization; Cinna Davis (PR1541) for workspace reasoning; Ross Richardson +(PR1722) for the saturation lemma and `research/four-swap-full-occupancy` for +the rotation step and uniform cut consequence whose open question 2 this +package narrows. `research/three-swap-cnot-census` and +`research/three-swap-compression-seed6` closed `t=3` at any workspace; +`research/four-swap-r4-cnot` records the `t=4` residual search. Overlap search +refreshed 2026-10-15 04:42 UTC with complete pagination (526 open PRs, 994 +discussion records); no claim on the `t=5` object was found. No matches is not +a novelty certificate. + +Prepared by **Aaron Wang** with help from opencode (substantial AI assistance; +no independent human review). New work is Apache-2.0; predecessor sources and +notices are unchanged. + +## Open next questions + +1. **Can noncommuting rank-one idempotents realize the strictly alternating + thirteen-call word for five fully occupied targets?** Why it matters: it is + the only remaining potential saving below the direct fifteen-call tariff at + five roles in this alphabet. First step: feed the four block equations and + the sign equation to a quadratic/backtracking search over noncommuting + tuples, smallest falsifying instance first (one class near-commuting). + Blocker: no SAT/SMT tooling on this host; the noncommuting + scalar-projector interactions are exactly where the reduction stops. +2. **Does the commuting obstruction survive one restored dirty extra + register?** Why it matters: it would extend the `q >= 3t` commuting tariff + toward the `t=4, r=5` workspace question of `research/four-swap-r4-cnot`. + First step: re-derive the block comparison for `P = diag(I_t, 0)` and test + the four conditions on the smallest coupled projector example. Blocker: at + partial targets conjugation leaves the paid alphabet (the recorded workspace + boundary), so the reduction needs a replacement for the frame argument. diff --git a/research/fiveswap-alt13-commuting-screen/SOURCES.json b/research/fiveswap-alt13-commuting-screen/SOURCES.json new file mode 100644 index 0000000000..befce00448 --- /dev/null +++ b/research/fiveswap-alt13-commuting-screen/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/RESULT.json", + "usage": "input", + "git_blob": "ad6c5892fd34c2b14ad70843ff9512048146d789", + "sha256": "810dfd32a127d9e850cf01783d45fbb509ac9eae1919c1de26bc3bfa0cb83140" + } + ] +} diff --git a/research/fiveswap-alt13-commuting-screen/TASK.json b/research/fiveswap-alt13-commuting-screen/TASK.json new file mode 100644 index 0000000000..24bf3a37d4 --- /dev/null +++ b/research/fiveswap-alt13-commuting-screen/TASK.json @@ -0,0 +1,69 @@ +{ + "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": "refined", + "actual_scope": "In the formal F2[GL_2(F2)] rank-one-idempotent register model at exactly t=5 fully occupied coordinate-SWAP roles, screen the strictly alternating thirteen-call candidate (isolated by research/four-swap-full-occupancy's uniform cut consequence) inside the pairwise-commuting projector subfamily, and derive the general block-equation handoff for the noncommuting remainder.", + "scope_change_reason": "Refinement of the drawn card's first experiment (price one smallest completed instance after a named changed premise). The changed premise is the target-count boundary t=5 left open by the predecessor's cut bound; the drawn GL3/Q8-style censuses are covered by #1974/#2248/#2303 and the paired agent's fresh Q8 claim, so this object was chosen to avoid those.", + "bottleneck_link": "Side result on the bit primitive: the bit side does not bind (complex side binds the selected kappa). The screen removes the pairwise-commuting part of the only remaining sub-direct saving (thirteen vs fifteen calls) in the coordinate-CNOT tariff, so any shared-work saving search can skip commuting tuples; no kappa or supplier claim follows.", + "budget_minutes": 45, + "stop_rule": "Stop once the commuting-family screen is complete (minimum admissible class size and five-class partition count computed), all positive and failure controls pass, and the noncommuting remainder is recorded as a handoff; no noncommuting tuple search in this session.", + "outcome": "completed", + "evidence": "PASS_FIVESWAP_ALT13_COMMUTING_SCREEN min_class=3 admissible_sets=1365 size_hist=3:91,5:455,7:546,9:247,11:26 partitions5=0 direct15_partitions=608 small_pairs=2046 commuting_pairs=196 frames3=28 no_new_kappa; formal product controls pass for t=1,3,5 direct words and a mutated word fails.", + "author": "Aaron Wang", + "ai_assistance": "with help from opencode (substantial AI assistance in reasoning, implementation and writing; no independent human review claimed)", + "open_questions": [ + { + "question": "Can noncommuting rank-one idempotents realize the strictly alternating thirteen-call word for five fully occupied targets?", + "why_it_matters": "It is the only remaining potential saving below the direct fifteen-call tariff at five roles in this alphabet.", + "first_step": "Feed the four block equations and the sign equation to a quadratic or backtracking search over noncommuting tuples, smallest falsifying instance first.", + "blocked_by": "No SAT/SMT tooling on this host; noncommuting scalar-projector interactions are exactly where the commuting reduction stops." + }, + { + "question": "Does the commuting obstruction survive one restored dirty extra register (t=4 or t=5, r>t)?", + "why_it_matters": "It would extend the q >= 3t commuting tariff toward the workspace question of research/four-swap-r4-cnot.", + "first_step": "Re-derive the block comparison for P = diag(I_t, 0) and test the four conditions on the smallest coupled projector example.", + "blocked_by": "At partial targets conjugation leaves the paid alphabet (recorded workspace boundary), so the frame reduction needs a replacement." + } + ] +} diff --git a/research/fiveswap-alt13-commuting-screen/VERIFY.json b/research/fiveswap-alt13-commuting-screen/VERIFY.json new file mode 100644 index 0000000000..ffb2e4ce20 --- /dev/null +++ b/research/fiveswap-alt13-commuting-screen/VERIFY.json @@ -0,0 +1,21 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/four-swap-full-occupancy/RESULT.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Formal group-algebra product controls (t = 1, 3, 5 direct words), exact admissibility screen of all 8191 nonempty position sets of the alternating thirteen-label word, zero five-class partitions, direct fifteen-call positive control, universal size-at-most-two inadmissibility through length six, mutated-word and family-boundary failure controls, and exhaustive commuting-pair orthogonality on F2^3." + } + ] +} diff --git a/research/fiveswap-alt13-commuting-screen/verify.py b/research/fiveswap-alt13-commuting-screen/verify.py new file mode 100644 index 0000000000..c7ce747a30 --- /dev/null +++ b/research/fiveswap-alt13-commuting-screen/verify.py @@ -0,0 +1,333 @@ +#!/usr/bin/env python3 +"""Exact screen of the pairwise-commuting projector family for fully occupied +coordinate-SWAP words in the formal F2[GL_2(F2)] register model. + +Model (the PR1333/1414/1491/1541/1722 coordinate-CNOT line, unchanged): + G = GL_2(F2) = , s = aba = bab. R = F2[G]. + Paid call D_N(g) = I + ([g]+1) N with g in {a, b} and N = u v^T, + v^T u = 1 over F2 (binary rank-one idempotent). + Target T = [s] I_t at exactly r = t fully occupied roles, arbitrary dirty + inputs, free scalar GL_t(F2) mixing (normalized by augmentation). + +Scoped negative result (no new kappa): + Any pairwise-commuting tuple of rank-one idempotent projectors satisfying the + sign equation sum N_i = I_t is, up to GL_t conjugation, a word over one + orthogonal frame of exactly t projectors, each appearing with odd + multiplicity. Every frame class occupies at least three word positions + (classes of size <= 2 fail four mod-2 conditions derived from the natural + quotient). Hence q >= 3t in this family: the direct 3t tariff is exact. In + particular there is no strictly alternating thirteen-call word for t = 5 with + pairwise-commuting projectors; any thirteen-call escape must use noncommuting + scalar projectors. + +Checks in this file: + 1. Formal group-algebra product engine (right-multiplication-free, exact). + 2. Positive word controls: t = 1 (3 calls), t = 3 (9 calls), t = 5 (15 + calls) direct words reach [s] I_t exactly. + 3. Necessary-condition screen: four (first, last) label categories of + label-alternating subsequences must each be odd per frame class; classes + of size <= 2 are inadmissible for every label word (exhaustive to length + 6); for the strictly alternating 13-label word the minimum admissible + class size is 3 and no partition of 13 positions into 5 admissible + classes exists (exact-cover DP). + 4. Failure controls: mutated direct word fails the formal product; a class + failing one category is rejected; a noncommuting projector pair exists + (the family is strict). + 5. Reduction-lemma support: pairwise-commuting distinct rank-one idempotents + are equal or orthogonal (exhaustive over F2^3), and an orthogonal + distinct sum equal to I_r uses exactly r frames. + +Aaron Wang, with help from opencode. Apache-2.0. Stdlib only. +""" + +import itertools +import sys + +# -------------------------------------------------------------------------- +# Group algebra F2[G], G = GL_2(F2) as 2x2 binary matrices packed in 0..15. +# -------------------------------------------------------------------------- + +def mmul(x, y): + """Product of two packed 2x2 binary matrices: bits b3..b0 = r0c0, r0c1, + r1c0, r1c1, over F2.""" + 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 + + +GL2 = [m for m in range(16) + if (((m >> 3) & 1) * (m & 1)) ^ (((m >> 2) & 1) * ((m >> 1) & 1))] +GL2.sort() +assert len(GL2) == 6 +GIDX = {m: i for i, m in enumerate(GL2)} +E_ID = GIDX[0b1001] # identity [[1,0],[0,1]] +A = GIDX[0b1101] # [[1,1],[0,1]] +B = GIDX[0b1011] # [[1,0],[1,1]] +S = GIDX[0b0110] # [[0,1],[1,0]] = aba = bab + +GTMUL = [[GIDX[mmul(GL2[i], GL2[j])] for j in range(6)] for i in range(6)] +assert GTMUL[GTMUL[A][B]][A] == S +assert GTMUL[GTMUL[B][A]][B] == S + + +def rmul(x, y): + """Product in R = F2[G]; elements are 6-bit masks indexed like GL2.""" + out = 0 + xs = [i for i in range(6) if (x >> i) & 1] + ys = [i for i in range(6) if (y >> i) & 1] + for i in xs: + for j in ys: + out ^= 1 << GTMUL[i][j] + return out + + +# -------------------------------------------------------------------------- +# Matrices over R: tuple of tuples of 6-bit masks. +# -------------------------------------------------------------------------- + +def eye(r): + return tuple(tuple((1 << E_ID) if i == j else 0 for j in range(r)) + for i in range(r)) + + +def matmul(p, q, r): + out = [[0] * r for _ in range(r)] + for i in range(r): + for k in range(r): + aik = p[i][k] + if aik: + for j in range(r): + bkj = q[k][j] + if bkj: + out[i][j] ^= rmul(aik, bkj) + return tuple(tuple(row) for row in out) + + +def call_matrix(r, g_idx, cls): + """D_N(g) with N = e_c e_c^T for the coordinate family (cls = c index).""" + one = 1 << E_ID + gbit = 1 << g_idx + rows = [] + for i in range(r): + row = [] + for j in range(r): + v = one if i == j else 0 + if i == j == cls: + v ^= gbit ^ one # ([g]+1) on the projector cell + row.append(v) + rows.append(tuple(row)) + return tuple(rows) + + +def word_product(r, labels, classes): + """Product D_q ... D_1 (labels[0] applied first).""" + acc = eye(r) + for lab, cls in zip(labels, classes): + g = A if lab == "a" else B + acc = matmul(call_matrix(r, g, cls), acc, r) + return acc + + +def target(r): + sbit = 1 << S + return tuple(tuple(sbit if i == j else 0 for j in range(r)) + for i in range(r)) + + +# -------------------------------------------------------------------------- +# Necessary-condition screen (natural quotient blocks). +# -------------------------------------------------------------------------- + +CATS = ("aa", "ab", "ba", "bb") + + +def category_counts(labels, positions): + """Parity of label-alternating nonempty subsequences of `positions` + (a sorted tuple of word indices) by (first label, last label).""" + counts = {c: 0 for c in CATS} + n = len(positions) + for mask in range(1, 1 << n): + picks = [positions[k] for k in range(n) if (mask >> k) & 1] + labs = [labels[i] for i in picks] + if any(labs[t] == labs[t + 1] for t in range(len(labs) - 1)): + continue # E-product vanishes + counts[labs[0] + labs[-1]] ^= 1 + return counts + + +def admissible(labels, positions): + counts = category_counts(labels, positions) + return all(counts[c] for c in CATS) + + +def partitions_into_admissible(labels, k): + """Number of unordered partitions of all word positions into exactly k + admissible classes (exact-cover DP over masks).""" + n = len(labels) + full = (1 << n) - 1 + adm = [m for m in range(1, full + 1) + if admissible(labels, tuple(i for i in range(n) if (m >> i) & 1))] + dp = [[0] * (k + 1) for _ in range(full + 1)] + dp[0][0] = 1 + for mask in range(1, full + 1): + low = mask & -mask + for sub in adm: + if (sub & low) and (sub & ~mask) == 0: + rest = mask ^ sub + for j in range(1, k + 1): + dp[mask][j] += dp[rest][j - 1] + return dp[full][k], len(adm) + + +# -------------------------------------------------------------------------- +# Reduction-lemma support (exhaustive over F2^3). +# -------------------------------------------------------------------------- + +def proj3(): + """All binary rank-one idempotents on F2^3: (image v, covector phi).""" + out = [] + for v in range(1, 8): + for phi in range(1, 8): + dot = bin(v & phi).count("1") & 1 + if dot: + out.append((v, phi)) + return out + + +def nmat(v, phi): + return tuple(tuple(1 if ((v >> i) & 1) and ((phi >> j) & 1) else 0 + for j in range(3)) for i in range(3)) + + +def nmul(x, y): + out = [[0] * 3 for _ in range(3)] + for i in range(3): + for k in range(3): + for j in range(3): + out[i][j] ^= x[i][k] & y[k][j] + return tuple(tuple(r) for r in out) + + +def lemma_checks(): + ps = proj3() + mats = [nmat(v, phi) for v, phi in ps] + assert len(ps) == 28 + checked = 0 + for i in range(28): + for j in range(28): + xi, xj = mats[i], mats[j] + if nmul(xi, xj) == nmul(xj, xi): + checked += 1 + if i != j: + # distinct commuting rank-one idempotents are orthogonal + v_i, phi_i = ps[i] + v_j, phi_j = ps[j] + assert bin(phi_i & v_j).count("1") & 1 == 0 + assert bin(phi_j & v_i).count("1") & 1 == 0 + # orthogonal distinct sets summing to I_3 have exactly 3 elements + frames = 0 + for comb in itertools.combinations(range(28), 3): + acc = tuple(tuple(0 for _ in range(3)) for _ in range(3)) + ok = True + for i in comb: + for j in comb: + if i != j: + v_i, phi_i = ps[i] + v_j, phi_j = ps[j] + if (bin(phi_i & v_j).count("1") & 1) or \ + (bin(phi_j & v_i).count("1") & 1): + ok = False + acc = tuple(tuple(acc[p][q] ^ mats[i][p][q] for q in range(3)) + for p in range(3)) + if ok and acc == tuple(tuple(1 if p == q else 0 for q in range(3)) + for p in range(3)): + frames += 1 + return checked, frames + + +# -------------------------------------------------------------------------- +# Main: positive controls, screen, failure controls. +# -------------------------------------------------------------------------- + +def main(): + sys.stdout.reconfigure(encoding="utf-8") + + # 2. Positive word controls: direct 3-call-per-swap words reach [s] I_t. + for t, expect_ok in ((1, True), (3, True), (5, True)): + labels = ["a", "b", "a"] * t + classes = [i // 3 for i in range(3 * t)] + got = word_product(t, labels, classes) + assert (got == target(t)) == expect_ok, t + + # mutated word must NOT reach the target + labels = ["a", "b", "a"] * 5 + labels[1] = "a" + classes = [i // 3 for i in range(15)] + assert word_product(5, labels, classes) != target(5) + + # 3. Screen on the strictly alternating 13-label word (t = 5 candidate). + alt13 = ["a" if i % 2 == 0 else "b" for i in range(13)] + sizes = {} + adm_sets = 0 + min_size = 99 + for mask in range(1, 1 << 13): + pos = tuple(i for i in range(13) if (mask >> i) & 1) + if admissible(alt13, pos): + adm_sets += 1 + sizes[len(pos)] = sizes.get(len(pos), 0) + 1 + min_size = min(min_size, len(pos)) + parts5, _ = partitions_into_admissible(alt13, 5) + assert min_size == 3, min_size + assert parts5 == 0, parts5 + + # positive structural control: the direct 15-call partition passes + direct15 = ["a", "b", "a"] * 5 + for c in range(5): + pos = tuple(range(3 * c, 3 * c + 3)) + assert admissible(direct15, pos), c + parts_direct, _ = partitions_into_admissible(direct15, 5) + assert parts_direct >= 1, parts_direct + + # universal small-size control: classes of size <= 2 fail for every + # label word of length <= 6 + small = 0 + for n in range(1, 7): + for labs in itertools.product("ab", repeat=n): + labs = list(labs) + for k in (1, 2): + for pos in itertools.combinations(range(n), k): + assert not admissible(labs, pos), (labs, pos) + small += 1 + + # failure control: a class failing one category is rejected + counts = category_counts(alt13, (0, 1, 2)) + assert all(counts[c] for c in CATS) + assert not admissible(alt13, (0,)) + + # 4/5. Reduction-lemma support and family-boundary witness. + checked, frames = lemma_checks() + assert checked > 0 and frames > 0 + n1 = nmat(1, 1) # e0 e0^T + n2 = nmat(1, 3) # e0 (e0+e1)^T, idempotent + assert nmul(n1, n1) == n1 and nmul(n2, n2) == n2 + assert nmul(n1, n2) != nmul(n2, n1) # noncommuting pair exists + + print("PASS_FIVESWAP_ALT13_COMMUTING_SCREEN", + "min_class=%d" % min_size, + "admissible_sets=%d" % adm_sets, + "size_hist=%s" % ",".join("%d:%d" % (k, sizes[k]) for k in sorted(sizes)), + "partitions5=%d" % parts5, + "direct15_partitions=%d" % parts_direct, + "small_pairs=%d" % small, + "commuting_pairs=%d" % checked, + "frames3=%d" % frames, + "no_new_kappa") + return 0 + + +if __name__ == "__main__": + raise SystemExit(main())