Prove an all-length radical pencil obstruction for any role count

research/multirole-radical-pencil/README.md

@@ -0,0 +1,238 @@
+# A multi-role square-zero radical pencil obstruction
+
+**Scoped proof, with finite corroboration. No new kappa.** Over any field K,
+let R = K[x,y]/(x,y)^2. Paid factors on n roles are I + u v^T, where u is
+in R^n and v is in K^n. Arbitrary GL_n(K) maps are free and may occur anywhere.
+If A in M_n(K) has no left eigenvector over K, then
+
+```text
+M = xI + yA
+```
+
+is unreachable by any finite word. This is an arbitrary-length obstruction,
+not a failed bounded search. Extra roles restored to the identity are outside
+the statement.
+
+An explicit three-role instance over F2 is
+
+```text
+    [0 0 1]
+A = [1 0 1],       A^3 + A + I = 0.
+    [0 1 0]
+```
+
+The polynomial t^3+t+1 has no binary root. The verifier also enumerates all
+512 binary three-by-three matrices and finds 48 with no binary left
+eigenvector. Each of the corresponding 48 pencils is unreachable by the
+theorem. This is not a count of every unreachable pencil.
+
+This package was produced by Nick Petalas. Apache-2.0.
+
+## What changes and predecessor credit
+
+[PR #4745](https://github.com/CrocSwap/integer-mult-bounds/pull/4745), exact
+head `3edea13af13b755932852e9306a714b317630dda`, gives the complete two-role
+square-zero radical criterion and introduces its first-zero scalar-prefix
+argument. Its README limits that classification to two roles. This package
+uses the same idea to obtain a necessary condition at arbitrary role count.
+It does not audit or replay #4745 and does not assert a multi-role converse.
+
+The free-map normal form is from Nick Petalas's
+[PR #4243](https://github.com/CrocSwap/integer-mult-bounds/pull/4243).
+The right-vector alphabet and column bound are Wentao Li's
+[PR #4099](https://github.com/CrocSwap/integer-mult-bounds/pull/4099), following
+[PR #2513](https://github.com/CrocSwap/integer-mult-bounds/pull/2513).
+ToikY's #4334 and Nick Petalas's #4276/#4601/#4749 are the related two-role
+general-target and invertible-target successors. No predecessor code or
+finite enumeration is imported. The proof below is self-contained.
+
+The `connector-alphabet-change` card is **changed** to an algebraic side
+question in the existing alphabet. It is not a new legally priced connector.
+The card's first working control passed with `pairings=945`, `queries=74`.
+That control is orientation, not evidence for this theorem.
+
+## Proof
+
+Write a ring-valued matrix uniquely as P_0 + xP_x + yP_y, with all three
+coefficient matrices over K. Products obey
+
+```text
+(TP)_0 = T_0 P_0
+(TP)_x = T_0 P_x + T_x P_0
+(TP)_y = T_0 P_y + T_y P_0.
+```
+
+### Normalize free maps
+
+For G in GL_n(K), conjugation sends I+u v^T to
+I+(Gu)(v^T G^-1), still a paid factor. Move every free map to the right.
+An alleged word for M therefore has the form
+
+```text
+M = F_L ... F_1 G = P G.
+```
+
+Consequently P_0=0, P_x=G^-1 and P_y=A G^-1. In particular P_x is invertible.
+
+### The first zero scalar prefix
+
+Let k be the first index at which the scalar part of F_k ... F_1 is zero.
+It exists since P_0=0. Immediately before it the scalar prefix H is nonzero.
+Write
+
+```text
+F_k = I + (a + xb + yc) v^T,
+T   = I + a v^T.
+```
+
+Here TH=0. A rank-one perturbation of I has nullity at most one. Since
+H is nonzero, T is singular, rank(H)=1, v^T a=-1, and v^T T=0.
+The kernel of T is K a, so H=a r^T for a nonzero row r^T. Thus
+psi = v^T H = -r^T is nonzero.
+
+Let C_x,C_y be the radical coefficient matrices before this step. Immediately
+after the step they are
+
+```text
+D_x = T C_x + b v^T H,
+D_y = T C_y + c v^T H.
+```
+
+Multiplication by v^T kills the first summands, giving
+
+```text
+v^T D_x = alpha psi,       alpha = v^T b,
+v^T D_y = beta  psi,       beta  = v^T c.
+```
+
+This common-row identity is the essential restriction imposed by the
+base-field right vector. No assumption on earlier radical coefficients was
+made.
+
+### Later factors cannot remove the restriction
+
+After the first zero scalar prefix, the scalar prefix stays zero. Radical
+parts of every later factor multiply a zero scalar prefix and contribute
+nothing. If S is the product of their scalar parts, the final coefficients are
+
+```text
+P_x = S D_x = G^-1,
+P_y = S D_y = A G^-1.
+```
+
+Invertibility of P_x forces both S and D_x to be invertible. Hence alpha is
+nonzero, because v^T is nonzero and v^T D_x cannot vanish. Put
+w^T = v^T S^-1 and lambda = beta/alpha. Then w^T is nonzero and
+
+```text
+w^T A G^-1 = w^T P_y
+            = v^T D_y
+            = lambda v^T D_x
+            = lambda w^T P_x
+            = lambda w^T G^-1.
+```
+
+Cancel G^-1 on the right. We obtain w^T A = lambda w^T, a left eigenvector
+over K. Its absence excludes the alleged word, irrespective of its length.
+
+For the displayed binary A, a left eigenvalue would be 0 or 1. Multiplying
+A^3+A+I=0 by its nonzero left eigenvector would give
+(lambda^3+lambda+1)w^T=w^T=0. This contradiction proves the explicit instance.
+
+## Finite corroboration and controls
+
+The standard-library verifier executes the following bounded checks. They
+corroborate the proof; they are not an enumeration of arbitrary-length words.
+
+- All 28 singular rank-two scalar factors on three binary roles and all
+  seven nonzero compatible scalar prefixes per factor give 196 pairs.
+  For each pair, the verifier checks all 512 preceding single-coefficient
+  matrices and all eight radical columns. The common-row identity holds in
+  all **802,816** cases. Exactly **150,528** have an invertible new coefficient;
+  each has a nonzero common-row multiplier. The identity is checked for one
+  arbitrary coefficient at a time, so it applies separately to x and y.
+- Every one of the 512 possible A is tested against all seven nonzero binary
+  rows and both scalar eigenvalues. There are **48** eigenvalue-free matrices.
+  All 168 free conjugations of the displayed companion remain eigenvalue-free
+  and give **24** distinct conjugates.
+- Three literal reachable controls are each executed on all 512 dirty ring
+  vectors, giving **1,536** chronological action comparisons. They are a rootful
+  upper-triangular pencil, the single-coefficient target yA, and the collapsed
+  target x(I+A) obtained if y is identified with x. The latter two show why an
+  invertible first coefficient and independent radical variables matter.
+- Two exact chronology controls reject reversing the first-zero product and
+  omitting its radical contribution. The second error would miss a full-rank
+  coefficient produced at a singular scalar step.
+
+Every run prints a generated receipt bound to the SHA256 of all five package
+files. No receipt is stored or hand-written. All checks use explicit exceptions
+and remain active under `-O`.
+
+## Reproduction
+
+From the repository root, with CPython 3.12 and no third-party dependencies:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B -W error research/multirole-radical-pencil/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -O -B -W error research/multirole-radical-pencil/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/multirole-radical-pencil
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/multirole-radical-pencil --check-source-history
+```
+
+Any CPython 3.12 installation can replace the local interpreter path. Each
+registered command has a 120-second timeout and takes less than one second
+locally. Expected final marker:
+
+```text
+PASS_MULTIROLE_RADICAL_PENCIL transitions=802816 full_rank=150528 excluded_pencils=48 no_new_kappa
+```
+
+## Limits and implementation bounds
+
+This is a necessary condition only. A scalar eigenvalue is not proved
+sufficient. The ring has two independent radical generators with all their
+products zero. Right vectors and free maps must be over K. Arbitrary
+ring-valued free maps, higher radical nilpotency, and restored auxiliary roles
+are outside scope. No native supplier, recursive cost, precision, stock or
+complete multiplication theorem is supplied. Independent human and formal
+proof-kernel review are unclaimed. No Lean, Docker or selected operator replay
+was run.
+
+The code has no recursion, accepts no variable search sizes, and bounds every
+loop by the displayed finite domains. Its largest table has 4,096 integers;
+the receipt reads at most 128 KiB from each of five fixed paths. Python's
+managed allocations depart from fixed steady-state allocation. Their domains
+and lifetimes are bounded here. No shared code or interpreter configuration
+changes are needed.
+
+## Open next questions
+
+1. Is a base-field eigenvalue sufficient when n>=3? Start with the direct sum
+   of a scalar block and the binary companion of t^2+t+1. The proof gives one
+   common row but no recursive criterion on its quotient.
+2. Can an extra role restored to the identity make the displayed pencil
+   reachable? Start with diag(xI_3+yA,I_1). Its nonzero scalar endpoint is the
+   precise reason the present first-zero proof does not apply.
+
+The structured questions, relevance, first steps and blockers are also in
+[TASK.json](TASK.json). These follow-ups are not investigated here.
+
+## Source and overlap scope
+
+The originating card and selected record are pinned at
+`b58ad9ef4d4e861b0eaa5dba41742bdc072dca51`. The clean branch was created from
+the refreshed canonical main `1f87c3578ae546c8f903f7f4d83dc2e2fb99650b`; the
+guidance and selected record are unchanged between those commits. Open
+predecessor #4745 is a credited conceptual source, not an imported executable
+or a required unmerged Git object. The theorem and verifier are self-contained.
+
+Before claiming, live open PRs, this account's recent PRs, the latest handoffs,
+active Discussions, local reservations, and distinctive merged/main
+searches were checked. The overlap helper's cached remote pagination was
+complete at approximately 19:22 UTC; its sparse local-note coverage was
+incomplete and cannot certify novelty. The related two-role all-field count,
+cube-zero example, rank-one-residue census and polynomial-ring cost claims
+study different questions. The main two-role predecessor's twelve unreachable
+radical targets are not rechecked or recounted here.
+
+Claim: [handoff post](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19131197).

research/multirole-radical-pencil/SOURCES.json

@@ -0,0 +1,18 @@
+{
+  "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"
+    }
+  ]
+}

research/multirole-radical-pencil/TASK.json

@@ -0,0 +1,68 @@
+{
+  "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": "For any field K and any role count, prove that xI+yA over K[x,y]/(x,y)^2 is unreachable at every finite paid length when A has no K-valued left eigenvector. Give the binary three-role cubic companion and exact finite corroboration.",
+  "scope_change_reason": "The card asks for a changed connector operation with a completed budget. This contribution instead extends the two-role square-zero question of PR4745 to a necessary condition at arbitrary role count in the same formal right-vector alphabet. It is a scoped algebraic side result, not a priced interface.",
+  "bottleneck_link": "A general-target rank estimate does not imply reachability in the base-field right-vector alphabet. The obstruction rejects a whole family before searching paid words; physical supplier costs are not inferred.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop at the first proved multi-role obstruction and its bounded reproducer; leave sufficiency and restored auxiliary roles open.",
+  "outcome": "negative-result",
+  "evidence": "Written arbitrary-field and arbitrary-word-length proof; 802816 binary single-coefficient first-zero transition checks, including 150528 invertible cases; direct enumeration excludes 48 of 512 binary three-role pencils; 1536 chronological dirty-input comparisons and two chronology controls.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Is a base-field eigenvalue sufficient for reachability of xI+yA when n>=3, or do nonsplit invariant factors still obstruct it?",
+      "why_it_matters": "The present theorem is a necessary condition only; a complete criterion could avoid unbounded word searches.",
+      "first_step": "Test the three-role direct sum of one scalar block and the companion of t^2+t+1 over F2.",
+      "blocked_by": "The first-zero step supplies one common row but does not recursively control its quotient."
+    },
+    {
+      "question": "Can extra roles restored to the identity make an excluded radical pencil reachable?",
+      "why_it_matters": "Physical dirty auxiliary roles change the scalar endpoint from zero to a nonzero projector.",
+      "first_step": "Study diag(xI3+yA,I1) for the displayed cubic companion with the same restricted right vectors.",
+      "blocked_by": "The proof uses a zero full scalar endpoint and does not apply to this padding."
+    }
+  ]
+}

research/multirole-radical-pencil/VERIFY.json

@@ -0,0 +1,32 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "-W",
+        "error",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "All 802816 binary first-zero coefficient transitions, 48 excluded pencils, free conjugacy, literal dirty-input controls and chronology rejection controls."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-O",
+        "-B",
+        "-W",
+        "error",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Repeat the complete finite corroboration with Python assertions disabled; all mathematical guards use explicit exceptions."
+    }
+  ]
+}