From c069c79e81dd97296e2cae07c7d627c26ab19947 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Tue, 3 Nov 2026 11:16:41 +0000 Subject: [PATCH] feat(research): add Gaussian-dyadic five-product Toom-3 --- research/gaussian-dyadic-toom3/PROOF.md | 207 +++++++++++++++++ research/gaussian-dyadic-toom3/README.md | 111 ++++++++++ research/gaussian-dyadic-toom3/SOURCES.json | 30 +++ research/gaussian-dyadic-toom3/TASK.json | 96 ++++++++ research/gaussian-dyadic-toom3/VERIFY.json | 34 +++ research/gaussian-dyadic-toom3/circuit.py | 114 ++++++++++ research/gaussian-dyadic-toom3/verify.py | 232 ++++++++++++++++++++ 7 files changed, 824 insertions(+) create mode 100644 research/gaussian-dyadic-toom3/PROOF.md create mode 100644 research/gaussian-dyadic-toom3/README.md create mode 100644 research/gaussian-dyadic-toom3/SOURCES.json create mode 100644 research/gaussian-dyadic-toom3/TASK.json create mode 100644 research/gaussian-dyadic-toom3/VERIFY.json create mode 100644 research/gaussian-dyadic-toom3/circuit.py create mode 100644 research/gaussian-dyadic-toom3/verify.py diff --git a/research/gaussian-dyadic-toom3/PROOF.md b/research/gaussian-dyadic-toom3/PROOF.md new file mode 100644 index 0000000000..cbd54bd9d0 --- /dev/null +++ b/research/gaussian-dyadic-toom3/PROOF.md @@ -0,0 +1,207 @@ +# Gaussian-dyadic five-product interpolation + +This contribution was produced by Nick Petalas. Apache-2.0. + +## Contract and result + +Put G = Z[i], pi = 1+i and R = G[1/2] = G[1/pi]. The inputs are +two independent coefficient triples a and b in G. Five output fields y +have arbitrary initial values in G. The endpoint is + + y_k += sum_(j+l=k) a_j b_l, 0 <= k <= 4. + +All six inputs are preserved. Two additional fields start at zero and +return to zero. A PRODUCT call is the exact additive operation +`target += left*right`, preserving its distinct source fields. Its full +implementation is a premise, and it is counted once wherever invoked. + +There is a word with five PRODUCT calls, sixty coefficient ADDs and four +SCALEs. A coefficient ADD means exactly `target += c*source`, with its +displayed Gaussian-integer coefficient c. It is a charged macro, not a +unit-cost claim about multiplication by c. Two SCALEs multiply by a +Gaussian associate of pi; two divide by an associate of pi. Every +intermediate value is a Gaussian integer on this contract. No division +by an odd integer, approximate rounding or hidden product uncomputation +is used. Every operation and its inverse is listed by `program()`. + +Five is the minimum number of scalar products in the usual bilinear +model over Q(i), with linear input forms and linear output decoding. +Among integral point-evaluation interpolation schemes, denominator +height one in pi is also optimal. These are algebraic statements, not +native, recursive or bit-operation tariffs. + +## The square of evaluation points + +Let A(z) = a_0+a_1 z+a_2 z^2 and similarly B(z). Use the five points + + 0, 1, i, pi, infinity. + +Infinity means the leading coefficient, so its product is a_2 b_2. +For c = (c_0,...,c_4), the five polynomial evaluations form Vc, where + + V = [1 0 0 0 0] + [1 1 1 1 1] + [1 i -1 -i 1] + [1 pi 2i -2+2i -4] + [0 0 0 0 1]. + +The determinant is 2. One way to see this is to expand at the infinity +row and use the cubic Vandermonde determinant on 0,1,i,pi. Its six +differences multiply to 2. Each finite Lagrange denominator has exactly +one factor pi, up to a Gaussian unit. Thus every entry of V^-1 lies in +pi^-1 G. This statement concerns the entries, and does not claim that +one scalar division suffices for the entire decoder. + +The following row operations give a more direct constructive proof. +Number rows 0,...,4. Starting from V, perform in the stated order: + +1. Subtract row 0 and row 4 from each of rows 1 and 2. Subtract row 0 + from row 3 and add four times row 4 to row 3. +2. Subtract i times row 1 from row 2. Subtract pi times row 1 from + row 3. Add i times row 2 to row 3. Add (1-i) times row 3 to row 2. +3. Divide row 2 by -pi and row 3 by i*pi. +4. Subtract rows 2 and 3 from row 1. + +After step 1 the nontrivial middle block has rows + + [1, 1, 1], [i, -1, -i], [pi, 2i, -2+2i]. + +After step 2 it has rows `[1,1,1]`, `[0,-pi,0]`, +`[0,0,i*pi]`. Steps 3 and 4 produce the identity. There are exactly +twelve coefficient ADDs and two SCALEs. Call their product D; then +DV=I. Reversing and inverting these operations implements V with +twelve coefficient ADDs and two integral SCALEs. + +The sole denominators in D are the two step-3 divisors. In particular, +the square removes the factor 3 in the historical 0,1,-1,2,infinity +interpolation without increasing its five bilinear products. It does +not assert a lower total scalar, native or physical cost. + +## Dirty outputs and scratch restoration + +First encode the five dirty outputs by V. Their current values become +Vy. Add A(z)B(z) to the corresponding output at each of the five points. +Evaluation commutes with polynomial multiplication, so these additions +give exactly Vy+Vc = V(y+c). Finally apply D, obtaining y+c. +The preexisting y is neither cleared nor assumed zero. + +At 0 and infinity, the PRODUCT inputs are the original a_0,b_0 and +a_2,b_2. At each of 1,i,pi, accumulate the three terms of A(z) into +the first clean field and the three terms of B(z) into the second. +Use the fields in one PRODUCT call, then reverse the six coefficient +ADDs. PRODUCT preserves its sources, so both fields return to zero. +They are reused only after restoration. The six public inputs are +never modified, including during evaluation and cleanup. + +Each of those three sites pays twelve coefficient ADDs including +cleanup, for 36 in total. Encoding and decoding pay 24 more ADDs and +four SCALEs. There are exactly five PRODUCT calls, not ten. Products +are added directly into the encoded dirty outputs; no product scratch +field has to be uncomputed. The word has 69 instructions on thirteen +Gaussian fields: six preserved inputs, five dirty outputs and two +initially clean evaluation fields. + +All encoder operations are integral. After the five products, the +outputs are V(y+c) with y+c in G^5. Every decoder prefix maps V times +an integral vector to an integral vector: this is immediate for the +ADDs; before the two divisions the affected rows are respectively +-pi and i*pi times one coordinate. Thus both divisions are exact. +This proves the integer-grid claim for all inputs, beyond finite tests. +It also proves the inverse word by reversing every operation. + +The same identity holds in an associative R-algebra with central i. +Polynomial expansion preserves the order a_j b_l, so no commutativity +of the data entries is needed. The executable implements scalar G only. + +## Sharp denominator and product obstructions + +First consider any five homogeneous degree-four evaluations at +Gaussian-integer point pairs (u,v). Such a row is + + (v^4, u v^3, u^2 v^2, u^3 v, u^4). + +Modulo pi, G/(pi) is F2. A nonzero pair reduces to one of the three +projective points (0,1), (1,0), (1,1); a zero pair gives a zero row. +The reduced evaluation matrix therefore has rank at most three. +It cannot have an integral inverse, since reducing that inverse would +give rank five. Allowing extra integral linear preprocessing of these +five returned evaluations does not raise their rank. + +Consequently no such interpolation scheme has all decoder entries in +G. If decoder entries are Gaussian dyadics, at least one has negative +pi valuation. The constructed V has all entries of its inverse in +pi^-1 G, and eight entries outside G, so height one is attained and +optimal. This obstruction assumes integral evaluation forms and linear +interpolation from those values. It excludes neither non-evaluation +bilinear algorithms nor moving divisions into nonintegral encoders. + +For the product count, flatten the convolution tensor with its output +index on one side. Its five rows have disjoint, nonempty supports among +the nine ordered monomials a_j b_l, hence rank five over Q(i). A product +of one linear a-form and one linear b-form, followed by a linear output +map, contributes rank at most one to this flattening. At least five +such products are necessary. The construction attains five. This is +the standard bilinear-rank argument; arbitrary nonlinear circuits and +unrelated native operators are outside its hypotheses. + +## Relevance and limits + +Gonzalo Mier's PR3974 supplies the historical Toom-3 screen, five-product +comparison and missing source-embedding question. Its calculations are +cited premises; none is replayed or audited here. The new contribution +is this source-relative Gaussian-dyadic interpolation, its optimal +denominator height, and its literal restoring five-call boundary. +Toom-Cook evaluation and Lagrange interpolation are classical; no +global literature priority for complex Toom formulas is claimed. + +Chris R / Clear1nsight's PR3992 already excludes the stated same-width +Toom-only boundary for the first selected nine-climb group. Changing +interpolation nodes supplies no extra information channel and does +not bypass that obstruction. This module needs an actual bilinear +convolution consumer, rather than nine independent linear outputs. +The six inputs, five outputs and clean fields must have compatible +frames, placement, ranges and ownership. The clean fields are an +explicit resource premise, not free dirty workspace. Their admission, +movement, exact Gaussian division, PRODUCT implementation, coefficient +access, precision, stock and complete signed recursive invoice are +unpriced. No selected record or frontier changes, and all five selected +framework assumptions retain their status. + +## Executable verification and resource scope + +`verify.py` independently forms and rationally inverts V, compares all +five columns of both literal transforms, checks 36 real/imaginary +bilinear coefficient cases and ten dirty-output columns, and checks +complete endpoints on 729 real cube cases, 257 complex dirty cases, +one large signed case and the maximum 4096-bit entrance. It exercises +the complete inverse as stated in the receipt. Every instruction +omission is detected on nine explicitly enumerated basis fixtures. +The binary projective obstruction is separately enumerated. Written +proofs supply the universal claims; these checks supply bounded exact +construction evidence. + +The code has no recursion, network, subprocess, dynamic execution or +output-file writes. Program lengths are bounded by 128; the actual +word has 69 instructions. Registers have at most 4096-bit components +on entry. The mathematical identity has no bit-size bound. A returned +value may exceed the API entrance cap, so composition with the inverse +requires checking that cap; inverse round trips are tested on the +257 complex fixtures. The two large fixtures test forward execution. + +Power-of-Ten rule 3 deviation: CPython allocates integers, tuples and +Fractions dynamically. The scientific run has thirteen registers, five +products, two 5-by-5 rational matrices and finitely bounded fixture +domains; only one endpoint fixture is live. Each coefficient is fixed, +and all data expressions have degree at most two, bounding intermediate +bit lengths by twice the entrance bit length plus a fixed constant. +The public finite word is the declared program or its inverse, not an +untrusted program language. The nine omission fixtures and API/domain +controls exercise failure paths. A fixed-storage implementation would +need a separately charged bit-array backend and is not supplied here. + +Every function is checked to fit within sixty physical lines. All +runtime checks use explicit exceptions and remain enabled under -O. +Warning-strict normal/optimized execution and AST inspection are the +available local Python diagnostics. No static type-checker proof or +production diagnostic-policy change is claimed. A generated stdout +receipt binds all package files by SHA256; no receipt is handwritten. diff --git a/research/gaussian-dyadic-toom3/README.md b/research/gaussian-dyadic-toom3/README.md new file mode 100644 index 0000000000..03a2c56e7f --- /dev/null +++ b/research/gaussian-dyadic-toom3/README.md @@ -0,0 +1,111 @@ +# Five-product Toom-3 with only Gaussian-dyadic interpolation + +This contribution was produced by Nick Petalas. Apache-2.0. + +Claim type: scoped algebraic proof and explicit restoring construction, +with exact finite corroboration. No new kappa or selected-frontier change. + +The Gaussian square `0, 1, i, 1+i`, together with infinity, replaces the +odd-denominator interpolation in Gonzalo Mier's +[PR3974](https://github.com/CrocSwap/integer-mult-bounds/pull/3974) +Toom-3 screen. Five products still recover all five coefficients of the +product of two degree-two polynomials. The evaluation matrix has +determinant 2, and every inverse entry belongs to `(1+i)^(-1) Z[i]`. +No odd division is required. Height one in `1+i` is optimal among +integral point-evaluation schemes with Gaussian-dyadic linear decoding. + +The literal word preserves six input fields, adds the convolution to +five arbitrary dirty outputs, and restores two initially clean fields. +It pays exactly five additive PRODUCT calls, sixty coefficient ADDs +and four SCALEs. A coefficient ADD is a charged macro with its explicit +Gaussian-integer coefficient. This is not a scalar-operation speedup +comparison with PR3974. Two SCALEs multiply by associates of `1+i`; +two divide by them exactly. All intermediate data remain Gaussian +integers on the declared boundary. Encoding the dirty outputs before +the five calls avoids product-scratch uncomputation. + +[PROOF.md](PROOF.md) gives the complete contract, twelve-ADD decoder, +restoration proof, denominator obstruction and standard bilinear-rank +proof that five products are necessary. [circuit.py](circuit.py) emits +the complete 69-instruction word; [verify.py](verify.py) checks it against +separate schoolbook and rational-matrix oracles. + +## Reproduce + +From the repository root, with the CPython 3.12 standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/gaussian-dyadic-toom3/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/gaussian-dyadic-toom3/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/gaussian-dyadic-toom3 +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/gaussian-dyadic-toom3 --check-source-history +``` + +Another CPython 3.12 executable may replace the local path. The last +command requires committed package bytes and full Git history. The +scientific checker is read-only and Git-free. It prints a generated +SHA256-bound receipt with `PASS_GAUSSIAN_DYADIC_TOOM3`. + +Both normal and optimized checks cover all 25 inverse entries, five +encoder and five decoder columns, 36 real/imaginary tensor coefficient +cases, ten dirty-output columns, 988 complete endpoint fixtures and +all 69 single-instruction omission controls. Complete inverse checks +cover the 729 real cube and 257 complex fixtures as described in the +proof. Five invalid entrances and one inexact division reject. +Warning-strict execution and an AST function-size check remain active +under optimization. The written proofs provide the universal quantifiers. + +## Limits and predecessor credit + +The result removes an arithmetic denominator, not the missing physical +interface. Chris R / Clear1nsight's +[PR3992](https://github.com/CrocSwap/integer-mult-bounds/pull/3992) +already excludes the specified same-width Toom-only replacement for +the first historical nine-climb group. The new interpolation supplies +no extra information channel and does not bypass that obstruction. +No selected-provider convolution sub-tensor or new native supplier is +claimed. The two clean fields are an explicit resource premise. +Their admission, coefficient access, compatible frames, PRODUCT +implementation, physical routing, precision, stock and complete +recursive/outer invoice remain unpriced. All five selected framework +assumptions retain their status. Independent human and formal +proof-kernel review are unclaimed. + +The executable accepts scalar Gaussian-integer entrances through 4096 +bits per component. Its output can exceed that cap, so a later API call +must check its own entrance bound. The mathematical proof has no bit +cap. Arbitrary dirty evaluation scratch is unsupported. The denominator +obstruction assumes integral point evaluations; it does not exclude +non-evaluation algorithms or nonintegral input encoders. The five-product +lower bound is the standard bilinear model, not an arbitrary-circuit +lower bound. No native or selected cold replay, Lean or Docker ran. + +Credit Gonzalo Mier for the source screen and missing embedding question; +Chris R / Clear1nsight for the typed-boundary obstruction; Josie Elliston, +Arham Tahir and the retained PR1094, Clifford and Toom-screen lineage. +Classical Toom-Cook evaluation, Lagrange interpolation and tensor +flattening retain their credit. No global literature priority for +complex Toom formulas is claimed. Predecessor code, numerical counts +and scientific verifiers are not replayed or audited by this package. + +Canonical base is `7c49fe32c55de02c2c873655c804b16e4c3fef0a`, priority +revision 8, selected PR6030. [SOURCES.json](SOURCES.json) pins provenance +only; no predecessor executable or pending Git object is a runtime +dependency. [TASK.json](TASK.json) records the changed side-result scope +and the [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19372301). +Main/general-form searches, live open PRs, handoffs, active Discussions, +recent account work and local reservations were checked. Arbitrary +historical diffs and unpublished work remain coverage limits. + +## Open next questions + +1. Can a genuine bilinear convolution consumer use this interface with a + favorable complete paid invoice? First specify its exact coefficient + triples, five outputs, bypasses and native product semantics. The + missing physical caller and signed invoice block an algorithmic gain. +2. Can the five-call advantage survive arbitrary dirty evaluation scratch + or fully charged clean-field admission? First state that workspace + contract and charge every extra product and field pass. This package + provides neither a dirty-scratch construction nor a clean-field tariff. + +The structured questions and blockers are in [TASK.json](TASK.json). diff --git a/research/gaussian-dyadic-toom3/SOURCES.json b/research/gaussian-dyadic-toom3/SOURCES.json new file mode 100644 index 0000000000..19104cc359 --- /dev/null +++ b/research/gaussian-dyadic-toom3/SOURCES.json @@ -0,0 +1,30 @@ +{ + "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/complex-toom3-five-product-screen/README.md", + "usage": "provenance", + "git_blob": "a390e64b68a43f61724130a8d02f35c4c11d8b06", + "sha256": "a41ce2de2bb1f6087383da64f0e71fe84e11526eb748ac734fc669533bb05f41" + }, + { + "path": "research/selected-toom3-typed-block/README.md", + "usage": "provenance", + "git_blob": "ad87055215a158817ff90f7599c012cf7a69cf3d", + "sha256": "259a0d675673adb0a5005cbd939029c013acf58b238d18ae216996505293a3a2" + } + ] +} diff --git a/research/gaussian-dyadic-toom3/TASK.json b/research/gaussian-dyadic-toom3/TASK.json new file mode 100644 index 0000000000..806c69713c --- /dev/null +++ b/research/gaussian-dyadic-toom3/TASK.json @@ -0,0 +1,96 @@ +{ + "schema_version": 1, + "task_id": "joint-query-controller", + "priority_revision": 8, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "original_card": { + "id": "joint-query-controller", + "question": "Can a changed query demand or caller remove real work while satisfying native chronology and restoration?", + "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": "Choose an exact caller and a new demand/interface hypothesis. Read the scoped #5617/#5631/#5649/#5747 and #5720/#5745 objections before rebuilding an excluded schedule. Compare the complete matched source/consumer protocols including all retained helper outputs. For an active-mode injection, first check #5745: its canonical delivery claim repays the eight removed centre jobs. Audit that exact claim or change its channel/feedback hypothesis; do not repeat the same free-injection search. Stop if the full favorable budget fails or the required restored output is unobservable.", + "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": [ + "query demand", + "active mode", + "5720", + "5745", + "5747", + "caller" + ], + "existing_checks": [ + { + "scope": "PR #4166: author-checked installed producer/service/return/bridge connection; native-component comparison loses.", + "evidence": "research/qq16-caller-install/README.md", + "remaining": "Complete matched physical protocol bill, or changed source-compatible demand/circuit; no affordable supplier yet.", + "status": "author-checked", + "source_commit": "0b082d22a0e9a442d264ab0633e35ef26c790630", + "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": "Replace the odd-denominator five-point Toom-3 interpolation by a Gaussian-dyadic square evaluation, prove sharp integral-evaluation denominator height, and emit a five-product word preserving six inputs and arbitrary dirty outputs while restoring two initially clean fields.", + "scope_change_reason": "This is a new algebraic bilinear interface, rather than an edit to the selected linear caller. PR3974 poses a missing Toom embedding; PR3992 excludes its first same-width candidate. This side result removes an arithmetic denominator without claiming either embedding or complete supplier acceptance.", + "bottleneck_link": "A conditional bilinear replacement needs a legal coefficient ring and full restoration. Gaussian-dyadic interpolation eliminates the odd divisor 3 in the retained Toom screen, but does not supply an actual selected-provider sub-tensor or its physical invoice.", + "budget_minutes": 60, + "stop_rule": "Stop after the first exact denominator improvement and full restoring word. Do not search for larger Toom blocks or claim the excluded PR3992 boundary is repaired.", + "outcome": "completed", + "evidence": "PROOF.md proves the five-product identity, dirty-output restoration, exact Gaussian divisions, optimal pi denominator height within integral point-evaluation schemes, and the usual five-product bilinear lower bound. The standalone checker constructs an independent rational inverse, checks all 25 entries and both literal matrix transforms, all 46 tensor/dirty columns, 988 complete endpoint fixtures, all 69 instruction omissions, five invalid entrances and an inexact-division control.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can a genuine bilinear convolution consumer use this Gaussian-dyadic interface with a favorable complete paid invoice?", + "why_it_matters": "The ring improvement cannot lower the selected recursive cost without an actual data-preserving caller.", + "first_step": "Identify exact paired coefficient triples and all five convolution outputs on one caller, including bypasses, compatible frames and product semantics. Do not reuse the excluded same-width PR3992 boundary.", + "blocked_by": "No selected-provider sub-tensor, physical PRODUCT implementation, frame delivery or complete signed invoice is supplied." + }, + { + "question": "Can the five-call module preserve its advantage with arbitrary dirty evaluation workspace or with fully charged clean-field admission?", + "why_it_matters": "The present restoring word explicitly needs two initially zero fields.", + "first_step": "State a priced workspace interface and compare the entire evaluation/cleanup program, counting every extra product and field pass.", + "blocked_by": "A physical clean-field allocation/erasure contract or a cheaper arbitrary-dirty construction is missing." + } + ], + "coordination": { + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19372301", + "upstream_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "checked_utc": "2026-11-03T11:16:18.409004+00:00", + "coverage": "Live open PRs, latest handoff and active Discussions, recent account PRs, local reservations, main README searches and merged/general-form searches. Arbitrary diffs and unpublished work are not covered." + } +} diff --git a/research/gaussian-dyadic-toom3/VERIFY.json b/research/gaussian-dyadic-toom3/VERIFY.json new file mode 100644 index 0000000000..fff4128502 --- /dev/null +++ b/research/gaussian-dyadic-toom3/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Complete exact tensor, interpolation, preserving/restoring word, inverse, domain and omission controls; generated source-hash receipt" + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Same complete exact checks under optimized Python" + } + ] +} diff --git a/research/gaussian-dyadic-toom3/circuit.py b/research/gaussian-dyadic-toom3/circuit.py new file mode 100644 index 0000000000..47c2705197 --- /dev/null +++ b/research/gaussian-dyadic-toom3/circuit.py @@ -0,0 +1,114 @@ +"""Five ordered products, Gaussian-integer data, and two clean restored fields.""" + +from math import gcd + +Gaussian = tuple[int, int] +Scalar = tuple[int, int, int] +Instruction = tuple[str, int, int, int, Scalar] +ONE: Scalar = (1, 0, 1) +ZERO: Gaussian = (0, 0) +MAX_BITS = 4096 + + +def multiply(a: Gaussian, b: Gaussian) -> Gaussian: + return a[0] * b[0] - a[1] * b[1], a[0] * b[1] + a[1] * b[0] + + +def scaled(a: Gaussian, coefficient: Scalar) -> Gaussian: + real, imag, denominator = coefficient + if denominator not in (1, 2): + raise ValueError("only the declared integral or half-integral scalars") + x, y = multiply(a, (real, imag)) + if x % denominator or y % denominator: + raise ValueError("inexact Gaussian division") + return x // denominator, y // denominator + + +def inverse(instruction: Instruction) -> Instruction: + kind, target, source, other, (a, b, d) = instruction + if kind in ("ADD", "PRODUCT"): + coefficient = (-a, -b, d) + elif kind == "SCALE": + norm = a * a + b * b + common = gcd(gcd(abs(a * d), abs(b * d)), norm) + if common == 0: + raise ValueError("zero SCALE") + coefficient = (a * d // common, -b * d // common, norm // common) + else: + raise ValueError("unknown instruction") + return kind, target, source, other, coefficient + + +def decoder() -> tuple[Instruction, ...]: + """Reduce V to I. Output fields are registers 6..10.""" + adds = ( + (7, 6, (-1, 0, 1)), (7, 10, (-1, 0, 1)), + (8, 6, (-1, 0, 1)), (8, 10, (-1, 0, 1)), + (9, 6, (-1, 0, 1)), (9, 10, (4, 0, 1)), + (8, 7, (0, -1, 1)), (9, 7, (-1, -1, 1)), + (9, 8, (0, 1, 1)), (8, 9, (1, -1, 1)), + ) + word = [("ADD", t, s, 0, c) for t, s, c in adds] + word.extend((("SCALE", 8, 0, 0, (-1, 1, 2)), + ("SCALE", 9, 0, 0, (-1, -1, 2)), + ("ADD", 7, 8, 0, (-1, 0, 1)), + ("ADD", 7, 9, 0, (-1, 0, 1)))) + return tuple(word) + + +def program() -> tuple[Instruction, ...]: + decode = decoder() + word = [inverse(op) for op in reversed(decode)] + word.append(("PRODUCT", 6, 0, 3, ONE)) + for target, z in ((7, (1, 0)), (8, (0, 1)), (9, (1, 1))): + evaluation = [] + for scratch, start in ((11, 0), (12, 3)): + for offset, value in enumerate(((1, 0), z, multiply(z, z))): + evaluation.append(("ADD", scratch, start + offset, 0, + (value[0], value[1], 1))) + word.extend(evaluation) + word.append(("PRODUCT", target, 11, 12, ONE)) + word.extend(inverse(op) for op in reversed(evaluation)) + word.append(("PRODUCT", 10, 2, 5, ONE)) + word.extend(decode) + return tuple(word) + + +def validate(registers: tuple[Gaussian, ...]) -> None: + if type(registers) is not tuple or len(registers) != 13: + raise ValueError("exactly thirteen Gaussian registers") + for value in registers: + if type(value) is not tuple or len(value) != 2: + raise ValueError("Gaussian integers are pairs") + for component in value: + if type(component) is not int or component.bit_length() > MAX_BITS: + raise ValueError("integer component exceeds the input contract") + if registers[11:] != (ZERO, ZERO): + raise ValueError("two initially clean evaluation fields are required") + + +def execute(registers: tuple[Gaussian, ...], word: tuple[Instruction, ...] + ) -> tuple[Gaussian, ...]: + validate(registers) + if len(word) > 128: + raise ValueError("word exceeds the finite instruction cap") + state = list(registers) + for kind, target, source, other, coefficient in word: + if not 6 <= target < 13 or not 0 <= source < 13 or not 0 <= other < 13: + raise ValueError("invalid register or modified source") + if kind == "SCALE": + state[target] = scaled(state[target], coefficient) + elif kind in ("ADD", "PRODUCT"): + value = state[source] + if kind == "PRODUCT": + if target in (source, other): + raise ValueError("aliased product target") + value = multiply(value, state[other]) + elif target == source: + raise ValueError("aliased ADD") + x, y = scaled(value, coefficient) + a, b = state[target] + state[target] = a + x, b + y + else: + raise ValueError("unknown instruction") + return tuple(state) diff --git a/research/gaussian-dyadic-toom3/verify.py b/research/gaussian-dyadic-toom3/verify.py new file mode 100644 index 0000000000..fcdbd2049f --- /dev/null +++ b/research/gaussian-dyadic-toom3/verify.py @@ -0,0 +1,232 @@ +"""Independent coefficient oracle, full restoring word, and rejection controls.""" + +import ast +from collections import Counter +from fractions import Fraction as F +import hashlib +from itertools import product +import json +from pathlib import Path +import sys + +sys.path.insert(0, str(Path(__file__).resolve().parent)) +from circuit import MAX_BITS, ZERO, decoder, execute, inverse, program, scaled + + +def need(condition: bool, message: str) -> None: + if not condition: + raise ValueError(message) + + +def expected(state: tuple, sign: int = 1) -> tuple: + """Schoolbook convolution; independent real/imaginary arithmetic.""" + output = [list(value) for value in state[6:11]] + for j in range(3): + for k in range(3): + ar, ai = state[j] + br, bi = state[3 + k] + output[j + k][0] += sign * (ar * br - ai * bi) + output[j + k][1] += sign * (ar * bi + ai * br) + return state[:6] + tuple(tuple(value) for value in output) + state[11:] + + +def fixture(values: tuple) -> tuple: + need(len(values) == 6, "six real input components") + return tuple((v, 0) for v in values) + ((2, -3),) * 5 + (ZERO, ZERO) + + +def endpoint_cases(word: tuple) -> dict: + backwards = tuple(inverse(op) for op in reversed(word)) + count = 0 + for values in product((-1, 0, 1), repeat=6): + state = fixture(values) + need(execute(state, word) == expected(state), "real cube endpoint") + need(execute(state, backwards) == expected(state, -1), "inverse endpoint") + count += 1 + for seed in range(257): + values = tuple(((seed * (j + 3) + j * j) % 37 - 18, + (seed * (2 * j + 1) + 7) % 41 - 20) for j in range(11)) + state = values + (ZERO, ZERO) + result = execute(state, word) + need(result == expected(state), "complex dirty endpoint") + need(execute(result, backwards) == state, "full restoration") + count += 1 + huge = tuple(((-1) ** j * ((1 << 1024) + j), (1 << 1019) - j) + for j in range(11)) + (ZERO, ZERO) + need(execute(huge, word) == expected(huge), "large signed endpoint") + limit = ((1 << MAX_BITS) - 1, -(1 << (MAX_BITS - 1))) + boundary = (limit,) * 11 + (ZERO, ZERO) + need(execute(boundary, word) == expected(boundary), "maximum admitted entrance") + return {"real_cube": 729, "complex_dirty": 257, "large_signed": 1, + "maximum_bits": 1, "total": count + 2} + + +def qadd(a: tuple, b: tuple) -> tuple: + return a[0] + b[0], a[1] + b[1] + + +def qmul(a: tuple, b: tuple) -> tuple: + return a[0] * b[0] - a[1] * b[1], a[0] * b[1] + a[1] * b[0] + + +def qinv(a: tuple) -> tuple: + norm = a[0] ** 2 + a[1] ** 2 + need(norm != 0, "invertible Gaussian rational") + return a[0] / norm, -a[1] / norm + + +def evaluation_matrix() -> list: + rows = [] + for z in ((F(0), F(0)), (F(1), F(0)), (F(0), F(1)), (F(1), F(1))): + row = [(F(1), F(0))] + for _ in range(4): + row.append(qmul(row[-1], z)) + rows.append(row) + rows.append([(F(int(j == 4)), F(0)) for j in range(5)]) + return rows + + +def invert_matrix(matrix: list) -> tuple: + """Rational Gauss-Jordan oracle, unrelated to the literal decoder.""" + rows = [row[:] + [(F(int(i == j)), F(0)) for j in range(5)] + for i, row in enumerate(matrix)] + determinant = (F(1), F(0)) + for column in range(5): + pivot = next(i for i in range(column, 5) if rows[i][column] != (0, 0)) + if pivot != column: + rows[column], rows[pivot] = rows[pivot], rows[column] + determinant = qmul(determinant, (F(-1), F(0))) + value = rows[column][column] + determinant = qmul(determinant, value) + rows[column] = [qmul(x, qinv(value)) for x in rows[column]] + for i in range(5): + if i != column: + value = rows[i][column] + rows[i] = [qadd(x, qmul((-value[0], -value[1]), y)) + for x, y in zip(rows[i], rows[column])] + return [row[5:] for row in rows], determinant + + +def matrix_cases() -> dict: + matrix = evaluation_matrix() + inv, determinant = invert_matrix(matrix) + need(determinant == (2, 0), "determinant two") + nonintegral = 0 + for row in inv: + for value in row: + integral = all(x.denominator == 1 for x in value) + nonintegral += not integral + times_pi = qmul(value, (F(1), F(1))) + need(all(x.denominator == 1 for x in times_pi), "one pi denominator") + need(nonintegral > 0, "division cannot disappear") + for j in range(5): + encoded = tuple((int(matrix[i][j][0]), int(matrix[i][j][1])) for i in range(5)) + state = (ZERO,) * 6 + encoded + (ZERO, ZERO) + target = (ZERO,) * 6 + tuple((int(i == j), 0) for i in range(5)) + (ZERO, ZERO) + need(execute(state, decoder()) == target, "literal decoder column") + encode = tuple(inverse(op) for op in reversed(decoder())) + need(execute(target, encode) == state, "literal encoder column") + return {"entries": 25, "nonintegral_inverse_entries": nonintegral, + "determinant": [2, 0], "decoder_columns": 5, "encoder_columns": 5} + + +def tensor_cases(word: tuple) -> int: + count = 0 + for left, right, phase_a, phase_b in product(range(3), range(3), (0, 1), (0, 1)): + state = [ZERO] * 13 + state[left] = (int(phase_a == 0), int(phase_a == 1)) + state[3 + right] = (int(phase_b == 0), int(phase_b == 1)) + need(execute(tuple(state), word) == expected(tuple(state)), "tensor coefficient") + count += 1 + for target, phase in product(range(6, 11), (0, 1)): + state = [ZERO] * 13 + state[target] = (int(phase == 0), int(phase == 1)) + need(execute(tuple(state), word) == tuple(state), "arbitrary dirty output column") + count += 1 + return count + + +def binary_obstruction() -> dict: + rows = set() + for u, v in product(range(2), repeat=2): + if u or v: + rows.add(tuple(u ** j * v ** (4 - j) % 2 for j in range(5))) + need(len(rows) == 3, "three projective rows over F2") + spans = {tuple(0 for _ in range(5))} + for row in sorted(rows): + spans |= {tuple(a ^ b for a, b in zip(x, row)) for x in tuple(spans)} + need(len(spans) == 8, "evaluation rank three, not five") + return {"projective_rows": 3, "span_size": 8} + + +def controls(word: tuple) -> dict: + killed = 0 + states = [] + for j in range(9): + state = [ZERO] * 13 + state[j // 3] = (1, 1) + state[3 + j % 3] = (2, -1) + state[6:11] = [(2, -3)] * 5 + states.append(tuple(state)) + for omitted in range(len(word)): + mutant = word[:omitted] + word[omitted + 1:] + detected = False + for state in states: + try: + detected |= execute(state, mutant) != expected(state) + except ValueError: + detected = True + need(detected, f"undetected instruction omission {omitted}") + killed += 1 + invalid = [(), fixture((0,) * 6)[:12], + fixture((0,) * 6)[:11] + ((1, 0), ZERO), + ((True, 0),) + fixture((0,) * 6)[1:], + ((1 << (MAX_BITS + 1), 0),) + fixture((0,) * 6)[1:]] + for state in invalid: + try: + execute(state, word) + except ValueError: + continue + raise ValueError("accepted invalid entrance") + try: + scaled((1, 0), (-1, 1, 2)) + except ValueError: + return {"instruction_omissions": killed, "invalid_entrances": len(invalid), + "inexact_division": 1} + raise ValueError("accepted inexact pi division") + + +def diagnostics() -> dict: + lengths = {} + for name in ("circuit.py", "verify.py"): + path = Path(__file__).resolve().parent / name + tree = ast.parse(path.read_text()) + for node in ast.walk(tree): + if isinstance(node, (ast.FunctionDef, ast.AsyncFunctionDef)): + length = node.end_lineno - node.lineno + 1 + need(length <= 60, "one-page function bound") + lengths[f"{name}:{node.name}"] = length + return {"functions": len(lengths), "maximum_function_lines": max(lengths.values())} + + +def main() -> None: + need(len(sys.argv) == 1, "no command-line arguments") + word = program() + counts = dict(Counter(op[0] for op in word)) + need(counts == {"ADD": 60, "SCALE": 4, "PRODUCT": 5}, "full word invoice") + result = {"status": "PASS_GAUSSIAN_DYADIC_TOOM3", "claim_type": "scoped construction", + "invoice": counts, "tensor_cases": tensor_cases(word), + "matrix": matrix_cases(), "endpoints": endpoint_cases(word), + "binary_obstruction": binary_obstruction(), "controls": controls(word), + "diagnostics": diagnostics()} + hashes = {} + for path in sorted(Path(__file__).resolve().parent.iterdir()): + if path.is_file(): + need(path.stat().st_size <= 128 * 1024, "package file-size bound") + hashes[path.name] = hashlib.sha256(path.read_bytes()).hexdigest() + result["package_sha256"] = hashes + print(json.dumps(result, sort_keys=True)) + + +if __name__ == "__main__": + main()