From 91235364f44bc0aaa0babb30b2448c3097cb7f5a Mon Sep 17 00:00:00 2001 From: Cinna Davis <1337isnot1337@users.noreply.github.com> Date: Wed, 14 Oct 2026 21:32:23 -0500 Subject: [PATCH] Research UT3(F4) central commutator sharing --- .../CERTIFICATE.json | 68 +++ .../README.md | 91 +++ .../SOURCES.json | 54 ++ .../TASK.json | 65 ++ .../ut3-f4-central-pair-seedfcd785a2/TASK.md | 15 + .../VERIFY.json | 38 ++ .../verify.py | 563 ++++++++++++++++++ 7 files changed, 894 insertions(+) create mode 100644 research/ut3-f4-central-pair-seedfcd785a2/CERTIFICATE.json create mode 100644 research/ut3-f4-central-pair-seedfcd785a2/README.md create mode 100644 research/ut3-f4-central-pair-seedfcd785a2/SOURCES.json create mode 100644 research/ut3-f4-central-pair-seedfcd785a2/TASK.json create mode 100644 research/ut3-f4-central-pair-seedfcd785a2/TASK.md create mode 100644 research/ut3-f4-central-pair-seedfcd785a2/VERIFY.json create mode 100644 research/ut3-f4-central-pair-seedfcd785a2/verify.py diff --git a/research/ut3-f4-central-pair-seedfcd785a2/CERTIFICATE.json b/research/ut3-f4-central-pair-seedfcd785a2/CERTIFICATE.json new file mode 100644 index 0000000000..a5dce95e87 --- /dev/null +++ b/research/ut3-f4-central-pair-seedfcd785a2/CERTIFICATE.json @@ -0,0 +1,68 @@ +{ + "alphabet_factor_count": 24, + "ball_sha256": "e36fec3f8f374c799dc4a973a56e6948c26b396eae88d980ccc0949a692bfbf3", + "central_targets": { + "Z_1": 16, + "Z_w": 32 + }, + "controls": { + "all_eight_single_deletions_fail": true, + "all_factor_involutions": true, + "direct_pair_positive": true, + "mutated_Z_w_to_Z_w2_fails": true, + "single_commutator_positive": true + }, + "dependent_three_role_block_pivot": { + "all_fourteen_single_deletions_fail": true, + "block_alphabet_size": 56, + "block_family_hit_through_three": false, + "block_family_scope": "concatenations of at most three D_N(Z_1) or D_N(Z_w) blocks, each expanded to four paid source factors", + "central_block_pair_product_checks": 3136, + "direct_coordinate_calls": 14, + "direct_word_full_and_generic_endpoints_match": true, + "four_call_block_endpoint_checks": 56, + "raw_block_sequences_total": 178808, + "raw_ordered_block_sequences_checked_by_depth": [ + 56, + 3136, + 175616 + ], + "target": [ + 16, + 32, + 48 + ] + }, + "direct_pair_word_length": 8, + "distinct_ball_states": 6877, + "distinct_state_layer_sizes": [ + 1, + 24, + 412, + 6440 + ], + "field_polynomial": "w^2+w+1=0", + "group_law": "(a,b,c)(a',b',c')=(a+a',b+b',c+c'+ab')", + "group_order": 64, + "labels": { + "X_1": 1, + "X_w": 2, + "Y_1": 4, + "Y_w": 8 + }, + "layer_sha256": [ + "33679eedd86f9637ab73892a064cdab3d82365cf5063b145affb2272327a6ddc", + "1529586f6030051053c39c1cdd30eeb49b1db0ca5872056600f6c4338f4f6f97", + "b3cdc922678436ab83a6967b11acc88dacc1fc83af7e71d9391e87660566008c", + "44af81e7aaf93307c0f3ede1dfef162b8d2665ab2ffb6a4c71229ff62f197372" + ], + "minimum_pair_word_length": 8, + "model": "F2[UT3(F4)]", + "packed_vs_generic_transitions": 10488, + "parity_lemma": "Every label occurs an even number of times because the target is trivial mod I^2 and each rank-one idempotent has trace one.", + "radius": 3, + "rank_one_idempotent_count": 6, + "raw_words_through_radius": 14425, + "shared_pair_word_through_six": false, + "single_output_positive_word_length": 4 +} diff --git a/research/ut3-f4-central-pair-seedfcd785a2/README.md b/research/ut3-f4-central-pair-seedfcd785a2/README.md new file mode 100644 index 0000000000..c16c8394e0 --- /dev/null +++ b/research/ut3-f4-central-pair-seedfcd785a2/README.md @@ -0,0 +1,91 @@ +# Two independent central commutators still cost eight calls + +**Scoped exact minimum in a new nonabelian address model; no new kappa.** In the full group algebra `F2[UT_3(F_4)]`, two independent central commutator outputs on two arbitrary dirty registers have exact minimum eight paid factors. The direct construction costs eight, the complete exact search excludes every word through six, and an augmentation-ideal parity argument excludes seven. The result tests whether separate commutators can share calls through rank-one register mixing; this target profile has no saving. + +The selected result remains the conditional `kappa = 0.001672660197076918` from #1094. Its complex side binds (`0.001675462676808103...` versus bit `0.001733427039589844...`). This formal word result has no physical supplier mapping and changes no selected primitive budget. + +## Model and construction + +Let `F_4 = F_2[w]/(w^2+w+1)` and write the unitriangular group as + +```text +H = UT_3(F_4) = {(a,b,c): a,b,c in F_4} +(a,b,c)(a',b',c') = (a+a', b+b', c+c'+a b'). +``` + +The group has order 64 and abelianization `F_4 x F_4`, an elementary abelian group of rank four. The four paid labels are + +```text +X_1 = (1,0,0), X_w = (w,0,0), Y_1 = (0,1,0), Y_w = (0,w,0). +``` + +Each label is an involution. Their central commutators include + +```text +Z_1 = [X_1,Y_1] = (0,0,1), +Z_w = [X_w,Y_1] = (0,0,w). +``` + +A paid factor is `D_N(g) = I + ([g]+[e])N`, where `g` is one of those four labels and `N` is any rank-one idempotent in `M_2(F_2)`. There are six such idempotents and 24 paid factors. Every factor costs one call; the identity must hold coefficientwise in all 64 group elements, so it applies to arbitrary dirty register values. + +For `E_11` and `E_22`, the eight-call word + +```text +D_E11(X_1) D_E11(Y_1) D_E11(X_1) D_E11(Y_1) +D_E22(X_w) D_E22(Y_1) D_E22(X_w) D_E22(Y_1) +``` + +is exactly `diag([Z_1],[Z_w])`. Each four-factor block is one central commutator on its coordinate. This is a fully charged upper bound: no call, clean role, copy, frame change or restoration is free in the model. + +## Exact lower bound + +Let `I` be the augmentation ideal of `F_2[H]`. Since `H/[H,H]` has the four paid labels as an `F_2` basis, `I/I^2` has four independent label coordinates. Both central target elements lie in `[H,H]`, so the target matrix is the identity modulo `M_2(I^2)`. + +For a word of paid factors, multiplication modulo `I^2` gives + +```text +I + sum_i ([g_i]+[e]) N_i. +``` + +Independence of the four label coordinates forces `sum_{i:g_i=g} N_i = 0` for each label `g`. Every rank-one idempotent over `F_2` has trace one, so each label occurs an even number of times. Thus every word for this target has even length. The only possible improvement on the eight-call upper bound is therefore a word of length at most six. + +The verifier builds the complete radius-three ball for the 24-factor alphabet, merging only equal exact `2 x 2` matrices over the full group algebra. Its new-state layer sizes are `[1, 24, 412, 6440]`, for 6,877 states total; the 14,425 raw words of lengths zero through three are all represented. For every left state `A`, it computes `A^{-1} target` exactly and checks whether that state lies in the same ball. Since each factor is an involution, any word of length at most six splits into two radius-three words. No match exists. Together with parity and the direct word, this proves the exact minimum eight in this finite model. + +The certificate records the exact state-layer SHA-256 digests. The packed transition implementation is cross-checked against generic group-algebra matrix multiplication on 10,488 transitions. The group law is checked on all 64^3 triples; all six idempotents, all factor inverses, the four-call one-output commutator, and the direct eight-call pair are checked. All eight one-factor deletions of the direct word and a mutation of `Z_w` to `Z_{w^2}` fail their endpoint controls. + +## One bounded pivot: a dependent three-output target + +The central relation `Z_{w^2}=Z_1 Z_w` suggests a separate three-role construction. The direct coordinate bill is 14 calls: four for `Z_1`, four for `Z_w`, and six for `Z_{w^2}` using the composite label `X_{w^2}=X_1 X_w`, which is not a primitive label. + +I tested the specific sharing mechanism that first builds commutators and then combines their rank-one updates. For each rank-one idempotent `N` in `M_3(F_2)`, + +```text +D_N(X_1) D_N(Y_1) D_N(X_1) D_N(Y_1) = D_N(Z_1) +D_N(X_w) D_N(Y_1) D_N(X_w) D_N(Y_1) = D_N(Z_w). +``` + +Each is a fully charged four-call block. The complete ordered family of up to three such blocks has 56 block choices and 178,808 total candidate sequences. Exact multiplication in the central four-element group algebra finds no sequence for `diag([Z_1],[Z_w],[Z_{w^2}])`. This rules out only that block family; it is not a lower bound for arbitrary words of 12 calls or fewer. + +An explicit 14-call control applies the first commutator on role 1, the second on role 2, and +`X_1 X_w Y_1 X_1 X_w Y_1` on role 3. The full group-algebra endpoint matches the target under both the packed engine and generic matrix multiplication. The verifier also checks all 56 four-call block endpoints, 3,136 pairwise block products against full group-algebra multiplication, and all 14 single-factor deletions of the direct word. + +## Reproduce + +From the repository root, standard library only: + +```sh +python3 -I -B research/ut3-f4-central-pair-seedfcd785a2/verify.py +python3 -I -O -B research/ut3-f4-central-pair-seedfcd785a2/verify.py +``` + +Both print `PASS_UT3_F4_CENTRAL_PAIR` and the certificate summary. `CERTIFICATE.json` contains the state counts and exact layer digests. `SOURCES.json` pins the base, selected-result chain and predecessor notes. + +## Scope and attribution + +This is a finite group-algebra result for this exact order-64 group and four-label alphabet: an exact two-role minimum plus a bounded three-role block-family obstruction. All paid matrices use the listed rank-one idempotents; the three-role pivot uses the 28 rank-one idempotents of M3(F2). It changes the address group and commutator geometry from the `Q8` central-pair result by Aaron Wang, while retaining the scalar-idempotent register model descended from eumemic's PR #288 and woklerx's PR #1443. It is distinct from the three-register abelian rational-frame obstruction and the `GL_2(F_2)` mixed-target census. It says nothing about larger alphabets, other groups, a physical bit supplier, or the multiplication exponent. + +## Open next questions + +Can an arbitrary word of at most 12 paid factors realize the dependent central triple `diag([Z_1],[Z_w],[Z_{w^2}])` outside the tested commutator-block family? A witness would reduce the 14-call direct bill. The first step is to derive a quotient bound or a small structured extension that admits noncentral intermediate factors, then screen its complete cost. The blocker is the 112-factor alphabet in `M_3(F_2)` and its larger exact state space. + +Prepared by Cinna Davis with substantial OpenAI Codex assistance. No independent human or proof-assistant review is claimed. Apache-2.0. diff --git a/research/ut3-f4-central-pair-seedfcd785a2/SOURCES.json b/research/ut3-f4-central-pair-seedfcd785a2/SOURCES.json new file mode 100644 index 0000000000..22efe99ed2 --- /dev/null +++ b/research/ut3-f4-central-pair-seedfcd785a2/SOURCES.json @@ -0,0 +1,54 @@ +{ + "schema_version": 1, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "input", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "e8870e5917057d59b730eb14721a778639eca050", + "sha256": "d46eb6d5b3e279428753d770653663fbdf1063e55c255ea073d768f344927ef7" + }, + { + "path": "docs/research/community-batch1099-review.md", + "usage": "input", + "git_blob": "6cb6ec061a071a06a2d18cd4dc3e9a2b05d28099", + "sha256": "7e76d2c38e5fce30587835b7251df1430488ae4dd372611ef69a3f03f476b6cb" + }, + { + "path": "research/bit-gl3-mixed-targets-length10/README.md", + "usage": "input", + "git_blob": "59ac7008af69ffb41e10e6574308d68c33d44c48", + "sha256": "f1f88a618fa998baa2bb5e8bc69c225405b6106b4c0a5646d84c42166cd4aff5" + }, + { + "path": "research/bit-three-register-lower-bound/README.md", + "usage": "input", + "git_blob": "25e41c370c101a33a6deb978de08b03ed7539b79", + "sha256": "c12b33ef388deece0cbf891505a2ce2c0779a0c3a6cf1f0f7f7039bab59cbebd" + }, + { + "path": "research/community-frontier1094-audit/ASSEMBLY.json", + "usage": "input", + "git_blob": "5fd676df060f3b450782fdf5ff5f6beb63a5eeb0", + "sha256": "1122cb3a575f8c788345fc1bf4c108ac7c3250fb81a5988671f5eb04b3ab3045" + }, + { + "path": "research/community-frontier1094-audit/SELECTED-SOURCE.json", + "usage": "input", + "git_blob": "6a75493790b4eff9c4a98051ef8b01d6aad0d5a8", + "sha256": "79b3de5db3dbcb9829789ba58e9e45758926031e2a7d80667a08429d369be53b" + }, + { + "path": "research/q8-central-commutator-pair/README.md", + "usage": "input", + "git_blob": "7a6277dc860ea5440ab39b06160c337f93353357", + "sha256": "ee819ee843e1a93d7d320d02ccd5f47af0d912295de9d9c379ccc22c90093948" + } + ] +} diff --git a/research/ut3-f4-central-pair-seedfcd785a2/TASK.json b/research/ut3-f4-central-pair-seedfcd785a2/TASK.json new file mode 100644 index 0000000000..46909f6cbc --- /dev/null +++ b/research/ut3-f4-central-pair-seedfcd785a2/TASK.json @@ -0,0 +1,65 @@ +{ + "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": "Exact minimum for diag([Z_1],[Z_w]) in F2[UT_3(F_4)] on two dirty roles, plus one bounded constructive pivot testing at most three four-call commutator blocks against the dependent three-role central target diag([Z_1],[Z_w],[Z_{w^2}]).", + "scope_change_reason": "The selected random method was a target-specific relaxation, while this session requires a construction-focused assignment. I used the other constructive method listed on the same card, refining its general nonabelian-model question to a class-two order-64 group with a two-dimensional central commutator subgroup and a fixed two-output target.", + "bottleneck_link": "A shorter exact word would reduce the fully charged local bit-call profile; this formal model has no selected-supplier mapping, so even a saving would remain conditional local evidence.", + "budget_minutes": 60, + "stop_rule": "The exact two-role search stops after the complete radius-three ball. The single pivot stops after all ordered sequences of up to three four-call central commutator blocks are checked; do not infer a bound on arbitrary three-role words or search longer.", + "outcome": "negative-result", + "evidence": "For the two-role target, exact MITM excludes all words through six, the I/I^2 trace lemma excludes seven, and a direct word attains eight. The one bounded pivot enumerates all 178,808 ordered sequences of up to three D_N(Z_1/Z_w) blocks in M3(F2); none reaches the dependent triple, while a 14-call direct word passes full and generic endpoints. Exact state digests and positive/deletion/mutation controls are in CERTIFICATE.json.", + "author": "Cinna Davis", + "ai_assistance": "Substantial OpenAI Codex assistance in mathematical derivation, implementation, verification and writing; no independent human or proof-assistant review.", + "open_questions": [ + { + "question": "Can an arbitrary word of at most 12 paid factors realize diag([Z_1],[Z_w],[Z_{w^2}]) outside the tested commutator-block family?", + "why_it_matters": "A witness would reduce the 14-call direct bill and would test whether noncentral intermediates exploit the F2-linear relation among central commutators.", + "first_step": "Derive a quotient bound or a small structured extension that admits noncentral intermediate factors, then screen its fully charged cost before any broad search.", + "blocked_by": "The 112-factor alphabet in M3(F2) and its larger exact state space; no physical supplier mapping is known." + } + ], + "selected_method": "Construct the smallest exact identity in a newly specified legal operation alphabet.", + "discussion": "https://github.com/CrocSwap/integer-mult-bounds/discussions/2256" +} diff --git a/research/ut3-f4-central-pair-seedfcd785a2/TASK.md b/research/ut3-f4-central-pair-seedfcd785a2/TASK.md new file mode 100644 index 0000000000..26f911dae5 --- /dev/null +++ b/research/ut3-f4-central-pair-seedfcd785a2/TASK.md @@ -0,0 +1,15 @@ +# Cycle AG task card + +- **Task ID:** `bit-new-register-model` +- **Track / accepted selector seed:** `bit-mechanisms` / `fcd785a2bcb2e2eaab8d76cf630ed268` +- **Selector catalogue:** revision 4; SHA-256 `d46eb6d5b3e279428753d770653663fbdf1063e55c255ea073d768f344927ef7` +- **Exact base:** `0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2` +- **Selected record:** SHA-256 `10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32` +- **Scope status:** refined; use the card's exact-construction method and change from a target-specific lower-bound relaxation to a constructive sharing test, as required by this session's construction-only scope. +- **Object:** `H=UT_3(F_4)`, with `F_4=F_2[w]/(w^2+w+1)`. Write elements as `(a,b,c)` with product `(a,b,c)(a',b',c')=(a+a',b+b',c+c'+ab')`. Labels are the four involutions `X_1=(1,0,0)`, `X_w=(w,0,0)`, `Y_1=(0,1,0)`, `Y_w=(0,w,0)`. +- **Question:** In `F_2[H]`, can a word of at most six paid factors `D_N(g)=I+([g]+[e])N`, where `g` is one of those four labels and `N` is any of the six rank-one idempotents of `M_2(F_2)`, equal `diag([Z_1],[Z_w])` on two arbitrary dirty registers? Here `Z_c=(0,0,c)`, `[X_1,Y_1]=Z_1`, and `[X_w,Y_1]=Z_w`. One bounded pivot tests whether the dependent three-role target `diag([Z_1],[Z_w],[Z_{w^2}])` is reachable as a product of at most three four-call `D_N(Z_1)` or `D_N(Z_w)` blocks in `M_3(F_2)`. +- **Changed hypothesis / cost:** Replace the single-central-involution Q8 model with an exponent-two class-two group whose commutator subgroup is a two-dimensional central vector space, and test two independent central outputs. Every factor costs one. Separate four-call commutators give a fully charged eight-call upper bound; a hit through six saves at least two calls (25%). Setup, clean roles, copies, hosting, restoration and precision are unavailable or zero only because the formal word model has no such operations. No physical supplier mapping or kappa change is claimed. +- **Method / stop rule:** Exact meet-in-the-middle over the complete 24-factor alphabet, with both halves of length at most three and exact group-algebra matrix equality. Check every element of the radius-three state ball against the exact target quotient. Stop after complete coverage; no search past length six. If absent, prove all valid words have even length using the augmentation ideal modulo its square, giving exact minimum eight together with the direct word. +- **Overlap:** At 2026-10-15 02:18 UTC the helper covered 482 open PRs and 960 Discussions with complete pagination and no warnings. Search terms `UT3(F4)`, `unitriangular 3x3 F4`, `Heisenberg group order 64`, and `commutator vector` gave zero matches. Adjacent group-word work includes #1999 (binary tetrahedral), #2094 (`UT5(Z)`), #2012 (S3), and the released Cycle AF Q8 work in #2243 / open PR #2248; these differ in group and target profile. The previously named rank-seven COPY handoff in #2198 is covered by open PR #2234; its remaining request is independent review and is outside this assignment. +- **Expected evidence:** Reproducible exact certificate and verifier, direct eight-call pair word and 14-call triple word, one-output four-call control, parity proof, exact 178,808-sequence block census, endpoint mutation/deletion controls, source and predecessor pins, and complete accounting. Package is at this directory. +- **Claim expiry:** 2026-10-15 04:20 UTC. diff --git a/research/ut3-f4-central-pair-seedfcd785a2/VERIFY.json b/research/ut3-f4-central-pair-seedfcd785a2/VERIFY.json new file mode 100644 index 0000000000..df67137752 --- /dev/null +++ b/research/ut3-f4-central-pair-seedfcd785a2/VERIFY.json @@ -0,0 +1,38 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "certificates/selected-result.json", + "docs/research/community-batch1099-review.md", + "research/bit-gl3-mixed-targets-length10/README.md", + "research/bit-three-register-lower-bound/README.md", + "research/community-frontier1094-audit/ASSEMBLY.json", + "research/community-frontier1094-audit/SELECTED-SOURCE.json", + "research/q8-central-commutator-pair/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact radius-three pair-state ball and length-six MITM exclusion; I/I^2 parity support; direct pair and dependent-triple constructions; 24-factor, M2 and M3 idempotent controls; generic multiplication cross-checks; one-to-three-block census; deletion and target-mutation controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact radius-three pair-state ball and length-six MITM exclusion; I/I^2 parity support; direct pair and dependent-triple constructions; 24-factor, M2 and M3 idempotent controls; generic multiplication cross-checks; one-to-three-block census; deletion and target-mutation controls." + } + ] +} diff --git a/research/ut3-f4-central-pair-seedfcd785a2/verify.py b/research/ut3-f4-central-pair-seedfcd785a2/verify.py new file mode 100644 index 0000000000..e70507e131 --- /dev/null +++ b/research/ut3-f4-central-pair-seedfcd785a2/verify.py @@ -0,0 +1,563 @@ +#!/usr/bin/env python3 +"""Exact radius-six search for two central commutators in UT_3(F_4).""" +from __future__ import annotations + +import argparse +import hashlib +import json +from pathlib import Path + +ROOT = Path(__file__).resolve().parents[2] +PACKAGE = Path(__file__).resolve().parent + + +def need(condition: bool, message: str) -> None: + if not condition: + raise RuntimeError(message) + + +def f4_mul(a: int, b: int) -> int: + """Multiply two F4 elements in the basis (1,w), w^2+w+1=0.""" + poly = 0 + for i in range(2): + if (a >> i) & 1: + poly ^= b << i + if poly & 4: + poly ^= 7 + return poly + + +F4_MUL = tuple(tuple(f4_mul(a, b) for b in range(4)) for a in range(4)) + + +def gid(a: int, b: int, c: int) -> int: + return a | (b << 2) | (c << 4) + + +def coords(g: int) -> tuple[int, int, int]: + return g & 3, (g >> 2) & 3, (g >> 4) & 3 + + +def gmul(g: int, h: int) -> int: + a, b, c = coords(g) + aa, bb, cc = coords(h) + return gid(a ^ aa, b ^ bb, c ^ cc ^ F4_MUL[a][bb]) + + +GROUP_MUL = tuple(tuple(gmul(g, h) for h in range(64)) for g in range(64)) +E = gid(0, 0, 0) +X1 = gid(1, 0, 0) +XW = gid(2, 0, 0) +Y1 = gid(0, 1, 0) +YW = gid(0, 2, 0) +Z1 = gid(0, 0, 1) +ZW = gid(0, 0, 2) +ZW2 = gid(0, 0, 3) +LABELS = (X1, XW, Y1, YW) +LABEL_NAMES = ("X_1", "X_w", "Y_1", "Y_w") + + +def idempotents() -> tuple[tuple[int, int, int, int], ...]: + out = set() + for u in range(1, 4): + for v in range(1, 4): + dot = (((u >> 0) & 1) & ((v >> 0) & 1)) ^ (((u >> 1) & 1) & ((v >> 1) & 1)) + if dot: + u0, u1 = u & 1, (u >> 1) & 1 + v0, v1 = v & 1, (v >> 1) & 1 + out.add((u0 * v0, u0 * v1, u1 * v0, u1 * v1)) + return tuple(sorted(out)) + + +IDEMPOTENTS = idempotents() +IDENTITY = (1 << E, 0, 0, 1 << E) + + +def idempotents3() -> tuple[tuple[int, ...], ...]: + out = set() + for u in range(1, 8): + for v in range(1, 8): + if (u & v).bit_count() % 2: + out.add(tuple(((u >> i) & 1) * ((v >> j) & 1) + for i in range(3) for j in range(3))) + return tuple(sorted(out)) + + +IDEMPOTENTS3 = idempotents3() +IDENTITY3 = tuple((1 << E) if row == col else 0 + for row in range(3) for col in range(3)) +CENTER = (E, Z1, ZW, ZW2) + + +def build_shift_tables() -> dict[int, tuple[tuple[int, ...], ...]]: + result = {} + for g in set(LABELS) | {E, Z1, ZW, ZW2}: + chunks = [] + for chunk in range(8): + table = [] + for byte in range(256): + image = 0 + for bit in range(8): + if (byte >> bit) & 1: + image |= 1 << GROUP_MUL[chunk * 8 + bit][g] + table.append(image) + chunks.append(tuple(table)) + result[g] = tuple(chunks) + return result + + +SHIFT_TABLES = build_shift_tables() + + +def shift(mask: int, g: int) -> int: + table = SHIFT_TABLES[g] + out = 0 + for chunk in range(8): + out |= table[chunk][(mask >> (8 * chunk)) & 255] + return out + + +# A factor code is 6 * label_index + idempotent_index. +FACTORS = tuple((label_i, idem_i) for label_i in range(4) for idem_i in range(6)) + + +def step(matrix: tuple[int, int, int, int], code: int) -> tuple[int, int, int, int]: + label_i, idem_i = FACTORS[code] + g = LABELS[label_i] + n = IDEMPOTENTS[idem_i] + out = [] + for row in range(2): + for col in range(2): + value = matrix[2 * row + col] + for k in range(2): + if n[2 * k + col]: + entry = matrix[2 * row + k] + value ^= shift(entry, g) ^ entry + out.append(value) + return tuple(out) # type: ignore[return-value] + + +def factor_matrix(code: int) -> tuple[int, int, int, int]: + label_i, idem_i = FACTORS[code] + g = LABELS[label_i] + n = IDEMPOTENTS[idem_i] + gp = (1 << E) | (1 << g) + return tuple( + ((1 << E) if i == j else 0) ^ (gp if n[2 * i + j] else 0) + for i in range(2) for j in range(2) + ) # type: ignore[return-value] + + +def ring_mul_generic(left: int, right: int) -> int: + out = 0 + a = left + while a: + bit_a = a & -a + i = bit_a.bit_length() - 1 + a ^= bit_a + b = right + while b: + bit_b = b & -b + j = bit_b.bit_length() - 1 + b ^= bit_b + out ^= 1 << GROUP_MUL[i][j] + return out + + +def matrix_mul_generic(a: tuple[int, int, int, int], b: tuple[int, int, int, int]) -> tuple[int, int, int, int]: + return tuple( + ring_mul_generic(a[2 * row], b[col]) ^ ring_mul_generic(a[2 * row + 1], b[2 + col]) + for row in range(2) for col in range(2) + ) # type: ignore[return-value] + + +def product(word: tuple[int, ...] | list[int]) -> tuple[int, int, int, int]: + matrix = IDENTITY + for code in word: + matrix = step(matrix, code) + return matrix + + +def target(z_left: int = Z1, z_right: int = ZW) -> tuple[int, int, int, int]: + return (1 << z_left, 0, 0, 1 << z_right) + + +def direct_word() -> tuple[int, ...]: + e11 = IDEMPOTENTS.index((1, 0, 0, 0)) + e22 = IDEMPOTENTS.index((0, 0, 0, 1)) + code = lambda label, idem: 6 * LABELS.index(label) + idem + return ( + code(X1, e11), code(Y1, e11), code(X1, e11), code(Y1, e11), + code(XW, e22), code(Y1, e22), code(XW, e22), code(Y1, e22), + ) + + +def single_word() -> tuple[int, ...]: + e11 = IDEMPOTENTS.index((1, 0, 0, 0)) + return tuple(6 * LABELS.index(g) + e11 for g in (X1, Y1, X1, Y1)) + + +def build_ball(radius: int = 3): + words = {IDENTITY: ()} + frontier = [IDENTITY] + layers = [1] + layer_digests = [matrix_digest(frontier)] + for _depth in range(1, radius + 1): + next_frontier = [] + for state in frontier: + prefix = words[state] + for code in range(len(FACTORS)): + successor = step(state, code) + if successor not in words: + words[successor] = prefix + (code,) + next_frontier.append(successor) + layers.append(len(next_frontier)) + layer_digests.append(matrix_digest(next_frontier)) + frontier = next_frontier + return words, layers, layer_digests + + +def matrix_digest(states) -> str: + digest = hashlib.sha256() + for state in sorted(states): + for coefficient in state: + digest.update(coefficient.to_bytes(8, "little")) + return digest.hexdigest() + + +def required_right(left_inverse: tuple[int, int, int, int], wanted: tuple[int, int, int, int]): + # wanted is diagonal with one group element in each diagonal slot. + left_z = wanted[0].bit_length() - 1 + right_z = wanted[3].bit_length() - 1 + return ( + shift(left_inverse[0], left_z), shift(left_inverse[1], right_z), + shift(left_inverse[2], left_z), shift(left_inverse[3], right_z), + ) + + +def find_within_six(wanted, words): + for left, left_word in words.items(): + inverse = product(tuple(reversed(left_word))) + need_right = required_right(inverse, wanted) + right_word = words.get(need_right) + if right_word is not None: + witness = left_word + right_word + need(product(witness) == wanted, "meet-in-the-middle witness failed exact endpoint") + return witness + return None + + +def group_checks() -> None: + need(len({GROUP_MUL[g][h] for g in range(64) for h in range(64)}) == 64, + "group product table does not cover all encoded elements") + for a in range(64): + need(GROUP_MUL[E][a] == a and GROUP_MUL[a][E] == a, "bad group identity") + for b in range(64): + for c in range(64): + need(GROUP_MUL[GROUP_MUL[a][b]][c] == GROUP_MUL[a][GROUP_MUL[b][c]], + "UT3(F4) multiplication is not associative") + need(len(IDEMPOTENTS) == 6, "wrong rank-one idempotent count") + for n in IDEMPOTENTS: + a, b, c, d = n + need((a ^ (b & c), (a & b) ^ (b & d), (c & a) ^ (d & c), (c & b) ^ d) == n, + "listed matrix is not idempotent") + need(a ^ d == 1, "rank-one idempotent does not have trace one") + for g in LABELS: + need(GROUP_MUL[g][g] == E, "label is not an involution") + need(GROUP_MUL[GROUP_MUL[X1][Y1]][GROUP_MUL[X1][Y1]] == Z1, + "[X_1,Y_1] is not Z_1") + need(GROUP_MUL[GROUP_MUL[XW][Y1]][GROUP_MUL[XW][Y1]] == ZW, + "[X_w,Y_1] is not Z_w") + reachable = {E} + frontier = [E] + while frontier: + next_frontier = [] + for state in frontier: + for label in LABELS: + successor = GROUP_MUL[state][label] + if successor not in reachable: + reachable.add(successor) + next_frontier.append(successor) + frontier = next_frontier + need(len(reachable) == 64, "four paid labels do not generate all of UT_3(F_4)") + need(len({E, Z1, ZW, ZW2}) == 4, "central commutator targets are not independent") + + +def transition_crosscheck() -> int: + states = {IDENTITY} + frontier = [IDENTITY] + for _ in range(2): + next_frontier = [] + for state in frontier: + for code in range(len(FACTORS)): + successor = step(state, code) + if successor not in states: + states.add(successor) + next_frontier.append(successor) + frontier = next_frontier + checked = 0 + for state in states: + for code in range(len(FACTORS)): + packed = step(state, code) + generic = matrix_mul_generic(state, factor_matrix(code)) + need(packed == generic, "packed transition differs from generic group-algebra multiplication") + checked += 1 + return checked + + +def step3(matrix: tuple[int, ...], g: int, n: tuple[int, ...]) -> tuple[int, ...]: + out = [] + for row in range(3): + for col in range(3): + value = matrix[3 * row + col] + for k in range(3): + if n[3 * k + col]: + entry = matrix[3 * row + k] + value ^= shift(entry, g) ^ entry + out.append(value) + return tuple(out) + + +def factor3(g: int, n: tuple[int, ...]) -> tuple[int, ...]: + gp = (1 << E) | (1 << g) + return tuple( + (((1 << E) if row == col else 0) ^ + (gp if n[3 * row + col] else 0)) + for row in range(3) for col in range(3) + ) + + +def product3(word: tuple[tuple[int, tuple[int, ...]], ...]) -> tuple[int, ...]: + matrix = IDENTITY3 + for g, n in word: + matrix = step3(matrix, g, n) + return matrix + + +def matrix_mul_generic3(a: tuple[int, ...], b: tuple[int, ...]) -> tuple[int, ...]: + return tuple( + ring_mul_generic(a[3 * row], b[col]) ^ + ring_mul_generic(a[3 * row + 1], b[3 + col]) ^ + ring_mul_generic(a[3 * row + 2], b[6 + col]) + for row in range(3) for col in range(3) + ) + + +def embed_center(matrix: tuple[int, ...]) -> tuple[int, ...]: + return tuple(sum((1 << CENTER[c]) for c in range(4) if (entry >> c) & 1) + for entry in matrix) + + +def center_ring_mul(a: int, b: int) -> int: + out = 0 + for i in range(4): + if (a >> i) & 1: + for j in range(4): + if (b >> j) & 1: + out ^= 1 << (i ^ j) + return out + + +CENTER_RING_MUL = tuple(tuple(center_ring_mul(a, b) for b in range(16)) + for a in range(16)) + + +def center_block(z: int, n: tuple[int, ...]) -> tuple[int, ...]: + delta = 1 | (1 << z) + return tuple( + ((1 if row == col else 0) ^ + (delta if n[3 * row + col] else 0)) + for row in range(3) for col in range(3) + ) + + +def center_matrix_mul(a: tuple[int, ...], b: tuple[int, ...]) -> tuple[int, ...]: + return tuple( + CENTER_RING_MUL[a[3 * row]][b[col]] ^ + CENTER_RING_MUL[a[3 * row + 1]][b[3 + col]] ^ + CENTER_RING_MUL[a[3 * row + 2]][b[6 + col]] + for row in range(3) for col in range(3) + ) + + +def triple_block_census(): + choices = tuple((z, n, center_block(z, n)) + for z in (1, 2) for n in IDEMPOTENTS3) + wanted = tuple((1 << z) if row == col else 0 + for row, z in enumerate((1, 2, 3)) for col in range(3)) + counts = [] + for depth in range(1, 4): + candidates = 0 + hit = None + for word in __import__("itertools").product(range(len(choices)), repeat=depth): + state = tuple((1 if row == col else 0) + for row in range(3) for col in range(3)) + for index in word: + state = center_matrix_mul(state, choices[index][2]) + candidates += 1 + if state == wanted: + hit = tuple((choices[index][0], choices[index][1]) for index in word) + break + counts.append(candidates) + if hit is not None: + return choices, wanted, counts, hit + return choices, wanted, counts, None + + +def center_product_crosscheck(choices) -> int: + checked = 0 + for left in choices: + for right in choices: + packed = center_matrix_mul(left[2], right[2]) + generic = matrix_mul_generic3(embed_center(left[2]), embed_center(right[2])) + need(embed_center(packed) == generic, + "central-ring matrix product differs from full group-algebra product") + checked += 1 + return checked + + +def triple_direct_word(): + e11 = (1, 0, 0, 0, 0, 0, 0, 0, 0) + e22 = (0, 0, 0, 0, 1, 0, 0, 0, 0) + e33 = (0, 0, 0, 0, 0, 0, 0, 0, 1) + return tuple((g, e11) for g in (X1, Y1, X1, Y1)) + \ + tuple((g, e22) for g in (XW, Y1, XW, Y1)) + \ + tuple((g, e33) for g in (X1, XW, Y1, X1, XW, Y1)) + + +def triple_controls(): + need(len(IDEMPOTENTS3) == 28, "wrong rank-one idempotent count for three roles") + for n in IDEMPOTENTS3: + for row in range(3): + for col in range(3): + value = 0 + for k in range(3): + value ^= n[3 * row + k] & n[3 * k + col] + need(value == n[3 * row + col], "listed 3x3 matrix is not idempotent") + need(n[0] ^ n[4] ^ n[8] == 1, "rank-one 3x3 idempotent does not have trace one") + + checked_blocks = 0 + for z, x in ((Z1, X1), (ZW, XW)): + for n in IDEMPOTENTS3: + packed = IDENTITY3 + generic = IDENTITY3 + for g in (x, Y1, x, Y1): + packed = step3(packed, g, n) + generic = matrix_mul_generic3(generic, factor3(g, n)) + expected = embed_center(center_block(1 if z == Z1 else 2, n)) + need(packed == expected == generic, + "four-call commutator block differs from its central block") + checked_blocks += 1 + + choices, wanted_center, counts, hit = triple_block_census() + need(hit is None, "three-call commutator-block family unexpectedly reaches the dependent triple") + central_product_checks = center_product_crosscheck(choices) + direct = triple_direct_word() + wanted_full = tuple((1 << z) if row == col else 0 + for row, z in enumerate((Z1, ZW, ZW2)) for col in range(3)) + packed_direct = product3(direct) + generic_direct = IDENTITY3 + for g, n in direct: + generic_direct = matrix_mul_generic3(generic_direct, factor3(g, n)) + need(len(direct) == 14 and packed_direct == wanted_full == generic_direct, + "direct 14-call dependent central triple failed") + for index in range(len(direct)): + shortened = direct[:index] + direct[index + 1:] + need(product3(shortened) != wanted_full, + "single-factor deletion of the direct central triple unexpectedly passes") + return { + "target": [Z1, ZW, ZW2], + "direct_coordinate_calls": len(direct), + "block_alphabet_size": len(choices), + "raw_ordered_block_sequences_checked_by_depth": counts, + "raw_block_sequences_total": sum(counts), + "block_family_hit_through_three": False, + "block_family_scope": "concatenations of at most three D_N(Z_1) or D_N(Z_w) blocks, each expanded to four paid source factors", + "four_call_block_endpoint_checks": checked_blocks, + "central_block_pair_product_checks": central_product_checks, + "direct_word_full_and_generic_endpoints_match": True, + "all_fourteen_single_deletions_fail": True, + } + + +def main() -> None: + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--write-certificate", action="store_true") + args = parser.parse_args() + group_checks() + packed_checks = transition_crosscheck() + identity = IDENTITY + for code in range(len(FACTORS)): + one = step(identity, code) + need(step(one, code) == identity, "paid factor is not involutive") + + one_output = single_word() + single_target = target(Z1, E) + need(len(one_output) == 4 and product(one_output) == single_target, + "four-call one-output positive control failed") + need(matrix_mul_generic(IDENTITY, IDENTITY) == IDENTITY, "generic identity control failed") + direct = direct_word() + wanted = target() + need(len(direct) == 8 and product(direct) == wanted, + "direct eight-call construction failed") + generic_direct = IDENTITY + for code in direct: + generic_direct = matrix_mul_generic(generic_direct, factor_matrix(code)) + need(generic_direct == wanted, "generic direct-word endpoint differs") + for index in range(len(direct)): + shortened = direct[:index] + direct[index + 1:] + need(product(shortened) != wanted, "one-factor deletion control unexpectedly reaches target") + mutated = target(Z1, ZW2) + need(product(direct) != mutated, "target mutation control unexpectedly passes") + triple_result = triple_controls() + + words, layers, layer_digests = build_ball(3) + raw_words = sum(24 ** depth for depth in range(4)) + need(raw_words == 14425, "raw radius-three word count changed") + found_single = find_within_six(single_target, words) + need(found_single is not None and len(found_single) == 4, + "meet-in-the-middle did not find the known four-call positive control") + found_pair = find_within_six(wanted, words) + need(found_pair is None, "unexpected shared word of at most six calls; inspect witness") + + cert = { + "model": "F2[UT3(F4)]", + "field_polynomial": "w^2+w+1=0", + "group_order": 64, + "group_law": "(a,b,c)(a',b',c')=(a+a',b+b',c+c'+ab')", + "labels": dict(zip(LABEL_NAMES, LABELS)), + "central_targets": {"Z_1": Z1, "Z_w": ZW}, + "alphabet_factor_count": 24, + "rank_one_idempotent_count": len(IDEMPOTENTS), + "radius": 3, + "raw_words_through_radius": raw_words, + "distinct_state_layer_sizes": layers, + "distinct_ball_states": len(words), + "layer_sha256": layer_digests, + "ball_sha256": matrix_digest(words), + "packed_vs_generic_transitions": packed_checks, + "single_output_positive_word_length": len(found_single), + "direct_pair_word_length": len(direct), + "shared_pair_word_through_six": False, + "minimum_pair_word_length": 8, + "dependent_three_role_block_pivot": triple_result, + "parity_lemma": "Every label occurs an even number of times because the target is trivial mod I^2 and each rank-one idempotent has trace one.", + "controls": { + "all_factor_involutions": True, + "single_commutator_positive": True, + "direct_pair_positive": True, + "all_eight_single_deletions_fail": True, + "mutated_Z_w_to_Z_w2_fails": True, + }, + } + certificate_path = PACKAGE / "CERTIFICATE.json" + if args.write_certificate: + certificate_path.write_text(json.dumps(cert, indent=2, sort_keys=True) + "\n") + else: + stored = json.loads(certificate_path.read_text()) + need(stored == cert, "recomputed result differs from CERTIFICATE.json") + print("PASS_UT3_F4_CENTRAL_PAIR", json.dumps(cert, sort_keys=True, separators=(",", ":"))) + + +if __name__ == "__main__": + main()