Extend the one-query carrier obstruction to every width below 2M

research/wide-one-query-threshold/PROOF.md

@@ -0,0 +1,136 @@
+# The full one-query width threshold
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+## Contract
+
+Let M be positive, let K be nonnegative, and let Q,N be invertible M by M
+matrices over a field. Both carrier inputs and all K helper coordinates are
+arbitrary and independent. The required complete endpoint is
+
+    C = [[Q-I, N], [Q, 0]],       T = C direct-sum I_K.
+
+The helper endpoint is the identity on its actual input. There is no promise
+that helpers start at zero. C is invertible: given outputs (a,b), first recover
+x=Q^-1 b and then y=N^-1(a-(Q-I)x).
+
+A single coordinate query J_W(U) acts by an arbitrary w by w matrix U on a
+chosen coordinate subset W of size w and by the identity on its coordinate
+complement. It has no cross blocks. W may meet several original banks. This
+grants at least as much freedom as a query restricted to one physical bank.
+The candidate factorization is
+
+    T G = F J_W(U),                                             (1)
+
+where F,G are invertible endpoints on all 2M+K coordinates. U is unrestricted;
+equation (1) would itself force it to be invertible.
+
+Fix positive support limits s,t. In each of the two carrier row blocks, every
+physical column of G has at most s nonzero entries, and every physical column
+of F has at most t. There is no sparsity restriction on helper row blocks.
+Assume the following separation property for each A in {Q,N}:
+
+    v != 0 and |supp(v)| <= s imply |supp(A v)| > t.             (2)
+
+## Theorem
+
+Under this contract every factorization (1) has
+
+    w >= 2M.                                                   (3)
+
+In particular no width M<w<2M is sufficient. The theorem holds for any finite
+K, any positions of queried coordinates, and any invertible endpoint helper
+blocks. It does not assume monomial endpoints or full-bank query alignment.
+
+### Proof
+
+For each j outside W, the query leaves the basis column e_j unchanged. Write
+the carrier components of G e_j as (g_0,g_1). Equation (1) says
+
+    (Q-I)g_0 + N g_1 = (F e_j)_0,
+               Q g_0 = (F e_j)_1.
+
+The support bounds and (2) first give g_0=0 from the bottom equation. The top
+equation then gives g_1=0. Thus G sends every unqueried coordinate basis
+vector into the helper coordinate subspace.
+
+Those 2M+K-w vectors are linearly independent because G is invertible. The
+helper subspace has dimension K. Consequently 2M+K-w<=K, proving (3).
+This is the complete new dimension step. In particular it does not use the
+older sufficient restriction w<=M. No endpoint or native tariff is inferred.
+
+## Complex unitary specialization
+
+For a unitary A with maximum entry modulus mu, the classical support
+uncertainty inequality is
+
+    |supp(v)| |supp(A v)| >= mu^-2       for v != 0.
+
+Indeed each output coordinate is bounded by mu sqrt(|supp(v)|) ||v||_2;
+summing over its support and using unitarity proves the inequality. Therefore
+(2) holds whenever
+
+    s t < min(mu_Q^-2, mu_N^-2).                                (4)
+
+This is a strict inequality. The theorem proves the combined necessary
+condition
+
+    w >= 2M   or   s t >= min(mu_Q^-2, mu_N^-2).                 (5)
+
+Ross Richardson's PR4057 supplies the native setting in which Q_f,N_f are
+unitary with mu_Q_f=mu_N_f=2^-f. Its native amplitudes and operator recipes are
+cited premises, not results checked again here. In that setting (5) becomes
+
+    w_f >= 2M_f   or   s_f t_f >= 4^f.                          (6)
+
+Thus the predecessor's support obstruction extends from queried widths at
+most M_f to every width below 2M_f. Under its support-doubling ADD contract,
+s_f<=2^a_G and t_f<=2^a_F, equation (6) also implies
+
+    w_f < 2M_f implies a_G+a_F >= 2f.
+
+The constant 2f is inherited. The new part is the complete width range on
+which that necessary condition applies.
+
+If the carrier endpoint blocks have fixed column-support bounds h_G,h_F,
+every f with 4^f>h_G h_F requires w_f>=2M_f. In particular a sum of at most
+h_G or h_F physical monomial terms in each such block has these bounds.
+This includes the predecessor's fixed finite uniform-tensor dictionaries
+whenever the stated carrier-block representation applies. Arbitrary growing
+helper dimensions do not change the dimension argument. Rectangular helper
+interfaces must still satisfy the explicit per-column bounds; a square-block
+dictionary is not automatically a representation theorem for those interfaces.
+
+## Exact boundaries
+
+The width threshold is sharp in the relaxed coordinate-query model. With
+F=G=I, take W to be all 2M carrier coordinates and U=C. Helpers remain exactly
+unchanged. For a nonmonomial unitary with mu<1 the support bounds s=t=1
+satisfy (4), so the lower threshold and this algebraic attainer coexist.
+This arbitrary 2M-dimensional query is not a native implementation, paid word
+or physical merger of two banks.
+
+The strictness of (4) is necessary. Let Q=N=H_4/2, where H_4 is the four by four
+Walsh sign matrix. Then mu^-2=4. Choose G=I, F=C and an empty query. Every
+carrier block column of F has support at most four; G's have support at most
+one. Equation (1) holds at s t=4 with w=0. Replacing < by <= would be false.
+
+Separation is necessary too. If Q=N=I, then C is the swap of the carriers.
+It is monomial. F=C, G=I and an empty query work with s=t=1. The finite checker
+executes these boundary examples exactly, including the rational unitary.
+
+## Attribution and limits
+
+The triangular carrier, untouched-column equations, support-uncertainty
+method, native four-flatness, and earlier w<=M statement are Ross Richardson's
+PR4057 at bf793d8739ad26f2aaba023de6bebca50fc67356. This contribution extends
+its width domain and states the sharp threshold in a relaxed coordinate-query
+contract. Rank-nullity and the uncertainty inequality are classical.
+
+There is no claim about a query on an arbitrary dense linear subspace,
+interleaved multiple queries, a changed carrier map, discarded helpers, free
+dense endpoint maps, or a rounded approximate endpoint. All such changes need
+their own proof. No native realization, stock, tape, precision, ownership,
+uniform compiler, supplier admission, new kappa, or complete multiplication
+theorem is supplied. The universal statement rests on this written proof;
+finite examples corroborate it and are not a formal proof-kernel check.

