diff --git a/research/dyadic-block-compiler/.gitattributes b/research/dyadic-block-compiler/.gitattributes new file mode 100644 index 0000000000..fa1385d99a --- /dev/null +++ b/research/dyadic-block-compiler/.gitattributes @@ -0,0 +1 @@ +* -text diff --git a/research/dyadic-block-compiler/ATTRIBUTION.md b/research/dyadic-block-compiler/ATTRIBUTION.md new file mode 100644 index 0000000000..1e711f5821 --- /dev/null +++ b/research/dyadic-block-compiler/ATTRIBUTION.md @@ -0,0 +1,11 @@ +# Attribution and overlap + +The retained native source and scalar pricing are pinned to canonical main `2a13eb1827784206202db90e5dc8327cf8a250db`. The source is zxv's native/compiler lineage, retaining its earlier contributors and notices. The cleanup windows are already present in that source; they are not new data or a new provider here. Credit Jacob Alan Sussman's mixed-target compiler and Cinna Davis's padding, query-thinning, retiming and joint-boundary work in #4359, #4416, #4440, #4441, #4447 and #4470. + +The immediate predecessor is Dugongue's #4489, head `67d1ded63edc604b3d9e6506a4f5d3689bdc9f41`, which proves the rank-one shared bridge and records no κ improvement. This package adds an alphabet-preserving arbitrary-rank factorization algorithm, executable emitted programs, direct source-window binding and exact local allowance reductions. It does not copy #4489's graph or repeat its chart searches. Integer unimodular reduction and low-rank linear-map factorization are classical; no literature priority or absence-of-overlap claim is made. + +Discovery consulted the shared MathProof DAG and `Meta/TITensorRank20260902.lean` for transported rank-one decompositions, and `Abstraction/VPVNPFixedGateVisiblePricing20260826.lean` for `linear_response_top_sum`. These are source-only precedents for moving a linear response through a finite sum, not freshly audited Lean imports or new proof dependencies. No Smith-normal-form theorem from that tree is asserted. The canonical DAG and Lean files remain unchanged. + +Main, recent PRs and the newest visible handoffs were checked. API title/body search required authentication unavailable to this worker; public web searches did not establish complete coverage. Unknown coverage is not evidence of novelty. Neighboring tensor-error and uniform-rank compiler PRs #4480–#4488 concern different proof obligations; this package makes no competing bound claim. + +Prepared for Dugongue with substantial OpenAI assistance in mathematics, discovery, implementation and verification. New work is Apache-2.0; existing notices remain. No independent human review or proof-assistant acceptance is claimed. diff --git a/research/dyadic-block-compiler/CASES.json b/research/dyadic-block-compiler/CASES.json new file mode 100644 index 0000000000..c2944f760f --- /dev/null +++ b/research/dyadic-block-compiler/CASES.json @@ -0,0 +1,434 @@ +[ + { + "phase": "full_frame_cleanup", + "first_ordinal": 4727, + "last_ordinal": 4764, + "frame": 1, + "source_roles": [ + 225, + 227, + 229, + 232, + 233, + 234, + 235, + 238, + 239, + 240, + 241, + 242, + 243, + 245, + 246, + 250, + 253, + 254, + 256, + 257, + 258, + 259, + 261, + 262, + 266, + 269, + 270, + 276, + 288, + 292, + 296, + 302, + 303, + 326, + 328, + 332, + 335, + 386 + ], + "target_roles": [ + 553 + ], + "matrix": [ + [ + "1/4", + "-1/4", + "-1/4", + "1/4", + "-1/4", + "1/2", + "-1/2", + "-1/4", + "1/4", + "-1/4", + "-1/4", + "-1/4", + "-1/2", + "-1/4", + "-1/4", + "1/4", + "-1/4", + "-1/4", + "-1/4", + "-1/4", + "-1/4", + "-1/2", + "-1/4", + "-1/4", + "1/4", + "-1/4", + "-1/4", + "1", + "-1/2", + "-1/4", + "1/2", + "-1/2", + "1", + "-1", + "2", + "-1", + "2", + "-1" + ] + ], + "rank": 1, + "old": 418, + "coalesced": 418, + "new": 366, + "gain_over_coalesced": 52, + "source_indices": [ + 22007, + 22044 + ] + }, + { + "phase": "full_frame_cleanup", + "first_ordinal": 1615, + "last_ordinal": 1620, + "frame": 1, + "source_roles": [ + 16, + 104 + ], + "target_roles": [ + 43, + 417, + 419 + ], + "matrix": [ + [ + "-1", + "-1" + ], + [ + "1", + "1" + ], + [ + "-1/2", + "-1/2" + ] + ], + "rank": 1, + "old": 52, + "coalesced": 52, + "new": 46, + "gain_over_coalesced": 6, + "source_indices": [ + 18895, + 18900 + ] + }, + { + "phase": "full_frame_cleanup", + "first_ordinal": 2900, + "last_ordinal": 2905, + "frame": 1, + "source_roles": [ + 22, + 23 + ], + "target_roles": [ + 108, + 321, + 591 + ], + "matrix": [ + [ + "-1", + "-1" + ], + [ + "1", + "1" + ], + [ + "-1/2", + "-1/2" + ] + ], + "rank": 1, + "old": 52, + "coalesced": 52, + "new": 46, + "gain_over_coalesced": 6, + "source_indices": [ + 20180, + 20185 + ] + }, + { + "phase": "full_frame_cleanup", + "first_ordinal": 4251, + "last_ordinal": 4276, + "frame": 1, + "source_roles": [ + 225, + 240, + 241, + 242, + 243, + 245, + 246, + 250, + 253, + 254, + 528 + ], + "target_roles": [ + 227, + 229, + 231, + 232, + 233, + 235, + 237, + 259, + 261, + 262, + 263, + 264, + 269, + 486, + 530, + 553 + ], + "matrix": [ + [ + "-1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "-1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "-1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "-1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "-1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "-1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "-1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "1", + "-1/4", + "-1/4", + "-1/4", + "-1/2", + "-1/4", + "-1/4", + "1/4", + "-1/4", + "-1/4", + "-1/2" + ], + [ + "-1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ] + ], + "rank": 2, + "old": 244, + "coalesced": 244, + "new": 240, + "gain_over_coalesced": 4, + "source_indices": [ + 21531, + 21556 + ] + } +] diff --git a/research/dyadic-block-compiler/LICENSE b/research/dyadic-block-compiler/LICENSE new file mode 100644 index 0000000000..261eeb9e9f --- /dev/null +++ b/research/dyadic-block-compiler/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/dyadic-block-compiler/PROOF.md b/research/dyadic-block-compiler/PROOF.md new file mode 100644 index 0000000000..bd71ca56f7 --- /dev/null +++ b/research/dyadic-block-compiler/PROOF.md @@ -0,0 +1,51 @@ +# Dyadic factorization and a one-temporary compiler + +Let D = ℤ[1/2] ⊂ ℚ. All matrix ranks in this note are over ℚ. Vectors may lie in any vector space over a characteristic-zero field containing these dyadic scalars. The arguments are informal proofs, not Lean formalizations. + +## Theorem 1: legal rank factors always exist + +For every nonempty finite m × n matrix M over D, with rational rank r, the algorithm in `compiler.factor` returns M = U V, where U has shape m × r over D and V has shape r × n over ℤ. It terminates using integer column operations; it never divides a scalar coefficient by an odd integer. + +Proof. Choose a power of two s clearing every denominator and initialize A = s M and S = I_n. Maintain the invariant A S = s M, with A and S integral and S unimodular. + +Swapping columns p,j of A and rows p,j of S preserves A S. Replacing column j of A by column j − q column p corresponds to A ← A E, with E = I − q e_p e_jᵀ. Since j ≠ p, E⁻¹ = I + q e_p e_jᵀ. The inverse row operation S ← E⁻¹ S replaces row p by row p + q row j, exactly as in the code. Negating column p and row p likewise preserves the invariant. Every operation is integral and unimodular. + +At pivot row i, choose a nonzero remaining column p. For each other remaining column j, divide the integer A[i,j] by the nonzero pivot A[i,p], subtract the quotient multiple and, if the remainder is nonzero, swap it into the pivot position. Every such swap strictly decreases the absolute nonzero pivot. Hence the Euclidean loop terminates and clears row i in every later column. Earlier pivot rows have zeros in all remaining columns, so these operations preserve all earlier clearances. + +Process successive rows. At termination, the first r columns H have distinct increasing pivot rows and a triangular nonsingular pivot minor; all later columns are zero. Thus A = [H 0] has rank r. Because S is invertible, rank A = rank M. The invariant gives M = (H/s) S[0:r,:]. Set U = H/s and V = S[0:r,:]. U is dyadic and V is integral, establishing every claimed property. If M = 0, r = 0 and the empty factor product is zero. No coefficient-size or polynomial bit-complexity bound is claimed. ∎ + +Why the alphabet condition matters: choosing the first column of [[3,1],[6,2]] as a rational rank basis gives the right factor [1,1/3], which is not native-dyadic. The integer column algorithm instead gives [[1],[2]] · [3,1]. This is an application of classical unimodular column reduction, not a new normal-form theorem or a claim of a canonical Hermite form. + +## Theorem 2: r physical bridge episodes suffice + +Let X_1,…,X_n and Y_1,…,Y_m be disjoint persistent fields. Let the sources use one invertible linear chart B and the destinations one chart A. Suppose the actual exact physical operator Q = A B⁻¹ is supplied, with its correct independently verified implementation. Then M = U V yields the shear + +Y_j ← Y_j + Σ_i M[j,i] X_i + +using r sequential invocations of Q and one reusable owned temporary, with zero productive credit for that temporary. The compiler does not certify a user-declared query rank; a rank bill for a nonidentity query remains conditional on its actual physical implementation. In the four source applications below A = B, so Q is exactly the identity and has no recursive cost or monomial wrapper. + +Proof. For each k, clear the temporary, add Σ_i V[k,i] B X_i into it, apply Q, add U[j,k] times its value to each physical A Y_j, then clear it. Linearity makes the transformed temporary A Σ_i V[k,i] X_i. Summing the updates over k gives A(Y_j + Σ_i M[j,i] X_i). Sources are never written. Both clears are emitted; arbitrary dirty owned entry is removed, and the owned return is zero. Only one temporary is live because the episodes run sequentially. All coefficients remain dyadic by Theorem 1, so the native scalar alphabet is respected. For r = 0, emit the identity and allocate no temporary. ∎ + +Write a(q) for the retained source `primitive_allowance` of a nonzero dyadic ADD. The complete scalar allowance is 4r + Σ a(U[j,k]) + Σ a(V[k,i]): each of the two clears per episode has allowance 2. Scalar ADDs with zero coefficient are omitted. A physical query of verified Fourier rank d would add r whole rank-d jobs when d > 0, plus its actual monomial factors and nonrecursive work; none are silently free. The new owned field must not alias any persistent field or a live source C0. This is a local sufficient construction, not admission of an arbitrary declared native job. + +## Corollary: both inverse-transpose orientations + +The persistent block matrix is [[I,0],[M,I]]. Its inverse transpose has the same form after exchanging source and target groups and replacing M by −Mᵀ. Factor −Mᵀ = (−Vᵀ) Uᵀ and apply Theorem 2. The factors remain dyadic and have the same multiset of coefficient magnitudes. Because the retained ADD allowance depends on magnitude and denominator, the scalar allowance is identical in both orientations, including every clear. Owned erasure is proved afresh; it is not obtained by formally inverting a destructive clear. ∎ + +## Four authenticated native applications + +The live source is canonical main's `THREE-base-FULL-IDENTITY-NATIVE.json.gz`, pinned in SOURCES.json. CASES.json selects four disjoint windows by phase and persistent-scalar ordinal. The verifier finds those selectors in the actual forward and backward programs, checks that each whole window consists solely of common-frame ADDs, derives its coefficient matrix and disjoint source/target sets, and compares all source coefficients. There is no hidden warp, scale, climb, owned action or source permutation between selected instructions. + +| Phase | Scalar ordinals | Rank | Old allowance | New allowance | +|---|---:|---:|---:|---:| +| full_frame_cleanup | 4727–4764 | 1 | 418 | 366 | +| full_frame_cleanup | 1615–1620 | 1 | 52 | 46 | +| full_frame_cleanup | 2900–2905 | 1 | 52 | 46 | +| full_frame_cleanup | 4251–4276 | 2 | 244 | 240 | +| Total, each orientation | | | 766 | 698 | + +Each old allowance already equals the allowance after repeated-edge coalescing. Thus the certified 68-unit reduction is not merely cancellation or duplicate ADD consolidation. The rank-two window is included; this is not only the one-source/rank-one special case. + +The verifier executes every emitted instruction on independent formal persistent and dirty-owned input columns. It checks all 160 local columns across both orientations. All other persistent fields, including the original C0, are untouched because their roles never appear. Theorem 2 therefore permits substitution in any surrounding program with the same common chart and a fresh owned field. It adds at most one owned field, reused across all four windows, and adds no productive credit or recursive jobs. Caller allocation, finite normalization, full stock and analytic admission remain separate obligations. + +The local allowance decreases by 68 per orientation. No new κ, asymptotic exponent, global runtime speedup, full 632-column native replay, selected-frontier update or new mathematical priority claim follows. The universal dyadic construction, exact source binding and emitted local programs are the deliverable. diff --git a/research/dyadic-block-compiler/README.md b/research/dyadic-block-compiler/README.md new file mode 100644 index 0000000000..0d804139ef --- /dev/null +++ b/research/dyadic-block-compiler/README.md @@ -0,0 +1,28 @@ +# Source-bound dyadic block compiler: 68 fewer scalar-allowance units + +This package compiles four actual disjoint scalar windows from the retained native source using one reusable owned temporary. Their complete scalar allowance falls from **766 to 698 per orientation**, including initialization and erasure. The compiler also handles higher-rank dyadic blocks without introducing illegal odd denominators. **No new κ is claimed.** + +[PROOF.md](PROOF.md) proves dyadic rank factorization by integer column operations, the one-temporary block construction and its inverse-transpose version. [CASES.json](CASES.json) binds the four source windows, including one rank-two block. [RESULT.json](RESULT.json) contains the actual emitted programs. This extends the rank-one shared bridge in [#4489](https://github.com/CrocSwap/integer-mult-bounds/pull/4489); the integer reduction is classical, with no novelty claim. + +## Reproduce + +From the repository root, using Python 3.12 and only its standard library: + +```sh +python3.12 -B scripts/research_package.py --package research/dyadic-block-compiler --check-only +python3.12 -B scripts/research_package.py --package research/dyadic-block-compiler +``` + +A Git-free exported tree can run `python3.12 -I -O -B research/dyadic-block-compiler/verify.py`. No Windows path, PowerShell, C++ compiler, GPU, SciPy or NumPy is required. Windows execution was checked; Linux execution remains untested. + +The replay authenticates two source inputs, locates the actual forward/backward windows, derives both matrices, checks an independent rational rank, compares every emitted local input column and owned return, and invokes the pinned source's actual scalar-pricing function. It checks 200 deterministic additional dyadic matrices and rejects omitted clears, a false factor, an illegal third and a shifted source selector. Unchanged repeated-edge coalescing costs are checked before reporting a gain. + +For a new matrix, `python3.12 research/dyadic-block-compiler/compiler.py matrix.json` prints a plan. A nonzero `--query-rank` is an explicitly declared interface premise, not a native Fourier-rank certificate. The four source cases use the actual identity query and therefore require no such premise. Rank minimization alone need not minimize scalar cost; inspect the complete output allowance before substituting a plan. These emitted macros are not claimed to be the best scalar rewrites; alternative gauge rescaling may improve them further. + +## Open next questions + +The result is a constructive local macro with one additional owned field, no temporary productive credit and unchanged recursive jobs. It does not install a changed global supplier, prove the complete caller stock bound, or improve κ. Local allowances are upper bounds under the retained pricing convention, not measured runtime. + +A useful next step is to find a different-chart source block whose independently verified physical bridge and full entry/exit costs improve the complete invoice. Begin with its exact source window and arbitrary-input contract, then replay both orientations and charge every owned field, monomial route and outer obligation. CASES.json already supplies source-bound examples for testing the compiler; do not treat their finite nonrecursive saving as an exponent gain. + +See [ATTRIBUTION.md](ATTRIBUTION.md) and [TASK.json](TASK.json). Prepared for Dugongue with substantial OpenAI assistance; Apache-2.0. diff --git a/research/dyadic-block-compiler/RESULT.json b/research/dyadic-block-compiler/RESULT.json new file mode 100644 index 0000000000..61c11cf05c --- /dev/null +++ b/research/dyadic-block-compiler/RESULT.json @@ -0,0 +1,2344 @@ +{ + "status": "PASS_DYADIC_SOURCE_BLOCK_COMPILER", + "source_cases": [ + { + "phase": "full_frame_cleanup", + "ordinals": [ + 4727, + 4764 + ], + "forward_source_indices": [ + 22007, + 22044 + ], + "backward_source_indices": [ + 22007, + 22044 + ], + "shape": [ + 1, + 38 + ], + "rank": 1, + "old_scalar_allowance": 418, + "new_scalar_allowance": 366, + "saving": 52, + "compiled_forward": [ + [ + "clear", + [ + "T", + 0 + ] + ], + [ + "add", + [ + "T", + 0 + ], + [ + "X", + 0 + ], + 1, + 1 + ], + [ + "add", + [ + "T", + 0 + ], + [ + "X", + 1 + ], + -1, + 1 + ], + [ + "add", + [ + "T", + 0 + ], + [ + "X", + 2 + ], + -1, + 1 + ], + [ + "add", + [ + "T", + 0 + ], + [ + "X", + 3 + ], + 1, + 1 + ], + [ + "add", + [ + "T", + 0 + ], + [ + "X", + 4 + ], + -1, + 1 + ], + [ + "add", + [ + "T", + 0 + ], + [ + "X", + 5 + ], + 2, + 1 + ], + [ + "add", + [ + "T", + 0 + ], + [ + "X", + 6 + ], + -2, + 1 + ], + [ + "add", + [ + "T", + 0 + ], + [ + "X", + 7 + ], + -1, + 1 + ], + [ + "add", + [ + "T", + 0 + ], + [ + "X", + 8 + ], + 1, + 1 + ], + [ + "add", + [ + "T", + 0 + ], + [ + "X", + 9 + ], + -1, + 1 + ], + [ + "add", + [ + "T", + 0 + ], + [ + "X", + 10 + ], + -1, + 1 + ], + [ + "add", + [ + "T", + 0 + ], + [ + "X", + 11 + ], + -1, + 1 + ], + [ + "add", + [ + "T", + 0 + ], + [ + "X", + 12 + ], + -2, + 1 + ], + [ + "add", + [ + "T", + 0 + ], + [ + "X", + 13 + ], + -1, + 1 + ], + [ + "add", + [ + "T", + 0 + ], + [ + "X", + 14 + ], + -1, + 1 + ], + [ + "add", + [ + "T", + 0 + ], + [ + "X", + 15 + ], + 1, + 1 + ], + [ + "add", + [ + "T", + 0 + ], + [ + "X", + 16 + ], + -1, + 1 + ], + [ + "add", + [ + "T", + 0 + ], + [ + "X", + 17 + ], + -1, + 1 + ], + [ + "add", + [ + "T", + 0 + ], + [ + "X", + 18 + ], + -1, + 1 + ], + [ + "add", + [ + "T", + 0 + ], + [ + "X", + 19 + ], + -1, + 1 + ], + [ + "add", + [ + "T", + 0 + ], + [ + "X", + 20 + ], + -1, + 1 + ], + [ + "add", + [ + "T", + 0 + ], + [ + "X", + 21 + ], + -2, + 1 + ], + [ + "add", + [ + "T", + 0 + ], + [ + "X", + 22 + ], + -1, + 1 + ], + [ + "add", + [ + "T", + 0 + ], + [ + "X", + 23 + ], + -1, + 1 + ], + [ + "add", + [ + "T", + 0 + ], + [ + "X", + 24 + ], + 1, + 1 + ], + [ + "add", + [ + "T", + 0 + ], + [ + "X", + 25 + ], + -1, + 1 + ], + [ + "add", + [ + "T", + 0 + ], + [ + "X", + 26 + ], + -1, + 1 + ], + [ + "add", + [ + "T", + 0 + ], + [ + "X", + 27 + ], + 4, + 1 + ], + [ + "add", + [ + "T", + 0 + ], + [ + "X", + 28 + ], + -2, + 1 + ], + [ + "add", + [ + "T", + 0 + ], + [ + "X", + 29 + ], + -1, + 1 + ], + [ + "add", + [ + "T", + 0 + ], + [ + "X", + 30 + ], + 2, + 1 + ], + [ + "add", + [ + "T", + 0 + ], + [ + "X", + 31 + ], + -2, + 1 + ], + [ + "add", + [ + "T", + 0 + ], + [ + "X", + 32 + ], + 4, + 1 + ], + [ + "add", + [ + "T", + 0 + ], + [ + "X", + 33 + ], + -4, + 1 + ], + [ + "add", + [ + "T", + 0 + ], + [ + "X", + 34 + ], + 8, + 1 + ], + [ + "add", + [ + "T", + 0 + ], + [ + "X", + 35 + ], + -4, + 1 + ], + [ + "add", + [ + "T", + 0 + ], + [ + "X", + 36 + ], + 8, + 1 + ], + [ + "add", + [ + "T", + 0 + ], + [ + "X", + 37 + ], + -4, + 1 + ], + [ + "query", + [ + "T", + 0 + ], + 0 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "T", + 0 + ], + 1, + 4 + ], + [ + "clear", + [ + "T", + 0 + ] + ] + ], + "compiled_backward": [ + [ + "clear", + [ + "T", + 0 + ] + ], + [ + "add", + [ + "T", + 0 + ], + [ + "X", + 0 + ], + 1, + 4 + ], + [ + "query", + [ + "T", + 0 + ], + 0 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "T", + 0 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 1 + ], + [ + "T", + 0 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 2 + ], + [ + "T", + 0 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 3 + ], + [ + "T", + 0 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 4 + ], + [ + "T", + 0 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 5 + ], + [ + "T", + 0 + ], + -2, + 1 + ], + [ + "add", + [ + "Y", + 6 + ], + [ + "T", + 0 + ], + 2, + 1 + ], + [ + "add", + [ + "Y", + 7 + ], + [ + "T", + 0 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 8 + ], + [ + "T", + 0 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 9 + ], + [ + "T", + 0 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 10 + ], + [ + "T", + 0 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 11 + ], + [ + "T", + 0 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 12 + ], + [ + "T", + 0 + ], + 2, + 1 + ], + [ + "add", + [ + "Y", + 13 + ], + [ + "T", + 0 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 14 + ], + [ + "T", + 0 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 15 + ], + [ + "T", + 0 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 16 + ], + [ + "T", + 0 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 17 + ], + [ + "T", + 0 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 18 + ], + [ + "T", + 0 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 19 + ], + [ + "T", + 0 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 20 + ], + [ + "T", + 0 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 21 + ], + [ + "T", + 0 + ], + 2, + 1 + ], + [ + "add", + [ + "Y", + 22 + ], + [ + "T", + 0 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 23 + ], + [ + "T", + 0 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 24 + ], + [ + "T", + 0 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 25 + ], + [ + "T", + 0 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 26 + ], + [ + "T", + 0 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 27 + ], + [ + "T", + 0 + ], + -4, + 1 + ], + [ + "add", + [ + "Y", + 28 + ], + [ + "T", + 0 + ], + 2, + 1 + ], + [ + "add", + [ + "Y", + 29 + ], + [ + "T", + 0 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 30 + ], + [ + "T", + 0 + ], + -2, + 1 + ], + [ + "add", + [ + "Y", + 31 + ], + [ + "T", + 0 + ], + 2, + 1 + ], + [ + "add", + [ + "Y", + 32 + ], + [ + "T", + 0 + ], + -4, + 1 + ], + [ + "add", + [ + "Y", + 33 + ], + [ + "T", + 0 + ], + 4, + 1 + ], + [ + "add", + [ + "Y", + 34 + ], + [ + "T", + 0 + ], + -8, + 1 + ], + [ + "add", + [ + "Y", + 35 + ], + [ + "T", + 0 + ], + 4, + 1 + ], + [ + "add", + [ + "Y", + 36 + ], + [ + "T", + 0 + ], + -8, + 1 + ], + [ + "add", + [ + "Y", + 37 + ], + [ + "T", + 0 + ], + 4, + 1 + ], + [ + "clear", + [ + "T", + 0 + ] + ] + ] + }, + { + "phase": "full_frame_cleanup", + "ordinals": [ + 1615, + 1620 + ], + "forward_source_indices": [ + 18895, + 18900 + ], + "backward_source_indices": [ + 18895, + 18900 + ], + "shape": [ + 3, + 2 + ], + "rank": 1, + "old_scalar_allowance": 52, + "new_scalar_allowance": 46, + "saving": 6, + "compiled_forward": [ + [ + "clear", + [ + "T", + 0 + ] + ], + [ + "add", + [ + "T", + 0 + ], + [ + "X", + 0 + ], + -1, + 1 + ], + [ + "add", + [ + "T", + 0 + ], + [ + "X", + 1 + ], + -1, + 1 + ], + [ + "query", + [ + "T", + 0 + ], + 0 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "T", + 0 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 1 + ], + [ + "T", + 0 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 2 + ], + [ + "T", + 0 + ], + 1, + 2 + ], + [ + "clear", + [ + "T", + 0 + ] + ] + ], + "compiled_backward": [ + [ + "clear", + [ + "T", + 0 + ] + ], + [ + "add", + [ + "T", + 0 + ], + [ + "X", + 0 + ], + 1, + 1 + ], + [ + "add", + [ + "T", + 0 + ], + [ + "X", + 1 + ], + -1, + 1 + ], + [ + "add", + [ + "T", + 0 + ], + [ + "X", + 2 + ], + 1, + 2 + ], + [ + "query", + [ + "T", + 0 + ], + 0 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "T", + 0 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 1 + ], + [ + "T", + 0 + ], + 1, + 1 + ], + [ + "clear", + [ + "T", + 0 + ] + ] + ] + }, + { + "phase": "full_frame_cleanup", + "ordinals": [ + 2900, + 2905 + ], + "forward_source_indices": [ + 20180, + 20185 + ], + "backward_source_indices": [ + 20180, + 20185 + ], + "shape": [ + 3, + 2 + ], + "rank": 1, + "old_scalar_allowance": 52, + "new_scalar_allowance": 46, + "saving": 6, + "compiled_forward": [ + [ + "clear", + [ + "T", + 0 + ] + ], + [ + "add", + [ + "T", + 0 + ], + [ + "X", + 0 + ], + -1, + 1 + ], + [ + "add", + [ + "T", + 0 + ], + [ + "X", + 1 + ], + -1, + 1 + ], + [ + "query", + [ + "T", + 0 + ], + 0 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "T", + 0 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 1 + ], + [ + "T", + 0 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 2 + ], + [ + "T", + 0 + ], + 1, + 2 + ], + [ + "clear", + [ + "T", + 0 + ] + ] + ], + "compiled_backward": [ + [ + "clear", + [ + "T", + 0 + ] + ], + [ + "add", + [ + "T", + 0 + ], + [ + "X", + 0 + ], + 1, + 1 + ], + [ + "add", + [ + "T", + 0 + ], + [ + "X", + 1 + ], + -1, + 1 + ], + [ + "add", + [ + "T", + 0 + ], + [ + "X", + 2 + ], + 1, + 2 + ], + [ + "query", + [ + "T", + 0 + ], + 0 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "T", + 0 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 1 + ], + [ + "T", + 0 + ], + 1, + 1 + ], + [ + "clear", + [ + "T", + 0 + ] + ] + ] + }, + { + "phase": "full_frame_cleanup", + "ordinals": [ + 4251, + 4276 + ], + "forward_source_indices": [ + 21531, + 21556 + ], + "backward_source_indices": [ + 21531, + 21556 + ], + "shape": [ + 16, + 11 + ], + "rank": 2, + "old_scalar_allowance": 244, + "new_scalar_allowance": 240, + "saving": 4, + "compiled_forward": [ + [ + "clear", + [ + "T", + 0 + ] + ], + [ + "add", + [ + "T", + 0 + ], + [ + "X", + 0 + ], + -1, + 1 + ], + [ + "query", + [ + "T", + 0 + ], + 0 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "T", + 0 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 1 + ], + [ + "T", + 0 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 2 + ], + [ + "T", + 0 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 3 + ], + [ + "T", + 0 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 4 + ], + [ + "T", + 0 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 5 + ], + [ + "T", + 0 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 6 + ], + [ + "T", + 0 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 7 + ], + [ + "T", + 0 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 8 + ], + [ + "T", + 0 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 9 + ], + [ + "T", + 0 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 10 + ], + [ + "T", + 0 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 11 + ], + [ + "T", + 0 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 12 + ], + [ + "T", + 0 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 13 + ], + [ + "T", + 0 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 14 + ], + [ + "T", + 0 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 15 + ], + [ + "T", + 0 + ], + -1, + 1 + ], + [ + "clear", + [ + "T", + 0 + ] + ], + [ + "clear", + [ + "T", + 0 + ] + ], + [ + "add", + [ + "T", + 0 + ], + [ + "X", + 1 + ], + -1, + 1 + ], + [ + "add", + [ + "T", + 0 + ], + [ + "X", + 2 + ], + -1, + 1 + ], + [ + "add", + [ + "T", + 0 + ], + [ + "X", + 3 + ], + -1, + 1 + ], + [ + "add", + [ + "T", + 0 + ], + [ + "X", + 4 + ], + -2, + 1 + ], + [ + "add", + [ + "T", + 0 + ], + [ + "X", + 5 + ], + -1, + 1 + ], + [ + "add", + [ + "T", + 0 + ], + [ + "X", + 6 + ], + -1, + 1 + ], + [ + "add", + [ + "T", + 0 + ], + [ + "X", + 7 + ], + 1, + 1 + ], + [ + "add", + [ + "T", + 0 + ], + [ + "X", + 8 + ], + -1, + 1 + ], + [ + "add", + [ + "T", + 0 + ], + [ + "X", + 9 + ], + -1, + 1 + ], + [ + "add", + [ + "T", + 0 + ], + [ + "X", + 10 + ], + -2, + 1 + ], + [ + "query", + [ + "T", + 0 + ], + 0 + ], + [ + "add", + [ + "Y", + 13 + ], + [ + "T", + 0 + ], + 1, + 4 + ], + [ + "clear", + [ + "T", + 0 + ] + ] + ], + "compiled_backward": [ + [ + "clear", + [ + "T", + 0 + ] + ], + [ + "add", + [ + "T", + 0 + ], + [ + "X", + 0 + ], + 1, + 1 + ], + [ + "add", + [ + "T", + 0 + ], + [ + "X", + 1 + ], + 1, + 1 + ], + [ + "add", + [ + "T", + 0 + ], + [ + "X", + 2 + ], + -1, + 1 + ], + [ + "add", + [ + "T", + 0 + ], + [ + "X", + 3 + ], + -1, + 1 + ], + [ + "add", + [ + "T", + 0 + ], + [ + "X", + 4 + ], + -1, + 1 + ], + [ + "add", + [ + "T", + 0 + ], + [ + "X", + 5 + ], + 1, + 1 + ], + [ + "add", + [ + "T", + 0 + ], + [ + "X", + 6 + ], + 1, + 1 + ], + [ + "add", + [ + "T", + 0 + ], + [ + "X", + 7 + ], + -1, + 1 + ], + [ + "add", + [ + "T", + 0 + ], + [ + "X", + 8 + ], + -1, + 1 + ], + [ + "add", + [ + "T", + 0 + ], + [ + "X", + 9 + ], + 1, + 1 + ], + [ + "add", + [ + "T", + 0 + ], + [ + "X", + 10 + ], + 1, + 1 + ], + [ + "add", + [ + "T", + 0 + ], + [ + "X", + 11 + ], + 1, + 1 + ], + [ + "add", + [ + "T", + 0 + ], + [ + "X", + 12 + ], + -1, + 1 + ], + [ + "add", + [ + "T", + 0 + ], + [ + "X", + 13 + ], + -1, + 1 + ], + [ + "add", + [ + "T", + 0 + ], + [ + "X", + 14 + ], + 1, + 1 + ], + [ + "add", + [ + "T", + 0 + ], + [ + "X", + 15 + ], + -1, + 1 + ], + [ + "query", + [ + "T", + 0 + ], + 0 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "T", + 0 + ], + 1, + 1 + ], + [ + "clear", + [ + "T", + 0 + ] + ], + [ + "clear", + [ + "T", + 0 + ] + ], + [ + "add", + [ + "T", + 0 + ], + [ + "X", + 13 + ], + 1, + 4 + ], + [ + "query", + [ + "T", + 0 + ], + 0 + ], + [ + "add", + [ + "Y", + 1 + ], + [ + "T", + 0 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 2 + ], + [ + "T", + 0 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 3 + ], + [ + "T", + 0 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 4 + ], + [ + "T", + 0 + ], + 2, + 1 + ], + [ + "add", + [ + "Y", + 5 + ], + [ + "T", + 0 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 6 + ], + [ + "T", + 0 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 7 + ], + [ + "T", + 0 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 8 + ], + [ + "T", + 0 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 9 + ], + [ + "T", + 0 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 10 + ], + [ + "T", + 0 + ], + 2, + 1 + ], + [ + "clear", + [ + "T", + 0 + ] + ] + ] + } + ], + "local_columns_both_orientations": 160, + "random_factor_and_program_cases": 200, + "old_allowance_per_orientation": 766, + "new_allowance_per_orientation": 698, + "saving_per_orientation": 68, + "additional_owned_fields": 1, + "new_recursive_calls": 0, + "productive_temporary_credit": 0, + "new_kappa": false +} diff --git a/research/dyadic-block-compiler/SOURCES.json b/research/dyadic-block-compiler/SOURCES.json new file mode 100644 index 0000000000..1d06375c9e --- /dev/null +++ b/research/dyadic-block-compiler/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "2a13eb1827784206202db90e5dc8327cf8a250db", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ed33caef5c5827693e9572d252a66f99cbb73d40", + "sha256": "5732707cc1e460b090b53f2463162749ad860de878a18f7408938671d295a9d9" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "64bfc5af6709ed9811171e0a2108f05e1219cb65", + "sha256": "352a6184713b8843d96fd2c2071eb7aeaa655906b7c51d45ad444912666c8a96" + }, + { + "path": "research/kappa-rebuild/complex/full-identity-certificates/THREE-base-FULL-IDENTITY-NATIVE.json.gz", + "usage": "input", + "git_blob": "b46d44c6ee624968dd57be928b0c15d9d45f3b2c", + "sha256": "c54b0a3e129d28e6dbf74fa731fc3bb70fe3c6705f07256750fbecddcc842d39" + }, + { + "path": "research/kappa-rebuild/complex/rebuild_native.py", + "usage": "input", + "git_blob": "78a7b1b0e6e43a1347fb361f45c6e0eaff8dd27b", + "sha256": "f94c527cc02215de49350d477618188c4c0da48bc8fb05b4e37b24c482cad7d5" + } + ] +} diff --git a/research/dyadic-block-compiler/TASK.json b/research/dyadic-block-compiler/TASK.json new file mode 100644 index 0000000000..1e790f29ef --- /dev/null +++ b/research/dyadic-block-compiler/TASK.json @@ -0,0 +1,66 @@ +{ + "schema_version": 1, + "task_id": "complex-new-helper-inventory", + "priority_revision": 7, + "base_commit": "2a13eb1827784206202db90e5dc8327cf8a250db", + "original_card": { + "id": "complex-new-helper-inventory", + "question": "Can a new local cost interface change the deficit-to-recursive-cost ratio beyond current packing?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/complex-local-word-ceiling/README.md", + "research/heterogeneous-owner-assembly/README.md", + "certificates/selected-result.json", + "research/selected-k8-unrestricted-ends/README.md" + ], + "methods": [ + "Propose a changed helper inventory and derive an optimistic exact moment.", + "Design a small completed instance and independently verify its endpoint and rank bill." + ], + "acceptance_gate": "A new physically realizable contract outside the frozen catalogue whose per-call profile, screened with ceiling.ceiling(), beats the selected word's packing ceiling; a lower cap does not establish identical circuitry or order attainable optima, and is insufficient to pass the stronger-budget target under this model. 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", + "research/complex-local-word-ceiling/verify.py" + ], + "expected": "PASS_COMPLEX_LOCAL_WORD_CEILING", + "inspect": "Read the selected word's per-call local profile, its packing ceiling and the lever table; run levers.py for the ideal budget of the lever you target.", + "scope": "Positive control and planning budget only; this is not a new construction or full cold replay." + }, + "first_experiment": "Before any synthesis, write the candidate per-call local profile (and centre charge / unpaid coordinates if changed) and screen it with ceiling.ceiling(); reject it if even the ideal ceiling does not beat the selected word's by your stated margin.", + "bottleneck_link": "Packing of the selected word is capped at +0.87% (ceiling model); only a lower local excess spend or a changed coverage law raises the cap.", + "allowed_variations": [ + "Narrow to one changed boundary or helper type with explicit counts.", + "If the coverage law, template or guard changes, derive an applicable fully charged replacement bound instead of applying the incumbent ceiling outside its scope." + ], + "scope_change_triggers": [ + "Mixing only providers already inside the pinned catalogue.", + "Only changing helper terminal subspaces and monotone frames within the fixed scalar word, entrances and cleanup contract already covered by #1995/#2013.", + "Continuing a partial cost improvement while leaving the same unpriced consumer, restoration or central-readout obligation unresolved; refresh the family expansion decision first. Local product-retiming evidence has a narrow scope and is not a ban on changed graphs or contracts." + ], + "overlap_terms": [ + "helper inventory", + "heterogeneous-owner", + "mutable leaver" + ] + }, + "scope_status": "refined", + "actual_scope": "Prove dyadic rank factorization and a one-temporary shear compiler; check four actual source windows in both orientations with scalar allowance 766 to 698.", + "scope_change_reason": "Take the shared-bridge handoff from #4489 to an executable higher-rank dyadic compiler and authenticated native cleanup windows; report finite scalar savings, not a new kappa.", + "bottleneck_link": "Rational rank bases can introduce illegal odd denominators. Integer column operations preserve the native dyadic alphabet and make grouped bridge plans executable.", + "budget_minutes": 60, + "stop_rule": "Require exact source binding, native scalar legality, both local arbitrary-input maps and complete allowance improvement; do not expand to a global kappa claim without a changed complete profile and caller audit.", + "outcome": "partial", + "evidence": "PROOF.md, CASES.json, RESULT.json, compiler.py, verify.py", + "author": "Dugongue", + "ai_assistance": "Substantial OpenAI assistance; no independent human or Lean acceptance.", + "open_questions": [ + { + "question": "Can the higher-rank compiler lower the complete paid moment at a different-chart source block?", + "why_it_matters": "The certified local scalar saving does not change kappa.", + "first_step": "Bind an actual block, verify its exact physical query, charge every entry/exit transport and owned field, then reprice the whole supplier.", + "blocked_by": "No improved complete supplier or global stock admission is included." + } + ] +} diff --git a/research/dyadic-block-compiler/VALIDATION.md b/research/dyadic-block-compiler/VALIDATION.md new file mode 100644 index 0000000000..e1c53cb2f1 --- /dev/null +++ b/research/dyadic-block-compiler/VALIDATION.md @@ -0,0 +1,5 @@ +# Validation scope + +The direct isolated/optimized replay passes on Windows with Python 3.12. It reconstructs four actual source windows in both orientations, checks 160 local formal columns and 200 additional deterministic matrices, and verifies scalar allowance 766 to 698 using the authenticated retained pricing function. All emitted coefficients are dyadic; the rank-factor construction's right factor is integral before inverse-transpose transport. + +Registered replay, source pins, committed bytes, source metadata and Git-free export are checked for the release and recorded in its external release receipt. No Linux execution, complete native all-column replay, full stock theorem, new κ, formal proof or human acceptance is claimed. Source archives are exact immutable inputs; generated RESULT.json is compared semantically as JSON. diff --git a/research/dyadic-block-compiler/VERIFY.json b/research/dyadic-block-compiler/VERIFY.json new file mode 100644 index 0000000000..01163decdb --- /dev/null +++ b/research/dyadic-block-compiler/VERIFY.json @@ -0,0 +1,21 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/kappa-rebuild/complex/full-identity-certificates/THREE-base-FULL-IDENTITY-NATIVE.json.gz", + "research/kappa-rebuild/complex/rebuild_native.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Authenticated actual native source windows in both orientations, integer/dyadic factors, independent ranks, all 160 local input/owned columns, complete source pricing, 200 matrix controls and invalid alternatives." + } + ] +} diff --git a/research/dyadic-block-compiler/compiler.py b/research/dyadic-block-compiler/compiler.py new file mode 100644 index 0000000000..80f838cbd7 --- /dev/null +++ b/research/dyadic-block-compiler/compiler.py @@ -0,0 +1,102 @@ +"""Exact dyadic column-lattice factorization and one-temporary block compiler. +Apache-2.0; Dugongue with substantial OpenAI assistance. +""" +from fractions import Fraction as Q + +def need(ok, why): + if not ok: raise ValueError(why) + +def dyadic(value): + value=Q(value) + need(value.denominator & (value.denominator-1)==0, 'Native scalars must be dyadic') + return value + +def factor(matrix): + M=[[dyadic(x) for x in row] for row in matrix] + need(M and M[0] and all(len(row)==len(M[0]) for row in M),'Nonempty rectangular matrix') + m,n=len(M),len(M[0]);scale=max(x.denominator for row in M for x in row) + # Invariant: A * S = scale * M; inverse column moves update rows of S. + A=[[int(x*scale) for x in row] for row in M] + S=[[int(i==j) for j in range(n)] for i in range(n)] + pivots=[];p=0;operations=0 + def swap(a,b): + for row in A:row[a],row[b]=row[b],row[a] + S[a],S[b]=S[b],S[a] + for i in range(m): + j=next((j for j in range(p,n) if A[i][j]),None) + if j is None:continue + swap(p,j) + for j in range(p+1,n): + while A[i][j]: + q=A[i][j]//A[i][p] + for row in A:row[j]-=q*row[p] + # col_j -= q * col_p; inverse action is row_p += q * row_j. + S[p]=[a+q*b for a,b in zip(S[p],S[j])] + operations+=1 + if A[i][j]:swap(p,j) + if A[i][p]<0: + for row in A:row[p]=-row[p] + S[p]=[-x for x in S[p]] + pivots.append(i);p+=1 + if p==n:break + need(all(not any(row[p:]) for row in A),'Zero trailing columns') + U=[[Q(x,scale) for x in row[:p]] for row in A];V=[[Q(x) for x in row]for row in S[:p]] + need(all(sum((U[i][k]*V[k][j] for k in range(p)),Q(0))==M[i][j] for i in range(m) for j in range(n)),'Exact factorization') + return {'matrix':M,'left':U,'right':V,'rank':p,'pivot_rows':pivots,'euclidean_steps':operations} + +def add_cost(value): + q=dyadic(value);n,d=abs(q.numerator),q.denominator + if not n:return 0 + return 2*(3+n.bit_length()-1+n.bit_count()+d.bit_length()-1) + +def emit_factor(U, V, query_rank): + need(isinstance(query_rank,int) and query_rank>=0,'Nonnegative query rank') + r=len(V) + need(U and all(len(row)==r for row in U), 'Factor dimensions') + if r:need(V[0] and all(len(row)==len(V[0]) for row in V), 'Right factor dimensions') + U=[[dyadic(x) for x in row] for row in U];V=[[dyadic(x) for x in row] for row in V] + program=[] + for k in range(r): + program.append(['clear',['T',0]]) + for i,q in enumerate(V[k]): + if q:program.append(['add',['T',0],['X',i],q.numerator,q.denominator]) + # Kept even at rank zero: a rank-zero physical map can have monomial work. + program.append(['query',['T',0],query_rank]) + for j,row in enumerate(U): + q=row[k] + if q:program.append(['add',['Y',j],['T',0],q.numerator,q.denominator]) + program.append(['clear',['T',0]]) + cost=sum(2 if e[0]=='clear' else add_cost(Q(e[3],e[4])) if e[0]=='add' else 0 for e in program) + return {'program':program,'owned_peak':int(r>0),'productive_temporary_credit':0,'conditional_paid':{query_rank:r}if query_rank and r else {},'scalar_allowance':cost,'monomial_route_episodes':r,'declared_query_rank':query_rank} + + +def compile_block(matrix, query_rank=0): + """Rank bill is conditional on the caller's exact physical query contract. + Same-chart source cases below supply the identity query, whose rank is zero. + """ + f=factor(matrix) + return f|emit_factor(f['left'],f['right'],query_rank) + +def dual_factor(left,right): + """Factor -M^T as (-V^T) U^T, with identical coefficient allowances.""" + r=len(right) + need(r>0,'Use the identity directly for a zero block') + return [[-right[k][i] for k in range(r)] for i in range(len(right[0]))], [[left[j][k] for j in range(len(left))]for k in range(r)] + +def encode(value): + if isinstance(value,Q):return str(value) + if isinstance(value,dict):return {str(k):encode(v) for k,v in value.items()} + if isinstance(value,list):return [encode(v) for v in value] + return value + +def main(): + import argparse,json + from pathlib import Path + ap=argparse.ArgumentParser(description='Compile a dyadic matrix into a one-temporary shear. Query rank is a declared interface premise, not certified by this compiler.') + ap.add_argument('matrix',type=Path) + ap.add_argument('--query-rank',type=int,default=0) + args=ap.parse_args() + result=compile_block(json.loads(args.matrix.read_text(encoding='utf-8')),args.query_rank) + print(json.dumps(encode(result),indent=2)) + +if __name__=='__main__':main() diff --git a/research/dyadic-block-compiler/verify.py b/research/dyadic-block-compiler/verify.py new file mode 100644 index 0000000000..8850624363 --- /dev/null +++ b/research/dyadic-block-compiler/verify.py @@ -0,0 +1,175 @@ +"""Exact source-bound checks for the dyadic block compiler. Apache-2.0. +Dugongue with substantial OpenAI assistance; no new kappa claim. +""" +from pathlib import Path +from fractions import Fraction as Q +import ast,gzip,hashlib,json,random,sys,types +HERE=Path(__file__).resolve().parent +ROOT=HERE.parents[1] + +def need(ok,why): + if not ok:raise ValueError(why) + +def load_local(): + # Execute the authenticated bytes; do not trust a preexisting bytecode cache. + data=(HERE/'compiler.py').read_bytes() + mod=types.ModuleType('dyadic_block_authenticated');mod.__file__=str(HERE/'compiler.py') + sys.modules[mod.__name__]=mod;exec(compile(data,mod.__file__,'exec'),mod.__dict__) + return mod + +B=load_local() + +def read(name):return json.loads((HERE/name).read_text(encoding='utf-8')) + +def authenticated_sources(): + out={} + for row in read('SOURCES.json')['files']: + if row['usage']=='input': + data=(ROOT/row['path']).read_bytes() + need(hashlib.sha256(data).hexdigest()==row['sha256'],'Changed input: '+row['path']) + out[row['path']]=data + return out + +def independent_rank(matrix): + A=[[Q(x)for x in row]for row in matrix];m,n=len(A),len(A[0]);r=0 + for j in range(n): + i=next((i for i in range(r,m)if A[i][j]),None) + if i is None:continue + A[r],A[i]=A[i],A[r];q=A[r][j];A[r]=[x/q for x in A[r]] + for i in range(r+1,m): + q=A[i][j];A[i]=[x-q*y for x,y in zip(A[i],A[r])] + r+=1 + if r==m:break + return r + +def check_factor(M,U,V): + m,n=len(M),len(M[0]);r=len(V) + need(len(U)==m and all(len(row)==r for row in U),'Left dimensions') + need(all(len(row)==n for row in V),'Right dimensions') + need(r==independent_rank(M),'Independent rational rank') + for row in U+V: + for x in row:B.dyadic(x) + need(all(Q(M[i][j])==sum((U[i][k]*V[k][j]for k in range(r)),Q(0))for i in range(m)for j in range(n)),'Factor product') + +def transpose(M):return [list(row)for row in zip(*M)] + +def state(n,m): + size=n+m+1 + rows={('X',i):[Q(k==i)for k in range(size)]for i in range(n)} + rows.update({('Y',j):[Q(k==n+j)for k in range(size)]for j in range(m)}) + rows['T',0]=[Q(k==n+m)for k in range(size)] + return rows + +def execute(program,n,m): + rows=state(n,m);size=n+m+1 + for e in program: + if e[0]=='clear': + need(e[1]==['T',0],'Only owned temporary may be cleared') + rows['T',0]=[Q(0)]*size + elif e[0]=='query': + need(e[1]==['T',0] and e[2]==0,'Source cases use the exact identity query') + else: + need(e[0]=='add','Known opcode');a,b=tuple(e[1]),tuple(e[2]) + need(a!=b and a in rows and b in rows,'Distinct valid roles') + q=B.dyadic(Q(e[3],e[4]));need(q!=0,'Nonzero ADD') + rows[a]=[x+q*y for x,y in zip(rows[a],rows[b])] + return rows + +def check_semantics(M,program,owned): + M=[[Q(x)for x in row]for row in M];m,n=len(M),len(M[0]);actual=execute(program,n,m);original=state(n,m) + for i in range(n):need(actual['X',i]==original['X',i],'Source column changed') + for j in range(m): + wanted=[original['Y',j][k]+sum(M[j][i]*original['X',i][k]for i in range(n))for k in range(n+m+1)] + need(actual['Y',j]==wanted,'Destination or dirty-owned column mismatch') + need(actual['T',0]==([Q(0)]*(n+m+1) if owned else original['T',0]),'Owned output condition') + return n+m+1 + +def gate_map(program): + phase=None;counts={};out={} + for i,e in enumerate(program): + if e[0]=='phase':phase=e[1] + if e[0]=='scalar': + g=e[1];roles=g[1:3]if g[0]in('add','copy')else g[1:2] + if all(r[0]=='L'for r in roles): + j=counts.get(phase,0);out[phase,j]=i;counts[phase]=j+1 + return out + +def source_matrix(words,case,backward): + program=words['backward'if backward else 'forward'];mapping=gate_map(program) + a=mapping[case['phase'],case['first_ordinal']];b=mapping[case['phase'],case['last_ordinal']] + need(a<=b,'Ordered source window') + window=program[a:b+1] + need(len(window)==case['last_ordinal']-case['first_ordinal']+1,'Contiguous actual scalar source window') + for e in window: + need(e[0]=='scalar'and e[1][0]=='add'and e[2]==case['frame'],'Only common-chart ADDs, no hidden warp/climb/scale') + need(all(r[0]=='L'for r in e[1][1:3]),'Only persistent source fields') + sources=sorted({e[1][2][1]for e in window});targets=sorted({e[1][1][1]for e in window}) + need(not set(sources)&set(targets),'Bipartite source/destination disjointness') + need(all(0<=r<632 for r in sources+targets),'Original 632-field ABI') + need(sources==(case['target_roles']if backward else case['source_roles'])and targets==(case['source_roles']if backward else case['target_roles']),'Exact source roles') + M=[[Q(0)for _ in sources]for _ in targets] + for e in window: + g=e[1];M[targets.index(g[1][1])][sources.index(g[2][1])]+=Q(g[3],g[4]) + expected=[[Q(x)for x in row]for row in case['matrix']] + if backward:expected=[[-x for x in row]for row in transpose(expected)] + need(M==expected,'Authenticated source coefficients') + return M,window,[a,b] + +def source_pricer(data): + tree=ast.parse(data.decode('utf-8')) + node=next(x for x in tree.body if isinstance(x,ast.FunctionDef)and x.name=='primitive_allowance') + module=ast.Module(body=[node],type_ignores=[]);namespace={'Q':Q,'need':need} + exec(compile(module,'authenticated primitive_allowance','exec'),namespace) + return namespace['primitive_allowance'] + +def plan_price(program,price): + total=0 + for e in program: + if e[0]=='query':need(e[2]==0,'No paid source query');continue + total+=price(e) + return total + +def rejects(action,label): + try:action() + except (ValueError,KeyError,IndexError,StopIteration):return + raise ValueError('Invalid control accepted: '+label) + +def verify(): + inputs=authenticated_sources() + src=next(v for k,v in inputs.items()if k.endswith('-NATIVE.json.gz'));words=json.loads(gzip.decompress(src)) + price=source_pricer(next(v for k,v in inputs.items()if k.endswith('/rebuild_native.py'))) + results=[];columns=0;intervals=[] + for case in read('CASES.json'): + M,window,indices=source_matrix(words,case,False);f=B.compile_block(M,0);check_factor(M,f['left'],f['right']) + need(all(x.denominator==1 for row in f['right']for x in row),'Integral right factor') + need(f['rank']==case['rank'] and f['owned_peak']==1 and not f['conditional_paid'],'Complete local interface') + forward=plan_price(f['program'],price);old=sum(price(e[1])for e in window);coalesced=sum(price(['add',['Y',i],['X',j],x.numerator,x.denominator])for i,row in enumerate(M)for j,x in enumerate(row)if x) + need(old==coalesced==case['old'] and forward==case['new']