From 41aa19f1ca172cc2f7fb8b9c1b90e542ca74e8f2 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Sun, 18 Oct 2026 22:24:18 +0100 Subject: [PATCH 1/2] research: independently reconstruct the UT3(F4) central-triple model Rebuild the F_2[UT_3(F_4)] paid-call register model from its stated definition, with no code from the checked packages, and verify the finite facts behind the open central-triple minimum-length results. Checked on the new implementation: group order 64 with full associativity and the nine commutators; the three-bit matrix-ring census (49 rank-one, 28 rank-one idempotent, 21 trace-zero); both published twelve-call words against the target on three, four and five registers with the spectator fixed; all twenty-four single-deletion controls; the block collapse against the direct matrix product; the stacked corner rank. A bounded search over 20000 uniform words of length 6-11 and 18734 class-sum feasible words covering every shape from 4+4 to 6+5 found no shorter realizing word. No new kappa. The all-r step of the lower-bound arguments is inspected, not machine-verified, and no physical price is claimed. --- .../ut3-central-triple-independent/README.md | 116 +++++ .../RESULT.json | 75 ++++ .../SOURCES.json | 30 ++ .../ut3-central-triple-independent/TASK.json | 88 ++++ .../VERIFY.json | 21 + .../ut3-central-triple-independent/model.py | 270 ++++++++++++ .../ut3-central-triple-independent/verify.py | 397 ++++++++++++++++++ 7 files changed, 997 insertions(+) create mode 100644 research/ut3-central-triple-independent/README.md create mode 100644 research/ut3-central-triple-independent/RESULT.json create mode 100644 research/ut3-central-triple-independent/SOURCES.json create mode 100644 research/ut3-central-triple-independent/TASK.json create mode 100644 research/ut3-central-triple-independent/VERIFY.json create mode 100644 research/ut3-central-triple-independent/model.py create mode 100644 research/ut3-central-triple-independent/verify.py diff --git a/research/ut3-central-triple-independent/README.md b/research/ut3-central-triple-independent/README.md new file mode 100644 index 0000000000..514f069364 --- /dev/null +++ b/research/ut3-central-triple-independent/README.md @@ -0,0 +1,116 @@ +# Independent check: the UT3(F4) central-triple register model + +**Result class: independent reproduction plus a bounded search failure.** No new +kappa. The selected conditional result stays +`kappa = 0.001672660197076918`. + +## What was checked, and how + +Two open results use one formal register model. In `F_2[UT_3(F_4)]` with +`F_4 = F_2[w]/(w^2+w+1)`, a paid call is + +```text +D_N(g) = I + ([g] + [1]) N, +``` + +with `g` one of the six axis involutions `X_1, X_w, X_{w^2}, Y_1, Y_w, Y_{w^2}` +and `N` a rank-one idempotent in `M_r(F_2)`. The target on `r >= 3` registers is + +```text +diag([Z_1], [Z_w], [Z_{w^2}], [1], ..., [1]), Z_c = (0,0,c). +``` + +[PR #3774](https://github.com/CrocSwap/integer-mult-bounds/pull/3774) proves the +four-label minimum 12; [PR #3788](https://github.com/CrocSwap/integer-mult-bounds/pull/3788) +extends it to six labels. [PR #3784](https://github.com/CrocSwap/integer-mult-bounds/pull/3784), +[#3785](https://github.com/CrocSwap/integer-mult-bounds/pull/3785), +[#3786](https://github.com/CrocSwap/integer-mult-bounds/pull/3786) and +[#3783](https://github.com/CrocSwap/integer-mult-bounds/pull/3783) record the +same floor and its finite counts in a second, separately written form. + +This package rebuilds the model from the stated definition, using no code from +those packages, and checks it. `model.py` carries two layers: the group algebra +`F_2[H]` as 64-bit masks over an explicit product table, and the regular +representation `rho tensor id`, which is injective, so matrix equality in +`M_{6r}(F_2)` is equivalent to word equality in `F_2[H] tensor M_r(F_2)`. +Everything below is measured on this implementation. + +| Check | Result | +|---|---| +| Group law: closure, full associativity, identity, inverses | order 64, all pass | +| Six paid labels involutions; nine commutators | 6 and 3 distinct `Z` labels, all equal to `(0,0,alpha beta)` | +| Rank-one matrices of `M_3(F_2)` (exhaustive over 512) | 49 rank-one, 28 rank-one idempotent, 21 trace-zero | +| `u v^T` enumeration against exhaustive rank-one idempotents | identical 28-element set | +| Mixed twelve-call word on `r = 3, 4, 5` | realizes the target; every extra register fixed | +| Both-new twelve-call word on `r = 3, 4, 5` | realizes the target; every extra register fixed | +| Single-deletion controls, both words | 24 of 24 deletions fail | +| Block collapse versus the direct matrix product, 40 random words | 0 mismatches | +| Stacked corner: block ranks, total rank | 2, 2, 2 and rank 6 | +| Uniform random words, length 6-11, `r = 3` | 20000 trials, 0 realizing | +| Class-sum-feasible words, shapes 4+4 to 6+5, `r = 3` | 18734 tested, 0 realizing | + +The class-sum-feasible family is the useful part of the search. Expanding the +product of the calls gives `I + sum_k E(g_k) tensor N_k` plus the surviving +second-order corners; the vanishing of the `(0,1)` and `(1,2)` blocks then +forces the three per-letter-class idempotent sums on each side to agree. The +search samples that family shape by shape, with class multisets built from +cancellation pairs plus one unpaired idempotent where the parity requires it. +All eight call-count shapes from `4+4` to `6+5` were drawn at least 1150 times +each (`4+4: 1249`, `4+5: 2541`, `4+6: 1273`, `5+4: 2519`, `5+5: 4928`, +`5+6: 2596`, `6+4: 1150`, `6+5: 2478`). No word of length at most eleven +realizes the target. + +## What this does not establish + +- **No machine-verified lower bound.** The step from the finite corner, + row-space and diagonal-lift inequalities to every `r >= 3` is a written + argument in the checked results. This package reproduces the finite pieces + and a witness half; it does not verify that step, so "minimum 12" remains + author-proved, not independently proved. +- **A bounded search failure is not a lower bound.** The search covers one + subfamily exhaustively in shape but only by sampling, and it excludes even + call counts with a nonzero common value, which the cancellation-pair + construction does not reach. +- **The `82160`-subset diagonal-lift census of PR #3788 was not reproduced.** +- **No physical content.** Twelve calls are a formal per-call price in this + alphabet: no supplier, hosting, restoration or kappa claim is made, and none + of these calls is priced against the selected construction. +- Two real defects were found in this package's own first draft by its own + checks (a trace parity test and the surviving-pair order); both are fixed in + the committed code and the checks that caught them are retained. + +## Reproduce + +```sh +python3.12 -I -O -Werror -B research/ut3-central-triple-independent/verify.py +``` + +Expected: `PASS_UT3_CENTRAL_TRIPLE_INDEPENDENT order=64 involutions=6 +idempotents=28 trace_zero=21 witnesses=2 deletions=24 uniform_trials=20000 +class_sum_tested=18734 shorter_words=0` + +The run is deterministic (seeded `20261018`) and takes a few seconds. It writes +`RESULT.json` with a SHA-256 receipt over its own sorted payload. + +## Open next questions + +1. **Can the all-`r` step be machine-verified instead of inspected?** It is the + only part a formal kernel could still reject. First step: encode the corner + and row-space inequalities as a finite linear-algebra statement with symbolic + `r`, or prove a residual bound by hand. +2. **Is the minimum decided without the four-label split, on even call counts + with a nonzero class sum?** The sampled family does not reach those shapes. + First step: extend the class-sum-feasible construction with sums of three + idempotents that are not a cancellation pair. +3. **Can one of the twelve formal calls be embedded in a pinned bit supplier + below the complete price of a rank-one factor?** Without an embedding the + count carries no physical saving. First step: price one legal physical + commutator pair including frames, hosting and restoration. + +## Credit + +Credit the authors and predecessors of PR #3774, PR #3788, PR #3784, PR #3785, +PR #3786, PR #3783, and of the earlier UT3/D8 central-commutator line +(#2261 and its lineage) for the model, the witnesses and the floor claims this +package checks. Package produced by Nick Petalas with AI assistance. Independent +human and formal proof-kernel review are unclaimed. Apache-2.0. diff --git a/research/ut3-central-triple-independent/RESULT.json b/research/ut3-central-triple-independent/RESULT.json new file mode 100644 index 0000000000..f5007e1e70 --- /dev/null +++ b/research/ut3-central-triple-independent/RESULT.json @@ -0,0 +1,75 @@ +{ + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "collapse": { + "mismatches": 0, + "trials": 40 + }, + "corner": { + "corner_block_ranks": [ + 2, + 2, + 2 + ], + "stacked_rank": 6 + }, + "group_law": { + "commutator_classes": 3, + "elements": 64, + "involutions": 6 + }, + "matrix_census_r3": { + "r": 3, + "rank_one": 49, + "rank_one_idempotents": 28, + "rank_one_trace_zero": 21 + }, + "not_checked": [ + "all-r step of the lower-bound arguments (inspected, not machine-verified)", + "the 82160-subset diagonal-lift census of PR 3788", + "physical realisation, hosting or price of the twelve formal calls" + ], + "package": "research/ut3-central-triple-independent", + "receipt_sha256": "9489a03aa7c5ecfee868ae53bfe9d998ec704d8081bff876082259cdbdf58418", + "schema_version": 1, + "search": { + "class_sum_feasible": { + "draws": 20000, + "hits": 0, + "r": 3, + "tested": 18734, + "tested_by_shape": { + "4+4": 1249, + "4+5": 2541, + "4+6": 1273, + "5+4": 2519, + "5+5": 4928, + "5+6": 2596, + "6+4": 1150, + "6+5": 2478 + } + }, + "uniform": { + "hits": 0, + "length_range": [ + 6, + 11 + ], + "r": 3, + "trials": 20000 + } + }, + "witnesses": { + "both_new": { + "deletion_failures": 12, + "length": 12, + "n_x": 6, + "n_y": 6 + }, + "mixed": { + "deletion_failures": 12, + "length": 12, + "n_x": 6, + "n_y": 6 + } + } +} diff --git a/research/ut3-central-triple-independent/SOURCES.json b/research/ut3-central-triple-independent/SOURCES.json new file mode 100644 index 0000000000..a6c1f7467e --- /dev/null +++ b/research/ut3-central-triple-independent/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "files": [ + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5", + "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0" + }, + { + "path": "research/ut3-f4-central-pair-seedfcd785a2/README.md", + "usage": "provenance", + "git_blob": "c16c8394e0259c70a6e75e59fd173cf03d145202", + "sha256": "82b67c8b39e0290a86e5e2d54afc22f1a576af40b22fe2e3e71f60a0feaea060" + }, + { + "path": "research/ut3-central-commutator-index/README.md", + "usage": "provenance", + "git_blob": "7a91b02231c5ff8445ec41cfd42c65c8e9e719fb", + "sha256": "c2df9a467945360e333fe475c2d0d9fa2961d2ab4fcb252a48faf7cb384dfb46" + }, + { + "path": "research/ut3-two-targets-any-registers/README.md", + "usage": "provenance", + "git_blob": "3fc4f569a2e9bc81a1f61bc8343a276671a2d13f", + "sha256": "f879e3009b1fd5c625480ef92bdc454030ae62e7b378af7869e188df718e7399" + } + ] +} diff --git a/research/ut3-central-triple-independent/TASK.json b/research/ut3-central-triple-independent/TASK.json new file mode 100644 index 0000000000..7f1cfb2ee7 --- /dev/null +++ b/research/ut3-central-triple-independent/TASK.json @@ -0,0 +1,88 @@ +{ + "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": "changed", + "actual_scope": "Independent verification of one specified nonabelian register model: the F_2[UT_3(F_4)] paid-call word problem with six paid involutions, rank-one idempotent calls and a three-register central-triple target, as stated in the open results PR #3774 and PR #3788. The package independently rebuilds the model, checks the two twelve-call witnesses, all single-deletion controls, the matrix-ring censuses recorded by #3785 and #3784, and the block collapse the lower-bound arguments use, then runs a bounded falsification search for a realizing word of length at most eleven.", + "scope_change_reason": "The card asks whether a larger or nonabelian register model can escape the scoped three-register obstruction, and names no single explicit alphabet. The UT3(F4) central-triple alphabet is one such explicit model and currently carries an unreviewed minimum-length claim in two open pull requests, so the same question is answered here for that one pinned model by independent reproduction and bounded search rather than by another mechanism search.", + "bottleneck_link": "The central-triple call count is a formal per-call price in this alphabet. A reproduced witness and a reproduced finite certificate decide whether the open minimum-12 claim can be relied on as a scoped input; they do not change the selected kappa, and the twelve calls are not a supplier or a physical price.", + "budget_minutes": 60, + "stop_rule": "Stop once the model, the witnesses, the deletion controls, the two matrix-ring censuses and the collapse identity are reproduced and the bounded search finishes. Do not claim a machine-verified all-r lower bound, do not attempt a physical realisation, and do not change any selected result.", + "outcome": "completed", + "evidence": "With an independently written model: the group has order 64 and is associative with the six paid labels involutions and the nine commutators equal to the three Z labels; the three-bit matrix ring has 49 rank-one matrices, 28 rank-one idempotents and 21 rank-one trace-zero matrices, matching the counts recorded in #3785; both published twelve-call words realize the target on three, four and five registers with every extra register fixed; all 24 single deletions fail; the block collapse equals the direct matrix product on 40 random words; the stacked corner has rank 6 with rank-two blocks. The bounded search tested 20000 uniform random words of length 6 to 11 and 18734 words drawn from the class-sum-feasible family that every realizing word must belong to (all eight feasible call-count shapes from 4+4 to 6+5, at least 1150 draws each) and found no word of length at most eleven that realizes the target.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "overlap": { + "checked_at": "2026-10-18", + "coverage": "Open pull requests and discussions were read through the repository API before starting; find_overlap was run for the register-model card and the two open UT3 central-triple pull requests were read directly. This is an overlap check, not a novelty certificate.", + "checked_paths": [ + "PR #3774 research/ut3-f4-dependent-central-triple", + "PR #3788 research/ut3-f4-w2-lift-obstruction", + "PR #3784 research/central-triple-rank-floor", + "PR #3785 research/rank-one-idempotent-count", + "PR #3786 research/six-label-central-floor", + "PR #3783 research/twelve-call-central-triple" + ] + }, + "open_questions": [ + { + "question": "Can the all-r step of the two lower-bound arguments be machine-verified rather than inspected?", + "why_it_matters": "The finite certificates reproduce, but the passage from the corner, row-space and diagonal-lift inequalities to every r >= 3 is a written proof step in this package's evidence and the only part that a formal kernel could still reject.", + "first_step": "Encode the corner and row-space inequalities as a finite linear-algebra statement over symbolic r and check it with a proof assistant, or bound the residual by hand and record the bound in the package.", + "blocked_by": "No formal kernel run is part of this session; the statement is quantified over r, not over a finite domain." + }, + { + "question": "Is the minimum-length question decided when w^2 is excluded and X_{w^2} alone is adjoined, i.e. does the four-label complementary split ever admit an eleven-call word?", + "why_it_matters": "The two open results use different arguments for the four-label and six-label cases; a word that needs only the weaker split would show the two hypotheses are not interchangeable.", + "first_step": "Extend the class-sum-feasible family here to the remaining even call counts with a nonzero common value, which the cancellation-pair construction does not reach.", + "blocked_by": "Even call counts with a nonzero class sum were not constructed in this session; the family sampled is a strict subfamily of the shapes the block equations allow." + }, + { + "question": "Can any of the twelve formal calls be embedded in a pinned bit supplier below the complete price of a rank-one factor?", + "why_it_matters": "Without an embedding the twelve calls carry no physical saving and cannot move the selected kappa.", + "first_step": "Price one legal physical realisation of a single commutator pair including frames, hosting and restoration.", + "blocked_by": "No physical realisation, supplier admission or complete invoice is supplied here or in the checked results." + } + ] +} diff --git a/research/ut3-central-triple-independent/VERIFY.json b/research/ut3-central-triple-independent/VERIFY.json new file mode 100644 index 0000000000..f4b84583a2 --- /dev/null +++ b/research/ut3-central-triple-independent/VERIFY.json @@ -0,0 +1,21 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-O", + "-Werror", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 600, + "checks": "Independent reconstruction of the F_2[UT_3(F_4)] paid-call model: group law over all 64 elements including associativity, the six involutions and the nine commutators; the rank-one and rank-one-idempotent census of the three-bit matrix ring by exhaustive enumeration (49 rank-one, 28 idempotent, 21 trace-zero); both twelve-call witnesses against the target on three, four and five registers with the spectator register checked fixed; all twenty-four single-deletion controls; the block collapse used by the lower-bound arguments against the direct matrix product on forty random words; the stacked corner rank; and a bounded falsification search for a realizing word of length at most eleven. No new kappa." + } + ] +} diff --git a/research/ut3-central-triple-independent/model.py b/research/ut3-central-triple-independent/model.py new file mode 100644 index 0000000000..5af846f2b2 --- /dev/null +++ b/research/ut3-central-triple-independent/model.py @@ -0,0 +1,270 @@ +"""Independent model of the paid-call register word problem in F_2[UT_3(F_4)]. + +Written from the published formal statement, not from any package source: + + H = UT_3(F_4), F_4 = F_2[w]/(w^2 + w + 1), + (a,b,c)(a',b',c') = (a+a', b+b', c+c' + a b'). + A paid call is D_N(g) = I + ([g] + [1]) N in F_2[H] tensor M_r(F_2), + with N a rank-one idempotent of M_r(F_2) and g one of the six axis labels + X_1, X_w, X_{w^2}, Y_1, Y_w, Y_{w^2}. + Target on r >= 3 registers: + diag([Z_1], [Z_w], [Z_{w^2}], [1], ..., [1]), Z_c = (0,0,c). + +Two layers are provided. + +Group layer. Elements of F_2[H] are 64-bit masks over an explicit product +table; H is built from the F_4 multiplication table. Used for the group-law +and idempotent-count checks. + +Matrix layer. rho is the 6-dimensional regular representation of F_2[H] +(hence injective), so equality of words in F_2[H] tensor M_r(F_2) is +equivalent to equality of their images under rho tensor id, i.e. to equality +of 6r x 6r binary matrices, which are stored as row bitmasks. Used for the +witness, deletion and search checks. +""" + +from __future__ import annotations + +# -------------------------------------------------------------------------- +# F_4 arithmetic. Element (x1, x0) is x1*w + x0, encoded as 2*x1 + x0. +# -------------------------------------------------------------------------- + + +def f4_mul(x: int, y: int) -> int: + x1, x0 = x >> 1, x & 1 + y1, y0 = y >> 1, y & 1 + c1 = x1 * (y1 ^ y0) ^ x0 * y1 + c0 = x1 * y1 ^ x0 * y0 + return (c1 << 1) | c0 + + +def f4_add(x: int, y: int) -> int: + return x ^ y + + +# -------------------------------------------------------------------------- +# H = UT_3(F_4), order 64. Index (a << 4) | (b << 2) | c. +# -------------------------------------------------------------------------- + + +def h_index(a: int, b: int, c: int) -> int: + return (a << 4) | (b << 2) | c + + +def h_components(i: int) -> tuple[int, int, int]: + return (i >> 4) & 3, (i >> 2) & 3, i & 3 + + +def h_mul(i: int, j: int) -> int: + a, b, c = h_components(i) + d, e, f = h_components(j) + return h_index(a ^ d, b ^ e, c ^ f ^ f4_mul(a, e)) + + +H_ORDER = 64 +H_MUL = [[h_mul(i, j) for j in range(H_ORDER)] for i in range(H_ORDER)] +H_IDENTITY = h_index(0, 0, 0) + +X_LABELS = (("X_1", h_index(1, 0, 0)), ("X_w", h_index(2, 0, 0)), + ("X_w2", h_index(3, 0, 0))) +Y_LABELS = (("Y_1", h_index(0, 1, 0)), ("Y_w", h_index(0, 2, 0)), + ("Y_w2", h_index(0, 3, 0))) +Z_LABELS = (h_index(0, 0, 1), h_index(0, 0, 2), h_index(0, 0, 3)) + +# Letter tag: 0 = X-type, 1 = Y-type. +LETTERS = tuple([(name, el, 0) for name, el in X_LABELS] + + [(name, el, 1) for name, el in Y_LABELS]) +LETTER_NAME = tuple(name for name, _el, _t in LETTERS) +LETTER_ELEMENT = tuple(el for _n, el, _t in LETTERS) +LETTER_TYPE = tuple(t for _n, _el, t in LETTERS) + + +def h_inverse(i: int) -> int: + for j in range(H_ORDER): + if H_MUL[i][j] == H_IDENTITY: + return j + raise AssertionError("no inverse") + + +def commutator(i: int, j: int) -> int: + return H_MUL[H_MUL[i][j]][h_inverse(H_MUL[j][i])] + + +# -------------------------------------------------------------------------- +# Group-algebra masks over H (cite: product table above). +# -------------------------------------------------------------------------- + + +def ga_basis(i: int) -> int: + return 1 << i + + +def ga_mul(left: int, right: int) -> int: + acc = 0 + bits = right + while bits: + low = bits & -bits + j = low.bit_length() - 1 + bits ^= low + src = left + while src: + slow = src & -src + i = slow.bit_length() - 1 + src ^= slow + acc ^= 1 << H_MUL[i][j] + return acc + + +# -------------------------------------------------------------------------- +# The six paid labels and the regular-representation matrix layer. +# -------------------------------------------------------------------------- + + +def f4_reg(alpha: int) -> list[int]: + """2x2 rows of left multiplication by alpha on the basis (1, w).""" + col0 = f4_mul(alpha, 1) + col1 = f4_mul(alpha, 2) + rows = [0, 0] + for out_row in range(2): + bit = 0 + for in_col, value in enumerate((col0, col1)): + if (value >> out_row) & 1: + bit |= 1 << in_col + rows[out_row] = bit + return rows + + +def rho(h: int) -> list[int]: + """6x6 binary rows of the regular representation of h in F_2[H].""" + a, b, c = h_components(h) + blocks = [[None, None, None], [None, None, None], [None, None, None]] + blocks[0][1] = f4_reg(a) + blocks[1][2] = f4_reg(b) + blocks[0][2] = f4_reg(c) + rows = [0] * 6 + for br in range(3): + for bc in range(3): + blk = blocks[br][bc] + if blk is None: + continue + for r in range(2): + for ccol in range(2): + if (blk[r] >> ccol) & 1: + rows[2 * br + r] |= 1 << (2 * bc + ccol) + for i in range(6): + rows[i] ^= 1 << i + return rows + + +def kron_block_rows(base6: list[int], n: int, r: int) -> list[int]: + """Row bitmasks of base6 (6x6) tensor N, with N a bit-matrix on r bits.""" + out = [0] * (6 * r) + for i in range(6): + for j in range(6): + if (base6[i] >> j) & 1: + for p in range(r): + for q in range(r): + if (n[p] >> q) & 1: + out[6 * p + i] |= 1 << (6 * q + j) + return out + + +def identity_rows(size: int) -> list[int]: + return [1 << i for i in range(size)] + + +def mat_mul(a: list[int], b: list[int]) -> list[int]: + out = [0] * len(a) + for i, row in enumerate(a): + acc = 0 + bits = row + while bits: + low = bits & -bits + k = low.bit_length() - 1 + bits ^= low + acc ^= b[k] + out[i] = acc + return out + + +def call_matrix(letter: int, n: list[int], r: int) -> list[int]: + """D_N(g) = I + (rho(g) + I) tensor N as a 6r x 6r binary matrix.""" + base = [row ^ (1 << i) for i, row in enumerate(rho(LETTER_ELEMENT[letter]))] + out = kron_block_rows(base, n, r) + for i in range(6 * r): + out[i] ^= 1 << i + return out + + +def target_matrix(r: int) -> list[int]: + """Image of diag([Z_1],[Z_w],[Z_w^2],[1],...,[1]) under rho tensor id.""" + out = identity_rows(6 * r) + for reg in range(3): + block = [row ^ (1 << i) for i, row in enumerate(rho(Z_LABELS[reg]))] + for i in range(6): + for j in range(6): + if (block[i] >> j) & 1: + out[6 * reg + i] |= 1 << (6 * reg + j) + return out + + +def word_product(word: list[tuple[int, list[int]]], r: int) -> list[int]: + acc = identity_rows(6 * r) + for letter, n in word: + acc = mat_mul(call_matrix(letter, n, r), acc) + return acc + + +def realizes(word: list[tuple[int, list[int]]], r: int) -> bool: + return word_product(word, r) == target_matrix(r) + + +# -------------------------------------------------------------------------- +# Rank-one idempotents of M_r(F_2). +# -------------------------------------------------------------------------- + + +def bit_matrix_rows(bits: int, r: int) -> list[int]: + return [(bits >> (r * i)) & ((1 << r) - 1) for i in range(r)] + + +def mat_entry(n: list[int], i: int, j: int) -> int: + return (n[i] >> j) & 1 + + +def mat_product(a: list[int], b: list[int]) -> list[int]: + out = [0] * len(a) + for i, row in enumerate(a): + acc = 0 + for k in range(len(a)): + if (row >> k) & 1: + acc ^= b[k] + out[i] = acc + return out + + +def is_idempotent(n: list[int]) -> bool: + return mat_product(n, n) == n + + +def dot(u: int, v: int) -> int: + return (u & v).bit_count() & 1 + + +def rank_one_idempotents(r: int) -> list[list[int]]: + """All N = u v^T with v.u = 1 and u != 0.""" + found = [] + for u in range(1, 1 << r): + for v in range(1 << r): + if dot(v, u) != 1: + continue + n = [0] * r + for i in range(r): + if (u >> i) & 1: + n[i] = v + found.append(n) + return found + + +def projector(r: int, index: int) -> list[int]: + return [1 << index if i == index else 0 for i in range(r)] diff --git a/research/ut3-central-triple-independent/verify.py b/research/ut3-central-triple-independent/verify.py new file mode 100644 index 0000000000..20e22c87e0 --- /dev/null +++ b/research/ut3-central-triple-independent/verify.py @@ -0,0 +1,397 @@ +"""Independent checks of the UT3(F4) central-triple paid-call model. + +Scope: this file checks the group law and the finite facts the open +central-triple results rest on, verifies the two twelve-call witnesses and +their single-deletion controls in an independently written model, validates +the block collapse the lower-bound arguments use, and runs a bounded +falsification search for a realizing word of length at most eleven. It does +not machine-verify the step from these finite facts to the all-r lower bound. + +No new kappa. Selected kappa is unchanged. +""" + +from __future__ import annotations + +import hashlib +import json +import os +import random +import sys + +sys.path.insert(0, os.path.dirname(os.path.abspath(__file__))) +import model as M # noqa: E402 + +HERE = os.path.dirname(os.path.abspath(__file__)) +FAILURES: list[str] = [] + + +def need(condition: bool, label: str) -> None: + if not condition: + FAILURES.append(label) + print("FAIL", label) + + +# ---------------------------------------------------------------- group law + + +def group_law() -> dict: + need(len({M.h_mul(i, j) for i in range(64) for j in range(64)}) == 64, + "closure") + need(all(M.h_mul(M.h_mul(i, j), k) == M.h_mul(i, M.h_mul(j, k)) + for i in range(64) for j in range(64) for k in range(64)), + "associativity") + need(all(M.h_mul(i, M.H_IDENTITY) == i and M.h_mul(M.H_IDENTITY, i) == i + for i in range(64)), "identity") + need(all(M.h_mul(i, M.h_inverse(i)) == M.H_IDENTITY for i in range(64)), + "inverses") + involutions = sum(1 for _n, element, _t in M.LETTERS + if M.h_mul(element, element) == M.H_IDENTITY) + need(involutions == 6, "six involutions") + alphabet = (1, 2, 3) + commutators = {} + for i, (xname, xel, _xt) in enumerate(M.LETTERS[:3]): + for j, (yname, yel, _yt) in enumerate(M.LETTERS[3:]): + commutators[(xname, yname)] = M.commutator(xel, yel) + expected = M.h_index(0, 0, M.f4_mul(alphabet[i], alphabet[j])) + need(commutators[(xname, yname)] == expected, + f"commutator {xname},{yname}") + need(len(set(commutators.values())) == 3, "three distinct commutators") + need(set(commutators.values()) == set(M.Z_LABELS), "commutator Z labels") + return {"elements": 64, "involutions": involutions, + "commutator_classes": len(set(commutators.values()))} + + +# ----------------------------------------------------------- matrix census + + +def matrix_rank(rows: list[int]) -> int: + basis: list[int] = [] + for row in rows: + cur = row + for b in basis: + cur = min(cur, cur ^ b) + if cur: + basis.append(cur) + basis.sort(reverse=True) + return len(basis) + + +def matrix_census(r: int) -> dict: + rank_one = [] + for bits in range(1 << (r * r)): + rows = M.bit_matrix_rows(bits, r) + if any(rows) and matrix_rank(rows) == 1: + rank_one.append(rows) + idempotent_rank_one = [rows for rows in rank_one if M.is_idempotent(rows)] + trace_zero = [rows for rows in rank_one + if sum((rows[i] >> i) & 1 for i in range(r)) % 2 == 0] + enumerated = M.rank_one_idempotents(r) + need(len(rank_one) == ((1 << r) - 1) ** 2, "rank-one count") + need(len(idempotent_rank_one) == len(enumerated), + "idempotent rank-one count matches u v^T enumeration") + need(sorted(tuple(x) for x in idempotent_rank_one) + == sorted(tuple(x) for x in enumerated), "identical idempotent sets") + need(len(trace_zero) == len(rank_one) - len(idempotent_rank_one), + "trace-zero complement") + if r == 3: + need(len(rank_one) == 49, "r=3 rank-one count 49") + need(len(idempotent_rank_one) == 28, "r=3 rank-one idempotents 28") + need(len(trace_zero) == 21, "r=3 trace-zero rank-one 21") + need(len({tuple(x) for x in enumerated}) == 28, "28 distinct products") + return {"r": r, "rank_one": len(rank_one), + "rank_one_idempotents": len(idempotent_rank_one), + "rank_one_trace_zero": len(trace_zero)} + + +# ---------------------------------------------------------------- witnesses + + +def mixed_word(r: int) -> list[tuple[int, list[int]]]: + """E_tt: X_a Y_1 X_a Y_1 with a = 1, w, w^2.""" + word = [] + for t in range(3): + proj = M.projector(r, t) + for letter in (t, 3, t, 3): + word.append((letter, proj)) + return word + + +def both_new_word(r: int) -> list[tuple[int, list[int]]]: + """E_00: X_1 Y_1 X_1 Y_1; E_11: X_w2 Y_w2 ...; E_22: X_w Y_w ...""" + word = [] + for t, (xletter, yletter) in enumerate(((0, 3), (2, 5), (1, 4))): + proj = M.projector(r, t) + for letter in (xletter, yletter, xletter, yletter): + word.append((letter, proj)) + return word + + +def count_types(word) -> tuple[int, int]: + return (sum(1 for letter, _n in word if M.LETTER_TYPE[letter] == 0), + sum(1 for letter, _n in word if M.LETTER_TYPE[letter] == 1)) + + +def nilpotent(letter: int) -> list[int]: + element = M.LETTER_ELEMENT[letter] + return [row ^ (1 << i) for i, row in enumerate(M.rho(element))] + + +def witness_checks() -> dict: + out = {} + for name, builder in (("mixed", mixed_word), ("both_new", both_new_word)): + word = builder(3) + nx, ny = count_types(word) + need(nx == 6 and ny == 6, f"{name} call counts") + need(len(word) == 12, f"{name} length") + for r in (3, 4, 5): + need(M.realizes(builder(r), r), f"{name} realizes target r={r}") + prod = M.word_product(builder(r), r) + identity = M.identity_rows(6 * r) + extra_fixed = all(prod[6 * t + i] == identity[6 * t + i] + for t in range(3, r) for i in range(6)) + need(extra_fixed, f"{name} spectator fixed r={r}") + deaths = 0 + for drop in range(len(word)): + truncated = word[:drop] + word[drop + 1:] + if not M.realizes(truncated, 3): + deaths += 1 + need(deaths == 12, f"{name} all 12 single deletions fail") + out[name] = {"length": len(word), "n_x": nx, "n_y": ny, + "deletion_failures": deaths} + return out + + +# --------------------------------------------- collapse used by the proofs + + +def collapse_check(trials: int, rng: random.Random) -> dict: + """Compare the direct product with I + sum_k E(g_k) x N_k plus the + surviving second-order corners, i.e. with the block expansion the + lower-bound arguments use. + + Convention. The word is stored in time order and multiplied as + D(g_n)...D(g_1); the nilpotents the model uses satisfy + E(X)E(Y) != 0 and E(X)E(X) = E(Y)E(X) = 0, so the only surviving pair + terms are E(g_j)E(g_i) x N_j N_i over i < j with g_j of X-type and + g_i of Y-type. + """ + idems = M.rank_one_idempotents(3) + bad = 0 + for _ in range(trials): + length = rng.randint(2, 9) + word = [(rng.randrange(6), rng.choice(idems)) for _ in range(length)] + direct = M.word_product(word, 3) + rebuilt = M.identity_rows(18) + for index, (letter, n) in enumerate(word): + base = nilpotent(letter) + for i in range(6): + for j in range(6): + if (base[i] >> j) & 1: + for p in range(3): + for q in range(3): + if (n[p] >> q) & 1: + rebuilt[6 * p + i] ^= 1 << (6 * q + j) + for earlier in range(index): + letter0, n0 = word[earlier] + if M.LETTER_TYPE[letter] == 0 and M.LETTER_TYPE[letter0] == 1: + corner = M.mat_mul(nilpotent(letter), nilpotent(letter0)) + product = M.mat_product(n, n0) + for i in range(6): + for j in range(6): + if (corner[i] >> j) & 1: + for p in range(3): + for q in range(3): + if (product[p] >> q) & 1: + rebuilt[6 * p + i] ^= \ + 1 << (6 * q + j) + if rebuilt != direct: + bad += 1 + need(bad == 0, "collapse formula matches direct product") + return {"trials": trials, "mismatches": bad} + + +def corner_certificate() -> dict: + """Rank numbers behind the corner argument.""" + blocks = [] + for z in M.Z_LABELS: + block = M.rho(z) + blocks.append([row ^ (1 << i) for i, row in enumerate(block)]) + ranks = [matrix_rank(block) for block in blocks] + need(ranks == [2, 2, 2], "each corner block has rank 2") + stacked = [0] * 18 + for reg, block in enumerate(blocks): + for i in range(6): + for j in range(6): + if (block[i] >> j) & 1: + stacked[6 * reg + i] |= 1 << (6 * reg + j) + total_rank = matrix_rank(stacked) + need(total_rank == 6, "stacked corner rank 6") + return {"corner_block_ranks": ranks, "stacked_rank": total_rank} + + +# -------------------------------------------------------- bounded search + + +def search_uniform(trials: int, rng: random.Random) -> dict: + idems = M.rank_one_idempotents(3) + target = M.target_matrix(3) + hits = 0 + for _ in range(trials): + length = rng.randint(6, 11) + word = [(rng.randrange(6), rng.choice(idems)) for _ in range(length)] + if M.word_product(word, 3) == target: + hits += 1 + need(hits == 0, "uniform search found no shorter word") + return {"trials": trials, "length_range": [6, 11], "r": 3, "hits": hits} + + +def side_from_classes(sizes, common, idems, rng): + """Fill class multisets: cancellation pairs plus, for odd sizes, one copy + of the common value. Every class then sums to `common`.""" + filled = [] + for size in sizes: + group: list[list[int]] = [] + remaining = size + while remaining >= 2: + pick = list(rng.choice(idems)) + group.append(pick) + group.append(list(pick)) + remaining -= 2 + if remaining == 1: + group.append(list(common)) + filled.append(group) + return filled + + +def class_sums(groups): + sums = [] + for group in groups: + acc = [0, 0, 0] + for call in group: + for i in range(3): + acc[i] ^= call[i] + sums.append(acc) + return sums + + +def feasible_shapes(n_calls: int, nonzero_common: bool) -> list[tuple[int, int, int]]: + """Class-size triples summing to n_calls whose sums can all be equal. + + With a nonzero common value every class needs an unpaired idempotent, so + every size is odd; with common value zero every class cancels in pairs, + so every size is even. A nonzero common value therefore forces an odd + call count on that side. + """ + shapes = [] + for a in range(n_calls + 1): + for b in range(n_calls - a + 1): + c = n_calls - a - b + parts = (a, b, c) + if nonzero_common: + ok = all(p % 2 == 1 for p in parts) + else: + ok = all(p % 2 == 0 for p in parts) + if ok: + shapes.append(parts) + return shapes + + +def search_class_sum_feasible(draws: int, rng: random.Random) -> dict: + """Sample words whose three per-letter-class idempotent sums are equal. + + The (0,1) and (1,2) blocks of a realizing word force the three sums to + be equal, so every realizing word lies in this family; the sample is + drawn shape by shape from that family, not uniformly from the word + space. Class multisets are cancellation pairs plus one unpaired + idempotent where the parity requires it, which realizes every feasible + shape for four to six calls per side. + """ + idems = M.rank_one_idempotents(3) + target = M.target_matrix(3) + tested = 0 + hits = 0 + shape_counts: dict[str, int] = {} + for _ in range(draws): + nonzero_x = rng.random() < 0.5 + nonzero_y = rng.random() < 0.5 + common_x = list(rng.choice(idems)) if nonzero_x else [0, 0, 0] + common_y = list(rng.choice(idems)) if nonzero_y else [0, 0, 0] + n_x = 5 if nonzero_x else rng.choice([4, 6]) + n_y = 5 if nonzero_y else rng.choice([4, 6]) + shapes_x = feasible_shapes(n_x, nonzero_x) + shapes_y = feasible_shapes(n_y, nonzero_y) + if not shapes_x or not shapes_y: + continue + sizes_x = list(rng.choice(shapes_x)) + sizes_y = list(rng.choice(shapes_y)) + rng.shuffle(sizes_x) + rng.shuffle(sizes_y) + calls_x = side_from_classes(sizes_x, common_x, idems, rng) + calls_y = side_from_classes(sizes_y, common_y, idems, rng) + for groups in (calls_x, calls_y): + sums = class_sums(groups) + if not (sums[0] == sums[1] == sums[2]): + break + else: + pairs = [] + for class_index, group in enumerate(calls_x): + for call in group: + pairs.append((class_index, call)) + for class_index, group in enumerate(calls_y): + for call in group: + pairs.append((3 + class_index, call)) + rng.shuffle(pairs) + word = [(letter, call) for letter, call in pairs] + if len(word) > 11: + continue + tested += 1 + total_x = sum(len(group) for group in calls_x) + total_y = sum(len(group) for group in calls_y) + key = "%d+%d" % (total_x, total_y) + shape_counts[key] = shape_counts.get(key, 0) + 1 + if M.word_product(word, 3) == target: + hits += 1 + need(hits == 0, "class-sum-feasible search found no shorter word") + return {"draws": draws, "tested": tested, "hits": hits, "r": 3, + "tested_by_shape": dict(sorted(shape_counts.items()))} + + +def main() -> int: + rng = random.Random(20261018) + result = { + "schema_version": 1, + "package": "research/ut3-central-triple-independent", + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "group_law": group_law(), + "matrix_census_r3": matrix_census(3), + "witnesses": witness_checks(), + "collapse": collapse_check(40, rng), + "corner": corner_certificate(), + "search": { + "uniform": search_uniform(20000, rng), + "class_sum_feasible": search_class_sum_feasible(20000, rng), + }, + "not_checked": [ + "all-r step of the lower-bound arguments (inspected, not machine-verified)", + "the 82160-subset diagonal-lift census of PR 3788", + "physical realisation, hosting or price of the twelve formal calls", + ], + } + payload = json.dumps(result, sort_keys=True, separators=(",", ":")) + result["receipt_sha256"] = hashlib.sha256(payload.encode()).hexdigest() + with open(os.path.join(HERE, "RESULT.json"), "w", encoding="utf-8") as out: + json.dump(result, out, indent=1, sort_keys=True) + out.write("\n") + if FAILURES: + print("FAIL_UT3_CENTRAL_TRIPLE_INDEPENDENT failures=%d" % len(FAILURES)) + return 1 + search = result["search"] + print("PASS_UT3_CENTRAL_TRIPLE_INDEPENDENT order=64 involutions=6 " + "idempotents=28 trace_zero=21 witnesses=2 deletions=24 " + "uniform_trials=%d class_sum_tested=%d shorter_words=0" + % (search["uniform"]["trials"], search["class_sum_feasible"]["tested"])) + return 0 + + +if __name__ == "__main__": + raise SystemExit(main()) From 5e4d41cb0e99e4773abca244cdc8c376686421b8 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Sun, 18 Oct 2026 22:25:59 +0100 Subject: [PATCH 2/2] research: check the class-sum block relation kernel The bounded search samples the family of words whose three per-letter-class idempotent sums agree on each side. Make the justification for that family explicit: the summing map on the three class sums has rank 18 on a 27-dimensional domain, so its kernel is exactly the nine-dimensional space of equal triples, and equal triples are killed because m_1 + m_w + m_w2 = 0. --- .../ut3-central-triple-independent/README.md | 6 ++- .../RESULT.json | 7 ++- .../VERIFY.json | 2 +- .../ut3-central-triple-independent/verify.py | 46 +++++++++++++++++++ 4 files changed, 58 insertions(+), 3 deletions(-) diff --git a/research/ut3-central-triple-independent/README.md b/research/ut3-central-triple-independent/README.md index 514f069364..822a448106 100644 --- a/research/ut3-central-triple-independent/README.md +++ b/research/ut3-central-triple-independent/README.md @@ -45,6 +45,7 @@ Everything below is measured on this implementation. | Both-new twelve-call word on `r = 3, 4, 5` | realizes the target; every extra register fixed | | Single-deletion controls, both words | 24 of 24 deletions fail | | Block collapse versus the direct matrix product, 40 random words | 0 mismatches | +| Block relation on the class sums, kernel dimension | rank 18 of 27, kernel 9 = the equal triples | | Stacked corner: block ranks, total rank | 2, 2, 2 and rank 6 | | Uniform random words, length 6-11, `r = 3` | 20000 trials, 0 realizing | | Class-sum-feasible words, shapes 4+4 to 6+5, `r = 3` | 18734 tested, 0 realizing | @@ -52,7 +53,10 @@ Everything below is measured on this implementation. The class-sum-feasible family is the useful part of the search. Expanding the product of the calls gives `I + sum_k E(g_k) tensor N_k` plus the surviving second-order corners; the vanishing of the `(0,1)` and `(1,2)` blocks then -forces the three per-letter-class idempotent sums on each side to agree. The +forces the three per-letter-class idempotent sums on each side to agree, and +that relation is checked here as a linear map: rank 18 on a 27-dimensional +domain, so its kernel is exactly the nine-dimensional space of equal triples. +The search samples that family shape by shape, with class multisets built from cancellation pairs plus one unpaired idempotent where the parity requires it. All eight call-count shapes from `4+4` to `6+5` were drawn at least 1150 times diff --git a/research/ut3-central-triple-independent/RESULT.json b/research/ut3-central-triple-independent/RESULT.json index f5007e1e70..ec66231cdb 100644 --- a/research/ut3-central-triple-independent/RESULT.json +++ b/research/ut3-central-triple-independent/RESULT.json @@ -1,5 +1,10 @@ { "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "block_relation": { + "domain_dim": 27, + "kernel_dim": 9, + "rank": 18 + }, "collapse": { "mismatches": 0, "trials": 40 @@ -29,7 +34,7 @@ "physical realisation, hosting or price of the twelve formal calls" ], "package": "research/ut3-central-triple-independent", - "receipt_sha256": "9489a03aa7c5ecfee868ae53bfe9d998ec704d8081bff876082259cdbdf58418", + "receipt_sha256": "a5c3f2fc2b3ad05bc721752d9f149c0a150afc7de551aa782db93a526cbc9db7", "schema_version": 1, "search": { "class_sum_feasible": { diff --git a/research/ut3-central-triple-independent/VERIFY.json b/research/ut3-central-triple-independent/VERIFY.json index f4b84583a2..e72e22b655 100644 --- a/research/ut3-central-triple-independent/VERIFY.json +++ b/research/ut3-central-triple-independent/VERIFY.json @@ -15,7 +15,7 @@ "{package}/verify.py" ], "timeout_seconds": 600, - "checks": "Independent reconstruction of the F_2[UT_3(F_4)] paid-call model: group law over all 64 elements including associativity, the six involutions and the nine commutators; the rank-one and rank-one-idempotent census of the three-bit matrix ring by exhaustive enumeration (49 rank-one, 28 idempotent, 21 trace-zero); both twelve-call witnesses against the target on three, four and five registers with the spectator register checked fixed; all twenty-four single-deletion controls; the block collapse used by the lower-bound arguments against the direct matrix product on forty random words; the stacked corner rank; and a bounded falsification search for a realizing word of length at most eleven. No new kappa." + "checks": "Independent reconstruction of the F_2[UT_3(F_4)] paid-call model: group law over all 64 elements including associativity, the six involutions and the nine commutators; the rank-one and rank-one-idempotent census of the three-bit matrix ring by exhaustive enumeration (49 rank-one, 28 idempotent, 21 trace-zero); both twelve-call witnesses against the target on three, four and five registers with the spectator register checked fixed; all twenty-four single-deletion controls; the block collapse used by the lower-bound arguments against the direct matrix product on forty random words; the class-sum block relation and its kernel dimension; the stacked corner rank; and a bounded falsification search for a realizing word of length at most eleven. No new kappa." } ] } diff --git a/research/ut3-central-triple-independent/verify.py b/research/ut3-central-triple-independent/verify.py index 20e22c87e0..f22c2ea459 100644 --- a/research/ut3-central-triple-independent/verify.py +++ b/research/ut3-central-triple-independent/verify.py @@ -356,6 +356,51 @@ def search_class_sum_feasible(draws: int, rng: random.Random) -> dict: "tested_by_shape": dict(sorted(shape_counts.items()))} +def block_relation_check() -> dict: + """The (0,1) block of a realizing word vanishes, so the linear relation + sum_alpha m_alpha x N_alpha = 0 must hold for the three per-letter-class + idempotent sums N_alpha. Its kernel is computed by Gaussian elimination + on the 27 images of the coordinate matrices; the equal-triples space is + contained in it and has the same dimension, so the relation is + equivalent to N_1 = N_w = N_w2.""" + def flat(rows: list[int]) -> int: + width = len(rows) + value = 0 + for i, row in enumerate(rows): + for j in range(width): + if (row >> j) & 1: + value |= 1 << (i * width + j) + return value + + images = [] + for slot in range(3): + base = nilpotent(slot) + for p in range(3): + for q in range(3): + projector = [1 << q if i == p else 0 for i in range(3)] + images.append(flat(M.kron_block_rows(base, projector, 3))) + basis: list[int] = [] + for vector in images: + cur = vector + for b in basis: + cur = min(cur, cur ^ b) + if cur: + basis.append(cur) + basis.sort(reverse=True) + rank = len(basis) + # equal triples must be killed: m_1 + m_w + m_w2 = 0 + equal_image = 0 + for slot in range(3): + base = nilpotent(slot) + for p in range(3): + for q in range(3): + projector = [1 << q if i == p else 0 for i in range(3)] + equal_image ^= flat(M.kron_block_rows(base, projector, 3)) + need(equal_image == 0, "equal triple killed by the block relation") + need(rank == 18 and 27 - rank == 9, "block relation kernel is the equal triples") + return {"domain_dim": 27, "rank": rank, "kernel_dim": 27 - rank} + + def main() -> int: rng = random.Random(20261018) result = { @@ -366,6 +411,7 @@ def main() -> int: "matrix_census_r3": matrix_census(3), "witnesses": witness_checks(), "collapse": collapse_check(40, rng), + "block_relation": block_relation_check(), "corner": corner_certificate(), "search": { "uniform": search_uniform(20000, rng),