petalas · Nov 3, 2026
diff --git a/research/frame-kernel-sparse-products/README.md b/research/frame-kernel-sparse-products/README.md
@@ -0,0 +1,186 @@
+# Sparse products for the complete frame-incidence replay
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+Claim type: scoped implementation-equivalence proof, exact operation-count
+certificate and local performance evidence. The new adapter removes
+**15,732,800 zero products** and **1,408,228 unit multiplications** from the
+complete pinned PR1668 replay. It retains every scientific check and produces
+identical scientific stdout. No mathematical result of PR1668 is claimed as
+new, audited or independently accepted here. No new kappa is claimed.
+
+The complete workload reaches 148 kernel calls and 353,069 dot products.
+The original contracts 17,141,028 coordinate pairs. The replacement sums
+1,408,228 selected coordinates and performs no scalar multiplication inside
+those dot products. Selection, validation, geometry, ranks and all other work
+remain paid by the measured process.
+
+## The replacement and its proof
+
+Let r be a binary incidence row and v an integer vector of equal width. Then
+
+```text
+sum_j r[j] v[j] = sum_(j with r[j]=1) v[j].
+```
+
+For each row, build its support once, then reuse it for the supplied kernel
+vectors in their original order. Both implementations return false at the
+first nonzero dot product, and true after the same final dot product. This
+proves equivalence for every valid call, including zero rows and empty vector
+lists. A zero coordinate contributes exactly zero; no rounding, modular
+reduction, approximate rank or altered mathematical premise is involved.
+
+The adapter validates its bounded binary-row/integer-vector domain. The pinned
+source supplies only this domain. This is a scoped replacement contract, not
+an equivalence for arbitrary iterators, side-effecting numeric objects,
+nonbinary rows or malformed inputs that the original zip might truncate.
+
+Only the fresh reference module's `kernel_ok` binding changes. Its main routine,
+fixtures, graph conditions, Fraction ranks, modular restore tests, certificate
+mutations and output formatting are unchanged. There is no persistent cache,
+reused result or skipped check. The SHA256 of the reference is checked before
+its bytes are compiled. Compilation explicitly uses `optimize=0`, including
+when the adapter runs under `-O`, so the retained assertions remain enabled.
+
+The scientific source remains byte-identical at
+`research/full-family-g-without-d/verify.py`, SHA256
+`2e45790da2cc2b2eea2e47900a94cadf7aa4a7d42a3d38390729cd9b409d73fb`.
+
+## Evidence
+
+`verify.py` compares the original, sparse and separately counted predicate at
+every reached call of the complete workload. Both full runs must finish and
+their entire stdout must agree. The scientific stdout SHA256 is
+`5ece3cdbfec55235c3d95cfcf7bae6448b31cc6b7d4504676c06a7200ec9ce4b`.
+The hash of the exact reached arguments and predicate results is
+`3df326c08d6f4b7eb7e811e6f3f67202c12b7836d42a75724b53128b674650e8`.
+These are implementation-conformance checks, not independent review of the
+scientific theorem or a new census of its objects.
+
+The operation counter follows the original row/vector short-circuit order.
+It enumerates 51,419 reached row scans and two false kernel calls, including
+the predecessor's damaged-certificate controls. Thus the claimed counts do
+not charge dots after a failure. No receipt is handwritten or trusted as an
+input; the verifier generates a report bound to every package file.
+
+All 55,987 combinations of a binary row and a ternary vector at widths zero
+through six also agree with literal dense arithmetic. Fourteen controls cover
+nonbinary values, ragged rows, vector dimensions/types, all three capacity
+bounds, empty predicates, a nonzero dot, altered/oversized source bytes and
+retained reference assertions under optimized execution.
+
+## Reproduce
+
+From the repository root, using CPython 3.12 and the standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/frame-kernel-sparse-products/replay.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/frame-kernel-sparse-products/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/frame-kernel-sparse-products/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/frame-kernel-sparse-products
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/frame-kernel-sparse-products --check-source-history
+```
+
+Other machines may substitute their absolute CPython 3.12 path. A sparse
+checkout must materialize both this package and `research/full-family-g-without-d`.
+`VERIFY.json` declares the sole scientific runtime input. The original README,
+catalogue and selected record are historical provenance pins in `SOURCES.json`.
+The direct conformance marker is `PASS_FRAME_KERNEL_SPARSE_PRODUCTS`.
+
+For a fresh-process end-to-end measurement:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/frame-kernel-sparse-products/benchmark.py --pairs 15
+```
+
+The benchmark times complete process creation, source authentication, reference
+compilation/initialization and the full main routine. It alternates the original
+kernel and sparse kernel with identical flags and no reused scientific state.
+Every process must exit zero with empty stderr and identical complete stdout.
+Timing is observational and is never a CI pass condition.
+
+## Local runtime
+
+Fifteen alternating fresh-process pairs on CPython 3.12.15, macOS arm64, give a **10.94%** median wall-time reduction. All fifteen pairs improve; all thirty complete outputs agree, with zero failures.
+
+| Version | Median seconds | Range seconds |
+| --- | ---: | ---: |
+| Original kernel | 1.801392 | 1.787448 to 1.983607 |
+| Sparse kernel | 1.604257 | 1.573416 to 1.769150 |
+
+The process runs on a shared 18-logical-CPU host. Its final load average was 2.96 / 3.06 / 2.45. Profiling was separate from reported timings. An initial seven-pair diagnostic overlapped one conformance run and was discarded; a later seven-pair observation had wider noise. The fifteen-pair serial run below is the published measurement, with no concurrent task-local replay or profiler. Other users and processes remained outside this task's control.
+
+| Pair | Original seconds | Sparse seconds |
+| ---: | ---: | ---: |
+| 1 | 1.797559208 | 1.574686667 |
+| 2 | 1.800518500 | 1.578095333 |
+| 3 | 1.787448333 | 1.584051208 |
+| 4 | 1.792102667 | 1.587584125 |
+| 5 | 1.800453875 | 1.604909792 |
+| 6 | 1.801391875 | 1.573415958 |
+| 7 | 1.792766666 | 1.585695583 |
+| 8 | 1.844230083 | 1.608174916 |
+| 9 | 1.821983042 | 1.649498250 |
+| 10 | 1.820826333 | 1.604256709 |
+| 11 | 1.804861750 | 1.769150084 |
+| 12 | 1.814463125 | 1.612519375 |
+| 13 | 1.791639083 | 1.668824833 |
+| 14 | 1.983606875 | 1.584959708 |
+| 15 | 1.833430208 | 1.744815625 |
+
+A separate baseline profile attributes 1.066 of 4.368 instrumented main-routine seconds to kernel products, about 24.4%. The observed wall-time reduction is below that ceiling. The separate candidate profile still spends 2.102 of 3.670 instrumented main-routine seconds in Fraction elimination. Fraction elimination remains the dominant unchanged cost; this optimization makes no rank arithmetic change. Profiles are diagnostics and their instrumented seconds are excluded from the wall-time comparison. The benchmark measures the whole direct replay, not CI setup, environment installation or the extra conformance runner. The time percentage is local evidence, not a portable speed guarantee or a claim that multiplication itself is faster.
+
+## Scope and credit
+
+Credit Josie Elliston / PR1668 for the full scientific replay, fixtures and
+mathematical result; PR1650 for its retained geometry and criterion execution;
+Andrey Mas / PR1560 for the incidence criterion; Aaron Wang / PR1649 for the
+selected-family boundary; and the retained Brett Halligan / PR1212,
+themilkman216 / PR968 and DreamingOfClouds / PR717 decoder lineage. Their files
+and notices remain unchanged. Sparse dot products are classical. The new
+contribution is this exact source-bound implementation and its complete-workload
+operation saving and runtime evidence.
+
+Canonical base is `7c49fe32c55de02c2c873655c804b16e4c3fef0a`, priorities
+revision eight, selected PR6030. The selected binding-only orientation passed.
+The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19370283)
+and `TASK.json` record the scope. Live overlap covered 506 open PR records and
+6,503 Discussion records. The helper searched 130 of 8,917 main-tree note
+records; distinctive Git-object and merged-PR searches supplemented that sparse
+coverage. Arbitrary historical diffs and unpublished work remain limits.
+
+No larger P105 timing, independent theorem audit, native supplier, physical
+caller, recursive invoice, selected-frontier improvement, proof-kernel review
+or complete multiplication theorem is supplied. All five selected framework
+assumptions remain. Selected cold replay, Lean and Docker are unrun.
+Independent human and formal proof-kernel review are unclaimed.
+
+## Implementation constraints
+
+New loops are bounded by 2,025 rows, 120 columns, eight kernel vectors,
+55,987 small fixtures, fourteen controls and at most twenty benchmark pairs.
+Each child process has a 120-second bound. Every new function is below sixty
+physical lines. Source reads stop after 65,537 bytes; package reads stop after
+one MiB plus a guard byte, with at most twelve files. Explicit exceptions remain
+enabled under `-O`; the scientific reference is deliberately unoptimized.
+
+Python managed allocation is a Power of Ten rule 3 deviation. The finite
+domains bound live matrices and support tuples; the authenticated scientific
+workload uses bounded integer coefficients. No fixed-allocation or arbitrary
+large-integer service claim is made. Rule 8's constrained dynamic-code deviation
+is the single fixed-hash reference program, compiled without edits. Its inherited
+frame enumeration has recursion bounded by eight levels; that frozen code is
+outside the new implementation. New call paths are acyclic. The verifier's
+one bounded comparison callback and stdlib dispatch are managed-runtime
+indirections. Warning-strict normal and optimized checks provide diagnostics.
+Build the Lever supplied the rerunnable adapter and counter; Prove It Works
+required full stdout and call equality; Explain the Number required complete
+alternating processes rather than a dot-product microbenchmark.
+
+## Open next questions
+
+Can a separately budgeted larger incidence replay benefit from this binary-row
+contraction? First profile one complete command and prove its replaced rows are
+binary. No larger workload, speed estimate or integration is supplied here.
+Stop after this first verified improvement; no rank or geometry optimization
+is included. Native and physical costs remain separate from verifier runtime.
diff --git a/research/frame-kernel-sparse-products/SOURCES.json b/research/frame-kernel-sparse-products/SOURCES.json
@@ -0,0 +1,30 @@
+{
+  "schema_version": 1,
+  "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+  "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": "research/full-family-g-without-d/README.md",
+      "usage": "provenance",
+      "git_blob": "50cb846dc47e238a3f751966555e52aae887f702",
+      "sha256": "4ebf92cebdf400ccd63a89d09376378be86bbe6fdb9f1565b39ddd234958d96c"
+    },
+    {
+      "path": "research/full-family-g-without-d/verify.py",
+      "usage": "input",
+      "git_blob": "15f65fa7ddf02f5907f00aa83f2bd52fbe0a8583",
+      "sha256": "2e45790da2cc2b2eea2e47900a94cadf7aa4a7d42a3d38390729cd9b409d73fb"
+    }
+  ]
+}
diff --git a/research/frame-kernel-sparse-products/TASK.json b/research/frame-kernel-sparse-products/TASK.json
@@ -0,0 +1,74 @@
+{
+  "schema_version": 1,
+  "task_id": "replay-runtime",
+  "priority_revision": 8,
+  "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+  "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": "Replace only PR1668 kernel_ok by support-index sums on its bounded binary incidence rows; prove exact predicate equivalence, enumerate removed scalar products and measure the complete unchanged replay.",
+  "scope_change_reason": "One isolated source-bound replay and one measured kernel-product bottleneck; this is implementation work rather than an audit or a new proof of the predecessor result.",
+  "bottleneck_link": "The adapter lowers the cost of an entire exact frame-incidence replay without changing any mathematical check. It supplies no supplier or kappa improvement.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop at the first complete output-equivalent speed improvement. Do not optimize ranks, geometry, frame enumeration, fixtures or controls.",
+  "outcome": "completed",
+  "evidence": "README.md proves the sparse integer predicate. verify.py compares every one of 148 reached kernel calls, the complete scientific stdout, 55987 small dot products and source/domain controls. benchmark.py times alternating fresh complete processes.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Can a separately budgeted larger incidence replay use this same binary-row contraction with a useful end-to-end saving?",
+      "why_it_matters": "The present result measures only the complete PR1668 workload; no P105 runtime is inferred.",
+      "first_step": "Profile one actual larger command and prove that every replaced row is binary before changing its execution.",
+      "blocked_by": "No source-bound larger workload or performance evidence is supplied here."
+    }
+  ],
+  "coordination": {
+    "source": "PR #1668",
+    "author": "JosieElliston",
+    "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19370283",
+    "base_checked": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+    "checked_utc": "2026-11-03T09:16:00Z",
+    "open_pr_records": 506,
+    "discussion_records": 6503,
+    "local_note_records": 130,
+    "head_note_records": 8917,
+    "limits": "Sparse local notes, arbitrary historical diffs and unpublished work are not completely covered; main-tree distinctive searches supplement the sparse helper.",
+    "predecessor_head": "5c959793a63332f54e7436cd8ded0e979774117e"
+  }
+}
diff --git a/research/frame-kernel-sparse-products/VERIFY.json b/research/frame-kernel-sparse-products/VERIFY.json
@@ -0,0 +1,36 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/full-family-g-without-d/verify.py"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Complete original/sparse predicate and stdout equality, exact operation counts, exhaustive small dots, source and capacity controls."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-O",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "The same complete conformance with optimized adapter; authenticated reference is compiled with optimize=0 and its assertion control must still reject."
+    }
+  ]
+}
diff --git a/research/frame-kernel-sparse-products/benchmark.py b/research/frame-kernel-sparse-products/benchmark.py
@@ -0,0 +1,65 @@
+"""Time alternating fresh processes; emit observations, never a timing gate.
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+"""
+
+import argparse
+import hashlib
+import json
+import os
+import platform
+import statistics
+import subprocess
+import sys
+import time
+from pathlib import Path
+
+HERE = Path(__file__).resolve().parent
+
+
+def run(baseline):
+    command = [sys.executable, "-I", "-W", "error", "-B", str(HERE / "replay.py")]
+    if baseline:
+        command.append("--baseline")
+    start = time.perf_counter_ns()
+    result = subprocess.run(command, capture_output=True, check=False, timeout=120)
+    elapsed = time.perf_counter_ns() - start
+    if result.returncode or result.stderr:
+        raise ValueError(f"replay failed: {result.returncode}, {result.stderr!r}")
+    if b"PASS_FULL_FAMILY_G_WITHOUT_D fixtures=2:" not in result.stdout:
+        raise ValueError("replay did not complete")
+    return elapsed, result.stdout
+
+
+def main():
+    parser = argparse.ArgumentParser(description=__doc__)
+    parser.add_argument("--pairs", type=int, default=7)
+    args = parser.parse_args()
+    if not 5 <= args.pairs <= 20:
+        raise ValueError("pairs must lie in 5..20")
+    results = {"baseline_ns": [], "candidate_ns": []}
+    expected = None
+    for _ in range(args.pairs):
+        for baseline, key in ((True, "baseline_ns"), (False, "candidate_ns")):
+            elapsed, output = run(baseline)
+            if expected is None:
+                expected = output
+            if output != expected:
+                raise ValueError("complete scientific stdout differs")
+            results[key].append(elapsed)
+    before = statistics.median(results["baseline_ns"])
+    after = statistics.median(results["candidate_ns"])
+    results.update(python=sys.version, platform=platform.platform(),
+                   cpu_count=os.cpu_count(), load_average=os.getloadavg(),
+                   order="baseline,candidate repeated", failures=0,
+                   median_reduction_percent=100 * (before - after) / before,
+                   scientific_stdout_sha256=hashlib.sha256(expected).hexdigest(),
+                   source_sha256=hashlib.sha256(
+                       (HERE.parent / "full-family-g-without-d" / "verify.py")
+                       .read_bytes()).hexdigest(),
+                   adapter_sha256=hashlib.sha256((HERE / "replay.py").read_bytes()).hexdigest())
+    print(json.dumps(results, indent=2, sort_keys=True))
+
+
+if __name__ == "__main__":
+    main()