Prove sharp uniform error from transient transfer leakage (no κ)

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.

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.

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"
+    }
+  ]
+}