Mister-Meeseeks · Oct 20, 2026 · Oct 19, 2026
diff --git a/research/qq16-query-schur/PROOF.md b/research/qq16-query-schur/PROOF.md
@@ -0,0 +1,126 @@
+# The ordered Schur residual at the actual future-query boundary
+
+Chris R / Clear1nsight, with substantial OpenAI Codex assistance. Apache-2.0.
+This is an exact source-bound logical obstruction to one proposed factorization.
+It is not a lower bound on native children or a supplier admission.
+
+## Boundary and source
+
+The source is the F0/B1 full-recovery word of ywz65's PR2707, using the
+retained Arham Tahir PR2681 source reconstruction. All runtime dependencies are
+pinned at canonical main `20ecf2891d80b5acf18d980b2164fb44ea7faa90`.
+PR3985, head `400df7fca8f60c19bf163c77564fe3fbe9154b04`, motivates the
+question; its executable package is not a dependency. Its rectangular future
+correction reads the 104 U+T fields and writes only the eight A fields.
+
+Write r_p for column p of the actual 8-by-112 matrix R. The selected minors obey
+R_A R_A^t=R_T R_T^t=4I, R_U R_U^t=48I. Let g_{s,p} be the actual
+involutive owner route at stage s. An ordered route [g][h] means first h,
+then g. The source routes are orthogonal; under the inherited pushforward
+owner convention their action on a character labelled v is labelled ghv. These are
+logical array operators; native convolution changes the physical frame and
+must still be charged by any implementation.
+
+At the first stage-2 event, the literal source prefix gives, with a=Q1(Y),
+
+    W_p = Y_p - (1/4) sum_j R[j,p] [g1,p] a_j       (p in U),
+    W_p = Y_p + X_p - (1/4) sum_j R[j,p] [g1,p] a_j (p in T).
+
+Here X and Y are the current borrowed arrays at entry, not an earlier record.
+The verifier reconstructs all 104 rows from the actual prefix and checks these
+identities in the rational owner group ring with all 224 current sources free.
+
+## Missing correction
+
+Replacing those W_p reads with borrowed Y_p loses exactly
+
+    Q2(W_(U+T)) - Q2(Y_(U+T)) = Q2(X_T) - M21 a,
+    M21 = (1/4) sum_(p in U+T) r_p r_p^t [g2,p g1,p].
+
+The multiplication order is essential. All 104 products g2,p g1,p are distinct,
+and reversing the products changes the action already on character v=1.
+The formula includes the eight T-port X terms: they are not part of the
+rank-eight correction and cannot be omitted.
+
+All actual g2,p fix q_p. Therefore mapping the borrowed Y_p hole frame with
+the actual affine shift really does reach the common F16 frame without the
+negative C_q child. This is checked for all 104 terms using the full quadratic
+phase polynomial. The proposed bypass passes that frame check but loses the
+logical residual above. A legal frame is insufficient to identify the value.
+
+## Why the scalar Schur shortcut passes constants and fails arrays
+
+The trivial owner character v=0 sends every owner permutation to 1. On that
+subspace M21 becomes (48I+4I)/4=13I. Thus constant-owner tests would accept a
+scalar correction 13a.
+
+On the single nontrivial character v=1, however, the 104 images
+
+    (g2,p g1,p) 1, p in U+T
+
+are pairwise distinct. For entry (0,0), 52 ports have R[0,p]^2=1. Its action
+on a_0=chi_1 is a sum of 52 distinct characters, each with coefficient 1/4;
+none is chi_1. This cannot equal 13chi_1. RESULT.json records every image,
+coefficient and source port so that the witness is directly inspectable.
+
+These are attainable query inputs, not an enlarged-domain fiction. For any
+eight logical arrays a, set X=0, Y_(U+T)=0, and
+
+    Y_p = (1/4) sum_j R[j,p] [g1,p] a_j, p in A.
+
+Then Q1(Y)=a because g1,p is involutive and R_A R_A^t=4I. The verifier checks
+this with eight independent array inputs. On this legitimate current input,
+the borrowed-Y bypass query is zero and the actual query is -M21 a.
+The A response cannot hide this discrepancy: undoing its eight stage-2 routes
+and applying R_A recovers the query. Hence the actual recovery boundary
+requires a correction; scalar 13I does not supply it for general arrays.
+
+## Exact scope of the 104-branch bound
+
+Consider only expressions of the form
+
+    M21 = sum_(b=1)^B C_b [h_b],
+
+where C_b is an arbitrary constant 8-by-8 rational matrix and each branch
+applies a single common linear owner permutation h_b to all eight channels.
+Scalar mixing before or after that route is included in C_b. There are no
+character-dependent projections, Fourier transforms, extra native kernels,
+sequentially reused intermediate branches, or sums of owner routes hidden
+inside a branch.
+
+Apply the expression to eight independent amplitudes times chi_1. A branch
+has one output character h_b 1, so B branches have at most B different
+character labels. The source expression has 104 distinct labels, with
+nonzero coefficient matrix r_p r_p^t/4 at each. Linear independence of
+characters gives B >= 104. The displayed source expression attains 104,
+so the restricted branch count is exactly 104. This uses the actual owner
+permutation representation, not an assumption that a formal group algebra
+acts faithfully. It also excludes the 8- or 16-branch versions of this model.
+
+This is **not** a claim that every implementation needs 104 H1 children,
+104 scalar additions, 104 physical cover sweeps, or 104 storage banks.
+A sequential circuit can reuse routes, and a genuine harmonic decomposition
+could use different primitives. Their frames, coefficient operations,
+restoration, precision and physical tariffs must be supplied separately.
+
+## Obligation ledger and stopping decision
+
+| Obligation | Status | Evidence or missing object |
+|---|---|---|
+| Actual prefix residual, including T-port X reads | Proved within pinned logical model | All 104 source rows and full operator equality |
+| Constant-character 13I and nontrivial counterexample | Proved | Exact rational character arithmetic |
+| Arbitrary query attainability and nonzero A response | Proved | Source A minor and actual involutive routes |
+| Single-owner-route branch optimum 104 | Proved for stated model | Character support bound and explicit 104-term expression |
+| Physical legality of borrowed-Y hole maps | Proved within inherited frame model | 104 full phase-polynomial equalities |
+| Cheaper complete residual circuit with fewer native children | Unknown | No typed literal construction supplied |
+| Retaining eight prefix queries across native calls | Unknown | Source private scratch is cleared; it cannot be kept for free |
+| Physical maps, storage, movement, all-depth precision and restoration | Unknown | A changed complete provider/consumer contract is required |
+| Supplier coverage, both moment budgets and improved kappa | Unknown | Local branch count supplies none of these |
+
+Stop the scalar-Schur/8-or-16-one-route-branch repair here. Its intended saving
+was removal of 104 negative normalizers from PR3985, but the residual is real
+and the proposed compressed repair fails. No native cost saving is claimed.
+A viable reopening must exhibit a different typed circuit for the ordered
+operator, price its retained inputs and final cleanup, and bind the result to
+an actual outer consumer. The conditional incidence budget of PR3976 is only
+an optimistic screen, not permission to treat unknown costs as zero.
diff --git a/research/qq16-query-schur/README.md b/research/qq16-query-schur/README.md
@@ -0,0 +1,72 @@
+# QQ16 ordered-query Schur obstruction
+
+The missing correction in the borrowed-current-Y shortcut is
+`Q2(X_T) - M21 Q1(Y)`, with
+`M21 = (1/4) sum_(p in U+T) r_p r_p^t [g2,p g1,p]`.
+The actual source has 104 distinct ordered owner routes. One character,
+`v=1`, separates all 104, establishing an exact **104-branch** optimum for
+constant channel mixing with one common owner route per parallel branch.
+This excludes the proposed 8- or 16-branch factorization in that precise model.
+
+The constant-character restriction is `13I`; using it on general arrays is
+wrong. A diagonal entry sends one character to 52 distinct characters with
+coefficient 1/4 each. All eight query inputs are attainable from actual current
+Y supported on A, and the A response is injective, so this failure applies to
+the real F0/B1 recovery boundary. The bypass's 104 hole-frame maps are legal;
+they do not repair its omitted value correction.
+
+This result does not lower native cost, establish native-child optimality or
+improve kappa. It supplies the exact missing operator and a discriminating
+counterexample before investing in an invalid compressed repair.
+See [PROOF.md](PROOF.md) for the model, proof, complete obligation ledger and
+stop decision. [RESULT.json](RESULT.json) retains the full source-bound receipt.
+
+## Reproduction
+
+Python 3.12, standard library, from the repository root:
+
+```sh
+python3 -I -B research/qq16-query-schur/verify.py
+python3 -I -O -Werror -B research/qq16-query-schur/test_verify.py
+python3 -B scripts/research_package.py --package research/qq16-query-schur
+```
+
+The verifier authenticates every declared transitive runtime source before
+executing inherited code. It compares the whole typed receipt, works in a
+minimal Git-free read-only export, and rejects source/receipt changes and
+semantic controls. It does not rerun the full selected supplier or prior
+native-kernel theorem. The inherited frame identities are checked only for
+the 104 maps involved in this proposed bypass.
+
+## Workflow and predecessor credit
+
+Canonical main is `20ecf2891d80b5acf18d980b2164fb44ea7faa90`, priority revision 6.
+This is the assigned representation-theory/harmonic-analysis item within the
+[coordinated claim](https://github.com/CrocSwap/integer-mult-bounds/pull/3985#issuecomment-6263114494).
+The live overlap check included PR1969: its source-level `M=12I` is for one
+chart's Gram identity; the cross-chart ordered `M21` here is a different
+operator. The current result retains Ali Romman's joint-query construction,
+ywz65's PR2707 line-normalized decoder, Arham Tahir's PR2681 source-bound
+recovery checker, and their credited native geometry and supplier lineage.
+Their files are unchanged. PR3985 at
+`400df7fca8f60c19bf163c77564fe3fbe9154b04` supplied the rectangular-correction
+question and failed borrowed-Y bypass; no pending PR executable is imported.
+
+This focused audit refines the `joint-query-controller` card. The family
+expansion decision is bounded: derive the actual residual, test a cheap
+factorization, and stop at a precise failure. Unknown complete physical costs
+remain unknown. The source archive is not a new supplier admission.
+
+New work: Chris R / Clear1nsight, with substantial OpenAI Codex assistance in
+mathematical derivation, implementation and review. Apache-2.0. No independent
+human review is claimed.
+
+## Open next questions
+
+Can a genuinely different typed circuit implement the ordered `M21` residual
+more cheaply than the 104 removed normalizers? First pin its retained-query
+input frames and dirty/owned lifetime contract, then exhibit a literal word
+and compare its full invoice with the source operations it replaces. Sequential
+route reuse, a paid character decomposition, or a changed producer may evade
+the restricted parallel-branch bound. Their costs and outer supplier binding
+are unresolved. Another constant-character test cannot answer that question.