From 7fdbf8040ea9a957af0576067df2d9cb6fcf0e51 Mon Sep 17 00:00:00 2001
From: Nick Petalas <webmasternikos@gmail.com>
Date: Thu, 22 Oct 2026 20:56:32 +0100
Subject: [PATCH] feat(research): classify rank-two right-vector costs

---
 research/right-vector-rank-two/PROOF.md     | 130 +++++++
 research/right-vector-rank-two/README.md    | 137 ++++++++
 research/right-vector-rank-two/SOURCES.json |  30 ++
 research/right-vector-rank-two/TASK.json    |  68 ++++
 research/right-vector-rank-two/VERIFY.json  |  35 ++
 research/right-vector-rank-two/verify.py    | 365 ++++++++++++++++++++
 6 files changed, 765 insertions(+)
 create mode 100644 research/right-vector-rank-two/PROOF.md
 create mode 100644 research/right-vector-rank-two/README.md
 create mode 100644 research/right-vector-rank-two/SOURCES.json
 create mode 100644 research/right-vector-rank-two/TASK.json
 create mode 100644 research/right-vector-rank-two/VERIFY.json
 create mode 100644 research/right-vector-rank-two/verify.py

diff --git a/research/right-vector-rank-two/PROOF.md b/research/right-vector-rank-two/PROOF.md
new file mode 100644
index 0000000000..c936663ac7
--- /dev/null
+++ b/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.
diff --git a/research/right-vector-rank-two/README.md b/research/right-vector-rank-two/README.md
new file mode 100644
index 0000000000..8a8bee262c
--- /dev/null
+++ b/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.
diff --git a/research/right-vector-rank-two/SOURCES.json b/research/right-vector-rank-two/SOURCES.json
new file mode 100644
index 0000000000..86ac92ab4b
--- /dev/null
+++ b/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"
+    }
+  ]
+}
diff --git a/research/right-vector-rank-two/TASK.json b/research/right-vector-rank-two/TASK.json
new file mode 100644
index 0000000000..5d929e3e97
--- /dev/null
+++ b/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."
+    }
+  ]
+}
diff --git a/research/right-vector-rank-two/VERIFY.json b/research/right-vector-rank-two/VERIFY.json
new file mode 100644
index 0000000000..2ae687dcbe
--- /dev/null
+++ b/research/right-vector-rank-two/VERIFY.json
@@ -0,0 +1,35 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/right-vector-rank-one/PROOF.md",
+    "research/right-vector-two-factor-criterion/PROOF.md"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "-W",
+        "error",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Complete binary rank-two census of 2542806 targets, full-matrix criterion/classification agreement, all 7644 literal exceptional words, ten explicit finite-field/block examples, dense two-factor witnesses and boundary/chronology/solver controls. Generated receipt binds package and live predecessor files."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-O",
+        "-B",
+        "-W",
+        "error",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Complete binary rank-two census of 2542806 targets, full-matrix criterion/classification agreement, all 7644 literal exceptional words, ten explicit finite-field/block examples, dense two-factor witnesses and boundary/chronology/solver controls. Generated receipt binds package and live predecessor files."
+    }
+  ]
+}
diff --git a/research/right-vector-rank-two/verify.py b/research/right-vector-rank-two/verify.py
new file mode 100644
index 0000000000..9ad99b6555
--- /dev/null
+++ b/research/right-vector-rank-two/verify.py
@@ -0,0 +1,365 @@
+#!/usr/bin/env python3
+"""Exact bounded replay of the rank-two classification; standard library only."""
+
+from hashlib import sha256
+from itertools import product
+import json
+from pathlib import Path
+
+
+def require(condition, message):
+    if not condition:
+        raise RuntimeError(message)
+
+
+def binary_rank(rows, width):
+    pivots = [0] * width
+    rank = 0
+    for value in rows:
+        for bit in range(width - 1, -1, -1):
+            if not (value >> bit) & 1:
+                continue
+            if pivots[bit]:
+                value ^= pivots[bit]
+            else:
+                pivots[bit] = value
+                rank += 1
+                break
+    return rank
+
+
+def rank_table(width):
+    require(width in (3, 6), "rank table domain")
+    mask = (1 << width) - 1
+    return bytes(binary_rank((v & mask, (v >> width) & mask,
+                              v >> (2 * width)), width)
+                 for v in range(1 << (3 * width)))
+
+
+def binary_product(left, right, width):
+    result = []
+    for row in left:
+        value = 0
+        for j in range(width):
+            if (row >> j) & 1:
+                value ^= right[j]
+        result.append(value)
+    return tuple(result)
+
+
+def literal_two_factor_criterion(rows, rank6, rank3):
+    """Apply the cited criterion to full 6x6 targets, without rank factors."""
+    for phi in (1, 2, 3):
+        r = rows[:3] if phi == 1 else rows[3:]
+        if phi == 3:
+            r = tuple(rows[i] ^ rows[i + 3] for i in range(3))
+        whole_rank = rank6[r[0] | (r[1] << 6) | (r[2] << 12)]
+        for v in (1, 2, 3):
+            c = tuple((x & 7) if v == 1 else (x >> 3) if v == 2
+                      else ((x & 7) ^ (x >> 3)) for x in r)
+            if rank3[c[0] | (c[1] << 3) | (c[2] << 6)] == whole_rank:
+                return True
+    return False
+
+
+def full_a_pencil(a, b):
+    for phi in (1, 2, 3):
+        x = (a & 7) if phi == 1 else (a >> 3) if phi == 2 else ((a & 7) ^ (a >> 3))
+        y = (b & 7) if phi == 1 else (b >> 3) if phi == 2 else ((b & 7) ^ (b >> 3))
+        if not x or not y or x == y:
+            return False
+    return True
+
+
+def common_b_row(b1, b2):
+    parts = (b1 & 7, b2 & 7, b1 >> 3, b2 >> 3)
+    return len({x for x in parts if x}) == 1
+
+
+def binary_coordinate_factor(rows, column):
+    other = 7 << (3 * (1 - column))
+    return all((row & other) == ((1 << i) & other)
+               for i, row in enumerate(rows))
+
+
+def binary_exception_word(a, b, b1, b2, target):
+    parts = (b1 & 7, b2 & 7, b1 >> 3, b2 >> 3)
+    base = next(x for x in parts if x)
+    c1 = int(parts[0] == base) | (int(parts[1] == base) << 1)
+    ac = (a if c1 & 1 else 0) ^ (b if c1 & 2 else 0)
+    first, second = ac & 7, ac >> 3
+    require(first != 0, "exceptional A_1 c_1 must be nonzero")
+    h = (first & -first).bit_length() - 1
+    ell = tuple((1 << h) if (second >> i) & 1 else 0 for i in range(3))
+    m11 = tuple(row & 7 for row in target[:3])
+    m12 = tuple(row >> 3 for row in target[:3])
+    m22 = tuple(row >> 3 for row in target[3:])
+    correction = binary_product(ell, m12, 3)
+    d = tuple(x ^ y for x, y in zip(m22, correction))
+    ident = (1, 2, 4)
+    f1 = ident + tuple(ell[i] | (ident[i] << 3) for i in range(3))
+    f2 = tuple(ident[i] | (m12[i] << 3) for i in range(3)) + tuple(x << 3 for x in d)
+    f3 = m11 + tuple(x << 3 for x in ident)
+    factors = (f1, f2, f3)
+    require(all(binary_coordinate_factor(f, j) for f, j in zip(factors, (0, 1, 0))),
+            "illegal right-vector factor")
+    require(binary_product(f1, binary_product(f2, f3, 6), 6) == target,
+            "three-factor word differs from target")
+    return factors
+
+
+def binary_census():
+    rank6, rank3 = rank_table(6), rank_table(3)
+    bases = [(a, b) for a in range(1, 64) for b in range(a + 1, 64) if b < (a ^ b)]
+    right = [(a, b, common_b_row(a, b)) for a in range(1, 64)
+             for b in range(1, 64) if a != b]
+    require(len(bases) == 651 and len(right) == 3906, "rank-factor coverage")
+    histogram = [0, 0, 0, 0]
+    digest = sha256()
+    samples = {}
+    full_pencils = 0
+    for a, b in bases:
+        full = full_a_pencil(a, b)
+        full_pencils += full
+        selectors = tuple(((a >> i) & 1) | (((b >> i) & 1) << 1) for i in range(6))
+        for b1, b2, common in right:
+            options = (0, b1, b2, b1 ^ b2)
+            rows = tuple(options[i] for i in selectors)
+            exception = full and common
+            passing = literal_two_factor_criterion(rows, rank6, rank3)
+            require(passing != exception, "classification disagrees with full-matrix criterion")
+            cost = 3 if exception else 2
+            if exception:
+                binary_exception_word(a, b, b1, b2, rows)
+            histogram[cost] += 1
+            digest.update(bytes(rows + (cost,)))
+            samples.setdefault((full, common), rows)
+    require(histogram == [0, 0, 2535162, 7644], "complete cost histogram")
+    require(full_pencils == 182 and len(samples) == 4, "pencil-class coverage")
+    return {"targets": sum(histogram), "histogram": histogram,
+            "column_spaces": len(bases), "right_factors": len(right),
+            "exceptional_column_spaces": full_pencils,
+            "table_sha256": digest.hexdigest()}, samples
+
+
+def add(a, b, q):
+    return a ^ b if q == 4 else (a + b) % q
+
+
+def multiply(a, b, q):
+    if q == 4:
+        return ((0, 0, 0, 0), (0, 1, 2, 3),
+                (0, 2, 3, 1), (0, 3, 1, 2))[a][b]
+    return a * b % q
+
+
+def negative(a, q):
+    return a if q == 4 else -a % q
+
+
+def inverse(a, q):
+    require(a != 0, "division by zero")
+    return next(b for b in range(1, q) if multiply(a, b, q) == 1)
+
+
+def matrix_product(a, b, q):
+    out = [[0] * len(b[0]) for _ in a]
+    for i in range(len(a)):
+        for j in range(len(b[0])):
+            value = 0
+            for k in range(len(b)):
+                value = add(value, multiply(a[i][k], b[k][j], q), q)
+            out[i][j] = value
+    return out
+
+
+def identity(n):
+    return [[int(i == j) for j in range(n)] for i in range(n)]
+
+
+def solve(a, b, q):
+    """Solve A X=B, with zero free variables; reject inconsistent systems."""
+    n, rhs = len(a[0]), len(b[0])
+    rows = [list(x) + list(y) for x, y in zip(a, b)]
+    pivots = []
+    for col in range(n):
+        candidates = [i for i in range(len(pivots), len(rows)) if rows[i][col]]
+        if not candidates:
+            continue
+        k, source = len(pivots), candidates[0]
+        rows[k], rows[source] = rows[source], rows[k]
+        factor = inverse(rows[k][col], q)
+        rows[k] = [multiply(x, factor, q) for x in rows[k]]
+        for i in range(len(rows)):
+            if i != k and rows[i][col]:
+                factor = negative(rows[i][col], q)
+                rows[i] = [add(x, multiply(factor, y, q), q)
+                           for x, y in zip(rows[i], rows[k])]
+        pivots.append(col)
+    if any(any(row[n:]) for row in rows[len(pivots):]):
+        return None
+    out = [[0] * rhs for _ in range(n)]
+    for i, col in enumerate(pivots):
+        out[col] = rows[i][n:]
+    require(matrix_product(a, out, q) == b, "linear solve postcondition")
+    return out
+
+
+def dense_rank(a, q):
+    basis = []
+    for column in zip(*a):
+        rhs = [[x] for x in column]
+        if not basis or solve([list(row) for row in zip(*basis)], rhs, q) is None:
+            if any(column):
+                basis.append(column)
+    return len(basis)
+
+
+def free_matrix(s, m):
+    return [[s[i // m][j // m] if i % m == j % m else 0
+             for j in range(2 * m)] for i in range(2 * m)]
+
+
+def coordinate_factor(f, column, m):
+    return all(f[i][j] == int(i == j) for i in range(2 * m)
+               for j in range(2 * m) if j // m != column)
+
+
+def projective(q):
+    return [(1, x) for x in range(q)] + [(0, 1)]
+
+
+def chart(first, q, columns=False):
+    second = next(v for v in projective(q)
+                  if add(multiply(first[0], v[1], q),
+                         negative(multiply(first[1], v[0], q), q), q))
+    rows = [list(first), list(second)]
+    return [list(x) for x in zip(*rows)] if columns else rows
+
+
+def two_factor_word(target, q):
+    m = len(target) // 2
+    for phi in projective(q):
+        g = free_matrix(chart(phi, q), m)
+        for v in projective(q):
+            h = free_matrix(chart(v, q, columns=True), m)
+            n = matrix_product(matrix_product(g, target, q), h, q)
+            a = [row[:m] for row in n[:m]]
+            b = [row[:m] for row in n[m:]]
+            c = solve(a, [row[m:] for row in n[:m]], q)
+            if c is None:
+                continue
+            bc = matrix_product(b, c, q)
+            d = [[add(n[i + m][j + m], negative(bc[i][j], q), q)
+                  for j in range(m)] for i in range(m)]
+            f1, f2 = identity(2 * m), identity(2 * m)
+            for i in range(m):
+                f1[i][:m], f1[i + m][:m] = a[i], b[i]
+                f2[i][m:], f2[i + m][m:] = c[i], d[i]
+            require(coordinate_factor(f1, 0, m) and coordinate_factor(f2, 1, m),
+                    "two-factor alphabet")
+            require(matrix_product(f1, f2, q) == n, "two-factor chart endpoint")
+            gi, hi = solve(g, identity(2 * m), q), solve(h, identity(2 * m), q)
+            require(gi is not None and hi is not None, "free chart inverse")
+            endpoint = matrix_product(matrix_product(gi, f1, q),
+                                      matrix_product(f2, hi, q), q)
+            require(endpoint == target, "two-factor actual endpoint")
+            return g, h, f1, f2
+    return None
+
+
+def explicit_example(m):
+    target = [[0] * (2 * m) for _ in range(2 * m)]
+    target[0][0] = target[1][m] = target[m + 1][0] = target[m + 2][m] = 1
+    f1, f2, f3 = identity(2 * m), identity(2 * m), identity(2 * m)
+    f1[m + 1][0] = f2[1][m] = 1
+    for i in range(m):
+        for j in range(m):
+            f2[m + i][m + j] = int((i, j) == (2, 0))
+            f3[i][j] = int((i, j) == (0, 0))
+    return target, (f1, f2, f3)
+
+
+def finite_field_examples(samples):
+    cases = []
+    for q, m in product((2, 3, 4, 5, 7), (3, 4)):
+        target, factors = explicit_example(m)
+        require(dense_rank(target, q) == 2, "explicit ordinary rank")
+        require(two_factor_word(target, q) is None, "explicit shorter word")
+        endpoint = matrix_product(factors[0], matrix_product(factors[1], factors[2], q), q)
+        require(endpoint == target, "all-field explicit three-factor word")
+        require(all(coordinate_factor(f, j, m) for f, j in zip(factors, (0, 1, 0))),
+                "all-field legal factor")
+        require(matrix_product(factors[2], matrix_product(factors[1], factors[0], q), q)
+                != target, "reversed chronology control")
+        require(matrix_product(factors[0], factors[2], q) != target, "omitted factor control")
+        cases.append({"q": q, "m": m, "cost": 3})
+    for (full, common), rows in sorted(samples.items()):
+        target = [[(row >> j) & 1 for j in range(6)] for row in rows]
+        require((two_factor_word(target, 2) is None) == (full and common),
+                "independent dense chart witnesses")
+    return cases
+
+
+def controls():
+    target, factors = explicit_example(3)
+    for data in product(range(2), repeat=6):
+        value = [[x] for x in data]
+        for factor in reversed(factors):
+            value = matrix_product(factor, value, 2)
+        require(value == matrix_product(target, [[x] for x in data], 2), "dirty input")
+    boundary = [[0] * 4 for _ in range(4)]
+    boundary[2][2] = boundary[3][3] = 1
+    require(dense_rank(boundary, 2) == 2 and coordinate_factor(boundary, 0, 2),
+            "m=2 one-factor boundary")
+    require(not full_a_pencil(9, 18), "dependent sum pencil control")
+    require(not common_b_row(1, 16), "rank-one blocks need a common row")
+    require(multiply(2, 2, 4) == 3 and add(2, 2, 4) == 0,
+            "F4 differs from integers modulo four")
+    require(solve([[0]], [[1]], 2) is None, "inconsistent solve must reject")
+    require(solve([[0]], [[0]], 2) == [[0]], "singular consistent solve")
+    changed = [row[:] for row in factors[0]]
+    changed[0][3] = 1
+    require(not coordinate_factor(changed, 0, 3), "changed fixed block column")
+    return {"dirty_inputs": 64, "boundary_and_mutation_controls": 7}
+
+
+def source_receipt():
+    package = Path(__file__).resolve().parent
+    root = package.parent.parent
+    manifest = json.loads(bounded_read(package / "SOURCES.json"))
+    require(len(manifest["files"]) <= 8, "source manifest capacity")
+    hashes = {}
+    for row in manifest["files"]:
+        if row["usage"] == "input":
+            digest = sha256(bounded_read(root / row["path"])).hexdigest()
+            require(digest == row["sha256"], "predecessor source drift: " + row["path"])
+            hashes[row["path"]] = digest
+    for name in ("PROOF.md", "README.md", "SOURCES.json", "TASK.json", "VERIFY.json", "verify.py"):
+        path = package / name
+        hashes[path.relative_to(root).as_posix()] = sha256(bounded_read(path)).hexdigest()
+    return hashes
+
+
+def bounded_read(path):
+    with path.open("rb") as stream:
+        data = stream.read(1048577)
+    require(len(data) <= 1048576, "source file exceeds one MiB")
+    return data
+
+
+def main():
+    hashes = source_receipt()
+    census, samples = binary_census()
+    fields = finite_field_examples(samples)
+    checks = controls()
+    receipt = {"schema": "rank-two-right-vector/v1", "census": census,
+               "field_examples": fields, "controls": checks, "file_sha256": hashes}
+    encoded = json.dumps(receipt, sort_keys=True, separators=(",", ":"))
+    print(encoded)
+    print("PASS_RIGHT_VECTOR_RANK_TWO targets=2542806 cost2=2535162 cost3=7644 "
+          "three_factor_words=7644 no_new_kappa receipt_sha256=" + sha256(encoded.encode()).hexdigest())
+
+
+if __name__ == "__main__":
+    main()