Tooling: 1.71x faster exhaustive data-corner replay with identical receipts

research/data-corner-performance/CLAIM.json

@@ -0,0 +1,29 @@
+{
+  "track": "verification engineering",
+  "assignment_seed": 86,
+  "seed_source": "Python secrets.randbelow(100), operating-system randomness",
+  "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60",
+  "claimed_at": "2026-10-13T05:41:09.483991+00:00",
+  "expected_finish": "2026-10-13T06:15:00Z",
+  "candidates": [
+    "ternary-side common-pair DAG signature construction",
+    "partial-swap positive-label propagation",
+    "copied-fixed exhaustive data-corner elimination"
+  ],
+  "selection": "86 mod 3 = 2; data-corner elimination",
+  "object": "research/copied-fixed/data_corners.cpp",
+  "method": "Collect the nonzero active columns of each pivot row once, then use the same ordered columns for every lower-row update. Keep all assertions and the full triple-pair domain.",
+  "expected_deliverable": "Opt-in source-pinned optimization, same-input full-domain benchmarks, byte-identical receipts, negative controls and equivalence note. No new kappa.",
+  "coordination": "No pinned sprint issue exists; only open issue #650 requests Discussions. GitHub browser signed out and credential helper unavailable; local claim and patch handoff.",
+  "initial_overlap": "Read latest 100 updated PRs through #788, review ledger, negative-search inventory, and relevant PR154 bottleneck report. Existing tooling #707/#709/#721/#727/#736/#752/#756/#778/#779 targets different kernels. Search API filename queries returned zero and are not relied on as completeness evidence.",
+  "outcome": {
+    "status": "completed tooling improvement; preparing one focused PR",
+    "result": "README.md",
+    "evidence": "RESULT.json",
+    "speedup": 1.7098637444120486,
+    "full_domain_receipts": "byte-identical in all six alternating benchmark processes",
+    "resumed_at": "2026-10-13T11:25:05.197584+00:00",
+    "pause": "User interrupted after the initial work and resumed several hours later; measurements completed at approximately 06:01 UTC before the pause.",
+    "publication": "User authenticated GitHub as just-mn and explicitly confirmed one PR after the final overlap check."
+  }
+}

research/data-corner-performance/NOTICE.md

@@ -0,0 +1,35 @@
+# Attribution and license
+
+This contribution is under the repository's Apache-2.0 license.
+
+Prepared for Denis (@just-mn) with substantial OpenAI Codex assistance in implementation,
+experiment design, documentation and scoped AI review. No independent human
+review is claimed.
+
+The actual checker is the unchanged source at
+`research/copied-fixed/data_corners.cpp`, pinned in `SOURCE.json`. Its header
+credits Rohan Arun's PR39 geometry checker, James Chang's PR34 pivots, and
+OpenAI Codex assistance. Douglas R. Colkitt maintains the repository and its
+historical integration and verification infrastructure. This package retains
+the original source header in both generated compilation units.
+
+The historical source manifest `research/copied-fixed/SOURCE.json` records:
+
+- James Chang / jamesyc, PR34, `7fecbe3651e095fb0f450756afdeefd2a9ee80a2`:
+  reversed geometry and all-weight rank-cut identities.
+- Rohan Arun, PR39, `70ae24129649f6d6d4ec6360962a80c3c42a38f1`:
+  fixed-middle modular nonvanishing method.
+- Rohan Arun, PR40, `43f59ff533598762cbc43a5e14af2bbbc76fabbd`:
+  the contemporaneous both-fixed baseline.
+- The same manifest retains the broader construction and recovery lineage,
+  including Dominik Scholz, icekylinx, RaD / hipotures and Chafik Boukhalfa.
+
+eumemic's PR154 (`f571bcbd6e06618aeae0b8279da48060032dc74b`) identified this
+repeated historical workload as a verification bottleneck. That report is the
+profiling lead; this package introduces the per-pivot update-column optimization
+and imports no code from PR154 or any pending optimization PR.
+
+Recent tooling contributions #707, #709, #721, #727, #736, #752, #756, #778 and
+#779 improve distinct determinant, geometry, archive, footprint, inverse,
+Hermitian, Fano, Gram and reclamation kernels. They were checked for overlap;
+they are not dependencies or independent reviewers of this contribution.

research/data-corner-performance/OVERLAP.json

