diff --git a/research/randomized-query-power-frontier/PROOF.md b/research/randomized-query-power-frontier/PROOF.md
new file mode 100644
index 0000000000..b56a8c47d6
--- /dev/null
+++ b/research/randomized-query-power-frontier/PROOF.md
@@ -0,0 +1,161 @@
+# The exact stochastic rank-power frontier
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+Claim type: scoped algebraic proof with finite corroboration. No physical
+supplier or new kappa is claimed.
+
+## Contract
+
+Fix integers `1 <= R <= k`, a real exponent `0 < t < 1`, and a budget
+`0 < B <= R^t`. A random complex `k` by `k` matrix `A` is chosen independently
+of the input. Require `E A = I_k`, `rank A <= R` almost surely and a finite
+second moment. Its declared query bill is `E (rank A)^t <= B`, with `0^t=0`.
+Define the worst-input relative mean-square error by
+
+```
+omega(A) = sup_{||x||_2=1} E ||(A-I)x||_2^2.
+```
+
+This is a linear response contract. It permits arbitrary complex encoders
+and decoders. It does not permit selecting the matrix as a function of the
+input, bias, nonlinear decoding or an exact correction supplied for free.
+Write `b=B/R^t` for the normalized expected bill.
+
+For interpretation as a shared-query interface, the target is `k` independent
+copies of a common unitary job `Q`. A fixed outcome with scalar lane response
+`A` has target part `A tensor Q`, so the relative error equals the expression
+above. A rank-`r` response factors through `r` linear channels. The price
+`r^t` is an **assumption of this optimistic relaxation**. Lane rank is not
+automatically a selected supplier's frame rank or recursive-child tariff.
+Any application must prove that bridge. Granting conversion, acquisition,
+randomness, workspace and restoration free does not supply that bridge.
+
+The inequality also applies if an implementation has a larger complete bill
+which dominates `E (rank A)^t`. For a single additive query layer, subadditivity
+gives `sum_j r_j^t >= (sum_j r_j)^t >= (rank A)^t`, provided each query really
+has response rank at most `r_j` and is charged at least `r_j^t` in the same
+normalization. Products, feedback and reused observations need a fresh rank
+argument. An arbitrary dirty auxiliary state cannot defeat the stated lower
+bound: restrict it to zero. No constructive dirty restoration is asserted.
+
+## Sharp theorem
+
+The exact infimum is attained and is
+
+```
+inf omega(A) = k R^(t-1)/B - 1 = k/(b R) - 1.       (1)
+```
+
+In particular, without a proper rank cap, `R=k`,
+
+```
+B >= k^t/(1+omega).
+```
+
+For `0 < t < 1`, equality at any budget in this interval has only the two
+response matrices
+
+```
+A = 0       with probability 1-B/k^t,
+A = (k^t/B) I_k   with probability B/k^t.             (2)
+```
+
+Thus the exact optimizer in this price model either omits the whole job or
+performs a rescaled whole job. Intermediate response ranks cannot attain it.
+This is a statement about expected work and mean-square error, not an
+exact-on-each-run implementation or a bound on successful recovery probability.
+
+### Lower bound
+
+Put `r=rank A`. For any fixed matrix let `P` be the orthogonal projection onto
+its image. Since `P A=A`, Frobenius Cauchy-Schwarz gives the classical inequality
+
+```
+|tr A| = |<P,A>_F| <= sqrt(r) ||A||_F.
+```
+
+It is valid for nonnormal and nonsymmetric matrices. Set both sides to zero
+when `r=0`. Applying Cauchy-Schwarz also over the probability space gives
+
+```
+k^2 = |E tr A|^2 <= (E r) E ||A||_F^2.              (3)
+```
+
+For every integer `0 <= r <= R`,
+
+```
+r <= R^(1-t) r^t,
+```
+
+strictly for `0<r<R`. Consequently `E r <= R^(1-t) B`. Unbiasedness yields
+
+```
+E ||A-I||_F^2 = E ||A||_F^2 - k.
+```
+
+The error covariance `E (A-I)* (A-I)` is positive semidefinite, and its largest
+eigenvalue is at least its trace divided by `k`. Substitution in (3) proves
+`omega >= k/(R^(1-t)B)-1`, which is (1).
+
+### Attainment and equality
+
+With probability `b` choose a uniformly random `R`-subset `S` of the `k`
+coordinates, let `P_S` be its coordinate projection, and set
+`A=k P_S/(bR)`. With probability `1-b` set `A=0`. Directly,
+
+```
+E A = I,     E (rank A)^t = b R^t = B,
+E (A-I)* (A-I) = (k/(bR)-1) I.
+```
+
+This finite law attains the worst-input bound, not only an average over
+inputs. More generally one may use any distribution of rank-`R` orthogonal
+projections satisfying `E P=(R/k)I` on the nonzero branch. Uniform coordinate
+sparsification and its usual `k/R-1` variance at `b=1` are classical; see
+Safaryan, Shulgin and Richtarik's [compression uncertainty paper](https://arxiv.org/abs/2002.08958).
+No priority is claimed for that construction or the trace inequality. The
+new interface calculation includes the concave rank-power bill, random zero
+branch, exact worst-input optimum and its equality restriction.
+
+To prove (2), equality in (1) forces equality in every intervening bound.
+In particular `E r=R^(1-t) E r^t=R^(1-t)B`. Strictness at intermediate ranks
+forces `r` to be either zero or `R`. When `R=k`, a nonzero `A` has image the
+whole space, so equality in the fixed-matrix trace inequality forces
+`A=alpha I`. Equality in probabilistic Cauchy-Schwarz forces the same scalar
+`alpha` on every nonzero branch, with common nonnegative trace phase.
+The cost fixes its probability to `b=B/k^t`; unbiasedness then gives
+`alpha=1/b`. Conversely (2) attains every bound. This includes `b=1`.
+
+## Consequences and boundary of the obstruction
+
+For a normalized tolerance `omega <= epsilon^2`, the unrestricted-cap
+interface cannot save more than the fraction `epsilon^2/(1+epsilon^2)` of
+the deterministic rank-power bill. At `epsilon=2^-g`, this is exactly
+`1/(4^g+1)`. This is a normalized relative MSE tolerance; `g` has not been
+identified with any selected word's precision guard. For example `g=6`
+allows at most `1/4097` expected fractional saving. Zero variance permits
+no saving. The explicit optimum still has a nonzero probability of returning
+zero when the budget is below the full bill.
+
+With a hard proper cap `R<k`, even the maximum allowed bill leaves the
+strict error floor `k/R-1`. Independent repetition reduces variance but pays
+every repetition; it does not supply a free refinement of (1).
+
+The result rejects cheap, uniformly accurate **input-independent linear**
+random compression under the stated tariff. It does not exclude adaptive or
+biased approximations, low-dimensional promised inputs, nonlinear methods,
+high-probability verification/retry, or another response-to-cost bridge.
+There is no selected invoice, supplier, compiler or multiplication theorem
+attached to this relaxation. All physical/native costs and the five selected
+framework assumptions remain unresolved.
+
+## Finite verification
+
+`verify.py` computes complete rational means and every error-covariance entry
+for the finite attainers. It also exhausts small integer matrices for (3)'s
+pointwise trace bound, tests equality by literal matrix products, checks the
+power-price comparison by integer powers, and rejects invalid distributions
+and corrupted scales. The written proof establishes arbitrary dimensions,
+complex fields and real `t`; the finite verifier does not establish those
+claims by extrapolation.
diff --git a/research/randomized-query-power-frontier/README.md b/research/randomized-query-power-frontier/README.md
new file mode 100644
index 0000000000..6286ba062f
--- /dev/null
+++ b/research/randomized-query-power-frontier/README.md
@@ -0,0 +1,141 @@
+# Exact error price of unbiased random query compression
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+Scoped algebraic proof with finite corroboration; no new kappa. For an
+input-independent unbiased random linear response on `k` lanes, with hard
+rank cap `R`, the exact worst-input relative mean-square error at expected
+rank-power bill `B=b R^t`, `0<t<1`, `0<b<=1`, is
+
+```
+omega_min = k/(b R) - 1.
+```
+
+Arbitrary complex encoders and decoders do not improve this frontier. Uniform
+coordinate projection, with a random zero branch and the specified rescaling,
+attains it. At `R=k`, the only optimal response law is a lottery between zero
+and `I_k/b`. Every intermediate nonzero response rank is strictly too expensive
+to attain the frontier under the concave tariff.
+
+For unrestricted rank and normalized error tolerance `omega<=epsilon^2`,
+the maximum expected fractional bill saving is exactly
+`epsilon^2/(1+epsilon^2)`. At `epsilon=2^-6` it is `1/4097`. These are relative
+MSE units, with no identification of six with a selected precision guard.
+
+[PROOF.md](PROOF.md) gives the universal proof, attaining finite law and equality
+classification. The trace/rank inequality and ordinary uniform sparsification
+are classical. The contribution is their exact concave rank-power query
+frontier, with random workload size, worst-input error and the full-rank
+optimizer restriction. This is an original changed-interface investigation,
+not a replay or audit of a previous construction. No literature priority is
+claimed for those classical tools. See Safaryan, Shulgin and Richtarik's
+[compression uncertainty paper](https://arxiv.org/abs/2002.08958) for the
+ordinary random-sparsification variance and a different bit-communication
+uncertainty model.
+
+## Connection and limits
+
+The optimistic one-layer interface asks whether `k` independent copies of
+a common unitary job can be replaced by an unbiased low-rank random linear
+sketch. Its scalar lane response is `A`; error for `A tensor Q` against
+`I tensor Q` is exactly the same as error for `A` against `I`.
+
+The declared price `rank(A)^t` is an assumption. Lane rank is not automatically
+a selected recursive frame rank. A physical application must establish a
+response-rank-to-complete-price bridge, or another price which dominates
+this one, with the same normalization. Acquisition, encoding, decoding,
+randomness, dirty restoration and all other charges are granted free here.
+No native implementation, selected caller, signed supplier invoice, recovery
+probability or new exponent is supplied. The exact frontier is an obstruction
+inside this relaxation, not a universal finite-network limit.
+
+Input-dependent matrices, bias, nonlinear decoding, promised input subspaces,
+feedback and verification/retry are outside the theorem. The written proof
+covers complex matrices and real `t`; the executable uses the finite real
+rational domains below. Independent human and formal proof-kernel review are
+unclaimed. No selected scientific replay, Lean or Docker run was performed.
+The five selected framework assumptions remain.
+
+## Evidence and reproduction
+
+From the repository root, using the CPython 3.12 standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/randomized-query-power-frontier/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/randomized-query-power-frontier/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/randomized-query-power-frontier
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/randomized-query-power-frontier --check-source-history
+```
+
+Another CPython 3.12 installation can replace the displayed local path.
+The direct marker is `PASS_RANDOMIZED_QUERY_POWER_FRONTIER`. A run prints
+a generated JSON receipt, including the environment and hashes of all six
+package files. It writes nothing; redirect stdout to an external scratch
+file to retain the receipt. Registered normal and optimized runs have
+120-second limits and retain every explicit check.
+
+The finite checks enumerate:
+
+- 204 attaining probability laws at `k=1..8`, every cap `R=1..k`, and
+  `b` in `{1,1/2,2/3,1/4}`. Coordinate laws and Walsh-conjugated laws for
+  power-of-two `k` have their complete means and every covariance entry
+  checked. Their 3,308 outcome records include the explicit zero record,
+  even when its probability is zero, and repeated matrices across laws.
+- All 19,767 matrices of dimensions one, two and three with entries in
+  `{-1,0,1}`. The trace/rank inequality holds; all 46 nonzero equality
+  matrices also pass the literal scalar-projector identity and symmetry.
+- 8,320 exact integer-power tariff comparisons at `R=1..64`, every positive
+  `r<=R`, and exponents `{1/2,2/3,9/10,499/500}`. Exactly 8,064 are strict.
+  The normalized tolerance formula is checked at every `g=0..16`.
+- 18 control cases, including invalid dimensions, probability sign/sum,
+  rank-cap violations, biased laws, corrupted scaling, omitted thinning
+  noise, confusing mean rank with power price, and every independent
+  average of one through eight Bernoulli whole-job samples.
+
+The universal result follows from the written proof. These finite checks
+corroborate its identities and hypotheses rather than enumerate its infinite
+domain. No predecessor program or scientific census is imported.
+
+## Scope and source record
+
+Base canonical main is `721c03822c421b7f7fcbb2598993b947c4d88419`, priority
+revision 8, selected PR6030. The baseline source-binding orientation passed
+after materializing its omitted sparse inputs. It is not an operator replay.
+The [advance CLAIM](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19241914)
+declares this stochastic contract. [TASK.json](TASK.json) preserves the original
+card and explicitly changes its scope to an optimistic algebraic side result.
+[SOURCES.json](SOURCES.json) binds the catalogue and selected record as historical
+provenance. There are no external runtime inputs or pending Git dependencies.
+
+Live open/account PRs, active Discussions, recent handoffs, merged term searches
+and main's omitted README files were checked before reservation. The overlap
+cache reports complete pagination for 379 open PRs and 5,782 Discussion records,
+but omits 8,278 local note paths from its sparse working-tree scan. Separate
+Git searches covered the proposed object's terms on main. These searches are
+bounded coordination evidence, not a proof of novelty. The deterministic
+multi-bank shear question in #6114 has a different contract and is not
+answered here.
+
+Power of Ten inspection finds no recursion, dynamic code, subprocesses or
+background work. Functions fit within 60 lines. Loops have fixed domains,
+matrices have at most eight rows, and one law has at most 71 outcome records.
+The exhaustive matrix domain is at most `3^9` per dimension. Source-hash reads
+are capped at 256 KiB per file. Python allocates managed objects dynamically,
+a deviation from fixed allocation; the fixed domains bound live mathematical
+state. Revisit those capacities before increasing the domain. Explicit checks
+survive optimized Python, and warnings are errors. No external static analyzer
+or proof assistant is claimed.
+
+## Open next questions
+
+1. Can one actual common-query supplier establish the response-rank-to-price
+   bridge and pay its full caller costs? Start with a named additive layer,
+   its response map and every paid rank and restoration obligation. The
+   physical producer/consumer and matching tariff are missing.
+2. Can bias or input-dependent coding yield a favorable complete cost with
+   certified recovery? Start with one approximation and verification/retry
+   contract, charging every retry and worst-input error. No such recovery
+   proof or selected precision allowance is supplied here.
+
+Structured relevance and blockers are in TASK.json. No further search or
+construction was undertaken after the sharp frontier was obtained.
diff --git a/research/randomized-query-power-frontier/SOURCES.json b/research/randomized-query-power-frontier/SOURCES.json
new file mode 100644
index 0000000000..40f96c767a
--- /dev/null
+++ b/research/randomized-query-power-frontier/SOURCES.json
@@ -0,0 +1,18 @@
+{
+  "schema_version": 1,
+  "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419",
+  "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"
+    }
+  ]
+}
diff --git a/research/randomized-query-power-frontier/TASK.json b/research/randomized-query-power-frontier/TASK.json
new file mode 100644
index 0000000000..21d93359f7
--- /dev/null
+++ b/research/randomized-query-power-frontier/TASK.json
@@ -0,0 +1,90 @@
+{
+  "schema_version": 1,
+  "task_id": "joint-query-controller",
+  "priority_revision": 8,
+  "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419",
+  "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": "changed",
+  "actual_scope": "Sharp expected rank-power bill versus worst-input mean-square error for input-independent unbiased linear query responses, with a hard rank cap; classify the unrestricted-cap optimizer.",
+  "scope_change_reason": "Change deterministic exact query delivery to a stochastic approximate one-layer linear response. This is an original optimistic interface obstruction, not construction or review of a selected supplier.",
+  "bottleneck_link": "Randomly sharing a common query is a possible changed interface. The theorem prices its unavoidable worst-input noise under an explicitly assumed rank-power tariff before spending effort on a physical realization. Lane rank is not identified with selected recursive frame rank.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop at the first sharp budget/error theorem, finite attaining law and equality classification. Do not search for or admit a physical supplier.",
+  "outcome": "negative-result",
+  "evidence": "PROOF.md proves the sharp bound and equality case; verify.py checks exact finite probability laws and failure controls.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Can an actual common-query supplier prove a response-rank-to-complete-price bridge for this relaxation?",
+      "why_it_matters": "Lane rank is not automatically recursive frame rank; the theorem does not yet exclude a selected supplier modification.",
+      "first_step": "Specify one actual additive query layer, its coefficient-response map and every paid rank, conversion, owned-output and restoration charge.",
+      "blocked_by": "No physical producer/consumer or matching tariff is supplied."
+    },
+    {
+      "question": "Can a biased or input-dependent response achieve a favorable complete cost and certified recovery probability?",
+      "why_it_matters": "Those contracts evade the input-independent unbiased hypothesis, so this obstruction does not cover them.",
+      "first_step": "Give one complete changed approximation and verification/retry contract, then charge its worst-input errors and all retries.",
+      "blocked_by": "No recovery proof, charged caller or compatible selected precision allowance is known."
+    }
+  ]
+}
diff --git a/research/randomized-query-power-frontier/VERIFY.json b/research/randomized-query-power-frontier/VERIFY.json
new file mode 100644
index 0000000000..0b5bbc8947
--- /dev/null
+++ b/research/randomized-query-power-frontier/VERIFY.json
@@ -0,0 +1,34 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Complete exact rational means and error covariances for finite coordinate/Walsh attaining laws; exhaustive small integer trace/rank inequality and equality checks; integer-power tariff inequalities; normalized tolerance frontier; invalid-law, scale, rank-cap, bias and independent-repetition controls."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-O",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Same complete domain with explicit exception checks active under optimized Python."
+    }
+  ]
+}
diff --git a/research/randomized-query-power-frontier/verify.py b/research/randomized-query-power-frontier/verify.py
new file mode 100644
index 0000000000..03357cb595
--- /dev/null
+++ b/research/randomized-query-power-frontier/verify.py
@@ -0,0 +1,236 @@
+#!/usr/bin/env python3
+"""Exact finite controls for the stochastic rank-power query frontier.
+
+Produced by Nick Petalas. Apache-2.0.
+"""
+
+from fractions import Fraction as F
+from hashlib import sha256
+from itertools import combinations, product
+from math import comb
+from pathlib import Path
+import json
+import sys
+
+
+def require(condition, message):
+    if not condition:
+        raise ValueError(message)
+
+
+def identity(k):
+    return tuple(tuple(F(i == j) for j in range(k)) for i in range(k))
+
+
+def zero(k):
+    return tuple(tuple(F(0) for _ in range(k)) for _ in range(k))
+
+
+def rank(matrix):
+    """Bounded exact elimination; every caller supplies at most eight rows."""
+    n = len(matrix)
+    require(1 <= n <= 8 and all(len(row) == n for row in matrix), "matrix size")
+    rows = [list(map(F, row)) for row in matrix]
+    pivot = 0
+    for col in range(n):
+        chosen = next((j for j in range(pivot, n) if rows[j][col]), None)
+        if chosen is None:
+            continue
+        rows[pivot], rows[chosen] = rows[chosen], rows[pivot]
+        scale = rows[pivot][col]
+        rows[pivot] = [x / scale for x in rows[pivot]]
+        for j in range(pivot + 1, n):
+            scale = rows[j][col]
+            rows[j] = [x - scale * y for x, y in zip(rows[j], rows[pivot])]
+        pivot += 1
+    return pivot
+
+
+def multiply(a, b):
+    k = len(a)
+    return tuple(tuple(sum(a[i][h] * b[h][j] for h in range(k))
+                       for j in range(k)) for i in range(k))
+
+
+def inspect_law(k, cap, law):
+    """Compute every entry of the mean and error covariance, not sampled x."""
+    require(1 <= cap <= k <= 8, "law dimensions")
+    require(1 <= len(law) <= 71, "law capacity")
+    require(all(isinstance(p, F) and p >= 0 for p, _ in law), "probability")
+    require(sum(p for p, _ in law) == 1, "probability sum")
+    mean = [[F(0) for _ in range(k)] for _ in range(k)]
+    error = [[F(0) for _ in range(k)] for _ in range(k)]
+    mean_rank = F(0)
+    for probability, matrix in law:
+        r = rank(matrix)
+        require(r <= cap, "rank cap")
+        mean_rank += probability * r
+        for i in range(k):
+            for j in range(k):
+                mean[i][j] += probability * matrix[i][j]
+                error[i][j] += probability * sum(
+                    (matrix[h][i] - (h == i)) * (matrix[h][j] - (h == j))
+                    for h in range(k))
+    require(tuple(map(tuple, mean)) == identity(k), "unbiased operator")
+    return tuple(map(tuple, error)), mean_rank
+
+
+def projection_law(k, cap, beta, walsh=False):
+    """Uniform coordinate projectors, optionally in a rational Walsh basis."""
+    require(1 <= cap <= k <= 8 and 0 < beta <= 1, "projection parameters")
+    require(not walsh or k & (k - 1) == 0, "Walsh width")
+    law = [(1 - beta, zero(k))]
+    weight = beta / comb(k, cap)
+    scale = F(k, cap) / beta
+    for subset in combinations(range(k), cap):
+        if walsh:
+            matrix = tuple(tuple(scale * sum(
+                (-1) ** ((i & h).bit_count() + (j & h).bit_count())
+                for h in subset) / k for j in range(k)) for i in range(k))
+        else:
+            matrix = tuple(tuple(scale * (i == j and i in subset)
+                                 for j in range(k)) for i in range(k))
+        law.append((weight, matrix))
+    return law
+
+
+def check_attainers():
+    cases = outcomes = 0
+    examples = []
+    for k in range(1, 9):
+        for cap in range(1, k + 1):
+            for beta in (F(1), F(1, 2), F(2, 3), F(1, 4)):
+                for walsh in ((False, True) if k & (k - 1) == 0 else (False,)):
+                    law = projection_law(k, cap, beta, walsh)
+                    covariance, mean_rank = inspect_law(k, cap, law)
+                    variance = F(k, cap) / beta - 1
+                    expected = tuple(tuple(variance * (i == j) for j in range(k))
+                                     for i in range(k))
+                    require(covariance == expected, "sharp worst-input covariance")
+                    require(mean_rank == beta * cap, "rank charge")
+                    require(all(p == 0 or rank(a) in (0, cap) for p, a in law),
+                            "only endpoint ranks attain the power relaxation")
+                    cases += 1
+                    outcomes += len(law)
+                    if (k, cap, beta, walsh) in ((8, 4, F(1, 2), False),
+                                                 (8, 8, F(2, 3), True)):
+                        examples.append({"k": k, "cap": cap, "beta": str(beta),
+                                         "variance": str(variance)})
+    return {"laws": cases, "outcomes": outcomes, "examples": examples}
+
+
+def check_trace_rank():
+    matrices = equalities = 0
+    for k in range(1, 4):
+        for entries in product((-1, 0, 1), repeat=k * k):
+            a = tuple(tuple(F(entries[i * k + j]) for j in range(k))
+                      for i in range(k))
+            r = rank(a)
+            trace = sum(a[i][i] for i in range(k))
+            norm2 = sum(x * x for row in a for x in row)
+            require(trace * trace <= r * norm2, "trace-rank inequality")
+            if r and trace * trace == r * norm2:
+                scale = trace / r
+                square = multiply(a, a)
+                require(all(a[i][j] == a[j][i] and square[i][j] == scale * a[i][j]
+                            for i in range(k) for j in range(k)),
+                        "equality is a scalar orthogonal projector")
+                equalities += 1
+            matrices += 1
+    return {"matrices": matrices, "nonzero_equalities": equalities}
+
+
+def check_power_and_precision():
+    inequalities = strict = 0
+    for cap in range(1, 65):
+        for r in range(1, cap + 1):
+            for numerator, denominator in ((1, 2), (2, 3), (9, 10), (499, 500)):
+                # ((r/cap)^t >= r/cap)^denominator, exactly over integers.
+                left = r ** numerator * cap ** denominator
+                right = r ** denominator * cap ** numerator
+                require(left >= right and (left == right) == (r == cap),
+                        "strict concave rank-price comparison")
+                inequalities += 1
+                strict += left > right
+    rows = []
+    for guard in range(17):
+        epsilon2 = F(1, 4 ** guard)
+        beta = 1 / (1 + epsilon2)
+        require(1 / beta - 1 == epsilon2, "variance-budget inverse")
+        require(1 - beta == F(1, 4 ** guard + 1), "precision saving fraction")
+        rows.append({"g": guard, "maximum_fractional_saving": str(1 - beta)})
+    return {"power_comparisons": inequalities, "strict": strict,
+            "normalized_tolerances": rows}
+
+
+def expect_rejection(k, cap, law, message):
+    try:
+        inspect_law(k, cap, law)
+    except ValueError as error:
+        require(str(error) == message, "wrong failure reason")
+        return 1
+    raise ValueError("invalid law was accepted: " + message)
+
+
+def check_controls():
+    controls = 0
+    controls += expect_rejection(2, 0, [(F(1), identity(2))], "law dimensions")
+    controls += expect_rejection(9, 1, [(F(1), identity(9))], "law dimensions")
+    controls += expect_rejection(2, 2, [(F(-1), zero(2)), (F(2), identity(2))],
+                                 "probability")
+    controls += expect_rejection(2, 2, [(F(1, 2), identity(2))], "probability sum")
+    controls += expect_rejection(2, 1, [(F(1), identity(2))], "rank cap")
+    controls += expect_rejection(2, 2, [(F(1), zero(2))], "unbiased operator")
+    law = projection_law(2, 1, F(1, 2))
+    damaged = [(p, tuple(tuple(x / 2 for x in row) for row in a)) for p, a in law]
+    controls += expect_rejection(2, 1, damaged, "unbiased operator")
+    biased = [(F(1), ((F(1), F(0)), (F(0), F(0))))]
+    controls += expect_rejection(2, 1, biased, "unbiased operator")
+    covariance, _ = inspect_law(2, 1, law)
+    require(covariance != ((F(1), F(0)), (F(0), F(1))), "omitted thinning noise")
+    controls += 1
+    coordinate = projection_law(2, 1, F(1))
+    lottery = projection_law(2, 2, F(1, 2))
+    covariance1, rank1 = inspect_law(2, 1, coordinate)
+    covariance2, rank2 = inspect_law(2, 2, lottery)
+    require(covariance1 == covariance2 and rank1 == rank2 == 1,
+            "equal mean rank and noise do not fix the power price")
+    # At t=1/2 the normalized prices are sqrt(1/2) and 1/2.
+    require(F(1, 2) ** 2 < F(1, 2), "strict price advantage for the full-rank lottery")
+    controls += 1
+    for copies in range(1, 9):
+        repeated = [(F(comb(copies, j), 2 ** copies),
+                     tuple(tuple(F(2 * j, copies) * (a == b) for b in range(2))
+                           for a in range(2))) for j in range(copies + 1)]
+        covariance, _ = inspect_law(2, 2, repeated)
+        require(covariance == ((F(1, copies), F(0)), (F(0), F(1, copies))),
+                "independent averaging covariance")
+        require(F(copies, 2) >= 1 / (1 + covariance[0][0]), "repeats pay")
+        controls += 1
+    return controls
+
+
+def package_hashes(root):
+    names = ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", "VERIFY.json", "verify.py")
+    hashes = {}
+    for name in names:
+        with (root / name).open("rb") as stream:
+            data = stream.read(262145)
+        require(len(data) <= 262144, "package file capacity")
+        hashes[name] = sha256(data).hexdigest()
+    return hashes
+
+
+def main():
+    require(len(sys.argv) == 1, "no command-line arguments")
+    root = Path(__file__).resolve().parent
+    result = {"status": "PASS_RANDOMIZED_QUERY_POWER_FRONTIER",
+              "attainers": check_attainers(), "trace_rank": check_trace_rank(),
+              "power_and_precision": check_power_and_precision(),
+              "controls": check_controls(), "python": sys.version.split()[0]}
+    result["sha256"] = package_hashes(root)
+    print(json.dumps(result, sort_keys=True, indent=2))
+
+
+if __name__ == "__main__":
+    main()