Prove exact additive cost for two anticommuting query types (no new κ)

research/anticommuting-query-additivity/PROOF.md

@@ -0,0 +1,156 @@
+# Exact additivity for two anticommuting query types
+
+This is a scoped algebraic proof. All fields, role counts and matrix sizes below
+are finite. No physical Gaussian realization or complete multiplication theorem
+is asserted.
+
+## Model and theorem
+
+Let K be any field of characteristic different from two. Fix a nonempty finite
+list of positive integers d_c and the ordinary coefficient algebra
+
+    A = product_c Mat_(d_c)(K).
+
+The payload operator algebra is H = A tensor_K Mat_2(K). Write
+
+    Q = I tensor [[0,1],[1,0]],   R = I tensor [[1,0],[0,-1]].
+
+Thus Q^2 = R^2 = I, RQ = -QR, and H is the direct sum of the four left
+A-modules A, AQ, AR, AQR. The result also holds in any faithful realization
+of this algebra. Faithfulness means equality on all payloads distinguishes
+these four A-coefficients. It is a hypothesis, not a finite-width inference.
+
+A program has arbitrary independent source fields x_1,...,x_n and arbitrary
+independent receivers y_1,...,y_m. Borrowed fields are arbitrary and must be
+restored. Owned fields start at zero and must return zero. The allowed ordinary
+instructions are finite A-linear maps on the fields, including accumulation
+and clearing owned fields. One paid query applies Q or R to one whole field.
+Each inverse has the same price, since both queries are involutions. Arbitrary
+linear feedback, overwriting, retention and interleaving are allowed. The
+ordinary algebra excludes Q and R and excludes choosing a different query type
+in different components of one paid call.
+
+For matrices A0,B,C in Mat_(m by n)(A), require the full endpoint
+
+    x stays x,   y becomes y + (A0 + BQ + CR)x,
+
+with every borrowed field restored and every owned field zero. There is no QR
+coefficient in this target. Expand B and C in component c to scalar matrices
+B_c,C_c of size (m d_c) by (n d_c), and define
+
+    k_B = max_c ceil(rank_K(B_c)/d_c),
+    k_C = max_c ceil(rank_K(C_c)/d_c).
+
+**Theorem.** Every admissible program uses at least k_B queries of type Q and
+at least k_C queries of type R. One program attains both bounds at once. Hence
+the exact minimum total is k_B+k_C. For positive prices w_Q,w_R the exact
+minimum charge is w_Q k_B + w_R k_C.
+
+## 1. One-query rank lemma
+
+Let E be a unital ordinary algebra and suppose the represented operator algebra
+is the direct sum E + ET, with T^2=I and T e = sigma(e) T for an automorphism
+sigma of E. Initially the ET-coefficient row of every arbitrary original input
+and every zero owned field is zero. Ordinary E-linear instructions only combine
+existing ET-coefficient rows. A T query creates one new such row, regardless of
+whether it overwrites a field or uses a retained field.
+
+Record the new row at each of the q query occurrences for this proof only.
+Induction over instructions puts every final ET row in their E-linear span.
+Therefore the final ET matrix factors through q E-rows. Restricting its columns
+to the original source fields preserves that factorization. This argument
+includes arbitrary receiver and borrowed inputs; it never assumes they vanish
+in the actual program. Clearing is an E-linear map and preserves the span
+statement. No runtime bank retaining all q rows is assumed.
+
+For E = product_j Mat_(e_j)(K), any factorization through q E-rows expands to a
+factorization through q e_j scalar coordinates in component j. Its component
+rank is at most q e_j. Conversely, scalar rank factorizations, padded to q e_j
+middle coordinates and assembled into e_j by e_j blocks, attain
+
+    inner_rank_E(D) = max_j ceil(rank_K(D_j)/e_j).
+
+This is ordinary finite-dimensional rank factorization. The proof of the
+present theorem does not require replaying any predecessor implementation.
+
+## 2. Count Q even when R is free
+
+Enlarge the ordinary algebra, solely for a lower bound, to
+
+    E_R = A + AR.
+
+Its projectors (I+R)/2 and (I-R)/2 give the explicit isomorphism
+E_R -> A times A, a+bR -> (a+b,a-b). Every original ordinary instruction and
+every R query is E_R-linear. Q normalizes E_R by a+bR -> a-bR. Moreover
+H = E_R + E_R Q is a direct sum. The one-query lemma thus applies to the
+number q_Q of Q queries in the original program, with all R queries granted
+for free in this relaxation.
+
+The target's E_R Q coefficient is exactly B. Its two components are (B,B),
+so its expanded ranks in both copies of component c equal rank_K(B_c).
+Consequently q_Q >= k_B. The receiver identity and the A0+CR part are E_R-even
+and create no extra odd coefficient. Restoration requirements remain in the
+full endpoint.
+
+## 3. Count R even when Q is free
+
+Use E_Q = A + AQ and its projectors (I+Q)/2 and (I-Q)/2. Now H = E_Q + E_Q R,
+and R normalizes E_Q by a+bQ -> a-bQ. The target's E_Q R coefficient is C,
+embedded as (C,C). The same argument gives q_R >= k_C. These are simultaneous
+inequalities for each original program, so their sum is a valid lower bound.
+They are not alternatives between which a program may choose.
+
+## 4. Attain both bounds with one owned query field
+
+Choose component rank factorizations B_c=L_c V_c, padding each middle dimension
+to k_B d_c. Reassemble the blocks to get B=L V through k_B A-rows. For row j:
+
+1. In a zero owned field h, accumulate h = sum_a V_(j,a) x_a.
+2. Apply Q once to h. Since Q commutes with A, h = sum_a V_(j,a) Q x_a.
+3. For each receiver i, add L_(i,j) h to y_i.
+4. Clear h to zero.
+
+Repeat for every row, then do the same for a k_C-row factorization of C using
+R. Accumulate A0x ordinarily. The original source bank never changes, receiver
+values remain arbitrary, and borrowed fields are untouched. All owned storage
+returns zero. The sequence uses exactly k_B Q queries and k_C R queries, and
+only one owned query field at a time. Its routing operations still have cost;
+only the query count is optimized here. If actual A coefficients require an
+evaluator, its workspace and literal words must be charged separately.
+
+## 5. A sharp sector accounting gap
+
+Take A=K times K and n=m=1, B=(1,0), C=(0,1), A0=0. In the first component
+only Q is needed, and in the second only R is needed. Each component alone has
+query total one, but the complete contract needs two calls. Thus
+
+    max_c (ceil(rank(B_c)/d_c) + ceil(rank(C_c)/d_c)) = 1
+
+is not the correct global answer. The sum of the two maxima is two. A paid
+operation that conditionally chooses Q in one component and R in the other
+would change the alphabet and defeat this example. It is expressly excluded.
+
+For a noncommutative packing example, take A=Mat_2(K), n=m=2 and
+B=C=diag(E_11,E_11). Both expanded ranks are two, so the minimum is two calls,
+one of each type. Matrix units pack the two same-type demands into one field;
+they do not turn the two different query types into one call.
+
+## Scope, novelty and remaining obligations
+
+This answers the faithful anticommuting-involution specialization of RQ09 in
+David Ganz's PR5803, at head 0acda5ab421d28b98fdf916968696c8f9453376f.
+R03-R06 there supply the single-query inner-rank framework and noncommutative
+matrix-block motivation. Ali Romman's PR5626 supplies the earlier faithful
+ordinary-sector query compiler. Their algebraic methods and the classical
+matrix-rank ingredients retain credit. The new step is the simultaneous
+opposite-type relaxation, exact two-type tariff and sharp sector conflict
+example. No worldwide novelty claim is made for classical Clifford algebra.
+
+The theorem does not cover a nonzero QR target coefficient, characteristic two,
+a nonfaithful payload action, ordinary maps outside A, nonlinear instructions,
+selectable per-component query types, or queries on several fields at once.
+It does not assert that actual Gaussian queries anticommute. Finding a lawful
+native realization, physical coefficient words, input/output matchers, paid
+movement, precision, restoration, stock, productive targets and a complete
+signed invoice remains a separate task. The proof is informal; finite checks
+corroborate it and do not discharge its universal quantifiers in a proof kernel.

