Prove exact heterogeneous tensor-cut multiplicities (no κ)

research/heterogeneous-tensor-schedules/PROOF.md

@@ -0,0 +1,139 @@
+# Exact multiplicities for two heterogeneous tensor cuts
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+## Contract and cited premises
+
+Let D = Z[1/2]. For a finite matrix H over D, let r(H) be its rational
+rank and c(H) its unit-channel capacity, the largest h for which dyadic
+matrices X,Y satisfy XHY = I_h. The cited single-cut theorem of Ali
+Romman, [PR5615](https://github.com/CrocSwap/integer-mult-bounds/pull/5615),
+and tensor formula of Nick Petalas,
+[PR5882](https://github.com/CrocSwap/integer-mult-bounds/pull/5882), give
+
+    c(H) = min over odd primes p of rank(H mod p),
+    c(tensor_i H_i) = min_p product_i rank(H_i mod p).
+
+These are premises, not new claims or replay targets here. zxv's
+[PR6054](https://github.com/CrocSwap/integer-mult-bounds/pull/6054) proves
+that exactly factored saturated causal cuts have these complete tensor
+modules, including arbitrary linear combinations across tensor coordinates.
+That implication is also a cited premise. Applying the present theorem to
+physical cuts requires all of its hypotheses and the unpaid physical work.
+
+Define the defect set Delta(H) to consist of odd primes p at which
+rank(H mod p) < r(H). This set is finite. Indeed, clear powers of two and
+take one nonzero maximal minor; every defective prime divides its nonzero
+integer numerator. Matrices may be rectangular.
+
+Fix K,L with
+
+    r(K)=r, c(K)=c, r(L)=s, c(L)=d,
+    0 < c < r, 0 < d < s, Delta(K) intersect Delta(L) empty.
+
+The objective is unit-channel density, capacity divided by rational rank,
+over every tensor word of a prescribed positive length n using these two
+types. No rank budget, per-type charge or productive-target weighting is
+included. Optimizing density need not optimize absolute capacity or a
+complete supplier invoice.
+
+## Fixed multiplicities
+
+If the word contains a copies of K and b=n-a copies of L, then its capacity
+and rational rank are exactly
+
+    C(a,b) = min(c^a s^b, r^a d^b),
+    R(a,b) = r^a s^b.
+
+For p in Delta(K), L has full rank s. The minimum prime-rank product in
+that set is c^a s^b, since some prime attains c. For p in Delta(L) the
+minimum is r^a d^b. At every other prime the product is r^a s^b, which is
+at least both displayed quantities. The same formula includes a=0 or b=0,
+using x^0=1. This proves the claim from the cited tensor formula.
+
+Order does not matter: swapping tensor factors gives invertible integral
+row and column permutation matrices. Every ordered word with the same
+multiplicities therefore has the same capacity and rank. This statement
+does not give free physical routing between different tensor orders.
+
+Put u=c/r and v=d/s, both strictly between zero and one. The exact density is
+
+    rho(a) = min(u^a, v^(n-a)),       0 <= a <= n.
+
+## The new finite-length optimization theorem
+
+Set A=r/c>1 and B=s/d>1. There is a unique integer k in {0,...,n-1} with
+
+    A^k <= B^(n-k),
+    A^(k+1) > B^(n-k-1).
+
+The optimal density and all attaining first-type counts are
+
+    rho_star = max(v^(n-k), u^(k+1)),
+
+    { k     if v^(n-k) = rho_star }
+      union
+    { k+1   if u^(k+1) = rho_star }.
+
+In particular there are either one or two optimal counts. Every tensor
+order with an optimal count attains the optimum; no other count does.
+
+Proof: A^a / B^(n-a) strictly increases with integer a, starts below one at
+a=0 and ends above one at a=n. Thus k exists and is unique. For a<=k,
+u^a>=v^(n-a), so rho(a)=v^(n-a), a strictly increasing function of a.
+For a>=k+1, rho(a)=u^a, a strictly decreasing function of a. Consequently
+only k and k+1 can maximize it, and their values are the two displayed
+quantities. Strict monotonicity excludes every other count, including
+when those two values tie. This proves the theorem for every positive n.
+
+The crossing can be found without logarithms. Test
+
+    r^a d^(n-a) <= c^a s^(n-a)
+
+by integer arithmetic. Binary search maintains a true left endpoint zero
+and false right endpoint n. Each iteration at least halves the interval
+up to rounding. At most bit_length(n)+1 iterations leave adjacent
+endpoints. `schedule.py` implements precisely this predicate and compares
+the two surviving densities as exact fractions. Its finite interface
+limits ranks and length to 4096; the written theorem has no such bound.
+
+## A strictly sharper heterogeneous catalogue bound
+
+Take the algebraic pairings
+
+    K = diag(1,1,3),      L = diag(1,5).
+
+Their ranks/capacities are (r,c)=(3,2) and (s,d)=(2,1), with defect sets
+{3} and {5}. At n=4, k=2 because
+
+    (3/2)^2 <= 2^2,       (3/2)^3 > 2^1.
+
+The unique optimal count is a=3, b=1, with density 8/27, capacity 16 and
+rational rank 54. The equal-count choice has density 1/4 and capacity 9
+at rank 36. Thus balancing multiplicities fails to maximize density.
+The difference in rational ranks is retained explicitly.
+
+PR6054's general two-type bound uses theta=max(2/3,1/2)=2/3 and gives
+rho <= theta^ceil(4/2)=4/9. The new sharp bound 8/27 is strictly smaller,
+and is attained by every word with three K factors and one L factor.
+This is an improvement of a scoped algebraic catalogue bound, with no
+claim that either diagonal pairing is a selected productive native cut.
+
+## Hypothesis and verification limits
+
+Disjoint defects cannot be inferred from capacities alone. With
+K=L=diag(1,3), both individual capacities are one at rank two. Their
+two-factor capacity is one at rank four, whereas the disjoint-defect
+formula would give density one half. The actual density is one quarter.
+The verifier retains this counterexample as a hypothesis control.
+
+The proof is a written all-length argument conditional on the cited
+capacity and module theorems. It is not a proof-kernel formalization.
+Finite tests enumerate the stated bounded domains only. No predecessor
+theorem is independently audited, reproduced or certified here.
+
+All physical basis preparation and inverses, common native charts,
+chronology, carriers, delivery, restoration, precision/growth, stock,
+tape, independent productive targets, compiler and outer obligations
+remain separate. No complete signed bill, new supplier, new kappa or
+complete multiplication theorem follows from this density optimum.

research/heterogeneous-tensor-schedules/README.md

@@ -0,0 +1,152 @@
+# Exact optimal multiplicities for heterogeneous tensor cuts
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+For two fixed dyadic helper-cut types with disjoint odd-prime defect sets,
+the optimal unit-channel density at every positive tensor length has an
+exact two-candidate formula. The bounded optimizer uses integer comparisons
+and returns every optimal multiplicity, including ties.
+
+This is a scoped written mathematical proof with exact finite corroboration.
+It sharpens a switching bound in zxv's
+[PR6054](https://github.com/CrocSwap/integer-mult-bounds/pull/6054).
+That contribution's full product-module theorem and general vanishing-density
+bound are cited premises. They are not audited or replayed here.
+
+Let the two rational ranks be r,s and their unit capacities c,d, with
+0<c<r and 0<d<s. Put A=r/c and B=s/d. For the unique integer k satisfying
+
+    A^k <= B^(n-k),       A^(k+1) > B^(n-k-1),
+
+the exact optimal density is
+
+    max((d/s)^(n-k), (c/r)^(k+1)).
+
+Only k and k+1 copies of the first type can be optimal. Retain whichever
+of the two displayed terms attains the maximum, or both if they tie.
+[PROOF.md](PROOF.md) proves the all-length result and states the exact
+disjoint-defect hypothesis. [schedule.py](schedule.py) implements it for
+ranks and lengths at most 4096. It does not authenticate a supplied physical
+cut or check disjoint defects from the four rank/capacity numbers alone.
+
+For K=diag(1,1,3) and L=diag(1,5), four factors have sharp density 8/27,
+attained by three K factors and one L factor. Capacity is 16 at rank 54.
+The equal-count choice has density 1/4, capacity 9 and rank 36. The
+predecessor's general catalogue upper bound is 4/9 for this instance;
+8/27 is a strictly sharper bound with attainment. This is an algebraic
+example, not a selected productive native cut or a new kappa.
+
+## Reproduce
+
+From the repository root, using CPython 3.12 and its standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -S -W error -B research/heterogeneous-tensor-schedules/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -S -O -W error -B research/heterogeneous-tensor-schedules/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/heterogeneous-tensor-schedules
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/heterogeneous-tensor-schedules --check-source-history
+```
+
+Other hosts may substitute their CPython 3.12 interpreter. Direct commands
+print `PASS_HETEROGENEOUS_TENSOR_SCHEDULES` and a generated JSON receipt
+bound to every package file's SHA256. No receipt is handwritten, and no
+generated files remain in the checkout. Registered replay runs both modes
+and prints `PASS_REGISTERED_RESEARCH_PACKAGE`. The final command checks
+the committed publication. The scientific checker needs no Git, network,
+third-party dependencies or predecessor executable.
+
+The new finite checks enumerate:
+
+- 14,112 profile/length contracts, with every candidate count observed
+  separately, giving 246,960 count observations and 562 two-optimum cases.
+  Ranks are 2 through 7, capacities every positive smaller integer, and
+  lengths 1 through 32. The oracle does not use the crossing rule.
+- All 248 binary words of lengths 1 through 5 in four declared diagonal
+  catalogues. Every one of their 18,504 tensor diagonal coefficients is
+  materialized. A separate integer gcd/lcm Smith oracle computes capacity
+  without prime-rank profiles or the optimizer. All 20 length/catalogue
+  optima and their complete attaining count sets agree.
+- Eleven invalid-profile rejections and nine semantic controls covering
+  ties, exact crossing equality, heterogeneous attainment, length one,
+  maximum accepted input sizes, shared-prime failure, strict improvement
+  and failure of equal multiplicities.
+
+These are new schedule-domain tests, not a predecessor theorem replay.
+They corroborate the written theorem only on their enumerated finite domains.
+The registered commands have separate 120-second limits. Timing observations
+and hosted results belong in the PR body; runtime speed is not a claim.
+
+## Scope and credit
+
+Credit zxv / PR6054 for the question of switching within a fixed defective
+catalogue, the full saturated product-module theorem and general bound.
+Nick Petalas / PR5882 supplies the primewise tensor-capacity formula.
+Ali Romman / PR5615 supplies the single-cut unit-capacity criterion,
+with PR5602/5611/5599 and the retained helper/native/controller lineage.
+Smith theory, tensor ranks and monotone crossing optimization are classical;
+no global literature-priority claim is made. The new contribution is the
+exact heterogeneous finite-length optimum, its bounded optimizer and
+standalone schedule certificate. Predecessor files and credit are unchanged.
+
+Scientific base is canonical main
+7c49fe32c55de02c2c873655c804b16e4c3fef0a, priority revision 8. The selected
+binding-only first example passes. [TASK.json](TASK.json) explicitly changes
+the coverage-law-change card to this algebraic side result, while
+[SOURCES.json](SOURCES.json) pins the cited provenance at the reachable base.
+There are no live external source inputs. The
+[advance CLAIM](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19376668)
+states this scope. Main and merged searches include general catalogue,
+prime-defect and scheduling wording; live PRs, Discussions and local claims
+were checked. Sparse local notes and unpublished work remain overlap limits.
+
+The objective fixes tensor length and maximizes capacity divided by rational
+rank. It does not fix total rank or per-type physical costs. Different
+orders are algebraically equivalent; physical routing can have different
+costs. Overlapping defects, zero capacities and full-capacity types are
+outside the strict two-defective-type theorem. Parallel direct-sum activation
+and Smith-axis ADD-precision ordering are different optimization contracts.
+
+Physical basis preparation and inverses, common native charts, chronology,
+carriers, delivery, restoration, precision/growth, stock, tape, independent
+productive targets, compiler and outer obligations remain unpaid. No
+complete signed bill, supplier admission, new kappa or complete multiplication
+theorem is claimed. Selected scientific replay, Lean and Docker are unrun.
+Independent human and formal proof-kernel review are unclaimed. The selected
+frontier and its five framework assumptions are unchanged.
+
+## Open next questions
+
+- What is the exact optimum with three or more heterogeneous types, or with
+  overlapping defect sets? Start from a finite prime-rank table and fixed
+  length, then derive the integer minimax problem. A complete optimality
+  certificate and a source-specific paid/target objective remain missing.
+- Can an actual native product-cut pair use the optimal mix profitably?
+  First extract two full saturated modules with legal common physical timing
+  and complete prime profiles. Physical basis preparation, delivery,
+  restoration, native charts and the complete signed invoice block a supplier
+  claim. Algebraic density alone does not fund those operations.
+
+Structured first steps and blockers are in TASK.json.
+
+## Executable bounds
+
+The autonomous-local-run playbook stops at this first exact improvement.
+Build the Lever led to the reusable rational optimizer. Prove It Works
+led to independent exhaustive-count and literal tensor/Smith oracles.
+Power of Ten inspection covers both new Python files. There is no recursion,
+network, subprocess, generated executable code or callback dispatch. Each
+function has fewer than 60 physical lines. The public numeric boundary rejects
+nonintegers, booleans, invalid strict capacities and ranks/lengths above 4096.
+The binary search has at most 14 iterations and uses integers of at most
+98,305 bits before reduction. Verification uses fixed finite domains,
+retains at most 33 densities per profile, and materializes at most 243
+diagonal entries per tensor. Smith elimination has at most 29,403 pair
+updates per tensor. Hashing covers seven files, each limited to 256 KiB.
+
+Python's integer, Fraction, dataclass and collection allocation is a managed
+runtime deviation from allocation-free execution. These commands are bounded
+offline calculations, with no steady service. Input and enumeration limits
+bound live objects; a lower-level port must preallocate before widening them.
+Warning-strict normal and optimized execution, in-memory compilation and
+whitespace checks provide diagnostics. No separate Python linter is available
+on PATH; shared build configuration is unchanged.

research/heterogeneous-tensor-schedules/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/dyadic-tensor-capacity/README.md",
+      "usage": "provenance",
+      "git_blob": "35e1b4ebd9ee8b84777c8a4a7b991866d0ac8a6c",
+      "sha256": "0a57beb4542a051889917fbac27d2c068cbe99abc6766b042e48ae97dc99d4a1"
+    },
+    {
+      "path": "research/tensor-helper-capacity/README.md",
+      "usage": "provenance",
+      "git_blob": "c57af943500632b250cfd2d86de144d1520f83ea",
+      "sha256": "78ecf0a3896aaf0945f4aeb332577d3f156bde6dee9d0dafc047b6e0edd8e194"
+    },
+    {
+      "path": "research/dyadic-helper-channel-capacity/README.md",
+      "usage": "provenance",
+      "git_blob": "771c11f6ac4f1c368b4c1dae110956b365dde09e",
+      "sha256": "e79f7b65102179fc7548f2c40db72fd1581ccf23ad4f30fefa371604a1479d1e"
+    }
+  ]
+}