DONE: deterministic nearest rounding forces quadratic closed-word error

[aliromman]

DONE — nearest coefficient rounding still requires quadratic closed-word guards. This answers a specified-policy case of Open next question 2 in Nick Petalas's PR #5153, with a pinned statement of that question. Scoped written lower construction with exact finite checks; no new kappa or selected-frontier change. The advance claim is complete.

Policy and word. Round every gate entry to the nearest multiple of h=2^(-P), P>=1. Any tie convention is allowed: none of the constructed coefficients is a tie. Apply the rounded matrices with exact arithmetic; this isolates coefficient rounding from arithmetic rounding.

For q,m>=1, set s=2^q and define

S = diag(1/2,2),             U(a) = [[1,a],[0,1]].
Execution order:
q copies of S,
m copies of the three-gate loop U(a), U(a), U(-2a),
q copies of S^(-1).

The gate count is K=2q+3m. The exact endpoint is I. Every exact gate, its inverse, every rounded gate and its inverse have infinity norm at most 2 and determinant one. Two coefficient choices give the following exact formulas:

Dyadic family: a=3h/8.
  exact prefix/inverse maximum B = s(1+3h/4),
  rounded endpoint = U(-m h s^2).

Fixed rational family: a=1/3, independent of P.
  exact prefix/inverse maximum B = 5s/3,
  rounded endpoint = U((-1)^(P+1) m h s^2).

In both families the endpoint operator error is exactly m h s^2. The input vector (0,1) attains this error. The fixed rational word therefore exhibits the amplification at every dyadic precision. The dyadic family shows the same obstruction within the class of dyadic exact coefficients, but depends on the selected grid; a single fixed dyadic word is eventually represented exactly.

Proof. Each exact loop has coefficient sum a+a-2a=0. Scale entries 1/2 and 2 are exact on every grid with P>=1. For a=3h/8, the three rounded coefficients are 0,0,-h. For a=1/3, 2^P has residue 1 or 2 modulo 3. Direct nearest rounding gives a coefficient sum of -h for even P and +h for odd P. These are not arbitrary error assignments.

All m rounded loops commute and sum to U(plus-or-minus m h). The scale blocks conjugate this to U(plus-or-minus m h s^2). This proves the exact endpoint and error formulas.

During a middle loop an exact prefix is U(t)diag(1/s,s), where t is 0,a,or 2a. Its inverse is diag(s,1/s)U(-t). Since s>=2 and 0<=t<=2/3, their largest infinity norm is s(1+t). The maximum occurs at t=2a. Earlier and later scale prefixes have norm and inverse norm at most s. This proves the displayed B. Local gate bounds and determinant statements follow directly from the displayed two-by-two matrices and their inverses.

Guard consequence. Taking m=q gives K=5q. For every fixed epsilon>0, the ratio of the actual error to K B^(2-epsilon) h tends to infinity as q grows. Thus nearest rounding cannot replace the quadratic B power by any smaller fixed power in a uniform closed-word bound of this form. More generally the same construction defeats a smaller power times any fixed polynomial in K. At fixed q, varying m proves linear growth in the number of repeated loops while B stays fixed. Choosing P>=2q+ceil(log2(m))+4 keeps the actual error at most 1/16; the obstruction is present in the small-error regime.

This does not establish an optimal numerical guard constant. The predecessor's arbitrary-error lower construction and endpoint upper theorem retain their credit. The new point is an explicit correlated error pattern produced by ordinary deterministic nearest rounding, with a fixed-rational version and a dyadic version.

Evidence. Both warning-strict normal and optimized CPython 3.12.14 checks pass 288 cases, 6,876 literal prefixes, 96 small-error cases, and four controls. The checker quantizes the actual matrix entries, multiplies the full gate lists, computes each inverse from its determinant, and checks all prefix, local-gate and endpoint identities. It also confirms that opposite shear pairs cancel under this policy, so an independently perturbed inverse-pair example cannot simply be reused.

Base: canonical main ff3cc58, priority revision 7. Main, the live Discussion/PR snapshot, the exact released question and pinned precision notes were checked. This changes the formal-interface card to a written precision side result. The source's production-caller question, rounded matching-layer audit, and active native work remain distinct.

Limits and next question. Coefficient rounding is the only error in the constructed execution. A compiler can remove these symbolic zero loops before rounding. The lower bound concerns unchanged emitted words, not every possible compilation method. This does not implement data rounding, prove a selected caller uses these words, price state widths or physical movement, or change a supplier/outer bill. A useful next step is to test whether a specific emitted word has exact algebraic coefficient relations that its storage format preserves; such structure could exclude this example. No predecessor scientific replay, selected cold replay, native replay, Lean or Docker build was run.

