diff --git a/research/noidle-root-defect/NOTICE b/research/noidle-root-defect/NOTICE
new file mode 100644
index 0000000000..e286e1ac07
--- /dev/null
+++ b/research/noidle-root-defect/NOTICE
@@ -0,0 +1,19 @@
+No-idle rank-two caller defect bound and exact verifier.
+Jerry Chen / @CubeJerry, with substantial OpenAI GPT-6 Astra Pro assistance.
+Apache-2.0.
+
+The header rank identity is rederived from DreamingOfClouds's
+CrocSwap/integer-mult-bounds#6832 (research/p104-query-block-bound).
+The shortest-header comparison is CrocSwap/integer-mult-bounds#6842.
+Earlier scoped rank/star arguments and the native monotonicity bound are
+CrocSwap/integer-mult-bounds#6840 and CrocSwap/integer-mult-bounds#6839.
+
+retained/pricing.py is unchanged from CrocSwap/integer-mult-bounds#6833,
+head 51f54e3c31f2f3a3e056a483b3ed66ae916ad06a. Its original header credits
+DreamingOfClouds, Jerry Chen / CubeJerry, zxv, Cao Yifan, Jacob Alan Sussman,
+and the binary/caller/native authors; the accompanying original NOTICE is
+retained as retained/NOTICE-pr6833.txt. The source is parsed for literal
+census constants only and is never imported by this package's verifier.
+
+The new graph/defect and complete-invoice result is a scoped obstruction.
+It does not claim a stronger kappa or change the selected frontier.
diff --git a/research/noidle-root-defect/PAIRED-DEFECT-ADDENDUM.md b/research/noidle-root-defect/PAIRED-DEFECT-ADDENDUM.md
new file mode 100644
index 0000000000..1fd751dcc6
--- /dev/null
+++ b/research/noidle-root-defect/PAIRED-DEFECT-ADDENDUM.md
@@ -0,0 +1,185 @@
+# Paired query blocks cannot supply six minimal commuting stages at defect two
+
+**Scoped obstruction; no new κ.** This addendum tests a proposed use of
+synchronized pairs of native copies sharing one fresh body variable. The
+aggregate query has rank two and its proposed productive stage has rank four.
+The following theorem permits arbitrary other queries, ordinary changes of
+basis, and arbitrary mixing within the four-dimensional productive stages.
+
+## Statement
+
+Let the ground field have characteristic different from two. On n independent
+coordinates, let
+
+\[
+R_i=X_iY_i,\qquad Y_iX_i=0,\qquad
+\operatorname{rank}X_i=\operatorname{rank}Y_i=r_i,
+\]
+
+and suppose the complete chronological query word satisfies
+
+\[
+(I-2R_s)\cdots(I-2R_0)=-I_n.
+\]
+
+Define the **rank defect** by
+
+\[
+\delta=\sum_{i=0}^{s}r_i-n.
+\]
+
+Assume δ=2. Select full positions with r_i=2, each supplied with a rank-four
+idempotent P_i satisfying P_iR_i=R_iP_i=R_i. If these P_i commute pairwise,
+there are at most five selected full positions.
+
+No actual-prefix commutation is needed for this theorem. Consequently it
+also applies to the stronger caller contract requiring that commutation.
+In particular, nine rank-two full blocks formed from eighteen native copies
+cannot have commuting rank-four productive stages at rank defect two,
+regardless of the number or placement of thin rank-one queries.
+
+This concerns the explicit square-zero block model. It does not classify
+arbitrary shared-variable calls whose aggregate query is not square-zero,
+higher rank defect, paid higher-rank stages, or noncommuting outputs. The
+bound five is not claimed sharp.
+
+## 1. Defect two fixes the cross-Gram blocks
+
+Stack X by block columns and Y by block rows. Put L=Σr_i, G=YX, and
+
+\[
+A=I_L+2\operatorname{lower}_{\mathrm{block}}(G).
+\]
+
+The same ordered-product expansion as the scalar query-defect identity gives
+product(I−2R_i)=I_n−2XA⁻¹Y. Thus XA⁻¹Y=I_n. The matrix Q=A⁻¹YX is an
+idempotent of rank n, so
+
+\[
+H=A-G=A(I_L-Q),\qquad \operatorname{rank}H=L-n=2.
+\]
+
+Its diagonal blocks are I_(r_i), and H_ij=sign(i−j)G_ij off the diagonal.
+Factor H=UV through a two-dimensional space. The block factors obey
+U_iV_i=I_(r_i). At every selected rank-two position, U_i and V_i are
+inverse square matrices. The factor gauge X_i↦X_iU_i and Y_i↦U_i⁻¹Y_i
+leaves R_i unchanged and makes both of its defect factors equal to I₂.
+Therefore selected positions have
+
+\[
+Y_iX_j=\operatorname{sign}(i-j)I_2\quad(i\ne j),
+\qquad Y_iX_i=0.
+\tag{1}
+\]
+
+This step includes every other query in A, G and the rank defect. It does
+not omit the cost or rank of thin queries. The block extension retains the
+query-defect mechanism of CrocSwap/integer-mult-bounds#6832; no new claim of
+priority is made for that mechanism.
+
+## 2. Six selected queries require twelve dimensions
+
+Take six selected positions in chronological order. Their Gram is S₆⊗I₂,
+where S₆[i,j]=sign(i−j). This matrix has rank twelve over every field: the
+integer inverse of S₆ has entries (−1)^(i+j)sign(i−j), using zero-based
+indices. Hence the twelve query columns span twelve independent dimensions.
+Every supporting stage union must contain them.
+
+Commuting idempotents admit a common coordinate basis over the ground field
+by successively splitting into images and kernels. In this basis each P_i
+has a four-element support C_i. The support equations imply P_iX_i=X_i
+and Y_iP_i=Y_i because the query factors have full rank. Consequently the
+rank-two product in (1) passes through C_i∩C_j, giving
+
+\[
+|C_i\cap C_j|\ge2\qquad(i\ne j).
+\tag{2}
+\]
+
+We show that six such supports satisfying (1) have union of size at most
+ten, contradicting the twelve-dimensional requirement.
+
+## 3. The set-family bound away from a common pair
+
+Consider m four-element supports satisfying (2), allowing repetitions. If
+every pair intersects in at least three elements, fixing one support shows
+that each later one adds at most one element. The union has size at most m+3.
+
+Otherwise choose C₁=A∪B and C₂=A∪C, where A, B and C are disjoint pairs.
+If every support contains A, proceed to Section4. Otherwise choose E missing
+at least one element of A. Meeting C₁ and C₂ twice forces E to contain at
+least three elements of their six-element union, or all four if E misses
+both elements of A. Thus T=C₁∪C₂∪E has size at most seven.
+
+Any further support D adds at most one element to T. If it added two or
+more, its at most two old elements would have to be exactly A to meet C₁
+and C₂ twice. It would then meet E at most once, contradicting (2). Therefore
+
+\[
+\left|\bigcup_i C_i\right|\le 7+(m-3)=m+4.
+\tag{3}
+\]
+
+## 4. The ordered signs bound the common-pair case
+
+Suppose every support contains a fixed pair A, and write E_i=C_i∖A. The
+two-element outside sets E_i form the edges of a graph.
+
+That graph cannot contain three pairwise disjoint edges E_i, E_j, E_k.
+Order their query indices i<j<k. Their stage intersections are exactly A.
+Let α_l=X_l[A,:] and β_l=Y_l[:,A]. These square two-by-two matrices are all
+invertible, since their cross-products in (1) are invertible. The equations
+
+\[
+\beta_i\alpha_j=\beta_i\alpha_k=-I_2,\qquad
+\beta_j\alpha_i=\beta_k\alpha_i=I_2
+\]
+
+force α_j=α_k and β_j=β_k. But then β_jα_k=β_kα_j, whereas (1) requires
+the first product to be −I₂ and the second I₂. Characteristic different
+from two rules this out.
+
+Thus the outside graph has matching number at most two. If it has v incident
+vertices, e distinct edges and c connected components, then v≤e+c: every
+component has at least its vertex count minus one edges. Selecting one edge
+in every component gives c≤2. Since e≤m, including repeated supports,
+
+\[
+\left|\bigcup_i C_i\right|=2+v\le2+e+2\le m+4.
+\tag{4}
+\]
+
+For m=6, both cases give union size at most ten. This contradicts the rank
+twelve Gram and proves the theorem.
+
+## Exact controls and the limits they check
+
+Run `python3.12 -I -B verify_paired_defect.py` or its optimized `-O` variant.
+Both return `PASS_PAIRED_DEFECT_TWO_STAGE_CAP`. The verifier uses only the
+Python standard library and exact rational or finite-field arithmetic.
+
+It verifies the integer sign-matrix inverse, 671 normalized set-extension
+cases, extremal ten-coordinate families in both set-family cases, and
+repeated supports. A three-full-block defect-two root with stages I₄ is a
+positive control, showing the hypotheses are nonempty.
+
+The omission controls are mathematical boundary examples. A literal
+seven-block defect-two root on twelve coordinates admits six rank-four
+supporting projectors with eleven noncommuting pairs; the commutation gate
+rejects it. A characteristic-two sunflower realizes six rank-two queries
+with the stipulated Gram and commuting rank-four supports on fourteen
+coordinates. This latter example concerns the isolated Gram/support lemma,
+not a native caller: it shows why the sign contradiction needs its stated
+characteristic restriction. An altered sign-matrix inverse is also rejected.
+
+The universal theorem is proved above; these finite checks are controls of
+its premises and algebra, not a finite-search impossibility claim. The
+optimistic positive cost margin for nine rank-four stages cannot yield a
+caller because those stages do not exist in this model. No κ is changed.
+
+Prepared for @CubeJerry with substantial OpenAI GPT-6 Astra Pro assistance.
+Canonical base: `7c49fe32c55de02c2c873655c804b16e4c3fef0a`.
+Credit the retained query/controller lineage and the defect identity in
+CrocSwap/integer-mult-bounds#6832. Related coupled geometry in
+CrocSwap/integer-mult-bounds#6773 and #6781 concerns different four-field
+stage budgets. The set-family/sign obstruction above is the present addition.
diff --git a/research/noidle-root-defect/PROOF.md b/research/noidle-root-defect/PROOF.md
new file mode 100644
index 0000000000..941747dba1
--- /dev/null
+++ b/research/noidle-root-defect/PROOF.md
@@ -0,0 +1,372 @@
+# A defect bound for no-idle rank-two query callers
+
+**Scoped obstruction; no new κ.** This note concerns a normalized,
+arbitrary-input caller with nonzero rank-one queries, a fresh coordinate
+rank-two stage at each full query, and no idle stage operations. It does not
+exclude the idle-bearing caller of CrocSwap/integer-mult-bounds#6833,
+noncommuting productive masks, or different native suppliers.
+
+## 1. Model and statement
+
+Work over a field of characteristic different from two. There are `n`
+independent productive fields. For `N` query positions, let
+
+\[
+R_i=x_i y_i,\quad y_i x_i=0,\quad
+T_i(S)=I+(S-1)R_i,\quad S^2=1.
+\]
+
+Here `x_i` is a column, `y_i` a row, and each query operator is nonzero rank one.
+The complete query word obeys
+
+\[
+T_N(S)\cdots T_1(S)=S I_n.\tag{1}
+\]
+
+No input is assumed zero; every field is an independent restored productive
+input. Put `δ=N−n`. Of these positions, `F` are full native calls. At each full
+position there is a fresh commuting formal stage `D_i`, of rank eight in the
+priced source, and a coordinate rank-two projector `P_i` with
+`P_i R_i=R_i P_i=R_i`. The full call has normalized form
+
+\[
+(I+(D_i-1)P_i)T_i(S).
+\]
+
+All `P_i` are coordinate projectors in **one common basis**. Their two-element
+supports may repeat; `F` counts full occurrences with multiplicity. The other
+`q=N−F` positions are thin queries with arbitrary rank-one square-zero operators,
+supports, and positions. There are no idle stage calls or other operations
+involving the `D_i`. The complete caller must produce independent whole targets
+with one `S` and each stage incident to that coordinate appearing once. Thus a
+coordinate of full-stage incidence degree `d` has target rank `1+8d`.
+These target conditions are hypotheses: (1) alone does not establish a caller.
+
+Ordinary invertible basis controls independent of `S` and all stages can be
+absorbed into normalized queries and projectors. If the resulting endpoint is
+diagonal in independent formal stages and equals the identity when all stages
+and `S` equal one, the product of those controls is the identity. Set `S=1`, set
+every stage except `D_i` to one, and compare the coefficient of `D_i−1`: the
+absorbed projector is the diagonal incidence projector of that stage in the
+target. This explains when the common-coordinate premise follows from a
+normalized whole-target contract. It does not justify it for stage-dependent
+controls, restricted-input states, quotient targets, or noncommuting outputs.
+
+**Theorem.** Every caller in this class satisfies
+
+\[
+F\le 2\delta(\delta+1).\tag{2}
+\]
+
+For eighteen native calls with the exact helper/paid profile retained from
+CrocSwap/integer-mult-bounds#6833, no caller in this class can reach that
+contribution's pending `κ=0.00337180`. Its complete signed moment has one of two
+explicit upper envelopes, whose unique crossings in `κ` obey
+
+\[
+0.0033288660495<\kappa_3<0.0033288660497,
+\]
+
+\[
+0.0029312090589<\kappa_{\ge4}<0.0029312090593.
+\]
+
+These are upper bounds on this class, not attained constructions or new
+multiplication bounds. Section 6 excludes any later positive interval.
+
+## 2. The rank defect of the entire query word
+
+Let `X=[x_1 ... x_N]`, let `Y` have rows `y_i`, and set
+
+\[
+G=YX,\qquad A=I_N+2\operatorname{lower}(G),
+\]
+
+where `lower` is the strictly lower triangular part. Expanding at `S=−1` gives
+
+\[
+(I-2R_N)\cdots(I-2R_1)=I_n-2XA^{-1}Y.\tag{3}
+\]
+
+Indeed, with `L=lower(G)`, the finite series `A^{-1}=I−2L+4L²−...` enumerates all
+strictly decreasing chains of query indices in the ordered product. Every term
+of degree `k` in `−2XA^{-1}Y` has coefficient `(-2)^k` and exactly the factors in
+the direct ordered-product expansion.
+
+Equation (1) implies `XA^{-1}Y=I_n`. Thus `Q=A^{-1}YX` is an idempotent of rank
+`n`: `Q²=Q`, and `XA^{-1}Y=I_n` makes `X` surjective and `A^{-1}Y` injective.
+Consequently
+
+\[
+B=A-G=A(I_N-Q),\qquad \operatorname{rank}B=N-n=\delta.\tag{4}
+\]
+
+In particular
+
+\[
+B_{ii}=1,\qquad B_{ij}=\operatorname{sgn}(i-j)G_{ij}\quad(i\ne j).\tag{5}
+\]
+
+This uses **all** positions, including every thin operator. No assumption about
+a thin operator's support or commutation was made. Adding arbitrary thin
+operators changes `N`, `δ`, and the paid query count; it cannot evade (4).
+The unit diagonal implies `δ≥1`. The determinant of (1) also requires even `n`,
+but the bounds below do not need this additional restriction.
+
+## 3. The full-support graph
+
+Form a simple graph `H` on the `v` coordinates incident to at least one full
+call, with an edge for each distinct full support pair. Parallel occurrences
+are discarded **only in this graph**. A nonzero rank-one square-zero operator
+cannot live in one coordinate, so each full support really is a pair. Write
+`ν` for maximum matching size and `Δ` for maximum degree.
+
+### 3.1 A matching costs rank
+
+Select one full occurrence on each edge of a matching. Their coordinate supports
+are disjoint, so every off-diagonal `G_ij` in their principal block vanishes.
+By (5) the block of `B` is `I_ν`. Hence
+
+\[
+\nu\le\delta.\tag{6}
+\]
+
+### 3.2 A star costs at least half its degree
+
+Fix hub `z` with `k` distinct neighbours; select one full query on each incident
+pair, in actual temporal order. Distinct supports meet only at `z`. Put
+`a_i=x_i[z]`, `c_i=y_i[z]`. Then
+
+\[
+G_{ij}=c_i a_j\quad(i\ne j).\tag{7}
+\]
+
+The pair `(a_i,c_i)` cannot be `(0,0)`: otherwise both factors would live on the
+other coordinate, where `y_i x_i=0` forces a zero operator.
+
+First assume every `σ_i=a_i c_i` is nonzero. Conjugating the principal block of
+`B` by `diag(a_i)` gives off-diagonal entries `sgn(i−j) σ_i`. Divide row `i` by
+`σ_i` to obtain `C` with off-diagonal entries `sgn(i−j)` and diagonal `1/σ_i`.
+Therefore
+
+\[
+C+C^T=2\operatorname{diag}(1/\sigma_i),\qquad
+k\le2\operatorname{rank}C.
+\]
+
+The principal block has rank at least `ceil(k/2)`.
+
+Now allow zeros. An index with `c_i=0` has a unit row in the principal block of
+`B`; one with `a_i=0` has a unit column. These sets are disjoint. Simultaneously
+permute rows and columns, putting zero-`c` indices first, nonzero-product
+indices next, and zero-`a` indices last. The block has shape
+
+\[
+\begin{pmatrix}I&0&0\\ *&M&0\\ *&*&I\end{pmatrix}.
+\]
+
+With `z_0` zero-product indices, elimination gives rank
+`z_0+rank(M)≥z_0+ceil((k−z_0)/2)≥ceil(k/2)`. The nonzero middle block retains its
+temporal order and the symmetrization applies. Thus
+
+\[
+\Delta\le2\delta.\tag{8}
+\]
+
+This degree counts distinct neighbours, not repeated occurrences. No coefficient
+alphabet or special hub sign pattern was assumed.
+
+### 3.3 Count parallel occurrences separately
+
+Restrict `A,G,B` to all full positions in increasing order. The principal block
+`A_F` is unit lower triangular, so has rank `F`. All selected columns and rows
+are supported in the same `v` active coordinates, so `rank(G_F)≤v`. Thus
+
+\[
+F=\operatorname{rank}A_F\le\operatorname{rank}B_F+
+\operatorname{rank}G_F\le\delta+v.\tag{9}
+\]
+
+This step counts every parallel full occurrence.
+
+### 3.4 Maximum matching controls active vertices
+
+Every simple graph without isolated vertices satisfies
+
+\[
+v\le\nu(\Delta+1).\tag{10}
+\]
+
+To prove it, fix a **maximum**, not merely maximal, matching. Unmatched vertices
+form an independent set and each has a neighbour on a matched edge. For a
+matched edge `ab`, if both endpoints have unmatched neighbours, their neighbour
+sets must be the same singleton: two distinct unmatched neighbours would give
+an augmenting path of length three. Otherwise only one endpoint has unmatched
+neighbours, at most `Δ−1` of them. For `Δ≥2`, every matched edge consequently
+sees at most `Δ−1` distinct unmatched vertices. Summing covers every unmatched
+vertex, bounding their number by `ν(Δ−1)`. Add the `2ν` matched vertices.
+For `Δ=1`, the graph itself is a matching. The empty graph is immediate.
+
+Combining (6), (8), (9), and (10),
+
+\[
+F\le v+\delta\le\nu(\Delta+1)+\delta
+\le\delta(2\delta+1)+\delta=2\delta(\delta+1).
+\]
+
+Eighteen full calls therefore require `δ≥3`. The necessary bounds `F≤4` at
+`δ=1` and `F≤12` at `δ=2` do not assert either bound is attainable.
+
+## 4. The exact eighteen-call price
+
+Parse the literal `HELPERS` and `LOCAL_PAID` dictionaries in byte-pinned
+`retained/pricing.py`, without importing it. Their difference at ranks one
+through nine is
+
+\[
+(d_1,\ldots,d_9)=(-2220,-446,-485,-1,-135,-4,1,39,359).
+\]
+
+For `0<t<1`, define
+
+\[
+D(t)=\sum_{r=1}^9d_r r^t,\qquad \phi_t(d)=(1+8d)^t-1.
+\]
+
+There are eighteen native calls and 104 ports. Every full support contributes
+two incidence units, so `sum_v d_v=36`, counting parallel calls each time.
+The `n` independent targets and `q=N−18=n+δ−18` thin queries have complete signed
+target-minus-paid moment
+
+\[
+\begin{aligned}
+M(t)&=18D(t)+104\left[\sum_{v=1}^n(1+8d_v)^t-q\right]\\
+&=18D(t)+104\left[18-\delta+\sum_{v=1}^n\phi_t(d_v)\right].\tag{11}
+\end{aligned}
+\]
+
+This includes every native helper, native paid request, main target, and thin
+query in the class. Degree-zero coordinates are not omitted: their rank-one
+target contribution cancels the corresponding part of the thin-query count.
+This is a favorable invoice for an obstruction. Additional paid operations or
+nonrecursive implementation overhead cannot repair a negative moment bound.
+
+## 5. Two universal moment envelopes
+
+### 5.1 Defect three
+
+By (6), a maximum matching has at most three edges. Its endpoints form a vertex
+cover of size at most six; pad with degree-zero slots if necessary. Let `h` be
+the sum of full-occurrence degrees in these slots. Each full edge meets the
+cover, including repeated edges, so `18≤h≤36`. Concavity gives
+
+\[
+\sum_{\mathrm{cover}}\phi_t(d_v)\le6\phi_t(h/6).
+\]
+
+For integral `d≥0`, concavity and `φ_t(0)=0` give `φ_t(d)≤d φ_t(1)`. The other
+slots contribute at most `(36−h)φ_t(1)`. The function
+
+\[
+f(h)=6\phi_t(h/6)+(36-h)\phi_t(1)
+\]
+
+is strictly decreasing for `18≤h≤36`: its derivative is
+`φ_t'(h/6)−φ_t(1)<0`, since `h/6≥3` and the derivative of a strictly concave
+function there is less than its average derivative on `[0,1]`. Therefore
+
+\[
+\sum_v\phi_t(d_v)\le6\phi_t(3)+18\phi_t(1).
+\]
+
+Substitute `δ=3` into (11):
+
+\[
+M(t)\le E_3(t):=18D(t)+104[6\,25^t+18\,9^t-9].\tag{12}
+\]
+
+### 5.2 Every larger defect
+
+For all `δ≥4`, use `sum_v φ_t(d_v)≤36φ_t(1)` and `18−δ≤14` in (11):
+
+\[
+M(t)\le E_4(t):=18D(t)+104[36\,9^t-22].\tag{13}
+\]
+
+This bounds every larger defect, every number of thin queries, and every number
+of unused productive coordinates in the stated class, without a finite cutoff.
+
+## 6. Crossings and no re-entry
+
+The rational interval verifier certifies the crossing brackets in Section 1.
+For orientation, proposal values are approximately
+`κ_3=0.003328866049597376` and `κ_≥4=0.002931209059061556`. At
+`C=0.0033718004755`, it certifies
+
+\[
+-7.086<E_3(1-C)<-7.085,\qquad
+-67.047<E_4(1-C)<-67.046.
+\]
+
+Rational arithmetic encloses these decimals; floating point determines no sign.
+The verifier also checks negativity at the pending headline `C=0.00337180`.
+
+Normalize by `9^t` to rule out a later positive interval. On `0≤t≤1`, the
+negative-coefficient terms with `r<9` in `D(t)/9^t` have positive derivative.
+Keep just the `r=1` positive derivative and bound the two negative derivatives:
+
+\[
+\begin{aligned}
+\frac{d}{dt}\frac{D(t)}{9^t}
+&\ge\frac{2220}{9}\log9-\log(9/7)-39\log(9/8)\\
+&\ge\frac{2220\cdot8}{81}-\frac27-\frac{39}{8}
+=\frac{323717}{1512}>0.\tag{14}
+\end{aligned}
+\]
+
+The elementary inequalities are `log x≥(x−1)/x` and `log x≤x−1` for `x≥1`.
+This native monotonicity estimate is retained from
+CrocSwap/integer-mult-bounds#6839 and recomputed here.
+
+The remaining nonconstant terms of `E_3(t)/9^t` are
+`624(25/9)^t−936/9^t`, both increasing. In `E_4(t)/9^t`, the remaining
+nonconstant term is `−2288/9^t`, also increasing. Both normalized envelopes are
+strictly increasing in `t`, hence decreasing in `κ=1−t`. The unnormalized envelopes at `t=1` equal
+552 and 448, and at `t=0` both are negative. Each has exactly one crossing;
+neither can become positive after its crossing.
+
+## 7. Prior and concurrent work; limitations
+
+CrocSwap/integer-mult-bounds#6833 supplies the pinned eighteen-call native
+profile and the stronger **idle-bearing** pending benchmark. Its native source
+is CrocSwap/integer-mult-bounds#6824. The header rank identity in Section 2 is a
+rederivation of the query-block defect identity in DreamingOfClouds's
+CrocSwap/integer-mult-bounds#6832 (`research/p104-query-block-bound`, head
+`99a165a81be808f45c1b6f4b0a809145ac7923d1`). The shortest-header classification in
+CrocSwap/integer-mult-bounds#6842 concerns `N=n+1`; this argument treats all
+defects but only coordinate rank-two no-idle callers.
+
+The star symmetrization extends scoped rank ideas in
+CrocSwap/integer-mult-bounds#6840. New here are arbitrary hub coefficients and
+zero-product cases, simple-graph versus occurrence counting, the universal
+full-call defect bound, and its complete native invoice consequence.
+CrocSwap/integer-mult-bounds#6839 provides a preceding chain-family ceiling and
+the native monotonicity estimate. The present family is not restricted to
+chains. Pending claims are not treated as admitted selected frontiers.
+
+An algebraic quotient can close a root with fewer fields and one thin query
+without contradicting this result. If such a quotient had eighteen nonzero
+full queries and `δ=1`, (2) says that its eighteen stage masks could not all be
+coordinate rank-two projectors in one independent-target basis under this
+model. The compatible productive projectors, not root closure alone, are the
+remaining obligation. This is a conditional consequence, not an assertion that
+an unfinished quotient proposal is incorrect.
+
+The theorem does not cover idle stage work, higher-rank full masks,
+noncoordinate productive output representations, stage-dependent controls,
+zero-query native calls, non-rank-one queries, dirty auxiliary fields that are
+restored but not independent productive targets, characteristic two, or changed
+native prices. Finite matrix/graph controls in `verify.py` test implementation
+and boundary cases; the universal statements are proved above, not inferred
+from finite tests. No claim about all multiplication algorithms, removal of
+inherited framework assumptions, or stronger selected κ follows.
diff --git a/research/noidle-root-defect/README.md b/research/noidle-root-defect/README.md
new file mode 100644
index 0000000000..03463cf605
--- /dev/null
+++ b/research/noidle-root-defect/README.md
@@ -0,0 +1,207 @@
+# Root-defect bounds for minimal productive stages
+
+**No new κ.** A normalized caller with `N` nonzero rank-one square-zero query
+operators on `n` independent productive fields, and `F` full calls with fresh
+coordinate rank-two stage masks in one common basis, must satisfy
+
+\[
+F\le2\delta(\delta+1),\qquad \delta=N-n,
+\]
+
+provided it has no idle stage operations. Thin queries may have arbitrary
+supports and positions; repeated full supports are counted with multiplicity.
+The proof covers every defect and does not assume a shortest root, a chain,
+fixed scalar signs, or a finite query-count cutoff.
+
+For the exact eighteen-call native profile from
+CrocSwap/integer-mult-bounds#6833, this forces `δ≥3`. Complete target/paid
+accounting gives the following rigorous raw upper ceilings:
+
+| Defect | Complete-moment crossing bracket in κ |
+|---|---|
+| `δ=3` | `(0.0033288660495, 0.0033288660497)` |
+| Every `δ≥4` | `(0.0029312090589, 0.0029312090593)` |
+
+Both ceilings are below the pending **idle-bearing** benchmark `κ=0.00337180`
+of CrocSwap/integer-mult-bounds#6833. At that headline, the respective upper
+moments are enclosed by `(-7.08514120910689,-7.08514120910688)` and
+`(-67.04640429875804,-67.04640429875803)`. A global monotonicity argument rules
+out a later favorable interval. These are upper bounds on a restricted caller
+family, not achievable κ values. The accepted selected frontier at the frozen
+base remains `κ=0.003125804`; this package makes no selection change.
+
+## A paired-query extension
+
+A separate theorem tests a route around the scalar-query restriction: couple
+pairs of native copies into square-zero rank-two query blocks and allow
+commuting productive stages of rank four. At total rank defect two, **at most
+five such full blocks can exist**, even with arbitrary intervening queries.
+Thus nine paired full blocks cannot realize the proposed eighteen-native-copy
+shortcut. The theorem does not require actual-prefix commutation, and five is
+not claimed attainable.
+
+The proof in [PAIRED-DEFECT-ADDENDUM.md](PAIRED-DEFECT-ADDENDUM.md) combines
+the block defect identity with an ordered-sign constraint on intersections of
+four-dimensional stage supports. Six full blocks require twelve dimensions,
+whereas their stage supports can span at most ten. It permits arbitrary mixing
+inside each stage and repeated supports. The separate reconstruction in
+[SIX-FULL-REVIEW.md](SIX-FULL-REVIEW.md) checks both branches of that argument;
+its verifier imports no author implementation. These finite controls corroborate
+the proof and demonstrate why commutation and the field characteristic matter.
+
+## Why this matters
+
+Adding query factors can improve a root's geometric freedom, but each additional
+factor also creates a paid request. The defect identity connects that query
+budget to the full stage-support graph. A matching costs defect rank, a star of
+`k` distinct neighbours costs at least `ceil(k/2)`, and repeated full occurrences
+are separately constrained by active coordinates plus defect. These constraints
+force the complete relaxed invoice to lose before the pending benchmark.
+
+The result isolates a real interface limitation: a short algebraic root on a
+quotient does not by itself produce eighteen compatible rank-two productive
+stage masks. With `δ=1`, the theorem would permit at most four full occurrences
+in the declared class. A quotient or moving-carrier mechanism can still be
+valuable if it changes the target representation or another stated premise and
+pays the resulting restoration and stage work.
+
+The complete proof, including zero hub entries and ordinary-control normalization,
+is in [PROOF.md](PROOF.md). Exact reproducibility evidence is in
+[RESULT.json](RESULT.json). The finite graph/matrix checks corroborate boundary
+cases; the universal theorem is established by the proof, not by enumeration.
+
+[REVIEW.md](REVIEW.md) records a separate mathematical derivation and a second
+rational arithmetic implementation, [audit_price.py](audit_price.py). Its
+positive-exponential enclosure and direct derivative proof independently
+corroborate the two losing envelopes. The registered replay runs both
+implementations normally and with assertions disabled.
+
+## Provenance and what is new
+
+Base: `7c49fe32c55de02c2c873655c804b16e4c3fef0a`. The selected record and original
+`joint-query-controller` task card are pinned as historical provenance in
+[SOURCES.json](SOURCES.json); the card is retained verbatim in [TASK.json](TASK.json).
+
+The native profile is parsed from an unchanged, retained source file from
+CrocSwap/integer-mult-bounds#6833, head
+`51f54e3c31f2f3a3e056a483b3ed66ae916ad06a`, Git blob
+`7d9ff06de9dfbba31c06a141e6cacd9806852a41`. Its SHA256 and exact originating path
+are in [retained/SOURCE-PINS.json](retained/SOURCE-PINS.json). Replay verifies both
+hashes, uses `ast.literal_eval` on the two census dictionaries, and never imports
+or executes the retained source. No remote file or uninstalled dependency is
+needed for direct replay.
+
+DreamingOfClouds's CrocSwap/integer-mult-bounds#6832
+(`research/p104-query-block-bound`, head
+`99a165a81be808f45c1b6f4b0a809145ac7923d1`) establishes the predecessor header
+rank identity; Section 2 rederives it. CrocSwap/integer-mult-bounds#6842 classifies
+the shortest-header case. CrocSwap/integer-mult-bounds#6840 supplies earlier
+scoped star symmetrization, and CrocSwap/integer-mult-bounds#6839 supplies the
+retained normalized native derivative estimate. The new result combines the
+rank defect with maximum matching, arbitrary-coefficient star rank including
+zeros, multiplicity accounting, and the complete no-idle invoice. It does not
+repeat the earlier chain-family ceiling or make a novelty claim for the
+inherited displacement identity.
+
+## Reproduce
+
+From the repository root, using Python 3.12 and only its standard library:
+
+```sh
+python3.12 -B research/noidle-root-defect/verify.py
+```
+
+Expected final output:
+
+```text
+PASS_NOIDLE_ROOT_DEFECT
+No new kappa; F=18 requires defect>=3; both complete envelopes lose to 0.00337180.
+Exact controls: 33867 graphs, 3905 star blocks, 10 roots, 9 rejection controls.
+```
+
+The registered package also runs the replay under `-O`, using explicit checks
+that remain active when assertions are disabled:
+
+```sh
+python3.12 scripts/research_package.py --package research/noidle-root-defect --check-only
+python3.12 scripts/research_package.py --package research/noidle-root-defect
+```
+
+`VERIFY.json` registers the scalar verifier, independent pricing audit, paired-query
+controls and their independent boundary checker, each normally and under `-O`. The only optional
+regeneration command is `python3.12 -B research/noidle-root-defect/verify.py --write`;
+ordinary replay recomputes and requires exact equality with `RESULT.json`.
+
+## Verification and negative controls
+
+The completed deterministic finite domain is all 33,867 labelled simple graphs
+on one through six vertices; all 3,905 ordered star blocks of sizes one through
+five over the explicitly recorded five-pair coefficient alphabet, including
+3,542 zero-product cases; and ten exact rational roots. Root fixtures include
+parallel full supports and dense thin identity pairs. There is no random seed
+and no early stopping: these finite domains are fully exhausted. Their purpose
+is to check implementation and delicate boundary cases, not to infer the
+universal theorem.
+
+Exact rational logarithm and exponential enclosures certify both crossing
+brackets, both negative benchmark tests, and the positive monotonicity lower
+bound. The source profile is byte-authenticated. Nine rejection controls cover
+source corruption, an invalid exponent, a changed root coefficient, zero and
+one-coordinate queries, the false stronger star bound, replacing maximum
+matching by maximal matching, omitting a thin-query charge, and collapsing
+parallel occurrences. Omitting a single thin charge actually changes the
+relaxed defect-three benchmark from negative to positive, so that control tests
+a mathematically consequential accounting failure.
+
+The lead reviewer separately reconstructed the graph/rank proof, including the
+zero-product pivots, and independently implemented rational bounds with a
+positive exponential series. That different arithmetic computation agrees with
+the author's alternating exponential computation to all fourteen displayed
+decimal places. The reviewer also obtained a separate no-re-entry proof from
+separation of the negative coefficient ranks `2..6` and positive ranks `7,8,9,25`.
+The author's self-contained replay remains the registered package verifier.
+
+## Scope and unfinished obligations
+
+The scalar theorem requires nonzero rank-one square-zero normalized queries,
+characteristic different from two, arbitrary independent productive inputs,
+fresh stages acting through rank-two coordinate projectors in one common basis,
+and no idle stage operations. It does not cover higher-rank full stage masks,
+stage-dependent controls, noncoordinate or noncommuting output representations,
+zero-query native calls, nonproductive restored auxiliaries, or changed native
+prices. It does not invalidate CrocSwap/integer-mult-bounds#6833, whose useful
+caller pays for idle work, and it does not remove the selected theorem's five
+inherited framework assumptions. No native/caller/compiler/outer admission
+replay is claimed or needed to prove this scoped negative result.
+
+## Open next questions
+
+The paired theorem leaves higher rank defect, larger paid stages, noncommuting
+outputs and non-square-zero shared-variable aggregates open. Can one of those
+changes support a complete favorable native/target/paid invoice? First exhibit
+its stage projectors and closure identity; an optimistic target census alone
+does not settle productive compatibility.
+
+A concrete algebraic quotient may have a short root yet lack compatible
+productive projectors. Can it instead realize a restored output representation
+outside the simultaneous coordinate rank-two contract, with a complete paid
+invoice below the pending threshold? First derive its exact stage operators and
+all restoration/output targets, then identify which premise above fails. The
+missing legal productive interface and full accounting remain the blocker.
+
+For idle-bearing callers, can a changed non-shortest root lower the combined
+native, thin-query, idle and restoration bill? The present theorem deliberately
+leaves that question open. A useful first experiment must derive an explicit
+stage/idle decomposition and a favorable complete moment before any expensive
+search; an algebraic root alone is insufficient.
+
+## Credit
+
+Prepared by Jerry Chen / **@CubeJerry**, with substantial **OpenAI GPT-6 Astra Pro**
+assistance for mathematical exploration, proof development, implementation, and
+review. The lead reviewer used a separate reasoning and arithmetic implementation.
+Credit DreamingOfClouds for the query-block rank identity and the retained
+chain-nested caller/native profile, the native source lineage of
+CrocSwap/integer-mult-bounds#6824, and all predecessors named in
+[NOTICE](NOTICE) and [retained/NOTICE-pr6833.txt](retained/NOTICE-pr6833.txt).
+New work is Apache-2.0; retained source headers and notices are unchanged.
diff --git a/research/noidle-root-defect/RESULT.json b/research/noidle-root-defect/RESULT.json
new file mode 100644
index 0000000000..69cf3d200b
--- /dev/null
+++ b/research/noidle-root-defect/RESULT.json
@@ -0,0 +1,293 @@
+{
+  "claim": "F <= 2*delta*(delta+1), coordinate rank-two no-idle class only",
+  "envelopes": {
+    "3": {
+      "crossing_bracket": [
+        "0.0033288660495",
+        "0.0033288660497"
+      ],
+      "lower_margin": [
+        "0.00000001607310",
+        "0.00000001607311"
+      ],
+      "pending_headline_margin": [
+        "-7.08514120910689",
+        "-7.08514120910688"
+      ],
+      "pending_raw_upper_margin": [
+        "-7.08521967330103",
+        "-7.08521967330102"
+      ],
+      "upper_margin": [
+        "-0.00000001693377",
+        "-0.00000001693376"
+      ]
+    },
+    "4": {
+      "crossing_bracket": [
+        "0.0029312090589",
+        "0.0029312090593"
+      ],
+      "lower_margin": [
+        "0.00000002456851",
+        "0.00000002456852"
+      ],
+      "pending_headline_margin": [
+        "-67.04640429875804",
+        "-67.04640429875803"
+      ],
+      "pending_raw_upper_margin": [
+        "-67.04647661625092",
+        "-67.04647661625091"
+      ],
+      "upper_margin": [
+        "-0.00000003633564",
+        "-0.00000003633563"
+      ]
+    }
+  },
+  "graph_controls": {
+    "all_labelled_simple_graphs_by_order": {
+      "1": 1,
+      "2": 2,
+      "3": 8,
+      "4": 64,
+      "5": 1024,
+      "6": 32768
+    },
+    "maximal_matching_counterexample": "P4 central edge",
+    "total": 33867
+  },
+  "invoice_controls": {
+    "actual_direct_sum_degrees": [
+      3,
+      3,
+      3,
+      3,
+      3,
+      3,
+      3,
+      3,
+      3,
+      3,
+      3,
+      3
+    ],
+    "inactive_cancellation": 4,
+    "omitted_thin_charge_rejected": true,
+    "parallel_collapse_rejected": true,
+    "relaxed_degree_censuses": {
+      "defect3": [
+        3,
+        3,
+        3,
+        3,
+        3,
+        3,
+        1,
+        1,
+        1,
+        1,
+        1,
+        1,
+        1,
+        1,
+        1,
+        1,
+        1,
+        1,
+        1,
+        1,
+        1,
+        1,
+        1,
+        1
+      ],
+      "defect4": [
+        1,
+        1,
+        1,
+        1,
+        1,
+        1,
+        1,
+        1,
+        1,
+        1,
+        1,
+        1,
+        1,
+        1,
+        1,
+        1,
+        1,
+        1,
+        1,
+        1,
+        1,
+        1,
+        1,
+        1,
+        1,
+        1,
+        1,
+        1,
+        1,
+        1,
+        1,
+        1,
+        1,
+        1,
+        1,
+        1
+      ]
+    }
+  },
+  "native_signed_profile": {
+    "1": -2220,
+    "2": -446,
+    "3": -485,
+    "4": -1,
+    "5": -135,
+    "6": -4,
+    "7": 1,
+    "8": 39,
+    "9": 359
+  },
+  "native_source": {
+    "git_blob": "7d9ff06de9dfbba31c06a141e6cacd9806852a41",
+    "head_commit": "51f54e3c31f2f3a3e056a483b3ed66ae916ad06a",
+    "pull_request": 6833,
+    "repository": "CrocSwap/integer-mult-bounds",
+    "retained_path": "retained/pricing.py",
+    "sha256": "3c23e7112b7b822c5d4ba71b412873a8572225001986cb76aa882c6f91226582",
+    "source_path": "research/p104-chain-nested-root/pricing.py",
+    "usage": "Parse literal native HELPERS and LOCAL_PAID without importing source code."
+  },
+  "negative_controls": [
+    "source-byte corruption",
+    "negative kappa",
+    "wrong root coefficient",
+    "zero query",
+    "one-coordinate nilpotent",
+    "false rank>=star-degree",
+    "maximal instead of maximum matching",
+    "omitted thin query",
+    "parallel-occurrence collapse"
+  ],
+  "no_new_kappa": true,
+  "normalized_derivative_lower_bound": "323717/1512",
+  "result": "PASS_NOIDLE_ROOT_DEFECT",
+  "root_fixtures": [
+    {
+      "F": 3,
+      "N": 3,
+      "active_coordinates": 2,
+      "defect": 1,
+      "distinct_supports": 1,
+      "n": 2
+    },
+    {
+      "F": 3,
+      "N": 5,
+      "active_coordinates": 2,
+      "defect": 3,
+      "distinct_supports": 1,
+      "n": 2
+    },
+    {
+      "F": 6,
+      "N": 6,
+      "active_coordinates": 4,
+      "defect": 2,
+      "distinct_supports": 2,
+      "n": 4
+    },
+    {
+      "F": 6,
+      "N": 8,
+      "active_coordinates": 4,
+      "defect": 4,
+      "distinct_supports": 2,
+      "n": 4
+    },
+    {
+      "F": 9,
+      "N": 9,
+      "active_coordinates": 6,
+      "defect": 3,
+      "distinct_supports": 3,
+      "n": 6
+    },
+    {
+      "F": 9,
+      "N": 11,
+      "active_coordinates": 6,
+      "defect": 5,
+      "distinct_supports": 3,
+      "n": 6
+    },
+    {
+      "F": 12,
+      "N": 12,
+      "active_coordinates": 8,
+      "defect": 4,
+      "distinct_supports": 4,
+      "n": 8
+    },
+    {
+      "F": 12,
+      "N": 14,
+      "active_coordinates": 8,
+      "defect": 6,
+      "distinct_supports": 4,
+      "n": 8
+    },
+    {
+      "F": 18,
+      "N": 18,
+      "active_coordinates": 12,
+      "defect": 6,
+      "distinct_supports": 6,
+      "n": 12
+    },
+    {
+      "F": 18,
+      "N": 20,
+      "active_coordinates": 12,
+      "defect": 8,
+      "distinct_supports": 6,
+      "n": 12
+    }
+  ],
+  "schema_version": 1,
+  "star_controls": {
+    "alphabet": [
+      [
+        0,
+        1
+      ],
+      [
+        1,
+        0
+      ],
+      [
+        1,
+        1
+      ],
+      [
+        1,
+        -1
+      ],
+      [
+        2,
+        3
+      ]
+    ],
+    "four_leaf_rank": 2,
+    "matrices_checked": 3905,
+    "matrices_with_zero_products": 3542,
+    "maximum_size": 5
+  },
+  "universal_proof": "PROOF.md; finite controls do not establish universal coverage"
+}
diff --git a/research/noidle-root-defect/REVIEW.md b/research/noidle-root-defect/REVIEW.md
new file mode 100644
index 0000000000..2ee4f79ea2
--- /dev/null
+++ b/research/noidle-root-defect/REVIEW.md
@@ -0,0 +1,68 @@
+# Independent mathematical and arithmetic review
+
+Prepared for @CubeJerry with substantial OpenAI assistance. This records a
+separate AI derivation and implementation, not human or proof-kernel acceptance.
+
+## Mathematical obligations checked
+
+The reviewer separately reconstructed the factorization
+`X A^(-1) Y=I`, the projection `A^(-1)YX`, and the rank-`delta` matrix
+`A-G`. Restricting its principal block to a matching gives an identity matrix.
+For a star, dividing by nonzero hub factors gives a diagonal matrix plus a
+skew-symmetric matrix. Symmetrization proves the half-degree lower bound.
+Zero row/column factors can be removed by unit pivots without changing the
+remaining principal matrix. This covers elementary transvections as well as
+full-support hub factors. Parallel full occurrences are handled separately by
+the rank of the unit-triangular full-position block.
+
+The maximum-matching argument was checked with its necessary distinction from
+an arbitrary maximal matching. An edge whose two endpoints have unmatched
+neighbors cannot have two distinct such neighbors, because that would create
+an augmenting path. This gives the active-vertex bound used in the theorem.
+
+The invoice was independently rebuilt from `q=n+delta-18` and the 36 full-stage
+incidences. Degree-zero coordinates cancel their corresponding part of the
+thin-query charge. For defect three, a six-vertex cover receives at least
+eighteen incidences; concavity gives the displayed six-bin envelope. For every
+larger defect, distributing all incidences singly gives the second, more
+favorable relaxation. Both bounds therefore retain every inherited native
+helper and payment and every productive field and thin query in the model.
+
+The normalization argument is limited to ordinary controls independent of the
+root and fresh stage variables and to independent whole-coordinate targets.
+It does not convert a quotient root or noncommuting output representation into
+a caller satisfying those hypotheses. In particular, this review finds no
+obstruction to the idle-bearing predecessor or to all multiplication schemes.
+
+## Separately implemented price certificate
+
+`audit_price.py` imports neither `verify.py` nor a predecessor arithmetic
+implementation. It authenticates the retained native source and compares the
+two parsed literal censuses with an independently transcribed profile.
+
+The author bounds `r^(1-C)` through an alternating expansion of `exp(-C log r)`.
+The review implementation bounds `exp((1-C) log r)` with a positive Taylor sum
+and an explicit geometric bound on its tail. Both use exact rational arithmetic;
+floating-point outputs and optimizer status determine no sign. The review
+also independently proves no re-entry using a different normalization-free
+argument: every negative nonconstant coefficient has rank at most six and
+every positive one rank at least seven. The certified derivative at `t=0` is
+positive, so scaling by `6^t` proves positivity for all `t>=0`.
+
+At the exact comparison `C=0.0033718004755`, the independent enclosures are
+
+| Envelope | Exact outward decimal enclosure |
+|---|---|
+| Defect three | `(-7.08521967330103, -7.08521967330102)` |
+| Every defect at least four | `(-67.04647661625092, -67.04647661625091)` |
+
+The derivative-at-zero lower bounds exceed 2594 and 4699 respectively.
+Corrupting the source is rejected. Omitting all eighteen native invoices changes
+the sign to positive, exposing the accounting error rather than silently
+preserving the obstruction. The registered replay includes this audit in both
+normal and optimized Python modes.
+
+This independent arithmetic check supports the two complete envelopes and the
+comparison with the pending benchmark. It does not independently execute the
+native word, admit its supplier, or remove any framework assumption. The
+retained profile is an authenticated premise of this scoped result.
diff --git a/research/noidle-root-defect/SIX-FULL-RESULT.json b/research/noidle-root-defect/SIX-FULL-RESULT.json
new file mode 100644
index 0000000000..7683012b06
--- /dev/null
+++ b/research/noidle-root-defect/SIX-FULL-RESULT.json
@@ -0,0 +1,11 @@
+{
+  "verdict": "PASS_INDEPENDENT_SIX_FULL_BOUNDARY_CONTROLS",
+  "canonical_noncommon_witnesses": 17,
+  "compatible_extensions": 671,
+  "noncommon_union": 10,
+  "common_pair_outside_matching": 2,
+  "common_pair_union": 10,
+  "unrestricted_sunflower_union": 14,
+  "characteristic_two_gram_rank": 12,
+  "scope": "Finite independent controls; universal proof in SIX-FULL-REVIEW.md."
+}
diff --git a/research/noidle-root-defect/SIX-FULL-REVIEW.md b/research/noidle-root-defect/SIX-FULL-REVIEW.md
new file mode 100644
index 0000000000..54d2ef5574
--- /dev/null
+++ b/research/noidle-root-defect/SIX-FULL-REVIEW.md
@@ -0,0 +1,116 @@
+# Independent review of the six-full-block obstruction
+
+**Verdict: PASS, with the stated characteristic, rank-defect, square-zero-query,
+and commuting-idempotent hypotheses. No new κ.**
+
+Reviewer: OpenAI GPT-6 Astra Pro research subagent A, for @CubeJerry,
+2026-11-07. The source Hall and no-idle packages remain unchanged. I read the
+following final author files and independently reconstructed their proof:
+
+- `PAIRED-DEFECT-ADDENDUM.md`, SHA256
+  `b4849cc8f7ee3803722636022077a08a29ab97ac5ecc76f3c293a59250139032`.
+- `verify_paired_defect.py`, SHA256
+  `f4952a62fa92e65b20774d8e461e0b54b827b87c482ce5add5a7f64736f55afa`.
+
+The two reviewed author files are retained unchanged at this package root. I did not import
+or execute the author's verifier. The separate exact controls below use my own
+implementation and do not establish the universal claim by finite search.
+
+## 1. The full-block gauge and rank requirement are valid
+
+The root identity gives `H=A−G` of rank two, including every other query.
+Write `H=UV`; at a selected rank-two block, `U_iV_i=I_2` implies that both
+matrices are invertible and `V_iU_i=I_2`. The query gauge
+`X_i→X_iU_i`, `Y_i→U_i^{-1}Y_i` changes neither the physical query nor its
+supporting projector. It makes every selected off-diagonal Gram block
+`sign(i−j)I_2`, regardless of intervening thin blocks.
+
+Six selected blocks therefore have Gram `S_6⊗I_2`. The displayed integral
+inverse of `S_6` multiplies to the identity, so the Gram has rank twelve over
+any field. Its twelve columns must lie in a stage union of dimension at least
+twelve. No reflection classification, two-thin census, prefix condition, or
+scalar-full-call theorem is used in this step.
+
+Commuting idempotents simultaneously diagonalize by successive image/kernel
+splittings over the original field. Their rank-four images therefore become
+four-element supports. Since the query factors have full rank, supporting
+`R_i` on both sides is equivalent to fixing `X_i` and `Y_i` on the appropriate
+side. The invertible cross-Gram factors through the intersection of two
+supports, forcing every pairwise intersection to have size at least two.
+
+## 2. The no-common-pair union argument withstands the boundary cases
+
+If all pair intersections have size at least three, every set adds at most one
+coordinate outside any fixed first set, giving union at most `m+3`.
+Otherwise normalize two supports to `A∪B` and `A∪C`, with three disjoint pairs.
+If their common pair `A` is not contained in every support, take a witness `E`
+missing an element of `A`. To meet both original supports twice, `E` must take
+at least three of their six coordinates. Their triple union `T` thus has size
+at most seven, while their triple intersection has size less than two.
+
+A further four-set adding at least two coordinates outside `T` has at most two
+coordinates inside `T`. Those coordinates must meet each of the three witness
+sets twice, hence would form a pair in their triple intersection. This is
+impossible. Each later support adds at most one coordinate, proving union at
+most `m+4`. This reasoning explicitly permits repeated supports and does not
+assume that all six supports are distinct.
+
+I checked the normalized finite boundary independently: 17 possible witness
+sets and 671 compatible extensions obey the claimed inequalities. A six-set
+family with triple-core variants reaches union ten with no common pair, so the
+combinatorial bound is not artificially strengthened.
+
+## 3. The common-pair case needs—and has—the ordered sign constraint
+
+If every support contains a pair `A`, its two remaining coordinates are an
+outside edge. Three disjoint outside edges would make the three pairwise
+stage intersections exactly `A`. The associated two-by-two column and row
+factors `α_i,β_i` are invertible because their cross-products are `±I_2`.
+For chronological `i<j<k`,
+
+\[
+\beta_i\alpha_j=\beta_i\alpha_k=-I_2,\qquad
+\beta_j\alpha_i=\beta_k\alpha_i=I_2
+\]
+
+imply `α_j=α_k` and `β_j=β_k`. Consequently `β_jα_k=β_kα_j`, contradicting the
+required values `−I_2` and `I_2` when the characteristic is not two. No scalar
+commutativity of those matrices was assumed; only invertibility was used.
+
+Thus the outside graph has matching number at most two. It has at most two
+edge-bearing components, and its incident vertex count satisfies `v≤e+c`.
+With at most `m` distinct edges, its union together with `A` has size at most
+`m+4`. Parallel edges arising from repeated supports only decrease `e`, so
+multiplicity causes no gap.
+
+Pairwise two-intersection alone would be insufficient: six disjoint outside
+pairs form a fourteen-coordinate sunflower. My controls explicitly preserve
+this counterexample to the falsely stronger bare set-family statement. The
+ordered sign equations, not an unstated set theorem, exclude that sunflower
+in characteristic other than two.
+
+## 4. Exact independent checks actually executed
+
+```sh
+python3.12 -B research/noidle-root-defect/six_full_check.py
+```
+
+Output: `PASS_INDEPENDENT_SIX_FULL_BOUNDARY_CONTROLS`.
+The standard-library script checks the integer sign-matrix inverse, the
+17 normalized witness sets and 671 compatible extensions, both ten-coordinate
+extremal union patterns, and the fourteen-coordinate sunflower that would be
+allowed without the sign obstruction. It independently constructs the
+characteristic-two sunflower Gram and verifies its rank twelve by binary
+elimination, while showing that its self-Gram equals `2I` over characteristic
+zero. This confirms the precise role of the field assumption; it is not a
+native caller in characteristic two.
+
+The packaged checker differs from the original review script only in report
+handling: it compares the retained `SIX-FULL-RESULT.json` instead of overwriting
+it. Its independent matrix and set-family algorithms are unchanged.
+
+For `m=6`, the stage union has dimension at most ten but the selected Gram
+requires twelve. The contradiction proves the at-most-five theorem. The
+claim does not establish that five is attainable, does not exclude higher
+rank defect or paid larger stages, and does not apply to noncommuting
+productive outputs or non-square-zero aggregates of shared-body calls.
diff --git a/research/noidle-root-defect/SOURCES.json b/research/noidle-root-defect/SOURCES.json
new file mode 100644
index 0000000000..b386d9fb6b
--- /dev/null
+++ b/research/noidle-root-defect/SOURCES.json
@@ -0,0 +1,19 @@
+{
+  "schema_version": 1,
+  "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a",
+      "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    }
+  ],
+  "external_sources_manifest": "retained/SOURCE-PINS.json"
+}
diff --git a/research/noidle-root-defect/TASK.json b/research/noidle-root-defect/TASK.json
new file mode 100644
index 0000000000..8065637254
--- /dev/null
+++ b/research/noidle-root-defect/TASK.json
@@ -0,0 +1,90 @@
+{
+  "schema_version": 1,
+  "task_id": "joint-query-controller",
+  "priority_revision": 8,
+  "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+  "original_card": {
+    "id": "joint-query-controller",
+    "question": "Can a changed query demand or caller remove real work while satisfying native chronology and restoration?",
+    "starting_points": [
+      "docs/research/current-priorities.md",
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md"
+    ],
+    "methods": [
+      "Construct and independently check one source-bound instance of the stated first experiment.",
+      "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change."
+    ],
+    "acceptance_gate": "A source-bound arbitrary-input identity and legal producer/consumer boundary with the complete paid and productive target invoice, including restoration, ownership, native alignment and extra charges. Price under the actual current model; historical ceiling.py assumptions must be established before use. A favorable optimistic relaxation keeps a route open but is not a completed supplier. A scoped local result remains useful; expansion requires the family-level budget gate.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_selected_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.",
+      "scope": "Source-bound orientation only, not a supplier replay or theorem proof."
+    },
+    "first_experiment": "Choose an exact caller and a new demand/interface hypothesis. Read the scoped #5617/#5631/#5649/#5747 and #5720/#5745 objections before rebuilding an excluded schedule. Compare the complete matched source/consumer protocols including all retained helper outputs. For an active-mode injection, first check #5745: its canonical delivery claim repays the eight removed centre jobs. Audit that exact claim or change its channel/feedback hypothesis; do not repeat the same free-injection search. Stop if the full favorable budget fails or the required restored output is unobservable.",
+    "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.",
+    "allowed_variations": [
+      "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes."
+    ],
+    "scope_change_triggers": [
+      "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.",
+      "Treating an archived proposal or local numerical pass as complete supplier admission."
+    ],
+    "overlap_terms": [
+      "query demand",
+      "active mode",
+      "5720",
+      "5745",
+      "5747",
+      "caller"
+    ],
+    "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": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.",
+        "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md",
+        "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.",
+        "status": "reviewed",
+        "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137",
+        "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5"
+      }
+    ]
+  },
+  "scope_status": "refined",
+  "actual_scope": "Prove a universal defect and complete-price obstruction for normalized no-idle rank-two callers with the exact eighteen-call native profile of CrocSwap/integer-mult-bounds#6833. Complementary paired-query extension: defect two permits at most five rank-two full blocks with commuting rank-four supporting projectors; arbitrary other square-zero queries are included.",
+  "scope_change_reason": "Seed 54 investigated longer exact query roots. A source-bound favorable-budget test led to a structural obstruction, rather than another finite root search. The fixed native source, whole-target contract, and every thin charge are retained.",
+  "bottleneck_link": "A longer root can change target incidence but also increases query cost. The defect bound forces F=18 to use delta>=3 and gives complete no-idle envelopes below the pending idle-bearing benchmark.",
+  "budget_minutes": 90,
+  "stop_rule": "Stop the no-idle root search once a universal algebraic bound and a certified complete-budget ceiling exclude every defect in this class. Enumerate only the stated finite matrix/graph regression domains and preserve excluded broader mechanisms as open questions.",
+  "outcome": "negative-result",
+  "evidence": "PROOF.md universal theorem; RESULT.json deterministic exact controls and certified crossings; byte-pinned retained/pricing.py; verify.py and VERIFY.json normal/optimized replay. PAIRED-DEFECT-ADDENDUM.md and SIX-FULL-REVIEW.md give separately reviewed universal proofs of the coupled-stage obstruction; two independent control implementations are registered.",
+  "author": "CubeJerry",
+  "ai_assistance": "Substantial OpenAI GPT-6 Astra Pro assistance for mathematical exploration, proof development, coding and independent lead review. Prepared and attributed to @CubeJerry.",
+  "open_questions": [
+    {
+      "question": "Can a short quotient root realize a complete restored productive interface outside the common coordinate rank-two contract?",
+      "why_it_matters": "The defect-one bound excludes eighteen full coordinate masks but does not exclude algebraic root closure or a changed representation.",
+      "first_step": "Derive exact quotient stage operators and all output/restoration targets, then identify the failed premise and price every operation.",
+      "blocked_by": "No complete compatible productive interface and invoice have been established."
+    },
+    {
+      "question": "Can a non-shortest root improve the complete native, thin-query and idle bill when idle work is allowed?",
+      "why_it_matters": "The pending stronger caller uses idle work and is outside this obstruction.",
+      "first_step": "Construct one explicit stage/idle decomposition and test its full favorable moment before searching.",
+      "blocked_by": "The present theorem deliberately imposes no idle stages and does not price a new idle-bearing construction."
+    }
+  ]
+}
diff --git a/research/noidle-root-defect/VERIFY.json b/research/noidle-root-defect/VERIFY.json
new file mode 100644
index 0000000000..05ad410317
--- /dev/null
+++ b/research/noidle-root-defect/VERIFY.json
@@ -0,0 +1,91 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "Exact source hashes, universal-proof boundary fixtures, all graphs through order six, zero-product star blocks, native moment intervals and consequential negative controls."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-O",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "Identical deterministic RESULT.json and rejection controls with Python assertions disabled."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-B",
+        "{package}/audit_price.py"
+      ],
+      "timeout_seconds": 30,
+      "checks": "Independent positive-exponential rational enclosures, direct derivative rank-separation proof, source authentication and omitted-native control."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-B",
+        "-O",
+        "{package}/audit_price.py"
+      ],
+      "timeout_seconds": 30,
+      "checks": "Independent positive-exponential rational enclosures, direct derivative rank-separation proof, source authentication and omitted-native control."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-B",
+        "{package}/verify_paired_defect.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "Paired rank-two query theorem boundary controls: exact sign inverse, set-family extension cases, valid root, omitted commutation and characteristic-two boundary."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-B",
+        "-O",
+        "{package}/verify_paired_defect.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "Paired rank-two query theorem boundary controls: exact sign inverse, set-family extension cases, valid root, omitted commutation and characteristic-two boundary."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-B",
+        "{package}/six_full_check.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "Independent integer and binary elimination plus set-family controls for the six-full obstruction; no author code imports."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-B",
+        "-O",
+        "{package}/six_full_check.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "Independent integer and binary elimination plus set-family controls for the six-full obstruction; no author code imports."
+    }
+  ]
+}
diff --git a/research/noidle-root-defect/audit_price.py b/research/noidle-root-defect/audit_price.py
new file mode 100644
index 0000000000..6317d89f76
--- /dev/null
+++ b/research/noidle-root-defect/audit_price.py
@@ -0,0 +1,120 @@
+"""Independent rational bounds for the proposed no-idle caller envelopes.
+
+This reviewer implementation uses atanh and Taylor bounds, and does not
+import the author's verifier or any predecessor arithmetic implementation.
+"""
+from collections import Counter
+from fractions import Fraction as Q
+from functools import lru_cache
+from math import factorial
+import json
+import ast
+import hashlib
+from pathlib import Path
+
+H = {1:14,2:8,3:4,4:109,5:17,6:3,7:10,8:40,9:359}
+PAID = {1:2234,2:454,3:489,4:110,5:152,6:7,7:9,8:1}
+
+def atanh_bounds(z):
+    if not 0 <= z <= Q(1,3): raise ValueError("atanh domain")
+    n = 55
+    lower = 2*sum((z**(2*j+1)/Q(2*j+1) for j in range(n)), Q(0))
+    upper = lower + 2*z**(2*n+1)/(Q(2*n+1)*(1-z*z))
+    return lower,upper
+
+@lru_cache(None)
+def log_bounds(r):
+    k = r.bit_length()-1
+    z = (Q(r,2**k)-1)/(Q(r,2**k)+1)
+    l,u = atanh_bounds(z)
+    l2,u2 = atanh_bounds(Q(1,3))
+    return l+k*l2,u+k*u2
+
+def exp_bounds(l,u):
+    if not 0 <= l <= u <= 4: raise ValueError("exp domain")
+    n=85
+    low=sum((l**j/factorial(j) for j in range(n+1)),Q(0))
+    high=sum((u**j/factorial(j) for j in range(n+1)),Q(0))
+    high += u**(n+1)/factorial(n+1)/(1-Q(4,n+2))
+    return low,high
+
+@lru_cache(None)
+def power_bounds(r,t):
+    l,u=log_bounds(r)
+    return exp_bounds(t*l,t*u)
+
+def envelope(kind):
+    c=Counter({r:18*(H.get(r,0)-PAID.get(r,0)) for r in set(H)|set(PAID)})
+    if kind==3:
+        c[25]+=104*6
+        c[9]+=104*18
+        c[1]-=104*9
+    else:
+        c[9]+=104*36
+        c[1]-=104*22
+    return c
+
+def interval(c,C):
+    lo=hi=Q(0)
+    for r,a in c.items():
+        l,u=power_bounds(r,1-C)
+        if a>=0:lo+=a*l;hi+=a*u
+        else:lo+=a*u;hi+=a*l
+    return lo,hi
+
+def decimal_enclosure(l,u,places=14):
+    scale=10**places
+    a=l.numerator*scale//l.denominator
+    b=-((-u.numerator*scale)//u.denominator)
+    return [str(Q(a,scale)),str(Q(b,scale))]
+
+def authenticate(raw):
+    if hashlib.sha256(raw).hexdigest() != "3c23e7112b7b822c5d4ba71b412873a8572225001986cb76aa882c6f91226582":
+        raise ValueError("frozen native source SHA256")
+    values = {}
+    for statement in ast.parse(raw).body:
+        if isinstance(statement, ast.Assign):
+            for target in statement.targets:
+                if isinstance(target, ast.Name) and target.id in ("HELPERS", "LOCAL_PAID"):
+                    if target.id in values: raise ValueError("repeated census")
+                    values[target.id] = ast.literal_eval(statement.value)
+    if values != {"HELPERS": H, "LOCAL_PAID": PAID}:
+        raise ValueError("independently transcribed native census differs")
+
+
+def main():
+    raw=(Path(__file__).resolve().parent/"retained"/"pricing.py").read_bytes()
+    authenticate(raw)
+    try:
+        authenticate(raw+b"\n")
+    except ValueError:
+        pass
+    else:
+        raise ValueError("source corruption accepted")
+    C=Q('0.0033718004755')
+    results={}
+    for kind in [3,4]:
+        c=envelope(kind)
+        lo,hi=interval(c,C)
+        if not hi<0:raise ValueError('envelope is not losing')
+        # A different monotonicity proof from the author's normalized quotient:
+        # all negative nonconstant ranks <=6 and positive ranks >=7.
+        deriv_lo=Q(0)
+        for r,a in c.items():
+            if r==1:continue
+            if (a<0 and r>6) or (a>0 and r<7):raise ValueError('rank separation')
+            l,u=log_bounds(r)
+            deriv_lo+=a*(l if a>=0 else u)
+        if not deriv_lo>0:raise ValueError('derivative at zero not positive')
+        results[str(kind)]={'C':str(C),'coefficients':dict(sorted(c.items())),
+                            'margin_enclosure':decimal_enclosure(lo,hi),
+                            'derivative_at_zero_certified_lower':str(deriv_lo.numerator//deriv_lo.denominator)}
+    print(json.dumps(results,indent=2))
+    # Omitting all eighteen negative native invoices must destroy the verdict.
+    wrong = {25:104*6,9:104*18,1:-104*9}
+    if interval(wrong,C)[0] <= 0:
+        raise ValueError("omitted-native control failed to reverse the verdict")
+    print("Negative controls: corrupted native source rejected; omitted-native invoice reverses verdict.")
+    print('PASS_INDEPENDENT_NOIDLE_ENVELOPE_AUDIT')
+
+if __name__=='__main__':main()
diff --git a/research/noidle-root-defect/retained/NOTICE-pr6833.txt b/research/noidle-root-defect/retained/NOTICE-pr6833.txt
new file mode 100644
index 0000000000..d03cab1fcb
--- /dev/null
+++ b/research/noidle-root-defect/retained/NOTICE-pr6833.txt
@@ -0,0 +1,5 @@
+Native main-retiming/helper retirement extension by Jerry Chen / @CubeJerry, with substantial OpenAI Codex assistance and separate source-bound review. Apache-2.0.
+
+Original retained headers, licenses and notices remain unchanged. See retained/caller/NOTICE for the full native/caller/compiler/interval lineage; Ali Romman supplies the helper-basis mechanism, DreamingOfClouds the #6702 native source, and zxv the #6726 caller.
+
+The chain-nested root caller (chain_root.py, CALLER.json) is by DreamingOfClouds with Claude Opus 5.5 (Anthropic), via Claude Code; it follows thu-nmrc's common idle fusion (#6716) and zxv's two-pair root (#6726), and uses the native word of #6824.
diff --git a/research/noidle-root-defect/retained/SOURCE-PINS.json b/research/noidle-root-defect/retained/SOURCE-PINS.json
new file mode 100644
index 0000000000..425737c1a4
--- /dev/null
+++ b/research/noidle-root-defect/retained/SOURCE-PINS.json
@@ -0,0 +1,15 @@
+{
+  "schema_version": 1,
+  "sources": [
+    {
+      "repository": "CrocSwap/integer-mult-bounds",
+      "pull_request": 6833,
+      "head_commit": "51f54e3c31f2f3a3e056a483b3ed66ae916ad06a",
+      "source_path": "research/p104-chain-nested-root/pricing.py",
+      "retained_path": "retained/pricing.py",
+      "git_blob": "7d9ff06de9dfbba31c06a141e6cacd9806852a41",
+      "sha256": "3c23e7112b7b822c5d4ba71b412873a8572225001986cb76aa882c6f91226582",
+      "usage": "Parse literal native HELPERS and LOCAL_PAID without importing source code."
+    }
+  ]
+}
diff --git a/research/noidle-root-defect/retained/pricing.py b/research/noidle-root-defect/retained/pricing.py
new file mode 100644
index 0000000000..7d9ff06de9
--- /dev/null
+++ b/research/noidle-root-defect/retained/pricing.py
@@ -0,0 +1,255 @@
+"""Complete price of the chain-nested root caller on the #6824 native word.
+
+The actual word and root are checked by chain_root.py and the verifier.
+This module independently counts every request and endpoint, then
+uses the retained zxv/Cao Yifan interval engines, Jacob Alan Sussman compiler
+and PR4359 outer ledger. Binary/caller/native authors retain their credit.
+Adapted to the recounted native helper split by @CubeJerry (#6805) with OpenAI assistance,
+to the shared-carrier input lift, and to the chain-nested root caller, by DreamingOfClouds
+with Claude Opus 5.5 (Anthropic), via Claude Code. Apache-2.0. No selected-frontier change is inferred.
+"""
+from collections import Counter
+from fractions import Fraction as Q
+
+KAPPA=Q('.00337180')
+TESTED=Q('.00337180035')
+PREVIOUS=Q('.00330823')
+RAW_LOWER,RAW_UPPER=Q('.0033718004754'),Q('.0033718004755')
+GATE_LOWER,GATE_UPPER=Q('.00330823456614'),Q('.00330823456615')
+# Literal census of the priced caller, recounted from the emitted word below.
+CENSUS={'LOCAL':18,'QUERY':3,'IDLE_ONE':16,'LAMBDA':62,'ADD':690,'SWAP':393,'SCALE':55}
+ROLES,EVENTS,PRODUCTIVE,PAID_CALLS,MAX_T,MAX_P=20,1237,12232,64184,145,64
+HELPERS={1:14,2:8,3:4,4:109,5:17,6:3,7:10,8:40,9:359}
+LOCAL_PAID={1:2234,2:454,3:489,4:110,5:152,6:7,7:9,8:1}
+
+def need(ok,message):
+    if not ok:raise ValueError(message)
+
+def encode(value):
+    if isinstance(value,Q):return str(value)
+    if isinstance(value,dict):return {str(k):encode(v)for k,v in value.items()}
+    if isinstance(value,(list,tuple)):return [encode(v)for v in value]
+    return value
+
+def formula_invoice(local,shape):
+    from chain_root import outer_formula
+    T=Counter({r:18*n for r,n in local['helpers'].items()})
+    P=Counter({r:18*n for r,n in local['paid'].items()})
+    t,p=outer_formula(*shape)
+    T.update({r:104*n for r,n in t.items()});P.update({r:104*n for r,n in p.items()})
+    return T,P
+
+def literal_invoice(local,word):
+    """Histogram of one literal caller over one native census; no census pin."""
+    T,P=Counter(),Counter();idle=Counter();main=Counter()
+    for event in word['events']:
+        op=event[0]
+        if op=='LOCAL':T.update(local['helpers']);P.update(local['paid'])
+        elif op=='QUERY':P[1]+=104
+        elif op in('IDLE','IDLE_ONE'):
+            stages=event[3]if op=='IDLE'else event[2]
+            need(stages and len(stages)==len(set(stages)),'No repeated fresh axis in a whole idle')
+            r=8*len(stages);n=208 if op=='IDLE'else 104
+            P[r]+=n;idle[r]+=n
+    for term in word['diagonal']:
+        need(not term[1],'No old nonfresh stage-zero factor is silently present')
+        main[int(term[0]%2)+8*sum(term[2:])]+=104
+    T.update(main)
+    return T,P,main,idle
+
+def assemble(local,native,word,physical):
+    need(dict(local['paid'])==LOCAL_PAID and dict(local['helpers'])==HELPERS,
+         'Exact new native paid and independent-helper boundary')
+    need(local['helpers']==native['helpers'],'Every productive helper has a checked native map')
+    need(word['roles']==ROLES and word['stages']==18,'All independent main inputs and native stages')
+    counts=Counter(e[0]for e in word['events'])
+    T,P,main,idle=literal_invoice(local,word)
+    need((T,P)==formula_invoice(local,(word['sL'],word['sR'])),'Formula and every emitted Gaussian request agree')
+    need(main==physical['main_targets'],'Every main target has its checked absolute physical phase')
+    need(idle==physical['whole_idle_jobs'],'Every fused and unfused whole idle is physically checked')
+    need(counts==Counter(CENSUS),'Complete literal paid/normalization census')
+    need(len(word['events'])==EVENTS,'Every ordinary basis and root gate is present')
+    need((sum(T.values()),sum(P.values()))==(PRODUCTIVE,PAID_CALLS),'All independent targets and paid requests')
+    need(sum(r*n for r,n in T.items())-sum(r*n for r,n in P.items())==760,'Exact unchanged rank-mass surplus')
+    need((max(T),max(P))==(MAX_T,MAX_P),'Actual maximum target and paid ranks')
+    return T,P,counts
+
+def word_queries(word):return sum(e[0]=='QUERY'for e in word['events'])
+
+def ordinary(local,native,word,adapters):
+    from scalars import verify as scalar_envelope
+    actual_scalars=scalar_envelope(word)
+    need(native['helper_normalizers']==2*sum(HELPERS.values()) and native['main_adapters']==208,
+         'Native normalization counts derive from every independent helper and main port')
+    need(local['owned_lifetimes']==47 and local['peak_owned_fields']==14,
+         'Unchanged actual native owned lifetimes and peak')
+    need(local['public_inputs']==772 and local['owned_fields']==29,
+         'Exact native public and owned label inventory')
+    # Source routes are literal whole-job / fixed17-axis route rates. The
+    # rates remain framework contracts; their counts are recomputed here.
+    routes=(sum(local['paid'].values())+native['helper_normalizers']+native['main_adapters']
+            +4*104+4*local['owned_lifetimes'])*1000
+    per_call=local['real_scalar_allowance']+routes
+    need(per_call<10**7,'All actual local scalar and route work fits the displayed per-call bound')
+    scalars=[abs(Q(e[-1]))for e in word['events']if e[0]in('ADD','SCALE')]
+    need(all(x and x.denominator&(x.denominator-1)==0 for x in scalars),'Every new basis coefficient is nonzero dyadic')
+    need(max(x.numerator.bit_length()for x in scalars)<=8 and max(x.denominator.bit_length()for x in scalars)<=7,
+         'Literal dyadic coefficient-height gate for the complete caller')
+    # The complete Horner work is checked gate by gate, including every caller coefficient.
+    # scalar_envelope checks every actual gate's complete joint Horner,
+    # halving/sign and destination-add cost and coefficient height.
+    # Scanning all fields for each gate is an explicit overcount.
+    caller=32*word['roles']*104*len(word['events'])
+    need(104*actual_scalars['real_scalar_units_per_port']<=caller and
+         104*actual_scalars['coefficient_height_units']<=caller,
+         'Actual complete scalar work and height fit the new envelope')
+    thin=word_queries(word)*16*104
+    main_maps=adapters['main_two_axis_exchanges']+adapters['main_nine_axis_basis_maps']+adapters['main_phase_translations']
+    idle_maps=adapters['idle_two_axis_exchanges']
+    query_maps=adapters['query_nine_axis_basis_maps']+adapters['query_phase_translations']
+    output=word['roles']*104*26+1000*main_maps
+    idle_adapter_work=1000*idle_maps;query_adapter_work=1000*query_maps
+    total=18*10**7+thin+caller+output+idle_adapter_work+query_adapter_work
+    need(total<10**9,'Fresh complete ordinary count, not an opaque predecessor allowance')
+    return {'local_scalar':local['real_scalar_allowance'],'local_routes':routes,'local_per_call_counted':per_call,
+            'local_per_call_upper':10**7,'native_invocations':18,'caller_gate_passes':caller,'thin_query_work':thin,
+            'all_main_input_output_adapters_and_normalizers':output,'whole_idle_adapter_work':idle_adapter_work,
+            'query_adapter_work':query_adapter_work,'elementary_canonical_maps':main_maps+idle_maps+query_maps,
+            'canonical_adapter_rate':1000,'raw_scalar_upper':total,'raw_budget':10**9,
+            'maximum_literal_scalar':max(scalars),'scalar_numerator_bits':8,'scalar_denominator_bits':7,
+            'actual_scalar_work_per_port':actual_scalars['real_scalar_units_per_port'],
+            'actual_scalar_height_per_port':actual_scalars['coefficient_height_units'],
+            'peak_owned_fields':14,'native_owned_lifetimes':47,
+            'native_public_inputs':772,'native_owned_labels':29,
+            'thin_owned_contract':'One uncredited copied-query stream reused sequentially, cleared on return; no new helper credit.',
+            'scalar_growth_bound':'At most 2^(10^9+R*f), R the recounted complete paid rank mass; inherited physical precision/tape rates remain assumptions.'}
+
+def local_lift_gain(E):
+    """Per-call sign of the input-lift saving, for every exponent t=1-k with 0<k<=.0034.
+
+    Delta(T-P)=g(t) with H_r=r^t and g(t)=H7+H3+H5-H9-H4-2*H1 (Delta T=H7-H9,
+    Delta P=2*H1+H4-H3-H5).  Rank masses agree (15=15) but the multiset is not majorized, so
+    concavity alone gives no sign.  Instead g(1)=0 and, for s in [1-.0034,1],
+    g'(s)<=g'(1)+(1-s)*M with M=sum |coeff| x ln^2 x, so g'<0 there and g(t)>=k*(-g'(1))-k^2*M/2.
+    """
+    def total(terms,s):
+        out=(Q(0),Q(0))
+        for x,c in terms:
+            out=(out[0]+c*E.power(x,s)[0],out[1]+c*E.power(x,s)[1])
+        return out
+    plus=[(7,1),(3,1),(5,1)];minus=[(9,1),(4,1),(1,2)]
+    need(sum(x*c for x,c in plus)==sum(x*c for x,c in minus),'Equal local rank mass')
+    cap=Q('.0034')
+    def dlog(terms):
+        lo=hi=Q(0)
+        for x,c in terms:
+            a=E.mul((Q(x),Q(x)),E.log_bounds(x));lo+=c*a[0];hi+=c*a[1]
+        return lo,hi
+    def d2log(terms):
+        hi=Q(0)
+        for x,c in terms:
+            a=E.mul(E.mul((Q(x),Q(x)),E.log_bounds(x)),E.log_bounds(x));hi+=c*a[1]
+        return hi
+    dp,dm=dlog(plus),dlog(minus)
+    derivative_one=(dp[0]-dm[1],dp[1]-dm[0])          # g'(1)
+    M=d2log(plus)+d2log(minus)
+    need(derivative_one[1]+cap*M<0,'g prime is negative on the whole interval 1-.0034..1')
+    out={'g_prime_at_1':E.display(derivative_one),'second_derivative_majorant':float(M)}
+    for name,k in [('claim',KAPPA),('tested',TESTED)]:
+        t=1-k;gain=(total(plus,t)[0]-total(minus,t)[1],total(plus,t)[1]-total(minus,t)[0])
+        need(gain[0]>0,'Exact interval engine: positive local saving at '+name)
+        derived=k*(-derivative_one[1])-k*k*M/2
+        need(derived>0 and derived<=gain[1],'Derivative lower bound is positive and consistent')
+        out[name]={'interval':E.display(gain),'derivative_lower_bound':float(derived)}
+    return out
+
+def run(local,native,word,physical,L,adapters,gate=None):
+    T,P,counts=assemble(local,native,word,physical)
+    work=ordinary(local,native,word,adapters)
+    E=L.load(L.ROOT/'research/higher-moment-strictification/verify.py','root8_first_intervals')
+    other=L.load(L.ROOT/'research/kappa-rebuild/architecture/mixed_target_probe.py','root8_second_intervals')
+    def margin(k):
+        t,p=E.moment(T,1-k),E.moment(P,1-k)
+        return t[0]-p[1],t[1]-p[0]
+    lower,upper=RAW_LOWER,RAW_UPPER
+    need(PREVIOUS<KAPPA<TESTED<lower,'Claim, tested price and raw crossing are strictly ordered')
+    endpoints={}
+    for name,k in [('lower',lower),('upper',upper),('tested',TESTED)]:
+        first=margin(k);tl,th=other.moment(T,k);pl,ph=other.moment(P,k);second=(tl-ph,th-pl)
+        need(max(first[0],second[0])<=min(first[1],second[1]),'Independent moment-engine agreement')
+        need(first[1]<0 and second[1]<0 if name=='upper'else first[0]>0 and second[0]>0,
+             'Both engines prove the raw endpoint/tested signs')
+        endpoints[name]={'first':E.display(first),'second':E.display(second)}
+    lift_gain=local_lift_gain(E)
+    # Gate: the same family at the shape (4,4,1|1,4,4) prices exactly at the #6824 crossing.
+    gate_margins={}
+    if gate is not None:
+        gT,gP,_,_=literal_invoice(local,gate)
+        need((gT,gP)==formula_invoice(local,(gate['sL'],gate['sR'])),'Gate shape formula and literal word agree')
+        for name,k,sign in (('lower',GATE_LOWER,1),('upper',GATE_UPPER,-1)):
+            a,b=E.moment(gT,1-k),E.moment(gP,1-k);first=(a[0]-b[1],a[1]-b[0])
+            tl,th=other.moment(gT,k);pl,ph=other.moment(gP,k);second=(tl-ph,th-pl)
+            need(first[0]>0 and second[0]>0 if sign>0 else first[1]<0 and second[1]<0,'Gate crossing equals the #6824 crossing')
+            gate_margins[name]={'first':E.display(first),'second':E.display(second)}
+    # The priced word must not reach the retained BIT cap: the outer BIT pin stays.
+    need(TESTED<Q('.0034'),'Claim stays below the retained BIT cap .0034')
+    signed=Counter(T);signed.subtract(P);derivative=Q(0)
+    for r,n in signed.items():
+        log=E.log_bounds(r)
+        derivative-=n*(E.mul(E.power(r,1-Q('.0034')),log)[0]if n>=0 else r*log[1])
+    need(derivative<0,'Unique raw crossing through the retained BIT cap')
+    t,offset,power,cutoff,floor=1-TESTED,Q(1,7),1920,11,12
+    target,paid=E.moment(T,t),E.moment(P,t)
+    alpha=E.divide(paid,target)
+    gamma=E.divide(E.moment(P,t+offset),E.mul(E.power(cutoff,offset),target))
+    delta=E.divide((Q(sum(T.values())*floor),)*2,E.mul(E.power(cutoff,TESTED),target))
+    reserve,decay=Q(1,10**27),Q(31,32)
+    need(alpha[1]<1-reserve and gamma[1]<decay and delta[1]<decay,'All completion and splitting tail ratios')
+    alternative_delta=E.divide((Q(sum(T.values())*13),)*2,E.mul(E.power(12,TESTED),target))
+    # This smaller productive census also makes the alternate12/13 cutoff viable;
+    # admission below still uses the independently checked11/12 choice.
+    normalized=1/(1+power*reserve)+4*decay**power
+    need(normalized<1 and cutoff**64<floor**63,'Exact finite strictification and rank-rounding inequalities')
+    theta,logarithm_power=Q(63,64),2100
+    # 145^(power*TESTED) by two exact squarings: the retained exponential enclosure takes
+    # arguments below 16 in absolute value, and 960*TESTED*ln(145) now exceeds 16.
+    quarter=E.power(145,Q(power,4)*TESTED);half=E.mul(quarter,quarter);factor=E.mul(half,half)
+    eta=E.scale(E.divide((Q(1),Q(1)),factor),t)
+    need(2*(cutoff**power)**64<=(145**power)**63 and eta[0]>theta**logarithm_power,'Compiler shifted exits and complement capacity')
+    need(factor[1]<2**logarithm_power,'Compiler initial range')
+    gap=(TESTED-KAPPA)/7;need(gap.numerator==1,'Exact positive compiler grid')
+    step=gap.denominator
+    def wins(j):return(step*j+1)**logarithm_power<2**j
+    left,right=1,2
+    while not wins(right):left,right=right,2*right
+    while right-left>1:
+        middle=(left+right)//2
+        if wins(middle):right=middle
+        else:left=middle
+    H=step*right
+    need(H>8*power and wins(right)and not wins(right-1),'Explicit uniform threshold and adjacent-grid control')
+    bit=L.read(L.ROOT/'research/query-thinned-controllers/RESULT.json')['ordinary_BIT']
+    atom=Q(bit['atom']);ordinary_bit=(1-atom)*Q(bit['after_cover'])+atom*Q('.0000384599');admitted=Q(bit['admitted'])
+    need(atom>ordinary_bit>admitted>TESTED and atom<1-ordinary_bit,'Retained ordinary/admitted BIT stock and savings')
+    outer_module=L.load(L.ROOT/'research/pr4359-p7-padding/dependencies/compiler-refill/endpoint.py','root8_outer')
+    params={'kappa':KAPPA,'tested_saving':TESTED,'complex_uniform_saving':KAPPA+6*gap,
+            'b':KAPPA+5*gap,'a':KAPPA+4*gap,'q':KAPPA+3*gap,'bit_saving':admitted,
+            'epsilon':1-gap,'beta':1-3*gap,'r0':gap/10,'stop':gap,'layout':gap,'d':gap}
+    outer=outer_module.ledger(params)
+    outer['functional_checks']['actual_new_BIT_stock_sublinear']=params['beta']*(1-atom)
+    need(len(outer['strict_checks'])==54 and len(outer['functional_checks'])==4,'Complete54+4 outer inventory')
+    need(all(v>0 for k in('strict_checks','functional_checks')for v in outer[k].values()),'Every outer inequality is strict')
+    bad=outer_module.ledger(dict(params,bit_saving=Q('.0027')))
+    need(any(v<=0 for v in bad['strict_checks'].values()),'Insufficient BIT budget rejected')
+    work['paid_rank_mass']=sum(r*n for r,n in P.items())
+    return encode({'status':'PASS_CHAIN_ROOT_COMPLETE_PRICE','kappa':KAPPA,'tested':TESTED,
+       'targets':T,'paid':P,'productive_fields':sum(T.values()),'paid_calls':sum(P.values()),'rank_mass_surplus':760,
+       'full_calls':18,'thin_queries':word_queries(word),'whole_idle_jobs':sum(n for r,n in literal_invoice(local,word)[3].items()),'counts':counts,'raw_root_interval':[lower,upper],
+       'raw_endpoint_margins':endpoints,'local_lift_gain':lift_gain,'gate_margins':gate_margins,'derivative_upper':derivative,'nonrecursive':work,
+       'strictification':{'power':power,'cutoff':cutoff,'floor':floor,'offset':offset,'reserve':reserve,'decay':decay,
+                         'alpha':E.display(alpha),'gamma':E.display(gamma),'delta':E.display(delta),
+                         'alternative_12_13_delta':E.display(alternative_delta),'normalized_upper':normalized},
+       'compiler':{'H':H,'N':'2^'+str(H),'integer_test_exponent':right,'theta':theta,'logarithm_power':logarithm_power,
+                   'eta':E.display(eta),'gap':gap,'uniform_saving':params['complex_uniform_saving'],'word_materialized':False},
+       'ordinary_BIT':bit,'outer':outer,'source_assumptions':['native_all_columns','owned_erasure','compiler','precision_tape','analytic_recovery'],
+       'scope':'Complete conditional price, requiring the supplied caller/native/physical inputs to be independently verified by the package. Does not itself verify those scientific inputs, discharge inherited assumptions, establish scientific admission, or change selected kappa.'})
diff --git a/research/noidle-root-defect/six_full_check.py b/research/noidle-root-defect/six_full_check.py
new file mode 100644
index 0000000000..c20b599dcc
--- /dev/null
+++ b/research/noidle-root-defect/six_full_check.py
@@ -0,0 +1,68 @@
+"""Independent boundary controls for the six-full-block obstruction.
+No author code is imported. Universal argument: SIX-FULL-REVIEW.md.
+"""
+from itertools import combinations
+from pathlib import Path
+import json
+
+def need(ok,msg):
+    if not ok:raise ValueError(msg)
+def mm(a,b):return [[sum(x*y for x,y in zip(r,c)) for c in zip(*b)] for r in a]
+def gf2_rank(a):
+    rows=[sum((x&1)<<i for i,x in enumerate(r)) for r in a];basis={}
+    for x in rows:
+        while x:
+            p=x.bit_length()-1
+            if p in basis:x^=basis[p]
+            else:basis[p]=x;break
+    return len(basis)
+def matching(edges):
+    if not edges:return 0
+    a,b=next(iter(edges));rest=edges-{(a,b)}
+    return max(matching(rest),1+matching({e for e in rest if a not in e and b not in e}))
+
+def main():
+    S=[[(i>j)-(i<j) for j in range(6)] for i in range(6)]
+    inv=[[(-1)**(i+j)*((i>j)-(i<j)) for j in range(6)] for i in range(6)]
+    need(mm(S,inv)==[[int(i==j) for j in range(6)] for i in range(6)],'integer inverse S6')
+    A={0,1,2,3};B={0,1,4,5};common=A&B
+    witnesses=extensions=0
+    for raw in combinations(range(7),4):
+        C=set(raw)
+        if len(A&C)<2 or len(B&C)<2 or common<=C:continue
+        witnesses+=1;T=A|B|C
+        need(len(T)<=7 and len(A&B&C)<2,'non-common-pair witness')
+        for rawD in combinations(range(9),4):
+            D=set(rawD)
+            if min(len(A&D),len(B&D),len(C&D))<2:continue
+            extensions+=1;need(len(D-T)<=1,'extension adds at most one vertex')
+    family=[A,B,{0,2,4,6},{0,2,4,7},{0,2,4,8},{0,2,4,9}]
+    need(all(len(x&y)>=2 for x,y in combinations(family,2)) and
+         len(set.intersection(*family))==1 and len(set.union(*family))==10,
+         'sharp non-common-pair fixture')
+    edges={(2,3),(2,4),(2,5),(6,7),(6,8),(6,9)}
+    need(matching(edges)==2 and len(set.union(*(set(e) for e in edges)))==8,'two outside stars')
+    sunflower=[{0,1,2+2*i,3+2*i} for i in range(6)]
+    need(len(set.union(*sunflower))==14 and all(len(x&y)==2 for x,y in combinations(sunflower,2)),
+         'intersection condition alone does not bound union by ten')
+    X=[[0]*12 for _ in range(14)];Y=[[0]*14 for _ in range(12)]
+    for i in range(6):
+        for c in range(2):
+            X[c][2*i+c]=1;X[2+2*i+c][2*i+c]=1
+            Y[2*i+c][c]=1;Y[2*i+c][2+2*i+c]=1
+    G=mm(Y,X)
+    need(all(G[2*i+a][2*j+b]%2==int(i!=j and a==b)
+             for i in range(6) for j in range(6) for a in range(2) for b in range(2)),
+         'characteristic-two sunflower Gram')
+    need(gf2_rank(G)==12 and all(G[i][i]==2 for i in range(12)),
+         'char2 rank12 control fails square-zero in characteristic zero')
+    result={'verdict':'PASS_INDEPENDENT_SIX_FULL_BOUNDARY_CONTROLS',
+            'canonical_noncommon_witnesses':witnesses,'compatible_extensions':extensions,
+            'noncommon_union':10,'common_pair_outside_matching':2,'common_pair_union':10,
+            'unrestricted_sunflower_union':14,'characteristic_two_gram_rank':12,
+            'scope':'Finite independent controls; universal proof in SIX-FULL-REVIEW.md.'}
+    expected=json.loads(Path(__file__).with_name('SIX-FULL-RESULT.json').read_text())
+    need(result==expected,'independent report matches retained result')
+    print(json.dumps(result,indent=2))
+
+if __name__=='__main__':main()
diff --git a/research/noidle-root-defect/verify.py b/research/noidle-root-defect/verify.py
new file mode 100644
index 0000000000..b632ecbf16
--- /dev/null
+++ b/research/noidle-root-defect/verify.py
@@ -0,0 +1,426 @@
+#!/usr/bin/env python3
+"""Exact finite controls for the no-idle defect theorem; see PROOF.md.
+Jerry Chen / @CubeJerry, substantial OpenAI GPT-6 Astra Pro assistance. Apache-2.0.
+"""
+import argparse
+import ast
+from fractions import Fraction as Q
+from functools import lru_cache
+import hashlib
+from itertools import product
+import json
+from pathlib import Path
+
+ROOT = Path(__file__).resolve().parent
+F, PORTS = 18, 104
+EXPECTED = {1:-2220,2:-446,3:-485,4:-1,5:-135,6:-4,7:1,8:39,9:359}
+
+
+def need(ok, message):
+    if not ok:
+        raise ValueError(message)
+
+
+def rejected(operation, message):
+    try:
+        operation()
+    except ValueError:
+        return
+    raise ValueError('Negative control accepted: ' + message)
+
+
+def authenticate(raw, pin):
+    need(hashlib.sha256(raw).hexdigest() == pin['sha256'], 'Retained SHA256')
+    framed = b'blob ' + str(len(raw)).encode() + b'\0' + raw
+    need(hashlib.sha1(framed).hexdigest() == pin['git_blob'], 'Retained Git blob')
+
+
+def source_profile():
+    pins = json.loads((ROOT/'retained/SOURCE-PINS.json').read_text())['sources']
+    need(len(pins) == 1, 'One exact external source')
+    pin = pins[0]
+    need(pin['head_commit'] == '51f54e3c31f2f3a3e056a483b3ed66ae916ad06a', 'Frozen #6833 head')
+    raw = (ROOT/pin['retained_path']).read_bytes()
+    authenticate(raw, pin)
+    rejected(lambda: authenticate(raw+b'\n', pin), 'source-byte mutation')
+    values = {}
+    for node in ast.parse(raw).body:
+        if isinstance(node, ast.Assign):
+            for target in node.targets:
+                if isinstance(target, ast.Name) and target.id in ('HELPERS','LOCAL_PAID'):
+                    need(target.id not in values, 'No repeated census assignment')
+                    values[target.id] = ast.literal_eval(node.value)
+    need(set(values) == {'HELPERS','LOCAL_PAID'}, 'Both native censuses')
+    need(all(type(k) is int and type(v) is int and k>0 and v>0
+             for row in values.values() for k,v in row.items()), 'Positive integral census')
+    helper, paid = values['HELPERS'], values['LOCAL_PAID']
+    d = {r:helper.get(r,0)-paid.get(r,0) for r in sorted(set(helper)|set(paid))}
+    need(d == EXPECTED, 'Recounted signed native profile')
+    need(sum(r*c for r,c in d.items()) == -1720, 'Native rank mass')
+    return d, pin
+
+
+# log(u)=2*atanh((u-1)/(u+1)); range reduction keeps 0<=z<=1/3.
+# The omitted positive tail after m terms is bounded by replacing every
+# denominator by 2*m+1 and summing the resulting geometric series.
+def log_unit(u):
+    need(Q(1)<=u<=Q(2), 'Logarithm range reduction')
+    z = (u-1)/(u+1)
+    total, power, m = Q(0), z, 48
+    for j in range(m):
+        total += power/(2*j+1)
+        power *= z*z
+    lo = 2*total
+    return lo, lo+2*power/((2*m+1)*(1-z*z))
+
+
+@lru_cache(maxsize=None)
+def log_bounds(r):
+    need(type(r) is int and r>=1, 'Positive integer logarithm')
+    k = r.bit_length()-1
+    a,b = log_unit(Q(2))
+    c,d = log_unit(Q(r,2**k))
+    return k*a+c,k*b+d
+
+
+def exp_polynomial(a, degree):
+    need(Q(0)<=a<=Q(1), 'Alternating exponential range')
+    total = term = Q(1)
+    for j in range(1,degree+1):
+        term *= -a/j
+        total += term
+    return total
+
+
+@lru_cache(maxsize=None)
+def power_bounds(r,kappa):
+    need(Q(0)<=kappa<=Q(1), 'Exponent domain')
+    if r==1 or kappa==0:
+        return Q(r),Q(r)
+    lo,hi = log_bounds(r)
+    # exp(-a) decreases: odd-degree Taylor at the upper a is a lower bound;
+    # even-degree Taylor at the lower a is an upper bound, by alternating terms.
+    lower = r*exp_polynomial(kappa*hi,11)
+    upper = r*exp_polynomial(kappa*lo,12)
+    need(0<lower<=upper<=r, 'Positive ordered power enclosure')
+    return lower,upper
+
+
+def interval_sum(coefficients,kappa):
+    lo=hi=Q(0)
+    for r,c in sorted(coefficients.items()):
+        a,b = power_bounds(r,kappa)
+        lo += c*(a if c>=0 else b)
+        hi += c*(b if c>=0 else a)
+    return lo,hi
+
+
+def enclosure(bounds, places=14):
+    scale = 10**places
+    low = bounds[0].numerator*scale//bounds[0].denominator
+    high = -((-bounds[1].numerator*scale)//bounds[1].denominator)
+    def text(value):
+        sign = '-' if value<0 else ''
+        value=abs(value)
+        return sign+str(value//scale)+'.'+str(value%scale).zfill(places)
+    return [text(low),text(high)]
+
+
+def envelope(native,defect):
+    c = {r:F*v for r,v in native.items()}
+    extra = {25:6,9:18,1:-9} if defect==3 else {9:36,1:-22}
+    for r,v in extra.items():
+        c[r]=c.get(r,0)+PORTS*v
+    return c
+
+
+def prices(native):
+    brackets = {3:('0.0033288660495','0.0033288660497'),
+                4:('0.0029312090589','0.0029312090593')}
+    out={}
+    for defect in (3,4):
+        c=envelope(native,defect)
+        lower,upper=brackets[defect]
+        left,right=interval_sum(c,Q(lower)),interval_sum(c,Q(upper))
+        need(left[0]>0 and right[1]<0, 'Strict crossing bracket')
+        headline=interval_sum(c,Q('.00337180'))
+        test=interval_sum(c,Q('.0033718004755'))
+        need(headline[1]<0 and test[1]<0, 'Cannot reach pending benchmark')
+        fence=(Q('-7.086'),Q('-7.085')) if defect==3 else (Q('-67.047'),Q('-67.046'))
+        need(fence[0]<test[0]<=test[1]<fence[1], 'Displayed negative interval')
+        need(sum(r*v for r,v in c.items())==(552 if defect==3 else 448), 'Exact t=1 endpoint')
+        need(sum(c.values())<0, 'Exact t=0 endpoint')
+        out[str(defect)]={'crossing_bracket':[lower,upper],
+                         'lower_margin':enclosure(left),'upper_margin':enclosure(right),
+                         'pending_headline_margin':enclosure(headline),
+                         'pending_raw_upper_margin':enclosure(test)}
+    bound=Q(2220*8,81)-Q(2,7)-Q(39,8)
+    need(bound==Q(323717,1512) and bound>0, 'Normalized derivative bound')
+    need(F>2*2*(2+1), 'Defects one and two exclude eighteen full calls')
+    rejected(lambda:power_bounds(9,Q(-1,100)), 'negative kappa')
+    need(power_bounds(25,Q(0))==(Q(25),Q(25)), 'Integer-power endpoint')
+    p9=power_bounds(9,Q('.00337180'))
+    for d in range(2,37):
+        pd=power_bounds(1+8*d,Q('.00337180'))
+        need(pd[1]-1<d*(p9[0]-1), 'Finite integer-degree concavity control')
+    return out,str(bound)
+
+
+def eye(n):
+    return [[Q(i==j) for j in range(n)] for i in range(n)]
+
+
+def multiply(a,b):
+    return [[sum((a[i][k]*b[k][j] for k in range(len(b))),Q(0))
+             for j in range(len(b[0]))] for i in range(len(a))]
+
+
+def rank(matrix):
+    if not matrix:
+        return 0
+    a=[[Q(x) for x in row] for row in matrix]
+    rows,cols,pivot=len(a),len(a[0]),0
+    for col in range(cols):
+        row=next((r for r in range(pivot,rows) if a[r][col]),None)
+        if row is None:
+            continue
+        a[pivot],a[row]=a[row],a[pivot]
+        divisor=a[pivot][col]
+        a[pivot]=[x/divisor for x in a[pivot]]
+        for r in range(pivot+1,rows):
+            if a[r][col]:
+                factor=a[r][col]
+                a[r]=[x-factor*y for x,y in zip(a[r],a[pivot])]
+        pivot+=1
+        if pivot==rows:
+            break
+    return pivot
+
+
+def inverse(a):
+    n=len(a)
+    work=[[Q(x) for x in row]+identity for row,identity in zip(a,eye(n))]
+    for col in range(n):
+        row=next((r for r in range(col,n) if work[r][col]),None)
+        need(row is not None,'Invertible matrix')
+        work[col],work[row]=work[row],work[col]
+        divisor=work[col][col]
+        work[col]=[x/divisor for x in work[col]]
+        for r in range(n):
+            if r!=col and work[r][col]:
+                factor=work[r][col]
+                work[r]=[x-factor*y for x,y in zip(work[r],work[col])]
+    return [row[n:] for row in work]
+
+
+def query_matrix(x,y):
+    n=len(x)
+    need(len(y)==n and any(x) and any(y),'Nonzero rank-one query')
+    need(sum((a*b for a,b in zip(x,y)),Q(0))==0,'Square-zero query')
+    return [[Q(i==j)-2*x[i]*y[j] for j in range(n)] for i in range(n)]
+
+
+def check_root(queries,full):
+    n,total=len(queries[0][0]),len(queries)
+    endpoint=eye(n)
+    for x,y in queries:
+        endpoint=multiply(query_matrix(x,y),endpoint)
+    need(endpoint==[[-x for x in row] for row in eye(n)],'Complete root endpoint')
+    xmat=[[queries[j][0][i] for j in range(total)] for i in range(n)]
+    ymat=[list(y) for _,y in queries]
+    gram=multiply(ymat,xmat)
+    a=[[Q(i==j)+(2*gram[i][j] if i>j else 0) for j in range(total)] for i in range(total)]
+    b=[[a[i][j]-gram[i][j] for j in range(total)] for i in range(total)]
+    need(multiply(multiply(xmat,inverse(a)),ymat)==eye(n),'Independent displacement identity')
+    defect=total-n
+    need(rank(b)==defect,'Complete A-G rank defect')
+    supports=[]
+    for index in full:
+        x,y=queries[index]
+        support={i for i in range(n) if x[i] or y[i]}
+        need(len(support)==2,'Full support is a coordinate pair')
+        supports.append(tuple(sorted(support)))
+    active=set(v for edge in supports for v in edge)
+    bfull=[[b[i][j] for j in full] for i in full]
+    need(len(full)<=len(active)+rank(bfull)<=len(active)+defect,
+         'Full occurrences versus active coordinates and defect')
+    need(len(full)<=2*defect*(defect+1),'Universal full-call bound on root fixture')
+    return {'n':n,'N':total,'F':len(full),'defect':defect,
+            'distinct_supports':len(set(supports)),'active_coordinates':len(active)}
+
+
+def direct_sum_root(blocks):
+    # In two dimensions these three I-2xy factors multiply to -I.
+    template=[((1,0),(0,-1)),((0,1),(1,0)),((-1,1),(1,1))]
+    out=[]
+    for block in range(blocks):
+        for x,y in template:
+            xx=[Q(0)]*(2*blocks);yy=xx[:]
+            xx[2*block:2*block+2]=map(Q,x)
+            yy[2*block:2*block+2]=map(Q,y)
+            out.append((xx,yy))
+    return out
+
+
+def roots():
+    fixtures=[]
+    for blocks in (1,2,3,4,6):
+        word=direct_sum_root(blocks)
+        fixtures.append(check_root(word,list(range(len(word)))))
+        # Insert arbitrary dense thin queries R,-R: their product is identity
+        # because R^2=0. Neither is constrained to a full coordinate pair.
+        x=[Q(1)]*(2*blocks)
+        y=[Q((-1)**i) for i in range(2*blocks)]
+        word[1:1]=[(x,y),([-a for a in x],y)]
+        full=[0]+list(range(3,len(word)))
+        fixtures.append(check_root(word,full))
+    word=direct_sum_root(2)
+    x,y=word[0]
+    damaged=[([-a for a in x],y)]+word[1:]
+    rejected(lambda:check_root(damaged,list(range(6))),'wrong root coefficient')
+    rejected(lambda:query_matrix([Q(0),Q(0)],[Q(1),Q(0)]),'zero query')
+    rejected(lambda:query_matrix([Q(1)],[Q(1)]),'one-coordinate nonzero nilpotent')
+    need(fixtures[2]['F']==6 and fixtures[2]['distinct_supports']==2,
+         'Parallel occurrences retain native-call multiplicity')
+    return fixtures
+
+
+def star_controls():
+    alphabet=((0,1),(1,0),(1,1),(1,-1),(2,3))
+    checked=zero_cases=0
+    for size in range(1,6):
+        for pairs in product(alphabet,repeat=size):
+            b=[[Q(i==j)+((i>j)-(i<j))*pairs[i][1]*pairs[j][0]
+                for j in range(size)] for i in range(size)]
+            zeros=sum(a*c==0 for a,c in pairs)
+            need(rank(b)>=zeros+(size-zeros+1)//2,'Star rank with zero-product pivots')
+            checked+=1
+            zero_cases+=bool(zeros)
+    # The factor two in the isolated star rank estimate cannot be replaced by
+    # one without another premise. This does not assert a complete root exists.
+    signs=(-1,1,-1,1)
+    b=[[Q(i==j)+((i>j)-(i<j))*signs[i] for j in range(4)] for i in range(4)]
+    need(rank(b)==2,'Rank-two four-leaf principal-star fixture')
+    rejected(lambda:need(rank(b)>=4,'False star rank >= degree'),'false degree strengthening')
+    return {'alphabet':[list(pair) for pair in alphabet], 'maximum_size':5,
+            'matrices_checked':checked,'matrices_with_zero_products':zero_cases,
+            'four_leaf_rank':rank(b)}
+
+
+def graph_parameters(adjacency):
+    @lru_cache(maxsize=None)
+    def matching(mask):
+        if not mask:
+            return 0
+        bit=mask&-mask
+        vertex=bit.bit_length()-1
+        rest=mask^bit
+        best=matching(rest)
+        partners=adjacency[vertex]&rest
+        while partners:
+            partner=partners&-partners
+            partners^=partner
+            best=max(best,1+matching(rest^partner))
+        return best
+    v=sum(bool(row) for row in adjacency)
+    delta=max((row.bit_count() for row in adjacency),default=0)
+    nu=matching((1<<len(adjacency))-1)
+    return v,nu,delta
+
+
+def graph_controls():
+    counts={}
+    for n in range(1,7):
+        edges=[(i,j) for i in range(n) for j in range(i+1,n)]
+        for mask in range(1<<len(edges)):
+            adjacency=[0]*n
+            for k,(i,j) in enumerate(edges):
+                if mask>>k&1:
+                    adjacency[i]|=1<<j
+                    adjacency[j]|=1<<i
+            v,nu,delta=graph_parameters(tuple(adjacency))
+            need(v<=nu*(delta+1),'Maximum-matching graph inequality')
+        counts[str(n)]=1<<len(edges)
+    # The central edge is a maximal matching of P4, but not a maximum one.
+    # With that size-one matching, the claimed inequality would incorrectly say 4<=3.
+    path=(2,5,10,4)
+    v,nu,delta=graph_parameters(path)
+    need((v,nu,delta)==(4,2,2),'P4 independent matching control')
+    rejected(lambda:need(v<=1*(delta+1),'Wrong maximal matching'),'maximal versus maximum')
+    return {'all_labelled_simple_graphs_by_order':counts,'total':sum(counts.values()),
+            'maximal_matching_counterexample':'P4 central edge'}
+
+
+def invoice(native,degrees,defect,thin=None):
+    need(sum(degrees)==36 and all(type(d) is int and d>=0 for d in degrees),
+         'All thirty-six full-call incidences, with multiplicity')
+    q=len(degrees)+defect-F
+    need(q>=0,'Nonnegative thin-query count')
+    if thin is not None:
+        need(thin==q,'Thin count equals N-F=n+defect-F')
+    coefficients={r:F*c for r,c in native.items()}
+    for d in degrees:
+        r=1+8*d
+        coefficients[r]=coefficients.get(r,0)+PORTS
+    coefficients[1]-=PORTS*q
+    return {r:c for r,c in coefficients.items() if c}
+
+
+def invoice_controls(native):
+    d3=[3]*6+[1]*18
+    d4=[1]*36
+    need(invoice(native,d3,3)==envelope(native,3),'E3 relaxed degree census')
+    need(invoice(native,d4,4)==envelope(native,4),'E4 relaxed degree census')
+    # Actual direct sum: six independent two-dimensional roots, three full
+    # calls on each pair. Added degree-zero fields cancel with paid thin terms.
+    actual=[3]*12
+    need(invoice(native,actual,6)==invoice(native,actual+[0]*4,6),
+         'Inactive productive fields retain their cancelling query charge')
+    rejected(lambda:invoice(native,d3,3,thin=8),'omitted thin query')
+    rejected(lambda:invoice(native,[1]*12,6),'parallel calls collapsed to distinct supports')
+    paid=invoice(native,d3,3)
+    unpaid=dict(paid);unpaid[1]+=104
+    need(interval_sum(paid,Q('.00337180'))[1]<0<interval_sum(unpaid,Q('.00337180'))[0],
+         'Omitting one thin charge creates a false favorable envelope')
+    return {'relaxed_degree_censuses':{'defect3':d3,'defect4':d4},
+            'actual_direct_sum_degrees':actual,'inactive_cancellation':4,
+            'omitted_thin_charge_rejected':True,'parallel_collapse_rejected':True}
+
+
+def run():
+    native,pin=source_profile()
+    price,bound=prices(native)
+    return {'schema_version':1,'result':'PASS_NOIDLE_ROOT_DEFECT',
+            'claim':'F <= 2*delta*(delta+1), coordinate rank-two no-idle class only',
+            'no_new_kappa':True,'native_source':pin,
+            'native_signed_profile':{str(r):c for r,c in native.items()},
+            'envelopes':price,'normalized_derivative_lower_bound':bound,
+            'root_fixtures':roots(),'star_controls':star_controls(),
+            'graph_controls':graph_controls(),'invoice_controls':invoice_controls(native),
+            'negative_controls':['source-byte corruption','negative kappa',
+                'wrong root coefficient','zero query','one-coordinate nilpotent',
+                'false rank>=star-degree','maximal instead of maximum matching',
+                'omitted thin query','parallel-occurrence collapse'],
+            'universal_proof':'PROOF.md; finite controls do not establish universal coverage'}
+
+
+def main():
+    parser=argparse.ArgumentParser(description=__doc__)
+    parser.add_argument('--write',action='store_true',help='Regenerate deterministic RESULT.json')
+    args=parser.parse_args()
+    result=run()
+    path=ROOT/'RESULT.json'
+    if args.write:
+        path.write_text(json.dumps(result,indent=2,sort_keys=True)+'\n')
+    else:
+        need(path.is_file(),'RESULT.json exists; use --write only for author regeneration')
+        need(result==json.loads(path.read_text()),'Exact deterministic result replay')
+    print(result['result'])
+    print('No new kappa; F=18 requires defect>=3; both complete envelopes lose to 0.00337180.')
+    print('Exact controls: '+str(result['graph_controls']['total'])+' graphs, '+
+          str(result['star_controls']['matrices_checked'])+' star blocks, '+
+          str(len(result['root_fixtures']))+' roots, 9 rejection controls.')
+
+
+if __name__=='__main__':
+    main()
diff --git a/research/noidle-root-defect/verify_paired_defect.py b/research/noidle-root-defect/verify_paired_defect.py
new file mode 100644
index 0000000000..49fd5fc84e
--- /dev/null
+++ b/research/noidle-root-defect/verify_paired_defect.py
@@ -0,0 +1,220 @@
+#!/usr/bin/env python3
+"""Exact controls for PAIRED-DEFECT-ADDENDUM.md; no external dependencies.
+
+The universal result is the written proof, not a finite search conclusion.
+By @CubeJerry with substantial OpenAI GPT-6 Astra Pro assistance.
+"""
+from fractions import Fraction as Q
+from itertools import combinations
+import json
+
+
+def need(condition, message):
+    if not condition:
+        raise ValueError(message)
+
+
+def eye(n):
+    return [[Q(i == j) for j in range(n)] for i in range(n)]
+
+
+def mm(a, b):
+    return [[sum(x * y for x, y in zip(row, col)) for col in zip(*b)] for row in a]
+
+
+def add(a, b, scale=1):
+    return [[x + scale * y for x, y in zip(ar, br)] for ar, br in zip(a, b)]
+
+
+def tensor2(a):
+    return [[x * Q(i == j) for x in row for j in range(2)] for row in a for i in range(2)]
+
+
+def rank(a, modulus=None):
+    a = [[int(x) % modulus if modulus else Q(x) for x in row] for row in a]
+    r = 0
+    for c in range(len(a[0]) if a else 0):
+        p = next((i for i in range(r, len(a)) if a[i][c]), None)
+        if p is None:
+            continue
+        a[r], a[p] = a[p], a[r]
+        inv = pow(a[r][c], -1, modulus) if modulus else 1 / a[r][c]
+        a[r] = [(x * inv) % modulus if modulus else x * inv for x in a[r]]
+        for i in range(r + 1, len(a)):
+            factor = a[i][c]
+            if factor:
+                a[i] = [((x - factor * y) % modulus if modulus else x - factor * y)
+                        for x, y in zip(a[i], a[r])]
+        r += 1
+        if r == len(a):
+            break
+    return r
+
+
+def same(a, b, modulus=None):
+    return all((x - y) % modulus == 0 if modulus else x == y
+               for ar, br in zip(a, b) for x, y in zip(ar, br))
+
+
+def canonical(n):
+    need(n > 0 and n % 2 == 0, "even canonical dimension")
+    result = []
+    for i in range(n + 1):
+        x = [Q(i == j) for j in range(n)] if i < n else [Q((-1) ** (j + 1)) for j in range(n)]
+        y = [Q((i > j) - (i < j)) for j in range(n)]
+        result.append((tensor2([[v] for v in x]), tensor2([y])))
+    return result
+
+
+def check_root(queries):
+    n = len(queries[0][0])
+    prefix = eye(n)
+    for x, y in queries:
+        need(rank(x) == rank(y) == 2, "rank-two query factors")
+        need(mm(y, x) == [[0, 0], [0, 0]], "square-zero query")
+        prefix = add(prefix, mm(x, mm(y, prefix)), -2)
+    need(prefix == [[-v for v in row] for row in eye(n)], "literal root endpoint")
+
+
+def support(x, y, p, modulus=None):
+    need(rank(p, modulus) == 4, "rank-four stage")
+    need(same(mm(p, p), p, modulus), "idempotent stage")
+    need(same(mm(p, x), x, modulus), "left query support")
+    need(same(mm(y, p), y, modulus), "right query support")
+
+
+def rejected(fn, message):
+    try:
+        fn()
+    except ValueError:
+        return
+    raise ValueError("Negative control was accepted: " + message)
+
+
+def sign_gram():
+    s = [[Q((i > j) - (i < j)) for j in range(6)] for i in range(6)]
+    inv = [[((-1) ** (i + j)) * s[i][j] for j in range(6)] for i in range(6)]
+    need(mm(s, inv) == eye(6) and mm(inv, s) == eye(6), "integer sign-matrix inverse")
+    need(rank(tensor2(s)) == 12, "six-query block Gram rank")
+    bad = [row[:] for row in inv]
+    bad[0][1] *= -1
+    rejected(lambda: need(mm(s, bad) == eye(6), "corrupt inverse"), "inverse sign")
+    return {"scalar_order": 6, "block_width": 2, "block_gram_rank": 12}
+
+
+def matching(edges):
+    vertices = set().union(*edges) if edges else set()
+    if not vertices:
+        return 0
+    v = min(vertices)
+    best = matching([e for e in edges if v not in e])
+    for edge in edges:
+        if v in edge:
+            best = max(best, 1 + matching([e for e in edges if not e & edge]))
+    return best
+
+
+def set_controls():
+    c0, c1, a = {0, 1, 2, 3}, {0, 1, 4, 5}, {0, 1}
+    count = 0
+    for e0 in combinations(range(7), 4):
+        e = set(e0)
+        if a <= e or len(e & c0) < 2 or len(e & c1) < 2:
+            continue
+        t = c0 | c1 | e
+        need(len(t) <= 7, "three-set union bound")
+        for d0 in combinations(range(9), 4):
+            d = set(d0)
+            if min(len(d & c0), len(d & c1), len(d & e)) < 2:
+                continue
+            need(len(d - t) <= 1, "each extension adds at most one coordinate")
+            count += 1
+    no_pair = [c0, c1, {0, 2, 4, 6}, {0, 2, 4, 7}, {0, 2, 4, 8}, {0, 2, 4, 9}]
+    outside = [{2, 3}, {2, 4}, {2, 5}, {6, 7}, {6, 8}, {6, 9}]
+    common_pair = [a | e for e in outside]
+    for family in (no_pair, common_pair):
+        need(all(len(x & y) >= 2 for x, y in combinations(family, 2)), "pair intersections")
+        need(len(set().union(*family)) == 10, "sharp combinatorial union bound")
+    need(len(set.intersection(*no_pair)) == 1, "first extremal family has no common pair")
+    need(set.intersection(*common_pair) == a and matching(outside) == 2,
+         "second extremal family has outside matching two")
+    repeated = outside + [outside[0]]
+    need(matching(repeated) == 2 and len(set().union(*repeated)) <= len(repeated) + 2,
+         "repeated supports retain the edge bound")
+    sunflower = [{2 + 2 * i, 3 + 2 * i} for i in range(6)]
+    need(matching(sunflower) == 6 and len(a | set().union(*sunflower)) == 14,
+         "pair intersections alone do not imply the small-union bound")
+    return {"normalized_extension_checks": count,
+            "no_common_pair_extremal_union": 10, "common_pair_extremal_union": 10,
+            "repeated_support_control": True, "sunflower_union_without_sign_obstruction": 14}
+
+
+def positive_three_block_root():
+    queries = canonical(2)
+    check_root(queries)
+    for x, y in queries:
+        support(x, y, eye(4))
+    return {"full_blocks": 3, "ambient_dimension": 4, "defect": 2,
+            "all_three_stages": "I4; commute and satisfy every prefix"}
+
+
+def noncommuting_boundary():
+    queries = canonical(6)
+    check_root(queries)
+    projectors = []
+    for i in range(6):
+        j = 0 if i else 1
+        x = [Q(i == k) for k in range(6)]
+        y = [Q((i > k) - (i < k)) for k in range(6)]
+        w = [Q(k == j) * y[j] for k in range(6)]
+        p = [[x[a] * x[b] + w[a] * y[b] for b in range(6)] for a in range(6)]
+        p = tensor2(p)
+        support(*queries[i], p)
+        projectors.append(p)
+    bad_pairs = sum(mm(p, q) != mm(q, p) for p, q in combinations(projectors, 2))
+    need(bad_pairs > 0, "support alone does not imply commuting stages")
+    rejected(lambda: need(bad_pairs == 0, "stage commutation"), "commutation omitted")
+    return {"root_blocks": 7, "selected_full_blocks": 6, "ambient_dimension": 12,
+            "defect": 2, "selected_stage_ranks": [4] * 6,
+            "noncommuting_stage_pairs": bad_pairs}
+
+
+def characteristic_two_boundary():
+    xs, ys, ps = [], [], []
+    for i in range(6):
+        x = [[Q((r == c) or (r == 2 + 2 * i + c)) for c in range(2)] for r in range(14)]
+        y = [list(row) for row in zip(*x)]
+        mask = {0, 1, 2 + 2 * i, 3 + 2 * i}
+        p = [[Q(r == c and r in mask) for c in range(14)] for r in range(14)]
+        support(x, y, p, 2)
+        need(rank(x, 2) == rank(y, 2) == 2, "characteristic-two query rank")
+        need(same(mm(y, x), [[0, 0], [0, 0]], 2), "characteristic-two square zero")
+        xs.append(x); ys.append(y); ps.append(p)
+    for i, j in combinations(range(6), 2):
+        need(same(mm(ys[i], xs[j]), eye(2), 2) and same(mm(ys[j], xs[i]), eye(2), 2),
+             "ordered signs coincide in characteristic two")
+        need(mm(ps[i], ps[j]) == mm(ps[j], ps[i]), "coordinate stages commute")
+    xall = [[v for x in xs for v in x[r]] for r in range(14)]
+    yall = [row for y in ys for row in y]
+    need(rank(mm(yall, xall), 2) == 12, "characteristic-two Gram rank")
+    return {"field": "F2", "selected_full_blocks": 6, "stage_union_dimension": 14,
+            "block_gram_rank": 12, "isolated_Gram_support_lemma_only": True,
+            "purpose": "the characteristic restriction cannot be dropped from the sign contradiction"}
+
+
+def main():
+    result = {"status": "PASS_PAIRED_DEFECT_TWO_STAGE_CAP",
+              "claim": "at most five rank-two full blocks with commuting rank-four stages in defect two",
+              "sign_gram": sign_gram(), "set_controls": set_controls(),
+              "positive_three_full_block_root": positive_three_block_root(),
+              "commutation_boundary": noncommuting_boundary(),
+              "characteristic_boundary": characteristic_two_boundary(),
+              "negative_controls": ["corrupt inverse rejected", "noncommuting stages rejected",
+                                    "characteristic-two counterexample outside declared scope"],
+              "new_kappa": False}
+    print(json.dumps(result, indent=2))
+    print(result["status"])
+
+
+if __name__ == "__main__":
+    main()