Prove a nine-call returned-register minimum and restrict clean-helper words

research/bit-clean-extra-register/README.md

@@ -0,0 +1,93 @@
+# Restrictions for three active targets and one clean extra register
+
+This package proves restrictions on an eight-call formal binary circuit.
+There are three active targets and one extra input that starts at zero.
+The extra output is discarded. The required upper-left block is
+`diag([C_1],[C_2],[C_3])`, where the targets are invertible lower-triangular
+rational 3 by 3 frames. Paid factors are `I + ([A]-1)N`: `A` is nonzero
+and has rational rank one, and `N` is a binary rank-one idempotent on
+four registers. The coefficient ring is `F_2[M_3(Q)]`.
+The endpoint is the product of these listed paid factors. No additional
+free scalar map is applied at the end. The clean active-block condition
+alone does not justify removing such a map from a broader circuit model.
+
+The [final report](sources/four-register/FINAL-CLEAN-REPORT.txt) states
+the scope and proof dependencies. The results are:
+
+- Paid-frame span at most four needs at least nine calls. This bound
+  permits any number of clean extra registers.
+- Span eight is impossible. Span seven forces zero active off-diagonal
+  entries in every scalar projector.
+- For one clean extra register, the complete 24-projector class with
+  zero active off-diagonal entries is impossible in eight calls.
+- Eight calls are also impossible over the union of the coordinate-basis
+  projectors and one arbitrary binary-basis set of projectors.
+
+The remaining arbitrary four-register problem has frame span five or six,
+a nonzero active off-diagonal pattern, and an alphabet outside the last
+class. It remains open here. Fixing one basis to the coordinate basis is
+a restriction; it is not a normalization of every pair of bases. These
+results give no construction, complete clean-register lower bound, or
+new kappa value.
+
+The [span proof](sources/four-register/CLEAN-SPAN-FOUR.txt) extends the
+method in [PR #468](https://github.com/CrocSwap/integer-mult-bounds/pull/468),
+at its [recorded source](https://github.com/CrocSwap/integer-mult-bounds/blob/07a78bf335b0b5039a1fecd7cd74a0fe1d1605ea/research/bit-three-register-lower-bound/README.md).
+The [one-relation proof](sources/four-register/CLEAN-ONE-RELATION.txt),
+[zero-pattern proof](sources/four-register/independent/clean-zero/PROOF.txt),
+and [independent scope audit](sources/doubling-architecture/rank-independent/clean-audit/PROOF-AUDIT.txt)
+give the other arguments. The predecessor credits the scalar model to
+[PR #288](https://github.com/CrocSwap/integer-mult-bounds/pull/288), at
+[its recorded source](https://github.com/eumemic/integer-mult-bounds/blob/475a088b5862f75f0b10596cfd6842d19531a5ec/research/negative-results-paradigm-search/README.md).
+The pinned PR #468 proof also credits @huxint's
+[PR #203](https://github.com/CrocSwap/integer-mult-bounds/pull/203) for the
+related common triangular-frame obstruction, at
+[its recorded commit](https://github.com/huxint/integer-mult-bounds/commit/d2873e20750d0949d2ad75cbc4cd82b5b1a74e84).
+OpenAI Codex and research agents prepared the proof and checks under the
+user's direction. No independent human review is claimed.
+
+From this package directory, with Python 3.10 or later and a C++17 compiler:
+
+```sh
+python3 -B verify.py --build /tmp/clean-extra-register-replay
+```
+
+The build path must not exist. `CXX` can select the compiler. The runner
+copies the saved source files there before any generated output is written.
+It rejects optimized Python because some historical sources use assertions.
+No repository source or third-party Python module is required.
+
+The final line must be:
+
+```text
+PASS_CLEAN_RESTRICTED_CLASSES 314666 7406643
+```
+
+The replay checks all 314,666 zero-pattern words with primitive-integer and
+finite-field engines and compares every output record. A separate generator
+checks all 3,674,160 raw orders by dependence signatures. It also checks
+all 166 basis alphabets, with 7,406,643 words, in the finite-field engine.
+The basis catalogue is reconstructed through dual-vector tests. A separate
+rational engine checks 48 fixed words from the saved independent receipt.
+The full basis search does not have a second complete arithmetic replay.
+
+`SOURCE-MANIFEST.json` records the original paths and hashes. Source bytes
+are unchanged. The new runner only makes the existing checks portable and
+compares their outcomes. `expected/` contains historical receipts. The
+new `replayed-receipt.json` and `replay.log` record the cleanup audit run.
+Historical prose can name receipts at their old paths; `expected/`
+contains the receipts used by this replay. The earlier layer-only audits
+and returned-register controls are historical evidence. They are not
+replay dependencies. The current runner executes the 166 basis checks
+in sequence; the preserved historical scheduler used three workers.
+Python child processes ignore Python environment options so their
+assertions remain enabled.
+
+## Open next questions
+
+Does an eight-call clean circuit exist in frame span five or six outside
+the two excluded scalar classes? A first step is an exact completeness
+reduction for the remaining nonzero active off-diagonal patterns. The
+present reductions do not bound that full scalar search. A positive word
+would still need an all-size compiler and a full cost calculation before
+it could affect kappa.

research/bit-clean-extra-register/SOURCE-MANIFEST.json

@@ -0,0 +1,143 @@
+{
+  "main_pin": "cef4b52f2a59009865bf8eabde1be3f159063703",
+  "files": [
+    {
+      "original": "work/doubling-architecture/clean-ancilla/ALL-BASIS-SUMMARY.json",
+      "package": "expected/all-basis-summary.json",
+      "sha256": "46040fe7a442e117f9a28ce47caa53d3800ca45777a9bfb16463fc58125b1a4a",
+      "bytes": 64174
+    },
+    {
+      "original": "work/doubling-architecture/rank-independent/clean-audit/CATALOGUE-AUDIT.json",
+      "package": "expected/catalogue-audit.json",
+      "sha256": "5034f22651597e8710498194a185543735d2cdfd1d65b62b554045b1516638c8",
+      "bytes": 1493
+    },
+    {
+      "original": "work/four-register/independent-audit/CLEAN-ZERO-ORDER-RESULT.json",
+      "package": "expected/clean-zero-independent-order-result.json",
+      "sha256": "7dcd340eedf19388a4a2db364be4a00388e93a38ab4d08d7729971c88d1d2632",
+      "bytes": 178
+    },
+    {
+      "original": "work/four-register/independent/clean-zero/RESULT.json",
+      "package": "expected/clean-zero-result.json",
+      "sha256": "b8ce3ecf7bd762cfb9a2bfaa37f0dbd0034eba42ad59bb68e714c4d220c2d997",
+      "bytes": 2031
+    },
+    {
+      "original": "work/doubling-architecture/rank-independent/clean-audit/SELECTED-COMPARISON.json",
+      "package": "expected/selected-comparison.json",
+      "sha256": "5f0e29bb04fd0f44267237060728dfb8bca2e1f41181c940f30fe0ae8c2cee39",
+      "bytes": 37045
+    },
+    {
+      "original": "work/doubling-architecture/clean-ancilla/ALPHABETS.txt",
+      "package": "sources/doubling-architecture/clean-ancilla/ALPHABETS.txt",
+      "sha256": "9578ac3ba047a87502cc6e481f5bf8154f1c2477f3be4b2d1e7c1e8b35213da4",
+      "bytes": 5868
+    },
+    {
+      "original": "work/doubling-architecture/clean-ancilla/RESULT.txt",
+      "package": "sources/doubling-architecture/clean-ancilla/RESULT.txt",
+      "sha256": "bddf6f4a91273966179f36fd59734c125f2bad69d10ed27998595da438aa2c73",
+      "bytes": 3768
+    },
+    {
+      "original": "work/doubling-architecture/clean-ancilla/run_two_bases.py",
+      "package": "sources/doubling-architecture/clean-ancilla/run_two_bases.py",
+      "sha256": "33ac757f42b7e770d24ea82b70cc167627e28b1da98c1e0c8c5d0e35f9bb2931",
+      "bytes": 1748
+    },
+    {
+      "original": "work/doubling-architecture/clean-ancilla/search.py",
+      "package": "sources/doubling-architecture/clean-ancilla/search.py",
+      "sha256": "3f1301263134b1ed17d356f39bdd175f911c2c4cdddb5e3cab40fed6969e53bf",
+      "bytes": 3762
+    },
+    {
+      "original": "work/doubling-architecture/clean-ancilla/two_bases.cpp",
+      "package": "sources/doubling-architecture/clean-ancilla/two_bases.cpp",
+      "sha256": "7d7438f5c473eba5a0863afacdb7b0896b2c45325cf2f88c7cfb078d189ff132",
+      "bytes": 15146
+    },
+    {
+      "original": "work/doubling-architecture/rank-independent/clean-audit/PROOF-AUDIT.txt",
+      "package": "sources/doubling-architecture/rank-independent/clean-audit/PROOF-AUDIT.txt",
+      "sha256": "92f039fd3868592bc8cfa3b14ea90f42c5be9ed639ca84ac6ce7a6cb5fc59e5b",
+      "bytes": 7629
+    },
+    {
+      "original": "work/doubling-architecture/rank-independent/clean-audit/selected_words.cpp",
+      "package": "sources/doubling-architecture/rank-independent/clean-audit/selected_words.cpp",
+      "sha256": "bd5ee927c75a78ce4658d2290dd4301c78744178c2b95b3fe676153dae2a2fa0",
+      "bytes": 778
+    },
+    {
+      "original": "work/four-register/CLEAN-ONE-RELATION.txt",
+      "package": "sources/four-register/CLEAN-ONE-RELATION.txt",
+      "sha256": "9aebe7497d3ff594141ab1674bc34284c6cc410f2d066994ff8c059c940902e6",
+      "bytes": 6804
+    },
+    {
+      "original": "work/four-register/CLEAN-SPAN-FOUR.txt",
+      "package": "sources/four-register/CLEAN-SPAN-FOUR.txt",
+      "sha256": "a65edc9dfe3744322a4fad5f30d2d0c7fb737bb611f5b11de48264386e742019",
+      "bytes": 3817
+    },
+    {
+      "original": "work/four-register/F101-ARITHMETIC.txt",
+      "package": "sources/four-register/F101-ARITHMETIC.txt",
+      "sha256": "540dfa9f49488b92ee24e9f82704ac2032aa2117957dd4c9cbcf33ca4fafe09f",
+      "bytes": 3513
+    },
+    {
+      "original": "work/four-register/FINAL-CLEAN-REPORT.txt",
+      "package": "sources/four-register/FINAL-CLEAN-REPORT.txt",
+      "sha256": "a948c7380e22ff83030811c9e6b5a867b510609c89ee0b586feb7616374e748c",
+      "bytes": 6492
+    },
+    {
+      "original": "work/four-register/dirty_ancilla.py",
+      "package": "sources/four-register/dirty_ancilla.py",
+      "sha256": "81d8df0b7b08e0ad89dc13f65325e7091cb9c201d9c5bc4d8637f8325d0be876",
+      "bytes": 6293
+    },
+    {
+      "original": "work/four-register/independent-audit/check_clean_zero_orders.cpp",
+      "package": "sources/four-register/independent-audit/check_clean_zero_orders.cpp",
+      "sha256": "488f25346635fdebac5b0d928da59dabe0c92792d375938b5dfe1c2244309d6a",
+      "bytes": 4419
+    },
+    {
+      "original": "work/four-register/independent-audit/clean-zero-family-metadata.txt",
+      "package": "sources/four-register/independent-audit/clean-zero-family-metadata.txt",
+      "sha256": "6e4758a04985074fc78aca9a55aecff947573b66803d26f5f4d7676a30dd8dd7",
+      "bytes": 8410
+    },
+    {
+      "original": "work/four-register/independent/clean-zero/PROOF.txt",
+      "package": "sources/four-register/independent/clean-zero/PROOF.txt",
+      "sha256": "4dea498aee7f2e39a0607b6d4f1e7f8f9f7ad9a5f1e72241743180f1775fb7e7",
+      "bytes": 5049
+    },
+    {
+      "original": "work/four-register/independent/clean-zero/field.cpp",
+      "package": "sources/four-register/independent/clean-zero/field.cpp",
+      "sha256": "a39b5f3ca6dbd506c6008e356a0239173e8dff53047c4a6e71972c6c35226c9e",
+      "bytes": 13395
+    },
+    {
+      "original": "work/four-register/independent/clean-zero/generate.py",
+      "package": "sources/four-register/independent/clean-zero/generate.py",
+      "sha256": "f002f6479e244da91724ca2589c03c4067d82f2206304660a92f8355dfedb6ef",
+      "bytes": 2088
+    },
+    {
+      "original": "work/four-register/independent/clean-zero/integer.cpp",
+      "package": "sources/four-register/independent/clean-zero/integer.cpp",
+      "sha256": "927fcb11154edfeabfdf852c0f243f82b7d5d56475ced11bdaa3417b8528b6d9",
+      "bytes": 13367
+    }
+  ]
+}