Speed rational-rank certificate generation with primitive integer pivots

docs/research/rational-rank-integer-pivots-benchmark.json

@@ -0,0 +1,47 @@
+{
+  "benchmark_sha256": "af75f07c4da859705ce9679b0dbfcc0e98852ecf127179479d9104fa1c751f5f",
+  "certificate_sha256": "4c0ef08a132525002271c5a6a0415c78efe681e0d37af2eaebf5dfa391d30e60",
+  "cpu_count": 16,
+  "fixture": {
+    "columns": 64,
+    "rank": 8,
+    "rows": 48
+  },
+  "medians_ns": {
+    "after": 673682500,
+    "before": 727398100
+  },
+  "pairs": 7,
+  "parser_sha256": "3930c22c11da7bc6042cfeb6e459ecb06e4478430037bee3469d034353855fc6",
+  "platform": "Windows-11-10.0.26300-SP0",
+  "problem_sha256": "914197cf63eeab2157e26ad92720418a7924d3811bdddf7c057fb29b9c5dbbd7",
+  "python": "3.12.10 (tags/v3.12.10:0cc8128, Apr  8 2025, 12:21:36) [MSC v.1943 64 bit (AMD64)]",
+  "samples_ns": {
+    "after": [
+      624360100,
+      658604900,
+      673682500,
+      683518700,
+      716061500,
+      689858500,
+      639098800
+    ],
+    "before": [
+      663245300,
+      713954900,
+      738263800,
+      727398100,
+      875404400,
+      734227900,
+      677459200
+    ]
+  },
+  "schema": "rational-rank-pivot-benchmark/v1",
+  "source_sha256": {
+    "after": "6fb4fe3be86fc996ae60ee764ae67c3d824947b6cae067f43e55ee8ac358f647",
+    "before": "c09b90259f43cab334e6e6f39b786a7960aee1935daa94a31f28d8c504bdbd0b"
+  },
+  "successful_cli_commands": 32,
+  "wall_time_reduction": 0.07384621983477824,
+  "warmup_bundles": 2
+}

docs/research/rational-rank-integer-pivots.md

