Prove sharp tensor composition of dyadic helper capacity (no new κ)

research/tensor-helper-capacity/PROOF.md

@@ -0,0 +1,140 @@
+# Sharp tensor composition of dyadic helper capacity
+
+Let D = Z[1/2]. For a finite m-by-n matrix K over D, define
+
+    c(K) = max {s : there exist X,Y over D with X K Y = I_s}.
+
+The empty identity is allowed, so c(K) can be zero. Write r(K) for
+rational rank, and rho_p(K) for rank after reduction modulo an odd prime p.
+The reduction is defined because every denominator is a power of two.
+
+Ali Romman's [#5615](https://github.com/CrocSwap/integer-mult-bounds/pull/5615)
+establishes the single-cut criterion
+
+    c(K) = min_{p odd prime} rho_p(K).
+
+Its Smith-form argument constructs a unit block of that size. This result
+is a cited premise. The present contribution concerns how these capacities
+compose and how much information individual capacities discard.
+
+## The tensor composition theorem
+
+For any finite nonempty list K_1,...,K_t of dyadic matrices,
+
+    c(K_1 tensor ... tensor K_t) = min_{p odd prime} product_i rho_p(K_i).  (1)
+
+Put c_i = c(K_i) and r_i = r(K_i). Then
+
+    product_i c_i <= c(tensor_i K_i)
+                 <= min_i (c_i product_{j != i} r_j).                    (2)
+
+Both bounds are sharp for every prescribed positive integer rank tuple
+r_i and capacity tuple 1 <= c_i <= r_i. Rectangular zero padding preserves
+the constructions. If some c_i is zero, the tensor capacity is zero.
+
+When every c_i is positive, equality at the lower bound holds exactly when
+there is one odd prime p such that rho_p(K_i) = c_i for every i.
+In particular c(K tensor ... tensor K) = c(K)^t for repeated equal factors.
+
+### Proof
+
+Over a field, row and column changes put each K_i into a rectangular
+identity block with zeros elsewhere. Tensoring the changes shows that
+the rank of the tensor is the product of the ranks. Apply this fact
+modulo each odd prime, then apply the cited single-cut criterion to the
+tensor matrix. This proves (1).
+
+Every rho_p(K_i) is at least c_i, which proves the lower bound in (2).
+For a fixed i, choose an odd prime attaining c_i. Such a prime exists:
+the ranks are integers in the finite set {0,...,r_i}, so the minimum in
+the cited criterion is attained. At that prime all other ranks are at
+most their rational ranks. Taking the minimum over i proves the upper
+bound. If c_i = 0, that prime forces tensor rank zero.
+
+For positive capacities, equality of a product of integers rho_p(K_i)
+with product_i c_i requires equality in every positive factor. The
+minimum in (1) is attained for the same finite-integer reason. This
+proves both directions of the common-prime equality criterion. Applying
+(1) to equal factors gives the repeated-factor identity, including zero.
+
+To attain the lower bound for prescribed r_i,c_i, fix one odd prime p
+and take
+
+    K_i = diag(I_{c_i}, p I_{r_i-c_i}).
+
+Its rational rank is r_i, its rank modulo p is c_i and its rank at every
+other odd prime is r_i. Formula (1) gives product_i c_i.
+
+To attain the upper bound, choose distinct odd primes p_i and take
+
+    K_i = diag(I_{c_i}, p_i I_{r_i-c_i}).
+
+At prime p_i the tensor rank is c_i product_{j != i} r_j. Outside this
+finite set it is product_i r_i. The latter is no smaller than any of
+the displayed exceptional values. Formula (1) therefore gives the
+upper bound exactly. Smith reduction of the resulting diagonal matrix
+constructs X,Y attaining its unit block; existence is not inferred
+from a favorable rational rank alone. This completes the proof.
+
+## Explicit smallest strict composition
+
+Take A = diag(1,3) and B = diag(1,5). Each has capacity one. In the
+usual tensor order K = A tensor B = diag(1,5,3,15). The matrices
+
+    X = [[1, 0, 0, 0],     Y = [[1, 0],
+         [0,-1, 2, 0]]         [0, 1],
+                               [0, 1],
+                               [0, 0]]
+
+satisfy X K Y = I_2 by -5 + 2*3 = 1. Modulo either 3 or 5 the tensor
+has rank two, so a third unit channel is impossible. Thus c(A tensor B)
+= 2 > c(A)c(B) = 1. This is a new composition example, distinct from
+#5615's direct-sum example diag(3,5).
+
+For every n >= 2 and t >= 2, take t distinct primes and K_i =
+diag(1,p_i,...,p_i) of size n. Each individual capacity is one; the
+tensor capacity is exactly n^(t-1), the largest possible value with
+these rational ranks and individual capacities. This is an arbitrarily
+large failure of the product of individual capacities as an upper bound.
+The primes are fixed coefficients, not unpaid prime-provider operations.
+
+## Constructive finite corroboration
+
+The verifier uses two independent calculations on new matrices. Exact
+determinantal ideals compute capacity: the gcd of numerators of all
+k-by-k minors is a power of two exactly when that ideal is the unit
+ideal over D. Field elimination computes the prime profiles. For the
+two complete 2-by-2 entry alphabets {0,1,3} and {0,1,5}, the only possible
+odd divisors of a nonzero maximal minor are 3 and 5. Rational rank
+represents every other odd prime. No untested bad prime is omitted.
+
+For the diagonal extremizers, only 3,5,7 can be exceptional; rank modulo
+11 is the generic rank. A separate two-pivot Euclidean procedure returns
+literal X,Y and checks every entry of X K Y = I_c. If a,b are two
+diagonal entries and sa+tb=g=gcd(a,b), its integral transformations are
+
+    U = [[s,t],[-b/g,a/g]],
+    V = [[1,-tb/g],[1,sa/g]],
+    U diag(a,b) V = diag(g,ab/g),  det U = det V = 1.
+
+The zero-zero case is skipped. Both side transformations are retained,
+so the returned unit block is an executable witness. This elementary
+Smith operation is classical. It is used here to corroborate the new
+composition extremizers, without executing the predecessor's checker.
+
+## Scope and physical boundary
+
+This is a scoped algebraic proof for dyadic pairing matrices. It does not
+show that independently supplied physical cuts have a tensor-product
+eligible module, simultaneous timing, a common chart or the carriers
+required by that product. It does not bound scalar coefficient growth,
+basis-operation tariffs, native maps, dirty restoration, storage or
+compiler/outer costs. Those quantities are unknown here, not zero.
+No extra productive targets or new kappa follow from this theorem alone.
+
+Credit Ali Romman #5615 for the exact single-cut capacity theorem,
+#5602/#5609/#5611 for the causal pairing and completion interfaces, and
+the retained #5599 helper/controller/native lineage. Classical Smith
+normal form, Bezout identities and field rank retain their classical
+status. The sharp tensor envelope, equality criterion and composition
+examples in this application were produced by Nick Petalas.

