Classify exact rank-two matrix-algebra right-vector costs (no new κ)

research/right-vector-rank-two/PROOF.md

@@ -0,0 +1,130 @@
+# Exact rank-two classification on two roles
+
+Let K be a field, m>=3 and R=M_m(K). Paid factors are
+P(u,y)=I_2+u y^T, with u in R^2 and y in K^2. Free maps are
+GL_2(K), acting as S tensor I_m, anywhere in a word. Rank below means
+ordinary rank over K. Let M have rank two, and choose a rank factorization
+
+    M = A B,   A = [A_1; A_2],   B = [B_1 B_2],
+
+where A is 2m by 2 and injective, B is 2 by 2m and surjective,
+A_i is m by 2 and B_j is 2 by m.
+
+**Theorem.** The exact cost is three if and only if both conditions hold:
+
+1. B_1=c_1 b and B_2=c_2 b for one nonzero row b in K^(1 by m)
+   and a basis c_1,c_2 of K^2.
+2. For every nonzero (s,t) in K^2, the matrix s A_1+t A_2 has rank two.
+
+Every other rank-two target has exact cost two. In particular, all these
+targets are reachable. The conditions are independent of the chosen rank
+factorization.
+
+This answers the rank-two, two-role part of Open next question 1 of Nick
+Petalas's #4772. The two-factor criterion is Corollary C of Nick Petalas's
+#4276 and retains its credit. Rank factorization and the elementary
+rank-one pencil argument below are classical linear algebra. The new claim
+is their exact-cost classification in this alphabet and the attaining words.
+
+## Lower bound and predecessor criterion
+
+A paid factor fixes (ker y^T) tensor K^m, so its rank is at least m.
+Free maps preserve rank. Since rank M=2<m, zero or one paid factors cannot
+attain M. This is the rank-loss bound used in #4772.
+
+By #4276, two factors suffice exactly when some nonzero row phi and column
+v over K give
+
+    rank ((phi tensor I_m) M)
+      = rank ((phi tensor I_m) M (v tensor I_m)).             (1)
+
+Set A_phi=phi_1 A_1+phi_2 A_2 and B_v=v_1 B_1+v_2 B_2.
+Since B is surjective, (1) becomes
+
+    rank A_phi = rank (A_phi B_v).                           (2)
+
+If any B_v has rank two, it is surjective onto K^2, and (2) holds for
+every phi. Such a target has cost two.
+
+## The only deficient B pencil
+
+Suppose every B_v has rank at most one. Neither B_1 nor B_2 can be zero,
+since B is surjective. Write B_i=c_i b_i with nonzero factors. The columns
+c_1,c_2 are independent, again because B is surjective. If b_1,b_2 were
+independent, B_1+B_2 would have rank two: the map with rows b_1,b_2 is
+surjective, followed by the isomorphism with columns c_1,c_2. Thus b_2 is
+a nonzero multiple of b_1. Absorb that multiple into c_2 to obtain
+condition 1. Conversely, condition 1 makes every nonzero B_v rank one.
+This argument uses only v=e_1,e_2,e_1+e_2 and works over F_2 as well.
+
+Now suppose condition 1 holds. If A_phi has rank zero, (2) holds. If it
+has rank one, write A_phi=a ell with ell a nonzero row on K^2. Choose v
+so ell(v_1 c_1+v_2 c_2) is nonzero. This is possible because c_1,c_2 are
+a basis. Then A_phi B_v has rank one, so (2) again holds.
+
+If condition 2 also holds, A_phi is injective for every nonzero phi,
+while every B_v has rank one. The two sides of (2) are then two and one
+for every pair. No two-factor word exists, including arbitrary free maps.
+This proves exactly which targets cost at least three.
+
+A different rank factorization has the form A H, H^(-1) B for H in
+GL_2(K). Right multiplication by H preserves each rank in condition 2;
+left multiplication by H^(-1) preserves the common-row property and the
+independence of c_1,c_2 in condition 1. This proves independence of the
+rank factorization.
+
+## Attaining the exceptional class with three factors
+
+For an exceptional target, put a=A_1 c_1 and d=A_2 c_1. Condition 2 gives
+a!=0. Choose L in M_m(K) with L a=d, for example
+
+    L = d e_h^T / a_h,   where a_h!=0.
+
+Since M_11=a b and M_21=d b, we have L M_11=M_21. Set
+D=M_22-L M_12. Then the literal product is
+
+    [[I,0],[L,I]] [[I,M_12],[0,D]] [[M_11,0],[0,I]]
+      = [[M_11,M_12],[M_21,M_22]] = M.                       (3)
+
+Each displayed matrix differs from the identity in one block column,
+so each is a legal paid factor. Their right vectors in algebraic product
+order are e_1,e_2,e_1. Chronological execution on column data is from
+right to left. There are no auxiliary roles or free internal-coordinate
+changes. Together with the lower bound, (3) proves exact cost three.
+
+For a nonexceptional target, #4276 gives an attaining two-factor word:
+choose free G,H taking a passing phi,v to the first output row and input
+column. For N=G M H solve N_11 C=N_12, then use
+
+    N = [[N_11,0],[N_21,I]] [[I,C],[0,N_22-N_21 C]].          (4)
+
+Undo G,H at the free endpoints. The existence of C is precisely the
+column-space equality in (1). This attaining formula is predecessor
+credit, not a new two-factor theorem.
+
+## One explicit exception over every field
+
+For m>=3, take
+
+    A_1=[e_1 e_2], A_2=[e_2 e_3],
+    c_1=(1,0)^T, c_2=(0,1)^T, b=e_1^T.
+
+The columns of s A_1+t A_2 are s e_1+t e_2 and s e_2+t e_3.
+If s!=0, their first two rows have determinant s^2; if s=0, their
+last two displayed rows have determinant t^2. Thus condition 2 holds
+over every field. In matrix-unit notation the target is
+
+    M = [[E_11,E_21],[E_21,E_31]],   cost(M)=3.
+
+Its ordinary rank is two. Formula (3) specializes to L=E_21 and
+D=E_31, since E_21^2=0. Hence the three factors are explicit over every
+field and every permitted block size.
+
+## Scope
+
+The assertion concerns formal overwriting factors on two roles and m>=3.
+At m=2 a rank-two target can cost one, for example diag(0,I_2), so that
+boundary is excluded. Other ordinary ranks and more than two roles are
+unclassified here. Coefficient preparation, reversible restoration, routing,
+precision, stock and a complete supplier invoice are not supplied.
+No new kappa or complete multiplication theorem follows.

