From dfc3b4196557eec8b7196ca881b8beb4e62cb8eb Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Tue, 27 Oct 2026 15:23:01 +0000 Subject: [PATCH] feat(research): prove optimal Gaussian chirp origins --- research/gaussian-origin-optimum/PROOF.md | 126 +++++++++++++ research/gaussian-origin-optimum/README.md | 127 +++++++++++++ research/gaussian-origin-optimum/SOURCES.json | 30 +++ research/gaussian-origin-optimum/TASK.json | 83 +++++++++ research/gaussian-origin-optimum/VERIFY.json | 34 ++++ research/gaussian-origin-optimum/verify.py | 174 ++++++++++++++++++ 6 files changed, 574 insertions(+) create mode 100644 research/gaussian-origin-optimum/PROOF.md create mode 100644 research/gaussian-origin-optimum/README.md create mode 100644 research/gaussian-origin-optimum/SOURCES.json create mode 100644 research/gaussian-origin-optimum/TASK.json create mode 100644 research/gaussian-origin-optimum/VERIFY.json create mode 100644 research/gaussian-origin-optimum/verify.py diff --git a/research/gaussian-origin-optimum/PROOF.md b/research/gaussian-origin-optimum/PROOF.md new file mode 100644 index 0000000000..f2222e68db --- /dev/null +++ b/research/gaussian-origin-optimum/PROOF.md @@ -0,0 +1,126 @@ +# The unique optimal origin in the quadratic chirp family + +This proof and its finite corroboration were produced by Nick Petalas. + +## Model and statement + +Let n >= 2, 1 <= W <= n-1 be integers, let a, theta > 0 and beta be real, +and put rho = 1+theta. Vertices are 0,...,n-1. For every real c define +the matrix N(c) to have diagonal 1, zero outside bandwidth W, and entries + +```text +N(c)[i,j] = exp(-a rho h^2 - 2a beta h + + a theta ((i-c)^2-(j-c)^2)), h=j-i, +0 < |h| <= W. +``` + +This is exactly the Gaussian chirp formula in Cinna Davis's PR #4100 +gauge-free note, with t_i=i-c. We treat it as a specified mathematical +family. We do not assert that changing c is a free operation at its caller. +The individual fixed-origin results of James Reed's #4304/#4305 are +predecessors, not assumptions needed for the following optimization proof. + +Write R_i(c) for the sum of off-diagonal entries in row i and +R(c)=max_i R_i(c)=||N(c)-I||_infinity. Then its unique minimum over all +real c occurs at + +```text +c* = (n-1)/2 + beta/theta. (1) +``` + +This optimizes only c. It is not a claim about all positive diagonal +scalings, nor does optimality imply R(c*)<1 in every parameter regime. + +## Reflection and strict convexity + +Expand the squares and put m=(n-1)/2 and u=c-c*. The exponent becomes + +```text +-a ((1+2theta) h^2 + 2theta(i-m-u)h). (2) +``` + +Under i -> n-1-i, j -> n-1-j, u -> -u, both h and i-m-u change +sign. The bandwidth and endpoint truncation are preserved. Thus + +```text +R_i(c*+u) = R_(n-1-i)(c*-u), R(c*+u)=R(c*-u). (3) +``` + +Each R_i is a finite sum of positive exponentials of affine functions +of c. Its second derivative is + +```text +R_i''(c) = sum_(0<|j-i|<=W) (2a theta(j-i))^2 N(c)[i,j] > 0. (4) +``` + +Every vertex has at least one neighbor, so the inequality is strict. +The finite maximum R is also strictly convex. Indeed, at an interior +convex combination choose a maximizing row. Its strict convexity bounds +its value strictly below the same convex combination of its endpoint +values, which are at most the corresponding endpoint maxima. + +For u != 0, strict midpoint convexity and (3) give +R(c*) < (R(c*+u)+R(c*-u))/2 = R(c*+u). This proves existence and +uniqueness directly, even though R need not be differentiable. +No bounded numerical search supplies the universal quantifiers. + +## A usable sufficient contraction bound + +Suppose delta=1-(n-3)theta > 0. At c*, for k=|h| >= 1 the positive +coefficient q in the exponent -a q obeys + +```text +q = (1+2theta)h^2 + 2theta(i-m)h + >= (1+2theta)k^2 - theta(n-1)k + = delta k^2 + theta(n-1)k(k-1) + >= delta k^2. (5) +``` + +The first inequality uses |i-m|<=m, including truncated boundary rows. +There are at most two entries for each k, hence + +```text +R(c*) <= 2 sum_(k=1)^W exp(-a delta k^2) + <= 2W exp(-a delta). (6) +``` + +Delta>0 is sufficient for this bound, not necessary for the optimizer +or for contraction. The checker includes a regime with R(c*)>1. + +## The ten-vertex prime-scale section + +Use the parameters of James Reed's #4305: n=10, W=2, +theta=1/1444, beta=-1/2, a=9pi. Formula (1) gives c*=-1435/2, +and delta=1437/1444. Machin's identity and alternating arctangent +bounds give + +```text +pi > 16(1/5-1/375)-4/239 > 157/50, +9pi * 1437/1444 > 28. (7) +``` + +All terms of the exponential Taylor series are positive, and the exact +rational sum sum_(k=0)^12 7^k/k! is greater than 1024. Therefore +exp(7)>2^10 and exp(28)>2^40. Applying (6) proves + +```text +||N(-1435/2)-I||_infinity < 4 exp(-28) < 2^-38. (8) +``` + +The cited fixed-origin section at c=0 has the predecessor's bound 97/100. +Equation (8) is a new bound on a changed member of the same family, +not a re-computation of that predecessor. Uniqueness also proves the +actual norm strictly decreases when c moves from 0 to c*. + +The scaling has a material cost. For D(c)[i,i]=exp(a theta(i-c)^2), +the ratio of its largest to smallest diagonal at c* is + +```text +D(c*)[9,9]/D(c*)[0,0] = exp(81pi). (9) +``` + +Indeed, theta((9+1435/2)^2-(1435/2)^2)=9. Changing c is diagonal +similarity: N(c)=D(c) K D(c)^-1 for the same truncated Toeplitz K. +Thus the improvement of this infinity norm does not change eigenvalues. +We make no claim that its conversion, storage or precision costs fit a +physical supplier. No selected assumption is discharged by (8). diff --git a/research/gaussian-origin-optimum/README.md b/research/gaussian-origin-optimum/README.md new file mode 100644 index 0000000000..cb43c25140 --- /dev/null +++ b/research/gaussian-origin-optimum/README.md @@ -0,0 +1,127 @@ +# The unique optimal origin for a finite Gaussian chirp + +This contribution is produced by Nick Petalas. Apache-2.0. + +For every finite banded Gaussian chirp in the family below, the unique +real origin minimizing the largest off-diagonal row sum is +`c*=(n-1)/2+beta/theta`. At the ten-vertex, width-2, p=19 section of +James Reed's [PR #4305](https://github.com/CrocSwap/integer-mult-bounds/pull/4305), +the changed origin `-1435/2` gives `||N-I||_infinity < 2^-38`. +The cited origin-zero section has the predecessor's bound `97/100`. +The actual norm strictly decreases by uniqueness of the minimizer. + +Claim type: a scoped written analytic proof with exact finite corroboration. +No kappa, supplier admission or selected framework assumption changes. +The favorable norm requires a chirp diagonal range of `exp(81*pi)` in +the example, which has no paid implementation here. + +## Model and new step + +For integers `n>=2`, `1<=W<=n-1`, real `a,theta>0`, `beta` and origin `c`, +use diagonal 1 and, for `h=j-i`, + +```text +N(c)[i,j] = exp(-a(1+theta)h^2 - 2a beta h + + a theta((i-c)^2-(j-c)^2)), 0<|h|<=W. +``` + +All other entries are zero. This is Cinna Davis's PR #4100 Gaussian +chirp formula, the same family as James Reed's #4304/#4305 sections. +Their fixed-origin results are cited, not independently replayed. + +[PROOF.md](PROOF.md) expands the exponent, reflects the finite path and +proves strict convexity of each row sum and their maximum. These facts +give the unique optimizer over every real origin. If +`delta=1-(n-3)theta>0`, it also proves +`||N(c*)-I||_infinity <= 2W exp(-a delta)`. +At `n=10,W=2,theta=1/1444,beta=-1/2,a=9*pi`, exact elementary +bounds give `a delta>28` and `exp(28)>2^40`. + +Only the origin varies. This is not optimization over all positive +diagonal scalings. The matrices are diagonally similar and have the same +eigenvalues. Optimality does not imply contraction in every parameter regime. + +## Evidence and reproduction + +From the repository root, with standard-library CPython 3.12: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/gaussian-origin-optimum/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -O -B research/gaussian-origin-optimum/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/gaussian-origin-optimum +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/gaussian-origin-optimum --check-source-history +``` + +Another installed CPython 3.12 can replace the local interpreter path. +The direct verifier also runs in a Git-free export and prints +`PASS_GAUSSIAN_ORIGIN_OPTIMUM`. `--emit` prints only its generated JSON +receipt, including hashes of all six package files. It writes no files. +There is no handwritten receipt or expected-output file. + +The fixtures take `a=96 log(2)`, so every entry is an exact rational +power of two. They compare the literal squared-distance formula with +the expanded formula, check reflected rows and strict row midpoint +inequalities, and check strict improvement at two offsets from c*. +There are 216 parameter fixtures, 4,140 exponent fixtures, 2,790 +reflected-row equalities and 3,222 strict inequalities. +The prime-scale certificate checks all 34 in-band entries using rational +exponent inequalities, Machin's arctangent bound and a positive Taylor sum. +Finite fixtures corroborate the written proof's universal quantifiers. + +Fifteen controls cover invalid dimensions, bandwidths and theta values, +nonintegral and oversized fixture exponents, the wrong beta sign, +the wrong path midpoint, an omitted theta term, a valid noncontracting +regime and the degenerate theta-zero boundary. Explicit exceptions keep +checks active in optimized Python. + +## Sources and limits + +The scientific base is canonical main +`19fdb086ea96af9a9f87936a2b888e10af4ed810`, priority revision 8. +[SOURCES.json](SOURCES.json) pins the original catalogue, selected record, +James Reed's retained PR #4305 README and Cinna Davis's gauge-free formula +as bibliographic provenance. No predecessor executable or numerical +receipt is consumed. The selected metadata baseline passed for orientation; +it is not a scientific replay. + +The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19220028) +states the changed origin-optimization scope. Entry searches included live +open PRs, recent account PRs, active Discussions and handoffs, targeted +merged searches and all-main README terms. They rejected the already-solved +origin-zero question before this claim. Sparse cached local-note coverage +is incomplete, and search absence is not proof of novelty. + +No physical conversion, precision/tape invoice, source ownership, native +supplier, recursive Schur schedule, stock, compiler or analytic recovery +theorem is established. The five selected assumptions remain. Lean, +Docker, selected cold replay, independent human review and formal +proof-kernel review are unrun. No construction expansion is proposed. + +Build the Lever supplies a standalone exact verifier. Prove It Works +requires full row sums of its rational fixtures. Power of Ten bounds +fixtures by ten vertices, bandwidth three, rational exponents of magnitude +at most 4096, and six files of at most 128 KiB. Functions stay below +60 physical lines. Warning-strict normal and optimized Python provide +recurring diagnostics. Managed allocation is a bounded rule-3 deviation +because Python integers and Fractions allocate dynamically. There is no +recursion, subprocess, network access or dynamic code generation. +The rejection helper's ten callbacks are fixed local controls, a bounded +rule-9 deviation; no external callback is accepted. + +## Open next questions + +What origin is best under an explicit logarithmic range budget on the +chirp diagonal? This matters because the unconstrained example needs +range `exp(81*pi)`. First intersect the origins with a specified range +allowance and minimize the convex row-norm objective there. A real caller +must supply the scaling and precision budget. The structured question is +in [TASK.json](TASK.json) and is not reserved here. + +## Credit + +The new origin-optimization proof and verifier were produced by Nick Petalas. +James Reed / jwr404 supplied the origin question and fixed-origin sections +in #4304/#4305. Cinna Davis supplied the PR #4100 Gaussian and gauge-free +formulas. Their attribution and frozen files remain intact. Convexity, +path reflection, Machin's identity and Taylor bounds are classical methods. +Independent human and formal proof-kernel review are unclaimed. diff --git a/research/gaussian-origin-optimum/SOURCES.json b/research/gaussian-origin-optimum/SOURCES.json new file mode 100644 index 0000000000..0b373038e1 --- /dev/null +++ b/research/gaussian-origin-optimum/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8", + "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/gaussian-prime-origin/README.md", + "usage": "provenance", + "git_blob": "ffd1945a6cd39d7509acfb1c7c543babdbfc29d6", + "sha256": "aea95b73b3a4a048549c138ecee0a92fe549c10a568997931658a343522acc5d" + }, + { + "path": "research/unconditional-batched-crt/vendor/GAUGEFREE-INTERIORS.md", + "usage": "provenance", + "git_blob": "20585e44fa4e49b13b5d8495bbf6ed254459a362", + "sha256": "d1423ac0ea0003521797209f4396e6981a66994bbee4f8b48026e5b95f8c5116" + } + ] +} diff --git a/research/gaussian-origin-optimum/TASK.json b/research/gaussian-origin-optimum/TASK.json new file mode 100644 index 0000000000..7544619093 --- /dev/null +++ b/research/gaussian-origin-optimum/TASK.json @@ -0,0 +1,83 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 8, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "original_card": { + "id": "uniform-transfer-audit", + "question": "Can one of the selected record's five inherited assumptions be proved at its actual caller?", + "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": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.", + "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 one assumption ID (native_all_columns, owned_erasure, compiler, precision_tape, analytic_recovery), one quantified implication and exact dependency closure. Check current handoffs, including #5625 row reentry and #5707 root-prefix lowering, without treating their partial scope as the whole theorem. Prove or falsify that implication with a caller-bound argument; stop at the chosen obligation. Finite tests or root digits do not discharge an all-size statement.", + "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": [ + "native_all_columns", + "owned_erasure", + "compiler", + "precision_tape", + "analytic_recovery" + ], + "existing_checks": [ + { + "scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "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": "Prove the unique real origin minimizing the infinity norm of N(c)-I for every finite banded Gaussian chirp in the specified quadratic family; certify a strict improvement on the ten-vertex p=19 section.", + "scope_change_reason": "This is a new conditioning optimization lemma motivated by James Reed PR4305, rather than an audit or discharge of a selected framework assumption.", + "bottleneck_link": "The origin controls the row-gap hypothesis of Gaussian Neumann inversion. Optimizing it can improve conditioning, but the diagonal conversion range and full precision/tape invoice remain separate costs.", + "budget_minutes": 60, + "stop_rule": "Stop at the first proved strict origin improvement and its bounded exact corroboration. Do not extend to physical admission, other gauges or recursive Schur optimization.", + "outcome": "partial", + "evidence": "PROOF.md gives the all-parameter unique-minimizer theorem and the analytic norm bound below 2^-38. verify.py corroborates exact exponent identities, rational exponential fixtures and the constant certificate.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "What is the best row-norm bound after imposing an explicit logarithmic range budget on the chirp diagonal?", + "why_it_matters": "The unconstrained optimum in the ten-vertex example has diagonal range exp(81*pi); conditioning alone does not pay for conversion or precision.", + "first_step": "Intersect the allowed origins with a fixed bound on max_i log D_i(c)-min_i log D_i(c), then minimize the convex row-norm objective on that feasible set.", + "blocked_by": "A physical caller must supply its actual scaling and precision allowance." + } + ] +} diff --git a/research/gaussian-origin-optimum/VERIFY.json b/research/gaussian-origin-optimum/VERIFY.json new file mode 100644 index 0000000000..79e0cbe385 --- /dev/null +++ b/research/gaussian-origin-optimum/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": "Exact rational fixtures, strict-convexity/reflection identities, analytic prime-scale bound and boundary controls." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The same explicit scientific checks remain active with Python optimization." + } + ] +} diff --git a/research/gaussian-origin-optimum/verify.py b/research/gaussian-origin-optimum/verify.py new file mode 100644 index 0000000000..086315c5e0 --- /dev/null +++ b/research/gaussian-origin-optimum/verify.py @@ -0,0 +1,174 @@ +#!/usr/bin/env python3 +"""Exact finite corroboration of the written Gaussian-origin theorem.""" + +import hashlib +import json +from fractions import Fraction as F +from pathlib import Path +import sys + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def model(n, width, theta): + require(type(n) is int and 2 <= n <= 10, "fixture length outside 2..10") + require(type(width) is int and 1 <= width < n, "invalid bandwidth") + require(type(theta) is F and theta > 0, "theta must be a positive Fraction") + + +def origin(n, beta, theta): + return F(n - 1, 2) + beta / theta + + +def exponent(i, j, beta, theta, centre): + h = j - i + return (1 + theta) * h * h + 2 * beta * h - theta * ( + (i - centre) ** 2 - (j - centre) ** 2 + ) + + +def simplified(i, j, beta, theta, centre): + h = j - i + return (1 + 2 * theta) * h * h + 2 * (beta + theta * (i - centre)) * h + + +def power_two(exponent_value): + require(exponent_value.denominator == 1, "nonintegral dyadic exponent") + k = exponent_value.numerator + require(abs(k) <= 4096, "fixture exponent exceeds memory bound") + return F(1, 1 << k) if k >= 0 else F(1 << -k) + + +def rows(n, width, beta, theta, centre): + """Use a=96 log(2), so every admitted fixture has rational entries.""" + model(n, width, theta) + return tuple( + sum( + (power_two(96 * exponent(i, j, beta, theta, centre)) + for j in range(n) if 0 < abs(i - j) <= width), + F(0), + ) + for i in range(n) + ) + + +def fixtures(): + cases = edges = reflection_checks = strict_checks = 0 + for n in range(2, 11): + for width in range(1, min(n - 1, 3) + 1): + for theta in (F(1, 4), F(1, 8), F(1, 16)): + for beta in (F(-1, 2), F(0), F(1, 3)): + centre = origin(n, beta, theta) + best = rows(n, width, beta, theta, centre) + for offset in (F(1, 2), F(1)): + left = rows(n, width, beta, theta, centre - offset) + right = rows(n, width, beta, theta, centre + offset) + require(left == right[::-1], "reflection failed") + require(max(best) < max(left), "strict optimality failed") + require(all(2 * b < l + r for b, l, r in zip(best, left, right)), + "strict row convexity failed") + reflection_checks += n + strict_checks += n + 1 + for i in range(n): + for j in range(n): + if 0 < abs(i - j) <= width: + q = exponent(i, j, beta, theta, centre) + require(q == simplified(i, j, beta, theta, centre), + "chirp expansion failed") + expected = ((1 + 2 * theta) * (j - i) ** 2 + + 2 * theta * (i - F(n - 1, 2)) * (j - i)) + require(q == expected, "optimal exponent failed") + edges += 1 + cases += 1 + return dict(parameter_cases=cases, exponent_identities=edges, + reflected_rows=reflection_checks, strict_inequalities=strict_checks) + + +def analytic_example(): + n, width, theta, beta = 10, 2, F(1, 1444), F(-1, 2) + centre = origin(n, beta, theta) + delta = 1 - (n - 3) * theta + require(centre == F(-1435, 2) and delta == F(1437, 1444), "example parameters") + # Machin: atan(1/5) > 1/5-(1/5)^3/3 and atan(1/239) < 1/239. + pi_lower = 16 * (F(1, 5) - F(1, 375)) - F(4, 239) + require(pi_lower > F(157, 50), "pi lower certificate") + require(9 * pi_lower * delta > 28, "exponent lower certificate") + term = total = F(1) + for k in range(1, 13): + term *= F(7, k) + total += term + require(total > 1024, "positive Taylor certificate for exp(7)") + edges = 0 + for i in range(n): + for j in range(n): + if 0 < abs(i - j) <= width: + q = exponent(i, j, beta, theta, centre) + require(q >= delta * (i - j) ** 2 >= delta, "entry majorant") + edges += 1 + require(edges == 34 and 2 * width == 4, "banded entry count") + # 4 exp(-28) < 4 / 2^40 = 2^-38. + require(F(4, 1 << 40) == F(1, 1 << 38), "row-norm certificate") + chirp_range = 9 * theta * ((9 - centre) ** 2 - centre ** 2) + require(chirp_range == 81, "chirp range coefficient of pi") + return dict(example_entries=edges, optimal_origin=str(centre), + norm_upper="2^-38", chirp_range="exp(81*pi)") + + +def reject(call): + try: + call() + except ValueError: + return + raise ValueError("invalid input was accepted") + + +def controls(): + for args in ((1, 1, F(1, 4)), (11, 1, F(1, 4)), (4, 0, F(1, 4)), + (4, 4, F(1, 4)), (4, 1, F(0)), (4, 1, F(-1, 4)), + (4, 1, 0.25), (True, 1, F(1, 4))): + reject(lambda args=args: model(*args)) + reject(lambda: power_two(F(1, 2))) + reject(lambda: power_two(F(4097))) + n, w, beta, theta = 6, 2, F(-1, 2), F(1, 8) + centre = origin(n, beta, theta) + optimum = max(rows(n, w, beta, theta, centre)) + require(max(rows(n, w, beta, theta, F(n - 1, 2) - beta / theta)) > optimum, + "wrong-sign origin control") + require(max(rows(n, w, beta, theta, F(n, 2) + beta / theta)) > optimum, + "wrong-midpoint origin control") + require(exponent(0, 1, beta, theta, centre) != + (1 + theta) + 2 * (beta + theta * (0 - centre)), + "omitted quadratic theta control") + require(max(rows(8, 2, F(0), F(1, 4), origin(8, F(0), F(1, 4)))) > 1, + "optimality must not imply contraction in every parameter regime") + require(exponent(0, 1, F(0), F(0), F(0)) == + exponent(0, 1, F(0), F(0), F(5)), "theta-zero boundary") + return 15 + + +def receipt(): + package = Path(__file__).resolve().parent + names = ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", "VERIFY.json", "verify.py") + hashes = {} + for name in names: + with (package / name).open("rb") as source: + data = source.read(128 * 1024 + 1) + require(len(data) <= 128 * 1024, "package file exceeds receipt limit") + hashes[name] = hashlib.sha256(data).hexdigest() + return hashes + + +def main(): + require(sys.argv[1:] in ([], ["--emit"]), "usage: verify.py [--emit]") + result = dict(schema="gaussian-origin-optimum/v1", **fixtures(), + **analytic_example(), controls=controls(), files=receipt()) + if sys.argv[1:] != ["--emit"]: + print("PASS_GAUSSIAN_ORIGIN_OPTIMUM") + print(json.dumps(result, sort_keys=True, indent=2)) + + +if __name__ == "__main__": + main()