From b97ef8a66d105478b6077d431d1f96e8fbcc7bb5 Mon Sep 17 00:00:00 2001 From: Ali Romman <226877337+aliromman@users.noreply.github.com> Date: Fri, 23 Oct 2026 12:13:37 -0500 Subject: [PATCH 1/2] Retain variable-gap cyclic solver source for Gaussian binding --- .../vendor/PROOF.md | 182 ++++++++++++++++++ .../vendor/README.md | 75 ++++++++ .../vendor/solver.py | 133 +++++++++++++ 3 files changed, 390 insertions(+) create mode 100644 research/periodic-gaussian-uniform-solve/vendor/PROOF.md create mode 100644 research/periodic-gaussian-uniform-solve/vendor/README.md create mode 100644 research/periodic-gaussian-uniform-solve/vendor/solver.py diff --git a/research/periodic-gaussian-uniform-solve/vendor/PROOF.md b/research/periodic-gaussian-uniform-solve/vendor/PROOF.md new file mode 100644 index 0000000000..924929376c --- /dev/null +++ b/research/periodic-gaussian-uniform-solve/vendor/PROOF.md @@ -0,0 +1,182 @@ +# Cyclic band elimination with an explicit variable gap + +## Contract and result + +Let A be an N by N real dyadic matrix with positive diagonal. Suppose + + a_ii - sum_(j != i) |a_ij| >= delta > 0, + max_i sum_j |a_ij| <= M, + a_ij = 0 if min(|i-j|, N-|i-j|) > W. + +Here 0 <= W < N, and delta need not be constant. The input matrix is supplied +on a grid of precision p. A complex right-hand side b is supplied on the +internal grid or a coarser grid. Use the vector norm max_i(|Re b_i|+|Im b_i|), +and suppose it is at most Y>0. Let t>0 be the required solution error. + +Put K=max(1,2M). Choose internal grid step h=2^-q, q>=p, such that + + h <= delta/(2 N K), + h <= t delta^2 / (2 N K Y + 4 delta + 12 M^2). + +The algorithm below returns x with ||x-A^-1 b|| <= t. It has at most +4 N W^2 factor products and at most 8 N W products per complex solve. It +retains at most (4W+1)N factor entries, including zero entries in its fill +pattern. Setup and solve use O(N(W+1)) numeric storage. These are arithmetic +counts. They do not include matrix formation, a physical tape layout or a +complete native/outer invoice. + +Thus q=max(p, log2(1/t)+O(log N+log(1+M)+log(1+Y)+log(1+1/delta))). +In particular, a gap delta=1/(16r) costs logarithmic guards in r. The theorem +does not require ||A-I|| to be bounded by a fixed constant below one. It does +not assert that any unnamed Gaussian family satisfies the input contract. + +## Exact row-dominance bounds + +This paragraph is classical Gaussian elimination, with constants retained for +use below. Let a real matrix B have positive diagonal, row gap at least g>0 +and row norm at most R. In one Schur step, write l=b_ik/b_kk. The remaining +row gap increases by at least |l| times the pivot row gap, and the remaining +absolute row sum decreases by at least that same quantity. This follows from +the triangle inequality after deleting column k. The diagonal stays positive: +the update cannot cross zero while its row gap remains positive. + +All pivots are at least g, and every surviving row sum is at most R. For a +fixed row, let s be the sum of the absolute multipliers used to eliminate it. +The final gap is at least g(1+s), whereas the final row sum is at most R-gs. +The gap is no larger than the row sum. Therefore + + ||L|| <= (R+g)/(2g), ||U|| <= R. + +Every upper row has gap at least g. The maximum-coordinate argument gives +||B^-1|| <= 1/g and ||U^-1|| <= 1/g. Also L^-1=U B^-1, so +||L^-1|| <= R/g. The corresponding bounds hold for leading principal factor +pairs, since a principal submatrix cannot reduce a row-dominance gap. + +## One rounding per factor entry + +Use integers at scale S=2^q. Store the unfinished Schur entries C_ij at scale +S^2. Initially C_ij=A_ij S^2, exactly. At pivot k: + +1. Set U_kj=trunc(C_kj/S) for j>=k. These integers have scale S. +2. Set L_ik=trunc(C_ik/U_kk) for i>k. These integers have scale S. +3. Update C_ij -= L_ik U_kj exactly for every remaining nonzero pattern pair. + +Here trunc rounds toward zero. The diagonal of L is one. No product or Schur +update is rounded. Round only the factor entry at its final use. + +Expanding the stored integer updates gives a factor residual E=LU-A. +Each upper entry has residual at most h. Each lower entry has residual at +most h times its pivot magnitude. The same identities hold for a partial +factorization: assign these residuals to completed entries of A, and set the +residuals of unfinished entries to zero. Its completed factors are exact +factors of this partially perturbed matrix. + +This gives a closed induction, not an assumption of stable factors. Suppose +previous pivots are at most 2M. The errors in a newly completed upper row are +at most h, and those in a lower column are at most 2Mh. Thus the partial row +residual is at most e=NKh <= delta/2. The partially perturbed matrix has gap +at least delta-e and row norm at most M+e. Apply the preceding exact bounds. +The new upper row has norm at most M+e <= 3M/2 < 2M, and its pivot is at least +delta-e >= delta/2. This proves the induction and completes every division. +After all entries are completed, B=LU satisfies + + ||E|| <= e, + ||U|| <= 3M/2, gap(U) >= delta/2, + ||L|| <= 2M/delta, + ||B^-1|| <= 2/delta, ||L^-1|| <= 3M/delta. + +The sharper L estimate follows by using R=M+e and g=delta-e in the exact +formula: (R+g)/(2g)=(M+delta)/(2(delta-e)) <= 2M/delta. + +## Solve residual and error + +For each real and imaginary component, accumulate each triangular dot product +exactly, then round the solved coordinate once to the q-bit grid. The forward +and backward equations are + + L z = b + f, ||f|| <= 2h, + U x = z + g, ||g|| <= 3Mh. + +The factor two accounts for the two components. Thus + + B x = b + r, + ||r|| <= R_s = 2h(1+3M^2/delta). + +Compare with x_*=A^-1 b. Since ||A^-1||<=1/delta and +||B^-1||<=1/(delta-e), + + ||x-x_*|| <= (eY + delta R_s)/(delta(delta-e)) + <= h(2NKY+4delta+12M^2)/delta^2 <= t. + +The last inequality is the stated precision choice. If a caller rounds this +result to a different output grid, it must add that rounding error. If it +formed A as an approximation to another operator, it must also add the +coefficient and truncation errors through a separate perturbation bound. + +## Uniform integer range + +The proof first analyzes the same algorithm over unbounded integers. Put + + L_0=2M/delta, U_0=3M/2, + Z=(3M/delta)(Y+2h), X=(2/delta)(Y+R_s), + C=max(1, M+L_0 U_0, Y+L_0 Z, Z+U_0 X, L_0,U_0,Y,Z,X). + +All factor, forward and backward accumulators have absolute value at most +C S^2. For a partial dot product use the sum of absolute terms and the bounds +on the full row of L or U. The leading-principal bounds control all forward +prefixes. Every backward coordinate is a coordinate of the final vector, so +the final bound also controls each stored coordinate. It does not depend on +that coordinate being generated last. A signed integer width + + 2q + ceil(log2 C) + 2 + +therefore covers all products, sums, division numerators and stored integers. +The executable checks this range at every numeric update. This establishes a +uniform input bound; an observed peak from a finite test is not its proof. +The input and retained factors are preserved, and the owned forward buffer is +cleared after each solve. Clearing here is an array operation, not a physical +tape-erasure theorem. + +## Cyclic fill and arithmetic cost + +If N>2W, place the last W indices in a border set. The remaining indices form +an ordinary band of half-width W. Under natural-order elimination, an interior +pivot can touch only its next W interior indices and the W border indices. +An update can add only pairs among those indices; it cannot connect more +distant interior indices. Induction preserves this pattern. Each pivot +therefore has at most 2W later row neighbors and 2W later column neighbors. +Once only border indices remain, the same bound is immediate. If N<=2W, the +dense bound N-1<=2W suffices. W=0 is diagonal. + +There are at most 4W^2 updates at a pivot, at most 2NW lower entries and at +most 2NW+N upper entries. One solve uses each strict triangular entry once +per real component. A complex solve therefore uses at most 8NW products, +plus 4N scalar truncations/divisions. Numeric storage is O(N(W+1)); active +Schur entries and retained factors can coexist within that order. Indexing, +allocation and Python overhead are not a certified native instruction tariff. + +## Prior results and evidence + +Dugongue's [PR #4554](https://github.com/CrocSwap/integer-mult-bounds/pull/4554) +proves a near-identity ordinary-band fixed-point algorithm and a periodic +Woodbury reduction with constant norm bounds. Ryanson Jonathan's independent +banded-inverse check retains that exact scope. The earlier batched principal- +window note uses noncyclic factors. [PR #5260](https://github.com/CrocSwap/integer-mult-bounds/pull/5260) +supplies the fixed385-row direct consumer; its matrix-specific residual does +not provide this all-size precision guarantee. This result supplies direct +cyclic fill, one-round factor residuals and explicit variable-gap guards. + +Row-dominance and Gaussian-elimination stability are classical; see Nicholas +J. Higham's [growth-factor summary](https://nhigham.com/2020/07/14/what-is-the-growth-factor-for-gaussian-elimination/) +and the Wilkinson/Higham references there. No new general stability theorem +or global literature priority is claimed. The proof here makes the algorithm, +absolute error, integer range and cyclic cost explicit for this interface. + +Exact tests include an independently transcribed pivoted rational solver, +symbolic cyclic fill and original-matrix residuals at larger sizes. These +corroborate the written all-size proof. Independent human or proof-kernel +review is not claimed. Source matrix formation, analytic recovery, native +relations, fixed tapes and the full multiplication invoice remain open. +No new kappa, production-family admission or selected-frontier change is made. + +Prepared by Ali Romman with substantial OpenAI Codex assistance; Apache-2.0. diff --git a/research/periodic-gaussian-uniform-solve/vendor/README.md b/research/periodic-gaussian-uniform-solve/vendor/README.md new file mode 100644 index 0000000000..7069589b9e --- /dev/null +++ b/research/periodic-gaussian-uniform-solve/vendor/README.md @@ -0,0 +1,75 @@ +# Cyclic band solves with a variable row gap + +A complete integer solver now covers every real dyadic cyclic band matrix +with positive diagonal and a certified row gap delta>0. The gap may shrink +with the problem size. [PROOF.md](PROOF.md) gives an explicit all-input error +and integer-range proof. No constant near-identity or Woodbury-smallness +assumption is required. + +The factorization uses at most 4NW^2 integer products and retains at most +(4W+1)N entries. Each complex solve uses at most 8NW products and 4N component +roundings/divisions. Exact integer accumulation and one rounding per factor +entry give sufficient precision + + q = max(input precision, output precision + + O(log N + log(1+M) + log(1+Y) + log(1+1/delta))). + +Here M bounds the input matrix row norm and Y bounds the complex RHS norm. +The executable uses the explicit inequalities in the proof, not this O-term. +At delta=1/4096, the 4,097-row width-four fixture needs 60 fractional bits +and a proven signed width of 151 bits. Its observed peak is 132 bits. Factor +preparation uses 261,836 products; each complex solve uses 130,960 products. +The complete residual meets the 2^-20 solution target. + +This is an all-size numerical interface, with finite exact corroboration. +It extends the fixed-instance result in +[PR #5260](https://github.com/CrocSwap/integer-mult-bounds/pull/5260) and the +constant-gap band/Woodbury interface in Dugongue's +[PR #4554](https://github.com/CrocSwap/integer-mult-bounds/pull/4554). +Matrix formation, source approximation error, physical movement and the +complete multiplication invoice remain caller obligations. No new kappa, +Gaussian-family admission or selected-frontier change is claimed. + +## Reproduce + +Requires CPython 3.12 and the standard library: + +```sh +python3.12 -B scripts/research_package.py --package research/cyclic-band-gap-solver +``` + +Expected: `PASS_CYCLIC_BAND_GAP` in normal and optimized modes, followed by +`PASS_REGISTERED_RESEARCH_PACKAGE`. [RESULT.json](RESULT.json) binds all +package files and records the exact results. A separately transcribed pivoted +rational solver checks 72 complex right-hand sides on 36 small cases. The +replay also checks nine matrix/RHS scale pairs, 129 symbolic cyclic patterns, +eight control groups and +original-matrix residuals for 257, 1,025 and 4,097 rows with gap 1/4096. + +The source proofs and attribution are pinned in [SOURCES.json](SOURCES.json). +They are provenance, not imported runtime code. The base is canonical main +ff3cc58e370d0f678e529246f8c73e8094e18fcf, priority revision7. The #5260 result is prior-work context, not an imported runtime or proof +assumption. Every declared source commit is an ancestor of this publication. +No other package is edited. +The full-history wrapper, selected cold replay, Lean and Docker were not run. +No independent human or proof-kernel review is claimed. Dictionary/indexing +and Python allocation overhead are outside the arithmetic count. + +## Open next questions + +Can a paid Gaussian production family meet the dyadic input contract with an +adequate source error budget? First bind one admitted family's exact delta, +width and coefficient-generation method. Then add its source and final-grid +errors, physical layout and outer recurrence. The numerical solve alone does +not supply those obligations. This question is open and unreserved. + +## Credit + +Prepared by Ali Romman with substantial OpenAI Codex assistance; Apache-2.0. +Dugongue supplies the prior constant-gap native band/Woodbury proof; Ryanson +Jonathan supplies its independent scoped check. Classical diagonal dominance, +Gaussian elimination, Wilkinson's error analysis and Higham's exposition retain +their credit. The earlier batched principal-window note is a noncyclic +comparison. The Gaussian identity and source lineage retain OpenAI/math, +Harvey and van der Hoeven credit as stated in the pinned predecessor NOTICE. +No global novelty or new general stability theorem is claimed. diff --git a/research/periodic-gaussian-uniform-solve/vendor/solver.py b/research/periodic-gaussian-uniform-solve/vendor/solver.py new file mode 100644 index 0000000000..f28d518d56 --- /dev/null +++ b/research/periodic-gaussian-uniform-solve/vendor/solver.py @@ -0,0 +1,133 @@ +"""Solve a dyadic cyclic band system with an explicit variable-gap budget. + +Ali Romman, with substantial OpenAI Codex assistance. Apache-2.0. +Classical diagonal-dominance and elimination credit is in PROOF.md. +""" +from fractions import Fraction as Q + + +def need(value, message): + if not value: + raise ValueError(message) + + +def trunc(a, b): + need(b > 0, 'positive divisor required') + return a//b if a >= 0 else -((-a)//b) + + +def budget(n, delta, norm, rhs_bound, tolerance, input_bits): + delta, norm, rhs_bound, tolerance = map(Q, (delta, norm, rhs_bound, tolerance)) + need(n > 0 and 0 < delta <= norm and rhs_bound > 0 and tolerance > 0 and input_bits >= 0, + 'invalid budget') + k = max(Q(1), 2*norm) + ceiling = min(delta/(2*n*k), tolerance*delta**2/(2*n*k*rhs_bound+4*delta+12*norm**2)) + bits = input_bits + while Q(1, 1 << bits) > ceiling: + bits += 1 + h = Q(1, 1 << bits) + eta = n*k*h + lower_norm, upper_norm = 2*norm/delta, Q(3, 2)*norm + solve_residual = 2*h*(1+3*norm**2/delta) + z_bound = 3*norm/delta*(rhs_bound+2*h) + x_bound = 2/delta*(rhs_bound+solve_residual) + accumulator = max(Q(1), norm+lower_norm*upper_norm, + rhs_bound+lower_norm*z_bound, z_bound+upper_norm*x_bound, + lower_norm, upper_norm, rhs_bound, z_bound, x_bound) + magnitude_bits = 0 + while 1 << magnitude_bits < accumulator: + magnitude_bits += 1 + return {'bits': bits, 'word_bits': 2*bits+magnitude_bits+2, 'delta': delta, + 'norm': norm, 'rhs_bound': rhs_bound, 'tolerance': tolerance, + 'factor_residual': eta, 'solve_residual': solve_residual, + 'error': (eta*rhs_bound+delta*solve_residual)/(delta*(delta-eta)), + 'lower_norm': lower_norm, 'upper_norm': upper_norm, + 'z_bound': z_bound, 'x_bound': x_bound, 'accumulator_bound': accumulator} + + +class Guard: + def __init__(self, bits): + self.limit = (1 << (bits-1))-1 + self.peak = 0 + + def __call__(self, value): + need(type(value) is int and abs(value) <= self.limit, 'integer word overflow') + self.peak = max(self.peak, abs(value)) + return value + + +def factor(rows, input_bits, width, delta, norm, rhs_bound, tolerance): + n = len(rows) + need(type(width) is int and 0 <= width < n and type(input_bits) is int and input_bits >= 0, + 'invalid shape or input grid') + scale_in = 1 << input_bits + delta, norm = Q(delta), Q(norm) + for i, row in enumerate(rows): + need(all(type(j) is int and 0 <= j < n and type(x) is int for j, x in row.items()), 'invalid coefficient') + need(all(min(abs(i-j), n-abs(i-j)) <= width for j, x in row.items() if x), 'outside cyclic band') + diagonal = row.get(i, 0) + off = sum(abs(x) for j, x in row.items() if j != i) + need(diagonal > 0 and diagonal-off >= delta*scale_in, 'row gap violated') + need(diagonal+off <= norm*scale_in, 'row norm violated') + plan = budget(n, delta, norm, rhs_bound, tolerance, input_bits) + need(plan['factor_residual'] <= delta/2 and plan['error'] <= tolerance, 'precision gate failed') + bits = plan['bits']; scale = 1 << bits; checked = Guard(plan['word_bits']) + shift = bits-input_bits + active = [{j: checked((x << shift)*scale) for j, x in row.items() if x} for row in rows] + columns = [set() for _ in range(n)] + for i, row in enumerate(active): + for j in row: columns[j].add(i) + lower, upper = [dict() for _ in rows], [dict() for _ in rows] + products = divisions = max_front = 0 + for k in range(n): + upper[k] = {j: checked(trunc(value, scale)) for j, value in active[k].items() if j >= k} + divisions += len(upper[k]) + pivot = upper[k].get(k, 0) + need(pivot >= delta*scale/2, 'pivot bound failed') + successors = sorted(i for i in columns[k] if i > k) + outgoing = [j for j in upper[k] if j > k] + max_front = max(max_front, len(successors), len(outgoing)) + need(len(successors) <= 2*width and len(outgoing) <= 2*width, 'cyclic fill bound failed') + for i in successors: + multiplier = checked(trunc(active[i].pop(k), pivot)) + divisions += 1 + lower[i][k] = multiplier + for j in outgoing: + product = checked(multiplier*upper[k][j]); products += 1 + active[i][j] = checked(active[i].get(j, 0)-product) + columns[j].add(i) + for j in active[k]: columns[j].discard(k) + active[k].clear(); columns[k].clear() + need(products <= 4*n*width**2, 'factor product budget failed') + records = sum(map(len, lower))+sum(map(len, upper)) + need(records <= (4*width+1)*n, 'factor storage bound failed') + return {'lower': lower, 'upper': upper, 'plan': plan, 'width': width, + 'statistics': {'products': products, 'divisions': divisions, 'factor_records': records, + 'maximum_front': max_front, 'peak_integer_bits': checked.peak.bit_length()}} + + +def solve(factors, rhs, rhs_bits): + lower, upper, plan = factors['lower'], factors['upper'], factors['plan'] + n, bits = len(lower), plan['bits']; scale = 1 << bits + need(type(rhs_bits) is int and 0 <= rhs_bits <= bits and len(rhs) == n, 'invalid RHS grid or length') + need(all(len(x) == 2 and all(type(t) is int for t in x) for x in rhs), 'integer complex pairs required') + need(all(sum(abs(t) for t in x) <= plan['rhs_bound']*(1 << rhs_bits) for x in rhs), 'RHS bound violated') + checked = Guard(plan['word_bits']); products = divisions = 0 + z = [[0, 0] for _ in rhs]; result = [[0, 0] for _ in rhs] + for i in range(n): + for c in (0, 1): + accumulator = checked((rhs[i][c] << (bits-rhs_bits))*scale) + for j, value in lower[i].items(): + accumulator = checked(accumulator-checked(value*z[j][c])); products += 1 + z[i][c] = checked(trunc(accumulator, scale)); divisions += 1 + for i in reversed(range(n)): + for c in (0, 1): + accumulator = checked(z[i][c]*scale) + for j, value in upper[i].items(): + if j > i: + accumulator = checked(accumulator-checked(value*result[j][c])); products += 1 + result[i][c] = checked(trunc(accumulator, upper[i][i])); divisions += 1 + need(products <= 8*n*factors['width'], 'solve product budget failed') + for pair in z: pair[:] = [0, 0] + return result, {'products': products, 'divisions': divisions, + 'cleared_scratch_cells': 2*n, 'peak_integer_bits': checked.peak.bit_length()} From 234142af90b5e7afe0b33c4b78c3c0bd622d5fc3 Mon Sep 17 00:00:00 2001 From: Ali Romman <226877337+aliromman@users.noreply.github.com> Date: Fri, 23 Oct 2026 12:21:56 -0500 Subject: [PATCH 2/2] Bind periodic Gaussian sources to the variable-gap direct solver --- .../periodic-gaussian-uniform-solve/PROOF.md | 188 +++++++ .../periodic-gaussian-uniform-solve/README.md | 57 ++ .../RESULT.json | 510 ++++++++++++++++++ .../SOURCES.json | 144 +++++ .../periodic-gaussian-uniform-solve/TASK.json | 99 ++++ .../VALIDATION.md | 43 ++ .../VERIFY.json | 44 ++ .../consumer.py | 111 ++++ .../periodic-gaussian-uniform-solve/verify.py | 175 ++++++ 9 files changed, 1371 insertions(+) create mode 100644 research/periodic-gaussian-uniform-solve/PROOF.md create mode 100644 research/periodic-gaussian-uniform-solve/README.md create mode 100644 research/periodic-gaussian-uniform-solve/RESULT.json create mode 100644 research/periodic-gaussian-uniform-solve/SOURCES.json create mode 100644 research/periodic-gaussian-uniform-solve/TASK.json create mode 100644 research/periodic-gaussian-uniform-solve/VALIDATION.md create mode 100644 research/periodic-gaussian-uniform-solve/VERIFY.json create mode 100644 research/periodic-gaussian-uniform-solve/consumer.py create mode 100644 research/periodic-gaussian-uniform-solve/verify.py diff --git a/research/periodic-gaussian-uniform-solve/PROOF.md b/research/periodic-gaussian-uniform-solve/PROOF.md new file mode 100644 index 0000000000..d4bb4f44b8 --- /dev/null +++ b/research/periodic-gaussian-uniform-solve/PROOF.md @@ -0,0 +1,188 @@ +# A complete periodic Gaussian source-to-solver interface + +Prepared by Ali Romman with substantial OpenAI Codex assistance. Apache-2.0. +This is a written conditional proof, supported by exact finite tests. + +## Contract and result + +Let R be the unchanged narrow `Reference` of Jose Manuel's +`research/rational-unitary-fft/gaussian_reference.py`, pinned in SOURCES.json. +Its source size is n, excess is e with 0=0 such that + + H_ii=1, H_ij>=0, sum_(j!=i) H_ij <= 1-g, + ||H-H0|| <= E + +for the ideal analytic matrix H0. The norm on vectors is the maximum of +|Re z_i|+|Im z_i|. The first premises are also checked on all generated +nonzero positions. The analytic approximation premise is inherited from the +source. This package does not independently certify its interval backend. + +Let d be the largest number 2^-k, k>=0, with d<=g. Thus g/2=1, epsilon=2^-t, rational radius Y>0 +and boundary precision P>=t+3. Admit the source only if + + E=P so that + + coefficient = Y (2w) 2^-p/d^2 <= epsilon/4. + +These are explicit exact gates. They can fail for an insufficient source +precision or tail width. The statement is for every source and caller that +satisfies them, not an assertion that an unnamed production policy does so. + +**Theorem.** For every admitted unchanged Reference, preparation succeeds and +the consumer returns y with ||y-H0^-1 u||<=epsilon for every signed complex +P-grid input u with norm at most Y. All N coordinates are returned. Hole +coordinates are copied exactly. The direct factorization uses at most +4nw^2 products and each complex solve at most 8nw products, plus full target +scans and grid conversion. Factor/solve numeric storage is O(n(w+1)+N). +Coefficient generation and physical movement are separate paid costs below. + +## 1. Original-coordinate reduction + +Put rho=N/n and k_i=i+nearest_up((rho-1)i)=nearest_up(rho i). Since rho>1, +the k_i are strictly increasing and lie in [0,N). For the source's reverse +map, |k_i/rho-i|<=1/(2rho)<1/2, so nearest_up(k_i/rho)=i. Thus there are n +selected coordinates and exactly e holes, without an ambiguous inverse. + +The literal source returns the identity if either coordinate is a hole. +For selected row k_i and column k_j it computes + + lift = -nearest_up((j-i)/n), h=j+lift*n-i. + +It returns zero if |h|>w. Since 2w=d, ||Hhat||<=2-d, + ||H-Hhat|| <= (2w) 2^-p = Delta. + +The maximum-coordinate row argument gives ||H^-1||,||Hhat^-1||<=1/d. The +resolvent identity then gives + + ||Hhat^-1 u-H^-1 u|| <= Y Delta/d^2 = coefficient. + +Since E=p such that + + 2^-q <= d/(2nK), + 2^-q <= (epsilon/4)d^2/(2nKY+4d+12M^2). + +The retained proof establishes positive pivots, a complete factor residual, +both rounded triangular solves, and a uniform signed word range. It gives +an internal selected result v with error `solve<=epsilon/4` against +Bhat^-1 u_selected. It does not depend on a constant lower bound for d. +Since q>=p>=P, the input lift to the internal grid is exact. + +Round each selected real and imaginary component toward zero to the P-grid. +This adds at most `output=2*2^-P<=epsilon/4` in the stated norm. Copy each +hole input exactly. The returned vector therefore satisfies + + ||y-H0^-1 u|| <= analytic + coefficient + solve + output <= epsilon. + +In particular the required precisions have logarithmic dependence on n, +1/d, Y and 1/epsilon. Source entry precision and the input/output precision +can be larger, and are not hidden by this statement. The factor theorem's +word bound also applies unchanged. The source interval/rational arithmetic +has a separate, potentially much larger bit range. + +A raw residual of the finally rounded output divided by d can be a loose +error certificate. Its rounding contribution is amplified by the row norm +and 1/d. The verifier therefore also computes the original-H residual of +the internal q-grid solution, checks that the public output is its exact +P-grid truncation, and adds the final rounding and analytic allowances. It +retains the final-output residual as a separate diagnostic. This distinction +does not weaken the consumer target or assume that truncation is linear. + +## 4. Complete local invoice and ownership + +The source producer and its original precision policy are executed. Setup +includes the n(2w+1)+e entry requests, up to n retained weight records, up to +w kernel records, source interval/pi caches, the selected/holes map and the +quantized matrix. Cross-period exponential calls and rational weight +construction are included in source setup; the entry count is not a bit-time +bound for these calls. `RESULT.json` records actual cache counts and source +precision fields before verifier-only matrix reads. + +Factor preparation retains the direct cyclic fill. The inherited bounds are +4nw^2 factor products and at most (4w+1)n factor records. Quantized source +rows and active factor workspace coexist during preparation. A complex solve +uses at most 8nw products and 4n component divisions. It also pays a complete +2N-component input/radius scan, a 2n-component gather, 2n final truncations +and scatter writes, a complete target staging copy and returned tuple, and +all buffer clears. Hole values remain exact on the original P-grid. + +The input tuple and retained factors are borrowed and unchanged. The source +object and its caches remain caller-owned. `execute` requires the unchanged +Prepared object returned by `prepare`; arbitrary caller-built or modified +factor dictionaries are outside the theorem. The retained solver clears its +2n-component forward buffer. The adapter clears its 2n-component internal +answer and 2N-component staging list after a successful solve, including an +exception during final conversion. The gathered tuple holds references to +immutable input pairs and is released. These are logical array operations, +not physical allocator zeroization or a multitape ownership theorem. + +The complete local cost is source formation plus factorization plus each +solve and the O(N+n) boundary scans. No source, gather, scatter, persistent +factor or cache cost is assigned zero. Physical ordered delivery, primitive +acceptance and the full outer multiplication invoice remain open. + +## Evidence, scope and credit + +The finite checker compares all original entries and all outputs across +several source sizes, excesses, widths and source precisions. It uses a +separate pivoted rational dense solver on small cases and original-source +residuals on larger cases. It checks periodic couplings, multiple holes, +signed complex inputs, exact hole returns, source and factor preservation, +precision gates and a gap below any fixed 16-bit threshold. + +The theorem is an all-parameter conditional interface; finite tests do not +prove production parameter funding. There is no production-family or native +supplier admission, complete kappa improvement or selected-frontier change. +No independent human or proof-kernel review is claimed. + +Jose Manuel supplies the immutable Reference and its analytic contract. +JoyboyBrian's [PR #5159](https://github.com/CrocSwap/integer-mult-bounds/pull/5159) +supplies the earlier complete periodic recurrence and source/error boundary; +[PR #5216](https://github.com/CrocSwap/integer-mult-bounds/pull/5216) supplies +its weighted-power improvement. Ali Romman's +[PR #5260](https://github.com/CrocSwap/integer-mult-bounds/pull/5260) supplies +the fixed385-row direct consumer, and +[PR #5284](https://github.com/CrocSwap/integer-mult-bounds/pull/5284) supplies +the unchanged all-size cyclic solver used here. Dugongue's +[PR #4554](https://github.com/CrocSwap/integer-mult-bounds/pull/4554) and +Ryanson Jonathan's audit supply the earlier band/Woodbury scope. Retained +notices credit Vlado Vojdanovski, Jeremy Kothe, Cinna Davis, Mason Hale and +the Gaussian/precision lineage. Gaussian elimination, diagonal dominance, +resolvent bounds and coordinate permutations are classical. The new result +is their complete binding at this Reference caller, not a new general solver. diff --git a/research/periodic-gaussian-uniform-solve/README.md b/research/periodic-gaussian-uniform-solve/README.md new file mode 100644 index 0000000000..7d8d01251b --- /dev/null +++ b/research/periodic-gaussian-uniform-solve/README.md @@ -0,0 +1,57 @@ +# Uniform direct consumer for the narrow periodic Gaussian Reference + +This package binds the actual narrow `Reference` family to the retained +variable-gap cyclic direct solver. It supports every source parameter tuple +that passes the explicit positive-gap and analytic-error gates. It retains +all periodic and cross-cell coefficients, every hole and arbitrary signed +complex inputs. Source generation remains paid. + +The [proof](PROOF.md) gives an original-coordinate error theorem. It separates +analytic Reference error, downward coefficient rounding, the rounded direct +solve and final output rounding. Each term has one quarter of the target. +The gap is rounded down adaptively to a power of two; there is no fixed +16-bit floor. A source with an unfunded analytic error is rejected. + +For source size n, excess e, target period N=n+e and retained halfwidth w, +the consumer uses at most 4nw^2 factor products and 8nw products per complex +solve, plus O(N+n) input/output scans and grid conversion. Source formation, +its potentially large rational weights, retained caches and factor storage +are explicit additional costs. The selected block is cyclic in source +coordinates. Hole coordinates are copied exactly on the boundary grid. + +Run with Python 3.12 and the standard library: + +```sh +python3.12 -B scripts/research_package.py --package research/periodic-gaussian-uniform-solve +``` + +Both registered isolated, warning-strict modes must end with +`PASS_PERIODIC_GAUSSIAN_UNIFORM_SOLVE`. `RESULT.json` contains the exact +finite evidence. Direct `verify.py --write-result` regenerates it; +`verify.py --small` runs the two small source cases and rejection controls. +The normal command writes no package files. + +This extends the one-source direct result in +[PR #5260](https://github.com/CrocSwap/integer-mult-bounds/pull/5260) by binding +the all-size solver from +[PR #5284](https://github.com/CrocSwap/integer-mult-bounds/pull/5284) to the +unchanged source and arbitrary hole geometry. It does not prove that a given +production policy funds the gates. It is a host-array consumer, not a native +tape implementation or a complete multiplication theorem. Kappa and the +selected frontier remain unchanged. + +Prepared by Ali Romman with substantial OpenAI Codex assistance; Apache-2.0. +Credit Jose Manuel for the Reference; JoyboyBrian for the periodic recurrence +and weighted-power bound; Dugongue and Ryanson Jonathan for the prior +band/Woodbury scope; and their retained source notices. `SOURCES.json` pins +the live source inputs and the byte-exact solver retained in branch history. +The full credit and limits are in PROOF.md. + +## Open next questions + +Pin one production caller policy and fund all four terms with its actual +source size, excess, Gaussian width, truncation radii, target and input bound. +Then pay the original coefficient generation together with ordered physical +delivery, retained factors and restoration. The local arithmetic result does +not supply that bit-cost or tape proof. Independent acceptance of the +inherited analytic and interval contracts also remains separate. diff --git a/research/periodic-gaussian-uniform-solve/RESULT.json b/research/periodic-gaussian-uniform-solve/RESULT.json new file mode 100644 index 0000000000..6ea430e427 --- /dev/null +++ b/research/periodic-gaussian-uniform-solve/RESULT.json @@ -0,0 +1,510 @@ +{ + "status": "PASS", + "fixtures": [ + { + "specification": [ + 9, + 1, + 1, + 2, + 2, + 64 + ], + "target": 12, + "period": 10, + "holes": [ + 5 + ], + "gap": "1/4", + "boundary_bits": 15, + "coefficient_bits": 20, + "internal_bits": 25, + "word_bits": 61, + "error_terms": [ + "6325730235189507719762330560017543699614572791953628120195238101288074832140/30354199661915388090181307477474518394057347071252091809176157975450391842163795389", + "1/16384", + "403/16777153", + "1/16384" + ], + "source_requests": 46, + "source_setup": { + "weights": 9, + "kernels": 2, + "entries": 46, + "weight_precision": 89, + "kernel_error_bits": 84 + }, + "factor": { + "products": 50, + "divisions": 49, + "factor_records": 49, + "maximum_front": 4, + "peak_integer_bits": 51 + }, + "solve": { + "products": 80, + "divisions": 36, + "cleared_scratch_cells": 18, + "peak_integer_bits": 50, + "target_input_components": 20, + "target_output_components": 20, + "gather_components": 18, + "scatter_components": 18, + "output_roundings": 18, + "hole_copy_components": 2, + "answer_clear_components": 18, + "staging_clear_components": 20 + }, + "output_sha256": "1ef79df038b003b4d4e70710c804f8329648744ab93cdb5174ce7851d985a69d", + "reference_hash": "2978b846d72273da4a53ef217b417d155ae4bf444f57a5942e1371326563af68", + "final_grid_residual_certificate_meets_target": true, + "internal_residual_plus_rounding_meets_target": true + }, + { + "specification": [ + 13, + 5, + 1, + 3, + 3, + 64 + ], + "target": 18, + "period": 18, + "holes": [ + 2, + 5, + 9, + 13, + 16 + ], + "gap": "1/2", + "boundary_bits": 21, + "coefficient_bits": 25, + "internal_bits": 29, + "word_bits": 66, + "error_terms": [ + "28248786850321853254469605699240139596535623870031508122183062802585970/82887206067289722111086184132201712335122281645146697800188868338059147545904165327687", + "3/4194304", + "107/268435417", + "1/1048576" + ], + "source_requests": 96, + "source_setup": { + "weights": 12, + "kernels": 2, + "entries": 96, + "weight_precision": 77, + "kernel_error_bits": 92 + }, + "factor": { + "products": 49, + "divisions": 61, + "factor_records": 61, + "maximum_front": 3, + "peak_integer_bits": 59 + }, + "solve": { + "products": 96, + "divisions": 52, + "cleared_scratch_cells": 26, + "peak_integer_bits": 58, + "target_input_components": 36, + "target_output_components": 36, + "gather_components": 26, + "scatter_components": 26, + "output_roundings": 26, + "hole_copy_components": 10, + "answer_clear_components": 26, + "staging_clear_components": 36 + }, + "output_sha256": "228f6450056392fceee5debf35b21848cd604a8ff1db1cfe35ecda518ae1295d", + "reference_hash": "8c6de7ede9f47d66610363e6852887e1106b2b6960d39c58e62fc0db1e5e6f79", + "final_grid_residual_certificate_meets_target": true, + "internal_residual_plus_rounding_meets_target": true + }, + { + "specification": [ + 31, + 1, + 2, + 3, + 4, + 80 + ], + "target": 24, + "period": 32, + "holes": [ + 16 + ], + "gap": "1/2", + "boundary_bits": 27, + "coefficient_bits": 31, + "internal_bits": 36, + "word_bits": 80, + "error_terms": [ + "222800809911584415685611247169775736365004599674198405485030043197687431505642532549912414/9619630419041620901435201124044168671922952704271303426881453703991019093528074304396620811782947733226524134481", + "3/268435456", + "43/6871947655", + "1/67108864" + ], + "source_requests": 218, + "source_setup": { + "weights": 31, + "kernels": 3, + "entries": 218, + "weight_precision": 335, + "kernel_error_bits": 180 + }, + "factor": { + "products": 59, + "divisions": 109, + "factor_records": 109, + "maximum_front": 2, + "peak_integer_bits": 73 + }, + "solve": { + "products": 156, + "divisions": 124, + "cleared_scratch_cells": 62, + "peak_integer_bits": 72, + "target_input_components": 64, + "target_output_components": 64, + "gather_components": 62, + "scatter_components": 62, + "output_roundings": 62, + "hole_copy_components": 2, + "answer_clear_components": 62, + "staging_clear_components": 64 + }, + "output_sha256": "4d7cb873fe5607e0eabcf643ebfcc4fb72c611c3a31205daec2fcaa3eda39358", + "reference_hash": "7586c6cdae0cc5ca6bc749dec9f945bb26552283aa3dfd92331ddad5b0d3fedc", + "final_grid_residual_certificate_meets_target": true, + "internal_residual_plus_rounding_meets_target": true + }, + { + "specification": [ + 32, + 7, + 1, + 3, + 4, + 64 + ], + "target": 12, + "period": 39, + "holes": [ + 3, + 8, + 14, + 19, + 25, + 31, + 36 + ], + "gap": "1/2", + "boundary_bits": 15, + "coefficient_bits": 19, + "internal_bits": 24, + "word_bits": 56, + "error_terms": [ + "331040470902209217825815691787970385896901842226997164102219205783682/971334446101051430989291220299238816427214238029062864845963300797107044973760964543", + "3/65536", + "221/8388512", + "1/16384" + ], + "source_requests": 231, + "source_setup": { + "weights": 32, + "kernels": 3, + "entries": 231, + "weight_precision": 81, + "kernel_error_bits": 92 + }, + "factor": { + "products": 194, + "divisions": 189, + "factor_records": 189, + "maximum_front": 4, + "peak_integer_bits": 49 + }, + "solve": { + "products": 314, + "divisions": 128, + "cleared_scratch_cells": 64, + "peak_integer_bits": 48, + "target_input_components": 78, + "target_output_components": 78, + "gather_components": 64, + "scatter_components": 64, + "output_roundings": 64, + "hole_copy_components": 14, + "answer_clear_components": 64, + "staging_clear_components": 78 + }, + "output_sha256": "4cd8025a99dd82824197fba9d02ae310c42762355b102d4b27be241905ff7e8f", + "reference_hash": "c55d96696d2fecdb5a8263d5aaf90ce8c81c9d0ceed600e9b491d8d7bfd3a68c", + "final_grid_residual_certificate_meets_target": true, + "internal_residual_plus_rounding_meets_target": true + }, + { + "specification": [ + 65, + 13, + 2, + 3, + 5, + 80 + ], + "target": 18, + "period": 78, + "holes": [ + 3, + 9, + 15, + 21, + 27, + 33, + 39, + 45, + 51, + 57, + 63, + 69, + 75 + ], + "gap": "1/2", + "boundary_bits": 21, + "coefficient_bits": 25, + "internal_bits": 31, + "word_bits": 70, + "error_terms": [ + "7475954625723185288382575971593432401109474019455112551355867602381226173380806032927381549373382/322781234760863573706986158523063622698569025754687560388660710371714778784489409337823749054861841723260164293141910557", + "3/4194304", + "419/1073741629", + "1/1048576" + ], + "source_requests": 468, + "source_setup": { + "weights": 65, + "kernels": 3, + "entries": 468, + "weight_precision": 127, + "kernel_error_bits": 180 + }, + "factor": { + "products": 0, + "divisions": 117, + "factor_records": 117, + "maximum_front": 2, + "peak_integer_bits": 63 + }, + "solve": { + "products": 104, + "divisions": 260, + "cleared_scratch_cells": 130, + "peak_integer_bits": 62, + "target_input_components": 156, + "target_output_components": 156, + "gather_components": 130, + "scatter_components": 130, + "output_roundings": 130, + "hole_copy_components": 26, + "answer_clear_components": 130, + "staging_clear_components": 156 + }, + "output_sha256": "7423c5d7682b7b7ef6dcff833c1f2b527e8ed2d4e9388038da7bcf731abc08c2", + "reference_hash": "1061a30c781938a490cd2002b91c468415e3cfd11fe7a855e1fb29f437a4c72e", + "final_grid_residual_certificate_meets_target": true, + "internal_residual_plus_rounding_meets_target": true + }, + { + "specification": [ + 97, + 1, + 2, + 4, + 6, + 80 + ], + "target": 24, + "period": 98, + "holes": [ + 49 + ], + "gap": "1/8", + "boundary_bits": 27, + "coefficient_bits": 35, + "internal_bits": 42, + "word_bits": 97, + "error_terms": [ + "71614546043009276470375043733142200974465685714818071292374526795233532144914754950831640/150306725297525326584917806376262193592484886249665828910157313391760932917591578708406160718537926178506812477", + "1/67108864", + "12323/2199023254097", + "1/67108864" + ], + "source_requests": 874, + "source_setup": { + "weights": 97, + "kernels": 4, + "entries": 874, + "weight_precision": 863, + "kernel_error_bits": 212 + }, + "factor": { + "products": 228, + "divisions": 376, + "factor_records": 376, + "maximum_front": 2, + "peak_integer_bits": 85 + }, + "solve": { + "products": 558, + "divisions": 388, + "cleared_scratch_cells": 194, + "peak_integer_bits": 85, + "target_input_components": 196, + "target_output_components": 196, + "gather_components": 194, + "scatter_components": 194, + "output_roundings": 194, + "hole_copy_components": 2, + "answer_clear_components": 194, + "staging_clear_components": 196 + }, + "output_sha256": "8fb910cce47eed023757120269b098b39bfe41785fc60e9adac5a1cb9f4a4176", + "reference_hash": "9027ab264c59c30fc6c47f7495b9ed22d6fd59f71a720829c23a31b0227f8120", + "final_grid_residual_certificate_meets_target": false, + "internal_residual_plus_rounding_meets_target": true + }, + { + "specification": [ + 129, + 7, + 2, + 4, + 7, + 96 + ], + "target": 12, + "period": 136, + "holes": [ + 10, + 29, + 49, + 68, + 87, + 107, + 126 + ], + "gap": "1/2", + "boundary_bits": 15, + "coefficient_bits": 19, + "internal_bits": 26, + "word_bits": 60, + "error_terms": [ + "307582133172611051864883125688415504502789451219357998790545046727465344280215298476474362090884994/676921312041214565326761275271766478197980869422982405523184921417909784425169789136853054135935823179824195403820358927317055", + "1/16384", + "803/33554045", + "1/16384" + ], + "source_requests": 1168, + "source_setup": { + "weights": 129, + "kernels": 4, + "entries": 1168, + "weight_precision": 251, + "kernel_error_bits": 228 + }, + "factor": { + "products": 0, + "divisions": 251, + "factor_records": 251, + "maximum_front": 2, + "peak_integer_bits": 53 + }, + "solve": { + "products": 244, + "divisions": 516, + "cleared_scratch_cells": 258, + "peak_integer_bits": 53, + "target_input_components": 272, + "target_output_components": 272, + "gather_components": 258, + "scatter_components": 258, + "output_roundings": 258, + "hole_copy_components": 14, + "answer_clear_components": 258, + "staging_clear_components": 272 + }, + "output_sha256": "22bc2df526cd962fb2744870735f35454f7fb0cf7bf5e4694cc685deca3449f4", + "reference_hash": "a3cb4cf683cc0bfbd77e848bf9a6a6f7c7e82346351a392df631db201968abf8", + "final_grid_residual_certificate_meets_target": true, + "internal_residual_plus_rounding_meets_target": true + }, + { + "specification": [ + 257, + 1, + 2, + 4, + 9, + 96 + ], + "target": 18, + "period": 258, + "holes": [ + 129 + ], + "gap": "1/16", + "boundary_bits": 21, + "coefficient_bits": 31, + "internal_bits": 39, + "word_bits": 93, + "error_terms": [ + "307582133172611051864883125688415504502789451219357998790545046727465968201995098308132911249493872/10576895500643977583230644909300453313966284185873304150214541494658542268084637396405396727965696607779221785583704659418889", + "1/1048576", + "130371/274877898977", + "1/1048576" + ], + "source_requests": 2314, + "source_setup": { + "weights": 257, + "kernels": 4, + "entries": 2314, + "weight_precision": 2159, + "kernel_error_bits": 228 + }, + "factor": { + "products": 492, + "divisions": 914, + "factor_records": 914, + "maximum_front": 2, + "peak_integer_bits": 79 + }, + "solve": { + "products": 1314, + "divisions": 1028, + "cleared_scratch_cells": 514, + "peak_integer_bits": 79, + "target_input_components": 516, + "target_output_components": 516, + "gather_components": 514, + "scatter_components": 514, + "output_roundings": 514, + "hole_copy_components": 2, + "answer_clear_components": 514, + "staging_clear_components": 516 + }, + "output_sha256": "78f927193573de52477292f226e8ec454dee23f7b78a0b00c03f7dacbe56b4ed", + "reference_hash": "1fea294c1f63d3a9ecbb5670ad7c2a7782eeb6e33cb1e0a95e9433bcaff3c6ac", + "final_grid_residual_certificate_meets_target": false, + "internal_residual_plus_rounding_meets_target": true + } + ], + "original_entries": 103717, + "dense_rhs_checks": 6, + "complete_rhs_checks": 24, + "controls": 11, + "small_gap_checks": 7 +} diff --git a/research/periodic-gaussian-uniform-solve/SOURCES.json b/research/periodic-gaussian-uniform-solve/SOURCES.json new file mode 100644 index 0000000000..0b2d63d170 --- /dev/null +++ b/research/periodic-gaussian-uniform-solve/SOURCES.json @@ -0,0 +1,144 @@ +{ + "schema_version": 1, + "base_commit": "ff3cc58e370d0f678e529246f8c73e8094e18fcf", + "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/certified-gaussian-recovery/NOTICE.md", + "usage": "input", + "git_blob": "5e3269b5afe5e11f044ffae45216c4731b42c7af", + "sha256": "10acae9e78402ca70c6afd0e8d6da8fefc0da519c646cf43d93f923aba85b86d" + }, + { + "path": "research/certified-gaussian-recovery/intervals.py", + "usage": "input", + "git_blob": "91d458865aa026bdf0d59653a4ecbfe3a178ecbc", + "sha256": "159d2a7d32a8cc7c8f56632a8ef127308b984a0a6753c9d6bdccacc6e7d6d4df" + }, + { + "path": "research/native-word-fft/NATIVE-BANDED-INVERSE.md", + "usage": "provenance", + "git_blob": "8be8f9922dd6762a64e1d9e2c348f03cb4a4cb8d", + "sha256": "1259b4242ebf6ac7f14bfe72e371afb8dc530b2755d1fd82228d9dc6f01634ba" + }, + { + "path": "research/native-word-fft/band_solve.py", + "usage": "provenance", + "git_blob": "f89869d591bc2bfd5e70c0df7c68bb9709569e73", + "sha256": "f4e4471679cc89bbb01ab0b26e807b0dacdc6188ab95ba924fc57243369407bb" + }, + { + "path": "research/periodic-gaussian-weighted-power-bound/PROOF.md", + "usage": "provenance", + "git_blob": "b228900378d8ed3419145795f7081657892d5dbb", + "sha256": "bfdd893b084a8f14b5df5d200a86c2da2a7530e99bcff9bba820687c1a599095" + }, + { + "path": "research/periodic-reference-rounded-inverse-service/PROOF.md", + "usage": "provenance", + "git_blob": "5bbf8d4e4105d36a61c59ab17f64ef5d8de4c40c", + "sha256": "f848d6295137b2a6c80350e085e5da6b3d55f9a8624a63af0bb3938bc7969bbc" + }, + { + "path": "research/pr4554-banded-inverse-check/README.md", + "usage": "provenance", + "git_blob": "896b1274add87e5291f19ba4278e1d147509d7de", + "sha256": "ad659594d027c7fb96ca5a76cfe8c13502eeb7fc8737ee5a6c018cb293878d09" + }, + { + "path": "research/rational-unitary-fft/CORE-PROOF.md", + "usage": "provenance", + "git_blob": "a491eb52da272a9168e3c2fe2a5339977a6b9e61", + "sha256": "f5052dfdb42c1f0ea1cc06ea6866300897766f5230ad309e362a93a3978ba911" + }, + { + "path": "research/rational-unitary-fft/engine.py", + "usage": "input", + "git_blob": "e9f2f2b08dc2bc4c646e47dca92059351ca89384", + "sha256": "9e36aee0835e6b1b62997433581f88b5a434ccab8ae43e5c25d1deaaf1ebf653" + }, + { + "path": "research/rational-unitary-fft/exact.py", + "usage": "input", + "git_blob": "aae41e6acfb2e5a4fafdd85727891eb746b57b42", + "sha256": "c9b89d7357210af69865690ba12e695366961f8b501a8fab9d0fefe3fb30c479" + }, + { + "path": "research/rational-unitary-fft/full.py", + "usage": "input", + "git_blob": "7f85ad1a89e81b7dfc6b54e7bd9547120e86d5d3", + "sha256": "1f42d5f2858564ffb320e54ba6aa29651025491569823e25006bf5862457b803" + }, + { + "path": "research/rational-unitary-fft/gaussian.py", + "usage": "input", + "git_blob": "52ad2e1d605f5f7d669234567c25bc087306dd44", + "sha256": "08155357fd39b5fd7959f51f1d205b6511b8577b51520d793c89f92368b399ab" + }, + { + "path": "research/rational-unitary-fft/gaussian_reference.py", + "usage": "input", + "git_blob": "92addfabde50655cea7ad5a84cca9cff5457adee", + "sha256": "ed4d0908646e391d4a0ea32c988a0301a1793a72294ac7058a664ed3283ca3c3" + }, + { + "path": "research/rational-unitary-fft/generator.py", + "usage": "input", + "git_blob": "d761d3c88b1685fb64d92d69f699b8218c9ec30f", + "sha256": "827ef9fe1bd664859995892b59843c390f7969c938fb7e1e6dc585c31a54b555" + }, + { + "path": "research/rational-unitary-fft/triangular.py", + "usage": "input", + "git_blob": "2bd8de01a7ac80de7e6b9f8252bc69d0e0a291e8", + "sha256": "46780d95ddebfed22e8f0c18565fe2e768250afa5beeb31f450292cc06f7ec11" + }, + { + "path": "research/periodic-gaussian-uniform-solve/vendor/solver.py", + "usage": "provenance", + "pin": "head:b97ef8a66d105478b6077d431d1f96e8fbcc7bb5:research/periodic-gaussian-uniform-solve/vendor/solver.py", + "git_blob": "f28d518d564561449ef237604381659bfc69474e", + "sha256": "17fc2aa62a542d20dc8da3cd7eccbe7dbed91394e4bdafdaff11d94c7d744580", + "upstream": { + "commit": "72269696a9c5ae5b1c0b469afdd3db08080635cf", + "path": "research/cyclic-band-gap-solver/solver.py", + "url": "https://github.com/aliromman/integer-mult-bounds/blob/72269696a9c5ae5b1c0b469afdd3db08080635cf/research/cyclic-band-gap-solver/solver.py" + } + }, + { + "path": "research/periodic-gaussian-uniform-solve/vendor/PROOF.md", + "usage": "provenance", + "pin": "head:b97ef8a66d105478b6077d431d1f96e8fbcc7bb5:research/periodic-gaussian-uniform-solve/vendor/PROOF.md", + "git_blob": "924929376c304d743a15e67aed2ac7712fd89892", + "sha256": "508fd707fcfe1490ee3de0047b7d4d699cf341d2d22dfce1ea297e16e9beebb9", + "upstream": { + "commit": "72269696a9c5ae5b1c0b469afdd3db08080635cf", + "path": "research/cyclic-band-gap-solver/PROOF.md", + "url": "https://github.com/aliromman/integer-mult-bounds/blob/72269696a9c5ae5b1c0b469afdd3db08080635cf/research/cyclic-band-gap-solver/PROOF.md" + } + }, + { + "path": "research/periodic-gaussian-uniform-solve/vendor/README.md", + "usage": "provenance", + "pin": "head:b97ef8a66d105478b6077d431d1f96e8fbcc7bb5:research/periodic-gaussian-uniform-solve/vendor/README.md", + "git_blob": "7069589b9e84d5f9dfb30be2580deff6453b3a5b", + "sha256": "6e854c24947001682cded0ab95036305b719a2381d303551124aac0ff119400c", + "upstream": { + "commit": "72269696a9c5ae5b1c0b469afdd3db08080635cf", + "path": "research/cyclic-band-gap-solver/README.md", + "url": "https://github.com/aliromman/integer-mult-bounds/blob/72269696a9c5ae5b1c0b469afdd3db08080635cf/research/cyclic-band-gap-solver/README.md" + } + } + ] +} diff --git a/research/periodic-gaussian-uniform-solve/TASK.json b/research/periodic-gaussian-uniform-solve/TASK.json new file mode 100644 index 0000000000..402c20cf15 --- /dev/null +++ b/research/periodic-gaussian-uniform-solve/TASK.json @@ -0,0 +1,99 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 7, + "base_commit": "ff3cc58e370d0f678e529246f8c73e8094e18fcf", + "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": "Bind the actual narrow periodic Gaussian Reference family to a variable-gap cyclic direct solver with a complete original-coordinate error and cost contract.", + "scope_change_reason": "The fixed385-row direct consumer and abstract all-size cyclic solver leave source formation and arbitrary hole geometry separate. This contribution proves and implements that interface without a fixed gap floor.", + "bottleneck_link": "Turns a synthetic cyclic-band theorem into an actual Reference consumer, with source quantization, holes, final precision and analytic perturbation charged.", + "budget_minutes": 75, + "stop_rule": "Stop at the source-bound all-parameter consumer and exact source evidence. Do not claim parameter funding for a production family, physical tapes or complete kappa.", + "outcome": "completed", + "evidence": "PROOF.md, consumer.py, verify.py, RESULT.json", + "author": "Ali Romman", + "ai_assistance": "Substantial OpenAI Codex assistance for proof, implementation, verification and publication. No independent human or proof-kernel review.", + "open_questions": [ + { + "question": "Which production parameter policy funds the analytic Reference gap/error gate and pays coefficient generation together with physical delivery?", + "why_it_matters": "The consumer theorem supplies no free coefficients or native tape tariff.", + "first_step": "Pin one actual caller policy, substitute its n, excess, alpha, widths, target and input radius into the four error terms and source setup invoice.", + "blocked_by": "Production parameter funding, source bit complexity and physical data movement remain separate." + } + ], + "canonical_discussion": "https://github.com/CrocSwap/integer-mult-bounds/discussions/4202#discussioncomment-19147343", + "selection": { + "mode": "handoff-first", + "source_prs": [ + 5159, + 5216, + 4554 + ] + }, + "overlap": { + "searched_at": "2026-10-23T14:06:20.520586+00:00", + "open_prs": { + "fetched_at": "2026-10-23T14:05:07.432839+00:00", + "complete_pagination": true, + "records": 317 + }, + "discussions": { + "fetched_at": "2026-10-23T14:06:20.316172+00:00", + "complete_pagination": true, + "records": 4503 + }, + "local_notes": 131, + "head_notes": 7091, + "limits": "Sparse omitted notes, arbitrary diffs and unpublished work." + } +} diff --git a/research/periodic-gaussian-uniform-solve/VALIDATION.md b/research/periodic-gaussian-uniform-solve/VALIDATION.md new file mode 100644 index 0000000000..7b5f90713e --- /dev/null +++ b/research/periodic-gaussian-uniform-solve/VALIDATION.md @@ -0,0 +1,43 @@ +# Validation record + +Prepared by Ali Romman with substantial OpenAI Codex assistance. Apache-2.0. +Base: `ff3cc58e370d0f678e529246f8c73e8094e18fcf`. +Runtime: CPython 3.12.13; standard library only. + +Both registered isolated, warning-strict normal and optimized commands pass +and reproduce RESULT.json. Eight actual source tuples cover source sizes +9 through 257, excesses 1 through 13, two Gaussian alpha values, halfwidths +2 through 4, and entry precisions 64 through 96. The target precisions are +12, 18 and 24. All 103,717 original matrix entries are checked. Twenty-four +complete signed complex RHS cases pass; six also match a separate pivoted +rational dense solution. Eleven malformed, geometry or funding controls +reject. Seven exact gap cases include a gap smaller than 2^-1000. + +The 258-row case uses a 257-row selected block, gap 1/16, 31 coefficient +bits, 39 internal bits, 492 factor products and 1,314 solve products. These +counts exclude the separately recorded source setup and boundary scans. +This is not a production benchmark or an improvement to the selected kappa. + +The original-H residual before final rounding, plus the known final rounding +and analytic terms, certifies the target for every finite test input. The +finally rounded residual divided by d is too loose in the 97- and 257-source +cases. RESULT.json records that diagnostic as false; it is not described as +a failed consumer target. Exact public outputs agree with truncation of the +independently residual-checked internal output. + +Four actual code mutations fail in normal and optimized mode, before receipt +comparison: omitted wrap entries fail the original-reference residual; +source-index scatter changes a hole; a fixed 16-bit gap floor fails small-gap +checks; and omitting analytic error accepts an unfunded source. Mutation +copies use the same authenticated source inputs. Package bytes are unchanged. + +An initial receipt check found a tuple/list serialization mismatch in the +specification field. The verifier now uses the same JSON list representation. +No mathematical value or validation threshold changed for that repair. + +The all-parameter implication is a written proof. The finite checks do not +validate production parameter funding, the analytic interval backend or a +physical tape. No Lean, Docker, independent human review, selected cold replay +or complete kappa calculation was run. The full-history wrapper is unpassed +in the shallow checkout; direct declared-pin ancestry is checked separately +for publication. No predecessor or selected-frontier file is edited. diff --git a/research/periodic-gaussian-uniform-solve/VERIFY.json b/research/periodic-gaussian-uniform-solve/VERIFY.json new file mode 100644 index 0000000000..f973926675 --- /dev/null +++ b/research/periodic-gaussian-uniform-solve/VERIFY.json @@ -0,0 +1,44 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/certified-gaussian-recovery/NOTICE.md", + "research/certified-gaussian-recovery/intervals.py", + "research/rational-unitary-fft/engine.py", + "research/rational-unitary-fft/exact.py", + "research/rational-unitary-fft/full.py", + "research/rational-unitary-fft/gaussian.py", + "research/rational-unitary-fft/gaussian_reference.py", + "research/rational-unitary-fft/generator.py", + "research/rational-unitary-fft/triangular.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 240, + "checks": "Actual Reference parameter family, every original matrix entry, original-coordinate residual, independent dense rational solve, gaps, holes, aliases, immutable input and exact source/receipt checks." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 240, + "checks": "Actual Reference parameter family, every original matrix entry, original-coordinate residual, independent dense rational solve, gaps, holes, aliases, immutable input and exact source/receipt checks." + } + ] +} diff --git a/research/periodic-gaussian-uniform-solve/consumer.py b/research/periodic-gaussian-uniform-solve/consumer.py new file mode 100644 index 0000000000..c59e84af11 --- /dev/null +++ b/research/periodic-gaussian-uniform-solve/consumer.py @@ -0,0 +1,111 @@ +"""Bind the narrow periodic Gaussian Reference to a cyclic direct solve. + +Ali Romman, with substantial OpenAI Codex assistance. Apache-2.0. +Source and classical solver credit is in README.md and SOURCES.json. +""" +from dataclasses import dataclass +from fractions import Fraction as Q +from pathlib import Path +import sys + +sys.path.insert(0, str(Path(__file__).resolve().parent / 'vendor')) +from solver import factor, solve, trunc, need + + +def dyadic_gap(gap): + gap = Q(gap) + need(0 < gap <= 1, 'positive source gap at most one required') + bits = 0 + while Q(1, 1 << bits) > gap: + bits += 1 + return Q(1, 1 << bits) + + +@dataclass(frozen=True) +class Prepared: + source_hash: str + selected: tuple + holes: tuple + period: int + bits: int + coefficient_bits: int + radius: Q + gap: Q + error_terms: tuple + factors: dict + source_requests: int + + +def prepare(reference, target=20, radius=1, boundary_bits=None): + need(type(target) is int and target >= 1 and type(radius) in (int, Q) and radius > 0, + 'positive target and rational radius required') + boundary_bits = target + 3 if boundary_bits is None else boundary_bits + need(type(boundary_bits) is int and boundary_bits >= target + 3, 'output grid is not funded') + d = dyadic_gap(reference.narrow_gap) + epsilon, radius = Q(1, 1 << target), Q(radius) + error = reference.errors['narrow'] + need(0 <= error < d, 'analytic reference error exceeds gap') + analytic = radius * error / (d * (d-error)) + need(analytic <= epsilon/4, 'analytic error is not funded') + n, width = reference.spec.source_size, reference.spec.source_halfwidth + count = 2*width + p = boundary_bits + while radius*count*Q(1, 1 << p)/d**2 > epsilon/4: + p += 1 + selected = tuple(reference.selected) + need(len(selected) == n and len(set(selected)) == n, 'selected coordinates must be distinct') + holes = tuple(reference.holes) + need(set(selected).isdisjoint(holes) and set(selected) | set(holes) == set(range(reference.target_size)), + 'complete coordinate partition required') + rows, requests = [], 0 + for i, row in enumerate(selected): + coefficients, mass = {}, Q(0) + for h in range(-width, width+1): + j = (i+h) % n + value = reference.entry('narrow', row, selected[j]).value + requests += 1 + need(value >= 0, 'source entries must be nonnegative') + if i == j: + need(value == 1, 'source diagonal must be one') + else: + mass += value + coefficients[j] = value.numerator * (1 << p) // value.denominator + need(mass <= 1-d, 'literal source row gap failed') + rows.append(coefficients) + for row in holes: + need(reference.entry('narrow', row, row).value == 1, 'hole diagonal must be one') + requests += 1 + factors = factor(rows, p, width, d, 2-d, radius, epsilon/4) + coefficient = radius*count*Q(1, 1 << p)/d**2 + output = Q(2, 1 << boundary_bits) + terms = (analytic, coefficient, factors['plan']['error'], output) + need(sum(terms) <= epsilon, 'complete error budget failed') + return Prepared(reference.description_hash, selected, holes, reference.target_size, + boundary_bits, p, radius, d, terms, factors, requests) + + +def execute(prepared, data): + """Use an unchanged Prepared object returned by prepare and borrow data.""" + p = prepared + need(type(data) is tuple and len(data) == p.period and all( + type(z) is tuple and len(z) == 2 and all(type(x) is int for x in z) + and sum(abs(x) for x in z) <= p.radius*(1 << p.bits) for z in data), + 'immutable complex grid input and radius required') + gathered = tuple(data[j] for j in p.selected) + answer, bill = solve(p.factors, gathered, p.bits) + shift = p.factors['plan']['bits']-p.bits + output = list(data) + try: + for j, z in zip(p.selected, answer): + output[j] = tuple(trunc(x, 1 << shift) for x in z) + result = tuple(output) + bill.update(target_input_components=2*p.period, target_output_components=2*p.period, + gather_components=2*len(p.selected), scatter_components=2*len(p.selected), + output_roundings=2*len(p.selected), hole_copy_components=2*len(p.holes), + answer_clear_components=2*len(p.selected), staging_clear_components=2*p.period) + return result, bill + finally: + for z in answer: + z[:] = [0, 0] + for j in range(len(output)): + output[j] = (0, 0) diff --git a/research/periodic-gaussian-uniform-solve/verify.py b/research/periodic-gaussian-uniform-solve/verify.py new file mode 100644 index 0000000000..10a9d69d92 --- /dev/null +++ b/research/periodic-gaussian-uniform-solve/verify.py @@ -0,0 +1,175 @@ +"""Check actual Gaussian sources, independent solves and complete residuals. + +Ali Romman, with substantial OpenAI Codex assistance. Apache-2.0. +""" +import argparse +import copy +from dataclasses import replace +from fractions import Fraction as Q +import hashlib +import json +from pathlib import Path +import random +import sys + +ROOT = Path(__file__).resolve().parent +REPO = ROOT.parents[1] +sys.path.insert(0, str(ROOT)) +from consumer import prepare, execute, dyadic_gap +from solver import solve, trunc + + +def need(value, message): + if not value: + raise ValueError(message) + + +def reject(call): + try: + call() + except (ValueError, TypeError): + return + raise ValueError('invalid input accepted') + + +def source(): + raw = {} + for row in json.loads((ROOT/'SOURCES.json').read_text())['files']: + if row['usage'] == 'input' or '/vendor/' in row['path']: + b = (REPO/row['path']).read_bytes() + need(hashlib.sha256(b).hexdigest() == row['sha256'], 'source byte mismatch') + raw[row['path']] = b + sys.path.insert(0, str(REPO/'research/rational-unitary-fft')) + from gaussian_reference import Reference + return Reference, raw + + +def dense_solve(matrix, rhs): + n = len(matrix) + a = [list(row)+[Q(x) for x in pair] for row, pair in zip(matrix, rhs)] + for k in range(n): + pivot = next(i for i in range(k, n) if a[i][k]) + a[k], a[pivot] = a[pivot], a[k] + value = a[k][k] + a[k] = [x/value for x in a[k]] + for i in range(n): + if i != k: + value = a[i][k] + a[i] = [x-value*y for x, y in zip(a[i], a[k])] + return [row[n:] for row in a] + + +def run(small): + Reference, raw = source() + specifications = [(9,1,1,2,2,64), (13,5,1,3,3,64)] + if not small: + specifications += [(31,1,2,3,4,80),(32,7,1,3,4,64),(65,13,2,3,5,80), + (97,1,2,4,6,80),(129,7,2,4,7,96),(257,1,2,4,9,96)] + rng = random.Random(52845315) + receipt, dense_checks, entries, controls = [], 0, 0, 0 + for index, spec in enumerate(specifications): + reference = Reference(raw, *spec) + target = (12,18,24)[index % 3] + p = prepare(reference, target) + n, period = spec[0], reference.target_size + before = repr(p.factors) + setup_caches = dict(weights=len(reference.weights), kernels=len(reference.kernel), entries=len(reference.entries), + weight_precision=reference.weight_precision, kernel_error_bits=reference.kernel_error_bits) + matrix = [[reference.entry('narrow',i,j).value for j in range(period)] for i in range(period)] + entries += period**2 + selected = tuple(reference.selected) + holes = set(reference.holes) + # This scans the literal matrix, not the consumer's sparse table. + for i in range(period): + need(matrix[i][i] == 1 and sum(abs(x) for j,x in enumerate(matrix[i]) if j!=i) <= 1-p.gap, + 'full original row gap') + for j in range(period): + if i in holes or j in holes: + need(matrix[i][j] == int(i==j), 'literal hole identity') + elif matrix[i][j]: + a,b = selected.index(i), selected.index(j) + need(min(abs(a-b), n-abs(a-b)) <= spec[3], 'literal cyclic support') + max_residual = Q(0) + output_digest = hashlib.sha256() + scale = 1 << p.bits + for trial in range(3): + if trial == 0: + data = tuple((scale if j%2 else -scale,0) for j in range(period)) + elif trial == 1: + data = tuple((0,scale if j in holes else -scale) for j in range(period)) + else: + data = tuple((a, rng.randint(-(scale-abs(a)), scale-abs(a))) + for a in (rng.randint(-scale,scale) for _ in range(period))) + saved = data + output,bill = execute(p,data) + need(data == saved and repr(p.factors) == before, 'borrowed input or factors changed') + need(all(output[j] == data[j] for j in holes), 'hole output changed') + need(bill['products'] <= 8*n*spec[3], 'solve count bound') + residual = max(sum(abs(sum(matrix[i][j]*Q(output[j][c],scale) for j in range(period)) + - Q(data[i][c],scale)) for c in (0,1)) for i in range(period)) + need(residual <= (2-p.gap)*sum(p.error_terms[1:]), 'original-reference residual envelope') + raw_answer, _ = solve(p.factors, tuple(data[j] for j in selected), p.bits) + raw_bits = p.factors['plan']['bits'] + fine = [[Q(x,scale) for x in z] for z in data] + for j,z in zip(selected,raw_answer): + fine[j] = [Q(x,1 << raw_bits) for x in z] + need(output[j] == tuple(trunc(x,1 << (raw_bits-p.bits)) for x in z), + 'public output differs from final grid rounding') + raw_residual = max(sum(abs(sum(matrix[i][j]*fine[j][c] for j in range(period)) + - Q(data[i][c],scale)) for c in (0,1)) for i in range(period)) + need(raw_residual/p.gap + p.error_terms[0] + p.error_terms[3] <= Q(1,1 << target), + 'independent residual plus final rounding target') + max_residual = max(max_residual,residual/p.gap) + if index < 2: + exact = dense_solve(matrix, [[Q(x,scale) for x in z] for z in data]) + distance = max(sum(abs(Q(output[i][c],scale)-exact[i][c]) for c in (0,1)) for i in range(period)) + need(distance <= sum(p.error_terms[1:]), 'independent dense solution') + dense_checks += 1 + output_digest.update(json.dumps(output).encode()) + need(p.source_requests == n*(2*spec[3]+1)+spec[1], 'complete source call bill') + receipt.append({'specification':list(spec),'target':target,'period':period,'holes':list(p.holes), + 'gap':str(p.gap),'boundary_bits':p.bits,'coefficient_bits':p.coefficient_bits, + 'internal_bits':p.factors['plan']['bits'],'word_bits':p.factors['plan']['word_bits'], + 'error_terms':[str(x) for x in p.error_terms], + 'source_requests':p.source_requests,'source_setup':setup_caches,'factor':p.factors['statistics'], + 'solve':bill,'output_sha256':output_digest.hexdigest(), + 'reference_hash':p.source_hash, + 'final_grid_residual_certificate_meets_target':max_residual < Q(1,1 << target), + 'internal_residual_plus_rounding_meets_target':True}) + if index == 0: + reject(lambda: execute(p,list(data)));controls+=1 + reject(lambda: execute(p,data[:-1]));controls+=1 + reject(lambda: execute(p,((scale+1,0),)+data[1:]));controls+=1 + reject(lambda: prepare(reference,target,boundary_bits=target));controls+=1 + for gap in (Q(0),Q(-1),Q(1)): + bad = copy.copy(reference);bad.narrow_gap=gap + reject(lambda: prepare(bad,target));controls+=1 + bad = copy.copy(reference);bad.errors={'narrow':Q(1)} + reject(lambda: prepare(bad,target));controls+=1 + bad = copy.copy(reference);bad.errors={'narrow':p.gap/4} + reject(lambda: prepare(bad,target));controls+=1 + bad = copy.copy(reference);bad._holes=() + reject(lambda: prepare(bad,target));controls+=1 + key=('narrow',selected[0],selected[1]);old=reference.entries[key] + reference.entries[key]=replace(old,value=-Q(1,8)) + try:reject(lambda: prepare(reference,target));controls+=1 + finally:reference.entries[key]=old + for e in (0,1,15,16,17,80,1000): + need(dyadic_gap(Q(3, 1 << (e+2))) == Q(1, 1 << (e+1)), 'no fixed gap floor') + return {'status':'PASS','fixtures':receipt,'original_entries':entries, + 'dense_rhs_checks':dense_checks,'complete_rhs_checks':3*len(specifications), + 'controls':controls,'small_gap_checks':7} + + +def main(): + ap=argparse.ArgumentParser();ap.add_argument('--small',action='store_true');ap.add_argument('--write-result',action='store_true') + args=ap.parse_args();result=run(args.small) + if not args.small: + if args.write_result:(ROOT/'RESULT.json').write_text(json.dumps(result,indent=2)+'\n') + else:need(result == json.loads((ROOT/'RESULT.json').read_text()), 'receipt differs') + print(json.dumps(result,sort_keys=True)) + print('PASS_PERIODIC_GAUSSIAN_UNIFORM_SOLVE') + + +if __name__=='__main__': + main()