Reduce complete rational-rank certificate time by 54.94% (no κ)

docs/research/rational-rank-certificates.md

@@ -27,6 +27,14 @@ nonpivot rows. The producer uses elimination; the checker only uses products,
 coordinate identities and the rank factorization. Empty kernels and rank zero
 have explicit valid certificates.
 
+The product checker clears row and column denominators and compares exact
+integer dot products. If a common denominator exceeds 16384 bits, it uses
+the original Fraction predicate for that product. Certificate contents and
+acceptance conditions are unchanged. The
+[implementation proof and complete-CLI benchmark](../../research/integer-rank-product-checks/README.md)
+retain the original interface and credit; the integer-product implementation
+was produced by Nick Petalas.
+
 The CLI binds the exact problem bytes by SHA-256. It accepts integers and
 rational strings, rejects duplicate JSON keys and floats, and uses the Python
 standard library. Limits are 64 rows and columns, input numerator/denominator

research/integer-rank-product-checks/README.md

@@ -0,0 +1,168 @@
+# Integer product checks for complete rational-rank certificates
+
+The complete rational-rank certificate produce/save/check path takes 54.94%
+less wall time on the retained dense 48-by-64 rank-eight rational fixture.
+This contribution was produced by Nick Petalas. Claim type: scoped exact-arithmetic
+implementation proof with finite conformance and local performance evidence.
+No new rank theorem, kappa, native supplier or selected-frontier change is claimed.
+
+The shared `scripts/certify_rational_rank.py` keeps the existing input and output
+formats, pivot selection, elimination, certificate serialization and exact
+acceptance predicates. It changes the four multiplication checks for the pivot
+minor inverse, rank factorization and complete right/left kernel bases. The
+proof below covers arbitrary valid rational matrices in the existing interface.
+Finite conformance is additional evidence, not an all-input exhaustive search.
+
+## Exact replacement
+
+For a left row x and right column y, let d and e be positive common
+denominators, with X=d*x and Y=e*y integral. For every rational target z,
+
+```text
+sum(x_t*y_t) = z
+if and only if
+sum(X_t*Y_t) * denominator(z) = numerator(z) * d * e.
+```
+
+The new checker computes d by successive least common multiples and constructs
+X exactly. It computes e and Y independently for each right column, then uses
+integer dot products and the displayed cross-multiplication. Positivity makes
+both implications valid. A zero inner dimension gives d=e=1 and the empty
+integer sum zero, so rank zero and empty kernels retain their previous meaning.
+
+The other checks still validate the same shapes, pivot-index sets, free-coordinate
+identity blocks and rational syntax. Thus the inverse product still proves the
+rank lower bound, the factorization still proves the upper bound, and the exact
+kernel products and identity blocks still establish the same complete bases.
+The producer and serialized result do not change. If several fields are invalid,
+the first error message can change because kernel products are now batched;
+all the original rejection predicates and CLI failure status remain.
+
+To bound common-denominator growth, a row whose running least common multiple
+exceeds 16384 bits declines the integer path. The corresponding product then
+uses the original exact Fraction dot-product predicate. This branch changes
+cost only; it neither accepts a false product nor rejects a true one. It avoids
+constructing the full scaled row for a large coprime denominator product.
+
+## Measured complete path
+
+Each timed bundle starts a fresh certificate producer, captures its complete
+JSON output, saves that output and starts a fresh `--check` process. Both
+processes must exit successfully, the checker must print its exact success
+marker, and every output hash must agree. The fixture is generated before timing;
+profiling is a separate untimed run. Imports, input parsing, elimination, all
+certificate checks, serialization, process startup, saved-file I/O and replay
+are inside the timed region. There are no skipped mathematical checks.
+
+Five alternating pairs on CPython 3.12.15, macOS 27.0.1 arm64, 18 logical CPUs:
+
+| Complete bundle | Median | Observed range |
+| --- | ---: | ---: |
+| Original | 440.23 ms | 434.41 to 461.09 ms |
+| Integer checks | 198.39 ms | 195.43 to 210.60 ms |
+
+Raw samples in milliseconds, in each side's observation order:
+
+```text
+original: 434.406917, 450.502708, 461.090000, 436.349834, 440.234625
+integer:  198.391583, 201.852167, 210.603875, 197.723625, 195.430375
+```
+
+All ten bundles and twenty CLI commands succeeded. All ten produced the
+certificate SHA256 `48b99c3926885f307aef55c25bfed6336fe8c734834b3ce9805b24f63be81f26`.
+The fixture JSON SHA256 is
+`914197cf63eeab2157e26ad92720418a7924d3811bdddf7c057fb29b9c5dbbd7`.
+The generated benchmark report binds the actual measured source files to SHA256.
+The machine was shared; the reported end load average was about 3.09 across
+18 logical CPUs. Pair order reverses on alternate pairs to spread host noise.
+
+The untimed profile attributes 0.503 of 0.572 profiled seconds in the original
+`certify` call to `verify`, including 697321 Fraction arithmetic dispatch calls.
+Those instrumented times locate the bottleneck; they are not the reported
+performance measurement. The measured complete-path reduction is below that
+fraction of time. Parsing, elimination and process startup still limit the gain.
+This is a local result for one synthetic interface fixture, not a universal
+speed guarantee or a production supplier replay benchmark.
+
+## Reproduce
+
+From the repository root, using CPython 3.12 and the standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/integer-rank-product-checks/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -O -W error -B research/integer-rank-product-checks/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/integer-rank-product-checks
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/integer-rank-product-checks --check-source-history
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B -m unittest discover -s tests -p test_research_rational_rank.py -v
+```
+
+Replace the absolute interpreter with another CPython 3.12 executable as needed.
+Both direct commands print `PASS_INTEGER_RANK_PRODUCTS` in a generated JSON
+receipt bound to package and implementation hashes. The registered replay also
+prints `PASS_REGISTERED_RESEARCH_PACKAGE`. It checks 591 complete certificate
+equalities, 802 exact product/false-product cases and 24 certificate rejections.
+The product cases include zero dimensions and explicit scale-limit fallbacks.
+Seven relevant unit tests also pass normally and with `-O`.
+
+For timing, provide an existing external scratch directory:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/integer-rank-product-checks/benchmark.py --scratch /absolute/external/scratch
+```
+
+This emits a generated source-bound report, two final saved certificates,
+the fixture and an untimed profile into that directory. It runs exactly five
+pairs. Timing is deliberately opt-in rather than a CI performance threshold.
+Registered commands contain only bounded correctness checks.
+
+## Scope, source and credit
+
+Ali Romman's [PR5789](https://github.com/CrocSwap/integer-mult-bounds/pull/5789)
+supplies the rational-rank interface, rank factorization, complete kernel
+certificates and separate product checker. The byte-identical original script
+is retained as `baseline.py`, including its original attribution. Its bytes
+are checked against the provenance pin at canonical main
+`2485805a6d47f36ea83ddde6327d453ac82d44dc`. Classical denominator clearing,
+Gaussian elimination and rank factorization retain their credit. The new
+application changes implementation cost, not their mathematical content.
+The parser dependency is a source-bound live input. The changed shared script
+is a declared replay input; the original script's source pin is provenance.
+
+The current `replay-runtime` card is refined to this implementation question.
+The selected-binding first example passed. Existing published rank values and
+predecessor scientific conclusions are premises, not the deliverable being
+audited. All five framework assumptions, physical delivery, caller, precision,
+stock and supplier admission obligations remain outside this change. No Lean,
+Docker, complete selected replay or independent human/kernel review is claimed.
+
+## Verification constraints
+
+The changed shared functions are at most 35 physical lines. All their loops
+inherit the validated 64-row/column bound. Certificate boundary validation
+and arithmetic equalities remain enabled under `-O`. There is no recursion,
+code generation, approximate arithmetic or cache of certificate decisions.
+The fallback preserves the previous exact arithmetic when scaling is too large.
+
+Power-of-Ten rule 3 has a managed-runtime deviation: Python allocates integers,
+Fractions and matrices during arithmetic. The finite CLI bounds and 16384-bit
+scale guard bound the new scaled representation. The parser still limits
+certificate rational strings to 4096 characters and inputs to 64-by-64; no
+fixed-capacity embedded implementation is claimed. Interpreter allocations
+and Fraction fallback cost are not statically allocated. Warning-strict direct,
+registered and unit-test commands provide the available language diagnostics;
+no static type checker is configured for this script. The benchmark's subprocesses
+have 120-second timeouts and fixed invocation counts; all outputs go outside
+the checkout. The literal frozen baseline remains unchanged.
+
+## Open next questions
+
+1. Does the complete-path improvement persist on a named interface search's
+   actual exported matrices? First export and source-bind one such matrix,
+   then reuse the paired CLI harness. The missing input is a declared caller
+   workload; the synthetic benchmark does not settle this question.
+2. Can the scale threshold follow from a fixed-capacity backend's proven
+   memory and arithmetic budget? Start with that backend's integer capacity.
+   No such backend contract is supplied here.
+
+The structured versions are in `TASK.json`. Apache-2.0. Independent human and
+formal proof-kernel review are unclaimed.

