diff --git a/research/gaussian-low-rank-bypass/PROOF.md b/research/gaussian-low-rank-bypass/PROOF.md new file mode 100644 index 0000000000..762aa99403 --- /dev/null +++ b/research/gaussian-low-rank-bypass/PROOF.md @@ -0,0 +1,128 @@ +# A dense bypass must retain almost full rank + +This contribution was produced by Nick Petalas. New work is Apache-2.0. + +Claim type: scoped written proof with exact finite corroboration. + +## Endpoint contract + +Let T be a complex d by d unitary matrix. Let K be a complex N by N +unitary matrix with every entry of modulus 1/sqrt(N). Allow arbitrary +rectangular matrices A of size N by d and B of size d by N. Write + + T = B K A + H + E, + rank_C(H) = h, + ||E||_(2->2) <= eta < 1, + M = ||A||_1 ||B||_infinity. + +Here ||A||_1 is the maximum absolute column sum and ||B||_infinity is +the maximum absolute row sum. The bypass H can be dense, have arbitrary +coefficients and have arbitrarily large norm. No inverse, sparsity or +restoration condition is imposed on the adapters. Encoding into clean +workspace and erasing unwanted outputs are allowed in this relaxation. + +The theorem is + + (d-h)(1-eta)^2 <= ||B K A||_F^2 <= d^2 M^2/N. (1) + +In particular, + + h >= ceil(d - d^2 M^2/[N(1-eta)^2]). (2) + +An integer upper bound on h may be substituted on the left of (1). +The lower bound is vacuous when its right side in (2) is negative. +All ranks in this note are complex coordinate-matrix ranks. They are not +the logarithmic axis ranks used to price recursive native calls. + +## Proof + +Put X=BKA. For every i,j, the triangle inequality and flatness give + + |X_ij| <= N^(-1/2) (sum_s |B_is|) (sum_t |A_tj|) + <= M/sqrt(N). + +Squaring and summing over the d^2 entries proves the upper bound in (1). + +Choose an orthonormal basis v_1,...,v_(d-h) for ker(H), and extend it to +an orthonormal basis of C^d. For each of the first d-h vectors, + + X v_i = (T-E) v_i, + ||X v_i||_2 >= ||T v_i||_2 - ||E v_i||_2 >= 1-eta. + +The squared Frobenius norm is the sum of the squared column norms in +any orthonormal input basis. Its remaining summands are nonnegative. +Therefore ||X||_F^2 >= (d-h)(1-eta)^2. This proves (1) and (2). +The elementary rank/energy argument is not claimed as a new general +matrix-analysis technique. The repository result is its dense-bypass +Gaussian fusion application and the sharp witness below. + +## Gaussian specialization + +Let C be the two by two matrix with diagonal a=(1+i)/2 and off-diagonal +b=(1-i)/2. Direct multiplication gives C* C=I and C times (1,1)^t=(1,1)^t. +For positive integers f,r,q, put + + n=2^f, N=2^(rf), d=q n, + K=C^(tensor rf), T=direct_sum_q C^(tensor f). + +Both matrices are unitary, K is flat, and T fixes the all-ones vector. +Thus (1) implies + + h >= ceil(q*2^f - q^2 M^2 * 2^((2-r)f)/(1-eta)^2). (3) + +For two targets, one rank-two child, exact output and M<=1, + + h >= 2*2^f - 4. (4) + +For two targets, arbitrary r>1, and a dense bypass of rank at most one +target dimension, h<=2^f, equation (1) requires + + M >= (1-eta) * 2^((r-1)f/2) / sqrt(2). (5) + +A uniformly bounded M cannot satisfy +it for growing f when r>1 and eta is bounded away from one. This does not +price the bypass: even a single old complete transform has coordinate +rank 2^f, and a physical implementation of H needs its own full bill. + +## The constant is sharp within the Gaussian family + +Assume d<=N. Let u be the d-dimensional all-ones vector, e_0 the first +child coordinate, k=K e_0 and P=u u*/d. Then P is the orthogonal +projection onto span(u), and TP=P. For any real 0<=eta<1 choose + + A=(1-eta) e_0 u*/d, + B=u k*, + H=(1-eta)(T-P), + E=eta T. + +Since ||k||_2=1, BKA=(1-eta)P and T=BKA+H+E. Also + + rank(H)=rank(T(I-P))=d-1, + ||A||_1=(1-eta)/d, + ||B||_infinity=sqrt(N), + M=(1-eta)sqrt(N)/d, + ||BKA||_F^2=(1-eta)^2. + +Both inequalities in (1) are equalities. Consequently the constant one +cannot be reduced, even for these Gaussian targets and children. This +does not assert attainability for every prescribed h or M. In the +two-target rank-two case, equality uses M=(1-eta)/2 and h=2*2^f-1. +The witness has dense, almost full-rank bypass and receives no physical +cost advantage from this identity. + +## Scope and predecessors + +ToikY [#7166](https://github.com/CrocSwap/integer-mult-bounds/pull/7166), +scientific head `6efb5d028b3212fba68edfb725608413622d6ab6`, supplies the +rectangular Gaussian adapter normalization and the sparse-bypass amplitude +test. A rank restriction does not bound column support. For example J/d +has rank one and no zero entries. Hence the old missing-entry step cannot +be substituted for the kernel argument above. No predecessor invoice or +native census is rechecked here. + +Credit Clear1nsight #4932/#4045/#3989, Rohan Arun #7113, the retained +Gaussian native/compiler lineage, and the classical triangle inequality, +rank-nullity and orthonormal-basis facts. The model here concerns a local +endpoint. Arbitrary coordinate recoding that increases M, changed child +normalization, several children or a differently priced bypass require +their own analysis. No complete supplier or multiplication theorem follows. diff --git a/research/gaussian-low-rank-bypass/README.md b/research/gaussian-low-rank-bypass/README.md new file mode 100644 index 0000000000..73903a5230 --- /dev/null +++ b/research/gaussian-low-rank-bypass/README.md @@ -0,0 +1,126 @@ +# A sharp energy obstruction for dense low-rank Gaussian bypasses + +This contribution was produced by Nick Petalas. New work is Apache-2.0. + +For a d-dimensional unitary target T, an N-dimensional flat unitary child K, +and arbitrary rectangular adapters, write + + T = B K A + H + E, + rank_C(H)=h, ||E||_(2->2)<=eta<1, + M=||A||_1 ||B||_infinity. + +The new local obstruction is + + (d-h)(1-eta)^2 <= ||BKA||_F^2 <= d^2 M^2/N. + +The bypass H may be dense and have unbounded coefficients. Its kernel forces +the child path to carry d-h almost unit-length orthogonal input directions. +An exact Gaussian family attains both inequalities, so the constant is sharp. +[PROOF.md](PROOF.md) gives the self-contained argument and construction. +Claim type: scoped written proof with exact finite corroboration. +Independent human and formal proof-kernel review are unclaimed. + +For two independent width-f Gaussian targets and one rank-two flat child, +an exact endpoint with M<=1 requires bypass matrix rank at least +`2*2^f-4`. A dense bypass of rank at most `2^f` instead requires +`M >= (1-eta)*2^((r-1)f/2)/sqrt(2)` for a rank-r child. Coordinate-matrix +rank here differs from the axis rank used to charge recursive calls. + +## What changed + +ToikY [#7166](https://github.com/CrocSwap/integer-mult-bounds/pull/7166), +at `6efb5d028b3212fba68edfb725608413622d6ab6`, supplies the rectangular +Gaussian adapter model and sparse-bypass amplitude obstruction. A dense +rank-one matrix can touch every entry. The new argument therefore replaces +the missing-entry test with a kernel/Frobenius-energy bound. No predecessor +scientific verifier or invoice is replayed as this contribution. + +The concurrent [column-sparse approximation claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19541721) +restricts each bypass column's support and uses maximum column error. This +package restricts the bypass's complex matrix rank and uses operator error. +Neither hypothesis implies the other. ToikY +[#7245](https://github.com/CrocSwap/integer-mult-bounds/pull/7245) addresses +retained whole-output consolidation and leaves changed multi-output children +open. This local necessary condition constructs no paid multi-output child. + +## Evidence and reproduction + +From the repository root with the tested CPython 3.12.15 interpreter: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/gaussian-low-rank-bypass/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/gaussian-low-rank-bypass/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/gaussian-low-rank-bypass +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/gaussian-low-rank-bypass --check-source-history --check-modes +``` + +Other hosts may substitute their CPython 3.12 executable. The direct marker is +`PASS_GAUSSIAN_LOW_RANK_BYPASS`. The verifier emits a generated JSON receipt +with its interpreter version, exact coverage and all six package-file hashes. +It writes no files. The registered commands run normal and optimized Python. + +Exact Gaussian-rational arithmetic checks four flat unitary children of +dimensions 2, 4, 16 and 64; 28 equality witnesses; 48 additional adapter +fixtures; two zero-bypass full-child controls; and 14 rejecting controls. +The equality fixtures use the parameter pairs `(f,r)=(1,2),(1,4),(2,2), +(2,3),(3,2)`, every `q=1,...,min(3,N/2^f)`, and `eta=0,1/2`. +The additional adapters are a declared deterministic fixture family, not an +exhaustive census of all adapters. The error fixtures have `E=eta*T`; the +universal theorem permits arbitrary E with operator norm at most eta. + +The checks multiply the literal rectangular maps, eliminate the actual +bypass matrices over Q(i), verify each endpoint and both energy bounds, +and check equality in the sharp family. Rejection controls cover incorrect +rank, removed or sign-reversed bypass, changed error, invalid error domain, +changed child phase, altered adapters, dimension mismatch and invalid child +unitarity/dimensions/flatness. Checks remain active under optimized Python. + +## Scope and limits + +This is a local algebraic necessary condition and a sharp relaxed witness. +The bypass's rank is not its implementation price. No physical allocation, +dirty workspace restoration, routing, native adaptation, tape/precision +cost, supplier admission, new kappa or complete multiplication theorem is +established. The sharp witness uses an almost full-rank dense bypass and +does not claim a favorable recursive invoice. No Lean, Docker or full +selected-source replay is run. The selected #7000 record is unchanged. + +The `coverage-law-change` card changes scope from a completed productive +split to a dense low-rank bypass obstruction. Canonical base is +`e54523517d0f03e58352e647c403a5af3e525a57`, priority revision 8. Its catalogue +assessment still names #5599; `certificates/selected-result.json` resolves +the current #7000 context. The card's first metadata orientation passed +`PASS_RESEARCH_BASELINE_BINDINGS_ONLY`, without a scientific replay. +[SOURCES.json](SOURCES.json) pins the catalogue and selected record only as +historical provenance. The theorem and verifier import no predecessor code +or external scientific data. The exact predecessor head above is a model +citation, not a live input or a claimed source-availability certificate. + +The verifier has no recursion, subprocess or external dependencies. Matrix +dimensions are capped at 64; each product has at most 64^3 scalar steps. +Python dynamically allocates bounded rational matrices and integers, a +managed-runtime deviation from fixed-allocation rules. Its fixed fixture +domain bounds operand sizes; no arbitrary-input service is provided. +Every function is shorter than 60 lines. Warning-strict normal/optimized +execution and source compilation are the applicable local diagnostics. + +## Open next questions + +Structured questions are in [TASK.json](TASK.json). + +- Can actual eligible bypass maps be bounded by coordinate rank below the + required floor at one complete Gaussian caller? Start by identifying the + literal bypass input/output spaces. Charging those maps and every adapter + remains necessary before claiming a paid gain or a complete obstruction. +- At fixed Gaussian f,r,q and prescribed M, what is the exact minimum bypass + rank? Begin with one rank deficit greater than one. Sharpness of the + constant above does not prove that every point on the bound is attainable. + +## Credit + +Credit ToikY #7166 for the rectangular Gaussian normalization; Clear1nsight +#4932/#4045/#3989 for the earlier scoped fusion boundaries; Rohan Arun #7113 +and the retained Gaussian native, controller and compiler lineage. The +general matrix inequalities are elementary classical facts. The new +dense-bypass application, sharp Gaussian witness and finite verifier were +produced by Nick Petalas. diff --git a/research/gaussian-low-rank-bypass/SOURCES.json b/research/gaussian-low-rank-bypass/SOURCES.json new file mode 100644 index 0000000000..5335fa97d9 --- /dev/null +++ b/research/gaussian-low-rank-bypass/SOURCES.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "75d77b328ea02ded535e7f23aee5b1e55d0bb1a8", + "sha256": "154c3d30455d778fd3343b6b4851f0fa4665f0f7625b0adb3675e2bafbbf6bf1" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + } + ] +} diff --git a/research/gaussian-low-rank-bypass/TASK.json b/research/gaussian-low-rank-bypass/TASK.json new file mode 100644 index 0000000000..0a861183bc --- /dev/null +++ b/research/gaussian-low-rank-bypass/TASK.json @@ -0,0 +1,87 @@ +{ + "schema_version": 1, + "task_id": "coverage-law-change", + "priority_revision": 8, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "original_card": { + "id": "coverage-law-change", + "question": "Can a completed call earn more independent productive target credit without an offsetting paid bill?", + "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": "Use #5599 as a completed positive control, then choose one uncovered cut/module beyond an applicable frozen exclusion. Derive independence, saturation and chronological availability rather than counting rational rank alone. Price target credits and all new jobs together, then check compiler and actual caller compatibility. Stop on a nonphysical credit or an unfavorable complete relaxation.", + "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": [ + "target credit", + "helper split", + "coverage law" + ], + "existing_checks": [ + { + "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 Frobenius-energy obstruction for a dense low-complex-rank bypass around one flat Gaussian child, including operator-norm output error.", + "scope_change_reason": "Replace column-sparse bypass by arbitrary dense bypass of bounded coordinate-matrix rank. This is a scoped necessary condition rather than a complete productive split.", + "bottleneck_link": "Tests whether dense low-rank side channels can evade bounded-adapter fusion obstructions without providing a paid supplier.", + "budget_minutes": 60, + "stop_rule": "Stop after the first proved inequality with an exact attaining Gaussian family and bounded finite corroboration.", + "outcome": "completed", + "evidence": "PROOF.md; verify.py: 28 equality witnesses, 48 general-adapter fixtures, two full-child controls and 14 rejecting controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can one actual caller bound eligible bypass coordinate rank below the floor?", + "why_it_matters": "A caller-bound rank cap could close this dense-bypass fusion route.", + "first_step": "Pin its literal bypass domain and codomain, then charge all maps and adapters.", + "blocked_by": "No caller-bound bypass rank or complete physical bill is supplied." + }, + { + "question": "At prescribed Gaussian f,r,q,M, what is the exact minimum bypass rank?", + "why_it_matters": "Sharpness of the universal constant need not settle every constrained optimum.", + "first_step": "Seek one attaining construction or strict improvement for rank deficit greater than one.", + "blocked_by": "The present sharp family has rank deficit one." + } + ], + "claim_type": "scoped proof with exact finite corroboration", + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19541804", + "predecessor": { + "pr": 7166, + "author": "ToikY", + "head": "6efb5d028b3212fba68edfb725608413622d6ab6", + "usage": "Self-contained model citation; no live input or imported code" + } +} diff --git a/research/gaussian-low-rank-bypass/VERIFY.json b/research/gaussian-low-rank-bypass/VERIFY.json new file mode 100644 index 0000000000..f3c21f8b92 --- /dev/null +++ b/research/gaussian-low-rank-bypass/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": "Exact Gaussian unitary, endpoint, bypass rank and energy checks; sharp constructions and rejection controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Repeat all exact checks with optimized Python; no assert-dependent acceptance." + } + ] +} diff --git a/research/gaussian-low-rank-bypass/verify.py b/research/gaussian-low-rank-bypass/verify.py new file mode 100644 index 0000000000..2901c6f7c8 --- /dev/null +++ b/research/gaussian-low-rank-bypass/verify.py @@ -0,0 +1,298 @@ +"""Exact finite corroboration of the dense-bypass energy theorem. + +Produced by Nick Petalas. Apache-2.0. +The universal assertion is proved in PROOF.md. This program checks bounded +Gaussian-rational matrices and writes only its generated receipt to stdout. +""" + +from fractions import Fraction as F +from hashlib import sha256 +from math import isqrt +from pathlib import Path +import json +import platform + +type G = tuple[F, F] +type Matrix = tuple[tuple[G, ...], ...] +ZERO: G = (F(0), F(0)) +ONE: G = (F(1), F(0)) +MAX_DIMENSION = 64 + + +def require(condition: bool, message: str) -> None: + if not condition: + raise ValueError(message) + + +def check(condition: bool, message: str) -> None: + if not condition: + raise AssertionError(message) + + +def add(a: G, b: G) -> G: + return (a[0] + b[0], a[1] + b[1]) + + +def neg(a: G) -> G: + return (-a[0], -a[1]) + + +def mul(a: G, b: G) -> G: + return (a[0] * b[0] - a[1] * b[1], a[0] * b[1] + a[1] * b[0]) + + +def conjugate(a: G) -> G: + return (a[0], -a[1]) + + +def squared(a: G) -> F: + return a[0] ** 2 + a[1] ** 2 + + +def divide(a: G, b: G) -> G: + norm = squared(b) + require(norm != 0, "zero divisor") + product = mul(a, conjugate(b)) + return (product[0] / norm, product[1] / norm) + + +def modulus_upper(a: G) -> F: + norm = squared(a) + numerator, denominator = isqrt(norm.numerator), isqrt(norm.denominator) + if numerator**2 == norm.numerator and denominator**2 == norm.denominator: + return F(numerator, denominator) + return abs(a[0]) + abs(a[1]) + + +def shape(a: Matrix) -> tuple[int, int]: + require(1 <= len(a) <= MAX_DIMENSION, "row dimension") + columns = len(a[0]) + require(1 <= columns <= MAX_DIMENSION, "column dimension") + require(all(len(row) == columns for row in a), "ragged matrix") + return len(a), columns + + +def identity(n: int) -> Matrix: + require(1 <= n <= MAX_DIMENSION, "identity dimension") + return tuple(tuple(ONE if i == j else ZERO for j in range(n)) for i in range(n)) + + +def scale(a: Matrix, factor: F) -> Matrix: + shape(a) + return tuple(tuple((v[0] * factor, v[1] * factor) for v in row) for row in a) + + +def plus(a: Matrix, b: Matrix) -> Matrix: + require(shape(a) == shape(b), "sum dimensions") + return tuple(tuple(add(x, y) for x, y in zip(u, v)) for u, v in zip(a, b)) + + +def adjoint(a: Matrix) -> Matrix: + rows, columns = shape(a) + return tuple(tuple(conjugate(a[i][j]) for i in range(rows)) for j in range(columns)) + + +def product(a: Matrix, b: Matrix) -> Matrix: + rows, inner = shape(a) + other, columns = shape(b) + require(inner == other, "product dimensions") + sparse_rows = tuple(tuple((j, v) for j, v in enumerate(row) if v != ZERO) for row in b) + result = [] + for i in range(rows): + values = [ZERO] * columns + for k in range(inner): + if a[i][k] != ZERO: + for j, value in sparse_rows[k]: + values[j] = add(values[j], mul(a[i][k], value)) + result.append(tuple(values)) + return tuple(result) + + +def rank(a: Matrix) -> int: + rows, columns = shape(a) + work = [list(row) for row in a] + pivot_row = 0 + for column in range(columns): + candidates = [i for i in range(pivot_row, rows) if work[i][column] != ZERO] + if not candidates: + continue + selected = candidates[0] + work[pivot_row], work[selected] = work[selected], work[pivot_row] + divisor = work[pivot_row][column] + work[pivot_row] = [divide(v, divisor) for v in work[pivot_row]] + for i in range(rows): + coefficient = work[i][column] + if i != pivot_row and coefficient != ZERO: + work[i] = [add(x, neg(mul(coefficient, y))) for x, y in zip(work[i], work[pivot_row])] + pivot_row += 1 + if pivot_row == rows: + break + return pivot_row + + +def gaussian_entry(width: int, row: int, column: int) -> G: + require(1 <= width <= 6 and 0 <= row < 2**width and 0 <= column < 2**width, "Gaussian address") + value = ONE + for bit in range(width): + sign = -1 if ((row ^ column) >> bit) & 1 else 1 + value = mul(value, (F(1, 2), F(sign, 2))) + return value + + +def gaussian(width: int) -> Matrix: + require(1 <= width <= 6, "Gaussian width") + n = 2**width + return tuple(tuple(gaussian_entry(width, i, j) for j in range(n)) for i in range(n)) + + +def validate_unitary(a: Matrix) -> None: + rows, columns = shape(a) + require(rows == columns, "unitary dimensions") + check(product(adjoint(a), a) == identity(rows), "unitary identity") + + +def validate_child(k: Matrix) -> None: + validate_unitary(k) + n = len(k) + check(all(squared(value) == F(1, n) for row in k for value in row), "flat child") + + +def target(width: int, copies: int) -> Matrix: + require(1 <= width <= 3 and 1 <= copies <= 3, "target parameters") + n = 2**width + d = copies * n + return tuple(tuple(gaussian_entry(width, i % n, j % n) if i // n == j // n else ZERO + for j in range(d)) for i in range(d)) + + +def frobenius_squared(a: Matrix) -> F: + shape(a) + return sum((squared(value) for row in a for value in row), F(0)) + + +def adapter_bounds(a: Matrix, b: Matrix) -> tuple[F, F]: + rows, columns = shape(a) + shape(b) + column_bound = max(sum((modulus_upper(a[i][j]) for i in range(rows)), F(0)) for j in range(columns)) + row_bound = max(sum((modulus_upper(v) for v in row), F(0)) for row in b) + return column_bound, row_bound + + +def check_case(t: Matrix, k: Matrix, a: Matrix, b: Matrix, h: Matrix, + eta: F, claimed_rank: int | None = None) -> tuple[int, F, F]: + """K and T are immutable matrices validated by the fixture boundary. + + Error fixtures have E=eta*T, whose operator norm is exactly eta. + The theorem itself permits every E with operator norm at most eta. + """ + require(F(0) <= eta < F(1), "error domain") + d, columns = shape(t) + require(d == columns and shape(h) == (d, d), "endpoint dimensions") + child_path = product(b, product(k, a)) + check(plus(plus(child_path, h), scale(t, eta)) == t, "endpoint equation") + h_rank = rank(h) + if claimed_rank is not None: + check(h_rank == claimed_rank, "bypass rank") + column_bound, row_bound = adapter_bounds(a, b) + energy = frobenius_squared(child_path) + upper = F(d * d, len(k)) * (column_bound * row_bound) ** 2 + lower = (d - h_rank) * (1 - eta) ** 2 + check(lower <= energy <= upper, "energy sandwich") + return h_rank, energy, upper + + +def sharp_witness(t: Matrix, k: Matrix, eta: F) -> tuple[Matrix, Matrix, Matrix]: + d, n = len(t), len(k) + require(d <= n, "witness capacity") + a = tuple(tuple((F(1 - eta, d), F(0)) if i == 0 else ZERO for _ in range(d)) for i in range(n)) + b = tuple(tuple(conjugate(k[i][0]) for i in range(n)) for _ in range(d)) + projection = tuple(tuple((F(1, d), F(0)) for _ in range(d)) for _ in range(d)) + h = scale(plus(t, scale(projection, F(-1))), 1 - eta) + return a, b, h + + +def seeded_adapter(rows: int, columns: int, seed: int) -> Matrix: + require(1 <= rows <= 16 and 1 <= columns <= 16 and 0 <= seed < 100, "adapter seed") + return tuple(tuple((F(((i * 7 + j * 3 + seed) % 5) - 2, 4), + F(((i * 3 + j * 11 + seed * 2) % 3) - 1, 4)) + for j in range(columns)) for i in range(rows)) + + +def finite_checks() -> dict[str, int]: + children = {width: gaussian(width) for width in (1, 2, 4, 6)} + for k in children.values(): + validate_child(k) + counts = {"flat_unitaries": len(children), "sharp_witnesses": 0, + "general_adapters": 0, "full_child_controls": 0} + for width, recursive_rank in ((1, 2), (1, 4), (2, 2), (2, 3), (3, 2)): + k = children[width * recursive_rank] + for copies in range(1, min(3, len(k) // 2**width) + 1): + t = target(width, copies) + validate_unitary(t) + for eta in (F(0), F(1, 2)): + a, b, h = sharp_witness(t, k, eta) + h_rank, energy, upper = check_case(t, k, a, b, h, eta, len(t) - 1) + check(energy == upper == (1 - eta) ** 2, "sharp constant") + check(h_rank == len(t) - 1, "sharp rank") + counts["sharp_witnesses"] += 1 + for width in (1, 2): + k, t = children[2], target(width, 1) + validate_unitary(t) + for seed in range(24): + a = seeded_adapter(len(k), len(t), seed) + b = seeded_adapter(len(t), len(k), seed + 24) + h = plus(t, scale(product(b, product(k, a)), F(-1))) + check_case(t, k, a, b, h, F(0)) + counts["general_adapters"] += 1 + for width in (1, 2): + k = children[width] + check_case(k, k, identity(len(k)), identity(len(k)), scale(k, F(0)), F(0), 0) + counts["full_child_controls"] += 1 + return counts + + +def rejection_checks() -> int: + t, k = target(1, 2), gaussian(2) + validate_unitary(t) + validate_child(k) + a, b, h = sharp_witness(t, k, F(0)) + cases = ((t, k, a, b, h, F(0), 2), + (t, k, a, b, scale(h, F(0)), F(0), None), + (t, k, a, b, scale(h, F(-1)), F(0), None), + (t, k, a, b, h, F(1, 2), None), + (t, k, a, b, h, F(1), None), + (t, k, a, b, h, F(-1), None), + (t, scale(k, F(-1)), a, b, h, F(0), None), + (t, k, scale(a, F(2)), b, h, F(0), None), + (t, k, a, scale(b, F(0)), h, F(0), None), + (t, k, a[:-1], b, h, F(0), None), + (t, k, a, b, h[:-1], F(0), None)) + rejected = 0 + for case in cases: + try: + check_case(*case) + except (AssertionError, ValueError): + rejected += 1 + check(rejected == len(cases), "rejection controls") + for malformed in (scale(k, F(2)), k[:-1], identity(len(k))): + try: + validate_child(malformed) + except (AssertionError, ValueError): + rejected += 1 + else: + raise AssertionError("invalid child accepted") + return rejected + + +def main() -> None: + counts = finite_checks() + counts["rejection_controls"] = rejection_checks() + package = Path(__file__).resolve().parent + names = ("PROOF.md", "README.md", "SOURCES.json", "TASK.json", "VERIFY.json", "verify.py") + hashes = {name: sha256((package / name).read_bytes()).hexdigest() for name in names} + print(json.dumps({"status": "PASS_GAUSSIAN_LOW_RANK_BYPASS", "python": platform.python_version(), + "counts": counts, "sha256": hashes}, sort_keys=True, indent=2)) + + +if __name__ == "__main__": + main()