From 54cb03ce2837b0c7935b8147e28507e60114990b Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Tue, 27 Oct 2026 19:04:33 +0000 Subject: [PATCH] feat(research): classify four-term address-twist syzygies Answer the four-contribution case of PR5490's open question. At m=2 the residue always vanishes (exhaustive over 46,656 normalized triples). For m>=3 it survives only when all four frames agree and the transports sum to zero, with rank at most twice the frame rank; field witnesses attain rank two for every m>=3. --- research/bit-four-term-twist-escape/PROOF.md | 152 +++++++ research/bit-four-term-twist-escape/README.md | 84 ++++ .../bit-four-term-twist-escape/SOURCES.json | 24 ++ research/bit-four-term-twist-escape/TASK.json | 70 ++++ .../bit-four-term-twist-escape/VERIFY.json | 36 ++ research/bit-four-term-twist-escape/verify.py | 379 ++++++++++++++++++ 6 files changed, 745 insertions(+) create mode 100644 research/bit-four-term-twist-escape/PROOF.md create mode 100644 research/bit-four-term-twist-escape/README.md create mode 100644 research/bit-four-term-twist-escape/SOURCES.json create mode 100644 research/bit-four-term-twist-escape/TASK.json create mode 100644 research/bit-four-term-twist-escape/VERIFY.json create mode 100644 research/bit-four-term-twist-escape/verify.py diff --git a/research/bit-four-term-twist-escape/PROOF.md b/research/bit-four-term-twist-escape/PROOF.md new file mode 100644 index 0000000000..7893702732 --- /dev/null +++ b/research/bit-four-term-twist-escape/PROOF.md @@ -0,0 +1,152 @@ +# Four-term transport syzygies for two-sided address twists + +## Model and question + +Use the setting of JoyboyBrian's PR5490 (`research/bit-three-term-twist-rigidity/PROOF.md`), +which inherits the second-order quotient of Krzysztof Wójt's PR5003. Here +V = M_m(F2), m >= 2, and Sym^2(V) is the degree-two part of the +polynomial ring F2[V], with squares retained. A *two-sided transport* is a +map U(z) = L z R with L, R in GL_m(F2). Over F2 the pair (L, R) is +determined by U, because U corresponds to the rank-one tensor L ⊗ R^T and +the only nonzero scalar is 1. + +For an off-diagonal block (r, s), PR5490 Section 3 derives two necessary +conditions on the calls j contributing to that block. With a_j the role-r +frame reduction and U_j the induced relative transport, they are + + sum_j a_j = 0, sum_j a_j · (U_j z) = 0 in Sym^2(V) for all z. (1) + +The role-s frames are b_j = U_j^-1 a_j. Write + + beta = sum_j U_j^-1 a_j + +for the *role-s residue*. PR5490 shows that three contributions force +beta = 0. The residue then cancels from the diagonal block (s, s), which +is how its eight-call pattern is excluded. Its Open next question 1 asks +whether four or more contributions can survive this condition. This file +answers the four-contribution case. + +## Theorem + +Let a_1, ..., a_4 in V and two-sided transports U_1, ..., U_4 satisfy (1). + +1. **m = 2.** beta = 0 for all frames, not only rank-one frames. +2. **m >= 3.** If beta ≠ 0, then a_1 = a_2 = a_3 = a_4 = x ≠ 0 and + U_1 + U_2 + U_3 + U_4 = 0 as linear maps of V. Moreover + rank(beta) <= 2 rank(x). So rank(beta) <= 2 for rank-one frames. +3. **Sharpness.** For every m >= 3 there are four pairwise distinct + two-sided transports and a rank-one x with a_j = x for all j. They + satisfy (1), and rank(beta) = 2. + +So four contributions *can* survive the dirty degree-one condition once +m >= 3. The three-term rigidity does not extend. The escape is narrow: all +four role-r frames must agree modulo two, the transports must satisfy a +four-term relation, and the surviving residue has rank at most two. + +## Proof of parts 1 and 2 + +**Normalization.** Replacing z by U_4^-1 z turns (1) into the same +condition for U_j U_4^-1. The new residue is U_4 beta, which has the same +rank. Part 1 is therefore a finite statement over 36^3 transport triples +with U_4 = id. For each triple, (1) is a linear system in (a_1, a_2, a_3), +with a_4 = a_1 + a_2 + a_3. The verifier computes a kernel basis and checks +beta = 0 on every basis vector. This is enough because beta is linear in the +frames. It checks all 46,656 triples. + +**Part 2.** Assume m >= 3. Two facts are used: + +- **Rank distance.** PR5490 Section 1 proves that two distinct two-sided + transports differ by a map of rank at least m. +- **Linear syzygies.** If l_1, ..., l_d are linearly independent linear forms + and sum_i l_i f_i = 0 with each f_i linear, then f_i lies in the span of + {l_j : j ≠ i}. This is because l_1, ..., l_d form a regular sequence in the + polynomial ring, so the degree-one syzygies are spanned by the Koszul + relations. + +If some a_j = 0, at most three terms remain and PR5490's three-term lemma +gives beta = 0. So assume all four frames are nonzero. Since their sum is +zero, their span W has dimension 1, 2 or 3. + +*dim W = 3.* The frames are x, y, w, x+y+w with x, y, w independent. +Then (1) becomes + + x·((U_1+U_4)z) + y·((U_2+U_4)z) + w·((U_3+U_4)z) = 0. + +By the syzygy fact, each U_j + U_4 maps V into a span of two of x, y, w, +so it has rank at most 2 < m. Rank distance forces U_1 = U_2 = U_3 = U_4 = U. +Then beta = U^-1(sum a_j) = 0. + +*dim W = 2.* Every frame lies in {x, y, x+y}. The multiplicities +(n_x, n_y, n_(x+y)) sum to 4 with n_x + n_(x+y) and n_y + n_(x+y) even, and at +least two values occur. Up to renaming the three nonzero values, the +frames are x, x, y, y. Then (1) reads x·((U_1+U_2)z) + y·((U_3+U_4)z) = 0. +The syzygy fact gives rank(U_1+U_2) <= 1 and rank(U_3+U_4) <= 1. So +U_1 = U_2 and U_3 = U_4, and the two pairs cancel in beta. + +*dim W = 1.* All a_j = x ≠ 0. Then (1) is x·((sum_j U_j) z) = 0 for all z. The +polynomial ring has no zero divisors, so sum_j U_j = 0. Write +U_j(z) = L_j z R_j. The relation is the tensor identity +sum_j L_j ⊗ R_j^T = 0 with all factors invertible. Let d be the dimension of +span{L_j}. + +- d = 1: all L_j = L, and beta = L^-1 x (sum_j R_j^-1). Its rank is at most rank(x). +- d = 3: if some L_j were outside the span of the other three, its lone + coefficient R_j^T would vanish, which is impossible. So the one linear + dependency among the L_j has full support, and the values are + A, B, C, A+B+C. Comparing coefficients gives R_1 = R_2 = R_3 = R_4 = R, and + beta = (sum_j L_j^-1) x R^-1. Its rank is at most rank(x). +- d = 2: the values lie in {D, E, D+E}. If the multiplicities are 2, 2, 0, + then comparing coefficients gives equal R inside each pair. So the + transports cancel in pairs and beta = 0. Multiplicities 3, 1, 0 force a + lone coefficient R^T = 0, which is impossible. The remaining shape, up to + renaming, is L = (D, E, D+E, D+E). Coefficient comparison gives + R = (P, P, Q, Q+P). Then + beta = (D^-1 + E^-1) x P^-1 + (D+E)^-1 x (Q^-1 + (Q+P)^-1). Each summand has + rank at most rank(x). +- d = 4 is impossible, because then every coefficient would have to vanish. + +In every case rank(beta) <= 2 rank(x). This proves part 2. + +## Proof of part 3 + +Identify F2^m with the field F = F_(2^m), and let M_c be the matrix of +multiplication by c. Then c ↦ M_c is F2-linear and injective, and +M_c M_d = M_(cd). Take a = 1 and choose b in F outside F_4, which exists +because m >= 3. Set q = 1, q' = b and p = q + q'. Then a, b, a+b, p, q, q' are +all nonzero. Let + + L = (M_a, M_b, M_(a+b), M_(a+b)), R = (M_p, M_p, M_q, M_(q')), + +with U_j(z) = L_j z R_j and a_j = x = u v^T of rank one. Then +sum U_j(z) = M_(a+b) z M_p + M_(a+b) z M_(q+q') = 0. So (1) holds, and the +four transports are pairwise distinct. The residue is + + beta = M_(c1) x M_(d1) + M_(c2) x M_(d2), + c1 = a^-1 + b^-1, c2 = (a+b)^-1, d1 = p^-1, d2 = q^-1 + q'^-1. + +It has rank 2 exactly when M_(c1) u and M_(c2) u are independent and +M_(d1)^T v and M_(d2)^T v are independent. Since the M_c are injective and +linear in c, this holds when c1 ≠ c2 and d1 ≠ d2. In a field, +c1 = c2 is equivalent to (a+b)^2 = ab, that is, a^2 + ab + b^2 = 0. Then a/b +would be a primitive cube root of unity and would lie in F_4. With a = 1 +this would put b in F_4. The same argument applies to q, q' with q'/q = b. +Hence rank(beta) = 2. + +For m = 2 the same family uses F_4 itself. There c1 = c2 and d1 = d2, so +beta = 0, in agreement with part 1. + +The verifier checks the explicit witness for m = 3, 4, 5, 6 with the +moduli x^3+x+1, x^4+x+1, x^5+x^2+1 and x^6+x+1, taking b = x. It evaluates +(1) directly as polynomial products in Sym^2(V), independently of the +relation shortcut. It also checks pairwise rank distance, the transport +relation and rank(beta) = 2, plus a negative control. + +## Scope + +This is a statement about the necessary degree-one conditions (1) in a single +off-diagonal block. It does not synthesize a word or realize I_m diagonal +targets. It checks no other block, the PR5003 cross terms, native prices or +the five-or-more contribution case. Lifting the F2 frames and transports to +odd-denominator rank-one frames and GL_m(Z_(2)) twists, as in PR5490's model, +is routine, but this package does not check a complete group-ring word. +No kappa, supplier or multiplication-theorem claim is made. diff --git a/research/bit-four-term-twist-escape/README.md b/research/bit-four-term-twist-escape/README.md new file mode 100644 index 0000000000..1fed35db1f --- /dev/null +++ b/research/bit-four-term-twist-escape/README.md @@ -0,0 +1,84 @@ +# Four contributions survive the dirty degree-one twist condition + +**Scoped written proof with an exact finite certificate; no new κ.** +This answers the four-contribution case of Open next question 1 in +JoyboyBrian's [PR #5490](https://github.com/CrocSwap/integer-mult-bounds/pull/5490) +(`research/bit-three-term-twist-rigidity`). That package shows that three +off-diagonal contributions in the two-sided address-twist model force the +role-s residue β = Σ U_j⁻¹ a_j to vanish. That vanishing is what excludes its +eight-call pattern. + +For four contributions satisfying the same necessary conditions, +Σ a_j = 0 and Σ a_j·(U_j z) = 0 in Sym²(V) with V = M_m(F2): + +| m | Result | +|---|---| +| 2 | β = 0 for all frames. The exhaustive check covers all 46,656 normalized transport triples. | +| ≥ 3 | β ≠ 0 only if all four frames equal one x ≠ 0 and U₁+U₂+U₃+U₄ = 0. Then rank β ≤ 2·rank x. | +| ≥ 3 | Sharp: a field-multiplication family with rank-one x and four distinct transports gives rank β = 2. | + +So the three-term rigidity does **not** extend to four contributions once +m ≥ 3, but the escape is narrow. All four role-r frames must agree modulo +two, the transports must sum to zero, and the residue has rank at most two +for rank-one frames. [PROOF.md](PROOF.md) has the statement and the all-m +proof. + +This concerns the degree-one necessary conditions in one block. It is not a +synthesized word, a realization of I_m diagonal targets, a native tariff, a +supplier or a multiplication theorem. + +## Evidence + +- Part 1 (m = 2) is a finite certificate. For each normalized triple, the + verifier solves the linear system for all frames, not only rank-one + frames, and checks β = 0 on a kernel basis. +- Part 2 (m ≥ 3) is a written proof. It uses PR5490's rank-distance lemma, + linear Koszul syzygies and a classification of four-term rank-one tensor + relations Σ L_j ⊗ R_jᵀ = 0 with invertible factors. +- Part 3 is checked for m = 3, 4, 5, 6 by evaluating the products in + Sym²(V) directly. The checks also cover pairwise rank distance, the + transport relation, rank β = 2 and a perturbed-frame negative control. + The all-m argument is in PROOF.md. +- Controls: the three-term lemma at m = 2, unnormalized m = 2 spot checks, + 300 random m = 3 triples (none escapes), and the SHA256 of the pinned + PR5490 proof. + +## Reproduce + +From the repository root: + +```sh +python3.12 -I -W error -B research/bit-four-term-twist-escape/verify.py +python3.12 -I -O -W error -B research/bit-four-term-twist-escape/verify.py +python3.12 -B scripts/research_package.py --package research/bit-four-term-twist-escape +``` + +The expected last line is `PASS_FOUR_TERM_TWIST_ESCAPE`. Each run takes about +two seconds and uses only the standard library. + +## Open next questions + +1. **Can a complete pattern use the rank-two residue?** A four-term block + leaves up to rank two in the diagonal, where PR5490's three-term blocks + leave rank one. First choose a projector pattern with one block fed by four + calls whose role-r frames agree mod 2. Then impose a field-family transport + relation and check every other block and the PR5003 second-order cross + terms before any synthesis. Native twist prices remain unknown. +2. **What happens with five or more contributions?** The rank bound comes + from a short classification of four-term tensor relations. Start with the + exhaustive m = 2 census at k = 5 (36⁴ normalized quadruples), then classify + five-term relations. Frames that span two or three dimensions can now + combine with transport relations, so the four-term case split no longer + suffices. + +Structured versions are in [TASK.json](TASK.json). + +## Credit + +Produced by Nick Petalas. JoyboyBrian's PR #5490 supplies the model +reduction to condition (1), the rank-distance lemma and the three-term +lemma used here. Krzysztof Wójt's PR #5003 supplies the second-order +quotient and source compatibility, and JoyboyBrian's PR #4953 the two-sided +twist model. Retain the Cinna Davis/PR2110, Ali Romman, eumemic and huxint +lineage credited there. The four-term classification, the m = 2 census and +the field witnesses are new here. Apache-2.0. diff --git a/research/bit-four-term-twist-escape/SOURCES.json b/research/bit-four-term-twist-escape/SOURCES.json new file mode 100644 index 0000000000..bf0ab7a667 --- /dev/null +++ b/research/bit-four-term-twist-escape/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8", + "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/bit-three-term-twist-rigidity/PROOF.md", + "usage": "input", + "git_blob": "65120d64fb7e25765734584a7e389e53e83fa142", + "sha256": "6ca59361eefe1fa546d348aefce127b325149323a83d4ab10445ac6f28c6a854" + } + ] +} diff --git a/research/bit-four-term-twist-escape/TASK.json b/research/bit-four-term-twist-escape/TASK.json new file mode 100644 index 0000000000..bb25dacf1d --- /dev/null +++ b/research/bit-four-term-twist-escape/TASK.json @@ -0,0 +1,70 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "priority_revision": 8, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "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_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.", + "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse." + }, + "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": "Four-contribution case of the PR5490 dirty degree-one condition for two-sided address twists: exact classification of surviving role-s residues, rank bound 2 rank(x), sharp field witnesses for every m>=3 and four-term rigidity at m=2.", + "scope_change_reason": "Answers Open next question 1 of JoyboyBrian PR5490 (four or more off-diagonal contributions) in its four-term case, within that package's model, instead of a new register census.", + "bottleneck_link": "Scoped side result for the address-twist register model. It shows that the three-term rigidity route cannot exclude patterns with a four-contribution block when m>=3 and states exactly which frame and transport relations such a block needs. No native price, supplier or kappa change.", + "budget_minutes": 60, + "stop_rule": "Stop after the four-term classification, the exhaustive m=2 check and the explicit m>=3 witnesses; no five-term or whole-word synthesis.", + "outcome": "completed", + "evidence": "PROOF.md (all-m written proof of parts 2 and 3) and verify.py (exhaustive m=2 census for part 1, direct Sym^2 evaluation of the m=3..6 witnesses, controls).", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can a complete pattern use a four-contribution block's rank-two residue to reach invertible diagonal targets?", + "why_it_matters": "PR5490 excludes its eight-call pattern because three-term blocks leave rank-one diagonals. A four-term block now leaves up to rank two, which is the first opening for m=3 targets beyond that obstruction.", + "first_step": "Choose a projector pattern with one block fed by four calls whose role-r frames agree mod 2. Impose the transport relation sum U_j = 0 from the field family and check every other block and the PR5003 second-order cross terms before any synthesis.", + "blocked_by": "No pattern is supplied. Other blocks, chronology at second order and native twist prices are unchecked." + }, + { + "question": "What is the largest residue rank for k >= 5 contributions?", + "why_it_matters": "The four-term bound rank(beta) <= 2 rank(x) depends on a short tensor-relation classification. Longer syzygies may allow larger residues or new frame shapes.", + "first_step": "Run the same exhaustive normalized census for k = 5 at m = 2 (36^4 normalized transport quadruples), then classify five-term rank-one tensor relations among invertible pairs.", + "blocked_by": "Mixed cases where frames span two or three dimensions combine with transport relations, so the four-term case split no longer suffices." + } + ] +} diff --git a/research/bit-four-term-twist-escape/VERIFY.json b/research/bit-four-term-twist-escape/VERIFY.json new file mode 100644 index 0000000000..c014434f61 --- /dev/null +++ b/research/bit-four-term-twist-escape/VERIFY.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/bit-three-term-twist-rigidity/PROOF.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Pinned PR5490 proof bytes; exhaustive m=2 four-term census (46,656 normalized transport triples, all frames); unnormalized spot checks; three-term positive control; rank-2 field witnesses for m=3..6 evaluated directly in Sym^2(V); random m=3 controls and a negative control." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Same checks with assertions disabled (the verifier does not use assert)." + } + ] +} diff --git a/research/bit-four-term-twist-escape/verify.py b/research/bit-four-term-twist-escape/verify.py new file mode 100644 index 0000000000..1f34e52645 --- /dev/null +++ b/research/bit-four-term-twist-escape/verify.py @@ -0,0 +1,379 @@ +#!/usr/bin/env python3 +"""Exact checks for the four-term address-twist classification. + +V = M_m(F2) is stored as an m*m-bit integer (entry (r, c) at bit r*m+c). +A two-sided transport z -> L z R is stored as the tuple of images of the +basis matrices. Sym^2(V) is the degree-two part of F2[t_0, ..., t_(N-1)], +squares retained, as in PR5490 equation (1). + +Nick Petalas. Apache-2.0. Standard library only; no predecessor code imported. +""" +from itertools import product +from pathlib import Path +import hashlib +import json +import random + +PASS = 'PASS_FOUR_TERM_TWIST_ESCAPE' + + +def need(ok, why): + if not ok: + raise SystemExit('FAIL: ' + why) + + +# --- matrices over F2 ----------------------------------------------------- + +def mat_mul(a, b, m): + out = 0 + for r in range(m): + for c in range(m): + v = 0 + for k in range(m): + v ^= (a >> (r*m+k)) & (b >> (k*m+c)) & 1 + out |= v << (r*m+c) + return out + + +def mat_rank(a, m): + rows = [(a >> (r*m)) & ((1 << m)-1) for r in range(m)] + return vec_rank(rows) + + +def vec_rank(vectors): + pivots = {} + for x in vectors: + while x: + k = x.bit_length()-1 + if k not in pivots: + pivots[k] = x + break + x ^= pivots[k] + return len(pivots) + + +def identity(m): + return sum(1 << (r*m+r) for r in range(m)) + + +def general_linear(m): + return [a for a in range(1 << (m*m)) if mat_rank(a, m) == m] + + +def mat_inv(a, m): + one = identity(m) + power = a + while True: # finite group: some power of a is the identity + nxt = mat_mul(power, a, m) + if nxt == one: + return power + power = nxt + + +# --- transports on V ------------------------------------------------------ + +def transport(left, right, m): + return tuple(mat_mul(mat_mul(left, 1 << k, m), right, m) + for k in range(m*m)) + + +def apply(u, x): + y = 0 + k = 0 + while x: + if x & 1: + y ^= u[k] + x >>= 1 + k += 1 + return y + + +def map_sum(maps): + return tuple(_xor_all(column) for column in zip(*maps)) + + +def _xor_all(values): + y = 0 + for v in values: + y ^= v + return y + + +def map_rank(u): + return vec_rank(list(u)) + + +# --- Sym^2 condition, written two independent ways -------------------------- + +def sym2_product(a, w, n): + """Coefficients of the product of linear forms a and w in Sym^2(V).""" + coeff = {} + for p in range(n): + if not (a >> p) & 1: + continue + for q in range(n): + if (w >> q) & 1: + key = (min(p, q), max(p, q)) + coeff[key] = coeff.get(key, 0) ^ 1 + return {k for k, v in coeff.items() if v} + + +def degree_one_residue(frames, maps, n): + """Return (sum a_i, [sum_i a_i*(U_i e_t) for every basis e_t]).""" + constant = _xor_all(frames) + residues = [] + for t in range(n): + total = set() + for a, u in zip(frames, maps): + total ^= sym2_product(a, u[t], n) + residues.append(total) + return constant, residues + + +def survives(frames, maps, n): + constant, residues = degree_one_residue(frames, maps, n) + return constant == 0 and all(not r for r in residues) + + +def kernel_basis(equations, nvars): + pivots = {} + for e in equations: + for k, v in pivots.items(): + if (e >> k) & 1: + e ^= v + if e: + k = e.bit_length()-1 + for kk in list(pivots): + if (pivots[kk] >> k) & 1: + pivots[kk] ^= e + pivots[k] = e + basis = [] + for f in range(nvars): + if f in pivots: + continue + x = 1 << f + for k, v in pivots.items(): + if (v >> f) & 1: + x |= 1 << k + basis.append(x) + return basis + + +def solution_space(maps, n): + """Basis of all (a_1..a_k) with sum a_i = 0 and the degree-two identity. + + Variables are a_1..a_(k-1); a_k is their sum. The identity says that + the matrix sum_i a_i (U_i e_t)^T is alternating (symmetric, zero diagonal). + """ + k = len(maps) + last = maps[-1] + equations = [] + for t in range(n): + for p in range(n): + for q in range(p, n): + e = 0 + cells = [(p, q)] if p == q else [(p, q), (q, p)] + for j in range(k-1): + for row, col in cells: + if ((maps[j][t] ^ last[t]) >> col) & 1: + e ^= 1 << (j*n+row) + equations.append(e) + basis = [] + mask = (1 << n)-1 + for x in kernel_basis(equations, (k-1)*n): + frames = [(x >> (j*n)) & mask for j in range(k-1)] + frames.append(_xor_all(frames)) + basis.append(frames) + return basis + + +def residue_beta(frames, inverse_maps): + return _xor_all(apply(v, a) for v, a in zip(inverse_maps, frames)) + + +# --- checks --------------------------------------------------------------- + +def all_transports(m): + gl = general_linear(m) + pairs = {} + for left, right in product(gl, repeat=2): + pairs.setdefault(transport(left, right, m), (left, right)) + return pairs + + +def check_m2_exhaustive(): + m, n = 2, 4 + pairs = all_transports(m) + maps = sorted(pairs) + need(len(maps) == 36, 'GL2(F2) two-sided transports') + ident = tuple(1 << k for k in range(n)) + for u, v in product(maps, repeat=2): + if u != v: + need(map_rank(map_sum([u, v])) >= m, 'rank distance m=2') + inverse = {u: transport(mat_inv(l, m), mat_inv(r, m), m) + for u, (l, r) in pairs.items()} + need(all(apply(inverse[u], apply(u, x)) == x + for u in maps for x in range(1 << n)), 'inverse transports') + dims = {} + tuples = 0 + for triple in product(maps, repeat=3): + quad = list(triple)+[ident] + inv = [inverse[u] for u in quad] + basis = solution_space(quad, n) + dims[len(basis)] = dims.get(len(basis), 0)+1 + for frames in basis: + need(survives(frames, quad, n), 'kernel solves (1)') + need(residue_beta(frames, inv) == 0, 'm=2 four-term residue') + tuples += 1 + need(tuples == 36**3, 'm=2 tuple count') + return tuples, dict(sorted(dims.items())) + + +def check_m2_normalization_spot(): + """Spot-check U_4 = id normalization: beta transforms by U_4.""" + m, n = 2, 4 + pairs = all_transports(m) + maps = sorted(pairs) + inverse = {u: transport(mat_inv(l, m), mat_inv(r, m), m) + for u, (l, r) in pairs.items()} + rng = random.Random(5490) + for _ in range(200): + quad = [rng.choice(maps) for _ in range(4)] + for frames in solution_space(quad, n): + need(residue_beta(frames, [inverse[u] for u in quad]) == 0, + 'm=2 unnormalized four-term residue') + + +def field_multiplication(m, poly): + """Matrices of multiplication by every element of F2[x]/(poly).""" + def mulmod(a, b): + r = 0 + while b: + if b & 1: + r ^= a + b >>= 1 + a <<= 1 + if (a >> m) & 1: + a ^= poly + return r + mats = {} + for c in range(1 << m): + cols = [mulmod(c, 1 << j) for j in range(m)] + mats[c] = sum(((cols[j] >> i) & 1) << (i*m+j) + for i in range(m) for j in range(m)) + return mats, mulmod + + +IRREDUCIBLE = {3: 0b1011, 4: 0b10011, 5: 0b100101, 6: 0b1000011} + + +def field_inverse(c, m, mulmod): + for d in range(1, 1 << m): + if mulmod(c, d) == 1: + return d + raise SystemExit('FAIL: zero has no inverse') + + +def check_witness(m): + n = m*m + mats, mulmod = field_multiplication(m, IRREDUCIBLE[m]) + need(all(mat_rank(mats[c], m) == m for c in range(1, 1 << m)), + 'irreducible modulus for m=%d' % m) + a, b = 1, 0b10 # b = x is outside F4 for m >= 3 + need(mulmod(b, b) ^ b ^ 1 != 0, 'b^2+b+1 nonzero') + q, q2 = 1, 0b10 + p = q ^ q2 + lefts = [a, b, a ^ b, a ^ b] + rights = [p, p, q, q2] + need(all(v != 0 for v in lefts+rights), 'nonzero field elements') + maps = [transport(mats[l], mats[r], m) for l, r in zip(lefts, rights)] + need(len(set(maps)) == 4, 'four distinct transports') + for i in range(4): + for j in range(i+1, 4): + need(map_rank(map_sum([maps[i], maps[j]])) >= m, + 'witness rank distance') + need(all(c == 0 for c in map_sum(maps)), 'transport relation sum U_i = 0') + x = 1 # E_00, rank one + frames = [x]*4 + need(survives(frames, maps, n), 'witness satisfies (1) for m=%d' % m) + inverse = [transport(mats[field_inverse(l, m, mulmod)], + mats[field_inverse(r, m, mulmod)], m) + for l, r in zip(lefts, rights)] + for u, v in zip(maps, inverse): + need(all(apply(v, apply(u, 1 << k)) == 1 << k for k in range(n)), + 'witness inverse') + beta = residue_beta(frames, inverse) + need(mat_rank(beta, m) == 2, 'witness residue rank 2 for m=%d' % m) + # A perturbed control: changing one frame breaks the identity. + need(not survives([x, x, x, x ^ (1 << 1)], maps, n), 'negative control') + return beta + + +def check_m3_random_triples(samples): + """Random m=3 tuples: generic transports admit only beta = 0.""" + m, n = 3, 9 + gl = general_linear(m) + need(len(gl) == 168, '|GL3(F2)|') + rng = random.Random(1022) + ident = tuple(1 << k for k in range(n)) + nonzero = 0 + for _ in range(samples): + pairs = [(rng.choice(gl), rng.choice(gl)) for _ in range(3)] + quad = [transport(l, r, m) for l, r in pairs]+[ident] + inv = [transport(mat_inv(l, m), mat_inv(r, m), m) for l, r in pairs] + inv.append(ident) + rel = all(c == 0 for c in map_sum(quad)) + for frames in solution_space(quad, n): + if residue_beta(frames, inv): + need(rel and len(set(frames)) == 1, 'escape outside the form') + nonzero += 1 + return nonzero + + +def check_three_term_control(): + """Positive control: three terms at m=2 are rigid (PR5490 lemma).""" + m, n = 2, 4 + pairs = all_transports(m) + maps = sorted(pairs) + inverse = {u: transport(mat_inv(l, m), mat_inv(r, m), m) + for u, (l, r) in pairs.items()} + ident = tuple(1 << k for k in range(n)) + for u, v in product(maps, repeat=2): + triple = [u, v, ident] + for frames in solution_space(triple, n): + need(residue_beta(frames, [inverse[w] for w in triple]) == 0, + 'three-term control') + + +def check_pinned_sources(): + package = Path(__file__).resolve().parent + root = package.parents[1] + rows = json.loads((package / 'SOURCES.json').read_text())['files'] + live = [r for r in rows if r['usage'] == 'input'] + need(live, 'live input pins') + for row in live: + data = (root / row['path']).read_bytes() + need(hashlib.sha256(data).hexdigest() == row['sha256'], + 'pinned bytes for ' + row['path']) + proof = (root / live[0]['path']).read_text() + need('## 2. Three-term quadratic rigidity' in proof, + 'PR5490 three-term lemma present') + + +def main(): + check_pinned_sources() + tuples, dims = check_m2_exhaustive() + check_m2_normalization_spot() + check_three_term_control() + witnesses = {m: check_witness(m) for m in (3, 4, 5, 6)} + escapes = check_m3_random_triples(300) + need(escapes == 0, 'random m=3 triples should not hit a relation') + print('m=2 exhaustive four-term tuples (U_4 = id):', tuples) + print('m=2 solution-space dimension histogram:', dims) + print('rank-2 witnesses, residue bitmasks:', + {m: hex(b) for m, b in witnesses.items()}) + print(PASS) + + +if __name__ == '__main__': + main()