From 9b51d4bc57d3ecbc19994cc19644b2fde894b664 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Tue, 27 Oct 2026 10:48:01 +0000 Subject: [PATCH] feat(research): prove sharp dyadic tensor capacity bounds --- research/tensor-helper-capacity/PROOF.md | 140 ++++++++++ research/tensor-helper-capacity/README.md | 110 ++++++++ research/tensor-helper-capacity/SOURCES.json | 30 +++ research/tensor-helper-capacity/TASK.json | 113 ++++++++ research/tensor-helper-capacity/VERIFY.json | 32 +++ research/tensor-helper-capacity/verify.py | 257 +++++++++++++++++++ 6 files changed, 682 insertions(+) create mode 100644 research/tensor-helper-capacity/PROOF.md create mode 100644 research/tensor-helper-capacity/README.md create mode 100644 research/tensor-helper-capacity/SOURCES.json create mode 100644 research/tensor-helper-capacity/TASK.json create mode 100644 research/tensor-helper-capacity/VERIFY.json create mode 100644 research/tensor-helper-capacity/verify.py diff --git a/research/tensor-helper-capacity/PROOF.md b/research/tensor-helper-capacity/PROOF.md new file mode 100644 index 0000000000..09f921ccdc --- /dev/null +++ b/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. diff --git a/research/tensor-helper-capacity/README.md b/research/tensor-helper-capacity/README.md new file mode 100644 index 0000000000..c57af94350 --- /dev/null +++ b/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. diff --git a/research/tensor-helper-capacity/SOURCES.json b/research/tensor-helper-capacity/SOURCES.json new file mode 100644 index 0000000000..2e24864683 --- /dev/null +++ b/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" + } + ] +} diff --git a/research/tensor-helper-capacity/TASK.json b/research/tensor-helper-capacity/TASK.json new file mode 100644 index 0000000000..a167a30c7a --- /dev/null +++ b/research/tensor-helper-capacity/TASK.json @@ -0,0 +1,113 @@ +{ + "schema_version": 1, + "task_id": "scalar-to-moment", + "priority_revision": 8, + "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a", + "original_card": { + "id": "scalar-to-moment", + "question": "Can a scalar/frame rewrite improve the complete signed moment through paid jobs, productive targets, or both?", + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "docs/research/recursive-invoice-preflight.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "acceptance_gate": "Require a legal chronological rewrite and favorable complete signed target-minus-paid moment with all extra charges. Unchanged ADD counts or unchanged paid-call counts alone decide neither success nor failure. Compiler, native and outer admission remain separate obligations.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "Construct one legal source-bound rewrite and compare complete before/after P and T. Charge restoration, source windows and owned helpers. A paid call need not disappear: a legal target split or rank redistribution may win. Stop if the signed moment is unchanged or the consumer repays the gain. Do not extend a scalar-only census on ADD counts.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "overlap_terms": [ + "signed moment", + "target split", + "rank exchange", + "scalar rewrite" + ], + "existing_checks": [ + { + "scope": "PR #3998: consecutive A2 scalar contraction", + "evidence": "research/staged544-a2-graph-rewrite/README.md", + "remaining": "A genuinely changed paid itinerary or a distinct independent audit; no default scalar-only expansion.", + "status": "author-checked", + "source_commit": "389268a6b5e0373a3125d5c6fcd6995f4ea324f5", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4019: separated A2 sites with unchanged recursive histogram", + "evidence": "research/staged544-separated-a2/README.md", + "remaining": "A genuinely changed paid itinerary or a distinct independent audit; no default scalar-only expansion.", + "status": "author-checked", + "source_commit": "f408e09df300b575235f7f77f81948071397e16d", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4112: composition audit", + "evidence": "research/staged544-a2-composition-audit/README.md", + "remaining": "A genuinely changed paid itinerary or a distinct independent audit; no default scalar-only expansion.", + "status": "author-checked", + "source_commit": "205b7380656ba4b6316a8a493b1a3c679b8f7a0e", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4152: A1858 contraction audit", + "evidence": "research/staged544-a1858-contraction-audit/README.md", + "remaining": "A genuinely changed paid itinerary or a distinct independent audit; no default scalar-only expansion.", + "status": "author-checked", + "source_commit": "caaa14cde5962adc372fdca71f63d0f29e73c8b2", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Exact dyadic tensor-cut capacity, common-prime equality criterion and sharp bounds at prescribed individual ranks/capacities.", + "scope_change_reason": "The drawn card asks for a paid/target rewrite. This side result instead changes the single-cut hypothesis in PR5615 to tensor composition and identifies information lost by separately pricing capacity; it supplies no physical rewrite or signed-moment gain.", + "bottleneck_link": "A composition screen for legal helper targets. A physical tensor interface and its complete delivery/restoration invoice remain unpriced.", + "budget_minutes": 60, + "stop_rule": "Stop after the first proved sharp composition law with exact witnesses; do not expand a physical construction campaign.", + "outcome": "completed", + "evidence": "PROOF.md and standalone verify.py; source-hash receipts are emitted by each replay.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can one physical pair of cuts realize complementary prime-rank profiles in a tensor eligible module?", + "why_it_matters": "The algebraic capacity gain needs a legal physical interface before it can fund targets.", + "first_step": "Publish a literal source-bound prefix/suffix and saturated bases with carriers and timing.", + "blocked_by": "Physical tensor eligibility, restoration and complete invoice are unproved." + }, + { + "question": "What is the least complete basis-operation bill for the displayed two-channel example?", + "why_it_matters": "Basis delivery can consume the algebraic channel gain.", + "first_step": "Compile the displayed X,Y and all restoration operations in a named admissible caller.", + "blocked_by": "No physical caller or coefficient-growth budget is supplied." + } + ] +} diff --git a/research/tensor-helper-capacity/VERIFY.json b/research/tensor-helper-capacity/VERIFY.json new file mode 100644 index 0000000000..80877d15d8 --- /dev/null +++ b/research/tensor-helper-capacity/VERIFY.json @@ -0,0 +1,32 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 240, + "checks": "Complete new tensor-pair census, sharp extremizer unit blocks and boundary/mutation controls." + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "-O", + "{package}/verify.py" + ], + "timeout_seconds": 240, + "checks": "Same exact scientific coverage with optimization enabled; checks remain active." + } + ] +} diff --git a/research/tensor-helper-capacity/verify.py b/research/tensor-helper-capacity/verify.py new file mode 100644 index 0000000000..4980e433d6 --- /dev/null +++ b/research/tensor-helper-capacity/verify.py @@ -0,0 +1,257 @@ +"""New tensor-capacity checks; no predecessor executable is imported.""" + +from fractions import Fraction +from hashlib import sha256 +from itertools import combinations, permutations, product +import json +from math import gcd, prod +from pathlib import Path + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def matrix(rows): + require(isinstance(rows, (list, tuple)) and 1 <= len(rows) <= 32, "rows") + require(all(isinstance(row, (list, tuple)) for row in rows), "row type") + width = len(rows[0]) + require(1 <= width <= 32 and all(len(row) == width for row in rows), "shape") + require(all(type(x) is int or isinstance(x, Fraction) for row in rows for x in row), "scalar") + out = tuple(tuple(Fraction(x) for x in row) for row in rows) + require(all(x.denominator & (x.denominator - 1) == 0 for row in out for x in row), "nondyadic") + require(all(max(abs(x.numerator).bit_length(), x.denominator.bit_length()) <= 256 + for row in out for x in row), "scalar capacity") + return out + + +def multiply(a, b): + require(len(a[0]) == len(b), "product shape") + return tuple(tuple(sum(a[i][k] * b[k][j] for k in range(len(b))) + for j in range(len(b[0]))) for i in range(len(a))) + + +def identity(n): + return tuple(tuple(Fraction(i == j) for j in range(n)) for i in range(n)) + + +def tensor(a, b): + require(len(a) * len(b) <= 32 and len(a[0]) * len(b[0]) <= 32, "tensor capacity") + return tuple(tuple(x * y for x in row_a for y in row_b) + for row_a in a for row_b in b) + + +def determinant(a): + n = len(a) + require(n <= 4 and all(len(row) == n for row in a), "minor capacity") + total = Fraction(0) + for p in permutations(range(n)): + inversions = sum(p[i] > p[j] for i in range(n) for j in range(i + 1, n)) + total += (-1) ** inversions * prod(a[i][p[i]] for i in range(n)) + return total + + +def minor_capacity(a): + """Independent determinantal-ideal oracle, at most four by four.""" + require(max(len(a), len(a[0])) <= 4, "minor oracle capacity") + capacity = 0 + for k in range(1, min(len(a), len(a[0])) + 1): + divisor = 0 + for rows in combinations(range(len(a)), k): + for columns in combinations(range(len(a[0])), k): + minor = tuple(tuple(a[i][j] for j in columns) for i in rows) + divisor = gcd(divisor, determinant(minor).numerator) + if divisor and divisor & (divisor - 1) == 0: + capacity = k + return capacity + + +def rank(a, prime=0): + """Elimination over Q or a specified prime field, independent of minors.""" + require(prime == 0 or prime in (3, 5, 7, 11), "prime") + rows = [list(row) for row in a] + if prime: + rows = [[x.numerator * pow(x.denominator, -1, prime) % prime for x in row] + for row in rows] + pivot_row = 0 + for column in range(len(rows[0])): + pivot = next((i for i in range(pivot_row, len(rows)) if rows[i][column]), None) + if pivot is None: + continue + rows[pivot_row], rows[pivot] = rows[pivot], rows[pivot_row] + value = rows[pivot_row][column] + scale = pow(value, -1, prime) if prime else 1 / value + rows[pivot_row] = [x * scale % prime if prime else x * scale + for x in rows[pivot_row]] + for i in range(pivot_row + 1, len(rows)): + scale = rows[i][column] + rows[i] = [(x - scale * y) % prime if prime else x - scale * y + for x, y in zip(rows[i], rows[pivot_row])] + pivot_row += 1 + if pivot_row == len(rows): + break + return pivot_row + + +def bezout(a, b): + require(0 <= a < 2**256 and 0 <= b < 2**256 and a + b > 0, "gcd input") + old_r, r, old_s, s, old_t, t = a, b, 1, 0, 0, 1 + for _ in range(1024): + if r == 0: + require(old_s * a + old_t * b == old_r, "Bezout identity") + return old_r, old_s, old_t + quotient = old_r // r + old_r, r = r, old_r - quotient * r + old_s, s = s, old_s - quotient * s + old_t, t = t, old_t - quotient * t + raise ValueError("Euclidean iteration capacity") + + +def diagonal_witness(values): + """Construct X diag(values) Y = I_c by integral two-pivot Smith steps.""" + require(1 <= len(values) <= 32, "diagonal capacity") + require(all(type(x) is int and 0 <= x < 2**64 for x in values), "diagonal value") + n = len(values) + diagonal = list(values) + left, right = [list(row) for row in identity(n)], [list(row) for row in identity(n)] + for i in range(n): + for j in range(i + 1, n): + a, b = diagonal[i], diagonal[j] + if b == 0 or (a and b % a == 0): + continue + g, s, t = bezout(a, b) + first, second = left[i][:], left[j][:] + left[i] = [s * x + t * y for x, y in zip(first, second)] + left[j] = [-(b // g) * x + (a // g) * y for x, y in zip(first, second)] + for row in right: + x, y = row[i], row[j] + row[i], row[j] = x + y, -(t * b // g) * x + (s * a // g) * y + diagonal[i], diagonal[j] = g, a * b // g + positions = [i for i, x in enumerate(diagonal) if x and x & (x - 1) == 0] + x = tuple(tuple(value / diagonal[i] for value in left[i]) for i in positions) + y = tuple(tuple(row[i] for i in positions) for row in right) + return x, y, tuple(diagonal) + + +def diagonal_matrix(values): + return tuple(tuple(Fraction(values[i] if i == j else 0) + for j in range(len(values))) for i in range(len(values))) + + +def pair_census(): + lefts = [matrix((v[:2], v[2:])) for v in product((0, 1, 3), repeat=4)] + rights = [matrix((v[:2], v[2:])) for v in product((0, 1, 5), repeat=4)] + profiles = {} + for a in lefts + rights: + profiles[a] = (rank(a), *(rank(a, p) for p in (3, 5))) + require(minor_capacity(a) == min(profiles[a]), "factor oracle disagreement") + count = strict = 0 + for a in lefts: + for b in rights: + actual = minor_capacity(tensor(a, b)) + predicted = min(x * y for x, y in zip(profiles[a], profiles[b])) + ca, cb = min(profiles[a]), min(profiles[b]) + upper = min(ca * profiles[b][0], cb * profiles[a][0]) + require(ca * cb <= actual == predicted <= upper, "tensor capacity law") + if ca * cb: + common = any(x == ca and y == cb for x, y in zip(profiles[a], profiles[b])) + require((actual == ca * cb) == common, "common-prime equality law") + count += 1 + strict += actual > ca * cb + return {"ordered_matrix_pairs": count, "strict_compositions": strict, + "factor_checks": len(lefts) + len(rights)} + + +def extremal_census(): + count = witnesses = entries = 0 + for factors in range(1, 4): + for ranks in product((1, 2, 3), repeat=factors): + if prod(ranks) > 12: + continue + for capacities in product(*(range(1, r + 1) for r in ranks)): + low = prod(capacities) + high = min(capacities[i] * prod(ranks[j] for j in range(factors) if j != i) + for i in range(factors)) + for distinct, expected in ((False, low), (True, high)): + diagonals = [([1] * c + [(3, 5, 7)[i] if distinct else 3] * (r - c)) + for i, (r, c) in enumerate(zip(ranks, capacities))] + values = [prod(v) for v in product(*diagonals)] + a = diagonal_matrix(values) + actual = min(rank(a, p) for p in (3, 5, 7, 11)) + require(actual == expected, "sharp envelope") + x, y, smith = diagonal_witness(values) + require(len(x) == expected, "unit block size") + require(multiply(multiply(x, a), y) == identity(expected), "unit block endpoint") + require(all(smith[i + 1] % smith[i] == 0 for i in range(len(smith) - 1)), + "Smith divisibility") + witnesses += 1 + entries += expected * expected + count += 1 + return {"rank_capacity_tuples": count, "attaining_unit_blocks": witnesses, + "unit_block_entries": entries} + + +def rectangular_and_oblique(): + count = 0 + for height, width in ((1, 2), (2, 1), (1, 3), (3, 1)): + for values in product((0, 3, 5), repeat=height * width): + a = matrix(tuple(values[i * width:(i + 1) * width] for i in range(height))) + b = matrix(((1, 0), (0, 5))) if max(height, width) == 2 else matrix(((3,),)) + actual = minor_capacity(tensor(a, b)) + require(actual == min(rank(a, p) * rank(b, p) for p in (3, 5, 7)), "rectangular") + count += 1 + for i in range(-3, 4): + for j in range(-3, 4): + a = multiply(matrix(((1, i), (0, 1))), matrix(((1, 0), (0, 3)))) + a = multiply(a, matrix(((1, 0), (j, 1)))) + b = matrix(((Fraction(1, 2), 0), (0, 5))) + require(minor_capacity(a) == minor_capacity(b) == 1, "oblique factors") + require(minor_capacity(tensor(a, b)) == 2, "oblique dyadic activation") + count += 1 + return {"rectangular_oblique_cases": count} + + +def controls(): + count = 0 + for bad in ([], [[], []], [[1], [1, 2]], [[Fraction(1, 3)]], [["1"]], [[2**257]]): + try: + matrix(bad) + except ValueError: + count += 1 + else: + raise ValueError("invalid matrix accepted") + for values in ((0, 3), (0, 0), (2, 0), (3, 5), (3, 3)): + a = diagonal_matrix(values) + x, y, _ = diagonal_witness(values) + expected = minor_capacity(a) + require(len(x) == expected, "zero/unit boundary") + if expected: + require(multiply(multiply(x, a), y) == identity(expected), "boundary witness") + count += 1 + a, b = diagonal_matrix((1, 3)), diagonal_matrix((1, 5)) + displayed_x = matrix(((1, 0, 0, 0), (0, -1, 2, 0))) + displayed_y = matrix(((1, 0), (0, 1), (0, 1), (0, 0))) + require(multiply(multiply(displayed_x, tensor(a, b)), displayed_y) == identity(2), + "displayed witness") + require(minor_capacity(tensor(a, b)) != minor_capacity(a) * minor_capacity(b), + "product-only mutant escaped") + require(minor_capacity(tensor(a, a)) != 2, "separate-minimizers mutant escaped") + require(minor_capacity(diagonal_matrix((0, 3))) == 0, "rational-rank mutant escaped") + x, y, _ = diagonal_witness((1, 5, 3, 15)) + broken = tuple(tuple(0 for _ in row) for row in x) + require(multiply(multiply(broken, tensor(a, b)), y) != identity(2), "witness mutant escaped") + return {"boundary_rejection_mutation_controls": count + 5} + + +def main(): + results = pair_census() | extremal_census() | rectangular_and_oblique() | controls() + package = Path(__file__).resolve().parent + names = ("verify.py", "README.md", "PROOF.md", "TASK.json", "SOURCES.json", "VERIFY.json") + results["source_sha256"] = {name: sha256((package / name).read_bytes()).hexdigest() for name in names} + results["status"] = "PASS_TENSOR_HELPER_CAPACITY" + print(json.dumps(results, sort_keys=True)) + + +if __name__ == "__main__": + main()