diff --git a/research/bit-joint-dirty-pair/INPUT-SOURCES.json b/research/bit-joint-dirty-pair/INPUT-SOURCES.json new file mode 100644 index 0000000000..13b50fb71d --- /dev/null +++ b/research/bit-joint-dirty-pair/INPUT-SOURCES.json @@ -0,0 +1,26 @@ +{ + "predecessor_pr": "https://github.com/CrocSwap/integer-mult-bounds/pull/4068", + "predecessor_head": "5a34918402ae2c0c683d8820ad832970e77f6382", + "canonical_base": "bb4bccbf42844d2801487450727c2f63e10d1d0f", + "files": [ + { + "path": "inputs/WORD.json.gz", + "sha256": "c46ccd7d3eedabc6a7efbb1a91ec13f2928bad8ee0bac57c6e593a092d13d96c", + "source_path": "research/bit-shared-source-compensation/inputs/WORD.json.gz", + "source_commit": "5a34918402ae2c0c683d8820ad832970e77f6382" + }, + { + "path": "inputs/GEOMETRY.json.gz", + "sha256": "a353999bceac4ac957f540adfd3e5f8768297138b27132eeb83332e2ea4b1022", + "source_path": "research/bit-shared-source-compensation/inputs/GEOMETRY.json.gz", + "source_commit": "5a34918402ae2c0c683d8820ad832970e77f6382" + }, + { + "path": "inputs/PREDECESSOR-PINS.json", + "sha256": "4d03736c497eae94c4e98d33ac10ecacba9e914f9d604787237ff71075dc4e94", + "source_path": "research/bit-shared-source-compensation/inputs/PREDECESSOR-PINS.json", + "source_commit": "5a34918402ae2c0c683d8820ad832970e77f6382" + } + ], + "scope": "Exact copied input bytes; source attribution is retained in PREDECESSOR-PINS.json. New checker does not import producer code." +} diff --git a/research/bit-joint-dirty-pair/LICENSE b/research/bit-joint-dirty-pair/LICENSE new file mode 100644 index 0000000000..261eeb9e9f --- /dev/null +++ b/research/bit-joint-dirty-pair/LICENSE @@ -0,0 +1,201 @@ + Apache License + Version 2.0, January 2004 + http://www.apache.org/licenses/ + + TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION + + 1. Definitions. + + "License" shall mean the terms and conditions for use, reproduction, + and distribution as defined by Sections 1 through 9 of this document. + + "Licensor" shall mean the copyright owner or entity authorized by + the copyright owner that is granting the License. + + "Legal Entity" shall mean the union of the acting entity and all + other entities that control, are controlled by, or are under common + control with that entity. For the purposes of this definition, + "control" means (i) the power, direct or indirect, to cause the + direction or management of such entity, whether by contract or + otherwise, or (ii) ownership of fifty percent (50%) or more of the + outstanding shares, or (iii) beneficial ownership of such entity. + + "You" (or "Your") shall mean an individual or Legal Entity + exercising permissions granted by this License. + + "Source" form shall mean the preferred form for making modifications, + including but not limited to software source code, documentation + source, and configuration files. + + "Object" form shall mean any form resulting from mechanical + transformation or translation of a Source form, including but + not limited to compiled object code, generated documentation, + and conversions to other media types. + + "Work" shall mean the work of authorship, whether in Source or + Object form, made available under the License, as indicated by a + copyright notice that is included in or attached to the work + (an example is provided in the Appendix below). + + "Derivative Works" shall mean any work, whether in Source or Object + form, that is based on (or derived from) the Work and for which the + editorial revisions, annotations, elaborations, or other modifications + represent, as a whole, an original work of authorship. For the purposes + of this License, Derivative Works shall not include works that remain + separable from, or merely link (or bind by name) to the interfaces of, + the Work and Derivative Works thereof. + + "Contribution" shall mean any work of authorship, including + the original version of the Work and any modifications or additions + to that Work or Derivative Works thereof, that is intentionally + submitted to Licensor for inclusion in the Work by the copyright owner + or by an individual or Legal Entity authorized to submit on behalf of + the copyright owner. For the purposes of this definition, "submitted" + means any form of electronic, verbal, or written communication sent + to the Licensor or its representatives, including but not limited to + communication on electronic mailing lists, source code control systems, + and issue tracking systems that are managed by, or on behalf of, the + Licensor for the purpose of discussing and improving the Work, but + excluding communication that is conspicuously marked or otherwise + designated in writing by the copyright owner as "Not a Contribution." + + "Contributor" shall mean Licensor and any individual or Legal Entity + on behalf of whom a Contribution has been received by Licensor and + subsequently incorporated within the Work. + + 2. Grant of Copyright License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + copyright license to reproduce, prepare Derivative Works of, + publicly display, publicly perform, sublicense, and distribute the + Work and such Derivative Works in Source or Object form. + + 3. Grant of Patent License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + (except as stated in this section) patent license to make, have made, + use, offer to sell, sell, import, and otherwise transfer the Work, + where such license applies only to those patent claims licensable + by such Contributor that are necessarily infringed by their + Contribution(s) alone or by combination of their Contribution(s) + with the Work to which such Contribution(s) was submitted. If You + institute patent litigation against any entity (including a + cross-claim or counterclaim in a lawsuit) alleging that the Work + or a Contribution incorporated within the Work constitutes direct + or contributory patent infringement, then any patent licenses + granted to You under this License for that Work shall terminate + as of the date such litigation is filed. + + 4. Redistribution. You may reproduce and distribute copies of the + Work or Derivative Works thereof in any medium, with or without + modifications, and in Source or Object form, provided that You + meet the following conditions: + + (a) You must give any other recipients of the Work or + Derivative Works a copy of this License; and + + (b) You must cause any modified files to carry prominent notices + stating that You changed the files; and + + (c) You must retain, in the Source form of any Derivative Works + that You distribute, all copyright, patent, trademark, and + attribution notices from the Source form of the Work, + excluding those notices that do not pertain to any part of + the Derivative Works; and + + (d) If the Work includes a "NOTICE" text file as part of its + distribution, then any Derivative Works that You distribute must + include a readable copy of the attribution notices contained + within such NOTICE file, excluding those notices that do not + pertain to any part of the Derivative Works, in at least one + of the following places: within a NOTICE text file distributed + as part of the Derivative Works; within the Source form or + documentation, if provided along with the Derivative Works; or, + within a display generated by the Derivative Works, if and + wherever such third-party notices normally appear. The contents + of the NOTICE file are for informational purposes only and + do not modify the License. You may add Your own attribution + notices within Derivative Works that You distribute, alongside + or as an addendum to the NOTICE text from the Work, provided + that such additional attribution notices cannot be construed + as modifying the License. + + You may add Your own copyright statement to Your modifications and + may provide additional or different license terms and conditions + for use, reproduction, or distribution of Your modifications, or + for any such Derivative Works as a whole, provided Your use, + reproduction, and distribution of the Work otherwise complies with + the conditions stated in this License. + + 5. Submission of Contributions. Unless You explicitly state otherwise, + any Contribution intentionally submitted for inclusion in the Work + by You to the Licensor shall be under the terms and conditions of + this License, without any additional terms or conditions. + Notwithstanding the above, nothing herein shall supersede or modify + the terms of any separate license agreement you may have executed + with Licensor regarding such Contributions. + + 6. Trademarks. This License does not grant permission to use the trade + names, trademarks, service marks, or product names of the Licensor, + except as required for reasonable and customary use in describing the + origin of the Work and reproducing the content of the NOTICE file. + + 7. Disclaimer of Warranty. Unless required by applicable law or + agreed to in writing, Licensor provides the Work (and each + Contributor provides its Contributions) on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or + implied, including, without limitation, any warranties or conditions + of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A + PARTICULAR PURPOSE. You are solely responsible for determining the + appropriateness of using or redistributing the Work and assume any + risks associated with Your exercise of permissions under this License. + + 8. Limitation of Liability. In no event and under no legal theory, + whether in tort (including negligence), contract, or otherwise, + unless required by applicable law (such as deliberate and grossly + negligent acts) or agreed to in writing, shall any Contributor be + liable to You for damages, including any direct, indirect, special, + incidental, or consequential damages of any character arising as a + result of this License or out of the use or inability to use the + Work (including but not limited to damages for loss of goodwill, + work stoppage, computer failure or malfunction, or any and all + other commercial damages or losses), even if such Contributor + has been advised of the possibility of such damages. + + 9. Accepting Warranty or Additional Liability. While redistributing + the Work or Derivative Works thereof, You may choose to offer, + and charge a fee for, acceptance of support, warranty, indemnity, + or other liability obligations and/or rights consistent with this + License. However, in accepting such obligations, You may act only + on Your own behalf and on Your sole responsibility, not on behalf + of any other Contributor, and only if You agree to indemnify, + defend, and hold each Contributor harmless for any liability + incurred by, or claims asserted against, such Contributor by reason + of your accepting any such warranty or additional liability. + + END OF TERMS AND CONDITIONS + + APPENDIX: How to apply the Apache License to your work. + + To apply the Apache License to your work, attach the following + boilerplate notice, with the fields enclosed by brackets "[]" + replaced with your own identifying information. (Don't include + the brackets!) The text should be enclosed in the appropriate + comment syntax for the file format. We also recommend that a + file or class name and description of purpose be included on the + same "printed page" as the copyright notice for easier + identification within third-party archives. + + Copyright [yyyy] [name of copyright owner] + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. diff --git a/research/bit-joint-dirty-pair/MANIFEST.json b/research/bit-joint-dirty-pair/MANIFEST.json new file mode 100644 index 0000000000..c7cc621b30 --- /dev/null +++ b/research/bit-joint-dirty-pair/MANIFEST.json @@ -0,0 +1,22 @@ +{ + "files": { + "INPUT-SOURCES.json": "bbccd32d1decb57d9a0250055080c0b8687ee6ef0e75a6b550340c87d73d7c7c", + "LICENSE": "c71d239df91726fc519c6eb72d318ec65820627232b2f796219e87dcf35d0ab4", + "PROOF.md": "be917cba2bac53328ca6471c9a40720b11b3b686d93d3654758be9c10e1c7e69", + "README.md": "b307851d4260d59391ff77c25a7332baf81bba59f8843a98e77b97959ab8f3b1", + "RESULT.json": "3cb0c3f09a22bd9b2f6b1823390f0aed520ad473b4827aaf1d8296a6a1a6c5b5", + "REVIEW.md": "aa2c1e8c83a6679d944401698840e47eb12f358f966c30ecc49126b201c7aa10", + "SOURCE-NOTES.md": "3bb4a2c3d55135aba1925039c4548b2eb777ccd3d7a08cc87e31023abf1a0ae6", + "SOURCES.json": "150f944dc05d1d6a65a171ebf7f92ab331280676d859e7d23ab08bbdde6731c5", + "TASK.json": "a4afcd24ee1c30d67ca9ee6aa7b6b3acdbe17783abfc58b76abefcbd2fbea33f", + "VERIFY.json": "686022a6c6a25a107ea4e6b2616c32ede1a1d13a5a79b8d89b810e8b99645408", + "check.py": "c1cf94026e5733784dfa1d92ba007a7b6e2d3148e33e7daf88630cdfdef7c01b", + "inputs/GEOMETRY.json.gz": "a353999bceac4ac957f540adfd3e5f8768297138b27132eeb83332e2ea4b1022", + "inputs/PREDECESSOR-PINS.json": "4d03736c497eae94c4e98d33ac10ecacba9e914f9d604787237ff71075dc4e94", + "inputs/WORD.json.gz": "c46ccd7d3eedabc6a7efbb1a91ec13f2928bad8ee0bac57c6e593a092d13d96c", + "source_check.py": "cfd840feef006198d3efe27560cf034719dea6831825e48b466360851b7bf421", + "verify.py": "bcb67a10939ba0b5c42005972f2c9bf9bb7e0dad8d1067c17b10ec179a9abfc0" + }, + "schema_version": 1, + "scope": "Byte integrity plus complete semantic receipts; not formal-kernel or native proof." +} diff --git a/research/bit-joint-dirty-pair/PROOF.md b/research/bit-joint-dirty-pair/PROOF.md new file mode 100644 index 0000000000..2465a0e838 --- /dev/null +++ b/research/bit-joint-dirty-pair/PROOF.md @@ -0,0 +1,344 @@ +# A sharp query tariff for two independent dirty inputs + +This is a written all-parameter proof in the model below, not a formal-kernel +verification. The finite source checks accompanying it bind a particular pair +to the hypotheses; they do not replace this proof. + +## Model and theorem + +Fix an integer address half-dimension `d >= 2` and an independent common price +parameter `m > 0`. For each odd prime `ell`, the address space is + +\[ +\Omega_\ell=\mathbf F_\ell^{2d},\qquad N=|\Omega_\ell|=\ell^{2d}. +\] + +A VALUE register is an arbitrary function `Omega_ell -> F_2`. Free operations +are invertible matrices over `F_2` mixing whole VALUE registers, with the same +scalar coefficients at every address. They include register permutations and +CNOTs. They do not include address-dependent mixing, nonlinear gates, or free +address permutations. + +For a dyadic rational idempotent `P` of size `d` and rank `r > 0`, define + +\[ +S(P)=\begin{pmatrix}I-P&P\\P&I-P\end{pmatrix}. +\] + +A paid query applies this address involution to one VALUE register and leaves +all other registers unchanged. There are no frame-path restrictions or costs +in this relaxed model: every such fixed dyadic projector is eligible as a paid +query. This relaxation does not enlarge the free gate set just specified. +At parameter `0 <= b <= 1`, its tariff is + +\[ +H_r(m)=m^b r^{1-b}. +\] + +The price parameter `m` is not the address half-dimension `d`. For each fixed +pair `(d,m)`, the number of registers, finite gate word, scalar matrices, +and rational projectors must be independent of `ell`. The same word must have +the required endpoint for every sufficiently large odd prime `ell`. + +Let `p=S(P)` and `q=S(Q)` be distinct rank-two partial swaps. Initially there +are `a >= 2` arbitrary independent VALUE registers and any finite number of +additional zero VALUE registers. The first two arbitrary inputs must become +`p f_1` and `q f_2`; every other arbitrary input must be restored, and every +initially zero register must return to zero. No arbitrary-input column is +omitted from these requirements. The notation for the address action is fixed +below. + +**Theorem.** Every such word has tariff at least + +\[ +2H_2(m)=2m^b2^{1-b}. +\] + +Two separate queries, one applying `p` to register 1 and one applying `q` to +register 2, attain this tariff. Thus it is the exact optimum in this model, +including arbitrary restored dirty spectators and restored clean ancillas. + +## 1. Partial swaps and their Boolean operator defect + +All matrices are reduced modulo an odd prime using their dyadic entries. Since +`P^2=P`, its rational characteristic polynomial is +`X^(d-r)(X-1)^r`. The same polynomial identity holds after reduction at every +odd prime. An idempotent is diagonalizable with eigenvalues 0 and 1 over every +field, so the reduced projector still has rank exactly `r`. + +In the invertible coordinates `(x+y,x-y)`, the partial swap acts as + +\[ +(u,v)\longmapsto (u,(I-2P)v). +\] + +It is an involution, has rational determinant `(-1)^r`, and fixes exactly +`ell^(2d-r)` addresses. Its permutation of `Omega_ell` therefore consists of +that many fixed points and + +\[ +D_r=\frac{\ell^{2d}-\ell^{2d-r}}2 + =\frac N2(1-\ell^{-r}) +\] + +two-cycles. On Boolean VALUE functions, each two-cycle contributes rank one +to the operator `I+rho_ell(S(P))`, and each fixed point contributes zero. +Consequently this Boolean operator has rank exactly `D_r` over `F_2`. + +Here and throughout, + +\[ +(\rho_\ell(g)f)(z)=f(g^{-1}z). +\] + +This inverse pullback makes `rho_ell(g h)=rho_ell(g)rho_ell(h)`. For a queried +involution its inverse is itself, so this convention does not change the query. + +## 2. Scalar normalization and the full endpoint + +Let there be `R >= a` registers, ordered so the arbitrary inputs precede the +zero inputs, and let `J` be the constant `R`-by-`a` coordinate inclusion. The +endpoint is the equality of complete `R`-by-`a` VALUE operators + +\[ +WJ=JD,\qquad D=\operatorname{diag}(p,q,I,\ldots,I). \tag{1} +\] + +Here an address label means its VALUE action. In the dirty-only case `R=a`, +this specifies the entire square operator. When `R>a`, it specifies all +arbitrary input columns and the zero final rows of the clean ancillas; it does +not assert any action on hypothetical nonzero inputs in the clean slots. + +Write the word, in operator order, as + +\[ +W=A_k Q_k A_{k-1}\cdots Q_1 A_0, +\] + +where all `A_i` are scalar invertible matrices, and query `Q_i` acts on one +register with address label `g_i`. Let + +\[ +S=A_k\cdots A_0,\qquad B_i=A_{i-1}\cdots A_0. +\] + +Then the exact factorization is + +\[ +W=S T_k\cdots T_1,\qquad +T_i=B_i^{-1}Q_i B_i=I+(g_i+1)E_i, \tag{2} +\] + +where `E_i=u_i v_i` is a scalar rank-one idempotent: `u_i` is a column, +`v_i` a row, and `v_i u_i=1`. Scalar entries commute with address labels, but +address labels themselves are not commuted in (2). + +Queries fix constant VALUE functions. Applying (1) to arbitrary constants in +the first `a` slots therefore gives + +\[ +SJ=J. \tag{3} +\] + +In particular `S=I` in the dirty-only case. With clean slots only (3), not +`S=I`, is warranted. + +## 3. Zero, one, or two queries + +Fix any odd prime at which the endpoint holds. Applying (2), (3), and the +matrix-rank inequality `rank(AB-I) <= rank(A-I)+rank(B-I)` gives + +\[ +\begin{aligned} +2D_2 + &=\operatorname{rank}(JD-J)\\ + &=\operatorname{rank}\bigl(S(T_k\cdots T_1-I)J\bigr)\\ + &\le \sum_{i=1}^k \operatorname{rank}(T_i-I) + =\sum_{i=1}^k D_{r_i}. \tag{4} +\end{aligned} +\] + +The target rank is a sum because its two defects occupy independent input and +output register blocks. Conjugation by scalar invertible matrices preserves +each query's Boolean defect rank. + +Zero or one query cannot satisfy (4): `D_r < N/2`, whereas +`2D_2=N(1-ell^(-2)) > N/2`. If there are two queries and one has rank one, +then, for the other rank `s`, + +\[ +D_1+D_s + 2`. Thus a two-query word has +both ranks at least two, and its tariff is at least `2H_2(m)`. This argument +already holds over any single odd prime field where the endpoint holds. + +## 4. Lifting the uniform endpoint to a group algebra + +Let `G` be the subgroup of `GL_(2d)(Q)` generated by the finite collection of +queried address maps together with `p` and `q`. Interpret the fixed word in +the matrix algebra over `F_2[G]`. Distinct group elements are distinct +rational linear maps; a fixed finite-field permutation representation need +not be faithful on this group algebra. + +Nevertheless, the uniform endpoint (1) implies its formal `F_2[G]` version. +To see this, collect the finitely many distinct labels in each coefficient of +`WJ-JD`. For the finite union of these labels, choose an integer address `z` +such that all `g^{-1}z` are distinct over `Q`. Such a choice exists: each +coincidence is a proper rational linear subspace, and a finite union of these +subspaces cannot cover all integer vectors. More explicitly one can use +`z=(1,t,...,t^(2d-1))` for an integer `t` avoiding the roots of finitely many +nonzero rational polynomials. + +Clear denominators and, for each pair of distinct images, select one nonzero +integer coordinate of their difference. Outside the finitely many primes +dividing these selected numerators or denominators, the images remain +distinct after reduction. For a chosen input register, an indicator VALUE +function at any one of these images separates its coefficient from all other +labels, when the output is evaluated at `z`. Hence a nonzero formal +coefficient would violate (1) at every sufficiently large prime. This proves +the formal identity. + +This step uses fixed finite data and uniform correctness over sufficiently +large odd primes. It does not assert a lower bound for arbitrary +modulus-dependent words from one fixed-field representation. + +## 5. Three rank-one queries are impossible, including clean ancillas + +The determinant sign of a rational address map defines a homomorphism + +\[ +G\longrightarrow C_2,\qquad g\longmapsto t^{\sigma(g)}, +\] + +where `sigma(g)=0` for positive determinant and `1` for negative determinant. +All generators have determinant `+1` or `-1`. For a rank-`r` partial swap this +image is `t^r`. The induced ring map has codomain + +\[ +\mathbf F_2[C_2] + =\mathbf F_2[\varepsilon]/(\varepsilon^2),\qquad t=1+\varepsilon. +\] + +Suppose now that `k=3` and all three queries have rank one. Each label maps to +`1+epsilon`, while the even-rank target labels `p,q` both map to 1. Using the +formal identity from Section 4 and factorization (2), + +\[ +T_3T_2T_1\longmapsto I+\varepsilon(E_1+E_2+E_3). +\] + +Set + +\[ +U=\begin{pmatrix}u_1&u_2&u_3\end{pmatrix},\qquad +V=\begin{pmatrix}v_1\\v_2\\v_3\end{pmatrix}. +\] + +The constant coefficient of (1) is (3); its `epsilon` coefficient is +`SUVJ=0`. Since `S` is invertible, + +\[ +UVJ=0. \tag{5} +\] + +On the other hand, expand the ordered product `T_3T_2T_1-I` in `F_2[G]`. +Each scalar matrix multiplying an address word is a linear combination of +nonempty ordered products of the `E_i`. Every such product has the form + +\[ +E_{i_1}\cdots E_{i_s} + =u_{i_1}(v_{i_1}u_{i_2})\cdots + (v_{i_{s-1}}u_{i_s})v_{i_s}. +\] + +Therefore every group-label coefficient of + +\[ +WJ-J=S(T_3T_2T_1-I)J +\] + +has image contained in `im(SU)` and row space contained in `row(VJ)`. +Cancellation or coinciding address words cannot enlarge either containing +space. + +But the two distinct nonidentity target labels `p` and `q` have respective +coefficient matrices `e_1 e_1^T J` and `e_2 e_2^T J` in `JD-J`. Their images +span two independent register directions and their rows span two independent +input directions. Thus + +\[ +\operatorname{rank}U\ge2,\qquad +\operatorname{rank}(VJ)\ge2. +\] + +Sylvester's rank inequality over `F_2` now gives + +\[ +\operatorname{rank}(UVJ) + \ge \operatorname{rank}U+\operatorname{rank}(VJ)-3 + \ge1, +\] + +contradicting (5). This excludes three rank-one queries without assuming that +the clean inputs were arbitrary. It also does not require noncommutativity, +an intersection condition on the two projector images, or a bounded number +of restored spectators beyond finiteness. + +For comparison, in the dirty-only case a shorter parity argument is +available: taking determinants after the same ring map gives +`t^(sum r_i)=det(D)=1`, hence `sum r_i` is even. Each conjugated query has a +rank-one register coupling and determinant `t^r`; every scalar invertible +`F_2` matrix has determinant 1. This square-operator determinant argument alone +would not justify the clean-ancilla extension; the rectangular argument above +supplies it. + +## 6. Completing the tariff bound + +Put `alpha=1-b`, so `0 <= alpha <= 1`, and divide all tariffs by `m^b`. + +- With at most one query the endpoint is impossible. +- With two queries, Section 3 gives a cost of at least `2*2^alpha`. +- With three queries, Section 5 excludes three rank-one queries. At least one + rank is therefore at least two, giving cost at least `2+2^alpha`, which is + at least `2*2^alpha` because `2^alpha <= 2`. +- With at least four queries, each has positive integer rank and costs at + least 1, giving total at least `4 >= 2*2^alpha`. + +The two direct rank-two queries meet the bound, proving the theorem for every +`b` in the closed interval, including both endpoints. + +## 7. Conditional application and remaining scope + +The theorem applies to a source rewrite only after its required endpoint has +been identified with (1), including all independent dirty columns and restored +rows. It permits jointly mixing the two dirty inputs with each other and with +any finite number of restored dirty or clean registers. The lower bound is +on their complete replacement operator, not on an individual spelling of the +two original queries. + +One sufficient application condition is a fixed rejoining cut followed by an +unchanged injective suffix, with equality of the entire final state required. +When a replacement introduces clean ancillas, compare both words on the same +extended state space and extend the frozen suffix by the identity on those +new slots. This common extension remains injective, so equality of the entire +final state forces equality of the whole state at the cut, including zero in +the new slots. Cleaning them later with added gates changes the extended +suffix even if every old suffix record remains present. + +The source-specific audit must still identify the cut, the independent inputs, +and the target operator. Equality of selected public outputs alone does not +supply this implication. A changed later compensation or cleanup word is a +different endpoint problem and is not excluded by this theorem. + +The result charges only the stipulated query tariff with its independent +common parameter `m`; any native interpretation of that tariff is an inherited +conditional pricing premise, not a new conversion here. It does not certify a +native frame schedule, workspace or tape bound, integer precision bound, +compiler cost, or improved multiplication exponent. The field-uniform word, +linear scalar free gates, one-register queries, and complete endpoint are +substantive hypotheses. Other interfaces, nonlinear or address-dependent +free operations, and modulus-dependent constructions require new arguments. diff --git a/research/bit-joint-dirty-pair/README.md b/research/bit-joint-dirty-pair/README.md new file mode 100644 index 0000000000..507f2eb091 --- /dev/null +++ b/research/bit-joint-dirty-pair/README.md @@ -0,0 +1,165 @@ +# Joint dirty processing does not lower this pair's unary-query tariff + +For the two independently dirty rank-two inputs identified in +[PR4068](https://github.com/CrocSwap/integer-mult-bounds/pull/4068), the original +two queries attain the minimum tariff in the uniform unary-query model below. +Arbitrary scalar mixing and any finite number of restored dirty or initially +zero registers are allowed for free. The exact minimum remains +`2 Phi_m(2)`, where `Phi_m(r)=m^b r^(1-b)` and `0 <= b <= 1`. +There is no recursive-query saving or new kappa from this local mechanism. + +This is a written all-parameter proof with finite source and algebra controls, +not a proof-kernel certificate or a new native supplier. The substantive +premises are fixed rational address maps, one VALUE stream per query, scalar +mixing independent of the address, the same finite word for all sufficiently +large odd address primes, and restoration of the complete required state. +The price parameter `m` is independent of the address half-dimension `d`. + +## Actual source and endpoint + +The frozen input bytes are copied from PR4068 head +`5a34918402ae2c0c683d8820ad832970e77f6382` and independently pinned in +[INPUT-SOURCES.json](INPUT-SOURCES.json). This package starts from canonical +main `bb4bccbf42844d2801487450727c2f63e10d1d0f` and changes no predecessor. + +| Helper | Original record | Frames | Query rank | +|---|---:|---|---:| +| 413 | 23405 | 509 to 390 | 2 | +| 444 | 23424 | 509 to 392 | 2 | + +Both queries can be moved to the quiet cut before record23339, preserving the +remaining scalar word and frames. All660 ordinary rows at that cut are +independently arbitrary: a complete inverse-prefix replay returns their660 +input columns. The existing private slot660 is inactive and zero. The proof +grants access to additional clean scratch as a favorable relaxation, so it +does not depend on treating that private slot as dirty or unavailable. + +The two rank-two increment projectors `P,Q` satisfy `(PQ-QP)[0,1]=1/8`. +Their partial-swap address labels `p=S(P), q=S(Q)` are distinct. A nonzero +dyadic minor `1/256` also certifies `rank[P Q]=4`; the principal proof does +not require that stronger geometric fact or noncommutativity. + +The required local operator is `diag(p,q,I,...)` on all arbitrary rows, +with initially zero auxiliary rows returned to zero. This is the necessary +endpoint for a replacement that rejoins the same injective suffix and +preserves the entire final state. Reversible ADD/MOVE operations and guarded +COPY/ERASE pairs make the frozen suffix injective on its valid states. +New auxiliary ports have identity continuation, or the same explicitly +injective continuation on both sides. Cleaning them later with new gates +changes the extended suffix even if every old record remains. +The earlier two-public-output minor alone would not justify this endpoint +for arbitrary perturbations to other source, helper or output rows. +A rewrite that changes later compensation has a different endpoint problem. + +## Why all cheaper call profiles fail + +[PROOF.md](PROOF.md) gives the full argument, including clean input columns. +Let `N=ell^(2d)`. A rank-r partial swap has Boolean operator defect rank +`D_r=N(1-ell^(-r))/2`. Scalar mixing fixes the constant-input normalization, +so query defects must supply the target's two independent defects `2D_2`. +This excludes one query of any rank and two queries with either rank equal +to one. In particular, replacing `(2,2)` by `(1,3)` is impossible. + +For three rank-one queries, fixed uniform correctness lifts to the formal +group algebra: finitely many distinct rational address maps separate on a +generic integer address and remain separated modulo all sufficiently large +good primes. The address determinant character then maps odd queries to +`1+epsilon`, with `epsilon^2=0`, while both targets map to1. If `U` collects +the three query output directions and `VJ` their arbitrary-input directions, +this forces `UVJ=0`. The two required target coefficients force both ranks +to be at least two, contradicting Sylvester's inequality through a +three-dimensional intermediate space. This argument allows clean ancillas. + +Writing `x=2^(1-b)`, with `1 <= x <= 2`, exhausts every call count: + +| Calls | Necessary normalized tariff | +|---:|---| +| 0 or1 | Impossible | +| 2 | Both ranks at least2, hence at least `2x` | +| 3 | Not all rank1, hence at least `2+x >= 2x` | +| 4 or more | At least `4 >= 2x` | + +The two original rank-two calls attain `2x`. Free workspace and scalar +operations only favor a proposed replacement; charging them cannot turn +this local result into a saving. + +The uniform-prime hypothesis is essential to the argument. Our explicit +control sums all24 coordinate permutations of four coordinates. It is a +nonzero formal group-algebra element whose Boolean operator is zero on +all81 addresses over F3, yet is nonzero at a separating F5 address. +A single finite-address representation cannot silently replace the bridge. + +## Packing proposals and their missing costs + +The direct-product carrier `H(x,y)=f(x)+g(y)`, together with the anchor +`c=f(0)`, encodes both functions injectively. Applying the single address +map `diag(p,q)` to H and decoding its slices gives `pf` and `qg` because +linear maps fix zero. Its partial-swap rank is four after reordering +coordinates. But its address carrier has `N^2` cells, plus the anchor, +instead of the original `2N` cells. Encoding, access, scratch, restoration +and the query's changed payload volume are unpriced. It cannot be invoiced +as one original-sized `Phi_m(4)` call. + +A tagged two-bank primitive could instead specify +`F(0,x)=f(x), F(1,x)=g(x)` and act by `(0,x)->(0,px)`, +`(1,x)->(1,qx)`. This is a precise functional interface, but it is a +tag-controlled choice between two address maps, not the admitted single +linear partial swap on the original carrier. Rank-two involutions can also +be conjugated to a common label, but encoding and decoding that conjugation +on one bank require address adapters and a justified enlarged-carrier tariff. +Neither construction supplies those missing native costs. + +Even the hypothetical tariff `Phi_m(4)` leaves only +`m^b(2x-x^2)` of margin against `2 Phi_m(2)`. Since `x(2-x) <= 1`, +one extra ordinary rank-one query consumes that entire margin. A useful +tagged mechanism therefore needs both a genuinely admitted joint tariff +and a packing/consumer contract with no additional ordinary query overhead. +These are interface proposals, not positive query savings. + +## Reproduction and evidence + +From the repository root: + +```sh +python3.12 -B scripts/research_package.py --package research/bit-joint-dirty-pair +``` + +The self-contained package also runs without Git, predecessor checkouts, +network access or writable package files: + +```sh +python3 -I -B /absolute/path/to/bit-joint-dirty-pair/verify.py +python3 -I -O -B /absolute/path/to/bit-joint-dirty-pair/verify.py +``` + +The verifier checks immutable input hashes, the focused source prefix and +local retiming, all660 independent columns, private-slot guards, exact +projector geometry, finite Boolean defect ranks, all32768 pairs of small +matrices in the stated Sylvester control, and the finite-field representation +counterexample. Complete canonical JSON receipts are compared, including +Boolean types. The code does not verify the all-parameter proof in a kernel. +Normal and optimized execution run the same checks. + +[REVIEW.md](REVIEW.md) records separate AI mathematical and source reviews. +[SOURCE-NOTES.md](SOURCE-NOTES.md) retains attribution and overlap limits. +No physical controller, owner allocation, all-size precision/storage proof, +changed whole-word histogram, supplier admission or selected-frontier change +is claimed. + +## Open next questions + +The next concrete route is a larger joint helper/consumer rewrite that changes +the full rejoin state and cancels its effects later. Pin its earliest changed +reader and every borrowed row, then compare the entire output map and paid +query profile. No such downstream word is supplied here, and a public-output +projection alone does not establish restoration. + +A second route is to implement the tagged two-bank interface with its true +payload volume, physical layout and full adapter/cleanup price. The first +test is whether an actual packet already supplies and consumes the needed +layout without paid conversion. Its joint recursive price remains unknown. +Structured relevance, first steps and blockers are in [TASK.json](TASK.json). + +Ross Richardson, with substantial OpenAI Codex assistance in mathematics, +implementation and writing, and separate AI checks. Apache-2.0. No independent +human or formal-kernel review is claimed. diff --git a/research/bit-joint-dirty-pair/RESULT.json b/research/bit-joint-dirty-pair/RESULT.json new file mode 100644 index 0000000000..f555297f24 --- /dev/null +++ b/research/bit-joint-dirty-pair/RESULT.json @@ -0,0 +1,513 @@ +{ + "finite_controls": { + "defect_rank": { + "actual_permutation_cases": [ + { + "address_dimension": 2, + "boolean_defect_rank": 0, + "fixed_addresses": 9, + "prime": 3, + "query_rank": 0 + }, + { + "address_dimension": 2, + "boolean_defect_rank": 3, + "fixed_addresses": 3, + "prime": 3, + "query_rank": 1 + }, + { + "address_dimension": 4, + "boolean_defect_rank": 0, + "fixed_addresses": 81, + "prime": 3, + "query_rank": 0 + }, + { + "address_dimension": 4, + "boolean_defect_rank": 27, + "fixed_addresses": 27, + "prime": 3, + "query_rank": 1 + }, + { + "address_dimension": 4, + "boolean_defect_rank": 36, + "fixed_addresses": 9, + "prime": 3, + "query_rank": 2 + }, + { + "address_dimension": 6, + "boolean_defect_rank": 0, + "fixed_addresses": 729, + "prime": 3, + "query_rank": 0 + }, + { + "address_dimension": 6, + "boolean_defect_rank": 243, + "fixed_addresses": 243, + "prime": 3, + "query_rank": 1 + }, + { + "address_dimension": 6, + "boolean_defect_rank": 324, + "fixed_addresses": 81, + "prime": 3, + "query_rank": 2 + }, + { + "address_dimension": 6, + "boolean_defect_rank": 351, + "fixed_addresses": 27, + "prime": 3, + "query_rank": 3 + }, + { + "address_dimension": 4, + "boolean_defect_rank": 0, + "fixed_addresses": 625, + "prime": 5, + "query_rank": 0 + }, + { + "address_dimension": 4, + "boolean_defect_rank": 250, + "fixed_addresses": 125, + "prime": 5, + "query_rank": 1 + }, + { + "address_dimension": 4, + "boolean_defect_rank": 300, + "fixed_addresses": 25, + "prime": 5, + "query_rank": 2 + } + ], + "even_address_characteristic_does_not_have_strict_gap": true, + "normalized_target_minus_relaxed_rank1_plus_any_rank": { + "11": "9/242", + "3": "1/18", + "5": "3/50", + "7": "5/98" + } + }, + "limits": [ + "finite controls do not prove the all-parameter theorem", + "the uniform-prime bridge is a written proof", + "no changed consumer or native execution is verified" + ], + "no_new_kappa": true, + "odd_call_rank_obstruction": { + "complete_matrix_pairs": 32768, + "four_columns_allow_zero_product_with_two_directions": true, + "one_direction_allows_two_columns": true, + "pairs_with_both_ranks_at_least_two": 19404, + "zero_products_in_that_class": 0 + }, + "status": "PASS_FINITE_JOINT_QUERY_CONTROLS", + "uniformity_control": { + "F3_addresses_with_zero_operator_column": 81, + "F5_generic_point": [ + 0, + 1, + 2, + 3 + ], + "distinct_images_at_F5_point": 24, + "formal_support_size": 24, + "scope": "S4 coordinate-permutation example; not a counterexample to the uniform-prime bridge" + }, + "written_tariff_reduction": { + "attainment": "the original separate rank-two queries", + "four_or_more_queries": "cost >= 4 >= 2*x", + "three_queries": "not all rank one; cost >= 2+x >= 2*x", + "two_queries": "each rank >= 2; cost >= 2*x", + "x": "2^(1-b), with 1 <= x <= 2 for 0 <= b <= 1", + "zero_or_one_queries": "impossible by actual-action defect rank" + } + }, + "source": { + "address_displacement_concat_rank_over_Q": 4, + "address_swap_commutator_0_1": "1/4", + "commutator_0_1": "1/8", + "entrance_cut": 23339, + "geometric_concat_rank_over_Q": 4, + "geometric_minor": { + "columns": [ + 0, + 1, + 8, + 9 + ], + "determinant": "1/256", + "rows": [ + 0, + 1, + 2, + 4 + ] + }, + "independent_dirty_pivot": [ + [ + 1, + 0 + ], + [ + 0, + 1 + ] + ], + "limits": [ + "prefix and local retiming only; no repeated full-word metric audit", + "address geometry over Q is not a representation of payload F2[G]", + "formal common-cut diagonal endpoint requires its own algebra theorem", + "no changed-tail or source-compensation lower bound", + "no native physical execution, recursive moment improvement or new kappa" + ], + "negative_controls": { + "Q_replaced_by_P_collapses_concat_rank": true, + "Q_replaced_by_P_fails_noncommutation": true, + "clean_private_COPY_ERASE_control_accepted": true, + "dirty_private_port_rejected_by_original_COPY": true, + "discarding_independent_dirty_input_loses_rank": true, + "omitted_second_query_fails_frame_contract": true + }, + "no_new_kappa": true, + "ordinary_independent_input_columns": 660, + "predecessor_head": "5a34918402ae2c0c683d8820ad832970e77f6382", + "prefix_columns_sha256": "ed967ce61b4f04e73d8cf6c281ec880ee3ff03a2eb80d7af400e8716dee6e756", + "prefix_inverse_returns_all_660_columns": true, + "private_port": { + "contract": "inactive private zero, not a free active arbitrary-dirty role", + "first_future_COPY_record": 23524, + "frame": null, + "index": 660, + "prior_COPY_count": 0, + "value": "zero" + }, + "projectors": { + "P": [ + [ + "1/4", + "-1/4", + "0", + "0", + "1/4", + "-1/4", + "0", + "0" + ], + [ + "-1/4", + "1/2", + "0", + "1/4", + "0", + "1/4", + "-1/4", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "1/4", + "0", + "1/4", + "1/4", + "0", + "-1/4", + "0" + ], + [ + "1/4", + "0", + "0", + "1/4", + "1/2", + "-1/4", + "-1/4", + "0" + ], + [ + "-1/4", + "1/4", + "0", + "0", + "-1/4", + "1/4", + "0", + "0" + ], + [ + "0", + "-1/4", + "0", + "-1/4", + "-1/4", + "0", + "1/4", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ] + ], + "Q": [ + [ + "1/2", + "-1/4", + "-1/4", + "0", + "1/4", + "0", + "0", + "-1/4" + ], + [ + "-1/4", + "1/4", + "1/4", + "1/4", + "0", + "0", + "0", + "0" + ], + [ + "-1/4", + "1/4", + "1/4", + "1/4", + "0", + "0", + "0", + "0" + ], + [ + "0", + "1/4", + "1/4", + "1/2", + "1/4", + "0", + "0", + "-1/4" + ], + [ + "1/4", + "0", + "0", + "1/4", + "1/4", + "0", + "0", + "-1/4" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "-1/4", + "0", + "0", + "-1/4", + "-1/4", + "0", + "0", + "1/4" + ] + ], + "common_frame": [ + [ + "1/2", + "1/4", + "1/4", + "0", + "-1/4", + "0", + "0", + "1/4" + ], + [ + "1/4", + "1/2", + "0", + "-1/4", + "0", + "-1/4", + "1/4", + "0" + ], + [ + "1/4", + "0", + "1/2", + "-1/4", + "0", + "1/4", + "-1/4", + "0" + ], + [ + "0", + "-1/4", + "-1/4", + "1/2", + "-1/4", + "0", + "0", + "1/4" + ], + [ + "-1/4", + "0", + "0", + "-1/4", + "1/2", + "1/4", + "1/4", + "0" + ], + [ + "0", + "-1/4", + "1/4", + "0", + "1/4", + "1/2", + "0", + "1/4" + ], + [ + "0", + "1/4", + "-1/4", + "0", + "1/4", + "0", + "1/2", + "1/4" + ], + [ + "1/4", + "0", + "0", + "1/4", + "0", + "1/4", + "1/4", + "1/2" + ] + ] + }, + "query_rank_profile": { + "2": 2 + }, + "query_records": { + "23405": [ + 0, + 413, + 509, + 390, + 2, + 0 + ], + "23424": [ + 0, + 444, + 509, + 392, + 2, + 0 + ] + }, + "quiet_window_half_open": [ + 23339, + 23405 + ], + "record_indexing": "zero based original WORD", + "retimed_all_columns_and_frames_equal": true, + "retimed_end_columns_sha256": "46bdd46c654e1f2225693a5ee516173a823fc1575435890aa7b85f4b17c33d7b", + "retimed_local_inverse_checked": true, + "retimed_window_half_open": [ + 23339, + 23426 + ], + "selected_common_frame": 509, + "selected_rows": { + "17": { + "17": 1 + }, + "413": { + "17": 1, + "22": 1, + "33": 1, + "413": 1, + "469": -1, + "60": 1, + "605": -1, + "67": 1, + "87": 1, + "92": 1 + }, + "444": { + "17": 1, + "22": 1, + "33": 1, + "369": -1, + "38": 1, + "444": 1, + "60": 1, + "77": 1, + "87": 1, + "92": 1 + } + }, + "source17_unchanged_until_before": 24523, + "source_hashes": { + "inputs/GEOMETRY.json.gz": "a353999bceac4ac957f540adfd3e5f8768297138b27132eeb83332e2ea4b1022", + "inputs/PREDECESSOR-PINS.json": "4d03736c497eae94c4e98d33ac10ecacba9e914f9d604787237ff71075dc4e94", + "inputs/WORD.json.gz": "c46ccd7d3eedabc6a7efbb1a91ec13f2928bad8ee0bac57c6e593a092d13d96c" + }, + "status": "PASS_ACTUAL_JOINT_DIRTY_SOURCE_BINDING", + "trace_commutator_squared": "-1", + "word_canonical_sha256": "3bca74a2a8427eb18e86566baa19de597f10d0bc40c30b7443febd499ee2189a" + } +} diff --git a/research/bit-joint-dirty-pair/REVIEW.md b/research/bit-joint-dirty-pair/REVIEW.md new file mode 100644 index 0000000000..705427f422 --- /dev/null +++ b/research/bit-joint-dirty-pair/REVIEW.md @@ -0,0 +1,122 @@ +# Final scoped package review + +Reviewed the root-authored README, verifier wrapper, finite-control checker, +and source checker in `research/bit-joint-dirty-pair`. The all-parameter proof +was checked only for consistency with those claims, not independently +re-reviewed by its author. No full suite was rerun. The root owns final normal, +optimized, read-only-export, and mutant runs; their manifest/results were not +complete when this review began. + +## Verdict + +No remaining blocking mathematical or implementation finding in the reviewed +bytes. One source-to-execution binding issue was reported and fixed during +review. The README accurately limits the optimum to the uniform unary-query +full-endpoint model and keeps native packing and changed-tail questions open. + +## Reported issue and verified correction + +The initial `verify.py` hashed each child source and subsequently executed its +pathname. The bytes executed were therefore not bound to the authenticated +snapshot. This was an integrity gap, not a counterexample to the mathematics. + +The corrected `verify.py:10-17,44-47` bootstrap reads the child once, compares +its hash with the retained manifest value, and compiles those identical bytes. +It sets the correct `__file__` and `__name__` and retains isolated/optimized +interpreter flags. At lines50-57 the expected receipt is parsed from the +authenticated bytes, and package bytes/inventory are checked again afterward. +A focused wrong-hash subprocess probe rejected with +`executed checker hash check.py` before producing any checker output. This +probe did not execute either full checker. + +## Claim and capacity checks + +- **Full endpoint and clean continuation (README:42-52).** The source pair is + compared at a common cut with all ordinary rows independently arbitrary. + The same injective suffix must act on the same extended state space. The + added clarification correctly gives new ancillary slots identity + continuation, or an identical injective continuation in both words. Later + new cleanup gates change that extended suffix even when old records remain. + The corresponding clarification was added, under explicit parent ownership + authorization, to the proof's application paragraph. Public-output equality + alone remains insufficient. + +- **Product carrier (README:94-101).** The proposed encoding is injective: + with `H(x,y)=f(x)+g(y)` and `c=f(0)`, recover + `g(y)=H(0,y)+c`, `g(0)=H(0,0)+c`, and + `f(x)=H(x,0)+H(0,0)+c`. A linear address map fixes zero, so the same slice + identities decode after applying `diag(p,q)`. Reordering the two address + halves identifies this map with `S(P direct_sum Q)`, whose projector rank + is four. However the carrier has `N^2` VALUE cells plus the anchor, versus + `2N` original cells. The text does not invoice this larger payload as a + native original-size rank-four call or omit the unpriced encoding/cleanup. + +- **Tagged interface (README:103-110).** Choosing `p` or `q` according to a + bank tag is not the stated single linear partial swap on the original + address carrier. Conjugating one target to a common label does not make the + bank's address adapters free. The text preserves both missing obligations: + an admitted joint primitive and its actual carrier/adapter tariff. + +- **Hypothetical margin (README:112-117).** For `x=2^(1-b)` in `[1,2]`, + `Phi_m(4)=m^b x^2` and the optimistic saving is + `m^b*x*(2-x)=m^b*(1-(x-1)^2) <= m^b=Phi_m(1)`. Thus one extra ordinary + positive-rank query eliminates any strict saving under this hypothetical + price. At `b=1` it exactly consumes the margin; at `b=0` the initial margin + is zero. No positive saving is claimed. This is a necessary overhead screen, + not proof of an implementable tagged supplier. + +- **Tariff and geometry scope (README:3-16,37-40,54-90).** The price parameter + `m` is separated from address half-dimension `d`. Distinct/noncommuting + rational projector geometry is not used as a faithful representation of + payload `F_2[G]`. The finite-field kernel example supports the caution, while + the actual uniform lifting step remains a written proof. The minimum is + conditioned on a fixed finite word, scalar address-independent free gates, + one VALUE stream per paid query, and the complete endpoint. + +## Code coverage assessment + +`check.py` correctly implements bit-packed GF(2) row elimination and matrix +multiplication for the stated dimensions. The 32768 Sylvester cases are all +512 binary 3-by-3 matrices times all64 binary 3-by-2 matrices. Its four-column +and one-output positive controls prevent treating the three-column/two-output +obstruction as universal. The direct permutation controls measure Boolean +defect rank, rather than merely substituting the predicted formula. Their +coordinate-projector samples are expressly finite controls, not an exhaustive +test of all rational projectors. The S4 toggle computation really sums all24 +distinct formal labels and cancels on every F3 address; the F5 tuple has24 +distinct images. No fixed-field faithfulness is inferred. + +`source_check.py` authenticates the frozen compressed inputs before +decompressing those same bytes. Its prefix replay checks660 independent +columns, common frames, private-slot guards, and the exact inverse. The quiet +window predicates cover both reads and writes of the two selected helpers; +therefore moving the two queries across that window does not silently cross a +reader. Local retiming compares every row and frame and checks its literal +inverse. Exact rational geometry reconstructs P,Q from the supplied lines, +checks idempotence/rank/nesting/dyadic entries, and verifies the specified +commutator and nonzero rank-four minor. These are sufficient for the stated +source pair; they are not a new full-word precision or changed-tail audit. + +The wrapper compares complete canonical JSON receipts, including Boolean +values distinct from integer one, and all substantive checks use explicit +exceptions rather than assertions. This supports equal normal/optimized +coverage, subject to the root's pending complete executions. + +The omitted-query negative control in the source checker accepts any +`ValueError`; its current fixture is rejected by the next frame contract. +Making that control reason-specific would be optional hardening. No present +claim relies on interpreting an unrelated exception as a mathematical proof, +and this review does not treat that stylistic improvement as a blocker. + +## Reviewed content hashes + +| File | SHA256 | +|---|---| +| README.md | `b307851d4260d59391ff77c25a7332baf81bba59f8843a98e77b97959ab8f3b1` | +| verify.py | `bcb67a10939ba0b5c42005972f2c9bf9bb7e0dad8d1067c17b10ec179a9abfc0` | +| check.py | `c1cf94026e5733784dfa1d92ba007a7b6e2d3148e33e7daf88630cdfdef7c01b` | +| source_check.py | `cfd840feef006198d3efe27560cf034719dea6831825e48b466360851b7bf421` | +| PROOF.md (consistency only) | `be917cba2bac53328ca6471c9a40720b11b3b686d93d3654758be9c10e1c7e69` | + +This review does not certify the not-yet-generated manifest/receipts, a native +cost conversion, publication, human review, or a formal-kernel theorem. diff --git a/research/bit-joint-dirty-pair/SOURCE-NOTES.md b/research/bit-joint-dirty-pair/SOURCE-NOTES.md new file mode 100644 index 0000000000..63cb82c0ca --- /dev/null +++ b/research/bit-joint-dirty-pair/SOURCE-NOTES.md @@ -0,0 +1,94 @@ +# Sources, attribution and overlap + +This user-assigned follow-up starts from canonical +`bb4bccbf42844d2801487450727c2f63e10d1d0f`, priority revision6, and the +frozen shared-source package in +[PR4068](https://github.com/CrocSwap/integer-mult-bounds/pull/4068) at +`5a34918402ae2c0c683d8820ad832970e77f6382`. That predecessor saves four +scalar ADDs and identifies the two independent dirty query inputs; it does +not claim a recursive-query saving. Its new query-sharing question motivates +this package's broader scalar-mixing model and precise fixed-join answer. + +The bundled WORD and GEOMETRY are copied byte for byte from that public head. +Their paths and hashes are in [INPUT-SOURCES.json](INPUT-SOURCES.json). +The unchanged `inputs/PREDECESSOR-PINS.json` records historical lineage at +`8eefab699338b93400ca72ab22c6cf64352f7e05` and +`b628ba738802587a38e61affaa01fd188d0644f9`. Public byte-identical archives +also occur in [PR4021](https://github.com/CrocSwap/integer-mult-bounds/pull/4021) +at `c01f97ecfc7fa64847f6abd8f7b231e1df8c7b70`, as recorded in PR4068's +PUBLIC-PREDECESSOR.json. Reproduction needs only the bundled copies, not +historical local commits or checkouts. + +The source lineage credits Ali Romman's R438/PR1043 substitution, Sagar +Thakrar's transported word and window analysis, PR540 frame conventions, +PR589 hosting, PR1023 width-eight hosting, and the five-terminal package. +The retained controller lineage credits DreamingOfClouds, Zhihao Chen, +eumemic and chafreaky. These constructions are inherited, not new results. +The focused source checker was written for this package without importing +the producer implementation; the full predecessor metric audit is not repeated. + +## Mathematical antecedents + +Jose Manuel's +[two-register-three-mix / PR2108](https://github.com/CrocSwap/integer-mult-bounds/blob/bb4bccbf42844d2801487450727c2f63e10d1d0f/research/two-register-three-mix/README.md) +(package commit `b25eb9b6a95d8b644c582a5c0d8229bc2ffc3eb7`) is a direct +antecedent: two registers, arbitrary group and field, at most three +nonmonomial scalar blocks, and full group-diagonal endpoint admit unary +routes without increasing a subadditive tariff. A two-query word has at +most three scalar blocks, so the no-ancilla two-query case is not presented +as a new general discovery. Its bounded operator-separation argument also +motivates care about formal versus actual address actions. + +The source-archived +[S4 four-role census](https://github.com/CrocSwap/integer-mult-bounds/blob/bb4bccbf42844d2801487450727c2f63e10d1d0f/research/s4-noncommuting-threecycle-r4-seeda27b/README.md) +at package commit `90405b9498e4abfdd7d0eececcf11c7e83c6d13b` +uses formal F2[S4], four dirty roles and adjacent-transposition labels to +certify four-call minima for eight three-cycle target pairs. Its fixed +alphabet, role count and unit tariff differ from the present actual +rank-two involution pair and arbitrary finite clean/dirty ancilla allowance. + +The +[binary-affine register bound](https://github.com/CrocSwap/integer-mult-bounds/blob/bb4bccbf42844d2801487450727c2f63e10d1d0f/research/binary-affine-register-bound/PROOF.md) +at `7f25b6d0e1d7e995d4d2840f231d98b1a1a9fec2` is a precedent for +augmentation normalization and representation-rank bounds with arbitrary +restored dirty registers. Its homogeneous address representation has +characteristic two. Rational dyadic address matrices cannot simply be +substituted into that representation over the payload field F2. + +The +[nonlinear frame-cut bound](https://github.com/CrocSwap/integer-mult-bounds/blob/bb4bccbf42844d2801487450727c2f63e10d1d0f/research/nonlinear-frame-cut-bound/README.md) +at `78a1810e44bf08f845252cfe4c785ccc967c07a2` gives weighted cut +certificates and a common-flag corollary. The present pair has +`tr([P,Q]^2)=-1`, excluding simultaneous triangularization over any +characteristic-zero extension, so that common-flag corollary is not used +to certify this pair. Its general certificate framework is not refuted. + +These sources were read for attribution and scope; their full suites were +not rerun or silently imported as broader theorems. Defect rank, +telescoping, generic-point separation, the sign quotient and Sylvester's +inequality are standard tools. The contribution here is their complete +source-bound tariff argument, including clean input columns and the +explicit field-uniformity premise, together with reproducible controls. + +## Interface leads and limits + +Hanson Sun's [PR1522](https://github.com/CrocSwap/integer-mult-bounds/pull/1522), +building on Ross Richardson's PR953 and Wentao Li's PR840, already gives +restored source tours for distinct additive outputs. These do not supply +the missing action on two independent dirty helper inputs. The tagged +joint-child proposal in [PR1764](https://github.com/CrocSwap/integer-mult-bounds/pull/1764) +was read through its cached metadata/body as an interface lead; its source +implementation was not replayed or used as proof of an admitted BIT tariff. +Our product-carrier and tagged-bank discussion is explicitly conditional. + +The entry overlap scan at 2026-10-19T21:06:25.817477Z covered797 open PRs +and2627 Discussion records with complete pagination and no warnings. It +searched public titles/bodies and local package notes, not every code diff +or all closed PRs; it is not a novelty certificate. The three coordination +hubs and relevant nearby package statements were read. Local standalone +scope and review records preserve the full scan and exact source reads. + +The selected record and its inherited supplier assumptions remain unchanged. +No global BIT lower bound, native supplier admission, outer recurrence +improvement, human certification or new kappa is claimed. Ross Richardson, +with substantial OpenAI Codex assistance and separate AI review. Apache-2.0. diff --git a/research/bit-joint-dirty-pair/SOURCES.json b/research/bit-joint-dirty-pair/SOURCES.json new file mode 100644 index 0000000000..902d9ac98f --- /dev/null +++ b/research/bit-joint-dirty-pair/SOURCES.json @@ -0,0 +1,19 @@ +{ + "schema_version": 1, + "base_commit": "bb4bccbf42844d2801487450727c2f63e10d1d0f", + "files": [ + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5", + "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0" + }, + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ], + "bundled_input_provenance": "INPUT-SOURCES.json authenticates copies from public PR4068 head5a34918402ae2c0c683d8820ad832970e77f6382; inputs/PREDECESSOR-PINS.json preserves older lineage. Replay needs no predecessor checkout." +} diff --git a/research/bit-joint-dirty-pair/TASK.json b/research/bit-joint-dirty-pair/TASK.json new file mode 100644 index 0000000000..612645089e --- /dev/null +++ b/research/bit-joint-dirty-pair/TASK.json @@ -0,0 +1,68 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "base_commit": "bb4bccbf42844d2801487450727c2f63e10d1d0f", + "original_card": { + "id": "bit-new-register-model", + "question": "Can an explicitly larger or nonabelian register model escape the scoped three-register obstruction?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/bit-three-register-lower-bound/README.md", + "certificates/selected-result.json", + "research/bit-gl3-mixed-targets-length10/README.md", + "docs/research/community-efficient1000-review.md" + ], + "methods": [ + "Construct the smallest exact identity in a newly specified legal operation alphabet.", + "Derive a target-specific relaxation bound for that same explicit alphabet." + ], + "acceptance_gate": "Name the changed hypothesis, all counted roles and a uniform identity; finite column tests alone do not certify it. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read Model section 1 of the three-register bound and identify the exact excluded free operations.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "First compare the alphabet, role count and length with the fully replayed #1974 census and #2027 mixed-root tariff. Identify a changed premise and a legal native implementation; then price one smallest completed instance before searching larger words.", + "bottleneck_link": "A small-width completed saving changes the bit primitive; a finite-address identity alone is insufficient.", + "allowed_variations": [ + "Choose a fixed larger register count or a specified nonabelian operation family." + ], + "scope_change_triggers": [ + "Remaining inside the already-excluded three-register abelian model.", + "Repeating the two-register GL3 census or a covered three-register length without changing a hypothesis; a formal group-algebra word without native conversion is a partial result." + ], + "overlap_terms": [ + "three-register", + "nonabelian", + "group algebra" + ] + }, + "scope_status": "changed", + "actual_scope": "Decide the local recursive-query cost of jointly processing the two independently dirty rank-two helper inputs from PR4068, allowing arbitrary free scalar mixing and finite restored dirty or clean ancillas, in a fixed uniform rational unary-query model.", + "scope_change_reason": "User-assigned follow-up to the source-only screen. This is an actual-pair theorem with an explicit uniform-prime and full-state rejoin contract, not the entire catalogue question.", + "bottleneck_link": "The shared-source four-ADD saving has zero query delta. A local joint rewrite would need to beat the two rank-two calls to improve the recursive query profile.", + "stop_rule": "Close the fixed local mechanism if even a relaxation granting free scalar mixing and clean/dirty workspace has the original tariff as a sharp lower bound; do not declare a global supplier obstruction.", + "evidence": "PROOF.md; RESULT.json; REVIEW.md; README.md", + "author": "Ross Richardson", + "ai_assistance": "Substantial OpenAI Codex mathematics, implementation and writing, with separate AI constructive, source and proof checks; no independent human or proof-kernel review.", + "outcome": "negative-result", + "open_questions": [ + { + "question": "Can a larger joint helper/consumer rewrite eliminate one transformed independent demand without repaying its query cost?", + "why_it_matters": "The sharp local floor requires full state equality before the same suffix; changing future compensation changes that contract.", + "first_step": "Pin the earliest changed consumer, specify every borrowed row and compare the full resulting input/output map and complete query histogram.", + "blocked_by": "No changed downstream word or paid restoration schedule has been constructed here." + }, + { + "question": "Can a two-bank controlled query be implemented at a genuinely subadditive total tariff?", + "why_it_matters": "Calling a tagged direct sum one query does not establish its recursive cost.", + "first_step": "Specify the physical bank layout, permitted tag alphabet, address adapters, recursive child and complete packing/unpacking bill; compare with 2 Phi_m(2).", + "blocked_by": "The joint primitive and its price are hypotheses, not supplied mechanisms; any extra ordinary paid query consumes the optimistic rank-four margin." + } + ] +} diff --git a/research/bit-joint-dirty-pair/VERIFY.json b/research/bit-joint-dirty-pair/VERIFY.json new file mode 100644 index 0000000000..0243b1d861 --- /dev/null +++ b/research/bit-joint-dirty-pair/VERIFY.json @@ -0,0 +1,33 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/bit-joint-dirty-pair/inputs/WORD.json.gz", + "research/bit-joint-dirty-pair/inputs/GEOMETRY.json.gz" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Focused source binding, complete source-prefix columns, local retiming and finite defect/Sylvester/uniformity controls; full receipts and file hashes. Written proof is not kernel-checked." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "The same coverage with assertions disabled; canonical JSON receipts must still match, including Boolean types." + } + ] +} diff --git a/research/bit-joint-dirty-pair/check.py b/research/bit-joint-dirty-pair/check.py new file mode 100644 index 0000000000..664423dad4 --- /dev/null +++ b/research/bit-joint-dirty-pair/check.py @@ -0,0 +1,157 @@ +#!/usr/bin/env python3 +"""Finite controls for the written joint-dirty query bound; not a proof kernel. + +Apache-2.0. Ross Richardson, with substantial OpenAI Codex assistance. +Only Python's standard library is used; normal execution writes no files. +""" +from fractions import Fraction +from itertools import permutations, product +import json + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def binary_rank(rows): + pivots = {} + for row in rows: + while row: + pivot = row.bit_length() - 1 + if pivot in pivots: + row ^= pivots[pivot] + else: + pivots[pivot] = row + break + return len(pivots) + + +def multiply(a, b): + """Rows of a encode coefficients selecting whole rows of b.""" + out = [] + for row in a: + value = 0 + for j, selected in enumerate(b): + if row >> j & 1: + value ^= selected + out.append(value) + return tuple(out) + + +def defect_controls(): + results = [] + for prime, half_dimension in ((3, 1), (3, 2), (3, 3), (5, 2)): + dimension = 2 * half_dimension + addresses = list(product(range(prime), repeat=dimension)) + index = {v: i for i, v in enumerate(addresses)} + size = len(addresses) + for rank in range(half_dimension + 1): + action = [] + for point in addresses: + moved = list(point) + for i in range(rank): + moved[i], moved[half_dimension+i] = moved[half_dimension+i], moved[i] + action.append(index[tuple(moved)]) + require(all(action[action[i]] == i for i in range(size)), 'involution') + fixed = sum(i == j for i, j in enumerate(action)) + # The independently eliminated Boolean matrix is I + permutation. + measured = binary_rank((1 << i) ^ (1 << j) for i, j in enumerate(action)) + predicted_fixed = prime ** (dimension-rank) + predicted_defect = (size-predicted_fixed)//2 + require(fixed == predicted_fixed and measured == predicted_defect, + 'actual permutation defect formula') + results.append({'prime': prime, 'address_dimension': dimension, + 'query_rank': rank, 'fixed_addresses': fixed, + 'boolean_defect_rank': measured}) + # With one rank-one query and any second rank, the upper bound remains + # strictly below the two-rank-two target. The written proof covers all q>2. + gaps = {str(q): str(Fraction(q-2, 2*q*q)) for q in (3, 5, 7, 11)} + require(all(Fraction(v) > 0 for v in gaps.values()), 'strict two-call gap') + require(Fraction(2-2, 2*2*2) == 0, 'characteristic-two boundary control') + return {'actual_permutation_cases': results, + 'normalized_target_minus_relaxed_rank1_plus_any_rank': gaps, + 'even_address_characteristic_does_not_have_strict_gap': True} + + +def sylvester_controls(): + # All U in M_3(F2) and VJ in M_(3,2)(F2). This finite check corroborates + # the written all-dimension inequality; it does not supply its quantifier. + cases = 0 + both_ranks_at_least_two = 0 + zero_products = 0 + for u in product(range(8), repeat=3): + rank_u = binary_rank(u) + for v in product(range(4), repeat=3): + cases += 1 + rank_v = binary_rank(v) + rank_uv = binary_rank(multiply(u, v)) + require(rank_uv >= rank_u+rank_v-3, 'Sylvester inequality') + if rank_u >= 2 and rank_v >= 2: + both_ranks_at_least_two += 1 + zero_products += rank_uv == 0 + require(cases == 32768 and zero_products == 0, 'three-column obstruction') + # Four odd calls are allowed by this quotient: two duplicate columns/rows + # give UV=0 with both ranks two. The invariant must not reject this case. + u4 = (0b0101, 0b1010) + v4 = (0b01, 0b10, 0b01, 0b10) + require(binary_rank(u4) == binary_rank(v4) == 2 and multiply(u4, v4) == (0, 0), + 'four-column boundary positive control') + # A single required target direction does not force both ranks to be two. + u2, v2 = (0b11,), (1, 1) + require(binary_rank(u2) == binary_rank(v2) == 1 and multiply(u2, v2) == (0,), + 'one-output boundary positive control') + return {'complete_matrix_pairs': cases, + 'pairs_with_both_ranks_at_least_two': both_ranks_at_least_two, + 'zero_products_in_that_class': zero_products, + 'four_columns_allow_zero_product_with_two_directions': True, + 'one_direction_allows_two_columns': True} + + +def representation_controls(): + # A concrete reason a single finite address field cannot simply be called + # a faithful group-algebra model. S4 permutes four coordinates over F3. + # Every point has a repeated coordinate; its stabilizer has even order. + # Thus the sum of all 24 formal group elements is a nonzero formal vector + # whose Boolean permutation operator vanishes on all 81 addresses. + group = list(permutations(range(4))) + zero_columns = 0 + for point in product(range(3), repeat=4): + odd_images = set() + for permutation in group: + image = tuple(point[i] for i in permutation) + if image in odd_images: + odd_images.remove(image) + else: + odd_images.add(image) + zero_columns += not odd_images + require(len(group) == 24 and zero_columns == 81, 'fixed-field algebra kernel') + generic = (0, 1, 2, 3) + images = {tuple(generic[i] for i in permutation) for permutation in group} + require(len(images) == 24, 'generic point separates all labels over F5') + return {'formal_support_size': 24, 'F3_addresses_with_zero_operator_column': zero_columns, + 'F5_generic_point': list(generic), 'distinct_images_at_F5_point': len(images), + 'scope': 'S4 coordinate-permutation example; not a counterexample to the uniform-prime bridge'} + + +def main(): + result = {'status': 'PASS_FINITE_JOINT_QUERY_CONTROLS', + 'defect_rank': defect_controls(), + 'odd_call_rank_obstruction': sylvester_controls(), + 'uniformity_control': representation_controls(), + 'written_tariff_reduction': { + 'x': '2^(1-b), with 1 <= x <= 2 for 0 <= b <= 1', + 'zero_or_one_queries': 'impossible by actual-action defect rank', + 'two_queries': 'each rank >= 2; cost >= 2*x', + 'three_queries': 'not all rank one; cost >= 2+x >= 2*x', + 'four_or_more_queries': 'cost >= 4 >= 2*x', + 'attainment': 'the original separate rank-two queries'}, + 'no_new_kappa': True, + 'limits': ['finite controls do not prove the all-parameter theorem', + 'the uniform-prime bridge is a written proof', + 'no changed consumer or native execution is verified']} + print(json.dumps(result, sort_keys=True, indent=2)) + + +if __name__ == '__main__': + main() diff --git a/research/bit-joint-dirty-pair/inputs/GEOMETRY.json.gz b/research/bit-joint-dirty-pair/inputs/GEOMETRY.json.gz new file mode 100644 index 0000000000..e12a566658 Binary files /dev/null and b/research/bit-joint-dirty-pair/inputs/GEOMETRY.json.gz differ diff --git a/research/bit-joint-dirty-pair/inputs/PREDECESSOR-PINS.json b/research/bit-joint-dirty-pair/inputs/PREDECESSOR-PINS.json new file mode 100644 index 0000000000..c593121ce2 --- /dev/null +++ b/research/bit-joint-dirty-pair/inputs/PREDECESSOR-PINS.json @@ -0,0 +1,19 @@ +{ + "schema_version": 1, + "source_commit": "8eefab699338b93400ca72ab22c6cf64352f7e05", + "original_package_commit": "b628ba738802587a38e61affaa01fd188d0644f9", + "scientific_base": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "source_path": "research/bit-partial-demand-closure/inputs/partial-progress/boundary/inputs/", + "files": [ + { + "path": "inputs/WORD.json.gz", + "sha256": "c46ccd7d3eedabc6a7efbb1a91ec13f2928bad8ee0bac57c6e593a092d13d96c" + }, + { + "path": "inputs/GEOMETRY.json.gz", + "sha256": "a353999bceac4ac957f540adfd3e5f8768297138b27132eeb83332e2ea4b1022" + } + ], + "word_canonical_sha256": "3bca74a2a8427eb18e86566baa19de597f10d0bc40c30b7443febd499ee2189a", + "scope": "Two literal query records and their exact native projectors only; no full supplier replay." +} diff --git a/research/bit-joint-dirty-pair/inputs/WORD.json.gz b/research/bit-joint-dirty-pair/inputs/WORD.json.gz new file mode 100644 index 0000000000..aa9ec3c341 Binary files /dev/null and b/research/bit-joint-dirty-pair/inputs/WORD.json.gz differ diff --git a/research/bit-joint-dirty-pair/source_check.py b/research/bit-joint-dirty-pair/source_check.py new file mode 100644 index 0000000000..bf569a6bbb --- /dev/null +++ b/research/bit-joint-dirty-pair/source_check.py @@ -0,0 +1,329 @@ +#!/usr/bin/env python3 +"""Focused exact binding of the PR4068 common-cut query pair. + +Apache-2.0; substantial OpenAI Codex assistance. No producer imports. +Default execution writes deterministic JSON only to stdout. +""" +from fractions import Fraction as F +from functools import lru_cache +from hashlib import sha256 +from pathlib import Path +import gzip +import json + +ROOT = Path(__file__).resolve().parent +HEAD = '5a34918402ae2c0c683d8820ad832970e77f6382' +CANONICAL_WORD = '3bca74a2a8427eb18e86566baa19de597f10d0bc40c30b7443febd499ee2189a' +PINS = { + 'inputs/WORD.json.gz': 'c46ccd7d3eedabc6a7efbb1a91ec13f2928bad8ee0bac57c6e593a092d13d96c', + 'inputs/GEOMETRY.json.gz': 'a353999bceac4ac957f540adfd3e5f8768297138b27132eeb83332e2ea4b1022', + 'inputs/PREDECESSOR-PINS.json': '4d03736c497eae94c4e98d33ac10ecacba9e914f9d604787237ff71075dc4e94', +} +N, CUT, END = 660, 23339, 23426 +QUERY_RECORDS = {23405: [0, 413, 509, 390, 2, 0], + 23424: [0, 444, 509, 392, 2, 0]} + + +def require(ok, why): + if not ok: + raise ValueError(why) + + +def identity_rows(): + return [{i: 1} for i in range(N)]+[{}] + + +def add(a, b, coefficient): + out = a.copy() + for j, v in b.items(): + out[j] = out.get(j, 0)+coefficient*v + if not out[j]: + del out[j] + return out + + +def replay(records, values, frames, inverse=False): + values, frames = [x.copy() for x in values], frames[:] + opened = None + copies = 0 + ordered = list(reversed(records)) if inverse else records + for op, d, s, c, f, section in ordered: + if op == 0: + before, after = (c, s) if inverse else (s, c) + require(frames[d] == before, 'MOVE entrance frame') + frames[d] = after + elif op == 1: + require(d != s and d < N and 0 <= s <= N, 'ordinary ADD operands') + require(frames[d] == frames[s] == f, 'ADD common frame') + require(d != opened, 'COPY source immutability') + values[d] = add(values[d], values[s], -c if inverse else c) + elif op == (3 if inverse else 2): + require(s == N and opened is None and not values[N], 'COPY zero slot') + require(frames[d] == c and frames[N] is None, 'COPY frame') + opened, values[N], frames[N] = d, values[d].copy(), f + copies += 1 + else: + require(op == (2 if inverse else 3), 'known opcode') + require(s == N and opened == d and frames[d] == c and frames[N] == f, + 'ERASE matching source') + require(values[N] == values[d], 'ERASE equality') + opened, values[N], frames[N] = None, {}, None + require(opened is None, 'no live private copy at selected endpoint') + return values, frames, copies + + +def multiply(a, b): + return tuple(tuple(sum(x*y for x, y in zip(row, col)) for col in zip(*b)) + for row in a) + + +def subtract(a, b): + return tuple(tuple(x-y for x, y in zip(row, other)) for row, other in zip(a, b)) + + +def eye(n): + return tuple(tuple(F(i == j) for j in range(n)) for i in range(n)) + + +def matrix_rank(a): + a = [list(row) for row in a] + rank = 0 + for j in range(len(a[0])): + pivot = next((i for i in range(rank, len(a)) if a[i][j]), None) + if pivot is None: + continue + a[rank], a[pivot] = a[pivot], a[rank] + value = a[rank][j] + a[rank] = [x/value for x in a[rank]] + for i in range(rank+1, len(a)): + value = a[i][j] + a[i] = [x-value*y for x, y in zip(a[i], a[rank])] + rank += 1 + if rank == len(a): + break + return rank + + +def determinant(a): + a = [list(row) for row in a] + result = F(1) + for j in range(len(a)): + pivot = next((i for i in range(j, len(a)) if a[i][j]), None) + if pivot is None: + return F(0) + if pivot != j: + result = -result + a[j], a[pivot] = a[pivot], a[j] + value = a[j][j] + result *= value + a[j] = [x/value for x in a[j]] + for i in range(j+1, len(a)): + value = a[i][j] + a[i] = [x-value*y for x, y in zip(a[i], a[j])] + return result + + +def projector(raw, f): + basis = [] + for label in raw['frames'][f]: + v = list(map(F, raw['lines'][label])) + for u in basis: + coefficient = sum(x*y for x, y in zip(v, u))/sum(x*x for x in u) + v = [x-coefficient*y for x, y in zip(v, u)] + if any(v): + basis.append(v) + if len(basis) == 8: + break + out = tuple(tuple(sum((u[i]*u[j]/sum(x*x for x in u) + for u in basis), F(0)) for j in range(8)) + for i in range(8)) + require(multiply(out, out) == out and tuple(zip(*out)) == out, + 'orthogonal frame projector') + return out + + +def swap(p): + q = subtract(eye(8), p) + return tuple(q[i]+p[i] for i in range(8))+tuple(p[i]+q[i] for i in range(8)) + + +def same_frame_pair(record): + return record[1] in (413, 444) or (record[0] == 1 and record[2] in (413, 444)) + + +def row_digest(rows): + canonical = [[[j, row[j]] for j in sorted(row)] for row in rows] + return sha256(json.dumps(canonical, separators=(',', ':')).encode()).hexdigest() + + +def rejected(call, expected_reason=None): + try: + call() + except ValueError as exc: + return expected_reason is None or str(exc) == expected_reason + return False + + +def check_source(): + sources = json.loads((ROOT/'INPUT-SOURCES.json').read_text()) + require(sources['predecessor_head'] == HEAD, 'predecessor head') + manifest_files = {entry['path']: entry for entry in sources['files']} + blobs = {} + for path, digest in PINS.items(): + blobs[path] = (ROOT/path).read_bytes() + require(sha256(blobs[path]).hexdigest() == digest, 'immutable source '+path) + entry = manifest_files[path] + require(entry['sha256'] == digest and entry['source_commit'] == HEAD, + 'manifest source binding '+path) + pins = json.loads(blobs['inputs/PREDECESSOR-PINS.json']) + word_bytes = gzip.decompress(blobs['inputs/WORD.json.gz']) + require(sha256(word_bytes).hexdigest() == CANONICAL_WORD == pins['word_canonical_sha256'], + 'canonical word binding') + word = json.loads(word_bytes) + raw = json.loads(gzip.decompress(blobs['inputs/GEOMETRY.json.gz'])) + require(len(word['start']) == len(word['final']) == N and raw['h'] == 8, + 'source dimensions') + records = word['records'] + for i, record in QUERY_RECORDS.items(): + require(records[i] == record, 'actual query record '+str(i)) + require(records[23325] == [1, 444, 17, 1, 509, 2] and + records[23333] == [1, 413, 17, 1, 509, 2], 'actual common source reads') + + start_frames = word['start']+[None] + rows, frames, copies = replay(records[:CUT], identity_rows(), start_frames) + require(copies == 0 and rows[N] == {} and frames[N] is None, + 'private slot inactive at cut') + restored, old_frames, back_copies = replay(records[:CUT], rows, frames, inverse=True) + require(restored == identity_rows() and old_frames == start_frames and back_copies == 0, + 'all 660 cut rows unrestricted by exact inverse prefix') + expected_rows = { + 17: {17: 1}, + 413: {413: 1, 469: -1, 605: -1, 87: 1, 17: 1, 22: 1, + 33: 1, 60: 1, 67: 1, 92: 1}, + 444: {444: 1, 369: -1, 77: 1, 17: 1, 22: 1, 33: 1, + 60: 1, 87: 1, 38: 1, 92: 1}, + } + require(all(rows[h] == v and frames[h] == 509 for h, v in expected_rows.items()), + 'full shared source payload rows') + dirty_pivot = [[rows[h].get(j, 0) for j in (413, 444)] for h in (413, 444)] + require(dirty_pivot == [[1, 0], [0, 1]], 'independent dirty pivot') + require(all(word['start'][h] == 0 and word['final'][h] == 1 for h in (413, 444)), + 'selected helpers ZERO to FULL') + require(not any(same_frame_pair(r) for r in records[CUT:23405]), 'common quiet window') + require(not any(r[1] == 444 or (r[0] == 1 and r[2] == 444) for r in records[CUT:23424]), + 'second target has no earlier touch') + require(not any(r[0] in (0, 1) and r[1] == 17 for r in records[CUT:24523]), + 'source17 unchanged through window') + + old_local = records[CUT:END] + new_local = [records[23405], records[23424]]+[ + r for i, r in enumerate(old_local, CUT) if i not in QUERY_RECORDS] + old_end, old_end_frames, _ = replay(old_local, rows, frames) + new_end, new_end_frames, _ = replay(new_local, rows, frames) + require(old_end == new_end and old_end_frames == new_end_frames, + 'retiming preserves every relevant column and frame') + back, back_frames, _ = replay(new_local, new_end, new_end_frames, inverse=True) + require(back == rows and back_frames == frames, 'retimed local literal inverse') + + @lru_cache(None) + def p(f): + return projector(raw, f) + common = p(509) + P, Q = subtract(p(390), common), subtract(p(392), common) + zero8 = tuple((F(0),)*8 for _ in range(8)) + for delta in (P, Q): + require(multiply(delta, delta) == delta and tuple(zip(*delta)) == delta, + 'orthogonal query increment') + require(matrix_rank(delta) == 2 and multiply(delta, common) == zero8, + 'rank2 and nested query increment') + require(all(x.denominator & (x.denominator-1) == 0 for row in delta for x in row), + 'dyadic increment') + comm = subtract(multiply(P, Q), multiply(Q, P)) + require(comm[0][1] == F(1, 8), 'distinct noncommuting address labels') + require(sum(comm[i][j]*comm[j][i] for i in range(8) for j in range(8)) == -1, + 'no common characteristic-zero flag') + concat = tuple(P[i]+Q[i] for i in range(8)) + require(matrix_rank(concat) == 4, 'address span dimension4') + minor_rows, minor_cols = [0, 1, 2, 4], [0, 1, 8, 9] + minor = tuple(tuple(concat[i][j] for j in minor_cols) for i in minor_rows) + require(determinant(minor) == F(1, 256), 'dyadic address span minor') + S, T = swap(P), swap(Q) + require(multiply(S, S) == eye(16) and multiply(T, T) == eye(16), 'query involutions') + sdisp, tdisp = subtract(S, eye(16)), subtract(T, eye(16)) + require(matrix_rank(tuple(sdisp[i]+tdisp[i] for i in range(16))) == 4, + 'address displacement span dimension4') + require(subtract(multiply(S, T), multiply(T, S))[0][1] == F(1, 4), + 'address action noncommutation') + + first_copy_index = next(i for i in range(CUT, len(records)) if records[i][0] == 2) + first_copy = records[first_copy_index] + copy_frames = [None]*(N+1) + copy_frames[first_copy[1]] = first_copy[3] + dirty_zero_port = identity_rows() + dirty_zero_port[N] = {N: 1} + zero_port_rejected = rejected( + lambda: replay([first_copy], dirty_zero_port, copy_frames), 'COPY zero slot') + matching_erase = [3]+first_copy[1:] + clean_copy_rows, clean_copy_frames, clean_copy_count = replay( + [first_copy, matching_erase], identity_rows(), copy_frames) + clean_copy_accepted = (clean_copy_rows == identity_rows() and + clean_copy_frames == copy_frames and clean_copy_count == 1) + missing_query = [r for i, r in enumerate(old_local, CUT) if i != 23424] + controls = { + 'dirty_private_port_rejected_by_original_COPY': zero_port_rejected, + 'clean_private_COPY_ERASE_control_accepted': clean_copy_accepted, + 'Q_replaced_by_P_fails_noncommutation': + subtract(multiply(P, P), multiply(P, P))[0][1] != F(1, 8), + 'Q_replaced_by_P_collapses_concat_rank': matrix_rank(tuple(row+row for row in P)) == 2, + 'omitted_second_query_fails_frame_contract': rejected(lambda: replay(missing_query, rows, frames)), + } + bad_rows = [r.copy() for r in rows] + bad_rows[444].pop(444) + bad_pivot = [[F(bad_rows[h].get(j, 0)) for j in (413, 444)] for h in (413, 444)] + controls['discarding_independent_dirty_input_loses_rank'] = matrix_rank(bad_pivot) == 1 + require(all(controls.values()), 'all semantic defect controls detected') + + def strings(a): + return [[str(x) for x in row] for row in a] + return { + 'status': 'PASS_ACTUAL_JOINT_DIRTY_SOURCE_BINDING', + 'predecessor_head': HEAD, 'word_canonical_sha256': CANONICAL_WORD, + 'source_hashes': PINS, 'record_indexing': 'zero based original WORD', + 'entrance_cut': CUT, 'query_records': QUERY_RECORDS, + 'ordinary_independent_input_columns': N, + 'prefix_columns_sha256': row_digest(rows), + 'prefix_inverse_returns_all_660_columns': True, + 'selected_rows': expected_rows, 'independent_dirty_pivot': dirty_pivot, + 'selected_common_frame': 509, + 'private_port': {'index': N, 'value': 'zero', 'frame': None, + 'prior_COPY_count': copies, 'first_future_COPY_record': first_copy_index, + 'contract': 'inactive private zero, not a free active arbitrary-dirty role'}, + 'quiet_window_half_open': [CUT, 23405], + 'source17_unchanged_until_before': 24523, + 'retimed_window_half_open': [CUT, END], + 'retimed_all_columns_and_frames_equal': True, + 'retimed_local_inverse_checked': True, + 'retimed_end_columns_sha256': row_digest(new_end), + 'query_rank_profile': {'2': 2}, + 'projectors': {'common_frame': strings(common), 'P': strings(P), 'Q': strings(Q)}, + 'commutator_0_1': '1/8', 'address_swap_commutator_0_1': '1/4', + 'trace_commutator_squared': '-1', + 'geometric_concat_rank_over_Q': 4, + 'address_displacement_concat_rank_over_Q': 4, + 'geometric_minor': {'rows': minor_rows, 'columns': minor_cols, 'determinant': '1/256'}, + 'negative_controls': controls, + 'limits': ['prefix and local retiming only; no repeated full-word metric audit', + 'address geometry over Q is not a representation of payload F2[G]', + 'formal common-cut diagonal endpoint requires its own algebra theorem', + 'no changed-tail or source-compensation lower bound', + 'no native physical execution, recursive moment improvement or new kappa'], + 'no_new_kappa': True, + } + + +def main(): + print(json.dumps(check_source(), indent=2, sort_keys=True)) + + +if __name__ == '__main__': + main() diff --git a/research/bit-joint-dirty-pair/verify.py b/research/bit-joint-dirty-pair/verify.py new file mode 100644 index 0000000000..cb36494d2e --- /dev/null +++ b/research/bit-joint-dirty-pair/verify.py @@ -0,0 +1,65 @@ +#!/usr/bin/env python3 +"""Replay the source-bound finite evidence; the written proof is not kernel checked.""" +from hashlib import sha256 +from pathlib import Path +import json +import subprocess +import sys + +ROOT = Path(__file__).resolve().parent +BOOTSTRAP = """from hashlib import sha256 +from pathlib import Path +import sys +p = Path(sys.argv[1]).resolve() +b = p.read_bytes() +if sha256(b).hexdigest() != sys.argv[2]: + raise ValueError('executed checker hash ' + p.name) +exec(compile(b, str(p), 'exec'), {'__name__': '__main__', '__file__': str(p)}) +""" + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def canonical(value): + # String comparison preserves distinctions such as true versus 1. + return json.dumps(value, sort_keys=True, separators=(',', ':'), allow_nan=False) + + +def main(): + manifest_bytes = (ROOT/'MANIFEST.json').read_bytes() + manifest = json.loads(manifest_bytes) + expected_names = set(manifest['files']) + observed_names = {str(p.relative_to(ROOT)) for p in ROOT.rglob('*') if p.is_file()} + require(observed_names == expected_names | {'MANIFEST.json'}, 'complete package file inventory') + authenticated = {} + for name, digest in manifest['files'].items(): + path = ROOT/name + authenticated[name] = path.read_bytes() + require(not path.is_symlink() and sha256(authenticated[name]).hexdigest() == digest, + 'package hash '+name) + flags = ['-I', '-B'] + (['-O'] if sys.flags.optimize else []) + receipts = {} + for key, filename in (('source', 'source_check.py'), ('finite_controls', 'check.py')): + replay = subprocess.run([sys.executable, *flags, '-c', BOOTSTRAP, + str(ROOT/filename), manifest['files'][filename]], + check=True, capture_output=True, text=True, timeout=45) + require(not replay.stderr, 'unexpected checker stderr '+filename) + receipts[key] = json.loads(replay.stdout) + expected = json.loads(authenticated['RESULT.json']) + require(canonical(receipts) == canonical(expected), 'full semantic receipts') + require(receipts['source']['no_new_kappa'] is True and + receipts['finite_controls']['no_new_kappa'] is True, 'scope markers') + for name, original in authenticated.items(): + require((ROOT/name).read_bytes() == original, 'package changed during replay '+name) + require(observed_names == {str(p.relative_to(ROOT)) for p in ROOT.rglob('*') if p.is_file()}, + 'package inventory changed during replay') + require((ROOT/'MANIFEST.json').read_bytes() == manifest_bytes, 'manifest changed during replay') + print('PASS_JOINT_DIRTY_PAIR source_columns=660 sylvester_pairs=32768 ' + 'optimum=2Phi_m(2) uniform_unary_full_endpoint no_new_kappa') + + +if __name__ == '__main__': + main()