diff --git a/research/transfer-transient-leakage/PROOF.md b/research/transfer-transient-leakage/PROOF.md new file mode 100644 index 0000000000..6084f7a0d4 --- /dev/null +++ b/research/transfer-transient-leakage/PROOF.md @@ -0,0 +1,173 @@ +# Uniform error from one transient virtual block + +This is a scoped written proof. The finite executable corroborates the stated +identities; it does not supply their unbounded quantifiers. + +## Complete physical endpoint + +Use zxv's PR5441 fixed-transfer contract over the complex field. There are +`d` physical input and output letters, a fixed virtual space `V=U direct-sum W`, +and a fixed transfer matrix for each physical pair: + +```text +T[y,x] = [ A[y,x] C[y,x] ] + [ 0 D[y,x] ]. +F = [L 0], B = [0; R]. + +E_f[i,y_1...y_f ; j,x_1...x_f] + = (F T[y_1,x_1] ... T[y_f,x_f] B)[i,j]. +``` + +`L:U->C^p` and `R:C^q->W` include every output and input role required by +the endpoint. If this is an error certificate, `E_f` must represent the +complete implementation-minus-target operator, including required dirty +returns. The theorem does not license removal of a return block. The virtual +states are representation coordinates, not free physical workspace. + +All matrices, the splitting, and both boundaries are fixed across widths. +The lower-left zero is an exact hypothesis. Width-dependent tables require +their own explicitly represented controller. + +Let `P_U,P_W` be positive-definite Hermitian matrices. Give the virtual spaces +their induced Hilbert norms and physical spaces their ordinary Euclidean norms. +Put `P_dU=I_d tensor P_U` and `P_dW=I_d tensor P_W`. +Use physical-major ordering to assemble the full local operators +`Ahat=[A[y,x]]`, `Chat=[C[y,x]]`, `Dhat=[D[y,x]]`. +These are coherent operators on a physical column and its virtual state. + +## Theorem + +Suppose `alpha,beta,delta>=0`, `0<=rho<1`, and + +```text +Ahat* P_dU Ahat <= P_dU, +Dhat* P_dW Dhat <= rho^2 P_dW, +Chat* P_dU Chat <= delta^2 P_dW, +L* L <= alpha P_U, +R* P_W R <= beta I_q. +``` + +Then, at every positive integer width, + +```text +||E_f||_op <= sqrt(alpha beta) delta (1-rho^f)/(1-rho) + <= sqrt(alpha beta) delta/(1-rho). +``` + +The norm is on the full `p*d^f` by `q*d^f` operator. There is no physical +dimension factor. The inequalities include every off-diagonal physical-input +block. Bounds on individual columns or individual `T[y,x]` do not suffice. + +### Proof + +Lift each local block to its column in the full physical tensor product, +tensoring identities on the other columns. Its weighted operator norm is +unchanged. Apply the right boundary first, then columns `f,f-1,...,1`, +then the left boundary. The coefficient product is exactly the displayed +`T[y_1,x_1]...T[y_f,x_f]`, as in PR5451's physical contraction proof. + +Because the lower-left block is zero, every path from `W` at the right +boundary to `U` at the left boundary crosses `C` exactly once. The complete +upper-right block of the product is + +```text +sum_(k=1)^f A_1 ... A_(k-1) C_k D_(k+1) ... D_f. +``` + +The subscripts identify lifted columns; no commutation of virtual matrices +is assumed. Each summand has weighted norm at most `delta rho^(f-k)`. +The triangle inequality and geometric sum bound the complete upper-right +block by `delta(1-rho^f)/(1-rho)`. The two boundary inequalities multiply +this by `sqrt(alpha beta)`. This proves both assertions. For `rho=0`, +the sum consists only of its final nonzero term, with empty products +interpreted as identities. For `delta=0`, the endpoint is zero. QED. + +This is a different sufficient certificate from requiring a contraction +metric for the entire local `T` operator. It does not supersede that test +on arbitrary endpoints or characterize every uniformly bounded family. + +## A sharp family outside the whole-table metric test + +Let `d=2`, `dim U=dim W=p=q=1`, `delta>0`, and `0<=rho<1`. Take + +```text +T[0,0] = T_plus = [1 delta], + [0 rho], +T[1,1] = T_minus = [1 -delta], + [0 rho], +T[0,1] = T[1,0] = 0, +F=(1,0), B=(0,1)^T. +``` + +The scalar block metrics are both one, and `alpha=beta=1`. The full local +blocks are `Ahat=I_2`, `Dhat=rho I_2`, `Chat=delta diag(1,-1)`, so every +theorem inequality holds with equality. + +`E_f` is diagonal in the physical bit basis. On the word `x_1...x_f` its +diagonal entry is + +```text +delta sum_(k=1)^f (-1)^(x_k) rho^(f-k). +``` + +The absolute value is at most the geometric sum, and the all-zero input +attains it. Consequently + +```text +||E_f||_op = delta (1-rho^f)/(1-rho). +sup_(f>=1) ||E_f||_op = delta/(1-rho). +``` + +Thus the theorem's width bound and uniform constant are sharp. For +`rho=1/2, delta=1/1024`, the error is strictly below `1/512` at every finite +positive width, with supremum exactly `1/512`. + +### No common positive contraction metric in this representation + +Suppose a positive-definite Hermitian `G=[[a,z],[conjugate(z),b]]` and +`0<=c<=1` satisfy the full local PR5451 inequality. Since the physical +table is diagonal, this requires both `T_plus* G T_plus<=cG` and +`T_minus* G T_minus<=cG`. + +Both matrices fix `e_1`. Evaluation on that vector gives `a<=ca`, and +`a>0` forces `c=1`. The two positive-semidefinite matrices +`K_plus=G-T_plus*G T_plus` and `K_minus=G-T_minus*G T_minus` have zero +top-left entry. A zero diagonal entry of a positive-semidefinite Hermitian +matrix forces its row and column to vanish. One can see this from its +two-by-two principal minors, which would otherwise be negative. + +Their upper-right entries must therefore both vanish: + +```text +(1-rho) z - a delta = 0, +(1-rho) z + a delta = 0. +``` + +Subtracting yields `2 a delta=0`, contradicting positivity. No such metric +exists, including a metric with complex off-diagonal entries. QED. + +This impossibility concerns the exact two-state representation above and +the full-table contraction test with `c<=1`. It does not exclude another +representation, a different sufficient certificate, or the bounded endpoint +itself. In particular, it is no criticism of PR5451's correctly stated +sufficient test and no re-audit of that work. + +## What remains open + +No actual selected native word or physical caller is bound to this triangular +contract. Exact source/version extraction, physical realization and return, +coefficient access, movement, storage, precision, stock, recursive compilation +and a separately justified recovery tolerance remain obligations. The result +does not improve kappa or discharge a selected framework assumption. + +The block-product expansion, Hilbert norms and geometric-series estimates +are classical. The contribution is this sufficient physical endpoint +certificate, its sharp two-state separation from the whole-table metric +test, and its exact executable corroboration. No global literature-priority +claim is made. Credit zxv/PR5441 for the interface and approximation question, +and Ali Romman/PR5451 for the coherent local-metric certificate and retained +physical contraction argument. Their automata, matrix-product, native, +phase and compiler lineage retains its credit. + +This contribution was produced by Nick Petalas. Apache-2.0. +Independent human and formal proof-kernel review are unclaimed. diff --git a/research/transfer-transient-leakage/README.md b/research/transfer-transient-leakage/README.md new file mode 100644 index 0000000000..3f872cf8a8 --- /dev/null +++ b/research/transfer-transient-leakage/README.md @@ -0,0 +1,139 @@ +# Sharp uniform error from transient transfer leakage + +A fixed physical transfer table can have a small error at every width even +when it admits no positive contraction metric for its complete local operator. +This package proves a separate-block certificate and gives a sharp two-state +example outside the whole-table test in its stated representation. + +Claim type: scoped written proof with finite exact corroboration. No new +kappa, physical supplier or selected-frontier change is claimed. + +For a fixed triangular virtual table, suppose the active block has norm at +most one, the transient block has norm at most `rho<1`, and its leakage into +the active block has norm at most `delta`. Use the complete coherent physical +blocks and positive virtual metrics. With unit boundary norms, the complete +endpoint error satisfies + +```text +||E_f||_op <= delta (1-rho^f)/(1-rho), every f>=1. +``` + +[PROOF.md](PROOF.md) states the general boundary factors, fixed-table and +exact-zero hypotheses and proves the operator bound. It includes all physical +input/output entries and required role returns. There is no factor depending +on the exponentially growing payload dimension. + +For diagonal physical tables with virtual matrices +`[[1,delta],[0,rho]]` and `[[1,-delta],[0,rho]]`, the bound is an equality at +every positive width. The uniform supremum is exactly `delta/(1-rho)`. +The choice `delta=1/1024, rho=1/2` gives error strictly below `1/512` at each +finite width. No positive-definite Hermitian metric can make both matrices +nonexpanding. This last statement concerns this two-state representation, +not every representation of the same endpoint. + +## Source and contribution + +The question comes from zxv's +[PR5441](https://github.com/CrocSwap/integer-mult-bounds/pull/5441), uniform +approximation direction. Ali Romman's +[PR5451](https://github.com/CrocSwap/integer-mult-bounds/pull/5451) supplies +the whole-table sufficient metric test and coherent physical norm argument. +The new step is a transient-leakage certificate and a sharp bounded family +that cannot pass that test in its given representation. Neither predecessor +is audited, replayed or claimed as this contribution. + +Classical block-product expansions, Hilbert norms, geometric series and PSD +null-row arguments retain their credit. The predecessors' weighted-automata, +matrix-product, native, phase and compiler lineage retains its credit. No +global literature-priority or new general stability-algorithm claim is made. +This contribution was produced by Nick Petalas. Apache-2.0. +Independent human and formal proof-kernel review are unclaimed. + +The formal-interface-lemma card has explicitly changed to this written +numerical-interface side result. It is not a formal-kernel proof or a binding +to an actual selected caller. The selected-baseline metadata orientation +passed; it was not a scientific replay. Canonical base is +`7c49fe32c55de02c2c873655c804b16e4c3fef0a`, priority revision 8, selected PR6030. +[TASK.json](TASK.json) records the scope, overlap limits and next questions; +[SOURCES.json](SOURCES.json) pins the retained proof sources as provenance. +The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19375359) +matches the delivered mathematical scope. + +## Reproduce + +From the repository root, CPython 3.12 and its standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/transfer-transient-leakage/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/transfer-transient-leakage/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/transfer-transient-leakage +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/transfer-transient-leakage --check-source-history +``` + +Another CPython 3.12 executable may replace this local path. Direct replay +prints a generated JSON receipt with status `PASS_TRANSFER_TRANSIENT_LEAKAGE` +and SHA256 bindings for every package file. It writes nothing and requires +neither Git nor network access. The registered hook runs normal and optimized +warning-strict modes. The source-history preflight requires committed files. + +The checker enumerates all 65,520 physical words across eight rational +families at widths 1 through 12, confirming all 96 sharp norms. It constructs +24 complete physical matrices with 4,080 entries across six certificates at +widths 1 through 4. These include noncommuting virtual actions, coherent +physical mixing, two input/output roles and a nonidentity metric. Literal +weighted and unweighted endpoints agree entry by entry. + +An independent principal-minor/permutation-determinant oracle agrees with +the Schur PSD test on all 729 symmetric three-by-three ternary matrices. +Another 32 exact fixtures corroborate the incompatible metric equations. +Thirteen invalid certificates reject, including a coherent cross-input +sum whose individual columns pass their stated leakage bound, and omitted +input/output role charges. The universal theorems rest on the written proof. + +## Limits and implementation bounds + +This is a sufficient certificate for a fixed linear residual representation. +It neither classifies every bounded family nor certifies nonlinear rounding +merely from a local table. The triangular zero and block/boundary norm bounds +must all be established for the complete residual. Failure to find these +data is inconclusive. + +Actual native source/version extraction, physical realization, dirty restoration +outside the represented endpoint, coefficient access, tape movement, storage, +precision, stock, compiler and recovery budgets remain open. All five selected +framework assumptions remain. No selected scientific cold replay, predecessor +executable, Lean or Docker run is included. + +The terminating checker has no external data input, recursion, subprocess, +network or filesystem writes. The fixed fixture domains bound every loop. +The largest literal endpoint is 32 by 32; the word iterator holds one word +of at most 12 bits. Matrix helpers enforce a 64-by-64 ceiling, and source +authentication reads exactly six files capped at 128 KiB each. Functions are +under 60 physical lines. Meaningful exception-based contracts remain active +under optimization. File hashing assumes a stable package during replay. + +Power-of-ten rule 3 deviation: CPython and Fraction allocate bounded objects +during this offline checker. Fixed fixture dimensions and word lengths, streamed +word enumeration and 120-second registered timeouts constrain the work. A +fixed-storage implementation is needed before use in a steady service. +Rule 8 deviation: the standard-library frozen dataclass generates its fixed +record initializer; fields and the finite replacement controls are static. +No external registration or generated executable code is accepted. +An explicit record initializer is the replacement if this checker is ported +to an environment that prohibits generated initializers. +Warning-strict normal and optimized replay and AST inspection are the available +diagnostics. Ruff is absent in the local environment; no global lint setup is +changed. Build the Lever led to the rerunnable exact checker. Prove It Works +led to literal complete-operator checks and the separate PSD oracle. Laziness +Protocol kept the change within one six-file package. + +## Open next questions + +1. Can one actual consumer's complete residual be put in this triangular form + with a useful `rho` and `delta`? First extract all role/version blocks and + prove its exact lower-left zero. Source extraction, physical access and a + separately justified recovery tolerance are the blockers. +2. Can a paid physical implementation preserve the transient splitting without + introducing feedback or omitted returns? Start with one explicit local + operator and charge its preparation, use and cleanup. No such realization + or complete invoice is supplied here. diff --git a/research/transfer-transient-leakage/SOURCES.json b/research/transfer-transient-leakage/SOURCES.json new file mode 100644 index 0000000000..fcedb33665 --- /dev/null +++ b/research/transfer-transient-leakage/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/finite-memory-lifting/PROOF.md", + "usage": "provenance", + "git_blob": "36152f9e31555a88ce3636ae59abf07a8058d78d", + "sha256": "de4a6b79d480d7718b3d157d2be73b4f45723ccac6719160dd815f8cef40356b" + }, + { + "path": "research/finite-memory-lifting/README.md", + "usage": "provenance", + "git_blob": "5ce4fa86af1d5487f9a639acdc9fa0177c76c192", + "sha256": "ca0be421d5cb1835a8814685907db78a7a3ea24b7e1e474f3038c87b0e46498e" + }, + { + "path": "research/transfer-metric-error-bound/README.md", + "usage": "provenance", + "git_blob": "d0642b7857a1e6f14517f366ef9eade202a23a3d", + "sha256": "60d86e24f2efafe4e2e3600a7e8a49b6ce5f45d4bf3892d84f1f48bb475c6d9d" + } + ] +} diff --git a/research/transfer-transient-leakage/TASK.json b/research/transfer-transient-leakage/TASK.json new file mode 100644 index 0000000000..848e443625 --- /dev/null +++ b/research/transfer-transient-leakage/TASK.json @@ -0,0 +1,126 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 8, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "original_card": { + "id": "formal-interface-lemma", + "question": "Can one uncovered interface implication be formalized with exact caller and certificate bindings?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/gate-operand-parity-lean/README.md", + "research/staged544-certified-endpoint/README.md", + "research/unconditional-batched-crt/README.md" + ], + "methods": [ + "Formalize a missing boundary lemma identified by the selected review.", + "Audit a formal theorem-to-certificate binding independently." + ], + "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.", + "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse." + }, + "first_experiment": "Write one missing statement with quantified hypotheses, actual caller and existing coverage. A compact-switch lemma is a candidate only after its mathematical contract is reviewed. Establish a bounded proof plan before a separately budgeted proof-assistant build; do not rerun large Lean jobs as orientation.", + "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.", + "allowed_variations": [ + "Narrow to one formal lemma or one theorem-to-certificate binding." + ], + "scope_change_triggers": [ + "Formalizing already-covered arithmetic and claiming the full multiplication theorem." + ], + "overlap_terms": [ + "hyperplane end", + "formal interface", + "Lean binding", + "3807", + "3857", + "4100", + "gate-operand-parity-lean", + "staged544-certified-endpoint", + "unconditional-batched-crt" + ], + "existing_checks": [ + { + "scope": "PR #3807: scoped gate-operand parity formalization.", + "evidence": "research/gate-operand-parity-lean/README.md", + "remaining": "Exact theorem-to-caller binding and genuinely uncovered interface lemmas.", + "status": "author-checked", + "source_commit": "4c3530f42a6abcc48e7a6bcffd6c901911dc8269", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #3857: certified real-power moment/endpoint arithmetic.", + "evidence": "research/staged544-certified-endpoint/README.md", + "remaining": "Uniform algorithmic implications, not another endpoint digit.", + "status": "author-checked", + "source_commit": "ef4315b8caa605e47a2515004845eb2d2ed71a86", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4100: compact-switch formalization proposed as future validation.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Audit the statement and assumptions before a formal proof campaign.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "changed", + "actual_scope": "A written uniform physical operator-error certificate from a contracting transient virtual block, with a sharp family having no common whole-table contraction metric in its fixed representation.", + "scope_change_reason": "The task changes from a selected formal-kernel/caller binding to the uniform-approximation opening of zxv PR5441. This is an enabling numerical-interface side result with exact finite corroboration; no actual selected caller is bound.", + "bottleneck_link": "A complete changed consumer needs uniform precision evidence. The new certificate bounds full physical errors without a growing payload-dimension factor and admits a family outside the predecessor whole-table metric test. Native delivery and recovery funding remain unproved.", + "budget_minutes": 60, + "stop_rule": "Stop at the first proved uniform certificate and exact separation, or publish a precise negative handoff if that test fails.", + "outcome": "completed", + "evidence": "PROOF.md and verify.py; the direct replay emits a generated SHA256-bound receipt.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can one actual consumer complete residual satisfy this triangular contract?", + "why_it_matters": "A source-specific bound could support a precision decision.", + "first_step": "Extract every role/version block and prove the exact lower-left zero before searching for block metrics.", + "blocked_by": "A complete extracted residual, physical access and an independently justified recovery tolerance are missing." + }, + { + "question": "Can a paid physical implementation preserve the splitting without feedback or omitted returns?", + "why_it_matters": "The virtual-state representation does not price a supplier.", + "first_step": "Specify one literal local operator and charge preparation, use and cleanup.", + "blocked_by": "No physical realization or complete recursive invoice is supplied." + } + ], + "predecessors": [ + { + "pr": 5441, + "author": "zxv", + "head": "11fedb46fa199283f78282187c10aea432d8b0bb", + "use": "Question source and fixed physical transfer contract; cited, not replayed." + }, + { + "pr": 5451, + "author": "aliromman", + "head": "d2502d83b1b615b02ca3753b8567bd31afe71dd8", + "use": "Whole-table sufficient metric certificate and coherent physical-norm argument; cited, not replayed." + } + ], + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19375359", + "environment": { + "python": "3.12.15", + "dependencies": "standard library only" + }, + "overlap": { + "checked_at_utc": "2026-11-03T14:00:00Z", + "canonical_main": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "scope": "Live latest 100 open PR bodies before claim and commit, latest 200 account PRs, recent handoffs and active Discussions, local reservations, source-specific account searches, main README and merged general-form searches. The broader helper has complete pagination for 572 open PRs at 13:54 UTC and 6,637 Discussion records at 13:55 UTC, but only 122 of 8,917 local note records materialized. The targeted cached scan matches only the two predecessor packages and their metadata. PR6184 takes a different cut-spectrum question from PR5441; it is the only identified recent account contribution using PR5441 as its question source. Canonical main was fetched again before publication and remained unchanged.", + "limits": "Arbitrary historical diffs, sparse historical notes and unpublished work are not exhaustively covered." + } +} diff --git a/research/transfer-transient-leakage/VERIFY.json b/research/transfer-transient-leakage/VERIFY.json new file mode 100644 index 0000000000..d1e7c86ffc --- /dev/null +++ b/research/transfer-transient-leakage/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 sharp-word norms, complete physical operator bounds, independent PSD oracle, no-common-metric equations, role/coherence and domain rejection controls, generated file-hash receipt." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact sharp-word norms, complete physical operator bounds, independent PSD oracle, no-common-metric equations, role/coherence and domain rejection controls, generated file-hash receipt." + } + ] +} diff --git a/research/transfer-transient-leakage/verify.py b/research/transfer-transient-leakage/verify.py new file mode 100644 index 0000000000..3e88aae1be --- /dev/null +++ b/research/transfer-transient-leakage/verify.py @@ -0,0 +1,341 @@ +#!/usr/bin/env python3 +"""Exact bounded corroboration of the transient-leakage theorem.""" + +from dataclasses import dataclass, replace +from fractions import Fraction as Q +from hashlib import sha256 +from itertools import combinations, permutations, product +import json +from pathlib import Path + + +Matrix = tuple[tuple[Q, ...], ...] +FILES = ("PROOF.md", "README.md", "SOURCES.json", "TASK.json", "VERIFY.json", "verify.py") + + +def require(condition: bool, message: str) -> None: + if not condition: + raise ValueError(message) + + +def matrix(rows) -> Matrix: + require(1 <= len(rows) <= 64, "row capacity") + width = len(rows[0]) + require(1 <= width <= 64, "column capacity") + require(all(len(row) == width for row in rows), "rectangular matrix") + return tuple(tuple(Q(x) for x in row) for row in rows) + + +def identity(n: int) -> Matrix: + return matrix([[int(i == j) for j in range(n)] for i in range(n)]) + + +def transpose(a: Matrix) -> Matrix: + return tuple(zip(*a)) + + +def multiply(a: Matrix, b: Matrix) -> Matrix: + require(len(a[0]) == len(b), "matrix product shape") + columns = transpose(b) + return matrix([[sum((x * y for x, y in zip(row, col)), Q(0)) + for col in columns] for row in a]) + + +def scale(c: Q, a: Matrix) -> Matrix: + return matrix([[c * x for x in row] for row in a]) + + +def add(a: Matrix, b: Matrix, sign: int = 1) -> Matrix: + require((len(a), len(a[0])) == (len(b), len(b[0])), "matrix sum shape") + return matrix([[x + sign * y for x, y in zip(ar, br)] + for ar, br in zip(a, b)]) + + +def kron(a: Matrix, b: Matrix) -> Matrix: + return matrix([[x * y for x in ar for y in br] for ar in a for br in b]) + + +def sandwich(a: Matrix, p: Matrix) -> Matrix: + return multiply(transpose(a), multiply(p, a)) + + +def psd(a: Matrix, strict: bool = False) -> bool: + """Symmetric Schur elimination, including the zero-diagonal case.""" + require(len(a) == len(a[0]), "square PSD input") + require(a == transpose(a), "symmetric PSD input") + b = [list(row) for row in a] + for i in range(len(b)): + pivot = b[i][i] + if pivot < 0 or (strict and pivot == 0): + return False + if pivot == 0: + if any(b[i][j] != 0 for j in range(i + 1, len(b))): + return False + continue + for j in range(i + 1, len(b)): + for k in range(j, len(b)): + value = b[j][k] - b[j][i] * b[i][k] / pivot + b[j][k] = value + b[k][j] = value + return True + + +@dataclass(frozen=True) +class Certificate: + local_dimension: int + active: Matrix + leakage: Matrix + transient: Matrix + active_metric: Matrix + transient_metric: Matrix + left: Matrix + right: Matrix + rho: Q + delta: Q + left_squared: Q = Q(1) + right_squared: Q = Q(1) + + +def validate(c: Certificate) -> None: + d = c.local_dimension + a, b = len(c.active_metric), len(c.transient_metric) + require(1 <= d <= 3 and 1 <= a <= 3 and 1 <= b <= 3, "certificate capacity") + require(0 <= c.rho < 1 and c.delta >= 0, "rate domain") + require(c.left_squared >= 0 and c.right_squared >= 0, "boundary domain") + for value, rows, cols in ((c.active, d*a, d*a), (c.leakage, d*a, d*b), + (c.transient, d*b, d*b), (c.active_metric, a, a), + (c.transient_metric, b, b), (c.left, len(c.left), a), + (c.right, b, len(c.right[0]))): + require(len(value) == rows and all(len(row) == cols for row in value), "certificate shape") + require(len(c.left) <= 3 and len(c.right[0]) <= 3, "role capacity") + require(psd(c.active_metric, True) and psd(c.transient_metric, True), "positive metrics") + pa = kron(identity(d), c.active_metric) + pb = kron(identity(d), c.transient_metric) + require(psd(add(pa, sandwich(c.active, pa), -1)), "active contraction") + require(psd(add(scale(c.rho**2, pb), sandwich(c.transient, pb), -1)), "transient contraction") + require(psd(add(scale(c.delta**2, pb), sandwich(c.leakage, pa), -1)), "coherent leakage") + require(psd(add(scale(c.left_squared, c.active_metric), + multiply(transpose(c.left), c.left), -1)), "complete left boundary") + require(psd(add(scale(c.right_squared, identity(len(c.right[0]))), + sandwich(c.right, c.transient_metric), -1)), "complete right boundary") + + +def block(a: Matrix, y: int, x: int, rows: int, cols: int) -> Matrix: + return matrix([row[x*cols:(x+1)*cols] for row in a[y*rows:(y+1)*rows]]) + + +def transfer(c: Certificate, y: int, x: int) -> Matrix: + a, b = len(c.active_metric), len(c.transient_metric) + aa = block(c.active, y, x, a, a) + cc = block(c.leakage, y, x, a, b) + dd = block(c.transient, y, x, b, b) + return matrix([aa[i] + cc[i] for i in range(a)] + + [(Q(0),)*a + dd[i] for i in range(b)]) + + +def literal_endpoint(c: Certificate, width: int) -> Matrix: + require(1 <= width <= 4, "literal width capacity") + a, b = len(c.active_metric), len(c.transient_metric) + words = tuple(product(range(c.local_dimension), repeat=width)) + p, q = len(c.left), len(c.right[0]) + result = [[Q(0)] * (q * len(words)) for _ in range(p * len(words))] + for yi, ys in enumerate(words): + for xi, xs in enumerate(words): + value = identity(a+b) + for y, x in zip(ys, xs): + value = multiply(value, transfer(c, y, x)) + corner = matrix([row[a:] for row in value[:a]]) + endpoint = multiply(c.left, multiply(corner, c.right)) + for i in range(p): + for j in range(q): + result[i*len(words)+yi][j*len(words)+xi] = endpoint[i][j] + return matrix(result) + + +def bound(c: Certificate, width: int) -> Q: + require(1 <= width <= 64, "bound width capacity") + return c.delta * (1-c.rho**width) / (1-c.rho) + + +def sharp_certificate(rho: Q, delta: Q) -> Certificate: + return Certificate(2, identity(2), matrix([[delta, 0], [0, -delta]]), + scale(rho, identity(2)), identity(1), identity(1), + identity(1), identity(1), rho, delta) + + +def coupled_certificate(weighted: bool) -> Certificate: + a = matrix([[0, 1, 0, 0], [-1, 0, 0, 0], + [0, 0, 1, 0], [0, 0, 0, -1]]) + d = matrix([[0, 0, 1, 0], [0, 0, 0, -1], + [0, 1, 0, 0], [1, 0, 0, 0]]) + cc = matrix([[0, 0, 0, 1], [0, 0, 1, 0], + [0, 1, 0, 0], [1, 0, 0, 0]]) + sa = matrix([[2, 0], [0, 1]]) if weighted else identity(2) + ia = matrix([[Q(1, 2), 0], [0, 1]]) if weighted else identity(2) + sd = matrix([[1, 0], [0, 3]]) if weighted else identity(2) + ii = matrix([[1, 0], [0, Q(1, 3)]]) if weighted else identity(2) + return Certificate(2, multiply(kron(identity(2), ia), multiply(a, kron(identity(2), sa))), + scale(Q(1, 32), multiply(kron(identity(2), ia), multiply(cc, kron(identity(2), sd)))), + scale(Q(1, 2), multiply(kron(identity(2), ii), multiply(d, kron(identity(2), sd)))), + sandwich(sa, identity(2)), sandwich(sd, identity(2)), + sa, ii, Q(1, 2), Q(1, 32)) + + +def determinant(a: Matrix) -> Q: + n = len(a) + require(n <= 3, "determinant oracle capacity") + result = Q(0) + for perm in permutations(range(n)): + inversions = sum(perm[i] > perm[j] for i in range(n) for j in range(i+1, n)) + term = Q((-1)**inversions) + for i in range(n): + term *= a[i][perm[i]] + result += term + return result + + +def principal_minor_oracle(a: Matrix) -> bool: + for k in range(1, len(a)+1): + for indices in combinations(range(len(a)), k): + minor = matrix([[a[i][j] for j in indices] for i in indices]) + if determinant(minor) < 0: + return False + return True + + +def check_psd_oracle() -> int: + count = 0 + for values in product((-1, 0, 1), repeat=6): + x, y, z, u, v, w = values + a = matrix([[x, y, z], [y, u, v], [z, v, w]]) + require(psd(a) == principal_minor_oracle(a), "independent PSD oracle") + count += 1 + require(count == 729, "PSD domain completeness") + return count + + +def check_sharp_words() -> dict[str, int]: + counts = {"families": 0, "word_endpoints": 0, "width_norms": 0} + for rho in (Q(0), Q(1, 4), Q(1, 2), Q(3, 4)): + for delta in (Q(1, 8), Q(1, 1024)): + c = sharp_certificate(rho, delta) + validate(c) + counts["families"] += 1 + for width in range(1, 13): + maximum = Q(0) + for word in product((0, 1), repeat=width): + value = Q(0) + for bit in word: + value = rho*value + delta*(1-2*bit) + maximum = max(maximum, abs(value)) + counts["word_endpoints"] += 1 + require(maximum == bound(c, width), "sharp full diagonal norm") + counts["width_norms"] += 1 + return counts + + +def check_literal_operators() -> dict[str, int]: + fixtures = [sharp_certificate(rho, Q(1, 8)) for rho in (Q(0), Q(1, 2), Q(3, 4))] + fixtures.extend((coupled_certificate(False), coupled_certificate(True))) + mixed = replace(sharp_certificate(Q(1, 2), Q(1, 8)), + active=matrix([[Q(3, 5), Q(4, 5)], [-Q(4, 5), Q(3, 5)]]), + leakage=matrix([[0, Q(1, 8)], [Q(1, 8), 0]])) + fixtures.append(mixed) + counts = {"certificates": len(fixtures), "complete_matrices": 0, "physical_entries": 0} + for c in fixtures: + validate(c) + for width in range(1, 5): + e = literal_endpoint(c, width) + squared = c.left_squared*c.right_squared*bound(c, width)**2 + require(psd(add(scale(squared, identity(len(e[0]))), + multiply(transpose(e), e), -1)), "complete operator error") + counts["complete_matrices"] += 1 + counts["physical_entries"] += len(e)*len(e[0]) + for width in range(1, 5): + require(literal_endpoint(fixtures[3], width) == literal_endpoint(fixtures[4], width), + "weighted similarity preserves every endpoint entry") + aa = block(fixtures[3].active, 0, 0, 2, 2) + bb = block(fixtures[3].active, 1, 1, 2, 2) + require(multiply(aa, bb) != multiply(bb, aa), "noncommuting virtual fixture") + return counts + + +def check_metric_obstruction() -> int: + """Check the two forced null-row equations in an independent finite grid.""" + count = 0 + for rho in (Q(0), Q(1, 4), Q(1, 2), Q(3, 4)): + for delta in (Q(1, 8), Q(1, 1024)): + for x in range(1, 5): + z = Q(x)*delta/(1-rho) + metric = matrix([[x, z], [z, 1+z*z/Q(x)]]) + plus = matrix([[1, delta], [0, rho]]) + minus = matrix([[1, -delta], [0, rho]]) + kp = add(metric, sandwich(plus, metric), -1) + km = add(metric, sandwich(minus, metric), -1) + require(psd(metric, True), "obstruction positive metric") + require(kp[0][0] == km[0][0] == 0, "preserved active eigenvector") + require(kp[0][1] == 0 and km[0][1] == 2*x*delta, "incompatible null rows") + require(psd(kp), "first sign really is contractive in this metric") + require(not psd(km), "second sign rejects first-sign metric") + count += 1 + return count + + +def check_rejections() -> list[str]: + good = sharp_certificate(Q(1, 2), Q(1, 8)) + cases = ( + ("rho-one", replace(good, rho=Q(1))), + ("negative-rho", replace(good, rho=Q(-1, 2))), + ("negative-delta", replace(good, delta=Q(-1))), + ("singular-metric", replace(good, active_metric=matrix([[0]]))), + ("indefinite-metric", replace(good, transient_metric=matrix([[-1]]))), + ("active-growth", replace(good, active=scale(Q(2), identity(2)))), + ("transient-growth", replace(good, rho=Q(1, 4))), + ("understated-leakage", replace(good, delta=Q(1, 16))), + ("coherent-cross-input", replace(good, leakage=matrix([[Q(1, 8), Q(1, 8)], [0, 0]]))), + ("omitted-left-role", replace(good, left=matrix([[1], [1]]))), + ("omitted-right-role", replace(good, right=matrix([[1, 1]]))), + ("bad-shape", replace(good, leakage=identity(1))), + ("capacity", replace(good, local_dimension=4)), + ) + rejected = [] + for name, bad in cases: + try: + validate(bad) + except ValueError: + rejected.append(name) + else: + raise ValueError("accepted invalid certificate: " + name) + require(len(rejected) == len(cases), "rejection inventory") + return rejected + + +def source_bindings() -> dict[str, str]: + root = Path(__file__).resolve().parent + inventory = tuple(root.iterdir()) + require(len(inventory) == len(FILES), "package inventory") + require({p.name for p in inventory} == set(FILES), "package filenames") + bindings = {} + for name in FILES: + path = root / name + require(path.is_file() and not path.is_symlink(), "regular package file") + require(path.stat().st_size <= 131072, "source size capacity") + bindings[name] = sha256(path.read_bytes()).hexdigest() + return bindings + + +def main() -> None: + report = {"claim_type": "scoped proof with finite exact corroboration", + "psd_oracle_matrices": check_psd_oracle(), + "sharp_family": check_sharp_words(), + "literal_operators": check_literal_operators(), + "metric_obstruction_fixtures": check_metric_obstruction(), + "rejected_certificates": check_rejections(), + "uniform_example": {"rho": "1/2", "delta": "1/1024", "supremum_error": "1/512"}, + "source_sha256": source_bindings(), + "status": "PASS_TRANSFER_TRANSIENT_LEAKAGE"} + print(json.dumps(report, indent=2, sort_keys=True)) + + +if __name__ == "__main__": + main()