From 10b01f96f3b99afe587124425627d67cbdb0da4b Mon Sep 17 00:00:00 2001 From: Dugongue <49054532+Dugongue@users.noreply.github.com> Date: Wed, 21 Oct 2026 19:23:05 -0700 Subject: [PATCH] Restore borrowed persistent fields in rank-one adapters: 666 allowance --- research/borrowed-rankone/.gitattributes | 1 + research/borrowed-rankone/ATTRIBUTION.md | 13 + research/borrowed-rankone/CASES.json | 434 + research/borrowed-rankone/GAUGE-PROOF.md | 51 + research/borrowed-rankone/LICENSE | 201 + research/borrowed-rankone/PROOF.md | 59 + research/borrowed-rankone/README.md | 29 + research/borrowed-rankone/RESULT.json | 10473 +++++++++++++++++++++ research/borrowed-rankone/SOURCES.json | 30 + research/borrowed-rankone/TASK.json | 66 + research/borrowed-rankone/VALIDATION.md | 7 + research/borrowed-rankone/VERIFY.json | 21 + research/borrowed-rankone/compiler.py | 130 + research/borrowed-rankone/verify.py | 193 + 14 files changed, 11708 insertions(+) create mode 100644 research/borrowed-rankone/.gitattributes create mode 100644 research/borrowed-rankone/ATTRIBUTION.md create mode 100644 research/borrowed-rankone/CASES.json create mode 100644 research/borrowed-rankone/GAUGE-PROOF.md create mode 100644 research/borrowed-rankone/LICENSE create mode 100644 research/borrowed-rankone/PROOF.md create mode 100644 research/borrowed-rankone/README.md create mode 100644 research/borrowed-rankone/RESULT.json create mode 100644 research/borrowed-rankone/SOURCES.json create mode 100644 research/borrowed-rankone/TASK.json create mode 100644 research/borrowed-rankone/VALIDATION.md create mode 100644 research/borrowed-rankone/VERIFY.json create mode 100644 research/borrowed-rankone/compiler.py create mode 100644 research/borrowed-rankone/verify.py diff --git a/research/borrowed-rankone/.gitattributes b/research/borrowed-rankone/.gitattributes new file mode 100644 index 0000000000..fa1385d99a --- /dev/null +++ b/research/borrowed-rankone/.gitattributes @@ -0,0 +1 @@ +* -text diff --git a/research/borrowed-rankone/ATTRIBUTION.md b/research/borrowed-rankone/ATTRIBUTION.md new file mode 100644 index 0000000000..a49425051b --- /dev/null +++ b/research/borrowed-rankone/ATTRIBUTION.md @@ -0,0 +1,13 @@ +# Predecessors and overlap + +Immediate predecessor [#4499](https://github.com/CrocSwap/integer-mult-bounds/pull/4499), Dugongue, head fd18b37415986d818f643d74a69a2148374bead4, supplies the exact power-of-two gauge code, gauge proof, four selectors, 686 / 674 comparisons, source authentication and symbolic executor adapted here. [#4494](https://github.com/CrocSwap/integer-mult-bounds/pull/4494), head ad31d9fdf000d4ca98dd911afe489a45d2ea4f74, supplies the arbitrary-rank dyadic compiler and 698 comparison; [#4489](https://github.com/CrocSwap/integer-mult-bounds/pull/4489), head 67d1ded63edc604b3d9e6506a4f5d3689bdc9f41, supplies the owned rank-one shared sum. Their notices and Apache-2.0 license are retained. The new specialization is borrowed source/target conjugation, a sufficient cost-saving theorem, and the 666 zero-extra-field source-bound replacement. Reversible uncomputation and transvection conjugation are classical; no literature priority claim is made. + +The native cleanup windows and scalar pricing come from zxv's retained compiler lineage at canonical main 2a13eb1827784206202db90e5dc8327cf8a250db. Preserve the full source contributors and notices. 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. This package does not replace those contributions or reprice their recursive calls. + +Current main AGENTS.md, autoresearch.md, CONTRIBUTING.md, priority revision 7, selected record and family expansion guidance were read. This session follows #4499's compiler continuation as a scoped local resource improvement, not a complete family expansion or κ-oriented scalar search. Public PR title/body pagination covered 352 open PRs at 2026-10-22T02:19:37Z. Terms borrowed / rank-one / dirty / conjugation yielded broad neighbors, including #3906 (Q8 dirty spectator audit), #1931 (E8 source reflection) and #4017 (finite Gaussian-lattice dirty scratch implementation). Those address different operators and implementation obligations; their dirty-state work is relevant precedent, not duplicated as a new general concept here. No full diff audit of those neighbors is claimed. Discussion API retrieval was rate-limited; visible handoff browsing and local note coverage were incomplete. The cached local search covered only 4 notes out of a 5,731-path HEAD inventory. Unknown coverage is not novelty evidence. + +MathProof source discovery inspected WeightedTIStabilizerShears20260906.lean for explicit transvections and invertible transport, and Problem18P34Subfield20261003NRecursiveWorkspaceRestore.lean for exact counted restoration of arbitrary saved memory and protected names. IntegerKappaBorrowFactors20261014.lean and IntegerKappaBorrowFeedback20261014.lean concern Gaussian factor order and numerical feedback, respectively; they do not prove the adapter here. The inherited rank-one/finite-sum precedents Meta/TITensorRank20260902.lean and Abstraction/VPVNPFixedGateVisiblePricing20260826.lean remain credited. These are source-level discovery references, not freshly audited Lean dependencies; no full-DAG search or new kernel check is claimed. The authoritative DAG and compiled modules remain unchanged. + +A bounded alternative was tried first: exact gauges inside the predecessor's fixed rank factors gave 366, 46, 46, 240, with no improvement. This was a fixed-factor observation, not a general barrier. The constructive route then changed to borrowed persistent fields. Prepared for Dugongue with substantial OpenAI assistance in mathematics, implementation and verification; no independent human review or Lean formalization is claimed. + +Submission checkpoint: canonical main was fetched again and remained at the pinned base. The public #4499 head was rechecked as fd18b37415986d818f643d74a69a2148374bead4. GitHub write authentication still returns HTTP 401 here; no device login, public Discussion post, push or PR creation was attempted by this worker. diff --git a/research/borrowed-rankone/CASES.json b/research/borrowed-rankone/CASES.json new file mode 100644 index 0000000000..c2944f760f --- /dev/null +++ b/research/borrowed-rankone/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/borrowed-rankone/GAUGE-PROOF.md b/research/borrowed-rankone/GAUGE-PROOF.md new file mode 100644 index 0000000000..46105d251c --- /dev/null +++ b/research/borrowed-rankone/GAUGE-PROOF.md @@ -0,0 +1,51 @@ +> Retained predecessor proof from #4499. Its 686 / 674 totals and 320-column validation describe that predecessor; the current package receipt is RESULT.json, with 666 and 160 source-column checks. The general gauge construction below is retained as the fallback proof. + +# Exact sufficient construction and optimality certificate + +All statements concern exact dyadic linear arithmetic with the retained native primitive_allowance, not floating-point evaluation. Sources X_i and destinations Y_j are disjoint persistent fields in one common frame. Other fields may contain arbitrary dirty values. + +## Lemma 1: the dyadic ADD allowance is an absolute valuation cost + +Write a nonzero dyadic q uniquely as o · 2^v, where o is a signed odd integer and v is an integer. Substitution into the native price gives + +A(q) = 2(2 + bit_length(|o|) + popcount(|o|)) + 2|v|. + +Proof. For v ≥ 0 the denominator is 1, the numerator bit length increases by v, and popcount is unchanged by the left shift. For v < 0 the odd numerator is unchanged and the denominator bit length minus 1 is −v. These are precisely the two branches of the formula. A positive SCALE by 2^e costs 2|e|, so its scale/unscale pair costs 4|e|. ∎ + +## Theorem 2: arbitrary integer gauges give an exact zero-scratch replacement + +For any dyadic matrix M and integer source/target exponents a_i,b_j, scale X_i by 2^a_i and Y_j by 2^b_j. For each nonzero matrix entry execute ADD from X_i to Y_j with coefficient M_ji · 2^(b_j−a_i). Unscale all fields. This maps + +X ↦ X, Y ↦ Y + MX + +for arbitrary initial X,Y, preserves every exterior field, and needs no owned scratch or recursive calls. Its scalar allowance equals C + F(a,b), where + +C = Σ_nonzero 2(2 + bit_length(|odd(M_ji)|) + popcount(|odd(M_ji)|)), + +F(a,b) = 4 Σ_i |a_i| + 4 Σ_j |b_j| + 2 Σ_nonzero |v_ji + b_j − a_i|. + +Proof. At the ADD stage each source is 2^a_i X_i and each target begins as 2^b_j Y_j. The adjusted coefficient contributes 2^b_j M_ji X_i, so unscaling yields exactly the stated persistent map. Sources are never ADD destinations. Lemma 1 charges all adjusted ADDs and both SCALE instructions for every nonzero exponent. No positivity or clean-entry assumption on the data is used. ∎ + +## Theorem 3: an exact signed circulation certifies a globally optimal gauge + +Use an anchor node 0, source nodes and target nodes. Put an oriented edge 0 → each field with capacity c=4 and cost k=0. For each nonzero M_ji put an edge source i → target j with c=2 and k=−v_ji. A signed flow f obeys −c ≤ f ≤ c and zero divergence. Set p_0=0, p_X=a and p_Y=b. + +For any such flow and any potential p, conservation implies + +−Σ_e k_e f_e = Σ_e f_e(p_v−p_u−k_e) ≤ Σ_e c_e |p_v−p_u−k_e| = F(a,b). + +Thus a feasible flow attaining equality proves optimality over all integer gauges (indeed over real potentials). The verifier reconstructs these edges directly from M and checks capacities, divergence and equality using integers. It does not trust the optimizer's reported objective. + +Existence and termination of the included algorithm: start at f=0. For an edge f, forward residual capacity is c−f with cost k and reverse capacity is c+f with cost −k. Augment an integral bottleneck around a negative residual cycle. Each augmentation decreases integral total cost by at least 1; total cost is bounded below by −Σ c|k|, so this process terminates. Bellman–Ford with a zero-distance super-source either finds a negative cycle or returns integer shortest distances p. At termination, a forward residual edge implies p_v−p_u−k ≤ 0; a reverse residual edge implies the opposite inequality. Therefore each unsaturated edge has zero reduced potential, while a saturated edge has the sign that makes f_e(p_v−p_u−k)=c_e|p_v−p_u−k|. Summing gives equality. Normalize the anchor by subtracting its distance. All distances are integers, so Theorem 2 emits legal native powers of two. ∎ + +The algorithm is finite and exact; no strongly polynomial complexity claim is made. Disconnected nonzero patterns are harmless because each field has an anchor edge. Zero matrix entries are omitted, including in C and the flow graph. + +## Corollary 4: dual orientation and inherited rank-one alternative + +For the inverse-transpose block −Mᵀ, source gauges −b and target gauges −a preserve every absolute valuation term, and C is unchanged. Thus optimal gauge allowances agree in both orientations. The executable independently compiles and checks both authenticated source orientations. + +If M=u vᵀ with dyadic u,v, the predecessor's owned-field construction clears T, accumulates Σ_i v_i X_i into T, adds u_j T to each Y_j, and clears T again. This has the same persistent map and a zero owned-field exit for arbitrary dirty entry, at allowance 4 + Σ_i A(v_i) + Σ_j A(u_j). Zero coefficients are skipped. The included implementation only accepts an exact rank-one factor with legal dyadic coefficients. It selects this alternative only if cheaper, and reuses one field between disjoint windows. This is #4489/#4494's mechanism, not a second newly invented construction here. ∎ + +## Source specialization and limits + +The four windows are authenticated by source hashes, phase, common frame, actual native program indices, persistent ordinals and exact role sets. Each window contains only contiguous scalar ADDs with disjoint sources and destinations, so Theorem 2 applies without moving a recursive operation. The finite symbolic executor verifies every independent local data column, including arbitrary dirty owned entry, in both modes and orientations: 320 column checks in total. Scalar prices are evaluated with the actual pinned source function. This proves the local 686 and 674 bills and exact interface replacements. It does not prove a full rewritten multiplication program's coefficient/norm/stock invariants or a new κ. diff --git a/research/borrowed-rankone/LICENSE b/research/borrowed-rankone/LICENSE new file mode 100644 index 0000000000..261eeb9e9f --- /dev/null +++ b/research/borrowed-rankone/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/borrowed-rankone/PROOF.md b/research/borrowed-rankone/PROOF.md new file mode 100644 index 0000000000..3c6f545c77 --- /dev/null +++ b/research/borrowed-rankone/PROOF.md @@ -0,0 +1,59 @@ +# Borrowed rank-one adapters and exact cost guarantees + +Work over dyadic rationals with the retained native ADD allowance A(q), omitting zero coefficients. All source roles X_i and destination roles Y_j are distinct, disjoint, and expressed in the same chart. Other fields can contain arbitrary dirty data. No scalar operation is moved across a query or chart change. + +## Theorem 1: source-pivot conjugation + +Suppose M=u vᵀ and a coefficient pivot v_p is nonzero, with each ratio c_i=v_i/v_p dyadic. Set d_j=u_j v_p. Then the following native program implements X ↦ X, Y ↦ Y+MX: + +1. For i ≠ p with c_i ≠ 0, execute X_p ← X_p + c_i X_i. +2. For each nonzero d_j, execute Y_j ← Y_j + d_j X_p. +3. Reverse the first sequence with the negated coefficients. + +Proof. After preparation, X_p equals (Σ_i v_i X_i)/v_p; every other source remains unchanged. Thus the middle sequence adds u_j Σ_i v_i X_i to Y_j. Its reads do not alter any source. Reversing preparation recovers the original X_p exactly, because the other source fields are unchanged. No temporary is allocated or cleared; no value of X_p is assumed clean, nonzero or known. Division occurs only in fixed coefficient preparation, never on runtime data. Exterior fields are untouched. ∎ + +The complete scalar allowance is + +B_source = 2 Σ_(i≠p) A(v_i/v_p) + Σ_j A(u_j v_p). + +Both preparation and its inverse are included, since A(−q)=A(q). + +## Theorem 2: dirty-target conjugation + +Suppose M=u vᵀ, u_p ≠ 0 and every c_j=u_j/u_p is dyadic. Set d_i=u_p v_i. For each j ≠ p subtract c_j Y_p from Y_j; next add Σ_i d_i X_i to Y_p using scalar ADDs; finally add c_j Y_p back to each other destination. + +This program also implements X ↦ X, Y ↦ Y+MX with no extra field. Its allowance is + +B_target = 2 Σ_(j≠p) A(u_j/u_p) + Σ_i A(u_p v_i). + +Proof. Write s=Σ_i d_i X_i and let y denote the initial destination values. During the middle stage Y_p changes from y_p to y_p+s. Each other output becomes y_j−c_j y_p+c_j(y_p+s)=y_j+c_j s. The pivot output is y_p+s. These are precisely Y+MX, and no source is modified. In particular the subtraction cancels the arbitrary dirty initial y_p; omitting it would introduce unwanted cross-output terms. ∎ + +Source borrowing for M and target borrowing for −Mᵀ are the transpose-dual constructions. Their scalar allowances agree because transposition exchanges the two coefficient lists and sign does not change A. The verifier nevertheless derives and checks both actual native source orientations independently. + +## Corollary 3: a strict sufficient saving over an owned sum + +Normalize a source factor so v_p=1, with dyadic u,v. The owned-field program of #4489/#4494/#4499 clears T, accumulates Σ_i v_i X_i, reads u_j T into every output, and clears T again. It costs + +O = 4 + A(1) + Σ_(i≠p) A(v_i) + Σ_j A(u_j). + +Since A(1)=8, Theorem 1 gives O−B_source = 12−Σ_(i≠p) A(v_i). Therefore Σ_(i≠p) A(v_i) < 12 is a sufficient strict-saving condition; equality gives a tie. This is a quantitative sufficient result, not merely a necessary-condition test. + +For v=(1,1), u=(−1,1,−1/2), the owned bill is 4+8+8+8+8+10=46. The borrowed bill is 8+8+8+8+10=42. The original six-entry direct block costs 52. The emitted forward program is + +```text +X0 += X1 +Y0 -= X0 +Y1 += X0 +Y2 -= X0/2 +X0 -= X1 +``` + +Every input is restored. Both pinned repeated-input blocks have exactly this matrix. Their dual matrices use Theorem 2 at cost 42. ∎ + +## Compiler correctness and scope + +The implementation computes normalized coefficients from a proposed nonzero matrix entry, rejects any odd denominator, checks every entry of M equals the proposed outer product, and emits only proven legal pivots. It enumerates all source and target pivots admitted by these rules. If none is cheaper, it uses #4499's exact zero-scratch gauge program, whose retained proof is GAUGE-PROOF.md. This fallback is sufficient for every dyadic matrix, including zero maps. No claim that every dyadic rank-one matrix has a legal normalized source or target pivot is needed: for example, [[9,15],[15,25]] has neither. + +Selection between valid candidates preserves the exact persistent map. The four actual source windows are disjoint and contain contiguous common-frame scalar ADDs, so replacing them preserves the local interfaces and original 632-field ABI. The verifier authenticates source bytes and selectors, prices every emitted instruction with the source primitive_allowance, checks all independent local data columns, and requires every selected instruction to name only original X/Y fields. The combined scalar allowance is 358+42+42+224=666 in each orientation. + +This proves local exact replacements and their scalar bills. Finite program checks are not a full multiplication theorem: rebuilt stock/norm/coefficient, numerical precision and complete global-bound obligations remain. No new recursive calls, productive-helper credit, full supplier or new κ is established. diff --git a/research/borrowed-rankone/README.md b/research/borrowed-rankone/README.md new file mode 100644 index 0000000000..673fac5a83 --- /dev/null +++ b/research/borrowed-rankone/README.md @@ -0,0 +1,29 @@ +# Borrowed rank-one adapters: 666 allowance, no extra fields + +This package improves the same four native cleanup blocks as [#4494](https://github.com/CrocSwap/integer-mult-bounds/pull/4494) and [#4499](https://github.com/CrocSwap/integer-mult-bounds/pull/4499). The total scalar allowance per orientation is **666 with zero additional owned fields**, versus 686 for #4499's zero-scratch option or 674 for its one-field hybrid. Both actual source orientations are checked. This is a local exact-arithmetic improvement, **not a new κ**. + +| Forward persistent scalar ordinals in full_frame_cleanup | Original | #4499, zero fields | #4499, one field | This package, zero fields | +|---|---:|---:|---:|---:| +| 4727–4764 | 418 | 358 | 358 | 358 | +| 1615–1620 | 52 | 52 | 46 | 42 | +| 2900–2905 | 52 | 52 | 46 | 42 | +| 4251–4276 | 244 | 224 | 224 | 224 | +| Total per orientation | 766 | 686 | 674 | 666 | + +The new construction temporarily adds one input into another, reads the resulting shared sum into all destinations, then reverses the input addition. It preserves every input and every arbitrary dirty exterior field, uses no CLEAR and requires no clean entry. The inverse-transpose orientation uses the corresponding dirty-target conjugation, with explicit subtraction before the update and restoration afterward. The two affected blocks each save 4 over the owned-field predecessor and 10 over their direct source bill. The other two windows retain #4499's gauges. + +The general compiler enumerates every source and target rank-one pivot whose coefficient ratios are dyadic. It selects the cheapest such adapter or the inherited zero-scratch gauge program. This gives a sufficient universal construction and a finite pivot comparison; it does not solve unrestricted circuit minimization. PROOF.md includes exact cost formulas and a sufficient condition under which borrowing beats the owned sum. The programs and native-price receipts are in RESULT.json. + +```sh +python3 -I -O -B research/borrowed-rankone/verify.py +python3 scripts/research_package.py --package research/borrowed-rankone +``` + +The package is standalone against its pinned main inputs, using standard-library Python. It includes the inherited gauge code and proof rather than requiring either pending PR to be merged. No Lean formalization or Linux execution is claimed. + +## Open next questions + +1. Integrate only these exact source-window replacements into the full native rebuild and replay stock, coefficient/norm and multiplication-bound invariants. This is required before any global bound claim; this local package adds no recursive jobs or productive-temporary credit. +2. Look for a larger source-bound rank-one block whose admissible pivot satisfies the strict cost inequality in PROOF.md. First compare the complete preparation, application and uncomputation bill. A rank-one label or lower gate count alone is insufficient. + +Scope and overlap limitations are recorded in TASK.json and ATTRIBUTION.md. The selected frontier and authoritative MathProof DAG are unchanged. diff --git a/research/borrowed-rankone/RESULT.json b/research/borrowed-rankone/RESULT.json new file mode 100644 index 0000000000..b325fa8024 --- /dev/null +++ b/research/borrowed-rankone/RESULT.json @@ -0,0 +1,10473 @@ +{ + "status": "PASS_BORROWED_RANKONE", + "source_cases": [ + { + "ordinals": [ + 4727, + 4764 + ], + "phase": "full_frame_cleanup", + "orientations": [ + { + "backward": false, + "source_indices": [ + 22007, + 22044 + ], + "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" + ] + ], + "old": 418, + "previous_one_field_allowance": 358, + "previous_zero_field_allowance": 358, + "selected": { + "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" + ] + ], + "source_exponents": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "target_exponents": [ + 2 + ], + "program": [ + [ + "scale", + [ + "Y", + 0 + ], + 4, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 0 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 1 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 2 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 3 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 4 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 5 + ], + 2, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 6 + ], + -2, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 7 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 8 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 9 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 10 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 11 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 12 + ], + -2, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 13 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 14 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 15 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 16 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 17 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 18 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 19 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 20 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 21 + ], + -2, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 22 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 23 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 24 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 25 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 26 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 27 + ], + 4, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 28 + ], + -2, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 29 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 30 + ], + 2, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 31 + ], + -2, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 32 + ], + 4, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 33 + ], + -4, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 34 + ], + 8, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 35 + ], + -4, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 36 + ], + 8, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 37 + ], + -4, + 1 + ], + [ + "scale", + [ + "Y", + 0 + ], + 1, + 4 + ] + ], + "old": 418, + "new": 358, + "valuation_objective": 54, + "constant": 304, + "circulation_cost": -54, + "cycle_steps": 16, + "dual_flows": [ + [ + 0, + 1, + 4, + 0, + -2 + ], + [ + 0, + 2, + 4, + 0, + -2 + ], + [ + 0, + 3, + 4, + 0, + -2 + ], + [ + 0, + 4, + 4, + 0, + -2 + ], + [ + 0, + 5, + 4, + 0, + -2 + ], + [ + 0, + 6, + 4, + 0, + 2 + ], + [ + 0, + 7, + 4, + 0, + 2 + ], + [ + 0, + 8, + 4, + 0, + -2 + ], + [ + 0, + 9, + 4, + 0, + -2 + ], + [ + 0, + 10, + 4, + 0, + -2 + ], + [ + 0, + 11, + 4, + 0, + -2 + ], + [ + 0, + 12, + 4, + 0, + -2 + ], + [ + 0, + 13, + 4, + 0, + 2 + ], + [ + 0, + 14, + 4, + 0, + -2 + ], + [ + 0, + 15, + 4, + 0, + -2 + ], + [ + 0, + 16, + 4, + 0, + -2 + ], + [ + 0, + 17, + 4, + 0, + -2 + ], + [ + 0, + 18, + 4, + 0, + -2 + ], + [ + 0, + 19, + 4, + 0, + -2 + ], + [ + 0, + 20, + 4, + 0, + 0 + ], + [ + 0, + 21, + 4, + 0, + 0 + ], + [ + 0, + 22, + 4, + 0, + 2 + ], + [ + 0, + 23, + 4, + 0, + 0 + ], + [ + 0, + 24, + 4, + 0, + 0 + ], + [ + 0, + 25, + 4, + 0, + 0 + ], + [ + 0, + 26, + 4, + 0, + 0 + ], + [ + 0, + 27, + 4, + 0, + 0 + ], + [ + 0, + 28, + 4, + 0, + 2 + ], + [ + 0, + 29, + 4, + 0, + 2 + ], + [ + 0, + 30, + 4, + 0, + 0 + ], + [ + 0, + 31, + 4, + 0, + 2 + ], + [ + 0, + 32, + 4, + 0, + 2 + ], + [ + 0, + 33, + 4, + 0, + 2 + ], + [ + 0, + 34, + 4, + 0, + 2 + ], + [ + 0, + 35, + 4, + 0, + 2 + ], + [ + 0, + 36, + 4, + 0, + 2 + ], + [ + 0, + 37, + 4, + 0, + 2 + ], + [ + 0, + 38, + 4, + 0, + 2 + ], + [ + 0, + 39, + 4, + 0, + 4 + ], + [ + 1, + 39, + 2, + 2, + -2 + ], + [ + 2, + 39, + 2, + 2, + -2 + ], + [ + 3, + 39, + 2, + 2, + -2 + ], + [ + 4, + 39, + 2, + 2, + -2 + ], + [ + 5, + 39, + 2, + 2, + -2 + ], + [ + 6, + 39, + 2, + 1, + 2 + ], + [ + 7, + 39, + 2, + 1, + 2 + ], + [ + 8, + 39, + 2, + 2, + -2 + ], + [ + 9, + 39, + 2, + 2, + -2 + ], + [ + 10, + 39, + 2, + 2, + -2 + ], + [ + 11, + 39, + 2, + 2, + -2 + ], + [ + 12, + 39, + 2, + 2, + -2 + ], + [ + 13, + 39, + 2, + 1, + 2 + ], + [ + 14, + 39, + 2, + 2, + -2 + ], + [ + 15, + 39, + 2, + 2, + -2 + ], + [ + 16, + 39, + 2, + 2, + -2 + ], + [ + 17, + 39, + 2, + 2, + -2 + ], + [ + 18, + 39, + 2, + 2, + -2 + ], + [ + 19, + 39, + 2, + 2, + -2 + ], + [ + 20, + 39, + 2, + 2, + 0 + ], + [ + 21, + 39, + 2, + 2, + 0 + ], + [ + 22, + 39, + 2, + 1, + 2 + ], + [ + 23, + 39, + 2, + 2, + 0 + ], + [ + 24, + 39, + 2, + 2, + 0 + ], + [ + 25, + 39, + 2, + 2, + 0 + ], + [ + 26, + 39, + 2, + 2, + 0 + ], + [ + 27, + 39, + 2, + 2, + 0 + ], + [ + 28, + 39, + 2, + 0, + 2 + ], + [ + 29, + 39, + 2, + 1, + 2 + ], + [ + 30, + 39, + 2, + 2, + 0 + ], + [ + 31, + 39, + 2, + 1, + 2 + ], + [ + 32, + 39, + 2, + 1, + 2 + ], + [ + 33, + 39, + 2, + 0, + 2 + ], + [ + 34, + 39, + 2, + 0, + 2 + ], + [ + 35, + 39, + 2, + -1, + 2 + ], + [ + 36, + 39, + 2, + 0, + 2 + ], + [ + 37, + 39, + 2, + -1, + 2 + ], + [ + 38, + 39, + 2, + 0, + 2 + ] + ], + "owned_peak": 0, + "new_recursive_jobs": 0 + }, + "gauge_certificate": { + "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" + ] + ], + "source_exponents": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "target_exponents": [ + 2 + ], + "program": [ + [ + "scale", + [ + "Y", + 0 + ], + 4, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 0 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 1 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 2 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 3 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 4 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 5 + ], + 2, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 6 + ], + -2, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 7 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 8 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 9 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 10 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 11 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 12 + ], + -2, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 13 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 14 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 15 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 16 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 17 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 18 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 19 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 20 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 21 + ], + -2, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 22 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 23 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 24 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 25 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 26 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 27 + ], + 4, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 28 + ], + -2, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 29 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 30 + ], + 2, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 31 + ], + -2, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 32 + ], + 4, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 33 + ], + -4, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 34 + ], + 8, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 35 + ], + -4, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 36 + ], + 8, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 37 + ], + -4, + 1 + ], + [ + "scale", + [ + "Y", + 0 + ], + 1, + 4 + ] + ], + "old": 418, + "new": 358, + "valuation_objective": 54, + "constant": 304, + "circulation_cost": -54, + "cycle_steps": 16, + "dual_flows": [ + [ + 0, + 1, + 4, + 0, + -2 + ], + [ + 0, + 2, + 4, + 0, + -2 + ], + [ + 0, + 3, + 4, + 0, + -2 + ], + [ + 0, + 4, + 4, + 0, + -2 + ], + [ + 0, + 5, + 4, + 0, + -2 + ], + [ + 0, + 6, + 4, + 0, + 2 + ], + [ + 0, + 7, + 4, + 0, + 2 + ], + [ + 0, + 8, + 4, + 0, + -2 + ], + [ + 0, + 9, + 4, + 0, + -2 + ], + [ + 0, + 10, + 4, + 0, + -2 + ], + [ + 0, + 11, + 4, + 0, + -2 + ], + [ + 0, + 12, + 4, + 0, + -2 + ], + [ + 0, + 13, + 4, + 0, + 2 + ], + [ + 0, + 14, + 4, + 0, + -2 + ], + [ + 0, + 15, + 4, + 0, + -2 + ], + [ + 0, + 16, + 4, + 0, + -2 + ], + [ + 0, + 17, + 4, + 0, + -2 + ], + [ + 0, + 18, + 4, + 0, + -2 + ], + [ + 0, + 19, + 4, + 0, + -2 + ], + [ + 0, + 20, + 4, + 0, + 0 + ], + [ + 0, + 21, + 4, + 0, + 0 + ], + [ + 0, + 22, + 4, + 0, + 2 + ], + [ + 0, + 23, + 4, + 0, + 0 + ], + [ + 0, + 24, + 4, + 0, + 0 + ], + [ + 0, + 25, + 4, + 0, + 0 + ], + [ + 0, + 26, + 4, + 0, + 0 + ], + [ + 0, + 27, + 4, + 0, + 0 + ], + [ + 0, + 28, + 4, + 0, + 2 + ], + [ + 0, + 29, + 4, + 0, + 2 + ], + [ + 0, + 30, + 4, + 0, + 0 + ], + [ + 0, + 31, + 4, + 0, + 2 + ], + [ + 0, + 32, + 4, + 0, + 2 + ], + [ + 0, + 33, + 4, + 0, + 2 + ], + [ + 0, + 34, + 4, + 0, + 2 + ], + [ + 0, + 35, + 4, + 0, + 2 + ], + [ + 0, + 36, + 4, + 0, + 2 + ], + [ + 0, + 37, + 4, + 0, + 2 + ], + [ + 0, + 38, + 4, + 0, + 2 + ], + [ + 0, + 39, + 4, + 0, + 4 + ], + [ + 1, + 39, + 2, + 2, + -2 + ], + [ + 2, + 39, + 2, + 2, + -2 + ], + [ + 3, + 39, + 2, + 2, + -2 + ], + [ + 4, + 39, + 2, + 2, + -2 + ], + [ + 5, + 39, + 2, + 2, + -2 + ], + [ + 6, + 39, + 2, + 1, + 2 + ], + [ + 7, + 39, + 2, + 1, + 2 + ], + [ + 8, + 39, + 2, + 2, + -2 + ], + [ + 9, + 39, + 2, + 2, + -2 + ], + [ + 10, + 39, + 2, + 2, + -2 + ], + [ + 11, + 39, + 2, + 2, + -2 + ], + [ + 12, + 39, + 2, + 2, + -2 + ], + [ + 13, + 39, + 2, + 1, + 2 + ], + [ + 14, + 39, + 2, + 2, + -2 + ], + [ + 15, + 39, + 2, + 2, + -2 + ], + [ + 16, + 39, + 2, + 2, + -2 + ], + [ + 17, + 39, + 2, + 2, + -2 + ], + [ + 18, + 39, + 2, + 2, + -2 + ], + [ + 19, + 39, + 2, + 2, + -2 + ], + [ + 20, + 39, + 2, + 2, + 0 + ], + [ + 21, + 39, + 2, + 2, + 0 + ], + [ + 22, + 39, + 2, + 1, + 2 + ], + [ + 23, + 39, + 2, + 2, + 0 + ], + [ + 24, + 39, + 2, + 2, + 0 + ], + [ + 25, + 39, + 2, + 2, + 0 + ], + [ + 26, + 39, + 2, + 2, + 0 + ], + [ + 27, + 39, + 2, + 2, + 0 + ], + [ + 28, + 39, + 2, + 0, + 2 + ], + [ + 29, + 39, + 2, + 1, + 2 + ], + [ + 30, + 39, + 2, + 2, + 0 + ], + [ + 31, + 39, + 2, + 1, + 2 + ], + [ + 32, + 39, + 2, + 1, + 2 + ], + [ + 33, + 39, + 2, + 0, + 2 + ], + [ + 34, + 39, + 2, + 0, + 2 + ], + [ + 35, + 39, + 2, + -1, + 2 + ], + [ + 36, + 39, + 2, + 0, + 2 + ], + [ + 37, + 39, + 2, + -1, + 2 + ], + [ + 38, + 39, + 2, + 0, + 2 + ] + ], + "owned_peak": 0, + "new_recursive_jobs": 0 + } + }, + { + "backward": true, + "source_indices": [ + 22007, + 22044 + ], + "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" + ] + ], + "old": 418, + "previous_one_field_allowance": 358, + "previous_zero_field_allowance": 358, + "selected": { + "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" + ] + ], + "source_exponents": [ + -2 + ], + "target_exponents": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "program": [ + [ + "scale", + [ + "X", + 0 + ], + 1, + 4 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 0 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 1 + ], + [ + "X", + 0 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 2 + ], + [ + "X", + 0 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 3 + ], + [ + "X", + 0 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 4 + ], + [ + "X", + 0 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 5 + ], + [ + "X", + 0 + ], + -2, + 1 + ], + [ + "add", + [ + "Y", + 6 + ], + [ + "X", + 0 + ], + 2, + 1 + ], + [ + "add", + [ + "Y", + 7 + ], + [ + "X", + 0 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 8 + ], + [ + "X", + 0 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 9 + ], + [ + "X", + 0 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 10 + ], + [ + "X", + 0 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 11 + ], + [ + "X", + 0 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 12 + ], + [ + "X", + 0 + ], + 2, + 1 + ], + [ + "add", + [ + "Y", + 13 + ], + [ + "X", + 0 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 14 + ], + [ + "X", + 0 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 15 + ], + [ + "X", + 0 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 16 + ], + [ + "X", + 0 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 17 + ], + [ + "X", + 0 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 18 + ], + [ + "X", + 0 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 19 + ], + [ + "X", + 0 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 20 + ], + [ + "X", + 0 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 21 + ], + [ + "X", + 0 + ], + 2, + 1 + ], + [ + "add", + [ + "Y", + 22 + ], + [ + "X", + 0 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 23 + ], + [ + "X", + 0 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 24 + ], + [ + "X", + 0 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 25 + ], + [ + "X", + 0 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 26 + ], + [ + "X", + 0 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 27 + ], + [ + "X", + 0 + ], + -4, + 1 + ], + [ + "add", + [ + "Y", + 28 + ], + [ + "X", + 0 + ], + 2, + 1 + ], + [ + "add", + [ + "Y", + 29 + ], + [ + "X", + 0 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 30 + ], + [ + "X", + 0 + ], + -2, + 1 + ], + [ + "add", + [ + "Y", + 31 + ], + [ + "X", + 0 + ], + 2, + 1 + ], + [ + "add", + [ + "Y", + 32 + ], + [ + "X", + 0 + ], + -4, + 1 + ], + [ + "add", + [ + "Y", + 33 + ], + [ + "X", + 0 + ], + 4, + 1 + ], + [ + "add", + [ + "Y", + 34 + ], + [ + "X", + 0 + ], + -8, + 1 + ], + [ + "add", + [ + "Y", + 35 + ], + [ + "X", + 0 + ], + 4, + 1 + ], + [ + "add", + [ + "Y", + 36 + ], + [ + "X", + 0 + ], + -8, + 1 + ], + [ + "add", + [ + "Y", + 37 + ], + [ + "X", + 0 + ], + 4, + 1 + ], + [ + "scale", + [ + "X", + 0 + ], + 4, + 1 + ] + ], + "old": 418, + "new": 358, + "valuation_objective": 54, + "constant": 304, + "circulation_cost": -54, + "cycle_steps": 16, + "dual_flows": [ + [ + 0, + 1, + 4, + 0, + -4 + ], + [ + 0, + 2, + 4, + 0, + 2 + ], + [ + 0, + 3, + 4, + 0, + 2 + ], + [ + 0, + 4, + 4, + 0, + 2 + ], + [ + 0, + 5, + 4, + 0, + 2 + ], + [ + 0, + 6, + 4, + 0, + 2 + ], + [ + 0, + 7, + 4, + 0, + -2 + ], + [ + 0, + 8, + 4, + 0, + -2 + ], + [ + 0, + 9, + 4, + 0, + 2 + ], + [ + 0, + 10, + 4, + 0, + 2 + ], + [ + 0, + 11, + 4, + 0, + 2 + ], + [ + 0, + 12, + 4, + 0, + 2 + ], + [ + 0, + 13, + 4, + 0, + 2 + ], + [ + 0, + 14, + 4, + 0, + -2 + ], + [ + 0, + 15, + 4, + 0, + 2 + ], + [ + 0, + 16, + 4, + 0, + 2 + ], + [ + 0, + 17, + 4, + 0, + 2 + ], + [ + 0, + 18, + 4, + 0, + 2 + ], + [ + 0, + 19, + 4, + 0, + 2 + ], + [ + 0, + 20, + 4, + 0, + 2 + ], + [ + 0, + 21, + 4, + 0, + 0 + ], + [ + 0, + 22, + 4, + 0, + 0 + ], + [ + 0, + 23, + 4, + 0, + -2 + ], + [ + 0, + 24, + 4, + 0, + 0 + ], + [ + 0, + 25, + 4, + 0, + 0 + ], + [ + 0, + 26, + 4, + 0, + 0 + ], + [ + 0, + 27, + 4, + 0, + 0 + ], + [ + 0, + 28, + 4, + 0, + 0 + ], + [ + 0, + 29, + 4, + 0, + -2 + ], + [ + 0, + 30, + 4, + 0, + -2 + ], + [ + 0, + 31, + 4, + 0, + 0 + ], + [ + 0, + 32, + 4, + 0, + -2 + ], + [ + 0, + 33, + 4, + 0, + -2 + ], + [ + 0, + 34, + 4, + 0, + -2 + ], + [ + 0, + 35, + 4, + 0, + -2 + ], + [ + 0, + 36, + 4, + 0, + -2 + ], + [ + 0, + 37, + 4, + 0, + -2 + ], + [ + 0, + 38, + 4, + 0, + -2 + ], + [ + 0, + 39, + 4, + 0, + -2 + ], + [ + 1, + 2, + 2, + 2, + -2 + ], + [ + 1, + 3, + 2, + 2, + -2 + ], + [ + 1, + 4, + 2, + 2, + -2 + ], + [ + 1, + 5, + 2, + 2, + -2 + ], + [ + 1, + 6, + 2, + 2, + -2 + ], + [ + 1, + 7, + 2, + 1, + 2 + ], + [ + 1, + 8, + 2, + 1, + 2 + ], + [ + 1, + 9, + 2, + 2, + -2 + ], + [ + 1, + 10, + 2, + 2, + -2 + ], + [ + 1, + 11, + 2, + 2, + -2 + ], + [ + 1, + 12, + 2, + 2, + -2 + ], + [ + 1, + 13, + 2, + 2, + -2 + ], + [ + 1, + 14, + 2, + 1, + 2 + ], + [ + 1, + 15, + 2, + 2, + -2 + ], + [ + 1, + 16, + 2, + 2, + -2 + ], + [ + 1, + 17, + 2, + 2, + -2 + ], + [ + 1, + 18, + 2, + 2, + -2 + ], + [ + 1, + 19, + 2, + 2, + -2 + ], + [ + 1, + 20, + 2, + 2, + -2 + ], + [ + 1, + 21, + 2, + 2, + 0 + ], + [ + 1, + 22, + 2, + 2, + 0 + ], + [ + 1, + 23, + 2, + 1, + 2 + ], + [ + 1, + 24, + 2, + 2, + 0 + ], + [ + 1, + 25, + 2, + 2, + 0 + ], + [ + 1, + 26, + 2, + 2, + 0 + ], + [ + 1, + 27, + 2, + 2, + 0 + ], + [ + 1, + 28, + 2, + 2, + 0 + ], + [ + 1, + 29, + 2, + 0, + 2 + ], + [ + 1, + 30, + 2, + 1, + 2 + ], + [ + 1, + 31, + 2, + 2, + 0 + ], + [ + 1, + 32, + 2, + 1, + 2 + ], + [ + 1, + 33, + 2, + 1, + 2 + ], + [ + 1, + 34, + 2, + 0, + 2 + ], + [ + 1, + 35, + 2, + 0, + 2 + ], + [ + 1, + 36, + 2, + -1, + 2 + ], + [ + 1, + 37, + 2, + 0, + 2 + ], + [ + 1, + 38, + 2, + -1, + 2 + ], + [ + 1, + 39, + 2, + 0, + 2 + ] + ], + "owned_peak": 0, + "new_recursive_jobs": 0 + }, + "gauge_certificate": { + "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" + ] + ], + "source_exponents": [ + -2 + ], + "target_exponents": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "program": [ + [ + "scale", + [ + "X", + 0 + ], + 1, + 4 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 0 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 1 + ], + [ + "X", + 0 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 2 + ], + [ + "X", + 0 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 3 + ], + [ + "X", + 0 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 4 + ], + [ + "X", + 0 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 5 + ], + [ + "X", + 0 + ], + -2, + 1 + ], + [ + "add", + [ + "Y", + 6 + ], + [ + "X", + 0 + ], + 2, + 1 + ], + [ + "add", + [ + "Y", + 7 + ], + [ + "X", + 0 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 8 + ], + [ + "X", + 0 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 9 + ], + [ + "X", + 0 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 10 + ], + [ + "X", + 0 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 11 + ], + [ + "X", + 0 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 12 + ], + [ + "X", + 0 + ], + 2, + 1 + ], + [ + "add", + [ + "Y", + 13 + ], + [ + "X", + 0 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 14 + ], + [ + "X", + 0 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 15 + ], + [ + "X", + 0 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 16 + ], + [ + "X", + 0 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 17 + ], + [ + "X", + 0 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 18 + ], + [ + "X", + 0 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 19 + ], + [ + "X", + 0 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 20 + ], + [ + "X", + 0 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 21 + ], + [ + "X", + 0 + ], + 2, + 1 + ], + [ + "add", + [ + "Y", + 22 + ], + [ + "X", + 0 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 23 + ], + [ + "X", + 0 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 24 + ], + [ + "X", + 0 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 25 + ], + [ + "X", + 0 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 26 + ], + [ + "X", + 0 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 27 + ], + [ + "X", + 0 + ], + -4, + 1 + ], + [ + "add", + [ + "Y", + 28 + ], + [ + "X", + 0 + ], + 2, + 1 + ], + [ + "add", + [ + "Y", + 29 + ], + [ + "X", + 0 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 30 + ], + [ + "X", + 0 + ], + -2, + 1 + ], + [ + "add", + [ + "Y", + 31 + ], + [ + "X", + 0 + ], + 2, + 1 + ], + [ + "add", + [ + "Y", + 32 + ], + [ + "X", + 0 + ], + -4, + 1 + ], + [ + "add", + [ + "Y", + 33 + ], + [ + "X", + 0 + ], + 4, + 1 + ], + [ + "add", + [ + "Y", + 34 + ], + [ + "X", + 0 + ], + -8, + 1 + ], + [ + "add", + [ + "Y", + 35 + ], + [ + "X", + 0 + ], + 4, + 1 + ], + [ + "add", + [ + "Y", + 36 + ], + [ + "X", + 0 + ], + -8, + 1 + ], + [ + "add", + [ + "Y", + 37 + ], + [ + "X", + 0 + ], + 4, + 1 + ], + [ + "scale", + [ + "X", + 0 + ], + 4, + 1 + ] + ], + "old": 418, + "new": 358, + "valuation_objective": 54, + "constant": 304, + "circulation_cost": -54, + "cycle_steps": 16, + "dual_flows": [ + [ + 0, + 1, + 4, + 0, + -4 + ], + [ + 0, + 2, + 4, + 0, + 2 + ], + [ + 0, + 3, + 4, + 0, + 2 + ], + [ + 0, + 4, + 4, + 0, + 2 + ], + [ + 0, + 5, + 4, + 0, + 2 + ], + [ + 0, + 6, + 4, + 0, + 2 + ], + [ + 0, + 7, + 4, + 0, + -2 + ], + [ + 0, + 8, + 4, + 0, + -2 + ], + [ + 0, + 9, + 4, + 0, + 2 + ], + [ + 0, + 10, + 4, + 0, + 2 + ], + [ + 0, + 11, + 4, + 0, + 2 + ], + [ + 0, + 12, + 4, + 0, + 2 + ], + [ + 0, + 13, + 4, + 0, + 2 + ], + [ + 0, + 14, + 4, + 0, + -2 + ], + [ + 0, + 15, + 4, + 0, + 2 + ], + [ + 0, + 16, + 4, + 0, + 2 + ], + [ + 0, + 17, + 4, + 0, + 2 + ], + [ + 0, + 18, + 4, + 0, + 2 + ], + [ + 0, + 19, + 4, + 0, + 2 + ], + [ + 0, + 20, + 4, + 0, + 2 + ], + [ + 0, + 21, + 4, + 0, + 0 + ], + [ + 0, + 22, + 4, + 0, + 0 + ], + [ + 0, + 23, + 4, + 0, + -2 + ], + [ + 0, + 24, + 4, + 0, + 0 + ], + [ + 0, + 25, + 4, + 0, + 0 + ], + [ + 0, + 26, + 4, + 0, + 0 + ], + [ + 0, + 27, + 4, + 0, + 0 + ], + [ + 0, + 28, + 4, + 0, + 0 + ], + [ + 0, + 29, + 4, + 0, + -2 + ], + [ + 0, + 30, + 4, + 0, + -2 + ], + [ + 0, + 31, + 4, + 0, + 0 + ], + [ + 0, + 32, + 4, + 0, + -2 + ], + [ + 0, + 33, + 4, + 0, + -2 + ], + [ + 0, + 34, + 4, + 0, + -2 + ], + [ + 0, + 35, + 4, + 0, + -2 + ], + [ + 0, + 36, + 4, + 0, + -2 + ], + [ + 0, + 37, + 4, + 0, + -2 + ], + [ + 0, + 38, + 4, + 0, + -2 + ], + [ + 0, + 39, + 4, + 0, + -2 + ], + [ + 1, + 2, + 2, + 2, + -2 + ], + [ + 1, + 3, + 2, + 2, + -2 + ], + [ + 1, + 4, + 2, + 2, + -2 + ], + [ + 1, + 5, + 2, + 2, + -2 + ], + [ + 1, + 6, + 2, + 2, + -2 + ], + [ + 1, + 7, + 2, + 1, + 2 + ], + [ + 1, + 8, + 2, + 1, + 2 + ], + [ + 1, + 9, + 2, + 2, + -2 + ], + [ + 1, + 10, + 2, + 2, + -2 + ], + [ + 1, + 11, + 2, + 2, + -2 + ], + [ + 1, + 12, + 2, + 2, + -2 + ], + [ + 1, + 13, + 2, + 2, + -2 + ], + [ + 1, + 14, + 2, + 1, + 2 + ], + [ + 1, + 15, + 2, + 2, + -2 + ], + [ + 1, + 16, + 2, + 2, + -2 + ], + [ + 1, + 17, + 2, + 2, + -2 + ], + [ + 1, + 18, + 2, + 2, + -2 + ], + [ + 1, + 19, + 2, + 2, + -2 + ], + [ + 1, + 20, + 2, + 2, + -2 + ], + [ + 1, + 21, + 2, + 2, + 0 + ], + [ + 1, + 22, + 2, + 2, + 0 + ], + [ + 1, + 23, + 2, + 1, + 2 + ], + [ + 1, + 24, + 2, + 2, + 0 + ], + [ + 1, + 25, + 2, + 2, + 0 + ], + [ + 1, + 26, + 2, + 2, + 0 + ], + [ + 1, + 27, + 2, + 2, + 0 + ], + [ + 1, + 28, + 2, + 2, + 0 + ], + [ + 1, + 29, + 2, + 0, + 2 + ], + [ + 1, + 30, + 2, + 1, + 2 + ], + [ + 1, + 31, + 2, + 2, + 0 + ], + [ + 1, + 32, + 2, + 1, + 2 + ], + [ + 1, + 33, + 2, + 1, + 2 + ], + [ + 1, + 34, + 2, + 0, + 2 + ], + [ + 1, + 35, + 2, + 0, + 2 + ], + [ + 1, + 36, + 2, + -1, + 2 + ], + [ + 1, + 37, + 2, + 0, + 2 + ], + [ + 1, + 38, + 2, + -1, + 2 + ], + [ + 1, + 39, + 2, + 0, + 2 + ] + ], + "owned_peak": 0, + "new_recursive_jobs": 0 + } + } + ] + }, + { + "ordinals": [ + 1615, + 1620 + ], + "phase": "full_frame_cleanup", + "orientations": [ + { + "backward": false, + "source_indices": [ + 18895, + 18900 + ], + "matrix": [ + [ + "-1", + "-1" + ], + [ + "1", + "1" + ], + [ + "-1/2", + "-1/2" + ] + ], + "old": 52, + "previous_one_field_allowance": 46, + "previous_zero_field_allowance": 52, + "selected": { + "mechanism": "borrow-source", + "pivot": 0, + "preparation_count": 1, + "program": [ + [ + "add", + [ + "X", + 0 + ], + [ + "X", + 1 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 0 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 1 + ], + [ + "X", + 0 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 2 + ], + [ + "X", + 0 + ], + -1, + 2 + ], + [ + "add", + [ + "X", + 0 + ], + [ + "X", + 1 + ], + -1, + 1 + ] + ], + "new": 42, + "owned_peak": 0, + "new_recursive_jobs": 0 + }, + "gauge_certificate": { + "matrix": [ + [ + "-1", + "-1" + ], + [ + "1", + "1" + ], + [ + "-1/2", + "-1/2" + ] + ], + "source_exponents": [ + 0, + 0 + ], + "target_exponents": [ + 0, + 0, + 0 + ], + "program": [ + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 0 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 1 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 1 + ], + [ + "X", + 0 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 1 + ], + [ + "X", + 1 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 2 + ], + [ + "X", + 0 + ], + -1, + 2 + ], + [ + "add", + [ + "Y", + 2 + ], + [ + "X", + 1 + ], + -1, + 2 + ] + ], + "old": 52, + "new": 52, + "valuation_objective": 4, + "constant": 48, + "circulation_cost": -4, + "cycle_steps": 2, + "dual_flows": [ + [ + 0, + 1, + 4, + 0, + -2 + ], + [ + 0, + 2, + 4, + 0, + -2 + ], + [ + 0, + 3, + 4, + 0, + 0 + ], + [ + 0, + 4, + 4, + 0, + 0 + ], + [ + 0, + 5, + 4, + 0, + 4 + ], + [ + 1, + 3, + 2, + 0, + 0 + ], + [ + 2, + 3, + 2, + 0, + 0 + ], + [ + 1, + 4, + 2, + 0, + 0 + ], + [ + 2, + 4, + 2, + 0, + 0 + ], + [ + 1, + 5, + 2, + 1, + -2 + ], + [ + 2, + 5, + 2, + 1, + -2 + ] + ], + "owned_peak": 0, + "new_recursive_jobs": 0 + } + }, + { + "backward": true, + "source_indices": [ + 18895, + 18900 + ], + "matrix": [ + [ + "1", + "-1", + "1/2" + ], + [ + "1", + "-1", + "1/2" + ] + ], + "old": 52, + "previous_one_field_allowance": 46, + "previous_zero_field_allowance": 52, + "selected": { + "mechanism": "borrow-target", + "pivot": 0, + "preparation_count": 1, + "program": [ + [ + "add", + [ + "Y", + 1 + ], + [ + "Y", + 0 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 0 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 1 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 2 + ], + 1, + 2 + ], + [ + "add", + [ + "Y", + 1 + ], + [ + "Y", + 0 + ], + 1, + 1 + ] + ], + "new": 42, + "owned_peak": 0, + "new_recursive_jobs": 0 + }, + "gauge_certificate": { + "matrix": [ + [ + "1", + "-1", + "1/2" + ], + [ + "1", + "-1", + "1/2" + ] + ], + "source_exponents": [ + 0, + 0, + 0 + ], + "target_exponents": [ + 0, + 0 + ], + "program": [ + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 0 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 1 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 2 + ], + 1, + 2 + ], + [ + "add", + [ + "Y", + 1 + ], + [ + "X", + 0 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 1 + ], + [ + "X", + 1 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 1 + ], + [ + "X", + 2 + ], + 1, + 2 + ] + ], + "old": 52, + "new": 52, + "valuation_objective": 4, + "constant": 48, + "circulation_cost": -4, + "cycle_steps": 2, + "dual_flows": [ + [ + 0, + 1, + 4, + 0, + 0 + ], + [ + 0, + 2, + 4, + 0, + 0 + ], + [ + 0, + 3, + 4, + 0, + -4 + ], + [ + 0, + 4, + 4, + 0, + 2 + ], + [ + 0, + 5, + 4, + 0, + 2 + ], + [ + 1, + 4, + 2, + 0, + 0 + ], + [ + 2, + 4, + 2, + 0, + 0 + ], + [ + 3, + 4, + 2, + 1, + -2 + ], + [ + 1, + 5, + 2, + 0, + 0 + ], + [ + 2, + 5, + 2, + 0, + 0 + ], + [ + 3, + 5, + 2, + 1, + -2 + ] + ], + "owned_peak": 0, + "new_recursive_jobs": 0 + } + } + ] + }, + { + "ordinals": [ + 2900, + 2905 + ], + "phase": "full_frame_cleanup", + "orientations": [ + { + "backward": false, + "source_indices": [ + 20180, + 20185 + ], + "matrix": [ + [ + "-1", + "-1" + ], + [ + "1", + "1" + ], + [ + "-1/2", + "-1/2" + ] + ], + "old": 52, + "previous_one_field_allowance": 46, + "previous_zero_field_allowance": 52, + "selected": { + "mechanism": "borrow-source", + "pivot": 0, + "preparation_count": 1, + "program": [ + [ + "add", + [ + "X", + 0 + ], + [ + "X", + 1 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 0 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 1 + ], + [ + "X", + 0 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 2 + ], + [ + "X", + 0 + ], + -1, + 2 + ], + [ + "add", + [ + "X", + 0 + ], + [ + "X", + 1 + ], + -1, + 1 + ] + ], + "new": 42, + "owned_peak": 0, + "new_recursive_jobs": 0 + }, + "gauge_certificate": { + "matrix": [ + [ + "-1", + "-1" + ], + [ + "1", + "1" + ], + [ + "-1/2", + "-1/2" + ] + ], + "source_exponents": [ + 0, + 0 + ], + "target_exponents": [ + 0, + 0, + 0 + ], + "program": [ + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 0 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 1 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 1 + ], + [ + "X", + 0 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 1 + ], + [ + "X", + 1 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 2 + ], + [ + "X", + 0 + ], + -1, + 2 + ], + [ + "add", + [ + "Y", + 2 + ], + [ + "X", + 1 + ], + -1, + 2 + ] + ], + "old": 52, + "new": 52, + "valuation_objective": 4, + "constant": 48, + "circulation_cost": -4, + "cycle_steps": 2, + "dual_flows": [ + [ + 0, + 1, + 4, + 0, + -2 + ], + [ + 0, + 2, + 4, + 0, + -2 + ], + [ + 0, + 3, + 4, + 0, + 0 + ], + [ + 0, + 4, + 4, + 0, + 0 + ], + [ + 0, + 5, + 4, + 0, + 4 + ], + [ + 1, + 3, + 2, + 0, + 0 + ], + [ + 2, + 3, + 2, + 0, + 0 + ], + [ + 1, + 4, + 2, + 0, + 0 + ], + [ + 2, + 4, + 2, + 0, + 0 + ], + [ + 1, + 5, + 2, + 1, + -2 + ], + [ + 2, + 5, + 2, + 1, + -2 + ] + ], + "owned_peak": 0, + "new_recursive_jobs": 0 + } + }, + { + "backward": true, + "source_indices": [ + 20180, + 20185 + ], + "matrix": [ + [ + "1", + "-1", + "1/2" + ], + [ + "1", + "-1", + "1/2" + ] + ], + "old": 52, + "previous_one_field_allowance": 46, + "previous_zero_field_allowance": 52, + "selected": { + "mechanism": "borrow-target", + "pivot": 0, + "preparation_count": 1, + "program": [ + [ + "add", + [ + "Y", + 1 + ], + [ + "Y", + 0 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 0 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 1 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 2 + ], + 1, + 2 + ], + [ + "add", + [ + "Y", + 1 + ], + [ + "Y", + 0 + ], + 1, + 1 + ] + ], + "new": 42, + "owned_peak": 0, + "new_recursive_jobs": 0 + }, + "gauge_certificate": { + "matrix": [ + [ + "1", + "-1", + "1/2" + ], + [ + "1", + "-1", + "1/2" + ] + ], + "source_exponents": [ + 0, + 0, + 0 + ], + "target_exponents": [ + 0, + 0 + ], + "program": [ + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 0 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 1 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 2 + ], + 1, + 2 + ], + [ + "add", + [ + "Y", + 1 + ], + [ + "X", + 0 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 1 + ], + [ + "X", + 1 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 1 + ], + [ + "X", + 2 + ], + 1, + 2 + ] + ], + "old": 52, + "new": 52, + "valuation_objective": 4, + "constant": 48, + "circulation_cost": -4, + "cycle_steps": 2, + "dual_flows": [ + [ + 0, + 1, + 4, + 0, + 0 + ], + [ + 0, + 2, + 4, + 0, + 0 + ], + [ + 0, + 3, + 4, + 0, + -4 + ], + [ + 0, + 4, + 4, + 0, + 2 + ], + [ + 0, + 5, + 4, + 0, + 2 + ], + [ + 1, + 4, + 2, + 0, + 0 + ], + [ + 2, + 4, + 2, + 0, + 0 + ], + [ + 3, + 4, + 2, + 1, + -2 + ], + [ + 1, + 5, + 2, + 0, + 0 + ], + [ + 2, + 5, + 2, + 0, + 0 + ], + [ + 3, + 5, + 2, + 1, + -2 + ] + ], + "owned_peak": 0, + "new_recursive_jobs": 0 + } + } + ] + }, + { + "ordinals": [ + 4251, + 4276 + ], + "phase": "full_frame_cleanup", + "orientations": [ + { + "backward": false, + "source_indices": [ + 21531, + 21556 + ], + "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" + ] + ], + "old": 244, + "previous_one_field_allowance": 224, + "previous_zero_field_allowance": 224, + "selected": { + "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" + ] + ], + "source_exponents": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "target_exponents": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 2, + 0, + 0 + ], + "program": [ + [ + "scale", + [ + "Y", + 13 + ], + 4, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 0 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 1 + ], + [ + "X", + 0 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 2 + ], + [ + "X", + 0 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 3 + ], + [ + "X", + 0 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 4 + ], + [ + "X", + 0 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 5 + ], + [ + "X", + 0 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 6 + ], + [ + "X", + 0 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 7 + ], + [ + "X", + 0 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 8 + ], + [ + "X", + 0 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 9 + ], + [ + "X", + 0 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 10 + ], + [ + "X", + 0 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 11 + ], + [ + "X", + 0 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 12 + ], + [ + "X", + 0 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 13 + ], + [ + "X", + 0 + ], + 4, + 1 + ], + [ + "add", + [ + "Y", + 13 + ], + [ + "X", + 1 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 13 + ], + [ + "X", + 2 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 13 + ], + [ + "X", + 3 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 13 + ], + [ + "X", + 4 + ], + -2, + 1 + ], + [ + "add", + [ + "Y", + 13 + ], + [ + "X", + 5 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 13 + ], + [ + "X", + 6 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 13 + ], + [ + "X", + 7 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 13 + ], + [ + "X", + 8 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 13 + ], + [ + "X", + 9 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 13 + ], + [ + "X", + 10 + ], + -2, + 1 + ], + [ + "add", + [ + "Y", + 14 + ], + [ + "X", + 0 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 15 + ], + [ + "X", + 0 + ], + 1, + 1 + ], + [ + "scale", + [ + "Y", + 13 + ], + 1, + 4 + ] + ], + "old": 244, + "new": 224, + "valuation_objective": 16, + "constant": 208, + "circulation_cost": -16, + "cycle_steps": 5, + "dual_flows": [ + [ + 0, + 1, + 4, + 0, + 2 + ], + [ + 0, + 2, + 4, + 0, + -2 + ], + [ + 0, + 3, + 4, + 0, + -2 + ], + [ + 0, + 4, + 4, + 0, + -2 + ], + [ + 0, + 5, + 4, + 0, + 2 + ], + [ + 0, + 6, + 4, + 0, + -2 + ], + [ + 0, + 7, + 4, + 0, + -2 + ], + [ + 0, + 8, + 4, + 0, + 0 + ], + [ + 0, + 9, + 4, + 0, + 0 + ], + [ + 0, + 10, + 4, + 0, + 0 + ], + [ + 0, + 11, + 4, + 0, + 2 + ], + [ + 0, + 12, + 4, + 0, + 0 + ], + [ + 0, + 13, + 4, + 0, + 0 + ], + [ + 0, + 14, + 4, + 0, + 0 + ], + [ + 0, + 15, + 4, + 0, + 0 + ], + [ + 0, + 16, + 4, + 0, + 0 + ], + [ + 0, + 17, + 4, + 0, + 0 + ], + [ + 0, + 18, + 4, + 0, + 0 + ], + [ + 0, + 19, + 4, + 0, + 0 + ], + [ + 0, + 20, + 4, + 0, + 0 + ], + [ + 0, + 21, + 4, + 0, + 0 + ], + [ + 0, + 22, + 4, + 0, + 0 + ], + [ + 0, + 23, + 4, + 0, + 0 + ], + [ + 0, + 24, + 4, + 0, + 0 + ], + [ + 0, + 25, + 4, + 0, + 4 + ], + [ + 0, + 26, + 4, + 0, + 0 + ], + [ + 0, + 27, + 4, + 0, + 0 + ], + [ + 1, + 12, + 2, + 0, + 0 + ], + [ + 1, + 13, + 2, + 0, + 0 + ], + [ + 1, + 14, + 2, + 0, + 0 + ], + [ + 1, + 15, + 2, + 0, + 0 + ], + [ + 1, + 16, + 2, + 0, + 0 + ], + [ + 1, + 17, + 2, + 0, + 0 + ], + [ + 1, + 18, + 2, + 0, + 0 + ], + [ + 1, + 19, + 2, + 0, + 0 + ], + [ + 1, + 20, + 2, + 0, + 0 + ], + [ + 1, + 21, + 2, + 0, + 0 + ], + [ + 1, + 22, + 2, + 0, + 0 + ], + [ + 1, + 23, + 2, + 0, + 0 + ], + [ + 1, + 24, + 2, + 0, + 0 + ], + [ + 1, + 25, + 2, + 0, + 2 + ], + [ + 2, + 25, + 2, + 2, + -2 + ], + [ + 3, + 25, + 2, + 2, + -2 + ], + [ + 4, + 25, + 2, + 2, + -2 + ], + [ + 5, + 25, + 2, + 1, + 2 + ], + [ + 6, + 25, + 2, + 2, + -2 + ], + [ + 7, + 25, + 2, + 2, + -2 + ], + [ + 8, + 25, + 2, + 2, + 0 + ], + [ + 9, + 25, + 2, + 2, + 0 + ], + [ + 10, + 25, + 2, + 2, + 0 + ], + [ + 11, + 25, + 2, + 1, + 2 + ], + [ + 1, + 26, + 2, + 0, + 0 + ], + [ + 1, + 27, + 2, + 0, + 0 + ] + ], + "owned_peak": 0, + "new_recursive_jobs": 0 + }, + "gauge_certificate": { + "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" + ] + ], + "source_exponents": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "target_exponents": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 2, + 0, + 0 + ], + "program": [ + [ + "scale", + [ + "Y", + 13 + ], + 4, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 0 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 1 + ], + [ + "X", + 0 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 2 + ], + [ + "X", + 0 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 3 + ], + [ + "X", + 0 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 4 + ], + [ + "X", + 0 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 5 + ], + [ + "X", + 0 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 6 + ], + [ + "X", + 0 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 7 + ], + [ + "X", + 0 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 8 + ], + [ + "X", + 0 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 9 + ], + [ + "X", + 0 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 10 + ], + [ + "X", + 0 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 11 + ], + [ + "X", + 0 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 12 + ], + [ + "X", + 0 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 13 + ], + [ + "X", + 0 + ], + 4, + 1 + ], + [ + "add", + [ + "Y", + 13 + ], + [ + "X", + 1 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 13 + ], + [ + "X", + 2 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 13 + ], + [ + "X", + 3 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 13 + ], + [ + "X", + 4 + ], + -2, + 1 + ], + [ + "add", + [ + "Y", + 13 + ], + [ + "X", + 5 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 13 + ], + [ + "X", + 6 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 13 + ], + [ + "X", + 7 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 13 + ], + [ + "X", + 8 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 13 + ], + [ + "X", + 9 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 13 + ], + [ + "X", + 10 + ], + -2, + 1 + ], + [ + "add", + [ + "Y", + 14 + ], + [ + "X", + 0 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 15 + ], + [ + "X", + 0 + ], + 1, + 1 + ], + [ + "scale", + [ + "Y", + 13 + ], + 1, + 4 + ] + ], + "old": 244, + "new": 224, + "valuation_objective": 16, + "constant": 208, + "circulation_cost": -16, + "cycle_steps": 5, + "dual_flows": [ + [ + 0, + 1, + 4, + 0, + 2 + ], + [ + 0, + 2, + 4, + 0, + -2 + ], + [ + 0, + 3, + 4, + 0, + -2 + ], + [ + 0, + 4, + 4, + 0, + -2 + ], + [ + 0, + 5, + 4, + 0, + 2 + ], + [ + 0, + 6, + 4, + 0, + -2 + ], + [ + 0, + 7, + 4, + 0, + -2 + ], + [ + 0, + 8, + 4, + 0, + 0 + ], + [ + 0, + 9, + 4, + 0, + 0 + ], + [ + 0, + 10, + 4, + 0, + 0 + ], + [ + 0, + 11, + 4, + 0, + 2 + ], + [ + 0, + 12, + 4, + 0, + 0 + ], + [ + 0, + 13, + 4, + 0, + 0 + ], + [ + 0, + 14, + 4, + 0, + 0 + ], + [ + 0, + 15, + 4, + 0, + 0 + ], + [ + 0, + 16, + 4, + 0, + 0 + ], + [ + 0, + 17, + 4, + 0, + 0 + ], + [ + 0, + 18, + 4, + 0, + 0 + ], + [ + 0, + 19, + 4, + 0, + 0 + ], + [ + 0, + 20, + 4, + 0, + 0 + ], + [ + 0, + 21, + 4, + 0, + 0 + ], + [ + 0, + 22, + 4, + 0, + 0 + ], + [ + 0, + 23, + 4, + 0, + 0 + ], + [ + 0, + 24, + 4, + 0, + 0 + ], + [ + 0, + 25, + 4, + 0, + 4 + ], + [ + 0, + 26, + 4, + 0, + 0 + ], + [ + 0, + 27, + 4, + 0, + 0 + ], + [ + 1, + 12, + 2, + 0, + 0 + ], + [ + 1, + 13, + 2, + 0, + 0 + ], + [ + 1, + 14, + 2, + 0, + 0 + ], + [ + 1, + 15, + 2, + 0, + 0 + ], + [ + 1, + 16, + 2, + 0, + 0 + ], + [ + 1, + 17, + 2, + 0, + 0 + ], + [ + 1, + 18, + 2, + 0, + 0 + ], + [ + 1, + 19, + 2, + 0, + 0 + ], + [ + 1, + 20, + 2, + 0, + 0 + ], + [ + 1, + 21, + 2, + 0, + 0 + ], + [ + 1, + 22, + 2, + 0, + 0 + ], + [ + 1, + 23, + 2, + 0, + 0 + ], + [ + 1, + 24, + 2, + 0, + 0 + ], + [ + 1, + 25, + 2, + 0, + 2 + ], + [ + 2, + 25, + 2, + 2, + -2 + ], + [ + 3, + 25, + 2, + 2, + -2 + ], + [ + 4, + 25, + 2, + 2, + -2 + ], + [ + 5, + 25, + 2, + 1, + 2 + ], + [ + 6, + 25, + 2, + 2, + -2 + ], + [ + 7, + 25, + 2, + 2, + -2 + ], + [ + 8, + 25, + 2, + 2, + 0 + ], + [ + 9, + 25, + 2, + 2, + 0 + ], + [ + 10, + 25, + 2, + 2, + 0 + ], + [ + 11, + 25, + 2, + 1, + 2 + ], + [ + 1, + 26, + 2, + 0, + 0 + ], + [ + 1, + 27, + 2, + 0, + 0 + ] + ], + "owned_peak": 0, + "new_recursive_jobs": 0 + } + }, + { + "backward": true, + "source_indices": [ + 21531, + 21556 + ], + "matrix": [ + [ + "1", + "1", + "-1", + "-1", + "-1", + "1", + "1", + "-1", + "-1", + "1", + "1", + "1", + "-1", + "-1", + "1", + "-1" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1/4", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1/4", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1/4", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1/2", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1/4", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1/4", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "-1/4", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1/4", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1/4", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1/2", + "0", + "0" + ] + ], + "old": 244, + "previous_one_field_allowance": 224, + "previous_zero_field_allowance": 224, + "selected": { + "matrix": [ + [ + "1", + "1", + "-1", + "-1", + "-1", + "1", + "1", + "-1", + "-1", + "1", + "1", + "1", + "-1", + "-1", + "1", + "-1" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1/4", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1/4", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1/4", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1/2", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1/4", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1/4", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "-1/4", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1/4", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1/4", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1/2", + "0", + "0" + ] + ], + "source_exponents": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + -2, + 0, + 0 + ], + "target_exponents": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "program": [ + [ + "scale", + [ + "X", + 13 + ], + 1, + 4 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 0 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 1 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 2 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 3 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 4 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 5 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 6 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 7 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 8 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 9 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 10 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 11 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 12 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 13 + ], + -4, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 14 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 15 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 1 + ], + [ + "X", + 13 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 2 + ], + [ + "X", + 13 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 3 + ], + [ + "X", + 13 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 4 + ], + [ + "X", + 13 + ], + 2, + 1 + ], + [ + "add", + [ + "Y", + 5 + ], + [ + "X", + 13 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 6 + ], + [ + "X", + 13 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 7 + ], + [ + "X", + 13 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 8 + ], + [ + "X", + 13 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 9 + ], + [ + "X", + 13 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 10 + ], + [ + "X", + 13 + ], + 2, + 1 + ], + [ + "scale", + [ + "X", + 13 + ], + 4, + 1 + ] + ], + "old": 244, + "new": 224, + "valuation_objective": 16, + "constant": 208, + "circulation_cost": -16, + "cycle_steps": 5, + "dual_flows": [ + [ + 0, + 1, + 4, + 0, + 0 + ], + [ + 0, + 2, + 4, + 0, + 0 + ], + [ + 0, + 3, + 4, + 0, + 0 + ], + [ + 0, + 4, + 4, + 0, + 0 + ], + [ + 0, + 5, + 4, + 0, + 0 + ], + [ + 0, + 6, + 4, + 0, + 0 + ], + [ + 0, + 7, + 4, + 0, + 0 + ], + [ + 0, + 8, + 4, + 0, + 0 + ], + [ + 0, + 9, + 4, + 0, + 0 + ], + [ + 0, + 10, + 4, + 0, + 0 + ], + [ + 0, + 11, + 4, + 0, + 0 + ], + [ + 0, + 12, + 4, + 0, + 0 + ], + [ + 0, + 13, + 4, + 0, + 0 + ], + [ + 0, + 14, + 4, + 0, + -4 + ], + [ + 0, + 15, + 4, + 0, + 0 + ], + [ + 0, + 16, + 4, + 0, + 0 + ], + [ + 0, + 17, + 4, + 0, + -2 + ], + [ + 0, + 18, + 4, + 0, + 2 + ], + [ + 0, + 19, + 4, + 0, + 2 + ], + [ + 0, + 20, + 4, + 0, + 2 + ], + [ + 0, + 21, + 4, + 0, + -2 + ], + [ + 0, + 22, + 4, + 0, + 2 + ], + [ + 0, + 23, + 4, + 0, + 2 + ], + [ + 0, + 24, + 4, + 0, + 0 + ], + [ + 0, + 25, + 4, + 0, + 0 + ], + [ + 0, + 26, + 4, + 0, + 0 + ], + [ + 0, + 27, + 4, + 0, + -2 + ], + [ + 1, + 17, + 2, + 0, + 0 + ], + [ + 2, + 17, + 2, + 0, + 0 + ], + [ + 3, + 17, + 2, + 0, + 0 + ], + [ + 4, + 17, + 2, + 0, + 0 + ], + [ + 5, + 17, + 2, + 0, + 0 + ], + [ + 6, + 17, + 2, + 0, + 0 + ], + [ + 7, + 17, + 2, + 0, + 0 + ], + [ + 8, + 17, + 2, + 0, + 0 + ], + [ + 9, + 17, + 2, + 0, + 0 + ], + [ + 10, + 17, + 2, + 0, + 0 + ], + [ + 11, + 17, + 2, + 0, + 0 + ], + [ + 12, + 17, + 2, + 0, + 0 + ], + [ + 13, + 17, + 2, + 0, + 0 + ], + [ + 14, + 17, + 2, + 0, + 2 + ], + [ + 15, + 17, + 2, + 0, + 0 + ], + [ + 16, + 17, + 2, + 0, + 0 + ], + [ + 14, + 18, + 2, + 2, + -2 + ], + [ + 14, + 19, + 2, + 2, + -2 + ], + [ + 14, + 20, + 2, + 2, + -2 + ], + [ + 14, + 21, + 2, + 1, + 2 + ], + [ + 14, + 22, + 2, + 2, + -2 + ], + [ + 14, + 23, + 2, + 2, + -2 + ], + [ + 14, + 24, + 2, + 2, + 0 + ], + [ + 14, + 25, + 2, + 2, + 0 + ], + [ + 14, + 26, + 2, + 2, + 0 + ], + [ + 14, + 27, + 2, + 1, + 2 + ] + ], + "owned_peak": 0, + "new_recursive_jobs": 0 + }, + "gauge_certificate": { + "matrix": [ + [ + "1", + "1", + "-1", + "-1", + "-1", + "1", + "1", + "-1", + "-1", + "1", + "1", + "1", + "-1", + "-1", + "1", + "-1" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1/4", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1/4", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1/4", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1/2", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1/4", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1/4", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "-1/4", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1/4", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1/4", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1/2", + "0", + "0" + ] + ], + "source_exponents": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + -2, + 0, + 0 + ], + "target_exponents": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "program": [ + [ + "scale", + [ + "X", + 13 + ], + 1, + 4 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 0 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 1 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 2 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 3 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 4 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 5 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 6 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 7 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 8 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 9 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 10 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 11 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 12 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 13 + ], + -4, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 14 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 0 + ], + [ + "X", + 15 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 1 + ], + [ + "X", + 13 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 2 + ], + [ + "X", + 13 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 3 + ], + [ + "X", + 13 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 4 + ], + [ + "X", + 13 + ], + 2, + 1 + ], + [ + "add", + [ + "Y", + 5 + ], + [ + "X", + 13 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 6 + ], + [ + "X", + 13 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 7 + ], + [ + "X", + 13 + ], + -1, + 1 + ], + [ + "add", + [ + "Y", + 8 + ], + [ + "X", + 13 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 9 + ], + [ + "X", + 13 + ], + 1, + 1 + ], + [ + "add", + [ + "Y", + 10 + ], + [ + "X", + 13 + ], + 2, + 1 + ], + [ + "scale", + [ + "X", + 13 + ], + 4, + 1 + ] + ], + "old": 244, + "new": 224, + "valuation_objective": 16, + "constant": 208, + "circulation_cost": -16, + "cycle_steps": 5, + "dual_flows": [ + [ + 0, + 1, + 4, + 0, + 0 + ], + [ + 0, + 2, + 4, + 0, + 0 + ], + [ + 0, + 3, + 4, + 0, + 0 + ], + [ + 0, + 4, + 4, + 0, + 0 + ], + [ + 0, + 5, + 4, + 0, + 0 + ], + [ + 0, + 6, + 4, + 0, + 0 + ], + [ + 0, + 7, + 4, + 0, + 0 + ], + [ + 0, + 8, + 4, + 0, + 0 + ], + [ + 0, + 9, + 4, + 0, + 0 + ], + [ + 0, + 10, + 4, + 0, + 0 + ], + [ + 0, + 11, + 4, + 0, + 0 + ], + [ + 0, + 12, + 4, + 0, + 0 + ], + [ + 0, + 13, + 4, + 0, + 0 + ], + [ + 0, + 14, + 4, + 0, + -4 + ], + [ + 0, + 15, + 4, + 0, + 0 + ], + [ + 0, + 16, + 4, + 0, + 0 + ], + [ + 0, + 17, + 4, + 0, + -2 + ], + [ + 0, + 18, + 4, + 0, + 2 + ], + [ + 0, + 19, + 4, + 0, + 2 + ], + [ + 0, + 20, + 4, + 0, + 2 + ], + [ + 0, + 21, + 4, + 0, + -2 + ], + [ + 0, + 22, + 4, + 0, + 2 + ], + [ + 0, + 23, + 4, + 0, + 2 + ], + [ + 0, + 24, + 4, + 0, + 0 + ], + [ + 0, + 25, + 4, + 0, + 0 + ], + [ + 0, + 26, + 4, + 0, + 0 + ], + [ + 0, + 27, + 4, + 0, + -2 + ], + [ + 1, + 17, + 2, + 0, + 0 + ], + [ + 2, + 17, + 2, + 0, + 0 + ], + [ + 3, + 17, + 2, + 0, + 0 + ], + [ + 4, + 17, + 2, + 0, + 0 + ], + [ + 5, + 17, + 2, + 0, + 0 + ], + [ + 6, + 17, + 2, + 0, + 0 + ], + [ + 7, + 17, + 2, + 0, + 0 + ], + [ + 8, + 17, + 2, + 0, + 0 + ], + [ + 9, + 17, + 2, + 0, + 0 + ], + [ + 10, + 17, + 2, + 0, + 0 + ], + [ + 11, + 17, + 2, + 0, + 0 + ], + [ + 12, + 17, + 2, + 0, + 0 + ], + [ + 13, + 17, + 2, + 0, + 0 + ], + [ + 14, + 17, + 2, + 0, + 2 + ], + [ + 15, + 17, + 2, + 0, + 0 + ], + [ + 16, + 17, + 2, + 0, + 0 + ], + [ + 14, + 18, + 2, + 2, + -2 + ], + [ + 14, + 19, + 2, + 2, + -2 + ], + [ + 14, + 20, + 2, + 2, + -2 + ], + [ + 14, + 21, + 2, + 1, + 2 + ], + [ + 14, + 22, + 2, + 2, + -2 + ], + [ + 14, + 23, + 2, + 2, + -2 + ], + [ + 14, + 24, + 2, + 2, + 0 + ], + [ + 14, + 25, + 2, + 2, + 0 + ], + [ + 14, + 26, + 2, + 2, + 0 + ], + [ + 14, + 27, + 2, + 1, + 2 + ] + ], + "owned_peak": 0, + "new_recursive_jobs": 0 + } + } + ] + } + ], + "symbolic_columns_both_orientations": 160, + "random_rank_one_matrices": 100, + "random_borrowed_programs": 339, + "new_borrowed_source_programs": 4, + "original_allowance_per_orientation": 766, + "previous_zero_scratch_allowance": 686, + "previous_one_scratch_allowance": 674, + "new_zero_scratch_allowance": 666, + "additional_owned_fields": 0, + "new_recursive_calls": 0, + "productive_temporary_credit": 0, + "new_kappa": false +} diff --git a/research/borrowed-rankone/SOURCES.json b/research/borrowed-rankone/SOURCES.json new file mode 100644 index 0000000000..1d06375c9e --- /dev/null +++ b/research/borrowed-rankone/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/borrowed-rankone/TASK.json b/research/borrowed-rankone/TASK.json new file mode 100644 index 0000000000..231887d636 --- /dev/null +++ b/research/borrowed-rankone/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": "Borrowed persistent-field rank-one source/target conjugation with exact native pricing and four-window zero-extra-field specialization.", + "scope_change_reason": "Scoped continuation of #4499: replace an owned temporary by a restored persistent input or dirty output; not a complete supplier or frontier update.", + "bottleneck_link": "Changes local helper requirement from one additional owned field to zero while reducing the same four scalar-window bills. No recursive paid profile or kappa claim.", + "budget_minutes": 20, + "stop_rule": "Finish within 20 minutes after exact source-bound replay and release preflight; do not expand scalar-only results into a kappa campaign.", + "outcome": "partial", + "evidence": "RESULT.json: 666 per orientation, zero additional fields, 160 symbolic columns and 339 random borrowed programs. PROOF.md gives universal sufficient constructions and strict cost-saving condition.", + "author": "Dugongue", + "ai_assistance": "Substantial OpenAI assistance in mathematics, code and verification; exact standard-library arithmetic; no Lean.", + "open_questions": [ + { + "question": "Does the exact zero-extra-field replacement pass the complete native rebuild and norm/coefficient replay?", + "why_it_matters": "Required before global multiplication or kappa use.", + "first_step": "Install only the four pinned windows, preserving all queries and charts, then replay full invariants.", + "blocked_by": "Not run in this short local session." + } + ] +} diff --git a/research/borrowed-rankone/VALIDATION.md b/research/borrowed-rankone/VALIDATION.md new file mode 100644 index 0000000000..1f428928fc --- /dev/null +++ b/research/borrowed-rankone/VALIDATION.md @@ -0,0 +1,7 @@ +# Validation + +CPython 3.12 on Windows; Python standard library only. `python3 -I -O -B research/borrowed-rankone/verify.py` authenticates the two source inputs, derives four real scalar windows and both orientations, checks 160 independent symbolic local columns including arbitrary dirty entry and exterior, and checks all emitted instructions with the retained source scalar pricing function. Every selected instruction must be ADD or legal SCALE using only original X/Y roles; there is no scratch, CLEAR, COPY or recursive opcode. + +The four selected source programs contain two nontrivial borrowed-input adapters and two transpose-dual borrowed-target adapters. The verifier rejects missing input uncomputation, omitted dirty-target subtraction, false rank-one decompositions, illegal odd-denominator normalization, non-dyadic input and shifted source selectors. It also checks 339 borrowed programs from 100 deterministic small rank-one matrices, exercising all legal pivot candidates with exact endpoint and price checks. Exact feasible flow certificates are rechecked for the inherited gauge fallback on every actual source block. + +Registered replay, committed-byte transport checks, Git-free export replay and publisher preflight are performed for the release. No Linux execution is available; portability follows standard-library implementation choices but is not an observed Linux test. No global rewritten multiplication, norm/precision or κ audit is claimed. The optional source-history traversal is not used in the shallow checkout; explicit source pins and committed bytes are checked directly. diff --git a/research/borrowed-rankone/VERIFY.json b/research/borrowed-rankone/VERIFY.json new file mode 100644 index 0000000000..2f41d7b290 --- /dev/null +++ b/research/borrowed-rankone/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": "Exact borrowed-input restoration and dirty-target cancellation, authenticated real source windows, complete native scalar prices, structural zero-scratch check, 339 random pivot programs and malformed controls." + } + ] +} diff --git a/research/borrowed-rankone/compiler.py b/research/borrowed-rankone/compiler.py new file mode 100644 index 0000000000..5bd3944499 --- /dev/null +++ b/research/borrowed-rankone/compiler.py @@ -0,0 +1,130 @@ +"""Exact native power-of-two gauges. Apache-2.0; Dugongue, OpenAI assistance.""" +"""Exact integer min-cost circulation for zero-scratch dyadic unit gauges. +Apache-2.0; Dugongue with substantial OpenAI assistance. +""" +from fractions import Fraction as Q + +def need(ok,msg): + if not ok:raise ValueError(msg) + +def valuation(q): + q=Q(q);need(q!=0 and q.denominator&(q.denominator-1)==0,'Nonzero dyadic coefficient') + n=abs(q.numerator);return (n&-n).bit_length()-1-(q.denominator.bit_length()-1) + +def add_cost(q): + q=Q(q) + if not q:return 0 + n,d=abs(q.numerator),q.denominator;need(d&(d-1)==0,'Dyadic scalar') + return 2*(3+n.bit_length()-1+n.bit_count()+d.bit_length()-1) + +def power(e):return Q(2**e)if e>=0 else Q(1,2**(-e)) + +def optimize(matrix): + M=[[Q(x)for x in row]for row in matrix];need(M and M[0]and all(len(r)==len(M[0])for r in M),'Rectangular nonempty matrix') + m,n=len(M),len(M[0]);N=1+n+m;g=[[]for _ in range(N)];terms=[] + def edge(u,v,c,k): + a=len(g[u]);b=len(g[v]);g[u].append([v,b,c,k]);g[v].append([u,a,c,-k]);terms.append((u,a,c,k)) + for i in range(n+m):edge(0,1+i,4,0) + for j in range(m): + for i in range(n): + if M[j][i]:edge(1+i,1+n+j,2,-valuation(M[j][i])) + total=0;steps=0 + while True: + dist=[0]*N;pred=[None]*N;x=None + for _ in range(N): + x=None + for u in range(N): + for k,e in enumerate(g[u]): + v,rev,cap,cost=e + if cap and dist[v]>dist[u]+cost:dist[v]=dist[u]+cost;pred[v]=(u,k);x=v + if x is None:break + if x is None:break + for _ in range(N):x=pred[x][0] + cycle=[];v=x + while True: + u,k=pred[v];cycle.append((u,k));v=u + if v==x:break + delta=min(g[u][k][2]for u,k in cycle);cycle_cost=sum(g[u][k][3]for u,k in cycle) + need(delta>0 and cycle_cost<0,'Negative augmenting cycle') + for u,k in cycle: + v,rev,cap,cost=g[u][k];g[u][k][2]-=delta;g[v][rev][2]+=delta + total+=delta*cycle_cost;steps+=1 + p=[x-dist[0]for x in dist];a=p[1:n+1];b=p[n+1:] + offset=sum(add_cost(x)-2*abs(valuation(x))for row in M for x in row if x) + primal=4*sum(abs(x)for x in a+b)+2*sum(abs(valuation(x)+b[j]-a[i])for j,row in enumerate(M)for i,x in enumerate(row)if x) + need(primal==-total,'Exact circulation duality') + program=[] + for kind,exps in [('X',a),('Y',b)]: + for i,e in enumerate(exps): + if e:program.append(['scale',[kind,i],power(e).numerator,power(e).denominator]) + for j,row in enumerate(M): + for i,q in enumerate(row): + if q: + q*=power(b[j]-a[i]);program.append(['add',['Y',j],['X',i],q.numerator,q.denominator]) + for kind,exps in [('X',a),('Y',b)]: + for i,e in enumerate(exps): + if e:program.append(['scale',[kind,i],power(-e).numerator,power(-e).denominator]) + return {'matrix':M,'source_exponents':a,'target_exponents':b,'program':program,'old':sum(add_cost(x)for row in M for x in row),'new':offset+primal,'valuation_objective':primal,'constant':offset,'circulation_cost':total,'cycle_steps':steps,'dual_flows':[[u,g[u][k][0],c,kcost,c-g[u][k][2]]for u,k,c,kcost in terms],'owned_peak':0,'new_recursive_jobs':0} + +def rank_one(M): + M=[[Q(x) for x in row] for row in M];m,n=len(M),len(M[0]) + pivot=next(((j,i) for j in range(m) for i in range(n) if M[j][i]),None) + if pivot is None:return None + j0,i0=pivot;u=[row[i0] for row in M];v=[x/M[j0][i0] for x in M[j0]] + if any(q.denominator&(q.denominator-1) for q in u+v):return None + if any(M[j][i]!=u[j]*v[i] for j in range(m) for i in range(n)):return None + program=[['clear',['T',0]]] + for i,q in enumerate(v): + if q:program.append(['add',['T',0],['X',i],q.numerator,q.denominator]) + for j,q in enumerate(u): + if q:program.append(['add',['Y',j],['T',0],q.numerator,q.denominator]) + program.append(['clear',['T',0]]) + return {'program':program,'new':4+sum(add_cost(q) for q in u+v),'owned_peak':1,'mechanism':'rank-one predecessor macro'} +def encode(x): + if isinstance(x,Q):return str(x) + if isinstance(x,dict):return {k:encode(v) for k,v in x.items()} + if isinstance(x,(tuple,list)):return [encode(v) for v in x] + return x + + +def borrowed_candidates(matrix): + """Legal rank-one conjugations, restoring every borrowed persistent field. + No division by runtime data; all divisions below are coefficient arithmetic. + """ + M=[[Q(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),'Rectangular nonempty matrix') + m,n=len(M),len(M[0]) + for row in M: + for q in row: + if q:valuation(q) + out=[] + def add(dst,src,q):return ['add',dst,src,q.numerator,q.denominator] + def record(kind,pivot,prep,middle,undo): + program=prep+middle+undo + out.append({'mechanism':kind,'pivot':pivot,'preparation_count':len(prep),'program':program,'new':sum(add_cost(Q(e[3],e[4])) for e in program),'owned_peak':0,'new_recursive_jobs':0}) + for i in range(n): + j0=next((j for j in range(m) if M[j][i]),None) + if j0 is None:continue + u=[row[i] for row in M];v=[q/M[j0][i] for q in M[j0]] + if any(q.denominator&(q.denominator-1) for q in v):continue + if any(M[j][k]!=u[j]*v[k] for j in range(m) for k in range(n)):continue + prep=[add(['X',i],['X',k],q) for k,q in enumerate(v) if k!=i and q] + middle=[add(['Y',j],['X',i],q) for j,q in enumerate(u) if q] + undo=[add(e[1],e[2],-Q(e[3],e[4])) for e in reversed(prep)] + record('borrow-source',i,prep,middle,undo) + for j in range(m): + i0=next((i for i in range(n) if M[j][i]),None) + if i0 is None:continue + v=M[j];u=[row[i0]/M[j][i0] for row in M] + if any(q.denominator&(q.denominator-1) for q in u):continue + if any(M[k][i]!=u[k]*v[i] for k in range(m) for i in range(n)):continue + prep=[add(['Y',k],['Y',j],-q) for k,q in enumerate(u) if k!=j and q] + middle=[add(['Y',j],['X',i],q) for i,q in enumerate(v) if q] + undo=[add(e[1],e[2],-Q(e[3],e[4])) for e in reversed(prep)] + record('borrow-target',j,prep,middle,undo) + return out + +def compile_borrowed(matrix): + gauge=optimize(matrix) + candidates=[gauge]+borrowed_candidates(matrix) + return min(candidates,key=lambda x:x['new']) diff --git a/research/borrowed-rankone/verify.py b/research/borrowed-rankone/verify.py new file mode 100644 index 0000000000..68e7ed40cf --- /dev/null +++ b/research/borrowed-rankone/verify.py @@ -0,0 +1,193 @@ +"""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('borrowed_rankone_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 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') + elif e[0]=='scale': + a=tuple(e[1]);q=Q(e[2],e[3]);need(a in rows and a[0] in ('X','Y') and q>0 and q==B.power(B.valuation(q)),'Legal native SCALE') + rows[a]=[q*x for x in rows[a]] + 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=Q(e[3],e[4]);B.valuation(q);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 certificate(M,r): + m,n=len(M),len(M[0]);p=[0]+r['source_exponents']+r['target_exponents'] + edges=[(0,i,4,0) for i in range(1,1+n+m)] + edges += [(1+i,1+n+j,2,-B.valuation(q)) for j,row in enumerate(M) for i,q in enumerate(row) if q] + flows=r['dual_flows'];need(len(edges)==len(flows),'Certificate size') + bal=[0]*len(p);dual=primal=0 + for edge,row in zip(edges,flows): + need(list(edge)==row[:4],'Authenticated dual edge');u,v,c,k=edge;f=row[4] + need(type(f)==int and -c<=f<=c,'Capacity');bal[u]-=f;bal[v]+=f + dual-=k*f;primal+=c*abs(p[v]-p[u]-k) + need(not any(bal) and primal==dual==r['valuation_objective'],'Exact feasible primal-dual equality') + offset=sum(B.add_cost(q)-2*abs(B.valuation(q)) for row in M for q in row if q) + need(offset==r['constant'] and offset+primal==r['new'],'Complete scalar objective') + +def check_no_scratch(program): + for e in program: + need(e[0] in ('add','scale'),'No clear, copy or recursive opcode') + roles=e[1:3] if e[0]=='add' else e[1:2] + need(all(r[0] in ('X','Y') for r in roles),'Only original persistent fields') + +def verify(): + inputs=authenticated_sources();words=json.loads(gzip.decompress(next(v for k,v in inputs.items() if k.endswith('-NATIVE.json.gz')))) + price=source_pricer(next(v for k,v in inputs.items() if k.endswith('/rebuild_native.py'))) + results=[];columns=0;intervals=[];new_programs=0 + for case in read('CASES.json'): + entry={'ordinals':[case['first_ordinal'],case['last_ordinal']],'phase':case['phase'],'orientations':[]} + for backward in (False,True): + M,window,indices=source_matrix(words,case,backward);gauge=B.optimize(M);certificate(M,gauge) + borrowed=B.borrowed_candidates(M);plan=min([gauge]+borrowed,key=lambda x:x['new']) + one=B.rank_one(M);previous=min([gauge]+([one] if one else []),key=lambda x:x['new']) + old=sum(price(e[1]) for e in window);need(old==case['old'],'Original source bill') + need(plan_price(plan['program'],price)==plan['new'],'Complete emitted scalar bill') + need(plan['owned_peak']==0 and plan['new']<=previous['new'],'No extra field or allowance regression on source cases') + check_no_scratch(plan['program']);columns+=check_semantics(M,plan['program'],False) + if plan.get('mechanism','').startswith('borrow-'): + new_programs+=1 + need(plan['preparation_count']>0,'Nontrivial borrowed adapter') + if plan['mechanism']=='borrow-source': + rejects(lambda:check_semantics(M,plan['program'][:-1],False),'omit borrowed-input restoration') + else: + rejects(lambda:check_semantics(M,plan['program'][1:],False),'omit dirty-target subtraction') + entry['orientations'].append({'backward':backward,'source_indices':indices,'matrix':M,'old':old,'previous_one_field_allowance':previous['new'],'previous_zero_field_allowance':gauge['new'],'selected':plan,'gauge_certificate':gauge}) + if not backward: + for lo,hi in intervals:need(indices[1]