Prove restored dirty helpers preserve square-zero query capacity (no κ)

research/restored-dirty-query-capacity/PROOF.md

@@ -0,0 +1,171 @@
+# Restored dirty helpers do not increase square-zero query capacity
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+## 1. Statement and credited premise
+
+Let K be any field of characteristic two and let
+R = K[Q]/(Q^2-1). The symbol Q is a formal central involution.
+Fix n>0 target coordinates, h>=0 arbitrary dirty helper coordinates,
+k>=3 available paid calls, and a nonnegative integer rank cap r.
+Free gates are arbitrary constant matrices in GL_(n+h)(K).
+A paid gate is I+Q N, where N is constant, N^2=0, and rank(N)<=r.
+The complete required endpoint on every input is
+
+```text
+diag(Q I_n, I_h).
+```
+
+Thus every original helper value must return unchanged, without a promise
+on its value or correlations with the target inputs.
+Put m_k=2 floor((k-1)/2). The endpoint is possible with at most k calls iff
+
+```text
+n is even and n + ceil(n/m_k) <= k r.
+```
+
+Whenever feasible, its least total paid rank with at most k calls is
+n+ceil(n/m_k).
+Neither statement depends on h. Zero-rank calls may pad a shorter word.
+
+The new part is necessity for arbitrary h. Josie Elliston's
+[PR #6138](https://github.com/CrocSwap/integer-mult-bounds/pull/6138),
+`research/four-block-query-capacity-audit/README.md`, finding 5, supplies
+the workspace-free attaining construction. We use that theorem as a cited
+premise and extend its words by the identity on h helpers. We do not replay
+its computations or claim its construction. Its four-call theorem credits
+Nick Petalas #6122, its simplex credits Cinna Davis, its Gram framework
+credits Ali Romman #5617, and its source question credits Matarener #6114.
+
+## 2. Normalize to a projection, keeping every helper
+
+Set epsilon=Q+1, so epsilon^2=0 and R=K[epsilon]/(epsilon^2).
+For square-zero N,
+
+```text
+I+Q N = (I+N)(I+epsilon N).
+```
+
+Move the constant factors and free gates to one side, conjugating the N's
+by constant invertible matrices. Rank and square-zero are preserved.
+The constant part of the required endpoint is I, so the complete endpoint
+is equivalent to
+
+```text
+sum_(i=1)^k R_i = P,
+R_i^2=0,
+P=diag(I_n,0_h).
+```
+
+All products involving two epsilon terms vanish. Conversely, such a sum
+implements I+epsilon P by preceding each paid I+Q R_i with the free I+R_i.
+This equivalence keeps the whole arbitrary-input matrix, including both
+off-diagonal helper blocks. It does not discard helper information.
+
+Let r_i=rank(R_i) and S=sum r_i. Since a square-zero matrix has trace zero,
+trace(P)=n times 1_K=0, so n must be even.
+
+## 3. The projection Gram complement
+
+Factor R_i=U_i V_i with U_i injective and V_i surjective through K^(r_i).
+Then V_i U_i=0, since U_i(V_i U_i)V_i=R_i^2=0.
+Concatenate the U_i horizontally into U and the V_i vertically into V.
+Thus UV=P. Let
+
+```text
+X=VU on K^S,       Y=I_S+X,       d=S-n.
+```
+
+The call-diagonal blocks of X vanish, so Y_ii=I_(r_i).
+Although P is a projection, X need not be one. Instead,
+
+```text
+X^3=V P^2 U=V P U=X^2,
+Y^3=Y.
+```
+
+The fixed space of X has dimension n. Indeed, U and V restrict to inverse
+maps between ker(I_S+X) and im(P). For Xv=v, P(Uv)=Uv and VUv=v.
+For Pw=w, XVw=Vw and UVw=w. Therefore rank(Y)=S-n=d.
+
+Take a full-rank factorization Y=A B through K^d. Since Y^3=Y,
+injectivity of A and surjectivity of B give
+
+```text
+C=BA,             C^2=I_d.
+```
+
+In particular C is invertible. Partition A into call row blocks A_i
+and B into matching column blocks B_i. The call-diagonal equations give
+
+```text
+A_i B_i=I_(r_i),
+E_i=B_i A_i,      E_i^2=E_i,      rank(E_i)=r_i,
+sum E_i=C.
+```
+
+Consequently r_i<=d. When h=0, the old argument can take C=I_d.
+With dirty helpers, C can be a nonidentity involution I_d+Z with Z^2=0.
+Invertibility, rather than identity, is the property needed below.
+
+## 4. The rank bound for every call count
+
+If k is odd, sum r_i<=k d immediately gives
+
+```text
+(k-1) S >= k n,
+S >= n + ceil(n/(k-1)).
+```
+
+If k is even, characteristic two gives sum(I_d+E_i)=C.
+Each I_d+E_i has rank d-r_i, while C has rank d. Rank subadditivity yields
+
+```text
+d <= sum(d-r_i) = k d-S,
+(k-2) S >= (k-1) n,
+S >= n + ceil(n/(k-2)).
+```
+
+Together these say S>=n+ceil(n/m_k). Since S<=k r, the stated uniform-cap
+condition is necessary. The credited workspace-free construction proves
+sufficiency and equality for total rank. This finishes the scoped theorem.
+
+For example, four rank-two paid calls cannot twist six independent
+coordinates even when any number of arbitrary dirty helpers may be mixed
+into every call and must eventually return unchanged. The new conclusion
+is the independence from the helper count, not the predecessor's
+workspace-free numerical bound.
+
+## 5. A genuine nilpotent defect and the clean-helper boundary
+
+Write binary matrices as integer-coded rows, with the least significant
+bit the first column. The four three-by-three matrices
+
+```text
+(0,6,6), (6,6,6), (0,5,0), (7,7,0)
+```
+
+are square-zero rank-one matrices with sum diag(1,1,0). Their stacked
+X=VU is not idempotent, and the complement factor has C!=I but C^2=I.
+The verifier reconstructs these facts without treating the coded rows as
+a receipt. Thus replacing the predecessor's identity by a projection
+requires the new argument in section 3.
+
+Initialized clean helpers have a different contract. The two-by-two terms
+
+```text
+(2,0), (0,1), (3,3)
+```
+
+sum to I_2 and yield endpoint Q I_2. On (x,0) this twists one target and
+returns the zero helper, despite n=1 being odd. On (x,y) it also twists y.
+It therefore fails dirty restoration. The theorem does not cover a
+zero-initialized helper promise, discarded outputs, nonlinear controls,
+Q-dependent free gates, non-square-zero paid gates or approximate equality.
+
+This is an abstract query-capacity obstruction. Native implementation,
+physical basis-change costs, independent stage multipliers, storage,
+precision, a complete supplier invoice and the five selected framework
+assumptions remain outside the claim. No new kappa or complete
+multiplication theorem follows. The all-field proof is written mathematics;
+finite binary checks do not provide formal proof-kernel acceptance.

research/restored-dirty-query-capacity/README.md

@@ -0,0 +1,131 @@
+# Exact query capacity with restored dirty helpers
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+**Scoped proof with exact finite corroboration; no new kappa.** An arbitrary
+finite bank of restored dirty helpers cannot lower the square-zero query
+capacity in characteristic two. This answers the dirty-workspace part of
+Josie Elliston's [PR #6138](https://github.com/CrocSwap/integer-mult-bounds/pull/6138),
+second Open next question. Its workspace-free attaining theorem is a cited
+premise, not a replay target.
+
+Over any characteristic-two field K, let Q be a formal central involution.
+Free gates are constant invertible matrices. Each paid gate is I+Q N with
+N^2=0 and rank(N)<=r. There are n>0 independent targets and any h>=0
+independent dirty helpers. The full endpoint must be diag(Q I_n,I_h).
+For k>=3 available calls and m_k=2 floor((k-1)/2), feasibility is exactly
+
+```text
+n is even and n + ceil(n/m_k) <= k r.
+```
+
+Whenever feasible, the least total paid rank is n+ceil(n/m_k), independently of h.
+For example, adding restored dirty helpers cannot make four rank-two calls
+twist six independent targets. The same capacity without helpers was
+already proved by #6138; the new result is its invariance under arbitrary
+finite dirty workspace.
+
+[PROOF.md](PROOF.md) gives the all-field argument. Normalization replaces
+an identity endpoint by a projection P. The call Gram matrix X then only
+satisfies X^3=X^2. Factoring Y=I+X yields an invertible complement core C
+with C^2=I, rather than C=I. Its diagonal blocks still give idempotents.
+Rank subadditivity recovers the same even-call bound; a separate dimension
+count gives the odd-call bound. A nonidentity core occurs in the finite
+fixtures, so the identity-only predecessor argument cannot be reused
+without this step.
+
+## Evidence and reproduction
+
+From the repository root, with the interpreter used locally:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/restored-dirty-query-capacity/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/restored-dirty-query-capacity/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/restored-dirty-query-capacity
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/restored-dirty-query-capacity --check-source-history
+```
+
+Elsewhere substitute a CPython 3.12 path. Only the standard library is
+needed. The direct verifier emits `PASS_RESTORED_DIRTY_QUERY_CAPACITY`
+in a generated JSON receipt bound to the six package files' SHA256 hashes.
+It writes no files and imports no predecessor program.
+
+- A complete three-coordinate, four-call binary fixture uses two target
+  coordinates and one arbitrary restored dirty helper. Pair joins and a
+  separate direct scan of all 234,256 ordered four-tuples both find exactly
+  648 valid words. The new complement identities hold for each, including
+  all 288 nonidentity cores. Literal quotient-ring execution checks all
+  eight dirty inputs of each word, for 5,184 executions.
+- Padded dirty-helper fixtures exercise each call count from three through
+  eight, covering both parity branches of the new rank argument.
+- A separate complete two-pair minimization on four coordinates, two targets
+  and two dirty helpers, gives minimum total rank three for caps one and
+  two. It includes respectively 11,236 and 99,856 ordered pairs and retains
+  every pair-sum cost. It does not enumerate all ordered four-tuples in this
+  larger domain.
+- Four rejecting controls cover a non-square-zero summand with unchanged
+  total, the wrong complete endpoint, a nonprojection, and the enumeration
+  dimension limit. A literal clean-helper example shows why a zero-input
+  promise does not imply dirty restoration.
+
+The written proof, not these small fixtures, establishes arbitrary field,
+helper count and dimension. No predecessor counts were replayed as the
+contribution. [SOURCES.json](SOURCES.json) pins the source question and
+attainment theorem as historical provenance at canonical main
+`7c49fe32c55de02c2c873655c804b16e4c3fef0a`, priority revision 8.
+
+## Limits and expansion decision
+
+This theorem requires exact formal equality, constant free controls,
+square-zero paid terms, and restoration of every arbitrary helper input.
+Initialized clean helpers, discarded helper outputs, non-square-zero paid
+operations, nonlinear controls and approximation remain outside its scope.
+The clean-helper example in the proof can twist one target using three
+rank-one calls and a clean zero helper, while its full dirty endpoint fails.
+
+There is no physical multi-bank query, native alignment, charged basis
+implementation, stage chronology, complete signed invoice, compiler or
+precision/tape construction. The five selected framework assumptions are
+unchanged. No selected cold replay, Lean or Docker run, independent human
+review or formal proof-kernel acceptance is claimed.
+
+This closes the restored-dirty-workspace route in this model. Further
+construction work needs a changed hypothesis and a complete favorable
+physical bill. A larger search inside the same dirty model is unnecessary.
+The non-square-zero and initialized-clean alternatives remain open and
+are not assigned by this package.
+
+Power of Ten rule 3 has a managed-runtime deviation. Python allocates
+integers, tuples and dictionaries during verification. Scientific loops
+have fixed bounds: dimension at most four, at most 65,536 candidate
+matrices per census, 234,256 streamed raw four-tuples, and at most 65,536
+pair-sum keys. Gram fixtures use at most eight calls and matrices of width
+at most eight. There is no recursion, network operation, subprocess or
+dynamic code in the verifier. Every function is below 60 physical lines.
+Warning-strict normal and optimized commands are registered. The deviation
+is confined to this terminating verifier; any larger search must introduce
+new capacity bounds before expanding it.
+
+## Open next questions
+
+- Can initialized clean helpers reduce the paid-rank floor for even target
+  dimensions? This would separate clean from restored dirty capacity beyond
+  the odd-dimension example. First classify the permitted unspecified
+  helper-column blocks in a normalized endpoint. The complete endpoint and
+  clean-return contract need to be fixed before claiming a capacity.
+- Which invertible non-square-zero paid alphabet can improve a real caller?
+  This is the remaining distinct branch of #6138's second question. First
+  specify a native gate, its complete arbitrary-input response and paid
+  rank. No such physical gate or profitable invoice is supplied here.
+
+## Credit
+
+Josie Elliston's #6138 supplies the question, all-call workspace-free
+attainment theorem and its stated unresolved workspace boundary. Credit
+Nick Petalas #6122 for the earlier four-call theorem, Cinna Davis for the
+rank-one simplex and controller lineage, Ali Romman #5617 for the coupled
+Gram framework and block simplex, and Matarener #6114 for the higher-rank
+query question. Rank factorization, kernel correspondence and rank
+subadditivity are standard linear algebra. The new contribution is the
+projection-complement involution argument and the resulting sharp
+restored-dirty-workspace exclusion. No predecessor credit line is changed.

research/restored-dirty-query-capacity/SOURCES.json

@@ -0,0 +1,24 @@
+{
+  "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/four-block-query-capacity-audit/README.md",
+      "usage": "provenance",
+      "git_blob": "dce26f6675af8df3b236ae62c80f10b9166ac739",
+      "sha256": "157b0e171f7fd9e6b4b0a090ddd7afd2c680efa59b4026a36e4910e56802d4b5"
+    }
+  ]
+}