diff --git a/research/gaussian-phase-cell-lower/PROOF.md b/research/gaussian-phase-cell-lower/PROOF.md new file mode 100644 index 0000000000..6d69738f55 --- /dev/null +++ b/research/gaussian-phase-cell-lower/PROOF.md @@ -0,0 +1,134 @@ +# A matching lower order at a broad Gaussian cell edge + +This contribution was produced by Nick Petalas. Apache-2.0. + +## Theorem and domain + +Let alpha > 0, theta > 0, rho = 1+theta, b0 = pi/alpha^2, +gamma = b0/rho, and c = 1/(2rho). For integers 0 <= k,i < N define + +```text +K[k,i] = alpha^-1 exp(-b0 (i-k/rho-c)^2). +``` + +Assume theta(N-1) <= 1, so beta_k = theta k - 1/2 lies in the +closed phase interval [-1/2,1/2]. For every positive integer m with +2m <= N, + +```text +||K^-1||_2 >= alpha m exp(-gamma theta (2m-1)^2). (1) +``` + +In particular, if 0 < theta <= 1/16 and +N >= 2 floor(1/(2 sqrt(theta))), then + +```text +||K^-1||_2 >= (alpha/4) exp(-pi/alpha^2) theta^(-1/2). (2) +``` + +Thus the theta^(-1/2) upper order proved by JoyboyBrian in #5103 is +sharp for fixed alpha on these boundary sections. This is an order theorem, +not Ryanson Jonathan's #4435 proposed sharp leading coefficient. It is not +a lower bound for every section contained anywhere inside a phase cell. + +## Cited finite inverse and the new positive rectangle + +Put q = exp(-gamma), P_0=1 and +P_s=product_(r=1)^s(1-q^(2r)). The finite Gaussian Toeplitz matrix +G[i,j]=q^((i-j)^2) has the q-LDU factorization retained in Jose Manuel's +#4193 and reproduced in #5103. In the convention +[k choose i]_(q^2)=P_k/(P_i P_(k-i)), its inverse is + +```text +G^-1[i,j] = (-1)^(i+j) sum_(k=max(i,j))^(N-1) + q^(2k-i-j) [k choose i]_(q^2) [k choose j]_(q^2) / P_k. (3) +``` + +Every summand after the checkerboard sign is positive. For i <= j, the +k=j summand alone is q^(j-i)/(P_i P_(j-i)), which is at least q^(j-i). +Symmetry gives, for every i,j, + +```text +(-1)^(i+j) G^-1[i,j] >= q^|i-j|. (4) +``` + +The factorization and inverse sum are cited predecessor mathematics. The +new step keeps this positive lower term under the broad cell's gauges, +then tests a whole rectangle rather than a single entry. + +The exact diagonal factorization K=Dr G Dc is + +```text +Dc[i] = exp(-b0 (theta/rho i^2 - 2c i)), +Dr[j] = alpha^-1 exp(b0 (theta/rho^2 j^2 - 2c/rho j - c^2)). +``` + +These are positive real diagonals. Hence K is invertible, and +K^-1=Dc^-1 G^-1 Dr^-1 has the same checkerboard signs. Multiplying (4) +by the positive inverse gauges gives, when i <= j, + +```text +(-1)^(i+j) K^-1[i,j] + >= alpha exp(b0 beta_j^2/rho^2 - gamma theta (j^2-i^2)). (5) +``` + +To verify the exponent, before substituting c it is + +```text +b0 (theta/rho i^2 - 2c i - theta/rho^2 j^2 + + 2c/rho j + c^2) - gamma(j-i). +``` + +Set c=1/(2rho), beta_j=theta j-1/2, and expand. This gives the exponent +in (5) exactly. On 0 <= i < m and m <= j < 2m, its first term is +nonnegative and j^2-i^2 <= (2m-1)^2. Every entry of this m by m +rectangle, after checkerboard signs, is therefore at least + +```text +B = alpha exp(-gamma theta (2m-1)^2). +``` + +Choose x_j=(-1)^j/sqrt(m) on m <= j < 2m and zero elsewhere. +Its Euclidean norm is one. For each of the first m output rows, (5) +shows |(K^-1 x)_i| >= sqrt(m) B, with no cancellation. Summing their +squared magnitudes gives ||K^-1 x||_2 >= m B. This proves (1). + +## Matching order and scope + +For (2), set m=floor(1/(2 sqrt(theta))). Since theta <= 1/16, +1/(2 sqrt(theta)) >= 2, and floor(x) >= x/2 gives +m >= 1/(4 sqrt(theta)). Also theta(2m-1)^2 <= 1 and +gamma <= pi/alpha^2. Substitution into (1) proves (2). + +For example, N=floor(1/theta) meets the size and phase assumptions +for all 0 < theta <= 1/16. This includes N=400 at theta=1/400. +At alpha=3, m=10, the new bound is +30 exp(-361 pi/(3600 rho)), rho=401/400, and in particular exceeds +109/5. A rational certificate uses pi<22/7 and +exp(-t) >= 1-t+t^2/2-t^3/6 for 0= gamma0=16pi/(17alpha^2), giving a +finite fixed-alpha upper constant times theta^(-1/2). Combining that +cited upper result with (2) proves Theta_alpha(theta^(-1/2)) on the +stated family. No upper proof or numerical table of a predecessor is +claimed as new or replayed as a deliverable. + +The lower proof also works with arbitrary b0>0 independent of the positive +normalization alpha. The exact rational fixtures use this larger algebraic +family; specializing b0=pi/alpha^2 gives the source kernel. Finite tests +corroborate the inverse-sum, sign, gauge and rectangle steps. The written +argument carries the universal real-parameter claims. + +The sharp leading constant, a matching growing-alpha law, rounded inverse +execution, coefficient preparation, circuit prefixes, physical storage/tape, +native admission, outer transfer and integer recovery remain open. This +does not change the selected frontier or prove a multiplication theorem. diff --git a/research/gaussian-phase-cell-lower/README.md b/research/gaussian-phase-cell-lower/README.md new file mode 100644 index 0000000000..53e21a0926 --- /dev/null +++ b/research/gaussian-phase-cell-lower/README.md @@ -0,0 +1,121 @@ +# Broad Gaussian edge conditioning has sharp theta order + +This contribution was produced by Nick Petalas. Apache-2.0. + +Claim type: scoped analytic proof with exact finite corroboration. No new kappa. + +For the broad Gaussian matrix + +```text +K[k,i] = alpha^-1 exp(-pi/alpha^2 (i-k/rho-c)^2), +rho=1+theta, c=1/(2rho), 0<=k,i= alpha m exp(-pi theta (2m-1)^2/(alpha^2 rho)) +for every integer m>=1 with 2m<=N. +``` + +Consequently, for 0=2 floor(1/(2 sqrt(theta))), + +```text +||K^-1||_2 >= (alpha/4) exp(-pi/alpha^2) theta^(-1/2). +``` + +Together with the cited upper theorem of JoyboyBrian's +[PR5103](https://github.com/CrocSwap/integer-mult-bounds/pull/5103), this proves +the sharp order Theta_alpha(theta^(-1/2)) for these boundary sections at +fixed alpha. This answers its open matching-lower-estimate question. The +sharp leading coefficient in Ryanson Jonathan's +[PR4435](https://github.com/CrocSwap/integer-mult-bounds/pull/4435) remains open. + +[PROOF.md](PROOF.md) gives the universal argument. A checkerboard sign change +makes every inverse entry positive. One positive term of the cited finite +q-LDU inverse survives the exact diagonal gauges. An m by m rectangle at +the cell edge then gives an explicit alternating unit test vector and the +norm lower bound. No floating inverse, SVD or asymptotic boundary condition +is used in this proof. + +## Evidence and reproduction + +The verifier independently eliminates 36 rational Gaussian matrices of sizes +two through five, checks 416 inverse entries and 50 rectangle/test-vector +estimates. These fixtures use the larger algebraic family with independent +positive Gaussian exponent and normalization. They do not purport to sample +the transcendental source kernel exactly. Another 520 exact rational +exponent checks include the source fixture theta=1/400. There are 1,009 +floor-inequality checks and nine boundary/sign/overstatement controls. + +At the actual alpha=3, theta=1/400, N=400 fixture, m=10 gives a new +certified lower estimate exceeding 109/5. The rational polynomial +certificate is 8753084362189/400075200000 > 109/5. This is a lower bound +on the inverse norm, not its exact value or the sharp asymptotic constant. +The source fixture is used for this new estimate only; no predecessor +operator replay or numerical table is repeated as a contribution. + +From the repository root, using CPython 3.12 and its standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/gaussian-phase-cell-lower/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/gaussian-phase-cell-lower/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/gaussian-phase-cell-lower +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/gaussian-phase-cell-lower --check-source-history +``` + +Any CPython 3.12 installation can replace the displayed interpreter path. +The direct checks report PASS_GAUSSIAN_PHASE_CELL_LOWER; the registered +runner reports PASS_REGISTERED_RESEARCH_PACKAGE. Default execution writes +nothing. Optional --receipt NEW_EXTERNAL_PATH exclusively creates a generated +JSON receipt binding all six package files by SHA256. No receipt is handwritten. + +## Sources and limits + +The scientific base is canonical main +a5df48c55ea806d7952b65acc9c76d878ff09b13, priority revision 7. +[SOURCES.json](SOURCES.json) pins predecessor texts as provenance. No +predecessor code is imported and no external scientific input is read at replay. +The originating uniform-transfer-audit card is changed to this original +conditioning side result. The purpose is to settle the necessity of the edge +conditioning loss before refining its sharp constant or pricing a caller. + +Credit JoyboyBrian #5103 for the rigorous upper theorem and the open lower +question; Ryanson Jonathan #4408/#4435 for the scaling observation and formal +leading-coefficient prediction; Jose Manuel/jmbarrancoml #4193 for the finite +Toeplitz inverse estimate; Vlado Vojdanovski and the retained #1673 Gaussian +and q-LDU lineage; and Cinna Davis's later Gaussian caller. Classical finite +q-binomial identities retain their earlier mathematical credit. Their results, +credit lines and frozen evidence are unchanged. The positive lower rectangle +and the resulting matching-order theorem are the new contribution. + +This theorem fixes beta_0=-1/2 and requires a section containing a sufficiently +long boundary window. It gives no theta-dependent lower bound for arbitrary +tiny sections or sections separated from both edges. The alpha-dependent +constant is deliberately coarse. The universal claim rests on the written +proof, with finite exact checks as corroboration. Independent human and +formal proof-kernel review are unclaimed. + +Coefficient preparation, rounded inverse application, all circuit-prefix +norms, physical source access, restoration, storage/tape, native implementation, +compiler and outer integer recovery remain unpriced. No Lean, Docker, selected +operator replay or complete multiplication theorem is claimed. + +Live open PRs, recent account PRs, handoffs, active discussions, distinctive +main-tree and merged searches were checked before claiming and submission. +The initial cache covers 305 open PRs and 4,166 Discussion records. Sparse +local-note coverage is incomplete; no exhaustive novelty claim follows. +The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19144272) +records the scope. + +## Open next questions + +- Recover #4435's sharp leading coefficient, with a uniform boundary remainder + and a growing-alpha regime. Start by retaining more positive inverse terms + and optimizing boundary test vectors; a comparably sharp upper estimate is + still needed. The present lower constant does not establish that coefficient. +- Bind a complete rounded Gaussian caller before changing numerical guards. + Start with one pinned caller and retain its coefficient, prefix, restoration, + movement and storage costs. Endpoint conditioning alone supplies no physical + invoice. Structured questions are in [TASK.json](TASK.json). diff --git a/research/gaussian-phase-cell-lower/SOURCES.json b/research/gaussian-phase-cell-lower/SOURCES.json new file mode 100644 index 0000000000..613d839f72 --- /dev/null +++ b/research/gaussian-phase-cell-lower/SOURCES.json @@ -0,0 +1,54 @@ +{ + "schema_version": 1, + "base_commit": "a5df48c55ea806d7952b65acc9c76d878ff09b13", + "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/broad-phase-cell-inverse-bound/README.md", + "usage": "provenance", + "git_blob": "7f9ff994918c5c75e9006a8ceeed76a9cbbc2df8", + "sha256": "9fccbb6d58c5239c5f1072a2793df030657dd743b64ea44f637fba622c2f9a7f" + }, + { + "path": "research/broad-phase-cell-inverse-bound/PROOF.md", + "usage": "provenance", + "git_blob": "efc7842083ea33a69525f2baf17febae17bd8b6d", + "sha256": "3107aa37b026fef8b21f8ba859acfc7968eb94fed28a3169f5e559fbbd70e52d" + }, + { + "path": "research/forward-turning-point/README.md", + "usage": "provenance", + "git_blob": "3f487ef4f53021863060ca5b1a7560de22a287b5", + "sha256": "cae911dd36e8911333312a7640aa0ea513e76b2f4c4b8ef1eb1524302cd5a2d6" + }, + { + "path": "research/forward-fine-theta-conditioning/README.md", + "usage": "provenance", + "git_blob": "8e2831a88a7edc504daeba91261546437a2a5375", + "sha256": "8aafb8704479eefe1772b7f0d68284bac02ac916473f1a72c258be598c18e964" + }, + { + "path": "research/forward-fine-theta-conditioning/verify.py", + "usage": "provenance", + "git_blob": "48fdf11e4bb4da2928c439d03f05574f7b2c88a7", + "sha256": "0484ba72b20a805ae2a0e9bde0527f6d048389c6453642d5337064d2da23e547" + }, + { + "path": "research/capped-phase-fusion/FORWARD-SMALL-A-AUDIT.md", + "usage": "provenance", + "git_blob": "0f7f80b3f74d469c2f72f3b9f338d32568b4eae3", + "sha256": "e37aaa30b15671a1dff00676b14572213efaaac99df202dbba5e09f57af487c0" + } + ] +} diff --git a/research/gaussian-phase-cell-lower/TASK.json b/research/gaussian-phase-cell-lower/TASK.json new file mode 100644 index 0000000000..8965701069 --- /dev/null +++ b/research/gaussian-phase-cell-lower/TASK.json @@ -0,0 +1,86 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 7, + "base_commit": "a5df48c55ea806d7952b65acc9c76d878ff09b13", + "original_card": { + "id": "uniform-transfer-audit", + "question": "Does one quantified step of the proposed #4100 all-size construction hold at its actual caller?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/unconditional-batched-crt/README.md" + ], + "methods": [ + "Prove one missing implication with explicit quantified hypotheses.", + "Find an exact counterexample at the claimed interface boundary." + ], + "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_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read PROOF.md and AUDIT.md in #4100. Select one distinct obligation: CRT total repair, native/free-algebra lifting, precision/conditioning, or complete fixed-tape cost. This is an author-submitted proof, not an accepted unconditional theorem.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "Check live handoffs; name one proposition, its caller, quantified domain and dependency closure. Independently prove the implication or exhibit a precise gap/counterexample. Prioritize CRT.md total repair or COMPLEX.md free-algebra lift only if unclaimed. Stop at the chosen obligation; do not substitute finite samples or root arithmetic for an all-size proof, or launch the complete package by default.", + "bottleneck_link": "Finite supplier improvements are useful only under the retained transfer obligations.", + "allowed_variations": [ + "One CRT repair, native lift, precision/conditioning or tape-cost proposition, with its exact caller." + ], + "scope_change_triggers": [ + "Replacing a quantified obligation with another finite smoke test.", + "Treating archive intake, an author PASS receipt or a finite composed fixture as discharge of the universal hypotheses." + ], + "overlap_terms": [ + "uniform transfer", + "all-size", + "precision", + "4100", + "unconditional-batched-crt" + ], + "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_status": "changed", + "actual_scope": "Prove a matching theta^(-1/2) lower order for broad Gaussian phase-cell inverses at beta_0=-1/2, using a positive checkerboard rectangle.", + "scope_change_reason": "This answers the matching-lower-estimate question in PR5103 as an original precision-interface side result. It proves necessity of the cell-edge loss rather than auditing a predecessor's upper estimate.", + "bottleneck_link": "The Gaussian conditioning exponent affects precision budgets. A lower estimate distinguishes an unavoidable edge loss from slack in an upper proof; it does not price physical execution.", + "budget_minutes": 60, + "stop_rule": "Stop at the first proved matching-order lower estimate. Leave the sharp constant and complete physical caller open.", + "outcome": "completed", + "evidence": "PROOF.md supplies the universal argument. verify.py independently eliminates bounded rational Gaussian matrices, checks the new entry/rectangle inequalities and certifies the original alpha=3, theta=1/400 lower estimate.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "What is the sharp leading constant at the broad phase-cell boundary?", + "why_it_matters": "The order theorem does not prove the formal coefficient predicted in PR4435, especially as alpha grows.", + "first_step": "Retain more positive terms of the finite inverse and optimize boundary test vectors, then prove an equally sharp upper estimate.", + "blocked_by": "Uniform boundary remainder and control of the growing-alpha regime." + }, + { + "question": "Can a complete rounded Gaussian caller consume the matching-order estimates?", + "why_it_matters": "Endpoint conditioning alone gives no coefficient preparation, rounding, storage or tape implementation.", + "first_step": "Pin one actual caller and account for its complete prefix and preparation costs.", + "blocked_by": "A concrete physical caller and its full invoice." + } + ], + "claim_type": "Scoped analytic proof with exact finite corroboration", + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19144272", + "environment": { + "python": "Python 3.12.15", + "dependencies": "Python standard library only" + } +} diff --git a/research/gaussian-phase-cell-lower/VERIFY.json b/research/gaussian-phase-cell-lower/VERIFY.json new file mode 100644 index 0000000000..525d10d57f --- /dev/null +++ b/research/gaussian-phase-cell-lower/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": 240, + "checks": "Independent exact rational inverse, positive entry and rectangle lower bounds, rational source-fixture certificate and invalid/sign controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 240, + "checks": "The same mathematical and boundary checks with assertions disabled." + } + ] +} diff --git a/research/gaussian-phase-cell-lower/verify.py b/research/gaussian-phase-cell-lower/verify.py new file mode 100644 index 0000000000..8c208603e5 --- /dev/null +++ b/research/gaussian-phase-cell-lower/verify.py @@ -0,0 +1,170 @@ +#!/usr/bin/env python3 +"""Exact finite corroboration of the new Gaussian boundary lower estimate.""" +from __future__ import annotations + +import argparse +import hashlib +import json +from fractions import Fraction as F +from math import isqrt +from pathlib import Path + + +def need(condition: bool, message: str) -> None: + if not condition: + raise ValueError(message) + + +def inverse(matrix: list[list[F]]) -> list[list[F]]: + n = len(matrix) + need(1 <= n <= 5 and all(len(row) == n for row in matrix), "matrix size") + rows = [row[:] + [F(i == j) for j in range(n)] + for i, row in enumerate(matrix)] + for col in range(n): + pivot = next((k for k in range(col, n) if rows[k][col]), None) + need(pivot is not None, "singular matrix") + rows[col], rows[pivot] = rows[pivot], rows[col] + value = rows[col][col] + rows[col] = [x / value for x in rows[col]] + for k in range(n): + if k != col: + value = rows[k][col] + rows[k] = [x - value * y for x, y in zip(rows[k], rows[col])] + return [row[n:] for row in rows] + + +def inverse_sum(n: int, q: F) -> list[list[F]]: + """The cited finite q-LDU formula, with no predecessor code import.""" + products = [F(1)] + for k in range(1, n): + products.append(products[-1] * (1 - q ** (2 * k))) + result = [[F(0) for _ in range(n)] for _ in range(n)] + for i in range(n): + for j in range(n): + value = sum((q ** (2 * k - i - j) * products[k] + / (products[i] * products[k - i] + * products[j] * products[k - j]) + for k in range(max(i, j), n)), F(0)) + result[i][j] = (-1) ** (i + j) * value + return result + + +def fixture(n: int, h: int, r: F) -> dict[str, int]: + """Rational exact Gaussians with theta=1/h and arbitrary positive b0.""" + need(2 <= n <= 5 and n <= h <= 16, "fixture phase/size") + need(F(0) < r < F(1), "Gaussian base") + alpha, degree = F(3, 2), 4 * h * (h + 1) + q = r ** degree + gaussian = [[q ** ((i - j) ** 2) for j in range(n)] for i in range(n)] + exact_g = inverse(gaussian) + need(exact_g == inverse_sum(n, q), "finite inverse sum") + matrix = [[r ** ((2 * (h + 1) * i - 2 * h * k - h) ** 2) / alpha + for i in range(n)] for k in range(n)] + exact = inverse(matrix) + for i in range(n): + col = 4 * (h + 1) * i * i - 4 * h * (h + 1) * i + for j in range(n): + row = -4 * h * j * j + 4 * h * h * j + h * h + signed = (-1) ** (i + j) * exact[i][j] + need(exact[i][j] == alpha * r ** (-col - row) * exact_g[i][j], + "inverse gauge identity") + need(signed >= alpha * r ** (degree * abs(i - j) - col - row), + "positive single-term lower estimate") + rectangles = 0 + for m in range(1, n // 2 + 1): + floor = alpha * r ** (4 * (h + 1) * (2 * m - 1) ** 2) + for i in range(m): + for j in range(m, 2 * m): + need((-1) ** (i + j) * exact[i][j] >= floor, "rectangle") + vector = [F((-1) ** j if m <= j < 2 * m else 0) for j in range(n)] + output = [sum((x * y for x, y in zip(row, vector)), F(0)) + for row in exact] + need(sum(x * x for x in output) >= m * (m * floor) ** 2, + "explicit alternating test vector") + rectangles += 1 + return {"entries": n * n, "rectangles": rectangles} + + +def coefficient_checks() -> dict[str, int]: + pairs = 0 + for h in (16, 64, 400, 1600): + theta, rho = F(1, h), F(h + 1, h) + c, m = 1 / (2 * rho), isqrt(h) // 2 + for i in range(m): + for j in range(m, 2 * m): + beta_i, beta_j = theta * i - F(1, 2), theta * j - F(1, 2) + raw = (theta / rho * i * i - 2 * c * i + - theta / rho ** 2 * j * j + 2 * c / rho * j + + c * c - abs(i - j) / rho) + coupled = beta_j ** 2 / rho ** 2 - theta / rho * (j * j - i * i) + need(raw == coupled, "coupled boundary exponent") + need(-F(1, 2) <= beta_i <= beta_j <= F(1, 2), "phase") + need(raw >= -theta / rho * (2 * m - 1) ** 2, "exponent floor") + pairs += 1 + for h in range(16, 1025): + m = isqrt(h) // 2 + need(16 * m * m >= h and (2 * m - 1) ** 2 <= h, "floor inequalities") + # pi < 22/7 and exp(-t) >= 1-t+t^2/2-t^3/6 for 0 F(109, 5), "actual alpha=3, theta=1/400 lower certificate") + return {"exponent_pairs": pairs, "floor_cases": 1009, + "first_fixture_lower_numerator": lower.numerator, + "first_fixture_lower_denominator": lower.denominator} + + +def controls() -> int: + rejected = 0 + for n, h, r in ((1, 4, F(1, 2)), (4, 3, F(1, 2)), + (6, 8, F(1, 2)), (2, 17, F(1, 2)), + (2, 4, F(0)), (2, 4, F(1))): + try: + fixture(n, h, r) + except ValueError: + rejected += 1 + else: + raise ValueError("invalid fixture accepted") + try: + inverse([[F(1), F(1)], [F(1), F(1)]]) + except ValueError: + rejected += 1 + else: + raise ValueError("singular control accepted") + gi = inverse([[F(1), F(1, 2)], [F(1, 2), F(1)]]) + need(gi[0][1] < 0, "omitting checkerboard signs must fail") + need((-1) * gi[0][1] >= F(1, 2), "signed positive control") + need((-1) * gi[0][1] < F(1), "overstated one-term floor must fail") + return rejected + 2 + + +def main() -> None: + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--receipt", type=Path) + args = parser.parse_args() + entries = rectangles = cases = 0 + for h in (2, 3, 4, 6, 9, 16): + for n in range(2, min(h, 5) + 1): + for r in (F(1, 2), F(2, 3)): + result = fixture(n, h, r) + entries += result["entries"] + rectangles += result["rectangles"] + cases += 1 + report = {"status": "PASS_GAUSSIAN_PHASE_CELL_LOWER", "exact_gaussian_cases": cases, + "inverse_entries": entries, "rectangle_tests": rectangles, + "controls": controls(), **coefficient_checks(), "new_kappa": False} + package = Path(__file__).resolve().parent + names = ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", "VERIFY.json", "verify.py") + report["sha256"] = {name: hashlib.sha256((package / name).read_bytes()).hexdigest() + for name in names} + payload = json.dumps(report, indent=2, sort_keys=True) + "\n" + if args.receipt: + target = args.receipt.resolve() + need(not target.is_relative_to(package), "receipt must be outside package") + with target.open("x", encoding="utf-8") as handle: + written = handle.write(payload) + need(written == len(payload), "complete receipt write") + print(payload, end="") + + +if __name__ == "__main__": + main()