@@ -0,0 +1,131 @@
+{
+  "checked_at": "2026-10-13T05:52:08.462204+00:00",
+  "open_pr_count": 618,
+  "max_pr": 799,
+  "method": "REST pulls, seven pages at 100/page, updated descending; inspect titles/bodies for selected candidate keywords and latest tooling. Non-atomic snapshot, de-duplicated by number.",
+  "relevant": [
+    {
+      "number": 154,
+      "title": "Faster verification: concurrent checks, make verify-parallel, faster paired-cube frames, no joint-dual re-pins",
+      "html_url": "https://github.com/CrocSwap/integer-mult-bounds/pull/154",
+      "updated_at": "2026-10-09T07:37:04Z",
+      "head": "f571bcbd6e06618aeae0b8279da48060032dc74b"
+    },
+    {
+      "number": 47,
+      "title": "Hill-climbed producers for a conditional \u03ba = 4.105106623e-5 bound",
+      "html_url": "https://github.com/CrocSwap/integer-mult-bounds/pull/47",
+      "updated_at": "2026-10-08T15:05:44Z",
+      "head": "117caf164e3b235ef20188aa2dc1b49617e9255c"
+    },
+    {
+      "number": 44,
+      "title": "Weighted carrier matching: conditional \u03ba = 4.100629254e-5 > 2^-15",
+      "html_url": "https://github.com/CrocSwap/integer-mult-bounds/pull/44",
+      "updated_at": "2026-10-08T14:35:23Z",
+      "head": "1a21794eb5384db0e96d7bc2b11aa6f28cff7a85"
+    },
+    {
+      "number": 41,
+      "title": "Alternating pair-block networks for conditional \u03ba = 4.034168124 \u00d7 10\u207b\u2075 > 2\u207b\u00b9\u2075",
+      "html_url": "https://github.com/CrocSwap/integer-mult-bounds/pull/41",
+      "updated_at": "2026-10-08T13:46:27Z",
+      "head": "03bde70c0c2a453f1ceae20c619b602841405467"
+    },
+    {
+      "number": 35,
+      "title": "Fixed local bases in two stages for conditional \u03ba = 1.6631776e-5",
+      "html_url": "https://github.com/CrocSwap/integer-mult-bounds/pull/35",
+      "updated_at": "2026-10-08T12:37:15Z",
+      "head": "9c345a2a11e5f4f3649f7c68214bf9a2a0a3fe9c"
+    },
+    {
+      "number": 34,
+      "title": "Reversed two-stage basis and balanced assembly for conditional \u03ba = 1.639226629e-5",
+      "html_url": "https://github.com/CrocSwap/integer-mult-bounds/pull/34",
+      "updated_at": "2026-10-08T12:10:06Z",
+      "head": "7fecbe3651e095fb0f450756afdeefd2a9ee80a2"
+    },
+    {
+      "number": 33,
+      "title": "Compose smaller two-stage dimensions and data blocks for conditional \u03ba = 1.638103206e-5",
+      "html_url": "https://github.com/CrocSwap/integer-mult-bounds/pull/33",
+      "updated_at": "2026-10-08T11:49:21Z",
+      "head": "a499a345c040aa15b68e984a0904eadc485c7a7e"
+    },
+    {
+      "number": 31,
+      "title": "Exact data-corner certificates for conditional \u03ba = 1.5878574e-5 > 2^-16",
+      "html_url": "https://github.com/CrocSwap/integer-mult-bounds/pull/31",
+      "updated_at": "2026-10-08T11:37:30Z",
+      "head": "122e6453e80330633af701eabd1a6a72dfefd286"
+    },
+    {
+      "number": 29,
+      "title": "Two-stage controlled corners for a conditional 15536/10^9 > 2^-16 bound",
+      "html_url": "https://github.com/CrocSwap/integer-mult-bounds/pull/29",
+      "updated_at": "2026-10-08T11:20:11Z",
+      "head": "9d963275075fa98f1da821e27757b238dafd6b3c"
+    },
+    {
+      "number": 21,
+      "title": "Translated partial-swap frames for a conditional 5499/10^9 > 2^-18 bound",
+      "html_url": "https://github.com/CrocSwap/integer-mult-bounds/pull/21",
+      "updated_at": "2026-10-08T10:24:48Z",
+      "head": "5ba6cf0bfb68f2be8d15610e7972207c50254d6a"
+    },
+    {
+      "number": 17,
+      "title": "Compose nested geometry and smaller h30 producer for conditional \u03ba = 1.248342e-6 > 2^-20",
+      "html_url": "https://github.com/CrocSwap/integer-mult-bounds/pull/17",
+      "updated_at": "2026-10-08T10:04:07Z",
+      "head": "c915b4117626a512dd470adbdbd76963108f5cb3"
+    },
+    {
+      "number": 16,
+      "title": "Nested controlled bases for a conditional 9799/10^10 > 2^-20 bound",
+      "html_url": "https://github.com/CrocSwap/integer-mult-bounds/pull/16",
+      "updated_at": "2026-10-08T09:36:26Z",
+      "head": "a80f5e676c84b59def9791495df0655efe89a04f"
+    },
+    {
+      "number": 15,
+      "title": "Smaller h30 producer and full complex batching for conditional \u03ba > 2^-20",
+      "html_url": "https://github.com/CrocSwap/integer-mult-bounds/pull/15",
+      "updated_at": "2026-10-08T09:26:21Z",
+      "head": "a17cab396ce1c79c288bde9d06002cefdc0af8e6"
+    },
+    {
+      "number": 14,
+      "title": "Combine source frames and data corners for conditional kappa = 9.0799e-7",
+      "html_url": "https://github.com/CrocSwap/integer-mult-bounds/pull/14",
+      "updated_at": "2026-10-08T09:19:26Z",
+      "head": "1fa5b9a9aaccbebb3eb29ac7ea55811f46464eee"
+    }
+  ],
+  "conclusion": "No matching per-pivot data-corner update-list optimization found. PR154 is the credited profiling lead; related historical construction PRs are not new optimization dependencies.",
+  "final_refresh": {
+    "checked_at": "2026-10-13T11:23:38Z",
+    "open_pr_count": 693,
+    "highest_pr": 902,
+    "upstream_head": "f567884aeb8851b6e794af1184119a3bfbe1e631",
+    "execution_inputs_unchanged": true,
+    "new_tooling_reviewed": [
+      900,
+      898,
+      871,
+      865,
+      853,
+      849,
+      847,
+      841,
+      833,
+      824,
+      819,
+      818,
+      808,
+      797
+    ],
+    "conclusion": "New tooling concerns sparse fusion, Leech minors, joint frames, supplier receipts, dyadic arithmetic, cyclic routing, signed-sparse enumeration, stage pairs, gzip binding, RREF and reclamation. No matching data-corner update-list optimization found."
+  }
+}

