Prove four-term address-twist syzygies survive at m≥3 with residue rank ≤2 (no new κ)

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.

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.

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"
+    }
+  ]
+}

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."
+    }
+  ]
+}

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)."
+    }
+  ]
+}