From e605cd6ea888a9a4885473dea88ab8d131dfe489 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Mon, 2 Nov 2026 21:17:38 +0000 Subject: [PATCH] feat(research): prove exact square-zero tensor error --- research/square-zero-tensor-error/PROOF.md | 203 ++++++++++++++++ research/square-zero-tensor-error/README.md | 133 ++++++++++ .../square-zero-tensor-error/SOURCES.json | 30 +++ research/square-zero-tensor-error/TASK.json | 102 ++++++++ .../square-zero-tensor-error/VALIDATION.md | 52 ++++ research/square-zero-tensor-error/VERIFY.json | 34 +++ research/square-zero-tensor-error/verify.py | 229 ++++++++++++++++++ 7 files changed, 783 insertions(+) create mode 100644 research/square-zero-tensor-error/PROOF.md create mode 100644 research/square-zero-tensor-error/README.md create mode 100644 research/square-zero-tensor-error/SOURCES.json create mode 100644 research/square-zero-tensor-error/TASK.json create mode 100644 research/square-zero-tensor-error/VALIDATION.md create mode 100644 research/square-zero-tensor-error/VERIFY.json create mode 100644 research/square-zero-tensor-error/verify.py diff --git a/research/square-zero-tensor-error/PROOF.md b/research/square-zero-tensor-error/PROOF.md new file mode 100644 index 0000000000..625972328f --- /dev/null +++ b/research/square-zero-tensor-error/PROOF.md @@ -0,0 +1,203 @@ +# Exact ordinary tensor error of a square-zero border + +This contribution is produced by Nick Petalas. Apache-2.0. + +## Statement and scope + +All norms below are Euclidean operator norms on finite-dimensional complex +spaces. Let `D` be unitary, let `N^2=0`, and put + +```text +C(e) = D (I + e N), sigma = ||N||, a = |e| sigma. +``` + +For every positive integer `k`, both errors + +```text +||C(e)^(tensor k) - D^(tensor k)||, +||(C(e)^(-T))^(tensor k) - (D^(-T))^(tensor k)|| +``` + +equal `F_k(a)`. Define the `(k+1)` by `(k+1)` real matrix `B_k(a)` by + +```text +B[i,j] = a^(j-i) sqrt(binomial(j,i) binomial(k-i,j-i)) if 0 <= i < j <= k, +B[i,j] = 0 otherwise. +``` + +The exact spectral formula is + +```text +F_k(a) = ||B_k(a)||. +``` + +Thus the error can be determined by a matrix of size `k+1`, independently +of the original dimension or rank of `N`. This is an exact finite spectral +formula, not a radical expression for its largest singular value. The case +`a=0` is zero throughout. + +Write `gamma_k = sqrt(floor((k+1)^2/4))`. For every `a>=0`, + +```text +max(a gamma_k, (1+a/2)^k - 1) <= F_k(a) +F_k(a) <= a gamma_k + ((1+a)^k - 1 - k a) <= (1+a)^k - 1. +``` + +In particular, the sharp first-order coefficient is + +```text +lim_(a -> 0+) F_k(a)/a = gamma_k. +``` + +These are statements about ordinary tensor powers of completed matrices. +They do not identify the repository's chronological supplier product with +such a tensor power. No native invoice or multiplication exponent changes. + +## 1. Reduce an arbitrary square-zero matrix to its largest shear + +Since `im(N)` is contained in `ker(N)`, the orthogonal decomposition +`ker(N) + ker(N)^perp` writes `N` as a single off-diagonal block. Applying +the singular-value decomposition to that block gives mutually orthogonal +two-dimensional blocks + +```text +[[0, sigma_j], [0, 0]], +``` + +and zero blocks. Each `sigma_j` is nonnegative and their maximum is `sigma`. +Unitary diagonal changes remove the phase of `e`. Therefore `I+eN` is +unitarily similar to a direct sum of shears `J(b)=[[1,b],[0,1]]`, with +`0<=b<=a`, and identity blocks. A block with `b=a` is present if `a>0`. + +Its `k`th tensor power is the direct sum of tensor products of these +blocks. After subtracting identity, every such block has nonnegative +entries. Increasing any shear parameter increases entries. For real +nonnegative matrices, entrywise domination implies norm domination: +`|Mv| <= M|v| <= L|v|` when `0<=M<=L`, hence `||M||<=||L||`. +An identity block can be embedded into a two-dimensional zero-parameter +shear. Consequently the maximum is attained by `J(a)^(tensor k)-I`. + +Left multiplication by the unitary `D^(tensor k)` does not change the +forward error. Also + +```text +C(e)^(-T) = D^(-T) (I - e N^T). +``` + +Here `D^(-T)` is unitary, `(N^T)^2=0`, and `||N^T||=sigma`. The same +reduction proves equality of the two orientation errors. The analogous +inverse error has the same value as well, by right unitary multiplication. + +## 2. Reduce the largest shear tensor to its symmetric subspace + +Index the standard basis of `(C^2)^(tensor k)` by subsets of `{1,...,k}`. +For `M=J(a)^(tensor k)-I`, + +```text +M[S,T] = a^(|T|-|S|) if S is a proper subset of T, and 0 otherwise. +``` + +Suppose `a>0`. The empty-set column is zero. On all nonempty columns, +`M^T M` is strictly positive, since their shared empty-set row contributes +`a^(|S|+|T|)>0`. The elementary positive-matrix eigenvector theorem gives a +unique positive unit eigenvector for its largest eigenvalue. Permutations +of the `k` coordinates commute with `M^T M`, so uniqueness makes that +eigenvector permutation invariant. It is constant on each subset level. +Thus the largest right singular vector belongs to the symmetric subspace. + +Use the orthonormal level vectors which have value +`binomial(k,j)^(-1/2)` on subsets of size `j`, and zero elsewhere. For +a fixed size-`i` subset there are `binomial(k-i,j-i)` supersets of size `j`. +The matrix entry from level `j` to level `i sqrt(2) a for a>0. +``` + +The strict inequality matters: the sharp first-order expression is not +an exact nonzero-parameter error formula. + +## 4. A necessary precision budget, with a sufficient choice two bits away + +Let `00`. +Necessarily `|e| sigma gamma_k <= delta`. The explicit sufficient choice + +```text +|e| sigma <= delta/(2k) +``` + +works in both orientations. Indeed, with `x=ka<=delta/2<1`, + +```text +(1+a)^k-1 <= sum_(r>=1) x^r = x/(1-x) <= delta. +``` + +For a dyadic parameter `e=2^(-p)`, `p` a nonnegative integer, this gives + +```text +necessary p >= max(0, ceil(log2(sigma gamma_k/delta))), +sufficient p = max(0, ceil(log2(2k sigma/delta))). +``` + +The sufficient integer is at most two larger than the necessary lower +bound, because `2k/gamma_k<4`. In particular, the required parameter +precision grows as `log2(k)+log2(sigma/delta)+O(1)` when that quantity is +positive. Choosing a fixed nonzero parameter cannot maintain a fixed +error as `k` grows, already by the product-vector lower bound. + +This pays only for endpoint approximation. It does not bound the large +coefficients of a singular scalar wrapper, errors inserted inside paid +calls, intermediate magnitudes, owned restoration, storage, movement or +the cost of producing this parameter. Those are separate obligations in +PR4623's global approximation question. + +## Credit and limits + +Dillon Amburgey's PR4623 poses the global approximation problem and gives +the finite linear-circuit error contract. Its distinction between ordinary +tensor endpoints and chronological supplier substitution is retained here. +Credit Cinna Davis, Jacob Alan Sussman, zxv and the retained native, caller, +compiler and precision lineage. Singular-value decomposition, symmetry on +the Boolean lattice and the positive-matrix eigenvector theorem are +classical. No literature-priority claim is made for those tools. + +The new result is the exact square-zero tensor-error reduction, its sharp +all-k first-order constant and the resulting two-orientation precision +screen. The written proof is universal within these hypotheses; the +verifier supplies separate finite exact corroboration. No human or formal +proof-kernel acceptance, physical supplier or complete multiplication +theorem is claimed. diff --git a/research/square-zero-tensor-error/README.md b/research/square-zero-tensor-error/README.md new file mode 100644 index 0000000000..6c75d40412 --- /dev/null +++ b/research/square-zero-tensor-error/README.md @@ -0,0 +1,133 @@ +# Exact tensor error for square-zero borders + +This contribution is produced by Nick Petalas. Apache-2.0. + +Claim type: scoped proof with exact finite corroboration. No new kappa. + +For a unitary target `D` and relative error `N^2=0`, put +`C(e)=D(I+eN)` and `a=|e| ||N||`. The exact Euclidean error of every +ordinary tensor power, in both forward and inverse-transpose orientations, +is the norm of an explicit matrix of size `k+1`: + +```text +F_k(a) = || B_k(a) || +B[i,j] = a^(j-i) sqrt(binomial(j,i) binomial(k-i,j-i)), i=j + +lim_(a->0+) F_k(a)/a = sqrt(floor((k+1)^2/4)). +``` + +The reduction holds for every finite original dimension and every rank of +`N`. A rational weighted-coordinate version avoids all square roots in the +verifier. For `0= 0, + "tensor domain") + result = [[Q(1)]] + for _ in range(k): + result = kronecker(result, [[Q(1), a], [Q(0), Q(1)]]) + return subtract_identity(result) + + +def subset_error(k, a): + size = 1 << k + return [[a ** (column.bit_count() - row.bit_count()) + if row != column and row & column == row else Q(0) + for column in range(size)] for row in range(size)] + + +def compressed_error(k, a): + """Constant-on-level coordinates, with squared norms binomial(k, i).""" + require(type(k) is int and 1 <= k <= 64 and isinstance(a, Q) and a >= 0, + "compression domain") + return [[comb(k - i, j - i) * a ** (j - i) if i < j else Q(0) + for j in range(k + 1)] for i in range(k + 1)] + + +def weighted_gram(matrix, weights): + size = len(weights) + return [[sum((matrix[h][i] * weights[h] * matrix[h][j] + for h in range(size)), Q(0)) / weights[i] + for j in range(size)] for i in range(size)] + + +def action(matrix, vector): + return [sum((x * y for x, y in zip(row, vector, strict=True)), Q(0)) + for row in matrix] + + +def check_compression(full, compressed, k): + size = len(full) + weights = [comb(k, i) for i in range(k + 1)] + gram = weighted_gram(compressed, weights) + backward = transpose(full) + checked = 0 + for level in range(k + 1): + vector = [Q(column.bit_count() == level) for column in range(size)] + image = action(full, vector) + require(image == [compressed[row.bit_count()][level] + for row in range(size)], "compressed endpoint") + image = action(backward, image) + require(image == [gram[row.bit_count()][level] + for row in range(size)], "compressed Gram") + checked += 2 * size + return checked + + +def exact_endpoints(): + entries, compressed_entries, orientation_entries = 0, 0, 0 + for k in range(1, 7): + for a in (Q(1, 3), Q(1, 2), Q(1), Q(2)): + full = tensor_error(k, a) + require(full == subset_error(k, a), "literal tensor versus subsets") + entries += len(full) ** 2 + compressed_entries += check_compression(full, compressed_error(k, a), k) + # Inverse transpose has the same singular norm by parity conjugation. + signed = [[(-1) ** (i.bit_count() + j.bit_count()) * full[j][i] + for j in range(len(full))] for i in range(len(full))] + inverse = [[Q(1)]] + for _ in range(k): + inverse = kronecker(inverse, [[Q(1), Q(0)], [-a, Q(1)]]) + require(subtract_identity(inverse) == signed, "inverse transpose sign") + orientation_entries += len(full) ** 2 + return entries, compressed_entries, orientation_entries + + +def first_order_and_precision(): + incidence_cases, precision_cases = 0, 0 + for k in range(1, 65): + gamma_squared = max(j * (k - j + 1) for j in range(1, k + 1)) + require(gamma_squared == ((k + 1) ** 2) // 4, "sharp first-order coefficient") + incidence_cases += k + for delta in (Q(1), Q(1, 2), Q(1, 16)): + a = delta / (2 * k) + upper = (1 + a) ** k - 1 + require(upper <= delta, "sufficient parameter choice") + require(4 * k * k <= 16 * gamma_squared, "two-bit precision gap") + precision_cases += 1 + # Fixed epsilon cannot provide a dimension-independent small tensor error. + require((1 + Q(1, 32)) ** 64 - 1 > 1, "fixed-parameter error growth") + return incidence_cases, precision_cases + + +def mixed_square_zero(): + """A rank-two error mixed by an exact rational orthogonal matrix.""" + half = Q(1, 2) + rotation = [[half * x for x in row] for row in + ((1, 1, 1, 1), (1, -1, 1, -1), + (1, 1, -1, -1), (1, -1, -1, 1))] + require(multiply(rotation, transpose(rotation)) == identity(4), "orthogonal fixture") + raw = [[Q(0), Q(2), Q(0), Q(0)], [Q(0)] * 4, + [Q(0), Q(0), Q(0), Q(1)], [Q(0)] * 4] + mixed = multiply(multiply(rotation, raw), transpose(rotation)) + require(multiply(mixed, mixed) == [[Q(0)] * 4 for _ in range(4)], "square zero") + eps = Q(1, 4) + positive = [[Q(i == j) + eps * mixed[i][j] for j in range(4)] for i in range(4)] + negative = [[Q(i == j) - eps * mixed[i][j] for j in range(4)] for i in range(4)] + require(multiply(positive, negative) == identity(4), "inverse endpoint") + require(multiply(negative, positive) == identity(4), "reverse inverse endpoint") + tensor_rotation = kronecker(rotation, rotation) + raw_endpoint = [[Q(i == j) + eps * raw[i][j] for j in range(4)] for i in range(4)] + transformed = multiply(multiply(tensor_rotation, kronecker(raw_endpoint, raw_endpoint)), + transpose(tensor_rotation)) + require(transformed == kronecker(positive, positive), "mixed tensor similarity") + return 256 + + +def rejection_controls(): + rejected = 0 + wrong = compressed_error(2, Q(1, 2)) + wrong[0][1] = Q(1, 2) + try: + check_compression(tensor_error(2, Q(1, 2)), wrong, 2) + except ValueError: + rejected += 1 + require(tensor_error(1, Q(1, 2)) != [[Q(1), Q(1, 2)], [Q(0), Q(1)]], + "missing identity subtraction control") + rejected += 1 + for k, a in ((0, Q(1)), (True, Q(1)), (9, Q(1)), (1, Q(-1)), (1, 0.5)): + try: + tensor_error(k, a) + except ValueError: + rejected += 1 + # For k=2 and a>0, linearization is strictly smaller than the exact norm. + # det(B*B - 2a^2 I) on its two-dimensional active input block is -2a^6. + for a in (Q(1, 3), Q(1, 2), Q(1), Q(2)): + gram = weighted_gram(compressed_error(2, a), [1, 2, 1]) + determinant = ((gram[1][1] - 2 * a * a) * (gram[2][2] - 2 * a * a) + - gram[1][2] * gram[2][1]) + require(determinant == -2 * a ** 6 < 0, "false exact linear-error control") + rejected += 1 + require(rejected == 11, "rejection count") + return rejected + + +def write_receipt(path, result): + package = Path(__file__).resolve().parent + checkout = package.parents[1] + require(not path.resolve().is_relative_to(checkout), "receipt must be outside checkout") + names = ("PROOF.md", "README.md", "SOURCES.json", "TASK.json", + "VALIDATION.md", "VERIFY.json", "verify.py") + hashes = {name: hashlib.sha256((package / name).read_bytes()).hexdigest() + for name in names} + receipt = {"result": result, "package_sha256": hashes} + with path.open("x", encoding="utf-8") as stream: + stream.write(json.dumps(receipt, indent=2, sort_keys=True) + "\n") + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--receipt", type=Path) + args = parser.parse_args() + entries, compressed_entries, orientation_entries = exact_endpoints() + incidence_cases, precision_cases = first_order_and_precision() + result = { + "status": "PASS_SQUARE_ZERO_TENSOR_ERROR", + "literal_entries": entries, + "compressed_action_entries": compressed_entries, + "inverse_transpose_entries": orientation_entries, + "first_order_level_cases": incidence_cases, + "precision_cases": precision_cases, + "mixed_rank_two_entries": mixed_square_zero(), + "rejection_controls": rejection_controls(), + "claim_type": "scoped proof with exact finite corroboration", + "no_new_kappa": True, + } + if args.receipt is not None: + write_receipt(args.receipt, result) + print(json.dumps(result, sort_keys=True)) + + +if __name__ == "__main__": + main()