Prove sharp sqrt(|G|) prefix-encoder metric loss (no new κ)

research/prefix-encoder-metric-loss/PROOF.md

@@ -0,0 +1,132 @@
+# The sharp boundary loss of the prefix encoder
+
+This scoped proof was produced by Nick Petalas. Apache-2.0.
+
+Let G be any finite group, with identity e and order q. The physical column
+alphabet and virtual state space are both G. All vector spaces in this proof
+are complex Hilbert spaces with their coordinate inner products. Define
+
+    T[y,x]_(a,b) = 1 if y = a x and b = y, and 0 otherwise,
+    F = e_e*,       B = sum_(b in G) e_b.
+
+For every positive width f the physical endpoint is
+
+    E_f[Y,X] = F T[y_1,x_1] ... T[y_f,x_f] B.
+
+This uses the fixed physical-table convention of zxv's [PR5441](https://github.com/CrocSwap/integer-mult-bounds/pull/5441).
+For G=C2 it is the standard prefix-XOR encoder in that package. We use the
+table definition, not any claimed physical implementation or paid cost.
+
+## Claim and certificate being optimized
+
+The endpoint E_f is a permutation matrix, so ||E_f||_op=1 at every positive f.
+For the following specific sufficient certificate, however, the least uniform
+squared bound is exactly q. This remains true after grouping any fixed positive
+number k of columns and after any fixed invertible change of virtual basis.
+
+The certificate is Ali Romman's [PR5451](https://github.com/CrocSwap/integer-mult-bounds/pull/5451)
+metric criterion. Write L_k for the full local operator whose block from physical
+input X to output Y is T[y_1,x_1] ... T[y_k,x_k]. It asks for a positive definite
+Hermitian P and nonnegative scalars A,H,c, with c<=1, satisfying
+
+    F*F <= A P,     B* P B <= H,
+    L_k* (P tensor I_(q^k)) L_k <= c (P tensor I_(q^k)).
+
+The tensor factors here are ordered virtual then physical. Permuting both
+sides gives exactly the source's physical-then-virtual block convention.
+The resulting bound at f=k m is A H c^m. Its uniform positive-m bound is
+A H c. The theorem below optimizes precisely these inequalities. It neither
+asserts that all uniform bounds have this form nor alleges an error in the
+source's sufficient theorem.
+
+## 1. The endpoint and local operator are unitary
+
+For an initial state a and input X=(x_1,...,x_k), the only surviving path is
+
+    y_j = a x_1 ... x_j,      b = y_k.
+
+With a=e and the final state summed by B, E_f is the prefix-product map.
+Its inverse is x_1=y_1 and x_j=y_(j-1)^(-1) y_j for j>=2. Thus it is a
+permutation on G^f, including for noncommutative G.
+
+The direction of the virtual indices matters. As an operator L_k, the input
+virtual state is the terminal b, and the output virtual state is a.
+For each input (b,X), set a=b (x_1 ... x_k)^(-1), then form the unique Y above.
+This defines one output (a,Y). Conversely, (a,Y) determines X by successive
+group differences and determines b=y_k. Therefore L_k is itself a permutation
+matrix on q^(k+1) coordinates. In particular it is unitary.
+
+## 2. A contractive positive metric is scalar
+
+Put W=P tensor I_(q^k). Its trace is positive. Since L_k is unitary,
+
+    Tr(L_k* W L_k) = Tr(W).
+
+The contraction inequality and c<=1 imply Tr(W)<=c Tr(W), hence c=1.
+The positive semidefinite difference W-L_k* W L_k has trace zero, so it is zero.
+Equivalently, L_k preserves the full metric W exactly.
+
+Consider two input coordinates (b,X) and (b',X) with the same physical X
+and distinct b,b'. Their output physical words Y,Y' are distinct because their
+last letters are b,b'. Consequently
+
+    (L_k* W L_k)_((b,X),(b',X)) = 0,
+    W_((b,X),(b',X)) = P_(b,b').
+
+Metric invariance forces every off-diagonal entry of P to vanish, including
+its imaginary part. On a diagonal coordinate (b,X), invariance then says
+
+    P_(b,b) = P_(a,a),    a=b (x_1 ... x_k)^(-1).
+
+At every k>=1 the product x_1 ... x_k ranges over all G. Thus all diagonal
+entries agree. Positive definiteness gives P=t I_q with t>0. Conversely every
+such metric is preserved by the permutation L_k. This characterizes all
+feasible positive metrics, rather than searching a finite subset of them.
+
+## 3. The exact optimum is q
+
+For P=t I_q, the left inequality forces A>=1/t by evaluating it on e_e.
+The right inequality forces H>=q t because B has q unit entries. Thus
+
+    A H c >= (1/t) (q t) = q.
+
+Equality is attained at P=t I_q, A=1/t, H=q t, c=1. Hence the least certified
+squared bound is q, although the actual squared operator norm is one.
+The multiplicative loss in operator norm is exactly sqrt(q). It persists at
+every fixed blocking length. For a residual epsilon E_f with epsilon nonzero,
+the same argument gives the least squared bound q |epsilon|^2.
+
+## 4. A virtual basis change cannot remove the loss
+
+Let S be any invertible complex q-by-q matrix, and set
+
+    T'[y,x]=S^(-1) T[y,x] S,    F'=F S,    B'=S^(-1) B.
+
+Products telescope at every block length. A certificate for the primed table
+with metric P' is exactly a certificate for the original table with
+P=S^(-*) P' S^(-1), with the same A,H,c. Congruence by an invertible matrix
+preserves positive definiteness and semidefinite order in both directions.
+All feasible primed metrics are therefore P'=t S* S, and the optimum is q.
+This permits arbitrary conditioning of S. It is an algebraic statement, not
+a claim that a basis change has zero physical or precision cost.
+
+## Consequence and scope
+
+For a desired norm tolerance tau, an error epsilon E_f can satisfy the actual
+bound |epsilon|<=tau while this certificate demands sqrt(q)|epsilon|<=tau.
+Searching more positive metrics, or blocking more columns within this same
+representation and criterion, cannot close that gap. A useful next method
+must retain boundary correlation, use a different representation, or change
+the certificate. Those possibilities are not excluded by this proof.
+
+The example is a complete algebraic physical endpoint, not a materialized
+native/tape implementation. It supplies no paid supplier, dirty-workspace
+program, compiler closure, recovery budget, new kappa or multiplication
+theorem. No claim is made about arbitrary transfer tables, augmented virtual
+spaces, width-dependent metrics, or position-dependent metric sequences.
+
+The trace and congruence arguments and weighted operator norms are classical.
+The additional result is this exact optimum, its positive-metric rigidity,
+and its permanence under blocking and virtual gauges for the named encoder.
+Finite checks in verify.py corroborate the proof and do not replace its
+universal quantifiers or constitute formal proof-kernel acceptance.

research/prefix-encoder-metric-loss/README.md

@@ -0,0 +1,105 @@
+# A sharp boundary loss in uniform transfer-metric certificates
+
+This scoped written proof with exact finite corroboration was produced by Nick Petalas.
+For the standard prefix-product encoder on any finite group G of order q,
+every complete physical endpoint is unitary. Its true operator norm is one.
+The least uniform operator-norm bound obtainable from Ali Romman's
+[PR5451](https://github.com/CrocSwap/integer-mult-bounds/pull/5451) fixed positive
+transfer-metric criterion is exactly sqrt(q). Every fixed positive blocking
+length and every invertible complex virtual basis change retains that loss.
+
+The new [proof](PROOF.md) characterizes all feasible metrics. The local blocked
+operator is a permutation, so its contraction inequality forces c=1 and exact
+metric invariance. Physical output separation then forces P=t I. The two
+boundary inequalities have product at least q, with an attaining certificate.
+This is a sharp limit of that sufficient criterion, not a counterexample to
+its theorem. No new kappa or selected-frontier change is claimed.
+
+For the prefix-XOR example in zxv's
+[PR5441](https://github.com/CrocSwap/integer-mult-bounds/pull/5441), the loss is
+sqrt(2). Searching more positive metrics or blocking more columns cannot make
+that certificate sharp. A boundary-aware method or a changed representation
+is a separate question.
+
+## Evidence and reproduction
+
+The independent local implementation imports no predecessor executable. It
+checks complete endpoint entries by literal one-column contraction, complete
+blocked local permutations, exact ranks of the metric-invariance equations,
+explicit negative quadratic-form witnesses for non-scalar real and complex
+metrics, and rational gauge certificates. Six groups include noncommutative S3.
+The universal statement rests on the written proof, not extrapolation from
+these finite groups or block lengths. Generated stdout receipts bind all seven
+package files and both exact source-document inputs by SHA256.
+
+The fixed replay enumerates 21 blocked tables and 787 literal blocked paths,
+85,873 metric-commutator entries, 17,792 complete endpoint entries, 45 negative
+metric witnesses and 12 gauge certificates. Its 63 controls comprise seven
+invalid group/block cases, a changed terminal boundary, an imaginary
+off-diagonal metric and 54 strict boundary/rate underclaim witnesses.
+
+From the repository root, use CPython 3.12 and the standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/prefix-encoder-metric-loss/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/prefix-encoder-metric-loss/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/prefix-encoder-metric-loss
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/prefix-encoder-metric-loss --check-source-history
+```
+
+Other machines may substitute their CPython 3.12 interpreter. The verifier
+prints `PASS_PREFIX_ENCODER_METRIC_LOSS` in its JSON receipt and writes no files.
+Both warning-strict modes are registered. The source-history check is a
+publication integrity check, separate from the mathematics. A Git-free export
+needs this package and the two inputs declared in VERIFY.json.
+
+## Scope and credit
+
+Ali Romman supplies the sufficient metric criterion and its stated limitations.
+zxv supplies the concrete fixed-transfer contract and prefix-XOR example, with
+the retained weighted-automata, matrix-product, native and phase lineage.
+Trace invariance, congruence and weighted operator norms are classical. The
+additional result is the sharp optimized loss and its metric rigidity under
+blocking and virtual gauges. No predecessor result is audited or replayed.
+Source documents, Git blobs and hashes are pinned in [SOURCES.json](SOURCES.json).
+New work is Apache-2.0. Independent human and formal proof-kernel review are unclaimed.
+
+The `formal-interface-lemma` card is explicitly changed to this certificate
+obstruction. It explains a limitation of one possible route to uniform error
+control, without discharging a selected framework assumption. The result
+fixes this representation and certificate. Larger or different virtual
+representations, position-dependent metrics and boundary-aware certificates
+remain open. Physical synthesis, dirty restoration, native costs, the complete
+paid invoice, compiler closure, tape/precision and exact recovery are outside
+scope. No selected cold replay, native suite, Lean or Docker build was run.
+
+## Open next questions
+
+1. Can a boundary-aware finite certificate attain norm one for this encoder
+   while still controlling small complete residuals? Start with the reachable
+   boundary subspaces and retain coherent physical input sums. The obstruction
+   here only applies to the single fixed positive metric criterion.
+2. Does another finite transfer representation of the same endpoint remove
+   the loss? Start by allowing a changed virtual dimension and explicit boundary
+   maps. An invertible basis change in the present dimension is already covered.
+
+## Verifier constraints
+
+All functions have fewer than sixty physical lines, with structured iterative
+control flow and explicit exception checks that remain active under optimization.
+Groups have at most six elements; blocked local permutations have at most 216
+coordinates; exact constraint elimination has at most 36 variables and 2592
+distinct relations. Dense gauge matrices have at most 36 rows. Fixed fixture
+loops and these caps bound the complete run. The verifier has no subprocess,
+network or input-file argument. Source and package files are capped at one MB.
+
+Power of Ten rule 3 deviation: CPython allocates managed integers, Fractions and
+collections during this bounded one-shot check. The fixed domains above bound
+live data; no unbounded search or external resource is retained. Both registered
+modes exercise those domains. A fixed-allocation implementation would require
+a different arithmetic runtime. Rule 8/9 deviation: isolated execution uses one
+explicit file-based import of the package-local encoder.py. The only dynamic
+target is that fixed sibling file, which is included in the receipt and committed
+source. No external plugin or generated code is loaded. Reassess these controls
+before adding an external frontend. Warning-strict execution and AST compilation
+are the local diagnostics; no external static analyzer is claimed.

research/prefix-encoder-metric-loss/SOURCES.json

@@ -0,0 +1,30 @@
+{
+  "schema_version": 1,
+  "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419",
+  "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/README.md",
+      "usage": "input",
+      "git_blob": "5ce4fa86af1d5487f9a639acdc9fa0177c76c192",
+      "sha256": "ca0be421d5cb1835a8814685907db78a7a3ea24b7e1e474f3038c87b0e46498e"
+    },
+    {
+      "path": "research/transfer-metric-error-bound/README.md",
+      "usage": "input",
+      "git_blob": "d0642b7857a1e6f14517f366ef9eade202a23a3d",
+      "sha256": "60d86e24f2efafe4e2e3600a7e8a49b6ce5f45d4bf3892d84f1f48bb475c6d9d"
+    }
+  ]
+}