From afe5f0d86a51559075320ab392592dea16e8e247 Mon Sep 17 00:00:00 2001 From: Ali Romman <226877337+aliromman@users.noreply.github.com> Date: Fri, 23 Oct 2026 01:14:49 -0500 Subject: [PATCH 1/2] Use exact integer dot products in the downset replay --- research/downset-block-solve-bound/README.md | 42 +++++++++++++++++ research/downset-block-solve-bound/verify.py | 47 +++++++++++++++++--- 2 files changed, 82 insertions(+), 7 deletions(-) diff --git a/research/downset-block-solve-bound/README.md b/research/downset-block-solve-bound/README.md index 0b753c1b16..4192b1fc1d 100644 --- a/research/downset-block-solve-bound/README.md +++ b/research/downset-block-solve-bound/README.md @@ -239,3 +239,45 @@ The overlap helper covered 367 open PRs and 3,821 Discussion records at its HEAD notes; separate `git grep` searched all main package READMEs for the distinctive terms. No complete local-note inventory or novelty certificate is claimed. A canonical refresh after the first replay retained the same base. + +## 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`, this file 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. 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)) From 021affc49696b8a6fffbadae00f98e71f56920f7 Mon Sep 17 00:00:00 2001 From: Ali Romman <226877337+aliromman@users.noreply.github.com> Date: Fri, 23 Oct 2026 01:53:51 -0500 Subject: [PATCH 2/2] Preserve the frozen downset proof and separate runtime notes --- research/downset-block-solve-bound/README.md | 42 ------------------ research/downset-block-solve-bound/RUNTIME.md | 44 +++++++++++++++++++ 2 files changed, 44 insertions(+), 42 deletions(-) create mode 100644 research/downset-block-solve-bound/RUNTIME.md diff --git a/research/downset-block-solve-bound/README.md b/research/downset-block-solve-bound/README.md index 4192b1fc1d..0b753c1b16 100644 --- a/research/downset-block-solve-bound/README.md +++ b/research/downset-block-solve-bound/README.md @@ -239,45 +239,3 @@ The overlap helper covered 367 open PRs and 3,821 Discussion records at its HEAD notes; separate `git grep` searched all main package READMEs for the distinctive terms. No complete local-note inventory or novelty certificate is claimed. A canonical refresh after the first replay retained the same base. - -## 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`, this file 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. 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.