From ac75afd451e9375de50963c234439beaf27ccb23 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Tue, 27 Oct 2026 11:22:05 +0000 Subject: [PATCH] feat(research): prove the sharp Gaussian bulk denominator --- .../gaussian-bulk-sharp-denominator/README.md | 201 +++++++++++++++++ .../SOURCES.json | 18 ++ .../gaussian-bulk-sharp-denominator/TASK.json | 112 +++++++++ .../VERIFY.json | 32 +++ .../gaussian-bulk-sharp-denominator/verify.py | 212 ++++++++++++++++++ 5 files changed, 575 insertions(+) create mode 100644 research/gaussian-bulk-sharp-denominator/README.md create mode 100644 research/gaussian-bulk-sharp-denominator/SOURCES.json create mode 100644 research/gaussian-bulk-sharp-denominator/TASK.json create mode 100644 research/gaussian-bulk-sharp-denominator/VERIFY.json create mode 100644 research/gaussian-bulk-sharp-denominator/verify.py diff --git a/research/gaussian-bulk-sharp-denominator/README.md b/research/gaussian-bulk-sharp-denominator/README.md new file mode 100644 index 0000000000..1d23c444ea --- /dev/null +++ b/research/gaussian-bulk-sharp-denominator/README.md @@ -0,0 +1,201 @@ +# Sharp denominator and precision for the central Gaussian bulk + +This scoped mathematical proof makes the degree-R denominator upper bound in +David Ganz's [PR #5813](https://github.com/CrocSwap/integer-mult-bounds/pull/5813) +sharp. It also proves the matching worst-case numerator-precision requirement. +The result concerns the full ordinary bulk response, with unrestricted integral +inputs. It supplies no new κ, physical supplier or complete multiplication theorem. + +This contribution was produced by Nick Petalas. Apache-2.0. + +## Exact statement + +Put π=1+i. For integers n>=1, 0<=R<=n and 0<=a<=n-R, let X_j flip bit j +of the 2^n coordinate labels, W=(nI-sum_j X_j)/2, and + +```text +g(z) = i^a sum_(h=0)^R (i-1)^h binom(z-a,h), B = g(W). +``` + +The source construction agrees with the normalized Gaussian tensor on Walsh +weights a through a+R. Its constructive numerator grid is π^R B. The new conclusions are: + +1. In the unique convolution expansion B=sum_S c_S X_S, every |S|=R has + exactly c_S=i^a/π^R, and c_S=0 for |S|>R. Hence the least nonnegative + integer d with π^d B Gaussian-integral is exactly R. +2. B is the only permutation-symmetric convolution supported on displacements + of Hamming weight at most R that has the prescribed central-band response. + Therefore a different formula within that class cannot lower this grid debt. +3. For every p>=1, the integral numerator G=π^R B must in general be known + modulo π^(p+R) to recover Bx modulo π^p. One fewer numerator digit fails + for an explicit pair of integral inputs. Every individual output coordinate + has such a witness. Likewise x modulo π^(p+R) suffices, and x modulo + π^(p+R-1) does not suffice for arbitrary integral x. + +Fractional-output congruence means equality in Q(i)/π^p Z[i]. The precision +claim concerns the quotient contract, not an instruction count or every possible +algorithm that may have other information about x. + +## Proof + +The 2^n matrices X_S are linearly independent: applying them to the coordinate +vector e_0 gives the distinct vectors e_S. Thus convolution coefficients are +literal matrix entries, not coefficients that could cancel under a relation. + +For R>0 the leading coefficient of g is i^a(i-1)^R/R!. A product W^h has +no displacement of weight greater than h. To obtain displacement S of weight R +in W^R, all R factors must choose its distinct bit flips; there are R! orders. +Consequently + +```text +c_S = [i^a(i-1)^R/R!] [R! (-1/2)^R] + = i^a [(1-i)/2]^R + = i^a/π^R. +``` + +The same formula at R=0 is B=i^a I. Since i^a is a Gaussian unit, π^(R-1)B +is not integral when R>0. Ganz's constructive upper bound shows π^R B is +integral. For completeness, it follows from + +```text +B = sum_(j=0)^R b_j E_j, +E_j = sum_(|S|=j) product_(k in S)(I-X_k), +b_j = i^a 2^(-j) sum_(h=j)^R (i-1)^h binom(-a,h-j). +``` + +Each E_j is integral. Every term in b_j has π-valuation h-2j>=-R and has +only a power of 2 in its denominator. This proves the matching upper bound, +including n=R and negative integer offsets in the binomial expression. +The upper construction and Newton identity remain credited to Ganz. + +For uniqueness, a permutation-symmetric convolution of radius at most R is +H=sum_(d=0)^R t_d sum_(|S|=d)X_S. On a Walsh character of weight k its +eigenvalue is the polynomial + +```text +h(k) = sum_(d=0)^R t_d K_d(k;n), +K_d(k;n) = sum_(j=0)^d (-1)^j binom(k,j) binom(n-k,d-j). +``` + +Here binomial coefficients are polynomials in k. The leading coefficient of +K_d is (-2)^d/d!: multiply the leading coefficients in each summand and use +sum_j 1/(j!(d-j)!)=2^d/d!. Thus these polynomials have distinct degrees +0 through R. The central-band conditions fix h on R+1 distinct integers. +Polynomial uniqueness gives h=g, and the Walsh basis then gives H=B. +This also excludes degree below R when R>0. + +For precision, G has Gaussian-integer entries, and its entry at displacement S +of weight R is i^a. Fix any output coordinate t, choose such an S and put +s=t xor S. For any p>=1 take + +```text +x_0 = 0, x_1 = π^(p+R-1) e_s. +``` + +The inputs are congruent modulo π^(p+R-1). Their numerator responses Gx_0 +and Gx_1 are also congruent at that modulus. But their B responses differ at +coordinate t by i^a π^(p-1), which is not divisible by π^p. This proves +both insufficiency claims with actual reachable numerator vectors. Conversely, +knowing Gx modulo π^(p+R) permits division by π^R at the required output +modulus. An input change divisible by π^(p+R) changes Bx by π^p times an +integral vector because π^R B is integral. This proves input sufficiency. +All statements include R=0 with S empty. + +## Evidence and reproduction + +The written proof covers every finite n and every stated band and precision. +The verifier provides finite exact corroboration, not a proof-kernel certificate. +It uses independent exact Walsh inversion and falling-factorial evaluation in +the Boolean group ring. It checks the top coefficient and its minimal grid, +complete literal small Walsh spectra, and indistinguishable-input precision +witnesses. Mutations remove or negate the top coefficient, add an illegal +higher-degree term or odd denominator, and truncate the coefficient list. +The fixed census covers 285 bands, 114,686 coefficients and 11,263 top +coefficients through n=10; 1,022 independently evaluated group-ring +coefficients through n=5; 350 literal Walsh eigenvalues through n=4; +and 75,768 reachable precision witnesses through n=8 with p=1,...,4. +There are sixteen boundary and semantic controls. +Invalid bands and nonintegral valuation inputs are rejected. Checks use explicit +exceptions and remain enabled under optimization. + +From the repository root: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/gaussian-bulk-sharp-denominator/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/gaussian-bulk-sharp-denominator +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/gaussian-bulk-sharp-denominator --check-source-history +``` + +CPython 3.12 and the standard library suffice. The first command emits its own +counts and SHA256 bindings to all five package files. It writes no files. +The registered commands run normal and optimized warning-strict modes. +Run times and outputs are retained outside the checkout until publication is +settled. No predecessor verifier, native replay, Lean or Docker run is required +or claimed. Hosted CI status is recorded in the PR body. + +## Scope, sources and relation to open work + +The question is a narrowed side result of the decoder card, not a complete +signed-invoice improvement. The card's first working metadata control passed. +Canonical main was de5ec2e7a6074068452f45b1a191b5c72832df4a, priority revision 8. +The selected κ remains .00310045, with all five inherited assumptions. + +David Ganz's PR #5813 at af37059809ae41283142c6aeb217cc456852aff1 supplies +the explicit central spectral interpolation and R-unit constructive grid. +Its denominator-accounting question is the source of this refinement. The new +step is sharpness, uniqueness within the stated radius class, and reachable +precision witnesses. The source is +[gaussian-spectral-bridge.md at that head](https://github.com/CrocSwap/integer-mult-bounds/blob/af37059809ae41283142c6aeb217cc456852aff1/research/eth-gaussian-spectral-transport/gaussian-spectral-bridge.md). +It is cited rather than imported or replayed; this package is self-contained. +Classical Walsh diagonalization, Newton interpolation and Krawtchouk polynomials +retain their standard mathematical attribution. + +- [PR #5815](https://github.com/CrocSwap/integer-mult-bounds/pull/5815), David Ganz, + at f0fcda576df410dc15cd5b8183d4f74d284eba2b gives exceptional correction and + mixed-precision constructions; this proof prices neither implementation. +- [PR #5825](https://github.com/CrocSwap/integer-mult-bounds/pull/5825), Ali Romman, + at baea91d8c0044a0036006bdd3b4d7bce3d6cf783 gives a work lower bound for a + specified standalone Newton-W graph. Here the denominator obstruction is + independent of the realization graph, within the stated response class. +- [PR #5880](https://github.com/CrocSwap/integer-mult-bounds/pull/5880), Nick Petalas, + studies reversible clean storage for the raw tensor endpoint. That different + endpoint is not an input lemma or the target of this contribution. + +Restricted input lattices, restricted observables, nonsymmetric operators and +higher-degree spectral replacements are outside the uniqueness obstruction. +Native normalization, correction delivery, storage, restoration, movement and +whole-caller cost remain separate obligations. No favorable physical budget is +inferred from this local result. + +## Verifier bounds and diagnostics + +All finite checks fix n<=10 before allocation, hence at most 1024 coefficients; +the independent group-ring evaluation fixes n<=5 and literal spectra n<=4. +Precision witnesses fix n<=8 and p<=4. Every function is shorter than 60 lines; +there is no recursion or dynamic code generation. Valuation division has an +explicit bound from the norm's bit length. Invalid inputs and corruptions fail +with ValueError, including under -O. + +Power-of-ten rule 3 has a managed-runtime deviation: Python allocates exact +integer/Fraction objects during these bounded checks. The fixed dimensions, +precision and coefficient formulas bound live storage and integer size; no +input files, network reads or external subprocesses enter the mathematics. +Rule 9 has a bounded test-harness deviation: the rejection helper invokes only +the explicitly listed control closures, synchronously and without retained +state. These deviations apply only to this finite verifier. A future verifier +that accepts external ranges must impose equivalent resource limits before +allocation. Warning-strict normal and optimized execution are the available +Python diagnostics; no external linter or type-checker dependency is added. + +## Open next questions + +1. Allow Boolean degree above R while fixing the same central band. Can its + extra Krawtchouk coefficients lower the denominator? Solve a small exact + integrality system with one additional degree first. A physical benefit + still requires a complete paid correction and caller bill. +2. Which actual consumed observable removes every coefficient attaining the + R-unit denominator debt? Pin one provider response and multiply its exact + observable by B. No such physical consumer is supplied here. + +The structured versions are in TASK.json. These questions change hypotheses +of the proved obstruction and are not claims of a funded continuation. diff --git a/research/gaussian-bulk-sharp-denominator/SOURCES.json b/research/gaussian-bulk-sharp-denominator/SOURCES.json new file mode 100644 index 0000000000..fdb80ada25 --- /dev/null +++ b/research/gaussian-bulk-sharp-denominator/SOURCES.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8", + "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + } + ] +} diff --git a/research/gaussian-bulk-sharp-denominator/TASK.json b/research/gaussian-bulk-sharp-denominator/TASK.json new file mode 100644 index 0000000000..a4b1d379b3 --- /dev/null +++ b/research/gaussian-bulk-sharp-denominator/TASK.json @@ -0,0 +1,112 @@ +{ + "schema_version": 1, + "task_id": "complex-rank-shape-decoder", + "priority_revision": 8, + "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a", + "original_card": { + "id": "complex-rank-shape-decoder", + "question": "Can a legal decoder or coframe change improve the full signed moment, including changed helper targets?", + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "docs/research/recursive-invoice-preflight.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "acceptance_gate": "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": "Price one complete changed itinerary with both paid and productive histograms. Check #5693/#5698 for overlap and their exact hypotheses before another coframe search. Use the signed invoice preflight where its boundary contract agrees; an inconclusive concave comparison is not a power crossing. Stop if an optimistic complete budget fails at the chosen target or native delivery remains unspecified.", + "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": [ + "coframe", + "signed moment", + "5693", + "5698" + ], + "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": "Sharp denominator and numerator-precision lower bounds for the permutation-symmetric Boolean-degree-R central Gaussian bulk, with uniqueness at that degree.", + "scope_change_reason": "The decoder card is narrowed to a self-contained precision obstruction for the spectral bulk proposed in PR5813. No complete changed supplier or signed-moment gain is claimed.", + "bottleneck_link": "The R Gaussian denominator units cannot be removed by another symmetric radius-R formula for the same central-band response. A saving must change the degree, observable, input lattice or representation, and still pay the complete physical caller.", + "budget_minutes": 60, + "stop_rule": "Stop at the first proved original lower bound and bounded independent corroboration; no search for a larger result.", + "outcome": "completed", + "evidence": "README.md contains the all-parameter proof. verify.py independently compares Walsh inversion and falling-factorial group-ring evaluation, checks precision indistinguishability and rejects corrupted claims.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "What denominator is achievable if symmetric Boolean degree may exceed R while agreement is required only on the same band?", + "why_it_matters": "The sharp obstruction fixes degree R, so a changed degree is a concrete escape route.", + "first_step": "For a small band, solve the exact Gaussian-integrality constraints with one additional Krawtchouk coefficient.", + "blocked_by": "A favorable complete cost and exceptional-correction bill is still required." + }, + { + "question": "Which actual consumed observables kill every denominator-worst bulk coefficient?", + "why_it_matters": "The theorem observes the complete bulk output, whereas a provider may require fewer linear responses.", + "first_step": "Pin one literal provider response and multiply its exact observable by the bulk convolution.", + "blocked_by": "No physical consumer or free measurement bank is supplied here." + } + ], + "predecessors": [ + { + "pr": 5813, + "author": "David Ganz / Dugongue", + "head": "af37059809ae41283142c6aeb217cc456852aff1", + "role": "Four-phase central interpolation and constructive denominator upper bound; source of the refined denominator-accounting question." + }, + { + "pr": 5815, + "author": "David Ganz / Dugongue", + "head": "f0fcda576df410dc15cd5b8183d4f74d284eba2b", + "role": "Exceptional correction and physical-cost context; not replayed." + }, + { + "pr": 5825, + "author": "Ali Romman", + "head": "baea91d8c0044a0036006bdd3b4d7bce3d6cf783", + "role": "Standalone fixed-graph precision-work obstruction; not replayed." + } + ], + "environment": { + "python": "CPython 3.12.15", + "interpreter": "/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12", + "dependencies": "standard library only" + }, + "coordination": { + "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19215628", + "source": "PR #5813", + "overlap_checked_utc": "2026-10-27T11:17:40Z", + "coverage": "437 open PRs and 5356 Discussion records in paginated cache; all canonical-main top-level READMEs searched separately by git grep. Unpublished work and arbitrary code diffs are outside coverage." + } +} diff --git a/research/gaussian-bulk-sharp-denominator/VERIFY.json b/research/gaussian-bulk-sharp-denominator/VERIFY.json new file mode 100644 index 0000000000..e389c1e279 --- /dev/null +++ b/research/gaussian-bulk-sharp-denominator/VERIFY.json @@ -0,0 +1,32 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact coefficients, uniqueness witnesses, independent polynomial comparison, precision indistinguishability, boundary and mutation controls." + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Identical scientific checks with interpreter assertions disabled." + } + ] +} diff --git a/research/gaussian-bulk-sharp-denominator/verify.py b/research/gaussian-bulk-sharp-denominator/verify.py new file mode 100644 index 0000000000..7ad2746a32 --- /dev/null +++ b/research/gaussian-bulk-sharp-denominator/verify.py @@ -0,0 +1,212 @@ +"""Exact finite corroboration of the sharp central-bulk denominator theorem.""" +from __future__ import annotations + +from fractions import Fraction +from hashlib import sha256 +import json +from math import factorial, prod +from pathlib import Path +import platform + +Gaussian = tuple[Fraction, Fraction] +ZERO: Gaussian = (Fraction(0), Fraction(0)) +ONE: Gaussian = (Fraction(1), Fraction(0)) +I: Gaussian = (Fraction(0), Fraction(1)) +PI: Gaussian = (Fraction(1), Fraction(1)) +MAX_N = 10 + + +def require(condition: bool, message: str) -> None: + if not condition: + raise ValueError(message) + + +def add(x: Gaussian, y: Gaussian) -> Gaussian: + return x[0] + y[0], x[1] + y[1] + + +def mul(x: Gaussian, y: Gaussian) -> Gaussian: + return x[0]*y[0] - x[1]*y[1], x[0]*y[1] + x[1]*y[0] + + +def scale(q: Fraction | int, x: Gaussian) -> Gaussian: + return q*x[0], q*x[1] + + +def power(x: Gaussian, exponent: int) -> Gaussian: + require(0 <= exponent <= 4*MAX_N, 'power bound') + result = ONE + for _ in range(exponent): + result = mul(result, x) + return result + + +def parameters(n: int, a: int, degree: int) -> None: + require(type(n) is int and type(a) is int and type(degree) is int, + 'integer parameters required') + require(1 <= n <= MAX_N, 'finite verifier dimension bound') + require(0 <= degree <= n and 0 <= a <= n-degree, 'invalid band') + + +def choose(z: int, k: int) -> int: + require(0 <= k <= MAX_N, 'binomial bound') + return prod(z-j for j in range(k)) // factorial(k) + + +def value(k: int, a: int, degree: int) -> Gaussian: + result = ZERO + for h in range(degree+1): + term = scale(choose(k-a, h), power(add(I, scale(-1, ONE)), h)) + result = add(result, term) + return mul(power(I, a), result) + + +def coefficients(n: int, a: int, degree: int) -> list[Gaussian]: + """Invert the complete exact Walsh spectrum, without a numerator compiler.""" + parameters(n, a, degree) + data = [value(k.bit_count(), a, degree) for k in range(1 << n)] + for level in range(n): + half = 1 << level + for start in range(0, 1 << n, 2*half): + for j in range(half): + x, y = data[start+j], data[start+j+half] + data[start+j] = add(x, y) + data[start+j+half] = add(x, scale(-1, y)) + return [scale(Fraction(1, 1 << n), z) for z in data] + + +def polynomial_coefficients(n: int, a: int, degree: int) -> list[Gaussian]: + """Evaluate falling factorials directly in Q(i)[(Z/2)^n].""" + parameters(n, a, degree) + term = [ZERO for _ in range(1 << n)] + term[0] = ONE + result = term.copy() + for h in range(1, degree+1): + following = [] + for s in range(1 << n): + z = scale(Fraction(n, 2)-a-h+1, term[s]) + for axis in range(n): + z = add(z, scale(Fraction(-1, 2), term[s ^ (1 << axis)])) + following.append(scale(Fraction(1, h), z)) + term = following + factor = power(add(I, scale(-1, ONE)), h) + result = [add(x, mul(factor, y)) for x, y in zip(result, term, strict=True)] + return [mul(power(I, a), z) for z in result] + + +def integral(z: Gaussian) -> bool: + return z[0].denominator == 1 and z[1].denominator == 1 + + +def valuation(z: Gaussian) -> int | None: + require(integral(z), 'valuation requires a Gaussian integer') + if z == ZERO: + return None + real, imag = z[0].numerator, z[1].numerator + bound = 2*max(abs(real).bit_length(), abs(imag).bit_length())+1 + for exponent in range(bound): + if (real-imag) % 2: + return exponent + real, imag = (real+imag)//2, (imag-real)//2 + raise ValueError('Gaussian valuation bound exhausted') + + +def certify(n: int, a: int, degree: int, data: list[Gaussian]) -> int: + parameters(n, a, degree) + require(len(data) == 1 << n, 'coefficient count') + numerator = [mul(power(PI, degree), z) for z in data] + require(all(integral(z) for z in numerator), 'insufficient numerator grid') + for s, z in enumerate(data): + if s.bit_count() > degree: + require(z == ZERO, 'Boolean degree exceeded') + if s.bit_count() == degree: + require(numerator[s] == power(I, a), 'wrong top coefficient') + if degree: + require(not integral(mul(power(PI, degree-1), data[(1 << degree)-1])), + 'claimed smaller grid has no obstruction') + return sum(s.bit_count() == degree for s in range(1 << n)) + + +def precision_cases(n: int, a: int, degree: int, data: list[Gaussian]) -> int: + """Literal column response to two congruent numerator/input representatives.""" + numerator = [mul(power(PI, degree), z) for z in data] + count = 0 + for p in range(1, 5): + delta = power(PI, p+degree-1) + for source in range(1 << n): + output = source ^ ((1 << degree)-1) + entry = numerator[output ^ source] + difference = mul(entry, delta) + require(valuation(difference) == p+degree-1, 'precision witness lost') + # Division by pi^degree gives valuation p-1, so outputs differ mod pi^p. + require(valuation(difference)-degree == p-1, 'wrong output modulus') + count += 1 + return count + + +def expect_rejection(action) -> None: + try: + action() + except ValueError: + return + raise ValueError('negative control accepted') + + +def controls() -> int: + bad_parameters = [(0, 0, 0), (11, 0, 0), (3, -1, 1), (3, 0, -1), + (3, 1, 3), (3, 0, 4), (True, 0, 0)] + for args in bad_parameters: + expect_rejection(lambda args=args: parameters(*args)) + good = coefficients(4, 1, 2) + mutations = [] + for index, replacement in [(3, ZERO), (3, scale(-1, good[3])), + (15, ONE), (0, add(good[0], (Fraction(1, 3), Fraction(0))))]: + changed = good.copy() + changed[index] = replacement + mutations.append(changed) + mutations.append(good[:-1]) + for changed in mutations: + expect_rejection(lambda changed=changed: certify(4, 1, 2, changed)) + require(polynomial_coefficients(4, 1, 1) != good, 'omitted top term undetected') + require(valuation(power(PI, 5)) == 5, 'valuation control') + require(valuation(ZERO) is None, 'zero valuation control') + expect_rejection(lambda: valuation((Fraction(1, 2), Fraction(0)))) + return len(bad_parameters)+len(mutations)+4 + + +def main() -> None: + counts = {'bands': 0, 'coefficients': 0, 'top_coefficients': 0, + 'independent_polynomial_coefficients': 0, 'precision_witnesses': 0, + 'literal_walsh_eigenvalues': 0} + for n in range(1, MAX_N+1): + for degree in range(n+1): + for a in range(n-degree+1): + data = coefficients(n, a, degree) + counts['bands'] += 1 + counts['coefficients'] += len(data) + counts['top_coefficients'] += certify(n, a, degree, data) + if n <= 5: + require(data == polynomial_coefficients(n, a, degree), + 'independent polynomial/Walsh disagreement') + counts['independent_polynomial_coefficients'] += len(data) + if n <= 8: + counts['precision_witnesses'] += precision_cases(n, a, degree, data) + if n <= 4: + for label in range(1 << n): + actual = ZERO + for s, z in enumerate(data): + actual = add(actual, scale((-1)**((s & label).bit_count()), z)) + require(actual == value(label.bit_count(), a, degree), + 'literal Walsh spectrum mismatch') + counts['literal_walsh_eigenvalues'] += 1 + counts['controls'] = controls() + package = Path(__file__).resolve().parent + names = ('README.md', 'TASK.json', 'SOURCES.json', 'VERIFY.json', 'verify.py') + hashes = {name: sha256((package/name).read_bytes()).hexdigest() for name in names} + print(json.dumps({'status': 'PASS', 'claim_type': 'scoped proof with finite corroboration', + 'python': platform.python_version(), 'counts': counts, + 'sha256': hashes}, sort_keys=True, indent=2)) + + +if __name__ == '__main__': + main()