From 09d4b6bb8a30d6c616fa2263d6ec99ee8c47a483 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Tue, 3 Nov 2026 15:06:03 +0000 Subject: [PATCH] feat(research): optimize heterogeneous tensor-cut multiplicities --- .../heterogeneous-tensor-schedules/PROOF.md | 139 +++++++++++++++ .../heterogeneous-tensor-schedules/README.md | 152 +++++++++++++++++ .../SOURCES.json | 36 ++++ .../heterogeneous-tensor-schedules/TASK.json | 79 +++++++++ .../VERIFY.json | 34 ++++ .../schedule.py | 53 ++++++ .../heterogeneous-tensor-schedules/verify.py | 158 ++++++++++++++++++ 7 files changed, 651 insertions(+) create mode 100644 research/heterogeneous-tensor-schedules/PROOF.md create mode 100644 research/heterogeneous-tensor-schedules/README.md create mode 100644 research/heterogeneous-tensor-schedules/SOURCES.json create mode 100644 research/heterogeneous-tensor-schedules/TASK.json create mode 100644 research/heterogeneous-tensor-schedules/VERIFY.json create mode 100644 research/heterogeneous-tensor-schedules/schedule.py create mode 100644 research/heterogeneous-tensor-schedules/verify.py diff --git a/research/heterogeneous-tensor-schedules/PROOF.md b/research/heterogeneous-tensor-schedules/PROOF.md new file mode 100644 index 0000000000..7dd60ee31b --- /dev/null +++ b/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. diff --git a/research/heterogeneous-tensor-schedules/README.md b/research/heterogeneous-tensor-schedules/README.md new file mode 100644 index 0000000000..39c019f1d0 --- /dev/null +++ b/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 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. diff --git a/research/heterogeneous-tensor-schedules/SOURCES.json b/research/heterogeneous-tensor-schedules/SOURCES.json new file mode 100644 index 0000000000..2741a6d38e --- /dev/null +++ b/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" + } + ] +} diff --git a/research/heterogeneous-tensor-schedules/TASK.json b/research/heterogeneous-tensor-schedules/TASK.json new file mode 100644 index 0000000000..a55019b7f3 --- /dev/null +++ b/research/heterogeneous-tensor-schedules/TASK.json @@ -0,0 +1,79 @@ +{ + "schema_version": 1, + "task_id": "coverage-law-change", + "priority_revision": 8, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "original_card": { + "id": "coverage-law-change", + "question": "Can a completed call earn more independent productive target credit without an offsetting paid bill?", + "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" + ], + "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": "A source-bound arbitrary-input identity and legal producer/consumer boundary with the complete paid and productive target invoice, including restoration, ownership, native alignment and extra charges. Price under the actual current model; historical ceiling.py assumptions must be established before use. A favorable optimistic relaxation keeps a route open but is not a completed supplier. A scoped local result remains useful; expansion requires the family-level budget gate.", + "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": "Use #5599 as a completed positive control, then choose one uncovered cut/module beyond an applicable frozen exclusion. Derive independence, saturation and chronological availability rather than counting rational rank alone. Price target credits and all new jobs together, then check compiler and actual caller compatibility. Stop on a nonphysical credit or an unfavorable complete relaxation.", + "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": [ + "target credit", + "helper split", + "coverage law" + ], + "existing_checks": [ + { + "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 optimal multiplicities and unit-channel density of two heterogeneous dyadic tensor-cut types with disjoint odd-prime defect sets.", + "scope_change_reason": "The card requests a physical productive-target improvement. This is a scoped algebraic catalogue bound and schedule optimizer, with no physical cut or complete invoice supplied.", + "bottleneck_link": "Sharpens the optimistic tensor-unit density budget before paying basis preparation, delivery and productive-target costs. It cannot admit a supplier.", + "budget_minutes": 60, + "stop_rule": "Ship the first proved exact scheduling improvement; leave more types, overlapping defects and physical realization as open questions.", + "outcome": "completed", + "evidence": "PROOF.md and the standalone exact verifier; generated hash-bound receipts are printed, never handwritten.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "What is the exact optimum for three or more heterogeneous types or overlapping defect sets?", + "why_it_matters": "The two independent-loss crossing rule does not handle a general prime-profile catalogue.", + "first_step": "Specify a finite prime-rank table and fixed tensor length; derive the integer minimax objective before selecting a solver.", + "blocked_by": "A complete optimality certificate and a source-specific paid/target objective are not supplied." + }, + { + "question": "Can an actual native product-cut pair satisfy the disjoint-defect condition and use the optimal multiplicities profitably?", + "why_it_matters": "An algebraic density improvement gives no productive Gaussian targets without legal realization.", + "first_step": "Extract two full saturated cut modules with legal common physical timing and derive their complete prime profiles and charges.", + "blocked_by": "Physical basis preparation, delivery, restoration, native charts and the complete signed invoice remain unpaid." + } + ] +} diff --git a/research/heterogeneous-tensor-schedules/VERIFY.json b/research/heterogeneous-tensor-schedules/VERIFY.json new file mode 100644 index 0000000000..d06a3d46e2 --- /dev/null +++ b/research/heterogeneous-tensor-schedules/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-S", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exhaustive multiplicity optima, literal tensor Smith oracle, all ties, boundary and hypothesis controls." + }, + { + "argv": [ + "{python}", + "-S", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The same complete finite verification with Python assertions disabled." + } + ] +} diff --git a/research/heterogeneous-tensor-schedules/schedule.py b/research/heterogeneous-tensor-schedules/schedule.py new file mode 100644 index 0000000000..7c632e2967 --- /dev/null +++ b/research/heterogeneous-tensor-schedules/schedule.py @@ -0,0 +1,53 @@ +"""Exact multiplicities for two independent tensor-capacity losses. + +Produced by Nick Petalas. Apache-2.0. +The caller must establish the disjoint-prime hypothesis in PROOF.md. +""" + +from dataclasses import dataclass +from fractions import Fraction + +MAX_RANK = 4096 +MAX_LENGTH = 4096 + + +@dataclass(frozen=True, slots=True) +class Schedule: + crossing: int + counts: tuple[int, ...] + density: Fraction + + +def validate(r: int, c: int, s: int, d: int, n: int) -> None: + """Validate the bounded numeric interface, including strict defects.""" + if any(type(x) is not int for x in (r, c, s, d, n)): + raise TypeError("ranks, capacities and length must be integers") + if not (1 <= c < r <= MAX_RANK and 1 <= d < s <= MAX_RANK): + raise ValueError("require 1 <= capacity < rank <= 4096 for both types") + if not 1 <= n <= MAX_LENGTH: + raise ValueError("require 1 <= length <= 4096") + + +def optimize(r: int, c: int, s: int, d: int, n: int) -> Schedule: + """Return every optimal first-type count and the exact unit density. + + This optimizes min((c/r)**a, (d/s)**(n-a)). It does not certify that + physical cuts exist, or that supplied profiles have disjoint defects. + """ + validate(r, c, s, d, n) + low, high = 0, n + for _ in range(n.bit_length() + 1): + if high - low == 1: + break + middle = (low + high) // 2 + if r**middle * d ** (n - middle) <= c**middle * s ** (n - middle): + low = middle + else: + high = middle + if high - low != 1: + raise RuntimeError("crossing search exhausted its proven bound") + left = Fraction(d, s) ** (n - low) + right = Fraction(c, r) ** high + best = max(left, right) + counts = tuple(a for a, value in ((low, left), (high, right)) if value == best) + return Schedule(low, counts, best) diff --git a/research/heterogeneous-tensor-schedules/verify.py b/research/heterogeneous-tensor-schedules/verify.py new file mode 100644 index 0000000000..16c007a152 --- /dev/null +++ b/research/heterogeneous-tensor-schedules/verify.py @@ -0,0 +1,158 @@ +"""Independent finite corroboration of the new schedule optimum. + +Produced by Nick Petalas. Apache-2.0. No predecessor executable imports. +""" + +from fractions import Fraction +from hashlib import sha256 +from itertools import product +import json +from math import gcd, prod +from pathlib import Path + +from schedule import MAX_LENGTH, MAX_RANK, Schedule, optimize + + +def require(condition: bool, message: str) -> None: + if not condition: + raise AssertionError(message) + + +def exhaustive_profiles() -> dict[str, int]: + """Check every count, including all ties, without the crossing rule.""" + cases = observations = ties = 0 + profiles = tuple((r, c) for r in range(2, 8) for c in range(1, r)) + for (r, c), (s, d), n in product(profiles, profiles, range(1, 33)): + values = tuple(min(Fraction(c**a, r**a), Fraction(d ** (n - a), s ** (n - a))) + for a in range(n + 1)) + best = max(values) + counts = tuple(a for a, value in enumerate(values) if value == best) + answer = optimize(r, c, s, d, n) + require((answer.counts, answer.density) == (counts, best), "profile optimum") + k = answer.crossing + require(r**k * d ** (n - k) <= c**k * s ** (n - k), "left crossing") + require(r ** (k + 1) * d ** (n - k - 1) > c ** (k + 1) * s ** (n - k - 1), + "right crossing") + cases += 1 + observations += len(values) + ties += len(counts) == 2 + return {"profile_contracts": cases, "count_observations": observations, "ties": ties} + + +def tensor_diagonal(word: tuple[int, ...], first: tuple[int, ...], + second: tuple[int, ...]) -> list[int]: + """Materialize every diagonal coefficient, in chronological factor order.""" + entries = [1] + for letter in word: + factor = (first, second)[letter] + entries = [x * y for x in entries for y in factor] + require(len(entries) <= 256, "literal tensor capacity") + return entries + + +def smith_units(entries: list[int]) -> int: + """Count dyadic units by exact gcd/lcm diagonal Smith operations. + + A two-entry update diag(a,b) -> diag(gcd(a,b),lcm(a,b)) is unimodular + over Z. Subsequent updates preserve previous divisibility. This oracle + does not use prime ranks, a count formula, or the schedule optimizer. + """ + diagonal = entries.copy() + for i in range(len(diagonal)): + for j in range(i + 1, len(diagonal)): + a, b = diagonal[i], diagonal[j] + common = gcd(a, b) + diagonal[i], diagonal[j] = common, a // common * b + require(all(diagonal[i + 1] % diagonal[i] == 0 for i in range(len(diagonal) - 1)), + "Smith divisibility") + require(prod(diagonal) == prod(entries), "Smith determinant") + # All literal fixtures are positive odd integers, whose only dyadic unit is 1. + return diagonal.count(1) + + +def literal_schedules() -> dict[str, int]: + """Exhaust complete binary words and compare the new global optimum.""" + families = (((1, 1, 3), (1, 5)), ((1, 3), (1, 1, 5)), + ((1, 3), (1, 5)), ((1, 3, 3), (1, 1, 5))) + words = coefficients = lengths = 0 + for first, second in families: + r, c, s, d = len(first), first.count(1), len(second), second.count(1) + for n in range(1, 6): + best = Fraction(0) + attained = set() + for word in product((0, 1), repeat=n): + entries = tensor_diagonal(word, first, second) + density = Fraction(smith_units(entries), len(entries)) + if density > best: + best, attained = density, {word.count(0)} + elif density == best: + attained.add(word.count(0)) + words += 1 + coefficients += len(entries) + answer = optimize(r, c, s, d, n) + require((answer.counts, answer.density) == (tuple(sorted(attained)), best), + "literal tensor schedule optimum") + lengths += 1 + return {"literal_words": words, "literal_coefficients": coefficients, + "literal_length_contracts": lengths} + + +def controls() -> dict[str, int]: + rejected = 0 + bad = ((True, 1, 2, 1, 1), (2, 1, 2, 1, 1.0), (2, 0, 2, 1, 1), + (2, 2, 2, 1, 1), (1, 1, 2, 1, 1), (2, 1, 2, -1, 1), + (2, 1, 1, 1, 1), (MAX_RANK + 1, 1, 2, 1, 1), + (2, 1, MAX_RANK + 1, 1, 1), (2, 1, 2, 1, 0), + (2, 1, 2, 1, MAX_LENGTH + 1)) + for args in bad: + try: + optimize(*args) + except (TypeError, ValueError): + rejected += 1 + else: + raise AssertionError("invalid profile accepted") + edge = optimize(MAX_RANK, MAX_RANK - 1, 2, 1, MAX_LENGTH) + # A shared bad prime violates the theorem's hypothesis, and its answer differs. + common_prime_density = Fraction(smith_units(tensor_diagonal((0, 1), (1, 3), (1, 3))), 4) + semantic = ( + (optimize(3, 2, 2, 1, 4) == Schedule(2, (3,), Fraction(8, 27)), "attainment"), + (optimize(2, 1, 2, 1, 3).counts == (1, 2), "tie retention"), + (optimize(4, 1, 2, 1, 3).crossing == 1, "crossing equality"), + (optimize(3, 2, 2, 1, 1).counts == (1,), "single factor"), + (all(0 <= a <= MAX_LENGTH for a in edge.counts), "capacity boundary"), + (common_prime_density == Fraction(1, 4), "shared-prime fixture"), + (common_prime_density != optimize(2, 1, 2, 1, 2).density, "disjoint defects"), + (Fraction(8, 27) < Fraction(4, 9), "strict bound improvement"), + (Fraction(8, 27) > Fraction(1, 4), "unequal multiplicities"), + ) + for condition, message in semantic: + require(condition, message) + return {"invalid_profiles_rejected": rejected, "semantic_controls": len(semantic)} + + +def main() -> None: + counts = exhaustive_profiles() | literal_schedules() | controls() + root = Path(__file__).resolve().parent + files = ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", "VERIFY.json", + "schedule.py", "verify.py") + hashes = {} + for name in files: + path = root / name + require(path.stat().st_size <= 256 * 1024, "package file capacity before read") + data = path.read_bytes() + require(len(data) <= 256 * 1024, "package file capacity") + hashes[name] = sha256(data).hexdigest() + entries = tensor_diagonal((0, 0, 0, 1), (1, 1, 3), (1, 5)) + capacity = smith_units(entries) + example = {"r": 3, "c": 2, "s": 2, "d": 1, "n": 4, + "first_counts": list(optimize(3, 2, 2, 1, 4).counts), + "capacity": capacity, "rank": len(entries), + "density": str(Fraction(capacity, len(entries)))} + receipt = {"schema": "heterogeneous-tensor-schedules/1", "counts": counts, + "example": example, "sha256": hashes} + print(json.dumps(receipt, sort_keys=True)) + print("PASS_HETEROGENEOUS_TENSOR_SCHEDULES") + + +if __name__ == "__main__": + main()