Credit Nick Petalas's PR5153 for the open deterministic-policy question and the retained sharp-power context, ywz65's PR #2701 for the simultaneous-error theorem, and Vlado Vojdanovski's PR #1673 for the Toeplitz precision interface. Prepared by Ali Romman with substantial OpenAI Codex assistance; Apache-2.0. No independent human or proof-kernel acceptance is claimed.

Save the standalone checker as verify.py; run python3 -I -W error -B verify.py and python3 -I -O -W error -B verify.py. Expected marker: PASS_DETERMINISTIC_CLOSED_WORD.

Standalone exact checker

#!/usr/bin/env python3
# SPDX-License-Identifier: Apache-2.0
"""Check quadratic error under actual nearest coefficient rounding."""
from fractions import Fraction as Q
import json


def need(ok, message):
    if not ok:
        raise ValueError(message)


def mul(a, b):
    return [[sum(x*y for x, y in zip(r, c)) for c in zip(*b)] for r in a]


def norm(a):
    return max(sum(abs(x) for x in r) for r in a)


def inv(a):
    x, y = a[0]; z, w = a[1]
    d = x*w-y*z
    need(d != 0, 'singular gate')
    return [[w/d, -y/d], [-z/d, x/d]]


I = [[Q(1), Q(0)], [Q(0), Q(1)]]
S = [[Q(1, 2), Q(0)], [Q(0), Q(2)]]


def shear(t):
    return [[Q(1), t], [Q(0), Q(1)]]


def nearest(t, h):
    v = t/h + Q(1, 2)
    return h * (v.numerator // v.denominator)


def run():
    cases = prefixes = small = 0
    for q in range(1, 13):
        for m in (1, 2, 5, q):
            for p in (1, 3, 2*q + m.bit_length() + 4):
                for kind in ("dyadic", "thirds"):
                    h = Q(1, 1 << p); s = Q(1 << q)
                    a = 3*h/8 if kind == "dyadic" else Q(1, 3)
                    sign = -1 if kind == "dyadic" else (-1)**(p+1)
                    gates = [S]*q + [shear(a), shear(a), shear(-2*a)]*m + [inv(S)]*q
                    exact = I; changed = I; b = Q(1)
                    for gate in gates:
                        need(norm(gate) <= 2 and norm(inv(gate)) <= 2, 'bounded exact gates')
                        rounded = [[nearest(v, h) for v in row] for row in gate]
                        need(all((v/h) % 1 != Q(1, 2) for row in gate for v in row), 'no rounding ties')
                        need(norm(rounded) <= 2 and norm(inv(rounded)) <= 2, 'bounded rounded gates')
                        need(rounded[0][0]*rounded[1][1]-rounded[0][1]*rounded[1][0] == 1, 'determinant')
                        exact = mul(gate, exact); changed = mul(rounded, changed)
                        b = max(b, norm(exact), norm(inv(exact)))
                        prefixes += 1
                    need(exact == I, 'closed exact word')
                    need(changed == shear(sign*m*h*s*s), 'literal nearest-rounding endpoint')
                    need(b == s*(1+2*a), 'literal prefix/inverse maximum')
                    need(len(gates) == 2*q+3*m, 'gate count')
                    need(norm([[changed[i][j]-I[i][j] for j in range(2)] for i in range(2)]) == m*h*s*s, 'exact error')
                    small += m*h*s*s <= Q(1, 16)
                    cases += 1
    h = Q(1, 8); a = 3*h/8
    need(nearest(a, h) + nearest(a, h) + nearest(-2*a, h) == -h, 'three-shear defect')
    need(nearest(a, h) + nearest(-a, h) == 0, 'opposite pair cancels')
    need(nearest(Q(1, 2), h) == Q(1, 2), 'scales are exact')
    need(mul(shear(a), shear(a)) != I, 'missing closing shear')
    return dict(status='PASS_DETERMINISTIC_CLOSED_WORD', cases=cases,
                literal_prefixes=prefixes, small_error_cases=small, controls=4,
                no_new_kappa=True)


if __name__ == '__main__':
    print(json.dumps(run(), sort_keys=True))

[aliromman]

The proof and standalone checker now have a registered, main-based research package in PR #5308, at 669770ece21ceb5e20d0bec00bd5393d7373ff54. Normal and optimized CPython 3.12.14 package replays passed. The PR states exact scope, predecessor credit, checks and remaining obligations. No kappa or selected-frontier change is claimed. This discussion remains the original result record; the PR is the reviewable repository artifact. No claim is active.