diff --git a/research/clifford-residual-count-bound/PROOF.md b/research/clifford-residual-count-bound/PROOF.md
new file mode 100644
index 0000000000..1a604a4407
--- /dev/null
+++ b/research/clifford-residual-count-bound/PROOF.md
@@ -0,0 +1,211 @@
+# A uniform Clifford Gram bound from nonsingular residual forms
+
+kumagi, with substantial OpenAI Codex assistance. Apache-2.0.
+
+This sharpens the sufficient constant in Ali Romman's
+[pointwise-faithfulness proof](../clifford-pointwise-faithfulness/PROOF.md),
+PR #5526, Sections 3–5. The tensor-width threshold and operator alphabet
+are unchanged. This is a scoped algebraic result, not a multiplication
+algorithm or an improvement to the selected κ.
+
+## Statement
+
+Let n >= 1, D = 2^n, and choose one unitary representative U_g of each
+projective n-qubit Clifford class. For every integer f >= 4n+4, and arbitrary
+complex coefficients b_g chosen at that width,
+
+    α sum_g |b_g|²
+      <= D^(-f) ||sum_g b_g U_g^(tensor f)||_HS²
+      <= (2-α) sum_g |b_g|²,                         (1)
+
+where
+
+    α = 1491359 / 4161536 > 358367/1000000 > 1/3.
+
+Thus (1/3) I <= Gram_f <= (5/3) I is a convenient weaker statement,
+improving the predecessor's sufficient interval [1/9,17/9] at the same
+width. It applies to subsets and is invariant under representative phases.
+Neither α nor the width threshold is asserted to be spectrally optimal.
+
+More generally, for an integer s >= 0 and f >= 4n+4+2s, the absolute
+off-diagonal row sum is at most
+
+    T_s = sum_(k>=1) 2^(-k(k+1)/2-sk).               (2)
+
+Consequently [1-T_s,1+T_s] is a sufficient spectral interval.
+
+## 1. Residual forms, with a fixed coordinate convention
+
+Work over F_2. Let V have even dimension N = 2n and nondegenerate
+alternating form ω(x,y) = x^T J y. For S in Sp(V), put W = im(S-I) and
+k = dim W. The identity ker(S-I) = W-perp follows from
+
+    ω(x,(S-I)y) = ω((S^(-1)-I)x,y).
+
+Define B on W by
+
+    B((S-I)x,w) = ω(x,w).                            (3)
+
+It is well-defined by that kernel identity. If the left argument has zero
+pairing with all w, then x is in W-perp and (S-I)x = 0; hence B is
+nonsingular. Expanding S's preservation of ω gives
+
+    B(u,v) + B(v,u) = ω(u,v).                        (4)
+
+For example, with u=(S-I)x and v=(S-I)y, both sides of (4) reduce to
+ω(x,Sy)+ω(Sx,y). This also fixes the convention: interchanging the two
+arguments of B changes the reconstruction formula.
+
+Choose an ordered basis of W and let E be its N by k column matrix. Write
+B for the k by k matrix of the residual form in this basis. Then
+
+    E^T J E = B+B^T,                                 (5)
+    S = I + E B^(-T) E^T J.                          (6)
+
+Indeed (3) says B^T a = E^T J x for (S-I)x = E a.
+This proves uniqueness of S given (E,B).
+
+Conversely, any injective E and nonsingular B satisfying (5) give a
+symplectic S by (6), with displacement rank k. To check symplecticity,
+expand S^T J S: the extra middle factor is
+
+    B^(-T) + B^(-1) + B^(-1)(B+B^T)B^(-T) = 0.
+
+The rank follows because E is injective and E^T J is surjective. This
+converse is also checked in the finite enumeration, although only the
+forward direction and uniqueness are needed for the upper bound below.
+
+## 2. Count embeddings before forms
+
+Let c_(N,k) count S in Sp(V) with rank(S-I)=k. Each S has exactly
+|GL(k,2)| ordered bases for W, so the number of pairs (E,B) above is
+c_(N,k) |GL(k,2)|.
+
+Fix instead any nonsingular k by k matrix B. Construct the columns
+e_0,...,e_(k-1) of E in order. After i independent columns have been
+chosen, (5) imposes i linear equations on e_i:
+
+    ω(e_j,e_i) = B_(j,i)+B_(i,j),   0 <= j < i.
+
+The i linear functionals are independent by nondegeneracy of ω and
+independence of the previous columns. Thus there are exactly 2^(N-i)
+solutions before requiring e_i to lie outside their span, and at most
+that many after. Diagonal equations are automatic in characteristic two.
+Therefore, for every fixed B, the number of injective E is at most
+
+    product_(i=0..k-1) 2^(N-i) = 2^(Nk-k(k-1)/2).
+
+There are |GL(k,2)| possible nonsingular B. Dividing the resulting pair
+bound by the number of bases gives
+
+    c_(N,k) <= 2^(Nk-k(k-1)/2),   1 <= k <= N.        (7)
+
+The cancellation is the improvement: singular forms are never included,
+and the count is organized by B before E. In comparison, the predecessor
+first chooses W and bounds by all forms with its prescribed symmetrization.
+At k=1, (7) is slightly weaker than the exact 2^N-1 transvection count;
+the improvement comes from the other ranks. No formula for |GL(k,2)| is
+needed, and no independence between choices of E and B is assumed.
+
+## 3. From rank counts to the Gram envelope
+
+We retain the predecessor's signed-Pauli trace argument, restated here to
+make the multiplicity and normalization explicit. For a Clifford U with
+symplectic Pauli action S, let L=ker(S-I). Conjugation by U on the
+Hermitian Pauli basis has trace |tr U|². Its signs at the fixed labels
+form a character of L. Their sum is either zero or 2^dim L.
+
+All projective lifts of a fixed S differ by the 2^N Paulis. Their signs
+on L run through every character of L, with multiplicity 2^(N-dim L).
+Consequently, for rank(S-I)=k, exactly 2^k projective lifts have nonzero
+trace, with normalized trace modulus
+
+    |tr U|/D = 2^(-k/2).
+
+For k=0 only the identity projective class contributes; the other Paulis
+have trace zero. Relative products U_g^* U_h give the same trace-modulus
+distribution about every projective class. Therefore the exact absolute
+row sum of the full tensor Gram matrix is
+
+    R_(n,f) = sum_(k=1..N) 2^k c_(N,k) 2^(-kf/2).
+
+Using (7) at f >= 2N+4+2s gives, term by term,
+
+    2^k c_(N,k) 2^(-kf/2)
+        <= 2^(Nk+k-k(k-1)/2-k(N+2+s))
+         = 2^(-k(k+1)/2-sk).
+
+Extending this finite nonnegative sum to infinity proves (2). Larger
+widths, including odd widths, only decrease the absolute row sum.
+For a Hermitian matrix with diagonal one and row sum at most t, bounding
+each off-diagonal quadratic term by |b_g|²+|b_h|² gives the spectral
+interval [1-t,1+t]. This proves the claimed Gram inequalities.
+
+For an exact rational constant, keep k=1,...,5 in T_0. The first omitted
+term is 2^(-21); the ratio of each later term to its predecessor is at
+most 2^(-7). Hence
+
+    T_0 <= sum_(k=1..5) 2^(-k(k+1)/2)
+                + 2^(-21)/(1-2^(-7))
+         = 2670177/4161536 < 2/3.
+
+Subtracting from one gives α in (1). More generally the same cutoff gives
+an explicit rational upper bound on T_s, with first omitted term
+2^(-21-6s) and tail ratio at most 2^(-7-s). The verifier uses integer
+arithmetic and exact fractions for these bounds.
+
+## 4. Consequences and scope
+
+If a unitary Clifford target T is absent from a set of projective classes
+S, then at any f >= 4n+4,
+
+    D^(-f) ||T^(tensor f) - sum_(g in S) b_g U_g^(tensor f)||_HS²
+        >= α (1 + sum_g |b_g|²) >= α.
+
+Thus its operator norm approximation error is at least sqrt(α), in
+particular at least 1/sqrt(3). The implication uses
+||A||_HS <= sqrt(D^f) ||A||_op. This is a worst-case unit-input error;
+it is not a lower bound on every input's error.
+
+The predecessor's fixed-residual four-width theorem also inherits α.
+For its exact Gaussian-dyadic Clifford group, write each exact operator
+as i^j U_g and let M = sum_(g,j) |c_(g,j)|² after equal exact operators
+are combined. At residue r put β_(g,r)=sum_j c_(g,j)i^(jr). Parseval says
+(1/4) sum_(g,r)|β_(g,r)|²=M. Apply (1) separately at the four widths
+4n+4,...,4n+7 and average: at least one normalized squared residual norm
+is >= α M. Vanishing at all four widths is still equivalent to all
+coefficients being zero. The residual coefficients must be fixed across
+these tests; pointwise (1) itself permits width-dependent coefficients.
+
+Scalar-phase copies must be combined with the phase raised to f. The
+projective Gram bound does not hold for repeated exact-phase copies as
+separate columns. Four phase residues are specific to the predecessor's
+Gaussian-dyadic scalar group; this is not a four-test theorem for arbitrary
+unitary phases or nonunitary scalar multiples.
+
+We do not change the threshold 4n+4, determine sharp one-/two-axis spectra,
+improve the rectangular stabilizer-map theorem, or validate any new complete
+caller. In particular this is not a new paid-call count, matched QQ16 bill,
+physical routing bound, affordable supplier, or selected-frontier admission.
+Applying the stronger error constant to an actual caller still requires
+checking its full operator alphabet and retained state. No such new source
+application is claimed here.
+
+## 5. Evidence and attribution
+
+The written argument proves the all-n statement subject to mathematical
+review. The checker independently constructs signed Clifford actions from
+literal H, S and controlled-X conjugations, and constructs symplectic maps
+from every small residual subspace and nonsingular form. It compares the
+entire sets for n=1,2, not just their cardinalities. It also checks trace
+multiplicities, exact row sums, rational tails and invalid conventions.
+Finite enumeration corroborates the proof; it does not establish its
+universal quantifiers or constitute formal-kernel/human acceptance.
+
+The residual-form method is classical. Ali Romman's #5526 supplies the
+explicit residual/trace-lift framework and tensor Gram/four-width
+consequences reused above; its attribution to earlier stabilizer and
+finite-alphabet work remains in the pinned input. The contribution here
+is the nonsingular-form-first double count and the resulting improved
+uniform constants within this repository, not a literature-priority claim
+for residual forms, Clifford counts, Gershgorin bounds or Fourier inversion.
diff --git a/research/clifford-residual-count-bound/README.md b/research/clifford-residual-count-bound/README.md
new file mode 100644
index 0000000000..7126e769fb
--- /dev/null
+++ b/research/clifford-residual-count-bound/README.md
@@ -0,0 +1,142 @@
+# Stronger uniform Clifford tensor separation
+
+kumagi, with substantial OpenAI Codex assistance. Apache-2.0.
+
+For the same projective n-axis Clifford alphabet and the same sufficient
+width `f >= 4n+4`, this package improves the guaranteed tensor Gram interval
+from **[1/9,17/9] to [1/3,5/3]**. The proof actually gives the stronger
+lower constant `α = 1491359/4161536 > 0.358367` and upper constant `2-α`.
+The coefficients may be arbitrary complex numbers chosen at the tested width.
+This makes the existing algebraic separation guarantee more robust; it does
+not improve the multiplication exponent or supply a physical caller.
+
+The new step is a short double count: pair an ordered basis of the residual
+space with its nonsingular residual form, and count in the opposite order
+from the predecessor's loose estimate. For `1 <= k <= 2n`,
+
+```
+#{S in Sp(2n,2): rank(S-I)=k} <= 2^(2nk-k(k-1)/2).
+```
+
+With the existing `2^k` nonzero-trace Pauli lifts per such `S`, the absolute
+Gram row sum at `f >= 4n+4+2s` is at most
+`sum_{k>=1} 2^(-k(k+1)/2-sk)`. An exact geometric tail gives the constant
+above. See [PROOF.md](PROOF.md) for the all-dimension argument, including
+normalization, reconstruction transpose, phases and quantifiers.
+
+A missing projective target therefore has worst-case operator norm
+approximation error at least `sqrt(α)`, and in particular `1/sqrt(3)`,
+instead of the predecessor's `1/3`. For a fixed Gaussian-dyadic residual
+with squared coefficient norm `M`, one of the four widths `4n+4,...,4n+7`
+has normalized squared residual norm at least `α M`, improving `M/9`.
+These are direct algebraic corollaries, not a newly audited caller application.
+
+## Selection, sources and overlap
+
+Started from canonical main `df0137efd35e11b4445734bf612bdd4c7ebc330c`,
+priority revision 7, after reading the root guidance and #1166 handoffs.
+The current picker returned track `recursive-interfaces`, seed
+`1f66e16685e4ef83d568f7fabb3db680`. This is an explicit scope change from
+`joint-query-controller`: an enabling separation lemma, not the card's
+complete matched QQ16 bill. The card's resolved first example,
+`scripts/research_selected_baseline.py`, passed binding checks only.
+The selected κ and all inherited assumptions remain unchanged.
+
+The direct predecessor is Ali Romman's [PR #5526](https://github.com/CrocSwap/integer-mult-bounds/pull/5526),
+head `45f7de73b168721cdf7ec8c1769b1b594493716a`; its retained
+[proof](../clifford-pointwise-faithfulness/PROOF.md) is byte-pinned in
+[SOURCES.json](SOURCES.json). Its Section 3 supplies the signed trace-lift
+argument and residual forms; Sections 4–5 supply the Gram and four-width
+framework. We strengthen the count, preserving their attribution and that
+of their classical and repository predecessors. No predecessor executable
+is imported or rewritten.
+
+[Claim and canonical discussion](https://github.com/CrocSwap/integer-mult-bounds/discussions/5236#discussioncomment-19189185).
+The initial 05:37–05:40 UTC search on 2026-10-26 paginated all 374 open PRs
+and 5,002 Discussion records, supplemented by Git HEAD searches of package
+README/TASK notes and relevant proofs. The helper's sparse local coverage
+was incomplete; the supplemental searches are not a full proof audit or
+novelty certificate. A pre-submission refresh at 05:53–05:54 UTC covered 376 open PRs and
+5,007 Discussion records; targeted full-cache checks found the predecessor
+and this claim, but no competing nonsingular-form count claim. Canonical
+main was unchanged. The sharp one-axis work in #5549/#5594 and sharp
+two-axis work in #5675 concern different claims. This package changes the
+uniform all-n sufficient constant at the existing width, not those exact
+finite spectra or thresholds. #5547 and the paid-return/application audits
+remain their authors' independent work.
+
+## Verification
+
+The package uses only Python's standard library. Run from the repository root:
+
+```sh
+python3.12 -B scripts/research_package.py --package research/clifford-residual-count-bound
+python3.12 -B scripts/check_research_commit.py --package research/clifford-residual-count-bound --check-source-history
+```
+
+[VERIFY.json](VERIFY.json) registers both ordinary and optimized (`-O`)
+execution. Both passed on macOS with CPython 3.12.14. Checks use explicit
+exceptions, not removable Python assertions.
+The standalone verifier also runs in an exported tree without Git, with
+its declared predecessor proof present at the repository-relative path:
+
+```sh
+python3.12 -B research/clifford-residual-count-bound/verify.py
+```
+
+Two constructions agree on the entire small symplectic sets:
+
+| n | Projective signed Clifford actions | Symplectic rank histogram, k=0,...,2n | Exact Gram row sum at f=4n+4 |
+|---|---:|---|---|
+| 1 | 24 | 1, 3, 2 | 13/32 |
+| 2 | 11,520 | 1, 15, 100, 300, 304 | 37739/65536 |
+
+The first construction closes signed Pauli permutations under H, S and
+controlled-X. Each generator's full signed table is independently checked
+against literal Gaussian-integer matrix conjugation (unnormalized H with
+its factor two retained); these small integers are exactly representable
+in Python complex arithmetic. The second enumerates every binary subspace
+and compatible nonsingular residual form, then reconstructs the symplectic
+map. No group-enumeration or linear-algebra library is used.
+
+The verifier also checks every fiber's `2^k` nonzero-trace lifts, exact row
+sums and the infinite-tail rational certificate. Five negative controls
+reject a singular form, the wrong reconstruction transpose, a lost Pauli
+sign, an omitted lift multiplicity and a width below this sufficient bound.
+A failed sufficient bound is not evidence of dependence at smaller widths.
+
+The finite checks corroborate the written proof; neither they nor the
+metadata/replay checks constitute independent mathematical acceptance.
+No full selected-frontier replay is needed or claimed for this separate
+algebraic package. Source hashes, commit availability and source-export
+checks authenticate the declared evidence, not the theorem's correctness.
+
+## Limits
+
+The Gram columns must represent distinct **projective** Clifford operators.
+Scalar copies are combined with their phase raised to the tested width.
+Four-width testing requires the predecessor's fixed residual and four-element
+Gaussian-dyadic scalar group. The theorem does not cover arbitrary nonlinear,
+rounded, cross-column or non-Clifford operations, or arbitrary nonunitary
+scalings. It does not sharpen the predecessor's rectangular stabilizer-map
+bound, establish a least tensor width, or give an optimal spectral constant.
+
+A complete caller still needs its exact alphabet, retained dirty state,
+ownership and physical costs audited. No paid-call count, matched caller
+budget, new algorithm, unconditional multiplication theorem or frontier
+admission follows from this constant improvement alone.
+
+## Open next questions
+
+- Can phase cancellation yield a stronger all-n spectral bound than the
+  absolute-row estimate? Start from the existing #5594/#5675 finite spectra
+  and seek a uniform representation argument, without repeating those censuses.
+- Does one exact complete caller satisfy the alphabet premise for the
+  stronger error guarantee? Pin its operations and retained state and consult
+  the existing application audits before substituting this constant.
+
+The corresponding dependencies and first steps are in [TASK.json](TASK.json).
+The count is presented as an improvement to the repository's retained proof,
+not a claim of priority in the mathematical literature. All derivation, code
+and writing received substantial OpenAI Codex assistance for kumagi; no
+independent human review or formal-kernel proof is claimed.
diff --git a/research/clifford-residual-count-bound/SOURCES.json b/research/clifford-residual-count-bound/SOURCES.json
new file mode 100644
index 0000000000..8f2ce658ab
--- /dev/null
+++ b/research/clifford-residual-count-bound/SOURCES.json
@@ -0,0 +1,24 @@
+{
+  "schema_version": 1,
+  "base_commit": "df0137efd35e11b4445734bf612bdd4c7ebc330c",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8",
+      "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602",
+      "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72"
+    },
+    {
+      "path": "research/clifford-pointwise-faithfulness/PROOF.md",
+      "usage": "input",
+      "git_blob": "465009d9d1b6947e80e6f1e868022f47ddab1f3c",
+      "sha256": "45483e4b5f604a5e70602c5caaa4394d4a0d0d1a6d0b6e8a93b836d50b23f764"
+    }
+  ]
+}
diff --git a/research/clifford-residual-count-bound/TASK.json b/research/clifford-residual-count-bound/TASK.json
new file mode 100644
index 0000000000..6fece57ca9
--- /dev/null
+++ b/research/clifford-residual-count-bound/TASK.json
@@ -0,0 +1,102 @@
+{
+  "schema_version": 1,
+  "task_id": "joint-query-controller",
+  "priority_revision": 7,
+  "base_commit": "df0137efd35e11b4445734bf612bdd4c7ebc330c",
+  "original_card": {
+    "id": "joint-query-controller",
+    "question": "Can the installed QQ16 caller win a complete matched protocol bill, or can a changed demand eliminate actual paid work?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "research/qq16-caller-install/README.md"
+    ],
+    "methods": [
+      "Derive the matched whole-caller physical bill for installed and baseline protocols.",
+      "Change the actual demanded observations and prove a cheaper legal producer/consumer contract."
+    ],
+    "acceptance_gate": "Name the changed premise of the fixed F0/B1 observation obstruction. Show exactly which query is recovered, legal native reads and restoration, and a full favorable budget including cover maps, helpers and endpoints. Local inverse identities alone do not close the global controller. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Read #4166 COST.md and ADMISSION.json. An actual caller connection is now proposed. Its native-component profile loses; parent park/restore versus external-call costs remain unresolved. Retain the producer and recovery lineage rather than rebuild it.",
+      "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately."
+    },
+    "first_experiment": "At the actual installed cut, compare matched complete parent park/restore and external input/return protocols at the same bank/packet geometry, including every later root call and service cost. Alternatively pin both bridge observations and derive a genuinely smaller source-compatible demand. Stop if the complete necessary inequality fails or an essential cost is unknown; no larger decoder scan from a local tape-action saving.",
+    "bottleneck_link": "The native local words exist; retained query information and its physical access are the missing link to a composed recursive interface.",
+    "allowed_variations": [
+      "One paid query, one changed first pair, or one precisely specified affine helper state.",
+      "A counterexample or lower bound for that exact proposed repair.",
+      "One unresolved obligation of a newer local decoder, with exact source heads and a distinct claim/domain."
+    ],
+    "scope_change_triggers": [
+      "Retaining the fixed first pair and ordinary schedule while allowing only homogeneous selected-only control, already excluded by the witness.",
+      "Treating cover-map counts as zero-cost physical address operations.",
+      "Recreating the pending complete local decoder or early-record/output-bank coalescing already under investigation without a distinct audit or changed premise.",
+      "Treating a completed-output defect inequality as a producer-interior, dirty-range or physical-cost certificate.",
+      "Recreating completed-output recovery or caller wiring already supplied by #4166 without new independent coverage.",
+      "Dropping retained later root calls or claiming native-profile dominance from the isolated publication saving."
+    ],
+    "overlap_terms": [
+      "QQ16",
+      "joint-query",
+      "changing-chart controller",
+      "selected observation",
+      "1969",
+      "2540",
+      "early record",
+      "output-bank retention",
+      "complete native decoder",
+      "2965",
+      "producer defect",
+      "dirty-helper range",
+      "F17 consumer",
+      "4166",
+      "qq16-caller-install"
+    ],
+    "existing_checks": [
+      {
+        "scope": "PR #4166: author-checked installed producer/service/return/bridge connection; native-component comparison loses.",
+        "evidence": "research/qq16-caller-install/README.md",
+        "remaining": "Complete matched physical protocol bill, or changed source-compatible demand/circuit; no affordable supplier yet.",
+        "status": "author-checked",
+        "source_commit": "0b082d22a0e9a442d264ab0633e35ef26c790630",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      }
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Bound all-n symplectic displacement counts by nonsingular-form-first double counting, improving the Clifford tensor Gram lower constant at unchanged f >= 4n+4 from 1/9 to at least 1/3.",
+  "scope_change_reason": "The assigned recursive-interface card permits scoped decoder obligations, but this session takes an explicitly narrower algebraic side result suggested by the open best-constant question in PR5526. It does not provide a changed QQ16 demand or a favorable whole-caller bill.",
+  "bottleneck_link": "Quantitative tensor separation supports finite-alphabet obstructions for recursive interfaces. This improves a robust separation constant only; it does not remove the missing physical-cost or source-application obligations.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop after one all-dimension count and n=1,2 independent exact corroboration, or report a counterexample. No larger construction/caller search.",
+  "outcome": "completed",
+  "evidence": "PROOF.md Sections 1-3 give c_(2n,k) <= 2^(2nk-k(k-1)/2), hence uniform Gram lower constant 1491359/4161536 > 1/3. verify.py compares complete signed-action and residual-form constructions for n=1,2, trace-lift multiplicities, rational tails and five negative controls.",
+  "author": "kumagi",
+  "ai_assistance": "Prepared for kumagi with substantial OpenAI Codex assistance in task selection, mathematical derivation, code, verification and writing. No independent human review or formal-kernel proof claimed.",
+  "open_questions": [
+    {
+      "question": "Can the universal spectral lower constant at f=4n+4 be improved beyond the absolute-row estimate?",
+      "why_it_matters": "Phase cancellation may give a stronger robustness guarantee than the triangle inequality.",
+      "first_step": "Compare the universal bound with the exact one-/two-axis spectra in PR5594/PR5675, then formulate a representation-based all-n estimate rather than repeat those finite calculations.",
+      "blocked_by": "Requires a new spectral argument; this package controls only absolute row sums."
+    },
+    {
+      "question": "Does a specific complete recursive caller satisfy the alphabet premise for the stronger error bound?",
+      "why_it_matters": "An algebraic separation constant becomes a caller obstruction only after its full retained state and operations are checked.",
+      "first_step": "Pin one complete caller and audit every branch operator against the projective Clifford premise and existing paid-return audit before substituting the new constant.",
+      "blocked_by": "No new caller alphabet, ownership or complete cost audit is supplied here."
+    }
+  ],
+  "selection": {
+    "seed": "1f66e16685e4ef83d568f7fabb3db680",
+    "track": "recursive-interfaces",
+    "scope_key": "73442cf25caf1ed45f11",
+    "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/5236#discussioncomment-19189185"
+  }
+}
diff --git a/research/clifford-residual-count-bound/VERIFY.json b/research/clifford-residual-count-bound/VERIFY.json
new file mode 100644
index 0000000000..94cf88c267
--- /dev/null
+++ b/research/clifford-residual-count-bound/VERIFY.json
@@ -0,0 +1,30 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/clifford-pointwise-faithfulness/PROOF.md"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Complete n=1,2 signed-Pauli and residual-form set equality; trace lifts; exact uniform rational tail; literal generator signs; five negative controls."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-O",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Same substantive checks with Python assertions disabled; failures use explicit exceptions."
+    }
+  ]
+}
diff --git a/research/clifford-residual-count-bound/verify.py b/research/clifford-residual-count-bound/verify.py
new file mode 100644
index 0000000000..50fad0a06e
--- /dev/null
+++ b/research/clifford-residual-count-bound/verify.py
@@ -0,0 +1,294 @@
+#!/usr/bin/env python3
+"""Exact small Clifford/residual counts and rational tails; standard library only.
+
+kumagi, with substantial OpenAI Codex assistance. Apache-2.0.
+The all-dimension argument is in PROOF.md, not established by enumeration.
+"""
+from collections import Counter, defaultdict, deque
+from fractions import Fraction as Q
+from hashlib import sha256
+import json
+from pathlib import Path
+
+
+def require(ok, message):
+    if not ok:
+        raise ValueError(message)
+
+
+def expect_failure(action, message):
+    try:
+        action()
+    except ValueError:
+        return
+    raise ValueError("negative control accepted: " + message)
+
+
+def apply(columns, vector):
+    result = 0
+    for j, column in enumerate(columns):
+        if vector >> j & 1:
+            result ^= column
+    return result
+
+
+def reduced(vectors):
+    pivots = {}
+    for v in vectors:
+        while v:
+            p = v.bit_length() - 1
+            if p in pivots:
+                v ^= pivots[p]
+            else:
+                pivots[p] = v
+                break
+    for p in sorted(pivots):
+        for q in pivots:
+            if q != p and pivots[q] >> p & 1:
+                pivots[q] ^= pivots[p]
+    return tuple(pivots[p] for p in sorted(pivots))
+
+
+def transpose(columns):
+    return tuple(sum(((columns[j] >> i) & 1) << j
+                     for j in range(len(columns)))
+                 for i in range(len(columns)))
+
+
+def inverse(columns):
+    k = len(columns)
+    rows = [r | (1 << (k + i)) for i, r in enumerate(transpose(columns))]
+    for i in range(k):
+        pivot = next((j for j in range(i, k) if rows[j] >> i & 1), None)
+        require(pivot is not None, "singular residual form")
+        rows[i], rows[pivot] = rows[pivot], rows[i]
+        for j in range(k):
+            if i != j and rows[j] >> i & 1:
+                rows[j] ^= rows[i]
+    return transpose(tuple(r >> k for r in rows))
+
+
+def omega(u, v, n):
+    mask = (1 << n) - 1
+    return (((u & mask) & (v >> n)).bit_count()
+            + ((v & mask) & (u >> n)).bit_count()) & 1
+
+
+def generators(n):
+    width = 2 * n
+    result = []
+    for kind, a, b in ([('H', j, None) for j in range(n)]
+                       + [('S', j, None) for j in range(n)]
+                       + [('CX', j, k) for j in range(n) for k in range(n) if j != k]):
+        table = []
+        for v in range(1 << width):
+            x, z = v & ((1 << n) - 1), v >> n
+            xa, za = x >> a & 1, z >> a & 1
+            if kind == 'H':
+                sign = xa & za
+                x ^= (xa ^ za) << a
+                z ^= (xa ^ za) << a
+            elif kind == 'S':
+                sign = xa & za
+                z ^= xa << a
+            else:
+                xb, zb = x >> b & 1, z >> b & 1
+                sign = xa & zb & (xb ^ za ^ 1)
+                x ^= xa << b
+                z ^= zb << a
+            table.append(x | (z << n) | (sign << width))
+        result.append((kind, a, b, tuple(table)))
+    return result
+
+
+def adjoint(matrix):
+    return [list(map(complex.conjugate, row)) for row in zip(*matrix)]
+
+
+def matmul(a, b):
+    return [[sum(x * y for x, y in zip(row, col)) for col in zip(*b)] for row in a]
+
+
+def pauli(n, v):
+    d = 1 << n
+    x, z = v & (d - 1), v >> n
+    out = [[0j] * d for _ in range(d)]
+    for y in range(d):
+        out[y ^ x][y] = (1j ** ((x & z).bit_count())) * (-1) ** ((z & y).bit_count())
+    return out
+
+
+def validate_generator(n, entry):
+    kind, a, b, table = entry
+    d, signbit = 1 << n, 1 << (2 * n)
+    g = [[0j] * d for _ in range(d)]
+    denominator = 2 if kind == 'H' else 1
+    for y in range(d):
+        if kind == 'H':
+            for bit in range(2):
+                g[(y & ~(1 << a)) | (bit << a)][y] = complex((-1) ** (bit * (y >> a & 1)))
+        elif kind == 'S':
+            g[y][y] = 1j ** (y >> a & 1)
+        else:
+            g[y ^ ((y >> a & 1) << b)][y] = 1 + 0j
+    for v, image in enumerate(table):
+        actual = matmul(matmul(g, pauli(n, v)), adjoint(g))
+        expected = pauli(n, image & (signbit - 1))
+        factor = -denominator if image & signbit else denominator
+        require(actual == [[factor * x for x in row] for row in expected],
+                "literal generator conjugation/sign mismatch")
+
+
+def signed_cliffords(n):
+    width, signbit = 2 * n, 1 << (2 * n)
+    mask = signbit - 1
+    entries = generators(n)
+    for entry in entries:
+        validate_generator(n, entry)
+    identity = tuple(range(signbit))
+    seen, queue = {identity}, deque([identity])
+    while queue:
+        current = queue.popleft()
+        for _, _, _, gen in entries:
+            nxt = tuple(gen[v & mask] ^ (v & signbit) for v in current)
+            if nxt not in seen:
+                seen.add(nxt)
+                queue.append(nxt)
+    require(len(seen) == {1: 24, 2: 11520}[n], "projective Clifford group order")
+    lifts = defaultdict(list)
+    for table in seen:
+        columns = tuple(table[1 << j] & mask for j in range(width))
+        trace_adjoint = sum(-1 if image & signbit else 1
+                            for v, image in enumerate(table) if image & mask == v)
+        k = len(reduced(tuple(col ^ (1 << j) for j, col in enumerate(columns))))
+        require(trace_adjoint in (0, 1 << (width - k)), "trace magnitude")
+        lifts[columns].append(trace_adjoint)
+    histogram, nonzero, zeros = Counter(), Counter(), 0
+    for columns, values in lifts.items():
+        k = len(reduced(tuple(col ^ (1 << j) for j, col in enumerate(columns))))
+        require(len(values) == signbit, "Pauli fiber size")
+        good = sum(v != 0 for v in values)
+        require(good == 1 << k, "nonzero trace lifts")
+        histogram[k] += 1
+        nonzero[k] += good
+        zeros += len(values) - good
+    return set(lifts), histogram, nonzero, zeros
+
+
+def subspaces(width):
+    layer = {()}
+    result = []
+    for k in range(width + 1):
+        result.extend(layer)
+        layer = {basis for e in layer for v in range(1, 1 << width)
+                 if len(basis := reduced(e + (v,))) == k + 1}
+    return result
+
+
+def forms(e, n):
+    k = len(e)
+    coordinates = [(i, j) for j in range(k) for i in range(j + 1)]
+    for bits in range(1 << len(coordinates)):
+        columns = [0] * k
+        for b, (i, j) in enumerate(coordinates):
+            value = bits >> b & 1
+            columns[j] |= value << i
+            if i != j:
+                columns[i] |= (value ^ omega(e[i], e[j], n)) << j
+        if len(reduced(columns)) == k:
+            yield tuple(columns)
+
+
+def reconstruct(e, b, n, wrong_transpose=False):
+    inv = inverse(b if wrong_transpose else transpose(b))
+    columns = []
+    for j in range(2 * n):
+        x = 1 << j
+        rhs = sum(omega(x, w, n) << i for i, w in enumerate(e))
+        a = apply(inv, rhs)
+        require(all(((a & b[i]).bit_count() & 1) == omega(x, w, n)
+                    for i, w in enumerate(e)), "residual reconstruction relation")
+        columns.append(x ^ apply(e, a))
+    return tuple(columns)
+
+
+def residual_symplectics(n):
+    found, counts = set(), Counter()
+    spaces = subspaces(2 * n)
+    require(len(spaces) == {1: 5, 2: 67}[n], "binary subspace inventory")
+    for e in spaces:
+        k = len(e)
+        for b in forms(e, n):
+            s = reconstruct(e, b, n)
+            require(len(reduced(tuple(v ^ (1 << j) for j, v in enumerate(s)))) == k,
+                    "displacement rank")
+            require(all(omega(s[i], s[j], n) == omega(1 << i, 1 << j, n)
+                        for i in range(2 * n) for j in range(2 * n)), "symplecticity")
+            require(s not in found, "residual correspondence duplicate")
+            found.add(s)
+            counts[k] += 1
+    return found, counts
+
+
+def tail_upper(s, cutoff=5):
+    require(isinstance(s, int) and s >= 0, "width increment must be nonnegative")
+    require(cutoff >= 1, "positive tail cutoff")
+    partial = sum((Q(1, 2 ** (k * (k + 1) // 2 + s * k))
+                   for k in range(1, cutoff + 1)), Q(0))
+    first = Q(1, 2 ** ((cutoff + 1) * (cutoff + 2) // 2 + s * (cutoff + 1)))
+    ratio = Q(1, 2 ** (cutoff + 2 + s))
+    return partial + first / (1 - ratio)
+
+
+def check_sources():
+    package = Path(__file__).resolve().parent
+    root = package.parent.parent
+    sources = json.loads((package / 'SOURCES.json').read_text())
+    checked = 0
+    for source in sources['files']:
+        if source['usage'] == 'input':
+            digest = sha256((root / source['path']).read_bytes()).hexdigest()
+            require(digest == source['sha256'], "source digest: " + source['path'])
+            checked += 1
+    require(checked == 1, "expected one predecessor proof input")
+
+
+def main():
+    check_sources()
+    evidence = {}
+    for n in (1, 2):
+        signed, counts, nonzero, zeros = signed_cliffords(n)
+        residual, other_counts = residual_symplectics(n)
+        require(signed == residual and counts == other_counts, "independent enumerations differ")
+        for k, count in counts.items():
+            require(count <= 2 ** (2 * n * k - k * (k - 1) // 2), "new rank count bound")
+        row = sum((Q(count, 2 ** (k * (2 * n + 2)))
+                   for k, count in nonzero.items() if k), Q(0))
+        require(row < tail_upper(0) < Q(2, 3), "Gram row envelope")
+        evidence[str(n)] = {'symplectic_rank_counts': dict(sorted(counts.items())),
+                            'nonzero_trace_counts': dict(sorted(nonzero.items())),
+                            'zero_trace_classes': zeros, 'row_sum_at_4n_plus_4': str(row)}
+    lower = 1 - tail_upper(0)
+    require(lower > Q(358367, 1000000), "sharper rational constant")
+    require(tail_upper(2) < Q(3, 20) and tail_upper(6) < Q(1, 126), "later width comparison")
+    require(all(tail_upper(s + 1) < tail_upper(s) for s in range(8)), "monotone envelope")
+
+    # Failures exercise actual validation paths, and remain active under python -O.
+    expect_failure(lambda: inverse((0,)), "singular residual accepted")
+    expect_failure(lambda: reconstruct((1, 2), (3, 2), 1, wrong_transpose=True),
+                   "B inverse used in place of B inverse transpose")
+    h = generators(1)[0]
+    bad_table = tuple(v & 3 for v in h[3])
+    expect_failure(lambda: validate_generator(1, (*h[:3], bad_table)), "lost Y sign")
+    expect_failure(lambda: require(nonzero[1] == counts[1], "missing Pauli lift factor"),
+                   "missing Pauli lift multiplicity")
+    expect_failure(lambda: tail_upper(-1), "width below sufficient threshold")
+    print(json.dumps({'status': 'PASS_CLIFFORD_RESIDUAL_COUNT_BOUND',
+                      'scope': 'finite corroboration for n=1,2; all-n proof in PROOF.md',
+                      'enumeration': evidence, 'uniform_row_upper': str(tail_upper(0)),
+                      'uniform_gram_lower': str(lower), 'negative_controls': 5},
+                     indent=2, sort_keys=True))
+
+
+if __name__ == '__main__':
+    main()