@@ -0,0 +1,153 @@
+# Primitive integer pivots for rational-rank certificates
+
+The complete rational-rank generate/save/check path is **7.38% faster** in the
+local paired benchmark below: median 727.3981 ms becomes 673.6825 ms. The change
+replaces only pivot discovery's per-entry `Fraction` arithmetic with primitive
+integer rows. It retains the exact pivot policy and serialized certificates.
+This is a measured implementation improvement, not a new rank algorithm,
+supplier, exponent saving, or multiplication theorem.
+
+## Task, sources and overlap
+
+Started from canonical main
+`7c49fe32c55de02c2c873655c804b16e4c3fef0a`, priority revision 8. The
+`replay-runtime` card was selected using the verifier-engineering expertise
+override, nonce `3cf44b857eaf6b65fc973b72558b25c7`, scope key
+`b1dd41940c60d240b47a`. Scope is **refined** to the shared rank-certificate
+producer, with a stop rule of one measured full-path improvement preserving
+all existing checks. The selected binding-only orientation passed; it is not
+a scientific replay.
+
+Ali Romman's [PR5789](https://github.com/CrocSwap/integer-mult-bounds/pull/5789)
+supplies the exact rank, factorization and complete-kernel certificate interface.
+Nick Petalas's [PR6272](https://github.com/CrocSwap/integer-mult-bounds/pull/6272)
+already accelerates all four verification products. The present change acts on
+the remaining **forward pivot elimination**, not those product checks. The
+48-by-64 rank-eight benchmark fixture is reproduced from PR6272 with credit;
+the two reported speedups are not added together or compared across hosts.
+
+Before work, the live handoff thread #1166, onboarding #1163 and active
+Discussions were read. Targeted all-state PR-body searches covered `rational
+rank`, `certify_rational_rank`, and `rank`/`elimination`; a later open-PR search
+covered `rational-rank`. No matching pivot implementation was identified.
+`find_overlap.py --task replay-runtime --offline` explicitly reported incomplete
+local coverage (1 of 8,917 HEAD notes) and no remote cache; the authenticated
+GitHub connector and rendered Discussions supplied the bounded live checks.
+Hidden discussion items, arbitrary diffs and unpublished work are not covered.
+This is not a novelty certificate. No advance reservation was posted for this
+short session. Main was fetched again before publication and remained unchanged.
+
+The unchanged baseline source at the commit above has SHA-256
+`c09b90259f43cab334e6e6f39b786a7960aee1935daa94a31f28d8c504bdbd0b`.
+The exact parser dependency has SHA-256
+`3930c22c11da7bc6042cfeb6e459ecb06e4478430037bee3469d034353855fc6`.
+The benchmark receipt binds both compared sources and the harness. Frozen
+predecessor packages and selected-result files are unchanged.
+
+## Why the certificates are identical
+
+Clear each input row's denominators, then divide a nonzero integer row by the
+gcd of its entries. Each work row is a nonzero rational multiple of the
+corresponding row in the original forward elimination. This also makes sense
+for a zero row, which is left zero.
+
+Suppose the pivot row and another row are `s R` and `t S`, where `s,t` are
+nonzero rational numbers. Write their entries in the pivot column as `a,b`,
+with `a != 0`, and let `g = gcd(a,b)`. The new integer elimination is
+
+```text
+(a/g) (t S) - (b/g) (s R)
+  = (s t R[j]/g) (S - (S[j]/R[j]) R).
+```
+
+The coefficient is nonzero. Dividing the resulting nonzero row by its gcd
+preserves the invariant. A zero row remains zero; when `b=0`, both algorithms
+leave the row alone. All earlier pivot entries are already zero, so retaining
+only the tail and restoring the zero prefix is exact. Therefore both algorithms
+see the same zero pattern, take the same first available pivot in every
+column, and perform the same row swaps. Negative pivots require no special
+sign convention.
+
+The original matrix is untouched. Once pivot row/column indices are known,
+minor inversion, coefficient construction, both complete kernel bases,
+serialization and all verification predicates are unchanged. Consequently the
+complete certificate is identical for every accepted input, not merely its
+rank. Exact input-byte binding and damaged-certificate rejection remain active;
+there is no result cache or new invalidation rule.
+
+The existing interface permits at most 64 denominators of at most 10^9 per
+row. Thus the initial common denominator is below 2^1920. This observation
+bounds initial denominator clearing only; it is not a fixed-memory or universal
+runtime guarantee for intermediate elimination.
+
+## Evidence and reproduction
+
+On Windows 11 build 26300, CPython 3.12.10, 16 logical CPUs:
+
+- All eight rank unit tests pass normally and with isolated optimized Python.
+  The new test compares exact pivot choices and complete certificates for
+  154 matrices against the original Fraction pivot policy, including zero,
+  dependent, rectangular, signed, boundary-size and boundary-value cases.
+  Existing independent permutation-minor checks cover all 512 binary 3-by-3
+  matrices and 60 rational rectangular matrices; existing corruption and
+  exact input-byte rejection controls remain.
+- PR6272's unchanged conformance verifier passes normally and under `-O`:
+  591 complete certificate equalities, 802 product/mutation cases and 24
+  certificate rejections. These overlap some unit-test domains and are not
+  claimed as a disjoint census.
+- Seven alternating fresh-process timing pairs, after warming both complete
+  paths, all produce byte-identical certificates. All 32 CLI commands pass,
+  including warmups. Every timed bundle generates the certificate, saves it,
+  then verifies it in another process. All seven after measurements are below
+  their corresponding before measurements.
+
+Raw milliseconds, in pair order:
+
+```text
+before: 663.2453 713.9549 738.2638 727.3981 875.4044 734.2279 677.4592
+after:  624.3601 658.6049 673.6825 683.5187 716.0615 689.8585 639.0988
+```
+
+The [machine-readable receipt](rational-rank-integer-pivots-benchmark.json)
+retains exact nanoseconds, source/fixture/output hashes and environment.
+Windows stdout uses CRLF; certificate-byte hashes can differ on POSIX while
+the same-host before/after comparison must remain exact. The harness accepts
+either platform's success-line terminator.
+
+From the repository root, use Python 3.12+:
+
+```sh
+python -B -W error -m unittest discover -s tests -p test_research_rational_rank.py -v
+python -I -O -W error -B tests/test_research_rational_rank.py -v
+python -W error -B research/integer-rank-product-checks/verify.py
+python -O -W error -B research/integer-rank-product-checks/verify.py
+```
+
+To reproduce timing, save the exact original script outside the checkout and
+create an empty scratch directory. This Python command preserves source bytes
+on Windows and POSIX; substitute an actual external path for `/tmp/rank-before.py`:
+
+```sh
+python -c "import pathlib,subprocess; pathlib.Path('/tmp/rank-before.py').write_bytes(subprocess.check_output(['git','show','7c49fe32c55de02c2c873655c804b16e4c3fef0a:scripts/certify_rational_rank.py']))"
+python -B scripts/benchmark_rational_rank.py --before /tmp/rank-before.py --scratch /tmp/rank-benchmark
+```
+
+The opt-in benchmark writes only to the supplied scratch directory. It includes
+interpreter startup and file I/O; the improvement is specific to this synthetic
+fixture and host. No all-input speed claim, supplier cold replay, Lean proof,
+independent human review, or hosted CI success is asserted by these local checks.
+
+## Open next questions
+
+- Does the complete-path gain persist on a named consumer's exported matrices?
+  Pin one actual input and reuse the paired harness before making a production
+  throughput claim. Such a consumer workload is not supplied here.
+- How do high-rank matrices with unrelated denominators affect peak memory and
+  speed? First compare both exact implementations on a declared bounded family;
+  the current timing receipt establishes neither a worst-case bound nor a
+  fixed-capacity backend contract.
+
+Classical denominator clearing, Gaussian elimination and primitive-row
+normalization retain their usual credit. Prepared for
+`josecarlosgonzalezroque-design` with substantial OpenAI Codex assistance, one
+agent. Apache-2.0. Predecessor authors and their source notices are retained.