research/data-corner-performance/PRELIMINARY.json

@@ -0,0 +1,26 @@
+{
+  "status": "preliminary sequential original-then-optimized probe; separate from alternating benchmark",
+  "compiler": "Apple clang 21.0.0 (clang-2100.3.34.2)",
+  "flags": [
+    "-O3",
+    "-std=c++17"
+  ],
+  "original": {
+    "wall_seconds": 167.98,
+    "user_seconds": 165.66,
+    "system_seconds": 0.94
+  },
+  "optimized": {
+    "wall_seconds": 98.78,
+    "user_seconds": 98.05,
+    "system_seconds": 0.45
+  },
+  "complete_stdout_equal": true,
+  "stdout_sha256": "82dc2d3e116fc003348d6e9ff0cce90fd70d3d6c156580b769ff3d38b3399e17",
+  "source_sha256": {
+    "research/copied-fixed/data_corners.cpp": "d134f43d31b896daf504511991be8608c6ba9d20a6606c57e2e12d4b203b7d44",
+    "research/copied-fixed/data-corners.json": "82dc2d3e116fc003348d6e9ff0cce90fd70d3d6c156580b769ff3d38b3399e17"
+  },
+  "optimized_source_sha256": "406a850d496589cd1216eb709baa84fdd8633048b648f05022ae184d1f279448",
+  "scope": "Full primary-prime checker; unchanged separate rational recovery excluded. Timings from /usr/bin/time -p; no cache flush."
+}

research/data-corner-performance/README.md

