diff --git a/research/productive-controller-basis-search/GLOBAL-PROOF.md b/research/productive-controller-basis-search/GLOBAL-PROOF.md
new file mode 100644
index 0000000000..74b67e22e6
--- /dev/null
+++ b/research/productive-controller-basis-search/GLOBAL-PROOF.md
@@ -0,0 +1,183 @@
+# Two global obstructions for controllers without idle work
+
+Cinna Davis / 1337isnot1337, with substantial OpenAI Codex assistance.
+Apache-2.0. These are written binary-algebra proofs, supported by finite checks;
+there is no formal-kernel or independent human acceptance claim.
+
+## Contract
+
+Let n=2p main fields, Q a central involution, and work over
+`F2[Q,D_1,...,D_f]/(Q^2-1)`. Every full native call has its **own independent**
+commuting multiplier D_i and is
+
+    (I+(D_i+1)P_i)(I+Q N_i),
+
+with P_i a binary rank-two projector, N_i a rank-one nilpotent, and
+`P_i N_i=N_i P_i=N_i`. A thin call is `I+Q N_i`. Arbitrary invertible binary
+basis changes between calls are allowed and absorbed by conjugation. There
+are no idle multipliers or repeated/specialized stage variables.
+
+Success means constant invertible binary L,R give independent main jobs:
+
+    L M R = diag(Q*m_1(D), ..., Q*m_n(D)),
+
+where every m_j is a monomial. This is an algebraic prerequisite of the
+retained native/query supplier model, not a native implementation theorem.
+
+**Theorem A.** If every call is full, success requires at least 3p calls.
+For a fixed local inventory, its target-minus-paid concave moment **per full
+call** is no larger than that of a three-call unit. Thus it cannot admit a
+larger raw saving than the disjoint three-call construction.
+
+**Theorem B.** Every successful controller needs at least 2p+1 query-bearing
+calls. If it uses exactly 2p+1 and p>=2, at most **two** calls can be full.
+For the retained BIT inventory, its complete target-minus-paid moment is at
+most **-15 for every exponent t in [0,1]**, so it cannot supply a recursive
+saving. The binary theorem is not asserted for arbitrary complex words.
+
+Thus both all-full controllers of arbitrary length and minimum-query mixed
+controllers fail to supply the hoped-for large improvement by deleting idles.
+The changed premise still open is a mixed controller with additional queries,
+a changed target, dependent stage multipliers, or a different local family.
+
+## Common tangent and projector identities
+
+Set all D_i=1 and write Q=1+e with e^2=0. Normalize the derivative by the
+invertible constant operator at e=0. A call's contribution is a conjugate
+
+    R_i = u_i v_i^T,  v_i^T u_i=0,
+
+of its nilpotent. The desired endpoint gives
+
+    sum_i R_i = I_n.                                      (1)
+
+For a full call, differentiate in its unique D_i and normalize on the right.
+At D=1 its projector is conjugated by the later query calls. Since the desired
+endpoint is independently diagonal, these normalized projectors E_i are
+constant in Q, have rank two, commute pairwise, and satisfy
+
+    E_i R_i = R_i E_i = R_i,
+    [E_i, sum_{j>i} R_j] = 0.                             (2)
+
+The second identity is the Q derivative of the conjugated projector. Each
+R_j is written in the same final coordinate system. These are necessary
+identities; no converse or free physical implementation is assumed.
+
+## Proof of A: edge parity
+
+Use the common binary output basis diagonalizing all full projectors E_i.
+Each E_i selects two coordinates. Its R_i is therefore supported on that
+coordinate pair and is one of the three nonzero rank-one nilpotents
+
+    [0 1;0 0],  [0 0;1 0],  [1 1;1 1].
+
+For any unordered coordinate pair, (1) requires zero off-diagonal sum.
+Consequently the parity of the number of each of these three types is equal.
+If that common parity is odd, there are at least three calls on the pair,
+and the pair contributes one to both diagonal entries. Otherwise it contributes
+zero to the diagonal. Every coordinate must meet an odd number of the former
+pairs. There are at least n/2=p such pairs, and hence at least 3p calls.
+Disjoint three-call swaps attain the call bound.
+
+For the moment claim let f be the number of full calls, v the local port count,
+b the transverse block rank, and t in (0,1). Each independent D_i occurs with
+total degree two in the determinant, so `sum_j degree(m_j)=2f`. Jensen gives
+
+    main target moment <= n*v*(1+2*b*f/n)^t.
+
+Put a=f/p>=3. Dividing by f bounds this by
+`(2v/a)*(1+b*a)^t`. Its derivative in a has the sign of
+`(t-1)*b*a-1`, which is negative. The bound is therefore at most
+`(2v/3)*(1+3b)^t`, exactly the per-call main moment of disjoint three-call
+units. Helper targets and paid jobs are f copies of the same fixed local
+inventory, so adding them preserves the comparison. This is a global bound
+within the declared no-idle, all-full contract, not a bound on other families.
+
+## Proof of B: the minimum-query simplex
+
+If there are at most n rank-one terms in (1), rank already forces exactly n.
+Writing U for their columns and V for their rows gives UV=I with both square.
+Then VU=I, contradicting the zero diagonal `v_i^T u_i=0`. Thus there are
+at least n+1 calls.
+
+At exactly n+1, U has n+1 columns and V has n+1 rows. VU is a rank-n projector
+of corank one. Write `VU=I+a b^T`. Its zero diagonal forces `a_i b_i=1` for
+every i. Over F2, both a and b are the all-one vector. Hence
+
+    v_i^T u_j = 0 if i=j, and 1 otherwise;
+    sum_i u_i = 0,  sum_i v_i = 0.                        (3)
+
+Every proper subset of at most n of either frame is independent.
+Index the queries 0,...,n. For an interior position s, put
+
+    k=n-s,  U_s=sum_{j>s}u_j,  V_s=sum_{j>s}v_j^T.
+
+Commutation (2), applied to u_s and v_s^T, forces the image of E_s to contain
+u_s,U_s and its row space to contain v_s^T,V_s. Both pairs are independent.
+Their pairing matrix is `[0 k; k 0]` over F2. If k is even it is zero, so no
+rank-two projector exists. If k is odd, the projector is uniquely
+
+    E_s = u_s V_s + U_s v_s^T.                            (4)
+
+In particular s must be odd, since n is even.
+
+Two distinct interior positions s<t cannot both be full. Formula (4) gives
+
+    E_s u_t=U_s,  E_t u_t=u_t,  E_t U_s=0.
+
+Their commutator is nonzero on u_t.
+
+If the initial position 0 and an interior s>1 were both full, their commuting
+projectors would force the image of E_0 to be
+`span(u_0,u_s+U_s)` and its row space to be
+`span(v_0^T,v_s^T+V_s)`. These two independent pairs have **all four pairings
+zero**, contradicting idempotence. Thus an initial full call can coexist with
+an interior full call only at s=1.
+
+Similarly, a terminal full call at n can coexist with an interior full call
+only at s=n-1. Otherwise its forced image is `span(u_n,U_s)` and its forced
+row space `span(v_n^T,V_s)`, again with all pairings zero.
+
+For n>=4, the single possible interior full call cannot be both at 1 and n-1.
+There are therefore at most two full calls: either both endpoints, or one
+interior and one endpoint. For n=2 this exception disappears and the familiar
+three-full-call controller is permitted, as it must be.
+
+For the retained BIT profile, with L=2p+1 calls and f full calls, independent
+stage degrees give first-order surplus
+
+    2*p*111 - 63*f - 111*(L-f) = 48*f - 111.
+
+At f<=2 this is at most -15. Here we can also exclude every interior concave
+moment, rather than relying only on that first-order calculation. The BIT
+helper profile is 439 jobs of rank 8, and its paid profile is
+`{1:1323,2:1342,3:79,4:44,5:102,6:11,7:19}`. Let P(t) be its paid moment.
+The n monomial degrees are nonnegative integers summing to 2f. Since n>=4
+and f<=2, concavity maximizes their main moment by putting degree one on
+2f fields and zero on the others. The full margin is consequently at most
+
+    f B(t)-111,  B(t)=661*8^t-P(t)-111.
+
+For every t in [0,1],
+
+    B'(t)/8^t >= 661*log(8)-sum_{r=2}^7 P_r log(r) > 0.
+
+The last strict inequality is the exact integer comparison
+`8^661 > product_{r=2}^7 r^(P_r)`, checked without floating point.
+Thus B(t)<=B(1)=48, and the margin is at most `48f-111<=-15`.
+
+## Verification and unproved extensions
+
+`global_check.py` checks the simplex pairings, forced-projector formulas,
+noncommutators and endpoint degeneracies through 32 pairs. It independently
+exhausts the two-coordinate nilpotents and their parity table, tests the n=2
+exception, and checks a real n=4/f=2 factored word that attains the full-call
+bound. The exact logarithmic-product inequality certifies the all-t BIT
+rejection. The original complete n=4 search supports, but does not replace, the
+written all-p proof.
+
+The proof uses characteristic two and constant binary boundaries. It does not
+reduce arbitrary complex dyadic operators modulo two. It also leaves mixed
+words with more than 2p+1 calls open. Repeated or dependent D_i, nonmonomial
+outputs, nonbinary boundaries and changed recursive suppliers are outside its
+scope. No kappa improvement is claimed.
diff --git a/research/productive-controller-basis-search/PROOF.md b/research/productive-controller-basis-search/PROOF.md
new file mode 100644
index 0000000000..6b207b71c0
--- /dev/null
+++ b/research/productive-controller-basis-search/PROOF.md
@@ -0,0 +1,98 @@
+# Five-call controllers after arbitrary binary changes of basis
+
+This is a finite binary-algebra exclusion, not a new supplier or a multiplication
+bound. The result concerns four main fields, five chronological query-bearing
+calls, independent fresh stage multipliers, no idle calls, and constant binary
+input/output changes of basis. It does not restrict longer words, other fields,
+other output contracts, or arbitrary native resynthesis.
+
+## Model and completeness of the alphabet
+
+Work over `F2[Q,D0,...,D4]/(Q^2-1)`. The `Ds` are independent commuting
+indeterminates; their squares are **not** identified with one. A thin call is
+`I+QN`, where `N` is a rank-one nilpotent binary 4-by-4 matrix. There are
+15 nonzero image vectors `u`, seven nonzero annihilating covectors `v` per
+vector, and hence 105 distinct `N=u v^T` with `v^T u=0`.
+
+A full call is
+
+    (I+(Ds+1)P)(I+QN),
+
+where `P` is a rank-two projector and `PN=NP=N`. These are precisely the
+simultaneous conjugates of a native call acting on two coordinate fields.
+On the image of P the nilpotent has its single size-two Jordan block; on the
+kernel of P it is zero. An adapted binary basis therefore gives the ordinary
+coordinate call. For each N there are 16 distinct P, giving 1,680 full calls.
+The verifier checks ranks, idempotence, nilpotence, and both commutations.
+
+Allowing arbitrary scalar changes between calls produces no larger class:
+push each intervening basis change to the right, conjugating the subsequent
+call. The remaining terminal basis change is absorbed in the allowed output
+boundary. A simultaneous global conjugation fixes the first full or thin call
+to the canonical coordinate call. This preserves the desired property and
+explains the symmetry reduction used in the enumeration.
+
+## What counts as success
+
+A successful operator has constant invertible L,R with
+
+    L M R = diag(Q*m0, Q*m1, Q*m2, Q*m3),
+
+where each mi is a monomial in the stage multipliers. The coefficient of every
+Q-even term must first vanish. This necessary cancellation is not sufficient.
+Write the remaining matrix as `sum_g g A_g`, using distinct Q-odd monomials g.
+It has the required two-sided constant factorization exactly when
+
+    sum_g rank(A_g) = 4.
+
+Necessity follows by taking the coefficients of the diagonal form. For
+sufficiency, choose rank factorizations `A_g=U_g V_g` and concatenate U_g and
+V_g. The total rank assumption makes their inner dimension four. Evaluation
+at Q=Ds=1 gives an invertible product UV, since every call is invertible at
+that evaluation. Thus U and V are both invertible and supply the required
+left/right bases. This is an exact test, not a numerical eigenvalue test.
+
+## Safe finite-field pruning
+
+The search evaluates Ds at the five nonzero elements 2,3,4,5,6 of
+`F16 = F2[x]/(x^4+x+1)` and retains Q formally as `E+QO`. Every full scale is
+invertible. A query changes the even part from E to `E+NO`, so its rank can
+fall by at most one. With r calls remaining, `rank(E)>r` safely rejects a
+prefix. Specialization can lower a rank, so this pruning can retain false
+positives but cannot remove a symbolic success.
+
+For the last query, zero even part requires `E=NO`. Then
+`O+NE=O`, because `N^2=0`. Invertibility of the final evaluated word implies
+O was already invertible. The last nilpotent is therefore uniquely determined:
+`N=E O^-1`. The search checks whether it is a binary nilpotent in the declared
+alphabet and enumerates all compatible full projectors when appropriate.
+It never guesses a last call from a numerical near-equality.
+
+Every surviving word is then replayed separately over the original polynomial
+ring, using integer bitsets for exact monomial supports and binary Gaussian
+elimination for coefficient ranks. No F16 evaluation enters that final test.
+The 12,480 evaluated survivors all pass exact Q-even cancellation. Every one
+has coefficient-rank sum at least six; none has sum four. The per-mask rank
+histograms, actual prefix counts and survivor hashes are in RESULT.json.
+
+## Resource connection and limits
+
+For five calls on four main fields, with f full calls and 5-f thin calls,
+the original complex local inventory would have formal rank surplus
+`4*112 - 64*f - 112*(5-f) = 48*f - 112` in a no-idle exact diagonal unit.
+The BIT inventory gives `48*f-111`. The enumerated masks have f=3,4,5;
+these include every mask with positive first-order surplus under those
+inventories. The other masks have negative first-order surplus. That
+observation is not asserted to exclude every possible interior moment sign.
+
+The search is a result over F2 and does not prove the analogous complex
+exclusion: reduction modulo two need not preserve arbitrary dyadic boundaries.
+A complex lift would require its own exact coefficient calculation and native
+phase/contact proof. The positive control is two disjoint three-call words,
+which **do** factor. Thus the alphabet is not being rejected by an impossible
+success condition. An actual five-call all-Q survivor demonstrates that
+checking only query cancellation, or setting all stage multipliers to one,
+would incorrectly promote a candidate.
+
+The result blocks a precise small route to removing the controller's largest
+bill. It establishes no all-length obstruction and gives no new kappa.
diff --git a/research/productive-controller-basis-search/README.md b/research/productive-controller-basis-search/README.md
new file mode 100644
index 0000000000..7a1ddf35d8
--- /dev/null
+++ b/research/productive-controller-basis-search/README.md
@@ -0,0 +1,75 @@
+# Global binary controller barriers and a complete finite search
+
+**Two scoped all-pair-count proofs; no new supplier or kappa.** Deleting the
+productive controller's idle work fails in two broad binary classes, even
+with arbitrary changes of basis between native calls:
+
+- If every call is full, at least three native calls per main pair are needed.
+  The complete concave moment cannot beat disjoint three-call units.
+- At the minimum 2p+1 query count, p>=2 permits at most two full native calls.
+  With the retained BIT inventory, the complete target-minus-paid moment is
+  at most **-15 for every exponent in [0,1]**.
+
+[GLOBAL-PROOF.md](GLOBAL-PROOF.md) gives the all-pair-count arguments. The first
+uses edge parity after simultaneous diagonalization of native projectors.
+The second uses the corank-one simplex forced by a shortest rank-one query
+factorization. An exact integer inequality certifies the uniform BIT moment
+rejection. The written proofs remain subject to independent review; finite
+checks do not constitute proof-assistant acceptance.
+
+A complete four-field, five-call search led to these proofs and supplies an
+independent finite check of the obstruction. The search includes 1,680 conjugated native maps and 105 thin-query maps,
+rather than only coordinate-pair calls or the existing path's bridge choices.
+It uses safe finite-field rank pruning, then a separate exact polynomial
+replay. All **12,480** surviving query cancellations fail the complete output
+factorization: their coefficient-rank sums are at least six instead of four.
+[PROOF.md](PROOF.md) defines the alphabet, proves the pruning/factorization
+criteria and states precisely what the finite exclusion covers.
+
+The motivating target is the productive-helper controller's large idle bill.
+The selected #4470 construction is conditional kappa 0.00302015. Its local
+helper/paid profiles and query-only interface are retained unchanged. This
+experiment changes the controller topology/basis instead of optimizing another
+fixed scalar contact. It is a negative checkpoint, not the requested larger K.
+
+## Reproduce
+
+Python 3.12+ and a C++17 compiler (`g++` or `clang++`) are required; no Python
+packages or network access are needed. All binaries and search streams live
+in a temporary directory. Run from the repository root:
+
+```sh
+python3 -B scripts/research_package.py --package research/productive-controller-basis-search
+```
+
+The hook recompiles and reruns all 16 masks and compares the exact receipt.
+It checks all gate relations, the global proof formulas through 32 pairs,
+a sharp two-native-call word, an independent numeric/symbolic transition
+comparison on 128 words, a working six-call example, a wrong-query control, a genuine five-call query cancellation that fails factorization,
+and the false positive obtained by collapsing all fresh multipliers to one.
+`--write` regenerates the receipt and is only an authoring option.
+
+This does not run the selected cold supplier replay or an outer ledger:
+no changed supplier passed the algebraic gate. There is no native admission,
+formal-kernel acceptance, independent human review or new exponent. The two
+global theorems have the explicit alphabet and output hypotheses above. In particular this binary exclusion is not silently
+transferred to arbitrary complex dyadic boundary changes.
+
+## Open next questions
+
+1. Can a mixed branching controller with **more than 2p+1 queries** admit
+   independent monomial outputs and a favorable complete invoice? That changes
+   a premise of the global minimum-query obstruction. First give the complete
+   word and test coefficient ranks; another shortest no-idle search is closed.
+2. Can a changed output interface retain a rank-five/six coefficient pencil at
+   a funded recovery price? Query cancellation alone earns no output credit.
+3. Can a native local family make multiple ports share a query line, or reduce
+   the copied-center debt? That changes a premise outside this enumeration.
+
+Credit Cinna Davis's #4440/#4470 controller/helper work, zxv's productive
+native/compiler construction, Jacob Alan Sussman's mixed-target recursion,
+and the retained BIT, Clifford, precision and outer contributors. The current
+#4602/#4603 diagnosis motivated changing topology rather than repeating a
+fixed-window rewrite; #4623 studies a different border endpoint and recovery
+model. New algebra, code and writing by Cinna Davis / 1337isnot1337 with
+substantial OpenAI Codex assistance. No subagents. Apache-2.0.
diff --git a/research/productive-controller-basis-search/RESULT.json b/research/productive-controller-basis-search/RESULT.json
new file mode 100644
index 0000000000..ef0ad30296
--- /dev/null
+++ b/research/productive-controller-basis-search/RESULT.json
@@ -0,0 +1,186 @@
+{
+  "cases": {
+    "11": {
+      "counts": {
+        "factored": 0,
+        "numeric_survivors": 192,
+        "symbolic_all_Q": 192
+      },
+      "prefix_census": "mask=11 hits=192 s0=0/0 s1=1/0 s2=1680/1168 s3=53760/51712 s4=3440640/3437568",
+      "rank_sum_histogram": {
+        "10": 72,
+        "6": 12,
+        "7": 12,
+        "8": 60,
+        "9": 36
+      },
+      "survivor_sha256": "d9905fb9f728925a4f3c0c6640f6fdc9d2a32c08b7cf80fbc87245268017cb34"
+    },
+    "13": {
+      "counts": {},
+      "prefix_census": "mask=13 hits=0 s0=0/0 s1=1/0 s2=105/73 s3=53760/48640 s4=8601600/8598528",
+      "rank_sum_histogram": {},
+      "survivor_sha256": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855"
+    },
+    "14": {
+      "counts": {},
+      "prefix_census": "mask=14 hits=0 s0=0/0 s1=1/0 s2=1680/1168 s3=860160/827392 s4=55050240/55047168",
+      "rank_sum_histogram": {},
+      "survivor_sha256": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855"
+    },
+    "15": {
+      "counts": {},
+      "prefix_census": "mask=15 hits=0 s0=0/0 s1=1/0 s2=1680/1168 s3=860160/827392 s4=55050240/55047168",
+      "rank_sum_histogram": {},
+      "survivor_sha256": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855"
+    },
+    "19": {
+      "counts": {
+        "factored": 0,
+        "numeric_survivors": 3072,
+        "symbolic_all_Q": 3072
+      },
+      "prefix_census": "mask=19 hits=3072 s0=0/0 s1=1/0 s2=1680/1168 s3=53760/51712 s4=215040/214848",
+      "rank_sum_histogram": {
+        "10": 792,
+        "6": 192,
+        "7": 336,
+        "8": 888,
+        "9": 864
+      },
+      "survivor_sha256": "8fa41e21d46c92def427bf289b2ffc625da45b82a9e4bef5a53eab084328ae94"
+    },
+    "21": {
+      "counts": {},
+      "prefix_census": "mask=21 hits=0 s0=0/0 s1=1/0 s2=105/73 s3=53760/48640 s4=537600/537408",
+      "rank_sum_histogram": {},
+      "survivor_sha256": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855"
+    },
+    "22": {
+      "counts": {},
+      "prefix_census": "mask=22 hits=0 s0=0/0 s1=1/0 s2=1680/1168 s3=860160/827392 s4=3440640/3440448",
+      "rank_sum_histogram": {},
+      "survivor_sha256": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855"
+    },
+    "23": {
+      "counts": {},
+      "prefix_census": "mask=23 hits=0 s0=0/0 s1=1/0 s2=1680/1168 s3=860160/827392 s4=3440640/3440448",
+      "rank_sum_histogram": {},
+      "survivor_sha256": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855"
+    },
+    "25": {
+      "counts": {
+        "factored": 0,
+        "numeric_survivors": 3072,
+        "symbolic_all_Q": 3072
+      },
+      "prefix_census": "mask=25 hits=3072 s0=0/0 s1=1/0 s2=105/73 s3=3360/3040 s4=537600/534528",
+      "rank_sum_histogram": {
+        "10": 792,
+        "6": 192,
+        "7": 336,
+        "8": 888,
+        "9": 864
+      },
+      "survivor_sha256": "7d497755d297d162fbe9b26dad36e9dd12560fe172d28a4a6ff01f82dda7f6cb"
+    },
+    "26": {
+      "counts": {
+        "factored": 0,
+        "numeric_survivors": 3072,
+        "symbolic_all_Q": 3072
+      },
+      "prefix_census": "mask=26 hits=3072 s0=0/0 s1=1/0 s2=1680/1168 s3=53760/51712 s4=3440640/3437568",
+      "rank_sum_histogram": {
+        "10": 1152,
+        "6": 192,
+        "7": 192,
+        "8": 960,
+        "9": 576
+      },
+      "survivor_sha256": "13dfc7fad3d09e6adbc99acb0b82e395a19b98c334bc5536a6fb90874b6c2cd5"
+    },
+    "27": {
+      "counts": {
+        "factored": 0,
+        "numeric_survivors": 3072,
+        "symbolic_all_Q": 3072
+      },
+      "prefix_census": "mask=27 hits=3072 s0=0/0 s1=1/0 s2=1680/1168 s3=53760/51712 s4=3440640/3437568",
+      "rank_sum_histogram": {
+        "10": 288,
+        "11": 372,
+        "12": 216,
+        "13": 576,
+        "14": 360,
+        "15": 324,
+        "16": 324,
+        "17": 216,
+        "18": 108,
+        "6": 12,
+        "7": 24,
+        "8": 132,
+        "9": 120
+      },
+      "survivor_sha256": "3bb8a6eb111bc08ed2035e5f7f185f67dd6dbe0f2f46fcb4ce165c417d8b1d4d"
+    },
+    "28": {
+      "counts": {},
+      "prefix_census": "mask=28 hits=0 s0=0/0 s1=1/0 s2=105/73 s3=53760/48640 s4=8601600/8598528",
+      "rank_sum_histogram": {},
+      "survivor_sha256": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855"
+    },
+    "29": {
+      "counts": {},
+      "prefix_census": "mask=29 hits=0 s0=0/0 s1=1/0 s2=105/73 s3=53760/48640 s4=8601600/8598528",
+      "rank_sum_histogram": {},
+      "survivor_sha256": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855"
+    },
+    "30": {
+      "counts": {},
+      "prefix_census": "mask=30 hits=0 s0=0/0 s1=1/0 s2=1680/1168 s3=860160/827392 s4=55050240/55047168",
+      "rank_sum_histogram": {},
+      "survivor_sha256": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855"
+    },
+    "31": {
+      "counts": {},
+      "prefix_census": "mask=31 hits=0 s0=0/0 s1=1/0 s2=1680/1168 s3=860160/827392 s4=55050240/55047168",
+      "rank_sum_histogram": {},
+      "survivor_sha256": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855"
+    },
+    "7": {
+      "counts": {},
+      "prefix_census": "mask=7 hits=0 s0=0/0 s1=1/0 s2=1680/1168 s3=860160/827392 s4=3440640/3440448",
+      "rank_sum_histogram": {},
+      "survivor_sha256": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855"
+    }
+  },
+  "controls": {
+    "collapsed_stage_false_positive": true,
+    "five_call_all_Q_rank_sum": 6,
+    "gate_relations_checked": 1680,
+    "global_proof_controls": {
+      "all_full_edge_parity_patterns": 8,
+      "bit_all_concave_moments_upper": -15,
+      "endpoint_obstructions": 992,
+      "formal_kernel": false,
+      "largest_main_field_count": 64,
+      "log_product_inequality_exact": true,
+      "minimum_query_native_bound_sharp": true,
+      "odd_projectors": 528,
+      "simplex_pairings": 47904,
+      "status": "PASS_GLOBAL_BINARY_CONTROLLER_PROOF_CONTROLS"
+    },
+    "independent_transition_words": 128,
+    "positive_six_call_rank_sum": 4,
+    "wrong_query_rejected": true
+  },
+  "new_kappa": null,
+  "schema": "productive-controller-basis-search/1",
+  "status": "PASS_FINITE_FIVE_CALL_NO_IDLE_BINARY_SEARCH_NO_KAPPA",
+  "totals": {
+    "factored": 0,
+    "numeric_survivors": 12480,
+    "symbolic_all_Q": 12480
+  }
+}
diff --git a/research/productive-controller-basis-search/SOURCES.json b/research/productive-controller-basis-search/SOURCES.json
new file mode 100644
index 0000000000..d19bef3fd1
--- /dev/null
+++ b/research/productive-controller-basis-search/SOURCES.json
@@ -0,0 +1,30 @@
+{
+  "schema_version": 1,
+  "base_commit": "b58ad9ef4d4e861b0eaa5dba41742bdc072dca51",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395",
+      "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602",
+      "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72"
+    },
+    {
+      "path": "research/joint-helper-lattice/PROOF.md",
+      "usage": "input",
+      "git_blob": "e41106031da41fade7a7419c17a32c1bd9aa103b",
+      "sha256": "43ef4251cc300f1b18cbe8cdb060f96f95748e6797d2478b4c04b79a8373ef91"
+    },
+    {
+      "path": "research/query-thinned-controllers/controller.py",
+      "usage": "input",
+      "git_blob": "d4557e08cfb9fe57cc1ae4024705a72dc95f3583",
+      "sha256": "8b462d660487b1be4940357c4c7522967b1bfaede3c02b1c66109b85acae0fd2"
+    }
+  ]
+}
diff --git a/research/productive-controller-basis-search/TASK.json b/research/productive-controller-basis-search/TASK.json
new file mode 100644
index 0000000000..244c816ac7
--- /dev/null
+++ b/research/productive-controller-basis-search/TASK.json
@@ -0,0 +1,66 @@
+{
+  "schema_version": 1,
+  "task_id": "complex-new-helper-inventory",
+  "priority_revision": 7,
+  "base_commit": "b58ad9ef4d4e861b0eaa5dba41742bdc072dca51",
+  "original_card": {
+    "id": "complex-new-helper-inventory",
+    "question": "Can a new local cost interface change the deficit-to-recursive-cost ratio beyond current packing?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "research/complex-local-word-ceiling/README.md",
+      "research/heterogeneous-owner-assembly/README.md",
+      "certificates/selected-result.json",
+      "research/selected-k8-unrestricted-ends/README.md"
+    ],
+    "methods": [
+      "Propose a changed helper inventory and derive an optimistic exact moment.",
+      "Design a small completed instance and independently verify its endpoint and rank bill."
+    ],
+    "acceptance_gate": "A new physically realizable contract outside the frozen catalogue whose per-call profile, screened with ceiling.ceiling(), beats the selected word's packing ceiling; a lower cap does not establish identical circuitry or order attainable optima, and is insufficient to pass the stronger-budget target under this model. 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/complex-local-word-ceiling/verify.py"
+      ],
+      "expected": "PASS_COMPLEX_LOCAL_WORD_CEILING",
+      "inspect": "Read the selected word's per-call local profile, its packing ceiling and the lever table; run levers.py for the ideal budget of the lever you target.",
+      "scope": "Positive control and planning budget only; this is not a new construction or full cold replay."
+    },
+    "first_experiment": "Before any synthesis, write the candidate per-call local profile (and centre charge / unpaid coordinates if changed) and screen it with ceiling.ceiling(); reject it if even the ideal ceiling does not beat the selected word's by your stated margin.",
+    "bottleneck_link": "Packing of the selected word is capped at +0.87% (ceiling model); only a lower local excess spend or a changed coverage law raises the cap.",
+    "allowed_variations": [
+      "Narrow to one changed boundary or helper type with explicit counts.",
+      "If the coverage law, template or guard changes, derive an applicable fully charged replacement bound instead of applying the incumbent ceiling outside its scope."
+    ],
+    "scope_change_triggers": [
+      "Mixing only providers already inside the pinned catalogue.",
+      "Only changing helper terminal subspaces and monotone frames within the fixed scalar word, entrances and cleanup contract already covered by #1995/#2013.",
+      "Continuing a partial cost improvement while leaving the same unpriced consumer, restoration or central-readout obligation unresolved; refresh the family expansion decision first. Local product-retiming evidence has a narrow scope and is not a ban on changed graphs or contracts."
+    ],
+    "overlap_terms": [
+      "helper inventory",
+      "heterogeneous-owner",
+      "mutable leaver"
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Prove two all-pair-count binary no-idle controller obstructions and exhaust the five-call/four-field change-of-basis model.",
+  "scope_change_reason": "Explicit user request for a bottleneck breakthrough and frequent verified checkpoints; the older card predates productive-helper selection.",
+  "bottleneck_link": "Two global mechanism barriers separate closed all-full and shortest-query no-idle classes from mixed longer-query designs that could still change the large idle bill.",
+  "budget_minutes": 60,
+  "stop_rule": "Exhaust the declared finite class, reject all unpriced or unfactored endpoints, publish a scoped checkpoint, then continue larger mechanisms.",
+  "outcome": "negative-result",
+  "evidence": "GLOBAL-PROOF.md, PROOF.md, RESULT.json, global_check.py, search.cpp, algebra.py, verify.py",
+  "author": "Cinna Davis / 1337isnot1337, with substantial OpenAI Codex assistance",
+  "ai_assistance": "Substantial OpenAI Codex assistance in research, programming and writing; no subagents.",
+  "open_questions": [
+    {
+      "question": "Can a mixed branching controller with more than 2p+1 queries beat the complete current invoice?",
+      "why_it_matters": "This is a controller-level mechanism for a larger K on both suppliers.",
+      "first_step": "Define an exact larger finite word and test all polynomial coefficient ranks before pricing.",
+      "blocked_by": "No admitted changed word; all-full and minimum-query no-idle models are now excluded under the stated binary hypotheses."
+    }
+  ]
+}
diff --git a/research/productive-controller-basis-search/VERIFY.json b/research/productive-controller-basis-search/VERIFY.json
new file mode 100644
index 0000000000..c7c537e1c4
--- /dev/null
+++ b/research/productive-controller-basis-search/VERIFY.json
@@ -0,0 +1,21 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/joint-helper-lattice/PROOF.md",
+    "research/query-thinned-controllers/controller.py"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 180,
+      "checks": "All-pair-count proof controls, sharp native-bound word, exact all-t BIT inequality, complete binary five-call census, independent polynomial/numeric transition checks"
+    }
+  ]
+}
diff --git a/research/productive-controller-basis-search/algebra.py b/research/productive-controller-basis-search/algebra.py
new file mode 100644
index 0000000000..2f0d4f290c
--- /dev/null
+++ b/research/productive-controller-basis-search/algebra.py
@@ -0,0 +1,110 @@
+"""Literal GF(2) polynomial matrices, independently of the GF(16) search.
+
+Apache-2.0. Cinna Davis, with substantial OpenAI Codex assistance.
+"""
+from collections import Counter
+
+EVEN = sum(1 << i for i in range(0, 256, 2))
+
+
+def query(poly):
+    """Multiply by the formal involution Q, without setting Q = 1."""
+    return ((poly & EVEN) << 1) | ((poly & (EVEN << 1)) >> 1)
+
+
+def rank(rows):
+    basis = {}
+    for value in rows:
+        while value:
+            pivot = value.bit_length() - 1
+            if pivot not in basis:
+                basis[pivot] = value
+                break
+            value ^= basis[pivot]
+    return len(basis)
+
+
+def gate_inventory():
+    """All rank-one nilpotents and their rank-two projector extensions."""
+    full, thin = [], []
+    for u in range(1, 16):
+        for v in range(1, 16):
+            if (u & v).bit_count() % 2:
+                continue
+            nilpotent = tuple(v if u >> i & 1 else 0 for i in range(4))
+            thin.append(((0,) * 4, nilpotent))
+            seen = set()
+            for a in range(1, 16):
+                if not (v & a).bit_count() % 2:
+                    continue
+                for b in range(1, 16):
+                    if not (u & b).bit_count() % 2 or (a & b).bit_count() % 2:
+                        continue
+                    projector = tuple((b if u >> i & 1 else 0) ^
+                                      (v if a >> i & 1 else 0) for i in range(4))
+                    if projector not in seen:
+                        seen.add(projector)
+                        full.append((projector, nilpotent))
+    return full, thin
+
+
+FULL, THIN = gate_inventory()
+
+
+def identity():
+    return [[int(i == j) for j in range(4)] for i in range(4)]
+
+
+def literal(mask, ids):
+    """Each bit is a monomial Q^q product(D_s); no D is specialized."""
+    matrix = identity()
+    for stage, gate_id in enumerate(ids):
+        thick = bool(mask >> stage & 1)
+        projector, nilpotent = (FULL if thick else THIN)[gate_id]
+        sums = [[0] * 4 for _ in range(16)]
+        for subset in range(1, 16):
+            low = (subset & -subset).bit_length() - 1
+            sums[subset] = [a ^ b for a, b in
+                            zip(sums[subset & (subset - 1)], matrix[low])]
+        changed = [row[:] for row in matrix]
+        for i in range(4):
+            for j in range(4):
+                p = sums[projector[i]][j]
+                n = query(sums[nilpotent[i]][j])
+                if thick:
+                    shift = 1 << (stage + 1)
+                    changed[i][j] ^= p ^ (p << shift) ^ (n << shift)
+                else:
+                    changed[i][j] ^= n
+        matrix = changed
+    return matrix
+
+
+def coefficients(matrix):
+    result = {}
+    groups = {g for row in matrix for poly in row
+              for g in range(poly.bit_length()) if poly >> g & 1}
+    for g in groups:
+        result[g] = [sum(((matrix[i][j] >> g) & 1) << j for j in range(4))
+                     for i in range(4)]
+    return result
+
+
+def stats(matrix):
+    coeff = coefficients(matrix)
+    return {
+        'central_query_on_every_output': all(g & 1 for g in coeff),
+        'coefficient_rank_sum': sum(rank(rows) for rows in coeff.values()),
+        'ranks': dict(sorted((g, rank(rows)) for g, rows in coeff.items())),
+    }
+
+
+def elementary(source, destination):
+    nilpotent = tuple((1 << source) if i == destination else 0 for i in range(4))
+    projector = tuple((1 << i) if i in (source, destination) else 0 for i in range(4))
+    return FULL.index((projector, nilpotent))
+
+
+def multiply_binary(a, b):
+    return [sum(((sum(((row >> k) & 1) * ((b[k] >> j) & 1)
+                       for k in range(4))) % 2) << j for j in range(4)) for row in a]
diff --git a/research/productive-controller-basis-search/global_check.py b/research/productive-controller-basis-search/global_check.py
new file mode 100644
index 0000000000..9bca225f54
--- /dev/null
+++ b/research/productive-controller-basis-search/global_check.py
@@ -0,0 +1,123 @@
+"""Finite controls for the written all-p proofs; not a formal proof kernel.
+
+Apache-2.0. Cinna Davis, with substantial OpenAI Codex assistance.
+"""
+import algebra as A
+import ast
+from pathlib import Path
+
+
+def need(ok, message):
+    if not ok:
+        raise ValueError(message)
+
+
+def dot(row, column):
+    return (row & column).bit_count() % 2
+
+
+def outer(column, row, n):
+    return [row if column >> i & 1 else 0 for i in range(n)]
+
+
+def apply(matrix, column):
+    return sum(dot(row, column) << i for i, row in enumerate(matrix))
+
+
+def check():
+    paid = {1: 1323, 2: 1342, 3: 79, 4: 44, 5: 102, 6: 11, 7: 19}
+    source = Path(__file__).resolve().parents[1] / 'query-thinned-controllers/controller.py'
+    literals = []
+    for node in ast.walk(ast.parse(source.read_text())):
+        if isinstance(node, ast.Assign):
+            try:
+                literals.append(ast.literal_eval(node.value))
+            except (ValueError, TypeError):
+                pass
+    need(paid in literals and {8: 439} in literals, 'Actual pinned BIT inventory')
+    need(sum(r*c for r, c in paid.items()) - 439*8 - 2*111*7 == 63,
+         'Owned center debt is included')
+    product = 1
+    for r, count in paid.items():
+        product *= r**count
+    need(8**661 > product, 'Exact uniform positivity of B derivative')
+    need(661*8 - sum(r*c for r, c in paid.items()) - 111 == 48,
+         'Exact endpoint of all-t BIT bound')
+    # Independently enumerate every nonzero rank-one nilpotent on two coordinates.
+    nilpotents = set()
+    for u in range(1, 4):
+        for v in range(1, 4):
+            if not dot(v, u):
+                nilpotents.add(tuple(outer(u, v, 2)))
+    need(nilpotents == {(2, 0), (0, 1), (3, 3)}, 'Three edge types')
+    alphabet = sorted(nilpotents)
+    for mask in range(8):
+        rows = [0, 0]
+        for i, item in enumerate(alphabet):
+            if mask >> i & 1:
+                rows = [x ^ y for x, y in zip(rows, item)]
+        zero_offdiagonal = not (rows[0] & 2 or rows[1] & 1)
+        need(zero_offdiagonal == (mask in (0, 7)), 'Complete edge parity table')
+        if mask == 7:
+            need(rows == [1, 2], 'Three calls contribute identity on their edge')
+    pair_cases = interior_cases = endpoint_cases = 0
+    for n in range(2, 65, 2):
+        ones = (1 << n) - 1
+        u = [1 << i for i in range(n)] + [ones]
+        v = [ones ^ (1 << i) for i in range(n)] + [ones]
+        need(all(dot(v[i], u[j]) == int(i != j)
+                 for i in range(n+1) for j in range(n+1)), 'Simplex frame pairings')
+        pair_cases += (n+1)**2
+        projectors, sums_u, sums_v = {}, {}, {}
+        for s in range(1, n):
+            us = vs = 0
+            for j in range(s+1, n+1):
+                us ^= u[j]
+                vs ^= v[j]
+            sums_u[s], sums_v[s] = us, vs
+            k = n-s
+            gram = [dot(v[s], u[s]), dot(v[s], us), dot(vs, u[s]), dot(vs, us)]
+            need(gram == [0, k % 2, k % 2, 0], 'Forced image/row-space pairing')
+            if not k % 2:
+                continue
+            p = [a ^ b for a, b in zip(outer(u[s], vs, n), outer(us, v[s], n))]
+            need(apply(p, u[s]) == u[s] and apply(p, us) == us,
+                 'Odd interior projector is rank two and idempotent')
+            projectors[s] = p
+            interior_cases += 1
+            if s > 1:
+                w, z = u[s] ^ us, v[s] ^ vs
+                need(w not in (0, u[0]) and z not in (0, v[0]), 'Initial forced pairs independent')
+                need(not any(dot(a, b) for a in (v[0], z) for b in (u[0], w)),
+                     'Initial endpoint pairing obstruction')
+                endpoint_cases += 1
+            if s < n-1:
+                need(us not in (0, u[n]) and vs not in (0, v[n]), 'Final forced pairs independent')
+                need(not any(dot(a, b) for a in (v[n], vs) for b in (u[n], us)),
+                     'Final endpoint pairing obstruction')
+                endpoint_cases += 1
+        for s in projectors:
+            for t in projectors:
+                if s >= t:
+                    continue
+                ps, pt = projectors[s], projectors[t]
+                need(apply(ps, u[t]) == sums_u[s], 'Earlier projector response')
+                need(apply(pt, sums_u[s]) == 0 and apply(pt, u[t]) == u[t],
+                     'Distinct interior projectors do not commute')
+        if n == 2:
+            need(projectors[1] == [1, 2], 'Three-call n=2 exception remains valid')
+    # A two-native-call/five-query word saturates the all-p native upper bound.
+    sharp = A.stats(A.literal(24, [7, 0, 39, 832, 384]))
+    need(sharp['central_query_on_every_output'] and sharp['coefficient_rank_sum'] == 4,
+         'Actual sharp n=4/f=2 word factors')
+    return {'status': 'PASS_GLOBAL_BINARY_CONTROLLER_PROOF_CONTROLS',
+            'largest_main_field_count': 64, 'simplex_pairings': pair_cases,
+            'odd_projectors': interior_cases, 'endpoint_obstructions': endpoint_cases,
+            'all_full_edge_parity_patterns': 8, 'minimum_query_native_bound_sharp': True,
+            'bit_all_concave_moments_upper': -15,
+            'log_product_inequality_exact': True, 'formal_kernel': False}
+
+
+if __name__ == '__main__':
+    import json
+    print(json.dumps(check(), sort_keys=True))
diff --git a/research/productive-controller-basis-search/search.cpp b/research/productive-controller-basis-search/search.cpp
new file mode 100644
index 0000000000..84a903afae
--- /dev/null
+++ b/research/productive-controller-basis-search/search.cpp
@@ -0,0 +1,205 @@
+// Exact GF(16) pruning for the finite class in PROOF.md.
+// Apache-2.0. Cinna Davis, with substantial OpenAI Codex assistance.
+#include <array>
+#include <cstdint>
+#include <iostream>
+#include <map>
+#include <string>
+#include <vector>
+
+// Four field elements, packed into one row as four nibbles.
+using Matrix = std::array<uint16_t, 4>;
+struct State { Matrix even{}, odd{}; };
+struct Gate { std::array<int, 4> projector, nilpotent; };
+uint16_t times[16][65536];
+int product[16][16], inverse_element[16];
+std::vector<Gate> full, thin;
+std::vector<int> program;
+uint64_t nodes[6]{}, pruned[6]{}, hits = 0;
+int mask = 27;
+
+int rank(Matrix a) {
+    int r = 0;
+    for (int c = 0; c < 4; ++c) {
+        int j = r;
+        while (j < 4 && !((a[j] >> (4*c)) & 15)) ++j;
+        if (j == 4) continue;
+        std::swap(a[j], a[r]);
+        a[r] = times[inverse_element[(a[r] >> (4*c)) & 15]][a[r]];
+        for (j = r+1; j < 4; ++j) {
+            int q = (a[j] >> (4*c)) & 15;
+            if (q) a[j] ^= times[q][a[r]];
+        }
+        if (++r == 4) break;
+    }
+    return r;
+}
+
+Matrix inverse(Matrix a) {
+    Matrix b{};
+    for (int i = 0; i < 4; ++i) b[i] = 1 << (4*i);
+    for (int c = 0; c < 4; ++c) {
+        int j = c;
+        while (j < 4 && !((a[j] >> (4*c)) & 15)) ++j;
+        if (j == 4) return {};
+        std::swap(a[j], a[c]);
+        std::swap(b[j], b[c]);
+        int x = inverse_element[(a[c] >> (4*c)) & 15];
+        a[c] = times[x][a[c]];
+        b[c] = times[x][b[c]];
+        for (j = 0; j < 4; ++j) if (j != c) {
+            int q = (a[j] >> (4*c)) & 15;
+            a[j] ^= times[q][a[c]];
+            b[j] ^= times[q][b[c]];
+        }
+    }
+    return b;
+}
+
+std::array<uint16_t, 16> subset_sums(Matrix a) {
+    std::array<uint16_t, 16> sums{};
+    for (int i = 1; i < 16; ++i)
+        sums[i] = sums[i & (i-1)] ^ a[__builtin_ctz(i)];
+    return sums;
+}
+
+State apply(State state, const Gate &gate, int d) {
+    auto even = subset_sums(state.even), odd = subset_sums(state.odd);
+    State next;
+    for (int i = 0; i < 4; ++i) {
+        next.even[i] = state.even[i] ^ times[d ^ 1][even[gate.projector[i]]]
+                                      ^ times[d][odd[gate.nilpotent[i]]];
+        next.odd[i] = state.odd[i] ^ times[d ^ 1][odd[gate.projector[i]]]
+                                    ^ times[d][even[gate.nilpotent[i]]];
+    }
+    return next;
+}
+
+std::array<int, 4> forced_last_nilpotent(State state) {
+    auto oi = inverse(state.odd);
+    if (oi == Matrix{}) return {};
+    std::array<int, 4> n{};
+    for (int i = 0; i < 4; ++i) {
+        uint16_t row = 0;
+        for (int k = 0; k < 4; ++k)
+            row ^= times[(state.even[i] >> (4*k)) & 15][oi[k]];
+        for (int j = 0; j < 4; ++j) {
+            int a = (row >> (4*j)) & 15;
+            if (a > 1) return {}; // The actual call must be binary.
+            n[i] |= a << j;
+        }
+    }
+    return n;
+}
+
+void search(State state, int step) {
+    ++nodes[step];
+    int remaining = 5-step;
+    if (remaining < 4 && rank(state.even) > remaining) {
+        ++pruned[step];
+        return;
+    }
+    if (step == 4) {
+        auto n = forced_last_nilpotent(state);
+        if (n == std::array<int, 4>{}) return;
+        const auto &alphabet = (mask >> 4 & 1) ? full : thin;
+        for (int i = 0; i < int(alphabet.size()); ++i) {
+            if (alphabet[i].nilpotent != n) continue;
+            auto next = apply(state, alphabet[i], (mask >> 4 & 1) ? 6 : 1);
+            if (next.even != Matrix{}) continue;
+            ++hits;
+            std::cout << "HIT " << mask;
+            for (int g : program) std::cout << " " << g;
+            std::cout << " " << i << "\n";
+        }
+        return;
+    }
+    const auto &alphabet = (mask >> step & 1) ? full : thin;
+    int d = (mask >> step & 1) ? step+2 : 1;
+    // Each recursive edge is an exact matrix operation in the finite field.
+    for (int i = 0; i < int(alphabet.size()); ++i) {
+        program.push_back(i);
+        search(apply(state, alphabet[i], d), step+1);
+        program.pop_back();
+    }
+}
+
+void initialize() {
+    for (int a = 0; a < 16; ++a) for (int b = 0; b < 16; ++b) {
+        int value = 0;
+        for (int x = a, y = b; y; y >>= 1) {
+            if (y & 1) value ^= x;
+            x <<= 1;
+            if (x & 16) x ^= 19; // x^4+x+1
+        }
+        product[a][b] = value;
+    }
+    for (int a = 1; a < 16; ++a) for (int b = 1; b < 16; ++b)
+        if (product[a][b] == 1) inverse_element[a] = b;
+    for (int d = 0; d < 16; ++d) for (int x = 0; x < 65536; ++x) {
+        int value = 0;
+        for (int k = 0; k < 4; ++k)
+            value |= product[d][(x >> (4*k)) & 15] << (4*k);
+        times[d][x] = value;
+    }
+    for (int u = 1; u < 16; ++u) for (int v = 1; v < 16; ++v) {
+        if (__builtin_popcount(u & v) & 1) continue;
+        Gate gate{};
+        for (int i = 0; i < 4; ++i) if (u >> i & 1) gate.nilpotent[i] = v;
+        thin.push_back(gate);
+        std::map<std::array<int, 4>, bool> seen;
+        for (int a = 1; a < 16; ++a) if (__builtin_popcount(v & a) & 1)
+            for (int b = 1; b < 16; ++b) {
+                if (!(__builtin_popcount(u & b) & 1) ||
+                    (__builtin_popcount(a & b) & 1)) continue;
+                for (int i = 0; i < 4; ++i)
+                    gate.projector[i] = ((u >> i & 1) ? b : 0) ^
+                                        ((a >> i & 1) ? v : 0);
+                if (!seen[gate.projector]) {
+                    seen[gate.projector] = true;
+                    full.push_back(gate);
+                }
+            }
+    }
+}
+
+void traces() {
+    // No pruning: separately check transitions on 128 deterministic words.
+    for (int trial = 0; trial < 128; ++trial) {
+        int word_mask = (trial*13+7) & 31;
+        State state;
+        for (int i = 0; i < 4; ++i) state.even[i] = 1 << (4*i);
+        std::cout << "TRACE " << word_mask;
+        for (int stage = 0; stage < 5; ++stage) {
+            const auto &alphabet = (word_mask >> stage & 1) ? full : thin;
+            int g = (137*trial+37*stage) % alphabet.size();
+            std::cout << " " << g;
+            state = apply(state, alphabet[g], (word_mask >> stage & 1) ? stage+2 : 1);
+        }
+        for (auto row : state.even) std::cout << " " << row;
+        for (auto row : state.odd) std::cout << " " << row;
+        std::cout << "\n";
+    }
+}
+
+int main(int argc, char **argv) {
+    initialize();
+    if (argc > 1 && std::string(argv[1]) == "trace") { traces(); return 0; }
+    if (argc > 1) mask = std::stoi(argv[1]);
+    std::cerr << "full=" << full.size() << " thin=" << thin.size() << "\n";
+    State state;
+    for (int i = 0; i < 4; ++i) state.even[i] = 1 << (4*i);
+    const auto &alphabet = (mask & 1) ? full : thin;
+    for (int i = 0; i < int(alphabet.size()); ++i) {
+        if (alphabet[i].nilpotent != std::array<int, 4>{0, 1, 0, 0}) continue;
+        if ((mask & 1) && alphabet[i].projector != std::array<int, 4>{1, 2, 0, 0})
+            continue;
+        program.push_back(i);
+        search(apply(state, alphabet[i], (mask & 1) ? 2 : 1), 1);
+        break;
+    }
+    std::cerr << "mask=" << mask << " hits=" << hits;
+    for (int i = 0; i < 5; ++i)
+        std::cerr << " s" << i << "=" << nodes[i] << "/" << pruned[i];
+    std::cerr << "\n";
+}
diff --git a/research/productive-controller-basis-search/verify.py b/research/productive-controller-basis-search/verify.py
new file mode 100644
index 0000000000..3e53c37a36
--- /dev/null
+++ b/research/productive-controller-basis-search/verify.py
@@ -0,0 +1,163 @@
+#!/usr/bin/env python3
+"""Reproduce the complete finite search, then replay survivors symbolically."""
+import argparse
+from collections import Counter
+from hashlib import sha256
+import json
+from pathlib import Path
+import shutil
+import subprocess
+import tempfile
+
+import algebra as A
+import global_check
+
+HERE = Path(__file__).resolve().parent
+ROOT = HERE.parents[1]
+
+
+def need(condition, message):
+    if not condition:
+        raise ValueError(message)
+
+
+def authenticate():
+    pins = json.loads((HERE / 'SOURCES.json').read_text())
+    for row in pins['files']:
+        if row['usage'] == 'input':
+            need(sha256((ROOT / row['path']).read_bytes()).hexdigest() == row['sha256'],
+                 'Changed source input: ' + row['path'])
+
+
+def controls():
+    need(len(A.FULL) == 1680 and len(A.THIN) == 105, 'Complete gate inventories')
+    for p, n in A.FULL:
+        need(A.rank(p) == 2 and A.rank(n) == 1, 'Actual operator ranks')
+        need(A.multiply_binary(p, p) == list(p), 'Projector idempotence')
+        need(A.multiply_binary(n, n) == [0] * 4, 'Query nilpotence')
+        need(A.multiply_binary(p, n) == A.multiply_binary(n, p) == list(n),
+             'Full multiplier commutes with its query')
+    ids = [A.elementary(0, 1), A.elementary(1, 0), A.elementary(0, 1),
+           A.elementary(2, 3), A.elementary(3, 2), A.elementary(2, 3)]
+    positive = A.literal(63, ids)
+    positive_stats = A.stats(positive)
+    need(positive_stats['central_query_on_every_output'] and
+         positive_stats['coefficient_rank_sum'] == 4,
+         'Two independent three-call controllers factor')
+    broken = A.literal(63, ids[:2] + [ids[1]] + ids[3:])
+    need(not A.stats(broken)['central_query_on_every_output'],
+         'Wrong query orientation is rejected')
+    # Four native calls plus one thin call: cancellation alone is insufficient.
+    near = A.literal(27, [112, 0, 39, 832, 384])
+    near_stats = A.stats(near)
+    need(near_stats['central_query_on_every_output'] and
+         near_stats['coefficient_rank_sum'] == 6,
+         'A genuine all-Q controller still fails independent Fourier outputs')
+    # Setting all D=1 hides this failure; preserve them as distinct variables.
+    specialized = [[int(x.bit_count() % 2) for x in row] for row in near]
+    need(A.rank([sum(x << j for j, x in enumerate(row)) for row in specialized]) == 4,
+         'Collapsed-stage false positive is demonstrated')
+    return {'positive_six_call_rank_sum': 4, 'wrong_query_rejected': True,
+            'five_call_all_Q_rank_sum': 6, 'collapsed_stage_false_positive': True,
+            'gate_relations_checked': 1680}
+
+
+def check_numeric_transitions(executable):
+    """Compare C++ updates with evaluation of distinct symbolic monomials."""
+    def multiply(a, b):
+        value = 0
+        while b:
+            if b & 1:
+                value ^= a
+            b >>= 1
+            a <<= 1
+            if a & 16:
+                a ^= 19
+        return value
+
+    result = subprocess.run([str(executable), 'trace'], check=True,
+                            capture_output=True, text=True, timeout=5)
+    count = 0
+    for line in result.stdout.splitlines():
+        args = line.split()
+        need(args[0] == 'TRACE' and len(args) == 15, 'Numeric trace format')
+        mask, *values = map(int, args[1:])
+        ids, expected = values[:5], values[5:]
+        matrix = A.literal(mask, ids)
+        even, odd = [0] * 4, [0] * 4
+        for i, row in enumerate(matrix):
+            for j, poly in enumerate(row):
+                for g in range(poly.bit_length()):
+                    if not poly >> g & 1:
+                        continue
+                    value = 1
+                    for stage in range(5):
+                        if g >> (stage + 1) & 1:
+                            value = multiply(value, stage + 2)
+                    (odd if g & 1 else even)[i] ^= value << (4*j)
+        need(even + odd == expected, 'Independent polynomial/numeric transition check')
+        count += 1
+    need(count == 128, 'All numeric traces checked')
+    return count
+
+
+def run():
+    authenticate()
+    checked = controls()
+    checked['global_proof_controls'] = global_check.check()
+    compiler = shutil.which('g++') or shutil.which('clang++')
+    need(compiler is not None, 'A C++17 compiler is required')
+    cases, all_counts = {}, Counter()
+    with tempfile.TemporaryDirectory(prefix='controller-basis-') as tmp:
+        executable = Path(tmp) / 'search'
+        subprocess.run([compiler, '-O2', '-std=c++17', str(HERE / 'search.cpp'),
+                        '-o', str(executable)], check=True, capture_output=True, timeout=30)
+        checked['independent_transition_words'] = check_numeric_transitions(executable)
+        for mask in range(32):
+            if mask.bit_count() < 3:
+                continue
+            result = subprocess.run([str(executable), str(mask)], check=True,
+                                    capture_output=True, text=True, timeout=30)
+            counts, ranks, digest = Counter(), Counter(), sha256()
+            for line in result.stdout.splitlines():
+                args = line.split()
+                need(args[0] == 'HIT' and int(args[1]) == mask, 'Search record format')
+                ids = list(map(int, args[2:]))
+                need(len(ids) == 5, 'Five exact native/query calls')
+                stats = A.stats(A.literal(mask, ids))
+                counts['numeric_survivors'] += 1
+                need(stats['central_query_on_every_output'],
+                     'A numeric survivor must pass the distinct-variable replay')
+                counts['symbolic_all_Q'] += 1
+                ranks[stats['coefficient_rank_sum']] += 1
+                counts['factored'] += int(stats['coefficient_rank_sum'] == 4)
+                digest.update((line + '\n').encode())
+            need('full=1680 thin=105' in result.stderr, 'Search inventory sizes')
+            need('mask=' + str(mask) + ' hits=' + str(counts['numeric_survivors'])
+                 in result.stderr, 'Complete survivor stream')
+            # The prefix counts authenticate the actually run search, not a saved list.
+            cases[str(mask)] = {'counts': dict(sorted(counts.items())),
+                                'rank_sum_histogram': {str(k): v for k, v in sorted(ranks.items())},
+                                'survivor_sha256': digest.hexdigest(),
+                                'prefix_census': result.stderr.splitlines()[-1]}
+            all_counts.update(counts)
+    need(all_counts['factored'] == 0 and all_counts['symbolic_all_Q'] == 12480,
+         'Frozen complete census')
+    return {'schema': 'productive-controller-basis-search/1',
+            'status': 'PASS_FINITE_FIVE_CALL_NO_IDLE_BINARY_SEARCH_NO_KAPPA',
+            'cases': cases, 'totals': dict(sorted(all_counts.items())),
+            'controls': checked, 'new_kappa': None}
+
+
+if __name__ == '__main__':
+    parser = argparse.ArgumentParser()
+    parser.add_argument('--write', action='store_true')
+    args = parser.parse_args()
+    receipt = run()
+    target = HERE / 'RESULT.json'
+    if args.write:
+        target.write_text(json.dumps(receipt, indent=2, sort_keys=True) + '\n')
+    else:
+        need(receipt == json.loads(target.read_text()), 'Committed exact receipt')
+    print(receipt['status'])
+    print(json.dumps(receipt['totals'], sort_keys=True))