research/right-vector-rank-two/README.md

@@ -0,0 +1,137 @@
+# Exact rank-two right-vector costs on two roles
+
+Claim type: scoped proof with an exhaustive finite certificate. No new kappa.
+
+For every field K and block size m>=3, every ordinary rank-two target over
+M_m(K), on two roles, has exact paid cost two or three. The alphabet is
+I+u y^T with u over M_m(K) and y over K; arbitrary common GL_2(K) maps
+are free anywhere. There are no auxiliary roles.
+
+Choose a rank factorization M=A B, with A=[A_1; A_2] injective and
+B=[B_1 B_2] surjective through K^2. The exact classification is
+
+```text
+cost(M)=3 iff
+  B_1=c_1 b and B_2=c_2 b for a common nonzero row b and a basis c_1,c_2;
+  every nonzero scalar combination s A_1+t A_2 has rank two.
+Otherwise cost(M)=2.
+```
+
+[PROOF.md](PROOF.md) proves both directions and gives attaining words.
+The criterion is independent of the chosen rank factorization. This answers
+the rank-two, two-role part of Open next question 1 of
+[Nick Petalas's #4772](https://github.com/CrocSwap/integer-mult-bounds/pull/4772).
+It uses the two-factor criterion of
+[#4276](https://github.com/CrocSwap/integer-mult-bounds/pull/4276) as a cited
+theorem. It does not re-audit that predecessor.
+
+In particular, over every field and every m>=3,
+
+```text
+M = [[E_11,E_21],[E_21,E_31]]
+  = [[I,0],[E_21,I]] [[I,E_21],[0,E_31]] [[E_11,0],[0,I]]
+cost(M)=3, ordinary rank(M)=2.
+```
+
+Here E_ij denotes an m by m matrix unit. Each factor changes one block
+column, with right vectors e_1,e_2,e_1 in algebraic product order.
+Column-data execution applies the rightmost factor first.
+
+## Finite evidence
+
+The independent standard-library verifier enumerates all 2,542,806 ordinary
+rank-two binary 6 by 6 targets, with blocks of size three. Exactly
+2,535,162 cost two and 7,644 cost three.
+
+Coverage uses all 651 two-dimensional column spaces, each represented by
+its two least nonzero vectors, and all 3,906 surjections from K^6 to K^2.
+Each target occurs exactly once: its column space determines the chosen
+A, and the injectivity of A determines B uniquely. The verifier builds
+every complete target, applies the cited two-factor criterion directly to
+its full blocks, and separately evaluates the new rank-factor classification.
+All records agree. It hashes the entire ordered target/cost table, whose
+SHA256 is `37a68b33c4175157da0147c0b165f82909956a87750ff354a366f542f432c623`.
+The 182 exceptional column spaces pair with 42 common-row surjections.
+Every one of the 7,644 cost-three targets has its literal legal attaining
+word multiplied and compared with the complete target.
+
+A separate dense linear solver constructs the two-factor words in the
+three passing rank-factor categories and rejects the fourth category.
+The explicit exceptional target and its legal word pass over F_2, F_3,
+F_4, F_5 and F_7 at m=3 and m=4. All 64 binary dirty inputs of the
+displayed m=3 word pass chronological execution. The replay checks seven
+additional boundary/solver/alphabet controls, plus omission and reversal
+controls in each of the ten field/block cases. All checks remain active
+under optimized Python.
+
+The printed receipt is generated from executed checks. It binds all six
+package files and both live predecessor proof files by SHA256; no receipt
+is handwritten. The verifier writes no files.
+
+## Reproduce
+
+From the repository root, with the Python 3.12 standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B -W error research/right-vector-rank-two/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -O -B -W error research/right-vector-rank-two/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/right-vector-rank-two
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/right-vector-rank-two --check-source-history
+```
+
+Any CPython 3.12 installation can replace the local interpreter path.
+The scientific marker is
+`PASS_RIGHT_VECTOR_RANK_TWO targets=2542806 cost2=2535162 cost3=7644`.
+Both registered warning-strict commands replay every check, with separate
+120-second limits. Exact sources are in [SOURCES.json](SOURCES.json).
+
+## Limitations and engineering notes
+
+The universal statement is a written scoped proof, with finite corroboration.
+The exhaustive target census covers only F_2 and m=3. Other finite fields
+have the stated explicit examples, rather than full target censuses.
+The block-size condition matters: at m=2 the ordinary rank-two target
+diag(0,I_2) costs one. More roles and other ordinary ranks are unclassified.
+
+These factors overwrite data. Native coefficient preparation, routing,
+reversible dirty-state restoration, precision, stock and the complete
+recursive invoice are unknown. No native supplier, selected-frontier change
+or complete multiplication theorem is claimed. Independent human and formal
+proof-kernel review are unclaimed. Lean, Docker and the selected construction
+replay are outside this isolated result and were not run.
+
+The verifier has no recursion or dynamic evaluation; all functions are below
+60 lines. Its loops use fixed finite domains, at most 2,542,806 target visits,
+nine binary chart pairs per target and 64 dense chart pairs in the largest
+field example. Matrices have at most eight rows and columns. The two rank
+tables have 262,144 and 512 bytes; the census retains only 651 bases, 3,906
+surjections, four sample targets and one streaming digest. Python's required
+dynamic allocation is the managed-runtime deviation from static allocation;
+these fixed domains bound live memory. File reads are limited to one MiB and
+the source manifest to eight entries. The direct and optimized warning-strict
+replays and in-memory compilation are the interpreted-language diagnostics.
+No separate Python linter is installed in the supplied environment.
+
+## Open next questions
+
+1. Which ordinary rank-three targets on two roles over M_m(K), m>=4,
+   cost two or three, and can any cost more? Start with the rank-three
+   factorization and a named deficient 3 by m matrix pencil. The rank-one
+   pencil lemma used here no longer classifies that pencil.
+2. Can a literal native producer/consumer realize one of these formal
+   factors with a useful complete invoice? First specify coefficient
+   preparation, overwrite ownership and restoration. All physical costs
+   above remain blockers; no construction expansion is proposed here.
+
+## Credit
+
+This contribution was produced by Nick Petalas. Nick Petalas's #4772
+supplies the open higher-rank question and rank-loss bound; #4276 supplies
+the two-factor criterion and its attaining formula; #4265 and #4243 supply
+the general-target question and free-map normal form. Wentao Li's #4099,
+following #2513, supplies the right-vector alphabet and column bound.
+ToikY's #4334 supplies the related field-product cost framework, followed by
+Nick Petalas's #4601/#4749 local-product and semilocal results. Rank
+factorization and the rank-one pencil lemma are classical linear algebra.
+The new claims are the stated rank-two classification and exceptional
+attaining words. Apache-2.0.

research/right-vector-rank-two/SOURCES.json

@@ -0,0 +1,30 @@
+{
+  "schema_version": 1,
+  "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43",
+  "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-rank-one/PROOF.md",
+      "usage": "input",
+      "git_blob": "6ac032094c95bfb4edd8b9b748eceba4e84046fb",
+      "sha256": "c232b8b01a9481bf75267c48ac06165fab64565ac15207c40a99cbcad35e0757"
+    },
+    {
+      "path": "research/right-vector-two-factor-criterion/PROOF.md",
+      "usage": "input",
+      "git_blob": "71888afa0db63d6d332cbbdc408abf1aa879681c",
+      "sha256": "c1065c51c839d11b0d31bccb8d39ebc07a869eb0f29899038518e3090a58c895"
+    }
+  ]
+}

research/right-vector-rank-two/TASK.json

@@ -0,0 +1,68 @@
+{
+  "schema_version": 1,
+  "task_id": "connector-alphabet-change",
+  "priority_revision": 7,
+  "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43",
+  "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": "Classify exact costs two versus three for every ordinary rank-two target on two roles over M_m(K), m>=3, over every field.",
+  "scope_change_reason": "This takes the explicit rank-two case of Open next question 1 of PR4772 as a formal-alphabet side result. It does not extend the connector alphabet or price a native supplier.",
+  "bottleneck_link": "A complete singular-target exact-cost classification in the relaxed algebra-valued alphabet. Rank two can require an extra paid call; the result supplies no native preparation or recursive invoice.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop at the first proved rank-two classification with a bounded exact replay; leave rank three, more roles and physical implementation open.",
+  "outcome": "completed",
+  "evidence": "PROOF.md proves the all-field classification and attaining words. verify.py enumerates all 2542806 binary m=3 rank-two targets, checks the full-matrix criterion against the new classification, executes all 7644 exceptional words, and checks ten explicit finite-field/block cases and controls.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Which ordinary rank-three two-role targets over M_m(K), m>=4, cost two or three, and can any cost more?",
+      "why_it_matters": "This locates the next singular-rank boundary of the exact-cost problem.",
+      "first_step": "Take a named deficient 3 by m block pencil in a rank-three factorization and apply the cited two-factor criterion.",
+      "blocked_by": "The rank-one pencil lemma here does not classify rank-two deficient pencils."
+    },
+    {
+      "question": "Can one literal native producer and consumer implement these formal factors at a useful complete cost?",
+      "why_it_matters": "Formal factor cost does not price a recursive supplier.",
+      "first_step": "Specify one coefficient preparation, overwrite ownership, routing and restoration contract before any construction expansion.",
+      "blocked_by": "Native preparation, restoration, precision, stock and complete invoice costs remain unknown."
+    }
+  ]
+}