Tooling: 1.22x faster exact finite-bit block-core checks

research/finite-bit-rank-cache-seed87/CLAIM.md

@@ -0,0 +1,61 @@
+# Finite-bit repeated-transition rank cache
+
+Claim recorded 2026-10-14 03:05 UTC. Expected finish 03:37 UTC.
+Track: verification engineering. OS-random assignment seed: 87.
+Base: `680967accfd4311f3241dc154e1f434869747b43`.
+
+Investigate exact repeated frame-pair ranks inside
+`scripts/finite_bit_contract.py:inspect_candidate`. Intern normalized rational
+frames and reuse a rank only for an identical ordered pair within one call.
+Preserve validation, every physical edge, edge order and the full result.
+Deliver an opt-in source-pinned patch, complete same-input differential replay,
+failure controls and before/after measurements. Frozen scripts and certificates
+stay unchanged; this is verifier tooling, with no new kappa claim.
+
+Three candidates considered: repeated finite-bit edge ranks; Fano graph
+reachability; prime-subset exact arithmetic. The complete Fano profile spent
+0.305 of 0.430 profiled seconds in `inspect_candidate`. Prime-subset screening
+took 0.068 seconds and scalar Fano replay 0.008 seconds. The selected target
+has repeated work across larger rank-product and block-core fixtures too.
+Seed 87 fixes the rational perturbation/mutation test stream.
+
+Initial overlap: 719 open PRs with complete pagination, cached at 03:02 UTC;
+local package notes and review ledger; 83 discussion threads and their comments
+refreshed immediately before this claim. No pinned coordination issue exists,
+so this claim is local as requested. PR808 changes cyclic routing-state search,
+not exact edge-rank evaluation. PR1234 and PR1459/1461 address rational span
+normalization/containment, not this checker. No matching active claim found.
+Titles alone were not used: the repository overlap helper searched PR bodies,
+cached discussion comments/replies and local package metadata. Its live refresh
+timed out, so the direct discussion inventory supplied the freshness check.
+
+Acceptance: full receipt equality on unchanged Fano and nonzero rational
+rank-product/block-core fixtures; all existing relevant tests on both engines;
+invalid input and between-call mutation controls; same-input alternating-order
+wall-clock benchmark. No timing threshold is a mathematical acceptance rule.
+Stop implementation by 03:27 UTC, reserving the final ten minutes for checking
+and handoff. Contributor: Sagar Thakrar, with substantial OpenAI Codex assistance.
+
+## Result and release
+
+Completed 2026-10-14 03:26 UTC. [PR1584](https://github.com/CrocSwap/integer-mult-bounds/pull/1584)
+contains the opt-in adapter and exact replay. Research commit:
+`f1a8ff7d81f33621cc27b744e9eece5aea8bea94`. The final upstream refresh was
+`ddb4371c16a5a5de9e363afa8c0d6d7c27429e3c`; all 57 live inputs stayed unchanged.
+
+Nine alternating fresh-process pairs on Python 3.12.15 give median speedups
+1.2185x for both 64-dimensional block-core checks, 1.3864x for rank-product
+checks and 1.3503x for the complete Fano audit. The varied rational controls
+are about 2% slower. All complete receipts match, with digest
+`93acaade285fe35afc2a3ad87283c04c86d0a766d03e432dec738a60a8e52ca3`.
+Both engines pass all 53 existing tests on Python 3.12.15 and 3.14.8, eleven
+rejection controls and the mutate/restore check. Registered replay passes
+under inherited `PYTHONOPTIMIZE=2`; a worker invoked directly with `-O` fails.
+Metadata pins, Python 3.10 grammar, JSON and whitespace checks pass.
+
+Final overlap refresh covered 723 open PR bodies through PR1582 and 86
+discussion threads, 228 records including comments/replies with no pagination
+gaps. Only the distinct PR808 routing-state optimization matched the checker
+name. No matching active claim or pinned coordination issue was found.
+No selected cold replay, Linux execution, native compiler, hosting, precision,
+tape or analytic-interface proof was attempted. No new kappa. Scope released.

research/finite-bit-rank-cache-seed87/PORTABILITY.json

@@ -0,0 +1,105 @@
+{
+  "assignment_seed": 87,
+  "measurements": [
+    {
+      "cached": {
+        "rank_calls": {
+          "block_core": {
+            "calls": 360,
+            "eliminations": 63
+          },
+          "fano": {
+            "calls": 30,
+            "eliminations": 2
+          },
+          "rank_product": {
+            "calls": 914,
+            "eliminations": 117
+          },
+          "rational": {
+            "calls": 100,
+            "eliminations": 88
+          }
+        },
+        "seconds": {
+          "block_core": 3.9520934589672834,
+          "complete_fano_audit": 0.05631933402037248,
+          "fano": 0.020035666995681822,
+          "rank_product": 0.2659540000022389,
+          "rational": 0.019999415962956846
+        }
+      },
+      "order": [
+        "reference",
+        "cached"
+      ],
+      "reference": {
+        "rank_calls": {
+          "block_core": {
+            "calls": 764,
+            "eliminations": 63
+          },
+          "fano": {
+            "calls": 5532,
+            "eliminations": 2
+          },
+          "rank_product": {
+            "calls": 2869,
+            "eliminations": 117
+          },
+          "rational": {
+            "calls": 264,
+            "eliminations": 88
+          }
+        },
+        "seconds": {
+          "block_core": 4.770882459008135,
+          "complete_fano_audit": 0.05324716598261148,
+          "fano": 0.05275883403373882,
+          "rank_product": 0.323687499971129,
+          "rational": 0.018165000015869737
+        }
+      }
+    }
+  ],
+  "medians": {
+    "block_core": {
+      "cached_median_seconds": 3.9520934589672834,
+      "reference_median_seconds": 4.770882459008135,
+      "speedup": 1.2071785519603597
+    },
+    "complete_fano_audit": {
+      "cached_median_seconds": 0.05631933402037248,
+      "reference_median_seconds": 0.05324716598261148,
+      "speedup": 0.9454509167908537
+    },
+    "fano": {
+      "cached_median_seconds": 0.020035666995681822,
+      "reference_median_seconds": 0.05275883403373882,
+      "speedup": 2.633245703530092
+    },
+    "rank_product": {
+      "cached_median_seconds": 0.2659540000022389,
+      "reference_median_seconds": 0.323687499971129,
+      "speedup": 1.2170807732480207
+    },
+    "rational": {
+      "cached_median_seconds": 0.019999415962956846,
+      "reference_median_seconds": 0.018165000015869737,
+      "speedup": 0.9082765241502634
+    }
+  },
+  "platform": "macOS-26.5.2-arm64-arm-64bit-Mach-O",
+  "python": "3.14.8 (main, Sep 30 2026, 17:55:09) [Clang 21.0.0 (clang-2100.1.1.101)]",
+  "receipt_sha256": "93acaade285fe35afc2a3ad87283c04c86d0a766d03e432dec738a60a8e52ca3",
+  "scope": "Exact verifier tooling; no new kappa.",
+  "status": "PASS_FINITE_BIT_TRANSITION_CACHE",
+  "tests": {
+    "cached": {
+      "tests_run": 53
+    },
+    "reference": {
+      "tests_run": 53
+    }
+  }
+}

research/finite-bit-rank-cache-seed87/README.md

@@ -0,0 +1,142 @@
+# Exact finite-bit transition caching
+
+Verification tooling. No new kappa or construction is claimed.
+
+The retained finite-bit checker already caches exact elimination results, but
+still subtracts and hashes a rational matrix for every physical edge. The
+opt-in [adapter](adapter.py) interns normalized frames once per call and uses
+an integer pair to reuse an identical transition. Its nine-line replacement
+leaves all input, scalar, endpoint and deficit checks in place. Every physical
+edge still contributes its own charge, in its original position.
+
+Base commit: `680967accfd4311f3241dc154e1f434869747b43`.
+Final upstream refresh: `ddb4371c16a5a5de9e363afa8c0d6d7c27429e3c`;
+all 57 live inputs remain byte-identical to the research base.
+The selected record at that commit is PR1094's conditional
+`kappa = 836330098538459/500000000000000000`.
+[SOURCES.json](SOURCES.json) pins 57 live inputs and two provenance files by
+Git blob and SHA256. The original checker, frozen certificates and `upstream/`
+are unchanged. Loading fails if the checker's pinned source bytes differ.
+
+## Why the cache preserves the check
+
+Validation first converts every frame to an immutable tuple of exact
+`Fraction` entries. Python dictionary equality compares the complete tuple,
+including entries, so equal IDs imply equal matrices. A hash collision does
+not equate unequal keys. The key for an edge is its ordered source/sink ID
+pair. On the first occurrence, the unchanged expression computes
+`rank(sink - source)`. Every repeated pair has exactly the same difference
+matrix, hence the same rational rank. Appending that rank for every original
+edge preserves the complete edge-rank list, its sum and every returned field.
+
+Both dictionaries are local to one `inspect_candidate` call. A caller can
+change a frame between calls and must receive a newly checked result. The
+adapter caches no circuit validity or completed audit verdict. It uses the
+original arithmetic, including the existing bounded elimination cache.
+
+There are at most F frame keys and E transition keys for F frames and E edges.
+This adds O(F + E) references in the worst case. Workloads with few repeated
+frames need not benefit. The measurements are finite runtime evidence, not
+an asymptotic improvement or a formal proof of the multiplication theorem.
+
+## Reproduce
+
+From the repository root, with Python 3.12 and the standard library:
+
+```sh
+python3.12 -B scripts/research_package.py --package research/finite-bit-rank-cache-seed87
+```
+
+Expected result: `PASS_FINITE_BIT_TRANSITION_CACHE`. The command validates
+source pins, compares complete reference/cached receipts, and runs 53 existing
+tests under each engine. It does not write generated certificates.
+The registered replay also passes with `PYTHONOPTIMIZE=2` inherited by its
+driver. Child processes explicitly enable assertions, and directly launching a
+worker with `-O` fails. This retains assertions used by historical dependencies.
+
+For the benchmark, run:
+
+```sh
+python3.12 -B research/finite-bit-rank-cache-seed87/verify.py --pairs 9
+```
+
+Each engine runs in a fresh subprocess. Pair order alternates, and each
+fixture group starts with the inherited rank cache cleared. Timing includes
+normalization, scalar validation, all endpoints, the complete physical edge
+list and scoring. Fixture construction and process startup are excluded from
+the reported group times. The complete Fano audit is also timed separately.
+No wall-clock threshold controls acceptance.
+
+The fixed domain is all 15 Fano completion fixtures, all five existing
+rank-product controls, both existing 64-dimensional block-core controls, and
+12 rational-frame fixtures. The latter use seed 87, dimensions 2, 3, 4 and 8,
+and banks of 1, 3 and 17 frames, with signed numerators -3 through 3 and
+denominators 1 through 5. This is differential coverage, not a search for a
+stronger bound. The stopping rule is at most nine benchmark pairs.
+
+Eleven controls reject bad endpoints, a wrong permutation, an omitted scalar
+update, a float, a wrong dimension, repeated ports, a missing terminal, a zero
+denominator, equality submitted as a strict deficit, and two source-byte
+changes. A valid frame mutation changes the edge charges; restoring it recovers
+the original receipt. Reference and cached engines must agree on the full
+error class and message as well as accepted receipts.
+
+[BENCHMARK.json](BENCHMARK.json) records individual measurements, exact receipt
+digest, rank-call counts and environment. Every complete receipt is compared
+before it is reduced to a digest in that report. The existing test modules are
+listed explicitly in `verify.py`; no test is selected by a performance result.
+
+Nine alternating fresh-process pairs on macOS arm64, CPython 3.12.15:
+
+| Workload | Reference median | Cached median | Speedup |
+| --- | ---: | ---: | ---: |
+| Both 64-dimensional block-core controls | 4.6681 s | 3.8311 s | 1.2185x |
+| Five rank-product controls | 0.2614 s | 0.1885 s | 1.3864x |
+| Fifteen Fano frame checks | 0.0396 s | 0.0201 s | 1.9678x |
+| Complete Fano audit | 0.0724 s | 0.0536 s | 1.3503x |
+| Twelve varied rational-frame controls | 0.0181 s | 0.0184 s | 0.9809x |
+
+The last workload is about 2% slower, so this is not a universal speedup.
+For the Fano checks, rank-function calls fall from 5,532 to 30 while exact
+elimination misses remain two. Block-core calls fall from 764 to 360 with
+63 elimination misses in both engines. The benefit comes from avoiding repeated
+matrix construction and hashing, not from omitting a distinct elimination.
+Every pair produces the canonical full-receipt digest
+`93acaade285fe35afc2a3ad87283c04c86d0a766d03e432dec738a60a8e52ca3`.
+[PORTABILITY.json](PORTABILITY.json) records the same receipt and 53 tests per
+engine on CPython 3.14.8. Python 3.10 syntax parsing passes; execution on 3.10
+and Linux was not tested. The benchmark was not CPU-pinned or isolated from
+other host activity; individual samples remain in the report.
+
+## Credit and scope
+
+Douglas R. Colkitt authored the retained finite-bit contract, historical Fano,
+rank-product and block-core work used here. Their original sources and notices
+are preserved. This work is Sagar Thakrar's contribution, with substantial
+OpenAI Codex assistance in profiling, implementation, checking and writing.
+New work is Apache-2.0, the repository's license. No independent human review
+is claimed.
+
+Nearest parallel work: [4RchYMing's PR808](https://github.com/CrocSwap/integer-mult-bounds/pull/808)
+optimizes cyclic routing-state search;
+[Richard Hoekstra's PR1234](https://github.com/CrocSwap/integer-mult-bounds/pull/1234)
+optimizes rational span normalization and complements; CubeJerry's
+[PR1459](https://github.com/CrocSwap/integer-mult-bounds/pull/1459) and
+[PR1461](https://github.com/CrocSwap/integer-mult-bounds/pull/1461) optimize
+rational containment. Their methods and targets are separate from this per-call
+transition cache. Their source heads were inspected in the overlap check;
+none is a dependency of this adapter.
+
+This does not replay the selected supplier, its native compiler, hosting,
+precision, tape or analytic interface. All inherited conditional obligations
+remain. The added argument proves why identical transitions can reuse a rank;
+the finite replay checks implementation agreement on the declared fixtures.
+
+## Open next questions
+
+Should the retained checker adopt this cache? Review the replacement and repeat
+the same workload benchmark on Linux first. Adoption would require maintainer
+review and explicit migration of the six historical certificates that pin the
+original checker. There is no justification here to change the selected
+frontier or to optimize unrelated frame algorithms. [TASK.json](TASK.json)
+records the same bounded follow-up.