research/anticommuting-query-additivity/README.md

@@ -0,0 +1,126 @@
+# Two anticommuting query types have an additive exact tariff
+
+This contribution was produced by Nick Petalas. Claim type: scoped algebraic
+proof with exact finite corroboration. No new κ or physical supplier is claimed.
+
+For a faithful algebra with Q²=R²=I, RQ=-QR and ordinary coefficients
+A=product_c Mat_(d_c)(K), char(K)≠2, the input-preserving shear
+
+    y += (A0 + BQ + CR)x
+
+has the exact query count
+
+    max_c ceil(rank(B_c)/d_c) + max_c ceil(rank(C_c)/d_c).
+
+Every word needs the first summand in Q calls and the second in R calls, even
+with arbitrary linear feedback, retention, overwriting and restored borrowed
+dirty fields. One source-preserving word attains both bounds and streams its
+queries through one zero-return owned field. Positive unequal type prices give
+the corresponding weighted sum. Ordinary routing is still charged separately.
+
+[PROOF.md](PROOF.md) gives the complete model and argument. To lower-bound Q,
+grant every R call for free, split the enlarged ordinary algebra into R's two
+eigenspaces and factor the final Q coefficient through the Q outputs. Reverse
+the roles for R. The two inequalities hold for the same original word.
+
+The distinction matters even for A=K×K. Demands B=(1,0), C=(0,1) need two
+queries globally, although each component needs only one. Taking the maximum
+of each component's total would undercount. Noncommutative matrix blocks can
+still pack several same-type demands; the explicit Mat_2 example needs one Q
+and one R rather than four separately acquired responses.
+
+## Reproduce
+
+From the repository root, using standard-library CPython 3.12:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/anticommuting-query-additivity/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/anticommuting-query-additivity
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/anticommuting-query-additivity --check-source-history
+```
+
+Use the last command after committing. On another machine substitute its
+CPython 3.12 path. Both registered commands must finish with
+`PASS_ANTICOMMUTING_QUERY_ADDITIVITY`; the launcher then reports
+`PASS_REGISTERED_RESEARCH_PACKAGE`.
+
+The checker runs independently written formal-coefficient and literal-payload
+interpreters on every original source, receiver and borrowed input column:
+
+- All 6,561 pairs of scalar 2×2 response matrices over F_3.
+- All 6,561 pairs of one-role Mat_2(F_3) response matrices.
+- 216 rectangular/product-algebra fixtures over F_3,F_5,F_7, with nonzero
+  ordinary response terms and dimensions up to three source/receiver fields.
+- The explicit packed Mat_2 example and the two-component sector-conflict
+  example, including arbitrary receiver/borrowed inputs and scratch restoration.
+- All 1,555 words of length at most four in a six-instruction, two-role
+  feedback alphabet. Their complete mixed coefficients satisfy both type cuts.
+- Eight rejection controls for query deletion, wrong query type, dirty-owned
+  leakage, borrowed-field corruption and invalid finite-model parameters.
+
+The interpreters enumerate 149,742 input columns across the first three
+fixture families. These are basis-column comparisons, not that many input
+assignments. Their formal circuits contain 213,064 instructions in total.
+The feedback enumeration corroborates lower bounds and is not an exhaustive
+search over the theorem's arbitrary programs. Each run emits its counts and
+SHA256 hashes of the six package files as a generated receipt to stdout; it
+writes no files. No receipt is handwritten or retained as a frozen result.
+
+## Scope and provenance
+
+The target is the anticommuting-involution specialization of RQ09 in David
+Ganz's [PR5803](https://github.com/CrocSwap/integer-mult-bounds/pull/5803), exact
+head `0acda5ab421d28b98fdf916968696c8f9453376f`,
+[volume-algebra.md](https://github.com/CrocSwap/integer-mult-bounds/blob/0acda5ab421d28b98fdf916968696c8f9453376f/research/frontier-mathematical-atlas/volume-algebra.md).
+Credit its R03-R06 single-query inner-rank framework and explicit two-type
+question, Ali Romman's [PR5626](https://github.com/CrocSwap/integer-mult-bounds/pull/5626)
+faithful-sector compiler, Dugongue's PR5578 T6/T7, and the retained native,
+phase, ownership, controller and compiler lineage, including Cao Yifan,
+Cinna Davis, Ryanson Jonathan, zxv and Jacob Alan Sussman. Classical rank
+factorization and Clifford algebra are not claimed as globally new.
+
+The proof is self-contained. No predecessor verifier or numerical result is
+replayed, and no pending source object or network service is needed to run the
+checker. The cited atlas is bibliographic context, not a runtime input.
+[SOURCES.json](SOURCES.json) pins the original catalogue and selected record
+as historical provenance. [TASK.json](TASK.json) explicitly records the change
+from the source-bound decoder card to this algebraic side result.
+
+Live overlap checking included open PR metadata, this account's earlier PRs,
+recent handoffs, active Discussions, merged-PR searches and all-main README
+searches for the distinctive algebra and tariff. The overlap snapshot covered
+426 open PRs and 5,328 Discussion records. Its sparse local search covered only
+225 notes out of 7,845; the all-main Git searches cover omitted README paths,
+not every package file or historical wording. These checks are not proof of
+novelty.
+
+The theorem excludes mixed QR target terms, characteristic two, nonfaithful
+representations, extra ordinary operators, nonlinear instructions, queries on
+multiple fields and choosing query type per component. Actual native Gaussian
+realization, physical coefficient words, complete routing/precision/stock and
+signed-moment funding remain unproved. No selected source or frontier changes.
+Independent human and formal proof-kernel review are unclaimed.
+
+## Verification design
+
+The retained checker has no recursion, subprocesses, network access, external
+dependencies or writes. Its fixed enumeration bounds, at most two components,
+block size two, three source/receiver fields and 57 instructions bound all
+work. Each matrix operation checks its dimensions; mathematical checks raise
+explicit exceptions and survive optimized Python. Functions remain under 60
+lines. Managed Python allocations are a Power of Ten deviation: these bounded
+finite matrices allocate during evaluation; there is no fixed-memory runtime
+claim. Warning-strict normal and optimized execution supplies the available
+interpreter diagnostics. No separate static analyzer is installed.
+
+## Open next questions
+
+- Determine the exact minimum when a QR output coefficient is present. First
+  compare the two type-specific projected ranks with explicit mixed words.
+  The present proof supplies no attaining general constructor for that domain.
+- Instantiate one faithful native caller with both query types and ordinary
+  spectator matrix units. First pin the operators, phases and four-coefficient
+  independence, then price the full producer/consumer. Its physical contract
+  and complete paid/productive invoice are still missing.
+
+New work is Apache-2.0. The predecessor notices remain with their sources.

research/anticommuting-query-additivity/SOURCES.json

@@ -0,0 +1,18 @@
+{
+  "schema_version": 1,
+  "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8",
+      "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    }
+  ]
+}