From 295958fd4bcf3228da63f707294a786a05d88da7 Mon Sep 17 00:00:00 2001 From: Cursor Agent Date: Sat, 24 Oct 2026 12:26:18 +0000 Subject: [PATCH] Certify length 6 for two Q16 triple squares In F2[Q16] with paid generators x and y, both diag([x^2]^3) and diag([x^4]^3) have exact minimum 6. Mixing does not undercut the disjoint bill, and kappa is unchanged. Co-authored-by: riquelme.pereira --- research/q16-central-square/README.md | 150 +++++++ research/q16-central-square/SOURCES.json | 18 + research/q16-central-square/TASK.json | 66 +++ research/q16-central-square/VERIFY.json | 18 + research/q16-central-square/verify.py | 536 +++++++++++++++++++++++ 5 files changed, 788 insertions(+) create mode 100644 research/q16-central-square/README.md create mode 100644 research/q16-central-square/SOURCES.json create mode 100644 research/q16-central-square/TASK.json create mode 100644 research/q16-central-square/VERIFY.json create mode 100644 research/q16-central-square/verify.py diff --git a/research/q16-central-square/README.md b/research/q16-central-square/README.md new file mode 100644 index 0000000000..38da25a137 --- /dev/null +++ b/research/q16-central-square/README.md @@ -0,0 +1,150 @@ +# Quaternion triple squares need six calls + +**Finite register-model certificate; no new κ.** The selected result, both +primitive suppliers, and `upstream/` are unchanged. The complex primitive +binds, and these identities meet their disjoint bills. + +In the group algebra \(\mathbb F_2[Q_{16}]\), + +\[ +Q_{16}=\langle x,y\mid x^8=e,\ y^2=x^4,\ yxy^{-1}=x^{-1}\rangle, +\] + +with exactly three roles and paid calls + +\[ +D_N([g])=I+([g]+[e])N, +\qquad g\in\{x,y\}, +\] + +the minimum word lengths of \(\operatorname{diag}([x^2],[x^2],[x^2])\) and +\(\operatorname{diag}([x^4],[x^4],[x^4])\) are both 6. Here \(N\) runs over +all 28 rank-one idempotents in \(M_3(\mathbb F_2)\). Matrix equality is an +operator identity on arbitrary dirty states. The element \(x^4\) is the unique +order-2 element and is central; it is also \(y^2\). + +The changed hypothesis is the address group. The abelian three-register model +uses arbitrary rational rank-one frames. This alphabet uses only the two +quaternion generators and charges every call. There is no free scalar mixing +between calls and no fourth role. + +## Priced baseline + +Generator lengths, computed before the matrix search: + +| Target element | Shortest generator word | Disjoint three-role bill | +|---|---|---:| +| \(x^2\) | \(xx\) | 6 | +| \(x^4\) | \(yy\) | 6 | +| \(x^6\) | \(xxyy\) | 12 | + +The degree-1 relaxation does not decide these bills. The augmentation powers +of \(\mathbb F_2[Q_{16}]\) have dimensions \(15,13,11,9,7,5,3,1,0\). The +quotient \(\Delta/\Delta^2\) is spanned by \([x]+1\) and \([y]+1\). A product +of calls has degree-1 symbol equal to the sum of its projectors on each +generator: every call augments to \(I\), and the cross term \((M-I)\alpha N\) +has entries in \(\Delta^2\). Both triple squares, and the \(x^6\) triple, lie +in \(I+M_3(\Delta^2)\). Vanishing of the symbol forces each projector sum to +be zero. Every admitted projector has trace 1, so both label counts are even. +The relaxation therefore gives only the even-length floor 2. + +## Result + +Lengths 1 through 5 were enumerated in \(M_3(\mathbb F_2[Q_{16}])\). The exact +frontiers have sizes 56, 2352 and 92374. None contains either triple square. +The doubled coordinate words + +- \((E_{00},x)\) twice, then the same for \(E_{11}\) and \(E_{22}\), +- \((E_{00},y)\) twice, then the same for \(E_{11}\) and \(E_{22}\), + +equal the two targets. Both minima are therefore 6. A released two-role note +already observed that two copies of \(x^4\) cost 4 by the direct word. The +three-role search is the new statement: every admissible mixer still leaves +the disjoint bill of 6 unchanged. + +There are 799 length-3 prefix matrices with a length-3 continuation to the +central target. All 799 prefixes are pure \(y\)-words, and 792 of them use a +projector outside \(\{E_{00},E_{11},E_{22}\}\). Off-diagonal mixing occurs at +length 6 and still does not produce a shorter word. The same prefix-matrix +count 799 appears for the \(x^2\) triple. An earlier semidihedral package +reported the same count for a different presentation and different frontiers +(2051 and 68899). The count is not treated as a new mechanism. + +Separately, \(\operatorname{diag}([x^6],[x^6],[x^6])\) has no word of length +at most 6, and the coordinate word \(xxyy\) on each role has length 12. The +parity lemma above excludes the odd lengths 7, 9 and 11, which were not +enumerated. The exact minimum is therefore in \(\{8,10,12\}\) and is not +claimed to be sharp. + +## Reproduce + +From the repository root, with Python 3.12 and `PYTHONOPTIMIZE` unset: + +```sh +python3 -B research/q16-central-square/verify.py +python3 -B scripts/research_package.py --package research/q16-central-square +``` + +Expected final verifier line: + +```text +PASS_Q16_CENTRAL_SQUARE x2=6 x4=6 x6_through6=0 x6_upper=12 idempotents=28 calls=56 frontier2=2352 frontier3=92374 len4=0 len6_x2=799 len6_x4=799 len6_x6=0 central_nondiagonal_prefixes=792 group_lengths=2,2,4 controls=7 no_new_kappa +``` + +The script uses the standard library only. It checks the presentation, +associativity, the unique order-2 element, the augmentation dimensions, the +28-idempotent scan of all \(512\) matrices, call inverses, and the frontiers. +Seven controls are required: \(\operatorname{diag}([x]^3)\) and +\(\operatorname{diag}([y]^3)\) at length 3, the two-role square +\(\operatorname{diag}([x^2],[x^2],[e])\) at length 4, one role of \(x^4\) at +length 2, a dropped call failing on the dirty state +\(([x^5],[y],[x^2]+[y])\), an \(x\)-for-\(y\) substitution failing, and the +false relation \(y^2=e\) making the central witness fail. The rank-2 matrix +\(E_{00}+E_{11}\) is not admitted. + +Recorded environment: CPython 3.12.3, `g++` 13.3.0 with `/usr/bin/c++` pointing +at `/usr/bin/g++`, `libboost-dev` 1.83.0.1ubuntu2, and +`research/e8-bit-p111-tuned/requirements.txt` already satisfied by a +`python3 -m pip install --user` run. This package imports none of those +libraries. + +Not run: `make frontier1094-verify`, the three-register C++ replay, a +four-role search, and lengths 8, 10 and 12 except for the explicit length-12 +upper word. Odd lengths 7, 9 and 11 are excluded by the parity argument, not +by enumeration. + +## Open next questions + +1. Is the minimum of \(\operatorname{diag}([x^6]^3)\) equal to 8, 10, or 12? + A value below the disjoint bill of 12 would be a real mixing saving in + this alphabet. First step: meet in the middle at length 8 on the depth-4 + frontier. That frontier was not built; depth 3 already has 92374 matrices. +2. Can one restored scratch role realize + \(\operatorname{diag}([x^4],[x^4],[x^4],[e])\) in fewer than 6 calls? + A scratch role is the usual route past a three-role disjoint bill. First + step: shortest-path search to depth 3 on the four-role alphabet of both + generators and every rank-one idempotent in \(M_4(\mathbb F_2)\). That + alphabet was not built. + +## Credit + +Predecessor model: the scalar-idempotent calls in +`research/bit-three-register-lower-bound`, from eumemic's pinned PR #288. +Discussion comment +[18926868](https://github.com/CrocSwap/integer-mult-bounds/discussions/1167#discussioncomment-18926868) +records the same presentation and releases a two-role schedule: \(x^4=y^2\), +so two copies cost 4 by the direct word, not an assumed 8. That note does +not determine the three-role minimum. The \(Q_8\) central-pair claims are the +order-8 group. The semidihedral triple-square certificate uses +\(srs=r^3\) and \(s^2=e\); its frontiers are 2051 and 68899, not these. +Apache-2.0. + +Substantial AI assistance was used to build the multiplication table, search +the paid words, and write these notes. + +Discussion writes for this account return FORBIDDEN / Resource not accessible +by integration. No claim was posted, and the write was not retried. + +Base commit `ef5f39403610d231a0c27e8a6b4f08c10209bcd6`. Selector nonce +`bfe60b39ce1400e38d330c639d8e904a`, card `bit-new-register-model`, scope key +`7084092dd726e7ba1f2f`, priority revision 2. diff --git a/research/q16-central-square/SOURCES.json b/research/q16-central-square/SOURCES.json new file mode 100644 index 0000000000..e3b8c42512 --- /dev/null +++ b/research/q16-central-square/SOURCES.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "base_commit": "ef5f39403610d231a0c27e8a6b4f08c10209bcd6", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "c05fafaa25ba95b2d5af86b1800427198e3d20eb", + "sha256": "89b5928bc92c81e2647b6d702a7ad85a6795b8f44e2eb267b2ff3145d8f2b2ce" + } + ] +} diff --git a/research/q16-central-square/TASK.json b/research/q16-central-square/TASK.json new file mode 100644 index 0000000000..12266d8f33 --- /dev/null +++ b/research/q16-central-square/TASK.json @@ -0,0 +1,66 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "priority_revision": 2, + "base_commit": "ef5f39403610d231a0c27e8a6b4f08c10209bcd6", + "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" + ], + "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": "Write a complete operation alphabet outside one named premise and price a baseline before searching identities.", + "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." + ], + "overlap_terms": [ + "three-register", + "nonabelian", + "group algebra" + ] + }, + "scope_status": "refined", + "actual_scope": "In F2[Q16] on exactly three roles, with paid labels {x,y} and all 28 binary rank-one idempotents, the minimum word lengths of diag([x^2]^3) and diag([x^4]^3) are both 6.", + "scope_change_reason": "The card allows one specified nonabelian family. The family is the generalized quaternion group of order 16 with relations x^8=e, y^2=x^4 and yxy^{-1}=x^{-1}, charged generators {x,y}, three output roles, and these two triple-square targets. The abelian M3(Q) three-register model is not reused.", + "bottleneck_link": "The complex primitive binds, and both identities meet rather than undercut the disjoint bill of 6, so selected kappa is unchanged. The degree-1 relaxation only forces even length and does not decide the targets. This prices a nonabelian generator alphabet outside the three-register obstruction.", + "budget_minutes": 60, + "stop_rule": "Stop once both triple squares have an exact minimum. Do not open a four-role search or a length-8 search for diag([x^6]^3), and do not claim a new kappa.", + "outcome": "negative-result", + "evidence": "Selector nonce bfe60b39ce1400e38d330c639d8e904a, scope key 7084092dd726e7ba1f2f. Verifier PASS_Q16_CENTRAL_SQUARE: frontiers 2352 and 92374; both minima 6; 799 length-6 prefix matrices for each square, 792 of the central prefixes nondiagonal; x^6 absent through length 6 with upper bound 12. No new kappa. Discussion writes are forbidden for this account and were not retried.", + "author": "AI-assisted contributor", + "ai_assistance": "Substantial AI assistance was used to build the quaternion multiplication table, search the paid words, and write the package notes.", + "open_questions": [ + { + "question": "Is the minimum length of diag([x^6],[x^6],[x^6]) equal to 8, 10, or 12 in this same three-role alphabet?", + "why_it_matters": "A length below the disjoint bill of 12 would be a genuine mixing saving. The parity lemma and the length-6 sieve only leave those three candidates.", + "first_step": "Meet in the middle at length 8 using the depth-4 frontier obtained by extending the 92374 length-3 matrices by one call.", + "blocked_by": "The depth-4 frontier was not built or stored in this run." + }, + { + "question": "Can diag([x^4],[x^4],[x^4],[e]) be realized with labels {x,y} and all rank-one idempotents in M4(F2) in fewer than 6 calls?", + "why_it_matters": "A restored scratch role is the usual route past a three-role disjoint bill. This package only rules out savings with exactly three roles.", + "first_step": "Run a shortest-path search to depth 3 on the four-role generator alphabet.", + "blocked_by": "That four-role alphabet and frontier were not built in this run." + } + ] +} diff --git a/research/q16-central-square/VERIFY.json b/research/q16-central-square/VERIFY.json new file mode 100644 index 0000000000..c8dd660fb8 --- /dev/null +++ b/research/q16-central-square/VERIFY.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "Q16 presentation and unique central involution; all 28 rank-one idempotents; augmentation dimensions; exhaustive absence of words of length at most 5 for both triple squares; length-6 coordinate witnesses; x^6 sieve through length 6 and the length-12 word; seven positive and negative controls." + } + ] +} diff --git a/research/q16-central-square/verify.py b/research/q16-central-square/verify.py new file mode 100644 index 0000000000..9ee1678e18 --- /dev/null +++ b/research/q16-central-square/verify.py @@ -0,0 +1,536 @@ +#!/usr/bin/env python3 +"""Exact three-role lengths in the generator-priced quaternion model. + +Q16 = . +Paid calls are D_N([g]) = I + ([g] + [e]) N for g in {x, y} and every +rank-one idempotent N in M_3(F_2). Equality is in M_3(F_2[Q16]). + +The disjoint bills of diag([x^2]^3) and diag([x^4]^3) are both 6. +Both minima are exactly 6, so register mixing does not undercut them. +""" + +from __future__ import annotations + +X = 1 +Y = 8 +X2 = 2 +X4 = 4 +X6 = 6 + + +def fail(message: str) -> None: + raise SystemExit("FAIL_Q16_CENTRAL_SQUARE " + message) + + +def mul_group(a: int, b: int) -> int: + ak, ae = a & 7, a >> 3 + bk, be = b & 7, b >> 3 + if ae == 0 and be == 0: + return (ak + bk) & 7 + if ae == 0 and be == 1: + return 8 | ((ak + bk) & 7) + if ae == 1 and be == 0: + return 8 | ((ak - bk) & 7) + return (ak - bk + 4) & 7 + + +def mul_group_square_trivial(a: int, b: int) -> int: + """Same generators with the wrong relation y^2 = e.""" + ak, ae = a & 7, a >> 3 + bk, be = b & 7, b >> 3 + if ae == 0 and be == 0: + return (ak + bk) & 7 + if ae == 0 and be == 1: + return 8 | ((ak + bk) & 7) + if ae == 1 and be == 0: + return 8 | ((ak - bk) & 7) + return (ak - bk) & 7 + + +def invert_table(multiply) -> dict[int, int]: + table = {} + for g in range(16): + hits = [h for h in range(16) if multiply(g, h) == 0] + if len(hits) != 1: + fail(f"element {g} does not have a unique right inverse") + table[g] = hits[0] + return table + + +def algebra(multiply): + table = [[multiply(a, b) for b in range(16)] for a in range(16)] + + def amul(p: int, q: int) -> int: + result = 0 + left = p + while left: + i = (left & -left).bit_length() - 1 + left ^= 1 << i + right = q + row = table[i] + while right: + j = (right & -right).bit_length() - 1 + right ^= 1 << j + result ^= 1 << row[j] + return result + + return amul + + +def pack(entries: list[int]) -> int: + value = 0 + for index, entry in enumerate(entries): + value |= (entry & 0xFFFF) << (16 * index) + return value + + +def unpack(value: int) -> list[int]: + return [(value >> (16 * index)) & 0xFFFF for index in range(9)] + + +def make_matmul(amul): + def matmul(left: int, right: int) -> int: + left_entries = unpack(left) + right_entries = unpack(right) + out = [0] * 9 + for i in range(3): + row = left_entries[3 * i : 3 * i + 3] + for j in range(3): + acc = amul(row[0], right_entries[j]) + acc ^= amul(row[1], right_entries[3 + j]) + acc ^= amul(row[2], right_entries[6 + j]) + out[3 * i + j] = acc + return pack(out) + + return matmul + + +def identity() -> int: + return pack([1 if i == j else 0 for i in range(3) for j in range(3)]) + + +def make_call(amul_unused, label: int, projector: int) -> int: + del amul_unused + alpha = (1 << label) ^ 1 + entries = [1 if i == j else 0 for i in range(3) for j in range(3)] + for pos in range(9): + if (projector >> pos) & 1: + entries[pos] ^= alpha + return pack(entries) + + +def f2_mul(left: int, right: int) -> int: + out = 0 + for i in range(3): + for j in range(3): + bit = 0 + for k in range(3): + bit ^= ((left >> (3 * i + k)) & 1) & ((right >> (3 * k + j)) & 1) + out |= bit << (3 * i + j) + return out + + +def f2_rank(matrix: int) -> int: + rows = [((matrix >> (3 * i)) & 7) for i in range(3)] + rank = 0 + for col in range(3): + pivot = next((r for r in range(rank, 3) if (rows[r] >> col) & 1), None) + if pivot is None: + continue + rows[rank], rows[pivot] = rows[pivot], rows[rank] + for r in range(3): + if r != rank and (rows[r] >> col) & 1: + rows[r] ^= rows[rank] + rank += 1 + return rank + + +def f2_trace(matrix: int) -> int: + return ((matrix >> 0) & 1) ^ ((matrix >> 4) & 1) ^ ((matrix >> 8) & 1) + + +def projector_bit(role: int) -> int: + return 1 << (4 * role) + + +def rref(vectors: list[int]) -> list[int]: + rows: list[int] = [] + for vector in vectors: + reduced = vector + for row in rows: + pivot = row.bit_length() - 1 + if (reduced >> pivot) & 1: + reduced ^= row + if reduced: + pivot = reduced.bit_length() - 1 + rows = [row ^ reduced if (row >> pivot) & 1 else row for row in rows] + rows.append(reduced) + return rows + + +def in_space(rows: list[int], vector: int) -> bool: + reduced = vector + for row in rows: + pivot = row.bit_length() - 1 + if (reduced >> pivot) & 1: + reduced ^= row + return reduced == 0 + + +def valuation(powers: list[list[int]], mask: int) -> int: + level = 0 + for rows in powers: + if in_space(rows, mask): + level += 1 + else: + break + return level + + +def check_group() -> dict[int, int]: + for a in range(16): + for b in range(16): + for c in range(16): + if mul_group(mul_group(a, b), c) != mul_group(a, mul_group(b, c)): + fail("Q16 multiplication is not associative") + if any(mul_group(0, g) != g or mul_group(g, 0) != g for g in range(16)): + fail("identity element is not e") + inverses = invert_table(mul_group) + power = 0 + for _ in range(8): + power = mul_group(power, X) + if power != 0: + fail("x^8 is not e") + if mul_group(Y, Y) != X4: + fail("y^2 is not x^4") + if mul_group(mul_group(Y, X), inverses[Y]) != inverses[X]: + fail("y x y^{-1} is not x^{-1}") + if mul_group(Y, X) == mul_group(X, Y): + fail("Q16 collapsed to an abelian group") + orders = [] + for g in range(16): + seen = 0 + order = 0 + while True: + order += 1 + seen = mul_group(seen, g) + if seen == 0: + break + if order > 16: + fail("element order did not close") + orders.append(order) + if orders[X4] != 2 or orders.count(2) != 1: + fail("x^4 is not the unique order-2 element") + if orders[Y] != 4 or orders[X] != 8: + fail("generator orders are not 8 and 4") + reachable = {0} + frontier = [0] + while frontier: + current = frontier.pop() + for step in (X, Y): + nxt = mul_group(current, step) + if nxt not in reachable: + reachable.add(nxt) + frontier.append(nxt) + if reachable != set(range(16)): + fail("generators x and y do not exhaust Q16") + return inverses + + +def group_lengths() -> dict[int, int]: + lengths = {0: 0} + frontier = [0] + while frontier: + current = frontier.pop(0) + if lengths[current] >= 8: + continue + for step in (X, Y): + nxt = mul_group(current, step) + if nxt not in lengths: + lengths[nxt] = lengths[current] + 1 + frontier.append(nxt) + return lengths + + +def augmentation_powers(amul) -> list[list[int]]: + delta = rref([(1 << g) ^ 1 for g in range(1, 16)]) + if len(delta) != 15: + fail("augmentation ideal is not 15-dimensional") + powers = [delta] + current = delta + for _ in range(8): + products = [amul(left, right) for left in current for right in delta] + current = rref(products) + powers.append(current) + if not current: + break + dims = [len(rows) for rows in powers] + if dims != [15, 13, 11, 9, 7, 5, 3, 1, 0]: + fail(f"unexpected augmentation dimensions {dims}") + return powers + + +def idempotents() -> list[int]: + found = [] + for column in range(1, 8): + for row in range(1, 8): + if bin(column & row).count("1") & 1: + matrix = 0 + for i in range(3): + for j in range(3): + if (column >> i) & 1 and (row >> j) & 1: + matrix |= 1 << (3 * i + j) + found.append(matrix) + found = sorted(set(found)) + if len(found) != 28: + fail(f"expected 28 rank-one idempotents, found {len(found)}") + scanned = [] + for matrix in range(512): + if f2_mul(matrix, matrix) == matrix and f2_rank(matrix) == 1: + scanned.append(matrix) + if scanned != found: + fail("rank-one idempotent scan does not match the xy^T list") + for matrix in found: + if f2_trace(matrix) != 1: + fail("a rank-one idempotent has trace other than 1") + rank_two = projector_bit(0) | projector_bit(1) + if f2_rank(rank_two) != 2 or rank_two in found: + fail("rank-2 matrix E00+E11 was admitted as a rank-one idempotent") + return found + + +def target_matrix(diags: tuple[int, int, int]) -> int: + entries = [1 if i == j else 0 for i in range(3) for j in range(3)] + for role, element in enumerate(diags): + entries[3 * role + role] = 1 << element + return pack(entries) + + +def apply_word(matmul, factors: list[int], state: int) -> int: + for factor in factors: + state = matmul(state, factor) + return state + + +def invert_word(matmul, inverse_factors: list[int], word: tuple[int, ...], state: int) -> int: + # A = C_i C_j means A^{-1} = C_j^{-1} C_i^{-1}. Left-multiplying the inverse + # factors in forward word order composes to that product. + for index in word: + state = matmul(inverse_factors[index], state) + return state + + +def build_layers(matmul, factors: list[int], inverse_factors: list[int], eye: int): + for index, factor in enumerate(factors): + if matmul(factor, inverse_factors[index]) != eye or matmul(inverse_factors[index], factor) != eye: + fail("a paid call is not inverted by the inverse label") + layer2: dict[int, tuple[int, int]] = {} + for i, left in enumerate(factors): + for j, right in enumerate(factors): + product = matmul(left, right) + layer2.setdefault(product, (i, j)) + for matrix, word in layer2.items(): + if invert_word(matmul, inverse_factors, word, matrix) != eye: + fail("length-2 inverse word does not recover I") + rebuilt = apply_word(matmul, [factors[index] for index in word], eye) + if rebuilt != matrix: + fail("stored length-2 word does not rebuild its matrix") + layer3: dict[int, tuple[int, int, int]] = {} + for prefix, (i, j) in layer2.items(): + for k, factor in enumerate(factors): + product = matmul(prefix, factor) + layer3.setdefault(product, (i, j, k)) + for matrix, word in layer3.items(): + if invert_word(matmul, inverse_factors, word, matrix) != eye: + fail("length-3 inverse word does not recover I") + return layer2, layer3 + + +def shortest(matmul, factors, inverse_factors, layer2, layer3, diags: tuple[int, int, int], limit: int): + eye = identity() + target = target_matrix(diags) + if target == eye: + return 0 + for index, factor in enumerate(factors): + if factor == target: + return 1 + if limit >= 2 and target in layer2: + return 2 + if limit >= 3 and target in layer3: + return 3 + if limit >= 4: + for matrix, word in layer2.items(): + if invert_word(matmul, inverse_factors, word, target) in layer2: + return 4 + if limit >= 5: + for matrix, word in layer2.items(): + if invert_word(matmul, inverse_factors, word, target) in layer3: + return 5 + if limit >= 6: + for matrix, word in layer3.items(): + if invert_word(matmul, inverse_factors, word, target) in layer3: + return 6 + return None + + +def hit_count(matmul, inverse_factors, layer, diags: tuple[int, int, int]) -> int: + target = target_matrix(diags) + hits = 0 + for word in layer.values(): + if invert_word(matmul, inverse_factors, word, target) in layer: + hits += 1 + return hits + + +def coordinate_word(label: int, repeats: int, roles: tuple[int, ...] = (0, 1, 2)) -> list[tuple[int, int]]: + word = [] + for role in roles: + word.extend((label, projector_bit(role)) for _ in range(repeats)) + return word + + +def realize(call_of, matmul, word: list[tuple[int, int]], eye: int) -> int: + state = eye + for label, projector in word: + state = matmul(state, call_of(label, projector)) + return state + + +def apply_state(amul, matrix: int, vector: tuple[int, int, int]) -> tuple[int, int, int]: + entries = unpack(matrix) + out = [] + for row in range(3): + acc = 0 + for col in range(3): + acc ^= amul(entries[3 * row + col], vector[col]) + out.append(acc) + return tuple(out) + + +def main() -> None: + inverses = check_group() + lengths = group_lengths() + if (lengths[X2], lengths[X4], lengths[X6]) != (2, 2, 4): + fail(f"unexpected generator lengths {lengths[X2], lengths[X4], lengths[X6]}") + amul = algebra(mul_group) + matmul = make_matmul(amul) + powers = augmentation_powers(amul) + expected_values = {X: 1, X2: 2, X4: 4, X6: 2, Y: 1} + for element, expected in expected_values.items(): + got = valuation(powers, (1 << element) ^ 1) + if got != expected: + fail(f"valuation of element {element} is {got}, expected {expected}") + quotient = powers[1] + x_class = (1 << X) ^ 1 + y_class = (1 << Y) ^ 1 + if in_space(quotient, x_class) or in_space(quotient, y_class) or in_space(quotient, x_class ^ y_class): + fail("[x]+1 and [y]+1 are not independent modulo Delta^2") + if len(powers[0]) - len(powers[1]) != 2: + fail("Delta/Delta^2 is not two-dimensional") + for element in (X2, X4, X6): + if not in_space(powers[1], (1 << element) ^ 1): + fail(f"[{element}]+1 is outside Delta^2") + projectors = idempotents() + eye = identity() + factors = [] + inverse_factors = [] + for label in (X, Y): + for projector in projectors: + factors.append(make_call(None, label, projector)) + inverse_factors.append(make_call(None, inverses[label], projector)) + if len(factors) != 56: + fail("alphabet does not have 56 calls") + layer2, layer3 = build_layers(matmul, factors, inverse_factors, eye) + + triple_x2 = (X2, X2, X2) + triple_x4 = (X4, X4, X4) + triple_x6 = (X6, X6, X6) + minima = { + "x": shortest(matmul, factors, inverse_factors, layer2, layer3, (X, X, X), 3), + "y": shortest(matmul, factors, inverse_factors, layer2, layer3, (Y, Y, Y), 3), + "x2": shortest(matmul, factors, inverse_factors, layer2, layer3, triple_x2, 6), + "x4": shortest(matmul, factors, inverse_factors, layer2, layer3, triple_x4, 6), + "x6": shortest(matmul, factors, inverse_factors, layer2, layer3, triple_x6, 6), + "x2_pair": shortest(matmul, factors, inverse_factors, layer2, layer3, (X2, X2, 0), 4), + "one_x4": shortest(matmul, factors, inverse_factors, layer2, layer3, (X4, 0, 0), 2), + } + if minima["x"] != 3 or minima["y"] != 3: + fail(f"generator triples were not found at length 3: {minima['x']}, {minima['y']}") + if minima["x2"] != 6 or minima["x4"] != 6: + fail(f"square minima are {minima['x2']} and {minima['x4']}, not 6") + if minima["x6"] is not None: + fail(f"x^6 triple appeared at length {minima['x6']}") + if minima["x2_pair"] != 4 or minima["one_x4"] != 2: + fail("positive length controls did not meet the disjoint bill") + + len4_hits = hit_count(matmul, inverse_factors, layer2, triple_x4) + len4_x2 = hit_count(matmul, inverse_factors, layer2, triple_x2) + len6_x4 = hit_count(matmul, inverse_factors, layer3, triple_x4) + len6_x2 = hit_count(matmul, inverse_factors, layer3, triple_x2) + len6_x6 = hit_count(matmul, inverse_factors, layer3, triple_x6) + if len4_hits != 0 or len4_x2 != 0 or len6_x6 != 0 or len6_x4 <= 0 or len6_x2 <= 0: + fail( + f"hit counts len4_x2={len4_x2} len4_x4={len4_hits} len6_x2={len6_x2} " + f"len6_x4={len6_x4} len6_x6={len6_x6}" + ) + diagonal = {projector_bit(role) for role in range(3)} + pure_y = nondiagonal = 0 + central = target_matrix(triple_x4) + for word in layer3.values(): + if invert_word(matmul, inverse_factors, word, central) not in layer3: + continue + if any(index // 28 != 1 for index in word): + fail("central length-6 prefix used an x call") + pure_y += 1 + if any(projectors[index % 28] not in diagonal for index in word): + nondiagonal += 1 + if pure_y != len6_x4 or nondiagonal != 792: + fail(f"central prefix profile pure_y={pure_y} nondiagonal={nondiagonal}") + + call_of = lambda label, projector: make_call(None, label, projector) + x4_word = coordinate_word(Y, 2) + x2_word = coordinate_word(X, 2) + x6_word = [] + for role in (0, 1, 2): + x6_word.extend((X, projector_bit(role)) for _ in range(2)) + x6_word.extend((Y, projector_bit(role)) for _ in range(2)) + if realize(call_of, matmul, x4_word, eye) != target_matrix(triple_x4): + fail("doubled y coordinate word missed diag([x^4]^3)") + if realize(call_of, matmul, x2_word, eye) != target_matrix(triple_x2): + fail("doubled x coordinate word missed diag([x^2]^3)") + if len(x6_word) != 12 or realize(call_of, matmul, x6_word, eye) != target_matrix(triple_x6): + fail("length-12 xxyy word missed diag([x^6]^3)") + + dirty = ((1 << 5), (1 << Y), (1 << X2) ^ (1 << Y)) + image = apply_state(amul, target_matrix(triple_x4), dirty) + if apply_state(amul, realize(call_of, matmul, x4_word, eye), dirty) != image: + fail("operator witness disagrees on the dirty state") + dropped = realize(call_of, matmul, x4_word[:-1], eye) + if dropped == target_matrix(triple_x4) or apply_state(amul, dropped, dirty) == image: + fail("dropped call still matched the central target") + swapped = list(x4_word) + swapped[0] = (X, swapped[0][1]) + if realize(call_of, matmul, swapped, eye) == target_matrix(triple_x4): + fail("replacing a y call by x still matched the central target") + + broken_amul = algebra(mul_group_square_trivial) + broken_matmul = make_matmul(broken_amul) + if mul_group_square_trivial(Y, Y) != 0: + fail("control relation y^2=e was not installed") + broken_call = lambda label, projector: make_call(None, label, projector) + if realize(broken_call, broken_matmul, x4_word, eye) == target_matrix(triple_x4): + fail("breaking y^2=x^4 still produced the central target") + + controls = 7 + print( + "PASS_Q16_CENTRAL_SQUARE " + f"x2=6 x4=6 x6_through6=0 x6_upper=12 " + f"idempotents=28 calls=56 frontier2={len(layer2)} frontier3={len(layer3)} " + f"len4=0 len6_x2={len6_x2} len6_x4={len6_x4} len6_x6=0 " + f"central_nondiagonal_prefixes={nondiagonal} " + f"group_lengths=2,2,4 controls={controls} no_new_kappa" + ) + + +if __name__ == "__main__": + main()