research/wide-one-query-threshold/README.md

@@ -0,0 +1,130 @@
+# A one-query obstruction up to the combined carrier width
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+Claim type: scoped written proof with exact finite corroboration. No new kappa.
+For the triangular carrier
+
+    C = [[Q-I,N],[Q,0]],       T = C direct-sum I_K,
+
+one coordinate query of width w, arbitrary restored dirty helpers and invertible
+endpoints with carrier-block column supports s,t must satisfy
+
+    w >= 2M   or   s t >= min(mu_Q^-2,mu_N^-2),
+
+when Q,N are M by M unitaries with maximum entry moduli mu_Q,mu_N.
+The general all-field version uses an explicit sparse-vector separation
+condition. [PROOF.md](PROOF.md) gives the full contract and proof.
+
+This extends Ross Richardson's [PR4057](https://github.com/CrocSwap/integer-mult-bounds/pull/4057)
+width regime from w<=M to every w<2M. In particular, merely widening one query
+into the range M<w<2M does not bypass that endpoint obstruction. Its native
+specialization has support threshold 4^f; under its ADD support contract the
+inherited floor of 2f endpoint ADDs applies throughout the larger width range.
+Neither the threshold 4^f nor the coefficient 2f is claimed as new.
+
+The new step is the dimension inequality 2M+K-w<=K after the predecessor's
+carrier-row vanishing argument. It permits arbitrary query-coordinate positions
+and unrestricted helper row blocks. At w=2M an arbitrary query on the combined
+carriers attains the algebraic width threshold. That attainer supplies no native
+query implementation or physical bank merger. An exact rational example shows
+why the support inequality in the obstruction must be strict.
+
+## Evidence and reproduction
+
+From the repository root, using the standard library on CPython 3.12:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/wide-one-query-threshold/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/wide-one-query-threshold/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/wide-one-query-threshold
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/wide-one-query-threshold --check-source-history
+```
+
+Substitute another host's Python 3.12 executable as needed. The direct checker
+prints a generated JSON receipt followed by `PASS_WIDE_ONE_QUERY_THRESHOLD`.
+The generic runner adds `PASS_REGISTERED_RESEARCH_PACKAGE`. Normal verification
+writes no files. Optional `--receipt /absolute/path/outside/checkout.json`
+writes the generated receipt with SHA256 hashes of all six package files,
+refuses an existing destination and rejects paths inside the checkout.
+
+The finite checks are newly written examples of the extended width contract,
+not a replay or audit of the predecessor's native matrices or certificate:
+
+- Every one of the 147,456 pairs of invertible monomial endpoints over F3 in
+  dimension four is tested for one fixed dense two-carrier map. The checker
+  computes the smallest coordinate set containing every nonidentity row and
+  column of F^-1 T G. Every pair requires all four coordinates.
+- All 50,304 permutation/active-coordinate-set pairs with M=2 and K=0,1,2
+  are enumerated. Untouched literal columns obstruct all 33,720 cases with
+  w<4, including 15,696 cases at the newly covered width w=3. For the 3,144
+  feasible active sets the checker constructs and checks the query with F=G.
+  No scaling choices are enumerated in this separate helper census.
+- The eight invertible fully nonzero two by two matrices over F3 give 64
+  ordered pairs Q,N. The checker constructs 960 queries of width at least
+  four with up to four helper coordinates, verifies their invertibility,
+  and executes all 6,400 arbitrary-input basis columns. Thirty-two nonzero
+  one-sparse input checks establish the small separation fixtures.
+- The rational unitary H4/2 checks 80 nonzero vectors from {-1,0,1}^4,
+  including 40 support-uncertainty equalities. Exact two-sided inverses and
+  literal query matrices verify the width-2M attainer, the support-equality
+  zero-query counterexample and a monomial zero-query control. Four malformed
+  query descriptors reject in both Python modes.
+
+The all-parameter claim is the written dimension proof. These finite checks
+corroborate it; they are not human acceptance or a formal proof-kernel result.
+
+## Scope, sources and credit
+
+Canonical base is `7c49fe32c55de02c2c873655c804b16e4c3fef0a`, priority revision 8,
+with selected PR6030 unchanged. The card's first baseline command passed with
+`PASS_RESEARCH_BASELINE_BINDINGS_ONLY`. This changes the card's scope to one
+consumer-width obstruction, rather than a completed supplier or invoice.
+The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19372332)
+records the question before the new finite work.
+
+[SOURCES.json](SOURCES.json) pins the predecessor proof and README at
+`bf793d8739ad26f2aaba023de6bebca50fc67356` as historical provenance. No
+predecessor executable or external scientific input is imported. Credit Ross
+Richardson for the carrier, untouched-column argument, support method, native
+amplitudes and prior w<=M result; icekylinx/PR531, Rohan Arun/kernel92,
+Clear1nsight/PR3987 and ToikY/PR4002 for the retained native/compiler and
+signed-lift lineage. Rank-nullity and support uncertainty are classical.
+Independent human and formal proof-kernel review are unclaimed.
+
+Live open/account PRs, recent handoffs and local reservations, all-main README
+searches for the object and general width formula, and merged-PR searches were
+checked. Sparse local overlap coverage is incomplete; arbitrary historical
+diffs and unpublished work are not covered. No literature-priority claim is
+made for the linear-algebra methods.
+
+The theorem requires exact helper return, coordinate queries, the stated
+carrier and sparse endpoint blocks. Dense active subspaces, multiple
+interleaved queries, discarded helpers, rounded execution and changed carrier
+maps are outside it. Rectangular helper dictionaries must actually satisfy
+the column-support bounds. Native realization, ownership, hosting, precision,
+tape work, compiler closure and a complete paid supplier bill remain unproved.
+No selected cold replay, Lean or Docker run is warranted or claimed.
+
+## Engineering constraints
+
+Power of Ten inspection covers this checker only. All functions stay below
+60 lines; loops have fixed domains with matrices at most eight by eight,
+384 monomial endpoint descriptors, 147,456 endpoint pairs and at most 720
+permutations in the helper loop. There is no recursion, project import,
+dynamic code loading or subprocess. Explicit exceptions keep invariants
+enabled under optimization. Python's managed arithmetic, iterators and
+collections allocate during the finite run, a rule-3 deviation; live storage
+is bounded by those domains and the six small source files. Allocator internals
+are not inspected. A variable-size implementation needs its own capacity
+review. Warning-strict normal and optimized replay supply interpreter
+diagnostics; local lint availability and results are recorded in the PR.
+
+## Open next questions
+
+Can a physically legal query of width at least 2M improve the complete matched
+caller bill? First specify one widened query bank, acquisition word, arbitrary
+dirty inputs and full restoration. Then price every operation. The relaxed
+attainer supplies neither a native implementation nor a favorable full invoice.
+This contribution stops at the width obstruction; it proposes no construction
+expansion. [TASK.json](TASK.json) records the same question and blocker.

research/wide-one-query-threshold/SOURCES.json

@@ -0,0 +1,32 @@
+{
+  "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/one-query-endpoint-scan/README.md",
+      "usage": "provenance",
+      "pin": "head:bf793d8739ad26f2aaba023de6bebca50fc67356:research/one-query-endpoint-scan/README.md",
+      "git_blob": "0ba9c46c33572f6427b2ada5b159259713d93e5d",
+      "sha256": "06ba0d8d577cd5945524650f8389fcb1563a31a2d00236534733b896d7f94e1c"
+    },
+    {
+      "path": "research/one-query-endpoint-scan/source/q4-pauli-fusion/ONE-QUERY-ENDPOINT-OBSTRUCTION.md",
+      "usage": "provenance",
+      "pin": "head:bf793d8739ad26f2aaba023de6bebca50fc67356:research/one-query-endpoint-scan/source/q4-pauli-fusion/ONE-QUERY-ENDPOINT-OBSTRUCTION.md",
+      "git_blob": "a8e5dadac865b99cb57c7d43f4ff11486bd042b5",
+      "sha256": "9ca2528303f5b47ed7e21f2446ac89aec16e5973a4716169a8dc4b3ad35c6118"
+    }
+  ]
+}