From 64f90d7a7ca010c8c3bf77ca9b3663ee5e957055 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Tue, 3 Nov 2026 10:06:54 +0000 Subject: [PATCH] feat(research): balance native coarse-grid prefix errors --- .../ORIGIN.json | 9 + .../PROOF.md | 151 ++++++++++++ .../README.md | 115 +++++++++ .../SOURCES.json | 18 ++ .../TASK.json | 79 ++++++ .../VERIFY.json | 32 +++ .../inputs/PR6540-PROOF.md | 233 ++++++++++++++++++ .../model.py | 147 +++++++++++ .../verify.py | 179 ++++++++++++++ 9 files changed, 963 insertions(+) create mode 100644 research/native-prefix-balanced-coarsening/ORIGIN.json create mode 100644 research/native-prefix-balanced-coarsening/PROOF.md create mode 100644 research/native-prefix-balanced-coarsening/README.md create mode 100644 research/native-prefix-balanced-coarsening/SOURCES.json create mode 100644 research/native-prefix-balanced-coarsening/TASK.json create mode 100644 research/native-prefix-balanced-coarsening/VERIFY.json create mode 100644 research/native-prefix-balanced-coarsening/inputs/PR6540-PROOF.md create mode 100644 research/native-prefix-balanced-coarsening/model.py create mode 100644 research/native-prefix-balanced-coarsening/verify.py diff --git a/research/native-prefix-balanced-coarsening/ORIGIN.json b/research/native-prefix-balanced-coarsening/ORIGIN.json new file mode 100644 index 0000000000..872659df7e --- /dev/null +++ b/research/native-prefix-balanced-coarsening/ORIGIN.json @@ -0,0 +1,9 @@ +{ + "author": "Ali Romman", + "url": "https://github.com/aliromman/integer-mult-bounds/blob/5f7c893b6af9a75cb19ad22c6db06ed22eea6f54/research/native-coarse-grid-residue-codec/PROOF.md", + "pr": 6540, + "head": "5f7c893b6af9a75cb19ad22c6db06ed22eea6f54", + "path": "research/native-coarse-grid-residue-codec/PROOF.md", + "sha256": "2322e9b613004aa4278ba6cdefea2bf68df01fcd5eb502208928539b36dfa1c7", + "usage": "Cited Gaussian quotient and native-grid premises; no predecessor executable is invoked." +} diff --git a/research/native-prefix-balanced-coarsening/PROOF.md b/research/native-prefix-balanced-coarsening/PROOF.md new file mode 100644 index 0000000000..0aa0cff95c --- /dev/null +++ b/research/native-prefix-balanced-coarsening/PROOF.md @@ -0,0 +1,151 @@ +# Prefix-balanced native coarsening + +This is a scoped mathematical proof of a changed numerical interface. The new +step is the compatibility of cumulative stochastic rounding with the native +coarse-period codec, including simultaneous optimal prefix variances and the +extra scan cost. It is not a complete multiplication theorem. + +## Premises and credit + +Use Ali Romman's [PR6540](https://github.com/CrocSwap/integer-mult-bounds/pull/6540) +at `5f7c893b6af9a75cb19ad22c6db06ed22eea6f54` for the Gaussian operator and +quotient premises below. Its exact proof is retained in +[inputs/PR6540-PROOF.md](inputs/PR6540-PROOF.md), with origin and hash in +[ORIGIN.json](ORIGIN.json). Its scientific executable is not invoked. Gaussian +Smith coordinates and the earlier native/compiler lineage keep their credit. + +Cumulative rounding is classical. Knuth's +[two-way rounding](https://arxiv.org/abs/math/9504228) and Doerr, Friedrich, +Klein and Osbild's [unbiased matrix rounding](https://arxiv.org/abs/cs/0604068) +give broader controlled-rounding context. Neither cumulative rounding nor the +scalar unbiased-variance inequality is claimed as new here. + +Let A=L C_r R be the predecessor's Gaussian-unit monomial native recipe at +tensor width f>=1. Write N=512^f, a=r*f, d=ceil(a/2), m=2^k, k>=d and +D=2^(k+d). Its central pair is + +```text +C = [[1+i,1-i],[1-i,1+i]]/2. +``` + +For every x in Z[i]^N the vector n=2^d A x is integral Gaussian, and +B=m A^-1 is integral Gaussian. The lattice quotient Z[i]^N / B Z[i]^N +has exactly 2^(2kN) elements. The predecessor supplies a label ell(x) with +2kN bits and a representative x0(ell), with x-x0 in B Z[i]^N. These are cited +premises, not new quotient or source-admission claims. + +Fix an order of the 2N real components after applying A. The input and order +are fixed before drawing a fresh uniform u in {0,...,D-1}, conditionally on +the entire incoming state and history. Physical values use input unit h/m +and output unit h, for h>0. No initial component of x is assumed zero. + +## The new quantizer + +Flatten n into n_1,...,n_t, t=2N. Set S_j=sum_(i<=j) n_i, S_0=0, and + +```text +q_j = floor((S_j+u)/D) - floor((S_(j-1)+u)/D). +``` + +Equivalently, keep c_0=u and compute + +```text +(q_j,c_j) = divmod(n_j+c_(j-1),D), 0 <= c_j < D. +``` + +The invariant D*sum_(i<=j) q_i+c_j=S_j+u proves the equivalence even for +negative inputs. For a fixed j, c_(j-1)=(S_(j-1)+u) mod D is uniform on the +D residues. Consequently q_j is an adjacent-integer unbiased rounding of +n_j/D. Every individual coordinate retains the predecessor's pointwise +minimum mean squared error. In particular the total Euclidean mean squared +error remains at most N*h^2/2. + +More strongly, each prefix sum is exactly floor((S_j+u)/D). If +t_j=S_j mod D, then + +```text +E[h*sum_(i<=j) q_i | x] = h*S_j/D, +Var[h*sum_(i<=j) q_i | x] = h^2*t_j*(D-t_j)/D^2 <= h^2/4. +``` + +Its absolute error is less than h for every seed, and it is exact whenever +S_j/D is integral. All these statements hold simultaneously for every prefix +in the fixed order. For any integer-valued unbiased output with mean b+p, +0<=p<1, the inequality (Z-b)*(Z-b-1)>=0 gives Var(Z)>=p*(1-p). +Thus each displayed prefix variance is the least possible among all unbiased +grid-valued vector outputs, without any reversibility assumption. + +## Translation and the exact inverse + +For any integer real vector z, replacing n by n+D*z increases q_j by z_j +and leaves every carry unchanged. In Gaussian coordinates this proves + +```text +Q_u(x+B*z) = Q_u(x)+z. +``` + +Use exactly the cited label ell. Encode x as (Q_u(x),ell(x)). Given any +coarse q and label ell, compute + +```text +x0 = x0(ell), +z = q-Q_u(x0), +x = x0+B*z. +``` + +Translation gives Q_u(x)=q, and addition of B*z preserves ell. Conversely, +an original x differs from its representative by a unique B*z, and this +formula recovers it. Hence this is a two-sided bijection for each retained +seed. It changes neither the 2kN-bit label nor the k+d-bit uniform seed. +The predecessor's full-grid capacity and fixed-fair-bit lower bounds apply +to the same input domain and means. No better capacity bound is claimed. + +The finite reference instantiates the canonical C axes and their Gaussian +Smith coordinates. The written translation proof applies also to the cited +L,R phases/permutations and arbitrary tensor widths. The finite program's +size/payload guards are not an all-width physical implementation. + +## A strict native improvement and sharpness + +For the canonical unphased native operator at N=512, r=8, k=5, take every +Gaussian input component equal to 16+16i. C and all its tensor powers fix +constant vectors, so all 1024 real output means are 1/2. The predecessor's +common-coordinate threshold makes the entire sum either 0 or 1024 with equal +probability. Its error variance is 512^2*h^2=262144*h^2. + +The new total is identically 512, so its error variance is zero on this same +input. Both constructions have the same coordinate marginals, 5120-bit +residue capacity and nine-bit seed. This is a comparison for this fixed +reader and input, not a new Euclidean-error optimum or caller kappa. + +The new uniform quarter-variance bound is sharp for this native family. +Take x_0=16 and every other Gaussian input zero. Column sums of C and its +tensor powers are one, so the full real-component sum has ideal value 1/2. +Its rounded sum is an unbiased Bernoulli output and has variance h^2/4. + +## Complete cost change and remaining obligations + +Keep the predecessor's native evaluations, Gaussian quotient transforms, +digit extraction/reconstruction, routing and retained-label costs. Each of +the two quantizer passes in an encode/decode round trip visits 2N real +coordinates. Each visit still adds one offset and takes a floor quotient, +and now also computes its remainder modulo D. The added work is exactly +4N remainder extractions, plus two carry initializations from the retained +seed. The carry has k+d bits and can be reused between the sequential passes. +It introduces a serial dependence along the chosen output order. + +Because D is a power of two, a remainder is the low k+d bits, including for +negative integers under floor division. The carry never grows with N. If a +numerator has magnitude below 2^W, adding c=1, put +N=512^f, a=r*f, d=ceil(a/2), and use the tensor L,R with a active C axes. +Below, A denotes this complete tensor operator. Choose integer k>=d and m=2^k. +Input x is any vector in Z[i]^N, stored in units h/m for h>0. Output q is in +Z[i]^N, stored in units h. One fresh uniform integer u in [0,2^(k+d)) serves +every real and imaginary coordinate of the call. The seed stays unchanged. + +The selected PR6030 word has 3453 MOVE events, 2886 distinct directed frame +edges, and 1001 frames used by those edges. All endpoint frame checks pass. +An independent 18-bit matrix inverse/composition and finite-span pass agrees +with every B block and the complete rank census. +The rank census is 2219,457,496,100,163,11,6,1 for ranks 1 through 8. The +unchanged Clifford compiler and separate coordinate oracle agree on all 512 +columns of the first event of each rank. The new interpreter also checks all +4096 columns. It does not instantiate every one of the 2886 edge recipes. +The universal argument applies to any supplied L C_r R recipe in this class. + +Source pins are in SOURCES.json. The selected word and the retained native +implementations are unchanged. The native/global compiler and all-size supplier +premises are not discharged by these representative checks. + +## One common seed gives the minimum unbiased mean squared error + +Each entry of C^tensor a has an integer Gaussian numerator over 2^d. Products +of a factors 1+i or 1-i are divisible by 2^floor(a/2). Gaussian monomials +preserve this property. Thus n=2^d A x is an integer Gaussian vector. +Set D=2^(k+d), and round each real component by + +```text +q_j = floor((n_j+u)/D). +``` + +Write n_j=D*b_j+t_j with 0<=t_j=0 gives Var(Z)>=t*(D-t)/D^2. Summing over real coordinates +proves that this quantizer attains the least possible mean squared error among +ALL unbiased grid-valued outputs at each input. Reversibility is not required +for this lower bound. Some outcomes are the farther adjacent integer; no +minimum deterministic-error claim is made. + +A unit input column has a real or imaginary numerator equal to +1 or -1 after +the common reduction to denominator 2^d. Gaussian monomials preserve that +property. Its required mean is +1/D or -1/D. An integer-valued sampler using +a fixed b fair bits has a mean equal to an integer divided by 2^b. It needs +b>=k+d, even without the minimum-error condition. The common seed attains this +minimum fixed fair-bit count. This is not a minimum entropy or expected variable-length +sampling theorem. Reuse of the same seed in a later adaptive call is not +authorized by the conditional proof. The inverse uses the retained seed for +exact decoding; it is not a new stochastic call. + +## The coarse-period lattice and its explicit Gaussian digits + +Because k>=d, B=m*A^-1 is integral over Z[i]. The quantizer Q_u satisfies + +```text +Q_u(x+B*z) = Q_u(x)+z for every z in Z[i]^N. +``` + +Put pi=1+i and H=[[1,i],[i,1]]. Then C^-1=pi^-1 H. The integral unimodular +matrices U=[[1,0],[-i,1]] and V=[[1,-i],[0,1]] satisfy U H V=diag(1,2). +Tensor them over the a active axes. The source R maps the period lattice +B Z[i]^N to m*C^(-tensor a) Z[i]^N, since L^-1 preserves Z[i]^N. Applying U +maps it to a diagonal Gaussian lattice with coordinate ideals + +```text +(pi^e_j), e_j = 2*k-a+2*weight(active bits of address j). +``` + +Indeed m*pi^-a*2^weight is a Gaussian unit times pi^e_j. Every e_j is +nonnegative. Their sum is 2*k*N because each active address bit is one at +exactly half the coordinates. Thus + +```text +Z[i]^N / B Z[i]^N is isomorphic to product_j Z[i]/(pi^e_j), +number of cosets = 2^(2*k*N). +``` + +These Gaussian Smith methods are prior work, including +[PR5815](https://github.com/CrocSwap/integer-mult-bounds/pull/5815), its +[executed form](https://github.com/CrocSwap/integer-mult-bounds/pull/5821), and +the distinct modular-overwrite capacity in +[PR5880](https://github.com/CrocSwap/integer-mult-bounds/pull/5880). +The new use here is the quantizer's coarse-period quotient, its exact codec, +the minimum unbiased law and the actual selected native bindings. + +Each Gaussian remainder has exactly e_j binary pi-adic digits. For z=A+iB, +take digit b=(A+B) mod 2, subtract b and divide by pi. The quotient is +((A-b+B)/2)+i*((B-A+b)/2), with exact integer halves. Repeat e_j times. +The e_j bits give one representative of every coset modulo pi^e_j. Reverse +Horner evaluation with pi reconstructs the representative. The implementation +packs all digits into exactly 2*k*N bits; byte containers use ceiling(bits/8) +bytes with required zero padding. At N=512^f there is no padding. + +## Exact two-sided codec and sharp retained information + +Encode x by taking the digits of U R x and returning (Q_u(x),digits). Decode +the digits to a representative x0 by applying U^-1 and R^-1. Then set + +```text +z = q-Q_u(x0), +x = x0+B*z. +``` + +The translation identity proves Q_u(x)=q. The added B*z leaves the digits +unchanged. Conversely, any original x differs from its representative by a +unique B*z, so this formula recovers it exactly. For every fixed u, this is +a bijection between the fine-grid integer input representation and all pairs +(coarse integer output, 2*k*N-bit residue label). Every coarse output has +exactly 2^(2*k*N) fine-grid preimages. + +An injective implementation that retains the seed and coarse output therefore +needs at least 2*k*N bits of additional information. An arbitrary finite dirty +bank with Q possible initial values cannot reduce this bound: the preimage +slice has 2^(2*k*N)*Q states and the output side has at most 2^b*Q states. +The codec attains b=2*k*N. This is a retained-label capacity result on the +advertised full input lattice. It is NOT an initially clean hardware-register +minimum, a full-state permutation on identical finite registers, or a lower +bound on correlated inputs reached by the complete selected caller. + +The label cannot be erased from q and u alone. The inverse needs it. Any +physical uncompute, reuse, ownership or erasure schedule must still be paid. +The mathematical conversion between two representations does not silently +provide such a circuit. + +## Selected grid interface and its boundary + +At f=1 every selected MOVE rank is at most 8. Thus k=5 is sufficient. A call +accepts the h/32 grid and returns the h grid, matching the grid ratio in +[PR6499](https://github.com/CrocSwap/integer-mult-bounds/pull/6499) and +[PR6506](https://github.com/CrocSwap/integer-mult-bounds/pull/6506). Each full-grid +codec retains 5120 bits. Its seed has 5+ceil(r/2) bits, hence 6 through 9 for +the selected ranks. Allocating one such residue slot for each of the 3453 +MOVE events uses 17,679,360 bits; separate fresh seeds use 21,683 bits. +These are uncompressed slot counts for that proposed interface, not joint +entropy lower bounds or a complete multiplication invoice. + +This is only a grid match. The stochastic error contract is new; the scalar +predecessors' completed error budgets are not imported as proved consequences. +Whole-word restoration and caller probability bounds remain open. At tensor +width f, k>=ceil(r*f/2) is required for the stated integral-period codec. +Fixed k=5 does not cover all widths. For the rank-eight class, k>=4*f is +required. A larger fine grid can represent the scalar inputs but has a larger +full-grid residue code; its cost must not be omitted. + +The condition is exact for integral inclusion m*A^-1 Z[i]^N subset Z[i]^N: +a unit column has a primitive component over 2^d. If k=1, a sufficient signed +temporary width is W=w+4*a+2*k+12. One raw native stage enlarges a component +by at most four. A triangular stage enlarges it by at most two. A pi^e digit +representative has magnitude below 3*2^(e/2), and e<=2*k+a. These bounds give +an x0 component bound 2^(k+ceil(a/2)+a+2); the coarse q0, direct inverse and +final scale fit W. The width is sufficient, not optimal. Addresses need +O(f+log(k+1)) bits. The displayed algorithm thus uses +O((a+k+f)*N*(w+a+k+f)) indexed bit work and O(N*(w+a+k)) data storage, plus +the 2*k*N retained bits. At most six live Gaussian fields are needed during +decoding, including its coarse input, with separate precision/route tables. + +This ordinary integer reference does not provide a reversible gate circuit, +fixed multitape routing, physical clean storage, sampler access, entropy +recovery, an accelerated recursive tariff or a complete caller. It does not +imply additivity, native-graph flatness or dirty compensation after intervening +arithmetic. All five selected assumptions and the frontier remain unchanged. + +## Verification scope + +The finite checks enumerate 25,184 complete quotient endpoints and 16 retained- +bit collisions, compare 36 small tensors to a separate dense coefficient oracle, +and run 432 small seed round trips. The source checks include 4096 columns in +each of two interpreters, 128 signed source round trips, 64 arbitrary coarse/ +residue endpoints and exact means/variances for all 1920 relevant seeds. +A full 262,144-coordinate tensor uses a 524,288-bit label and all four seeds; +its exact mean squared error is 326311/4, below N/2. Eleven semantic/domain +controls and three source corruption controls are retained. These finite checks +corroborate the all-size proof. Independent human and proof-kernel acceptance, +all selected native instances and a complete selected cold replay are unrun. diff --git a/research/native-prefix-balanced-coarsening/model.py b/research/native-prefix-balanced-coarsening/model.py new file mode 100644 index 0000000000..eed203e381 --- /dev/null +++ b/research/native-prefix-balanced-coarsening/model.py @@ -0,0 +1,147 @@ +"""Finite exact reference for the prefix-balanced native codec. + +The rounding and codec substitution are the contribution. Gaussian Smith +coordinates are the cited PR6540 premise, instantiated for canonical C axes. +""" + +from dataclasses import dataclass + +Gaussian = tuple[int, int] + + +def require(condition: bool, message: str) -> None: + if not condition: + raise ValueError(message) + + +def balanced(numerators: tuple[int, ...], denominator: int, seed: int) -> tuple[int, ...]: + require(1 <= len(numerators) <= 1024, "coordinate limit") + require(1 <= denominator <= 1 << 24, "denominator limit") + require(0 <= seed < denominator, "seed range") + require(all(type(value) is int and value.bit_length() <= 8192 for value in numerators), + "numerator payload limit") + carry = seed + output = [] + for value in numerators: + quotient, carry = divmod(value + carry, denominator) + require(0 <= carry < denominator, "carry invariant") + output.append(quotient) + return tuple(output) + + +def flatten(values: tuple[Gaussian, ...]) -> tuple[int, ...]: + return tuple(component for value in values for component in value) + + +def gaussian(values: tuple[int, ...]) -> tuple[Gaussian, ...]: + require(len(values) % 2 == 0, "Gaussian component count") + return tuple((values[j], values[j + 1]) for j in range(0, len(values), 2)) + + +@dataclass(frozen=True) +class Native: + size: int + active: int + precision: int + + def __post_init__(self) -> None: + require(2 <= self.size <= 512 and self.size.bit_count() == 1, "size limit") + require(0 <= self.active <= 8 and self.active < self.size.bit_length(), "active-axis range") + require((self.active + 1) // 2 <= self.precision <= 16, "precision range") + + @property + def scale(self) -> int: + return 1 << ((self.active + 1) // 2) + + @property + def denominator(self) -> int: + return (1 << self.precision) * self.scale + + @property + def label_bits(self) -> int: + return 2 * self.precision * self.size + + def check(self, values: tuple[Gaussian, ...]) -> None: + require(len(values) == self.size, "field size") + require(all(type(v) is int and v.bit_length() <= 4096 for z in values for v in z), + "integer payload limit") + + def numerators(self, values: tuple[Gaussian, ...], inverse: bool = False) -> tuple[Gaussian, ...]: + self.check(values) + work = list(values) + for axis in range(self.active): + bit = 1 << axis + for j in range(self.size): + if j & bit: + continue + p, q = work[j] + r, s = work[j | bit] + first = (p - q + r + s, p + q - r + s) + second = (p + q + r - s, -p + q + r + s) + work[j], work[j | bit] = (second, first) if inverse else (first, second) + divisor = 1 << (self.active // 2) + require(all(v % divisor == 0 for z in work for v in z), "native denominator") + return tuple((p // divisor, q // divisor) for p, q in work) + + def period(self, values: tuple[Gaussian, ...]) -> tuple[Gaussian, ...]: + factor = (1 << self.precision) // self.scale + return tuple((factor * p, factor * q) for p, q in self.numerators(values, True)) + + def triangular(self, values: tuple[Gaussian, ...], inverse: bool = False) -> tuple[Gaussian, ...]: + self.check(values) + work = list(values) + axes = range(self.active - 1, -1, -1) if inverse else range(self.active) + sign = 1 if inverse else -1 + for axis in axes: + bit = 1 << axis + for j in range(self.size): + if j & bit: + continue + p, q = work[j] + r, s = work[j | bit] + work[j | bit] = (r - sign * q, s + sign * p) + return tuple(work) + + def exponents(self) -> tuple[int, ...]: + mask = (1 << self.active) - 1 + return tuple(2 * self.precision - self.active + 2 * (j & mask).bit_count() + for j in range(self.size)) + + def label(self, values: tuple[Gaussian, ...]) -> int: + label = 0 + offset = 0 + for (p, q), width in zip(self.triangular(values), self.exponents(), strict=True): + for _ in range(width): + digit = (p + q) % 2 + label |= digit << offset + p, q = (p - digit + q) // 2, (q - p + digit) // 2 + offset += 1 + require(offset == self.label_bits, "label capacity") + return label + + def representative(self, label: int) -> tuple[Gaussian, ...]: + require(type(label) is int and 0 <= label < 1 << self.label_bits, "label range") + values = [] + offset = 0 + for width in self.exponents(): + p, q = 0, 0 + for bit in range(width - 1, -1, -1): + digit = (label >> (offset + bit)) & 1 + p, q = p - q + digit, p + q + values.append((p, q)) + offset += width + return self.triangular(tuple(values), True) + + def quantize(self, values: tuple[Gaussian, ...], seed: int) -> tuple[Gaussian, ...]: + return gaussian(balanced(flatten(self.numerators(values)), self.denominator, seed)) + + def encode(self, values: tuple[Gaussian, ...], seed: int) -> tuple[tuple[Gaussian, ...], int]: + return self.quantize(values, seed), self.label(values) + + def decode(self, coarse: tuple[Gaussian, ...], label: int, seed: int) -> tuple[Gaussian, ...]: + self.check(coarse) + representative = self.representative(label) + rounded = self.quantize(representative, seed) + difference = tuple((p - r, q - s) for (p, q), (r, s) in zip(coarse, rounded, strict=True)) + correction = self.period(difference) + return tuple((p + r, q + s) for (p, q), (r, s) in zip(representative, correction, strict=True)) diff --git a/research/native-prefix-balanced-coarsening/verify.py b/research/native-prefix-balanced-coarsening/verify.py new file mode 100644 index 0000000000..7e5c2f08bd --- /dev/null +++ b/research/native-prefix-balanced-coarsening/verify.py @@ -0,0 +1,179 @@ +"""Check the new rounded interface, exact inverse, and rejection controls.""" + +import argparse +import hashlib +import itertools +import json +from pathlib import Path + +from model import Native, balanced, flatten, require + +PACKAGE = Path(__file__).resolve().parent + + +def moments(numerators: tuple[int, ...], denominator: int) -> int: + first = [0] * len(numerators) + second = [0] * len(numerators) + prefix_first = [0] * len(numerators) + prefix_second = [0] * len(numerators) + for seed in range(denominator): + output = balanced(numerators, denominator, seed) + exact_sum = 0 + rounded_sum = 0 + for j, (value, rounded) in enumerate(zip(numerators, output, strict=True)): + exact_sum += value + rounded_sum += rounded + error = denominator * rounded - value + prefix_error = denominator * rounded_sum - exact_sum + first[j] += error + second[j] += error * error + prefix_first[j] += prefix_error + prefix_second[j] += prefix_error * prefix_error + require(abs(error) < denominator, "coordinate nearest neighbors") + require(abs(prefix_error) < denominator, "prefix nearest neighbors") + require(rounded_sum == (exact_sum + seed) // denominator, "dense prefix oracle") + exact_sum = 0 + for j, value in enumerate(numerators): + exact_sum += value + residue = value % denominator + prefix_residue = exact_sum % denominator + require(first[j] == prefix_first[j] == 0, "exact unbiasedness") + require(second[j] == denominator * residue * (denominator - residue), "coordinate optimum") + require(prefix_second[j] == denominator * prefix_residue * (denominator - prefix_residue), + "prefix optimum") + return denominator + + +def exhaustive_rounding() -> dict[str, int]: + fixtures = 0 + seeds = 0 + translations = 0 + for denominator in (2, 4, 8): + for length in range(1, 5): + for residues in itertools.product(range(denominator), repeat=length): + offsets = tuple((-1 if j % 2 else 1) * (j + 1) for j in range(length)) + signed = tuple(r + denominator * z for r, z in zip(residues, offsets, strict=True)) + seeds += moments(signed, denominator) + fixtures += 1 + for seed in (0, denominator - 1): + old = balanced(residues, denominator, seed) + new = balanced(signed, denominator, seed) + require(new == tuple(q + z for q, z in zip(old, offsets, strict=True)), "translation") + translations += 1 + return dict(fixtures=fixtures, seed_vectors=seeds, translations=translations) + + +def quotient_endpoints() -> int: + endpoints = 0 + for size, active, precision in ((2, 1, 1), (4, 2, 1)): + native = Native(size, active, precision) + coarse_fields = ( + tuple((0, 0) for _ in range(size)), + tuple((j - 3, 2 - j) for j in range(size)), + tuple((7 - j, -5 - j) for j in range(size)), + ) + for label in range(1 << native.label_bits): + for seed in range(native.denominator): + for coarse in coarse_fields: + fine = native.decode(coarse, label, seed) + require(native.encode(fine, seed) == (coarse, label), "two-sided endpoint") + endpoints += 1 + return endpoints + + +def native_fields() -> dict[str, int]: + seeds = 0 + roundtrips = 0 + for active in range(1, 9): + native = Native(512, active, 5) + values = tuple(((17 * j + 3) % 23 - 11, (19 * j + 5) % 29 - 14) for j in range(512)) + seeds += moments(flatten(native.numerators(values)), native.denominator) + for seed in (0, native.denominator // 2, native.denominator - 1): + coarse, label = native.encode(values, seed) + require(native.decode(coarse, label, seed) == values, "native fine roundtrip") + arbitrary = tuple((p + j % 3 - 1, q - j % 5 + 2) + for j, (p, q) in enumerate(coarse)) + fine = native.decode(arbitrary, label, seed) + require(native.encode(fine, seed) == (arbitrary, label), "native coarse roundtrip") + roundtrips += 2 + return dict(ranks=8, complete_seed_vectors=seeds, two_sided_roundtrips=roundtrips) + + +def improvement() -> dict[str, int]: + native = Native(512, 8, 5) + half_field = tuple((16, 16) for _ in range(512)) + numerators = flatten(native.numerators(half_field)) + require(set(numerators) == {native.denominator // 2}, "reachable half-grid input") + common_square_sum = 0 + balanced_square_sum = 0 + for seed in range(native.denominator): + common = tuple((n + seed) // native.denominator for n in numerators) + new = balanced(numerators, native.denominator, seed) + common_square_sum += (sum(common) - 512) ** 2 + balanced_square_sum += (sum(new) - 512) ** 2 + require(common_square_sum == native.denominator * 512**2, "old reader variance") + require(balanced_square_sum == 0, "exact new reader") + sharp = tuple((16, 0) if j == 0 else (0, 0) for j in range(512)) + sharp_n = flatten(native.numerators(sharp)) + require(sum(sharp_n) * 2 == native.denominator, "sharp total mean") + square = sum((2 * sum(balanced(sharp_n, native.denominator, seed)) - 1) ** 2 + for seed in range(native.denominator)) + require(square == native.denominator, "sharp quarter variance") + return dict(common_variance=512**2, balanced_variance=0, sharp_bound_numerator=1, + sharp_bound_denominator=4, coordinates=1024, retained_bits=native.label_bits, + fair_seed_bits=native.denominator.bit_length() - 1) + + +def controls() -> int: + rejected = 0 + for numerators, denominator, seed in (((1,), 0, 0), ((1,), 2, -1), ((1,), 2, 2), ((), 2, 0)): + try: + balanced(numerators, denominator, seed) + except ValueError: + rejected += 1 + for args in ((3, 1, 1), (2, 2, 1), (2, 1, 0)): + try: + Native(*args) + except ValueError: + rejected += 1 + native = Native(2, 1, 1) + for label in (-1, 1 << native.label_bits): + try: + native.representative(label) + except ValueError: + rejected += 1 + require(rejected == 9, "domain rejection count") + require(sum((n + 0) // 2 for n in (1, 1)) != sum(balanced((1, 1), 2, 0)), + "reset-carry mutant rejected") + require(balanced((1, 0), 2, 0) != balanced((1, 0), 2, 1), "missing-seed mutant rejected") + zero = ((0, 0), (0, 0)) + first = native.decode(zero, 0, 0) + second = native.decode(zero, 1, 0) + require(first != second and native.quantize(first, 0) == native.quantize(second, 0), + "missing-residue collision") + return rejected + 3 + + +def main() -> None: + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--receipt", type=Path) + arguments = parser.parse_args() + origin = json.loads((PACKAGE / "ORIGIN.json").read_text()) + source = PACKAGE / "inputs" / "PR6540-PROOF.md" + require(hashlib.sha256(source.read_bytes()).hexdigest() == origin["sha256"], "source provenance") + result = dict(rounding=exhaustive_rounding(), quotient_endpoints=quotient_endpoints(), + native=native_fields(), improvement=improvement(), controls=controls()) + result["package_sha256"] = { + path.relative_to(PACKAGE).as_posix(): hashlib.sha256(path.read_bytes()).hexdigest() + for path in sorted(PACKAGE.rglob("*")) if path.is_file() and "__pycache__" not in path.parts + } + payload = json.dumps(result, indent=2, sort_keys=True) + "\n" + if arguments.receipt: + require(not arguments.receipt.resolve().is_relative_to(PACKAGE), "receipt must be outside package") + require(arguments.receipt.write_text(payload) == len(payload), "complete receipt write") + print(payload, end="") + print("PASS_NATIVE_PREFIX_BALANCED_COARSENING") + + +if __name__ == "__main__": + main()