research/tensor-helper-capacity/README.md

@@ -0,0 +1,110 @@
+# Sharp tensor composition of dyadic helper capacity
+
+For dyadic pairing matrices K_i, the exact simultaneous unit-channel count is
+
+```text
+c(tensor_i K_i) = min_{odd primes p} product_i rank_Fp(K_i mod p).
+```
+
+If factor i has rational rank r_i and positive capacity c_i, the sharp bounds are
+
+```text
+product_i c_i <= c(tensor_i K_i) <= min_i c_i product_{j != i} r_j.
+```
+
+Both endpoints are attainable for every prescribed rank/capacity tuple. Thus t
+rank-n factors, each with capacity one, can have tensor capacity n^(t-1).
+Repeated equal factors retain exactly the product capacity. Different odd-prime
+rank losses are what permit a strict gain.
+
+Claim type: scoped algebraic proof with exact finite corroboration. No new kappa
+or physical supplier is claimed. [PROOF.md](PROOF.md) gives the theorem, equality
+criterion and explicit X K Y = I_2 witness for
+`diag(1,3) tensor diag(1,5) = diag(1,5,3,15)`.
+
+Ali Romman's [#5615](https://github.com/CrocSwap/integer-mult-bounds/pull/5615)
+supplies the cited single-cut unit-block theorem. The new step is its sharp
+composition envelope and the failure of individual capacities to determine
+tensor capacity. No predecessor executable is imported or replayed. The
+predecessor's direct-sum example `diag(3,5)` is credited and is not our result.
+
+## Reproduce
+
+From the repository root, using CPython 3.12 and the standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/tensor-helper-capacity/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/tensor-helper-capacity
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/tensor-helper-capacity --check-source-history
+```
+
+Use any CPython 3.12 interpreter in place of that local absolute path. Both
+registered normal and optimized commands must print `PASS_TENSOR_HELPER_CAPACITY`;
+the launcher must print `PASS_REGISTERED_RESEARCH_PACKAGE`. The verifier emits
+a generated JSON receipt with counts and SHA256 of all six package source files.
+It writes no files and needs no Git, network or predecessor package at runtime.
+
+The complete ordered-pair census uses all 2-by-2 matrices over entry alphabets
+{0,1,3} and {0,1,5}. A determinant-ideal oracle independently computes capacity
+of every 4-by-4 tensor; field elimination computes the predicted profile. The
+extremizer checks construct actual unit blocks for both sharp bounds. Separate
+rectangular, oblique dyadic, zero-capacity and deliberately false rules test
+the boundary. Exact executed counts and local timings are recorded in the PR.
+The all-size theorem rests on the written proof, not finite extrapolation.
+
+## Scope and relevance
+
+This is a changed-scope side result under `scalar-to-moment`, prompted by the
+current legal-helper-splitting priority and #5615. It identifies an algebraic
+condition to examine before multiplying capacities of separately normalized
+cuts. A physical tensor cut, simultaneous timing, saturated eligible modules,
+common charts and sufficient carriers are additional hypotheses. Basis work,
+coefficient growth, native execution, dirty restoration, storage and complete
+paid/target invoices remain unpriced. No selected replay, compiler/outer
+admission or complete multiplication theorem is supplied. Independent human
+and formal proof-kernel review are unclaimed.
+
+Base `de5ec2e7a6074068452f45b1a191b5c72832df4a`, priority revision 8.
+The selected source-binding orientation passed. The live open PR/discussion
+cache had complete remote pagination, but its sparse local note inventory was
+incomplete. Separate all-main README and merged-PR searches addressed the
+composition terms; this bounded overlap check does not establish global novelty.
+[Advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19214979).
+
+## Implementation bounds
+
+The minor oracle accepts at most 4-by-4 matrices. Field elimination and tensor
+helpers have at most 32 rows/columns at their checked entry points. Executed
+extremizers have at most 12 diagonal entries and at most three factors. All
+censuses are fixed finite products. The Euclidean routine has a 1,024-step cap
+and a checked Bezout identity. Every mathematical check remains active under
+`-O`; malformed inputs and corrupted endpoints must reject.
+
+Power of Ten rule 3 deviation: CPython and Fraction allocate during evaluation.
+This finite verifier uses fixed census sizes, matrices of bounded dimension and
+bounded input bit sizes; it has no service loop or external resource ownership.
+Rules 8 and 9 use ordinary Python iteration and standard-library arithmetic,
+with no dynamic evaluation or generated code. Warning-strict normal/optimized
+replays are the recurring diagnostics. Reassess capacities before widening a
+census; the finite implementation does not implement arbitrary-size Smith form.
+
+## Open next questions
+
+1. Can a named physical pair of helper cuts realize the tensor eligible modules
+   with complementary odd-prime losses? First exhibit its complete prefix,
+   suffix, saturated bases and carrier/timing contract. A static tensor matrix
+   is insufficient; physical delivery and restoration are blockers.
+2. What is the least complete basis-operation bill for the displayed two-channel
+   example in an admissible caller? First compile its explicit X,Y with bounded
+   coefficients and include all inverse/restoration operations. No free basis
+   change or independent-target credit is assumed here.
+
+## Credit
+
+This contribution was produced by Nick Petalas. Credit Ali Romman #5615 for the
+single-cut capacity theorem, #5602/#5609/#5611 for causal pairing and completion,
+and #5599 with the retained helper/controller/native lineage. The predecessor
+also credits Nick Petalas #5115 for a different Euclidean row preparation.
+Smith normal form, Bezout identities and rank multiplicativity are classical.
+The claimed addition is the sharp composition result in this interface, not a
+new general Smith theorem. Apache-2.0.

research/tensor-helper-capacity/SOURCES.json

@@ -0,0 +1,30 @@
+{
+  "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"
+    },
+    {
+      "path": "research/dyadic-helper-channel-capacity/README.md",
+      "usage": "provenance",
+      "git_blob": "771c11f6ac4f1c368b4c1dae110956b365dde09e",
+      "sha256": "e79f7b65102179fc7548f2c40db72fd1581ccf23ad4f30fefa371604a1479d1e"
+    },
+    {
+      "path": "research/dyadic-helper-channel-capacity/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "c97a6edce3070414c81f0ef6e6c099ebb17f3a90",
+      "sha256": "b258a217f2cd0fc48461285fe8ae24de26b0c5963668d9d8f0955fc6e759e929"
+    }
+  ]
+}