diff --git a/research/radical-common-flag/PROOF.md b/research/radical-common-flag/PROOF.md
new file mode 100644
index 0000000000..8474444c13
--- /dev/null
+++ b/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.
diff --git a/research/radical-common-flag/README.md b/research/radical-common-flag/README.md
new file mode 100644
index 0000000000..2886ccd202
--- /dev/null
+++ b/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.
diff --git a/research/radical-common-flag/SOURCES.json b/research/radical-common-flag/SOURCES.json
new file mode 100644
index 0000000000..fe336e73f7
--- /dev/null
+++ b/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"
+    }
+  ]
+}
diff --git a/research/radical-common-flag/TASK.json b/research/radical-common-flag/TASK.json
new file mode 100644
index 0000000000..819f2e54f3
--- /dev/null
+++ b/research/radical-common-flag/TASK.json
@@ -0,0 +1,117 @@
+{
+  "schema_version": 1,
+  "task_id": "formal-interface-lemma",
+  "priority_revision": 8,
+  "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+  "original_card": {
+    "id": "formal-interface-lemma",
+    "question": "Can one uncovered interface implication be formalized with exact caller and certificate bindings?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "research/gate-operand-parity-lean/README.md",
+      "research/staged544-certified-endpoint/README.md",
+      "research/unconditional-batched-crt/README.md"
+    ],
+    "methods": [
+      "Formalize a missing boundary lemma identified by the selected review.",
+      "Audit a formal theorem-to-certificate binding independently."
+    ],
+    "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_selected_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.",
+      "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse."
+    },
+    "first_experiment": "Write one missing statement with quantified hypotheses, actual caller and existing coverage. A compact-switch lemma is a candidate only after its mathematical contract is reviewed. Establish a bounded proof plan before a separately budgeted proof-assistant build; do not rerun large Lean jobs as orientation.",
+    "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.",
+    "allowed_variations": [
+      "Narrow to one formal lemma or one theorem-to-certificate binding."
+    ],
+    "scope_change_triggers": [
+      "Formalizing already-covered arithmetic and claiming the full multiplication theorem."
+    ],
+    "overlap_terms": [
+      "hyperplane end",
+      "formal interface",
+      "Lean binding",
+      "3807",
+      "3857",
+      "4100",
+      "gate-operand-parity-lean",
+      "staged544-certified-endpoint",
+      "unconditional-batched-crt"
+    ],
+    "existing_checks": [
+      {
+        "scope": "PR #3807: scoped gate-operand parity formalization.",
+        "evidence": "research/gate-operand-parity-lean/README.md",
+        "remaining": "Exact theorem-to-caller binding and genuinely uncovered interface lemmas.",
+        "status": "author-checked",
+        "source_commit": "4c3530f42a6abcc48e7a6bcffd6c901911dc8269",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #3857: certified real-power moment/endpoint arithmetic.",
+        "evidence": "research/staged544-certified-endpoint/README.md",
+        "remaining": "Uniform algorithmic implications, not another endpoint digit.",
+        "status": "author-checked",
+        "source_commit": "ef4315b8caa605e47a2515004845eb2d2ed71a86",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #4100: compact-switch formalization proposed as future validation.",
+        "evidence": "research/unconditional-batched-crt/README.md",
+        "remaining": "Audit the statement and assumptions before a formal proof campaign.",
+        "status": "author-checked",
+        "source_commit": "337d04939571a637aeab54a0f58f54fde811663a",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      }
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Classify all finite-length reachability of pure square-zero radical targets with an invertible coefficient, for every field, role count and finite coefficient tuple; prove exact paid cost n when reachable.",
+  "scope_change_reason": "The formal-interface-lemma card is changed to the algebraic common-flag question explicitly posed in PR5854. This is a new written proof, not proof-assistant formalization, an audit or a selected-assumption discharge.",
+  "bottleneck_link": "A complete reachability criterion can reject formal coefficient interfaces before unbounded word search. This is algebraic side work: no native coefficient producer or favorable complete physical bill is supplied.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop at the first proved common-flag criterion and exact attaining word with bounded corroboration; leave other endpoint and auxiliary-role contracts open.",
+  "outcome": "completed",
+  "evidence": "PROOF.md proves necessity at every chronological cut and an exact n-factor construction. verify.py supplies complete small coefficient-pair domains, literal matrix words, arbitrary-input basis checks, abstract cut identities and rejecting controls.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Can an extra role restored to the identity make a nonsimultaneously triangularizable radical target reachable?",
+      "why_it_matters": "The scalar endpoint becomes nonzero and the cut lemma no longer forces the full invariant flag.",
+      "first_step": "Test diag(M,1) for the explicit four-role fixture while keeping base-field right vectors and every dirty-input column.",
+      "blocked_by": "The distinguished radical coefficient is singular on the enlarged role space; no replacement invariant or attaining word is supplied."
+    },
+    {
+      "question": "Which zero-residue targets without an invertible coefficient are reachable?",
+      "why_it_matters": "The proved classification uses invertibility to turn each scalar-prefix kernel into an invariant subspace.",
+      "first_step": "Specify one singular coefficient tuple and its simultaneous source/image flags, then seek a complete paid word or obstruction.",
+      "blocked_by": "The cut image can have excess dimension, so the rank equality in the proof is unavailable."
+    }
+  ],
+  "claim_type": "scoped written algebraic proof with exact finite corroboration",
+  "coordination": {
+    "source_question": "PR #5854, Open next question 1",
+    "source_author": "petalas",
+    "source_head": "e70246e3aabe63aacbddb41dfa2253e865798d1d",
+    "source_created_at": "2026-10-27T09:11:04Z",
+    "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19375372",
+    "overlap": "Live open/account PRs and handoffs, active Discussions, main README general forms, merged searches, and local reservations. Cached snapshot: 572 open PRs, 6639 Discussion records, complete remote pagination; sparse local notes incomplete. No novelty claim about arbitrary historical diffs or unpublished work."
+  },
+  "environment": {
+    "python": "3.12.15",
+    "implementation": "CPython",
+    "system": "Darwin",
+    "machine": "arm64",
+    "dependencies": "standard library only"
+  }
+}
diff --git a/research/radical-common-flag/VERIFY.json b/research/radical-common-flag/VERIFY.json
new file mode 100644
index 0000000000..0d7884b468
--- /dev/null
+++ b/research/radical-common-flag/VERIFY.json
@@ -0,0 +1,38 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-W",
+        "error",
+        "-X",
+        "dev",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Complete geometric/basis coefficient-pair comparison, exact attaining words and all-input basis action, chronological and abstract cut identities, strict obstruction and twelve boundary and semantic controls."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-O",
+        "-W",
+        "error",
+        "-X",
+        "dev",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Identical full finite corroboration with optimization enabled; every gate uses explicit exceptions."
+    }
+  ]
+}
diff --git a/research/radical-common-flag/verify.py b/research/radical-common-flag/verify.py
new file mode 100644
index 0000000000..24744b27af
--- /dev/null
+++ b/research/radical-common-flag/verify.py
@@ -0,0 +1,344 @@
+#!/usr/bin/env python3
+"""Exact finite corroboration. Produced by Nick Petalas. Apache-2.0."""
+
+import hashlib
+import itertools
+import json
+from pathlib import Path
+
+
+def need(condition, message):
+    if not condition:
+        raise ValueError(message)
+
+
+def eye(n):
+    return tuple(int(i == j) for i in range(n) for j in range(n))
+
+
+def add(a, b, p):
+    need(len(a) == len(b), "matrix size")
+    return tuple((x+y) % p for x, y in zip(a, b, strict=True))
+
+
+def mul(a, b, n, p):
+    need(len(a) == len(b) == n*n, "matrix product size")
+    return tuple(sum(a[i*n+k]*b[k*n+j] for k in range(n)) % p
+                 for i in range(n) for j in range(n))
+
+
+def mv(a, v, n, p):
+    return tuple(sum(a[i*n+j]*v[j] for j in range(n)) % p for i in range(n))
+
+
+def vm(v, a, n, p):
+    return tuple(sum(v[i]*a[i*n+j] for i in range(n)) % p for j in range(n))
+
+
+def reduce_matrix(a, n, p):
+    rows = [list(a[i*n:(i+1)*n]) + list(eye(n)[i*n:(i+1)*n]) for i in range(n)]
+    pivot = 0
+    for j in range(n):
+        choices = [i for i in range(pivot, n) if rows[i][j]]
+        if not choices:
+            continue
+        i = choices[0]
+        rows[pivot], rows[i] = rows[i], rows[pivot]
+        scale = pow(rows[pivot][j], -1, p)
+        rows[pivot] = [x*scale % p for x in rows[pivot]]
+        for i in range(n):
+            if i != pivot:
+                scale = rows[i][j]
+                rows[i] = [(x-scale*y) % p
+                           for x, y in zip(rows[i], rows[pivot], strict=True)]
+        pivot += 1
+    inverse = tuple(x for row in rows for x in row[n:]) if pivot == n else None
+    if inverse is not None:
+        need(mul(a, inverse, n, p) == eye(n), "inverse invariant")
+    return pivot, inverse
+
+
+def upper(a, n):
+    return all(a[i*n+j] == 0 for i in range(n) for j in range(i))
+
+
+def points(n, p):
+    return tuple(v for v in itertools.product(range(p), repeat=n)
+                 if next((x for x in v if x), None) == 1)
+
+
+def multiple(v, w, p):
+    return any(v == tuple(c*x % p for x in w) for c in range(p))
+
+
+def flag_mask(a, flags, n, p):
+    mask = 0
+    for i, (v, w) in enumerate(flags):
+        if multiple(mv(a, v, n, p), v, p):
+            if w is None or multiple(vm(w, a, n, p), w, p):
+                mask |= 1 << i
+    return mask
+
+
+def census(n, p):
+    need((n, p) in ((2, 2), (2, 3), (3, 2)), "census capacity")
+    matrices = tuple(itertools.product(range(p), repeat=n*n))
+    lines = points(n, p)
+    flags = (tuple((v, None) for v in lines) if n == 2 else
+             tuple((v, w) for v in lines for w in lines
+                   if sum(x*y for x, y in zip(v, w, strict=True)) % p == 0))
+    bases = [(g, reduce_matrix(g, n, p)[1]) for g in matrices]
+    bases = [(g, gi) for g, gi in bases if gi is not None]
+    geometric = [flag_mask(a, flags, n, p) for a in matrices]
+    triangular = []
+    for a in matrices:
+        mask = 0
+        for i, (g, gi) in enumerate(bases):
+            if upper(mul(mul(gi, a, n, p), g, n, p), n):
+                mask |= 1 << i
+        triangular.append(mask)
+    histogram = {}
+    for i in range(len(matrices)):
+        for j in range(len(matrices)):
+            common = geometric[i] & geometric[j]
+            need(bool(common) == bool(triangular[i] & triangular[j]), "flag criteria")
+            k = common.bit_count()
+            histogram[k] = histogram.get(k, 0)+1
+    visited = sum(histogram.values())
+    need(visited == len(matrices)**2, "incomplete pair domain")
+    return {"n": n, "q": p, "pairs": visited, "flags": len(flags),
+            "bases": len(bases), "reachable": visited-histogram.get(0, 0),
+            "common_flag_histogram": histogram}
+
+
+def ring_identity(n, size):
+    return (eye(n),) + ((0,)*(n*n),)*(size-1)
+
+
+def ring_mul(a, b, n, p):
+    need(2 <= len(a) == len(b) <= 4, "radical dimension")
+    return (mul(a[0], b[0], n, p),) + tuple(
+        add(mul(a[0], b[j], n, p), mul(a[j], b[0], n, p), p)
+        for j in range(1, len(a)))
+
+
+def word(coefficients, g, c0, n, p):
+    need(1 <= n <= 4 and p in (2, 3, 5), "constructor capacity")
+    need(1 <= len(coefficients) <= 3, "coefficient count")
+    need(coefficients[0] == eye(n), "distinguished coefficient")
+    need(all(upper(a, n) for a in coefficients), "supplied flag")
+    gi = reduce_matrix(g, n, p)[1]
+    need(gi is not None and reduce_matrix(c0, n, p)[1] is not None, "free maps")
+    size = len(coefficients)+1
+    factors = [(gi,) + ((0,)*(n*n),)*(size-1)]
+    for j in range(n):
+        scalar = list(eye(n))
+        scalar[j*n+j] = 0
+        columns = tuple(tuple(a[i*n+k] if k == j else 0
+                              for i in range(n) for k in range(n))
+                        for a in coefficients)
+        factors.append((tuple(scalar),) + columns)
+    left = mul(c0, g, n, p)
+    factors.append((left,) + ((0,)*(n*n),)*(size-1))
+    target = ((0,)*(n*n),) + tuple(
+        mul(mul(left, a, n, p), gi, n, p) for a in coefficients)
+    return factors, target
+
+
+def endpoint(factors, n, p, size):
+    result = ring_identity(n, size)
+    for factor in factors:
+        result = ring_mul(factor, result, n, p)
+    return result
+
+
+def literal(factors, data, n, p):
+    state = [list(v) for v in data]
+    for factor in factors:
+        after = [[0]*n for _ in range(len(state))]
+        for i in range(n):
+            for j in range(n):
+                after[0][i] += factor[0][i*n+j]*state[0][j]
+                for k in range(1, len(state)):
+                    after[k][i] += (factor[0][i*n+j]*state[k][j]
+                                    + factor[k][i*n+j]*state[0][j])
+        state = [[x % p for x in v] for v in after]
+    return tuple(tuple(v) for v in state)
+
+
+def literal_columns(factors, target, n, p):
+    count = 0
+    for k in range(len(target)):
+        for i in range(n):
+            data = tuple(tuple(int(j == i and h == k) for j in range(n))
+                         for h in range(len(target)))
+            need(literal(factors, data, n, p) == literal([target], data, n, p),
+                 "arbitrary-input column")
+            count += 1
+    return count
+
+
+def cuts(factors, target, n, p):
+    need(target[0] == (0,)*(n*n), "scalar endpoint")
+    xi = reduce_matrix(target[1], n, p)[1]
+    need(xi is not None, "invertible distinguished coefficient")
+    normalized = [mul(xi, a, n, p) for a in target[2:]]
+    dimensions = []
+    vectors = tuple(itertools.product(range(p), repeat=n))
+    for cut in range(len(factors)+1):
+        prefix = endpoint(factors[:cut], n, p, len(target))
+        suffix = endpoint(factors[cut:], n, p, len(target))
+        h, s = prefix[0], suffix[0]
+        need(mul(s, h, n, p) == (0,)*(n*n), "scalar cut product")
+        kernel = {v for v in vectors if mv(h, v, n, p) == (0,)*n}
+        k = n-reduce_matrix(h, n, p)[0]
+        need(reduce_matrix(s, n, p)[0] == k, "cut rank equality")
+        need({mv(target[1], v, n, p) for v in kernel}
+             == {mv(s, v, n, p) for v in vectors}, "cut image equality")
+        for j in range(1, len(target)):
+            need(target[j] == add(mul(s, prefix[j], n, p),
+                                  mul(suffix[j], h, n, p), p), "cut coefficient")
+        need(all(mv(a, v, n, p) in kernel for a in normalized for v in kernel),
+             "cut invariance")
+        dimensions.append(k)
+    need(set(dimensions) == set(range(n+1)), "complete flag dimensions")
+    need(all(0 <= b-a <= 1 for a, b in zip(dimensions, dimensions[1:])), "rank drop")
+    return len(dimensions)
+
+
+def constructions():
+    count = columns = cut_count = 0
+    for n, p in ((2, 2), (2, 3), (3, 2)):
+        positions = [(i, j) for i in range(n) for j in range(i, n)]
+        triangular = []
+        for values in itertools.product(range(p), repeat=len(positions)):
+            a = [0]*(n*n)
+            for (i, j), value in zip(positions, values, strict=True):
+                a[i*n+j] = value
+            triangular.append(tuple(a))
+        for a in triangular:
+            for b in triangular:
+                factors, target = word((eye(n), a, b), eye(n), eye(n), n, p)
+                need(endpoint(factors, n, p, len(target)) == target, "attaining word")
+                if count % 257 == 0:
+                    columns += literal_columns(factors, target, n, p)
+                    cut_count += cuts(factors, target, n, p)
+                count += 1
+    a, b = (0, 1, 0, 0, 0, 1, 0, 0, 0), (1, 0, 1, 0, 0, 0, 0, 0, 1)
+    for g in itertools.product(range(2), repeat=9):
+        if reduce_matrix(g, 3, 2)[1] is not None:
+            factors, target = word((eye(3), a, b), g, g, 3, 2)
+            need(endpoint(factors, 3, 2, len(target)) == target, "changed bases")
+            columns += literal_columns(factors, target, 3, 2)
+            cut_count += cuts(factors, target, 3, 2)
+            count += 1
+    for n, p in ((1, 2), (1, 5), (4, 3), (4, 5)):
+        a = tuple((i+j+1) % p if i <= j else 0 for i in range(n) for j in range(n))
+        factors, target = word((eye(n), a), eye(n), eye(n), n, p)
+        need(endpoint(factors, n, p, len(target)) == target, "boundary sizes")
+        columns += literal_columns(factors, target, n, p)
+        cut_count += cuts(factors, target, n, p)
+        count += 1
+    factors, target = word((eye(1),), eye(1), eye(1), 1, 2)
+    need(endpoint(factors, 1, 2, len(target)) == target, "vacuous tuple")
+    columns += literal_columns(factors, target, 1, 2)
+    cut_count += cuts(factors, target, 1, 2)
+    count += 1
+    return {"words": count, "dirty_basis_columns": columns, "cuts": cut_count}
+
+
+def abstract_cuts():
+    matrices = tuple(itertools.product(range(2), repeat=4))
+    pair_count = coefficient_count = 0
+    for h in matrices:
+        kernel = {v for v in itertools.product(range(2), repeat=2)
+                  if mv(h, v, 2, 2) == (0, 0)}
+        for s in matrices:
+            if mul(s, h, 2, 2) != (0,)*4:
+                continue
+            pair_count += 1
+            image = {add(mul(s, d, 2, 2), mul(e, h, 2, 2), 2)
+                     for d in matrices for e in matrices}
+            for x in image:
+                xi = reduce_matrix(x, 2, 2)[1]
+                if xi is None:
+                    continue
+                need(reduce_matrix(s, 2, 2)[0] == 2-reduce_matrix(h, 2, 2)[0],
+                     "abstract cut rank")
+                for y in image:
+                    a = mul(xi, y, 2, 2)
+                    need(all(mv(a, v, 2, 2) in kernel for v in kernel), "abstract flag")
+                    coefficient_count += 1
+    return {"scalar_pairs": pair_count, "admissible_cut_cases": coefficient_count}
+
+
+def strict_fixture():
+    a = (0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 1, 0, 0, 0, 0)
+    b = (0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 2, 0)
+    common = [v for v in points(4, 3) if mv(a, v, 4, 3) == (0,)*4
+              and mv(b, v, 4, 3) == (0,)*4]
+    need(common == [(1, 0, 0, 0)], "forced first line")
+    qa = tuple(a[i*4+j] for i in range(1, 4) for j in range(1, 4))
+    qb = tuple(b[i*4+j] for i in range(1, 4) for j in range(1, 4))
+    need(not any(mv(qa, v, 3, 3) == (0,)*3 and mv(qb, v, 3, 3) == (0,)*3
+                 for v in points(3, 3)), "irreducible flag quotient")
+    need(mul(mul(a, a, 4, 3), a, 4, 3) == (0,)*16
+         and mul(mul(b, b, 4, 3), b, 4, 3) == (0,)*16, "nilpotent coefficients")
+    return {"q": 3, "roles": 4, "common_lines": 1, "quotient_common_lines": 0}
+
+
+def controls():
+    count = 0
+    invalid = [((eye(2), (0, 0, 1, 0)), eye(2), eye(2), 2, 2),
+               ((eye(2),), (0,)*4, eye(2), 2, 2),
+               ((eye(2),), eye(2), (0,)*4, 2, 2),
+               ((eye(2),)*4, eye(2), eye(2), 2, 2),
+               ((eye(2),), eye(2), eye(2), 2, 7),
+               (((0,)*4,), eye(2), eye(2), 2, 2)]
+    for args in invalid:
+        try:
+            word(*args)
+        except ValueError:
+            count += 1
+        else:
+            raise ValueError("invalid constructor accepted")
+    a = (0, 1, 0, 0, 0, 1, 0, 0, 0)
+    factors, target = word((eye(3), a), eye(3), eye(3), 3, 2)
+    for i in range(1, 4):
+        need(endpoint(factors[:i]+factors[i+1:], 3, 2, len(target)) != target,
+             "omitted paid factor")
+        count += 1
+    need(endpoint(list(reversed(factors)), 3, 2, len(target)) != target, "chronology")
+    count += 1
+    h, s, y = (1, 0, 0, 0), eye(2), (0, 1, 0, 0)
+    need(mul(s, h, 2, 2) != (0,)*4 and mv(y, (0, 1), 2, 2) == (1, 0),
+         "missing scalar-endpoint countercontrol")
+    count += 1
+    try:
+        cuts([target], ((0,)*9, (0,)*9, a), 3, 2)
+    except ValueError:
+        count += 1
+    else:
+        raise ValueError("singular coefficient accepted")
+    return count
+
+
+def main():
+    result = {"status": "PASS_RADICAL_COMMON_FLAG",
+              "claim_type": "scoped written proof with exact finite corroboration",
+              "pair_censuses": [census(n, p) for n, p in ((2, 2), (2, 3), (3, 2))],
+              "construction": constructions(), "cut_lemma": abstract_cuts(),
+              "strict_obstruction": strict_fixture(), "controls": controls()}
+    package = Path(__file__).resolve().parent
+    hashes = {}
+    for name in ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", "VERIFY.json", "verify.py"):
+        with (package/name).open("rb") as source:
+            content = source.read(131073)
+        need(len(content) <= 131072, "file capacity")
+        hashes[name] = hashlib.sha256(content).hexdigest()
+    result["sha256"] = hashes
+    print(json.dumps(result, sort_keys=True, indent=2))
+
+
+if __name__ == "__main__":
+    main()