scripts/benchmark_rational_rank.py

@@ -0,0 +1,91 @@
+#!/usr/bin/env python3
+# SPDX-License-Identifier: Apache-2.0
+"""Compare complete rank-certificate CLI bundles against a saved source file.
+
+The dense rank-eight fixture is Nick Petalas's PR6272 fixture, using Ali
+Romman's PR5789 certificate interface. Prepared with OpenAI Codex assistance.
+Timing is opt-in, local evidence; outputs go only to --scratch.
+"""
+import argparse
+from fractions import Fraction
+from hashlib import sha256
+import json
+import os
+from pathlib import Path
+import platform
+import random
+import statistics
+import subprocess
+import sys
+import time
+
+ROOT=Path(__file__).resolve().parents[1]
+
+
+def fixture():
+    rng=random.Random(5789)
+    left=[[rng.randrange(-4,5) for _ in range(8)] for _ in range(48)]
+    right=[[rng.randrange(-4,5) for _ in range(64)] for _ in range(8)]
+    return {'schema':'rational-rank-problem/v1','matrix':[
+        [str(Fraction(sum(left[i][k]*right[k][j] for k in range(8)),
+                      2**(i%5)*3**(j%4))) for j in range(64)] for i in range(48)]}
+
+
+def bundle(script,problem,certificate,environment):
+    command=[sys.executable,'-B','-W','error','-X',
+             'pycache_prefix='+str(problem.parent/'bytecode'),str(script),str(problem)]
+    start=time.perf_counter_ns()
+    result=subprocess.run(command,env=environment,capture_output=True,timeout=120)
+    if result.returncode or result.stderr:
+        raise RuntimeError('Certificate production failed: '+repr(result.stderr))
+    certificate.write_bytes(result.stdout)
+    checked=subprocess.run(command+['--check',str(certificate)],env=environment,
+                           capture_output=True,timeout=120)
+    elapsed=time.perf_counter_ns()-start
+    if (checked.returncode or checked.stderr
+            or checked.stdout.splitlines()!=[b'PASS_RATIONAL_RANK_CERTIFICATE']):
+        raise RuntimeError('Saved certificate check failed: '+repr(checked.stderr))
+    return elapsed,sha256(result.stdout).hexdigest()
+
+
+def main():
+    parser=argparse.ArgumentParser(description=__doc__)
+    parser.add_argument('--before',required=True,type=Path,help='Unchanged baseline Python source')
+    parser.add_argument('--scratch',required=True,type=Path,help='Existing output directory')
+    args=parser.parse_args()
+    if not args.before.is_file() or not args.scratch.is_dir():
+        parser.error('--before must be a file and --scratch an existing directory')
+    scratch=args.scratch.resolve();before=args.before.resolve()
+    problem=scratch/'rank-problem.json'
+    problem.write_bytes(json.dumps(fixture(),sort_keys=True).encode('utf-8'))
+    scripts={'before':before,'after':ROOT/'scripts/certify_rational_rank.py'}
+    environment=dict(os.environ,PYTHONPATH=str(ROOT/'scripts'),PYTHONDONTWRITEBYTECODE='1')
+    environment.pop('PYTHONOPTIMIZE',None)
+    environment.pop('PYTHONPYCACHEPREFIX',None)
+    samples={side:[] for side in scripts};digests=set()
+    # Warm both complete paths; warmup times are excluded, hashes still checked.
+    for side,script in scripts.items():
+        _,digest=bundle(script,problem,scratch/(side+'-certificate.json'),environment)
+        digests.add(digest)
+    for pair in range(7):
+        for side in (('before','after') if pair%2==0 else ('after','before')):
+            elapsed,digest=bundle(scripts[side],problem,scratch/(side+'-certificate.json'),environment)
+            samples[side].append(elapsed);digests.add(digest)
+    if len(digests)!=1:
+        raise RuntimeError('Serialized certificates differ')
+    medians={side:statistics.median(values) for side,values in samples.items()}
+    report={'schema':'rational-rank-pivot-benchmark/v1',
+            'python':sys.version,'platform':platform.platform(),'cpu_count':os.cpu_count(),
+            'fixture':{'rows':48,'columns':64,'rank':8},'pairs':7,'warmup_bundles':2,
+            'successful_cli_commands':32,'samples_ns':samples,'medians_ns':medians,
+            'wall_time_reduction':1-medians['after']/medians['before'],
+            'problem_sha256':sha256(problem.read_bytes()).hexdigest(),
+            'certificate_sha256':next(iter(digests)),
+            'source_sha256':{side:sha256(path.read_bytes()).hexdigest() for side,path in scripts.items()},
+            'parser_sha256':sha256((ROOT/'scripts/compare_recursive_invoices.py').read_bytes()).hexdigest(),
+            'benchmark_sha256':sha256(Path(__file__).read_bytes()).hexdigest()}
+    (scratch/'benchmark.json').write_text(json.dumps(report,indent=2,sort_keys=True)+'\n',encoding='utf-8')
+    print(json.dumps(report,sort_keys=True))
+
+
+if __name__=='__main__':main()

