From f3f4ebdc0bd93d106a3acc17e857abfee81f3884 Mon Sep 17 00:00:00 2001 From: Wentao Li Date: Wed, 14 Oct 2026 13:33:43 +0000 Subject: [PATCH 1/2] =?UTF-8?q?Tooling:=203.58=C3=97=20faster=20joint-fram?= =?UTF-8?q?e=20product=20with=20identical=20receipts?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Clear denominators once per factor in audit_joint_frames.product, multiply with Python integers, and rebuild canonical Fractions. Positive-side experiment receipts stay fieldwise identical; only the rank-product certificate pin for audit_joint_frames.py changes. --- certificates/rank-product-core.json | 2 +- .../joint-frames-cleared-product/NOTICE.md | 19 + .../joint-frames-cleared-product/README.md | 108 +++ .../joint-frames-cleared-product/RESULT.json | 673 ++++++++++++++++++ .../joint-frames-cleared-product/SOURCES.json | 90 +++ .../joint-frames-cleared-product/TASK.json | 70 ++ .../joint-frames-cleared-product/VERIFY.json | 60 ++ .../joint-frames-cleared-product/baseline.py | 229 ++++++ .../joint-frames-cleared-product/benchmark.py | 175 +++++ .../joint-frames-cleared-product/verify.py | 260 +++++++ scripts/audit_joint_frames.py | 46 +- tests/test_joint_frames_cleared_product.py | 84 +++ 12 files changed, 1813 insertions(+), 3 deletions(-) create mode 100644 research/joint-frames-cleared-product/NOTICE.md create mode 100644 research/joint-frames-cleared-product/README.md create mode 100644 research/joint-frames-cleared-product/RESULT.json create mode 100644 research/joint-frames-cleared-product/SOURCES.json create mode 100644 research/joint-frames-cleared-product/TASK.json create mode 100644 research/joint-frames-cleared-product/VERIFY.json create mode 100644 research/joint-frames-cleared-product/baseline.py create mode 100644 research/joint-frames-cleared-product/benchmark.py create mode 100644 research/joint-frames-cleared-product/verify.py create mode 100644 tests/test_joint_frames_cleared_product.py diff --git a/certificates/rank-product-core.json b/certificates/rank-product-core.json index 63e8c3fa30..50694f7d22 100644 --- a/certificates/rank-product-core.json +++ b/certificates/rank-product-core.json @@ -6052,7 +6052,7 @@ "source_sha256": { "certificates/paired-network.json": "3b28a213059130bf683c3c70c57e083d90d2ffb0a401b8a50332b98b9ebb303f", "docs/research/rank-product-core.md": "1028abd145b367f94960264a874b847cdbeb3b4d84dd6d3a890fe4203922bd41", - "scripts/audit_joint_frames.py": "3df8061392ce0ba42bbde8c02f2a30c8141145e70e9a48c18da73d3aafb14423", + "scripts/audit_joint_frames.py": "818e86b4152b4eeb853f173c9aa795510caa593ec0e25b05a246f1df52575466", "scripts/audit_rank_product_core.py": "1471f17e86d6c02d5c288116cc3a53544c881ded47a3500f70dac97b366e46a7", "scripts/audit_stage_pair.py": "f4823525abb553f76ea33adf61ed51e88ec38dd6c346dbcac86f69ffa8fb0375", "scripts/experiments/rank_product_core.py": "7a91c1188c5d42e864a5d2e42397b09c435b526ae4f4210c44bf615de488708e", diff --git a/research/joint-frames-cleared-product/NOTICE.md b/research/joint-frames-cleared-product/NOTICE.md new file mode 100644 index 0000000000..c7c82cf449 --- /dev/null +++ b/research/joint-frames-cleared-product/NOTICE.md @@ -0,0 +1,19 @@ +# Notice + +This package accelerates Douglas R. Colkitt's exact rational matrix product in +`scripts/audit_joint_frames.py` while preserving the positive-side and +rank-product historical checkers. + +Predecessor credit: + +- Douglas R. Colkitt — joint-frame helpers, positive-side compiler, rank-product + core recovery and the historical certificates. +- Closest tooling priors on *different* objects: CrocSwap/integer-mult-bounds + PRs #756 (balanced-Fano packed replay), #1793 (inplace-side prefix), #1861 + (parity-side basis/contains), #1217 (ternary frame-pair memoization), and the + local modular-rank adapter in `research/joint-frame-modular-screen/`. + +Prepared by Wentao Li with substantial AI assistance under Apache-2.0. +No Cursor/Composer/Codex/model names are claimed as co-authors. This is not +independent human peer review and is not a formal proof of the multiplication +theorem. diff --git a/research/joint-frames-cleared-product/README.md b/research/joint-frames-cleared-product/README.md new file mode 100644 index 0000000000..8ab6d6ea8f --- /dev/null +++ b/research/joint-frames-cleared-product/README.md @@ -0,0 +1,108 @@ +# Faster exact joint-frame product with identical receipts + +**Tooling improvement; no new kappa.** At base +`0b1cccf86e2f5132ed286a26ef0a681a495740ea`, the historical positive-side audit +(`scripts/audit_positive_side.py`) builds cancellation-free side DAGs and checks +every physical frame transition for small signed label families. Profiling shows +most time in `scripts/audit_joint_frames.py:product`, which previously formed +each entry as a left-associated sum of `Fraction` multiplies (each multiply and +add reducing by GCD). + +This change clears denominators once per factor, multiplies with Python +integers, then rebuilds canonical `Fraction` entries. Empty left factors, +integer matrices, projector squares and every Boolean/arithmetical API besides +`product` are unchanged. Only the source pin for `scripts/audit_joint_frames.py` +changes inside the one certificate that binds that file +(`certificates/rank-product-core.json`). The positive-side certificate does not +pin `audit_joint_frames.py`; its mathematical payload is unchanged. + +## Reproduce + +Python **3.12**, standard library only, from the repository root: + +```sh +python3.12 -I -B research/joint-frames-cleared-product/verify.py +python3.12 -I -O -B research/joint-frames-cleared-product/verify.py +python3.12 -B scripts/research_package.py --package research/joint-frames-cleared-product +python3.12 -I -B research/joint-frames-cleared-product/benchmark.py --rounds 5 +``` + +Expected: + +```text +PASS_JOINT_FRAMES_CLEARED_PRODUCT positive_side_cases=12 random_cases=2500 certs=1 no_new_kappa +PASS_REGISTERED_RESEARCH_PACKAGE research/joint-frames-cleared-product outcome=completed +PASS_IDENTICAL_POSITIVE_SIDE_RECEIPTS +``` + +Default verify is read-only. Use `--write-certificate` only after editing the +production source. Full `make verify`, selected cold replay, Lean, and +multiplication-theorem obligations were not rerun for this isolated +historical-checker change. + +## Result + +On Linux / CPython 3.12.3 (Linux-6.12.94+-x86_64-with-glibc2.39), five alternating fresh-process pairs of the full +positive-side experiment stream gave median wall time +**26.143 → 7.302 seconds (3.58×)**. Timing is host-descriptive and is not a +correctness gate; all samples and environment pins are in +[RESULT.json](RESULT.json). Every experiment receipt matches the baseline +checker fieldwise (`side_roles`, `additions`, `dag_sha256`, invocation and frame +fields). Restoring the old `audit_joint_frames.py` pin recovers the base +rank-product certificate byte-for-byte after that single substitution. + +## Equivalence + +Write matrices \(A=(a_{ij}/d_{ij})\) and \(B=(b_{jk}/e_{jk})\) over \(\mathbb{Q}\). +Let \(D_A=\mathrm{lcm}(d_{ij})\) and \(D_B=\mathrm{lcm}(e_{jk})\). Form integer +matrices \(A'=D_A A\) and \(B'=D_B B\). Then + +\[ +(AB)_{ik}=\frac{(A'B')_{ik}}{D_A D_B}. +\] + +Canonical `Fraction` reduction of each right-hand entry matches the historical +entrywise `sum(x*y for ...)` result, including when \(D_A=D_B=1\) (pure integer +path). No modular or floating-point acceptance is used. + +## Open next questions + +1. **Question:** Can the same cleared-denominator pattern accelerate + `inverse` / `row_basis` on the joint-frame and ternary frame streams without + changing receipts? + **Why it matters:** Those helpers still allocate many intermediate + `Fraction`s on large ambient forms. + **First step:** Profile `verify_invocation_frames` for h=9 with the ternary + package’s baseline and time a cleared `inverse` prototype against receipt + equality. + **Blocked by:** Out of this session’s stop rule; `product` was the profiled + positive-side bottleneck. + +2. **Question:** Should rank-product and positive-side certificates both pin + `audit_joint_frames.py` going forward? + **Why it matters:** Only rank-product currently records that digest, so a + silent product drift would not bump the positive-side pin list. + **First step:** Add the pin in a dedicated provenance follow-up if maintainers + want symmetric coverage. + **Blocked by:** Provenance expansion is outside this tooling change. + +## Overlap and credit + +Closest priors (different objects): +[CrocSwap/integer-mult-bounds#756](https://github.com/CrocSwap/integer-mult-bounds/pull/756) +packed balanced-Fano replay; +[CrocSwap/integer-mult-bounds#1793](https://github.com/CrocSwap/integer-mult-bounds/pull/1793) +inplace-side prefix scan; +[CrocSwap/integer-mult-bounds#1861](https://github.com/CrocSwap/integer-mult-bounds/pull/1861) +parity-side basis/contains memoization; +[CrocSwap/integer-mult-bounds#1217](https://github.com/CrocSwap/integer-mult-bounds/pull/1217) +ternary frame-pair memoization; +local `research/joint-frame-modular-screen/` (modular *rank* screen for the +joint-frame certificate, not matrix product). +No competing open PR on cleared-denominator `product` at refresh. + +Douglas R. Colkitt authored the joint-frame helpers and positive/rank-product +side compilers. Prepared by Wentao Li +([VictorLiwentao](https://github.com/VictorLiwentao), +[@Is__Victor](https://x.com/Is__Victor)) with substantial AI assistance, under +Apache-2.0. diff --git a/research/joint-frames-cleared-product/RESULT.json b/research/joint-frames-cleared-product/RESULT.json new file mode 100644 index 0000000000..215e528950 --- /dev/null +++ b/research/joint-frames-cleared-product/RESULT.json @@ -0,0 +1,673 @@ +{ + "environment": { + "executable": "/usr/bin/python3.12", + "platform": "Linux-6.12.94+-x86_64-with-glibc2.39", + "python": "3.12.3 (main, Aug 31 2026, 10:18:26) [GCC 13.3.0]" + }, + "fixture": "scripts/audit_positive_side.py experiment stream (h,q) in {(4,2),(5,2),(4,4),(5,4),(6,4),(8,8)}", + "median_baseline_seconds": 26.143317678999665, + "median_optimized_seconds": 7.302057014000184, + "median_speedup_ratio": 3.5802675367879573, + "no_new_kappa": true, + "note": "Timing is host-descriptive and is not a correctness gate.", + "rounds": 5, + "samples": [ + { + "baseline_seconds": 25.99826523899992, + "optimized_seconds": 7.254153341999881, + "order": [ + "baseline", + "optimized" + ], + "pair": 0, + "rows": [ + { + "additions": 21, + "dag_sha256": "1c6d331e32d44f744f9b42df90e71550422b9675ac81c247cc508dff587c28a2", + "frames_transitions": null, + "h": 4, + "independent_roles": 60, + "q": 2, + "side_roles": 33, + "strategy": "balanced" + }, + { + "additions": 18, + "dag_sha256": "b8da858bf00688d73dd7b429f63d122a12004482a4b1d7bba6d8df9da959efd5", + "frames_transitions": 96, + "h": 4, + "independent_roles": 57, + "q": 2, + "side_roles": 30, + "strategy": "frequent-pairs" + }, + { + "additions": 77, + "dag_sha256": "85fba498650e21355c5963a66aee0b91c50b9964f3ed2d0767056b127322a5ea", + "frames_transitions": null, + "h": 5, + "independent_roles": 142, + "q": 2, + "side_roles": 97, + "strategy": "balanced" + }, + { + "additions": 50, + "dag_sha256": "ebfde085246538b7eb35acd3646e28a924e6b91e609e00164ae74b13ead3295d", + "frames_transitions": 230, + "h": 5, + "independent_roles": 115, + "q": 2, + "side_roles": 70, + "strategy": "frequent-pairs" + }, + { + "additions": 14, + "dag_sha256": "378c9c69a471046fa58f3cd0f15b61bf20e9b8bc0964ddc2e59f26cbee600938", + "frames_transitions": null, + "h": 4, + "independent_roles": 40, + "q": 4, + "side_roles": 22, + "strategy": "balanced" + }, + { + "additions": 12, + "dag_sha256": "6b10b517cd2032f05aa6e21a084a5646dd6124eb5c1470dfcfb7cf8b971ad3cc", + "frames_transitions": 64, + "h": 4, + "independent_roles": 38, + "q": 4, + "side_roles": 20, + "strategy": "frequent-pairs" + }, + { + "additions": 70, + "dag_sha256": "3a60ab87a926e4198823ed65bd94fd114b21d5cae7f03cb6388a310a0a99e7ee", + "frames_transitions": null, + "h": 5, + "independent_roles": 200, + "q": 4, + "side_roles": 110, + "strategy": "balanced" + }, + { + "additions": 60, + "dag_sha256": "d5dfbc6f59f6a2a31d5bb4bd9868647f8b941003ea9b77a32e1236229e3a8296", + "frames_transitions": 640, + "h": 5, + "independent_roles": 190, + "q": 4, + "side_roles": 100, + "strategy": "frequent-pairs" + }, + { + "additions": 1480, + "dag_sha256": "866a5fd77363c823e0fe5a9eaf1b5f912ae237ecb8e41a32dd8338f1f2bee6ca", + "frames_transitions": null, + "h": 6, + "independent_roles": 1869, + "q": 4, + "side_roles": 1600, + "strategy": "balanced" + }, + { + "additions": 960, + "dag_sha256": "eb3f75f921738797842a6eb21a91d9d2b293a803103716ae06500f48e400d450", + "frames_transitions": 4476, + "h": 6, + "independent_roles": 1349, + "q": 4, + "side_roles": 1080, + "strategy": "frequent-pairs" + }, + { + "additions": 1636, + "dag_sha256": "495fc442198158e8ca8bf3d8749fcb4248c3087a442d122b332a8368a954620a", + "frames_transitions": null, + "h": 8, + "independent_roles": 2036, + "q": 8, + "side_roles": 1764, + "strategy": "balanced" + }, + { + "additions": 1072, + "dag_sha256": "e1ed429b376fac109a340c1817e60386edaa67eec58fb6e8f55c9547592a8f69", + "frames_transitions": 6464, + "h": 8, + "independent_roles": 1472, + "q": 8, + "side_roles": 1200, + "strategy": "frequent-pairs" + } + ] + }, + { + "baseline_seconds": 26.243759324000166, + "optimized_seconds": 7.302057014000184, + "order": [ + "optimized", + "baseline" + ], + "pair": 1, + "rows": [ + { + "additions": 21, + "dag_sha256": "1c6d331e32d44f744f9b42df90e71550422b9675ac81c247cc508dff587c28a2", + "frames_transitions": null, + "h": 4, + "independent_roles": 60, + "q": 2, + "side_roles": 33, + "strategy": "balanced" + }, + { + "additions": 18, + "dag_sha256": "b8da858bf00688d73dd7b429f63d122a12004482a4b1d7bba6d8df9da959efd5", + "frames_transitions": 96, + "h": 4, + "independent_roles": 57, + "q": 2, + "side_roles": 30, + "strategy": "frequent-pairs" + }, + { + "additions": 77, + "dag_sha256": "85fba498650e21355c5963a66aee0b91c50b9964f3ed2d0767056b127322a5ea", + "frames_transitions": null, + "h": 5, + "independent_roles": 142, + "q": 2, + "side_roles": 97, + "strategy": "balanced" + }, + { + "additions": 50, + "dag_sha256": "ebfde085246538b7eb35acd3646e28a924e6b91e609e00164ae74b13ead3295d", + "frames_transitions": 230, + "h": 5, + "independent_roles": 115, + "q": 2, + "side_roles": 70, + "strategy": "frequent-pairs" + }, + { + "additions": 14, + "dag_sha256": "378c9c69a471046fa58f3cd0f15b61bf20e9b8bc0964ddc2e59f26cbee600938", + "frames_transitions": null, + "h": 4, + "independent_roles": 40, + "q": 4, + "side_roles": 22, + "strategy": "balanced" + }, + { + "additions": 12, + "dag_sha256": "6b10b517cd2032f05aa6e21a084a5646dd6124eb5c1470dfcfb7cf8b971ad3cc", + "frames_transitions": 64, + "h": 4, + "independent_roles": 38, + "q": 4, + "side_roles": 20, + "strategy": "frequent-pairs" + }, + { + "additions": 70, + "dag_sha256": "3a60ab87a926e4198823ed65bd94fd114b21d5cae7f03cb6388a310a0a99e7ee", + "frames_transitions": null, + "h": 5, + "independent_roles": 200, + "q": 4, + "side_roles": 110, + "strategy": "balanced" + }, + { + "additions": 60, + "dag_sha256": "d5dfbc6f59f6a2a31d5bb4bd9868647f8b941003ea9b77a32e1236229e3a8296", + "frames_transitions": 640, + "h": 5, + "independent_roles": 190, + "q": 4, + "side_roles": 100, + "strategy": "frequent-pairs" + }, + { + "additions": 1480, + "dag_sha256": "866a5fd77363c823e0fe5a9eaf1b5f912ae237ecb8e41a32dd8338f1f2bee6ca", + "frames_transitions": null, + "h": 6, + "independent_roles": 1869, + "q": 4, + "side_roles": 1600, + "strategy": "balanced" + }, + { + "additions": 960, + "dag_sha256": "eb3f75f921738797842a6eb21a91d9d2b293a803103716ae06500f48e400d450", + "frames_transitions": 4476, + "h": 6, + "independent_roles": 1349, + "q": 4, + "side_roles": 1080, + "strategy": "frequent-pairs" + }, + { + "additions": 1636, + "dag_sha256": "495fc442198158e8ca8bf3d8749fcb4248c3087a442d122b332a8368a954620a", + "frames_transitions": null, + "h": 8, + "independent_roles": 2036, + "q": 8, + "side_roles": 1764, + "strategy": "balanced" + }, + { + "additions": 1072, + "dag_sha256": "e1ed429b376fac109a340c1817e60386edaa67eec58fb6e8f55c9547592a8f69", + "frames_transitions": 6464, + "h": 8, + "independent_roles": 1472, + "q": 8, + "side_roles": 1200, + "strategy": "frequent-pairs" + } + ] + }, + { + "baseline_seconds": 26.2079586130003, + "optimized_seconds": 7.345162873999925, + "order": [ + "baseline", + "optimized" + ], + "pair": 2, + "rows": [ + { + "additions": 21, + "dag_sha256": "1c6d331e32d44f744f9b42df90e71550422b9675ac81c247cc508dff587c28a2", + "frames_transitions": null, + "h": 4, + "independent_roles": 60, + "q": 2, + "side_roles": 33, + "strategy": "balanced" + }, + { + "additions": 18, + "dag_sha256": "b8da858bf00688d73dd7b429f63d122a12004482a4b1d7bba6d8df9da959efd5", + "frames_transitions": 96, + "h": 4, + "independent_roles": 57, + "q": 2, + "side_roles": 30, + "strategy": "frequent-pairs" + }, + { + "additions": 77, + "dag_sha256": "85fba498650e21355c5963a66aee0b91c50b9964f3ed2d0767056b127322a5ea", + "frames_transitions": null, + "h": 5, + "independent_roles": 142, + "q": 2, + "side_roles": 97, + "strategy": "balanced" + }, + { + "additions": 50, + "dag_sha256": "ebfde085246538b7eb35acd3646e28a924e6b91e609e00164ae74b13ead3295d", + "frames_transitions": 230, + "h": 5, + "independent_roles": 115, + "q": 2, + "side_roles": 70, + "strategy": "frequent-pairs" + }, + { + "additions": 14, + "dag_sha256": "378c9c69a471046fa58f3cd0f15b61bf20e9b8bc0964ddc2e59f26cbee600938", + "frames_transitions": null, + "h": 4, + "independent_roles": 40, + "q": 4, + "side_roles": 22, + "strategy": "balanced" + }, + { + "additions": 12, + "dag_sha256": "6b10b517cd2032f05aa6e21a084a5646dd6124eb5c1470dfcfb7cf8b971ad3cc", + "frames_transitions": 64, + "h": 4, + "independent_roles": 38, + "q": 4, + "side_roles": 20, + "strategy": "frequent-pairs" + }, + { + "additions": 70, + "dag_sha256": "3a60ab87a926e4198823ed65bd94fd114b21d5cae7f03cb6388a310a0a99e7ee", + "frames_transitions": null, + "h": 5, + "independent_roles": 200, + "q": 4, + "side_roles": 110, + "strategy": "balanced" + }, + { + "additions": 60, + "dag_sha256": "d5dfbc6f59f6a2a31d5bb4bd9868647f8b941003ea9b77a32e1236229e3a8296", + "frames_transitions": 640, + "h": 5, + "independent_roles": 190, + "q": 4, + "side_roles": 100, + "strategy": "frequent-pairs" + }, + { + "additions": 1480, + "dag_sha256": "866a5fd77363c823e0fe5a9eaf1b5f912ae237ecb8e41a32dd8338f1f2bee6ca", + "frames_transitions": null, + "h": 6, + "independent_roles": 1869, + "q": 4, + "side_roles": 1600, + "strategy": "balanced" + }, + { + "additions": 960, + "dag_sha256": "eb3f75f921738797842a6eb21a91d9d2b293a803103716ae06500f48e400d450", + "frames_transitions": 4476, + "h": 6, + "independent_roles": 1349, + "q": 4, + "side_roles": 1080, + "strategy": "frequent-pairs" + }, + { + "additions": 1636, + "dag_sha256": "495fc442198158e8ca8bf3d8749fcb4248c3087a442d122b332a8368a954620a", + "frames_transitions": null, + "h": 8, + "independent_roles": 2036, + "q": 8, + "side_roles": 1764, + "strategy": "balanced" + }, + { + "additions": 1072, + "dag_sha256": "e1ed429b376fac109a340c1817e60386edaa67eec58fb6e8f55c9547592a8f69", + "frames_transitions": 6464, + "h": 8, + "independent_roles": 1472, + "q": 8, + "side_roles": 1200, + "strategy": "frequent-pairs" + } + ] + }, + { + "baseline_seconds": 26.143317678999665, + "optimized_seconds": 7.389878417000091, + "order": [ + "optimized", + "baseline" + ], + "pair": 3, + "rows": [ + { + "additions": 21, + "dag_sha256": "1c6d331e32d44f744f9b42df90e71550422b9675ac81c247cc508dff587c28a2", + "frames_transitions": null, + "h": 4, + "independent_roles": 60, + "q": 2, + "side_roles": 33, + "strategy": "balanced" + }, + { + "additions": 18, + "dag_sha256": "b8da858bf00688d73dd7b429f63d122a12004482a4b1d7bba6d8df9da959efd5", + "frames_transitions": 96, + "h": 4, + "independent_roles": 57, + "q": 2, + "side_roles": 30, + "strategy": "frequent-pairs" + }, + { + "additions": 77, + "dag_sha256": "85fba498650e21355c5963a66aee0b91c50b9964f3ed2d0767056b127322a5ea", + "frames_transitions": null, + "h": 5, + "independent_roles": 142, + "q": 2, + "side_roles": 97, + "strategy": "balanced" + }, + { + "additions": 50, + "dag_sha256": "ebfde085246538b7eb35acd3646e28a924e6b91e609e00164ae74b13ead3295d", + "frames_transitions": 230, + "h": 5, + "independent_roles": 115, + "q": 2, + "side_roles": 70, + "strategy": "frequent-pairs" + }, + { + "additions": 14, + "dag_sha256": "378c9c69a471046fa58f3cd0f15b61bf20e9b8bc0964ddc2e59f26cbee600938", + "frames_transitions": null, + "h": 4, + "independent_roles": 40, + "q": 4, + "side_roles": 22, + "strategy": "balanced" + }, + { + "additions": 12, + "dag_sha256": "6b10b517cd2032f05aa6e21a084a5646dd6124eb5c1470dfcfb7cf8b971ad3cc", + "frames_transitions": 64, + "h": 4, + "independent_roles": 38, + "q": 4, + "side_roles": 20, + "strategy": "frequent-pairs" + }, + { + "additions": 70, + "dag_sha256": "3a60ab87a926e4198823ed65bd94fd114b21d5cae7f03cb6388a310a0a99e7ee", + "frames_transitions": null, + "h": 5, + "independent_roles": 200, + "q": 4, + "side_roles": 110, + "strategy": "balanced" + }, + { + "additions": 60, + "dag_sha256": "d5dfbc6f59f6a2a31d5bb4bd9868647f8b941003ea9b77a32e1236229e3a8296", + "frames_transitions": 640, + "h": 5, + "independent_roles": 190, + "q": 4, + "side_roles": 100, + "strategy": "frequent-pairs" + }, + { + "additions": 1480, + "dag_sha256": "866a5fd77363c823e0fe5a9eaf1b5f912ae237ecb8e41a32dd8338f1f2bee6ca", + "frames_transitions": null, + "h": 6, + "independent_roles": 1869, + "q": 4, + "side_roles": 1600, + "strategy": "balanced" + }, + { + "additions": 960, + "dag_sha256": "eb3f75f921738797842a6eb21a91d9d2b293a803103716ae06500f48e400d450", + "frames_transitions": 4476, + "h": 6, + "independent_roles": 1349, + "q": 4, + "side_roles": 1080, + "strategy": "frequent-pairs" + }, + { + "additions": 1636, + "dag_sha256": "495fc442198158e8ca8bf3d8749fcb4248c3087a442d122b332a8368a954620a", + "frames_transitions": null, + "h": 8, + "independent_roles": 2036, + "q": 8, + "side_roles": 1764, + "strategy": "balanced" + }, + { + "additions": 1072, + "dag_sha256": "e1ed429b376fac109a340c1817e60386edaa67eec58fb6e8f55c9547592a8f69", + "frames_transitions": 6464, + "h": 8, + "independent_roles": 1472, + "q": 8, + "side_roles": 1200, + "strategy": "frequent-pairs" + } + ] + }, + { + "baseline_seconds": 25.635363176999817, + "optimized_seconds": 7.171803948999695, + "order": [ + "baseline", + "optimized" + ], + "pair": 4, + "rows": [ + { + "additions": 21, + "dag_sha256": "1c6d331e32d44f744f9b42df90e71550422b9675ac81c247cc508dff587c28a2", + "frames_transitions": null, + "h": 4, + "independent_roles": 60, + "q": 2, + "side_roles": 33, + "strategy": "balanced" + }, + { + "additions": 18, + "dag_sha256": "b8da858bf00688d73dd7b429f63d122a12004482a4b1d7bba6d8df9da959efd5", + "frames_transitions": 96, + "h": 4, + "independent_roles": 57, + "q": 2, + "side_roles": 30, + "strategy": "frequent-pairs" + }, + { + "additions": 77, + "dag_sha256": "85fba498650e21355c5963a66aee0b91c50b9964f3ed2d0767056b127322a5ea", + "frames_transitions": null, + "h": 5, + "independent_roles": 142, + "q": 2, + "side_roles": 97, + "strategy": "balanced" + }, + { + "additions": 50, + "dag_sha256": "ebfde085246538b7eb35acd3646e28a924e6b91e609e00164ae74b13ead3295d", + "frames_transitions": 230, + "h": 5, + "independent_roles": 115, + "q": 2, + "side_roles": 70, + "strategy": "frequent-pairs" + }, + { + "additions": 14, + "dag_sha256": "378c9c69a471046fa58f3cd0f15b61bf20e9b8bc0964ddc2e59f26cbee600938", + "frames_transitions": null, + "h": 4, + "independent_roles": 40, + "q": 4, + "side_roles": 22, + "strategy": "balanced" + }, + { + "additions": 12, + "dag_sha256": "6b10b517cd2032f05aa6e21a084a5646dd6124eb5c1470dfcfb7cf8b971ad3cc", + "frames_transitions": 64, + "h": 4, + "independent_roles": 38, + "q": 4, + "side_roles": 20, + "strategy": "frequent-pairs" + }, + { + "additions": 70, + "dag_sha256": "3a60ab87a926e4198823ed65bd94fd114b21d5cae7f03cb6388a310a0a99e7ee", + "frames_transitions": null, + "h": 5, + "independent_roles": 200, + "q": 4, + "side_roles": 110, + "strategy": "balanced" + }, + { + "additions": 60, + "dag_sha256": "d5dfbc6f59f6a2a31d5bb4bd9868647f8b941003ea9b77a32e1236229e3a8296", + "frames_transitions": 640, + "h": 5, + "independent_roles": 190, + "q": 4, + "side_roles": 100, + "strategy": "frequent-pairs" + }, + { + "additions": 1480, + "dag_sha256": "866a5fd77363c823e0fe5a9eaf1b5f912ae237ecb8e41a32dd8338f1f2bee6ca", + "frames_transitions": null, + "h": 6, + "independent_roles": 1869, + "q": 4, + "side_roles": 1600, + "strategy": "balanced" + }, + { + "additions": 960, + "dag_sha256": "eb3f75f921738797842a6eb21a91d9d2b293a803103716ae06500f48e400d450", + "frames_transitions": 4476, + "h": 6, + "independent_roles": 1349, + "q": 4, + "side_roles": 1080, + "strategy": "frequent-pairs" + }, + { + "additions": 1636, + "dag_sha256": "495fc442198158e8ca8bf3d8749fcb4248c3087a442d122b332a8368a954620a", + "frames_transitions": null, + "h": 8, + "independent_roles": 2036, + "q": 8, + "side_roles": 1764, + "strategy": "balanced" + }, + { + "additions": 1072, + "dag_sha256": "e1ed429b376fac109a340c1817e60386edaa67eec58fb6e8f55c9547592a8f69", + "frames_transitions": 6464, + "h": 8, + "independent_roles": 1472, + "q": 8, + "side_roles": 1200, + "strategy": "frequent-pairs" + } + ] + } + ], + "status": "PASS_IDENTICAL_POSITIVE_SIDE_RECEIPTS", + "warmup": 1 +} diff --git a/research/joint-frames-cleared-product/SOURCES.json b/research/joint-frames-cleared-product/SOURCES.json new file mode 100644 index 0000000000..c33567e8bb --- /dev/null +++ b/research/joint-frames-cleared-product/SOURCES.json @@ -0,0 +1,90 @@ +{ + "schema_version": 1, + "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea", + "files": [ + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "06c96f5579bb67ed1b86d334e78fbed7da6945f1", + "sha256": "6686ad58f1fbdbc87134a78901b60fd53a20d3984355e91defbbebc9e9fa8075" + }, + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "certificates/rank-product-core.json", + "usage": "provenance", + "git_blob": "63e8c3fa30871f6dc755f68d165e40f13e785e88", + "sha256": "e0d2cb39be3502251f8f8c4a62e0fe6b743be50eef41dda35646762daaec40b9" + }, + { + "path": "certificates/positive-side-core.json", + "usage": "provenance", + "git_blob": "b3698be4e8e62b8e994a60e801bc7ee4625b62ae", + "sha256": "06e53b6b1b70bfd84650d4c66ef2666c638b8b20690b5e50fe4e4fae72e2b966" + }, + { + "path": "docs/research/positive-side-core.md", + "usage": "provenance", + "git_blob": "ae16884ecd3d8364aa7d68c48756b0872f30600d", + "sha256": "fab9ff0ed8de56cb9c4c1587b65f956f706ab8f3b8afcb9212366218e227f49d" + }, + { + "path": "docs/research/rank-product-core.md", + "usage": "provenance", + "git_blob": "9b683864233d79b4d9d982a48bdefd1a1bc875d0", + "sha256": "1028abd145b367f94960264a874b847cdbeb3b4d84dd6d3a890fe4203922bd41" + }, + { + "path": "scripts/audit_joint_frames.py", + "usage": "provenance", + "git_blob": "913be4a1f0a651f3aaf7b4ed1901916918ba2cef", + "sha256": "3df8061392ce0ba42bbde8c02f2a30c8141145e70e9a48c18da73d3aafb14423" + }, + { + "path": "scripts/audit_positive_side.py", + "usage": "provenance", + "git_blob": "e3114282b1877cca386e19bdb4e259f62f68bf1b", + "sha256": "b021aad944d8a6c023e57b1b48937854803bbb370240c93e0fe359d831c838c9" + }, + { + "path": "scripts/audit_rank_product_core.py", + "usage": "provenance", + "git_blob": "62e1863c128d371af5a07ced80e13740d05979c8", + "sha256": "1471f17e86d6c02d5c288116cc3a53544c881ded47a3500f70dac97b366e46a7" + }, + { + "path": "scripts/experiments/positive_side_core.py", + "usage": "provenance", + "git_blob": "df3d6d565f2639482b959ecd26a5dffe27c8207f", + "sha256": "0d453ab7e869d2cf6a43d6865de82583edb390d3c75038271f0fc09e0f3828ba" + }, + { + "path": "scripts/experiments/rank_product_core.py", + "usage": "provenance", + "git_blob": "e5c093f467aa1edf1fea0e058ccc88806fbc09a1", + "sha256": "7a91c1188c5d42e864a5d2e42397b09c435b526ae4f4210c44bf615de488708e" + }, + { + "path": "scripts/experiments/signed_sparse_core.py", + "usage": "provenance", + "git_blob": "251bbd759fa6a5a1d05f1f25cf26586f9c695c91", + "sha256": "e20e038ef5c290d0ceeac49de1053a48e12f1052121063f6ff7227cde8b8b20e" + }, + { + "path": "tests/test_joint_frames.py", + "usage": "provenance", + "git_blob": "e5b42cd94e0234a2925cd143f2b760c4ea1b4b0e", + "sha256": "a34d1780213585a4fa490f7ecb1eba031120d61bc78bfc945a4638b68d7ef927" + }, + { + "path": "tests/test_positive_side_core.py", + "usage": "provenance", + "git_blob": "643a3020b9b6dbdf2230be7b9bb6c5a3ce2e637d", + "sha256": "46bd4173c6a3fd9295fc2682bf7f572161e95abc6c61e0859bb2f8eee7fb6319" + } + ] +} diff --git a/research/joint-frames-cleared-product/TASK.json b/research/joint-frames-cleared-product/TASK.json new file mode 100644 index 0000000000..43b4427193 --- /dev/null +++ b/research/joint-frames-cleared-product/TASK.json @@ -0,0 +1,70 @@ +{ + "schema_version": 1, + "task_id": "replay-runtime", + "priority_revision": 3, + "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea", + "chooser_seed": "79c3cf58a04ab05b039e968bb04812a5", + "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_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read the selected reproduction command and choose a single replay stage for profiling.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "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": "Can scripts/audit_joint_frames.py product be sped up for the historical positive-side audit (scripts/audit_positive_side.py on the six (h,q) experiment pairs) without changing any experiment receipt field, dag_sha256, invocation/frame evidence, or any certificate except the single audit_joint_frames.py source pin in certificates/rank-product-core.json?", + "scope_change_reason": "The catalogue card asks for one measured replay bottleneck with before/after wall time and retained checks. The OS-random recursive-interfaces draw (seed 560ea64f08df0bb946b45c68558f678e) landed on coverage-law / connector / centre-share cards that are saturated or deferred (centre-share, line-port). Expertise override selected verifier-engineering (seed 79c3cf58a04ab05b039e968bb04812a5). Profiling named audit_joint_frames.product inside positive_side_core.verify_frames / rank_product_core.check_core as the bottleneck on this fixed historical screen.", + "bottleneck_link": "Side result on review throughput: positive-side and rank-product certificates are part of verify-certificates. A faster identical replay does not change kappa or the binding complex supplier.", + "budget_minutes": 60, + "stop_rule": "Ship an equivalence-preserving product change with frozen baseline, identical positive-side experiment receipts, pin discipline on the one binding certificate, registered replay and a measured before/after median. Do not reopen the mathematical obstruction or run the selected cold frontier replay.", + "outcome": "completed", + "evidence": "PASS_JOINT_FRAMES_CLEARED_PRODUCT via research/joint-frames-cleared-product/verify.py (also under -O); PASS_IDENTICAL_POSITIVE_SIDE_RECEIPTS via benchmark.py; certificates/rank-product-core.json differs from base only in the audit_joint_frames.py source pin.", + "author": "Wentao Li", + "github": "VictorLiwentao", + "email": "wentaol4@illinois.edu", + "ai_assistance": "Substantial AI assistance for orientation, overlap search, profiling, implementation, packaging, benchmarking and writing. Not independent human peer review.", + "open_questions": [ + { + "question": "Can the same cleared-denominator pattern accelerate inverse / row_basis on the joint-frame and ternary frame streams without changing receipts?", + "why_it_matters": "Those helpers still allocate many intermediate Fraction objects on large ambient forms.", + "first_step": "Profile verify_invocation_frames for h=9 with the ternary package baseline and time a cleared inverse prototype against receipt equality.", + "blocked_by": "Out of this session's stop rule; product was the profiled positive-side bottleneck." + }, + { + "question": "Should rank-product and positive-side certificates both pin audit_joint_frames.py going forward?", + "why_it_matters": "Only rank-product currently records that digest, so a silent product drift would not bump the positive-side pin list.", + "first_step": "Add the pin in a dedicated provenance follow-up if maintainers want symmetric coverage.", + "blocked_by": "Provenance expansion is outside this tooling change." + } + ] +} diff --git a/research/joint-frames-cleared-product/VERIFY.json b/research/joint-frames-cleared-product/VERIFY.json new file mode 100644 index 0000000000..0f0d6fbaac --- /dev/null +++ b/research/joint-frames-cleared-product/VERIFY.json @@ -0,0 +1,60 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "scripts/audit_joint_frames.py", + "scripts/audit_positive_side.py", + "scripts/audit_rank_product_core.py", + "scripts/experiments/positive_side_core.py", + "scripts/experiments/rank_product_core.py", + "scripts/experiments/signed_sparse_core.py", + "certificates/rank-product-core.json", + "certificates/positive-side-core.json", + "docs/research/positive-side-core.md", + "docs/research/rank-product-core.md", + "tests/test_joint_frames.py", + "tests/test_positive_side_core.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 300, + "checks": "Exact baseline copy of the base-commit audit_joint_frames.py; identical product on 2500 random rational matrices plus edge cases; identical positive-side experiment receipts for all twelve (h,q,strategy) rows including dag_sha256; the rank-product certificate differs from base only in the audit_joint_frames.py source pin; scale-mutant foil rejected." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 300, + "checks": "Same equivalence and certificate discipline under -O (require() gates, not assert)." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "-m", + "unittest", + "discover", + "-s", + "tests", + "-p", + "test_joint_frames*.py", + "-v" + ], + "timeout_seconds": 180, + "checks": "Existing joint-frame unit tests plus focused cleared-product package controls." + } + ] +} diff --git a/research/joint-frames-cleared-product/baseline.py b/research/joint-frames-cleared-product/baseline.py new file mode 100644 index 0000000000..913be4a1f0 --- /dev/null +++ b/research/joint-frames-cleared-product/baseline.py @@ -0,0 +1,229 @@ +#!/usr/bin/env python3 +"""Exact rational-frame audit with fixed invocation boundaries; no new kappa.""" +from collections import Counter +from fractions import Fraction as Q +from functools import lru_cache +from itertools import combinations +from math import comb +from pathlib import Path +import json +import random + +from audit_cancellation import line_projection +from audit_fused_block import rational_rank +from certify import require, verify_sources +from paired_network import circuit +from prepare_layers import serializable + +ROOT=Path(__file__).resolve().parents[1] + + +def matrix(rows):return tuple(tuple(Q(x) for x in row) for row in rows) +def eye(h):return matrix([[int(i==j) for j in range(h)] for i in range(h)]) +def zero(h):return matrix([[0]*h for _ in range(h)]) +def sub(A,B):return tuple(tuple(x-y for x,y in zip(a,b)) for a,b in zip(A,B)) +def add(A,B):return tuple(tuple(x+y for x,y in zip(a,b)) for a,b in zip(A,B)) +def scale(A,c):return tuple(tuple(c*x for x in a) for a in A) + + +@lru_cache(maxsize=32768) +def rank(A):return rational_rank(A) + + +def row_basis(rows): + basis={} + for row in rows: + r=[Q(x) for x in row] + for p,b in sorted(basis.items()): + c=r[p] + r=[x-c*y for x,y in zip(r,b)] + pivot=next((i for i,x in enumerate(r) if x),None) + if pivot is not None: + c=r[pivot];basis[pivot]=[x/c for x in r] + return tuple(tuple(b) for _,b in sorted(basis.items())) + + +def inverse(A): + n=len(A);rows=[list(a)+list(b) for a,b in zip(A,eye(n))] + for j in range(n): + p=next((i for i in range(j,n) if rows[i][j]),None) + require(p is not None,'Singular Gram matrix') + rows[j],rows[p]=rows[p],rows[j] + c=rows[j][j];rows[j]=[x/c for x in rows[j]] + for i in range(n): + if i!=j: + c=rows[i][j];rows[i]=[x-c*y for x,y in zip(rows[i],rows[j])] + return matrix([r[n:] for r in rows]) + + +def product(A,B): + return matrix([[sum(x*y for x,y in zip(a,b)) for b in zip(*B)] for a in A]) + + +def span_projection(rows,h): + U=row_basis(rows) + if not U:return zero(h) + H=matrix([[Q(int(i==j))-Q(1,9) for j in range(h)] for i in range(h)]) + Ut=matrix(zip(*U));UH=product(U,H) + return product(product(Ut,inverse(product(UH,Ut))),UH) + + +def paired_invocation(h=6): + """Build every physical edge of the forward paired invocation. + + Terminals are active-factor cuts, not the negative X source terminals + of the complete three-stage network. All scalar gates retain their + published grouping. The returned graph admits arbitrary gate matrices. + """ + c=circuit(h);code=c.compile();v=len(c.inputs);R=code['roles'] + I=eye(h);Z=zero(h) + P=[matrix(line_projection(h,t)) for t in c.inputs] + spans={} + labels={} + for node in sorted(c.active): + if c.args[node]: + a,b=c.args[node];spans[node]=row_basis(spans[a]+spans[b]) + else: + t=c.inputs[node-1];spans[node]=(tuple(Q(i in t) for i in range(h)),) + labels[node]=span_projection(spans[node],h) + require(product(labels[node],labels[node])==labels[node],'Not a projection') + groups=['X']*v+['Y']*v+['side']*R+['center']*h + starts=P+[Z]*v+[Z]*(R+h) + ends=[I]*v+[sub(I,p) for p in P]+[I]*(R+h) + frames={('in',i):M for i,M in enumerate(starts)} + last=[('in',i) for i in range(len(starts))];edges=[] + def gate(name,roles,M): + require(name not in frames,'Repeated vertex') + frames[name]=M + for r in sorted(set(roles)): + edges.append((last[r],name,groups[r]));last[r]=name + sources={t:[] for t in c.inputs};outputs={t:[] for t in c.inputs} + for t,s in code['sources'].items():sources[t].append(2*v+s) + for (_,t),s in code['outputs'].items():outputs[t].append(2*v+s) + centers=list(range(2*v+R,2*v+R+h)) + ops=('L','J','Li','R','V','G','R','L','J','Li','G','V') + central=[] + for step,op in enumerate(ops): + if op in ('L','Li'): + gates=code['gates'] if op=='L' else reversed(code['gates']) + for node,ins,outs in gates: + M=labels[node] if step==7 else I if step==9 else Z + gate((step,node),[2*v+s for s in set(ins+outs)],M) + elif op in ('V','J'): + for j,t in enumerate(c.inputs): + if op=='V':roles=[j]+sources[t];M=P[j] if step==4 else I + else:roles=[v+j]+outputs[t];M=Z if step==1 else sub(I,P[j]) + gate((step,j),roles,M) + else: + gate((step,'central'),list(range(v)) if op=='G' else list(range(v,2*v)), + I if op=='G' else Z) + # The scalar central gate is common to the data bank AND centers. + name=(step,'central') + for r in centers: + edges.append((last[r],name,groups[r]));last[r]=name + central.append(name) + for r,M in enumerate(ends): + name=('out',r);frames[name]=M;edges.append((last[r],name,groups[r])) + return dict(h=h,v=v,R=R,frames=frames,edges=edges,central=central) + + +def score_graph(graph,changes=None): + frames=graph['frames']|dict(changes or {});score=Counter() + require(all(k in graph['frames'] and k[0] not in ('in','out') + for k in (changes or {})),'Only internal gates may change') + for u,v,kind in graph['edges']:score[kind]+=rank(sub(frames[v],frames[u])) + return dict(score) + + +def invocation_counts(h,R): + v=comb(h,3) + return dict(h=h,v=v,side_roles=R,data_rank=2*v*(h-1), + side_rank=R*h,center_rank=3*h*h, + total_rank=R*h+2*v*(h-1)+3*h*h, + center_return_loss=h*h,density=Q(v,h), + density_minus_center_roles=Q(v,h)-h) + + +def central_score(h,D,A,C,B): + """Exact data and center path charge after eliminating side gates. + + Paths: P_t -> A -> B -> I; 0 -> D -> C -> I-P_t; + and h copies of 0 -> D -> A -> C -> B -> I. + """ + I=eye(h);Z=zero(h);v=comb(h,3) + data=sum(rank(sub(A,matrix(line_projection(h,t))))+ + rank(sub(sub(I,matrix(line_projection(h,t))),C)) + for t in combinations(range(h),3)) + data+=v*(rank(sub(B,A))+rank(sub(I,B))+rank(D)+rank(sub(C,D))) + center=h*(rank(D)+rank(sub(A,D))+rank(sub(C,A))+rank(sub(B,C))+rank(sub(I,B))) + return data+center + + +def central_lower_bound(h,A,C): + """All-rational-matrix bound, proved in the accompanying note.""" + I=eye(h);v=comb(h,3) + x=h-rank(A);y=h-rank(sub(I,C)) + u=rank(A)+rank(sub(I,A))-h + w=rank(C)+rank(sub(I,C))-h + return (v-h)*(u+w)+2*(Q(v,h)-h)*(x+y) + + +def density_control(h,M): + k=rank(M);v=comb(h,3) + actual=sum(rank(sub(M,matrix(line_projection(h,t)))) + for t in combinations(range(h),3)) + lower=v*(k-1)+2*Q(v,h)*(h-k) + require(actual>=lower,'Rational rank-density inequality failed') + return actual,lower + + +def rational_controls(h=10): + """Bounded nonsymmetric, nonprojector controls, not the general proof.""" + rng=random.Random(10959);I=eye(h);Z=zero(h) + P=matrix(line_projection(h,(0,1,2))) + E=matrix([[int(i==0 and j==1) for j in range(h)] for i in range(h)]) + matrices=[Z,I,P,sub(I,P),scale(P,Q(2,3)),E,sub(I,E)] + for _ in range(5): + U=matrix([[rng.randrange(-2,3) for _ in range(2)] for _ in range(h)]) + V=matrix([[Q(rng.randrange(-2,3),3) for _ in range(h)] for _ in range(2)]) + matrices.append(product(U,V)) + for M in matrices:density_control(h,M) + S0=2*comb(h,3)*(h-1)+3*h*h + records=[] + for j,M in enumerate(matrices): + A=M;C=matrices[-1-j] + # Noncanonical outer gates ensure both sides of each change are charged. + D=matrices[(j+2)%len(matrices)];B=matrices[(j+3)%len(matrices)] + actual=central_score(h,D,A,C,B) + lower=central_lower_bound(h,A,C) + require(actual-S0>=lower>=0,'Central all-matrix lower bound failed') + records.append(dict(score=actual,lower_excess=lower)) + require(central_score(h,Z,I,Z,I)==S0,'Baseline central score changed') + return dict(h=h,matrix_controls=len(matrices),central_controls=records, + baseline_central_score=S0) + + +def certificate(): + graph=paired_invocation(6);scores=score_graph(graph) + n=invocation_counts(6,graph['R']) + require(scores==dict(X=n['data_rank']//2,Y=n['data_rank']//2, + side=n['side_rank'],center=n['center_rank']), + 'Physical edge score does not reproduce formula') + # Read the published exact role count without changing that certificate. + published=json.loads((ROOT/'certificates/paired-network.json').read_text())['bit_counts'] + full=invocation_counts(50,int(published['side_roles_per_invocation'])) + require(full['center_return_loss']*3*full['v']**2==int(published['L']), + 'Local loss does not reproduce published loss') + return dict(status='FIXED-BOUNDARY BIT INVOCATION RANK OPTIMALITY; NO NEW KAPPA', + upstream_commit=verify_sources(),small_physical_graph=n, + physical_edge_scores=scores,physical_edges=len(graph['edges']), + rational_controls=rational_controls(),published_invocation=full, + theorem='For h>=10, arbitrary rational internal active-factor matrices cannot lower the complete rank score with fixed invocation boundaries, side-role count, and the four grouped central gates.', + scope='Allows joint copy, injection, side and central frame changes. Retains active-factor embedding and all boundary matrices. Does not exclude new cross-invocation boundaries, changed central gate grouping, fewer roles or new scalar topology.', + next_step='Optimize a region crossing invocation boundaries or split the grouped central gates; optimizing only internal matrices of the present invocation is exhausted in this model.') + + +if __name__=='__main__': + (ROOT/'certificates/joint-frame-audit.json').write_text( + json.dumps(serializable(certificate()),indent=2,sort_keys=True)+'\n') + print('PASS fixed-boundary rational-frame audit; no new kappa.') diff --git a/research/joint-frames-cleared-product/benchmark.py b/research/joint-frames-cleared-product/benchmark.py new file mode 100644 index 0000000000..150d8e5c0a --- /dev/null +++ b/research/joint-frames-cleared-product/benchmark.py @@ -0,0 +1,175 @@ +#!/usr/bin/env python3 +"""Alternating fresh-process before/after timing for the positive-side audit. + +Timing is descriptive and never a correctness gate. Receipts must match +fieldwise between baseline and optimized workers. +""" +from __future__ import annotations + +import argparse +from hashlib import sha256 +import json +import os +from pathlib import Path +import platform +import statistics +import subprocess +import sys +import time + +ROOT = Path(__file__).resolve().parents[2] +PACKAGE = Path(__file__).resolve().parent +sys.path.insert(0, str(ROOT / "scripts")) +from certify import require # noqa: E402 + +WORKER = r''' +import json, sys, time +from hashlib import sha256 +from pathlib import Path + +root = Path(sys.argv[1]) +mode = sys.argv[2] +sys.path.insert(0, str(root / "scripts")) + +import importlib.util + +if mode == "baseline": + spec = importlib.util.spec_from_file_location( + "baseline_jf", root / "research/joint-frames-cleared-product/baseline.py" + ) + jf = importlib.util.module_from_spec(spec) + sys.modules["baseline_jf"] = jf + spec.loader.exec_module(jf) +else: + import audit_joint_frames as jf + +import experiments.positive_side_core as positive_side_core +import experiments.rank_product_core as rank_product_core +from experiments.positive_side_core import PositiveSide +from experiments.signed_sparse_core import vectors + +positive_side_core.product = jf.product +rank_product_core.product = jf.product +if hasattr(jf.rank, "cache_clear"): + jf.rank.cache_clear() + +t0 = time.perf_counter() +rows = [] +for h, q in ((4, 2), (5, 2), (4, 4), (5, 4), (6, 4), (8, 8)): + labels = list(vectors(h, q)) + bit_rows = [ + sum( + 1 << j + for j, y in enumerate(labels) + if i == j or sum(a * b for a, b in zip(x, y)) == 0 + ) + for i, x in enumerate(labels) + ] + for strategy in ("balanced", "frequent-pairs"): + c = PositiveSide(bit_rows, labels, strategy) + record = c.verify() + invocation = c.verify_invocation() + frames = c.verify_frames() if strategy == "frequent-pairs" else None + dag = sha256( + json.dumps(dict(args=c.args, outputs=c.outputs), sort_keys=True, separators=(",", ":")).encode() + ).hexdigest() + rows.append( + dict( + h=h, + q=q, + strategy=strategy, + side_roles=record["side_roles"], + additions=record["additions"], + dag_sha256=dag, + independent_roles=invocation["independent_roles"], + frames_transitions=(frames or {}).get("distinct_transitions"), + ) + ) +elapsed = time.perf_counter() - t0 +print(json.dumps(dict(mode=mode, elapsed=elapsed, rows=rows), sort_keys=True)) +''' + + +def run_worker(mode: str) -> dict: + env = os.environ.copy() + env["PYTHONDONTWRITEBYTECODE"] = "1" + env.pop("PYTHONOPTIMIZE", None) + proc = subprocess.run( + [sys.executable, "-I", "-B", "-c", WORKER, str(ROOT), mode], + cwd=ROOT, + env=env, + check=True, + capture_output=True, + text=True, + ) + return json.loads(proc.stdout.strip().splitlines()[-1]) + + +def main(argv=None) -> int: + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--rounds", type=int, default=5) + parser.add_argument("--warmup", type=int, default=1) + parser.add_argument("--output", type=Path, default=None) + args = parser.parse_args(argv) + require(args.rounds >= 1, "rounds must be positive") + + for _ in range(args.warmup): + run_worker("baseline") + run_worker("optimized") + + samples = [] + for i in range(args.rounds): + order = ("baseline", "optimized") if i % 2 == 0 else ("optimized", "baseline") + pair = {} + for mode in order: + pair[mode] = run_worker(mode) + require( + pair["baseline"]["rows"] == pair["optimized"]["rows"], + f"receipt mismatch in pair {i}", + ) + samples.append( + dict( + pair=i, + order=list(order), + baseline_seconds=pair["baseline"]["elapsed"], + optimized_seconds=pair["optimized"]["elapsed"], + rows=pair["optimized"]["rows"], + ) + ) + + base_med = statistics.median(s["baseline_seconds"] for s in samples) + opt_med = statistics.median(s["optimized_seconds"] for s in samples) + ratio = base_med / opt_med if opt_med else None + payload = dict( + status="PASS_IDENTICAL_POSITIVE_SIDE_RECEIPTS", + fixture="scripts/audit_positive_side.py experiment stream (h,q) in {(4,2),(5,2),(4,4),(5,4),(6,4),(8,8)}", + rounds=args.rounds, + warmup=args.warmup, + median_baseline_seconds=base_med, + median_optimized_seconds=opt_med, + median_speedup_ratio=ratio, + samples=samples, + environment=dict( + python=sys.version, + platform=platform.platform(), + executable=sys.executable, + ), + note="Timing is host-descriptive and is not a correctness gate.", + no_new_kappa=True, + ) + text = json.dumps(payload, indent=2, sort_keys=True) + "\n" + if args.output is not None: + require(not args.output.exists(), f"output exists: {args.output}") + args.output.write_text(text, encoding="utf-8") + else: + (PACKAGE / "RESULT.json").write_text(text, encoding="utf-8") + print( + "PASS_IDENTICAL_POSITIVE_SIDE_RECEIPTS " + f"rounds={args.rounds} median_baseline={base_med:.3f}s " + f"median_optimized={opt_med:.3f}s ratio={ratio:.3f}x" + ) + return 0 + + +if __name__ == "__main__": + raise SystemExit(main()) diff --git a/research/joint-frames-cleared-product/verify.py b/research/joint-frames-cleared-product/verify.py new file mode 100644 index 0000000000..213ecbb1dc --- /dev/null +++ b/research/joint-frames-cleared-product/verify.py @@ -0,0 +1,260 @@ +#!/usr/bin/env python3 +"""Equivalence, pin and mutation controls for cleared-denominator joint-frame product. + +Read-only by default. Regenerates no certificate unless --write-certificate is +passed. Timing is not a pass gate; see benchmark.py / RESULT.json. +""" +from __future__ import annotations + +import argparse +from fractions import Fraction as Q +from hashlib import sha256 +import importlib.util +import json +from pathlib import Path +import random +import subprocess +import sys + +ROOT = Path(__file__).resolve().parents[2] +PACKAGE = Path(__file__).resolve().parent +SCRIPTS = ROOT / "scripts" +sys.path.insert(0, str(SCRIPTS)) + +from certify import require # noqa: E402 +from prepare_layers import serializable # noqa: E402 +import audit_joint_frames as production # noqa: E402 +from audit_rank_product_core import certificate as rank_product_certificate # noqa: E402 +from audit_positive_side import certificate as positive_side_certificate # noqa: E402 + +BASE_COMMIT = "0b1cccf86e2f5132ed286a26ef0a681a495740ea" +ORIGINAL_BLOB = "913be4a1f0a651f3aaf7b4ed1901916918ba2cef" +ORIGINAL_SHA256 = "3df8061392ce0ba42bbde8c02f2a30c8141145e70e9a48c18da73d3aafb14423" +OPTIMIZED_SHA256 = "818e86b4152b4eeb853f173c9aa795510caa593ec0e25b05a246f1df52575466" +BASE_RANK_PRODUCT_CERT_SHA256 = "e0d2cb39be3502251f8f8c4a62e0fe6b743be50eef41dda35646762daaec40b9" +PINNED_CERTS = ("certificates/rank-product-core.json",) + + +def load_module(path: Path, name: str): + spec = importlib.util.spec_from_file_location(name, path) + require(spec is not None and spec.loader is not None, f"missing module {path}") + module = importlib.util.module_from_spec(spec) + # Baseline is a full audit_joint_frames copy; give it the scripts path. + sys.modules[name] = module + spec.loader.exec_module(module) + return module + + +def digest_file(path: Path) -> str: + return sha256(path.read_bytes()).hexdigest() + + +def git_show(path: str) -> bytes: + return subprocess.check_output(["git", "show", f"{BASE_COMMIT}:{path}"], cwd=ROOT) + + +def check_baseline_bytes() -> None: + baseline = PACKAGE / "baseline.py" + original = git_show("scripts/audit_joint_frames.py") + require(sha256(original).hexdigest() == ORIGINAL_SHA256, "base audit_joint_frames.py sha256 drift") + blob = ( + subprocess.check_output( + ["git", "rev-parse", f"{BASE_COMMIT}:scripts/audit_joint_frames.py"], cwd=ROOT + ) + .decode() + .strip() + ) + require(blob == ORIGINAL_BLOB, "base audit_joint_frames.py blob drift") + require(baseline.read_bytes() == original, "baseline.py must be an exact copy of the base commit source") + require( + digest_file(SCRIPTS / "audit_joint_frames.py") == OPTIMIZED_SHA256, + "production audit_joint_frames.py does not match the claimed optimized digest", + ) + + +def random_matrix(rng: random.Random, rows: int, cols: int): + dens = (1, 1, 1, 2, 3, 4, 5, 6, 8, 9) + return tuple( + tuple(Q(rng.randint(-7, 7), rng.choice(dens)) for _ in range(cols)) for _ in range(rows) + ) + + +def check_primitive_equivalence(baseline, optimized) -> dict: + rng = random.Random(20261014) + cases = 0 + for _ in range(2500): + n = rng.randint(1, 6) + k = rng.randint(1, 6) + m = rng.randint(1, 6) + A = random_matrix(rng, n, k) + B = random_matrix(rng, k, m) + old = baseline.product(A, B) + new = optimized.product(A, B) + require(old == new, f"product mismatch on shapes {(n, k, m)}") + cases += 1 + # Edge cases: empty left factor, integer matrices, projector-like dens. + empty = optimized.product(tuple(), ((Q(1),),)) + require(empty == tuple(), "empty left factor") + I = optimized.eye(3) + require(optimized.product(I, I) == I, "I*I") + require(baseline.product(I, I) == optimized.product(I, I), "I*I baseline") + P = ( + (Q(1, 2), Q(1, 2), Q(0)), + (Q(1, 2), Q(1, 2), Q(0)), + (Q(0), Q(0), Q(0)), + ) + require(baseline.product(P, P) == optimized.product(P, P) == P, "rank-one projector square") + # Mutant foil: dropping the common scale yields a wrong nonzero product. + bad_scale = tuple( + tuple(Q(x.numerator * 2, 1) for x in row) for row in optimized.product(P, P) + ) + require(bad_scale != P, "mutant scale foil differs") + return {"random_cases": cases, "edge_cases": 4, "scale_mutant": "rejected"} + + +def _bind_product(module_jf) -> None: + import experiments.positive_side_core as positive_side_core + import experiments.rank_product_core as rank_product_core + + production.product = module_jf.product + positive_side_core.product = module_jf.product + rank_product_core.product = module_jf.product + if hasattr(production.rank, "cache_clear"): + production.rank.cache_clear() + + +def positive_side_receipt(module_jf) -> list[dict]: + """Replay the historical positive-side experiment stream under one product.""" + from experiments.positive_side_core import PositiveSide + from experiments.signed_sparse_core import vectors + + _bind_product(module_jf) + rows = [] + for h, q in ((4, 2), (5, 2), (4, 4), (5, 4), (6, 4), (8, 8)): + labels = list(vectors(h, q)) + n = len(labels) + bit_rows = [ + sum( + 1 << j + for j, y in enumerate(labels) + if i == j or sum(a * b for a, b in zip(x, y)) == 0 + ) + for i, x in enumerate(labels) + ] + for strategy in ("balanced", "frequent-pairs"): + circuit = PositiveSide(bit_rows, labels, strategy) + record = circuit.verify() + invocation = circuit.verify_invocation() + frames = circuit.verify_frames() if strategy == "frequent-pairs" else None + dag = sha256( + json.dumps( + dict(args=circuit.args, outputs=circuit.outputs), + sort_keys=True, + separators=(",", ":"), + ).encode() + ).hexdigest() + rows.append( + dict( + h=h, + q=q, + strategy=strategy, + side_roles=record["side_roles"], + additions=record["additions"], + dag_sha256=dag, + invocation=invocation, + frames=frames, + ) + ) + return rows + + +def check_positive_side_experiments(baseline, optimized) -> list[dict]: + old = positive_side_receipt(baseline) + new = positive_side_receipt(optimized) + require(old == new, "positive-side experiment stream drifted") + require(new[-1]["side_roles"] == 1200, "h=8 frequent-pairs side_roles drifted") + return new + + +def check_certificate_pin_discipline() -> dict: + """Working rank-product certificate may change only the joint_frames source pin.""" + reports = {} + for rel in PINNED_CERTS: + base = json.loads(git_show(rel)) + live = json.loads((ROOT / rel).read_text(encoding="utf-8")) + base_pin = base["source_sha256"]["scripts/audit_joint_frames.py"] + live_pin = live["source_sha256"]["scripts/audit_joint_frames.py"] + require(base_pin == ORIGINAL_SHA256, f"{rel}: unexpected base pin") + require(live_pin == OPTIMIZED_SHA256, f"{rel}: optimized pin missing") + restored = json.loads(json.dumps(live)) + restored["source_sha256"]["scripts/audit_joint_frames.py"] = ORIGINAL_SHA256 + require(restored == base, f"{rel}: changed fields beyond the audit_joint_frames pin") + reports[rel] = { + "base_pin": base_pin, + "live_pin": live_pin, + "only_pin_changed": True, + } + base_cert = git_show("certificates/rank-product-core.json") + require( + sha256(base_cert).hexdigest() == BASE_RANK_PRODUCT_CERT_SHA256, + "base rank-product certificate digest drift", + ) + return reports + + +def maybe_write_certificate(write: bool) -> None: + _bind_product(production) + if not write: + live = serializable(rank_product_certificate()) + committed = json.loads((ROOT / "certificates/rank-product-core.json").read_text(encoding="utf-8")) + # Compare mathematical payload; pin already updated in the working tree. + for key in live: + if key in ("source_sha256", "upstream_commit"): + continue + require(live[key] == committed[key], f"live rank-product field drifted: {key}") + require( + live["source_sha256"]["scripts/audit_joint_frames.py"] == OPTIMIZED_SHA256, + "live rank-product pin mismatch", + ) + # Positive-side certificate does not pin audit_joint_frames.py; payload must match base. + pos_live = serializable(positive_side_certificate()) + pos_base = json.loads(git_show("certificates/positive-side-core.json")) + for key in ("small_signed_experiments", "expanded_complete_controls", "status", "scope"): + require(pos_live[key] == pos_base[key], f"positive-side field drifted: {key}") + return + result = rank_product_certificate() + (ROOT / "certificates/rank-product-core.json").write_text( + json.dumps(serializable(result), indent=2, sort_keys=True) + "\n", encoding="utf-8" + ) + + +def main(argv=None) -> int: + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument( + "--write-certificate", + action="store_true", + help="regenerate certificates/rank-product-core.json from the production audit", + ) + args = parser.parse_args(argv) + + check_baseline_bytes() + baseline = load_module(PACKAGE / "baseline.py", "joint_frames_product_baseline") + optimized = production + + primitive = check_primitive_equivalence(baseline, optimized) + experiments = check_positive_side_experiments(baseline, optimized) + pins = check_certificate_pin_discipline() + _bind_product(optimized) + maybe_write_certificate(args.write_certificate) + + print( + "PASS_JOINT_FRAMES_CLEARED_PRODUCT " + f"positive_side_cases={len(experiments)} " + f"random_cases={primitive['random_cases']} " + f"certs={len(pins)} no_new_kappa" + ) + return 0 + + +if __name__ == "__main__": + raise SystemExit(main()) diff --git a/scripts/audit_joint_frames.py b/scripts/audit_joint_frames.py index 913be4a1f0..ec51fdceee 100644 --- a/scripts/audit_joint_frames.py +++ b/scripts/audit_joint_frames.py @@ -4,7 +4,7 @@ from fractions import Fraction as Q from functools import lru_cache from itertools import combinations -from math import comb +from math import comb, lcm from pathlib import Path import json import random @@ -57,7 +57,49 @@ def inverse(A): def product(A,B): - return matrix([[sum(x*y for x,y in zip(a,b)) for b in zip(*B)] for a in A]) + """Exact matrix product over Q. + + Clear denominators once per factor, multiply with Python integers, then + rebuild canonical ``Fraction`` entries. Equivalent to entrywise + ``sum(x*y for ...)``; see ``research/joint-frames-cleared-product/``. + """ + if not A: + return tuple() + n=len(A);k=len(A[0]);m=len(B[0]) + DA=1 + for row in A: + for x in row: + if x.denominator!=1: + DA=lcm(DA,x.denominator) + DB=1 + for row in B: + for x in row: + if x.denominator!=1: + DB=lcm(DB,x.denominator) + if DA==1 and DB==1: + out=[] + for i in range(n): + ai=A[i];row=[] + for j in range(m): + s=0 + for t in range(k): + s+=ai[t].numerator*B[t][j].numerator + row.append(Q(s)) + out.append(tuple(row)) + return tuple(out) + Ai=[[x.numerator*(DA//x.denominator) for x in row] for row in A] + Bi=[[x.numerator*(DB//x.denominator) for x in row] for row in B] + scale=DA*DB + out=[] + for i in range(n): + ai=Ai[i];row=[] + for j in range(m): + s=0 + for t in range(k): + s+=ai[t]*Bi[t][j] + row.append(Q(s,scale)) + out.append(tuple(row)) + return tuple(out) def span_projection(rows,h): diff --git a/tests/test_joint_frames_cleared_product.py b/tests/test_joint_frames_cleared_product.py new file mode 100644 index 0000000000..99ee62b049 --- /dev/null +++ b/tests/test_joint_frames_cleared_product.py @@ -0,0 +1,84 @@ +"""Focused controls for the joint-frames cleared-product tooling package.""" +from __future__ import annotations + +import importlib.util +import json +import subprocess +import sys +import unittest +from fractions import Fraction as Q +from hashlib import sha256 +from pathlib import Path + +ROOT = Path(__file__).resolve().parents[1] +PACKAGE = ROOT / "research/joint-frames-cleared-product" +SCRIPTS = ROOT / "scripts" +sys.path.insert(0, str(SCRIPTS)) + +import audit_joint_frames as jf # noqa: E402 + + +def load_baseline(): + spec = importlib.util.spec_from_file_location( + "joint_frames_product_baseline", PACKAGE / "baseline.py" + ) + module = importlib.util.module_from_spec(spec) + sys.modules[spec.name] = module + spec.loader.exec_module(module) + return module + + +class JointFramesClearedProductTests(unittest.TestCase): + @classmethod + def setUpClass(cls): + cls.baseline = load_baseline() + + def test_baseline_bytes_match_base_commit(self): + original = subprocess.check_output( + ["git", "show", "0b1cccf86e2f5132ed286a26ef0a681a495740ea:scripts/audit_joint_frames.py"], + cwd=ROOT, + ) + self.assertEqual((PACKAGE / "baseline.py").read_bytes(), original) + self.assertEqual( + sha256(original).hexdigest(), + "3df8061392ce0ba42bbde8c02f2a30c8141145e70e9a48c18da73d3aafb14423", + ) + + def test_product_agrees_on_rational_matrices(self): + A = ((Q(1, 2), Q(1, 3)), (Q(-1), Q(2, 5))) + B = ((Q(3), Q(0), Q(1, 7)), (Q(1, 4), Q(-2), Q(1))) + self.assertEqual(self.baseline.product(A, B), jf.product(A, B)) + I = jf.eye(2) + self.assertEqual(jf.product(I, A), A) + self.assertEqual(self.baseline.product(I, A), jf.product(I, A)) + + def test_empty_left_factor(self): + self.assertEqual(jf.product(tuple(), ((Q(1),),)), tuple()) + self.assertEqual(self.baseline.product(tuple(), ((Q(1),),)), tuple()) + + def test_certificate_pin_only_joint_frames(self): + rel = "certificates/rank-product-core.json" + base = json.loads( + subprocess.check_output( + ["git", "show", f"0b1cccf86e2f5132ed286a26ef0a681a495740ea:{rel}"], + cwd=ROOT, + ) + ) + live = json.loads((ROOT / rel).read_text(encoding="utf-8")) + self.assertEqual( + base["source_sha256"]["scripts/audit_joint_frames.py"], + "3df8061392ce0ba42bbde8c02f2a30c8141145e70e9a48c18da73d3aafb14423", + ) + self.assertEqual( + live["source_sha256"]["scripts/audit_joint_frames.py"], + "818e86b4152b4eeb853f173c9aa795510caa593ec0e25b05a246f1df52575466", + ) + restored = json.loads(json.dumps(live)) + restored["source_sha256"]["scripts/audit_joint_frames.py"] = base["source_sha256"][ + "scripts/audit_joint_frames.py" + ] + self.assertEqual(restored, base) + + +if __name__ == "__main__": + unittest.main() From 98dd6ef113e1e6a4ca3848b0889cd13b1970fd32 Mon Sep 17 00:00:00 2001 From: Wentao Li Date: Wed, 14 Oct 2026 13:36:14 +0000 Subject: [PATCH 2/2] Attribution: remove product/model names from NOTICE --- research/joint-frames-cleared-product/NOTICE.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/research/joint-frames-cleared-product/NOTICE.md b/research/joint-frames-cleared-product/NOTICE.md index c7c82cf449..c572c4c225 100644 --- a/research/joint-frames-cleared-product/NOTICE.md +++ b/research/joint-frames-cleared-product/NOTICE.md @@ -14,6 +14,6 @@ Predecessor credit: local modular-rank adapter in `research/joint-frame-modular-screen/`. Prepared by Wentao Li with substantial AI assistance under Apache-2.0. -No Cursor/Composer/Codex/model names are claimed as co-authors. This is not +No product or model names are claimed as co-authors. This is not independent human peer review and is not a formal proof of the multiplication theorem.