Prove exact radical reachability through a common flag (no κ)

research/radical-common-flag/PROOF.md

@@ -0,0 +1,161 @@
+# Exact reachability through a common invariant flag
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+## Contract and theorem
+
+Let K be any field, n>=1, s>=0, and
+
+```text
+R = K[t_0,...,t_s]/(t_i t_j : 0<=i,j<=s).
+```
+
+There are exactly n roles. A paid factor is `I+uv^T`, where u is in R^n
+and v is in K^n. Singular paid factors are allowed. Arbitrary GL_n(K)
+maps are free and may occur anywhere in a finite word. Products specify
+the complete action on arbitrary elements of R^n. There are no additional
+roles, input promises or ring-valued free maps.
+
+For matrices C_0,...,C_s over K, with C_0 invertible, put
+
+```text
+M = sum_(j=0)^s t_j C_j,
+A_j = C_0^-1 C_j,  1<=j<=s.
+```
+
+**Theorem.** M is reachable exactly when the A_j have a common complete
+invariant flag over K. Equivalently, they are simultaneously upper
+triangularizable over K. When reachable, its exact paid cost is n.
+Otherwise no finite word reaches M.
+
+For s=0 the flag condition is vacuous. A complete flag is
+`0=V_0<V_1<...<V_n=K^n` with dim V_k=k. Invariance means each A_j maps
+each V_k into itself. Choosing an adapted basis proves the equivalence
+with simultaneous triangularization. Commutation is not required.
+
+This settles Open next question 1 of Nick Petalas's PR5854, source head
+`e70246e3aabe63aacbddb41dfa2253e865798d1d`. Its first-zero argument gives
+one common eigenrow. The new step uses every chronological cut and gives
+the entire flag. PR4776 already classifies two-generator pencils by
+characteristic-polynomial splitting. Neither predecessor is replayed here.
+
+## The cut lemma
+
+Split an alleged word at any chronological cut as M=QP, with P the
+executed prefix and Q the remaining suffix. Include all free maps. Write
+their unique square-zero expansions as
+
+```text
+P = H + sum_j t_j D_j,
+Q = S + sum_j t_j E_j.
+```
+
+Comparing constant and linear coefficients gives
+
+```text
+SH=0,
+C_j = S D_j + E_j H,  0<=j<=s.                 (1)
+```
+
+Let V=ker H and k=dim V. Equation (1) gives `C_0 V` contained in im S.
+Invertibility of C_0 makes this image k-dimensional. Also SH=0 gives
+`im H` contained in ker S, so `rank S<=n-rank H=k`. Therefore
+
+```text
+rank S=k,
+C_0 V=im S.                                   (2)
+```
+
+Every C_j maps V into im S by (1). Equation (2) implies
+`C_0^-1 C_j V` is contained in V. Each scalar-prefix kernel is consequently
+a common invariant subspace of all normalized coefficients.
+
+This lemma imposes no further restrictions on D_j or E_j. It covers
+arbitrary feedback, free maps, extra paid factors and singular intermediate
+matrices. It divides by no singular prefix or suffix and requires no
+quotient word in the paid alphabet.
+
+## Every kernel dimension occurs
+
+The scalar prefix starts at I and ends at zero. A free map leaves its
+kernel unchanged. A paid factor changes H to `(I+av^T)H`, where a is the
+constant coefficient of u. Its kernel can only grow. Rank drops by at
+most one, since `rank(I+av^T)>=n-1` and
+`rank((I+av^T)H)>=rank H-1`.
+
+The nested scalar-prefix kernels thus include every dimension 0 through n.
+Choose one cut per dimension. The cut lemma gives a common complete
+invariant flag, proving necessity. The same rank-drop bound forces at
+least n paid factors in every realizing word.
+
+## An attaining word
+
+Given a common flag, choose G in GL_n(K) with
+`T_j=G^-1 A_j G` upper triangular for every j. Set T_0=I and
+
+```text
+U=sum_j t_j T_j,
+c_i=column i of U,
+F_i=I+(c_i-e_i)e_i^T,  1<=i<=n.
+```
+
+Every F_i is legal. Execute F_1 through F_n in that order. The only changed
+columns of `P_(i-1)=F_(i-1)...F_1` have indices below i and support in
+rows of indices below i. Thus `e_i^T P_(i-1)=e_i^T`, and
+
+```text
+F_i P_(i-1)=P_(i-1)+(c_i-e_i)e_i^T.
+```
+
+Precisely column i changes from e_i to c_i. Induction gives
+`F_n...F_1=U`. The complete word is
+
+```text
+M=(C_0 G) F_n...F_1 G^-1.
+```
+
+The outer maps are free. Exactly n paid factors attain the lower bound.
+This is a matrix identity on every input over R, including arbitrary
+initial radical coefficients. The alphabet permits singular operations;
+no reversible physical implementation is asserted.
+
+## A strict separation from the common-row test
+
+Over every field, define
+
+```text
+J=[[0,1,0],[0,0,1],[0,0,0]],
+B=[[0,0,0],[1,0,0],[0,-1,0]],
+A'=diag(0,J),  B'=diag(0,B).
+```
+
+The four-role target `t_0 I_4+t_1 A'+t_2 B'` has homogeneous determinant
+X^4, a common left eigenrow and a common right eigenline. Nevertheless
+it is unreachable. Both coefficients are nilpotent, so any common
+eigenline lies in their common kernel. That kernel is exactly the first
+coordinate line. In the quotient by it, the coefficients are J and B,
+whose kernels are the first and third coordinate lines. They have no
+common eigenline, so the forced first line cannot extend to a complete
+common flag. The theorem excludes every finite word.
+
+The determinant follows from `det(XI_3+YJ+ZB)=X^3`, the credited PR5854
+example. The new four-role consequence shows that supplying a common
+eigenrow still does not suffice. The verifier checks its forced line
+and quotient over F3. The written argument covers every field.
+
+## Boundaries and credit
+
+The statement requires an invertible distinguished coefficient and
+normalization by its left inverse. Targets without such a coefficient,
+nonzero scalar endpoints, higher nilpotency, restored additional roles
+and broader alphabets remain outside scope. No native realization,
+physical coefficient preparation, restoration bill, precision, stock,
+complete recursive invoice, supplier admission or new kappa follows.
+All five selected framework assumptions remain separate. Independent
+human and formal proof-kernel review are unclaimed.
+
+Rank-nullity, rank-one perturbation bounds and adapted bases are classical.
+The new contribution is their chronological-cut application proving the
+multi-coefficient criterion and exact cost. Retain the alphabet and
+normal-form credit to Nick Petalas / PR4243, PR4773 and PR4776; Wentao Li /
+PR4099 following PR2513; and ToikY / PR4334.

