Prove unbounded two-role right-vector cost over F2[t] (no new κ)

research/right-vector-polynomial-cost/PROOF.md

@@ -0,0 +1,132 @@
+# Exact polynomial right-vector cost
+
+Work over K=F2, R=F2[t], with two data roles and no scratch roles.
+A paid factor is P(u,y)=I+u y^T, u in R^2 and y in K^2.
+Every GL2(K) map is free anywhere. Cost counts paid factors.
+All words below are written in algebraic product order.
+
+## Statement
+
+For each nonzero binary row y=(a,b), put v_y=(b,a)^T and
+N_y=v_y y. For f in t F2[t], write T_y(f)=I+f N_y.
+Every invertible target has a unique expression
+
+    T_(y1)(f1) ... T_(yr)(fr) S,
+
+where S is in GL2(F2), every f_i is nonzero with zero constant term,
+and consecutive directions y_i differ. Its exact paid cost is r.
+In particular, with U=T_(0,1)(t), L=T_(1,0)(t),
+
+    M = U L U L = [[1+t^2+t^4, t^3], [t^3, 1+t^2]]
+
+has cost 4. More generally (UL)^k has cost 2k for every k>=1.
+Thus there is no uniform finite cost bound over all K-algebras, even
+for two-role invertible targets over a commutative integral domain.
+For k>=1, delta((UL)^k)=2, so the gap from the column lower bound
+is unbounded too.
+
+This is the right-vector cost consequence of classical polynomial-matrix
+normal forms, not a claim to a new group-theoretic normal-form theorem.
+Nagao, *On GL(2,K[x])* (1959), Theorem 2 and its degree argument,
+provides the classical structural context:
+https://www.i-repository.net/contents/osakacu/sugaku/DB-M-010-02-04.pdf .
+The proof below is self-contained for this binary cost statement.
+
+## 1. An invertible word only uses invertible paid factors
+
+Since R is commutative, det of a product is the product of determinants.
+The only unit of F2[t] is 1. If a word has invertible endpoint, each
+factor has determinant 1. For P(u,y), det P=1+y^T u. If y is nonzero,
+invertibility therefore forces y^T u=0. The solution space of that
+equation is u=f v_y for a unique polynomial f, including f=0.
+Hence every usable paid factor is T_y(f). The case y=0 is identity.
+Singular factors cannot evade this reduction.
+
+We have N_y^2=0 and T_y(f)T_y(g)=T_y(f+g). Split
+f=f(0)+(f+f(0)); the constant part T_y(f(0)) is free. For any free S,
+conjugation S T_y(f) S^-1 is T_z(f) for another nonzero binary row z.
+Indeed the conjugated nonzero nilpotent has image equal to kernel,
+and over F2 there is exactly one nonzero rank-one nilpotent with each
+of the three kernel lines. This also follows directly from z=y S^-1
+and S v_y=v_z, since every invertible binary 2x2 determinant is 1.
+
+Move all free factors to the right, split off all constant parts,
+and merge adjacent equal directions, deleting zero coefficients.
+Every finite invertible word thus has the stated form with at most
+as many nonconstant factors as its original paid count. Evaluation at
+t=0 shows the final free matrix is necessarily S=M(0).
+
+## 2. A reduced nonempty word cannot be constant
+
+For distinct nonzero binary rows y,z,
+
+    y v_z = a d + b c = 1
+
+when y=(a,b), z=(c,d). Consequently
+
+    N_(y1) ... N_(yr) = v_(y1) y_r != 0
+
+whenever adjacent directions differ. Let d_i=deg f_i>=1. In the
+expansion of a reduced product, the term choosing f_i N_(yi) from
+every factor has degree D=sum d_i and nonzero leading coefficient
+v_(y1) y_r. Every term omitting at least one factor has smaller degree.
+Thus the degree of the matrix product, defined as the maximum entry
+degree, is exactly D>0. Multiplication by an invertible constant S
+preserves this degree because its leading matrix remains nonzero.
+
+This proves the degree test for arbitrary polynomial coefficients,
+without any degree cap or finite search assumption.
+
+## 3. Uniqueness and exact cost
+
+Suppose two reduced products are equal. Their free endpoints agree by
+evaluation at zero, so cancel them. Multiply the inverse of one product
+by the other. Since each T_y(f) is its own inverse, cancel the common
+initial factors at the middle of this concatenation. At the first
+mismatch, either the directions differ, or their nonzero coefficients
+sum to a nonzero polynomial in tF2[t]. In the latter case merge that
+pair. The remaining concatenation is reduced and nonempty unless the
+original products agreed factor by factor. A nonempty reduced product
+has positive degree by Section 2, so cannot be identity. This proves
+uniqueness.
+
+Now a target with reduced length r has a literal r-paid-factor word.
+Any other word with q paid factors reduces to the same unique expression
+and the reduction does not increase the number of paid factors. Hence
+q>=r, proving cost=r.
+
+For completeness every GL2(F2[t]) target is reachable. Euclidean row
+reduction on its first column uses row swaps and shears adding a
+polynomial multiple of one row to the other. The swaps are free and
+the shears are paid factors. The first-column gcd is 1 because the
+determinant is 1. After it is changed to (1,0)^T, the remaining matrix
+is [[1,b],[0,1]], also a paid factor. The usual polynomial division
+strictly decreases the nonzero remainder degree, so this process
+terminates. Reversing these invertible operations gives a finite word.
+This existence argument is not needed for the four-factor lower bound.
+
+## 4. The first counterexample and its corollary
+
+U,L have different directions and coefficient t. Their alternating
+word of length 2k is already reduced, so costs exactly 2k. Direct
+multiplication at k=2 gives the displayed M. In particular a third
+factor never suffices for M. This answers Open next question 1 of
+Nick Petalas's #4276 negatively. The proof covers arbitrary polynomial
+left coefficients and all insertions of free binary maps, rather than
+only words in U and L.
+
+By the column lower bound and one-factor criterion of #4243/#4276,
+delta<=1 would imply cost<=1. Delta is at most two for two roles,
+so every (UL)^k with k>=1 has delta=2. This is predecessor use, not
+an independent re-verification of that criterion.
+
+## Scope
+
+This is a scoped algebraic proof, with a finite corroborating census.
+The algebra F2[t] is not semilocal: its distinct irreducible polynomials
+give infinitely many maximal ideals. It lies outside #4749's hypothesis.
+No contradiction with the semilocal three-factor theorem follows.
+The polynomial t here is an algebra coefficient, not a free change of
+basis. Allowing GL2(F2[t]) for free would change the question.
+No native preparation, conversion, precision, routing, restoration,
+stock, supplier admission or multiplication theorem is proved.

