Reduce exact downset replay time with integer dot products

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.

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))