research/radical-common-flag/README.md

@@ -0,0 +1,148 @@
+# Exact radical reachability through a common flag
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+For every field K, n>=1 and finite coefficient tuple, a pure square-zero
+target with an invertible coefficient has a complete reachability criterion:
+
+```text
+R=K[t_0,...,t_s]/(all t_i*t_j), C_0 invertible,
+M=sum_j t_j*C_j,
+paid factors I+u*v^T, u in R^n, v in K^n; free GL_n(K) maps.
+
+M is reachable exactly when C_0^-1*C_1,...,C_0^-1*C_s
+have a common complete invariant flag over K.
+When reachable, the exact paid cost is n.
+```
+
+Claim type: scoped written algebraic proof with exact finite corroboration.
+The theorem concerns exactly n roles and the stated formal alphabet.
+No new kappa or supplier admission is claimed.
+
+[PROOF.md](PROOF.md) answers Open next question 1 of
+[PR5854](https://github.com/CrocSwap/integer-mult-bounds/pull/5854).
+The new argument identifies a common invariant subspace at every scalar
+rank drop, giving the full flag. A column-replacement word attains the
+lower bound. The earlier common-eigenrow obstruction and PR4776's
+two-generator classification are credited results, not audit targets.
+A four-role example passes the split-determinant and common-eigenrow
+tests but fails the new complete criterion over every field.
+
+## Exact evidence
+
+The standalone verifier imports no predecessor code. Two separately
+constructed finite descriptions, projective lines and planes versus every
+invertible change of basis, agree on all ordered coefficient pairs in:
+
+- M_2(F2)^2, all 256 pairs, with 148 reachable;
+- M_2(F3)^2, all 6,561 pairs, with 2,457 reachable;
+- M_3(F2)^2, all 262,144 pairs, with 47,968 reachable.
+
+These counts concern targets `t_0 I+t_1 A+t_2 B`. They are new finite
+corroboration of the criterion, not a classification of all radical matrices.
+The checker also records the complete common-flag multiplicity histogram.
+
+Exact square-zero matrix multiplication checks 5,062 attaining words.
+They include every pair of upper-triangular coefficients in the three
+domains, all 168 binary three-role basis changes of one noncommuting
+tuple with a nonidentity distinguished coefficient, one- and four-role
+boundaries, odd characteristics and the vacuous coefficient tuple.
+A separate literal coefficient interpreter checks 2,272 arbitrary-input
+basis columns. At 1,150 chronological cuts, the rank, image, coefficient
+and invariance identities hold. The abstract cut check covers all 58
+binary two-by-two scalar pairs with SH=0 and all 1,584 indexed (H,S,X,Y)
+cases with X invertible. It enumerates each cut's coefficient
+image from every D/E choice before deduplication.
+
+Twelve controls cover six invalid constructor contracts, three omitted
+paid factors, reversed chronology, a singular distinguished coefficient
+and a counterexample when SH=0 is omitted. The four-role strict
+obstruction is checked separately over F3. The universal claim rests on
+the written proof, not extrapolation from these finite domains.
+
+## Reproduce
+
+From the repository root, with CPython 3.12 and its standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -X dev -B research/radical-common-flag/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -X dev -B research/radical-common-flag/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/radical-common-flag
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/radical-common-flag --check-source-history
+```
+
+Any CPython 3.12 path can replace the host-specific interpreter. The direct
+marker is `PASS_RADICAL_COMMON_FLAG`. Each run generates a stdout JSON
+receipt bound to all six package files by SHA256. No receipt is handwritten
+or stored in the package. Both registered modes run the same checks and
+write nothing to the checkout. Each command has a 120-second limit.
+
+[SOURCES.json](SOURCES.json) pins the task catalogue, selected record and
+two predecessor texts as historical provenance. None is an executable or
+runtime input. The direct verifier works in a Git-free package export;
+the repository metadata and source-history checks require Git history.
+
+## Scope and verification limits
+
+The formal-interface-lemma card is explicitly changed to this algebraic
+side question in [TASK.json](TASK.json). Base is canonical main
+`7c49fe32c55de02c2c873655c804b16e4c3fef0a`, priority revision 8, selected
+PR6030. The source-binding orientation passed; it authenticates metadata,
+not a mathematical or native supplier claim. The
+[advance CLAIM](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19375372)
+followed live overlap and reservation checks. Cached overlap covered 572
+open PRs and 6,639 Discussion records with complete remote pagination.
+Sparse local notes omitted most main-tree packages, so targeted Git-tree
+and merged/general-form searches supplement that incomplete coverage.
+Unpublished work and arbitrary historical diffs remain outside coverage.
+
+Without an invertible coefficient, with a nonzero scalar endpoint, with
+higher nilpotency or with restored extra roles, a new argument is needed.
+The paid factors may be singular. Native realization, physical coefficient
+preparation, reversible restoration, precision, stock, tape, complete paid
+invoice, compiler and outer admission remain separate. No selected-frontier
+change or complete multiplication theorem follows. All five framework
+assumptions remain. Selected cold replay, Lean, Docker, independent human
+and formal proof-kernel review are unrun or unclaimed.
+
+The verifier has no recursion, subprocesses, network, dynamic evaluation or
+write path. Matrices have at most four rows and coefficients are in F2,
+F3 or F5. Complete pair domains stop at 512^2. Invertible basis inventories
+stop at 168 matrices. The largest cut-vector domain has 625 vectors. All functions are
+below 60 physical lines and all gates use explicit exceptions under -O.
+Six file reads are capped at 128 KiB each. Warning-strict normal and
+optimized execution and syntax/AST inspection provide diagnostics.
+
+Power of Ten rule 3 has a managed-runtime deviation in verify.py. Python
+allocates integers, tuples and sets during execution; the fixed domains
+above bound live collections, including at most 512 matrix masks of
+168 bits and one active finite pair scan. No fixed-memory runtime or
+allocator-overhead bound is claimed. A larger input domain requires new
+capacity limits before changing this verifier. No shared build setting or
+historical implementation is changed.
+
+## Open next questions
+
+- Can a restored extra role enable an excluded target? Start with diag(M,1)
+  for the four-role example and preserve every dirty-input column. The
+  scalar endpoint is then nonzero and the distinguished coefficient is
+  singular on the larger space, so the present cut equality does not apply.
+- Which zero-residue targets without an invertible coefficient are reachable?
+  Start with one explicit singular tuple and its source/image flags. Excess
+  dimension in the cut image prevents the current invariant-flag conclusion.
+
+Structured first steps and blockers are in TASK.json. No further extension
+is included in this contribution.
+
+## Credit
+
+Nick Petalas / PR5854 supplied the explicit question and common-eigenrow
+obstruction; PR4773 supplied the first-zero argument; PR4776 supplied the
+two-generator split-pencil classification; and PR4243 supplied the free-map
+normal form. Retain Wentao Li / PR4099 following PR2513 and ToikY / PR4334
+for the paid alphabet and shared-chart context. Rank-nullity, rank-one
+perturbations and adapted bases are classical. The new contribution is the
+all-cut flag criterion, exact attaining cost and finite corroboration.
+Predecessor bytes and credit remain unchanged. No general literature
+priority is claimed. Independent human and formal proof-kernel review
+are unclaimed.

research/radical-common-flag/SOURCES.json

@@ -0,0 +1,30 @@
+{
+  "schema_version": 1,
+  "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a",
+      "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "research/split-determinant-radical-obstruction/README.md",
+      "usage": "provenance",
+      "git_blob": "89dd725b862d65d68cf2093c2c716ef492987db3",
+      "sha256": "4eb4b8963726608045b824819e6af0cd8f65dcac8756ab3ecb6d68716e0e035c"
+    },
+    {
+      "path": "research/split-radical-pencil/README.md",
+      "usage": "provenance",
+      "git_blob": "c75b9d49627a47c6924ab64b7f4fb065cda7fa4b",
+      "sha256": "b419063a6de89a36b8ba552e580f73b0af2bbb2104c947db9f4a69f7728a79f2"
+    }
+  ]
+}