research/right-vector-polynomial-cost/README.md

@@ -0,0 +1,108 @@
+# Two-role polynomial targets have unbounded right-vector cost
+
+Claim type: scoped proof, with a finite exact certificate. No new kappa.
+
+In the alphabet `I+u y^T`, with `u in F2[t]^2`, binary `y`, and free
+`GL2(F2)` maps anywhere, put
+
+```text
+U = [[1,t],[0,1]], L = [[1,0],[t,1]].
+M = (UL)^2 = [[1+t^2+t^4, t^3], [t^3, 1+t^2]].
+cost(M) = 4; cost((UL)^k) = 2k for every k >= 1.
+```
+
+This answers Open next question 1 of
+[Nick Petalas's #4276](https://github.com/CrocSwap/integer-mult-bounds/pull/4276)
+negatively: reachable two-role targets need not have three-factor words over
+every coefficient algebra. The gap from `delta`, which equals two on this
+family, is unbounded. The algebra is commutative but not semilocal, so this
+lies outside the three-factor theorem of
+[#4749](https://github.com/CrocSwap/integer-mult-bounds/pull/4749), pinned at
+`29e4d3a25225a219f97c3a2815ed3a5a8fd9b891`.
+
+[PROOF.md](PROOF.md) reduces every invertible paid factor to a transvection,
+removes its constant part using the free group, and proves uniqueness of the
+resulting reduced word by polynomial degree. Its reduced length is the exact
+paid cost. The normal-form structure is classical polynomial-matrix theory;
+the contribution is its explicit cost consequence for the repository's
+restricted alphabet and its open three-factor question.
+
+## Evidence and reproduction
+
+The verifier uses literal binary polynomial arithmetic and no predecessor
+code. It enumerates every invertible 2x2 polynomial matrix whose maximum
+entry degree is at most four. The 1,536 distinct targets have exact cost
+histogram `[6,270,612,504,144]` for costs zero through four. The written degree
+proof establishes why arbitrary larger coefficients cannot produce additional
+shorter words in this domain. All 1,008 reduced expressions of degree four
+and length at most three, including every free endpoint, miss M.
+
+A separate literal alphabet check enumerates all three nonzero binary right
+vectors and all `32^2` polynomial left vectors of degree at most four.
+Exactly 96 parameter tuples are invertible, including repeated identities.
+Every tuple passes the constant split and all six free conjugations.
+Seven controls distinguish equal-direction cancellation, constant polynomial
+relations, specialization at zero, a dropped factor, reversed order, a
+singular factor and a changed target entry. Every comparison remains active
+under optimized Python. No generated output is written to the checkout.
+
+From the repository root, using the Python 3.12 standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B -W error research/right-vector-polynomial-cost/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -O -B -W error research/right-vector-polynomial-cost/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/right-vector-polynomial-cost
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/right-vector-polynomial-cost --check-source-history
+```
+
+Expected marker: `PASS_RIGHT_VECTOR_POLYNOMIAL_COST targets=1536 cost4=144
+target_cost=4 shorter_exclusions=1008 controls=7 no_new_kappa`.
+The receipt is freshly generated from actual checks and hashes every package
+file. It is not a handwritten verification receipt.
+
+## Limitations
+
+The universal argument is a written scoped proof. Its finite certificate
+corroborates the degree-four domain; it does not prove the infinite statement
+by enumeration. The base field is binary, the coefficient algebra is F2[t],
+and there are two data roles with no scratch. Singular targets, other base
+fields and multivariate algebras are not classified. Free maps must be binary.
+Native preparation, conversion, routing, control, precision, restoration and
+stock costs are unknown. No supplier, selected-frontier change or complete
+multiplication theorem is claimed. Independent human and formal proof-kernel
+review are unclaimed. Lean, Docker and the selected operator replay were not
+run and are outside this result's obligations.
+
+The verifier uses managed Python allocation with an explicit finite domain.
+The census stores 256 normal words and 1,536 targets. Enumeration has at most
+four factor rounds, three directions, 15 nonconstant coefficients and six free
+maps; the literal control examines 3,072 tuples. Polynomial multiplication
+accepts at most 32 bits per operand and iterates over at most 32 bits.
+Functions are below 60 lines, recursion and dynamic code are absent, and both
+registered commands make warnings errors. Python allocation is a documented
+allocation deviation with these fixed bounds; no real-time claim is made.
+
+## Open next questions
+
+1. Classify exact costs over `F2[s,t]`. Start with a named reachable word and
+   distinguish its cost from general reachability. The present one-variable
+   normal-form and Euclidean arguments do not settle that algebra.
+2. Identify one coefficient algebra in a literal native producer/consumer,
+   then price left-coefficient preparation and the complete physical bill.
+   All native costs listed above remain blockers to a supplier construction.
+
+## Credit
+
+This contribution was produced by Nick Petalas. The right-vector alphabet and
+column lower bound are Wentao Li's #4099, building on #2513. Nick Petalas's
+#4243 supplies the free-map normal form, and #4276 supplies the one-factor
+criterion and asks the all-algebra three-factor question answered here.
+ToikY's #4334 and Nick Petalas's #4601/#4749 supply the field-product,
+local-product and semilocal predecessor boundaries. Their proofs and
+certificates are cited, not re-audited.
+
+The polynomial-matrix group structure and degree method retain Hirosi
+Nagao's credit, *On GL(2,K[x])*, 1959, Theorem 2 and its proof
+([original paper](https://www.i-repository.net/contents/osakacu/sugaku/DB-M-010-02-04.pdf)).
+The restricted-alphabet cost consequence is proved here without relying on
+a machine implementation of that theorem. Apache-2.0.

research/right-vector-polynomial-cost/SOURCES.json

@@ -0,0 +1,24 @@
+{
+  "schema_version": 1,
+  "base_commit": "b58ad9ef4d4e861b0eaa5dba41742bdc072dca51",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395",
+      "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602",
+      "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72"
+    },
+    {
+      "path": "research/right-vector-two-factor-criterion/PROOF.md",
+      "usage": "input",
+      "git_blob": "71888afa0db63d6d332cbbdc408abf1aa879681c",
+      "sha256": "c1065c51c839d11b0d31bccb8d39ebc07a869eb0f29899038518e3090a58c895"
+    }
+  ]
+}

research/right-vector-polynomial-cost/TASK.json

@@ -0,0 +1,74 @@
+{
+  "schema_version": 1,
+  "task_id": "connector-alphabet-change",
+  "priority_revision": 7,
+  "base_commit": "b58ad9ef4d4e861b0eaa5dba41742bdc072dca51",
+  "original_card": {
+    "id": "connector-alphabet-change",
+    "question": "Does one explicit extension of the connector alphabet offer a favorable completed budget?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "research/universal-connector-boundary/README.md",
+      "certificates/selected-result.json"
+    ],
+    "methods": [
+      "Construct and charge a legal extra operation on a minimal instance.",
+      "Prove a target-specific bound after adding one specified operation family."
+    ],
+    "acceptance_gate": "State which fixed-alphabet premise changes and charge its implementation; do not declare it free. 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",
+        "research/universal-connector-boundary/verify.py"
+      ],
+      "expected": "PASS_UNIVERSAL_CONNECTOR_BOUNDARY",
+      "inspect": "Reproduce the 945-pairing control, then read Exact interface to list the allowed calls.",
+      "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay."
+    },
+    "first_experiment": "Add exactly one legally priced operation and test a tiny dirty-input instance before enumerating larger cases.",
+    "bottleneck_link": "A new legal connector operation could change recursive interface cost; a larger census in the same alphabet is a separate side result.",
+    "allowed_variations": [
+      "Choose one additional operation and a small source count for its first counterexample."
+    ],
+    "scope_change_triggers": [
+      "Keeping the alphabet and only increasing the source count; record this as a changed assignment.",
+      "Extending a source-count census without naming a supplier/interface decision it could change; audit #2973 pruning concerns before relying on the affected predecessor exclusions."
+    ],
+    "overlap_terms": [
+      "universal connector",
+      "source-toggle",
+      "connector alphabet"
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Exact right-vector paid cost for invertible two-role targets over F2[t]; cost four for (UL)^2 and unbounded cost 2k for (UL)^k.",
+  "scope_change_reason": "The connector card is changed to the all-algebra three-factor question explicitly left open by #4276. The non-semilocal polynomial coefficient algebra changes the semilocal premise of #4749. This is a formal-alphabet side result, not an extension of the source-toggle census.",
+  "bottleneck_link": "A scoped obstruction to a universal three-factor abstraction. The result gives no native implementation or multiplication saving.",
+  "budget_minutes": 60,
+  "stop_rule": "Package the first exact cost-four target, its reduced-word lower bound and direct corollary; do not search larger examples.",
+  "outcome": "completed",
+  "evidence": "PROOF.md gives a self-contained quantified degree proof. verify.py enumerates all 1536 invertible polynomial matrices of maximum entry degree at most four, with cost histogram [6,270,612,504,144], checks 96 literal invertible paid parameter tuples and seven negative controls, and emits a generated file-bound receipt.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "What is the exact right-vector cost over a multivariate polynomial algebra such as F2[s,t]?",
+      "why_it_matters": "The one-variable degree normal form and Euclidean reachability do not supply a classification there.",
+      "first_step": "Specify one reachable word whose two variable directions cannot be collapsed by the single-variable argument; separate reachability from lower bounds.",
+      "blocked_by": "No multivariate normal-form or reachability theorem is supplied here."
+    },
+    {
+      "question": "Which finitely generated coefficient algebras occurring in a literal native interface preserve a bounded two-role cost?",
+      "why_it_matters": "The abstract alphabet can have unbounded cost, while the semilocal theorem gives a three-factor bound.",
+      "first_step": "Identify one actual coefficient algebra and price polynomial left-coefficient preparation, conversion and the complete consumer.",
+      "blocked_by": "Native preparation, conversion, routing, precision, restoration and stock costs are unknown."
+    }
+  ],
+  "upstream_check": {
+    "commit": "1f87c3578ae546c8f903f7f4d83dc2e2fb99650b",
+    "checked_at": "2026-10-22T19:22:25.168050+00:00",
+    "priority_revision": 7,
+    "result": "Relevant guidance, selected record, catalogue and pinned proof input unchanged from the frozen scientific baseline. New main research README searches found no polynomial-cost duplicate."
+  }
+}

research/right-vector-polynomial-cost/VERIFY.json

@@ -0,0 +1,34 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/right-vector-two-factor-criterion/PROOF.md"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "-W",
+        "error",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Literal polynomial-matrix census of all 1536 degree-at-most-four invertible targets, reduced-word degree identities, cost-four witness, 1008 shorter degree-four exclusions, 96 literal invertible paid parameter tuples, free conjugation and seven negative controls. Generated receipt binds all six package files. Checks remain active under optimization."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-O",
+        "-B",
+        "-W",
+        "error",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Literal polynomial-matrix census of all 1536 degree-at-most-four invertible targets, reduced-word degree identities, cost-four witness, 1008 shorter degree-four exclusions, 96 literal invertible paid parameter tuples, free conjugation and seven negative controls. Generated receipt binds all six package files. Checks remain active under optimization."
+    }
+  ]
+}