diff --git a/research/block3-hook-error-spectrum/PROOF.md b/research/block3-hook-error-spectrum/PROOF.md new file mode 100644 index 0000000000..b482fd7c82 --- /dev/null +++ b/research/block3-hook-error-spectrum/PROOF.md @@ -0,0 +1,150 @@ +# The block-three hook has a nonzero error gap + +This scoped proof was produced by Nick Petalas. Apache-2.0. +Independent human and formal proof-kernel review are unclaimed. + +## 1. Space and predecessor premise + +Let V=C^8 with its standard orthonormal basis indexed by F_2^3. At +digit width five, restrict V^(tensor 5) to the isometrically embedded space + + H = V tensor exterior^4 V. + +Exterior basis vectors are normalized antisymmetrizations. Thus H has the +orthonormal basis (x,T), where T is an increasing four-subset of {0,...,7}. +Let N be the coordinate subspace with x in T. Both N and its orthogonal +complement have dimension 280. Write P for the orthogonal projection onto N. +For a single-column matrix g, let rho(g)=g tensor exterior^4(g). + +Jacob Alan Sussman's [PR #4628, PROOF sections 1 and 2](https://github.com/CrocSwap/integer-mult-bounds/blob/ee4fd87f064017c23e5a86fc1dcfe0a5237caed3/research/complex-small-m-lower-bounds/PROOF.md) +supplies the hook construction and the paid-call bound + + rank((I-P) rho(C_v) P) <= 80, v != 0, + C_v = ((1+i)/2) I + ((1-i)/2) X_v. + +That theorem is a cited premise, not a replay target of this package. +Every columnwise monomial map preserves N. Arbitrary linear mixing among +registers, including singular mixing, also preserves the direct sum of their +N spaces. The target on one array is K=C_(e_0) C_(e_1) C_(e_2). + +## 2. The new exact spectrum + +Define L=(I-P) rho(K)|N. Its squared singular values, with multiplicities, are + + 0:56, 1/8:48, 5/8:112, 1:64. (1) + +Here is an exact finite certificate for (1), generated directly from the +matrix formula. Let h[y,x]=(-1)^popcount(x AND y), so F=h/sqrt(8) is the +normalized eight-point Walsh matrix. Put D_0=diag(1,-i). The two-point +identity C=e^(i*pi/4) D_0 F_2 D_0 gives + + K = e^(3i*pi/4) D F D, D[x,x]=(-i)^popcount(x). + +Both rho(D) factors are diagonal unitary and preserve N and N-perp. +Consequently L has the same singular values as (I-P)rho(F)|N. + +In the indicated exterior bases the latter matrix has entries + + h[y,x] det(h[S,T]) / sqrt(32768), + x in T, y not in S, |T|=|S|=4. (2) + +Indeed the first tensor factor contributes 1/sqrt(8), and the four-by-four +minor contributes 1/64. Let D_num be the integer numerator in (2). +The verifier constructs all 78,400 entries using the 24-term determinant +formula. Every entry of D_num^t D_num is divisible by 4096. Define + + A = D_num^t D_num / 4096 = 8 L^* L, + +where the second equality is up to the harmless diagonal unitary basis +change just described. The verifier checks the exact integer identities + + A(A-I)(A-5I)(A-8I) = 0, + (tr I, tr A, tr A^2, tr A^3) = (280,1120,6944,46816). (3) + +A is real symmetric. The first identity confines its eigenvalues to +{0,1,5,8}. Their multiplicities solve the four Vandermonde equations +supplied by the traces. The unique solution is (56,48,112,64), proving (1). +This is a computer-assisted finite spectral proof. Floating eigensolvers +and predecessor rank certificates are not used by the verifier. + +## 3. From spectrum to approximate completed outputs + +Consider any finite linear program with R registers, W designated inputs, +zero initial scratch, and W distinct output registers. It may use arbitrary +complex scalar mixing and columnwise monomial free letters. Each paid letter +is a C_v call. The program can depend on width; only its width-five instance +is needed here. Let M be its joint map from the W data inputs to the W +completed outputs at that width, and suppose it uses s paid calls. + +Restrict every data input to N. At an intermediate cut let B be the map +from N^W to the quotient by N in all R registers. Initially rank B=0. +Free steps cannot increase rank B. For a paid letter on register r, +decompose its old content into its N and N-perp components. The image of +the old quotient components has dimension at most rank B. The new leakage +from the N component in register r has dimension at most 80 by section 1. +Subadditivity therefore gives rank B_new <= rank B_old + 80. Projection to +the completed output registers cannot increase rank. Hence + + rank((I-P)^W M|N^W) <= 80s. (4) + +The intended target leakage is L_W=diag(L,...,L), W copies. Compression +by orthogonal projections and restriction to a subspace do not increase +operator norm. Thus + + ||M - diag(K^(tensor 5),...,K^(tensor 5))|| + >= ||(I-P)^W M|N^W - L_W||. (5) + +The isometric exterior embedding makes the target restriction rho(K). +For any rank-at-most-k map Q, its kernel meets the space spanned by the +first k+1 right singular vectors of L_W. A unit vector in that intersection +shows ||L_W-Q|| >= sigma_(k+1)(L_W). Truncating the singular expansion +attains equality among unrestricted rank-at-most-k linear maps. + +Combining (1), (4) and (5), the squared joint operator error is at least + + 1 if 80s < 64W, + 5/8 if 64W <= 80s < 176W, + 1/8 if 176W <= 80s < 224W, + 0 if 224W <= 80s. (6) + +The endpoints in (6) are inclusive on the left. In particular, error +strictly below 1/sqrt(8) requires s >= ceil(14W/5). Five targets with +thirteen calls have error at least 1/sqrt(8). Fourteen calls merely remove +this rank obstruction; they are not constructed here. + +The whole piecewise bound is sharp for the rank relaxation. No optimal +approximate circuit, or attainment within the paid-call game, is asserted. +The theorem uses joint operator error, not a separate error bound for each +input/output block. It concerns exactly linear programs. A nonlinear +rounding process can inject new leakage and needs a separate argument. + +## 4. Verification scope and code bounds + +The standard-library verifier regenerates (2), checks all entries of (3), +and checks the multiplicity equations. It rejects two explicitly changed +Gram diagonals and four invalid rank-budget inputs. An explicit ordered +list of squared singular values checks the rank/error function for every +rank budget at W=1,...,20, including every endpoint. W=5,s=13 and s=14 +are separate obstruction/relaxation controls. These finite controls support +the implementation; section 3 proves the statement for arbitrary W. + +All matrix dimensions are fixed at 280. Determinants use 24 permutations, +Gram products use at most 280 terms per entry, and matrix products have at +most 280^3 scalar updates. Functions stay below 60 physical lines. Checks +use explicit exceptions and remain active with Python optimization enabled. +There is no recursion, dynamic code execution or subprocess in the verifier. + +Power-of-Ten rule 3 has a Python-runtime deviation: integer arithmetic and +tuples allocate during verification. At most a fixed number of 280-square +matrices is live; the control list has at most 5,600 entries. No size is +read from untrusted input, and the registered process has a 120-second cap. +The workload bounds and normal/optimized replays are the compensating +controls. A fixed-capacity numeric implementation would be needed only if +this certificate were moved to a runtime that prohibits allocation. + +The external predecessor theorem is cited at an exact public commit. It +is not imported, vendored, checked by this verifier or represented as a +locally available source-history pin. The retained main-tree prefix README +is provenance for the hook conventions, not a replay dependency. No Lean, +native supplier, compiler, physical precision or multiplication theorem is +verified by this package. diff --git a/research/block3-hook-error-spectrum/README.md b/research/block3-hook-error-spectrum/README.md new file mode 100644 index 0000000000..8e17e205f6 --- /dev/null +++ b/research/block3-hook-error-spectrum/README.md @@ -0,0 +1,109 @@ +# Exact block-three hook spectrum and an operator-error gap + +This contribution was produced by Nick Petalas. Apache-2.0. +Independent human and formal proof-kernel review are unclaimed. + +The block-three hook leakage has squared singular values +`0:56, 1/8:48, 5/8:112, 1:64`, where each suffix is a multiplicity. +This new finite spectral certificate strengthens the use of Jacob Alan +Sussman's exact kept-subspace obstruction to approximate completed outputs. +In its linear, columnwise model, joint operator error strictly below +`1/sqrt(8)` still requires at least `ceil(14W/5)` paid calls for W targets. +Five targets with thirteen calls therefore have error at least `1/sqrt(8)`. + +The claim type is a **scoped proof**, supported by an exact finite spectral +certificate. It is not a new kappa, supplier construction, optimal +approximate circuit, or complete multiplication theorem. + +## Result and exact evidence + +At digit width five let `H=V tensor exterior^4 V`, `V=C^8`, and let N be +the 280-dimensional coordinate hook `span{(x,T): x in T, |T|=4}`. +For target `K=C_(e_0) C_(e_1) C_(e_2)`, set +`L=(I-P_N) (K tensor exterior^4 K)|N`. +The [proof](PROOF.md) gives the exact matrix formula and the argument +for arbitrary W, with zero scratch and arbitrary complex register mixing. +Any program allowing arbitrary dirty scratch is also subject to this bound +on its zero-scratch restriction, if that restriction obeys the stated error +contract. + +The verifier constructs the Walsh-equivalent leakage as `D/sqrt(32768)`, +then forms the integer Gram matrix `A=D^t D/4096`. It proves + +```text +A(A-I)(A-5I)(A-8I) = 0 +tr(A^0), tr(A^1), tr(A^2), tr(A^3) = 280, 1120, 6944, 46816 +``` + +These identities determine every spectral multiplicity exactly. No +floating eigensolver, rank census from a predecessor, or external library +is used by the registered verifier. Its output includes SHA256 hashes of +all six package files, computed at execution time. + +More generally, the squared joint operator error is bounded below by +`1`, `5/8`, `1/8`, or `0` as the rank budget `80s` lies respectively in +`[0,64W)`, `[64W,176W)`, `[176W,224W)`, or `[224W,infinity)`. +These values are exact for the unrestricted rank approximation relaxation. +Their attainment by legal circuits is not claimed. + +## Reproduction + +From the repository root, with CPython 3.12 and its standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/block3-hook-error-spectrum/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -O -B research/block3-hook-error-spectrum/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/block3-hook-error-spectrum +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/block3-hook-error-spectrum --check-source-history +``` + +Another CPython 3.12 executable may replace the local interpreter path. +Expected verifier status is `PASS_BLOCK3_HOOK_ERROR_SPECTRUM`, with moments +`[280,1120,6944,46816]` and six rejected controls. The controls include two +changed Gram diagonals, four invalid rank inputs, every rank endpoint for +W=1,...,20, and the five-target thirteen/fourteen-call boundary. +All replay output belongs outside the checkout. The verifier writes no files. + +## Scope and predecessor credit + +Credit Jacob Alan Sussman for the hook and kept-subspace call cap in +[PR #4628](https://github.com/CrocSwap/integer-mult-bounds/pull/4628), exact +head `ee4fd87f064017c23e5a86fc1dcfe0a5237caed3`; eumemic for the earlier +kept-subspace certificate method; and Swapnil Jain for the retained P1/P2 +lineage. Lee-phys's retained +[two-image prefix](../complex-two-image-hook-prefix/README.md), PR #4688, +records the same width-five hook conventions. No predecessor computation +is replayed here. The new contribution is the exact spectrum and its +quantitative operator-error consequence. + +The external #4628 theorem is a cited mathematical premise. Its exact +public source URL is in the proof; this package's source-history preflight +does not certify that external theorem. SOURCES.json pins the main-tree +convention reference as provenance only. The verifier has no external inputs. + +The independent-moment card is changed from auditing a paid ledger to a new +approximation obstruction for a small complex unit. This is a side result +about tolerance in a fixed model. It does not affect the selected result. +The complete new family budget is only the rank bound `80s`; it is not a +physical cost invoice. Native lowering, restoration cost, routing, compiler, +stock and finite-precision execution remain outside this package. No family +implementation expansion is proposed. + +The norm is the joint operator norm on all designated data inputs and +completed outputs, at width five. Separate blockwise error bounds and +nonlinear rounding require new arguments. No Lean build, physical replay +or complete multiplication-theorem audit is claimed. + +## Open next questions + +The structured questions are in [TASK.json](TASK.json). + +- Can the best error achievable by actual paid-call circuits reach any of + the rank-relaxation thresholds? Begin with the five-target thirteen-call + case and a literal linear program; the spectrum alone gives no circuit. +- Can the leakage spectrum be derived in a short symbolic form for general + hook dimensions? Start with the signed translation symmetries of this + 280-square Gram matrix. No general-dimension formula is claimed here. + +Canonical investigation and advance claim: +[handoff comment 19141367](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19141367). diff --git a/research/block3-hook-error-spectrum/SOURCES.json b/research/block3-hook-error-spectrum/SOURCES.json new file mode 100644 index 0000000000..08c746b718 --- /dev/null +++ b/research/block3-hook-error-spectrum/SOURCES.json @@ -0,0 +1,28 @@ +{ + "schema_version": 1, + "base_commit": "4c0a359d88f22f05189d51f48387750b801a45d4", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395", + "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/complex-two-image-hook-prefix/README.md", + "usage": "provenance", + "git_blob": "ac33ab36287fe1f1d9ba51b5360f44536c2ff3fc", + "sha256": "91d45b5af6063e30c6860a4cb46cfc44960ecd67f37c3bce9675924e30b89b4e" + } + ], + "mathematical_citation": { + "url": "https://github.com/CrocSwap/integer-mult-bounds/blob/ee4fd87f064017c23e5a86fc1dcfe0a5237caed3/research/complex-small-m-lower-bounds/PROOF.md", + "use": "Cited paid-call cap80 theorem; not a live input or history-availability claim." + } +} diff --git a/research/block3-hook-error-spectrum/TASK.json b/research/block3-hook-error-spectrum/TASK.json new file mode 100644 index 0000000000..bec48bf214 --- /dev/null +++ b/research/block3-hook-error-spectrum/TASK.json @@ -0,0 +1,128 @@ +{ + "schema_version": 1, + "task_id": "independent-moment", + "priority_revision": 7, + "base_commit": "4c0a359d88f22f05189d51f48387750b801a45d4", + "original_card": { + "id": "independent-moment", + "question": "Does a new paid-profile or mixture-ceiling claim have independent source-bound coverage of its actual changed ledger?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/staged544-mixed-fourth-entry/README.md", + "research/staged-fourth-mixture-ceiling/README.md", + "research/r437-two-window-carrier/README.md" + ], + "methods": [ + "Independently reconstruct one changed paid ledger or pooled dual with exact source and model binding.", + "Check a genuinely uncovered moment implication with a different enclosure method and semantic controls." + ], + "acceptance_gate": "Demonstrate independence, source binding, positive cases and semantic failure controls. Name the existing checks and the missing coverage. More digits or another equivalent evaluation of an unchanged root is not by itself new verification coverage.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Choose one uncovered implication in #4088 literal mixed fill, #4091 pooled dual/model binding or #4067 changed frame/host bill. #4091 pins an earlier #4088 head: validate word, capacity and stock equivalence before applying that ceiling to the later fill.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "Independently reconstruct one changed ledger or pooled certificate with a positive case and a semantic failure control. Compare exact sources and name what existing checks miss. Keep this separate from supplier-boundary-audit (ordinary/outer dispatch) and uniform-transfer-audit (all-size proof). Stop after the chosen implication; more digits of an unchanged root are not additional mechanism coverage.", + "bottleneck_link": "Independent pricing prevents unsupported frontier claims and can reveal genuine accounting slack.", + "allowed_variations": [ + "Reconstruct either a source ledger or a numeric enclosure with a different method." + ], + "scope_change_triggers": [ + "Importing the primary function and calling its output independent verification.", + "Calling an aggregate histogram or source archive an independently accepted physical supplier." + ], + "overlap_terms": [ + "independent moment", + "rank histogram", + "exact enclosure", + "2979", + "rank7 joint endframes", + "paired extraction", + "joint lowering", + "4088", + "4091", + "4067", + "staged544-mixed-fourth-entry", + "staged-fourth-mixture-ceiling", + "r437-two-window-carrier" + ], + "existing_checks": [ + { + "scope": "PR #4088: mixed local/owner/phase ledger and moment reported.", + "evidence": "research/staged544-mixed-fourth-entry/README.md", + "remaining": "Independent binding of changed construction to paid histogram, distinct from full admission.", + "status": "author-checked", + "source_commit": "72d7efc181edb21806a878f174847c96dd410ab0", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4091: sharp pooled ceiling proposed for fixed THREE/FOUR words and inventory.", + "evidence": "research/staged-fourth-mixture-ceiling/README.md", + "remaining": "Validate dual, exhaustive pattern scope and exact source equivalence before applying to newer fills.", + "status": "author-checked", + "source_commit": "a29bdd8f56cd18b805917775cdec09ff935eddc4", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4067: paid (2,2) to (1,3) exchange and fixed OQ4 host reported.", + "evidence": "research/r437-two-window-carrier/README.md", + "remaining": "Independent full cost delta; remaining caller/precision/stock obligations are separate.", + "status": "author-checked", + "source_commit": "a95f11c52e3ca1e4c5171b3c20d8f4b0815aee2e", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Exact singular spectrum of the width-five block-three coordinate-hook leakage, and the resulting paid-call versus joint operator-error lower bound for linear completed outputs.", + "scope_change_reason": "The donor requests an original result, not predecessor verification. The card is redirected from paid-ledger auditing to new quantitative approximation information for the small complex unit model.", + "bottleneck_link": "Side result: establishes a nonzero error tolerance below which the existing small-unit call obstruction survives; does not improve the selected kappa or admit a supplier.", + "budget_minutes": 60, + "stop_rule": "Stop after the first exact spectral certificate and its stated operator-error implication. No larger hook census or circuit synthesis.", + "outcome": "completed", + "evidence": "PROOF.md sections 2 and 3; verify.py regenerates the integer Walsh-minor Gram matrix, annihilator, moments and six rejection controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can legal paid-call circuits attain a rank-relaxation error threshold?", + "why_it_matters": "Distinguishes a sharp rank-method obstruction from the actual approximate circuit optimum.", + "first_step": "Specify and price a literal five-target thirteen-call program and compute its joint operator error.", + "blocked_by": "No candidate circuit or physical realization is supplied here." + }, + { + "question": "Is there a symbolic general-hook spectrum formula?", + "why_it_matters": "Could replace finite spectral certificates with reusable all-dimension approximation bounds.", + "first_step": "Decompose the signed translation symmetries of the present 280-square Gram matrix.", + "blocked_by": "No general hook spectral decomposition is proved here." + } + ], + "claim_type": "scoped-proof", + "environment": { + "python": "CPython 3.12; standard library only" + }, + "coordination": { + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19141367", + "upstream_commit": "4c0a359d88f22f05189d51f48387750b801a45d4", + "priority_revision": 7 + }, + "predecessors": [ + { + "author": "Jacob Alan Sussman", + "pr": 4628, + "commit": "ee4fd87f064017c23e5a86fc1dcfe0a5237caed3", + "use": "Cited hook call-cap theorem, not replayed." + }, + { + "author": "lee-phys", + "pr": 4688, + "use": "Retained hook conventions; provenance only." + } + ] +} diff --git a/research/block3-hook-error-spectrum/VERIFY.json b/research/block3-hook-error-spectrum/VERIFY.json new file mode 100644 index 0000000000..5077a1489f --- /dev/null +++ b/research/block3-hook-error-spectrum/VERIFY.json @@ -0,0 +1,32 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact Walsh-minor Gram spectrum, integer annihilator and trace moments; rank-error endpoint oracle and six rejection controls." + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Same complete exact certificate with Python optimization enabled; explicit checks remain active." + } + ] +} diff --git a/research/block3-hook-error-spectrum/verify.py b/research/block3-hook-error-spectrum/verify.py new file mode 100644 index 0000000000..3edb27eca0 --- /dev/null +++ b/research/block3-hook-error-spectrum/verify.py @@ -0,0 +1,165 @@ +#!/usr/bin/env python3 +"""Exact block-three hook spectrum; produced by Nick Petalas, Apache-2.0.""" + +from collections import Counter +from fractions import Fraction +from hashlib import sha256 +from itertools import combinations, permutations +import json +from pathlib import Path + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def determinant4(rows, columns): + """Leibniz determinant, at most 24 products of four Walsh signs.""" + require(len(rows) == len(columns) == 4, "minor shape") + total = 0 + for order in permutations(range(4)): + inversions = sum(order[i] > order[j] + for i in range(4) for j in range(i + 1, 4)) + term = (-1) ** inversions + for i in range(4): + term *= (-1) ** ((rows[i] & columns[order[i]]).bit_count()) + total += term + return total + + +def leakage_numerator(): + """D/sqrt(32768) is the leakage matrix in normalized exterior bases.""" + subsets = tuple(combinations(range(8), 4)) + minors = tuple(tuple(determinant4(s, t) for t in subsets) for s in subsets) + inside = tuple((x, t) for t, subset in enumerate(subsets) for x in subset) + outside = tuple((y, s) for s, subset in enumerate(subsets) + for y in range(8) if y not in subset) + require(len(inside) == len(outside) == 280, "hook partition") + return tuple(tuple((-1) ** ((x & y).bit_count()) * minors[s][t] + for x, t in inside) for y, s in outside) + + +def scaled_gram(numerator): + """Construct A=8 L*L with integer arithmetic, checking every division.""" + require(len(numerator) == 280, "leakage rows") + require(all(len(row) == 280 for row in numerator), "leakage columns") + columns = tuple(zip(*numerator)) + matrix = [[0] * 280 for _ in range(280)] + for i in range(280): + for j in range(i, 280): + product = sum(x * y for x, y in zip(columns[i], columns[j])) + require(product % 4096 == 0, "nonintegral scaled Gram entry") + matrix[i][j] = matrix[j][i] = product // 4096 + return tuple(tuple(row) for row in matrix) + + +def multiply(left, right): + """Fixed 280-square sparse product, at most 280^3 scalar updates.""" + require(len(left) == len(right) == 280, "product rows") + require(all(len(row) == 280 for row in left + right), "product columns") + right_sparse = tuple(tuple((j, v) for j, v in enumerate(row) if v) + for row in right) + result = [[0] * 280 for _ in range(280)] + for i, row in enumerate(left): + for k, value in enumerate(row): + if value: + for j, other in right_sparse[k]: + result[i][j] += value * other + return tuple(tuple(row) for row in result) + + +def subtract_diagonal(matrix, value): + return tuple(tuple(x - (value if i == j else 0) + for j, x in enumerate(row)) for i, row in enumerate(matrix)) + + +def trace(matrix): + require(len(matrix) == 280, "trace rows") + return sum(matrix[i][i] for i in range(280)) + + +def certify(matrix): + """Symmetry, a square-free annihilator and four moments fix the spectrum.""" + require(all(matrix[i][j] == matrix[j][i] + for i in range(280) for j in range(280)), "Gram symmetry") + product = matrix + for root in (1, 5, 8): + product = multiply(product, subtract_diagonal(matrix, root)) + require(all(value == 0 for row in product for value in row), "annihilator") + square = multiply(matrix, matrix) + cube = multiply(square, matrix) + moments = (280, trace(matrix), trace(square), trace(cube)) + require(moments == (280, 1120, 6944, 46816), "spectral moments") + multiplicities = {0: 56, 1: 48, 5: 112, 8: 64} + for power in range(4): + require(sum(count * root ** power for root, count in multiplicities.items()) + == moments[power], "multiplicity equation") + # Distinct roots make these four Vandermonde equations nonsingular. + return moments, multiplicities + + +def rank_error_squared(rank_budget, targets): + require(isinstance(targets, int) and 1 <= targets <= 100, "target bound") + require(isinstance(rank_budget, int) and 0 <= rank_budget <= 280 * targets, + "rank bound") + for eigenvalue, multiplicity in ((8, 64), (5, 112), (1, 48)): + if rank_budget < multiplicity * targets: + return Fraction(eigenvalue, 8) + rank_budget -= multiplicity * targets + return Fraction(0) + + +def controls(matrix): + rejected = 0 + for change in (1, -1): + mutant = [list(row) for row in matrix] + mutant[0][0] += change + try: + certify(tuple(tuple(row) for row in mutant)) + except ValueError: + rejected += 1 + else: + raise ValueError("changed Gram diagonal accepted") + require(rejected == 2, "mutation coverage") + require(determinant4((0, 1, 2, 3), (0, 1, 2, 3)) == 16, "minor control") + for targets in range(1, 21): + explicit = ([Fraction(1)] * (64 * targets) + + [Fraction(5, 8)] * (112 * targets) + + [Fraction(1, 8)] * (48 * targets) + + [Fraction(0)] * (56 * targets)) + for budget in range(280 * targets + 1): + expected = explicit[budget] if budget < len(explicit) else Fraction(0) + require(rank_error_squared(budget, targets) == expected, + "ordered singular-value oracle") + require(rank_error_squared(80 * 13, 5) == Fraction(1, 8), "13-call obstruction") + require(rank_error_squared(80 * 14, 5) == 0, "14-call rank relaxation") + for arguments in ((-1, 1), (281, 1), (0, 0), (0, 101)): + try: + rank_error_squared(*arguments) + except ValueError: + rejected += 1 + else: + raise ValueError("invalid rank parameters accepted") + return rejected + + +def main(): + numerator = leakage_numerator() + require(Counter(value for row in numerator for value in row) + == {-16: 2600, -8: 24944, 0: 22848, 8: 25232, 16: 2776}, + "complete numerator census") + matrix = scaled_gram(numerator) + moments, multiplicities = certify(matrix) + rejected = controls(matrix) + here = Path(__file__).resolve().parent + files = ("verify.py", "PROOF.md", "README.md", "TASK.json", "SOURCES.json", "VERIFY.json") + hashes = {name: sha256((here / name).read_bytes()).hexdigest() for name in files} + print(json.dumps({"status": "PASS_BLOCK3_HOOK_ERROR_SPECTRUM", + "scaled_gram_dimension": 280, "moments": moments, + "scaled_gram_eigenvalues": multiplicities, + "rejected_controls": rejected, "source_sha256": hashes}, sort_keys=True)) + + +if __name__ == "__main__": + main()