research/integer-rank-product-checks/SOURCES.json

@@ -0,0 +1,30 @@
+{
+  "schema_version": 1,
+  "base_commit": "2485805a6d47f36ea83ddde6327d453ac82d44dc",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a",
+      "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "scripts/certify_rational_rank.py",
+      "usage": "provenance",
+      "git_blob": "dcbd47f60f009a6402702d704e49ea1e6e1e252b",
+      "sha256": "a8416038115d638adc388c9bb66ee17d350f9a7e1712675a683d6a6f3e0590e7"
+    },
+    {
+      "path": "scripts/compare_recursive_invoices.py",
+      "usage": "input",
+      "git_blob": "fda2a852e9937e42fe40df0707694465ca7c1b48",
+      "sha256": "3930c22c11da7bc6042cfeb6e459ecb06e4478430037bee3469d034353855fc6"
+    }
+  ]
+}

research/integer-rank-product-checks/TASK.json

@@ -0,0 +1,76 @@
+{
+  "schema_version": 1,
+  "task_id": "replay-runtime",
+  "priority_revision": 8,
+  "base_commit": "2485805a6d47f36ea83ddde6327d453ac82d44dc",
+  "original_card": {
+    "id": "replay-runtime",
+    "question": "Can one measured replay bottleneck be sped up without dropping coverage?",
+    "starting_points": [
+      "scripts/run_isolated_tests.py",
+      "scripts/verify_replay_coverage.py",
+      "certificates/selected-result.json"
+    ],
+    "methods": [
+      "Profile one isolated replay and optimize the measured bottleneck.",
+      "Design source-bound reuse with explicit dependency invalidation and negative controls."
+    ],
+    "acceptance_gate": "Report before/after wall time on the same fixture, retained checks and invalidation behavior.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_selected_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.",
+      "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse."
+    },
+    "first_experiment": "Measure one unchanged fixture, preserve check coverage, and test one optimization with invalidation controls.",
+    "bottleneck_link": "Faster trustworthy replays increase review throughput and let mechanism candidates be checked sooner.",
+    "allowed_variations": [
+      "Profile one stage or design one source-bound cache boundary."
+    ],
+    "scope_change_triggers": [
+      "Skipping coverage or comparing different fixtures to claim speedup."
+    ],
+    "overlap_terms": [
+      "replay runtime",
+      "cache invalidation",
+      "isolated tests"
+    ]
+  },
+  "scope_status": "refined",
+  "actual_scope": "Accelerate the complete rational-rank certificate produce/save/check path by exact bounded denominator clearing in all four product checks.",
+  "scope_change_reason": "The replay-runtime card is refined to the PR5789 rank certificate interface and its bounded dense rectangular fixture; this is an implementation improvement, not a scientific audit.",
+  "bottleneck_link": "Exact interface searches require full rank and both kernel certificates. Faster complete certificate production and checking reduce that verification cost while retaining every certificate predicate.",
+  "budget_minutes": 60,
+  "stop_rule": "Ship the first measured full-path improvement after exact conformance and rejection checks. Do not extend to other consumers.",
+  "outcome": "completed",
+  "evidence": "591 complete certificate equalities, 802 rational product/mutant cases, 24 witness rejections and seven unit tests; five paired complete CLI bundles per side, twenty successful commands, byte-identical output and a local 54.94% median wall-time reduction. See README.md and the generated benchmark report.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Does this full-path improvement persist on an actual large interface-search workload with heterogeneous certificate denominators?",
+      "why_it_matters": "The retained fixture is dense and rational but synthetic; a broader production speed claim requires that workload.",
+      "first_step": "Export one source-bound interface matrix and run the unchanged paired CLI harness on it.",
+      "blocked_by": "A named consumer and its exact matrix export are not supplied here."
+    },
+    {
+      "question": "Can the 16384-bit scaling threshold be chosen from a proved allocation and arithmetic budget for a constrained backend?",
+      "why_it_matters": "The fallback preserves exact acceptance while the current threshold only bounds this Python fast path.",
+      "first_step": "Compare fixed-memory product algorithms under an explicit integer-capacity limit.",
+      "blocked_by": "No fixed-capacity runtime or whole-supplier resource contract is declared."
+    }
+  ],
+  "evidence_details": {
+    "complete_certificates": 591,
+    "rational_products_and_mutants": 802,
+    "certificate_rejections": 24,
+    "benchmark": "Five alternating fresh-process produce/save/check bundles per side; twenty successful CLI commands; identical serialized certificate hash. Raw timing arrays and profile attribution are retained in README.md.",
+    "local_python": "3.12.15",
+    "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19294774"
+  },
+  "claim_type": "Scoped exact-arithmetic implementation proof with finite conformance and a measured local 54.94% complete-CLI wall-time reduction."
+}

research/integer-rank-product-checks/VERIFY.json

@@ -0,0 +1,35 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "scripts/certify_rational_rank.py",
+    "scripts/compare_recursive_invoices.py"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Complete certificate equality, exact rational products, zero-dimensional factors and corrupted witnesses."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-O",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Same arithmetic and rejection checks with assertions disabled."
+    }
+  ]
+}