From 7537009c656e441ad943ed75a4b32b010433b582 Mon Sep 17 00:00:00 2001
From: Ali Romman <226877337+aliromman@users.noreply.github.com>
Date: Sun, 25 Oct 2026 18:20:48 -0500
Subject: [PATCH 1/2] Prove query Gram capacity cuts for complete caller words

---
 .../PROOF.md                                  |  562 +++++
 .../README.md                                 |  165 ++
 .../RESULT.json                               |  287 +++
 .../SOURCES.json                              |   50 +
 .../TASK.json                                 |  110 +
 .../VALIDATION.md                             |   36 +
 .../VERIFY.json                               |   35 +
 .../cuts.py                                   |   87 +
 .../discovery/README.md                       |   80 +
 .../discovery/colour-query-search.json        | 1860 +++++++++++++++++
 .../discovery/pair_search.py                  |   91 +
 .../discovery/price-screens.json              |  140 ++
 .../discovery/price_screens.py                |   40 +
 .../discovery/rational_pair_search.py         |   72 +
 .../discovery/receipts/ENVIRONMENT.json       |   26 +
 .../receipts/imb-advancing-smt4.json          |    9 +
 .../receipts/imb-advancing-smt6-query.json    |   10 +
 .../receipts/imb-advancing-smt6.json          |   10 +
 .../discovery/receipts/imb-formal-cut6.json   |    7 +
 .../discovery/receipts/imb-pair10.json        |    9 +
 .../discovery/receipts/imb-pair4-tangent.json |   29 +
 .../discovery/receipts/imb-pair4.json         |    8 +
 .../discovery/receipts/imb-pair6-core.json    |   42 +
 .../discovery/receipts/imb-pair6-leading.json |   51 +
 .../discovery/receipts/imb-pair6-tangent.json |   51 +
 .../discovery/receipts/imb-pair6.json         |    8 +
 .../discovery/receipts/imb-pair8.json         |    8 +
 .../receipts/imb-rational-pair2.json          |   20 +
 .../receipts/imb-rational-pair4.json          |    8 +
 .../receipts/imb-rational-pair6.json          |    9 +
 .../discovery/receipts/imb-relation4.json     |   13 +
 .../discovery/receipts/imb-relation6.json     |   15 +
 .../discovery/relation_search.py              |   82 +
 .../discovery/search_cuts.py                  |   93 +
 .../discovery/signed-simplex-census.json      |   18 +
 .../discovery/simplex-census.json             |   34 +
 .../discovery/simplex_search.cpp              |  131 ++
 .../discovery/solve.py                        |  106 +
 .../fourteen-query-intersection-rejected.json |  128 ++
 .../examples/shortest-repeat-rejected.json    |   32 +
 .../examples/six-query-positive.json          |   60 +
 .../verify.py                                 |  499 +++++
 42 files changed, 5131 insertions(+)
 create mode 100644 research/shortest-controller-stage-capacity/PROOF.md
 create mode 100644 research/shortest-controller-stage-capacity/README.md
 create mode 100644 research/shortest-controller-stage-capacity/RESULT.json
 create mode 100644 research/shortest-controller-stage-capacity/SOURCES.json
 create mode 100644 research/shortest-controller-stage-capacity/TASK.json
 create mode 100644 research/shortest-controller-stage-capacity/VALIDATION.md
 create mode 100644 research/shortest-controller-stage-capacity/VERIFY.json
 create mode 100644 research/shortest-controller-stage-capacity/cuts.py
 create mode 100644 research/shortest-controller-stage-capacity/discovery/README.md
 create mode 100644 research/shortest-controller-stage-capacity/discovery/colour-query-search.json
 create mode 100644 research/shortest-controller-stage-capacity/discovery/pair_search.py
 create mode 100644 research/shortest-controller-stage-capacity/discovery/price-screens.json
 create mode 100644 research/shortest-controller-stage-capacity/discovery/price_screens.py
 create mode 100644 research/shortest-controller-stage-capacity/discovery/rational_pair_search.py
 create mode 100644 research/shortest-controller-stage-capacity/discovery/receipts/ENVIRONMENT.json
 create mode 100644 research/shortest-controller-stage-capacity/discovery/receipts/imb-advancing-smt4.json
 create mode 100644 research/shortest-controller-stage-capacity/discovery/receipts/imb-advancing-smt6-query.json
 create mode 100644 research/shortest-controller-stage-capacity/discovery/receipts/imb-advancing-smt6.json
 create mode 100644 research/shortest-controller-stage-capacity/discovery/receipts/imb-formal-cut6.json
 create mode 100644 research/shortest-controller-stage-capacity/discovery/receipts/imb-pair10.json
 create mode 100644 research/shortest-controller-stage-capacity/discovery/receipts/imb-pair4-tangent.json
 create mode 100644 research/shortest-controller-stage-capacity/discovery/receipts/imb-pair4.json
 create mode 100644 research/shortest-controller-stage-capacity/discovery/receipts/imb-pair6-core.json
 create mode 100644 research/shortest-controller-stage-capacity/discovery/receipts/imb-pair6-leading.json
 create mode 100644 research/shortest-controller-stage-capacity/discovery/receipts/imb-pair6-tangent.json
 create mode 100644 research/shortest-controller-stage-capacity/discovery/receipts/imb-pair6.json
 create mode 100644 research/shortest-controller-stage-capacity/discovery/receipts/imb-pair8.json
 create mode 100644 research/shortest-controller-stage-capacity/discovery/receipts/imb-rational-pair2.json
 create mode 100644 research/shortest-controller-stage-capacity/discovery/receipts/imb-rational-pair4.json
 create mode 100644 research/shortest-controller-stage-capacity/discovery/receipts/imb-rational-pair6.json
 create mode 100644 research/shortest-controller-stage-capacity/discovery/receipts/imb-relation4.json
 create mode 100644 research/shortest-controller-stage-capacity/discovery/receipts/imb-relation6.json
 create mode 100644 research/shortest-controller-stage-capacity/discovery/relation_search.py
 create mode 100644 research/shortest-controller-stage-capacity/discovery/search_cuts.py
 create mode 100644 research/shortest-controller-stage-capacity/discovery/signed-simplex-census.json
 create mode 100644 research/shortest-controller-stage-capacity/discovery/simplex-census.json
 create mode 100644 research/shortest-controller-stage-capacity/discovery/simplex_search.cpp
 create mode 100644 research/shortest-controller-stage-capacity/discovery/solve.py
 create mode 100644 research/shortest-controller-stage-capacity/examples/fourteen-query-intersection-rejected.json
 create mode 100644 research/shortest-controller-stage-capacity/examples/shortest-repeat-rejected.json
 create mode 100644 research/shortest-controller-stage-capacity/examples/six-query-positive.json
 create mode 100644 research/shortest-controller-stage-capacity/verify.py

