diff --git a/research/audit-pr6134-query-power-frontier/README.md b/research/audit-pr6134-query-power-frontier/README.md new file mode 100644 index 0000000000..76243b4ad9 --- /dev/null +++ b/research/audit-pr6134-query-power-frontier/README.md @@ -0,0 +1,155 @@ +# Audit of PR6134's stochastic rank-power frontier + +Audit by Josie Elliston with Claude Opus 5.5 (Anthropic) assistance. Apache-2.0. +Claim type: independent proof review with exact finite corroboration. No new +κ, supplier or selected-frontier change. + +Audited: [PR6134](https://github.com/CrocSwap/integer-mult-bounds/pull/6134) +by Nick Petalas, head `b7889209ef72f7086d49024cd7c35c1d55ed61d8`, package +`research/randomized-query-power-frontier/` (hashes in [SOURCES.json](SOURCES.json)). +Base main `721c03822c421b7f7fcbb2598993b947c4d88419`. + +## Verdict + +**No error.** Every step of PROOF.md holds as written for complex matrices, +`1 <= R <= k`, `0 < t < 1` and `0 < B <= R^t`: + +``` +inf omega(A) = k/(bR) - 1, b = B/R^t, +``` + +attained by the stated thinned coordinate law. The `R = k` uniqueness +statement and the saving corollary `epsilon^2/(1+epsilon^2)` (`1/4097` at +`epsilon = 2^-6`) are correct. PR6134's verifier replays `PASS` under +CPython 3.12.14, normal and `-O` (about 7 s each). + +## Step-by-step review + +1. **Pointwise trace bound.** `PA = A` for the orthogonal projection `P` + onto the image, so `tr A = _F`, and `|tr A| <= sqrt(r) ||A||_F` + by Cauchy-Schwarz with `||P||_F = sqrt(r)`. Valid for nonnormal `A`. +2. **Inequality (3).** `k = E tr A`, then `|E tr A| <= E |tr A| <= + E[sqrt(r) ||A||_F] <= sqrt(E r) sqrt(E ||A||_F^2)`. Correct; the finite + second moment makes every term finite. +3. **Price step.** `r <= R^(1-t) r^t` for integer `0 <= r <= R` is + `(r/R)^(1-t) <= 1`, strict for `0 < r < R` when `t < 1`. So + `E r <= R^(1-t) B`. +4. **Error identity.** `E ||A - I||_F^2 = E ||A||_F^2 - 2 Re tr E A + k + = E ||A||_F^2 - k` by unbiasedness. +5. **Worst input.** `omega = lambda_max(C)` for `C = E (A-I)^*(A-I)`, and + `lambda_max(C) >= tr C / k`. Combining: `omega >= k/E r - 1 >= k/(R^(1-t) B) - 1`. + Note that `E r > 0` because `E A = I`. +6. **Attainment.** With probability `b`, `A = (k/(bR)) P_S` for a uniform + `R`-subset `S`: `E A = I`, `E (rank A)^t = b R^t`, `C = (k/(bR) - 1) I`. +7. **Uniqueness at `R = k`.** Equality forces `r` into `{0, k}`, then + `A = alpha I` on each nonzero branch, one common `alpha` (Cauchy-Schwarz + equality fixes `|alpha|`; `|E tr A| = E |tr A|` fixes its phase), and + `alpha = 1/b` with probability `b`. Correct. +8. **Corollary.** `k/(bk) - 1 <= epsilon^2` gives `1 - b <= epsilon^2/(1+epsilon^2)`. + +## Findings + +**F1 (strengthening, proper cap `R < k`).** PROOF.md states the general +attaining family only as a sufficient construction. The converse also holds, +which completes the equality set for every cap: + +> For `R < k`, `omega(A) = k/(bR) - 1` holds exactly for the laws with +> `A = 0` with probability `1 - b` and, otherwise, `A = (k/(bR)) P` for a random +> rank-`R` orthogonal (Hermitian) projection `P` with `E[P | A != 0] = (R/k) I`. + +*Proof.* Equality forces equality in steps 1-5. Step 3 forces `r` into +`{0, R}`, and `E r^t = B` (otherwise step 3 is strict), so `P(r = R) = b`. +Step 1 forces `A = alpha P` with `P` the image projection. Step 2's two +equalities force `|alpha|` and the phase of `tr A = alpha R` to be common, +so `alpha` is common. Then `E A = b alpha E[P | r = R] = I`, and the trace +gives `alpha = k/(bR)` and `E[P | r = R] = (R/k) I`. Conversely, every such law +has `C = b alpha^2 (R/k) I - I = (k/(bR) - 1) I`, so step 5 is an equality too. +At `R = k` the only such `P` is `I`, which recovers (2). ∎ + +So the optimal laws for a proper cap are exactly the rank-`R` projection +designs that are isotropic in mean, scaled and thinned. Coordinate and Walsh +subsets (PR6134's verifier) are two instances; the tetrahedral and +Pythagorean frames checked here are others. + +**F2 (precision, not an error).** Equality in (3) alone does not force one +common rank: a law with one common scale and ranks `1` and `2` attains (3) +exactly (checked at `k = 3`). The endpoint-rank conclusion comes only from +the strict concave price in step 3, which PROOF.md uses correctly. Hence +`t < 1` is essential to the uniqueness statement; at `t = 1` mixed-rank +laws are also optimal. + +**F3 (wording).** PROOF.md says "An arbitrary dirty auxiliary state cannot +defeat the stated lower bound: restrict it to zero." The analyst cannot +restrict an implementation's random auxiliary state. The conclusion still +holds by another route: if the response is `A x + c` with `c` independent of +`x` (and possibly correlated with `A`), unbiasedness at `x = 0` gives +`E c = 0`. Averaging the inputs `x` and `-x` gives +`E ||(A-I)x||^2 + E ||c||^2`, so the worst input is never below the +linear-part error. The verifier exhibits an offset that lowers the error at one +input (`0` instead of `1`) while the opposite input pays `4`. The suggested fix is +to replace that sentence with the `±x` argument. + +**F4 (verifier coverage, not an error).** PR6134's check "only endpoint +ranks attain" runs only on laws that it built with endpoint ranks, so it is +tautological. Its verifier never tests the lower bound on a non-attaining +law. This package adds that coverage for the trace steps (1, 2, 4, 5); see below. + +Remark (not checked beyond the proof sketch): if inputs are promised to lie in +a known `d`-dimensional subspace with `R <= d`, the same argument applied to +`tr(QAQ)` with `Q` the subspace projector gives `d/(bR) - 1`. Coordinate +sparsification inside the subspace attains it. This quantifies one of +PR6134's listed escapes as "replace `k` by `d`", not as a new saving. + +## Independent exact checks + +[verify.py](verify.py) is standard-library Python. It was written from +PROOF.md's statement and imports no code from PR6134. It works over real +rational matrices; the complex case rests on the written proof. + +- **Random unbiased laws.** The verifier builds 2,631 seeded laws as `A_i = M_i M^{-1}` + (`M = sum p_i M_i`, entries in `{-1, 0, 1, 2}`, `k <= 3`, up to three + outcomes). These have oblique, nonsymmetric and mixed-rank outcomes. + On every law, inequality (3) and `tr C/k >= k/E r - 1` hold, and some + basis input `e_i` already has error `C_ii >= k/E r - 1`. The last step + `E r <= R^(1-t) E r^t` is a per-outcome elementary inequality and is not + evaluated (`E r^t` is irrational). Each of the + 1,343 exact equalities has every nonzero outcome equal to `alpha P` with + one common `alpha`. Most are trivial (`A = I` or `k = 1`); four have `k >= 2` + and two distinct nonzero outcomes, and one has mixed ranks (F2). +- **Non-coordinate attainers.** The verifier checks four rank-one frames in `k = 2, 3` + at `b` in `{1, 1/2, 3/7}`, plus a rank-two tetrahedral-complement law at + `b = 2/3`. Each has exactly isotropic `C = (k/(bR) - 1) I`. +- **Necessity controls.** An oblique rank-one idempotent law, an + unequal-scale law and a mixed-rank, mixed-scale law are all strict. + A mixed-rank law with one common scale attains (3) (F2). +- **Auxiliary offsets.** The `±x` identity of F3 is checked exactly. + +``` +python3.12 -I -W error -B research/audit-pr6134-query-power-frontier/verify.py +python3.12 -I -O -W error -B research/audit-pr6134-query-power-frontier/verify.py +``` + +Both commands print `PASS_AUDIT_PR6134` in about 0.3 s. They also pass under +CPython 3.10. + +## Remaining obligations + +These are unchanged from PR6134. The response-rank-to-price bridge to any +actual supplier is unproved, so this relaxation is not attached to any +invoice, compiler or multiplication theorem. Biased, adaptive, nonlinear and +retry-based schemes are outside its contract. This audit covers PR6134's head +above only. + +## Open next questions + +1. Does the frontier survive a bridge that charges `r^t` only up to constants + (`c r^t <= price <= C r^t`)? A real supplier bridge is unlikely to be + exact, so the saving corollary would then become a ratio statement. + First step: rerun step 3 with `E price >= c E r^t` and record the saving + fraction at `epsilon = 2^-g`. Not blocked. + +## Credit + +The theorem, attaining law and corollary are Nick Petalas's (PR6134). The +trace/rank inequality and coordinate sparsification are classical; PR6134 +credits Safaryan, Shulgin and Richtárik for the latter. diff --git a/research/audit-pr6134-query-power-frontier/SOURCES.json b/research/audit-pr6134-query-power-frontier/SOURCES.json new file mode 100644 index 0000000000..4e9bcc7f0d --- /dev/null +++ b/research/audit-pr6134-query-power-frontier/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419", + "audited_pr": { + "number": 6134, + "head": "b7889209ef72f7086d49024cd7c35c1d55ed61d8", + "author": "petalas (Nick Petalas)", + "package": "research/randomized-query-power-frontier/" + }, + "files": [ + { + "path": "research/randomized-query-power-frontier/PROOF.md", + "usage": "audited (PR6134 head, not on main)", + "git_blob": "b56a8c47d6d18a49a6d118e3a03ec4fe276f9b6d", + "sha256": "5cc17c5e2fec67c88ed382d4dadd5e81b14dcd709f6de1da3877b1fdff6743c3" + }, + { + "path": "research/randomized-query-power-frontier/README.md", + "usage": "audited (PR6134 head, not on main)", + "git_blob": "6286ba062f9d2b1504a64693efcf30649e8c8e06", + "sha256": "0ca6dca4727bdf3a96ed8459beba04392816349ca363a274bf0c457326ad673b" + }, + { + "path": "research/randomized-query-power-frontier/verify.py", + "usage": "replayed (PR6134 head, not on main); not imported", + "git_blob": "03357cb59531ca0564755b80520e257efa5e5341", + "sha256": "8898b3779d059a345a00eeabc68bf076fdde4e32e56612c87a62787f578e6322" + } + ] +} diff --git a/research/audit-pr6134-query-power-frontier/TASK.json b/research/audit-pr6134-query-power-frontier/TASK.json new file mode 100644 index 0000000000..2f0cd43c0f --- /dev/null +++ b/research/audit-pr6134-query-power-frontier/TASK.json @@ -0,0 +1,84 @@ +{ + "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": "Independent adversarial audit of open PR #6134 (head b7889209ef72f7086d49024cd7c35c1d55ed61d8): the exact stochastic rank-power frontier inf omega = k/(bR) - 1 for unbiased input-independent random linear responses with rank <= R and expected bill E(rank A)^t <= B = b R^t, its R = k uniqueness statement and its epsilon^2/(1+epsilon^2) saving corollary.", + "scope_change_reason": "PR #6134 already changed this card's scope to an optimistic algebraic side result; a fresh, unreviewed proof is most useful checked independently before anyone cites it as an obstruction.", + "bottleneck_link": "Side result only: confirms the relaxation's lower bound and completes its equality set; no supplier, invoice, tariff bridge or kappa changes.", + "budget_minutes": 30, + "stop_rule": "Stop after a step-by-step proof review, an independent exact engine on laws outside #6134's attaining families, and a written converse for the proper-cap equality case; report gaps rather than repairing #6134.", + "outcome": "completed", + "evidence": "PROOF.md reviewed step by step: no error. #6134 verify.py replays PASS (normal and -O, CPython 3.12.14). Own verify.py (no #6134 code imported): inequality (3) and trace(C)/k >= k/E r - 1 on 2631 seeded random unbiased laws A_i = M_i M^-1; every exact equality has the classified shape; 13 non-coordinate attainers; oblique/unequal-scale/mixed-rank controls strict; mixed ranks with one common scale attain (3), so t < 1 is what forces endpoint ranks; +/- x averaging bounds auxiliary offsets.", + "author": "Josie Elliston with Claude Opus 5.5 (Anthropic) assistance", + "ai_assistance": "Claude Opus 5.5 (Anthropic) wrote the review and verifier under Josie Elliston's donated session; no code from #6134 is imported.", + "open_questions": [ + { + "question": "Does the frontier survive a rank-to-price bridge that charges r^t per query only up to a constant (c r^t <= price <= C r^t)?", + "why_it_matters": "Any actual supplier bridge (#6134 open question 1) is unlikely to be exact; the saving corollary then degrades to a ratio statement that should be stated before citing it.", + "first_step": "Repeat the lower bound with E price >= c E r^t and record the resulting saving fraction at epsilon = 2^-g.", + "blocked_by": "none" + } + ] +} diff --git a/research/audit-pr6134-query-power-frontier/VERIFY.json b/research/audit-pr6134-query-power-frontier/VERIFY.json new file mode 100644 index 0000000000..8d72cd789e --- /dev/null +++ b/research/audit-pr6134-query-power-frontier/VERIFY.json @@ -0,0 +1,19 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": ["{python}", "-I", "-W", "error", "-B", "{package}/verify.py"], + "timeout_seconds": 60, + "checks": "Exact rational checks: inequality (3) and the trace bound on 2631 seeded random unbiased laws with oblique, nonsymmetric and mixed-rank outcomes, with every equality classified; 13 non-coordinate attaining laws (rank one and two, k=2,3); necessity controls; the +/- x auxiliary-offset argument." + }, + { + "argv": ["{python}", "-I", "-O", "-W", "error", "-B", "{package}/verify.py"], + "timeout_seconds": 60, + "checks": "The same checks with assertions disabled (the verifier uses explicit raises)." + } + ] +} diff --git a/research/audit-pr6134-query-power-frontier/verify.py b/research/audit-pr6134-query-power-frontier/verify.py new file mode 100644 index 0000000000..707915fbda --- /dev/null +++ b/research/audit-pr6134-query-power-frontier/verify.py @@ -0,0 +1,312 @@ +#!/usr/bin/env python3 +"""Independent exact checks for the PR6134 stochastic rank-power frontier. + +Audit by JosieElliston's session 52 (Claude). Apache-2.0. Standard library only. +Written from PR6134's PROOF.md statement, without importing its verify.py. + +Checks, all in exact rational arithmetic over real matrices: + +1. Inequality (3) of PR6134, k^2 <= E[rank A] * E||A||_F^2, on seeded random + unbiased finite laws built as A_i = M_i M^{-1} (M = sum p_i M_i), which + have arbitrary nonsymmetric, oblique and mixed-rank outcomes. The + resulting lower bound trace(C)/k >= k/E[rank] - 1 on the error covariance C + is checked, and every exact equality is tested against the classification + proved in AUDIT.md (every nonzero outcome is alpha * P with one common + alpha and P an orthogonal projection; ranks may differ in (3) alone, and + the strict concave price is what forces one common rank R in (1)). +2. Attaining laws with non-coordinate projections (not covered by PR6134's + coordinate and Walsh families), in k = 2, 3, with a zero branch. +3. Necessity controls: equal-cost laws that violate one equality condition + (oblique idempotent, mixed endpoint scale, mixed ranks) are strictly above + the bound. +4. The auxiliary-offset remark: an affine offset c with E c = 0 can lower the + error at one input, but the +/- x average never goes below the linear part. +""" +from fractions import Fraction as F +from itertools import product +import json +import random +import sys + + +def require(cond, msg): + if not cond: + raise ValueError(msg) + + +def mat_mul(a, b): + n, m, p = len(a), len(b), len(b[0]) + return [[sum(a[i][h] * b[h][j] for h in range(m)) for j in range(p)] + for i in range(n)] + + +def transpose(a): + return [list(r) for r in zip(*a)] + + +def eye(k): + return [[F(int(i == j)) for j in range(k)] for i in range(k)] + + +def rank(a): + rows = [list(r) for r in a] + n, m = len(rows), len(rows[0]) + piv = 0 + for col in range(m): + sel = next((j for j in range(piv, n) if rows[j][col] != 0), None) + if sel is None: + continue + rows[piv], rows[sel] = rows[sel], rows[piv] + for j in range(n): + if j != piv and rows[j][col] != 0: + s = rows[j][col] / rows[piv][col] + rows[j] = [x - s * y for x, y in zip(rows[j], rows[piv])] + piv += 1 + return piv + + +def inverse(a): + k = len(a) + aug = [list(a[i]) + eye(k)[i] for i in range(k)] + for col in range(k): + sel = next((j for j in range(col, k) if aug[j][col] != 0), None) + if sel is None: + return None + aug[col], aug[sel] = aug[sel], aug[col] + s = aug[col][col] + aug[col] = [x / s for x in aug[col]] + for j in range(k): + if j != col and aug[j][col] != 0: + t = aug[j][col] + aug[j] = [x - t * y for x, y in zip(aug[j], aug[col])] + return [row[k:] for row in aug] + + +def stats(law): + """Return (mean, error covariance C = E (A-I)^T (A-I), E rank, E||A||^2).""" + k = len(law[0][1]) + mean = [[F(0)] * k for _ in range(k)] + cov = [[F(0)] * k for _ in range(k)] + er = F(0) + efro = F(0) + for p, a in law: + d = [[a[i][j] - int(i == j) for j in range(k)] for i in range(k)] + dd = mat_mul(transpose(d), d) + for i in range(k): + for j in range(k): + mean[i][j] += p * a[i][j] + cov[i][j] += p * dd[i][j] + er += p * rank(a) + efro += p * sum(x * x for r in a for x in r) + return mean, cov, er, efro + + +def is_scaled_orth_projection(a): + """a = alpha * P with P symmetric idempotent; returns (alpha, rank) or None.""" + r = rank(a) + if r == 0: + return (F(0), 0) + if any(a[i][j] != a[j][i] for i in range(len(a)) for j in range(len(a))): + return None + alpha = sum(a[i][i] for i in range(len(a))) / r + if alpha == 0: + return None + sq = mat_mul(a, a) + if any(sq[i][j] != alpha * a[i][j] for i in range(len(a)) for j in range(len(a))): + return None + return (alpha, r) + + +def classify_equality(law, common_rank=False): + """Equality in (3): nonzero outcomes are alpha * P with one common alpha. + + Ranks may differ in (3) alone; common_rank=True adds the endpoint-rank + condition that the strict concave price r <= R^(1-t) r^t forces in (1). + """ + shapes = set() + for p, a in law: + if p == 0: + continue + s = is_scaled_orth_projection(a) + if s is None: + return False + if s[1]: + shapes.add(s if common_rank else s[0]) + return len(shapes) == 1 + + +def bound_gap(law): + """Return (k^2 vs E r * E||A||^2 slack, trace(C)/k - (k/E r - 1)).""" + k = len(law[0][1]) + mean, cov, er, efro = stats(law) + require(mean == eye(k), "unbiased") + tr = sum(cov[i][i] for i in range(k)) + require(tr == efro - k, "E||A-I||^2 = E||A||^2 - k") + return er * efro - k * k, tr / k - (F(k) / er - 1), cov + + +def check_random(seed=6134, trials=4000): + rng = random.Random(seed) + tested = equalities = mixed_rank_equalities = nontrivial = 0 + for _ in range(trials): + k = rng.choice((1, 2, 3)) + m = rng.choice((1, 2, 3)) + ms = [[[F(rng.choice((-1, 0, 0, 1, 2))) for _ in range(k)] for _ in range(k)] + for _ in range(m)] + ws = [rng.randint(0, 3) for _ in range(m)] + if sum(ws) == 0: + continue + ps = [F(w, sum(ws)) for w in ws] + mean = [[sum(p * x[i][j] for p, x in zip(ps, ms)) for j in range(k)] + for i in range(k)] + inv = inverse(mean) + if inv is None: + continue + law = [(p, mat_mul(x, inv)) for p, x in zip(ps, ms)] + slack, gap, cov = bound_gap(law) + require(slack >= 0, "inequality (3)") + require(gap >= 0, "trace(C)/k >= k/E r - 1") + # A literal input e_i realizes error C_ii, so omega >= max_i C_ii. + er = stats(law)[2] + require(max(cov[i][i] for i in range(k)) >= F(k) / er - 1, + "an actual basis input meets the bound") + if slack == 0: + require(gap == 0, "equality propagates") + require(classify_equality(law), "equality classification") + equalities += 1 + mixed_rank_equalities += not classify_equality(law, True) + nonzero = {tuple(map(tuple, a)) for p, a in law if p and rank(a)} + nontrivial += k >= 2 and len(nonzero) >= 2 + tested += 1 + return {"laws": tested, "exact_equalities": equalities, + "mixed_rank_equalities_in_3": mixed_rank_equalities, + "equalities_k2plus_two_distinct_nonzero_outcomes": nontrivial} + + +def proj(u): + n = sum(x * x for x in u) + return [[F(x * y, n) for y in u] for x in u] + + +def scaled(a, s): + return [[s * x for x in r] for r in a] + + +def zero(k): + return [[F(0)] * k for _ in range(k)] + + +def frame_law(vectors, beta): + """Rank-one frame with E P = I/k on the nonzero branch, scaled k/beta.""" + k = len(vectors[0]) + w = beta / len(vectors) + law = [(1 - beta, zero(k))] + law += [(w, scaled(proj(u), F(k) / beta)) for u in vectors] + return law + + +FRAMES = { + "k2_hadamard_axis": [(1, 1), (1, -1)], + "k2_axis_plus_diagonal": [(1, 0), (0, 1), (1, 1), (1, -1)], + "k3_tetrahedral": [(1, 1, 1), (1, -1, -1), (-1, 1, -1), (-1, -1, 1)], + "k3_pythagorean": [(3, 4, 0), (4, -3, 0), (0, 0, 5)], +} + + +def check_attainers(): + rows = [] + for name, vecs in FRAMES.items(): + for beta in (F(1), F(1, 2), F(3, 7)): + law = frame_law(vecs, beta) + k = len(vecs[0]) + slack, gap, cov = bound_gap(law) + target = F(k) / beta - 1 + require(slack == 0 and gap == 0, "attains (3)") + require(cov == scaled(eye(k), target), "isotropic covariance: omega = trace/k") + require(classify_equality(law, True), "attainer has the classified shape") + rows.append(name + "@" + str(beta)) + # Rank-two complement projections in k = 3 (R = 2): I - u u^T / |u|^2. + vecs = FRAMES["k3_tetrahedral"] + beta = F(2, 3) + law = [(1 - beta, zero(3))] + law += [(beta / 4, scaled([[int(i == j) - x for j, x in enumerate(r)] + for i, r in enumerate(proj(u))], F(3, 2) / beta)) + for u in vecs] + slack, gap, cov = bound_gap(law) + require(slack == 0 and gap == 0 and classify_equality(law, True), "rank-two attainer") + require(cov == scaled(eye(3), F(3) / (beta * 2) - 1), "rank-two covariance") + rows.append("k3_R2_tetrahedral_complement@2/3") + return rows + + +def check_necessity_controls(): + out = {} + # Oblique idempotent of rank one in k = 2 with E A = I and E rank = 1: + # E = [[1, 1], [0, 0]] and F = [[0, -1], [0, 1]] (both idempotent, E + F = I). + e = [[F(1), F(1)], [F(0), F(0)]] + f = [[F(0), F(-1)], [F(0), F(1)]] + law = [(F(1, 2), scaled(e, 2)), (F(1, 2), scaled(f, 2))] + slack, gap, _ = bound_gap(law) + require(slack > 0 and gap > 0 and not classify_equality(law), "oblique is strict") + out["oblique_rank1_k2_trace_gap"] = str(gap) + # Unequal scales on two orthogonal rank-one branches (still unbiased). + p1, p2 = proj((1, 0)), proj((0, 1)) + law = [(F(1, 3), scaled(p1, 3)), (F(2, 3), scaled(p2, F(3, 2)))] + slack, gap, _ = bound_gap(law) + require(slack > 0 and not classify_equality(law), "unequal scale is strict") + out["unequal_scale_k2_slack"] = str(slack) + # Mixed ranks (rank 2 at scale 1, rank 1 at scale 2): strict in (3). + law2 = [(F(1, 2), eye(2)), (F(1, 4), scaled(p1, 2)), (F(1, 4), scaled(p2, 2))] + slack, gap, _ = bound_gap(law2) + require(slack > 0, "mixed ranks with different scales are strict in (3)") + out["mixed_rank_k2_slack"] = str(slack) + # Mixed ranks with one common alpha attain (3) exactly (k = 3, ranks 1, 2): + # (3) alone does not force a common rank. For 0 < t < 1, R = 2 this law has + # E r^t = (1 + 2^t)/2 and (1) gives 3 * 2^t/(1 + 2^t) - 1 < 1 = omega, + # strict because 2^t < 2; at t = 1 it would attain. + d1 = [[F(0)] * 3 for _ in range(3)] + d1[1][1] = F(2) + d2 = [[F(0)] * 3 for _ in range(3)] + d2[0][0] = d2[2][2] = F(2) + law = [(F(1, 2), d1), (F(1, 2), d2)] + slack, gap, cov = bound_gap(law) + require(slack == 0 and gap == 0 and cov == eye(3), "mixed-rank equality in (3)") + require(classify_equality(law) and not classify_equality(law, True), + "common alpha, two ranks") + out["mixed_rank_common_alpha_k3_attains_3"] = True + return out + + +def check_aux_offset(): + """Output A x + c, E A = I, E c = 0. Cross terms can help at one x only.""" + # k = 1: A in {0, 2} each w.p. 1/2; c = +1 when A = 2, -1 when A = 0. + law = [(F(1, 2), F(2), F(1)), (F(1, 2), F(0), F(-1))] + require(sum(p * a for p, a, _ in law) == 1 and sum(p * c for p, _, c in law) == 0, + "unbiased affine response") + + def err(x): + return sum(p * ((a - 1) * x + c) ** 2 for p, a, c in law) + + lin = sum(p * (a - 1) ** 2 for p, a, _ in law) + require(err(F(-1)) < lin, "offset lowers error at x = -1") + require(max(err(F(1)), err(F(-1))) >= lin, "worst of +/- x is not lowered") + require((err(F(1)) + err(F(-1))) / 2 == lin + sum(p * c * c for p, _, c in law), + "+/- x average = linear error + E|c|^2") + return {"err_minus1": str(err(F(-1))), "err_plus1": str(err(F(1))), + "linear": str(lin)} + + +def main(): + result = { + "random_unbiased_laws": check_random(), + "non_coordinate_attainers": check_attainers(), + "necessity_controls": check_necessity_controls(), + "aux_offset": check_aux_offset(), + "status": "PASS_AUDIT_PR6134", + } + json.dump(result, sys.stdout, indent=1) + sys.stdout.write("\n") + + +if __name__ == "__main__": + main()