From 51d72c1563beff5a49cd796f77da45e23384d497 Mon Sep 17 00:00:00 2001 From: juper997 <149030977+juper997@users.noreply.github.com> Date: Wed, 14 Oct 2026 08:10:12 +0700 Subject: [PATCH 1/2] Register scoped UT3 commutator research replay --- .../ut3-commutator-register-bound/VERIFY.json | 21 +++++++++++++++++++ 1 file changed, 21 insertions(+) create mode 100644 research/ut3-commutator-register-bound/VERIFY.json diff --git a/research/ut3-commutator-register-bound/VERIFY.json b/research/ut3-commutator-register-bound/VERIFY.json new file mode 100644 index 0000000000..01246bf9c7 --- /dev/null +++ b/research/ut3-commutator-register-bound/VERIFY.json @@ -0,0 +1,21 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/bit-three-register-lower-bound/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Complete formal and independently implemented faithful-regular radius-three censuses; parity checks, eight-call witness, 37 controls and receipt comparison." + } + ] +} From b30fdba48f3db70e3589ba740b0782b56ec0ba2e Mon Sep 17 00:00:00 2001 From: juper997 <149030977+juper997@users.noreply.github.com> Date: Wed, 14 Oct 2026 08:17:04 +0700 Subject: [PATCH 2/2] Certify eight-call UT3 commutator boundary for two and three registers Exact formal and faithful-regular censuses agree on all states. Includes parity proof, eight-call witnesses, 37 controls, source pins, scoped limitations and predecessor credit. Prepared with substantial OpenAI Codex assistance. --- .../EXPECTED.json | 25 ++ .../ut3-commutator-register-bound/README.md | 171 +++++++++++++ .../SOURCES.json | 24 ++ .../ut3-commutator-register-bound/TASK.json | 69 ++++++ .../VALIDATION.md | 33 +++ .../independent.py | 118 +++++++++ .../ut3-commutator-register-bound/verify.py | 224 ++++++++++++++++++ 7 files changed, 664 insertions(+) create mode 100644 research/ut3-commutator-register-bound/EXPECTED.json create mode 100644 research/ut3-commutator-register-bound/README.md create mode 100644 research/ut3-commutator-register-bound/SOURCES.json create mode 100644 research/ut3-commutator-register-bound/TASK.json create mode 100644 research/ut3-commutator-register-bound/VALIDATION.md create mode 100644 research/ut3-commutator-register-bound/independent.py create mode 100644 research/ut3-commutator-register-bound/verify.py diff --git a/research/ut3-commutator-register-bound/EXPECTED.json b/research/ut3-commutator-register-bound/EXPECTED.json new file mode 100644 index 0000000000..6c9cda2af0 --- /dev/null +++ b/research/ut3-commutator-register-bound/EXPECTED.json @@ -0,0 +1,25 @@ +{ + "controls": 37, + "minimum": 8, + "model": "F2[UT3(F2)]; paid a,b rank-one scalar idempotents", + "registers": { + "2": { + "ball_size": 565, + "generators": 12, + "independent_transition_attempts": 1116, + "layers": [1, 12, 80, 472], + "single_target_minimum": 4, + "state_sha256": "fee0c4d6f7c2450af5c06258d0a6a24dc56709aea24c16c128aae64bec44da85", + "target_intersection": 0 + }, + "3": { + "ball_size": 47231, + "generators": 56, + "independent_transition_attempts": 101192, + "layers": [1, 56, 1750, 45424], + "single_target_minimum": 4, + "state_sha256": "2d66bf31796711244a41efc678d433da22b9ee110855ec00d21c34c332f54de5", + "target_intersection": 0 + } + } +} diff --git a/research/ut3-commutator-register-bound/README.md b/research/ut3-commutator-register-bound/README.md new file mode 100644 index 0000000000..26af5fcb94 --- /dev/null +++ b/research/ut3-commutator-register-bound/README.md @@ -0,0 +1,171 @@ +# Two UT3 commutators require eight paid calls with at most one dirty extra + +**Scoped computer-assisted result; no new kappa.** In the formal model below, +the exact cost of `diag([c],[c])` and `diag([c],[c],1)` is eight. Free scalar +register mixing and one arbitrary restored dirty register do not improve the +direct four-plus-four construction. This answers one three-dimensional instance +of the restricted-coordinate-alphabet question in Gareth Davidson's +[PR1333](https://github.com/CrocSwap/integer-mult-bounds/pull/1333) and the second +open question of commdata2338's +[PR1414](https://github.com/CrocSwap/integer-mult-bounds/pull/1414). + +This is a finite formal-algebra boundary result, not an admitted multiplication +supplier. The address alphabet is different from the rational additive frames +of the root three-register theorem. No rational frame entry is reduced modulo two. + +## Model and complete bill + +Let `G=UT_3(F2)` consist of upper unitriangular three-by-three binary matrices. +Write an element as `(x,y,z)` for entries `01,12,02`. Its product is +`(x,y,z)(X,Y,Z)=(x+X,y+Y,z+Z+xY)` over F2. Set + +```text +a = I+E01, b = I+E12, c = abab = I+E02. +``` + +The group has eight elements; a and b are involutions and c is a central +involution. Work in the **full formal group algebra** `R=F2[G]`. For exactly +`r=2` or `r=3` registers, each paid unit is + +```text +D_N(g) = I + ([g]+1)N, g in {a,b}, +N = xy^T over F2, x,y nonzero, y^T x = 1. +``` + +All scalar `GL_r(F2)` changes are free. There are no additional free address +maps, clean allocations, copies, erasures, higher-rank paid calls or free undo +operations. The endpoint is equality of every formal coefficient to +`T_r=diag([c],[c],1,...,1)` on arbitrary inputs; the third role, when present, +must be returned identically. The direct word uses `(a,b,a,b)` on the first +coordinate projector followed by the same four labels on the second. Its +complete bill is eight paid calls, two data roles and zero or one dirty extra, +with no scalar mixing needed. Both engines check this word exactly. + +Free scalar normalization uses PR1333's augmentation argument: move all scalar +maps to one end, conjugating each projector as necessary. Augmentation sends +every paid factor and the target to I, so the remaining scalar map must be I. +Conversely, every binary rank-one idempotent is conjugate to a coordinate +projector (use its image and kernel as a basis). Thus the enumerated alphabet +covers all allowed interleaved scalar mixing. + +## Lower-bound argument and exhaustive coverage + +**Parity lemma (any finite register count).** The character `chi(x,y,z)=x+y` +is a homomorphism `G -> C2`, with a,b sent to its generator t and c to 1. +In `F2[C2]=F2[epsilon]/(epsilon^2)`, t=1+epsilon. The image of a paid factor +is `I+epsilon N`. By the rank-one determinant lemma its determinant is +`1+epsilon trace(N)=1+epsilon`, since `trace(xy^T)=y^T x=1`. +The target's image is I, so `(1+epsilon)^k=1`; k is even. This excludes every +odd length, including seven. This parity statement alone is not an eight-call +lower bound for arbitrary register count. + +**Finite even-length exclusion (r=2,3 only).** Every generator is involutory, +because `N^2=N` and `g^2=1`. Enumerate the exact radius-three ball `B3` from I, +deduplicating by the complete formal matrix and retaining minimum distance. +Any word of length at most six can be split as `PQ` with both lengths at most +three. If `PQ=T_r`, then `P=T_r Q^{-1}` and hence `B3 intersect T_r B3` is +nonempty. Both enumerations find that intersection empty. Together with parity, +this excludes every length below eight. The direct word attains eight. + +| r | Dirty extras | Generators | Distance layers 0,1,2,3 | Ball size | Target intersection | +|---|---|---|---|---|---| +| 2 | 0 | 12 | 1, 12, 80, 472 | 565 | 0 | +| 3 | 1 | 56 | 1, 56, 1750, 45424 | 47231 | 0 | + +The first implementation enumerates all outer products with `y^T x=1`, stores +eight formal coefficients per entry and right-multiplies using the triple +group law. `independent.py` imports none of that implementation: it constructs +three-by-three address matrices, enumerates every binary scalar matrix to find +rank-one idempotents, and multiplies ordinary binary matrices of dimensions 16 +and 24 in the faithful right regular representation. **Entire state sets and +minimum distances agree**, including all 1,116 and 101,192 transition attempts +in the second engine. Faithful decoding also reconstructs each complete regular +matrix, rather than comparing only a natural three-dimensional image. + +`EXPECTED.json` records deterministic receipts. Hashes concatenate the sorted +formal states, each encoded as r*r bytes in row-major order, one eight-bit +coefficient mask per entry; group index is `x+2y+4z`. The hash is a compact +receipt, not a substitute for the full state-by-state comparison. + +The 37 controls include all eight single-call omissions for both register counts, +wrong labels, invalid scalar projectors and expanded address labels, involution +and quotient checks, dirty leakage/restoration faults, and a nonregular matrix +mutation. Identity and a single-commutator target have independently recovered +minima zero and four. A nonzero formal sum of all eight group elements vanishes +in the natural three-by-three representation but survives the regular one: +natural matrix equality cannot certify formal equality here. + +## Reproduce and observed verification + +Python 3.12+ and the standard library suffice. From the repository root: + +```sh +python3 -I -B research/ut3-commutator-register-bound/verify.py +python3 scripts/research_package.py --package research/ut3-commutator-register-bound --check-only +# The registered hook requires Python 3.12: +python3.12 scripts/research_package.py --package research/ut3-commutator-register-bound +``` + +Expected final line: + +```text +PASS_UT3_COMMUTATOR_REGISTER_BOUND minimum=8 registers=2,3 dirty_extras=0,1 no_new_kappa +``` + +`--emit` prints a fresh receipt without modifying files. The replay is read-only +and uses explicit checks under Python's optimized mode. `VALIDATION.md` records +the measured runs, environment, relocation and corruption controls. The generic +hook runs the complete bounded census, with no skipped larger census. + +## Task, sources, overlap and limitations + +Base main: `410026dc5513b87db92ae98571d1d5984c69a983`; task +`bit-new-register-model`, scope key `7084092dd726e7ba1f2f`, priority revision 2, +chooser nonce `d556c3c1fbf3d1a397fbb6604c6f5772`. The broad assignment is refined +to this fixed group, alphabet, target and register count. Claim and updates: +[Discussion1317](https://github.com/CrocSwap/integer-mult-bounds/discussions/1317#discussioncomment-18912406). +`TASK.json` preserves the original card and structured next questions; +`SOURCES.json` pins the base and contextual input. + +Immediate research leads: Gareth Davidson (@bitplane), PR1333 head +`7f25b6d0e1d7e995d4d2840f231d98b1a1a9fec2`; commdata2338, PR1414 head +`9e1640094f649ba6db9742796825a8d6c238989b`. Their S3 coordinate-swap model and +this D8 central-commutator model have different groups and targets. No pending +implementation is imported. The local overlap helper searched 326 records, +with two contextual matches and no usable remote snapshot. Live PR and +Discussion searches were checked at entry and before submission; coverage is +incomplete and no novelty or literature-priority claim is made. + +This does not exclude improvements with two or more extra dirty registers, +different targets, a larger address alphabet, or other primitive prices. It does +not prove a rational-frame identity, physical compiler/hosting feasibility, +precision/tape or analytic transfer, or a new kappa. The full selected-supplier +cold replay was not run. The prescribed orientation baseline was attempted but +could not validate its complete source inventory in this sparse checkout; +large archived supplier inputs are absent. This package consumes no supplier +data and makes no selected-source acceptance claim. The result is not Lean +verification or independent human proof review. + +## Open next questions + +1. **Two additional dirty registers.** Does r=4 admit a six-call word for the + same two targets, or is eight still minimal? This would test whether the + obstruction scales with workspace. First enumerate the 120 rank-one + idempotents and a radius-three ball with packed formal states. The blocker + is a substantially larger census; the present r=3 proof does not imply r=4. +2. **An all-register coefficient obstruction.** Can six paid a/b factors be + excluded without fixing r? This would replace the finite register boundary + with a structural theorem. First classify the 64 length-six label patterns + and derive rank constraints on the c coefficient under the identity of all + other coefficients. Noncommuting scalar products and cancellations are the + blocker; parity alone is insufficient. + +## Credit and license + +Prepared for @juper997 with substantial OpenAI Codex assistance (research, +implementation, checking and writing). No subagents were used. Credit Gareth +Davidson for the affine/restricted-alphabet question and augmentation +normalization; commdata2338 for the adjacent coordinate-swap investigation and +faithful-census approach; eumemic (PR288), Ali Romman (PR468) and David Govea +(PR720) for the register-model lineage. The root abelian bound and all source +notices remain unchanged. New work is licensed Apache-2.0. diff --git a/research/ut3-commutator-register-bound/SOURCES.json b/research/ut3-commutator-register-bound/SOURCES.json new file mode 100644 index 0000000000..3fdab7c8f8 --- /dev/null +++ b/research/ut3-commutator-register-bound/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "410026dc5513b87db92ae98571d1d5984c69a983", + "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" + }, + { + "path": "research/bit-three-register-lower-bound/README.md", + "usage": "input", + "git_blob": "25e41c370c101a33a6deb978de08b03ed7539b79", + "sha256": "c12b33ef388deece0cbf891505a2ce2c0779a0c3a6cf1f0f7f7039bab59cbebd" + } + ] +} diff --git a/research/ut3-commutator-register-bound/TASK.json b/research/ut3-commutator-register-bound/TASK.json new file mode 100644 index 0000000000..420f29514e --- /dev/null +++ b/research/ut3-commutator-register-bound/TASK.json @@ -0,0 +1,69 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "priority_revision": 2, + "base_commit": "410026dc5513b87db92ae98571d1d5984c69a983", + "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": "Exact paid-call minimum for two central UT3(F2) commutator targets with r=2 or r=3 registers, free scalar mixing and restored dirty extras.", + "scope_change_reason": "Specify the permitted nonabelian binary address model, restricted a/b alphabet, target and finite register domain; no rational frames are reduced modulo two.", + "bottleneck_link": "A scoped model-boundary result on the restricted-coordinate alphabet question; it tests whether scalar mixing and one dirty role lower a fully charged direct bill. It is not an admitted bit supplier.", + "budget_minutes": 60, + "stop_rule": "Complete radius-three censuses for r=2,3 and the parity/witness controls; do not expand to r=4 during this session.", + "outcome": "negative-result", + "evidence": "README proof and two exact full-state censuses with EXPECTED.json receipts; eight-call formal witness; 37 controls.", + "author": "juper997 (substantial OpenAI Codex assistance)", + "ai_assistance": "Substantial OpenAI Codex assistance for research, code, verification and writing; no subagents.", + "open_questions": [ + { + "question": "Does r=4 permit six a/b calls for the same target?", + "why_it_matters": "Tests whether a second dirty extra changes the bound.", + "first_step": "Enumerate all 120 rank-one idempotents and a packed radius-three formal ball.", + "blocked_by": "Larger state census; no inference from the r=3 result." + }, + { + "question": "Can all six-call words be excluded for arbitrary finite r?", + "why_it_matters": "Would replace the finite register boundary by a structural theorem.", + "first_step": "Classify all 64 six-label patterns and derive coefficient-rank constraints.", + "blocked_by": "Noncommuting scalar products and cancellations; parity alone is insufficient." + } + ], + "chooser_nonce": "d556c3c1fbf3d1a397fbb6604c6f5772", + "scope_key": "7084092dd726e7ba1f2f", + "discussion": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1317#discussioncomment-18912406" +} diff --git a/research/ut3-commutator-register-bound/VALIDATION.md b/research/ut3-commutator-register-bound/VALIDATION.md new file mode 100644 index 0000000000..b9e69d505c --- /dev/null +++ b/research/ut3-commutator-register-bound/VALIDATION.md @@ -0,0 +1,33 @@ +# Local verification receipt — 2026-10-14 + +Base: `410026dc5513b87db92ae98571d1d5984c69a983`. +Host: Windows 11, build 26300, x86-64. Standard library only. + +1. Python 3.12.14: `python -B scripts/research_package.py --package + research/ut3-commutator-register-bound` passed metadata/source provenance and + the complete registered replay, ending with `PASS_REGISTERED_RESEARCH_PACKAGE`. +2. Python 3.14.7: copied the eight package files to a different directory and + ran `python -I -O -B verify.py`. The complete replay passed in 28.42 seconds. + SHA256 of every copied input file before/after agreed; no generated files + were created. Explicit predicates remain active with assertions disabled. +3. In that disposable relocated copy only, incremented the r=3 receipt's + `ball_size` by one. The same optimized replay exited 1 with `ValueError: + receipt drift` (23.44 seconds), after recomputing the census. The submitted + package's receipt was never changed. + +Both successful engines compare the full state sets and their minimum +distances, not only the hashes or layer counts. Positive endpoints, empty +two-target intersections, independently recovered single-target minima and +37 boundary/algebra controls passed. Python 3.12 and 3.14 agree on the committed +receipt. These are two implementations written in one Codex session, not +independent human review. + +The initial prescribed `scripts/research_baseline.py` was attempted and failed +the selected-package inventory check because this sparse checkout omits large +frozen supplier inputs. No selected supplier circuit replay or baseline PASS is +claimed. This result has no selected-supplier runtime dependency. + +Hosted Linux CI was not run locally. The opt-in `VERIFY.json` requests the full +bounded replay on Python 3.12 with a 120-second timeout. No historical suites, +physical/compiler/hosting checks, all-register proof, precision/tape audit or +outer analytic transfer were run. The selected frontier remains unchanged. diff --git a/research/ut3-commutator-register-bound/independent.py b/research/ut3-commutator-register-bound/independent.py new file mode 100644 index 0000000000..fb5550dc62 --- /dev/null +++ b/research/ut3-commutator-register-bound/independent.py @@ -0,0 +1,118 @@ +"""Dense faithful-regular census; no primary-engine imports. Apache-2.0.""" +from itertools import product + + +def address_matrix(label): + return (1, label & 1, (label >> 2) & 1, 0, 1, (label >> 1) & 1, 0, 0, 1) + + +def address_product(left, right): + return tuple(sum(left[i * 3 + k] * right[k * 3 + j] for k in range(3)) % 2 + for i in range(3) for j in range(3)) + + +ADDRESSES = [address_matrix(i) for i in range(8)] +PRODUCT = [[ADDRESSES.index(address_product(g, h)) for h in ADDRESSES] for g in ADDRESSES] + + +def multiply_labels(g, h): + return PRODUCT[g][h] + + +def natural_sum(): + return tuple(sum(g[i] for g in ADDRESSES) % 2 for i in range(9)) + + +def binary_product(left, right): + out = [] + for row in left: + result = 0 + while row: + bit = row & -row + result ^= right[bit.bit_length() - 1] + row ^= bit + out.append(result) + return tuple(out) + + +def scalar_projectors(r): + result = [] + for rows in product(range(1 << r), repeat=r): + if len(set(rows) - {0}) == 1 and binary_product(rows, rows) == rows: + result.append(rows) + return result + + +def regular_from_formal(state, r): + result = [] + for i in range(r): + for h in range(8): + row = 0 + for j in range(r): + p = state[i * r + j] + for g in range(8): + if (p >> g) & 1: + row ^= 1 << (8 * j + PRODUCT[h][g]) + result.append(row) + return tuple(result) + + +def decode(matrix, r): + formal = tuple((matrix[8 * i] >> (8 * j)) & 255 for i in range(r) for j in range(r)) + if regular_from_formal(formal, r) != matrix: + raise ValueError("regular matrix left the group-algebra image") + return formal + + +def generator(rows, g): + r = len(rows) + answer = [] + for i in range(r): + for h in range(8): + row = 1 << (8 * i + h) + for j in range(r): + if (rows[i] >> j) & 1: + row ^= (1 << (8 * j + h)) ^ (1 << (8 * j + PRODUCT[h][g])) + answer.append(row) + return tuple(answer) + + +BALLS = {} + + +def census(r): + scalar = scalar_projectors(r) + generators = [generator(rows, g) for rows in scalar for g in (1, 2)] + start = tuple(1 << i for i in range(8 * r)) + seen = {start: 0} + frontier = {start} + attempts = 0 + for depth in range(1, 4): + following = set() + for matrix in frontier: + for gate in generators: + attempts += 1 + result = binary_product(matrix, gate) + if result not in seen: + following.add(result) + seen.update((m, depth) for m in following) + frontier = following + BALLS[r] = seen + decoded = {decode(m, r): d for m, d in seen.items()} + if len(decoded) != len(seen): + raise ValueError("faithful decoding collision") + ids = {sum(row << (i * r) for i, row in enumerate(rows)) for rows in scalar} + return decoded, attempts, ids + + +def meet_distance(r, copies): + formal = tuple((16 if i < copies else 1) if i == j else 0 + for i in range(r) for j in range(r)) + wanted = regular_from_formal(formal, r) + seen = BALLS[r] + values = [] + for matrix, depth in seen.items(): + other = binary_product(wanted, matrix) + if other in seen: + values.append(depth + seen[other]) + return min(values) if values else None diff --git a/research/ut3-commutator-register-bound/verify.py b/research/ut3-commutator-register-bound/verify.py new file mode 100644 index 0000000000..905f73d022 --- /dev/null +++ b/research/ut3-commutator-register-bound/verify.py @@ -0,0 +1,224 @@ +#!/usr/bin/env python3 +"""Exact formal UT3 register census. juper997 / OpenAI Codex; Apache-2.0.""" +import argparse +import hashlib +import importlib.util +import json +from itertools import permutations +from pathlib import Path + +HERE = Path(__file__).resolve().parent + + +def require(ok, message): + if not ok: + raise ValueError(message) + + +def group_mul(g, h): + x, y, z = g & 1, (g >> 1) & 1, (g >> 2) & 1 + X, Y, Z = h & 1, (h >> 1) & 1, (h >> 2) & 1 + return (x ^ X) | ((y ^ Y) << 1) | ((z ^ Z ^ (x & Y)) << 2) + + +def translate(p, g): + return sum(1 << group_mul(h, g) for h in range(8) if (p >> h) & 1) + + +DELTA = {g: tuple(p ^ translate(p, g) for p in range(256)) for g in (1, 2)} + + +def projectors(r): + return [(x, y) for x in range(1, 1 << r) for y in range(1, 1 << r) + if (x & y).bit_count() % 2 == 1] + + +def identity(r): + return tuple(int(i == j) for i in range(r) for j in range(r)) + + +def target(r, copies=2): + return tuple((16 if i < copies else 1) if i == j else 0 + for i in range(r) for j in range(r)) + + +def step(state, r, g, x, y): + require(g in (1, 2), "address label outside the paid alphabet") + require(0 < x < 1 << r and 0 < y < 1 << r and (x & y).bit_count() % 2, + "paid scalar factor is not a rank-one idempotent") + out = list(state) + for i in range(r): + p = 0 + for k in range(r): + if (x >> k) & 1: + p ^= state[i * r + k] + q = DELTA[g][p] + for j in range(r): + if (y >> j) & 1: + out[i * r + j] ^= q + return tuple(out) + + +def ball(r, radius=3): + generators = [(g, x, y) for g in (1, 2) for x, y in projectors(r)] + seen = {identity(r): 0} + frontier = {identity(r)} + for depth in range(1, radius + 1): + following = set() + for state in frontier: + for generator in generators: + result = step(state, r, *generator) + if result not in seen: + following.add(result) + seen.update((s, depth) for s in following) + frontier = following + return seen + + +def left_target(state, r, copies): + # c is central and involutory, so either side's c-translation is the same. + return tuple(translate(state[i * r + j], 4) if i < copies else state[i * r + j] + for i in range(r) for j in range(r)) + + +def meet_distance(states, r, copies): + distances = [d + states[t] for s, d in states.items() + if (t := left_target(s, r, copies)) in states] + return min(distances) if distances else None + + +def witness(r): + return [(g, 1 << i, 1 << i) for i in range(2) for g in (1, 2, 1, 2)] + + +def evaluate(word, r): + state = identity(r) + for generator in word: + state = step(state, r, *generator) + return state + + +def dual_mul(a, b): + # bit 0 = constant, bit 1 = epsilon coefficient; epsilon^2 = 0. + return ((a & 1) & (b & 1)) | ((((a & 1) & (b >> 1)) ^ ((a >> 1) & (b & 1))) << 1) + + +def dual_determinant(matrix, r): + result = 0 + for perm in permutations(range(r)): + term = 1 + for i, j in enumerate(perm): + term = dual_mul(term, matrix[i * r + j]) + result ^= term + return result + + +def controls(independent): + count = 0 + require(group_mul(1, 2) != group_mul(2, 1), "lost noncommutativity") + require(group_mul(group_mul(group_mul(1, 2), 1), 2) == 4, "wrong commutator") + require(all(group_mul(4, g) == group_mul(g, 4) for g in range(8)), "c not central") + count += 3 + chi = lambda g: (g & 1) ^ ((g >> 1) & 1) + require(all(chi(group_mul(g, h)) == (chi(g) ^ chi(h)) + for g in range(8) for h in range(8)), "invalid parity quotient") + count += 1 + for r in (2, 3): + word = witness(r) + wanted = target(r) + require(evaluate(word, r) == wanted, "eight-call formal witness failed") + regular = tuple(1 << i for i in range(8 * r)) + for g, x, y in word: + rows = tuple(y if (x >> i) & 1 else 0 for i in range(r)) + regular = independent.binary_product(regular, independent.generator(rows, g)) + require(regular == independent.regular_from_formal(wanted, r), "independent witness failed") + count += 1 + for i in range(8): + require(evaluate(word[:i] + word[i + 1:], r) != wanted, "omitted call accepted") + count += 1 + wrong = word.copy() + wrong[0] = (2, 1, 1) + require(evaluate(wrong, r) != wanted, "wrong address call accepted") + count += 1 + for g, x, y in [(4, 1, 1), (1, 1, 2)]: + try: + step(identity(r), r, g, x, y) + except ValueError: + count += 1 + else: + raise ValueError("invalid alphabet or nilpotent scalar factor accepted") + for x, y in projectors(r): + matrix = tuple(int(i == j) | ((((x >> i) & 1) & ((y >> j) & 1)) << 1) + for i in range(r) for j in range(r)) + require(dual_determinant(matrix, r) == 3, "odd-length determinant step failed") + for g in (1, 2): + require(evaluate([(g, x, y)] * 2, r) == identity(r), "generator not involutory") + count += 2 + bad = list(target(3)) + bad[2] = 1 + require(tuple(bad) != target(3) and bad[:2] == list(target(3))[:2], "dirty leakage control") + bad = list(target(3)) + bad[8] = 16 + require(tuple(bad) != target(3), "dirty endpoint corruption accepted") + count += 2 + require(independent.natural_sum() == (0,) * 9, "natural kernel fixture failed") + require(independent.regular_from_formal((255,), 1) != (0,) * 8, + "nonfaithful representation used for formal equality") + # A dense matrix mutation outside the regular image must fail decoding. + corrupted = list(independent.regular_from_formal(identity(2), 2)) + corrupted[1] ^= 1 + try: + independent.decode(tuple(corrupted), 2) + except ValueError: + count += 1 + else: + raise ValueError("nonregular matrix mutation accepted") + count += 2 + return count + + +def replay(): + spec = importlib.util.spec_from_file_location("ut3_independent", HERE / "independent.py") + independent = importlib.util.module_from_spec(spec) + spec.loader.exec_module(independent) + require(all(group_mul(g, h) == independent.multiply_labels(g, h) + for g in range(8) for h in range(8)), "group implementations disagree") + report = {"model": "F2[UT3(F2)]; paid a,b rank-one scalar idempotents", + "minimum": 8, "registers": {}, "controls": controls(independent)} + for r in (2, 3): + states = ball(r) + other, attempts, scalar_ids = independent.census(r) + require(states == other, "full state sets or shortest distances disagree") + outer_ids = {sum((((x >> i) & 1) & ((y >> j) & 1)) << (i * r + j) + for i in range(r) for j in range(r)) for x, y in projectors(r)} + require(outer_ids == scalar_ids, "rank-one idempotent alphabets disagree") + require(meet_distance(states, r, 2) is None, "two targets attainable in at most six calls") + require(independent.meet_distance(r, 2) is None, "independent target intersection not empty") + require(meet_distance(states, r, 0) == 0, "identity meet control failed") + require(meet_distance(states, r, 1) == 4, "single-commutator meet control failed") + require(independent.meet_distance(r, 1) == 4, "independent positive intersection failed") + require(all(tuple(p.bit_count() % 2 for p in s) == identity(r) for s in states), + "nonidentity free scalar residue") + digest = hashlib.sha256(b"".join(bytes(s) for s in sorted(states))).hexdigest() + report["registers"][str(r)] = {"generators": 2 * len(projectors(r)), + "layers": [sum(d == k for d in states.values()) for k in range(4)], + "ball_size": len(states), "state_sha256": digest, + "independent_transition_attempts": attempts, "target_intersection": 0, + "single_target_minimum": 4} + return report + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--emit", action="store_true", help="print the computed deterministic receipt") + args = parser.parse_args() + receipt = replay() + if args.emit: + print(json.dumps(receipt, indent=2, sort_keys=True)) + else: + require(receipt == json.loads((HERE / "EXPECTED.json").read_text()), "receipt drift") + print("PASS_UT3_COMMUTATOR_REGISTER_BOUND minimum=8 registers=2,3 dirty_extras=0,1 no_new_kappa") + + +if __name__ == "__main__": + main()