From 1f1ea775d1d67800f29e28d7c2d174fb34964b05 Mon Sep 17 00:00:00 2001 From: Ali Romman <226877337+aliromman@users.noreply.github.com> Date: Fri, 23 Oct 2026 14:25:57 -0500 Subject: [PATCH] Evaluate multi-shift nullity counts by exact convolution --- .../BENCHMARK.json | 34 +++++ .../DISCUSSION-5261.md | 105 +++++++++++++ .../multishift-nullity-convolution/PROOF.md | 82 ++++++++++ .../multishift-nullity-convolution/README.md | 69 +++++++++ .../RESULT.json | 12 ++ .../SOURCES.json | 42 ++++++ .../multishift-nullity-convolution/TASK.json | 99 ++++++++++++ .../VERIFY.json | 38 +++++ .../benchmark.py | 27 ++++ .../multishift-nullity-convolution/count.py | 63 ++++++++ .../multishift-nullity-convolution/verify.py | 142 ++++++++++++++++++ 11 files changed, 713 insertions(+) create mode 100644 research/multishift-nullity-convolution/BENCHMARK.json create mode 100644 research/multishift-nullity-convolution/DISCUSSION-5261.md create mode 100644 research/multishift-nullity-convolution/PROOF.md create mode 100644 research/multishift-nullity-convolution/README.md create mode 100644 research/multishift-nullity-convolution/RESULT.json create mode 100644 research/multishift-nullity-convolution/SOURCES.json create mode 100644 research/multishift-nullity-convolution/TASK.json create mode 100644 research/multishift-nullity-convolution/VERIFY.json create mode 100644 research/multishift-nullity-convolution/benchmark.py create mode 100644 research/multishift-nullity-convolution/count.py create mode 100644 research/multishift-nullity-convolution/verify.py diff --git a/research/multishift-nullity-convolution/BENCHMARK.json b/research/multishift-nullity-convolution/BENCHMARK.json new file mode 100644 index 0000000000..9ed81d6ac6 --- /dev/null +++ b/research/multishift-nullity-convolution/BENCHMARK.json @@ -0,0 +1,34 @@ +{ + "python": "3.12.13", + "platform": "macOS-26.6.1-arm64-arm-64bit", + "q": 7, + "n": 12, + "nullities": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "count": "14205377417054223568605086286850373466178389542026476613751214157362164095416027117142999261709388305840065638313998993984", + "seconds": { + "simplex": [ + 0.736021124990657, + 0.7415261249989271, + 0.7229337090393528, + 1.0183688329998404, + 1.0691068340092897 + ], + "convolution": [ + 0.001355165964923799, + 0.001228584034834057, + 0.0013631670153699815, + 0.0012127910158596933, + 0.001460874977055937 + ] + }, + "median_speedup": 547.1847317539613, + "timing_is_not_an_acceptance_test": true +} diff --git a/research/multishift-nullity-convolution/DISCUSSION-5261.md b/research/multishift-nullity-convolution/DISCUSSION-5261.md new file mode 100644 index 0000000000..8f8f54b88e --- /dev/null +++ b/research/multishift-nullity-convolution/DISCUSSION-5261.md @@ -0,0 +1,105 @@ +DONE: exact joint nullities at any number of distinct scalar shifts. + +This answers the first open question in Nick Petalas's [PR #4803](https://github.com/CrocSwap/integer-mult-bounds/pull/4803), which asks for a three-shift formula. The result counts all shifts at once and retains their dependence. It does not change kappa or supply a paid header cover. + +**Source and scope.** Start point: canonical main `ff3cc58e370d0f678e529246f8c73e8094e18fcf`, priority revision 7. The [source question and two-shift result](https://github.com/CrocSwap/integer-mult-bounds/blob/ff3cc58e370d0f678e529246f8c73e8094e18fcf/research/schur-rank-pair-law/README.md) credit @petalas for the two-eigenspace count and ssafwann's [PR #4678](https://github.com/CrocSwap/integer-mult-bounds/pull/4678) for the binary Schur-header application. The argument below extends the same subspace-counting method. Gaussian binomial inversion is classical; no priority claim outside this repository is made. + +**Formula.** Let q be a prime power, V=F_q^n, and let lambda_1,...,lambda_t be distinct elements of F_q, so t<=q. Let a_i be nonnegative integers. Write G(N,k) for the Gaussian binomial coefficient, with value zero outside 0<=k<=N. For k=(k_1,...,k_t), put K=sum_i k_i and s_i=sum_{j=a_i, sum_i k_i<=n} + M(k) * product_i (G(k_i,a_i) * mu(k_i-a_i)). +``` + +If sum a_i>n, the count is zero. An empty shift list gives q^(n*n). The formula depends on the number of distinct shifts, not on their values. For one vector a it has at most binomial(n-sum(a)+t,t) summands. This is a bound on arithmetic summands for fixed t, not a bit-complexity or measured runtime claim. + +**Proof.** Count pairs (H,(W_i)), where each W_i has dimension k_i and H acts as lambda_i I on W_i. Eigenspaces for distinct eigenvalues have a direct sum. Given the first i-1 subspaces, their sum has dimension s_i. Choose the image of W_i in V/(sum_{ja it contains the zero factor at j=0; for e=a it is the empty product. Applying this identity to every coordinate gives exactly the required indicator. This proves the formula for every n, q and set of distinct shifts. + +**Checks and use.** The script below compares the formula to an independent Gaussian-elimination census in ten contexts: q=2 and q=3, n=0,...,3, using all scalar shifts; and q=5, n=2, using three and five shifts. It checks 21,549 matrix/context cases and all 400 nullity bins. It also checks impossible dimensions and an empty shift list. Calibrations over F_3 are N_2(0,0,0)=18, N_3(0,0,0)=3456, and N_3(1,1,1)=1404. These are exact finite checks, not the proof of the all-size claim. + +Save the following block as `multiple_shift_nullities.py` and run CPython 3.12: + +```sh +python3.12 -I -W error -B multiple_shift_nullities.py +python3.12 -I -W error -O -B multiple_shift_nullities.py +``` + +Both modes passed with CPython 3.12.13. Expected output: + +```text +PASS_MULTIPLE_SHIFT_NULLITIES contexts=10 matrices=21549 bins=400 no_new_kappa +``` + +```python +from itertools import product +from collections import Counter + +def ck(x,s): + if not x:raise ValueError(s) +def gb(n,k,q): + if not 0<=k<=n:return 0 + a=b=1 + for i in range(k):a*=q**(n-i)-1;b*=q**(k-i)-1 + ck(a%b==0,'Gaussian integrality');return a//b +def count(q,n,a): + t=len(a) + if any(x<0 for x in a) or sum(a)>n:return 0 + ans=0 + for k in product(*(range(x,n+1) for x in a)): + if sum(k)>n:continue + taken=0;moment=1;weight=1 + for x,y in zip(k,a): + moment*=gb(n-taken,x,q)*q**(taken*x);taken+=x + d=x-y;weight*=gb(x,y,q)*(-1)**d*q**(d*(d-1)//2) + moment*=q**(n*(n-taken));ans+=moment*weight + return ans +def rank(a,q): + a=[r[:] for r in a];r=0;n=len(a) + for j in range(n): + v=next((i for i in range(r,n) if a[i][j]%q),None) + if v is None:continue + a[r],a[v]=a[v],a[r];u=pow(a[r][j],-1,q);a[r]=[(x*u)%q for x in a[r]] + for i in range(n): + if i!=r: + c=a[i][j];a[i]=[(x-c*y)%q for x,y in zip(a[i],a[r])] + r+=1 + return r +contexts=[(2,n,2) for n in range(4)]+[(3,n,3) for n in range(4)]+[(5,2,3),(5,2,5)] +matrices=0;bins=0 +for q,n,t in contexts: + hist=Counter() + for values in product(range(q),repeat=n*n): + a=[list(values[i*n:(i+1)*n]) for i in range(n)] + dims=tuple(n-rank([[(a[i][j]-(lam if i==j else 0))%q for j in range(n)] for i in range(n)],q) for lam in range(t)) + hist[dims]+=1;matrices+=1 + for dims in product(range(n+1),repeat=t): + ck(count(q,n,dims)==hist[dims],('census',q,n,dims));bins+=1 + ck(sum(hist.values())==q**(n*n),'total') +ck(count(3,3,(0,0,0))==3456,'irreducible cubic calibration') +ck(count(3,3,(1,1,1))==1404,'three distinct eigenspaces') +ck(count(3,2,(1,1,1))==0,'dimension control') +ck(count(3,2,(0,0,0))==18,'irreducible quadratic calibration') +ck(count(3,3,())==3**9,'empty shift set') +print('PASS_MULTIPLE_SHIFT_NULLITIES contexts='+str(len(contexts))+' matrices='+str(matrices)+' bins='+str(bins)+' no_new_kappa') +``` + +**Limits and handoff.** No predecessor executable, extension-field matrix census, Lean proof, Docker run, selected cold replay or physical supplier was tested. The proof, rather than a modulo-prime implementation, supplies the extension-field claim. To use the result, replace a sum over compressed matrices by this exact joint-nullity distribution only when the weight depends on these nullities. The nonbinary Schur criterion, actual request weights, cover selection/emission, physical reads, dirty restoration and complete bill remain separate obligations. A useful next step is to state one nonbinary equal-scalar Schur weight and apply this distribution to it. + +Before this work, the overlap helper covered all 7,091 current local notes, 323 open PRs and 4,526 Discussion records with complete pagination. Targeted all-state PR search and the current source question were also checked. The search found the predecessor question; arbitrary diffs and unpublished work remain outside that coverage. Prepared by @aliromman with OpenAI Codex assistance. No independent human or formal proof-kernel review is claimed. New text and code: Apache-2.0. diff --git a/research/multishift-nullity-convolution/PROOF.md b/research/multishift-nullity-convolution/PROOF.md new file mode 100644 index 0000000000..903f550dbf --- /dev/null +++ b/research/multishift-nullity-convolution/PROOF.md @@ -0,0 +1,82 @@ +# Exact coefficient reduction + +Let q be a prime power. Let n >= 0 and let lambda_1,...,lambda_t be +distinct elements of F_q, with 0 <= t <= q. Let a_i >= 0 and R=sum a_i. +The target N(a) counts n by n matrices H with nullity(H-lambda_i I)=a_i. +If R>n, distinct eigenspaces cannot fit, and N(a)=0. + +This proof starts from the exact multi-shift formula in the retained +[Discussion](DISCUSSION-5261.md). That formula extends Nick Petalas's +[two-shift proof](../schur-rank-pair-law/PROOF.md). We claim the coefficient +reduction, not a new eigenspace counting formula. + +Put P_j=product_{l=1}^j(q^l-1), P_0=1, and m=n-R. Define coefficients by + +```text +C(z) = product_i [sum_{u=0}^m z^u / (P_u q^(a_i u))] mod z^(m+1) +c_U = coefficient of z^U in C(z). + +N(a) = P_n / product_i P_(a_i) + * sum_{U=0}^m (-1)^U + q^[n(n-R-U) + binom(R+U,2) - sum_i binom(a_i,2)] + c_U / P_(m-U). +``` + +All operations use rational numbers. The final value is a nonnegative +integer because it equals the matrix count below. The exponent in the +outer sum is nonnegative. The first term is nonnegative, and +binom(R+U,2) >= sum_i binom(a_i,2). + +## Derivation + +In the prior formula write k_i=a_i+u_i, K=sum k_i=R+U, and +s_i=sum_{j=0 with sum u_i=U is c_U. +Grouping the prior finite sum by U proves the formula for every stated +n, q and nullity vector. For t=0, C=1 and the expression is q^(n*n). +For m=0, it reduces to P_n q^[binom(n,2)-sum_i binom(a_i,2)] / +product_i P_(a_i), as required for a direct sum of full eigenspaces. + +## Algorithm and cost + +Multiply each factor into an array of m+1 coefficients and discard +higher degrees after each factor. This does not change any retained +coefficient. The implementation performs exactly t(m+1)(m+2)/2 rational +coefficient products. Product construction and the final sum add O(n+tm) +arithmetic operations. The complete bound is O(n+t(m+1)^2) arithmetic +operations. It keeps O(m) live coefficients and O(n) factorial values. + +These are arithmetic counts, not bit-complexity bounds. Rational values, +integer exponents and the result can have many bits. Prime-power input +validation also has its own cost. The implementation accepts distinct +shift counts through t<=q; it does not accept a list with repeated shifts. + +The direct sum has binom(m+t,t) feasible terms. The benchmark visits only +these feasible terms; it does not compare against a wasteful Cartesian +product. A measured speedup applies only to its stated host and fixture. + +## Research boundary + +This is an exact evaluation algorithm for a known distribution. A Schur +weight must depend only on these joint nullities before this reduction +can replace its matrix sum. The actual ensemble, weight, paid selector, +header emission, reads, dirty restoration and complete supplier bill are +not supplied here. No complete multiplication exponent changes. + +Ali Romman with substantial OpenAI Codex assistance. Apache-2.0. diff --git a/research/multishift-nullity-convolution/README.md b/research/multishift-nullity-convolution/README.md new file mode 100644 index 0000000000..27e89bc0e1 --- /dev/null +++ b/research/multishift-nullity-convolution/README.md @@ -0,0 +1,69 @@ +# Multi-shift nullity convolution + +**Algorithmic improvement; no new kappa.** Evaluate the existing exact +joint-nullity distribution with O(n+t(m+1)^2) rational operations, where +m=n-sum(a_i), instead of binom(m+t,t) feasible dimension tuples. The +[proof](PROOF.md) covers every prime power and every set of distinct +scalar shifts. It does not assume independent ranks. + +The implementation keeps O(m) live coefficients and O(n) factorial +values. These are arithmetic and storage counts, not bit-complexity +claims. At q=17, n=24, t=17 and a_i=0, it uses 5525 coefficient products; +the direct formula has 151584480450 terms. [RESULT.json](RESULT.json) +retains the exact 709-digit count. + +## Evidence and replay + +The [verifier](verify.py) compares 2821 cases with the direct formula, +checks 21805 literal matrices in 11 contexts (including F4), checks 481 +nullity bins, checks three full distributions and their marginals, and +checks eleven failure controls. It also compares two-shift results with +the unchanged predecessor executable. The source hash and the saved +result must match. There are no assert-based acceptance checks. + +From the repository root, use CPython 3.12 with no third-party packages: + +```sh +python3.12 -I -W error -B research/multishift-nullity-convolution/verify.py +python3.12 -I -W error -O -B research/multishift-nullity-convolution/verify.py +python3.12 -B scripts/research_package.py --package research/multishift-nullity-convolution +python3.12 -I -B research/multishift-nullity-convolution/benchmark.py +``` + +Expected status: `PASS_MULTISHIFT_CONVOLUTION_NO_NEW_KAPPA`. +[BENCHMARK.json](BENCHMARK.json) records five alternating-order runs at +q=7,n=12,t=7. Both methods return the same exact count. The reference visits +only feasible simplex tuples. Time is not an acceptance test. The large +q=17 case was not compared with its 151 billion-term reference. + +Normal and optimized CPython 3.12.13 passed. An official Git-free package +export and the source and receipt corruption controls are recorded in the +PR evidence. No Lean, Docker, native supplier admission, selected cold +replay or full multiplication theorem was checked. The algebraic proof +has author review; no independent human or proof-kernel review is claimed. + +## Sources and attribution + +Base: `7c472563474e60185e6ca101a17622133d047e56`, priority revision 7. +[SOURCES.json](SOURCES.json) pins all consumed files. The selected result +and catalogue are historical provenance, not runtime dependencies. +The retained [Discussion #5261](DISCUSSION-5261.md) gives the multi-shift +formula and its proof. Its source URL and SHA256 are recorded; a Discussion +is mutable, so this package retains the consumed text. Nick Petalas +(@petalas) supplied the two-shift result and field arithmetic in +[PR #4803](https://github.com/CrocSwap/integer-mult-bounds/pull/4803). +The Schur application comes from ssafwann's +[PR #4678](https://github.com/CrocSwap/integer-mult-bounds/pull/4678), +as credited in that source. Gaussian inversion and generating functions +are classical methods. No external mathematical priority is claimed. + +Prepared by Ali Romman with substantial OpenAI Codex assistance. +New work: Apache-2.0. Prior source notices remain unchanged. + +## Open next questions + +State one nonbinary Schur weight for an actual producer ensemble and test +whether it depends only on these nullities. This gives a concrete use for +the faster count. A paid selection and emission algorithm, physical reads, +dirty restoration and the complete consumer bill still block a supplier +claim. This package does not reserve that work. diff --git a/research/multishift-nullity-convolution/RESULT.json b/research/multishift-nullity-convolution/RESULT.json new file mode 100644 index 0000000000..0689bebc35 --- /dev/null +++ b/research/multishift-nullity-convolution/RESULT.json @@ -0,0 +1,12 @@ +{ + "status": "PASS_MULTISHIFT_CONVOLUTION_NO_NEW_KAPPA", + "direct_comparisons": 2821, + "matrix_contexts": 11, + "matrices": 21805, + "bins": 481, + "consistency_contexts": 3, + "negative_controls": 11, + "large_count": "1835688115634210185628832138500516653723478382939376085182232943878083468080395934178922499081873390932737712440374301790695927960005939574482737925559857154024489357320384745009508671597412124286072621332213821318548099185311125938209793104947862831782550223939952893705897797175753171033120256149047132761218307291436295835214546185198268170976695505665410419661707427281750902572531228237237921422479581628527023045409610270944803812700614604535317665823833148961989255149174389540331189664118735398319932064384590774479124163427145488482401633074971921941656379095049062342912038101657070241157732364554161797989534084909366039587138360885088915507216590951563787417987222714364334469977654206158147158016", + "large_direct_summands": 151584480450, + "large_convolution_products": 5525 +} diff --git a/research/multishift-nullity-convolution/SOURCES.json b/research/multishift-nullity-convolution/SOURCES.json new file mode 100644 index 0000000000..11e7ea4ec7 --- /dev/null +++ b/research/multishift-nullity-convolution/SOURCES.json @@ -0,0 +1,42 @@ +{ + "schema_version": 1, + "base_commit": "7c472563474e60185e6ca101a17622133d047e56", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395", + "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/schur-rank-pair-law/PROOF.md", + "usage": "input", + "git_blob": "9673ed63693032fe4841400cd617d1a8122c3366", + "sha256": "d29465a73aa399c3e632b7b77ca5b31615c0de1a60cbc4984ad7c7668d3937dc" + }, + { + "path": "research/schur-rank-pair-law/README.md", + "usage": "input", + "git_blob": "f81da1f15cc3e388c57e89d8a3a36a4e6ecf3969", + "sha256": "b81dd6c355f4d13e03be85dfe76ab99b0840eeaeddaf1da65deca7d3e83046ba" + }, + { + "path": "research/schur-rank-pair-law/verify.py", + "usage": "input", + "git_blob": "8af1b3c435550c831adad88bbb1f5d5594fa20df", + "sha256": "9b378420723d2f4aa331388f65d7c12ef767e1bc5bf2d1320d78b3e1587730c4" + } + ], + "discussion": { + "url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/5261", + "updated_at": "2026-10-23T14:41:06Z", + "path": "DISCUSSION-5261.md", + "sha256": "65171c857387f44dbc855be84ad84bd7d8200e4fa84961a82fb61d778335323d" + } +} diff --git a/research/multishift-nullity-convolution/TASK.json b/research/multishift-nullity-convolution/TASK.json new file mode 100644 index 0000000000..e8a3706343 --- /dev/null +++ b/research/multishift-nullity-convolution/TASK.json @@ -0,0 +1,99 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 7, + "base_commit": "7c472563474e60185e6ca101a17622133d047e56", + "original_card": { + "id": "formal-interface-lemma", + "question": "Can one uncovered interface implication be formalized with exact caller and certificate bindings?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/gate-operand-parity-lean/README.md", + "research/staged544-certified-endpoint/README.md", + "research/unconditional-batched-crt/README.md" + ], + "methods": [ + "Formalize a missing boundary lemma identified by the selected review.", + "Audit a formal theorem-to-certificate binding independently." + ], + "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Inventory the gate-operand parity lemma (#3807) and certified endpoint arithmetic (#3857). Neither is a full multiplication proof. For #4100, audit the compact-switch statement and its hypotheses before formalizing it.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "Write one missing statement with quantified hypotheses, actual caller and existing coverage. A compact-switch lemma is a candidate only after its mathematical contract is reviewed. Establish a bounded proof plan before a separately budgeted proof-assistant build; do not rerun large Lean jobs as orientation.", + "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.", + "allowed_variations": [ + "Narrow to one formal lemma or one theorem-to-certificate binding." + ], + "scope_change_triggers": [ + "Formalizing already-covered arithmetic and claiming the full multiplication theorem." + ], + "overlap_terms": [ + "hyperplane end", + "formal interface", + "Lean binding", + "3807", + "3857", + "4100", + "gate-operand-parity-lean", + "staged544-certified-endpoint", + "unconditional-batched-crt" + ], + "existing_checks": [ + { + "scope": "PR #3807: scoped gate-operand parity formalization.", + "evidence": "research/gate-operand-parity-lean/README.md", + "remaining": "Exact theorem-to-caller binding and genuinely uncovered interface lemmas.", + "status": "author-checked", + "source_commit": "4c3530f42a6abcc48e7a6bcffd6c901911dc8269", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #3857: certified real-power moment/endpoint arithmetic.", + "evidence": "research/staged544-certified-endpoint/README.md", + "remaining": "Uniform algorithmic implications, not another endpoint digit.", + "status": "author-checked", + "source_commit": "ef4315b8caa605e47a2515004845eb2d2ed71a86", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4100: compact-switch formalization proposed as future validation.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Audit the statement and assumptions before a formal proof campaign.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "changed", + "actual_scope": "An exact convolution algorithm for the existing multi-shift joint-nullity law.", + "scope_change_reason": "The existing multiple-shift formula has a combinatorial dimension-tuple sum. This is an algorithmic side result, not a formalization.", + "bottleneck_link": "Supports dependent shifted-rank weights in nonbinary Schur counts. No physical supplier or kappa improvement.", + "budget_minutes": 60, + "stop_rule": "Finish one exact evaluation algorithm, independent checks and a fair timing comparison. Do not start a header-cover construction.", + "outcome": "completed", + "evidence": "PROOF.md, RESULT.json and BENCHMARK.json; source sums, literal matrices, marginals and controls.", + "author": "Ali Romman", + "ai_assistance": "Substantial OpenAI Codex assistance. No independent human or proof-kernel review claimed.", + "open_questions": [ + { + "question": "Which actual nonbinary Schur weight can use these counts?", + "why_it_matters": "A count alone does not reduce the paid header bill.", + "first_step": "State one producer ensemble and its rank-dependent weight.", + "blocked_by": "Selection, emission, reads, restoration and complete pricing." + } + ], + "coordination": { + "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/5261#discussioncomment-19153208", + "overlap": "305 open PRs, 4634 Discussion records, complete remote pagination; all 7267 main README/TASK notes and targeted all-state searches. No arbitrary-diff or unpublished coverage." + } +} diff --git a/research/multishift-nullity-convolution/VERIFY.json b/research/multishift-nullity-convolution/VERIFY.json new file mode 100644 index 0000000000..1eb461a31a --- /dev/null +++ b/research/multishift-nullity-convolution/VERIFY.json @@ -0,0 +1,38 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/schur-rank-pair-law/PROOF.md", + "research/schur-rank-pair-law/README.md", + "research/schur-rank-pair-law/verify.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact source sums, F4-inclusive matrix census, marginal consistency, input controls and receipt comparison." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact source sums, F4-inclusive matrix census, marginal consistency, input controls and receipt comparison." + } + ] +} diff --git a/research/multishift-nullity-convolution/benchmark.py b/research/multishift-nullity-convolution/benchmark.py new file mode 100644 index 0000000000..1a3712817d --- /dev/null +++ b/research/multishift-nullity-convolution/benchmark.py @@ -0,0 +1,27 @@ +"""Compare the same exact count with a feasible simplex reference.""" +import json +import platform +from pathlib import Path +from statistics import median +import sys +from time import perf_counter +sys.path.insert(0, str(Path(__file__).resolve().parent)) +from verify import source, direct +from count import joint_count, require + +old = source() +q, n, a = 7, 12, (0,) * 7 +samples = {"simplex": [], "convolution": []} +answers = {} +for repetition in range(5): + order = ("simplex", "convolution") if repetition % 2 == 0 else ("convolution", "simplex") + for method in order: + start = perf_counter() + answer = direct(q, n, a, old) if method == "simplex" else joint_count(q, n, a) + samples[method].append(perf_counter() - start) + answers[method] = answer +require(answers["simplex"] == answers["convolution"], "benchmark count mismatch") +print(json.dumps({"python": platform.python_version(), "platform": platform.platform(), + "q": q, "n": n, "nullities": a, "count": str(answers["simplex"]), + "seconds": samples, "median_speedup": median(samples["simplex"]) / + median(samples["convolution"]), "timing_is_not_an_acceptance_test": True}, indent=2)) diff --git a/research/multishift-nullity-convolution/count.py b/research/multishift-nullity-convolution/count.py new file mode 100644 index 0000000000..602b3ba7af --- /dev/null +++ b/research/multishift-nullity-convolution/count.py @@ -0,0 +1,63 @@ +"""Evaluate the credited joint-nullity law by exact convolution. + +Ali Romman with OpenAI Codex assistance. Apache-2.0. +""" +from fractions import Fraction +from math import comb, prod + + +def require(ok, message): + if not ok: + raise ValueError(message) + + +def prime_power(q): + if type(q) is not int or q < 2: + return False + p = 2 + while p * p <= q and q % p: + p += 1 + if p * p > q: + return True + while q % p == 0: + q //= p + return q == 1 + + +def joint_count(q, n, nullities): + """Count matrices for distinct shifts; return an exact nonnegative integer.""" + require(prime_power(q), "q must be a prime power") + require(type(n) is int and n >= 0, "n must be nonnegative") + a = tuple(nullities) + require(len(a) <= q, "too many distinct shifts") + require(all(type(x) is int and x >= 0 for x in a), "invalid nullity") + r = sum(a) + if r > n: + return 0 + m = n - r + factorial = [1] + powers = [1] + for j in range(1, n + 1): + powers.append(powers[-1] * q) + factorial.append(factorial[-1] * (powers[-1] - 1)) + coefficients = [Fraction(1)] + [Fraction(0)] * m + for x in a: + factor = [] + power = 1 + for u in range(m + 1): + factor.append(Fraction(1, factorial[u] * power)) + power *= powers[x] + coefficients = [sum((coefficients[j] * factor[k - j] + for j in range(k + 1)), Fraction(0)) + for k in range(m + 1)] + exponent = n * (n - r) + comb(r, 2) - sum(comb(x, 2) for x in a) + weight = q**exponent + total = Fraction(0) + for u in range(m + 1): + total += (-1)**u * weight * coefficients[u] / factorial[m - u] + if u < m: + require(weight % powers[m - u] == 0, "invalid weight recurrence") + weight //= powers[m - u] + value = total * Fraction(factorial[n], prod(factorial[x] for x in a)) + require(value.denominator == 1 and value >= 0, "invalid exact count") + return value.numerator diff --git a/research/multishift-nullity-convolution/verify.py b/research/multishift-nullity-convolution/verify.py new file mode 100644 index 0000000000..fbaf89dbc2 --- /dev/null +++ b/research/multishift-nullity-convolution/verify.py @@ -0,0 +1,142 @@ +#!/usr/bin/env python3 +"""Check the convolution against source sums and literal matrices. + +Ali Romman with OpenAI Codex assistance. Apache-2.0. +""" +from collections import Counter +from hashlib import sha256 +from importlib.util import module_from_spec, spec_from_file_location +from itertools import product +import json +from math import comb, prod +from pathlib import Path +import sys + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +sys.path.insert(0, str(HERE)) +from count import joint_count, require + + +def load(path, name): + spec = spec_from_file_location(name, path) + module = module_from_spec(spec) + spec.loader.exec_module(module) + return module + + +def source(): + manifest = json.loads((HERE / "SOURCES.json").read_text()) + for item in manifest["files"]: + if item["usage"] == "input": + require(sha256((ROOT / item["path"]).read_bytes()).hexdigest() + == item["sha256"], "source hash mismatch") + frozen = manifest["discussion"] + require(sha256((HERE / frozen["path"]).read_bytes()).hexdigest() + == frozen["sha256"], "Discussion hash mismatch") + return load(ROOT / "research/schur-rank-pair-law/verify.py", "pair_source") + + +def simplex(t, remaining): + if t == 0: + yield () + else: + for k in range(remaining + 1): + for tail in simplex(t - 1, remaining - k): + yield (k,) + tail + + +def direct(q, n, a, old, omit_lifts=False, wrong_sign=False): + """Use the Discussion formula with only feasible dimension tuples.""" + if sum(a) > n: + return 0 + result = 0 + for extra in simplex(len(a), n - sum(a)): + taken, moment, weight = 0, 1, 1 + for x, u in zip(a, extra): + k = x + u + moment *= old.gaussian(n - taken, k, q) + if not omit_lifts: + moment *= q**(taken * k) + taken += k + weight *= old.gaussian(k, x, q) * q**(u * (u - 1) // 2) + if not wrong_sign: + weight *= (-1)**u + result += moment * weight * q**(n * (n - taken)) + return result + + +def replay(): + old = source() + comparisons = 0 + for q in (2, 3, 4, 5, 7): + for n in range(7): + for t in range(min(q, 4) + 1): + for a in simplex(t, n): + require(joint_count(q, n, a) == direct(q, n, a, old), + "simplex disagreement") + if t == 2: + require(joint_count(q, n, a) == old.joint_count(n, *a, q), + "two-shift disagreement") + comparisons += 1 + contexts = [(2, n, 2) for n in range(4)] + [(3, n, 3) for n in range(4)] + contexts += [(4, 2, 4), (5, 2, 3), (5, 2, 5)] + matrices = bins = 0 + for q, n, t in contexts: + histogram = Counter() + for entries in product(range(q), repeat=n * n): + nullities = [] + for shift in range(t): + negative = shift if q == 4 else -shift + shifted = tuple(old.add(entries[n * i + j], negative if i == j else 0, q) + for i in range(n) for j in range(n)) + nullities.append(n - old.rank(shifted, n, q)) + histogram[tuple(nullities)] += 1 + matrices += 1 + for a in product(range(n + 1), repeat=t): + require(joint_count(q, n, a) == histogram[a], "matrix census disagreement") + bins += 1 + require(sum(histogram.values()) == q**(n * n), "census total") + for q, n, t in ((3, 5, 3), (5, 6, 4), (7, 5, 7)): + values = {a: joint_count(q, n, a) for a in simplex(t, n)} + require(sum(values.values()) == q**(n * n), "distribution total") + for a, value in values.items(): + require(value == joint_count(q, n, tuple(reversed(a))), "shift symmetry") + for a in simplex(t - 1, n): + require(sum(values[a + (b,)] for b in range(n - sum(a) + 1)) + == joint_count(q, n, a), "marginal consistency") + require(joint_count(3, 2, (0, 0, 0)) == 18, "quadratic calibration") + require(joint_count(3, 3, (1, 1, 1)) == 1404, "split calibration") + require(joint_count(3, 3, (0, 0, 0)) == 3456, "cubic calibration") + require(joint_count(2, 2, (1, 1)) != direct(2, 2, (1, 1), old, omit_lifts=True), + "lift control") + require(joint_count(3, 2, (0, 0, 0)) != direct(3, 2, (0, 0, 0), old, wrong_sign=True), + "sign control") + require(joint_count(2, 2, (0, 0)) * 16 != joint_count(2, 2, (0,))**2, + "independence control") + rejected = 0 + for args in ((6, 2, (0,)), (1, 2, (0,)), (True, 2, (0,)), + (2, -1, (0,)), (2, True, (0,)), (2, 2, (-1,)), + (2, 2, (True,)), (2, 2, (0, 0, 0))): + try: + joint_count(*args) + except ValueError: + rejected += 1 + require(rejected == 8, "invalid input accepted") + large = joint_count(17, 24, (0,) * 17) + return {"status": "PASS_MULTISHIFT_CONVOLUTION_NO_NEW_KAPPA", + "direct_comparisons": comparisons, "matrix_contexts": len(contexts), + "matrices": matrices, "bins": bins, "consistency_contexts": 3, + "negative_controls": 11, + "large_count": str(large), "large_direct_summands": comb(41, 17), + "large_convolution_products": 17 * 25 * 26 // 2} + + +if __name__ == "__main__": + result = replay() + receipt = HERE / "RESULT.json" + if "--record" in sys.argv: + receipt.write_text(json.dumps(result, indent=2) + "\n") + else: + require(result == json.loads(receipt.read_text()), "receipt mismatch") + print(json.dumps(result, sort_keys=True))