From 6022a32a01cf8bdc19d382fa1a657ecd4afada14 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Fri, 23 Oct 2026 00:42:57 +0100 Subject: [PATCH] feat(research): prove sharp mixed-quadratic inverse bound --- .../mixed-quadratic-circle-bound/PROOF.md | 119 ++++++++ .../mixed-quadratic-circle-bound/README.md | 104 +++++++ .../mixed-quadratic-circle-bound/SOURCES.json | 37 +++ .../mixed-quadratic-circle-bound/TASK.json | 85 ++++++ .../mixed-quadratic-circle-bound/VERIFY.json | 34 +++ .../mixed-quadratic-circle-bound/verify.py | 267 ++++++++++++++++++ 6 files changed, 646 insertions(+) create mode 100644 research/mixed-quadratic-circle-bound/PROOF.md create mode 100644 research/mixed-quadratic-circle-bound/README.md create mode 100644 research/mixed-quadratic-circle-bound/SOURCES.json create mode 100644 research/mixed-quadratic-circle-bound/TASK.json create mode 100644 research/mixed-quadratic-circle-bound/VERIFY.json create mode 100644 research/mixed-quadratic-circle-bound/verify.py diff --git a/research/mixed-quadratic-circle-bound/PROOF.md b/research/mixed-quadratic-circle-bound/PROOF.md new file mode 100644 index 0000000000..8e3012db80 --- /dev/null +++ b/research/mixed-quadratic-circle-bound/PROOF.md @@ -0,0 +1,119 @@ +# Sharp inverse bounds for a mixed quadratic + +This scoped proof is produced by Nick Petalas. The cyclic operator setting and +the general degree multiplier are credited to Ali Romman #621 and Rafael +Guevara #803. Geometric series, partial fractions and the triangle inequality +are classical. No literature-priority claim is made for those methods. + +Let + + P(z) = c (z-a)(1-bz), c != 0, |a|=A<1, 0<|b|=B<1. + +Thus P has exactly one root in the open unit disk and one outside its closure. +Put m=min(A,B) and delta=min_{|z|=1}|P(z)|>0. For an absolutely convergent +Laurent series, its Wiener norm is the sum of the absolute values of its +coefficients. Then + + delta ||1/P||_W <= (1+m)^2/(1+m^2) < 2. (1) + +For every fixed 0<=m<1 the displayed factor is best possible among this +class with min(A,B)=m. Consequently the best factor independent of the roots +is two. In particular, the general degree-two multiplier 81 obtained by +substituting n=2 in #803 can be replaced by two on this subclass. This is a +strengthening of a bound, not a defect in that predecessor. + +## Exact Laurent norm + +It suffices to take c=1, since delta scales by |c| and the inverse norm by +its reciprocal. On the unit circle the two absolutely convergent geometric +series give + + 1/((z-a)(1-bz)) + = 1/(1-ab) [ sum_{j>=0} b^(j+1) z^j + + sum_{h>=1} a^(h-1) z^(-h) ]. (2) + +One can obtain (2) by multiplying the geometric series for each factor, +or by partial fractions. The positive and negative exponent sets are disjoint. +Since A,B<1, their absolute sums are geometric, so + + ||1/P||_W = (1-AB)/((1-A)(1-B)|1-ab|). (3) + +No cancellation or asymptotic estimate enters (3). + +## The sharp upper bound + +For 0<=x<=y<1 and every real theta, + + |1-y exp(i theta)| / |1-x exp(i theta)| + <= (1+y)/(1+x). (4) + +To prove this, square the ratio and put t=cos(theta). Its derivative in t +has the sign of (x-y)(1-xy), which is nonpositive. The maximum is at t=-1. +This also proves (4) at x=0 and at x=y without division by a vanishing quantity. + +Suppose first A>=B. Here A>0. Evaluate P at z=a/A and apply (4) with +x=AB, y=B and exp(i theta)=ab/(AB). Equations (3) and (4) give + + delta ||1/P||_W + <= (1-AB)(1+B)/((1-B)(1+AB)) + <= (1-B^2)(1+B)/((1-B)(1+B^2)) + = (1+B)^2/(1+B^2). (5) + +The second inequality follows because (1-x)/(1+x) decreases for x>=0 +and AB>=B^2. If B>A, evaluate instead at z=conjugate(b)/B. The identical +argument with A,B interchanged gives (1). This also covers A=0 directly: +(3) and delta=1-B give product one. Finally +(1+m)^2<2(1+m^2) is equivalent to (1-m)^2>0. + +## Attainment and the uniform factor + +For any 0= (1-r^2)^2. + +Equality holds at z=1 and z=-1, so delta=1-r^2. Equation (3) yields + + delta ||1/P||_W = (1+r)^2/(1+r^2). (6) + +This proves sharpness for every fixed m=r>0 and tends to two as r tends +to one from below. At m=0, use a=0 and any 0=0 and L>2K, the coefficients with |k|<=K have distinct residues. +Writing T_K=sum_{|k|>K}|d_k|, the triangle inequality in both directions gives + + ||1/P||_W - 2T_K <= sum_j |q_j| <= ||1/P||_W. + +Since T_K tends to zero, these finite cyclic norms tend to the Wiener norm. +Apply this to the rational family in (6), first taking L large at fixed r, +then taking r towards one. No smaller uniform cyclic constant can work. + +## Boundaries + +The proof uses the exactly quadratic mixed-root factorization. It does not +improve #803's general arbitrary-degree theorem. It supplies no coefficient +preparation, rounded algorithm, source restoration, paid tape schedule, +physical supplier, new kappa or complete multiplication theorem. The finite +checks corroborate formulas and finite cyclic inverses; the universal result +rests on this written proof. Independent human and formal proof-kernel review +are unclaimed. diff --git a/research/mixed-quadratic-circle-bound/README.md b/research/mixed-quadratic-circle-bound/README.md new file mode 100644 index 0000000000..e99005b96b --- /dev/null +++ b/research/mixed-quadratic-circle-bound/README.md @@ -0,0 +1,104 @@ +# Sharp factor two for mixed quadratic cyclic inverses + +This scoped proof is produced by Nick Petalas. For + + P(z)=c(z-a)(1-bz), c!=0, |a|<1, 0<|b|<1, + delta=min_{|z|=1}|P(z)|, m=min(|a|,|b|), + +the [written proof](PROOF.md) establishes + + delta ||1/P||_W <= (1+m)^2/(1+m^2) < 2. + +The Wiener norm sums the absolute values of the Laurent coefficients. The +radius-sensitive factor is optimal at each fixed m, and two is the least +uniform factor. Both statements also hold for the induced infinity norm of +`P(tau Z_L^w)^(-1)`, uniformly over positive cyclic lengths, integer strides +and unit phases. Sharpness there is a limit over cyclic lengths. + +Rafael Guevara's [#803](https://github.com/CrocSwap/integer-mult-bounds/pull/803) +proves the general degree bound `(1+4n)^2/delta` and leaves its degree factor +nonoptimal. On this mixed-root degree-two subclass, the sufficient multiplier +therefore falls from 81 to two. The new step is the exact two-sided Laurent +norm and a sharp endpoint bound. The antipodal family `a=r,b=-r` attains +`(1+r)^2/(1+r^2)` and approaches two. No predecessor result is replayed or audited. + +## Evidence and reproduction + +Standard-library CPython 3.12 is sufficient. From the repository root: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/mixed-quadratic-circle-bound +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/mixed-quadratic-circle-bound/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/mixed-quadratic-circle-bound/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/mixed-quadratic-circle-bound --check-source-history +``` + +A reviewer can substitute their CPython 3.12 executable. Direct verification +also works from a Git-free export. Ordinary verification writes no files. +`--emit-to NEW_EXTERNAL_FILE` exclusively creates a generated receipt with all +six package source hashes; `--check-receipt FILE` recomputes every result and +compares it with the receipt, including integer/Boolean types. No receipt is +hand-written or required as an external replay input. + +The executed finite coverage is: + +- 192 exact endpoint inequalities across four interior radii, three reciprocal + exterior radii and every pair of phases in `{1,-1,i,-i}`. +- 768 cyclic inverse comparisons between dense elimination and a finite + geometric resolvent construction, with 2,688 inverse entries. Eight root + pairs, lengths 1 through 6, strides `-1,0,1,2` and all four unit phases are + crossed. Both inverse identities and rational upper enclosures of the norms + are checked. The 192 antipodal cases also use their exact circle gap. +- 63 rational sharpness identities at `r=(d-1)/d`, `d=2,...,64`. The final + normalized Wiener norm is `16129/8065`, with exact deficit `1/8065` from two. +- Eight controls cover three invalid root domains, wrong factor sign, wrong + inverse direction, wrong gauge, omitted negative Fourier frequencies, and a + finite cyclic counterexample to replacing the factor by one. + +The enumerations corroborate the universal proof. They do not exhaust complex +roots or establish the universal theorem by sampling. Receipt mutation, +exclusive-create and source-hash controls are separate publication checks. + +## Scope and implementation limits + +This is a scoped proof with finite corroboration, not a finite supplier +certificate or complete multiplication theorem. No new kappa is claimed. +The theorem concerns exact operators with one interior and one exterior root. +It gives no coefficient preparation, rounded execution, dirty restoration, +fixed-tape schedule, complete caller invoice or supplier admission. The selected +frontier remains unchanged. Independent human and formal proof-kernel review +are unclaimed. No Lean, Docker or selected cold replay is required or run. + +The verifier has no recursive calls. Its finite mathematical loops are bounded +by the displayed corpus, matrix size six and exponent 64; functions remain +below 60 lines. Explicit exceptions retain the checks under optimization. +Python's managed allocation is a deviation from fixed storage: all matrix +storage is bounded by six rows of seven Gaussian rationals, and external +receipt size is bounded by one MiB. Library arithmetic and JSON parsing use +runtime allocation. A lower-level implementation would require its own storage +proof. Warning-strict normal and optimized execution provide available +diagnostics; no separate linter or type checker is installed in this environment. + +Source pins in [SOURCES.json](SOURCES.json) are historical provenance at canonical +main `624de9dc66858af0945e5f8a0942488d62280d43`. There are no imported predecessor +executables or live mathematical dependencies. [TASK.json](TASK.json) records +the changed card scope and structured next questions. + +## Open next questions + +1. Determine the best multiplier when both quadratic roots are outside the + unit circle. Start with separated two-pole phases and exact coefficient + sums. Coefficient cancellation blocks the disjoint-series argument here. +2. Apply the bound to one actual source-bound mixed quadratic caller's complete + rounding recurrence. First identify the factor, then charge preparation, + every prefix and restoration. A complete physical invoice remains missing. + +## Credit + +Credit Rafael Guevara #803 for the general degree-controlled bound and its +nonoptimality question, Ali Romman #621 for the cyclic kernel setting, and +Thiago Costa #802 for the related Fourier-transfer work. Geometric-series +resolvents and Fourier substitution are classical; Ryan Pinto #692 retains +credit for the retained finite-geometric cyclic implementation lineage. No +literature-priority claim is made for those methods. This result is produced +by Nick Petalas. New files are under Apache-2.0. diff --git a/research/mixed-quadratic-circle-bound/SOURCES.json b/research/mixed-quadratic-circle-bound/SOURCES.json new file mode 100644 index 0000000000..cfac9f6e69 --- /dev/null +++ b/research/mixed-quadratic-circle-bound/SOURCES.json @@ -0,0 +1,37 @@ +{ + "schema_version": 1, + "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43", + "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/rational-circle-bound/README.md", + "usage": "provenance", + "git_blob": "1a1d3068a85a41ceabdf512e30aa15c448ccd321", + "sha256": "77dcfe10cf69b66e092c4bf9501353cd82e61d899fca0b983f60dec25e012c4f" + }, + { + "path": "research/rational-circle-bound/PROOF.md", + "usage": "provenance", + "git_blob": "15d344789d1ae475790f5d6a45cd37ae27f05d1c", + "sha256": "6c28d93d9d1d37da0bbc3876070ef8c6f0f5dad8e186b31b31330028e5420c0e" + }, + { + "path": "research/prime-power-cyclic-inverse/PROOF.md", + "usage": "provenance", + "git_blob": "0c757c37c70fdeb261d73f111ceedd3b233287bf", + "sha256": "2b8056c88e66f692f407450fff0414d41bcd09db8597be22e274a6c3dc20eb9e" + } + ], + "note": "Historical mathematical context only. No predecessor executable is imported or replayed." +} diff --git a/research/mixed-quadratic-circle-bound/TASK.json b/research/mixed-quadratic-circle-bound/TASK.json new file mode 100644 index 0000000000..806ff331b7 --- /dev/null +++ b/research/mixed-quadratic-circle-bound/TASK.json @@ -0,0 +1,85 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 7, + "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43", + "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": "Sharp Wiener and cyclic inverse-circle-gap factor two for quadratics with one interior and one exterior root, and sharp radius-sensitive factor (1+m)^2/(1+m^2).", + "scope_change_reason": "The assignment requires original work rather than rechecking predecessors. This card is redirected to the nonoptimal conditioning multiplier in #803, a scoped cyclic-interface side result.", + "bottleneck_link": "Scoped conditioning side result for the cyclic inverse interface. It reduces a sufficient norm multiplier for mixed quadratic factors, without a paid implementation or new kappa.", + "budget_minutes": 60, + "stop_rule": "Stop after the first proved sharp mixed-quadratic strengthening and exact bounded corroboration; do not extend to other degrees.", + "outcome": "completed", + "evidence": "PROOF.md and warning-strict normal/optimized verify.py. Finite cases corroborate the proof, rather than prove universal quantifiers.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "What is the optimal inverse-circle-gap multiplier for quadratics whose two roots are both outside the unit circle?", + "why_it_matters": "This would address another subclass of the nonoptimal general degree bound.", + "first_step": "Derive the exact coefficient absolute sum for a two-pole rational family with separated phases.", + "blocked_by": "Coefficient cancellation prevents the disjoint two-sided geometric-series argument used here." + }, + { + "question": "Can one actual cyclic-factor caller use the sharper bound in its complete rounding recurrence?", + "why_it_matters": "A norm improvement only reduces physical precision if it reaches a paid implementation.", + "first_step": "Identify a source-bound mixed quadratic and reprice coefficient preparation, every rounded prefix and restoration.", + "blocked_by": "No such caller or complete resource invoice is supplied here." + } + ], + "environment": { + "python": "3.12.15", + "implementation": "CPython", + "dependencies": "standard library only" + } +} diff --git a/research/mixed-quadratic-circle-bound/VERIFY.json b/research/mixed-quadratic-circle-bound/VERIFY.json new file mode 100644 index 0000000000..fc37fb94ad --- /dev/null +++ b/research/mixed-quadratic-circle-bound/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": "192 exact endpoint inequalities, 768 dense/geometric cyclic inverse comparisons, 63 sharpness identities and eight semantic controls; source-bound receipt emission is optional and external." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "192 exact endpoint inequalities, 768 dense/geometric cyclic inverse comparisons, 63 sharpness identities and eight semantic controls; source-bound receipt emission is optional and external." + } + ] +} diff --git a/research/mixed-quadratic-circle-bound/verify.py b/research/mixed-quadratic-circle-bound/verify.py new file mode 100644 index 0000000000..37e8eb8947 --- /dev/null +++ b/research/mixed-quadratic-circle-bound/verify.py @@ -0,0 +1,267 @@ +#!/usr/bin/env python3 +"""Exact finite corroboration for the mixed-quadratic circle bound.""" +from __future__ import annotations + +import argparse +import hashlib +import json +from fractions import Fraction as F +from itertools import product +from math import isqrt +from pathlib import Path + +G = tuple[F, F] +ZERO: G = (F(0), F(0)) +ONE: G = (F(1), F(0)) +PHASES: tuple[G, ...] = (ONE, (F(-1), F(0)), (F(0), F(1)), (F(0), F(-1))) +HERE = Path(__file__).resolve().parent + + +def need(condition: bool, message: str) -> None: + if not condition: + raise ValueError(message) + + +def add(a: G, b: G) -> G: + return a[0] + b[0], a[1] + b[1] + + +def neg(a: G) -> G: + return -a[0], -a[1] + + +def mul(a: G, b: G) -> G: + return a[0] * b[0] - a[1] * b[1], a[0] * b[1] + a[1] * b[0] + + +def abs2(a: G) -> F: + return a[0] ** 2 + a[1] ** 2 + + +def scale(a: G, value: F) -> G: + return a[0] * value, a[1] * value + + +def inverse(a: G) -> G: + norm = abs2(a) + need(norm != 0, "singular scalar") + return a[0] / norm, -a[1] / norm + + +def power(a: G, exponent: int) -> G: + need(0 <= exponent <= 64, "power bound") + result = ONE + for _ in range(exponent): + result = mul(result, a) + return result + + +def contract(a: G, b: G) -> None: + need(abs2(a) < 1 and 0 < abs2(b) < 1, "mixed-root domain") + + +def sqrt_bounds(value: F) -> tuple[F, F]: + need(value >= 0, "nonnegative square") + numerator, denominator = isqrt(value.numerator), isqrt(value.denominator) + if numerator**2 == value.numerator and denominator**2 == value.denominator: + exact = F(numerator, denominator) + return exact, exact + bits = 1 << 96 + lower = isqrt(value.numerator * bits**2 // value.denominator) + return F(lower, bits), F(lower + 1, bits) + + +def circle_checks() -> int: + count = 0 + for A, B, alpha, beta in product( + (F(0), F(1, 4), F(1, 2), F(3, 4)), + (F(1, 4), F(1, 2), F(3, 4)), PHASES, PHASES + ): + a, b = scale(alpha, A), scale(beta, B) + contract(a, b) + wiener2 = ((1 - A * B) / ((1 - A) * (1 - B))) ** 2 + wiener2 /= abs2(add(ONE, neg(mul(a, b)))) + z = alpha if A >= B else (beta[0], -beta[1]) + endpoint2 = abs2(mul(add(z, neg(a)), add(ONE, neg(mul(b, z))))) + m = min(A, B) + cap = (1 + m) ** 2 / (1 + m * m) + need(endpoint2 * wiener2 <= cap**2, "sharp endpoint inequality") + count += 1 + return count + + +def kernel(a: G, b: G, length: int, stride: int, tau: G) -> list[G]: + need(1 <= length <= 6 and -1 <= stride <= 2, "finite cyclic domain") + contract(a, b) + need(abs2(tau) == 1, "unit gauge") + coefficients = [neg(a), add(ONE, mul(a, b)), neg(b)] + row = [ZERO] * length + for degree, coefficient in enumerate(coefficients): + slot = degree * stride % length + row[slot] = add(row[slot], mul(coefficient, power(tau, degree))) + return row + + +def convolution(a: list[G], b: list[G]) -> list[G]: + need(len(a) == len(b) and 1 <= len(a) <= 6, "convolution shape") + length = len(a) + result = [ZERO] * length + for i in range(length): + for j in range(length): + slot = (i + j) % length + result[slot] = add(result[slot], mul(a[i], b[j])) + return result + + +def geometric_inverse(a: G, b: G, length: int, stride: int, tau: G) -> list[G]: + contract(a, b) + need(1 <= length <= 6 and -1 <= stride <= 2 and abs2(tau) == 1, + "geometric cyclic domain") + left, right = [ZERO] * length, [ZERO] * length + left_den = inverse(add(power(tau, length), neg(power(a, length)))) + right_den = inverse(add(ONE, neg(mul(power(b, length), power(tau, length))))) + for k in range(length): + slot = k * stride % length + left_term = mul(mul(power(a, length - 1 - k), power(tau, k)), left_den) + right_term = mul(mul(power(b, k), power(tau, k)), right_den) + left[slot] = add(left[slot], left_term) + right[slot] = add(right[slot], right_term) + return convolution(left, right) + + +def dense_inverse(row: list[G]) -> list[G]: + length = len(row) + need(1 <= length <= 6, "dense size bound") + matrix = [[row[(i - j) % length] for j in range(length)] + + [ONE if i == 0 else ZERO] for i in range(length)] + for column in range(length): + pivot = next((i for i in range(column, length) if matrix[i][column] != ZERO), None) + need(pivot is not None, "singular cyclic polynomial") + matrix[column], matrix[pivot] = matrix[pivot], matrix[column] + divisor = inverse(matrix[column][column]) + matrix[column] = [mul(value, divisor) for value in matrix[column]] + for i in range(length): + if i != column: + coefficient = matrix[i][column] + matrix[i] = [add(x, neg(mul(coefficient, y))) + for x, y in zip(matrix[i], matrix[column])] + return [matrix[i][-1] for i in range(length)] + + +def cyclic_checks() -> dict[str, int]: + root_pairs = ((ZERO, (F(1, 2), F(0))), + ((F(1, 2), F(0)), (F(-1, 2), F(0))), + ((F(3, 4), F(0)), (F(-3, 4), F(0))), + ((F(1, 4), F(0)), (F(1, 2), F(0))), + ((F(0), F(1, 2)), (F(1, 4), F(0))), + ((F(1, 4), F(0)), (F(0), F(3, 4))), + ((F(0), F(1, 2)), (F(0), F(1, 2))), + ((F(0), F(-1, 2)), (F(1, 2), F(0)))) + count, entries, antipodal = 0, 0, 0 + for (a, b), length, stride, tau in product(root_pairs, range(1, 7), range(-1, 3), PHASES): + row = kernel(a, b, length, stride, tau) + oracle = geometric_inverse(a, b, length, stride, tau) + need(dense_inverse(row) == oracle, "dense/geometric disagreement") + identity = [ONE] + [ZERO] * (length - 1) + need(convolution(row, oracle) == identity, "right inverse") + need(convolution(oracle, row) == identity, "left inverse") + a_bounds, b_bounds = sqrt_bounds(abs2(a)), sqrt_bounds(abs2(b)) + need(a_bounds[0] == a_bounds[1] and b_bounds[0] == b_bounds[1], + "fixture radii must be rational") + A, B = a_bounds[0], b_bounds[0] + wiener2 = ((1 - A * B) / ((1 - A) * (1 - B))) ** 2 + wiener2 /= abs2(add(ONE, neg(mul(a, b)))) + norm_upper = sum(sqrt_bounds(abs2(value))[1] for value in oracle) + need(norm_upper**2 <= wiener2, "cyclic norm exceeds exact Wiener norm") + if a[1] == 0 and a[0] > 0 and b == neg(a): + delta = 1 - a[0] ** 2 + cap = (1 + a[0]) ** 2 / (1 + a[0] ** 2) + need(norm_upper * delta <= cap, "antipodal sharp bound") + antipodal += 1 + count += 1 + entries += length + return {"cases": count, "inverse_entries": entries, "antipodal_cases": antipodal} + + +def sharpness_checks() -> dict[str, object]: + ratios = [] + for denominator in range(2, 65): + r = F(denominator - 1, denominator) + delta = 1 - r * r + wiener = (1 + r) / ((1 - r) * (1 + r * r)) + ratio = delta * wiener + need(ratio == (1 + r)**2 / (1 + r * r), "attainment formula") + need(2 - ratio == (1 - r)**2 / (1 + r * r), "sharp limit identity") + need((1 + r*r)**2 - 4*r*r == delta**2, "circle minimum identity") + ratios.append(str(ratio)) + return {"cases": len(ratios), "last_ratio": ratios[-1]} + + +def controls() -> int: + count = 0 + invalid = ((ONE, (F(1, 2), F(0))), (ZERO, ONE), (ZERO, ZERO)) + for a, b in invalid: + try: + contract(a, b) + except ValueError: + count += 1 + else: + raise ValueError("invalid root pair accepted") + a, b = (F(1, 2), F(0)), (F(-1, 2), F(0)) + row = kernel(a, b, 5, 1, ONE) + result = geometric_inverse(a, b, 5, 1, ONE) + need(result != geometric_inverse(a, neg(b), 5, 1, ONE), "wrong-sign control") + need(convolution(row, list(reversed(result))) != [ONE] + [ZERO]*4, + "wrong-direction control") + need(geometric_inverse(a, b, 5, 1, PHASES[2]) != result, "gauge control") + norm_lower = sum(sqrt_bounds(abs2(value))[0] for value in result) + omitted_negative_norm = F(1, 2) / ((1 - F(1, 2)) * (1 + F(1, 4))) + need(norm_lower > omitted_negative_norm, "missing-negative-frequency control") + need(norm_lower * F(3, 4) > 1, "finite cyclic factor-one counterexample") + return count + 5 + + +def result() -> dict[str, object]: + names = ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", "VERIFY.json", "verify.py") + hashes = {name: hashlib.sha256((HERE/name).read_bytes()).hexdigest() for name in names} + return {"schema_version": 1, "claim_type": "scoped proof with finite corroboration", + "circle_cases": circle_checks(), "cyclic": cyclic_checks(), + "sharpness": sharpness_checks(), "controls": controls(), + "source_sha256": hashes, "no_new_kappa": True} + + +def read_receipt(path: Path) -> object: + need(path.stat().st_size <= 1 << 20, "receipt size limit") + + def unique_pairs(pairs: list[tuple[str, object]]) -> dict[str, object]: + need(len(pairs) <= 256, "receipt object size limit") + result = {} + for key, value in pairs: + need(key not in result, "duplicate receipt key") + result[key] = value + return result + + return json.loads(path.read_text(encoding="utf-8"), object_pairs_hook=unique_pairs) + + +def main() -> None: + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--emit-to", type=Path) + parser.add_argument("--check-receipt", type=Path) + args = parser.parse_args() + payload = result() + serialized = json.dumps(payload, indent=2, sort_keys=True) + "\n" + if args.check_receipt: + actual = read_receipt(args.check_receipt) + need(json.dumps(actual, sort_keys=True) == json.dumps(payload, sort_keys=True), + "receipt differs from recomputed result and source hashes") + if args.emit_to: + destination = args.emit_to.resolve() + need(not destination.is_relative_to(HERE.parent.parent), "receipt must be outside checkout") + with destination.open("x", encoding="utf-8") as output: + need(output.write(serialized) == len(serialized), "short receipt write") + print("PASS_MIXED_QUADRATIC_CIRCLE_BOUND", serialized.strip()) + + +if __name__ == "__main__": + main()