From 1c5f06546c1348e7a7cfdae044c5002322acd064 Mon Sep 17 00:00:00 2001 From: Sagar Thakrar <18622288+thakrarsagar@users.noreply.github.com> Date: Mon, 19 Oct 2026 15:59:10 +0530 Subject: [PATCH 1/2] Research A4 four-role target exact minimum eight (no seven-call word) Written C3-determinant plus radical-rank proof excludes length 7 and <=5; two independently written exhaustive C joins exclude every word of length <=7 (covering length 6); the direct eight-call word is replayed exactly. Formal model of PR #2116 only; no kappa or supplier claim. Co-Authored-By: Claude Opus 5.5 --- research/a4-seven-call-radical-rank/README.md | 237 ++++++++++ .../a4-seven-call-radical-rank/SOURCES.json | 24 + research/a4-seven-call-radical-rank/TASK.json | 70 +++ .../a4-seven-call-radical-rank/VERIFY.json | 21 + research/a4-seven-call-radical-rank/join_a.c | 343 ++++++++++++++ research/a4-seven-call-radical-rank/join_b.c | 254 +++++++++++ research/a4-seven-call-radical-rank/verify.py | 421 ++++++++++++++++++ 7 files changed, 1370 insertions(+) create mode 100644 research/a4-seven-call-radical-rank/README.md create mode 100644 research/a4-seven-call-radical-rank/SOURCES.json create mode 100644 research/a4-seven-call-radical-rank/TASK.json create mode 100644 research/a4-seven-call-radical-rank/VERIFY.json create mode 100644 research/a4-seven-call-radical-rank/join_a.c create mode 100644 research/a4-seven-call-radical-rank/join_b.c create mode 100644 research/a4-seven-call-radical-rank/verify.py diff --git a/research/a4-seven-call-radical-rank/README.md b/research/a4-seven-call-radical-rank/README.md new file mode 100644 index 0000000000..a2da1ee187 --- /dev/null +++ b/research/a4-seven-call-radical-rank/README.md @@ -0,0 +1,237 @@ +# The four-output A4 target has exact minimum eight: no seven-call word + +**Scoped exact closure in a formal model; no new `kappa`.** In the formal +`F2[A4]` four-role model of [PR #2116](https://github.com/CrocSwap/integer-mult-bounds/pull/2116), +every word realizing `T = diag([a],[b],[c],[d])` uses at least three `a`-calls +and at least three `b`-calls, and the numbers of `a`- and `b`-calls agree +modulo 3. A written proof therefore excludes length 7 and every length up to 5. +Length 6 would need exactly three calls of each label. Two independently +written exhaustive joins exclude every word of length up to 7, including that +case. Together with the direct eight-call word, this gives an **exact minimum +of 8**. The model has no cross-role paid-call saving for this target. + +| Length | Status | Evidence | +|---|---|---| +| 1-5 | impossible | written proof (Lemmas 1-2); also both joins | +| 6 | impossible | exhaustive joins A and B (reproduces #2116); not covered by the written lemmas | +| 7 | impossible | written proof (Lemmas 1-2); independently both exhaustive joins | +| 8 | realized | direct word (`a`, `b`, `abba`, `ab` on roles 1-4), replayed exactly on all 48 basis inputs | + +The evidence has three different kinds. For length 7 and lengths up to 5 it is +a proof of impossibility. For length 6 it is a finite exhaustive certificate. +For length 8 it is an explicit construction. None of these is a multiplication +theorem, a supplier result or a `kappa` change. + +## Model + +The model is unchanged from #2116. Take `a=(123)`, `b=(124)`, +`c=aba^-1b^-1=(12)(34)`, `d=ab=(13)(24)` and `e=ba=(14)(23)` in `A4`, composing +as `(pq)(t)=p(q(t))`. Then `V = {1,c,d,e}` is the normal Klein subgroup. A paid +call is + +```text +D_N(g) = I + ([g]+[1]) N, g in {a,b}, N = x y^T in M4(F2), x,y != 0, y^T x = 1. +``` + +There are 120 rank-one idempotents `N`, so the alphabet has 240 factors. +Factor `120*gi + n` uses label `a` (`gi=0`) or `b` (`gi=1`). It also uses the +`n`-th pair `(x,y)`, ordered by `x` and then by `y`. This is the ordering of +#2116, so its direct word is `[0,128,24,144,144,24,56,176]`. A word realizes `T` +when the 4x4 product over `F2[A4]` equals `T` in every formal coefficient. The +model has four roles, allows arbitrary dirty inputs and has no workspace. Each +call costs one, and no helper, copy or restoration operation is charged. + +## Proof + +Write `n_a` and `n_b` for the numbers of `a`- and `b`-calls in a word. + +**Lemma 1 (C3 determinant; the screen named in #2116).** Map `F2[A4]` to the +commutative ring `F2[A4/V] = F2[t]/(t^3-1)`, with `a -> t` and `b -> t^2`. +The matrix determinant lemma gives `det D_N(g) = 1 + (g+1) y^T x = g`. +So a word has determinant `t^(n_a - n_b)`. The target has determinant +`t * t^2 * 1 * 1 = 1`. The elements `1,t,t^2` are distinct, so +`n_a = n_b (mod 3)`. + +**Lemma 2 (radical rank).** Every word equal to `T` has `n_b >= 3`, and +symmetrically `n_a >= 3`. + +*Setup.* Let `J` be the kernel of `F2[A4] -> F2[A4/V]`. This is the Jacobson +radical. It has dimension 9 and `J = sum_i a^i I_V`, where `I_V` is the +augmentation ideal of `F2[V]`. Also `J^2 = sum_i a^i I_V^2`, and +`I_V^2 = F2 * sum_{v in V} [v]`. Put `S = F2[] = span{1,a,a^2}`. Then +`S` meets `J` only in `0`, so `S` maps isomorphically onto `F2[A4]/J`. Write +`eps_v = [v]+[1]`, which lies in `J`. + +1. *Splitting the b-calls.* For a fixed idempotent `N`, + `D_N(g) D_N(h) = D_N(gh)`. Since `b = a^2 d`, this gives + `D_N(b) = D_N(a^2) D_N(d)` and `D_N(d) = I + eps_d N`. Each call is therefore + `F_k = B_k E_k`. Here `B_k` is `D_{N_k}(a)` or `D_{N_k}(a^2)` in `GL4(S)`. + The factor `E_k` is `I` for an `a`-call and `I + eps_d N_k` for a `b`-call. +2. *Moving radical parts right.* Put `C_k = B_{k+1}...B_L` and + `A = B_1...B_L`, which lies in `GL4(S)`. Then + `W = A * prod_k (I + X_k)`. The product runs over the `b`-calls in order, + with `X_k = C_k^-1 eps_d N_k C_k` in `M4(J)`. +3. *The lift.* If `W = T`, then `A = T (mod J)`. Since `S` meets `J` only in + `0`, the lift is unique: `A = diag(a, a^2, 1, 1)`. Hence + `U := A^-1 T = diag(1, a^-2 b, c, d) = diag(1, d, c, d)`. +4. *A twisted functional.* Let `mu: V -> F4` be given by `mu(1)=0`, `mu(c)=1`, + `mu(a^-1 c a)=w` and `mu(a^-2 c a^2)=w^2`, where `w^2+w+1=0`. Because + `1+w+w^2=0`, the map `mu` is `F2`-linear on `V = F2^2`. It is injective and + satisfies `mu(a^-1 v a) = w mu(v)`. Define the linear map + `Phi(sum beta_{i,v} [a^i v]) = sum beta_{i,v} mu(v)` from `F2[A4]` to `F4`. + For `y` in `J` and `r,s` in `S`, we have + `Phi(r y s) = aug(r) Phi(y) psi(s)`, where `aug(a)=1` and `psi(a)=w`. The + reason is `a^i (a^m eps_v) a^j = a^(i+m+j) eps_(a^-j v a^j)`. Also + `Phi(J^2) = 0`, because `sum_v mu(v) = 0`. +5. *Counting rank.* Modulo `M4(J^2)` we have + `prod (I+X_k) = I + sum X_k`. Apply `Phi` entrywise, and note that `aug` + is a ring map `M4(S) -> M4(F2)`. This gives + + ```text + sum_{b-calls k} aug(C_k)^-1 (mu(d) N_k) psi(C_k) = Phi(U - I) = diag(0, mu(d), mu(c), mu(d)). + ``` + + Over `F4`, the left side is a sum of `n_b` matrices of rank at most 1. The + right side has rank 3 because `mu` is injective. So `n_b >= 3`. + +The same steps with base `b` start from `a = b^2 e`. The lift is +`diag(b^2, b, 1, 1)` and the defect is `U = diag(e, 1, c, d)`, again of rank +3, so `n_a >= 3`. + +**Theorem.** Every word realizing `T` has `n_a, n_b >= 3` and +`n_a = n_b (mod 3)`. So its length is 6, with `(n_a,n_b)=(3,3)`, or at least 8. +At length 7, Lemma 1 allows only `(2,5)` and `(5,2)`, and Lemma 2 rules out +both. The exhaustive joins below exclude length 6, and the direct word has +length 8. The exact minimum is 8. + +Lemma 2 explains why the direct word is optimal. Each target role in `V` +contributes an independent rank to the radical layer. Every call of the other +label can pay at most one unit of that rank, after any conjugation by the +semisimple part. The C3 determinant then rules out the one unbalanced split +that would save a call. + +## Independent exhaustive joins + +Both programs build `S3`, the distinct products of length at most 3. They +deduplicate by the full 4x4 state of 12-bit coefficients and keep each state's +minimal length. Any word of length at most 6 is `X Y` with `X` and `Y` in `S3`. +A word of length 7 is `X f Y`, where `X` can be taken to have minimal length +exactly 3; otherwise a shorter word would exist. So each join tests +`X^-1 T in S3` for every `X`, and tests `f^-1 X^-1 T in S3` for every +minimal-length-3 class `X` and every factor `f`. That covers all lengths +through 7. + +| | Join A (`join_a.c`) | Join B (`join_b.c`) | +|---|---|---| +| state representation | 4x4 matrix of 12-bit masks over `A4` | 12 coefficient matrices `M_g` in `M4(F2)`, 16 bits each | +| group construction | all even permutations | closure of `` on packed codes | +| `S3` built by | right multiplication | left multiplication | +| enumerated end | left: `X^-1 T`, then `D_f^-1 (X^-1 T)` | right: `T Y^-1`, then `(T Y^-1) D_f^-1` | +| hash | `GF(2)`-linear (child hashes by XOR) | nonlinear multiply-xorshift | +| distinct `S3` states by minimal length | 1, 240, 41,920, 6,655,830 (total 6,697,991) | identical | +| minimal-length-3 classes expanded | 6,655,830 | 6,655,830 | +| children looked up | 1,597,399,200 | 1,597,399,200 | +| words of length at most 7 found | none | none | +| local wall time / peak RSS (2 threads, `-march=native` development build) | 27 s / 369 MB | 39 s / 316 MB | + +The `S3` total, 6,697,991, matches #2116's `right_distinct_exact_states`. The +verifier reads that value from the pinned predecessor `RESULT.json`. Every +reported hit is confirmed in C, by comparing full states and multiplying out +the word. Python then replays it independently. The Python code does not reuse +#2116's `search.cpp` or its verifier. + +## Controls + +- Direct eight-call word: its exact product equals `T`, and it agrees on all + 48 role/address basis inputs. All 8 single-call omissions are rejected, and + so is a mutated final label (`b -> a`). +- Lemma 2 checks: `D_N(b) = D_N(a^2) D_N(d)` and `D_N(a) = D_N(b^2) D_N(e)` + hold for all 120 idempotents. `J` is exactly the kernel, with dimension 9. + `S` meets `J` only in `0`, and lifts are unique. The twisted bimodule law + holds for all 512 elements of `J` and all `r,s` in `S`, and `Phi(J^2)=0`. + The defect rank is 3 in both bases. The step-5 identity + `Phi(A^-1 W - I) = sum aug(C_k)^-1 mu(v) N_k psi(C_k)` holds for 60 random + words per base, of lengths 1 to 8, with rank at most the number of calls of + the other label. Lemma 1 holds for 200 random words. +- Mutation control for the lemma: the three-output target + `diag([a],[b],[c],[1])` has defect rank only 2 in each base. Both joins find + a 6-call word for it, `128 144 34 0 34 144` from A and `144 34 0 34 144 128` + from B, with `(n_a,n_b)=(3,3)`. Python replays both words exactly. +- Planted 7-words: two random seeds per join (sampled run, every 64th class plus + the planted class). Each must return a length-7 word, confirmed in Python to + equal the planted product. This exercises the `X f Y` path in both joins. + +## Reproduce + +From the repository root, with Python 3 and a C compiler with POSIX threads: + +```sh +python3 -I -B research/a4-seven-call-radical-rank/verify.py +python3 scripts/research_package.py --package research/a4-seven-call-radical-rank --check-only +``` + +The expected final line is `PASS_A4_FOUR_ROLE_EXACT_MINIMUM_EIGHT`, preceded by +a JSON report with the counts above. The local run took 79 s wall time with +369 MB peak RSS. It used Python 3.14.4 and gcc 15.2.0 on 4 shared CPUs. The +generic runner requests Python 3.12, which was not used locally. + +## Scope, inherited assumptions and unresolved obligations + +- This is a formal model only. It inherits #2116's alphabet, unit call + prices, four roles, dirty inputs, absence of workspace and exact-coefficient + target. The lemmas are proved for this alphabet and target. The rank argument + uses only that each call is `I + (g+1)N` with `N` an `F2`-rational rank-one + idempotent. +- Unresolved, and not addressed here: native conversion of `F2[A4]` calls, + restored workspace, a physical caller, chronology, hosting, precision, + recursive transfer and supplier admission. These costs are unknown, not + zero. +- Decision consequence: the A4 four-role endpoint gives no formal saving. The + nonabelian-register route through this target therefore does not merit a + priced native-conversion step. A 7-word would have saved 1 of 8 calls in the + formal model only. + +## Open next questions + +The same questions are structured in [TASK.json](TASK.json). + +1. **Can the length-6 case `(n_a,n_b)=(3,3)` be excluded in writing?** This + would turn the exact minimum into a fully written theorem. That matters for + role counts where exhaustive search is infeasible. First step: at `(3,3)`, + both step-5 identities must be tight rank-3 decompositions with + `F2`-rational columns `aug(C_k)^-1 x_k`. Look for a contradiction between + the two bases, or at the `J^2` layer. Blocked by: nothing beyond the + bookkeeping. +2. **Does the radical-rank bound extend to `G = P x| H`, with `P` a normal + 2-group and `H` of odd order?** Examples include more roles over `A4`, or + `SL2(F3)`. The goal is uniform label-count floors in place of censuses. + First step: state the lemma with `S = F2[H]` and an equivariant functional + `mu` on the Frattini quotient of `P`, then test it against an existing finite census. Blocked + by: nothing for the formal statement. Native conversion stays unpriced. + +## Predecessors and attribution + +- Model, alphabet, direct word, C3 screen and the length-6 exclusion come from + [PR #2116](https://github.com/CrocSwap/integer-mult-bounds/pull/2116) + (`research/a4-commutator-four-role-seed-dcbf`, GitHub `1337isnot1337`, + commit author Cinna Davis, head `19cdf74af162f1444830f1a0f0a8e0fe306564ad`; + Discussion [#2095](https://github.com/CrocSwap/integer-mult-bounds/discussions/2095)). + This package answers that package's named open question. It re-proves the + length-6 exclusion with new code and does not modify the predecessor. +- The untwisted `J/J^2` coefficient-matrix argument for the 2-group `Q8`, in + `research/q8-central-minus-one-any-registers-seed0332f4` and + `research/q8-r3-two-central-one-generator-seed809fc39d`, is the closest + prior technique. The new ingredients are three. First, splitting off the + semisimple part `F2[]` in a group algebra that is not local. Second, the + twisted functional `Phi` that absorbs conjugation by that part. Third, using + both bases together with the C3 determinant. +- Exact pins are in [SOURCES.json](SOURCES.json). The base is + `20ecf2891d80b5acf18d980b2164fb44ea7faa90` and priority revision 6 is in + force. The live input is #2116's `RESULT.json`. + +Provenance: the lemma, both joins and the verifier were written in one AI-assisted +session. The written proof's steps are each checked numerically by the verifier, +as described above. No independent human review is claimed. + +Prepared by Sagar Thakrar (thakrarsagar) with substantial AI assistance from +Claude (Anthropic, Claude Opus 5.5). Apache-2.0. diff --git a/research/a4-seven-call-radical-rank/SOURCES.json b/research/a4-seven-call-radical-rank/SOURCES.json new file mode 100644 index 0000000000..105b7f3202 --- /dev/null +++ b/research/a4-seven-call-radical-rank/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5", + "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0" + }, + { + "path": "research/a4-commutator-four-role-seed-dcbf/RESULT.json", + "usage": "input", + "git_blob": "fa78cc9381f27efea106aac5947a465daa89b795", + "sha256": "2ff56618b041bbfe7d8c3c4e521cdf1b33b70d0f7299c1f56c780e76ec40a5c6" + } + ] +} diff --git a/research/a4-seven-call-radical-rank/TASK.json b/research/a4-seven-call-radical-rank/TASK.json new file mode 100644 index 0000000000..929fdcaefa --- /dev/null +++ b/research/a4-seven-call-radical-rank/TASK.json @@ -0,0 +1,70 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "priority_revision": 6, + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "original_card": { + "id": "bit-new-register-model", + "question": "Can an explicitly larger or nonabelian register model escape the scoped three-register obstruction?", + "starting_points": [ + "docs/research/research-family-status.md", + "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. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "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": "Decide the open length-7 slice of PR #2116's formal F2[A4] four-role target diag([a],[b],[c],[d]) (240 rank-one paid factors D_N(g), g in {a,b}, four roles, no workspace, every formal coefficient): exact minimum 7 or 8.", + "scope_change_reason": "The card asks broadly whether a nonabelian register model escapes the three-register obstruction; PR #2116 instantiated it as this A4 four-role target and left length 7 open. This package closes that one named slice (no other groups, targets, role counts or census extension), because a 7-word would have been the first sub-direct cross-role saving in the formal four-role finite-group family and an exact 8 closes the model on four roles.", + "bottleneck_link": "Side result for the bit-mechanisms track: it decides that this nonabelian formal register endpoint has no paid-call saving (exact minimum equals the direct 8), so it gives no reason to price a native conversion of A4 group-algebra calls toward the bit primitive. It changes no selected supplier or kappa.", + "budget_minutes": 90, + "stop_rule": "Submission rule committed before searching: a verified 7-word is submitted; an exact 8 is submitted only with a written structural lemma beyond the C3 determinant screen, otherwise nothing is posted. Stop with no PR if the primary join exceeds ~15 min wall or 1.5 GB RSS, or if the two joins disagree unresolved by the experiment deadline.", + "outcome": "negative-result", + "evidence": "Written proof: C3 determinant (n_a = n_b mod 3) plus a radical-rank lemma (n_a >= 3 and n_b >= 3) exclude length 7 and lengths <= 5. Two independently written exhaustive C joins (different state representation, multiplication side, enumerated end and hash) each expand all 6,655,830 minimal-length-3 classes against all 6,697,991 distinct products of length <= 3 (1,597,399,200 lookups each) and find no word of length <= 7, which also excludes length 6. The direct 8-word replays exactly on all 48 basis inputs. Controls: omissions, label mutation, three-output 6-words, planted 7-words, numeric checks of every lemma step. Verifier: research/a4-seven-call-radical-rank/verify.py, PASS_A4_FOUR_ROLE_EXACT_MINIMUM_EIGHT.", + "author": "Sagar Thakrar (thakrarsagar)", + "ai_assistance": "Substantial AI assistance from Claude (Anthropic, Claude Opus 5.5) in derivation, both C joins, the Python verifier and writing; no independent human review is claimed.", + "open_questions": [ + { + "question": "Can the length-6 case (n_a,n_b)=(3,3) be excluded by a written argument rather than exhaustive search?", + "why_it_matters": "It would make the exact minimum a fully written theorem, reusable for role counts or targets where exhaustive search is infeasible.", + "first_step": "At (3,3) both step-5 identities are tight rank-3 decompositions with F2-rational columns aug(C_k)^-1 x_k; look for an incompatibility between the a-base and b-base decompositions or at the J^2 layer.", + "blocked_by": "Nothing beyond the bookkeeping." + }, + { + "question": "Does the radical-rank label-count bound extend to G = P x| H with P a normal 2-group and H of odd order (more roles over A4, SL2(F3))?", + "why_it_matters": "It would replace finite censuses by uniform per-label floors for nonabelian register models.", + "first_step": "State the lemma with S = F2[H] and an H-equivariant functional mu on the Frattini quotient of P, then test it against an existing finite census.", + "blocked_by": "Nothing for the formal statement; native conversion remains unpriced." + } + ] +} diff --git a/research/a4-seven-call-radical-rank/VERIFY.json b/research/a4-seven-call-radical-rank/VERIFY.json new file mode 100644 index 0000000000..36ce2b4555 --- /dev/null +++ b/research/a4-seven-call-radical-rank/VERIFY.json @@ -0,0 +1,21 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/a4-commutator-four-role-seed-dcbf/RESULT.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 600, + "checks": "Exact direct 8-word replay on all 48 basis inputs with 8 omission and 1 label-mutation rejections; C3 determinant on 200 random words; every step of the radical-rank lemma in both bases (factor split for all 120 idempotents, J = kernel of dimension 9, unique lifts, twisted bimodule law on all of J, Phi(J^2)=0, defect rank 3 and three-output control rank 2, step-5 identity on 60 random words per base); compile both C joins with warnings as errors and check S3 counts 1/240/41920/6655830 (total 6697991, equal to PR #2116's pinned value), 1,597,399,200 lookups and no word of length <= 7 in each; three-output 6-word and planted 7-word positive controls in each join, all replayed in Python." + } + ] +} diff --git a/research/a4-seven-call-radical-rank/join_a.c b/research/a4-seven-call-radical-rank/join_a.c new file mode 100644 index 0000000000..b23ce3e4e6 --- /dev/null +++ b/research/a4-seven-call-radical-rank/join_a.c @@ -0,0 +1,343 @@ +/* join_a.c - primary exact 3+1+3 join (left side of length 4) for the A4 four-role target. + * + * State: 4x4 matrix over F2[A4]; entry (i,j) is a 12-bit mask over the 12 group elements. + * Paid factor f = 120*gi + n: D_N(g) = I + ([g]+[1]) x y^T, g = a (gi=0) or b (gi=1), + * n enumerates (x,y) in F2^4 x F2^4, x,y != 0, popcount(x&y) odd, x-major then y ascending. + * S3 = distinct products of length <= 3 (built by right multiplication, BFS). + * Search: for every X in S3, Q = X^-1 T; Q in S3 => word of length <= 6. For every X whose + * minimal length is 3 and every f, Q' = D_f^-1 Q; Q' in S3 => word X f Y of length <= 7. + * A word of length 7 whose prefix of length 3 has a shorter equivalent has a word of length <= 6, + * which the first check covers. The hash is GF(2)-linear so the 240 children hashes are XOR updates; + * every accepted hit is confirmed by full-state comparison and by multiplying out the word. + * usage: join_a MODE [threads] [sample] [seed] + * MODE = target | three | planted. sample K>1 processes only X with idx%K==0 plus forced X. + */ +#include +#include +#include +#include +#include + +typedef struct { uint16_t m[16]; } St; + +static int perm_[12][4], mul_[12][12], inv_[12]; +static uint16_t LT[12][4096], RT[12][4096]; +static int fx[240], fy[240], fg[240], flabel[2]; +static uint64_t H6[16][2][64]; + +#define TBITS 24 +#define TSIZE (1u << TBITS) +#define TMASK (TSIZE - 1) +#define MAXS 7000000u +static uint64_t *table_; +static St *states; +static uint8_t *level_; +static uint8_t (*word_)[3]; +static uint32_t nstates; +static St T; + +static uint64_t rng_state; +static uint64_t splitmix(void) { + uint64_t z = (rng_state += 0x9E3779B97F4A7C15ull); + z = (z ^ (z >> 30)) * 0xBF58476D1CE4E5B9ull; + z = (z ^ (z >> 27)) * 0x94D049BB133111EBull; + return z ^ (z >> 31); +} + +static int find_perm(const int *p) { + for (int k = 0; k < 12; k++) + if (!memcmp(perm_[k], p, sizeof(int) * 4)) return k; + return -1; +} + +static void build_group(void) { + int n = 0, p[4]; + for (p[0] = 0; p[0] < 4; p[0]++) + for (p[1] = 0; p[1] < 4; p[1]++) + for (p[2] = 0; p[2] < 4; p[2]++) + for (p[3] = 0; p[3] < 4; p[3]++) { + int seen = 0, inv = 0; + for (int i = 0; i < 4; i++) seen |= 1 << p[i]; + if (seen != 15) continue; + for (int i = 0; i < 4; i++) + for (int j = i + 1; j < 4; j++) inv += p[i] > p[j]; + if (inv & 1) continue; + memcpy(perm_[n++], p, sizeof p); + } + if (n != 12) { fprintf(stderr, "group size %d\n", n); exit(2); } + for (int i = 0; i < 12; i++) + for (int j = 0; j < 12; j++) { + int q[4]; + for (int t = 0; t < 4; t++) q[t] = perm_[i][perm_[j][t]]; /* (p o q)(t) = p(q(t)) */ + mul_[i][j] = find_perm(q); + } + for (int i = 0; i < 12; i++) + for (int j = 0; j < 12; j++) + if (mul_[i][j] == 0) inv_[i] = j; + for (int g = 0; g < 12; g++) + for (int m = 0; m < 4096; m++) { + uint16_t l = 0, r = 0; + for (int k = 0; k < 12; k++) + if (m >> k & 1) { l |= 1u << mul_[g][k]; r |= 1u << mul_[k][g]; } + LT[g][m] = l; RT[g][m] = r; + } +} + +static void build_factors(void) { + int pa[4] = {1, 2, 0, 3}, pb[4] = {1, 3, 2, 0}; /* a=(123), b=(124) on points 1..4 */ + flabel[0] = find_perm(pa); flabel[1] = find_perm(pb); + int n = 0; + for (int x = 1; x < 16; x++) + for (int y = 1; y < 16; y++) + if (__builtin_popcount(x & y) & 1) { fx[n] = x; fy[n] = y; n++; } + if (n != 120) { fprintf(stderr, "idempotents %d\n", n); exit(2); } + for (int gi = 0; gi < 2; gi++) + for (int k = 0; k < 120; k++) { + fx[120 * gi + k] = fx[k]; fy[120 * gi + k] = fy[k]; fg[120 * gi + k] = flabel[gi]; + } +} + +static void build_hash(void) { + uint64_t B[16][12]; + rng_state = 0x5EED0A4A4A4A4ull; + for (int e = 0; e < 16; e++) + for (int b = 0; b < 12; b++) B[e][b] = splitmix(); + for (int e = 0; e < 16; e++) + for (int h = 0; h < 2; h++) + for (int v = 0; v < 64; v++) { + uint64_t s = 0; + for (int b = 0; b < 6; b++) + if (v >> b & 1) s ^= B[e][6 * h + b]; + H6[e][h][v] = s; + } +} + +static inline uint64_t hent(int e, uint16_t v) { return H6[e][0][v & 63] ^ H6[e][1][v >> 6]; } +static uint64_t hash_st(const St *s) { + uint64_t h = 0; + for (int e = 0; e < 16; e++) h ^= hent(e, s->m[e]); + return h; +} + +/* X <- X * D_f */ +static void right_mul(St *X, int f) { + int x = fx[f], y = fy[f], g = fg[f]; + for (int i = 0; i < 4; i++) { + uint16_t v = 0; + for (int k = 0; k < 4; k++) + if (x >> k & 1) v ^= X->m[4 * i + k]; + uint16_t u = RT[g][v] ^ v; + for (int j = 0; j < 4; j++) + if (y >> j & 1) X->m[4 * i + j] ^= u; + } +} + +/* Q <- D_f^-1 * Q, with D_f^-1 = D_N(g^-1) */ +static void left_inv(St *Q, int f) { + int x = fx[f], y = fy[f], h = inv_[fg[f]]; + for (int j = 0; j < 4; j++) { + uint16_t w = 0; + for (int k = 0; k < 4; k++) + if (y >> k & 1) w ^= Q->m[4 * k + j]; + uint16_t u = LT[h][w] ^ w; + for (int i = 0; i < 4; i++) + if (x >> i & 1) Q->m[4 * i + j] ^= u; + } +} + +static int64_t lookup(const St *s, uint64_t h) { + uint32_t pos = (uint32_t)h & TMASK, tag = (uint32_t)(h >> 32); + for (;;) { + uint64_t e = table_[pos]; + if (!e) return -1; + if ((uint32_t)(e >> 32) == tag) { + uint32_t idx = (uint32_t)e - 1; + if (!memcmp(&states[idx], s, sizeof(St))) return idx; + } + pos = (pos + 1) & TMASK; + } +} + +static void insert(uint32_t idx, uint64_t h) { + uint32_t pos = (uint32_t)h & TMASK; + while (table_[pos]) pos = (pos + 1) & TMASK; + table_[pos] = ((h >> 32) << 32) | (uint64_t)(idx + 1); +} + +static St identity(void) { + St s; memset(&s, 0, sizeof s); + for (int i = 0; i < 4; i++) s.m[5 * i] = 1u << 0; /* group element 0 is the identity */ + return s; +} + +static uint32_t level_count[4]; +static void build_S3(void) { + states = malloc(sizeof(St) * MAXS); level_ = malloc(MAXS); word_ = malloc(3 * (size_t)MAXS); + table_ = calloc(TSIZE, sizeof(uint64_t)); + if (!states || !level_ || !word_ || !table_) { fprintf(stderr, "oom\n"); exit(2); } + nstates = 0; + St id = identity(); + states[0] = id; level_[0] = 0; insert(0, hash_st(&id)); nstates = 1; level_count[0] = 1; + uint32_t lo = 0, hi = 1; + for (int L = 1; L <= 3; L++) { + for (uint32_t s = lo; s < hi; s++) + for (int f = 0; f < 240; f++) { + St c = states[s]; right_mul(&c, f); + uint64_t h = hash_st(&c); + if (lookup(&c, h) >= 0) continue; + if (nstates >= MAXS) { fprintf(stderr, "MAXS\n"); exit(2); } + states[nstates] = c; level_[nstates] = (uint8_t)L; + memcpy(word_[nstates], word_[s], 3); word_[nstates][L - 1] = (uint8_t)f; + insert(nstates, h); nstates++; + } + lo = hi; hi = nstates; level_count[L] = hi - lo; + } +} + +static int nthreads = 2, sample = 1; +static int64_t forced = -1; +static pthread_mutex_t mu = PTHREAD_MUTEX_INITIALIZER; +static uint64_t short_hits, long_hits, tag_matches, children, processed3; +static int best_len = 99, best_word[8]; + +static void record(const int *w, int len) { + pthread_mutex_lock(&mu); + if (len < best_len) { best_len = len; memcpy(best_word, w, sizeof(int) * len); } + pthread_mutex_unlock(&mu); +} + +static int product_is(const int *w, int len, const St *target) { + St s = identity(); + for (int k = 0; k < len; k++) right_mul(&s, w[k]); + return !memcmp(&s, target, sizeof(St)); +} + +static void *worker(void *arg) { + int tid = (int)(intptr_t)arg; + uint64_t sh = 0, lh = 0, tm = 0, ch = 0, p3 = 0; + static __thread uint64_t sub[2][16][16]; + static __thread uint16_t uu[2][16][4]; + uint64_t hc[240]; + for (uint32_t idx = (uint32_t)tid; idx < nstates; idx += (uint32_t)nthreads) { + if (sample > 1 && idx % (uint32_t)sample && (int64_t)idx != forced) continue; + St Q = T; + int L = level_[idx]; + for (int k = 0; k < L; k++) left_inv(&Q, word_[idx][k]); + uint64_t hq = hash_st(&Q); + int64_t y = lookup(&Q, hq); + if (y >= 0) { + int w[8], n = 0; + for (int k = 0; k < L; k++) w[n++] = word_[idx][k]; + for (int k = 0; k < level_[y]; k++) w[n++] = word_[y][k]; + if (!product_is(w, n, &T)) { fprintf(stderr, "short hit failed replay\n"); exit(3); } + sh++; record(w, n); + } + if (L != 3) continue; + p3++; + /* w_y for all y, then u_{gi,y} and subset hash deltas */ + uint16_t wy[16][4]; + memset(wy[0], 0, sizeof wy[0]); + for (int yy = 1; yy < 16; yy++) { + int k = __builtin_ctz(yy), prev = yy & (yy - 1); + for (int j = 0; j < 4; j++) wy[yy][j] = wy[prev][j] ^ Q.m[4 * k + j]; + } + for (int gi = 0; gi < 2; gi++) { + int h = inv_[flabel[gi]]; + for (int yy = 1; yy < 16; yy++) { + uint64_t r[4]; + for (int j = 0; j < 4; j++) uu[gi][yy][j] = LT[h][wy[yy][j]] ^ wy[yy][j]; + for (int i = 0; i < 4; i++) { + r[i] = 0; + for (int j = 0; j < 4; j++) r[i] ^= hent(4 * i + j, uu[gi][yy][j]); + } + sub[gi][yy][0] = 0; + for (int xs = 1; xs < 16; xs++) sub[gi][yy][xs] = sub[gi][yy][xs & (xs - 1)] ^ r[__builtin_ctz(xs)]; + } + } + for (int f = 0; f < 240; f++) { + hc[f] = hq ^ sub[f / 120][fy[f]][fx[f]]; + __builtin_prefetch(&table_[(uint32_t)hc[f] & TMASK]); + } + for (int f = 0; f < 240; f++) { + uint32_t pos = (uint32_t)hc[f] & TMASK, tag = (uint32_t)(hc[f] >> 32); + ch++; + for (;;) { + uint64_t e = table_[pos]; + if (!e) break; + if ((uint32_t)(e >> 32) == tag) { + tm++; + St c = Q; + const uint16_t *u = uu[f / 120][fy[f]]; + for (int i = 0; i < 4; i++) + if (fx[f] >> i & 1) + for (int j = 0; j < 4; j++) c.m[4 * i + j] ^= u[j]; + St chk = Q; left_inv(&chk, f); + if (memcmp(&chk, &c, sizeof(St))) { fprintf(stderr, "incremental child mismatch\n"); exit(3); } + uint32_t yi = (uint32_t)e - 1; + if (!memcmp(&states[yi], &c, sizeof(St))) { + int w[8], n = 0; + for (int k = 0; k < 3; k++) w[n++] = word_[idx][k]; + w[n++] = f; + for (int k = 0; k < level_[yi]; k++) w[n++] = word_[yi][k]; + if (!product_is(w, n, &T)) { fprintf(stderr, "long hit failed replay\n"); exit(3); } + lh++; record(w, n); + } + } + pos = (pos + 1) & TMASK; + } + } + } + pthread_mutex_lock(&mu); + short_hits += sh; long_hits += lh; tag_matches += tm; children += ch; processed3 += p3; + pthread_mutex_unlock(&mu); + return NULL; +} + +int main(int argc, char **argv) { + const char *mode = argc > 1 ? argv[1] : "target"; + if (argc > 2) nthreads = atoi(argv[2]); + if (argc > 3) sample = atoi(argv[3]); + uint64_t seed = argc > 4 ? strtoull(argv[4], 0, 10) : 1; + build_group(); build_factors(); build_hash(); + int a = flabel[0], b = flabel[1]; + int d = mul_[a][b], c = mul_[mul_[a][b]][mul_[inv_[a]][inv_[b]]]; + printf("A4 c=[%d%d%d%d] d=[%d%d%d%d] (0-based images)\n", perm_[c][0], perm_[c][1], perm_[c][2], + perm_[c][3], perm_[d][0], perm_[d][1], perm_[d][2], perm_[d][3]); + build_S3(); + printf("S3 distinct by minimal length: %u %u %u %u total %u\n", level_count[0], level_count[1], + level_count[2], level_count[3], nstates); + memset(&T, 0, sizeof T); + int planted[7]; + if (!strcmp(mode, "target") || !strcmp(mode, "three")) { + int t[4] = {a, b, c, !strcmp(mode, "three") ? 0 : d}; + for (int i = 0; i < 4; i++) T.m[5 * i] = 1u << t[i]; + } else if (!strcmp(mode, "planted")) { + rng_state = seed * 0x1000003ull + 17; + for (;;) { /* random 7-word whose two length-3 ends are minimal-length-3 classes */ + for (int k = 0; k < 7; k++) planted[k] = (int)(splitmix() % 240); + St p = identity(), s = identity(); + for (int k = 0; k < 3; k++) right_mul(&p, planted[k]); + for (int k = 4; k < 7; k++) right_mul(&s, planted[k]); + int64_t ip = lookup(&p, hash_st(&p)), is = lookup(&s, hash_st(&s)); + if (ip < 0 || is < 0) { fprintf(stderr, "planted lookup failed\n"); exit(3); } + if (level_[ip] == 3 && level_[is] == 3) { forced = ip; break; } + } + T = identity(); + for (int k = 0; k < 7; k++) right_mul(&T, planted[k]); + printf("planted word:"); + for (int k = 0; k < 7; k++) printf(" %d", planted[k]); + printf("\n"); + } else { fprintf(stderr, "mode?\n"); return 2; } + pthread_t th[16]; + for (int t = 0; t < nthreads; t++) pthread_create(&th[t], NULL, worker, (void *)(intptr_t)t); + for (int t = 0; t < nthreads; t++) pthread_join(th[t], NULL); + printf("mode=%s sample=%d processed_len3=%llu children=%llu tag_matches=%llu short_hits=%llu long_hits=%llu\n", + mode, sample, (unsigned long long)processed3, (unsigned long long)children, + (unsigned long long)tag_matches, (unsigned long long)short_hits, (unsigned long long)long_hits); + if (best_len < 99) { + printf("best_word len=%d:", best_len); + for (int k = 0; k < best_len; k++) printf(" %d", best_word[k]); + printf("\n"); + } else printf("best_word none\n"); + return 0; +} diff --git a/research/a4-seven-call-radical-rank/join_b.c b/research/a4-seven-call-radical-rank/join_b.c new file mode 100644 index 0000000000..d445a4b9e6 --- /dev/null +++ b/research/a4-seven-call-radical-rank/join_b.c @@ -0,0 +1,254 @@ +/* join_b.c - independent exact join for the A4 four-role target (right side of length 4). + * + * Different representation from join_a: a state is sum_k [k] (x) M_k with one 4x4 F2 matrix + * M_k per group element k, packed as 16 bits (entry (i,j) at bit 4i+j). The group is generated + * by closure from a and b on packed permutation codes. S3 (distinct products of length <= 3) is + * built by LEFT multiplication; the search runs over the RIGHT end: for every Y in S3, + * R = T Y^-1 in S3 gives a word of length <= 6, and for every Y of minimal length 3 and every + * paid factor f, R D_f^-1 in S3 gives a word X f Y of length <= 7. Nonlinear hash, full compare. + * usage: join_b MODE [threads] [sample] [seed] MODE = target | three | planted + */ +#include +#include +#include +#include +#include + +typedef struct { uint16_t g[12]; } St; /* g[k] = 4x4 F2 matrix coefficient of group element k */ + +static uint8_t code_[12]; /* packed permutation: image of t in bits 2t..2t+1 */ +static int mulk[12][12], invk[12]; /* mulk[p][q] = index of p o q */ +static int nfac = 0, fxs[240], fyx[240], fyb[240], flab[240], la, lb; +static uint16_t fxrep[240], fxspread[240]; + +static int img(uint8_t c, int t) { return c >> (2 * t) & 3; } +static uint8_t comp(uint8_t p, uint8_t q) { /* (p o q)(t) = p(q(t)) */ + uint8_t r = 0; + for (int t = 0; t < 4; t++) r |= (uint8_t)(img(p, img(q, t)) << (2 * t)); + return r; +} +static int gidx(uint8_t c) { + for (int k = 0; k < 12; k++) if (code_[k] == c) return k; + return -1; +} + +static void build(void) { + uint8_t id = 0 | 1 << 2 | 2 << 4 | 3 << 6; + uint8_t a = 1 | 2 << 2 | 0 << 4 | 3 << 6; /* (123): 0->1,1->2,2->0 */ + uint8_t b = 1 | 3 << 2 | 2 << 4 | 0 << 6; /* (124): 0->1,1->3,3->0 */ + int n = 0; code_[n++] = id; + for (int i = 0; i < n; i++) { + uint8_t c1 = comp(code_[i], a), c2 = comp(code_[i], b); + int f1 = 0, f2 = 0; + for (int k = 0; k < n; k++) { f1 |= code_[k] == c1; f2 |= code_[k] == c2; } + if (!f1) code_[n++] = c1; + if (!f2 && c2 != c1) code_[n++] = c2; + if (n > 12) break; + } + if (n != 12) { fprintf(stderr, "closure size %d\n", n); exit(2); } + for (int p = 0; p < 12; p++) + for (int q = 0; q < 12; q++) mulk[p][q] = gidx(comp(code_[p], code_[q])); + for (int p = 0; p < 12; p++) + for (int q = 0; q < 12; q++) if (mulk[p][q] == 0) invk[p] = q; + la = gidx(a); lb = gidx(b); + for (int lab = 0; lab < 2; lab++) + for (int x = 1; x <= 15; x++) + for (int y = 1; y <= 15; y++) { + int par = 0; + for (int t = 0; t < 4; t++) par ^= (x >> t & 1) & (y >> t & 1); + if (!par) continue; + fxs[nfac] = x; fyx[nfac] = y; flab[nfac] = lab ? lb : la; + fxrep[nfac] = (uint16_t)(x * 0x1111); + uint16_t sp = 0; + for (int t = 0; t < 4; t++) if (x >> t & 1) sp |= (uint16_t)(1u << (4 * t)); + fxspread[nfac] = sp; fyb[nfac] = y; nfac++; + } + if (nfac != 240) { fprintf(stderr, "factors %d\n", nfac); exit(2); } +} + +/* row parities of z (bit 4i set iff row i of z has odd weight) */ +static inline uint16_t rowpar(uint16_t z) { z ^= z >> 1; z ^= z >> 2; return z & 0x1111; } + +/* S <- S * D_N(h): (S D)_k = S_k + (S_k + S_{k h^-1}) N, N = x y^T, Z N = rowpar(Z & xrep) * y */ +static void rmul(St *s, int f, int h) { + St o = *s; + int hi = invk[h]; + for (int k = 0; k < 12; k++) { + uint16_t z = o.g[k] ^ o.g[mulk[k][hi]]; + s->g[k] = o.g[k] ^ (uint16_t)(rowpar(z & fxrep[f]) * fyb[f]); + } +} +/* S <- D_N(h) * S: (D S)_k = S_k + N (S_k + S_{h^-1 k}), N Z = (y^T Z) placed in rows of x */ +static void lmul(St *s, int f, int h) { + St o = *s; + int hi = invk[h]; + for (int k = 0; k < 12; k++) { + uint16_t z = o.g[k] ^ o.g[mulk[hi][k]]; + uint16_t r = 0; + for (int t = 0; t < 4; t++) if (fyx[f] >> t & 1) r ^= (uint16_t)(z >> (4 * t) & 15); + s->g[k] = o.g[k] ^ (uint16_t)(r * fxspread[f]); + } +} + +static uint64_t hst(const St *s) { + uint64_t w[3]; + memcpy(w, s->g, 24); + uint64_t h = w[0] * 0xD6E8FEB86659FD93ull; + h ^= h >> 32; h += w[1] * 0xA0761D6478BD642Full; + h ^= h >> 29; h += w[2] * 0xE7037ED1A0B428DBull; + h ^= h >> 32; h *= 0x8EBC6AF09C88C6E3ull; h ^= h >> 31; + return h; +} + +#define TB 24 +#define TS (1u << TB) +#define TM (TS - 1) +#define MAXS 7000000u +static uint64_t *tab; static St *st; static uint8_t *lev; static uint8_t (*wd)[3]; static uint32_t ns; +static uint32_t lcount[4]; +static St T; + +static int64_t find(const St *s, uint64_t h) { + uint32_t p = (uint32_t)(h >> 40) & TM; /* index from high bits, tag from low 32 */ + uint32_t tag = (uint32_t)h; + for (;;) { + uint64_t e = tab[p]; + if (!e) return -1; + if ((uint32_t)(e >> 32) == tag && !memcmp(&st[(uint32_t)e - 1], s, sizeof(St))) return (uint32_t)e - 1; + p = (p + 1) & TM; + } +} +static void put(uint32_t i, uint64_t h) { + uint32_t p = (uint32_t)(h >> 40) & TM; + while (tab[p]) p = (p + 1) & TM; + tab[p] = (uint64_t)(uint32_t)h << 32 | (uint64_t)(i + 1); +} + +static St ident(void) { + St s; memset(&s, 0, sizeof s); s.g[0] = 0x8421; return s; +} + +static void build_S3(void) { + st = malloc(sizeof(St) * MAXS); lev = malloc(MAXS); wd = malloc(3 * (size_t)MAXS); + tab = calloc(TS, 8); + if (!st || !lev || !wd || !tab) { fprintf(stderr, "oom\n"); exit(2); } + St id = ident(); st[0] = id; lev[0] = 0; put(0, hst(&id)); ns = 1; lcount[0] = 1; + uint32_t lo = 0, hi = 1; + for (int L = 1; L <= 3; L++) { + for (uint32_t s = lo; s < hi; s++) + for (int f = 0; f < 240; f++) { + St c = st[s]; lmul(&c, f, flab[f]); /* new = D_f * old: word = f, old word */ + uint64_t h = hst(&c); + if (find(&c, h) >= 0) continue; + if (ns >= MAXS) { fprintf(stderr, "MAXS\n"); exit(2); } + st[ns] = c; lev[ns] = (uint8_t)L; wd[ns][0] = (uint8_t)f; + for (int k = 0; k < L - 1; k++) wd[ns][k + 1] = wd[s][k]; + put(ns, h); ns++; + } + lo = hi; hi = ns; lcount[L] = hi - lo; + } +} + +static int prod_eq(const int *w, int n, const St *t) { + St s = ident(); + for (int k = n - 1; k >= 0; k--) lmul(&s, w[k], flab[w[k]]); + return !memcmp(&s, t, sizeof(St)); +} + +static int nth = 2, samp = 1; static int64_t forced = -1; +static pthread_mutex_t mu = PTHREAD_MUTEX_INITIALIZER; +static uint64_t n_short, n_long, n_child, n_y3; +static int best = 99, bw[8]; + +static void rec(const int *w, int n) { + pthread_mutex_lock(&mu); + if (n < best) { best = n; memcpy(bw, w, sizeof(int) * n); } + pthread_mutex_unlock(&mu); +} + +static void *work(void *arg) { + int tid = (int)(intptr_t)arg; + uint64_t cs = 0, cl = 0, cc = 0, c3 = 0; + St *kid = malloc(sizeof(St) * 240); uint64_t hk[240]; + for (uint32_t yi = (uint32_t)tid; yi < ns; yi += (uint32_t)nth) { + if (samp > 1 && yi % (uint32_t)samp && (int64_t)yi != forced) continue; + St R = T; + int L = lev[yi]; + for (int k = L - 1; k >= 0; k--) { int f = wd[yi][k]; rmul(&R, f, invk[flab[f]]); } /* R = T Y^-1 */ + int64_t xi = find(&R, hst(&R)); + if (xi >= 0) { + int w[8], n = 0; + for (int k = 0; k < lev[xi]; k++) w[n++] = wd[xi][k]; + for (int k = 0; k < L; k++) w[n++] = wd[yi][k]; + if (!prod_eq(w, n, &T)) { fprintf(stderr, "short replay failed\n"); exit(3); } + cs++; rec(w, n); + } + if (L != 3) continue; + c3++; + for (int f = 0; f < 240; f++) { + kid[f] = R; rmul(&kid[f], f, invk[flab[f]]); /* R D_f^-1 */ + hk[f] = hst(&kid[f]); + __builtin_prefetch(&tab[(uint32_t)(hk[f] >> 40) & TM]); + } + for (int f = 0; f < 240; f++) { + cc++; + int64_t x = find(&kid[f], hk[f]); + if (x < 0) continue; + int w[8], n = 0; + for (int k = 0; k < lev[x]; k++) w[n++] = wd[x][k]; + w[n++] = f; + for (int k = 0; k < 3; k++) w[n++] = wd[yi][k]; + if (!prod_eq(w, n, &T)) { fprintf(stderr, "long replay failed\n"); exit(3); } + cl++; rec(w, n); + } + } + free(kid); + pthread_mutex_lock(&mu); + n_short += cs; n_long += cl; n_child += cc; n_y3 += c3; + pthread_mutex_unlock(&mu); + return NULL; +} + +int main(int argc, char **argv) { + const char *mode = argc > 1 ? argv[1] : "target"; + if (argc > 2) nth = atoi(argv[2]); + if (argc > 3) samp = atoi(argv[3]); + uint64_t seed = argc > 4 ? strtoull(argv[4], 0, 10) : 1; + build(); + int c = mulk[mulk[la][lb]][mulk[invk[la]][invk[lb]]], d = mulk[la][lb]; + build_S3(); + printf("S3 distinct by minimal length: %u %u %u %u total %u\n", lcount[0], lcount[1], lcount[2], lcount[3], ns); + memset(&T, 0, sizeof T); + if (!strcmp(mode, "target") || !strcmp(mode, "three")) { + int lab[4] = {la, lb, c, !strcmp(mode, "three") ? 0 : d}; + for (int i = 0; i < 4; i++) T.g[lab[i]] |= (uint16_t)(1u << (5 * i)); + } else if (!strcmp(mode, "planted")) { + uint64_t z = seed * 0x9E3779B97F4A7C15ull + 0x1234567ull; + int pw[7]; + for (;;) { + for (int k = 0; k < 7; k++) { z ^= z << 13; z ^= z >> 7; z ^= z << 17; pw[k] = (int)(z % 240); } + St p = ident(), s = ident(); /* p = product of pw[0..2], s = product of pw[4..6] */ + for (int k = 2; k >= 0; k--) lmul(&p, pw[k], flab[pw[k]]); + for (int k = 6; k >= 4; k--) lmul(&s, pw[k], flab[pw[k]]); + int64_t ip = find(&p, hst(&p)), is = find(&s, hst(&s)); + if (ip < 0 || is < 0) { fprintf(stderr, "planted lookup failed\n"); exit(3); } + if (lev[ip] == 3 && lev[is] == 3) { forced = is; break; } + } + T = ident(); + for (int k = 6; k >= 0; k--) lmul(&T, pw[k], flab[pw[k]]); + printf("planted word:"); + for (int k = 0; k < 7; k++) printf(" %d", pw[k]); + printf("\n"); + } else { fprintf(stderr, "mode?\n"); return 2; } + pthread_t th[16]; + for (int t = 0; t < nth; t++) pthread_create(&th[t], NULL, work, (void *)(intptr_t)t); + for (int t = 0; t < nth; t++) pthread_join(th[t], NULL); + printf("mode=%s sample=%d processed_len3=%llu children=%llu short_hits=%llu long_hits=%llu\n", mode, samp, + (unsigned long long)n_y3, (unsigned long long)n_child, (unsigned long long)n_short, (unsigned long long)n_long); + if (best < 99) { + printf("best_word len=%d:", best); + for (int k = 0; k < best; k++) printf(" %d", bw[k]); + printf("\n"); + } else printf("best_word none\n"); + return 0; +} diff --git a/research/a4-seven-call-radical-rank/verify.py b/research/a4-seven-call-radical-rank/verify.py new file mode 100644 index 0000000000..76cdd290ed --- /dev/null +++ b/research/a4-seven-call-radical-rank/verify.py @@ -0,0 +1,421 @@ +#!/usr/bin/env python3 +"""Replay the A4 four-role exact minimum: radical-rank lemma, controls and two exact joins. + +Standard library only. Needs a C compiler (cc or gcc) with POSIX threads for the joins. +Prepared by Sagar Thakrar (thakrarsagar) with substantial AI assistance from Claude +(Anthropic, Claude Opus 5.5). Apache-2.0. +""" + +from __future__ import annotations + +import itertools +import json +import random +import re +import shutil +import subprocess +import tempfile +from pathlib import Path + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] +PRED = ROOT / "research/a4-commutator-four-role-seed-dcbf/RESULT.json" + +# ---------------------------------------------------------------- group A4 and F2[A4] +PERMS = sorted(p for p in itertools.permutations(range(4)) + if sum(p[i] > p[j] for i in range(4) for j in range(i + 1, 4)) % 2 == 0) +IDX = {p: k for k, p in enumerate(PERMS)} +ONE = IDX[(0, 1, 2, 3)] +MUL = [[IDX[tuple(p[q[t]] for t in range(4))] for q in PERMS] for p in PERMS] # (p o q)(t)=p(q(t)) +INV = [next(j for j in range(12) if MUL[i][j] == ONE) for i in range(12)] +A, B = IDX[(1, 2, 0, 3)], IDX[(1, 3, 2, 0)] # a=(123), b=(124) +D = MUL[A][B] # d = ab = (13)(24) +C = MUL[MUL[A][B]][MUL[INV[A]][INV[B]]] # c = a b a^-1 b^-1 = (12)(34) +E = MUL[B][A] # e = ba = (14)(23) +V4 = [ONE, C, D, E] +COSET = {MUL[p][v]: i for i, p in enumerate([ONE, A, MUL[A][A]]) for v in V4} # k in a^i V4 + + +def amul(x: int, y: int) -> int: + """Product in F2[A4]; elements are 12-bit masks over PERMS.""" + out = 0 + for i in range(12): + if x >> i & 1: + for j in range(12): + if y >> j & 1: + out ^= 1 << MUL[i][j] + return out + + +def g(k: int) -> int: + return 1 << k + + +def pi(x: int) -> int: + """Image in F2[A4/V4] = F2[C3], as a 3-bit mask over the cosets V4, aV4, a^2V4.""" + out = 0 + for k in range(12): + if x >> k & 1: + out ^= 1 << COSET[k] + return out + + +def mat_id() -> list[list[int]]: + return [[g(ONE) if i == j else 0 for j in range(4)] for i in range(4)] + + +def mat_mul(X, Y): + out = [[0] * 4 for _ in range(4)] + for i in range(4): + for j in range(4): + acc = 0 + for k in range(4): + if X[i][k] and Y[k][j]: + acc ^= amul(X[i][k], Y[k][j]) + out[i][j] = acc + return out + + +# paid factors: id = 120*gi + n, (x, y) x-major, y ascending, popcount(x&y) odd +PAIRS = [(x, y) for x in range(1, 16) for y in range(1, 16) if bin(x & y).count("1") % 2] +assert len(PAIRS) == 120 + + +def factor_matrix(x: int, y: int, label: int): + """D_N(label) = I + ([label]+[1]) x y^T.""" + s = g(label) ^ g(ONE) + M = mat_id() + for i in range(4): + for j in range(4): + if x >> i & 1 and y >> j & 1: + M[i][j] ^= s + return M + + +FACTORS = [factor_matrix(x, y, A if gi == 0 else B) for gi in range(2) for (x, y) in PAIRS] + + +def word_product(word): + M = mat_id() + for f in word: + M = mat_mul(M, FACTORS[f]) + return M + + +def target(labels): + T = [[0] * 4 for _ in range(4)] + for i, lab in enumerate(labels): + T[i][i] = g(lab) + return T + + +TARGET = target([A, B, C, D]) +THREE = target([A, B, C, ONE]) +DIRECT = [0, 128, 24, 144, 144, 24, 56, 176] + + +def regular_replay(M, T) -> int: + """Apply both matrices to all 48 role/address basis inputs e_j [h]; count agreements.""" + ok = 0 + for j in range(4): + for h in range(12): + if all(amul(M[i][j], g(h)) == amul(T[i][j], g(h)) for i in range(4)): + ok += 1 + return ok + + +# ---------------------------------------------------------------- F4 linear algebra +# F4 = {0,1,w,w^2} coded 0,1,2,3; addition is XOR. +F4MUL = [[0, 0, 0, 0], [0, 1, 2, 3], [0, 2, 3, 1], [0, 3, 1, 2]] +F4INV = {1: 1, 2: 3, 3: 2} +W = 2 +WPOW = [1, 2, 3] + + +def f4_rank(M) -> int: + M = [row[:] for row in M] + rank = 0 + for col in range(len(M[0])): + piv = next((r for r in range(rank, len(M)) if M[r][col]), None) + if piv is None: + continue + M[rank], M[piv] = M[piv], M[rank] + inv = F4INV[M[rank][col]] + M[rank] = [F4MUL[inv][v] for v in M[rank]] + for r in range(len(M)): + if r != rank and M[r][col]: + fac = M[r][col] + M[r] = [v ^ F4MUL[fac][w] for v, w in zip(M[r], M[rank])] + rank += 1 + return rank + + +def f4_matmul(X, Y): + out = [[0] * len(Y[0]) for _ in range(len(X))] + for i in range(len(X)): + for k in range(len(Y)): + if X[i][k]: + for j in range(len(Y[0])): + out[i][j] ^= F4MUL[X[i][k]][Y[k][j]] + return out + + +def f4_inverse(M): + n = len(M) + aug = [row[:] + [1 if i == j else 0 for j in range(n)] for i, row in enumerate(M)] + for col in range(n): + piv = next(r for r in range(col, n) if aug[r][col]) + aug[col], aug[piv] = aug[piv], aug[col] + inv = F4INV[aug[col][col]] + aug[col] = [F4MUL[inv][v] for v in aug[col]] + for r in range(n): + if r != col and aug[r][col]: + fac = aug[r][col] + aug[r] = [v ^ F4MUL[fac][w] for v, w in zip(aug[r], aug[col])] + return [row[n:] for row in aug] + + +# ---------------------------------------------------------------- the radical-rank lemma +class Base: + """Lemma data for a base generator s in {a, b}; the other generator is s^2 v, v in V4.""" + + def __init__(self, s: int, other: int): + self.s = s + self.powers = [ONE, s, MUL[s][s]] + self.v_other = MUL[INV[MUL[s][s]]][other] + assert self.v_other in V4 and self.v_other != ONE + + def conj(v): + return MUL[MUL[INV[s]][v]][s] + + # mu: V4 -> F4 is F2-linear and conjugation-equivariant: mu(s^-1 v s) = w mu(v) + self.mu = {ONE: 0, C: 1, conj(C): W, conj(conj(C)): F4MUL[W][W]} + assert sorted(self.mu) == sorted(V4) + self.vpart = {} + for p in self.powers: + for v in V4: + self.vpart[MUL[p][v]] = v # g = s^i v + assert len(self.vpart) == 12 + + def phi(self, x: int) -> int: + out = 0 + for k in range(12): + if x >> k & 1: + out ^= self.mu[self.vpart[k]] + return out + + def aug(self, r: int) -> int: # trivial character of F2[] + return sum(r >> p & 1 for p in self.powers) % 2 + + def psi(self, r: int) -> int: # character s -> w of F2[] + out = 0 + for i, p in enumerate(self.powers): + if r >> p & 1: + out ^= WPOW[i] + return out + + def in_sub(self, r: int) -> bool: + return all(not (r >> k & 1) or k in self.powers for k in range(12)) + + +def sub_inverse(word, is_other, base): + """Inverse of the F2[]-part product P1...Pn, using D_N(t)^-1 = D_N(t^-1).""" + inv = mat_id() + for f, o in zip(word, is_other): + x, y = PAIRS[f % 120] + t = MUL[base.s][base.s] if o else base.s + inv = mat_mul(factor_matrix(x, y, INV[t]), inv) + return inv + + +def lemma_checks() -> dict: + out = {} + J_basis = [g(MUL[p][v]) ^ g(p) for p in [ONE, A, MUL[A][A]] for v in [C, D, E]] + J_all = {0} + for y in J_basis: + J_all |= {z ^ y for z in J_all} + assert len(J_all) == 512 and all(pi(y) == 0 for y in J_all) + assert sum(1 for x in range(4096) if pi(x) == 0) == 512 # J = ker pi exactly + for name, s, other in (("a", A, B), ("b", B, A)): + base = Base(s, other) + sub = [r for r in range(1 << 12) if base.in_sub(r)] + assert len(sub) == 8 + # (1) F2[] meets J only in 0, so a lift mod J into M4(F2[]) is unique + assert [r for r in sub if pi(r) == 0] == [0] + # (2) D_N(other) = D_N(s^2) D_N(v_other) for all 120 rank-one idempotents N + for (x, y) in PAIRS: + rhs = mat_mul(factor_matrix(x, y, MUL[s][s]), factor_matrix(x, y, base.v_other)) + assert factor_matrix(x, y, other) == rhs + # (3) Phi(r y t) = aug(r) Phi(y) psi(t) on J, Phi(J^2) = 0, Phi(v+1) != 0 for v != 1 + for y in J_all: + py = base.phi(y) + for r in sub: + ry = amul(r, y) + for t in sub: + assert base.phi(amul(ry, t)) == F4MUL[F4MUL[base.aug(r)][py]][base.psi(t)] + for y1 in J_basis: + for y2 in J_basis: + assert base.phi(amul(y1, y2)) == 0 + assert all(base.phi(g(v) ^ g(ONE)) for v in (C, D, E)) + # (4) unique lift of T mod J and the radical defect U - I = lift^-1 T - I + def defect_rank(labels): + lift = [] + for lab in labels: + cands = [r for r in sub if pi(r) == pi(g(lab))] + assert len(cands) == 1 + lift.append(cands[0]) + lift_inv = [next(r for r in sub if amul(r, l) == g(ONE)) for l in lift] + defect = [amul(lift_inv[i], g(lab)) ^ g(ONE) for i, lab in enumerate(labels)] + assert all(pi(x) == 0 for x in defect) + return f4_rank([[base.phi(defect[i]) if i == j else 0 for j in range(4)] for i in range(4)]) + + rank = defect_rank([A, B, C, D]) + rank3 = defect_rank([A, B, C, ONE]) + assert rank == 3 and rank3 == 2 + out[f"base_{name}"] = { + "other_label_split": f"{'b' if name == 'a' else 'a'} = {name}^2 * {''.join(map(str, PERMS[base.v_other]))}", + "defect_rank_target": rank, "defect_rank_three_output_control": rank3, + "bound": f"n_{'b' if name == 'a' else 'a'} >= {rank}"} + # (5) random words: Phi(A^-1 W - I) = sum_k aug(C_k)^-1 mu(v) N_k psi(C_k); rank <= #other + rng = random.Random(20261019 + s) + for _ in range(60): + word = [rng.randrange(240) for _ in range(rng.randrange(1, 9))] + is_other = [(f >= 120) == (name == "a") for f in word] + parts = [] + for f, o in zip(word, is_other): + x, y = PAIRS[f % 120] + parts.append(factor_matrix(x, y, MUL[s][s] if o else s)) + Wm = word_product(word) + Am = mat_id() + for P in parts: + Am = mat_mul(Am, P) + assert all(base.in_sub(Am[i][j]) for i in range(4) for j in range(4)) + assert all(pi(Wm[i][j]) == pi(Am[i][j]) for i in range(4) for j in range(4)) + Ainv = sub_inverse(word, is_other, base) + assert mat_mul(Ainv, Am) == mat_id() + U = mat_mul(Ainv, Wm) + lhs = [[base.phi(U[i][j] ^ (g(ONE) if i == j else 0)) for j in range(4)] for i in range(4)] + rhs = [[0] * 4 for _ in range(4)] + for k, (f, o) in enumerate(zip(word, is_other)): + if not o: + continue + Ck = mat_id() + for P in parts[k + 1:]: + Ck = mat_mul(Ck, P) + aug_inv = f4_inverse([[base.aug(Ck[i][j]) for j in range(4)] for i in range(4)]) + psiC = [[base.psi(Ck[i][j]) for j in range(4)] for i in range(4)] + x, y = PAIRS[f % 120] + Nk = [[base.mu[base.v_other] if (x >> i & 1 and y >> j & 1) else 0 for j in range(4)] + for i in range(4)] + term = f4_matmul(f4_matmul(aug_inv, Nk), psiC) + rhs = [[rhs[i][j] ^ term[i][j] for j in range(4)] for i in range(4)] + assert lhs == rhs + assert f4_rank(lhs) <= sum(is_other) + out[f"base_{name}"]["random_word_identity_checks"] = 60 + return out + + +def det_check() -> None: + """C3 determinant: det over F2[C3] of a word is t^(n_a - n_b); the target has det 1.""" + def cm(x, y): + out = 0 + for i in range(3): + if x >> i & 1: + for j in range(3): + if y >> j & 1: + out ^= 1 << ((i + j) % 3) + return out + + def det(M): + total = 0 + for p in itertools.permutations(range(4)): + term = 1 + for i in range(4): + term = cm(term, M[i][p[i]]) + total ^= term + return total + + assert COSET[A] == 1 and COSET[B] == 2 + rng = random.Random(7) + for _ in range(200): + word = [rng.randrange(240) for _ in range(rng.randrange(0, 9))] + Wm = word_product(word) + na = sum(f < 120 for f in word) + assert det([[pi(Wm[i][j]) for j in range(4)] for i in range(4)]) == 1 << ((2 * na - len(word)) % 3) + assert det([[pi(TARGET[i][j]) for j in range(4)] for i in range(4)]) == 1 + + +# ---------------------------------------------------------------- C joins +def compile_join(src: Path, out: Path) -> None: + cc = shutil.which("cc") or shutil.which("gcc") + assert cc, "a C compiler is required" + subprocess.run([cc, "-std=c11", "-O3", "-Wall", "-Wextra", "-Werror", "-pthread", + "-o", str(out), str(src)], check=True) + + +def run_join(exe: Path, *args: str) -> dict: + proc = subprocess.run([str(exe), *args], check=True, capture_output=True, text=True, timeout=500) + text = proc.stdout + s3 = re.search(r"S3 distinct by minimal length: (\d+) (\d+) (\d+) (\d+) total (\d+)", text) + stats = re.search(r"processed_len3=(\d+) children=(\d+).*short_hits=(\d+) long_hits=(\d+)", text) + best = re.search(r"best_word (none|len=(\d+):([\d ]+))", text) + planted = re.search(r"planted word:([\d ]+)", text) + return { + "s3": [int(v) for v in s3.groups()], + "processed_len3": int(stats.group(1)), "children": int(stats.group(2)), + "short_hits": int(stats.group(3)), "long_hits": int(stats.group(4)), + "best": None if best.group(1) == "none" else [int(v) for v in best.group(3).split()], + "planted": None if not planted else [int(v) for v in planted.group(1).split()], + } + + +def main() -> None: + pred = json.loads(PRED.read_text()) + report: dict = {} + assert (PERMS[C], PERMS[D], PERMS[E]) == ((1, 0, 3, 2), (2, 3, 0, 1), (3, 2, 1, 0)) + assert C == MUL[MUL[A][B]][MUL[B][A]] # c = abba in this presentation + assert DIRECT == pred["direct_word"]["factor_ids_in_search_alphabet"] + M = word_product(DIRECT) + assert M == TARGET and regular_replay(M, TARGET) == 48 + omissions = sum(word_product(DIRECT[:k] + DIRECT[k + 1:]) != TARGET for k in range(8)) + assert omissions == 8 + mutated = DIRECT[:7] + [56] # last call b -> a on role 4 + assert regular_replay(word_product(mutated), TARGET) < 48 + report["direct_word"] = {"paid_calls": 8, "regular_inputs_checked": 48, + "single_omissions_rejected": omissions, "mutated_label_rejected": True} + det_check() + report["c3_determinant"] = "n_a = n_b mod 3 for every word equal to the target (200 random-word checks)" + report["radical_rank_lemma"] = lemma_checks() + threads = "2" + with tempfile.TemporaryDirectory() as tmp: + exe_a, exe_b = Path(tmp) / "join_a", Path(tmp) / "join_b" + compile_join(PACKAGE / "join_a.c", exe_a) + compile_join(PACKAGE / "join_b.c", exe_b) + expected_s3 = [1, 240, 41920, 6655830, 6697991] + joins = {} + for name, exe in (("join_a", exe_a), ("join_b", exe_b)): + res = run_join(exe, "target", threads, "1") + assert res["s3"] == expected_s3, res + assert res["s3"][4] == pred["exact_join"]["right_distinct_exact_states"] + assert res["processed_len3"] == 6655830 and res["children"] == 6655830 * 240 + assert res["short_hits"] == 0 and res["long_hits"] == 0 and res["best"] is None + three = run_join(exe, "three", threads, "64") + assert three["short_hits"] >= 1 and len(three["best"]) == 6 + assert word_product(three["best"]) == THREE + planted_found = 0 + for seed in ("1", "2"): + pl = run_join(exe, "planted", threads, "64", seed) + assert pl["long_hits"] >= 1 and len(pl["best"]) == 7 + assert word_product(pl["best"]) == word_product(pl["planted"]) + planted_found += 1 + joins[name] = {"no_word_through_length": 7, "len3_classes_expanded": res["processed_len3"], + "children_checked": res["children"], "three_output_6word": three["best"], + "planted_7words_found": planted_found} + report["joins"] = joins + report["result"] = "PASS_A4_FOUR_ROLE_EXACT_MINIMUM_EIGHT" + print(json.dumps(report, indent=1, sort_keys=True)) + print("PASS_A4_FOUR_ROLE_EXACT_MINIMUM_EIGHT") + + +if __name__ == "__main__": + main() From f257bd837d39a2172e8fefaec45e9b37112ebdf7 Mon Sep 17 00:00:00 2001 From: Sagar Thakrar <18622288+thakrarsagar@users.noreply.github.com> Date: Mon, 19 Oct 2026 16:21:22 +0530 Subject: [PATCH 2/2] Revise A4 seven-call package after review round 1 Scope the "why 8" sentence to length 7 (length 6 is search-only), fix the per-role rank wording, add the free scalar mixing and extra identity-role remarks, state the per-label radical-rank floor over F2[A4], rename the product set to P<=3, cite PRs #2047/#2248/#2085/#2010/#3893 with authors, hedge novelty, describe the joins as separately implemented in one session, record the Python 3.12.15 runner pass, and fix the c3_determinant report string. Verifier rerun: PASS_A4_FOUR_ROLE_EXACT_MINIMUM_EIGHT (82 s, 369 MB). Co-Authored-By: Claude Opus 5.5 --- research/a4-seven-call-radical-rank/README.md | 119 ++++++++++++------ research/a4-seven-call-radical-rank/TASK.json | 8 +- .../a4-seven-call-radical-rank/VERIFY.json | 2 +- research/a4-seven-call-radical-rank/verify.py | 8 +- 4 files changed, 91 insertions(+), 46 deletions(-) diff --git a/research/a4-seven-call-radical-rank/README.md b/research/a4-seven-call-radical-rank/README.md index a2da1ee187..ab5ea83019 100644 --- a/research/a4-seven-call-radical-rank/README.md +++ b/research/a4-seven-call-radical-rank/README.md @@ -5,16 +5,16 @@ every word realizing `T = diag([a],[b],[c],[d])` uses at least three `a`-calls and at least three `b`-calls, and the numbers of `a`- and `b`-calls agree modulo 3. A written proof therefore excludes length 7 and every length up to 5. -Length 6 would need exactly three calls of each label. Two independently -written exhaustive joins exclude every word of length up to 7, including that -case. Together with the direct eight-call word, this gives an **exact minimum +Length 6 would need exactly three calls of each label. Two exhaustive joins, +implemented separately in the same session, exclude every word of length up +to 7, including that case. Together with the direct eight-call word, this gives an **exact minimum of 8**. The model has no cross-role paid-call saving for this target. | Length | Status | Evidence | |---|---|---| | 1-5 | impossible | written proof (Lemmas 1-2); also both joins | | 6 | impossible | exhaustive joins A and B (reproduces #2116); not covered by the written lemmas | -| 7 | impossible | written proof (Lemmas 1-2); independently both exhaustive joins | +| 7 | impossible | written proof (Lemmas 1-2); also both exhaustive joins | | 8 | realized | direct word (`a`, `b`, `abba`, `ab` on roles 1-4), replayed exactly on all 48 basis inputs | The evidence has three different kinds. For length 7 and lengths up to 5 it is @@ -22,6 +22,15 @@ a proof of impossibility. For length 6 it is a finite exhaustive certificate. For length 8 it is an explicit construction. None of these is a multiplication theorem, a supplier result or a `kappa` change. +**New here: a per-label radical-rank floor over `F2[A4]`.** Steps 1-5 below use +nothing specific to `T` beyond its lift modulo the radical `J` and the +resulting defect. So, in this alphabet with any number `r` of roles, every word equal to a target +`T in GL_r(F2[A4])` has `n_b >= rank_F4 Phi(L^-1 T - I)`, where `L` is the unique +lift of `T mod J` into `GL_r(F2[])`; symmetrically for `n_a` with base `b`. +The verifier checks this floor (at `r = 4`) on random words and on two targets: +rank 3 for `T`, rank 2 for the three-output control. Whether it extends beyond +`A4 = V x| C3` is open question 2. + ## Model The model is unchanged from #2116. Take `a=(123)`, `b=(124)`, @@ -41,6 +50,13 @@ when the 4x4 product over `F2[A4]` equals `T` in every formal coefficient. The model has four roles, allows arbitrary dirty inputs and has no workspace. Each call costs one, and no helper, copy or restoration operation is charged. +Free scalar mixing does not change the answer. Suppose free matrices +`G_i in GL4(F2)`, including role permutations, may be interleaved with the +paid calls. Conjugate each one to the left: `G^-1 D_N(g) G = D_{G^-1 N G}(g)` +is again a paid factor, so `W = H * W'` with `W'` a pure paid word of the same +length and `H in GL4(F2)`. Entrywise augmentation gives `aug(D_N(g)) = I` and +`aug(T) = I`, so `H = I`. The search over pure paid words is therefore complete. + ## Proof Write `n_a` and `n_b` for the numbers of `a`- and `b`-calls in a word. @@ -104,20 +120,28 @@ At length 7, Lemma 1 allows only `(2,5)` and `(5,2)`, and Lemma 2 rules out both. The exhaustive joins below exclude length 6, and the direct word has length 8. The exact minimum is 8. -Lemma 2 explains why the direct word is optimal. Each target role in `V` -contributes an independent rank to the radical layer. Every call of the other -label can pay at most one unit of that rank, after any conjugation by the -semisimple part. The C3 determinant then rules out the one unbalanced split -that would save a call. +Lemmas 1-2 explain why no one-call saving (length 7) exists; length 6 is +excluded only by exhaustive search. Each role whose label is not a power of the +base generator contributes one independent rank unit through its +`V`-component: roles 2, 3 and 4 in base `a`, roles 1, 3 and 4 in base `b`. +Every call of the other label can pay at most one unit of that rank, after any +conjugation by the semisimple part. The C3 determinant then rules out the +unbalanced splits `(2,5)` and `(5,2)`. + +The written exclusion of length 7 and of lengths up to 5 also holds with any +number of additional dirty roles whose target is `1`: the defect becomes +`diag(1,d,c,d,1,...,1)`, still of rank 3, and the target determinant is still +1. Length 6 is certified only for four roles. -## Independent exhaustive joins +## Separately implemented exhaustive joins -Both programs build `S3`, the distinct products of length at most 3. They +Both programs build `P<=3`, the distinct products of length at most 3 (the C +output and #2116 call this set `S3`; it is unrelated to the ring `S` above). They deduplicate by the full 4x4 state of 12-bit coefficients and keep each state's -minimal length. Any word of length at most 6 is `X Y` with `X` and `Y` in `S3`. +minimal length. Any word of length at most 6 is `X Y` with `X` and `Y` in `P<=3`. A word of length 7 is `X f Y`, where `X` can be taken to have minimal length exactly 3; otherwise a shorter word would exist. So each join tests -`X^-1 T in S3` for every `X`, and tests `f^-1 X^-1 T in S3` for every +`X^-1 T in P<=3` for every `X`, and tests `f^-1 X^-1 T in P<=3` for every minimal-length-3 class `X` and every factor `f`. That covers all lengths through 7. @@ -125,16 +149,16 @@ through 7. |---|---|---| | state representation | 4x4 matrix of 12-bit masks over `A4` | 12 coefficient matrices `M_g` in `M4(F2)`, 16 bits each | | group construction | all even permutations | closure of `` on packed codes | -| `S3` built by | right multiplication | left multiplication | +| `P<=3` built by | right multiplication | left multiplication | | enumerated end | left: `X^-1 T`, then `D_f^-1 (X^-1 T)` | right: `T Y^-1`, then `(T Y^-1) D_f^-1` | | hash | `GF(2)`-linear (child hashes by XOR) | nonlinear multiply-xorshift | -| distinct `S3` states by minimal length | 1, 240, 41,920, 6,655,830 (total 6,697,991) | identical | +| distinct `P<=3` states by minimal length | 1, 240, 41,920, 6,655,830 (total 6,697,991) | identical | | minimal-length-3 classes expanded | 6,655,830 | 6,655,830 | | children looked up | 1,597,399,200 | 1,597,399,200 | | words of length at most 7 found | none | none | | local wall time / peak RSS (2 threads, `-march=native` development build) | 27 s / 369 MB | 39 s / 316 MB | -The `S3` total, 6,697,991, matches #2116's `right_distinct_exact_states`. The +The `P<=3` total, 6,697,991, matches #2116's `right_distinct_exact_states`. The verifier reads that value from the pinned predecessor `RESULT.json`. Every reported hit is confirmed in C, by comparing full states and multiplying out the word. Python then replays it independently. The Python code does not reuse @@ -171,9 +195,11 @@ python3 scripts/research_package.py --package research/a4-seven-call-radical-ran ``` The expected final line is `PASS_A4_FOUR_ROLE_EXACT_MINIMUM_EIGHT`, preceded by -a JSON report with the counts above. The local run took 79 s wall time with -369 MB peak RSS. It used Python 3.14.4 and gcc 15.2.0 on 4 shared CPUs. The -generic runner requests Python 3.12, which was not used locally. +a JSON report with the counts above. Local runs took about 80-90 s wall time +with 369 MB peak RSS, using Python 3.14.4 and gcc 15.2.0 on 4 shared CPUs. The +generic runner `scripts/research_package.py --package +research/a4-seven-call-radical-rank` also passed under a private Python 3.12.15 +(`PASS_REGISTERED_RESEARCH_PACKAGE`, 84 s, 369 MB). ## Scope, inherited assumptions and unresolved obligations @@ -186,10 +212,13 @@ generic runner requests Python 3.12, which was not used locally. restored workspace, a physical caller, chronology, hosting, precision, recursive transfer and supplier admission. These costs are unknown, not zero. -- Decision consequence: the A4 four-role endpoint gives no formal saving. The - nonabelian-register route through this target therefore does not merit a - priced native-conversion step. A 7-word would have saved 1 of 8 calls in the - formal model only. +- Decision consequence: the A4 four-role endpoint gives no formal saving, so + this target gives no reason to price a native conversion of `F2[A4]` calls. + The package closes #2116's named open question and extends the existing + direct-optimal pattern of the formal finite-group family (for example `Q8` + in #2047 and #2248, `SL2(F3)` in #2010) to one more target. It changes no + current lead, supplier or selected result. A 7-word would have saved 1 of 8 + calls in the formal model only. ## Open next questions @@ -203,11 +232,13 @@ The same questions are structured in [TASK.json](TASK.json). the two bases, or at the `J^2` layer. Blocked by: nothing beyond the bookkeeping. 2. **Does the radical-rank bound extend to `G = P x| H`, with `P` a normal - 2-group and `H` of odd order?** Examples include more roles over `A4`, or - `SL2(F3)`. The goal is uniform label-count floors in place of censuses. + 2-group and `H` of odd order?** An example is + `SL2(F3) = Q8 x| C3`. The goal is uniform label-count floors in place of censuses. First step: state the lemma with `S = F2[H]` and an equivariant functional - `mu` on the Frattini quotient of `P`, then test it against an existing finite census. Blocked - by: nothing for the formal statement. Native conversion stays unpriced. + `mu` on the Frattini quotient of `P`, then test it against the existing + `SL2(F3)` census of [PR #2010](https://github.com/CrocSwap/integer-mult-bounds/pull/2010) + (`research/sl2f3-conjugate-triple-seed592f`). Blocked by: nothing for the + formal statement. Native conversion stays unpriced. ## Predecessors and attribution @@ -218,20 +249,34 @@ The same questions are structured in [TASK.json](TASK.json). Discussion [#2095](https://github.com/CrocSwap/integer-mult-bounds/discussions/2095)). This package answers that package's named open question. It re-proves the length-6 exclusion with new code and does not modify the predecessor. -- The untwisted `J/J^2` coefficient-matrix argument for the 2-group `Q8`, in - `research/q8-central-minus-one-any-registers-seed0332f4` and - `research/q8-r3-two-central-one-generator-seed809fc39d`, is the closest - prior technique. The new ingredients are three. First, splitting off the - semisimple part `F2[]` in a group algebra that is not local. Second, the - twisted functional `Phi` that absorbs conjugation by that part. Third, using - both bases together with the C3 determinant. +- Prior untwisted `J/J^2` arguments, all by GitHub `1337isnot1337` (commit + author Cinna Davis) and merged: the coefficient-matrix argument for the + 2-group `Q8` in [PR #2047](https://github.com/CrocSwap/integer-mult-bounds/pull/2047) + (`research/q8-central-minus-one-any-registers-seed0332f4`, head `46bce88f`) + and [PR #2248](https://github.com/CrocSwap/integer-mult-bounds/pull/2248) + (`research/q8-r3-two-central-one-generator-seed809fc39d`, head `835bd7b1`); + and the abelian four-role rational-frame floor of + [PR #2085](https://github.com/CrocSwap/integer-mult-bounds/pull/2085) + (`research/bit-four-register-rational-frame-floor-seed3573e12e`, head + `5302b9ba`), whose `J/J^2` per-label count with rank-one calls is the closest + analogue of the step-5 rank count. To our knowledge (a search of + `research/*/README.md` and open PRs at base `20ecf289`), three ingredients + here are new: splitting off the semisimple part `F2[]` in a group algebra + that is not local; the twisted functional `Phi` that absorbs conjugation by + that part; and using both bases together with the C3 determinant. The open + [PR #3893](https://github.com/CrocSwap/integer-mult-bounds/pull/3893) + (`1337isnot1337`, S3 three-register rank lower bound) is a concurrent, + different rank floor. - Exact pins are in [SOURCES.json](SOURCES.json). The base is `20ecf2891d80b5acf18d980b2164fb44ea7faa90` and priority revision 6 is in force. The live input is #2116's `RESULT.json`. -Provenance: the lemma, both joins and the verifier were written in one AI-assisted -session. The written proof's steps are each checked numerically by the verifier, -as described above. No independent human review is claimed. +Provenance: the lemma, both joins and the verifier were written in one +AI-assisted session; the two joins are separately implemented, not +independently authored. The written proof's steps are each checked numerically +by the verifier, as described above. The package was reviewed by four +independent AI review passes in the same loop. No independent human review is +claimed. Prepared by Sagar Thakrar (thakrarsagar) with substantial AI assistance from Claude (Anthropic, Claude Opus 5.5). Apache-2.0. diff --git a/research/a4-seven-call-radical-rank/TASK.json b/research/a4-seven-call-radical-rank/TASK.json index 929fdcaefa..5a0699ea8e 100644 --- a/research/a4-seven-call-radical-rank/TASK.json +++ b/research/a4-seven-call-radical-rank/TASK.json @@ -50,9 +50,9 @@ "budget_minutes": 90, "stop_rule": "Submission rule committed before searching: a verified 7-word is submitted; an exact 8 is submitted only with a written structural lemma beyond the C3 determinant screen, otherwise nothing is posted. Stop with no PR if the primary join exceeds ~15 min wall or 1.5 GB RSS, or if the two joins disagree unresolved by the experiment deadline.", "outcome": "negative-result", - "evidence": "Written proof: C3 determinant (n_a = n_b mod 3) plus a radical-rank lemma (n_a >= 3 and n_b >= 3) exclude length 7 and lengths <= 5. Two independently written exhaustive C joins (different state representation, multiplication side, enumerated end and hash) each expand all 6,655,830 minimal-length-3 classes against all 6,697,991 distinct products of length <= 3 (1,597,399,200 lookups each) and find no word of length <= 7, which also excludes length 6. The direct 8-word replays exactly on all 48 basis inputs. Controls: omissions, label mutation, three-output 6-words, planted 7-words, numeric checks of every lemma step. Verifier: research/a4-seven-call-radical-rank/verify.py, PASS_A4_FOUR_ROLE_EXACT_MINIMUM_EIGHT.", + "evidence": "Written proof: C3 determinant (n_a = n_b mod 3) plus a radical-rank lemma (n_a >= 3 and n_b >= 3) exclude length 7 and lengths <= 5. Two exhaustive C joins, separately implemented in the same AI-assisted session (different state representation, multiplication side, enumerated end and hash) each expand all 6,655,830 minimal-length-3 classes against all 6,697,991 distinct products of length <= 3 (1,597,399,200 lookups each) and find no word of length <= 7, which also excludes length 6. The direct 8-word replays exactly on all 48 basis inputs. Controls: omissions, label mutation, three-output 6-words, planted 7-words, numeric checks of every lemma step. Verifier: research/a4-seven-call-radical-rank/verify.py, PASS_A4_FOUR_ROLE_EXACT_MINIMUM_EIGHT.", "author": "Sagar Thakrar (thakrarsagar)", - "ai_assistance": "Substantial AI assistance from Claude (Anthropic, Claude Opus 5.5) in derivation, both C joins, the Python verifier and writing; no independent human review is claimed.", + "ai_assistance": "Substantial AI assistance from Claude (Anthropic, Claude Opus 5.5) in derivation, both C joins, the Python verifier and writing; reviewed by four independent AI review passes in the same loop; no independent human review is claimed.", "open_questions": [ { "question": "Can the length-6 case (n_a,n_b)=(3,3) be excluded by a written argument rather than exhaustive search?", @@ -61,9 +61,9 @@ "blocked_by": "Nothing beyond the bookkeeping." }, { - "question": "Does the radical-rank label-count bound extend to G = P x| H with P a normal 2-group and H of odd order (more roles over A4, SL2(F3))?", + "question": "Does the radical-rank label-count bound extend to G = P x| H with P a normal 2-group and H of odd order (for example SL2(F3) = Q8 x| C3)?", "why_it_matters": "It would replace finite censuses by uniform per-label floors for nonabelian register models.", - "first_step": "State the lemma with S = F2[H] and an H-equivariant functional mu on the Frattini quotient of P, then test it against an existing finite census.", + "first_step": "State the lemma with S = F2[H] and an H-equivariant functional mu on the Frattini quotient of P, then test it against the existing SL2(F3) census of PR #2010 (research/sl2f3-conjugate-triple-seed592f).", "blocked_by": "Nothing for the formal statement; native conversion remains unpriced." } ] diff --git a/research/a4-seven-call-radical-rank/VERIFY.json b/research/a4-seven-call-radical-rank/VERIFY.json index 36ce2b4555..6706c7ad51 100644 --- a/research/a4-seven-call-radical-rank/VERIFY.json +++ b/research/a4-seven-call-radical-rank/VERIFY.json @@ -15,7 +15,7 @@ "{package}/verify.py" ], "timeout_seconds": 600, - "checks": "Exact direct 8-word replay on all 48 basis inputs with 8 omission and 1 label-mutation rejections; C3 determinant on 200 random words; every step of the radical-rank lemma in both bases (factor split for all 120 idempotents, J = kernel of dimension 9, unique lifts, twisted bimodule law on all of J, Phi(J^2)=0, defect rank 3 and three-output control rank 2, step-5 identity on 60 random words per base); compile both C joins with warnings as errors and check S3 counts 1/240/41920/6655830 (total 6697991, equal to PR #2116's pinned value), 1,597,399,200 lookups and no word of length <= 7 in each; three-output 6-word and planted 7-word positive controls in each join, all replayed in Python." + "checks": "Exact direct 8-word replay on all 48 basis inputs with 8 omission and 1 label-mutation rejections; C3 determinant formula on 200 random words; every step of the radical-rank lemma in both bases (factor split for all 120 idempotents, J = kernel of dimension 9, unique lifts, twisted bimodule law on all of J, Phi(J^2)=0, defect rank 3 and three-output control rank 2, step-5 identity on 60 random words per base); compile both C joins with warnings as errors and check P<=3 counts (printed as S3) 1/240/41920/6655830 (total 6697991, equal to PR #2116's pinned value), 1,597,399,200 lookups and no word of length <= 7 in each; three-output 6-word and planted 7-word positive controls in each join, all replayed in Python." } ] } diff --git a/research/a4-seven-call-radical-rank/verify.py b/research/a4-seven-call-radical-rank/verify.py index 76cdd290ed..be5c80cbf4 100644 --- a/research/a4-seven-call-radical-rank/verify.py +++ b/research/a4-seven-call-radical-rank/verify.py @@ -361,7 +361,7 @@ def run_join(exe: Path, *args: str) -> dict: best = re.search(r"best_word (none|len=(\d+):([\d ]+))", text) planted = re.search(r"planted word:([\d ]+)", text) return { - "s3": [int(v) for v in s3.groups()], + "p_le3": [int(v) for v in s3.groups()], "processed_len3": int(stats.group(1)), "children": int(stats.group(2)), "short_hits": int(stats.group(3)), "long_hits": int(stats.group(4)), "best": None if best.group(1) == "none" else [int(v) for v in best.group(3).split()], @@ -384,7 +384,7 @@ def main() -> None: report["direct_word"] = {"paid_calls": 8, "regular_inputs_checked": 48, "single_omissions_rejected": omissions, "mutated_label_rejected": True} det_check() - report["c3_determinant"] = "n_a = n_b mod 3 for every word equal to the target (200 random-word checks)" + report["c3_determinant"] = "det formula t^(n_a-n_b) checked on 200 random words; target det = 1, so n_a = n_b mod 3 for any target word" report["radical_rank_lemma"] = lemma_checks() threads = "2" with tempfile.TemporaryDirectory() as tmp: @@ -395,8 +395,8 @@ def main() -> None: joins = {} for name, exe in (("join_a", exe_a), ("join_b", exe_b)): res = run_join(exe, "target", threads, "1") - assert res["s3"] == expected_s3, res - assert res["s3"][4] == pred["exact_join"]["right_distinct_exact_states"] + assert res["p_le3"] == expected_s3, res + assert res["p_le3"][4] == pred["exact_join"]["right_distinct_exact_states"] assert res["processed_len3"] == 6655830 and res["children"] == 6655830 * 240 assert res["short_hits"] == 0 and res["long_hits"] == 0 and res["best"] is None three = run_join(exe, "three", threads, "64")