@@ -0,0 +1,131 @@
+# Exact data-corner replay with cached update columns
+
+**Tooling improvement; no new κ or construction claim.** This optional runner
+accelerates the historical `research/copied-fixed/data_corners.cpp` checker.
+It preserves the complete domain of 4,073,300 pairs of triples, every existing
+assertion, and the complete output receipt, including all ten modular failures.
+At the recorded base, the selected #626/#543 conditional result was
+κ = 51110230636731/31250000000000000 = 0.001635527380375392.
+
+## Reproduce
+
+Use Python 3.9+ on macOS or Linux and a C++17 compiler, from the repository root:
+
+```sh
+python3 -B research/data-corner-performance/replay.py --benchmark 3 --output /tmp/data-corner-result.json
+```
+
+Use an output path that does not exist. Expected final line:
+
+```text
+PASS_DATA_CORNER_REPLAY pairs=4073300 complete_receipts_equal=true
+```
+
+This compiles the pinned original and the optimized source, then runs three
+sequential pairs in alternating order. Each process replays the entire domain;
+every receipt field must equal the frozen predecessor receipt, and every run's
+stdout must be byte-identical. Timings are descriptive, with no pass threshold.
+Compilation and receipt comparison are outside the measured process interval.
+The interval includes process startup, computation, and captured output.
+OS caches are not flushed and other system activity is uncontrolled.
+
+For the faster complete replay alone, omit `--benchmark`. `CXX` selects the
+compiler; both variants use the same `-O3 -std=c++17` flags. The runner refuses
+changed source or receipt bytes and refuses a build with `NDEBUG` defined.
+No Python or C++ package dependencies are required.
+
+Focused controls:
+
+```sh
+python3 -B research/data-corner-performance/test_replay.py -v
+python3 -O -B research/data-corner-performance/test_replay.py -v
+```
+
+## Why the change is exact
+
+After accepting pivot `(i,c)`, the original loop removes `c` from `available`.
+For every lower row `r` with `M[r][c] != 0`, it scans all 47 columns, updating
+precisely those satisfying `available[j] && M[i][j] != 0`.
+
+Neither `available` nor pivot row `M[i]` changes during that lower-row loop:
+all writes have row index `r > i`. The new code collects this exact ordered
+column list once per pivot. Each lower row then performs the identical modular
+updates in the identical order, with the identical ratio, and clears the same
+pivot entry. By induction over rows and pivots, the matrices, pivot products,
+zero checks and first-failure positions agree. List construction occurs after
+the existing ordered-zero assertions and does not replace any of them.
+
+The pivot order is not natural column order. Eligible columns **left of the
+pivot must be included**. The separate `j > c` condition belongs only to the
+ordered-zero assertions. A regression embeds
+`[[2,1],[1,1]]` with pivot order `[1,0]`: the correct pivot product is −1 modulo
+1000003; deliberately omitting left-of-pivot updates gives +1 and is detected.
+Reversing the cached list is a positive control: distinct column updates
+commute, and both the receipt and complete final matrix remain equal.
+
+The additional stack array holds only 47 integers. The optimization removes
+repeated eligibility scans; it does not reuse a result across matrices, omit
+pairs, change the prime, or replace exact arithmetic with numerical arithmetic.
+
+## Evidence and coverage
+
+`RESULT.json` contains the measured compiler/platform, raw alternating samples,
+implementation/generated-source hashes, input pins, and coverage counters.
+`PRELIMINARY.json` retains the first same-input measurement separately.
+Three alternating process pairs on Apple clang 21.0.0 / macOS arm64 gave
+median wall times **169.198 s → 98.954 s (1.710× faster; 41.5% less time)**.
+Every stdout and stderr hash agreed. These measurements finished before the
+session pause; `VALIDATION.json` records the final checks after resuming.
+
+The full predecessor receipt covers:
+
+| Obligation | Count |
+|---|---:|
+| Triple pairs | 4,073,300 |
+| Primary-prime successes | 4,073,290 |
+| Primary-prime fallback records | 10 |
+| Nonzero pivot checks | 191,444,880 |
+| Ordered-zero checks | 1,409,360,440 |
+| Per-first-triple product records | 1,771 |
+
+Seven focused test groups compile the actual original and transformed C++
+elimination bodies in an eight-column harness. They compare complete final
+matrices and partial receipts on 48 seed-86 dense/sparse cases and each of eight
+failure positions. An independent Python determinant implementation uses
+natural-column elimination with row swaps and verifies successful products,
+including the sign of non-natural column permutations. These tests also cover
+the left-of-pivot mutation, valid reversed updates, invalid ordered zeros,
+repeated pivots, source and fixture drift, ambiguous transformation sites,
+disabled C++ assertions, and eight corruptions of proof-relevant receipt fields.
+This is finite differential validation plus a loop-equivalence argument, not a
+formal proof of the multiplication theorem.
+
+The ten primary-prime failures remain failures in this runner's output. The
+historical producer subsequently calls `data_recovery.py`, which verifies their
+47 ordered pivots over the rationals. That separate recovery is unchanged and
+is outside this optimization and its timing claims. No modular zero is called
+a rational counterexample.
+
+## Scope, provenance and handoff
+
+Base: `66849e1475c930fd7732b1a0067ffee7e1e95f60`.
+`SOURCE.json` pins the two execution inputs by SHA-256 and Git blob identity.
+The runner requires only this package and those two repository-relative files;
+it does not access the network or depend on Git during execution.
+
+`CLAIM.json` records OS-random seed 86, the three candidates, scope and overlap
+checks. There was no pinned coordination issue, so the claim is local. The user later
+authenticated GitHub and confirmed submission of one focused PR.
+A final overlap sweep covered 693 open PRs through #902; no matching optimization
+was found. After a user-requested pause, upstream was refreshed to
+`f567884aeb8851b6e794af1184119a3bfbe1e631`; both execution input blobs are unchanged there. Existing source
+packages, manifests, certificates, default targets and `upstream/` are unchanged.
+Only files in this directory are added.
+
+The selected supplier cold replay, whole-repository `make verify`, Lean, and
+remote CI were not rerun for this isolated opt-in historical checker. The
+all-size/compiler/common-label/hosting/residual/precision/tape/analytic
+assumptions remain. Measurements concern this finite checker, not the selected
+frontier or practical integer multiplication.
+
+See `NOTICE.md` for predecessor credit and AI disclosure.