diff --git a/research/shortest-controller-stage-capacity/PROOF.md b/research/shortest-controller-stage-capacity/PROOF.md
new file mode 100644
index 0000000000..3e1a1f6b1f
--- /dev/null
+++ b/research/shortest-controller-stage-capacity/PROOF.md
@@ -0,0 +1,562 @@
+# A rank cut for stage reuse
+
+Ali Romman, with substantial OpenAI Codex assistance. Apache-2.0.
+
+## 1. Result and exact model
+
+This is a scoped obstruction for complete caller words. It does not keep
+the inputs to earlier paid calls fixed. It allows arbitrary invertible
+binary changes of basis between calls.
+
+There are n independent main fields, a central involution Q, and independent
+commuting involutions z_x, one for each transverse axis. Work in the group
+algebra over F2. A full call has the form
+
+```text
+(I + (d_i + 1) P_i) (I + Q N_i),
+d_i = product(z_x : x in S_i),   |S_i| = b.
+```
+
+Here P_i is an idempotent of rank two, N_i is a nilpotent of rank one,
+and P_i N_i = N_i P_i = N_i. A thin call is I + Q N_i. The sets S_i can
+overlap or repeat in any way. Ordinary scalar changes of basis are free
+for this necessary test. Helpers stay separate independent jobs. The
+main target, after constant invertible binary input and output bases, is
+
+```text
+diag(Q * product(z_x : x in T_j) : j = 1,...,n).
+```
+
+Its charged Fourier rank is 1 + |T_j|. Each full call uses a fresh complete
+local helper inventory. A thin call costs one rank-one query per port.
+Sections 1-8 describe the controller on each port. The complete price
+applies these bounds across the v ports. Those sections keep ports
+separate. Section 9 extends the shortest-query result to arbitrary
+scalar mixing across all ports at the stated saturated main-field count.
+The principal theorem permits no idle axis maps or other paid main maps.
+Section 2 also gives a necessary cut when such idle maps are present.
+
+Let L count all query-bearing calls and f count the full calls. The
+shortest case is L = n + 1. For n >= 4, the following statements hold.
+
+1. If axis x occurs in k_x full calls, it can occur in at most
+   k_x + (k_x mod 2) independent main targets.
+2. At most two full calls can have an axis that occurs in no other call.
+3. With b = 8 and either pinned P104 local inventory, the complete
+   target moment minus paid moment is at most -8 for every exponent
+   0 < t <= 1. The bound is sharp at t = 1.
+
+This includes all main-field counts, all full/thin placements, every
+commuting coordinate overlap, and all scalar bases in the declared
+binary model. A finite search is not the proof of these statements.
+
+For n = 2, the three-full-call unit is the exception. Its optimistic
+complete moment is already negative at kappa = 0.002 for both pinned
+inventories, and remains negative for every larger kappa below one.
+Thus no shortest caller in this model improves the selected bound.
+
+The binary model does not cover arbitrary complex scalar codes with
+even denominators, noncommuting stage operators, an advancing operator
+with unbounded order, joint main/helper codes, or a changed target
+contract. An integral symbolic caller that reduces to this model must
+pass its test. No reduction of every physical Clifford program to this
+model is asserted.
+
+## 2. General query-frame cut
+
+Set Q = 1 + e, with e squared equal to zero. Absorb the ordinary changes
+of basis and each call's constant value at Q = 1 into adjacent bases.
+Each query then has the form I + e R_i, where
+
+```text
+R_i = u_i v_i,   v_i u_i = 0,   sum_i R_i = I_n.
+```
+
+The corresponding full-call projector still has rank two and satisfies
+P_i R_i = R_i P_i = R_i. This normalization is a conjugation. It does
+not change ranks, independence, or the number of paid calls.
+
+Put U_0 = [u_0 ... u_(L-1)] and let V_0 have rows v_i. Then U_0 V_0 = I.
+The query Gram matrix K = V_0 U_0 is an idempotent of rank n. Its diagonal
+is zero. If L <= n, rank forces L = n and V_0 U_0 = I, a contradiction.
+Thus L >= n + 1. Write h = L - n. The complementary idempotent I - K
+has rank h.
+
+For any axis x, let S be the set of its full-call occurrences, with
+|S| = k. Set that axis to 1 + d, where d squared is zero; set all other
+axes and Q to one. The full-call derivative is P_i at an occurrence and
+zero elsewhere. The monomial target gives an idempotent E_x whose rank
+r_x is the number of target jobs that contain x. Hence
+
+```text
+E_x = sum_(i in S) P_i.
+```
+
+More generally, h_x separately charged one-field idle occurrences add
+h_x matrices of rank at most one to this sum. The same argument below
+allows those terms.
+
+For each i, choose a_i in the image of P_i with v_i a_i = 1. Such a
+choice exists because v_i P_i = v_i is nonzero. Choose b_i as the
+coordinate of u_i in the basis (u_i, a_i) of that image, with b_i zero
+on the kernel of P_i. Then
+
+```text
+P_i = u_i b_i + a_i v_i,
+b_i u_i = v_i a_i = 1,   b_i a_i = v_i u_i = 0.
+```
+
+Factor the sum E_x = A B. Use the columns u_i, a_i of A and the rows
+b_i, v_i of B, then append a rank-one factor for each idle term. Thus A
+has 2k + h_x columns. Because E_x is an idempotent,
+
+```text
+rank(I_(2k+h_x) - B A) = 2k + h_x - r_x.                 (1)
+```
+
+To prove (1), U: w -> A w maps the kernel of I - B A bijectively onto
+the image of E_x. Its inverse is y -> B y. This proves the dimension
+identity even when A or B has a kernel.
+
+Select the rows of B A that came from v_i and the columns that came
+from u_j. The corresponding submatrix of the identity is zero. The
+selected submatrix of I - B A is therefore -K[S,S]. A submatrix cannot
+have larger rank than its parent. Equation (1) gives the necessary cut
+
+```text
+r_x <= 2k + h_x - rank K[S,S].                         (2)
+```
+
+This cut uses the actual query Gram matrix. It applies to longer words
+as well as shortest words. Since K[S,S] = I_k - (I-K)[S,S],
+
+```text
+rank K[S,S] >= max(0, k-h),
+r_x <= k + min(k,h) + h_x.                             (3)
+```
+
+The cut can reject a proposed target inventory before the full stage
+polynomial is built. Passing it is not an operator identity or admission.
+
+## 3. Sharp capacity at the shortest query count
+
+Suppose L = n + 1. The rank-one complementary idempotent I - K has
+diagonal one. Over F2 it is the all-one matrix. Thus
+
+```text
+v_i u_j = 1 for i != j, and 0 for i = j.
+```
+
+In particular, n is even. Every k by k principal submatrix is I_k + J_k,
+where J_k is all one. It has rank k when k is even, and rank k-1 when
+k is odd. Substitution in (2) gives
+
+```text
+r_x <= k + (k mod 2) + h_x.                            (4)
+```
+
+The algebraic bound is sharp. In a space with coordinates 0,1,...,k,
+take, for i = 1,...,k,
+
+```text
+u_i = e_0 + e_i,   v_i = e_0^T + e_i^T,
+P_i = e_0 e_0^T + e_i e_i^T.
+```
+
+These R_i have the required pairings. Each P_i is an idempotent of
+rank two that contains its R_i. Their sum is diagonal: it is one on
+each private coordinate and is k mod 2 on coordinate zero. Its rank
+is exactly k + (k mod 2). This is a sharp local algebraic witness,
+not a complete profitable caller.
+
+The written results also extend to any field of characteristic two.
+In that case the rank-one complement is a b^T, with a_i b_i=1, rather
+than necessarily the all-one matrix. Replace u_i by a_i u_i and v_i
+by v_i/a_i. This preserves each R_i and makes every off-diagonal
+pairing equal to one. The proofs below then use the same simplex.
+The general cuts and the rank-two complement argument use only field
+linear algebra and integer target counts. The executable filters and
+finite controls in this package use F2; they do not enumerate extension
+fields. This extension still gives no characteristic-zero reduction.
+
+## 4. At most two calls can have private axes
+
+This step uses Cinna Davis's minimum-query projector lemma from
+`productive-controller-basis-search/GLOBAL-PROOF.md`. Its hypotheses
+hold for every call with a private axis, even when other calls share
+arbitrary axes. The other stages need not have independent multipliers.
+
+For a private axis at call s, its target derivative is P_s. Independence
+of that target projector from Q gives
+
+```text
+[P_s, sum_(j>s) R_j] = 0.
+```
+
+All private-axis target projectors commute with one another because
+they are diagonal in the same output basis. They also satisfy
+P_s R_s = R_s P_s = R_s.
+
+Here is the retained argument. Normalize the simplex to
+u_i = e_i and v_i = 1 + e_i for i < n, with u_n = v_n = 1. For an
+interior position s, set U_s = sum_(j>s) u_j and V_s = sum_(j>s) v_j.
+Commutation forces the image of P_s to contain u_s,U_s and its row
+space to contain v_s,V_s. These two pairs are independent. Their
+pairing matrix is
+
+```text
+[0  n-s; n-s  0] over F2.
+```
+
+There is no rank-two projector if n-s is even. If n-s is odd, the only
+choice is P_s = u_s V_s + U_s v_s. Two different interior choices do
+not commute: for s < t, P_s u_t = U_s, P_t u_t = u_t, and P_t U_s = 0.
+
+An initial private-axis call can coexist with an interior one only at
+s = 1. Otherwise its forced two-dimensional image and row space have
+zero pairing. A terminal private-axis call can coexist with an interior
+one only at s = n-1, for the same reason. For n >= 4 one interior call
+cannot be both positions. There are at most two private-axis calls.
+
+With b axes per full call, at most 2b axes can have multiplicity one.
+Let s count those axes. The total axis occurrence count is b f. For
+k >= 2, k + (k mod 2) <= 4k/3. With no idles, (4) therefore gives
+
+```text
+R := sum_x r_x
+   <= 2s + (4/3)(bf-s)
+   <= (4bf+4b)/3.                                     (5)
+```
+
+Also R <= 2bf. These are bounds on all main outputs together. They do
+not count a stage map as a new independent field.
+
+For future callers with idles, let H = sum_x h_x. At most H private
+axes can have h_x > 0. The same argument gives the weaker useful tradeoff
+
+```text
+R - H <= (4bf + 4b + 2H)/3.                           (6)
+```
+
+Equation (6) is a linear rank budget. It is not an all-concave rejection
+when idle calls can combine several axes at a concave price.
+
+## 5. Complete P104 price, for every concave tariff
+
+Both pinned source inventories have v = 104 ports, b = 8, and
+
+```text
+sum_r r (paid[r] - helpers[r]) = Lambda = 1720
+                                   = 2*b*v + 56.
+```
+
+The 56 includes the local owned-copy debt. The helper targets are
+independent source inputs. Their complete bill is retained at every
+full call. The inputs are the main P104 package and PR5599 at
+09dd0965711ca7eeb169057a420abab1c9052137. The latter source changes
+helper inputs and includes PR5565's paid profile. Its native result
+is inherited here; this package does not rerun its native construction.
+
+For c_r = paid[r] - helpers[r], both exact profiles satisfy
+
+```text
+sum_r c_r max(r-j,0) <= 0  for every integer j >= 1.     (7)
+```
+
+The verifier checks the complete finite list. Beyond the largest
+source rank, the sums are zero. Let g be any nondecreasing concave
+tariff on the nonnegative integers, with g(0)=0 and g(1)=1. Its
+successive slope drops a_j are nonnegative, and
+
+```text
+g(r) = r - sum_(j>=1) a_j max(r-j,0).
+```
+
+Only finitely many terms matter at each source rank. Equation (7) gives
+
+```text
+sum_r c_r g(r) >= Lambda.                              (8)
+```
+
+Also g(1+r) <= 1+r. There are n main targets per port and L-f thin
+queries. The complete target-minus-paid moment is therefore at most
+
+```text
+v (n+R) - v(L-f) - Lambda*f
+  = 104(f-1+R) - 1720f.                               (9)
+```
+
+For f = 0,1,2, the bound R <= 16f gives, respectively, -104, -56, -8.
+For f >= 3, (5) gives
+
+```text
+moment <= (3016 - 1520f)/3 < -8.                       (10)
+```
+
+Thus the complete moment is at most -8 for every such tariff. In
+particular, this holds for g(r)=r^(1-kappa), 0 <= kappa < 1. Adding
+nonnegative compiler or ordinary-work costs cannot change this failure
+of the necessary recursive moment inequality.
+
+The same calculation gives an inventory design condition. Let a local
+family have v ports, b>=1 transverse axes and net rank mass
+Lambda=2bv+d. Suppose its paid-minus-helper hinge sums are nonpositive,
+as in (7). If d>=v/2, no shortest caller with n>=4 can have a positive
+complete concave moment. At f=0,1,2 the bounds are -v,-d,v-2d. For f>=3,
+the bound is
+
+```text
+v*(4b/3-1) + f*(v*(1-2b/3)-d).
+```
+
+It decreases in f. At f=3 and d=v/2 it is v*(1/2-2b/3)<0.
+Thus d<v/2 is necessary to reopen this shortest-query route while
+keeping the hinge condition. P104 has d=56 and v/2=52. Changes to the
+local paid distribution or helper endpoints that retain these two
+conditions do not escape the obstruction. This is a necessary design
+condition, not a construction when the inequality is reversed.
+
+The n=4, f=2, L=5 factored word already recorded by Cinna Davis attains
+-8 at the linear tariff. Its main jobs have ranks 1,1,17,17, and its
+three thin queries remain charged. The verifier checks the whole
+binary polynomial matrix, the four independent coefficient images,
+and a separate interpreter. This shows that the numerical upper bound
+is sharp in the declared model, rather than only a loose negative bound.
+
+## 6. The two-field exception
+
+For n = 2, every full projector is I_2. There are three queries. With
+f <= 2, (9) and R <= 16f still reject the complete bill. With f = 3,
+each main target has rank at most 25. Its best possible complete moment is
+
+```text
+208 * 25^t - 3 * sum_r c_r r^t.
+```
+
+Exact integer-root intervals make this quantity negative at t=499/500
+for both sources. Its negative coefficients have lower rank than all
+its positive coefficients. After division by the first positive rank
+to the power t, it is increasing in t. It therefore stays negative for
+every 0 < t <= 499/500. The two-field exception cannot improve kappa
+past 0.002. This is separate from the sharper no-saving result for n>=4.
+
+## 7. Joint axis cuts
+
+There is also a necessary intersection cut. It can reject profiles that
+pass every separate capacity test. Let S and T be the occurrence sets
+of two axes x and y. Define
+
+```text
+delta_x = 2|S| + h_x - r_x,
+delta_y = 2|T| + h_y - r_y.
+```
+
+These numbers are nonnegative. In the factorizations E_x=A_x B_x and
+E_y=A_y B_y from Section 2, the rows V_S occur in B_x and the columns
+U_T occur in A_y. Since E_x is an idempotent and its row space is
+contained in the row space of B_x,
+
+```text
+rank(V_S (I-E_x)) <= rank(B_x)-r_x <= delta_x.
+rank((I-E_y) U_T) <= rank(A_y)-r_y <= delta_y.
+```
+
+Decompose V_S U_T as
+
+```text
+V_S E_x E_y U_T + V_S(I-E_x)U_T + V_S E_x(I-E_y)U_T.
+```
+
+The target projectors commute and select their target axis sets. Hence
+the number r_xy of independent main jobs that contain both axes obeys
+
+```text
+r_xy = rank(E_x E_y)
+     >= rank K[S,T] - delta_x - delta_y.                (11)
+```
+
+This is a necessary cut for arbitrary query counts and includes the
+stated idle terms. A negative right side gives no constraint. At full
+capacity, both deltas vanish. The cut then forces target intersections
+directly from the off-diagonal query Gram blocks.
+
+## 8. A longer paired-stage obstruction
+
+Consider a second, narrower family. Every call is full. There are
+L=n+2=2m calls. Each of m independent stage blocks occurs exactly twice;
+each block has eight axes and different blocks have disjoint axes. The
+two calls in a pair need not be adjacent. All binary scalar bases and
+all call orders remain allowed. There are no idles.
+
+Let r_c be the number of main targets that contain stage block c.
+Every word coefficient is a product of whole blocks. Constant boundary
+bases cannot add new monomials, so each target contains a whole block
+or none of that block. The count r_c is at most four.
+Suppose first that every r_c=4. Write I-K=XY,
+where X has two columns, Y has two rows and YX=I_2. For each two-call
+index set S_c, (2) forces K[S_c,S_c]=0. Thus
+
+```text
+X[S_c,:] Y[:,S_c] = I_2.
+```
+
+Both two-by-two factors are invertible. Their product in the reverse
+order is also I_2. Summing in c gives YX=m I_2, so m must be odd.
+For any two distinct classes, K[S_c,S_d] has rank two. Equation (11)
+therefore requires at least two common target coordinates for every
+pair of stage blocks.
+
+At full capacity, E_c=A_c B_c has rank four with four inner columns.
+It follows that B_c A_c=I_4. In particular, E_c U_c=U_c and V_c E_c=V_c.
+Use the common basis in which all E_c are diagonal. Every row of U_0
+is nonzero, since U_0 V_0=I. No row can be supported in just one class:
+U_0 X=0 and X[S_c,:] is invertible. Thus every main coordinate belongs
+to at least two stage sets.
+
+Let d_j count the stage sets that contain coordinate j. We now have
+
+```text
+n=2m-2,   2 <= d_j <= m,   sum_j d_j=4m,
+sum_j binomial(d_j,2) >= 2*binomial(m,2)=m(m-1).        (12)
+```
+
+Only four units remain after assigning degree two to all coordinates.
+Convexity makes the largest intersection sum by putting those units
+on as few coordinates as possible. At m=5 this maximum is 19, below
+20. For m>=6 it is
+
+```text
+binomial(6,2)+(2m-3)*binomial(2,2) = 2m+12 < m(m-1).
+```
+
+Even m already fails the parity condition. Thus full capacity is
+impossible for every m>=4, or n>=6. For m=3, two disjoint three-query
+units on four fields attain full capacity. Their three corresponding
+stage pairs each reach all four outputs. This positive exact word
+passes (2) and (11), and prevents an invalid extension of the shortest
+query bound to all longer words.
+
+At least one stage occurrence must therefore be lost for n>=6:
+
+```text
+sum_c r_c <= 4m-1.
+```
+
+The complete linear-tariff bound for either pinned P104 inventory is
+
+```text
+104*(n+8*(4m-1)) - 2m*1720 = 96m-1040.                (13)
+```
+
+It is negative for m<=10. The same bound holds for every normalized
+nondecreasing concave tariff by (8). This rejects, in particular, the
+fourteen-call/twelve-field candidate and the eighteen-call/sixteen-field
+candidate for every such tariff. The former had a floating optimistic
+crossing near .003393385 before the intersection cut. That crossing is
+not a caller or a kappa claim.
+
+For larger m, discrete concavity gives the sharper power-tariff bound
+
+```text
+M_m(t) <= 104*((2m-5)*17^t + 3*25^t) - 2m*sum_r c_r r^t. (14)
+```
+
+The verifier proves that this bound is negative at t=997/1000 for
+m=4 and m=26. It is affine in m, so it is negative for all 4<=m<=26.
+All negative coefficients have lower rank than all positive ones.
+The sign-separation argument from Section 6 extends this rejection to
+every 0<t<=997/1000. Therefore no paired-stage caller with 6<=n<=50
+in this family can improve kappa beyond .003. At n=4, full capacity
+forces all four jobs to contain all three stages. Its bill is twice
+the two-field bill from Section 6. Any loss of capacity instead gives
+the negative bound (13). At n=2, every full projector is I_2, and each
+paired stage cancels. These smaller cases also fail beyond .003.
+
+More queries, partially overlapping axis sets, mixed full/thin words,
+paid idles or a nonbinary construction require a new complete test.
+A common advancing operator remains a different route: it has
+unbounded-order powers, so the involutive-axis proof does not exclude it.
+
+## 9. The shortest obstruction also permits coupled ports
+
+The shortest theorem is not limited to a tensor copy of one scalar
+controller. Let each query have rank q, each full projector have rank
+2q, and let the total main dimension be N=nq. Use L=n+1 calls. Allow
+arbitrary binary scalar bases on all N fields, including across ports.
+Write R_i=U_i V_i, where U_i has q independent columns, V_i has q
+independent rows and V_i U_i=0. Then U V=I_N. The query Gram matrix
+K=VU has zero q-by-q diagonal blocks. Its complement C=I-K has rank q.
+
+Factor C=A B with A of size qL by q and B of size q by qL, and BA=I_q.
+For each call block i, A_i B_i=I_q. Thus A_i is invertible and B_i=A_i^-1.
+Rescale the query factors to U_i A_i and A_i^-1 V_i. This preserves R_i.
+The rescaled Gram matrix has zero diagonal blocks and I_q in every
+off-diagonal block. Also BA=L I_q=I_q, so n is even. This proves the
+block simplex, rather than assuming it from separate ports.
+
+A compatible rank-2q full projector factors as
+
+```text
+P_i = U_i B'_i + A'_i V_i,
+B'_i U_i = V_i A'_i = I_q,   B'_i A'_i = V_i U_i = 0.
+```
+
+Choose A'_i as a right inverse of V_i inside the image of P_i, and use
+B'_i as the coordinate map for U_i along that complement. The argument
+of Section 2 now selects a qk-by-qk Gram block. For an axis used by k
+calls, its rank is q*(k-(k mod 2)). Consequently
+
+```text
+r_x <= q*(k+(k mod 2)).                               (15)
+```
+
+The private-axis argument also extends. Replace each u_i,v_i by the
+q-column/row blocks U_i,V_i. An interior private projector must contain
+the two independent q-dimensional spaces U_s and sum_(j>s) U_j, and
+the corresponding row spaces. Their pairing matrix is
+
+```text
+[0  (n-s)I_q; (n-s)I_q  0].
+```
+
+Even n-s is impossible; odd n-s gives the unique projector
+`U_s V_tail + U_tail V_s`. The noncommuting interior pair and both
+zero-pairing endpoint arguments in Section 4 apply to these blocks.
+Thus at most two call positions have private axes.
+
+The total main transverse rank therefore satisfies
+
+```text
+R <= 2qbf,   R <= q*(4bf+4b)/3.
+```
+
+There are nq target jobs and q(L-f) thin paid queries. With q=v=104,
+b=8 and the same autonomous helper inventory per full call, the
+complete price calculation in Section 5 is unchanged. Its sharp -8
+bound covers arbitrary cross-port scalar codes at N=104n, L=n+1.
+The proof also holds over characteristic-two extension fields.
+
+This extension does not extend Section 8's complete paired-stage price
+bound to arbitrary coupled ports. At L=n+2 the complement has rank 2q;
+one lost target occurrence need not mean one loss on every port.
+Different main counts with N not equal to q(L-1), mixed query ranks,
+and main/helper mixing also need separate arguments. The general
+rank and intersection cuts still apply after each rank-q query and
+rank-2q projector are factored into compatible rank-one/rank-two terms.
+
+## Credit and verification boundary
+
+Cinna Davis supplies the simplex, private-projector obstruction, the
+sharp five-query word, and the controller lineage. The new result is
+the Gram-submatrix rank and intersection cuts, their sharp repeat
+capacity, their use for arbitrary coordinate overlap, the paired-stage
+obstruction, and the complete all-concave P104 bound.
+The equality cuts in PR5588 motivated the search; passing those cuts
+alone did not supply an endpoint. The scalar, native, helper, compiler,
+precision and analytic sources retain their attribution in SOURCES.json
+and the package README.
+
+The written arguments prove the unbounded statements under their stated
+algebraic hypotheses. The exact verifier checks finite instances and
+discriminating controls. It is not a proof-assistant kernel or an
+independent human review. No selected frontier is changed.
diff --git a/research/shortest-controller-stage-capacity/README.md b/research/shortest-controller-stage-capacity/README.md
new file mode 100644
index 0000000000..bec818fcad
--- /dev/null
+++ b/research/shortest-controller-stage-capacity/README.md
@@ -0,0 +1,165 @@
+# Query Gram cuts for complete caller words
+
+This package gives two necessary cuts for a changed global caller. They bound
+both the number of independent outputs that can use one stage axis and the
+number that must share two axes. The proof allows changed paid inputs and
+arbitrary constant binary bases throughout the word. No earlier caller input
+is held fixed. **No new kappa is claimed.**
+
+The cuts turn two promising price relaxations into scoped obstructions:
+
+| Caller family | Proven consequence for both pinned P104 bills |
+| --- | --- |
+| Shortest query count L=n+1, n>=4, arbitrary overlapping commuting involutive axis sets, full/thin calls, no idles | Complete target-minus-paid moment <= -8 for every normalized nondecreasing concave tariff; the bound is sharp |
+| L=n+2, all full, separate ports, each disjoint eight-axis stage block used twice, no idles | Full stage capacity is impossible for n>=6; no caller with 2<=n<=50 passes a power-tariff saving >= .003 |
+| Fourteen calls on twelve fields in the second family | Complete moment <= -368 for every such concave tariff; the optimistic raw crossing near .003393385 is not realizable |
+
+The shortest-family statement has no upper size limit. The longer-family
+capacity statement also has no upper size limit; its complete price rejection
+is bounded as stated. These are written proofs with exact finite controls,
+not extrapolations from search failures.
+
+Section 9 also proves the shortest result for arbitrary scalar mixing
+across all 104 ports, with total main dimension N=104n and L=n+1 calls.
+Its block-simplex proof derives the required Gram matrix. The longer
+paired-stage price statement keeps ports separate. The written arguments
+extend to fields of characteristic two; the executable controls use F2.
+
+## What the cuts measure
+
+Normalize the central-query tangent terms as R_i=u_i v_i, with sum R_i=I.
+The query Gram matrix K has entries v_i u_j. If axis x occurs in call set S,
+has h_x charged one-field idle occurrences, and reaches r_x main jobs, then
+
+```text
+r_x <= 2|S| + h_x - rank K[S,S].
+```
+
+For two axes, put delta_x=2|S|+h_x-r_x and define delta_y in the same way.
+Their target sets must have at least
+
+```text
+rank K[S,T] - delta_x - delta_y
+```
+
+common main jobs. At the shortest count the first cut becomes
+`r_x <= |S|+(|S| mod 2)+h_x`. At one additional query, separate axis tests
+can pass while their required intersections are impossible. Sections 2, 7
+and 8 of [PROOF.md](PROOF.md) give the general cuts and this distinction.
+
+There is also an inventory design condition. Write the net local rank mass
+as `2*b*v+d`, where v is the port count and b is the transverse rank. If the
+paid-minus-helper hinge sums remain nonpositive, a shortest no-idle caller
+needs `d<v/2` before it can have a positive concave moment. Both pinned P104
+bills have `d=56`, while `v/2=52`. Section 5 gives the proof. Satisfying this
+necessary threshold would not by itself supply a caller.
+
+## Use the filter
+
+[cuts.py](cuts.py) accepts a JSON query frame and proposed target sets. Vectors
+are binary integers. `u[i]` and `v[i]` describe the rank-one query R_i. Each
+axis lists its call indices, target indices and optional `idle_terms`.
+An axis can represent one whole disjoint stage block when all its axes have
+the same occurrences and target set.
+
+```sh
+python3 research/shortest-controller-stage-capacity/cuts.py research/shortest-controller-stage-capacity/examples/six-query-positive.json
+python3 research/shortest-controller-stage-capacity/cuts.py research/shortest-controller-stage-capacity/examples/fourteen-query-intersection-rejected.json
+```
+
+The first command returns `PASS_NECESSARY_CUTS_ONLY` and exit code zero.
+The second returns `REJECT_NECESSARY_CUT` and exit code one. It passes every
+separate capacity test but fails the intersection test. The proof excludes
+all target assignments with full capacity in that family, not just this file.
+
+A passing filter does not supply compatible native projectors, an operator
+endpoint, paid scalar bases, helpers, ordinary maps or a compiler budget.
+The retained six-query example is an actual binary operator word; it is a
+positive control for the cut, and its complete P104 bill still loses.
+
+## Evidence and reproduction
+
+[RESULT.json](RESULT.json) records the exact checks. Two literal interpreters
+agree on the five-query sharp word and the six-query longer control. The
+replay checks 4,352 two/three-projector combinations, simplex identities
+through 64 fields, the AB/BA kernel identity, intersection inequalities,
+target-incidence maxima, complete helper/paid histograms and exact integer
+root intervals. A deleted query, an invalid query frame, a non-idempotent
+sum and the false extension of the shortest cut are discriminating controls.
+
+```sh
+python3.12 -B scripts/research_package.py --package research/shortest-controller-stage-capacity
+python3.12 -I -O -B research/shortest-controller-stage-capacity/verify.py
+```
+
+Expected marker: `PASS_CALLER_STAGE_CAPACITY_CUTS`. The replay needs only
+Python 3.12 and the standard library. It reads and compares the committed
+receipt. `--write-result` is an explicit regeneration option. The direct
+verifier also works in a source export containing the five declared inputs.
+It authenticates those bytes before it loads the credited interpreter.
+
+The local inventories are original P104 and PR5599 at
+`09dd0965711ca7eeb169057a420abab1c9052137`. They are exact historical inputs,
+not a claim about the strongest pending frontier. Both have complete net
+rank mass 1720. Source pins and hashes are in [SOURCES.json](SOURCES.json).
+Native and outer admission of those sources is inherited, not rerun here.
+The negative necessary moment leaves no compiler or ordinary-work saving
+to establish. [VALIDATION.md](VALIDATION.md) records the checks actually run.
+
+The initial advancing-operator and repeated-stage searches are saved in
+[discovery/README.md](discovery/README.md). Solver `unknown` stays unknown;
+solver `unsat` is not a separately checked proof certificate. Those searches
+are not dependencies of the theorem replay.
+
+## Scope and coordination
+
+The model is binary with independent commuting involutive coordinate axes.
+Helpers are separate independent inputs. The principal obstructions permit
+no idle maps. The generic cuts allow explicitly counted one-field idle
+terms, but their concave cost needs a separate bill. Arbitrary complex or
+even-denominator codes, noncommuting stages, unbounded-order advancing maps,
+joint main/helper codes and different target contracts are outside the proof.
+
+This is a user-directed change from the QQ16-specific card. It does not
+complete that card's installed-protocol question. [TASK.json](TASK.json)
+preserves the original card and states the changed scope. Canonical main was
+refreshed from `5e0052ca0aa3036a3afa8b0438927377c8d97d53` to
+`d7633ce230196a1d5d061347de7a0fd8be512ed6`; the frozen source pins remain.
+Priorities and the selected record did not change at that checkpoint.
+[Discussion5593](https://github.com/CrocSwap/integer-mult-bounds/discussions/5593)
+is the canonical investigation. Local contact, helper-basis and G20 claims
+are separate. No selected-frontier change or scientific acceptance is implied.
+
+## Open next questions
+
+- Extend the intersection bound to a quantitative rank loss that grows with
+  caller size. Start from the rank-two complement and allow unsaturated
+  stage classes. This could close the remaining large paired-stage cases.
+  The present proof only forces one lost stage occurrence.
+- Search a changed caller with more queries, mixed calls or partially
+  overlapping axis blocks. Apply both cuts before a full polynomial search,
+  then verify the whole endpoint and complete bill. The filter is necessary
+  only; no such favorable word is supplied here.
+- Test the advancing operator route in characteristic zero. The recorded
+  rational four-field screen is negative and the six-field screen timed out.
+  An infinite-order stage is outside the involutive-axis obstruction. A
+  surviving word still needs native maps, helpers and complete pricing.
+- Independently review the normalization, private-axis extension and joint
+  incidence argument. Start with Sections 2, 4, 7 and 8 of the proof. Finite
+  controls do not replace a proof audit or a formal kernel.
+
+## Credit
+
+Cinna Davis / 1337isnot1337 supplies the minimum-query simplex, private-stage
+projector obstruction, five-query sharp word and controller lineage. The
+new contribution is the rank/intersection cut, its application to coordinate
+reuse, the paired-stage packing obstruction and the complete concave price
+test. Elementary rank and convexity tools are standard; no claim of worldwide
+priority is made for those tools.
+
+Credit the P104 productive-helper and source-word authors, the PR5565 cascade
+and PR5599 helper-split authors, Jacob Alan Sussman's productive recursion,
+the native suppliers, Cao Yifan/zxv compiler and moment work, and all retained
+precision and analytic sources. Source-specific notices remain unchanged.
+The equality cuts in Ali Romman's PR5588 motivated this whole-word search.
+Prepared for Ali Romman with substantial OpenAI Codex assistance. Apache-2.0.
diff --git a/research/shortest-controller-stage-capacity/RESULT.json b/research/shortest-controller-stage-capacity/RESULT.json
new file mode 100644
index 0000000000..fe5ac435fe
--- /dev/null
+++ b/research/shortest-controller-stage-capacity/RESULT.json
@@ -0,0 +1,287 @@
+{
+  "authenticated_inputs": 5,
+  "block_simplex_controls": {
+    "includes_port_count_104": true,
+    "rank_controls": 80,
+    "total_dimension_contract": "N=q*n and L=n+1"
+  },
+  "complete_prices": {
+    "PR5599_at_09dd0965": {
+      "helpers": {
+        "1": 2,
+        "2": 5,
+        "4": 89,
+        "5": 11,
+        "7": 5,
+        "8": 16,
+        "9": 412
+      },
+      "hinges_at_1_through_9": [
+        -1187,
+        -1893,
+        -2145,
+        -1904,
+        -1660,
+        -1259,
+        -840,
+        -412,
+        0
+      ],
+      "n12_previous_equality_cut": {
+        "checks": [
+          {
+            "k": 1,
+            "paid": "966665/32",
+            "paid_minus_targets": "22572866061/1048576",
+            "targets": "9102812659/1048576"
+          }
+        ],
+        "polynomial": {
+          "0": 39450,
+          "1": -30814,
+          "17": 832,
+          "2": -6356,
+          "25": 416,
+          "3": -6902,
+          "4": -42,
+          "5": -2198,
+          "6": -252,
+          "7": -126,
+          "8": 224,
+          "9": 5768
+        },
+        "schema": "native-equality-cut/v1",
+        "scope": "necessary conditions; no native admission or kappa claim",
+        "status": "PASS_NECESSARY_EQUALITY_CUTS",
+        "tail": {
+          "certified_from_k": 1,
+          "first_degree": 0,
+          "leading_coefficient": 39450,
+          "remaining_absolute_sum": 53930,
+          "strict_sign": 1
+        },
+        "width": null
+      },
+      "n12_without_incidence_cut_positive": true,
+      "net_rank_mass": 1720,
+      "paid": {
+        "1": 2203,
+        "2": 459,
+        "3": 493,
+        "4": 92,
+        "5": 168,
+        "6": 18,
+        "7": 14
+      },
+      "paired_margin_at_kappa_003": {
+        "26": {
+          "denominator": 281474976710656,
+          "lower_decimal": "-30.924007237089384148021053988487",
+          "lower_numerator": -8704334216859892,
+          "upper_decimal": "-30.924007236782344421044399496168",
+          "upper_numerator": -8704334216773468
+        },
+        "4": {
+          "denominator": 281474976710656,
+          "lower_decimal": "-884.87666334030629400331235956401",
+          "lower_numerator": -249070638205515704,
+          "upper_decimal": "-884.87666334025968239984649699181",
+          "upper_numerator": -249070638205502584
+        }
+      },
+      "two_field_margin_at_kappa_002": {
+        "denominator": 281474976710656,
+        "lower_decimal": "-20.665999385967381840600864961743",
+        "lower_numerator": -5816961695867600,
+        "upper_decimal": "-20.665999385949994859856815310195",
+        "upper_numerator": -5816961695862706
+      }
+    },
+    "original_P104": {
+      "helpers": {
+        "4": 51,
+        "5": 36,
+        "7": 24,
+        "8": 122,
+        "9": 294
+      },
+      "hinges_at_1_through_9": [
+        -1378,
+        -2047,
+        -2159,
+        -1882,
+        -1544,
+        -1134,
+        -708,
+        -293,
+        0
+      ],
+      "n12_previous_equality_cut": {
+        "checks": [
+          {
+            "k": 1,
+            "paid": "7927437/256",
+            "paid_minus_targets": "23507257869/1048576",
+            "targets": "8963524083/1048576"
+          }
+        ],
+        "polynomial": {
+          "0": 42124,
+          "1": -34006,
+          "17": 832,
+          "2": -7798,
+          "25": 416,
+          "3": -5446,
+          "4": -854,
+          "5": -1008,
+          "6": -224,
+          "7": 154,
+          "8": 1708,
+          "9": 4102
+        },
+        "schema": "native-equality-cut/v1",
+        "scope": "necessary conditions; no native admission or kappa claim",
+        "status": "PASS_NECESSARY_EQUALITY_CUTS",
+        "tail": {
+          "certified_from_k": 1,
+          "first_degree": 0,
+          "leading_coefficient": 42124,
+          "remaining_absolute_sum": 56548,
+          "strict_sign": 1
+        },
+        "width": null
+      },
+      "n12_without_incidence_cut_positive": true,
+      "net_rank_mass": 1720,
+      "paid": {
+        "1": 2429,
+        "2": 557,
+        "3": 389,
+        "4": 112,
+        "5": 108,
+        "6": 16,
+        "7": 13,
+        "9": 1
+      },
+      "paired_margin_at_kappa_003": {
+        "26": {
+          "denominator": 281474976710656,
+          "lower_decimal": "-72.488495253100026616266404744238",
+          "lower_numerator": -20403697513156828,
+          "upper_decimal": "-72.488495252800561274852952919900",
+          "upper_numerator": -20403697513072536
+        },
+        "4": {
+          "denominator": 281474976710656,
+          "lower_decimal": "-891.27119995815408515227318275720",
+          "lower_numerator": -250870540251099848,
+          "upper_decimal": "-891.27119995810863883889396674931",
+          "upper_numerator": -250870540251087056
+        }
+      },
+      "two_field_margin_at_kappa_002": {
+        "denominator": 281474976710656,
+        "lower_decimal": "-22.264631701482969106109521817416",
+        "lower_numerator": -6266936689646252,
+        "upper_decimal": "-22.264631701466019109147964627482",
+        "upper_numerator": -6266936689641481
+      }
+    }
+  },
+  "incidence_controls": {
+    "gl2_pair_controls": 36,
+    "n12_all_concave_upper": -368,
+    "n16_all_concave_upper": -176,
+    "packing_dp_max_m": 65,
+    "paired_stage_cases": {
+      "3": {
+        "max_intersections": 12,
+        "parity_admissible": true,
+        "required": 6
+      },
+      "4": {
+        "max_intersections": 16,
+        "parity_admissible": false,
+        "required": 12
+      },
+      "5": {
+        "max_intersections": 19,
+        "parity_admissible": true,
+        "required": 20
+      },
+      "6": {
+        "max_intersections": 24,
+        "parity_admissible": false,
+        "required": 30
+      },
+      "7": {
+        "max_intersections": 26,
+        "parity_admissible": true,
+        "required": 42
+      }
+    }
+  },
+  "limits": {
+    "formal_kernel": false,
+    "independent_review": false,
+    "model": "Binary constant bases; commuting independent involutive axes; autonomous helpers",
+    "native_word_replay": false,
+    "new_kappa": false
+  },
+  "operator_controls": {
+    "deleted_query_rejected": true,
+    "sharp_five_query_degrees": {
+      "0": 2,
+      "2": 2
+    },
+    "sharp_margin_at_linear_tariff": -8,
+    "six_query_gram": [
+      6,
+      5,
+      3,
+      48,
+      40,
+      24
+    ],
+    "six_query_paired_degrees": {
+      "3": 4
+    },
+    "two_literal_interpreters": true
+  },
+  "rank_cut_controls": {
+    "intersection_factor_cases": 21808,
+    "kernel_identity_cases": 172,
+    "non_idempotent_control_rejected": true,
+    "simplex_projector_census": {
+      "2": {
+        "idempotent_sums": 7,
+        "ranks": [
+          0,
+          2
+        ],
+        "words": 256
+      },
+      "3": {
+        "idempotent_sums": 222,
+        "ranks": [
+          2,
+          4
+        ],
+        "words": 4096
+      }
+    }
+  },
+  "reusable_filter_controls": {
+    "fourteen-query-intersection-rejected": "REJECT_NECESSARY_CUT",
+    "invalid_query_frame": "REJECTED",
+    "shortest-repeat-rejected": "REJECT_NECESSARY_CUT",
+    "six-query-positive": "PASS_NECESSARY_CUTS_ONLY"
+  },
+  "simplex_controls": {
+    "max_main_fields": 64,
+    "private_stage_controls": 6448,
+    "sharp_local_capacities": 64,
+    "simplex_pairings": 47904
+  },
+  "status": "PASS_CALLER_STAGE_CAPACITY_CUTS"
+}
diff --git a/research/shortest-controller-stage-capacity/SOURCES.json b/research/shortest-controller-stage-capacity/SOURCES.json
new file mode 100644
index 0000000000..90eb0aef2b
--- /dev/null
+++ b/research/shortest-controller-stage-capacity/SOURCES.json
@@ -0,0 +1,50 @@
+{
+  "schema_version": 1,
+  "base_commit": "5e0052ca0aa3036a3afa8b0438927377c8d97d53",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "fc3d4ba105e1f097d0d7d051a308281e86ab1446",
+      "sha256": "66974efdced4083c00025f97d95d83909a226cdf801edb9301c195c6641f6903"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602",
+      "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72"
+    },
+    {
+      "path": "research/p104-productive-controller/RESULT.json",
+      "usage": "input",
+      "git_blob": "5637130d4a3884948eda39c185e3b6e8f4b4717b",
+      "sha256": "03e9f8424b9166899d3ae3b188d9defb851162a3183ecab237fb783d78216782"
+    },
+    {
+      "path": "research/productive-controller-basis-search/GLOBAL-PROOF.md",
+      "usage": "input",
+      "git_blob": "74b67e22e6c063193a83825207cdec19a8fef7a4",
+      "sha256": "adc377b13924701bf5b0b50b091d8b69c90195d50ce0f6808f7fb4c7e0b16457"
+    },
+    {
+      "path": "research/productive-controller-basis-search/algebra.py",
+      "usage": "input",
+      "git_blob": "2f0d4f290c280cfdfc17714009a2ae0f220556d4",
+      "sha256": "ab85b113cd70e20c38f6b0c0e0501876b751206bcd2a7ea5a61054ce3b92f2b2"
+    },
+    {
+      "path": "research/p104-helper-subspace-splits/RESULT.json",
+      "usage": "input",
+      "pin": "head:09dd0965711ca7eeb169057a420abab1c9052137:research/p104-helper-subspace-splits/RESULT.json",
+      "git_blob": "35f75c8555193c6e845cd52cc562ca23fd5924cb",
+      "sha256": "1d92e587915052110dfb3aca8890df5afdaf496164efa5a4a52e69ceeb3c70f3"
+    },
+    {
+      "path": "research/native-equality-cut/cuts.py",
+      "usage": "input",
+      "pin": "head:97db3fb45cd93a350e300781d75440d14e6a1f73:research/native-equality-cut/cuts.py",
+      "git_blob": "516e2b641e4329c79ce8a3065019e02e30ac8491",
+      "sha256": "14ee80e067f4db07464c5594841adef98cd4e098cfcf527b1a9b253dd6ae05d1"
+    }
+  ]
+}
diff --git a/research/shortest-controller-stage-capacity/TASK.json b/research/shortest-controller-stage-capacity/TASK.json
new file mode 100644
index 0000000000..622a884885
--- /dev/null
+++ b/research/shortest-controller-stage-capacity/TASK.json
@@ -0,0 +1,110 @@
+{
+  "schema_version": 1,
+  "task_id": "joint-query-controller",
+  "priority_revision": 7,
+  "base_commit": "5e0052ca0aa3036a3afa8b0438927377c8d97d53",
+  "original_card": {
+    "id": "joint-query-controller",
+    "question": "Can the installed QQ16 caller win a complete matched protocol bill, or can a changed demand eliminate actual paid work?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "research/qq16-caller-install/README.md"
+    ],
+    "methods": [
+      "Derive the matched whole-caller physical bill for installed and baseline protocols.",
+      "Change the actual demanded observations and prove a cheaper legal producer/consumer contract."
+    ],
+    "acceptance_gate": "Name the changed premise of the fixed F0/B1 observation obstruction. Show exactly which query is recovered, legal native reads and restoration, and a full favorable budget including cover maps, helpers and endpoints. Local inverse identities alone do not close the global controller. 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",
+        "scripts/research_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Read #4166 COST.md and ADMISSION.json. An actual caller connection is now proposed. Its native-component profile loses; parent park/restore versus external-call costs remain unresolved. Retain the producer and recovery lineage rather than rebuild it.",
+      "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately."
+    },
+    "first_experiment": "At the actual installed cut, compare matched complete parent park/restore and external input/return protocols at the same bank/packet geometry, including every later root call and service cost. Alternatively pin both bridge observations and derive a genuinely smaller source-compatible demand. Stop if the complete necessary inequality fails or an essential cost is unknown; no larger decoder scan from a local tape-action saving.",
+    "bottleneck_link": "The native local words exist; retained query information and its physical access are the missing link to a composed recursive interface.",
+    "allowed_variations": [
+      "One paid query, one changed first pair, or one precisely specified affine helper state.",
+      "A counterexample or lower bound for that exact proposed repair.",
+      "One unresolved obligation of a newer local decoder, with exact source heads and a distinct claim/domain."
+    ],
+    "scope_change_triggers": [
+      "Retaining the fixed first pair and ordinary schedule while allowing only homogeneous selected-only control, already excluded by the witness.",
+      "Treating cover-map counts as zero-cost physical address operations.",
+      "Recreating the pending complete local decoder or early-record/output-bank coalescing already under investigation without a distinct audit or changed premise.",
+      "Treating a completed-output defect inequality as a producer-interior, dirty-range or physical-cost certificate.",
+      "Recreating completed-output recovery or caller wiring already supplied by #4166 without new independent coverage.",
+      "Dropping retained later root calls or claiming native-profile dominance from the isolated publication saving."
+    ],
+    "overlap_terms": [
+      "QQ16",
+      "joint-query",
+      "changing-chart controller",
+      "selected observation",
+      "1969",
+      "2540",
+      "early record",
+      "output-bank retention",
+      "complete native decoder",
+      "2965",
+      "producer defect",
+      "dirty-helper range",
+      "F17 consumer",
+      "4166",
+      "qq16-caller-install"
+    ],
+    "existing_checks": [
+      {
+        "scope": "PR #4166: author-checked installed producer/service/return/bridge connection; native-component comparison loses.",
+        "evidence": "research/qq16-caller-install/README.md",
+        "remaining": "Complete matched physical protocol bill, or changed source-compatible demand/circuit; no affordable supplier yet.",
+        "status": "author-checked",
+        "source_commit": "0b082d22a0e9a442d264ab0633e35ef26c790630",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      }
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Derive query Gram rank and target-intersection cuts for changed whole caller words; price shortest arbitrary coordinate reuse and longer paired-stage P104 callers.",
+  "scope_change_reason": "The user explicitly requested a new global caller route using the equality cuts from PR5588. This changes the QQ16-specific card. Common advancing-stage searches led to a coordinate-reuse rank proof and a separate longer paired-stage obstruction; no QQ16 protocol task is claimed complete.",
+  "bottleneck_link": "A favorable recursive inventory is insufficient without an independent operator endpoint. These cuts bind achievable target ranks and their shared axes to the actual query frame before a large word search.",
+  "budget_minutes": 180,
+  "stop_rule": "Finish one source-bound reusable result with written proof, exact positive and negative controls, complete scoped prices and public handoff. A solver timeout or optimistic price does not satisfy this rule.",
+  "outcome": "negative-result",
+  "evidence": "PROOF.md Sections 2-8; RESULT.json; cuts.py and examples; retained discovery receipts. No kappa change. The general cuts and unbounded proofs are separate from finite controls.",
+  "author": "Ali Romman with substantial OpenAI Codex assistance",
+  "ai_assistance": "Substantial OpenAI Codex assistance for proof development, search programs, exact replay, documentation and publication. One agent; no independent human or proof-kernel review.",
+  "open_questions": [
+    {
+      "question": "Can the rank-two query complement force a stage-capacity loss that grows with caller size?",
+      "why_it_matters": "One lost occurrence rejects small paired callers but leaves a large-size relaxation open.",
+      "first_step": "Keep the off-diagonal intersection cuts with nonzero deficits and derive a target-incidence inequality.",
+      "blocked_by": "No quantitative packing theorem for unsaturated classes is supplied."
+    },
+    {
+      "question": "Can a caller with more queries, mixed calls or partially overlapping axes pass both cuts and a complete P104 price?",
+      "why_it_matters": "These changes escape at least one hypothesis of the complete negative bounds.",
+      "first_step": "Provide a binary query frame and proposed target sets to cuts.py before solving the full endpoint.",
+      "blocked_by": "Passing necessary cuts does not provide compatible projectors, physical maps or an endpoint."
+    },
+    {
+      "question": "Does a characteristic-zero caller with a common advancing operator exist with a favorable complete bill?",
+      "why_it_matters": "An unbounded-order stage is outside the involutive-axis theorem.",
+      "first_step": "Inspect the rational pair equations and exact n=2 positive control; change or solve the timed-out n=6 instance.",
+      "blocked_by": "The present rational searches have no favorable full word or native realization."
+    },
+    {
+      "question": "Does independent review accept the rank and intersection proof and the private-axis extension?",
+      "why_it_matters": "Finite verification does not certify the unbounded arguments.",
+      "first_step": "Read PROOF.md Sections 2, 4, 7 and 8 and replay the sharp and longer positive controls.",
+      "blocked_by": "No independent human or formal-kernel review has occurred."
+    }
+  ],
+  "refreshed_main_commit": "d7633ce230196a1d5d061347de7a0fd8be512ed6",
+  "coordination": "https://github.com/CrocSwap/integer-mult-bounds/discussions/5593"
+}
diff --git a/research/shortest-controller-stage-capacity/VALIDATION.md b/research/shortest-controller-stage-capacity/VALIDATION.md
new file mode 100644
index 0000000000..06b32dc49a
--- /dev/null
+++ b/research/shortest-controller-stage-capacity/VALIDATION.md
@@ -0,0 +1,36 @@
+# Verification record
+
+Prepared on 2026-10-25 on macOS arm64 with CPython 3.12.13.
+The registered package has no third-party dependency.
+
+The warning-strict registered command passed. It runs normal and isolated
+optimized verification in sequence. Both runs compare the complete output
+with the same committed RESULT.json. The five declared input byte streams
+pass their SHA256 and Git blob checks before source code is loaded.
+
+```sh
+python3.12 -W error -B scripts/research_package.py --package research/shortest-controller-stage-capacity
+```
+
+Markers: `PASS_CALLER_STAGE_CAPACITY_CUTS` and
+`PASS_REGISTERED_RESEARCH_PACKAGE`. The finite checks include two literal
+operator interpreters, 4,352 projector combinations, 47,904 simplex
+pairings, 21,808 intersection-factor cases, exact incidence maximization,
+the block-simplex capacity at q=104, two complete P104 price inputs and
+exact rational-power intervals. The fourteen-call relaxation passes the
+pinned PR5588 equality cuts; the new joint cut rejects its target geometry.
+
+The controls reject a deleted query, an invalid query frame and a
+non-idempotent use of the kernel identity. A six-query positive word
+detects an incorrect extension of the shortest bound. The reusable CLI
+accepts that word's necessary data and rejects both committed false targets.
+
+The direct source-export and publication checks are recorded after the
+committed export is made. No native source word, huge uniform compiler word,
+full integer multiplier, independent human review or proof-assistant kernel
+was run. Full-history provenance preflight was not run in this partial
+checkout; the required pinned source objects and bytes were checked.
+
+The optional discovery responses are retained in discovery/receipts.
+Solver timeouts are unknown, and no solver proof certificate is claimed.
+They are not dependencies of the written proof or registered replay.
diff --git a/research/shortest-controller-stage-capacity/VERIFY.json b/research/shortest-controller-stage-capacity/VERIFY.json
new file mode 100644
index 0000000000..8b0151ccaa
--- /dev/null
+++ b/research/shortest-controller-stage-capacity/VERIFY.json
@@ -0,0 +1,35 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/p104-productive-controller/RESULT.json",
+    "research/productive-controller-basis-search/GLOBAL-PROOF.md",
+    "research/productive-controller-basis-search/algebra.py",
+    "research/p104-helper-subspace-splits/RESULT.json",
+    "research/native-equality-cut/cuts.py"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Exact operator words, query Gram and rank controls, joint-axis packing, complete P104 concave and rational-power bounds, and committed receipt equality"
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-O",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Optimized isolated replay must equal the same committed scientific result"
+    }
+  ]
+}
diff --git a/research/shortest-controller-stage-capacity/cuts.py b/research/shortest-controller-stage-capacity/cuts.py
new file mode 100644
index 0000000000..9c1f001a1c
--- /dev/null
+++ b/research/shortest-controller-stage-capacity/cuts.py
@@ -0,0 +1,87 @@
+#!/usr/bin/env python3
+"""Screen a binary query frame and proposed target axis sets.
+
+Ali Romman, with substantial OpenAI Codex assistance. Apache-2.0.
+Passing these necessary cuts does not certify an operator word or a price.
+"""
+import argparse
+from itertools import combinations
+import json
+from pathlib import Path
+
+
+def require(condition, message):
+    if not condition:
+        raise ValueError(message)
+
+
+def rank(rows):
+    rows = list(rows)
+    pivot = 0
+    for bit in range(max(rows, default=0).bit_length()-1, -1, -1):
+        chosen = next((i for i in range(pivot, len(rows)) if rows[i] >> bit & 1), None)
+        if chosen is None:
+            continue
+        rows[pivot], rows[chosen] = rows[chosen], rows[pivot]
+        for i in range(pivot+1, len(rows)):
+            if rows[i] >> bit & 1:
+                rows[i] ^= rows[pivot]
+        pivot += 1
+    return pivot
+
+
+def audit(candidate):
+    n, us, vs = candidate['n'], candidate['u'], candidate['v']
+    require(type(n) is int and n > 0, 'n must be a positive integer')
+    require(len(us) == len(vs) and len(us) > n, 'A query frame needs L>n terms')
+    require(all(type(x) is int and 0 < x < (1 << n) for x in us+vs), 'Invalid query vector')
+    require(all((u & v).bit_count() % 2 == 0 for u, v in zip(us, vs)), 'Non-nilpotent query')
+    total = [0]*n
+    for u, v in zip(us, vs):
+        for j in range(n):
+            if u >> j & 1:
+                total[j] ^= v
+    require(total == [1 << i for i in range(n)], 'Query frame does not sum to identity')
+    gram = [sum(((v & u).bit_count() % 2) << i for i, u in enumerate(us)) for v in vs]
+    axes, singles, failures = [], [], []
+    for axis in candidate['axes']:
+        calls, outputs = axis['calls'], axis['outputs']
+        idles = axis.get('idle_terms', 0)
+        require(len(calls) == len(set(calls)) and len(outputs) == len(set(outputs)), 'Duplicate index')
+        require(all(type(i) is int and 0 <= i < len(us) for i in calls), 'Invalid call index')
+        require(all(type(i) is int and 0 <= i < n for i in outputs), 'Invalid output index')
+        require(type(idles) is int and idles >= 0, 'Invalid idle count')
+        require(all(axis['name'] != a['name'] for a in axes), 'Duplicate axis name')
+        block = [sum(((gram[i] >> j) & 1) << t for t, j in enumerate(calls)) for i in calls]
+        block_rank = rank(block)
+        capacity = 2*len(calls)+idles-block_rank
+        deficit = 2*len(calls)+idles-len(outputs)
+        singles.append({'axis': axis['name'], 'target_count': len(outputs),
+                        'capacity': capacity, 'gram_rank': block_rank})
+        if len(outputs) > capacity:
+            failures.append({'kind': 'axis_capacity', 'axis': axis['name'],
+                             'requested': len(outputs), 'maximum': capacity})
+        axes.append({**axis, 'deficit': deficit})
+    intersections = []
+    for a, b in combinations(axes, 2):
+        block = [sum(((gram[i] >> j) & 1) << t for t, j in enumerate(b['calls']))
+                 for i in a['calls']]
+        demand = max(0, rank(block)-a['deficit']-b['deficit'])
+        actual = len(set(a['outputs']) & set(b['outputs']))
+        intersections.append({'axes': [a['name'], b['name']], 'required': demand, 'actual': actual})
+        if actual < demand:
+            failures.append({'kind': 'axis_intersection', 'axes': [a['name'], b['name']],
+                             'requested': actual, 'minimum': demand})
+    return {'status': 'REJECT_NECESSARY_CUT' if failures else 'PASS_NECESSARY_CUTS_ONLY',
+            'n': n, 'query_count': len(us), 'query_surplus': len(us)-n,
+            'single_axis': singles, 'intersections': intersections, 'failures': failures,
+            'limits': 'Assumes compatible full projectors and independent target jobs. Does not construct them or price helpers, native maps, scalar work or compiler costs.'}
+
+
+if __name__ == '__main__':
+    parser = argparse.ArgumentParser(description=__doc__)
+    parser.add_argument('candidate', type=Path)
+    args = parser.parse_args()
+    result = audit(json.loads(args.candidate.read_text()))
+    print(json.dumps(result, indent=2, sort_keys=True))
+    raise SystemExit(bool(result['failures']))
diff --git a/research/shortest-controller-stage-capacity/discovery/README.md b/research/shortest-controller-stage-capacity/discovery/README.md
new file mode 100644
index 0000000000..1383e34668
--- /dev/null
+++ b/research/shortest-controller-stage-capacity/discovery/README.md
@@ -0,0 +1,80 @@
+# Discovery record
+
+These files preserve the searches that led to the rank cuts. They are not
+part of the registered proof replay and do not establish a physical caller.
+No positive kappa result was found. The proof does not depend on solver trust.
+
+## Common advancing stage
+
+The initial idea used U=S*H8, where S moves the next eight-axis block and
+fixes the central query axis. Before wraparound, U^d can retain 8d transverse
+axes. This can escape the fixed involution D^2=I. It does not supply the
+scalar controller needed to extract independent outputs.
+
+`simplex_search.cpp` enumerates compatible binary projectors on four fields
+and five normalized query positions. It treats D as a formal variable.
+`simplex-census.json` covers all 32 full/thin masks. For the all-full mask,
+all 16^5=1,048,576 choices fail the central-query endpoint. Every mask with
+three or more full calls fails the complete coefficient-factor test.
+
+```sh
+c++ -std=c++17 -O3 research/shortest-controller-stage-capacity/discovery/simplex_search.cpp -o /tmp/imb-simplex-search
+/tmp/imb-simplex-search 31 0
+```
+
+The signed census tests the all-full mask with inverse masks 0 through 15.
+It is not a recorded enumeration of all 32 inverse masks. Some words factor,
+but their retained degrees lose the optimistic profile. The command takes
+the full mask first and inverse mask second. Do not reinterpret a normalized
+degree as free inverse-stage work.
+
+The Python discovery programs used Python 3.12, z3-solver 5.3.2.0 and sympy
+1.14.0. The exact environment and raw responses are in `receipts/`.
+`pair_search.py` checks necessary pair equations for a common positive
+formal D. At n=4,6,8 the solver returned `unsat`; at n=10 it timed out.
+Leading-only and tangent-only controls are satisfiable. No solver proof
+certificate was exported. The pair equations do not themselves construct
+or diagonalize a full word.
+
+```sh
+python3 pair_search.py --n 6 --seconds 60 --output /tmp/pair6.json
+python3 pair_search.py --n 6 --seconds 60 --constraint tangent --output /tmp/pair6-tangent.json
+```
+
+Run these commands from this directory with the optional dependencies
+installed. `solve.py` instead expands the whole query polynomial. The
+four-field query screen returned `unsat`; six-field query and balanced
+endpoint screens timed out. `rational_pair_search.py` tests a rational
+analogue: n=2 is satisfiable, n=4 returned `unsat`, and n=6 timed out.
+These are bounded discovery statements, not characteristic-zero theorems.
+
+## Relations and coordinate reuse
+
+`relation_search.py` imposes involutive stage labels. The tested single
+relation on three interior stages at n=4, and on five at n=6, returned
+`unsat`. The saved `colour-query-search.json` contains all 52 set partitions
+of five interior stage positions: 17 returned `sat` and 35 `unsat`, with
+no unknown response in that run. Each partition used a three-second limit.
+The positive responses are query-equation witnesses, not full endpoints.
+
+In particular, label patterns `[0,1,1,1,0]` and `[0,1,1,1,2]` pass those
+equations. They invalidate the tempting claim that adjacent equal-label
+cancellation must reduce every successful query pattern to one letter.
+This failure led to a rank-capacity proof instead of a word-reduction claim.
+
+`search_cuts.py` tests a separate finite linear-subspace cut. With seed 5593,
+100 random common stages and all 1,395 three-dimensional subspaces of F2^6
+gave 139,500 tests and no positive separator for the balanced six-field
+profile. This is a failed finite separator search, not a universal barrier.
+
+```sh
+python3 relation_search.py --n 6 --seconds 60 --output /tmp/relation6.json
+python3 relation_search.py --n 6 --seconds 3 --labels 1,2,2,2,1 --output /tmp/colour-control.json
+python3 search_cuts.py --half 3 --rounds 100 --seed 5593 --output /tmp/subspace-cut.json
+```
+
+The registered verifier uses neither these solver responses nor their
+search bounds. The retained rigorous result is in `../PROOF.md`. The
+advancing operator route remains open; the involutive-axis theorem does
+not exclude it. New work is by Ali Romman with substantial OpenAI Codex
+assistance, with Cinna Davis's simplex and query-frame lineage. Apache-2.0.
diff --git a/research/shortest-controller-stage-capacity/discovery/colour-query-search.json b/research/shortest-controller-stage-capacity/discovery/colour-query-search.json
new file mode 100644
index 0000000000..0ff3e2d240
--- /dev/null
+++ b/research/shortest-controller-stage-capacity/discovery/colour-query-search.json
@@ -0,0 +1,1860 @@
+[
+  {
+    "full_calls": 7,
+    "interior_projectors": {
+      "1": [
+        61,
+        14,
+        0,
+        0,
+        61,
+        61
+      ],
+      "2": [
+        59,
+        59,
+        31,
+        59,
+        59,
+        59
+      ],
+      "3": [
+        0,
+        55,
+        55,
+        25,
+        0,
+        55
+      ],
+      "4": [
+        47,
+        47,
+        0,
+        47,
+        55,
+        0
+      ],
+      "5": [
+        0,
+        31,
+        0,
+        31,
+        31,
+        37
+      ]
+    },
+    "labels": {
+      "1": 1,
+      "2": 1,
+      "3": 1,
+      "4": 1,
+      "5": 1
+    },
+    "n": 6,
+    "partition": [
+      0,
+      0,
+      0,
+      0,
+      0
+    ],
+    "scope": "binary query equations with involutive stages; no endpoint or rank admission",
+    "solver_result": "sat",
+    "timeout_seconds": 3,
+    "z3_version": "5.3.2"
+  },
+  {
+    "full_calls": 7,
+    "interior_projectors": {
+      "1": [
+        0,
+        42,
+        0,
+        0,
+        61,
+        0
+      ],
+      "2": [
+        0,
+        59,
+        47,
+        59,
+        59,
+        0
+      ],
+      "3": [
+        0,
+        55,
+        0,
+        9,
+        0,
+        0
+      ],
+      "4": [
+        47,
+        0,
+        47,
+        47,
+        50,
+        0
+      ],
+      "5": [
+        31,
+        31,
+        31,
+        31,
+        31,
+        32
+      ]
+    },
+    "labels": {
+      "1": 1,
+      "2": 1,
+      "3": 1,
+      "4": 1,
+      "5": 2
+    },
+    "n": 6,
+    "partition": [
+      0,
+      0,
+      0,
+      0,
+      1
+    ],
+    "scope": "binary query equations with involutive stages; no endpoint or rank admission",
+    "solver_result": "sat",
+    "timeout_seconds": 3,
+    "z3_version": "5.3.2"
+  },
+  {
+    "full_calls": 7,
+    "labels": {
+      "1": 1,
+      "2": 1,
+      "3": 1,
+      "4": 2,
+      "5": 1
+    },
+    "n": 6,
+    "partition": [
+      0,
+      0,
+      0,
+      1,
+      0
+    ],
+    "scope": "binary query equations with involutive stages; no endpoint or rank admission",
+    "solver_result": "unsat",
+    "timeout_seconds": 3,
+    "z3_version": "5.3.2"
+  },
+  {
+    "full_calls": 7,
+    "interior_projectors": {
+      "1": [
+        0,
+        50,
+        0,
+        61,
+        0,
+        0
+      ],
+      "2": [
+        59,
+        59,
+        62,
+        59,
+        0,
+        0
+      ],
+      "3": [
+        55,
+        0,
+        0,
+        10,
+        0,
+        0
+      ],
+      "4": [
+        0,
+        0,
+        0,
+        0,
+        31,
+        47
+      ],
+      "5": [
+        0,
+        0,
+        0,
+        0,
+        31,
+        47
+      ]
+    },
+    "labels": {
+      "1": 1,
+      "2": 1,
+      "3": 1,
+      "4": 2,
+      "5": 2
+    },
+    "n": 6,
+    "partition": [
+      0,
+      0,
+      0,
+      1,
+      1
+    ],
+    "scope": "binary query equations with involutive stages; no endpoint or rank admission",
+    "solver_result": "sat",
+    "timeout_seconds": 3,
+    "z3_version": "5.3.2"
+  },
+  {
+    "full_calls": 7,
+    "labels": {
+      "1": 1,
+      "2": 1,
+      "3": 1,
+      "4": 2,
+      "5": 4
+    },
+    "n": 6,
+    "partition": [
+      0,
+      0,
+      0,
+      1,
+      2
+    ],
+    "scope": "binary query equations with involutive stages; no endpoint or rank admission",
+    "solver_result": "unsat",
+    "timeout_seconds": 3,
+    "z3_version": "5.3.2"
+  },
+  {
+    "full_calls": 7,
+    "interior_projectors": {
+      "1": [
+        0,
+        59,
+        61,
+        0,
+        0,
+        0
+      ],
+      "2": [
+        59,
+        0,
+        6,
+        59,
+        59,
+        0
+      ],
+      "3": [
+        55,
+        55,
+        55,
+        56,
+        0,
+        0
+      ],
+      "4": [
+        0,
+        0,
+        0,
+        0,
+        28,
+        47
+      ],
+      "5": [
+        0,
+        0,
+        0,
+        0,
+        31,
+        47
+      ]
+    },
+    "labels": {
+      "1": 1,
+      "2": 1,
+      "3": 2,
+      "4": 1,
+      "5": 1
+    },
+    "n": 6,
+    "partition": [
+      0,
+      0,
+      1,
+      0,
+      0
+    ],
+    "scope": "binary query equations with involutive stages; no endpoint or rank admission",
+    "solver_result": "sat",
+    "timeout_seconds": 3,
+    "z3_version": "5.3.2"
+  },
+  {
+    "full_calls": 7,
+    "labels": {
+      "1": 1,
+      "2": 1,
+      "3": 2,
+      "4": 1,
+      "5": 2
+    },
+    "n": 6,
+    "partition": [
+      0,
+      0,
+      1,
+      0,
+      1
+    ],
+    "scope": "binary query equations with involutive stages; no endpoint or rank admission",
+    "solver_result": "unsat",
+    "timeout_seconds": 3,
+    "z3_version": "5.3.2"
+  },
+  {
+    "full_calls": 7,
+    "labels": {
+      "1": 1,
+      "2": 1,
+      "3": 2,
+      "4": 1,
+      "5": 4
+    },
+    "n": 6,
+    "partition": [
+      0,
+      0,
+      1,
+      0,
+      2
+    ],
+    "scope": "binary query equations with involutive stages; no endpoint or rank admission",
+    "solver_result": "unsat",
+    "timeout_seconds": 3,
+    "z3_version": "5.3.2"
+  },
+  {
+    "full_calls": 7,
+    "interior_projectors": {
+      "1": [
+        0,
+        3,
+        61,
+        0,
+        0,
+        0
+      ],
+      "2": [
+        0,
+        0,
+        6,
+        59,
+        59,
+        59
+      ],
+      "3": [
+        0,
+        0,
+        0,
+        47,
+        55,
+        0
+      ],
+      "4": [
+        0,
+        0,
+        0,
+        47,
+        55,
+        0
+      ],
+      "5": [
+        31,
+        31,
+        31,
+        31,
+        31,
+        35
+      ]
+    },
+    "labels": {
+      "1": 1,
+      "2": 1,
+      "3": 2,
+      "4": 2,
+      "5": 1
+    },
+    "n": 6,
+    "partition": [
+      0,
+      0,
+      1,
+      1,
+      0
+    ],
+    "scope": "binary query equations with involutive stages; no endpoint or rank admission",
+    "solver_result": "sat",
+    "timeout_seconds": 3,
+    "z3_version": "5.3.2"
+  },
+  {
+    "full_calls": 7,
+    "interior_projectors": {
+      "1": [
+        0,
+        59,
+        61,
+        0,
+        0,
+        0
+      ],
+      "2": [
+        0,
+        59,
+        61,
+        0,
+        0,
+        0
+      ],
+      "3": [
+        55,
+        55,
+        55,
+        31,
+        55,
+        55
+      ],
+      "4": [
+        0,
+        0,
+        0,
+        47,
+        48,
+        0
+      ],
+      "5": [
+        0,
+        0,
+        0,
+        31,
+        0,
+        39
+      ]
+    },
+    "labels": {
+      "1": 1,
+      "2": 1,
+      "3": 2,
+      "4": 2,
+      "5": 2
+    },
+    "n": 6,
+    "partition": [
+      0,
+      0,
+      1,
+      1,
+      1
+    ],
+    "scope": "binary query equations with involutive stages; no endpoint or rank admission",
+    "solver_result": "sat",
+    "timeout_seconds": 3,
+    "z3_version": "5.3.2"
+  },
+  {
+    "full_calls": 7,
+    "interior_projectors": {
+      "1": [
+        0,
+        59,
+        61,
+        0,
+        0,
+        0
+      ],
+      "2": [
+        0,
+        59,
+        61,
+        0,
+        0,
+        0
+      ],
+      "3": [
+        0,
+        0,
+        0,
+        47,
+        55,
+        0
+      ],
+      "4": [
+        0,
+        0,
+        0,
+        47,
+        55,
+        0
+      ],
+      "5": [
+        31,
+        31,
+        31,
+        31,
+        31,
+        32
+      ]
+    },
+    "labels": {
+      "1": 1,
+      "2": 1,
+      "3": 2,
+      "4": 2,
+      "5": 4
+    },
+    "n": 6,
+    "partition": [
+      0,
+      0,
+      1,
+      1,
+      2
+    ],
+    "scope": "binary query equations with involutive stages; no endpoint or rank admission",
+    "solver_result": "sat",
+    "timeout_seconds": 3,
+    "z3_version": "5.3.2"
+  },
+  {
+    "full_calls": 7,
+    "labels": {
+      "1": 1,
+      "2": 1,
+      "3": 2,
+      "4": 4,
+      "5": 1
+    },
+    "n": 6,
+    "partition": [
+      0,
+      0,
+      1,
+      2,
+      0
+    ],
+    "scope": "binary query equations with involutive stages; no endpoint or rank admission",
+    "solver_result": "unsat",
+    "timeout_seconds": 3,
+    "z3_version": "5.3.2"
+  },
+  {
+    "full_calls": 7,
+    "labels": {
+      "1": 1,
+      "2": 1,
+      "3": 2,
+      "4": 4,
+      "5": 2
+    },
+    "n": 6,
+    "partition": [
+      0,
+      0,
+      1,
+      2,
+      1
+    ],
+    "scope": "binary query equations with involutive stages; no endpoint or rank admission",
+    "solver_result": "unsat",
+    "timeout_seconds": 3,
+    "z3_version": "5.3.2"
+  },
+  {
+    "full_calls": 7,
+    "interior_projectors": {
+      "1": [
+        0,
+        59,
+        61,
+        0,
+        0,
+        0
+      ],
+      "2": [
+        0,
+        59,
+        61,
+        0,
+        0,
+        0
+      ],
+      "3": [
+        55,
+        55,
+        55,
+        56,
+        0,
+        0
+      ],
+      "4": [
+        0,
+        0,
+        0,
+        0,
+        31,
+        47
+      ],
+      "5": [
+        0,
+        0,
+        0,
+        0,
+        31,
+        47
+      ]
+    },
+    "labels": {
+      "1": 1,
+      "2": 1,
+      "3": 2,
+      "4": 4,
+      "5": 4
+    },
+    "n": 6,
+    "partition": [
+      0,
+      0,
+      1,
+      2,
+      2
+    ],
+    "scope": "binary query equations with involutive stages; no endpoint or rank admission",
+    "solver_result": "sat",
+    "timeout_seconds": 3,
+    "z3_version": "5.3.2"
+  },
+  {
+    "full_calls": 7,
+    "labels": {
+      "1": 1,
+      "2": 1,
+      "3": 2,
+      "4": 4,
+      "5": 8
+    },
+    "n": 6,
+    "partition": [
+      0,
+      0,
+      1,
+      2,
+      3
+    ],
+    "scope": "binary query equations with involutive stages; no endpoint or rank admission",
+    "solver_result": "unsat",
+    "timeout_seconds": 3,
+    "z3_version": "5.3.2"
+  },
+  {
+    "full_calls": 7,
+    "labels": {
+      "1": 1,
+      "2": 2,
+      "3": 1,
+      "4": 1,
+      "5": 1
+    },
+    "n": 6,
+    "partition": [
+      0,
+      1,
+      0,
+      0,
+      0
+    ],
+    "scope": "binary query equations with involutive stages; no endpoint or rank admission",
+    "solver_result": "unsat",
+    "timeout_seconds": 3,
+    "z3_version": "5.3.2"
+  },
+  {
+    "full_calls": 7,
+    "interior_projectors": {
+      "1": [
+        61,
+        62,
+        0,
+        0,
+        0,
+        0
+      ],
+      "2": [
+        0,
+        0,
+        7,
+        59,
+        59,
+        59
+      ],
+      "3": [
+        0,
+        0,
+        0,
+        47,
+        55,
+        0
+      ],
+      "4": [
+        0,
+        0,
+        0,
+        47,
+        55,
+        0
+      ],
+      "5": [
+        0,
+        0,
+        31,
+        31,
+        31,
+        35
+      ]
+    },
+    "labels": {
+      "1": 1,
+      "2": 2,
+      "3": 1,
+      "4": 1,
+      "5": 2
+    },
+    "n": 6,
+    "partition": [
+      0,
+      1,
+      0,
+      0,
+      1
+    ],
+    "scope": "binary query equations with involutive stages; no endpoint or rank admission",
+    "solver_result": "sat",
+    "timeout_seconds": 3,
+    "z3_version": "5.3.2"
+  },
+  {
+    "full_calls": 7,
+    "labels": {
+      "1": 1,
+      "2": 2,
+      "3": 1,
+      "4": 1,
+      "5": 4
+    },
+    "n": 6,
+    "partition": [
+      0,
+      1,
+      0,
+      0,
+      2
+    ],
+    "scope": "binary query equations with involutive stages; no endpoint or rank admission",
+    "solver_result": "unsat",
+    "timeout_seconds": 3,
+    "z3_version": "5.3.2"
+  },
+  {
+    "full_calls": 7,
+    "labels": {
+      "1": 1,
+      "2": 2,
+      "3": 1,
+      "4": 2,
+      "5": 1
+    },
+    "n": 6,
+    "partition": [
+      0,
+      1,
+      0,
+      1,
+      0
+    ],
+    "scope": "binary query equations with involutive stages; no endpoint or rank admission",
+    "solver_result": "unsat",
+    "timeout_seconds": 3,
+    "z3_version": "5.3.2"
+  },
+  {
+    "full_calls": 7,
+    "labels": {
+      "1": 1,
+      "2": 2,
+      "3": 1,
+      "4": 2,
+      "5": 2
+    },
+    "n": 6,
+    "partition": [
+      0,
+      1,
+      0,
+      1,
+      1
+    ],
+    "scope": "binary query equations with involutive stages; no endpoint or rank admission",
+    "solver_result": "unsat",
+    "timeout_seconds": 3,
+    "z3_version": "5.3.2"
+  },
+  {
+    "full_calls": 7,
+    "labels": {
+      "1": 1,
+      "2": 2,
+      "3": 1,
+      "4": 2,
+      "5": 4
+    },
+    "n": 6,
+    "partition": [
+      0,
+      1,
+      0,
+      1,
+      2
+    ],
+    "scope": "binary query equations with involutive stages; no endpoint or rank admission",
+    "solver_result": "unsat",
+    "timeout_seconds": 3,
+    "z3_version": "5.3.2"
+  },
+  {
+    "full_calls": 7,
+    "labels": {
+      "1": 1,
+      "2": 2,
+      "3": 1,
+      "4": 4,
+      "5": 1
+    },
+    "n": 6,
+    "partition": [
+      0,
+      1,
+      0,
+      2,
+      0
+    ],
+    "scope": "binary query equations with involutive stages; no endpoint or rank admission",
+    "solver_result": "unsat",
+    "timeout_seconds": 3,
+    "z3_version": "5.3.2"
+  },
+  {
+    "full_calls": 7,
+    "labels": {
+      "1": 1,
+      "2": 2,
+      "3": 1,
+      "4": 4,
+      "5": 2
+    },
+    "n": 6,
+    "partition": [
+      0,
+      1,
+      0,
+      2,
+      1
+    ],
+    "scope": "binary query equations with involutive stages; no endpoint or rank admission",
+    "solver_result": "unsat",
+    "timeout_seconds": 3,
+    "z3_version": "5.3.2"
+  },
+  {
+    "full_calls": 7,
+    "labels": {
+      "1": 1,
+      "2": 2,
+      "3": 1,
+      "4": 4,
+      "5": 4
+    },
+    "n": 6,
+    "partition": [
+      0,
+      1,
+      0,
+      2,
+      2
+    ],
+    "scope": "binary query equations with involutive stages; no endpoint or rank admission",
+    "solver_result": "unsat",
+    "timeout_seconds": 3,
+    "z3_version": "5.3.2"
+  },
+  {
+    "full_calls": 7,
+    "labels": {
+      "1": 1,
+      "2": 2,
+      "3": 1,
+      "4": 4,
+      "5": 8
+    },
+    "n": 6,
+    "partition": [
+      0,
+      1,
+      0,
+      2,
+      3
+    ],
+    "scope": "binary query equations with involutive stages; no endpoint or rank admission",
+    "solver_result": "unsat",
+    "timeout_seconds": 3,
+    "z3_version": "5.3.2"
+  },
+  {
+    "full_calls": 7,
+    "interior_projectors": {
+      "1": [
+        61,
+        31,
+        61,
+        61,
+        61,
+        61
+      ],
+      "2": [
+        0,
+        0,
+        55,
+        59,
+        0,
+        0
+      ],
+      "3": [
+        0,
+        0,
+        55,
+        59,
+        0,
+        0
+      ],
+      "4": [
+        47,
+        0,
+        0,
+        0,
+        16,
+        0
+      ],
+      "5": [
+        0,
+        31,
+        31,
+        31,
+        0,
+        33
+      ]
+    },
+    "labels": {
+      "1": 1,
+      "2": 2,
+      "3": 2,
+      "4": 1,
+      "5": 1
+    },
+    "n": 6,
+    "partition": [
+      0,
+      1,
+      1,
+      0,
+      0
+    ],
+    "scope": "binary query equations with involutive stages; no endpoint or rank admission",
+    "solver_result": "sat",
+    "timeout_seconds": 3,
+    "z3_version": "5.3.2"
+  },
+  {
+    "full_calls": 7,
+    "interior_projectors": {
+      "1": [
+        0,
+        35,
+        61,
+        61,
+        61,
+        0
+      ],
+      "2": [
+        0,
+        0,
+        55,
+        59,
+        0,
+        0
+      ],
+      "3": [
+        0,
+        0,
+        55,
+        59,
+        0,
+        0
+      ],
+      "4": [
+        0,
+        47,
+        47,
+        47,
+        49,
+        0
+      ],
+      "5": [
+        31,
+        31,
+        31,
+        31,
+        31,
+        32
+      ]
+    },
+    "labels": {
+      "1": 1,
+      "2": 2,
+      "3": 2,
+      "4": 1,
+      "5": 2
+    },
+    "n": 6,
+    "partition": [
+      0,
+      1,
+      1,
+      0,
+      1
+    ],
+    "scope": "binary query equations with involutive stages; no endpoint or rank admission",
+    "solver_result": "sat",
+    "timeout_seconds": 3,
+    "z3_version": "5.3.2"
+  },
+  {
+    "full_calls": 7,
+    "interior_projectors": {
+      "1": [
+        0,
+        35,
+        61,
+        61,
+        61,
+        0
+      ],
+      "2": [
+        0,
+        0,
+        55,
+        59,
+        0,
+        0
+      ],
+      "3": [
+        0,
+        0,
+        55,
+        59,
+        0,
+        0
+      ],
+      "4": [
+        0,
+        47,
+        47,
+        47,
+        49,
+        0
+      ],
+      "5": [
+        31,
+        31,
+        31,
+        31,
+        31,
+        32
+      ]
+    },
+    "labels": {
+      "1": 1,
+      "2": 2,
+      "3": 2,
+      "4": 1,
+      "5": 4
+    },
+    "n": 6,
+    "partition": [
+      0,
+      1,
+      1,
+      0,
+      2
+    ],
+    "scope": "binary query equations with involutive stages; no endpoint or rank admission",
+    "solver_result": "sat",
+    "timeout_seconds": 3,
+    "z3_version": "5.3.2"
+  },
+  {
+    "full_calls": 7,
+    "interior_projectors": {
+      "1": [
+        61,
+        62,
+        0,
+        0,
+        0,
+        0
+      ],
+      "2": [
+        0,
+        0,
+        23,
+        59,
+        0,
+        0
+      ],
+      "3": [
+        55,
+        55,
+        0,
+        44,
+        55,
+        0
+      ],
+      "4": [
+        47,
+        47,
+        0,
+        47,
+        55,
+        0
+      ],
+      "5": [
+        31,
+        31,
+        31,
+        31,
+        31,
+        32
+      ]
+    },
+    "labels": {
+      "1": 1,
+      "2": 2,
+      "3": 2,
+      "4": 2,
+      "5": 1
+    },
+    "n": 6,
+    "partition": [
+      0,
+      1,
+      1,
+      1,
+      0
+    ],
+    "scope": "binary query equations with involutive stages; no endpoint or rank admission",
+    "solver_result": "sat",
+    "timeout_seconds": 3,
+    "z3_version": "5.3.2"
+  },
+  {
+    "full_calls": 7,
+    "interior_projectors": {
+      "1": [
+        61,
+        62,
+        0,
+        0,
+        0,
+        0
+      ],
+      "2": [
+        59,
+        59,
+        28,
+        0,
+        0,
+        59
+      ],
+      "3": [
+        55,
+        55,
+        55,
+        56,
+        0,
+        0
+      ],
+      "4": [
+        47,
+        47,
+        0,
+        0,
+        28,
+        47
+      ],
+      "5": [
+        31,
+        31,
+        0,
+        0,
+        31,
+        44
+      ]
+    },
+    "labels": {
+      "1": 1,
+      "2": 2,
+      "3": 2,
+      "4": 2,
+      "5": 2
+    },
+    "n": 6,
+    "partition": [
+      0,
+      1,
+      1,
+      1,
+      1
+    ],
+    "scope": "binary query equations with involutive stages; no endpoint or rank admission",
+    "solver_result": "sat",
+    "timeout_seconds": 3,
+    "z3_version": "5.3.2"
+  },
+  {
+    "full_calls": 7,
+    "interior_projectors": {
+      "1": [
+        61,
+        62,
+        0,
+        0,
+        0,
+        0
+      ],
+      "2": [
+        0,
+        0,
+        23,
+        59,
+        0,
+        0
+      ],
+      "3": [
+        55,
+        55,
+        0,
+        44,
+        55,
+        0
+      ],
+      "4": [
+        47,
+        47,
+        0,
+        47,
+        55,
+        0
+      ],
+      "5": [
+        31,
+        31,
+        31,
+        31,
+        31,
+        32
+      ]
+    },
+    "labels": {
+      "1": 1,
+      "2": 2,
+      "3": 2,
+      "4": 2,
+      "5": 4
+    },
+    "n": 6,
+    "partition": [
+      0,
+      1,
+      1,
+      1,
+      2
+    ],
+    "scope": "binary query equations with involutive stages; no endpoint or rank admission",
+    "solver_result": "sat",
+    "timeout_seconds": 3,
+    "z3_version": "5.3.2"
+  },
+  {
+    "full_calls": 7,
+    "labels": {
+      "1": 1,
+      "2": 2,
+      "3": 2,
+      "4": 4,
+      "5": 1
+    },
+    "n": 6,
+    "partition": [
+      0,
+      1,
+      1,
+      2,
+      0
+    ],
+    "scope": "binary query equations with involutive stages; no endpoint or rank admission",
+    "solver_result": "unsat",
+    "timeout_seconds": 3,
+    "z3_version": "5.3.2"
+  },
+  {
+    "full_calls": 7,
+    "labels": {
+      "1": 1,
+      "2": 2,
+      "3": 2,
+      "4": 4,
+      "5": 2
+    },
+    "n": 6,
+    "partition": [
+      0,
+      1,
+      1,
+      2,
+      1
+    ],
+    "scope": "binary query equations with involutive stages; no endpoint or rank admission",
+    "solver_result": "unsat",
+    "timeout_seconds": 3,
+    "z3_version": "5.3.2"
+  },
+  {
+    "full_calls": 7,
+    "interior_projectors": {
+      "1": [
+        61,
+        62,
+        0,
+        0,
+        0,
+        0
+      ],
+      "2": [
+        0,
+        0,
+        55,
+        59,
+        0,
+        0
+      ],
+      "3": [
+        0,
+        0,
+        55,
+        59,
+        0,
+        0
+      ],
+      "4": [
+        0,
+        0,
+        0,
+        0,
+        31,
+        47
+      ],
+      "5": [
+        0,
+        0,
+        0,
+        0,
+        31,
+        47
+      ]
+    },
+    "labels": {
+      "1": 1,
+      "2": 2,
+      "3": 2,
+      "4": 4,
+      "5": 4
+    },
+    "n": 6,
+    "partition": [
+      0,
+      1,
+      1,
+      2,
+      2
+    ],
+    "scope": "binary query equations with involutive stages; no endpoint or rank admission",
+    "solver_result": "sat",
+    "timeout_seconds": 3,
+    "z3_version": "5.3.2"
+  },
+  {
+    "full_calls": 7,
+    "labels": {
+      "1": 1,
+      "2": 2,
+      "3": 2,
+      "4": 4,
+      "5": 8
+    },
+    "n": 6,
+    "partition": [
+      0,
+      1,
+      1,
+      2,
+      3
+    ],
+    "scope": "binary query equations with involutive stages; no endpoint or rank admission",
+    "solver_result": "unsat",
+    "timeout_seconds": 3,
+    "z3_version": "5.3.2"
+  },
+  {
+    "full_calls": 7,
+    "labels": {
+      "1": 1,
+      "2": 2,
+      "3": 4,
+      "4": 1,
+      "5": 1
+    },
+    "n": 6,
+    "partition": [
+      0,
+      1,
+      2,
+      0,
+      0
+    ],
+    "scope": "binary query equations with involutive stages; no endpoint or rank admission",
+    "solver_result": "unsat",
+    "timeout_seconds": 3,
+    "z3_version": "5.3.2"
+  },
+  {
+    "full_calls": 7,
+    "labels": {
+      "1": 1,
+      "2": 2,
+      "3": 4,
+      "4": 1,
+      "5": 2
+    },
+    "n": 6,
+    "partition": [
+      0,
+      1,
+      2,
+      0,
+      1
+    ],
+    "scope": "binary query equations with involutive stages; no endpoint or rank admission",
+    "solver_result": "unsat",
+    "timeout_seconds": 3,
+    "z3_version": "5.3.2"
+  },
+  {
+    "full_calls": 7,
+    "labels": {
+      "1": 1,
+      "2": 2,
+      "3": 4,
+      "4": 1,
+      "5": 4
+    },
+    "n": 6,
+    "partition": [
+      0,
+      1,
+      2,
+      0,
+      2
+    ],
+    "scope": "binary query equations with involutive stages; no endpoint or rank admission",
+    "solver_result": "unsat",
+    "timeout_seconds": 3,
+    "z3_version": "5.3.2"
+  },
+  {
+    "full_calls": 7,
+    "labels": {
+      "1": 1,
+      "2": 2,
+      "3": 4,
+      "4": 1,
+      "5": 8
+    },
+    "n": 6,
+    "partition": [
+      0,
+      1,
+      2,
+      0,
+      3
+    ],
+    "scope": "binary query equations with involutive stages; no endpoint or rank admission",
+    "solver_result": "unsat",
+    "timeout_seconds": 3,
+    "z3_version": "5.3.2"
+  },
+  {
+    "full_calls": 7,
+    "labels": {
+      "1": 1,
+      "2": 2,
+      "3": 4,
+      "4": 2,
+      "5": 1
+    },
+    "n": 6,
+    "partition": [
+      0,
+      1,
+      2,
+      1,
+      0
+    ],
+    "scope": "binary query equations with involutive stages; no endpoint or rank admission",
+    "solver_result": "unsat",
+    "timeout_seconds": 3,
+    "z3_version": "5.3.2"
+  },
+  {
+    "full_calls": 7,
+    "labels": {
+      "1": 1,
+      "2": 2,
+      "3": 4,
+      "4": 2,
+      "5": 2
+    },
+    "n": 6,
+    "partition": [
+      0,
+      1,
+      2,
+      1,
+      1
+    ],
+    "scope": "binary query equations with involutive stages; no endpoint or rank admission",
+    "solver_result": "unsat",
+    "timeout_seconds": 3,
+    "z3_version": "5.3.2"
+  },
+  {
+    "full_calls": 7,
+    "labels": {
+      "1": 1,
+      "2": 2,
+      "3": 4,
+      "4": 2,
+      "5": 4
+    },
+    "n": 6,
+    "partition": [
+      0,
+      1,
+      2,
+      1,
+      2
+    ],
+    "scope": "binary query equations with involutive stages; no endpoint or rank admission",
+    "solver_result": "unsat",
+    "timeout_seconds": 3,
+    "z3_version": "5.3.2"
+  },
+  {
+    "full_calls": 7,
+    "labels": {
+      "1": 1,
+      "2": 2,
+      "3": 4,
+      "4": 2,
+      "5": 8
+    },
+    "n": 6,
+    "partition": [
+      0,
+      1,
+      2,
+      1,
+      3
+    ],
+    "scope": "binary query equations with involutive stages; no endpoint or rank admission",
+    "solver_result": "unsat",
+    "timeout_seconds": 3,
+    "z3_version": "5.3.2"
+  },
+  {
+    "full_calls": 7,
+    "labels": {
+      "1": 1,
+      "2": 2,
+      "3": 4,
+      "4": 4,
+      "5": 1
+    },
+    "n": 6,
+    "partition": [
+      0,
+      1,
+      2,
+      2,
+      0
+    ],
+    "scope": "binary query equations with involutive stages; no endpoint or rank admission",
+    "solver_result": "unsat",
+    "timeout_seconds": 3,
+    "z3_version": "5.3.2"
+  },
+  {
+    "full_calls": 7,
+    "interior_projectors": {
+      "1": [
+        61,
+        62,
+        0,
+        0,
+        0,
+        0
+      ],
+      "2": [
+        0,
+        0,
+        7,
+        59,
+        59,
+        59
+      ],
+      "3": [
+        0,
+        0,
+        0,
+        47,
+        55,
+        0
+      ],
+      "4": [
+        0,
+        0,
+        0,
+        47,
+        55,
+        0
+      ],
+      "5": [
+        0,
+        0,
+        31,
+        31,
+        31,
+        35
+      ]
+    },
+    "labels": {
+      "1": 1,
+      "2": 2,
+      "3": 4,
+      "4": 4,
+      "5": 2
+    },
+    "n": 6,
+    "partition": [
+      0,
+      1,
+      2,
+      2,
+      1
+    ],
+    "scope": "binary query equations with involutive stages; no endpoint or rank admission",
+    "solver_result": "sat",
+    "timeout_seconds": 3,
+    "z3_version": "5.3.2"
+  },
+  {
+    "full_calls": 7,
+    "labels": {
+      "1": 1,
+      "2": 2,
+      "3": 4,
+      "4": 4,
+      "5": 4
+    },
+    "n": 6,
+    "partition": [
+      0,
+      1,
+      2,
+      2,
+      2
+    ],
+    "scope": "binary query equations with involutive stages; no endpoint or rank admission",
+    "solver_result": "unsat",
+    "timeout_seconds": 3,
+    "z3_version": "5.3.2"
+  },
+  {
+    "full_calls": 7,
+    "labels": {
+      "1": 1,
+      "2": 2,
+      "3": 4,
+      "4": 4,
+      "5": 8
+    },
+    "n": 6,
+    "partition": [
+      0,
+      1,
+      2,
+      2,
+      3
+    ],
+    "scope": "binary query equations with involutive stages; no endpoint or rank admission",
+    "solver_result": "unsat",
+    "timeout_seconds": 3,
+    "z3_version": "5.3.2"
+  },
+  {
+    "full_calls": 7,
+    "labels": {
+      "1": 1,
+      "2": 2,
+      "3": 4,
+      "4": 8,
+      "5": 1
+    },
+    "n": 6,
+    "partition": [
+      0,
+      1,
+      2,
+      3,
+      0
+    ],
+    "scope": "binary query equations with involutive stages; no endpoint or rank admission",
+    "solver_result": "unsat",
+    "timeout_seconds": 3,
+    "z3_version": "5.3.2"
+  },
+  {
+    "full_calls": 7,
+    "labels": {
+      "1": 1,
+      "2": 2,
+      "3": 4,
+      "4": 8,
+      "5": 2
+    },
+    "n": 6,
+    "partition": [
+      0,
+      1,
+      2,
+      3,
+      1
+    ],
+    "scope": "binary query equations with involutive stages; no endpoint or rank admission",
+    "solver_result": "unsat",
+    "timeout_seconds": 3,
+    "z3_version": "5.3.2"
+  },
+  {
+    "full_calls": 7,
+    "labels": {
+      "1": 1,
+      "2": 2,
+      "3": 4,
+      "4": 8,
+      "5": 4
+    },
+    "n": 6,
+    "partition": [
+      0,
+      1,
+      2,
+      3,
+      2
+    ],
+    "scope": "binary query equations with involutive stages; no endpoint or rank admission",
+    "solver_result": "unsat",
+    "timeout_seconds": 3,
+    "z3_version": "5.3.2"
+  },
+  {
+    "full_calls": 7,
+    "labels": {
+      "1": 1,
+      "2": 2,
+      "3": 4,
+      "4": 8,
+      "5": 8
+    },
+    "n": 6,
+    "partition": [
+      0,
+      1,
+      2,
+      3,
+      3
+    ],
+    "scope": "binary query equations with involutive stages; no endpoint or rank admission",
+    "solver_result": "unsat",
+    "timeout_seconds": 3,
+    "z3_version": "5.3.2"
+  },
+  {
+    "full_calls": 7,
+    "labels": {
+      "1": 1,
+      "2": 2,
+      "3": 4,
+      "4": 8,
+      "5": 16
+    },
+    "n": 6,
+    "partition": [
+      0,
+      1,
+      2,
+      3,
+      4
+    ],
+    "scope": "binary query equations with involutive stages; no endpoint or rank admission",
+    "solver_result": "unsat",
+    "timeout_seconds": 3,
+    "z3_version": "5.3.2"
+  }
+]
diff --git a/research/shortest-controller-stage-capacity/discovery/pair_search.py b/research/shortest-controller-stage-capacity/discovery/pair_search.py
new file mode 100644
index 0000000000..429b50b7f9
--- /dev/null
+++ b/research/shortest-controller-stage-capacity/discovery/pair_search.py
@@ -0,0 +1,91 @@
+"""Search the pair constraints forced by a shortest query word.
+
+Ali Romman, with substantial OpenAI Codex assistance. Apache-2.0.
+"""
+import argparse
+import json
+from pathlib import Path
+import z3
+
+
+def search(n, seconds, constraint='all'):
+    solver = z3.Solver()
+    solver.set(timeout=seconds*1000)
+    zero = z3.BitVecVal(0, n)
+    mask = (1 << n)-1
+    us = [(1 << i) if i < n else mask for i in range(n+1)]
+    vs = [mask ^ (1 << i) if i < n else mask for i in range(n+1)]
+
+    def parity(x):
+        out = z3.Extract(0, 0, x) == 1
+        for k in range(1, n):
+            out = z3.Xor(out, z3.Extract(k, k, x) == 1)
+        return out
+
+    av, bv = {}, {}
+    for i in range(1, n):
+        av[i], bv[i] = z3.BitVec(f'a{i}', n), z3.BitVec(f'b{i}', n)
+        solver.assert_and_track(z3.And(parity(av[i] & vs[i]), parity(bv[i] & us[i]),
+                   z3.Not(parity(av[i] & bv[i])),
+                   z3.Extract(i, i, av[i]) == 0), f'projector_{i}')
+    for transpose in (False, True):
+        for first in range(n-1):
+            coeff = [z3.BitVecVal(vs[first] if transpose else us[first], n)]
+            for last in range(first+2, n+1):
+                s = last-1
+                out = [zero for _ in range(len(coeff)+1)]
+                for d, x in enumerate(coeff):
+                    if transpose:
+                        px = z3.If(parity(x & us[s]), bv[s], zero) ^ z3.If(parity(x & av[s]), z3.BitVecVal(vs[s], n), zero)
+                    else:
+                        px = z3.If(parity(x & bv[s]), z3.BitVecVal(us[s], n), zero) ^ z3.If(parity(x & vs[s]), av[s], zero)
+                    out[d] = out[d] ^ x ^ px
+                    out[d+1] = out[d+1] ^ px
+                coeff = [z3.BitVec(f'x{int(transpose)}_{first}_{last}_{d}', n) for d in range(len(out))]
+                solver.add([x == y for x, y in zip(coeff, out)])
+                target = us[last] if transpose else vs[last]
+                conditions = []
+                tangent = zero
+                for d, x in enumerate(coeff):
+                    if d % 2:
+                        tangent = tangent ^ x
+                    if constraint == 'tangent':
+                        continue
+                    if constraint == 'constant' and d != 0:
+                        continue
+                    if constraint == 'leading' and d != len(coeff)-1:
+                        continue
+                    conditions.append(parity(x & target) == (d == len(coeff)-1))
+                if constraint == 'tangent':
+                    conditions.append(parity(tangent & target) == bool((len(coeff)-1) % 2))
+                solver.assert_and_track(z3.And(conditions), f'pair_{int(transpose)}_{first}_{last}')
+    result = solver.check()
+    receipt = {'n': n, 'full_calls': n+1, 'solver_result': str(result),
+               'timeout_seconds': seconds, 'z3_version': z3.get_version_string(),
+               'constraint': constraint,
+               'scope': 'positive common-stage binary query identity; endpoint factorization not imposed'}
+    if result == z3.sat:
+        model = solver.model()
+        receipt['interior_projectors'] = {
+            str(s): [(model.eval(bv[s]).as_long() if (us[s] >> i) & 1 else 0)
+                     ^ (vs[s] if (model.eval(av[s]).as_long() >> i) & 1 else 0)
+                     for i in range(n)] for s in range(1, n)}
+    elif result == z3.unknown:
+        receipt['reason_unknown'] = solver.reason_unknown()
+    else:
+        receipt['core'] = [str(x) for x in solver.unsat_core()]
+    return receipt
+
+
+if __name__ == '__main__':
+    parser = argparse.ArgumentParser(description=__doc__)
+    parser.add_argument('--n', type=int, required=True)
+    parser.add_argument('--seconds', type=int, default=60)
+    parser.add_argument('--output', type=Path, required=True)
+    parser.add_argument('--constraint', choices=('all', 'constant', 'leading', 'tangent'), default='all')
+    args = parser.parse_args()
+    if args.n < 2 or args.n % 2:
+        parser.error('n must be positive and even')
+    result = search(args.n, args.seconds, args.constraint)
+    args.output.write_text(json.dumps(result, indent=2, sort_keys=True)+'\n')
+    print(json.dumps(result, sort_keys=True))
diff --git a/research/shortest-controller-stage-capacity/discovery/price-screens.json b/research/shortest-controller-stage-capacity/discovery/price-screens.json
new file mode 100644
index 0000000000..93d5f41518
--- /dev/null
+++ b/research/shortest-controller-stage-capacity/discovery/price-screens.json
@@ -0,0 +1,140 @@
+{
+  "paired_after_one_lost_occurrence": [
+    {
+      "floating_margin_at_003": -768.42857387,
+      "floating_raw_crossing": null,
+      "full_calls": 14,
+      "main_degree_counts": {
+        "2": 9,
+        "3": 3
+      },
+      "n": 12
+    },
+    {
+      "floating_margin_at_003": -690.79651423,
+      "floating_raw_crossing": null,
+      "full_calls": 18,
+      "main_degree_counts": {
+        "2": 13,
+        "3": 3
+      },
+      "n": 16
+    },
+    {
+      "floating_margin_at_003": -30.92400724,
+      "floating_raw_crossing": 0.002937339443,
+      "full_calls": 52,
+      "main_degree_counts": {
+        "2": 47,
+        "3": 3
+      },
+      "n": 50
+    },
+    {
+      "floating_margin_at_003": 7.89202259,
+      "floating_raw_crossing": 0.003015400932,
+      "full_calls": 54,
+      "main_degree_counts": {
+        "2": 49,
+        "3": 3
+      },
+      "n": 52
+    },
+    {
+      "floating_margin_at_003": 85.52408223,
+      "floating_raw_crossing": 0.003155418817,
+      "full_calls": 58,
+      "main_degree_counts": {
+        "2": 53,
+        "3": 3
+      },
+      "n": 56
+    }
+  ],
+  "paired_before_joint_cut": [
+    {
+      "floating_margin_at_003": -101.71540773,
+      "floating_raw_crossing": 0.001317297159,
+      "full_calls": 6,
+      "main_degree_counts": {
+        "2": 0,
+        "3": 4
+      },
+      "n": 4
+    },
+    {
+      "floating_margin_at_003": -24.08334809,
+      "floating_raw_crossing": 0.00275495873,
+      "full_calls": 10,
+      "main_degree_counts": {
+        "2": 4,
+        "3": 4
+      },
+      "n": 8
+    },
+    {
+      "floating_margin_at_003": 53.54871156,
+      "floating_raw_crossing": 0.003393385059,
+      "full_calls": 14,
+      "main_degree_counts": {
+        "2": 8,
+        "3": 4
+      },
+      "n": 12
+    },
+    {
+      "floating_margin_at_003": 131.1807712,
+      "floating_raw_crossing": 0.003754065674,
+      "full_calls": 18,
+      "main_degree_counts": {
+        "2": 12,
+        "3": 4
+      },
+      "n": 16
+    }
+  ],
+  "scope": "Floating optimistic profiles only; no exact operator or complete kappa claim",
+  "shortest_common_advance": [
+    {
+      "floating_margin_at_003": -12.04167404,
+      "floating_raw_crossing": 0.00275495873,
+      "full_calls": 5,
+      "main_degree_counts": {
+        "2": 2,
+        "3": 2
+      },
+      "n": 4
+    },
+    {
+      "floating_margin_at_003": 26.77435578,
+      "floating_raw_crossing": 0.003393385059,
+      "full_calls": 7,
+      "main_degree_counts": {
+        "2": 4,
+        "3": 2
+      },
+      "n": 6
+    },
+    {
+      "floating_margin_at_003": 65.5903856,
+      "floating_raw_crossing": 0.003754065674,
+      "full_calls": 9,
+      "main_degree_counts": {
+        "2": 6,
+        "3": 2
+      },
+      "n": 8
+    },
+    {
+      "floating_margin_at_003": 220.85450489,
+      "floating_raw_crossing": 0.004357697679,
+      "full_calls": 17,
+      "main_degree_counts": {
+        "2": 14,
+        "3": 2
+      },
+      "n": 16
+    }
+  ],
+  "source_head": "09dd0965711ca7eeb169057a420abab1c9052137"
+}
diff --git a/research/shortest-controller-stage-capacity/discovery/price_screens.py b/research/shortest-controller-stage-capacity/discovery/price_screens.py
new file mode 100644
index 0000000000..8598699d75
--- /dev/null
+++ b/research/shortest-controller-stage-capacity/discovery/price_screens.py
@@ -0,0 +1,40 @@
+"""Print optimistic floating prices. These are not certified caller bounds.
+
+Ali Romman, with substantial OpenAI Codex assistance. Apache-2.0.
+"""
+import json
+from pathlib import Path
+
+ROOT = Path(__file__).resolve().parents[3]
+local = json.loads((ROOT / 'research/p104-helper-subspace-splits/RESULT.json').read_text())['local']
+paid = {int(r): c for r, c in local['paid'].items()}
+helpers = {int(r): c for r, c in local['helpers'].items()}
+
+
+def screen(n, calls, degrees):
+    def margin(kappa):
+        t = 1-kappa
+        return (104*sum(c*(1+8*d)**t for d, c in degrees.items())
+                + calls*sum(c*r**t for r, c in helpers.items())
+                - calls*sum(c*r**t for r, c in paid.items()))
+    low, high = 0.0, 0.01
+    root = None
+    if margin(0) > 0 and margin(high) < 0:
+        for _ in range(60):
+            mid = (low+high)/2
+            if margin(mid) > 0:
+                low = mid
+            else:
+                high = mid
+        root = round((low+high)/2, 12)
+    return {'n': n, 'full_calls': calls, 'main_degree_counts': degrees,
+            'floating_raw_crossing': root, 'floating_margin_at_003': round(margin(.003), 8)}
+
+
+if __name__ == '__main__':
+    print(json.dumps({'scope': 'Floating optimistic profiles only; no exact operator or complete kappa claim',
+                      'source_head': '09dd0965711ca7eeb169057a420abab1c9052137',
+                      'shortest_common_advance': [screen(n, n+1, {2: n-2, 3: 2}) for n in (4, 6, 8, 16)],
+                      'paired_before_joint_cut': [screen(n, n+2, {2: n-4, 3: 4}) for n in (4, 8, 12, 16)],
+                      'paired_after_one_lost_occurrence': [screen(n, n+2, {2: n-3, 3: 3}) for n in (12, 16, 50, 52, 56)]},
+                     indent=2, sort_keys=True))
diff --git a/research/shortest-controller-stage-capacity/discovery/rational_pair_search.py b/research/shortest-controller-stage-capacity/discovery/rational_pair_search.py
new file mode 100644
index 0000000000..aa463350d2
--- /dev/null
+++ b/research/shortest-controller-stage-capacity/discovery/rational_pair_search.py
@@ -0,0 +1,72 @@
+"""Test the shortest-query pairing equations in characteristic zero.
+
+Ali Romman, with substantial OpenAI Codex assistance. Apache-2.0.
+"""
+import argparse
+import json
+from pathlib import Path
+import z3
+
+
+def search(n, seconds):
+    solver = z3.SolverFor('QF_NRA')
+    solver.set(timeout=seconds*1000)
+    us = [[int(i == j) for j in range(n)] for i in range(n)]
+    us.append([(-1)**(i+1) for i in range(n)])
+    vs = [[(1 if j < i else -1 if j > i else 0) for j in range(n)] for i in range(n)]
+    vs.append([1]*n)
+
+    def dot(a, b):
+        return sum(x*y for x, y in zip(a, b))
+
+    av, bv = {}, {}
+    for s in range(1, n):
+        av[s] = [z3.Real(f'a{s}_{j}') for j in range(n)]
+        bv[s] = [z3.Real(f'b{s}_{j}') for j in range(n)]
+        solver.add(dot(av[s], vs[s]) == 1, dot(bv[s], us[s]) == 1,
+                   dot(av[s], bv[s]) == 0, av[s][s] == 0)
+    for transpose in (False, True):
+        for first in range(n-1):
+            coeff = [vs[first] if transpose else us[first]]
+            for last in range(first+2, n+1):
+                s = last-1
+                out = [[0]*n for _ in range(len(coeff)+1)]
+                for d, x in enumerate(coeff):
+                    if transpose:
+                        px = [dot(x, us[s])*bv[s][k]+dot(x, av[s])*vs[s][k] for k in range(n)]
+                    else:
+                        px = [dot(x, bv[s])*us[s][k]+dot(x, vs[s])*av[s][k] for k in range(n)]
+                    for k in range(n):
+                        out[d][k] += x[k]-px[k]
+                        out[d+1][k] += px[k]
+                coeff = [[z3.Real(f'x{int(transpose)}_{first}_{last}_{d}_{k}') for k in range(n)]
+                         for d in range(len(out))]
+                solver.add([x == y for xx, yy in zip(coeff, out) for x, y in zip(xx, yy)])
+                target = us[last] if transpose else vs[last]
+                value = dot(vs[first], us[last]) if transpose else dot(vs[last], us[first])
+                for d, x in enumerate(coeff):
+                    solver.add(dot(x, target) == (value if d == len(coeff)-1 else 0))
+    result = solver.check()
+    receipt = {'n': n, 'full_calls': n+1, 'solver_result': str(result),
+               'timeout_seconds': seconds, 'z3_version': z3.get_version_string(),
+               'scope': 'real common-stage query equations; no endpoint or dyadic admission'}
+    if result == z3.sat:
+        model = solver.model()
+        receipt['a'] = {str(s): [str(model.eval(x)) for x in av[s]] for s in av}
+        receipt['b'] = {str(s): [str(model.eval(x)) for x in bv[s]] for s in bv}
+    elif result == z3.unknown:
+        receipt['reason_unknown'] = solver.reason_unknown()
+    return receipt
+
+
+if __name__ == '__main__':
+    parser = argparse.ArgumentParser(description=__doc__)
+    parser.add_argument('--n', type=int, required=True)
+    parser.add_argument('--seconds', type=int, default=60)
+    parser.add_argument('--output', type=Path, required=True)
+    args = parser.parse_args()
+    if args.n < 2 or args.n % 2:
+        parser.error('n must be positive and even')
+    result = search(args.n, args.seconds)
+    args.output.write_text(json.dumps(result, indent=2, sort_keys=True)+'\n')
+    print(json.dumps(result, sort_keys=True))
diff --git a/research/shortest-controller-stage-capacity/discovery/receipts/ENVIRONMENT.json b/research/shortest-controller-stage-capacity/discovery/receipts/ENVIRONMENT.json
new file mode 100644
index 0000000000..4a059b85d6
--- /dev/null
+++ b/research/shortest-controller-stage-capacity/discovery/receipts/ENVIRONMENT.json
@@ -0,0 +1,26 @@
+{
+  "host": "macOS-26.6.1-arm64-arm-64bit-Mach-O",
+  "python": "Python 3.12.13",
+  "z3_solver": "5.3.2.0",
+  "sympy": "1.14.0",
+  "scope": "Optional discovery evidence. Not used by the theorem replay. No solver proof certificates were retained.",
+  "files": [
+    "imb-pair4.json",
+    "imb-pair6.json",
+    "imb-pair8.json",
+    "imb-pair10.json",
+    "imb-pair6-core.json",
+    "imb-pair6-leading.json",
+    "imb-pair6-tangent.json",
+    "imb-pair4-tangent.json",
+    "imb-rational-pair2.json",
+    "imb-rational-pair4.json",
+    "imb-rational-pair6.json",
+    "imb-relation4.json",
+    "imb-relation6.json",
+    "imb-advancing-smt4.json",
+    "imb-advancing-smt6.json",
+    "imb-advancing-smt6-query.json",
+    "imb-formal-cut6.json"
+  ]
+}
diff --git a/research/shortest-controller-stage-capacity/discovery/receipts/imb-advancing-smt4.json b/research/shortest-controller-stage-capacity/discovery/receipts/imb-advancing-smt4.json
new file mode 100644
index 0000000000..19238d8599
--- /dev/null
+++ b/research/shortest-controller-stage-capacity/discovery/receipts/imb-advancing-smt4.json
@@ -0,0 +1,9 @@
+{
+  "balanced_target": false,
+  "full_calls": 5,
+  "n": 4,
+  "scope": "finite binary model, not a physical caller",
+  "solver_result": "unsat",
+  "timeout_seconds": 45,
+  "z3_version": "5.3.2"
+}
diff --git a/research/shortest-controller-stage-capacity/discovery/receipts/imb-advancing-smt6-query.json b/research/shortest-controller-stage-capacity/discovery/receipts/imb-advancing-smt6-query.json
new file mode 100644
index 0000000000..9f4bf0fab2
--- /dev/null
+++ b/research/shortest-controller-stage-capacity/discovery/receipts/imb-advancing-smt6-query.json
@@ -0,0 +1,10 @@
+{
+  "balanced_target": false,
+  "full_calls": 7,
+  "n": 6,
+  "reason_unknown": "timeout",
+  "scope": "finite binary model, not a physical caller",
+  "solver_result": "unknown",
+  "timeout_seconds": 60,
+  "z3_version": "5.3.2"
+}
diff --git a/research/shortest-controller-stage-capacity/discovery/receipts/imb-advancing-smt6.json b/research/shortest-controller-stage-capacity/discovery/receipts/imb-advancing-smt6.json
new file mode 100644
index 0000000000..43119ce5f1
--- /dev/null
+++ b/research/shortest-controller-stage-capacity/discovery/receipts/imb-advancing-smt6.json
@@ -0,0 +1,10 @@
+{
+  "balanced_target": true,
+  "full_calls": 7,
+  "n": 6,
+  "reason_unknown": "timeout",
+  "scope": "finite binary model, not a physical caller",
+  "solver_result": "unknown",
+  "timeout_seconds": 60,
+  "z3_version": "5.3.2"
+}
diff --git a/research/shortest-controller-stage-capacity/discovery/receipts/imb-formal-cut6.json b/research/shortest-controller-stage-capacity/discovery/receipts/imb-formal-cut6.json
new file mode 100644
index 0000000000..0210cbf122
--- /dev/null
+++ b/research/shortest-controller-stage-capacity/discovery/receipts/imb-formal-cut6.json
@@ -0,0 +1,7 @@
+{
+  "best_gap": 0,
+  "checked": 139500,
+  "half": 3,
+  "seed": 5593,
+  "witness": null
+}
diff --git a/research/shortest-controller-stage-capacity/discovery/receipts/imb-pair10.json b/research/shortest-controller-stage-capacity/discovery/receipts/imb-pair10.json
new file mode 100644
index 0000000000..f6c44dc967
--- /dev/null
+++ b/research/shortest-controller-stage-capacity/discovery/receipts/imb-pair10.json
@@ -0,0 +1,9 @@
+{
+  "full_calls": 11,
+  "n": 10,
+  "reason_unknown": "timeout",
+  "scope": "positive common-stage binary query identity; endpoint factorization not imposed",
+  "solver_result": "unknown",
+  "timeout_seconds": 60,
+  "z3_version": "5.3.2"
+}
diff --git a/research/shortest-controller-stage-capacity/discovery/receipts/imb-pair4-tangent.json b/research/shortest-controller-stage-capacity/discovery/receipts/imb-pair4-tangent.json
new file mode 100644
index 0000000000..3db200c780
--- /dev/null
+++ b/research/shortest-controller-stage-capacity/discovery/receipts/imb-pair4-tangent.json
@@ -0,0 +1,29 @@
+{
+  "constraint": "tangent",
+  "full_calls": 5,
+  "interior_projectors": {
+    "1": [
+      0,
+      2,
+      0,
+      13
+    ],
+    "2": [
+      0,
+      0,
+      6,
+      11
+    ],
+    "3": [
+      7,
+      0,
+      0,
+      10
+    ]
+  },
+  "n": 4,
+  "scope": "positive common-stage binary query identity; endpoint factorization not imposed",
+  "solver_result": "sat",
+  "timeout_seconds": 30,
+  "z3_version": "5.3.2"
+}
diff --git a/research/shortest-controller-stage-capacity/discovery/receipts/imb-pair4.json b/research/shortest-controller-stage-capacity/discovery/receipts/imb-pair4.json
new file mode 100644
index 0000000000..6e7ef2a4e3
--- /dev/null
+++ b/research/shortest-controller-stage-capacity/discovery/receipts/imb-pair4.json
@@ -0,0 +1,8 @@
+{
+  "full_calls": 5,
+  "n": 4,
+  "scope": "positive common-stage binary query identity; endpoint factorization not imposed",
+  "solver_result": "unsat",
+  "timeout_seconds": 30,
+  "z3_version": "5.3.2"
+}
diff --git a/research/shortest-controller-stage-capacity/discovery/receipts/imb-pair6-core.json b/research/shortest-controller-stage-capacity/discovery/receipts/imb-pair6-core.json
new file mode 100644
index 0000000000..cf9bb48535
--- /dev/null
+++ b/research/shortest-controller-stage-capacity/discovery/receipts/imb-pair6-core.json
@@ -0,0 +1,42 @@
+{
+  "constraint": "all",
+  "core": [
+    "projector_1",
+    "projector_2",
+    "projector_3",
+    "projector_4",
+    "projector_5",
+    "pair_0_0_3",
+    "pair_0_1_3",
+    "pair_0_1_4",
+    "pair_0_1_5",
+    "pair_0_1_6",
+    "pair_0_2_4",
+    "pair_0_2_5",
+    "pair_0_2_6",
+    "pair_0_3_5",
+    "pair_0_3_6",
+    "pair_0_4_6",
+    "pair_1_0_2",
+    "pair_1_0_3",
+    "pair_1_0_4",
+    "pair_1_0_5",
+    "pair_1_0_6",
+    "pair_1_1_3",
+    "pair_1_1_4",
+    "pair_1_1_5",
+    "pair_1_1_6",
+    "pair_1_2_4",
+    "pair_1_2_5",
+    "pair_1_2_6",
+    "pair_1_3_5",
+    "pair_1_3_6",
+    "pair_1_4_6"
+  ],
+  "full_calls": 7,
+  "n": 6,
+  "scope": "positive common-stage binary query identity; endpoint factorization not imposed",
+  "solver_result": "unsat",
+  "timeout_seconds": 30,
+  "z3_version": "5.3.2"
+}
diff --git a/research/shortest-controller-stage-capacity/discovery/receipts/imb-pair6-leading.json b/research/shortest-controller-stage-capacity/discovery/receipts/imb-pair6-leading.json
new file mode 100644
index 0000000000..dc1e7ec320
--- /dev/null
+++ b/research/shortest-controller-stage-capacity/discovery/receipts/imb-pair6-leading.json
@@ -0,0 +1,51 @@
+{
+  "constraint": "leading",
+  "full_calls": 7,
+  "interior_projectors": {
+    "1": [
+      61,
+      47,
+      61,
+      61,
+      61,
+      61
+    ],
+    "2": [
+      59,
+      59,
+      47,
+      59,
+      59,
+      59
+    ],
+    "3": [
+      0,
+      55,
+      0,
+      9,
+      0,
+      0
+    ],
+    "4": [
+      0,
+      47,
+      47,
+      0,
+      30,
+      47
+    ],
+    "5": [
+      31,
+      31,
+      0,
+      0,
+      31,
+      44
+    ]
+  },
+  "n": 6,
+  "scope": "positive common-stage binary query identity; endpoint factorization not imposed",
+  "solver_result": "sat",
+  "timeout_seconds": 30,
+  "z3_version": "5.3.2"
+}
diff --git a/research/shortest-controller-stage-capacity/discovery/receipts/imb-pair6-tangent.json b/research/shortest-controller-stage-capacity/discovery/receipts/imb-pair6-tangent.json
new file mode 100644
index 0000000000..a790b1701e
--- /dev/null
+++ b/research/shortest-controller-stage-capacity/discovery/receipts/imb-pair6-tangent.json
@@ -0,0 +1,51 @@
+{
+  "constraint": "tangent",
+  "full_calls": 7,
+  "interior_projectors": {
+    "1": [
+      61,
+      6,
+      0,
+      61,
+      61,
+      0
+    ],
+    "2": [
+      59,
+      0,
+      37,
+      0,
+      59,
+      59
+    ],
+    "3": [
+      55,
+      55,
+      55,
+      27,
+      0,
+      0
+    ],
+    "4": [
+      0,
+      0,
+      47,
+      0,
+      17,
+      0
+    ],
+    "5": [
+      31,
+      31,
+      31,
+      31,
+      31,
+      35
+    ]
+  },
+  "n": 6,
+  "scope": "positive common-stage binary query identity; endpoint factorization not imposed",
+  "solver_result": "sat",
+  "timeout_seconds": 30,
+  "z3_version": "5.3.2"
+}
diff --git a/research/shortest-controller-stage-capacity/discovery/receipts/imb-pair6.json b/research/shortest-controller-stage-capacity/discovery/receipts/imb-pair6.json
new file mode 100644
index 0000000000..a111c2787a
--- /dev/null
+++ b/research/shortest-controller-stage-capacity/discovery/receipts/imb-pair6.json
@@ -0,0 +1,8 @@
+{
+  "full_calls": 7,
+  "n": 6,
+  "scope": "positive common-stage binary query identity; endpoint factorization not imposed",
+  "solver_result": "unsat",
+  "timeout_seconds": 60,
+  "z3_version": "5.3.2"
+}
diff --git a/research/shortest-controller-stage-capacity/discovery/receipts/imb-pair8.json b/research/shortest-controller-stage-capacity/discovery/receipts/imb-pair8.json
new file mode 100644
index 0000000000..8de9404575
--- /dev/null
+++ b/research/shortest-controller-stage-capacity/discovery/receipts/imb-pair8.json
@@ -0,0 +1,8 @@
+{
+  "full_calls": 9,
+  "n": 8,
+  "scope": "positive common-stage binary query identity; endpoint factorization not imposed",
+  "solver_result": "unsat",
+  "timeout_seconds": 60,
+  "z3_version": "5.3.2"
+}
diff --git a/research/shortest-controller-stage-capacity/discovery/receipts/imb-rational-pair2.json b/research/shortest-controller-stage-capacity/discovery/receipts/imb-rational-pair2.json
new file mode 100644
index 0000000000..967d9031f6
--- /dev/null
+++ b/research/shortest-controller-stage-capacity/discovery/receipts/imb-rational-pair2.json
@@ -0,0 +1,20 @@
+{
+  "a": {
+    "1": [
+      "1",
+      "0"
+    ]
+  },
+  "b": {
+    "1": [
+      "0",
+      "1"
+    ]
+  },
+  "full_calls": 3,
+  "n": 2,
+  "scope": "real common-stage query equations; no endpoint or dyadic admission",
+  "solver_result": "sat",
+  "timeout_seconds": 10,
+  "z3_version": "5.3.2"
+}
diff --git a/research/shortest-controller-stage-capacity/discovery/receipts/imb-rational-pair4.json b/research/shortest-controller-stage-capacity/discovery/receipts/imb-rational-pair4.json
new file mode 100644
index 0000000000..a02794dabf
--- /dev/null
+++ b/research/shortest-controller-stage-capacity/discovery/receipts/imb-rational-pair4.json
@@ -0,0 +1,8 @@
+{
+  "full_calls": 5,
+  "n": 4,
+  "scope": "real common-stage query equations; no endpoint or dyadic admission",
+  "solver_result": "unsat",
+  "timeout_seconds": 60,
+  "z3_version": "5.3.2"
+}
diff --git a/research/shortest-controller-stage-capacity/discovery/receipts/imb-rational-pair6.json b/research/shortest-controller-stage-capacity/discovery/receipts/imb-rational-pair6.json
new file mode 100644
index 0000000000..7e362509f1
--- /dev/null
+++ b/research/shortest-controller-stage-capacity/discovery/receipts/imb-rational-pair6.json
@@ -0,0 +1,9 @@
+{
+  "full_calls": 7,
+  "n": 6,
+  "reason_unknown": "timeout",
+  "scope": "real common-stage query equations; no endpoint or dyadic admission",
+  "solver_result": "unknown",
+  "timeout_seconds": 60,
+  "z3_version": "5.3.2"
+}
diff --git a/research/shortest-controller-stage-capacity/discovery/receipts/imb-relation4.json b/research/shortest-controller-stage-capacity/discovery/receipts/imb-relation4.json
new file mode 100644
index 0000000000..33fbb7510b
--- /dev/null
+++ b/research/shortest-controller-stage-capacity/discovery/receipts/imb-relation4.json
@@ -0,0 +1,13 @@
+{
+  "full_calls": 5,
+  "labels": {
+    "1": 1,
+    "2": 2,
+    "3": 3
+  },
+  "n": 4,
+  "scope": "binary query equations with involutive stages; no endpoint or rank admission",
+  "solver_result": "unsat",
+  "timeout_seconds": 30,
+  "z3_version": "5.3.2"
+}
diff --git a/research/shortest-controller-stage-capacity/discovery/receipts/imb-relation6.json b/research/shortest-controller-stage-capacity/discovery/receipts/imb-relation6.json
new file mode 100644
index 0000000000..7dc9e6c7db
--- /dev/null
+++ b/research/shortest-controller-stage-capacity/discovery/receipts/imb-relation6.json
@@ -0,0 +1,15 @@
+{
+  "full_calls": 7,
+  "labels": {
+    "1": 1,
+    "2": 2,
+    "3": 4,
+    "4": 8,
+    "5": 15
+  },
+  "n": 6,
+  "scope": "binary query equations with involutive stages; no endpoint or rank admission",
+  "solver_result": "unsat",
+  "timeout_seconds": 60,
+  "z3_version": "5.3.2"
+}
diff --git a/research/shortest-controller-stage-capacity/discovery/relation_search.py b/research/shortest-controller-stage-capacity/discovery/relation_search.py
new file mode 100644
index 0000000000..e4fc10ea3b
--- /dev/null
+++ b/research/shortest-controller-stage-capacity/discovery/relation_search.py
@@ -0,0 +1,82 @@
+"""Search shortest-query words with one relation among interior stages.
+
+Ali Romman, with substantial OpenAI Codex assistance. Apache-2.0.
+"""
+import argparse
+import json
+from pathlib import Path
+import z3
+
+
+def search(n, seconds, supplied_labels=None):
+    solver = z3.Solver()
+    solver.set(timeout=seconds*1000)
+    zero = z3.BitVecVal(0, n)
+    mask = (1 << n)-1
+    us = [(1 << i) if i < n else mask for i in range(n+1)]
+    vs = [mask ^ (1 << i) if i < n else mask for i in range(n+1)]
+    labels = {s: 1 << (s-1) for s in range(1, n-1)}
+    labels[n-1] = (1 << (n-2))-1
+    if supplied_labels is not None:
+        if len(supplied_labels) != n-1 or any(x <= 0 for x in supplied_labels):
+            raise ValueError('one positive label is required for each interior stage')
+        labels = dict(enumerate(supplied_labels, 1))
+
+    def parity(x):
+        out = z3.Extract(0, 0, x) == 1
+        for k in range(1, n):
+            out = z3.Xor(out, z3.Extract(k, k, x) == 1)
+        return out
+
+    av, bv = {}, {}
+    for i in range(1, n):
+        av[i], bv[i] = z3.BitVec(f'a{i}', n), z3.BitVec(f'b{i}', n)
+        solver.add(parity(av[i] & vs[i]), parity(bv[i] & us[i]),
+                   z3.Not(parity(av[i] & bv[i])), z3.Extract(i, i, av[i]) == 0)
+    for transpose in (False, True):
+        for first in range(n-1):
+            coeff = {0: z3.BitVecVal(vs[first] if transpose else us[first], n)}
+            expected_label = 0
+            for last in range(first+2, n+1):
+                s = last-1
+                expected_label ^= labels[s]
+                out = {}
+                for label, x in coeff.items():
+                    if transpose:
+                        px = z3.If(parity(x & us[s]), bv[s], zero) ^ z3.If(parity(x & av[s]), z3.BitVecVal(vs[s], n), zero)
+                    else:
+                        px = z3.If(parity(x & bv[s]), z3.BitVecVal(us[s], n), zero) ^ z3.If(parity(x & vs[s]), av[s], zero)
+                    out[label] = out.get(label, zero) ^ x ^ px
+                    other = label ^ labels[s]
+                    out[other] = out.get(other, zero) ^ px
+                coeff = {label: z3.BitVec(f'x{int(transpose)}_{first}_{last}_{label}', n) for label in out}
+                solver.add([coeff[label] == value for label, value in out.items()])
+                target = us[last] if transpose else vs[last]
+                solver.add([parity(x & target) == (label == expected_label) for label, x in coeff.items()])
+    result = solver.check()
+    receipt = {'n': n, 'full_calls': n+1, 'solver_result': str(result),
+               'timeout_seconds': seconds, 'z3_version': z3.get_version_string(),
+               'labels': labels, 'scope': 'binary query equations with involutive stages; no endpoint or rank admission'}
+    if result == z3.sat:
+        model = solver.model()
+        receipt['interior_projectors'] = {
+            str(s): [(model.eval(bv[s]).as_long() if (us[s] >> i) & 1 else 0)
+                     ^ (vs[s] if (model.eval(av[s]).as_long() >> i) & 1 else 0)
+                     for i in range(n)] for s in range(1, n)}
+    elif result == z3.unknown:
+        receipt['reason_unknown'] = solver.reason_unknown()
+    return receipt
+
+
+if __name__ == '__main__':
+    parser = argparse.ArgumentParser(description=__doc__)
+    parser.add_argument('--n', type=int, required=True)
+    parser.add_argument('--seconds', type=int, default=60)
+    parser.add_argument('--output', type=Path, required=True)
+    parser.add_argument('--labels', help='Comma-separated nonzero group labels for interior stages')
+    args = parser.parse_args()
+    if args.n < 4 or args.n % 2:
+        parser.error('n must be even and at least four')
+    result = search(args.n, args.seconds, list(map(int, args.labels.split(','))) if args.labels else None)
+    args.output.write_text(json.dumps(result, indent=2, sort_keys=True)+'\n')
+    print(json.dumps(result, sort_keys=True))
diff --git a/research/shortest-controller-stage-capacity/discovery/search_cuts.py b/research/shortest-controller-stage-capacity/discovery/search_cuts.py
new file mode 100644
index 0000000000..e739c1c6ec
--- /dev/null
+++ b/research/shortest-controller-stage-capacity/discovery/search_cuts.py
@@ -0,0 +1,93 @@
+"""Search exact subspace cuts for the formal common-stage caller.
+
+Ali Romman, with substantial OpenAI Codex assistance. Apache-2.0.
+"""
+import argparse
+from itertools import combinations
+import json
+from pathlib import Path
+import random
+
+
+def basis(values):
+    pivots = {}
+    for x in values:
+        for p in sorted(pivots, reverse=True):
+            if (x >> p) & 1:
+                x ^= pivots[p]
+        if x:
+            p = x.bit_length()-1
+            for j in pivots:
+                if (pivots[j] >> p) & 1:
+                    pivots[j] ^= x
+            pivots[p] = x
+    return tuple(pivots[p] for p in sorted(pivots, reverse=True))
+
+
+def apply(matrix, x):
+    y = 0
+    for k, column in enumerate(matrix):
+        if (x >> k) & 1:
+            y ^= column
+    return y
+
+
+def cut(matrix, u):
+    return len(basis((*u, *(apply(matrix, x) for x in u))))-len(u)
+
+
+def check(d, q, u, max_degree=8):
+    dim = len(d)
+    doubled = (*u, *(x << dim for x in u))
+    images = [apply(d, x) for x in u]
+    images += [apply(d, apply(q, x)) ^ (apply(d, x) << dim) for x in u]
+    full = len(basis((*doubled, *images)))-2*len(u)
+    power = [1 << i for i in range(dim)]
+    targets = []
+    for _ in range(max_degree+1):
+        targets.append(cut([apply(q, x) for x in power], u))
+        power = [apply(d, x) for x in power]
+    return full, targets
+
+
+def search(half, rounds, seed):
+    rng = random.Random(seed)
+    dim = 2*half
+    q = [1 << i for i in range(half)] + [(1 << i) ^ (1 << (i+half)) for i in range(half)]
+    if dim == 6:
+        subspaces = sorted({basis(c) for c in combinations(range(1, 1 << dim), 3) if len(basis(c)) == 3})
+    else:
+        subspaces = sorted({basis(rng.randrange(1, 1 << dim) for _ in range(half)) for _ in range(2000)})
+        subspaces = [u for u in subspaces if len(u) == half]
+    best, witness = 0, None
+    checked = 0
+    for _ in range(rounds):
+        while True:
+            a = [rng.randrange(1 << half) for _ in range(half)]
+            if len(basis(a)) == half:
+                break
+        b = [rng.randrange(1 << half) for _ in range(half)]
+        d = a + [x ^ (y << half) for x, y in zip(b, a)]
+        for u in subspaces:
+            full, targets = check(d, q, u, 4)
+            checked += 1
+            # The six-field balanced candidate uses seven full calls.
+            gap = 4*targets[2]+2*targets[3]-7*full
+            if gap > best:
+                best, witness = gap, {'d': d, 'q': q, 'u': list(u), 'full_cut': full, 'target_cuts': targets}
+                print(json.dumps({'new_gap': best, 'witness': witness}), flush=True)
+                if gap > 0:
+                    return {'checked': checked, 'seed': seed, 'half': half, 'best_gap': best, 'witness': witness}
+    return {'checked': checked, 'seed': seed, 'half': half, 'best_gap': best, 'witness': witness}
+
+
+if __name__ == '__main__':
+    parser = argparse.ArgumentParser(description=__doc__)
+    parser.add_argument('--half', type=int, default=3)
+    parser.add_argument('--rounds', type=int, default=100)
+    parser.add_argument('--seed', type=int, default=5593)
+    parser.add_argument('--output', type=Path, required=True)
+    args = parser.parse_args()
+    result = search(args.half, args.rounds, args.seed)
+    args.output.write_text(json.dumps(result, indent=2, sort_keys=True)+'\n')
+    print(json.dumps(result, sort_keys=True))
diff --git a/research/shortest-controller-stage-capacity/discovery/signed-simplex-census.json b/research/shortest-controller-stage-capacity/discovery/signed-simplex-census.json
new file mode 100644
index 0000000000..2de0a72cf7
--- /dev/null
+++ b/research/shortest-controller-stage-capacity/discovery/signed-simplex-census.json
@@ -0,0 +1,18 @@
+{
+  "0": "INVENTORY 0 14 16\nINVENTORY 1 208 16\nINVENTORY 2 2816 16\nINVENTORY 3 28672 16\nINVENTORY 4 65535 16\nTOTAL 1048576 ALL_QUERY 0 FACTORED 0\n",
+  "1": "INVENTORY 0 14 16\nINVENTORY 1 208 16\nINVENTORY 2 2816 16\nINVENTORY 3 28672 16\nINVENTORY 4 65535 16\nTOTAL 1048576 ALL_QUERY 0 FACTORED 0\n",
+  "2": "INVENTORY 0 14 16\nINVENTORY 1 208 16\nINVENTORY 2 2816 16\nINVENTORY 3 28672 16\nINVENTORY 4 65535 16\nTOTAL 1048576 ALL_QUERY 256 FACTORED 0\nRANK_SUM 6 24\nRANK_SUM 7 82\nRANK_SUM 8 112\nRANK_SUM 9 34\nRANK_SUM 10 4\n",
+  "3": "INVENTORY 0 14 16\nINVENTORY 1 208 16\nINVENTORY 2 2816 16\nINVENTORY 3 28672 16\nINVENTORY 4 65535 16\nTOTAL 1048576 ALL_QUERY 256 FACTORED 0\nRANK_SUM 6 42\nRANK_SUM 7 62\nRANK_SUM 8 104\nRANK_SUM 9 36\nRANK_SUM 10 12\n",
+  "4": "INVENTORY 0 14 16\nINVENTORY 1 208 16\nINVENTORY 2 2816 16\nINVENTORY 3 28672 16\nINVENTORY 4 65535 16\nTOTAL 1048576 ALL_QUERY 2048 FACTORED 0\nRANK_SUM 5 2\nRANK_SUM 6 94\nRANK_SUM 7 291\nRANK_SUM 8 658\nRANK_SUM 9 523\nRANK_SUM 10 299\nRANK_SUM 11 143\nRANK_SUM 12 36\nRANK_SUM 13 2\n",
+  "5": "INVENTORY 0 14 16\nINVENTORY 1 208 16\nINVENTORY 2 2816 16\nINVENTORY 3 28672 16\nINVENTORY 4 65535 16\nWORD 225 3376 46592 46967 34951 COEFF 0 102 0 33863 0 0\nWORD 237 109 1035 34560 34696 COEFF 0 771 170 1792 32904 0\nWORD 237 237 46848 46848 4577 COEFF 0 0 38336 4577 0 0\nWORD 237 237 46848 46848 7697 COEFF 0 0 39472 7697 0 0\nWORD 237 237 46848 46848 8749 COEFF 0 0 42508 8749 0 0\nWORD 237 237 46848 46848 11554 COEFF 0 0 43267 11554 0 0\nWORD 237 237 46848 46848 17483 COEFF 0 0 49258 17483 0 0\nWORD 237 237 46848 46848 17588 COEFF 0 0 49301 17588 0 0\nWORD 237 237 46848 46848 34679 COEFF 0 0 854 34679 0 0\nWORD 237 237 46848 46848 34696 COEFF 0 0 937 34696 0 0\nTOTAL 1048576 ALL_QUERY 2048 FACTORED 20\nRANK_SUM 4 20\nRANK_SUM 5 87\nRANK_SUM 6 297\nRANK_SUM 7 510\nRANK_SUM 8 490\nRANK_SUM 9 321\nRANK_SUM 10 204\nRANK_SUM 11 88\nRANK_SUM 12 27\nRANK_SUM 13 4\nDEGREES 0 0 2 2 0 0 COUNT 16\nDEGREES 0 1 0 3 0 0 COUNT 2\nDEGREES 0 1 1 1 1 0 COUNT 2\n",
+  "6": "INVENTORY 0 14 16\nINVENTORY 1 208 16\nINVENTORY 2 2816 16\nINVENTORY 3 28672 16\nINVENTORY 4 65535 16\nWORD 225 237 46848 46848 8749 COEFF 0 0 42496 8737 0 0\nWORD 225 237 46848 46848 17483 COEFF 0 0 49254 17479 0 0\nWORD 225 237 46848 46848 34951 COEFF 0 0 3242 34955 0 0\nWORD 225 237 46848 46848 61153 COEFF 0 0 27340 61165 0 0\nWORD 237 237 46848 46848 4577 COEFF 0 0 38336 4577 0 0\nWORD 237 237 46848 46848 7697 COEFF 0 0 39472 7697 0 0\nWORD 237 237 46848 46848 8749 COEFF 0 0 42508 8749 0 0\nWORD 237 237 46848 46848 11554 COEFF 0 0 43267 11554 0 0\nWORD 237 237 46848 46848 17483 COEFF 0 0 49258 17483 0 0\nWORD 237 237 46848 46848 17588 COEFF 0 0 49301 17588 0 0\nTOTAL 1048576 ALL_QUERY 256 FACTORED 25\nRANK_SUM 4 25\nRANK_SUM 5 36\nRANK_SUM 6 83\nRANK_SUM 7 66\nRANK_SUM 8 46\nDEGREES 0 0 2 2 0 0 COUNT 25\n",
+  "7": "INVENTORY 0 14 16\nINVENTORY 1 208 16\nINVENTORY 2 2816 16\nINVENTORY 3 28672 16\nINVENTORY 4 65535 16\nTOTAL 1048576 ALL_QUERY 256 FACTORED 0\nRANK_SUM 6 42\nRANK_SUM 7 62\nRANK_SUM 8 104\nRANK_SUM 9 36\nRANK_SUM 10 12\n",
+  "8": "INVENTORY 0 14 16\nINVENTORY 1 208 16\nINVENTORY 2 2816 16\nINVENTORY 3 28672 16\nINVENTORY 4 65535 16\nTOTAL 1048576 ALL_QUERY 256 FACTORED 0\nRANK_SUM 6 24\nRANK_SUM 7 82\nRANK_SUM 8 112\nRANK_SUM 9 34\nRANK_SUM 10 4\n",
+  "9": "INVENTORY 0 14 16\nINVENTORY 1 208 16\nINVENTORY 2 2816 16\nINVENTORY 3 28672 16\nINVENTORY 4 65535 16\nWORD 237 237 46848 46848 4577 COEFF 0 0 38336 4577 0 0\nWORD 237 237 46848 46848 7697 COEFF 0 0 39472 7697 0 0\nWORD 237 237 46848 46848 8749 COEFF 0 0 42508 8749 0 0\nWORD 237 237 46848 46848 11554 COEFF 0 0 43267 11554 0 0\nWORD 237 237 46848 46848 17483 COEFF 0 0 49258 17483 0 0\nWORD 237 237 46848 46848 17588 COEFF 0 0 49301 17588 0 0\nWORD 237 237 46848 46848 34679 COEFF 0 0 854 34679 0 0\nWORD 237 237 46848 46848 34696 COEFF 0 0 937 34696 0 0\nWORD 237 237 46848 46848 34936 COEFF 0 0 3161 34936 0 0\nWORD 237 237 46848 46848 34951 COEFF 0 0 3238 34951 0 0\nTOTAL 1048576 ALL_QUERY 256 FACTORED 16\nRANK_SUM 4 16\nRANK_SUM 5 34\nRANK_SUM 6 72\nRANK_SUM 7 82\nRANK_SUM 8 52\nDEGREES 0 0 2 2 0 0 COUNT 16\n",
+  "10": "INVENTORY 0 14 16\nINVENTORY 1 208 16\nINVENTORY 2 2816 16\nINVENTORY 3 28672 16\nINVENTORY 4 65535 16\nWORD 225 237 46848 46848 8749 COEFF 0 0 42496 8737 0 0\nWORD 225 237 46848 46848 17483 COEFF 0 0 49254 17479 0 0\nWORD 225 237 46848 46848 34951 COEFF 0 0 3242 34955 0 0\nWORD 225 237 46848 46848 61153 COEFF 0 0 27340 61165 0 0\nWORD 225 3376 46592 46967 34951 COEFF 0 3264 0 35041 0 0\nWORD 225 3504 3504 34679 34679 COEFF 0 0 33984 225 0 0\nWORD 225 3504 3504 34679 34951 COEFF 0 0 35632 3857 0 0\nWORD 229 109 1035 34560 34679 COEFF 0 0 32981 1268 0 0\nWORD 229 109 1035 34560 34696 COEFF 0 0 32810 1035 0 0\nWORD 229 109 3248 34560 34696 COEFF 0 0 34961 3248 0 0\nTOTAL 1048576 ALL_QUERY 2048 FACTORED 66\nRANK_SUM 4 66\nRANK_SUM 5 184\nRANK_SUM 6 477\nRANK_SUM 7 522\nRANK_SUM 8 383\nRANK_SUM 9 251\nRANK_SUM 10 94\nRANK_SUM 11 49\nRANK_SUM 12 22\nDEGREES 0 0 2 2 0 0 COUNT 64\nDEGREES 0 1 0 3 0 0 COUNT 2\n",
+  "11": "INVENTORY 0 14 16\nINVENTORY 1 208 16\nINVENTORY 2 2816 16\nINVENTORY 3 28672 16\nINVENTORY 4 65535 16\nWORD 225 3376 46592 46967 34951 COEFF 0 0 3105 0 34816 0\nWORD 225 3504 3504 34679 34679 COEFF 0 0 225 33984 0 0\nWORD 229 109 1035 34560 34679 COEFF 0 85 176 32896 1092 0\nWORD 229 3504 3504 34679 34679 COEFF 0 0 229 33988 0 0\nWORD 233 3504 3504 34679 34679 COEFF 0 0 233 33992 0 0\nWORD 237 3504 3504 34679 34679 COEFF 0 0 237 33996 0 0\nWORD 3585 3504 3504 34679 34679 COEFF 0 0 3585 35360 0 0\nWORD 3587 3376 48827 46967 34679 COEFF 0 771 3328 2730 32904 0\nWORD 3587 3504 3504 34679 34679 COEFF 0 0 3587 35362 0 0\nWORD 3593 3504 3504 34679 34679 COEFF 0 0 3593 35368 0 0\nTOTAL 1048576 ALL_QUERY 2048 FACTORED 20\nRANK_SUM 4 20\nRANK_SUM 5 87\nRANK_SUM 6 297\nRANK_SUM 7 510\nRANK_SUM 8 490\nRANK_SUM 9 321\nRANK_SUM 10 204\nRANK_SUM 11 88\nRANK_SUM 12 27\nRANK_SUM 13 4\nDEGREES 0 0 2 2 0 0 COUNT 16\nDEGREES 0 0 3 0 1 0 COUNT 2\nDEGREES 0 1 1 1 1 0 COUNT 2\n",
+  "12": "INVENTORY 0 14 16\nINVENTORY 1 208 16\nINVENTORY 2 2816 16\nINVENTORY 3 28672 16\nINVENTORY 4 65535 16\nWORD 225 3504 3504 34679 34679 COEFF 0 0 33984 225 0 0\nWORD 225 3504 3504 34679 34951 COEFF 0 0 35632 3857 0 0\nWORD 229 3504 3504 34679 34679 COEFF 0 0 33988 229 0 0\nWORD 233 3504 3504 34679 34679 COEFF 0 0 33992 233 0 0\nWORD 237 3504 3504 34679 34679 COEFF 0 0 33996 237 0 0\nWORD 3585 3504 3504 34679 34679 COEFF 0 0 35360 3585 0 0\nWORD 3585 3504 3504 34679 34951 COEFF 0 0 34256 497 0 0\nWORD 3587 3504 3504 34679 34679 COEFF 0 0 35362 3587 0 0\nWORD 3593 3504 3504 34679 34679 COEFF 0 0 35368 3593 0 0\nWORD 3595 3504 3504 34679 34679 COEFF 0 0 35370 3595 0 0\nTOTAL 1048576 ALL_QUERY 256 FACTORED 25\nRANK_SUM 4 25\nRANK_SUM 5 36\nRANK_SUM 6 83\nRANK_SUM 7 66\nRANK_SUM 8 46\nDEGREES 0 0 2 2 0 0 COUNT 25\n",
+  "13": "INVENTORY 0 14 16\nINVENTORY 1 208 16\nINVENTORY 2 2816 16\nINVENTORY 3 28672 16\nINVENTORY 4 65535 16\nWORD 225 3504 3504 34679 34679 COEFF 0 0 225 33984 0 0\nWORD 229 3504 3504 34679 34679 COEFF 0 0 229 33988 0 0\nWORD 233 3504 3504 34679 34679 COEFF 0 0 233 33992 0 0\nWORD 237 3504 3504 34679 34679 COEFF 0 0 237 33996 0 0\nWORD 3585 3504 3504 34679 34679 COEFF 0 0 3585 35360 0 0\nWORD 3587 3504 3504 34679 34679 COEFF 0 0 3587 35362 0 0\nWORD 3593 3504 3504 34679 34679 COEFF 0 0 3593 35368 0 0\nWORD 3595 3504 3504 34679 34679 COEFF 0 0 3595 35370 0 0\nWORD 57345 3504 3504 34679 34679 COEFF 0 0 57345 25632 0 0\nWORD 57347 3504 3504 34679 34679 COEFF 0 0 57347 25634 0 0\nTOTAL 1048576 ALL_QUERY 256 FACTORED 16\nRANK_SUM 4 16\nRANK_SUM 5 34\nRANK_SUM 6 72\nRANK_SUM 7 82\nRANK_SUM 8 52\nDEGREES 0 0 2 2 0 0 COUNT 16\n",
+  "14": "INVENTORY 0 14 16\nINVENTORY 1 208 16\nINVENTORY 2 2816 16\nINVENTORY 3 28672 16\nINVENTORY 4 65535 16\nTOTAL 1048576 ALL_QUERY 0 FACTORED 0\n",
+  "15": "INVENTORY 0 14 16\nINVENTORY 1 208 16\nINVENTORY 2 2816 16\nINVENTORY 3 28672 16\nINVENTORY 4 65535 16\nTOTAL 1048576 ALL_QUERY 0 FACTORED 0\n"
+}
diff --git a/research/shortest-controller-stage-capacity/discovery/simplex-census.json b/research/shortest-controller-stage-capacity/discovery/simplex-census.json
new file mode 100644
index 0000000000..51e59ca6c0
--- /dev/null
+++ b/research/shortest-controller-stage-capacity/discovery/simplex-census.json
@@ -0,0 +1,34 @@
+{
+  "0": "INVENTORY 0 14 1\nINVENTORY 1 208 1\nINVENTORY 2 2816 1\nINVENTORY 3 28672 1\nINVENTORY 4 65535 1\nWORD 0 0 0 0 0 COEFF 33825 0 0 0 0 0\nTOTAL 1 ALL_QUERY 1 FACTORED 1\nRANK_SUM 4 1\nDEGREES 4 0 0 0 0 0 COUNT 1\n",
+  "1": "INVENTORY 0 14 16\nINVENTORY 1 208 1\nINVENTORY 2 2816 1\nINVENTORY 3 28672 1\nINVENTORY 4 65535 1\nWORD 225 0 0 0 0 COEFF 33984 225 0 0 0 0\nWORD 229 0 0 0 0 COEFF 33988 229 0 0 0 0\nWORD 233 0 0 0 0 COEFF 33992 233 0 0 0 0\nWORD 237 0 0 0 0 COEFF 33996 237 0 0 0 0\nWORD 3585 0 0 0 0 COEFF 35360 3585 0 0 0 0\nWORD 3587 0 0 0 0 COEFF 35362 3587 0 0 0 0\nWORD 3593 0 0 0 0 COEFF 35368 3593 0 0 0 0\nWORD 3595 0 0 0 0 COEFF 35370 3595 0 0 0 0\nWORD 57345 0 0 0 0 COEFF 25632 57345 0 0 0 0\nWORD 57347 0 0 0 0 COEFF 25634 57347 0 0 0 0\nTOTAL 16 ALL_QUERY 16 FACTORED 16\nRANK_SUM 4 16\nDEGREES 2 2 0 0 0 0 COUNT 16\n",
+  "2": "INVENTORY 0 14 1\nINVENTORY 1 208 16\nINVENTORY 2 2816 1\nINVENTORY 3 28672 1\nINVENTORY 4 65535 1\nWORD 0 237 0 0 0 COEFF 33996 237 0 0 0 0\nTOTAL 16 ALL_QUERY 1 FACTORED 1\nRANK_SUM 4 1\nDEGREES 2 2 0 0 0 0 COUNT 1\n",
+  "3": "INVENTORY 0 14 16\nINVENTORY 1 208 16\nINVENTORY 2 2816 1\nINVENTORY 3 28672 1\nINVENTORY 4 65535 1\nWORD 237 237 0 0 0 COEFF 33996 0 237 0 0 0\nTOTAL 256 ALL_QUERY 16 FACTORED 1\nRANK_SUM 4 1\nRANK_SUM 5 6\nRANK_SUM 6 9\nDEGREES 2 0 2 0 0 0 COUNT 1\n",
+  "4": "INVENTORY 0 14 1\nINVENTORY 1 208 1\nINVENTORY 2 2816 16\nINVENTORY 3 28672 1\nINVENTORY 4 65535 1\nTOTAL 16 ALL_QUERY 0 FACTORED 0\n",
+  "5": "INVENTORY 0 14 16\nINVENTORY 1 208 1\nINVENTORY 2 2816 16\nINVENTORY 3 28672 1\nINVENTORY 4 65535 1\nTOTAL 256 ALL_QUERY 0 FACTORED 0\n",
+  "6": "INVENTORY 0 14 1\nINVENTORY 1 208 16\nINVENTORY 2 2816 16\nINVENTORY 3 28672 1\nINVENTORY 4 65535 1\nTOTAL 256 ALL_QUERY 0 FACTORED 0\n",
+  "7": "INVENTORY 0 14 16\nINVENTORY 1 208 16\nINVENTORY 2 2816 16\nINVENTORY 3 28672 1\nINVENTORY 4 65535 1\nTOTAL 4096 ALL_QUERY 0 FACTORED 0\n",
+  "8": "INVENTORY 0 14 1\nINVENTORY 1 208 1\nINVENTORY 2 2816 1\nINVENTORY 3 28672 16\nINVENTORY 4 65535 1\nWORD 0 0 0 34679 0 COEFF 854 34679 0 0 0 0\nTOTAL 16 ALL_QUERY 1 FACTORED 1\nRANK_SUM 4 1\nDEGREES 2 2 0 0 0 0 COUNT 1\n",
+  "9": "INVENTORY 0 14 16\nINVENTORY 1 208 1\nINVENTORY 2 2816 1\nINVENTORY 3 28672 16\nINVENTORY 4 65535 1\nTOTAL 256 ALL_QUERY 16 FACTORED 0\nRANK_SUM 6 16\n",
+  "10": "INVENTORY 0 14 1\nINVENTORY 1 208 16\nINVENTORY 2 2816 1\nINVENTORY 3 28672 16\nINVENTORY 4 65535 1\nTOTAL 256 ALL_QUERY 1 FACTORED 0\nRANK_SUM 6 1\n",
+  "11": "INVENTORY 0 14 16\nINVENTORY 1 208 16\nINVENTORY 2 2816 1\nINVENTORY 3 28672 16\nINVENTORY 4 65535 1\nTOTAL 4096 ALL_QUERY 16 FACTORED 0\nRANK_SUM 6 2\nRANK_SUM 7 8\nRANK_SUM 8 6\n",
+  "12": "INVENTORY 0 14 1\nINVENTORY 1 208 1\nINVENTORY 2 2816 16\nINVENTORY 3 28672 16\nINVENTORY 4 65535 1\nTOTAL 256 ALL_QUERY 0 FACTORED 0\n",
+  "13": "INVENTORY 0 14 16\nINVENTORY 1 208 1\nINVENTORY 2 2816 16\nINVENTORY 3 28672 16\nINVENTORY 4 65535 1\nTOTAL 4096 ALL_QUERY 0 FACTORED 0\n",
+  "14": "INVENTORY 0 14 1\nINVENTORY 1 208 16\nINVENTORY 2 2816 16\nINVENTORY 3 28672 16\nINVENTORY 4 65535 1\nTOTAL 4096 ALL_QUERY 0 FACTORED 0\n",
+  "15": "INVENTORY 0 14 16\nINVENTORY 1 208 16\nINVENTORY 2 2816 16\nINVENTORY 3 28672 16\nINVENTORY 4 65535 1\nTOTAL 65536 ALL_QUERY 0 FACTORED 0\n",
+  "16": "INVENTORY 0 14 1\nINVENTORY 1 208 1\nINVENTORY 2 2816 1\nINVENTORY 3 28672 1\nINVENTORY 4 65535 16\nWORD 0 0 0 0 4577 COEFF 38336 4577 0 0 0 0\nWORD 0 0 0 0 7697 COEFF 39472 7697 0 0 0 0\nWORD 0 0 0 0 8749 COEFF 42508 8749 0 0 0 0\nWORD 0 0 0 0 11554 COEFF 43267 11554 0 0 0 0\nWORD 0 0 0 0 17483 COEFF 49258 17483 0 0 0 0\nWORD 0 0 0 0 17588 COEFF 49301 17588 0 0 0 0\nWORD 0 0 0 0 34679 COEFF 854 34679 0 0 0 0\nWORD 0 0 0 0 34696 COEFF 937 34696 0 0 0 0\nWORD 0 0 0 0 34936 COEFF 3161 34936 0 0 0 0\nWORD 0 0 0 0 34951 COEFF 3238 34951 0 0 0 0\nTOTAL 16 ALL_QUERY 16 FACTORED 16\nRANK_SUM 4 16\nDEGREES 2 2 0 0 0 0 COUNT 16\n",
+  "17": "INVENTORY 0 14 16\nINVENTORY 1 208 1\nINVENTORY 2 2816 1\nINVENTORY 3 28672 1\nINVENTORY 4 65535 16\nWORD 229 0 0 0 17588 COEFF 49344 17489 176 0 0 0\nWORD 233 0 0 0 34936 COEFF 3264 34961 112 0 0 0\nWORD 3587 0 0 0 11554 COEFF 43520 8993 3328 0 0 0\nWORD 3593 0 0 0 34696 COEFF 2720 35201 1792 0 0 0\nWORD 57347 0 0 0 53794 COEFF 26112 12833 53248 0 0 0\nWORD 57349 0 0 0 46148 COEFF 24672 21569 45056 0 0 0\nWORD 61153 0 0 0 61153 COEFF 27328 0 61153 0 0 0\nTOTAL 256 ALL_QUERY 256 FACTORED 7\nRANK_SUM 4 7\nRANK_SUM 5 66\nRANK_SUM 6 141\nRANK_SUM 7 36\nRANK_SUM 8 6\nDEGREES 1 2 1 0 0 0 COUNT 6\nDEGREES 2 0 2 0 0 0 COUNT 1\n",
+  "18": "INVENTORY 0 14 1\nINVENTORY 1 208 16\nINVENTORY 2 2816 1\nINVENTORY 3 28672 1\nINVENTORY 4 65535 16\nTOTAL 256 ALL_QUERY 16 FACTORED 0\nRANK_SUM 6 16\n",
+  "19": "INVENTORY 0 14 16\nINVENTORY 1 208 16\nINVENTORY 2 2816 1\nINVENTORY 3 28672 1\nINVENTORY 4 65535 16\nTOTAL 4096 ALL_QUERY 256 FACTORED 0\nRANK_SUM 6 24\nRANK_SUM 7 82\nRANK_SUM 8 112\nRANK_SUM 9 34\nRANK_SUM 10 4\n",
+  "20": "INVENTORY 0 14 1\nINVENTORY 1 208 1\nINVENTORY 2 2816 16\nINVENTORY 3 28672 1\nINVENTORY 4 65535 16\nTOTAL 256 ALL_QUERY 0 FACTORED 0\n",
+  "21": "INVENTORY 0 14 16\nINVENTORY 1 208 1\nINVENTORY 2 2816 16\nINVENTORY 3 28672 1\nINVENTORY 4 65535 16\nTOTAL 4096 ALL_QUERY 0 FACTORED 0\n",
+  "22": "INVENTORY 0 14 1\nINVENTORY 1 208 16\nINVENTORY 2 2816 16\nINVENTORY 3 28672 1\nINVENTORY 4 65535 16\nTOTAL 4096 ALL_QUERY 0 FACTORED 0\n",
+  "23": "INVENTORY 0 14 16\nINVENTORY 1 208 16\nINVENTORY 2 2816 16\nINVENTORY 3 28672 1\nINVENTORY 4 65535 16\nTOTAL 65536 ALL_QUERY 0 FACTORED 0\n",
+  "24": "INVENTORY 0 14 1\nINVENTORY 1 208 1\nINVENTORY 2 2816 1\nINVENTORY 3 28672 16\nINVENTORY 4 65535 16\nWORD 0 0 0 34679 34679 COEFF 854 0 34679 0 0 0\nTOTAL 256 ALL_QUERY 16 FACTORED 1\nRANK_SUM 4 1\nRANK_SUM 5 6\nRANK_SUM 6 9\nDEGREES 2 0 2 0 0 0 COUNT 1\n",
+  "25": "INVENTORY 0 14 16\nINVENTORY 1 208 1\nINVENTORY 2 2816 1\nINVENTORY 3 28672 16\nINVENTORY 4 65535 16\nTOTAL 4096 ALL_QUERY 256 FACTORED 0\nRANK_SUM 6 24\nRANK_SUM 7 82\nRANK_SUM 8 112\nRANK_SUM 9 34\nRANK_SUM 10 4\n",
+  "26": "INVENTORY 0 14 1\nINVENTORY 1 208 16\nINVENTORY 2 2816 1\nINVENTORY 3 28672 16\nINVENTORY 4 65535 16\nTOTAL 4096 ALL_QUERY 16 FACTORED 0\nRANK_SUM 6 2\nRANK_SUM 7 8\nRANK_SUM 8 6\n",
+  "27": "INVENTORY 0 14 16\nINVENTORY 1 208 16\nINVENTORY 2 2816 1\nINVENTORY 3 28672 16\nINVENTORY 4 65535 16\nTOTAL 65536 ALL_QUERY 256 FACTORED 0\nRANK_SUM 6 1\nRANK_SUM 7 2\nRANK_SUM 8 44\nRANK_SUM 9 62\nRANK_SUM 10 113\nRANK_SUM 11 34\n",
+  "28": "INVENTORY 0 14 1\nINVENTORY 1 208 1\nINVENTORY 2 2816 16\nINVENTORY 3 28672 16\nINVENTORY 4 65535 16\nTOTAL 4096 ALL_QUERY 0 FACTORED 0\n",
+  "29": "INVENTORY 0 14 16\nINVENTORY 1 208 1\nINVENTORY 2 2816 16\nINVENTORY 3 28672 16\nINVENTORY 4 65535 16\nTOTAL 65536 ALL_QUERY 0 FACTORED 0\n",
+  "30": "INVENTORY 0 14 1\nINVENTORY 1 208 16\nINVENTORY 2 2816 16\nINVENTORY 3 28672 16\nINVENTORY 4 65535 16\nTOTAL 65536 ALL_QUERY 0 FACTORED 0\n",
+  "31": "INVENTORY 0 14 16\nINVENTORY 1 208 16\nINVENTORY 2 2816 16\nINVENTORY 3 28672 16\nINVENTORY 4 65535 16\nTOTAL 1048576 ALL_QUERY 0 FACTORED 0\n"
+}
diff --git a/research/shortest-controller-stage-capacity/discovery/simplex_search.cpp b/research/shortest-controller-stage-capacity/discovery/simplex_search.cpp
new file mode 100644
index 0000000000..c978b6af76
--- /dev/null
+++ b/research/shortest-controller-stage-capacity/discovery/simplex_search.cpp
@@ -0,0 +1,131 @@
+// Apache-2.0. Ali Romman, with substantial OpenAI Codex assistance.
+// The simplex and projector parametrization are due to Cinna Davis.
+#include <array>
+#include <cstdint>
+#include <cstdlib>
+#include <iostream>
+#include <map>
+#include <set>
+#include <vector>
+
+using Mat = uint16_t;
+constexpr Mat ID = 0x8421;
+constexpr int N = 4;
+constexpr int L = 5;
+using Poly = std::array<Mat, L + 1>;
+
+Mat mul(Mat a, Mat b) {
+    Mat out = 0;
+    for (int i = 0; i < N; ++i) {
+        int row = 0;
+        for (int j = 0; j < N; ++j)
+            if ((a >> (4*i+j)) & 1) row ^= (b >> (4*j)) & 15;
+        out |= row << (4*i);
+    }
+    return out;
+}
+
+Mat outer(int u, int v) {
+    Mat out = 0;
+    for (int i = 0; i < N; ++i)
+        if ((u >> i) & 1) out |= v << (4*i);
+    return out;
+}
+
+int rank(Mat a) {
+    int pivots[4] = {}, count = 0;
+    for (int i = 0; i < N; ++i) {
+        int row = (a >> (4*i)) & 15;
+        for (int k = 3; k >= 0; --k) {
+            if (!((row >> k) & 1)) continue;
+            if (pivots[k]) row ^= pivots[k];
+            else { pivots[k] = row; ++count; break; }
+        }
+    }
+    return count;
+}
+
+int parity(int x) { return __builtin_parity(static_cast<unsigned>(x)); }
+
+std::array<Mat, L> r;
+std::array<std::vector<Mat>, L> ps;
+std::array<Mat, L> word;
+uint64_t total = 0, all_query = 0, factored = 0;
+std::map<int, uint64_t> rank_histogram;
+std::map<std::array<int, L+1>, uint64_t> degree_histogram;
+int full_mask = 31;
+int inverse_mask = 0;
+
+void visit(int depth, const Poly& a, const Poly& b) {
+    if (depth == L) {
+        ++total;
+        if (a != b) return;
+        ++all_query;
+        std::array<int, L+1> ranks;
+        int sum = 0;
+        for (int d = 0; d <= L; ++d) { ranks[d] = rank(a[d]); sum += ranks[d]; }
+        ++rank_histogram[sum];
+        if (sum != N) return;
+        ++factored;
+        ++degree_histogram[ranks];
+        if (factored <= 10) {
+            std::cout << "WORD";
+            for (Mat p : word) std::cout << ' ' << p;
+            std::cout << " COEFF";
+            for (Mat c : a) std::cout << ' ' << c;
+            std::cout << '\n';
+        }
+        return;
+    }
+    for (Mat p : ps[depth]) {
+        word[depth] = p;
+        Poly aa{}, bb{};
+        for (int d = 0; d <= depth; ++d) {
+            Mat pa = mul(p, a[d]), pb = mul(p, b[d]);
+            bool inverse = (inverse_mask >> depth) & 1;
+            aa[d] ^= inverse ? pa : a[d] ^ pa;
+            aa[d+1] ^= inverse ? a[d] ^ pa : pa;
+            bb[d] ^= inverse ? pb : b[d] ^ pb;
+            bb[d+1] ^= inverse ? b[d] ^ pb : pb;
+            bb[d + (((full_mask >> depth) & 1) && !inverse)] ^= mul(r[depth], a[d]);
+        }
+        visit(depth+1, aa, bb);
+    }
+}
+
+int main(int argc, char** argv) {
+    if (argc >= 2) full_mask = std::atoi(argv[1]);
+    if (argc >= 3) inverse_mask = std::atoi(argv[2]);
+    if ((inverse_mask & full_mask) != inverse_mask) return 2;
+    for (int i = 0; i < L; ++i) {
+        int u = i < N ? 1 << i : 15;
+        int v = i < N ? 15 ^ u : 15;
+        r[i] = outer(u, v);
+        std::set<Mat> unique;
+        for (int a = 1; a < 16; ++a) {
+            if (!parity(v & a)) continue;
+            for (int b = 1; b < 16; ++b) {
+                if (!parity(u & b) || parity(a & b)) continue;
+                unique.insert(outer(u, b) ^ outer(a, v));
+            }
+        }
+        ps[i].assign(unique.begin(), unique.end());
+        if (!((full_mask >> i) & 1)) ps[i] = {0};
+        std::cout << "INVENTORY " << i << ' ' << r[i] << ' ' << ps[i].size() << '\n';
+        for (Mat p : ps[i]) {
+            if (!p) continue;
+            if (rank(p) != 2 || mul(p,p) != p || mul(p,r[i]) != r[i] || mul(r[i],p) != r[i])
+                return 2;
+        }
+    }
+    Poly a{}, b{};
+    a[0] = ID;
+    visit(0, a, b);
+    std::cout << "TOTAL " << total << " ALL_QUERY " << all_query << " FACTORED " << factored << '\n';
+    for (const auto& [k, v] : rank_histogram) std::cout << "RANK_SUM " << k << ' ' << v << '\n';
+    for (const auto& [k, v] : degree_histogram) {
+        std::cout << "DEGREES";
+        for (int x : k) std::cout << ' ' << x;
+        std::cout << " COUNT " << v << '\n';
+    }
+}
diff --git a/research/shortest-controller-stage-capacity/discovery/solve.py b/research/shortest-controller-stage-capacity/discovery/solve.py
new file mode 100644
index 0000000000..c9686d2b82
--- /dev/null
+++ b/research/shortest-controller-stage-capacity/discovery/solve.py
@@ -0,0 +1,106 @@
+"""Search the common-stage simplex with exact binary polynomial equations.
+
+Ali Romman, with substantial OpenAI Codex assistance. Apache-2.0.
+The simplex and rank-two projector parametrization are due to Cinna Davis.
+"""
+import argparse
+import json
+from pathlib import Path
+import z3
+
+
+def search(n, seconds, factor):
+    solver = z3.Solver()
+    solver.set(timeout=seconds * 1000)
+    zero = z3.BitVecVal(0, n)
+
+    def bit(v, k):
+        return z3.Extract(k, k, v) == 1
+
+    def parity(v):
+        terms = [bit(v, k) for k in range(n)]
+        out = terms[0]
+        for t in terms[1:]:
+            out = z3.Xor(out, t)
+        return out
+
+    def dot(rows, selector):
+        out = zero
+        for k, row in enumerate(rows):
+            out = out ^ z3.If(bit(selector, k), row, zero)
+        return out
+
+    def fresh(label, depth):
+        return [[z3.BitVec(f'{label}_{depth}_{d}_{i}', n) for i in range(n)]
+                for d in range(depth + 1)]
+
+    a = [[z3.BitVecVal(1 << i, n) for i in range(n)]]
+    b = [[zero for _ in range(n)]]
+    projectors = []
+    for stage in range(n + 1):
+        u = (1 << stage) if stage < n else (1 << n)-1
+        v = ((1 << n)-1) ^ u if stage < n else u
+        av = z3.BitVec(f'a_{stage}', n)
+        bv = z3.BitVec(f'b_{stage}', n)
+        solver.add(parity(av & v), parity(bv & u), z3.Not(parity(av & bv)))
+        solver.add(z3.Not(bit(av, (u & -u).bit_length()-1)))
+        projectors.append((u, v, av, bv))
+        aa, bb = fresh('A', stage+1), fresh('B', stage+1)
+        ca = [[zero for _ in range(n)] for _ in aa]
+        cb = [[zero for _ in range(n)] for _ in aa]
+        for d in range(stage+1):
+            va, vb = dot(a[d], z3.BitVecVal(v, n)), dot(b[d], z3.BitVecVal(v, n))
+            ba, bb0 = dot(a[d], bv), dot(b[d], bv)
+            for i in range(n):
+                pa = (ba if (u >> i) & 1 else zero) ^ z3.If(bit(av, i), va, zero)
+                pb = (bb0 if (u >> i) & 1 else zero) ^ z3.If(bit(av, i), vb, zero)
+                ca[d][i] = ca[d][i] ^ a[d][i] ^ pa
+                ca[d+1][i] = ca[d+1][i] ^ pa
+                cb[d][i] = cb[d][i] ^ b[d][i] ^ pb
+                cb[d+1][i] = cb[d+1][i] ^ pb ^ (va if (u >> i) & 1 else zero)
+        solver.add([aa[d][i] == ca[d][i] for d in range(len(aa)) for i in range(n)])
+        solver.add([bb[d][i] == cb[d][i] for d in range(len(bb)) for i in range(n)])
+        a, b = aa, bb
+    solver.add([a[d][i] == b[d][i] for d in range(n+2) for i in range(n)])
+    if factor:
+        # The balanced target has n-2 jobs of degree two and two of degree three.
+        left = [z3.BitVec(f'left_{i}', 2) for i in range(n)]
+        right = [z3.BitVec(f'right_{i}', n) for i in range(2)]
+        for i in range(2):
+            for j in range(2):
+                terms = [z3.And(bit(right[i], k), bit(left[k], j)) for k in range(n)]
+                value = terms[0]
+                for term in terms[1:]:
+                    value = z3.Xor(value, term)
+                solver.add(value == (i == j))
+        for i in range(n):
+            p = z3.If(bit(left[i], 0), right[0], zero) ^ z3.If(bit(left[i], 1), right[1], zero)
+            for d in range(n+2):
+                solver.add(a[d][i] == (p if d == 3 else (p ^ (1 << i) if d == 2 else zero)))
+    result = solver.check()
+    receipt = {'n': n, 'full_calls': n+1, 'balanced_target': factor,
+               'z3_version': z3.get_version_string(), 'timeout_seconds': seconds,
+               'solver_result': str(result), 'scope': 'finite binary model, not a physical caller'}
+    if result == z3.sat:
+        model = solver.model()
+        receipt['projectors'] = [[(model.eval(bv).as_long() if (u >> i) & 1 else 0)
+                                 ^ (v if (model.eval(av).as_long() >> i) & 1 else 0)
+                                 for i in range(n)] for u, v, av, bv in projectors]
+        receipt['coefficients'] = [[model.eval(x).as_long() for x in rows] for rows in a]
+    elif result == z3.unknown:
+        receipt['reason_unknown'] = solver.reason_unknown()
+    return receipt
+
+
+if __name__ == '__main__':
+    parser = argparse.ArgumentParser(description=__doc__)
+    parser.add_argument('--n', type=int, required=True)
+    parser.add_argument('--seconds', type=int, default=60)
+    parser.add_argument('--factor', action='store_true')
+    parser.add_argument('--output', type=Path, required=True)
+    args = parser.parse_args()
+    if args.n < 2 or args.n % 2:
+        parser.error('n must be positive and even')
+    receipt = search(args.n, args.seconds, args.factor)
+    args.output.write_text(json.dumps(receipt, indent=2, sort_keys=True)+'\n')
+    print(json.dumps(receipt, sort_keys=True))
diff --git a/research/shortest-controller-stage-capacity/examples/fourteen-query-intersection-rejected.json b/research/shortest-controller-stage-capacity/examples/fourteen-query-intersection-rejected.json
new file mode 100644
index 0000000000..d257315086
--- /dev/null
+++ b/research/shortest-controller-stage-capacity/examples/fourteen-query-intersection-rejected.json
@@ -0,0 +1,128 @@
+{
+  "n": 12,
+  "u": [
+    1,
+    2,
+    4,
+    8,
+    16,
+    32,
+    63,
+    64,
+    128,
+    256,
+    512,
+    1024,
+    2048,
+    4032
+  ],
+  "v": [
+    62,
+    61,
+    59,
+    55,
+    47,
+    31,
+    63,
+    3968,
+    3904,
+    3776,
+    3520,
+    3008,
+    1984,
+    4032
+  ],
+  "axes": [
+    {
+      "name": "d0",
+      "calls": [
+        0,
+        7
+      ],
+      "outputs": [
+        0,
+        1,
+        2,
+        3
+      ]
+    },
+    {
+      "name": "d1",
+      "calls": [
+        1,
+        8
+      ],
+      "outputs": [
+        4,
+        5,
+        6,
+        7
+      ]
+    },
+    {
+      "name": "d2",
+      "calls": [
+        2,
+        9
+      ],
+      "outputs": [
+        8,
+        9,
+        10,
+        11
+      ]
+    },
+    {
+      "name": "d3",
+      "calls": [
+        3,
+        10
+      ],
+      "outputs": [
+        0,
+        1,
+        2,
+        3
+      ]
+    },
+    {
+      "name": "d4",
+      "calls": [
+        4,
+        11
+      ],
+      "outputs": [
+        4,
+        5,
+        6,
+        7
+      ]
+    },
+    {
+      "name": "d5",
+      "calls": [
+        5,
+        12
+      ],
+      "outputs": [
+        8,
+        9,
+        10,
+        11
+      ]
+    },
+    {
+      "name": "d6",
+      "calls": [
+        6,
+        13
+      ],
+      "outputs": [
+        8,
+        9,
+        10,
+        11
+      ]
+    }
+  ]
+}
diff --git a/research/shortest-controller-stage-capacity/examples/shortest-repeat-rejected.json b/research/shortest-controller-stage-capacity/examples/shortest-repeat-rejected.json
new file mode 100644
index 0000000000..fd86e5e152
--- /dev/null
+++ b/research/shortest-controller-stage-capacity/examples/shortest-repeat-rejected.json
@@ -0,0 +1,32 @@
+{
+  "n": 4,
+  "u": [
+    1,
+    2,
+    4,
+    8,
+    15
+  ],
+  "v": [
+    14,
+    13,
+    11,
+    7,
+    15
+  ],
+  "axes": [
+    {
+      "name": "x",
+      "calls": [
+        0,
+        1
+      ],
+      "outputs": [
+        0,
+        1,
+        2,
+        3
+      ]
+    }
+  ]
+}
diff --git a/research/shortest-controller-stage-capacity/examples/six-query-positive.json b/research/shortest-controller-stage-capacity/examples/six-query-positive.json
new file mode 100644
index 0000000000..d5ceb80a87
--- /dev/null
+++ b/research/shortest-controller-stage-capacity/examples/six-query-positive.json
@@ -0,0 +1,60 @@
+{
+  "n": 4,
+  "u": [
+    1,
+    2,
+    3,
+    4,
+    8,
+    12
+  ],
+  "v": [
+    2,
+    1,
+    3,
+    8,
+    4,
+    12
+  ],
+  "axes": [
+    {
+      "name": "d0",
+      "calls": [
+        0,
+        3
+      ],
+      "outputs": [
+        0,
+        1,
+        2,
+        3
+      ]
+    },
+    {
+      "name": "d1",
+      "calls": [
+        1,
+        4
+      ],
+      "outputs": [
+        0,
+        1,
+        2,
+        3
+      ]
+    },
+    {
+      "name": "d2",
+      "calls": [
+        2,
+        5
+      ],
+      "outputs": [
+        0,
+        1,
+        2,
+        3
+      ]
+    }
+  ]
+}
diff --git a/research/shortest-controller-stage-capacity/verify.py b/research/shortest-controller-stage-capacity/verify.py
new file mode 100644
index 0000000000..07d695bb87
--- /dev/null
+++ b/research/shortest-controller-stage-capacity/verify.py
@@ -0,0 +1,499 @@
+#!/usr/bin/env python3
+"""Check exact controls and complete prices for the written rank-cut proof.
+
+Ali Romman, with substantial OpenAI Codex assistance. Apache-2.0.
+The simplex formulas and literal word are due to Cinna Davis.
+"""
+import argparse
+from collections import Counter
+from decimal import Decimal, localcontext
+from fractions import Fraction
+import hashlib
+from itertools import combinations, product
+import json
+from pathlib import Path
+from types import ModuleType
+
+
+PACKAGE = Path(__file__).resolve().parent
+ROOT = PACKAGE.parents[1]
+
+
+def need(condition, message):
+    if not condition:
+        raise ValueError(message)
+
+
+def authenticate():
+    manifest = json.loads((PACKAGE / 'SOURCES.json').read_text())
+    count = 0
+    for row in manifest['files']:
+        if row['usage'] != 'input':
+            continue
+        raw = (ROOT / row['path']).read_bytes()
+        need(hashlib.sha256(raw).hexdigest() == row['sha256'],
+             'Source SHA256 mismatch: ' + row['path'])
+        blob = b'blob ' + str(len(raw)).encode() + b'\0' + raw
+        need(hashlib.sha1(blob).hexdigest() == row['git_blob'],
+             'Source Git blob mismatch: ' + row['path'])
+        count += 1
+    return count
+
+
+def rank(rows):
+    pivots = {}
+    for value in rows:
+        while value:
+            p = value.bit_length()-1
+            if p not in pivots:
+                pivots[p] = value
+                break
+            value ^= pivots[p]
+    return len(pivots)
+
+
+def eye(n):
+    return [1 << i for i in range(n)]
+
+
+def add(a, b):
+    return [x ^ y for x, y in zip(a, b)]
+
+
+def mul(a, b):
+    out = []
+    for row in a:
+        value = 0
+        while row:
+            low = row & -row
+            value ^= b[low.bit_length()-1]
+            row ^= low
+        out.append(value)
+    return out
+
+
+def outer(u, v, n):
+    return [v if (u >> i) & 1 else 0 for i in range(n)]
+
+
+def dot(v, u):
+    return (u & v).bit_count() % 2
+
+
+def apply(a, u):
+    return sum(dot(row, u) << i for i, row in enumerate(a))
+
+
+def inverse(a):
+    n = len(a)
+    rows = [r | (1 << (n+i)) for i, r in enumerate(a)]
+    for j in range(n):
+        pivot = next((i for i in range(j, n) if (rows[i] >> j) & 1), None)
+        need(pivot is not None, 'Singular constant endpoint')
+        rows[j], rows[pivot] = rows[pivot], rows[j]
+        for i in range(n):
+            if i != j and (rows[i] >> j) & 1:
+                rows[i] ^= rows[j]
+    return [row >> n for row in rows]
+
+
+def submatrix(a, row_ids, column_ids):
+    return [sum(((a[i] >> j) & 1) << t for t, j in enumerate(column_ids))
+            for i in row_ids]
+
+
+def factor_rank_one(a):
+    v = next(row for row in a if row)
+    need(all(row in (0, v) for row in a), 'Rank-one factor')
+    u = sum(bool(row) << i for i, row in enumerate(a))
+    need(dot(v, u) == 0, 'Nilpotent factor')
+    return u, v
+
+
+def word(gates, labels, omit_query=None):
+    """Multiply sparse group-algebra coefficient matrices directly."""
+    n = len(gates[0][1])
+    result = {0: eye(n)}
+    for i, ((p, r), label) in enumerate(zip(gates, labels)):
+        terms = {0: eye(n)} if label is None else {0: add(eye(n), p), label: p}
+        if i != omit_query:
+            key = 1 if label is None else label ^ 1
+            terms[key] = add(terms.get(key, [0]*n), r)
+        changed = {}
+        for left, a in terms.items():
+            for right, b in result.items():
+                key = left ^ right
+                changed[key] = add(changed.get(key, [0]*n), mul(a, b))
+        result = {key: value for key, value in changed.items() if any(value)}
+    return result
+
+
+def endpoint(coefficients):
+    n = len(next(iter(coefficients.values())))
+    need(all(key & 1 for key in coefficients), 'Missing central query')
+    constant = [0]*n
+    for value in coefficients.values():
+        constant = add(constant, value)
+    inv = inverse(constant)
+    projections = {key: mul(value, inv) for key, value in coefficients.items()}
+    for a, b in product(projections, repeat=2):
+        want = projections[a] if a == b else [0]*n
+        need(mul(projections[a], projections[b]) == want,
+             'Independent coefficient images')
+    degrees = Counter()
+    for key, value in projections.items():
+        degrees[key.bit_count()-1] += rank(value)
+    need(sum(degrees.values()) == n, 'All independent fields are retained')
+    return dict(sorted(degrees.items()))
+
+
+def query_frame(gates):
+    n = len(gates[0][1])
+    tail, undo = eye(n), eye(n)
+    us, vs, ps = [], [], []
+    for p, nilpotent in reversed(gates):
+        r = mul(mul(tail, nilpotent), undo)
+        u, v = factor_rank_one(r)
+        us.append(u)
+        vs.append(v)
+        ps.append(mul(mul(tail, p), undo))
+        constant = add(eye(n), nilpotent)
+        tail = mul(tail, constant)
+        undo = mul(constant, undo)
+    us.reverse()
+    vs.reverse()
+    ps.reverse()
+    total = [0]*n
+    for u, v in zip(us, vs):
+        total = add(total, outer(u, v, n))
+    need(total == eye(n), 'Whole-word query frame sums to identity')
+    gram = [sum(dot(v, u) << j for j, u in enumerate(us)) for v in vs]
+    need(mul(gram, gram) == gram and rank(gram) == n, 'Query Gram projection')
+    need(all(not ((row >> i) & 1) for i, row in enumerate(gram)), 'Zero Gram diagonal')
+    return gram, ps
+
+
+def operator_controls():
+    source = ROOT / 'research/productive-controller-basis-search/algebra.py'
+    a = ModuleType('credited_controller_algebra')
+    exec(compile(source.read_bytes(), str(source), 'exec'), a.__dict__)
+    ids = [7, 0, 39, 832, 384]
+    gates = [(a.FULL if (24 >> i) & 1 else a.THIN)[g] for i, g in enumerate(ids)]
+    labels = [None, None, None, 16, 32]
+    direct = word(gates, labels)
+    literal = a.coefficients(a.literal(24, ids))
+    need(direct == literal, 'Two literal interpreters agree on the sharp word')
+    need(endpoint(direct) == {0: 2, 2: 2}, 'Independent main ranks 1,1,17,17')
+    gram, _ = query_frame(gates)
+    need(gram == [31 ^ (1 << i) for i in range(5)], 'Sharp shortest-query Gram')
+    try:
+        endpoint(word(gates, labels, omit_query=1))
+    except ValueError:
+        pass
+    else:
+        raise ValueError('Deleted query escaped the endpoint control')
+    pairs = [(0, 1), (1, 0), (0, 1), (2, 3), (3, 2), (2, 3)]
+    gates = [a.FULL[a.elementary(*pair)] for pair in pairs]
+    independent = word(gates, [1 << (i+1) for i in range(6)])
+    literal = a.coefficients(a.literal(63, [a.elementary(*p) for p in pairs]))
+    need(independent == literal, 'Two literal interpreters agree on the longer word')
+    paired = word(gates, [2, 4, 8, 2, 4, 8])
+    need(endpoint(paired) == {3: 4}, 'Actual six-call paired-stage endpoint')
+    gram, ps = query_frame(gates)
+    groups = [(i, i+3) for i in range(3)]
+    for group in groups:
+        need(rank(submatrix(gram, group, group)) == 0, 'Zero within-pair Gram')
+        need(add(ps[group[0]], ps[group[1]]) == eye(4), 'Full pair capacity')
+    for s, t in combinations(groups, 2):
+        need(rank(submatrix(gram, s, t)) == 2, 'Off-diagonal intersection demand')
+    need(4 > 2 + (2 % 2), 'Longer positive control defeats a false shortest extension')
+    return {'sharp_five_query_degrees': {'0': 2, '2': 2}, 'sharp_margin_at_linear_tariff': -8,
+            'six_query_paired_degrees': {'3': 4}, 'six_query_gram': gram,
+            'two_literal_interpreters': True, 'deleted_query_rejected': True}
+
+
+def simplex_controls():
+    pairings = private_tests = 0
+    for n in range(2, 65, 2):
+        ones = (1 << n)-1
+        us = [1 << i for i in range(n)] + [ones]
+        vs = [ones ^ (1 << i) for i in range(n)] + [ones]
+        gram = [sum(dot(v, u) << j for j, u in enumerate(us)) for v in vs]
+        need(gram == [((1 << (n+1))-1) ^ (1 << i) for i in range(n+1)], 'Simplex pairings')
+        pairings += (n+1)**2
+        for k in range(1, n+2):
+            need(rank(submatrix(gram, range(k), range(k))) == k-k % 2,
+                 'Every principal-block rank formula')
+        projectors, suffixes = {}, {}
+        for s in range(1, n):
+            u_tail = v_tail = 0
+            for j in range(s+1, n+1):
+                u_tail ^= us[j]
+                v_tail ^= vs[j]
+            pairing = [dot(vs[s], us[s]), dot(vs[s], u_tail),
+                       dot(v_tail, us[s]), dot(v_tail, u_tail)]
+            need(pairing == [0, (n-s) % 2, (n-s) % 2, 0], 'Private-stage pairing')
+            if (n-s) % 2 == 0:
+                continue
+            p = add(outer(us[s], v_tail, n), outer(u_tail, vs[s], n))
+            need(rank(p) == 2 and mul(p, p) == p, 'Forced private projector')
+            projectors[s], suffixes[s] = p, u_tail
+            for boundary, u_extra, v_extra in (
+                    (0, us[s] ^ u_tail, vs[s] ^ v_tail), (n, u_tail, v_tail)):
+                if (boundary == 0 and s == 1) or (boundary == n and s == n-1):
+                    continue
+                need(u_extra not in (0, us[boundary]) and v_extra not in (0, vs[boundary]),
+                     'Endpoint pairs are independent')
+                need(not any(dot(v, u) for v in (vs[boundary], v_extra)
+                             for u in (us[boundary], u_extra)), 'Endpoint degeneracy')
+                private_tests += 1
+        for s, t in combinations(projectors, 2):
+            need(apply(projectors[s], us[t]) == suffixes[s] != 0, 'Earlier private projector')
+            need(apply(projectors[t], suffixes[s]) == 0 and
+                 apply(projectors[t], us[t]) == us[t], 'Private projectors fail to commute')
+            private_tests += 1
+    for k in range(1, 65):
+        n, total = k+1, [0]*(k+1)
+        for i in range(1, n):
+            p = add(outer(1, 1, n), outer(1 << i, 1 << i, n))
+            r = outer(1 | (1 << i), 1 | (1 << i), n)
+            need(mul(p, p) == p and mul(p, r) == mul(r, p) == r, 'Local capacity witness')
+            total = add(total, p)
+        need(mul(total, total) == total and rank(total) == k+k % 2, 'Sharp local reuse capacity')
+    return {'max_main_fields': 64, 'simplex_pairings': pairings,
+            'private_stage_controls': private_tests, 'sharp_local_capacities': 64}
+
+
+def rank_cut_controls():
+    n, us, vs = 4, [1, 2, 4, 8, 15], [14, 13, 11, 7, 15]
+    choices = []
+    for u, v in zip(us, vs):
+        ps = set()
+        for a, b in product(range(16), repeat=2):
+            if dot(v, a) and dot(b, u) and not dot(b, a):
+                ps.add(tuple(add(outer(u, b, n), outer(a, v, n))))
+        need(len(ps) == 16, 'Complete compatible projector alphabet')
+        choices.append(sorted(ps))
+    counts = {}
+    for k in (2, 3):
+        passed, ranks = 0, set()
+        for terms in product(*choices[:k]):
+            e = [0]*n
+            for p in terms:
+                e = add(e, p)
+            if mul(e, e) != e:
+                continue
+            passed += 1
+            ranks.add(rank(e))
+            need(rank(e) <= k+k % 2, 'Enumerated repeated-axis cut')
+        need(passed > 0 and max(ranks) == k+k % 2, 'Nonvacuous sharp capacity census')
+        counts[str(k)] = {'words': 16**k, 'idempotent_sums': passed, 'ranks': sorted(ranks)}
+    kernel_cases, factors = 0, []
+    for a, b in product(product(range(4), repeat=2), repeat=2):
+        e = mul(a, b)
+        if mul(e, e) == e:
+            need(rank(add(eye(2), mul(b, a))) == 2-rank(e), 'AB/BA kernel identity')
+            kernel_cases += 1
+            factors.append((a, b, e))
+    intersection_cases = 0
+    for (a, b, e), (c, d, f) in product(factors, repeat=2):
+        if mul(e, f) != mul(f, e):
+            continue
+        need(rank(mul(b, c)) <= rank(mul(e, f)) + 4-rank(e)-rank(f),
+             'Intersection cut with rank deficits')
+        intersection_cases += 1
+    bad = [2, 0]
+    need(mul(bad, bad) != bad and rank(add(eye(2), bad)) != 2-rank(bad),
+         'Non-idempotent control must fail the kernel identity')
+    return {'simplex_projector_census': counts, 'kernel_identity_cases': kernel_cases,
+            'intersection_factor_cases': intersection_cases,
+            'non_idempotent_control_rejected': True}
+
+
+def reusable_filter_controls():
+    path = PACKAGE / 'cuts.py'
+    module = ModuleType('caller_capacity_cuts')
+    exec(compile(path.read_bytes(), str(path), 'exec'), module.__dict__)
+    results = {}
+    for name in ('shortest-repeat-rejected', 'six-query-positive',
+                 'fourteen-query-intersection-rejected'):
+        candidate = json.loads((PACKAGE / 'examples' / (name+'.json')).read_text())
+        receipt = module.audit(candidate)
+        expected = 'PASS_NECESSARY_CUTS_ONLY' if name == 'six-query-positive' else 'REJECT_NECESSARY_CUT'
+        need(receipt['status'] == expected, 'Reusable cut filter fixture')
+        if name == 'fourteen-query-intersection-rejected':
+            need(all(x['target_count'] <= x['capacity'] for x in receipt['single_axis']),
+                 'Longer negative passes every separate rank cut')
+            need(all(x['kind'] == 'axis_intersection' for x in receipt['failures']),
+                 'Joint cut is the discriminating condition')
+        results[name] = receipt['status']
+    candidate['u'][0] = 0
+    try:
+        module.audit(candidate)
+    except ValueError:
+        results['invalid_query_frame'] = 'REJECTED'
+    else:
+        raise ValueError('Invalid query frame was accepted')
+    return results
+
+
+def incidence_controls():
+    records = {}
+    for m in range(3, 66):
+        n, dp = 2*m-2, {0: 0}
+        for _ in range(n):
+            new = {}
+            for used, value in dp.items():
+                for extra in range(min(m-2, 4-used)+1):
+                    d, key = 2+extra, used+extra
+                    new[key] = max(new.get(key, -1), value+d*(d-1)//2)
+            dp = new
+        maximum = dp[4]
+        need(maximum == {3: 12, 4: 16, 5: 19}.get(m, 2*m+12), 'Exact intersection maximum')
+        if m >= 4:
+            need(m % 2 == 0 or maximum < m*(m-1), 'Paired-stage saturation rejected')
+        if m <= 7:
+            records[str(m)] = {'max_intersections': maximum, 'required': m*(m-1),
+                               'parity_admissible': bool(m % 2)}
+    gl2 = [list(a) for a in product(range(4), repeat=2) if rank(a) == 2]
+    for x, z in product(gl2, repeat=2):
+        need(mul(inverse(x), x) == eye(2) and rank(mul(x, inverse(z))) == 2,
+             'Pair saturation forces full cross-pair rank')
+    need(96*7-1040 == -368 and 96*9-1040 == -176, 'Longer complete linear bounds')
+    return {'paired_stage_cases': records, 'packing_dp_max_m': 65,
+            'gl2_pair_controls': len(gl2)**2, 'n12_all_concave_upper': -368,
+            'n16_all_concave_upper': -176}
+
+
+def block_simplex_controls():
+    cases = 0
+    for n, q in [(n, q) for n in (4, 6, 12) for q in (2, 3, 7)] + [(4, 104)]:
+        blocks = [[(0 if i == j else 1) for j in range(n+1)] for i in range(n+1)]
+        gram = [sum(blocks[i][j] << (j*q+a) for j in range(n+1))
+                for i in range(n+1) for a in range(q)]
+        need(mul(gram, gram) == gram and rank(gram) == n*q, 'Block query Gram projection')
+        need(rank(add(eye(q*(n+1)), gram)) == q, 'Rank-q complement')
+        for k in range(1, n+2):
+            indices = range(q*k)
+            need(rank(submatrix(gram, indices, indices)) == q*(k-k % 2),
+                 'Block stage-capacity formula')
+            cases += 1
+    return {'rank_controls': cases, 'includes_port_count_104': True,
+            'total_dimension_contract': 'N=q*n and L=n+1'}
+
+
+def power_interval(r, numerator, denominator, bits=48):
+    """Enclose r^(numerator/denominator) with checked integer powers."""
+    scale = 1 << bits
+    if r == 1:
+        return scale, scale
+    target = pow(r, numerator) << (bits*denominator)
+    low, high = 0, r*scale+1
+    while high-low > 1:
+        mid = (low+high)//2
+        if pow(mid, denominator) <= target:
+            low = mid
+        else:
+            high = mid
+    need(pow(low, denominator) <= target < pow(high, denominator), 'Exact integer root bounds')
+    return low, high
+
+
+def moment_interval(coefficients, powers):
+    low = high = 0
+    for r, coefficient in coefficients.items():
+        a, b = powers[r]
+        low += coefficient * (a if coefficient >= 0 else b)
+        high += coefficient * (b if coefficient >= 0 else a)
+    return low, high
+
+
+def display_interval(pair):
+    with localcontext() as context:
+        context.prec = 32
+        return {'denominator': 1 << 48, 'lower_numerator': pair[0], 'upper_numerator': pair[1],
+                'lower_decimal': str(Decimal(pair[0])/(1 << 48)),
+                'upper_decimal': str(Decimal(pair[1])/(1 << 48))}
+
+
+def price_controls():
+    paths = {'original_P104': ROOT / 'research/p104-productive-controller/RESULT.json',
+             'PR5599_at_09dd0965': ROOT / 'research/p104-helper-subspace-splits/RESULT.json'}
+    source = ROOT / 'research/native-equality-cut/cuts.py'
+    equality = ModuleType('credited_equality_cuts')
+    exec(compile(source.read_bytes(), str(source), 'exec'), equality.__dict__)
+    ranks = [*range(1, 10), 17, 25]
+    p998 = {r: power_interval(r, 499, 500) for r in ranks}
+    p997 = {r: power_interval(r, 997, 1000) for r in ranks}
+    results = {}
+    for name, path in paths.items():
+        source = json.loads(path.read_text())['local']
+        paid = {int(r): c for r, c in source['paid'].items()}
+        helpers = {int(r): c for r, c in source['helpers'].items()}
+        c = {r: paid.get(r, 0)-helpers.get(r, 0) for r in set(paid) | set(helpers)}
+        debt = sum(r*count for r, count in c.items())
+        need(debt == 1720, 'Complete paid-minus-helper rank mass')
+        need(debt-2*8*104 == 56 > 104//2, 'P104 fails the debt design threshold')
+        hinges = [sum(count*max(r-j, 0) for r, count in c.items()) for j in range(1, 10)]
+        need(all(value <= 0 for value in hinges), 'All-concave local lower bound')
+        need([104*(f-1+16*f)-1720*f for f in range(3)] == [-104, -56, -8],
+             'Sharp complete shortest upper bounds')
+        need(Fraction(3016-1520*3, 3) < -8, 'All f>=3 excluded by decreasing bound')
+        costs = {r: -3*count for r, count in c.items()}
+        costs[25] = costs.get(25, 0)+208
+        need(max(r for r, value in costs.items() if value < 0) <
+             min(r for r, value in costs.items() if value > 0), 'Two-field sign separation')
+        two = moment_interval(costs, p998)
+        need(two[1] < 0, 'Two-field exception excluded at kappa .002')
+        longer = {}
+        for m in (4, 26):
+            coefficients = {r: -2*m*count for r, count in c.items()}
+            coefficients.update({17: 104*(2*m-5), 25: 312})
+            need(max(r for r, v in coefficients.items() if v < 0) <
+                 min(r for r, v in coefficients.items() if v > 0), 'Longer sign separation')
+            interval = moment_interval(coefficients, p997)
+            need(interval[1] < 0, 'Paired caller size endpoint excluded at kappa .003')
+            longer[str(m)] = display_interval(interval)
+        relaxed = {r: -14*count for r, count in c.items()}
+        relaxed.update({17: 8*104, 25: 4*104})
+        need(moment_interval(relaxed, p997)[0] > 0, 'Fourteen-call relaxation passes before joint cut')
+        invoice = {'paid': {str(r): 14*count for r, count in paid.items()},
+                   'targets': {str(r): 14*count for r, count in helpers.items()}}
+        invoice['targets'].update({'17': 8*104, '25': 4*104})
+        earlier_cut = equality.audit(invoice)
+        need(earlier_cut['status'] == 'PASS_NECESSARY_EQUALITY_CUTS',
+             'Earlier equality cuts do not reject the longer relaxation')
+        results[name] = {'paid': paid, 'helpers': helpers, 'net_rank_mass': debt,
+                         'hinges_at_1_through_9': hinges,
+                         'two_field_margin_at_kappa_002': display_interval(two),
+                         'paired_margin_at_kappa_003': longer,
+                         'n12_previous_equality_cut': earlier_cut,
+                         'n12_without_incidence_cut_positive': True}
+    return results
+
+
+def check():
+    sources = authenticate()
+    return {'status': 'PASS_CALLER_STAGE_CAPACITY_CUTS', 'authenticated_inputs': sources,
+            'operator_controls': operator_controls(), 'simplex_controls': simplex_controls(),
+            'rank_cut_controls': rank_cut_controls(), 'incidence_controls': incidence_controls(),
+            'block_simplex_controls': block_simplex_controls(),
+            'reusable_filter_controls': reusable_filter_controls(),
+            'complete_prices': price_controls(),
+            'limits': {'formal_kernel': False, 'independent_review': False, 'new_kappa': False,
+                       'native_word_replay': False,
+                       'model': 'Binary constant bases; commuting independent involutive axes; autonomous helpers'}}
+
+
+if __name__ == '__main__':
+    parser = argparse.ArgumentParser(description=__doc__)
+    parser.add_argument('--write-result', action='store_true')
+    args = parser.parse_args()
+    result = check()
+    serialized = json.dumps(result, indent=2, sort_keys=True)+'\n'
+    destination = PACKAGE / 'RESULT.json'
+    if args.write_result:
+        destination.write_text(serialized)
+    else:
+        need(destination.read_text() == serialized, 'Committed result differs from replay')
+    print(json.dumps(result, sort_keys=True))

From 6c088037e13b87faf7cfe3233c53d0ae51850dd8 Mon Sep 17 00:00:00 2001
From: Ali Romman <226877337+aliromman@users.noreply.github.com>
Date: Sun, 25 Oct 2026 18:23:41 -0500
Subject: [PATCH 2/2] Record portable replay and publication checkpoint

---
 .../README.md                                 |  7 +++++--
 .../VALIDATION.json                           | 14 +++++++++++++
 .../VALIDATION.md                             | 20 +++++++++++++++++--
 3 files changed, 37 insertions(+), 4 deletions(-)
 create mode 100644 research/shortest-controller-stage-capacity/VALIDATION.json

diff --git a/research/shortest-controller-stage-capacity/README.md b/research/shortest-controller-stage-capacity/README.md
index bec818fcad..4c99b88554 100644
--- a/research/shortest-controller-stage-capacity/README.md
+++ b/research/shortest-controller-stage-capacity/README.md
@@ -126,6 +126,8 @@ preserves the original card and states the changed scope. Canonical main was
 refreshed from `5e0052ca0aa3036a3afa8b0438927377c8d97d53` to
 `d7633ce230196a1d5d061347de7a0fd8be512ed6`; the frozen source pins remain.
 Priorities and the selected record did not change at that checkpoint.
+The final refresh to `6cf7a683f447b9f1e2333791907fd92be5009a63` also found
+no change in those authorities. The source pins stay fixed.
 [Discussion5593](https://github.com/CrocSwap/integer-mult-bounds/discussions/5593)
 is the canonical investigation. Local contact, helper-basis and G20 claims
 are separate. No selected-frontier change or scientific acceptance is implied.
@@ -134,8 +136,9 @@ are separate. No selected-frontier change or scientific acceptance is implied.
 
 - Extend the intersection bound to a quantitative rank loss that grows with
   caller size. Start from the rank-two complement and allow unsaturated
-  stage classes. This could close the remaining large paired-stage cases.
-  The present proof only forces one lost stage occurrence.
+  stage classes and permit coupled ports. This could close more of the
+  longer-caller domain. The separate-port proof only forces one lost
+  stage occurrence; its complete size bound does not cover coupled ports.
 - Search a changed caller with more queries, mixed calls or partially
   overlapping axis blocks. Apply both cuts before a full polynomial search,
   then verify the whole endpoint and complete bill. The filter is necessary
diff --git a/research/shortest-controller-stage-capacity/VALIDATION.json b/research/shortest-controller-stage-capacity/VALIDATION.json
new file mode 100644
index 0000000000..764e01bf90
--- /dev/null
+++ b/research/shortest-controller-stage-capacity/VALIDATION.json
@@ -0,0 +1,14 @@
+{
+  "commit": "7537009c656e441ad943ed75a4b32b010433b582",
+  "status": "PASS_CALLER_STAGE_CAPACITY_CUTS",
+  "git_free": true,
+  "read_only": true,
+  "path": "/nonexistent",
+  "elapsed_seconds": 1.2302264999598265,
+  "corrupted_source_rejected": true,
+  "restored_source_sha256": "1d92e587915052110dfb3aca8890df5afdaf496164efa5a4a52e69ceeb3c70f3",
+  "archive_sha256": "f1e20b53d105a1d142556367221f8fb8974c690a139bc7b9bf8b61d62d7edb05",
+  "exported_files": 47,
+  "final_main_refresh": "6cf7a683f447b9f1e2333791907fd92be5009a63",
+  "authoritative_guidance_changed": false
+}
diff --git a/research/shortest-controller-stage-capacity/VALIDATION.md b/research/shortest-controller-stage-capacity/VALIDATION.md
index 06b32dc49a..e3e80760b8 100644
--- a/research/shortest-controller-stage-capacity/VALIDATION.md
+++ b/research/shortest-controller-stage-capacity/VALIDATION.md
@@ -25,8 +25,24 @@ non-idempotent use of the kernel identity. A six-query positive word
 detects an incorrect extension of the shortest bound. The reusable CLI
 accepts that word's necessary data and rejects both committed false targets.
 
-The direct source-export and publication checks are recorded after the
-committed export is made. No native source word, huge uniform compiler word,
+The committed export at `7537009c656e441ad943ed75a4b32b010433b582` contains
+42 package files and five external inputs. Its manifest check passed. An
+isolated optimized replay passed in about 1.23 seconds with read-only files,
+no Git metadata and PATH set to `/nonexistent`. Changing one source byte
+was rejected by SHA256 before source code was loaded. The original bytes
+were restored. [VALIDATION.json](VALIDATION.json) records the exact archive
+hash, commit, runtime and source hash. Later validation prose does not
+change the scientific files checked by that export.
+
+Canonical main was refreshed to `6cf7a683f447b9f1e2333791907fd92be5009a63`
+before publication. AGENTS.md, autoresearch.md, the task catalogue, family
+guidance and selected result did not change from the previous refresh.
+The updated active claims were read. The p2 fixed-leakage projection-rank
+claim, P104 scalar rewrites and helper-basis work use different sources
+and contracts. Publication links and readbacks are saved with the project
+handoff after the PR is opened.
+
+No native source word, huge uniform compiler word,
 full integer multiplier, independent human review or proof-assistant kernel
 was run. Full-history provenance preflight was not run in this partial
 checkout; the required pinned source objects and bytes were checked.