[petalas]

Summary

Scoped algebraic proof with finite corroboration; no new κ. For input-independent unbiased random linear response A on k lanes, rank(A)≤R, exponent 0<t<1 and expected rank-power bill B=b R^t:

E A = I,  0 < b ≤ 1
exact minimum worst-input relative MSE = k/(bR) - 1
R=k: the unique optimum is {0 with probability 1-b, I/b with probability b}

The complete stochastic error price rules out a uniformly accurate cheap random sketch inside this declared one-layer relaxation. Intermediate ranks cannot attain the unrestricted-cap concave-price optimum. A normalized tolerance ε gives maximum expected fractional saving ε²/(1+ε²), exactly 1/4097 at ε=2^-6; six is not identified with a selected precision guard.

This contribution was produced by Nick Petalas. The trace/rank inequality and ordinary random coordinate sparsification are classical, with credit to Safaryan, Shulgin and Richtarik's compression uncertainty paper. The contribution is the exact concave rank-power query frontier, random workload size and equality restriction. No predecessor supplier is audited or replayed. Advance CLAIM.

Evidence

• Before: declaring an unbiased shared query says nothing about its fully charged error at a proposed expected budget.
• After: PROOF.md proves the optimum for arbitrary complex dimensions and real 0<t<1, with an explicit attaining finite probability law and a unique full-rank optimizer.
• The standard-library verifier checks complete rational means and every error-covariance entry for 204 laws and 3,308 outcome records; all 19,767 small integer matrices; 8,320 exact tariff comparisons; and 18 controls. Normal and optimized receipts agree in full.
• CPython 3.12.15 local direct times were 2.84 and 2.83 seconds. Both registered checks pass, 6.23 seconds total, with 120-second limits per command. These are check durations, not runtime improvement claims.
• Committed bytes and source history pass for all six files at b7889209ef72f7086d49024cd7c35c1d55ed61d8. The official package export integrity check passes. Normal and optimized Git-free exported replays pass without PATH or PYTHONPATH dependencies and leave exported bytes and modes unchanged.

From the repository root, using the exact local interpreter path:

/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

Elsewhere substitute a CPython 3.12 executable. Expected markers are PASS_RANDOMIZED_QUERY_POWER_FRONTIER, PASS_REGISTERED_RESEARCH_PACKAGE and PASS_RESEARCH_COMMIT_BYTES. Each direct run generates a hash-bound stdout receipt and writes no files. There are no external runtime inputs.

Limitations and unrun obligations

The price rank(A)^t is an explicitly assumed optimistic tariff. Lane rank is not automatically native frame rank. No physical response-to-price bridge, legal caller, acquisition, conversion, random-bit generation, dirty restoration, precision/recovery probability or signed supplier invoice is supplied. Input-dependent matrices, bias, nonlinear decoding, feedback and verification/retry are outside the theorem. The written proof establishes the infinite domain; finite rational checks corroborate it.

No selected cold replay, Lean, Docker, full multiplier, supplier admission or selected-frontier update was run or claimed. Independent human and formal proof-kernel review are unclaimed. The five selected framework assumptions remain.

Open next questions

• Establish one actual common-query supplier's response-rank-to-complete-price bridge. Start with a named additive query layer and every paid rank, conversion, returned helper and restoration charge. A matching physical caller and tariff are missing.
• Give a fully charged biased or input-dependent approximation with certified recovery and retry behavior. Such contracts evade this theorem; no compatible selected precision allowance is supplied here.

Related open work

• Controller income is capped at full calls minus one: even-part rank bound in the p16 Laurent alphabet (scoped negative result; no new kappa) #6114: a deterministic rational Laurent controller income bound. This package studies unbiased approximate random responses and an assumed rank-power tariff; it does not compare its income numbers.

• Prove exact four-query capacity 2 floor(4r/3) (no new κ) #6122: exact four-query capacity for binary square-zero shears. This package has no such finite word or involution premise and does not compare its capacity counts.

• Coupled inverse rounding restores dirty inputs in the PR6026 scalar prefix #6066: logical dirty restoration for stochastic scalar rounding. This package selects a linear response independently of the input and supplies no rounding or restoration implementation.

• Prove the exact power-tariff transition for direct-flow leaves (no new κ) #6125: computes power-tariff asymptotics for a fixed historical direct-flow leaf law. This PR instead prices random linear response rank against worst-input MSE; the probability laws and objectives differ.

• Prove sharp nearest-even Walsh-stage error (no new kappa) #6129: proves deterministic nearest-even Walsh-stage error. This PR has an input-independent stochastic linear response and relative MSE; no numerical error values are compared.

The completion refresh read this account's fourteen other open PRs created since the CLAIM: #6121 through #6133 and #6135. They concern defect guards, deterministic query capacity, centre kernels, sampler services, leaf laws, Gaussian bounds, dyadic gauges, cut58 characters, scalar resynthesis and verifier memory. No additional PR studies this stochastic rank-power frontier or reports a competing value in its contract. No extra computations were run to compare their results.

CI notes

Uncertified by CI. At commit b7889209ef72f7086d49024cd7c35c1d55ed61d8, run 40694205637 failed plan in the onboarding helper tests. The package replay was skipped and did not run in CI. This hosted run certified none of the package's scientific checks. A maintainer re-run is needed after main is fixed.

The failure comes from current main 721c03822c421b7f7fcbb2598993b947c4d88419, the PR6030 κ-admission commit pushed with [skip ci]. It updated the selected record without matching the onboarding documents:

• test_research_current_status.CurrentStatusTests.test_current_section_matches_selected_record expects the literal **0.003125804** in docs/research/current-status.md. The document instead bolds 0.003125804 = 781451/250000000 as one expression, so that exact marker is absent.
• test_research_current_status.CurrentCiNavigationTests.test_current_ci_section_matches_selected_record expects make frontier6030-verify in docs/ci.md, which still describes Raise conditional kappa to 0.00310045 with independent helper splits #5599 and make frontier5599-verify.

The same two failures occur in PR #6120's run 40691776027, confirmed from its failed-job log. The completed checks for this PR were read once. Neither failing document nor the selected record is changed by this contribution. No push, main-document repair or CI re-run was performed for this blocker. The normal/optimized registered replay, committed-byte/source-history and portable-export checks passed locally; those passes remain separate from the missing hosted certification.

Merge danger

Two-way door; blast radius is the isolated six-file research package. No shared implementation, frozen predecessor evidence or selected record changes.

[JosieElliston]

Independent audit at head b7889209: #6142. No error found. It completes the proper-cap equality set: optimal laws are exactly thinned, scaled rank-R projections with E P = (R/k) I. One wording note: the "restrict it to zero" sentence about dirty auxiliary state is better replaced by the ±x averaging argument (README F3 there).