scripts/certify_rational_rank.py

@@ -9,7 +9,7 @@
 from fractions import Fraction as Q
 from hashlib import sha256
 import json
-from math import lcm
+from math import gcd, lcm
 from pathlib import Path
 import re
 import sys
@@ -67,8 +67,20 @@ def inverse(a):
     return [row[n:] for row in rows]
 
 
-def certify(value):
-    a=validate(value);m,n=len(a),len(a[0]);work=[row[:] for row in a]
+def _pivot_minor(a):
+    """Choose the same pivots as rational elimination, using primitive rows.
+
+    Each work row is a nonzero rational multiple of the corresponding row
+    in ordinary elimination. Clearing denominators and dividing by the gcd
+    preserve that invariant, so zero tests and first-pivot choices agree.
+    Validated inputs have at most 64 denominators of at most 10^9 per row.
+    """
+    m,n=len(a),len(a[0]);work=[]
+    for row in a:
+        denominator=lcm(*(x.denominator for x in row))
+        values=[x.numerator*(denominator//x.denominator) for x in row]
+        divisor=gcd(*values)
+        work.append([x//divisor for x in values] if divisor else values)
     row_ids=list(range(m));chosen_rows=[];cols=[]
     for j in range(n):
         r=len(cols);pivot=next((i for i in range(r,m) if work[i][j]),None)
@@ -77,8 +89,18 @@ def certify(value):
         chosen_rows.append(row_ids[r]);cols.append(j)
         for i in range(r+1,m):
             if work[i][j]:
-                c=work[i][j]/work[r][j]
-                for k in range(j,n):work[i][k]-=c*work[r][k]
+                divisor=gcd(work[r][j],work[i][j])
+                p,c=work[r][j]//divisor,work[i][j]//divisor
+                tail=[p*work[i][k]-c*work[r][k] for k in range(j+1,n)]
+                divisor=gcd(*tail)
+                if divisor:tail=[x//divisor for x in tail]
+                work[i]=[0]*(j+1)+tail
+    return chosen_rows,cols
+
+
+def certify(value):
+    a=validate(value);m,n=len(a),len(a[0])
+    chosen_rows,cols=_pivot_minor(a)
     r=len(cols);inv=inverse([[a[i][j] for j in cols] for i in chosen_rows])
     coeff=[[sum((inv[k][l]*a[chosen_rows[l]][j] for l in range(r)),Q(0)) for j in range(n)] for k in range(r)]
     right=[]