Construct transported-query substitution for noncommuting coded jobs (no κ)

research/transported-coded-query/PROOF.md

@@ -0,0 +1,186 @@
+# An exact transport contract for a coded child substitution
+
+This scoped construction and written proof were produced by Nick Petalas.
+It addresses the typed-child-substitution question in Dillon Amburgey's
+[PR4933](https://github.com/CrocSwap/integer-mult-bounds/pull/4933).
+The four-field scaffold comes from Ali Romman's
+[PR6348](https://github.com/CrocSwap/integer-mult-bounds/pull/6348).
+The new step is its exact intertwining condition, ordered residual and
+transported-query construction. No predecessor result is reverified here.
+
+## Contract and theorem
+
+Let A, B and q be units in any unital ring, and let c be an arbitrary ring
+element. Ring elements act on the left of four original, arbitrary fields
+`(x,y,u,v)`. One may take the fields in the ring's left regular module;
+more generally they may be in any left module. Products act rightmost first.
+There are no commutation assumptions on A, B and q.
+
+Put H=AB. Define the two child maps on the first two fields by
+
+```text
+child A = diag(A,A) [[1,c],[0,1]],
+child B = diag(B,B) [[1,0],[-q^-1,1]].
+```
+
+Define the scalar bridges, thin query and complete complement by
+
+```text
+R(x,y,u,v) = (x+v,u,x,y),
+S(x,y,u,v) = (x+u,y,u,v),
+L(x,y,u,v) = (x,v,x-u,v-y),
+C(q): u <- u+q(v-y),
+I(H) = diag(1,1,H,H).
+```
+
+Use this chronological word, retaining the full complement:
+
+```text
+R, C(q), S^-1, I(H), child B, child A, S, L.
+```
+
+**Theorem.** Write E=A(cB-Bq). The exact endpoint is
+
+```text
+(H(x+qy), Hy, Hqu, Hq^-1 v)
+    + (E(y-q^-1 v), 0, E(y-q^-1 v), 0).             (1)
+```
+
+Consequently the endpoint is the desired coded query supplier and two
+independent coded jobs,
+
+```text
+diag(H,H,H,H) [ U(q) direct-sum q direct-sum q^-1 ],
+```
+
+if and only if `cB=Bq` as operators on the admitted module. For a ring
+identity, or a faithful module, this is the ring equation `cB=Bq`.
+Since B is a unit, the unique ring solution is
+
+```text
+c = BqB^-1.                                          (2)
+```
+
+In particular, taking the same query c=q in both children works precisely
+when B commutes with q on that module. A need not commute with B or q.
+Equation (2) gives a construction for arbitrary ordered, noncommuting
+stage factors. It does not grant physical access to that transported query.
+
+## Direct proof with all inputs retained
+
+After R, C(q) and S^-1, the fields are
+
+```text
+(v-qy+qu, u, x+qy-qu, y).
+```
+
+After I(H) and child B they are
+
+```text
+(B(v-qy+qu), B(y-q^-1 v), H(x+qy-qu), Hy).
+```
+
+After child A, the first field is
+
+```text
+Hqu + (AcB-Hq)y + (H-AcBq^-1)v,
+```
+
+and the second is `H(y-q^-1 v)`. Apply S and then L. The identity
+`H-AcBq^-1 = -(AcB-Hq)q^-1` gives (1), with no reordered factors.
+
+For necessity, set x=u=v=0 and vary the independent original input y.
+The first output defect is Ey. Thus correctness on a left module requires
+E to act as zero. Multiplication by the invertible A gives exactly the
+operator intertwining equation. In the left regular module, taking y=1
+also proves the ring equation. Conversely E=0 in the admitted action makes
+every displayed defect zero. This proves both directions.
+
+For (2), multiply cB=Bq on the right by B^-1. All signs and inverses are
+literal ring operations. The argument includes characteristic two and
+noncommutative rings with zero divisors. It requires neither division by an
+integer nor a finite-order relation on q.
+
+## The next scalar bridge and the local bill
+
+Every displayed scalar bridge is invertible over the integers. Their
+inverses are
+
+```text
+R^-1(x,y,u,v) = (u,v,y,x-u),
+S^-1(x,y,u,v) = (x-u,y,u,v),
+L^-1(x,y,u,v) = (x,y-v,x-u,y).
+```
+
+The following in-place recipes require no initialized or borrowed field.
+Here each SWAP exchanges whole fields.
+
+```text
+R: b+=x; SWAP(x,b); SWAP(y,a); SWAP(a,b).
+C: b-=y; a+=q*b; b+=y.
+S^-1: x-=a.
+S: x+=a.
+L: a=-a; a+=x; y=-y; y+=b; SWAP(y,b).
+```
+
+The recipe uses `(a,b)` for `(u,v)`. The middle instruction of C is one
+complete thin query. Outside the supplied child and complement calls,
+there are seven ordinary field additions/subtractions, four field swaps
+and two field negations. These are finite operation counts, not a TM tariff.
+
+The complete abstract bill contains one child A, one child B, one thin q
+query and two H applications. In particular, I(H) has not disappeared.
+Its H is the ordered product AB, not BA or a product declared Gaussian.
+Transporting q inside child A and realizing each H are unpaid physical
+obligations until a concrete implementation and invoice are supplied.
+
+For a typed substitution, the two child types must therefore be
+`Upper(A,BqB^-1)` and `Lower(B,q)`, with `Lower` using `-q^-1` as above.
+The parent returns `Upper(AB,q)` and jobs `ABq`, `ABq^-1`. Its next scalar
+bridge S is compatible because integer field mixing commutes with the
+same left action AB on every field. This statement needs no mutual
+commutation of the stage factors. Any independent child helper outputs
+remain unchanged if all these operations act only on the four main fields.
+
+All four main inputs remain arbitrary. The successful endpoint is
+invertible, so the two returned terminal fields are independent jobs,
+not initialized scratch or duplicate productive credits. Their coded
+operators have not been assigned Gaussian ranks. This is one abstract
+substitution contract; it does not admit the actual negative banks of
+PR4933 or prove closure of its physical compiler.
+
+## Evidence and limits
+
+The new checker expands every entry in an integer free-group algebra.
+It checks (1) with an independent c, (2) with transported c and all three
+nonzero free commutators. The residual uses no inverse of c, so its
+reduction also applies when c is not a unit. Six altered words reject.
+
+A separate engine propagates literal two-coordinate vectors over F2 and
+F3. It exhausts every A,B,q in GL2(F2), then every B,q in GL2(F3) with
+A=[[1,1],[0,1]]. Every one of the eight arbitrary input basis columns is
+checked. It separately verifies that c=q succeeds exactly for the
+commuting B,q fixtures. Finite checks corroborate the written universal
+proof; they are not proof-kernel acceptance or independent human review.
+
+This does not establish a cheaper physical operation, native all-column
+binding, transport/complement tariff, owned-erasure permission, uniform
+compiler, precision/tape bound or analytic recovery theorem. No selected
+frontier, improved kappa or complete multiplication theorem is claimed.
+
+## Credit and distinction
+
+Dillon Amburgey / PR4933 posed the coded recursive-substitution question and
+supplies the phase-correct coded-caller context, following Dugongue's
+PR4929 producer and noncommuting-controller work. Ali Romman / PR6348
+supplies R, C, S, L, the paid complement and the four-field query extension
+for commuting fresh-axis factors. Those maps and that original identity
+are predecessor work. This proof adds their exact residual for a different
+child query and the necessary and sufficient transport contract.
+
+Cinna Davis retains the thin-query and query-thinned caller lineage;
+Cao Yifan, zxv, Jacob Alan Sussman, Ryanson Jonathan and the retained native,
+helper, compiler and outer authors keep their predecessor credit. Ordered
+block multiplication and conjugation are classical tools. No global
+literature-priority claim is made. Source text is linked and pinned as
+provenance; no predecessor executable is imported or replayed. Apache-2.0.

research/transported-coded-query/README.md

@@ -0,0 +1,102 @@
+# Transported queries for noncommuting coded child substitution
+
+This scoped algebraic construction and written proof were produced by Nick Petalas.
+In the four-field query extension, arbitrary ordered stage factors
+A and B need no commutation assumptions if the first child's query is
+transported to `c=BqB^-1`. The exact necessary and sufficient condition is
+`cB=Bq`. Keeping c=q instead leaves the explicit defect
+`A(qB-Bq)(y-q^-1 v)` in two output fields.
+
+[PROOF.md](PROOF.md) gives the universal ring/module statement, all four
+independent input fields, the complete chronological word and its residual.
+It provides one typed child substitution and its next scalar bridge toward
+Dillon Amburgey's [PR4933](https://github.com/CrocSwap/integer-mult-bounds/pull/4933)
+question. It builds on Ali Romman's
+[PR6348](https://github.com/CrocSwap/integer-mult-bounds/pull/6348) module.
+The original commuting module, native words and controller results remain
+predecessor work.
+
+The abstract bill retains both child suppliers, one thin query and two
+applications of the ordered complement AB. The literal scalar bridges
+need seven additions/subtractions, four swaps and two negations. No clean
+scratch field is used. Realizing the transported query and the coded
+complement at an affordable native tariff remains open. This is not a new
+kappa, physical supplier or complete multiplication theorem.
+
+## Reproduce
+
+From the repository root, with CPython 3.12 and its standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/transported-coded-query
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/transported-coded-query/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/transported-coded-query --check-source-history
+```
+
+Other machines may substitute their CPython 3.12 path. Both registered
+commands, ordinary and optimized Python, print
+`PASS_TRANSPORTED_CODED_QUERY`. The verifier writes no files and imports
+no predecessor executable. Its generated JSON receipt binds all six
+package-file hashes. Predecessor text is provenance, not a live input.
+
+The free-group-algebra engine checks all 16 endpoint entries, all 16
+residual entries, three nonzero commutators and six rejecting mutants.
+The separate literal-vector engine checks 2,520 operator triples and all
+20,160 arbitrary-input basis columns over F2/F3. It tests the exact
+untransported commutator criterion on every one of those fixtures and
+rejects singular operators. The written proof supplies the universal
+claim; these finite domains are corroboration.
+
+## Scope, sources and overlap
+
+Question source is PR4933's typed recursive-product question, distinct from
+its rounding/recovery questions. PR4940 changes the entire path's stage
+assignment; PR4948 instantiates a dyadic coded path; PR5562 compiles coded
+thin service. None of those paths or reported numbers is replayed here.
+The fixed nineteen-leaf topology question on PR6348 is separate work.
+This changes the operator contract of one merge, with no tree optimization.
+
+Canonical base is `7c49fe32c55de02c2c873655c804b16e4c3fef0a`, priority
+revision 8. The selected binding baseline passed and identifies the
+selected record's own current value; historical prose is not used as a
+frontier source. Live claims, 100 open PRs, this account's 200 most recent
+PRs, main README searches and merged term searches were checked. The
+overlap helper additionally reported 331 open PRs and 6,205 Discussion
+records with complete remote pagination. This does not cover unpublished
+work or prove novelty.
+
+No actual negative-bank output of PR4933 is admitted by this result. Its
+native realization, transported-query access, restoration and complete
+physical invoice remain unresolved. The five framework assumptions remain.
+No selected cold replay or formal-kernel proof was run. Independent human
+and formal proof-kernel review are unclaimed. Exact provenance and the
+original task card are in SOURCES.json and TASK.json. Apache-2.0.
+
+## Open next questions
+
+- Bind one actual coded child pair to `cB=Bq` and price c, the two AB
+  complements and all frame/ownership boundaries. Begin with a single
+  chronological PR4933 child substitution; physical query access is the
+  blocker, and a formal conjugation alone is insufficient.
+- Can a changed scaffold avoid the transported query at lower complete
+  cost? Begin with one explicit replacement operation and independent
+  inputs. The present necessity theorem applies only to this fixed
+  scaffold and cannot exclude that different interface.
+
+## Verifier constraints
+
+The verifier has no recursion, subprocesses, dynamic code execution or
+network access. Functions stay below 60 lines. Its fixed domains have at
+most 81 raw matrices per field, 2,520 tested triples, eight basis columns
+per triple and 4-by-4 symbolic matrices. Symbolic products enforce at most
+128 nonzero output terms and 64 letters per reduced-product input. A product
+can hold up to 16,384 terms before combining equal words. It fails on
+capacity exhaustion. Package reads are limited to one MiB per file.
+
+Power-of-ten rule 3 deviation: CPython allocates managed dictionaries,
+tuples and integers during this bounded one-shot check. The explicit
+domains, term/word capacities and file limits bound live data, rather than
+providing a fixed-allocation runtime. A fixed-storage deployment would
+need a separate implementation. Both warning-strict registered modes
+exercise the actual checker; no external static type checker is required
+or claimed. No predecessor or shared implementation is modified.

research/transported-coded-query/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/coded-native-caller/README.md",
+      "usage": "provenance",
+      "git_blob": "886bccc303eab39ccb029b992a342028a16d3ada",
+      "sha256": "c6daafcc5fbca994ec72c24aab7688f3eeff63457eefb60a542cfe3780998621"
+    },
+    {
+      "path": "research/coded-native-caller/GAUGE.md",
+      "usage": "provenance",
+      "git_blob": "13269f7b1f98535151de173477f9e7d9a0d81079",
+      "sha256": "09c4e86d99245734761569efd13473623ffdd857e9eae092bd7f54bfd2f42f06"
+    },
+    {
+      "path": "research/balanced-query-tree/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "08dd3e35b0bdd5a6e39f88183b2793c6bb5af6ca",
+      "sha256": "1fab54bc665bf6882f0bbd772af15fbf69a92eac040951ccd19a5accf02f328e"
+    }
+  ]
+}