diff --git a/research/downset-block-solve-bound/RUNTIME.md b/research/downset-block-solve-bound/RUNTIME.md new file mode 100644 index 0000000000..652f49ff5b --- /dev/null +++ b/research/downset-block-solve-bound/RUNTIME.md @@ -0,0 +1,44 @@ +# Exact product replay improvement + +Ali Romman, with substantial OpenAI Codex assistance, changed only the +matrix-product arithmetic and added direct product controls. Apache-2.0. +The proof, fixtures, inverse algorithm, original controls, source pins and +registered commands are unchanged. This work follows the remaining `mul` +question in [PR #4947](https://github.com/CrocSwap/integer-mult-bounds/pull/4947) +by Brian (JoyboyBrian). His inverse-cache result is separate work. At the +checked main `f259dabc7d70e0db8d6d36bfda888f008bbfecc1`, the checker still uses +the original inverse algorithm. The timings below compare those exact +main-branch bytes with this change; they do not compare against his cache. + +For row `i` of `A`, let `d_i` be the least common multiple of its entry +denominators. For column `j` of `B`, define `e_j` in the same way. Then + +```text +(AB)_ij = sum_k ((d_i A_ik)(e_j B_kj)) / (d_i e_j). +``` + +Both scaled factors are integers. The implementation forms integer dot +products and reduces one Fraction per output. It uses no cache or floating +point arithmetic. The denominator identity proves equality for the valid +rectangular rational matrices used here. Fixed matrix capacities still +apply; this is not an arbitrary-size performance guarantee. + +A separate literal Fraction dot-product oracle checks 90 signed, zero-row +and rectangular cases, including dimensions one and ten. Each case checks +input preservation, Fraction result types and independent output storage. +Three further controls check empty inputs, shape mismatch and zero output. +The receipt adds `product_controls: 93`. Every field in the original +`finite_evidence` object remains equal, including all rejection-witness +counts. No original check is skipped or cached. + +Local sequential CPython 3.12.13 trials on macOS measured full normal +replays of 19.488/21.431 seconds before and 16.765/16.696 seconds after, +before the small new product-control group was added. These are two trials +per version on a shared host, not a statistical or cross-platform guarantee. +A final sequential pair, including the new controls, measured 19.814 seconds +before and 16.715 seconds after (about 16% less time). Both registered +normal and optimized replays pass with identical original evidence. No new mathematical +bound, kappa change, compiler change or selected replay is claimed. + +The proof document remains byte-exact because `full-downset-allocation` +authenticates it as a frozen input. This runtime note is separate. diff --git a/research/downset-block-solve-bound/verify.py b/research/downset-block-solve-bound/verify.py index afe1d85d0c..0ef612a851 100644 --- a/research/downset-block-solve-bound/verify.py +++ b/research/downset-block-solve-bound/verify.py @@ -3,6 +3,7 @@ from fractions import Fraction as F from hashlib import sha256 from itertools import product +from math import lcm import json from pathlib import Path @@ -37,12 +38,16 @@ def transpose(a): def mul(a, b): require(bool(a) and bool(b) and len(a[0]) == len(b), 'product shape') out = zeros(len(a), len(b[0])) - for i, row in enumerate(a): - for k, value in enumerate(row): - if value: - for j, other in enumerate(b[k]): - if other: - out[i][j] += value * other + columns = list(zip(*b)) + row_scale = [lcm(*(x.denominator for x in row)) for row in a] + col_scale = [lcm(*(x.denominator for x in col)) for col in columns] + left = [[x.numerator * (scale // x.denominator) for x in row] + for row, scale in zip(a, row_scale)] + right = [[x.numerator * (scale // x.denominator) for x in col] + for col, scale in zip(columns, col_scale)] + for i, row in enumerate(left): + for j, col in enumerate(right): + out[i][j] = F(sum(x*y for x, y in zip(row, col)), row_scale[i]*col_scale[j]) return out @@ -377,12 +382,40 @@ def run(): return counts +def product_controls(): + checked = 0 + shapes = list(product((1, 2, 3), repeat=3)) + [(1, 10, 2), (10, 1, 10), (5, 10, 3)] + for rows, inner, cols in shapes: + for variant in range(3): + a = [[F(((i+1)*(k+2)+variant) % 7-3, 2+i+2*k) + for k in range(inner)] for i in range(rows)] + b = [[F(((k+2)*(j+1)+variant) % 5-2, 3+2*k+j) + for j in range(cols)] for k in range(inner)] + if variant == 0: + a[0] = [F(0)] * inner + before_a, before_b = [r[:] for r in a], [r[:] for r in b] + expected = [[sum((a[i][k]*b[k][j] for k in range(inner)), F(0)) + for j in range(cols)] for i in range(rows)] + actual = mul(a, b) + require(actual == expected, 'integer product differs from Fraction oracle') + require(a == before_a and b == before_b, 'product changed an input') + require(all(type(x) is F for row in actual for x in row), 'product result type') + actual[0][0] += 1 + require(mul(a, b) == expected, 'product result is not independent') + checked += 1 + rejected(lambda: mul([], [[F(1)]])) + rejected(lambda: mul([[F(1), F(2)]], [[F(1)]])) + require(mul([[F(0), F(0)]], [[F(2)], [F(3)]]) == [[F(0)]], 'zero product') + return checked + 3 + + def main(): + product_cases = product_controls() counts = run() root = Path(__file__).resolve().parent hashes = {name: sha256((root / name).read_bytes()).hexdigest() for name in FILES} print(json.dumps({'status': 'PASS_DOWNSET_BLOCK_SOLVE', 'claim_type': 'scoped proof', - 'finite_evidence': counts, 'source_sha256': hashes, + 'finite_evidence': counts, 'product_controls': product_cases, 'source_sha256': hashes, 'no_new_kappa': True}, sort_keys=True))