diff --git a/research/chain-root-global-ceiling/LICENSE b/research/chain-root-global-ceiling/LICENSE new file mode 100644 index 0000000000..261eeb9e9f --- /dev/null +++ b/research/chain-root-global-ceiling/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/chain-root-global-ceiling/ORIGINS.json b/research/chain-root-global-ceiling/ORIGINS.json new file mode 100644 index 0000000000..ae4d6de658 --- /dev/null +++ b/research/chain-root-global-ceiling/ORIGINS.json @@ -0,0 +1,68 @@ +{ + "schema_version": 1, + "files": [ + { + "local_path": "retained/RESULT.json", + "repository": "DreamingOfClouds/integer-mult-bounds", + "pr": "CrocSwap/integer-mult-bounds#6833", + "head": "ad24ad966b857dbfed50d9121624db84b2eccc92", + "path": "research/p104-chain-nested-root/RESULT.json", + "git_blob": "2e9c2183e8939d12762d751c89abac41daa0fa2d", + "sha256": "da448ecb925b2c7c7f23167ae6ab082d482dc38ccf7a59cc462338094d0e1eaa" + }, + { + "local_path": "retained/CALLER.json", + "repository": "DreamingOfClouds/integer-mult-bounds", + "pr": "CrocSwap/integer-mult-bounds#6833", + "head": "ad24ad966b857dbfed50d9121624db84b2eccc92", + "path": "research/p104-chain-nested-root/CALLER.json", + "git_blob": "ac49576bf71ceb43a1052361b6ba7c148c1e7421", + "sha256": "9a46d79125ea0bfab7112b46c4f907b00364c3ff3c47d2b3d078ea490e7ef4f6" + }, + { + "local_path": "retained/PROOF.md", + "repository": "DreamingOfClouds/integer-mult-bounds", + "pr": "CrocSwap/integer-mult-bounds#6833", + "head": "ad24ad966b857dbfed50d9121624db84b2eccc92", + "path": "research/p104-chain-nested-root/PROOF.md", + "git_blob": "d0bfd74266b48fe47e630cef28853c3c444cd433", + "sha256": "ef26968138b7b9dfeebc9beea9d81b4026bd493df0223011ae6967ea5e5e1910" + }, + { + "local_path": "retained/README.md", + "repository": "DreamingOfClouds/integer-mult-bounds", + "pr": "CrocSwap/integer-mult-bounds#6833", + "head": "ad24ad966b857dbfed50d9121624db84b2eccc92", + "path": "research/p104-chain-nested-root/README.md", + "git_blob": "a2c71f0e6c13374d320613657e055bc4bcd6b4ee", + "sha256": "bddcca5d1e70601b3173ff95bd1142cb26bc8cb24e8d3785bc5b91e34be39fa9" + }, + { + "local_path": "retained/NOTICE", + "repository": "DreamingOfClouds/integer-mult-bounds", + "pr": "CrocSwap/integer-mult-bounds#6833", + "head": "ad24ad966b857dbfed50d9121624db84b2eccc92", + "path": "research/p104-chain-nested-root/NOTICE", + "git_blob": "d03cab1fcb0e91731a5b82b072496997ccb986da", + "sha256": "039f5005bbe42d76d27a8a4318ac1ae6777afe1cd4417519ea23337994fc137e" + }, + { + "local_path": "retained/RESEARCH-NOTES.md", + "repository": "DreamingOfClouds/integer-mult-bounds", + "pr": "CrocSwap/integer-mult-bounds#6833", + "head": "ad24ad966b857dbfed50d9121624db84b2eccc92", + "path": "research/p104-chain-nested-root/RESEARCH-NOTES.md", + "git_blob": "933152d3fdc7fe4490ecf0375d6e3ef8db8e4b79", + "sha256": "73cfa9e06643862b46da55191cc8909b588251c8e016fa6d708644ecf0395c5f" + }, + { + "local_path": "retained/chain_root.py", + "repository": "DreamingOfClouds/integer-mult-bounds", + "pr": "CrocSwap/integer-mult-bounds#6833", + "head": "ad24ad966b857dbfed50d9121624db84b2eccc92", + "path": "research/p104-chain-nested-root/chain_root.py", + "git_blob": "ca1e0244f1329c153c1224b05bf0c0c5d5e2367b", + "sha256": "6f4046c804f27071d88ce05820c75baebe9cbf32533c4ba89285c413bfc8edaa" + } + ] +} diff --git a/research/chain-root-global-ceiling/PROOF.md b/research/chain-root-global-ceiling/PROOF.md new file mode 100644 index 0000000000..5fbb13abf7 --- /dev/null +++ b/research/chain-root-global-ceiling/PROOF.md @@ -0,0 +1,297 @@ +# A global ceiling for the declared two-chain invoice + +Prepared for @CubeJerry with substantial OpenAI assistance. Apache-2.0. +The caller, native profile and chain idea are due to DreamingOfClouds in +CrocSwap/integer-mult-bounds#6833, frozen at +`ad24ad966b857dbfed50d9121624db84b2eccc92`. This proof adds an infinite-family +optimization result; it does not reprove that predecessor's supplier contract. + +## 1. Exact statement and applicability + +Let each of two chains have a positive integer length, denoted by `l` and `r`, +and write `M=l+r`. Freeze the 104-port native profile in the retained source. +Its signed helper-minus-paid multiplicities, in ranks 1 through 9, are + +\[ +d=(-2220,-446,-485,-1,-135,-4,1,39,359). +\] + +The **declared family** charges `M` copies of this native profile, 104 copies of +one target of rank `8M+1`, 104 targets of rank `8j+1` for every `1<=j<=l` and +every `1<=j<=r`, and 104 paid jobs of rank `8j` for every `1<=j=0.0033718004755` with `C<1`, the signed moment is +strictly negative. For totals at least 3 the crossing is unique. Total 2 has +no positive favorable interval. These are statements about the frozen signed +invoice, not a new admitted multiplication exponent. + +## 2. Complete moment and balancing + +Put `t=1-C`, so `0=1`, + +\[ +A_{g+1}(t)-A_g(t)=(8g+9)^t-(8g)^t. +\] + +This difference is strictly decreasing in `g`: for any positive width `h`, +the function `(x+h)^t-x^t` has strictly negative derivative in `x` when +`0=r+2`, replacing `(l,r)` by `(l-1,r+1)` therefore strictly +increases (1). For a fixed total `M`, the largest invoice is attained precisely +by the balanced pair, up to interchange. Write its margin as + +\[ +B_M(t)=F_{\lfloor M/2\rfloor,\lceil M/2\rceil}(t),\qquad M\ge2. +\] + +## 3. Strict discrete concavity in the total + +Direct subtraction, including the new native copy, gives + +\[ +B_{M+1}(t)-B_M(t)=D(t)+104\left[ +(8M+9)^t-(8M+1)^t ++(8\lfloor M/2\rfloor+9)^t-(8\lfloor M/2\rfloor)^t +\right]. \tag{2} +\] + +The first bracketed difference is strictly decreasing in `M`. The second is +nonincreasing, repeating at most once because of the floor. Thus (2) is strictly +decreasing for every `00.3232560777>0, +\qquad B_{19}-B_{18}<-0.1714023579<0. +\] + +Hence `B18` uniquely maximizes the balanced family throughout that interval. +Balancing then makes `(9,9)` the unique maximizing pair there. At the two exact +rational endpoints its margins have the directed enclosures + +| Saving C | Enclosure of F(9,9; 1-C) | +|---|---| +| 0.0033718004754 | [0.000000021652415920367122, 0.000000021652415920367123] | +| 0.0033718004755 | [-0.000000000734152088876529, -0.000000000734152088876528] | + +Continuity gives a root between them. The next section rules out a later +favorable interval, for this or any other pair, and proves uniqueness. + +## 4. Monotonic normalization excludes later crossings + +It is not sufficient merely to exhibit a negative margin at one value of `C`: +a general signed moment could change sign again. Here every `F/9^t` is strictly +increasing in `t` on `00. \tag{3} +\] + +The first inequality uses `9^(-t)>=1/9`, `(7/9)^t<=1`, `(8/9)^t<=1`; +the rank-nine term is constant. The second uses `log x>=1-1/x` and +`log x<=x-1` for `x>0`. Thus (3) is a rational certificate, with no numerical +logarithm premise. + +For the remaining terms rewrite + +\[ +A_g(t)=(8g+1)^t+\sum_{j=1}^{g-1}\big((8j+1)^t-(8j)^t\big). +\] + +After division by `9^t`, the terminal term is `( (8g+1)/9 )^t`, nondecreasing. +The `j=1` summand, when present, is `1-(8/9)^t`, strictly increasing. For +`j>=2`, both bases are at least one; the derivative of `a^t-b^t` for +`a>b>=1` is positive because `x^t log x` strictly increases in `x>=1`. +The normalized root term is increasing, and `-2/9^t` is increasing. Combining +these observations with (3) proves strict monotonicity of `F/9^t`. + +Consequently, every invoice negative at the upper endpoint stays negative as +`C` increases. At the crossing `C*` of `(9,9)`, Sections 2 and 3 make every +other pair strictly negative; monotonicity places any other crossing strictly +below `C*`. Finally, + +\[ +F_{l,r}(0)=104-2892M<0,\qquad F_{l,r}(1)=48M-104. +\] + +Thus a unique crossing exists for `M>=3`; for `M=2` both the monotonicity and +the negative endpoint exclude a favorable interval. This completes the proof. + +## 5. Exact arithmetic and scope of computational evidence + +The new interval implementation uses integer endpoints scaled by `2^192`. +Each arithmetic operation rounds outward. For a positive integer `n`, reduction +`n=2^k u`, `1<=u<2`, expresses its logarithm using `log 2` and +`2 atanh((u-1)/(u+1))`, whose argument lies in `[0,1/3]`. The first 80 terms +are enclosed with a positive tail at most +`9/[4(161)3^161]`. Exponentials are scaled to arguments at most `1/2`, summed +through degree 40, and supplied with the geometric upper bound on the remaining +positive terms before outward repeated squaring. Finally +`n^(1-C)=n/exp(C log n)`. No floating-point sign is trusted. + +The verifier recounts the literal caller bill, checks both root signs and +the uniform adjacent-increment signs, and checks the rational derivative bound. +Its 961-pair grid (`1<=l,r<=31`, deterministic, exhaust the grid) only +corroborates the formula: the infinite conclusion comes from Sections 2–4. +Algebraic square-root and integer-power controls test the interval mechanism. +Negative controls reject omitted queries, omitted or undercharged idle jobs, +lost target axes, incorrect target exponents, altered native bills, false +maximizers, the favorable lower endpoint as a ceiling, malformed lengths, and +each altered retained source file. The checks do not replace a formal proof +assistant or a full supplier replay. + +Changed native profiles, additional coupling fields, different target supports, +different merged-idle lifetimes and different caller topologies are outside +this theorem. Compiler admissibility of the predecessor's merged jobs remains +an inherited obligation, even if investigated independently elsewhere. The five +framework assumptions (`native_all_columns`, `owned_erasure`, `compiler`, +`precision_tape`, `analytic_recovery`) remain outside this invoice theorem. +The selected frontier is unchanged. **No new κ.** + +## 6. Extension to arbitrary binary children and ordered partitions + +The preceding theorem used one native call per chain site. The source also +permits a chain site to contain a binary child tree; its `(4,4,1|1,4,4)` gate +uses this option. The following extension rules out an improvement by **any** +ordered partition into binary children, even allowing arbitrary full binary +tree shapes instead of the source constructor's balanced children. + +The relevant source is retained `chain_root.py`, function `outer_formula`. +An internal binary node with `m>=2` native leaves adds two targets of rank +`8m+1`, two paid jobs of rank `8m`, and one rank-one thin query. With + +\[ +\delta_j(t)=(8j+1)^t-(8j)^t, +\] + +its per-port signed contribution is `2 delta_m-1`. The source node rule and +complete outer bill are inherited; no claim is made that arbitrary new tree +shapes have been operator-replayed. Allowing all their declared invoices is a +relaxation sufficient for an upper bound. The checker also reproduces the +source's gate crossing `(0.00330823456614,0.00330823456615)` from its own tree +invoice implementation. + +Consider a side containing `L` native leaves, partitioned into `g` chain children. +Up to reversing the left partition, its chain contribution is the terminal +`(8L+1)^t` plus `delta_j` at each of the `g-1` internal partition boundaries. +There are `L-g` missing boundaries relative to the all-one partition. A forest +of full binary trees on those children has exactly `L-g` internal nodes. + +Since `delta_j` decreases strictly with `j`, each internal node contributes at +most + +\[ +c(t)=2\delta_2(t)-1. +\] + +Consequently every side bill is bounded above by + +\[ +U_L(t)=(8L+1)^t+\sum_{j=1}^{L-1}\max\{\delta_j(t),c(t)\}. \tag{4} +\] + +Indeed, each retained boundary contributes its `delta_j`; each missing boundary +can be assigned one of the equally many node contributions, each at most `c`. +Taking the larger alternative at each boundary can only increase the bill. +This is an envelope, and need not be simultaneously attained by a forest. + +Its increments satisfy + +\[ +U_{L+1}-U_L=(8L+9)^t-(8L+1)^t+\max\{\delta_L,c\}. \tag{5} +\] + +The width-eight difference decreases strictly and the maximum decreases weakly +in `L`; hence (5) is strictly decreasing. Balancing and total-length concavity +therefore apply to the envelope + +\[ +\mathcal B_M=M D(t)+104\big((8M+1)^t+ +U_{\lfloor M/2\rfloor}+U_{\lceil M/2\rceil}-2\big). +\] + +The new exact interval check proves `delta_9-c>0.00783179` throughout the +same raw-root bracket. All earlier `delta_j` exceed `c` too. It follows that +`U9=A9`, and that the envelope's increments from total 17 to 18 and 18 to 19 +are exactly the increments in Section 3. Thus its unique maximum is still +`(9,9)`, and its value there is exactly the ungrouped bill. A nontrivial grouping +at `(9,9)` loses strictly, because its omitted boundaries have `j<=8` and +`delta_j>c`. + +Finally, the actual grouped invoices retain the monotonic-normalization +argument. Every added binary term divided by `9^t` is + +\[ +2\left[\left(\frac{8m+1}{9}\right)^t- +\left(\frac{8m}{9}\right)^t\right]-9^{-t},\qquad m\ge2, +\] + +which strictly increases in `t`. Each retained chain boundary and endpoint +has the same property established in Section 4. If `I` is the number of +binary internal nodes, the endpoint identities become + +\[ +F_{\rm grouped}(0)=104-2892M-104I<0, +\qquad F_{\rm grouped}(1)=48M-104. +\] + +**Corollary.** Over all positive side lengths, all ordered partitions and all +full binary child-tree invoices with the source accounting rule, the unique +maximum raw crossing is the all-one `(9,9)` member. It has the same bracket as +in Section 1, and no member has a favorable margin above the upper endpoint. +This does not cover a changed root topology, changed native profile, altered +internal-node interface or different idle-sharing rule. + +The checker corroborates the accounting on every ordered pair of full binary +forests with total native leaves 2 through 7, and verifies both endpoint +identities. That finite domain is exhausted deterministically. The infinite +conclusion is (4)–(5), not a search extrapolation. A semantic control removes the +internal thin-query charge and correctly fails the envelope certificate; that +charge is essential and cannot be optimized away by assertion. diff --git a/research/chain-root-global-ceiling/README.md b/research/chain-root-global-ceiling/README.md new file mode 100644 index 0000000000..c696ce815b --- /dev/null +++ b/research/chain-root-global-ceiling/README.md @@ -0,0 +1,127 @@ +# Global ceiling for the two-chain invoice + +**No new κ.** For the frozen 104-port native profile and complete two-chain +invoice defined in `PROOF.md`, the unique best positive-integer length pair is +`(9,9)`. Its raw crossing lies strictly between `0.0033718004754` and +`0.0033718004755`. Concavity and a monotonic normalization prove the result over +all lengths; a finite search is not the impossibility argument. + +The pending construction in CrocSwap/integer-mult-bounds#6833 expressly leaves +global optimality open. This package independently recounts its literal caller +and proves that changing the two lengths, ordered child partitions or full binary child trees cannot improve the declared bill. +This identifies which restriction a further complex-supplier improvement must +change. It does not establish compiler admission, replace the selected result, +or rule out different roots, native circuits or idle lifetimes. + +### Concurrent work and the remaining distinction + +A publication checkpoint located the concurrently opened +CrocSwap/integer-mult-bounds#6836 by DreamingOfClouds, exact head +`99b18108eda17764d55301aae12948b547b17635`. Its +`research/p104-chain-idle-cover-optimal/PROOF.md`, Proposition 4, independently +checks the same maximizing shape at 18 native stages over all ordered +compositions with optimized binary children, and reports a scaled-native +dynamic program for totals 10 through 40. It also gives separate idle-cover, +top-target and retirement results. Those contributions are credited and are +not claimed here. + +The distinct result here is the analytic ceiling over **every positive total +length**, every ordered child partition and every full binary child-tree +invoice, with a proof excluding later favorable saving intervals. The fixed +18-stage optimum is independently corroborated by #6836 rather than claimed +as an exclusive discovery. The present verifier was developed independently +and imports neither that package nor its pricing implementation. The +concurrent proof was read at the checkpoint; no unmerged result from it is a +dependency of this package. + +## Exact sources and scope + +- Canonical base: `7c49fe32c55de02c2c873655c804b16e4c3fef0a`. +- Construction: DreamingOfClouds, CrocSwap/integer-mult-bounds#6833, + `ad24ad966b857dbfed50d9121624db84b2eccc92`, + `research/p104-chain-nested-root/`. +- Seven required source files are retained byte for byte with their notice; + `ORIGINS.json` records paths, Git blob IDs and SHA256 digests. No network, + unmerged Git object or predecessor Python module is required to run the + standalone verifier. +- `SOURCES.json` binds the original task card and selected record as provenance. + The native helper/paid profile is an authenticated inherited input, not a new + operator replay. The `(9,9)` complete bill is recounted from `CALLER.json`. + +The all-positive-length invoice family is deliberately broader than the +source-proved odd/odd construction. Its all-parity extension only strengthens +the upper bound; realizability of every even or mixed-parity bill is not claimed. +Applicability requires exactly the declared native, productive-target and paid +profiles. The five inherited framework assumptions remain outside this result: +`native_all_columns`, `owned_erasure`, `compiler`, `precision_tape`, +`analytic_recovery`. + +## Result and proof mechanism + +For a fixed total length, strict concavity balances the two sides. The balanced +margin then has strictly decreasing increments in total length. Independent +directed intervals certify a positive increment from 17 to 18 and a negative +increment from 18 to 19 throughout the raw-root bracket. A rational derivative +bound after normalization by `9^(1-C)` rules out a later favorable interval. +A concave envelope additionally bounds arbitrary ordered partitions and full +binary child trees, including all their internal thin-query costs. The unique +optimum has nine individual native calls on each side. + +The source recount returns 12,232 target fields, 64,184 paid jobs, paid rank mass +166,812 and surplus 760. The interval implementation is new and uses integer +arithmetic, explicit logarithm/exponential tails and outward rounding. It does +not import the construction, pricing engine or predecessor arithmetic. +`PROOF.md` contains the complete argument; `RESULT.json` contains deterministic +certificate endpoints and check coverage. + +## Reproduction and executed checks + +```sh +python3 -B research/chain-root-global-ceiling/verify.py +``` + +Expected first line: `PASS_CHAIN_ROOT_GLOBAL_CEILING`. The second line reports +the rational root bracket, `(9,9)`, 20 rejected negative controls and 961 finite +corroboration pairs. The same command with `-O` checks that optimized Python +does not disable rejection. Standard-library Python 3.12 is sufficient. + +The grid is exactly `1<=left,right<=31`, with no random seed; its stopping rule +is exhaustion of those 961 pairs. It corroborates the formula and is not used +to infer the infinite-domain theorem. Exact integer-power and square-root +controls independently check power enclosures. Semantic controls reject omitted +thin queries and idle jobs, an undercharged merged rank, a missing target axis, +an incorrect target exponent, an undercharged native job, false maximizing +lengths, and the favorable lower endpoint as a ceiling. Every retained source +file is separately altered and rejected. The grouped-tree extension additionally checks every ordered forest pair with +total native leaves 2 through 7, the predecessor gate crossing, and a control +that omits an internal thin-query charge. Full native operator replay and full +supplier admission were not performed. + +The registered package runner can additionally validate provenance and run both +normal and optimized commands: + +```sh +python3 -B scripts/research_package.py --package research/chain-root-global-ceiling +``` + +## Open next questions + +1. Can a changed root or multiple coupling fields improve the complete bill? + Derive the full productive and paid profile first. A concrete alternative + caller with an exact operator and physical-interface proof is still needed. +2. How does a verified new native profile move the best length? Substitute its + authenticated coefficients, then recheck the derivative and adjacent signs; + the present ceiling does not transfer automatically. + +These questions and blockers are also recorded in `TASK.json`. + +## Credit and license + +Prepared for @CubeJerry with substantial OpenAI assistance in the proof, +implementation and review. The two-chain construction, native payload and +retained source evidence are due to DreamingOfClouds in +CrocSwap/integer-mult-bounds#6833, extending the native profile of +CrocSwap/integer-mult-bounds#6824 and its credited predecessors. This package's +new contribution is the global fixed-family proof and independently implemented +source-bound certificate. Retained files are unchanged, with their original +notice. Apache-2.0. diff --git a/research/chain-root-global-ceiling/RESULT.json b/research/chain-root-global-ceiling/RESULT.json new file mode 100644 index 0000000000..7ce220d1fd --- /dev/null +++ b/research/chain-root-global-ceiling/RESULT.json @@ -0,0 +1,129 @@ +{ + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "binary_child_envelope": { + "arbitrary_tree_corroboration_cases": 804, + "delta9_minus_node_upper": [ + "0.007831795243007162652279", + "0.007831795322559906317743" + ], + "gate_crossing_bracket": [ + "0.00330823456614", + "0.00330823456615" + ], + "gate_margin_lower": [ + "0.000000000726834149080815", + "0.000000000726834149080816" + ], + "gate_margin_upper": [ + "-0.000000001555206042433269", + "-0.000000001555206042433268" + ], + "stop_rule": "all ordered pairs of full binary forests in domain", + "total_leaves": [ + 2, + 7 + ] + }, + "ceiling_certificate": { + "after": [ + "-0.171402370243713434368534", + "-0.171402370243713434368533" + ], + "before": [ + "0.323256087703523030615899", + "0.323256087703523030615900" + ], + "maximum": [ + "-0.000000000734152088876529", + "-0.000000000734152088876528" + ] + }, + "exact_power_control_ranks": [ + 1, + 2, + 3, + 4, + 8, + 9, + 16, + 17, + 64, + 73, + 81, + 137, + 145, + 153 + ], + "finite_corroboration": { + "left": [ + 1, + 31 + ], + "pairs": 961, + "right": [ + 1, + 31 + ], + "seed": null, + "stop_rule": "exhaust all declared pairs" + }, + "negative_controls": [ + "omit binary internal thin-query charge", + "favorable lower endpoint cannot certify ceiling", + "wrong maximizing total 17", + "wrong maximizing total 19", + "omit thin query", + "omit merged idle job", + "undercharge merged rank", + "omit productive target axis", + "wrong target q exponent", + "undercharge native job", + "invalid chain length 0", + "invalid chain length True", + "invalid chain length 1.5", + "source mutation retained/RESULT.json", + "source mutation retained/CALLER.json", + "source mutation retained/PROOF.md", + "source mutation retained/README.md", + "source mutation retained/NOTICE", + "source mutation retained/RESEARCH-NOTES.md", + "source mutation retained/chain_root.py" + ], + "normalized_native_derivative_rational_lower_bound": "323717/1512", + "root_bracket_increment_signs": { + "17_to_18": [ + "0.323256077745442297513321", + "0.323256099064547120187563" + ], + "18_to_19": [ + "-0.171402381114079472757090", + "-0.171402357956005498223831" + ] + }, + "root_margin_lower": [ + "0.000000021652415920367122", + "0.000000021652415920367123" + ], + "root_margin_upper": [ + "-0.000000000734152088876529", + "-0.000000000734152088876528" + ], + "saving_bracket": [ + "16859002377/5000000000000", + "6743600951/2000000000000" + ], + "scope": "Declared two-chain invoice family only; analytical proof extends beyond finite corroboration. No new kappa; no supplier admission.", + "source_counts": { + "paid_jobs": 64184, + "paid_rank_mass": 166812, + "surplus": 760, + "target_fields": 12232 + }, + "source_head": "ad24ad966b857dbfed50d9121624db84b2eccc92", + "source_pr": "CrocSwap/integer-mult-bounds#6833", + "status": "PASS_CHAIN_ROOT_GLOBAL_CEILING", + "unique_maximizing_lengths": [ + 9, + 9 + ] +} diff --git a/research/chain-root-global-ceiling/REVIEW.md b/research/chain-root-global-ceiling/REVIEW.md new file mode 100644 index 0000000000..facd0956bb --- /dev/null +++ b/research/chain-root-global-ceiling/REVIEW.md @@ -0,0 +1,33 @@ +# Independent review and verification record + +Prepared for @CubeJerry with substantial OpenAI assistance. This records a +separate research agent's review of the author's proof and implementation; +it is not a human acceptance decision or proof-kernel verification. + +The reviewer independently checked the balancing step, strict concavity in total +length, the whole-bracket adjacent-sign argument, and monotonicity after division +by `9^t`. In particular the rank-seven and rank-eight derivative charges were +included, and the rational lower bound was independently reduced to +`323717/1512`. The reviewer examined the outward logarithm and exponential tails, +reciprocal scaling, and the t=0 and t=1 endpoint identities. No issue was found. +An independent 80-digit Decimal calculation also agreed with the two root +endpoint signs; that numerical corroboration is not a certified sign premise. + +The subsequent binary-child extension received a separate algebraic review. +The reviewer checked that full binary internal nodes and omitted chain boundaries +have the same count; replacing each node contribution by `2 delta_2-1` yields +the stated concave envelope. The reviewer specifically required the envelope gap +to be certified over the whole root bracket and corrected the grouped t=0 +endpoint to `104-2892M-104I`. Both points are included in the final proof and +verifier. The author independently bound the node accounting to the retained +source and reproduced the source gate crossing without importing its code. + +Executed package checks use Python 3.12.14 and the standard library. The registered +runner passes both normal and optimized Python; all 20 semantic/source rejection +controls remain active. The all-one corroboration exhausts 961 pairs and the +binary-forest corroboration exhausts 804 ordered forest pairs. Neither finite +domain supplies the infinite quantifier in the theorem. The exact interval +certificate and the analytical argument have separate roles. + +No native operator replay, full supplier admission, selected-frontier update, +formal proof assistant, or discharge of framework assumptions is claimed. diff --git a/research/chain-root-global-ceiling/SOURCES.json b/research/chain-root-global-ceiling/SOURCES.json new file mode 100644 index 0000000000..594089b9c7 --- /dev/null +++ b/research/chain-root-global-ceiling/SOURCES.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + } + ] +} diff --git a/research/chain-root-global-ceiling/TASK.json b/research/chain-root-global-ceiling/TASK.json new file mode 100644 index 0000000000..04780e2782 --- /dev/null +++ b/research/chain-root-global-ceiling/TASK.json @@ -0,0 +1,105 @@ +{ + "schema_version": 1, + "task_id": "independent-moment", + "priority_revision": 8, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "original_card": { + "id": "independent-moment", + "question": "Does a changed construction's serialized target/paid invoice independently support its claimed improvement?", + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "docs/research/recursive-invoice-preflight.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "acceptance_gate": "Demonstrate independence, source binding, positive cases and semantic failure controls. Name the existing checks and the missing coverage. More digits or another equivalent evaluation of an unchanged root is not by itself new verification coverage.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "Independently recount one changed emitted word and its complete caller, importing no constructor or pricing engine. Include target losses, owned lifetimes, native orientation and extra charges. Check existing #5633/#5708/#5717/#5719 coverage to avoid duplicate audits and preserve its exact head. Stop after the chosen missing implication; a correct root alone is not supplier admission.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "overlap_terms": [ + "invoice", + "signed moment", + "productive target", + "independent recount" + ], + "existing_checks": [ + { + "scope": "PR #4088: mixed local/owner/phase ledger and moment reported.", + "evidence": "research/staged544-mixed-fourth-entry/README.md", + "remaining": "Independent binding of changed construction to paid histogram, distinct from full admission.", + "status": "author-checked", + "source_commit": "72d7efc181edb21806a878f174847c96dd410ab0", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4091: sharp pooled ceiling proposed for fixed THREE/FOUR words and inventory.", + "evidence": "research/staged-fourth-mixture-ceiling/README.md", + "remaining": "Validate dual, exhaustive pattern scope and exact source equivalence before applying to newer fills.", + "status": "author-checked", + "source_commit": "a29bdd8f56cd18b805917775cdec09ff935eddc4", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4067: paid (2,2) to (1,3) exchange and fixed OQ4 host reported.", + "evidence": "research/r437-two-window-carrier/README.md", + "remaining": "Independent full cost delta; remaining caller/precision/stock obligations are separate.", + "status": "author-checked", + "source_commit": "a95f11c52e3ca1e4c5171b3c20d8f4b0815aee2e", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "refined", + "actual_scope": "Prove the unique optimal complete two-chain invoice over all positive lengths, ordered partitions and full binary child-tree invoices; independently bind the all-one (9,9) member to the literal pending caller.", + "scope_change_reason": "The original card permits a target-specific complete-budget obstruction. The pending source makes no global chain-length optimality claim; this adds an infinite-family argument and its applicability boundary.", + "bottleneck_link": "The complex supplier is binding. This closes pure length tuning of the frozen native and two-chain invoice, directing improvements toward changed profiles or caller structure.", + "budget_minutes": 120, + "stop_rule": "Stop after an analytical global certificate, source recount, source authentication and semantic failure controls; finite corroboration is exactly 961 pairs with each length 1 through 31. The grouped-tree corroboration exhausts all ordered forest pairs with total leaves2 through7; its analytical envelope proves the unbounded conclusion.", + "outcome": "completed", + "evidence": "PROOF.md and RESULT.json: unique optimal declared invoice (9,9), crossing in (0.0033718004754,0.0033718004755), exact root-bracket increment signs and monotonic normalization. Section6 extends the ceiling through a concave binary-child envelope, source-bound to the retained node accounting.", + "author": "@CubeJerry", + "ai_assistance": "Prepared for @CubeJerry with substantial OpenAI assistance in mathematical reasoning, verifier implementation and review.", + "open_questions": [ + { + "question": "Can a changed caller topology or multiple coupling fields beat this two-chain ceiling?", + "why_it_matters": "The theorem exhausts length tuning with the frozen native profile.", + "first_step": "Derive the complete productive and paid profile of one changed root, including thin queries and idle lifetimes.", + "blocked_by": "A concrete caller and exact operator and physical-interface proof." + }, + { + "question": "How does the optimum shift under a verified native profile change?", + "why_it_matters": "This ceiling freezes the native signed coefficients.", + "first_step": "Replace authenticated coefficients and recheck derivative and adjacent increment signs.", + "blocked_by": "A source-verified new native profile." + } + ] +} diff --git a/research/chain-root-global-ceiling/VERIFY.json b/research/chain-root-global-ceiling/VERIFY.json new file mode 100644 index 0000000000..2771c48c0b --- /dev/null +++ b/research/chain-root-global-ceiling/VERIFY.json @@ -0,0 +1,28 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Source-bound caller and child accounting, exact root/increment/binary-envelope interval signs, 961 all-one and all forests of total leaves2..7 corroboration cases, algebraic interval controls and20 negative controls." + }, + { + "argv": [ + "{python}", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Checks remain active under optimized Python." + } + ] +} diff --git a/research/chain-root-global-ceiling/intervals.py b/research/chain-root-global-ceiling/intervals.py new file mode 100644 index 0000000000..8941e77afd --- /dev/null +++ b/research/chain-root-global-ceiling/intervals.py @@ -0,0 +1,136 @@ +"""Directed integer intervals. @CubeJerry/OpenAI assistance, Apache-2.0. + +No predecessor arithmetic implementation is imported. All endpoints are +multiples of 2**-192; logarithm and exponential tails are bounded explicitly. +""" +from dataclasses import dataclass +from fractions import Fraction +from functools import lru_cache +BITS = 192 +SCALE = 1 << BITS +LOG_TERMS = 80 +EXP_TERMS = 40 + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def ceiling(a, b): + need(b > 0, "positive divisor") + return -((-a) // b) + + +@dataclass(frozen=True) +class Interval: + lo: int + hi: int + + def __post_init__(self): + need(self.lo <= self.hi, "ordered interval") + + def __add__(self, other): + return Interval(self.lo+other.lo, self.hi+other.hi) + + def __sub__(self, other): + return Interval(self.lo-other.hi, self.hi-other.lo) + + def times(self, value): + q = Fraction(value) + if q >= 0: + return Interval(self.lo*q.numerator//q.denominator, + ceiling(self.hi*q.numerator,q.denominator)) + return Interval(self.hi*q.numerator//q.denominator, + ceiling(self.lo*q.numerator,q.denominator)) + + def product(self, other): + need(self.lo>=0 and other.lo>=0, "nonnegative product") + return Interval(self.lo*other.lo//SCALE, + ceiling(self.hi*other.hi,SCALE)) + + def decimal(self, places=24): + def show(value): + sign = "-" if value<0 else "" + whole,frac = divmod(abs(value),10**places) + return sign+str(whole)+"."+str(frac).zfill(places) + return [show(self.lo*10**places//SCALE), + show(ceiling(self.hi*10**places,SCALE))] + + +ZERO = Interval(0,0) +ONE = Interval(SCALE,SCALE) + + +def rational(q): + q=Fraction(q) + return Interval(q.numerator*SCALE//q.denominator, + ceiling(q.numerator*SCALE,q.denominator)) + + +def log_from_atanh(numerator, denominator): + need(0<=3*numerator<=denominator, "atanh reduction domain") + if numerator==0: + return ZERO + z=rational(Fraction(numerator,denominator)) + square=z.product(z) + term=z + total=ZERO + for j in range(LOG_TERMS): + total=total+term.times(Fraction(1,2*j+1)) + term=term.product(square) + # 2 sum_{j=N}^infty z^(2j+1)/(2j+1) + # <= 9/[4(2N+1)3^(2N+1)], since z<=1/3. + tail=ceiling(9*SCALE,4*(2*LOG_TERMS+1)*3**(2*LOG_TERMS+1)) + return Interval(2*total.lo,2*total.hi+tail) + + +@lru_cache(None) +def log_integer(rank): + need(type(rank) is int and rank>=1, "positive integer rank") + if rank==1: + return ZERO + exponent=rank.bit_length()-1 + base=1<SCALE//2: + argument=argument.times(Fraction(1,2)) + squarings+=1 + term=ONE + total=ONE + for j in range(1,EXP_TERMS+1): + term=term.product(argument).times(Fraction(1,j)) + total=total+term + following=term.product(argument).times(Fraction(1,EXP_TERMS+1)) + # Each following term ratio <= argument.hi/[SCALE*(N+2)]. + tail=ceiling(following.hi*(EXP_TERMS+2)*SCALE, + (EXP_TERMS+2)*SCALE-argument.hi) + result=Interval(total.lo,total.hi+tail) + for _ in range(squarings): + result=result.product(result) + return result + + +@lru_cache(None) +def power(rank, saving): + saving=Fraction(saving) + need(0<=saving<=1, "saving in [0,1]") + denominator=exponential(log_integer(rank).times(saving)) + need(denominator.lo>0, "positive exponential") + return Interval(rank*SCALE*SCALE//denominator.hi, + ceiling(rank*SCALE*SCALE,denominator.lo)) + + +def signed_moment(coefficients, saving): + result=ZERO + for rank,count in coefficients.items(): + need(type(rank) is int and rank>=1 and type(count) is int, + "integer signed profile") + result=result+power(rank,Fraction(saving)).times(count) + return result diff --git a/research/chain-root-global-ceiling/retained/CALLER.json b/research/chain-root-global-ceiling/retained/CALLER.json new file mode 100644 index 0000000000..ac49576bf7 --- /dev/null +++ b/research/chain-root-global-ceiling/retained/CALLER.json @@ -0,0 +1 @@ +{"ambient_rank":153,"diagonal":[[-1,0,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1],[-1,0,1,1,1,1,1,1,1,1,1,0,0,0,0,0,0,0,0,0],[-1,0,0,1,1,1,1,1,1,1,1,0,0,0,0,0,0,0,0,0],[-1,0,0,0,1,1,1,1,1,1,1,0,0,0,0,0,0,0,0,0],[-1,0,0,0,0,1,1,1,1,1,1,0,0,0,0,0,0,0,0,0],[-1,0,0,0,0,0,1,1,1,1,1,0,0,0,0,0,0,0,0,0],[-1,0,0,0,0,0,0,1,1,1,1,0,0,0,0,0,0,0,0,0],[-1,0,0,0,0,0,0,0,1,1,1,0,0,0,0,0,0,0,0,0],[-1,0,0,0,0,0,0,0,0,1,1,0,0,0,0,0,0,0,0,0],[-1,0,0,0,0,0,0,0,0,0,1,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],[-1,0,0,0,0,0,0,0,0,0,0,1,1,0,0,0,0,0,0,0],[-1,0,0,0,0,0,0,0,0,0,0,1,1,1,0,0,0,0,0,0],[-1,0,0,0,0,0,0,0,0,0,0,1,1,1,1,0,0,0,0,0],[-1,0,0,0,0,0,0,0,0,0,0,1,1,1,1,1,0,0,0,0],[-1,0,0,0,0,0,0,0,0,0,0,1,1,1,1,1,1,0,0,0],[-1,0,0,0,0,0,0,0,0,0,0,1,1,1,1,1,1,1,0,0],[-1,0,0,0,0,0,0,0,0,0,0,1,1,1,1,1,1,1,1,0],[-1,0,0,0,0,0,0,0,0,0,0,1,1,1,1,1,1,1,1,1],[-1,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0]],"events":[["ADD",0,1,"-1"],["SWAP",0,1],["LAMBDA",0,-1],["LOCAL",1,1,0],["LAMBDA",0,1],["ADD",0,1,"-1"],["ADD",0,1,"1"],["SCALE",1,"-1"],["ADD",1,0,"1"],["ADD",1,2,"-2"],["ADD",0,2,"-1"],["SWAP",1,2],["ADD",2,0,"-2"],["SWAP",0,1],["LAMBDA",0,-1],["LOCAL",2,1,0],["LAMBDA",0,1],["ADD",0,1,"-1"],["IDLE_ONE",2,[2,3,4,5,6,7,8,9]],["ADD",0,1,"1"],["SCALE",1,"-1"],["SWAP",1,2],["ADD",2,0,"1"],["ADD",1,0,"2"],["ADD",2,3,"-2"],["ADD",1,3,"-2"],["ADD",0,3,"-1"],["SWAP",2,3],["SWAP",1,2],["ADD",3,0,"-2"],["ADD",2,0,"-2"],["SWAP",0,1],["LAMBDA",0,-1],["LOCAL",3,1,0],["LAMBDA",0,1],["ADD",0,1,"-1"],["IDLE_ONE",3,[3,4,5,6,7,8,9]],["SWAP",2,3],["ADD",0,1,"1"],["SCALE",1,"-1"],["SWAP",1,3],["ADD",3,0,"1"],["ADD",2,0,"2"],["ADD",1,0,"2"],["ADD",3,4,"-2"],["ADD",2,4,"-2"],["ADD",1,4,"-2"],["ADD",0,4,"-1"],["SWAP",3,4],["SWAP",2,3],["SWAP",1,2],["ADD",4,0,"-2"],["ADD",3,0,"-2"],["ADD",2,0,"-2"],["SWAP",0,1],["LAMBDA",0,-1],["LOCAL",4,1,0],["LAMBDA",0,1],["ADD",0,1,"-1"],["IDLE_ONE",4,[4,5,6,7,8,9]],["SWAP",3,4],["SWAP",2,4],["ADD",0,1,"1"],["SCALE",1,"-1"],["SWAP",1,4],["ADD",4,0,"1"],["ADD",3,0,"2"],["ADD",2,0,"2"],["ADD",1,0,"2"],["ADD",4,5,"-2"],["ADD",3,5,"-2"],["ADD",2,5,"-2"],["ADD",1,5,"-2"],["ADD",0,5,"-1"],["SWAP",4,5],["SWAP",3,4],["SWAP",2,3],["SWAP",1,2],["ADD",5,0,"-2"],["ADD",4,0,"-2"],["ADD",3,0,"-2"],["ADD",2,0,"-2"],["SWAP",0,1],["LAMBDA",0,-1],["LOCAL",5,1,0],["LAMBDA",0,1],["ADD",0,1,"-1"],["IDLE_ONE",5,[5,6,7,8,9]],["SWAP",4,5],["SWAP",3,5],["SWAP",2,5],["ADD",0,1,"1"],["SCALE",1,"-1"],["SWAP",1,5],["ADD",5,0,"1"],["ADD",4,0,"2"],["ADD",3,0,"2"],["ADD",2,0,"2"],["ADD",1,0,"2"],["ADD",5,6,"-2"],["ADD",4,6,"-2"],["ADD",3,6,"-2"],["ADD",2,6,"-2"],["ADD",1,6,"-2"],["ADD",0,6,"-1"],["SWAP",5,6],["SWAP",4,5],["SWAP",3,4],["SWAP",2,3],["SWAP",1,2],["ADD",6,0,"-2"],["ADD",5,0,"-2"],["ADD",4,0,"-2"],["ADD",3,0,"-2"],["ADD",2,0,"-2"],["SWAP",0,1],["LAMBDA",0,-1],["LOCAL",6,1,0],["LAMBDA",0,1],["ADD",0,1,"-1"],["IDLE_ONE",6,[6,7,8,9]],["SWAP",5,6],["SWAP",4,6],["SWAP",3,6],["SWAP",2,6],["ADD",0,1,"1"],["SCALE",1,"-1"],["SWAP",1,6],["ADD",6,0,"1"],["ADD",5,0,"2"],["ADD",4,0,"2"],["ADD",3,0,"2"],["ADD",2,0,"2"],["ADD",1,0,"2"],["ADD",6,7,"-2"],["ADD",5,7,"-2"],["ADD",4,7,"-2"],["ADD",3,7,"-2"],["ADD",2,7,"-2"],["ADD",1,7,"-2"],["ADD",0,7,"-1"],["SWAP",6,7],["SWAP",5,6],["SWAP",4,5],["SWAP",3,4],["SWAP",2,3],["SWAP",1,2],["ADD",7,0,"-2"],["ADD",6,0,"-2"],["ADD",5,0,"-2"],["ADD",4,0,"-2"],["ADD",3,0,"-2"],["ADD",2,0,"-2"],["SWAP",0,1],["LAMBDA",0,-1],["LOCAL",7,1,0],["LAMBDA",0,1],["ADD",0,1,"-1"],["IDLE_ONE",7,[7,8,9]],["SWAP",6,7],["SWAP",5,7],["SWAP",4,7],["SWAP",3,7],["SWAP",2,7],["ADD",0,1,"1"],["SCALE",1,"-1"],["SWAP",1,7],["ADD",7,0,"1"],["ADD",6,0,"2"],["ADD",5,0,"2"],["ADD",4,0,"2"],["ADD",3,0,"2"],["ADD",2,0,"2"],["ADD",1,0,"2"],["ADD",7,8,"-2"],["ADD",6,8,"-2"],["ADD",5,8,"-2"],["ADD",4,8,"-2"],["ADD",3,8,"-2"],["ADD",2,8,"-2"],["ADD",1,8,"-2"],["ADD",0,8,"-1"],["SWAP",7,8],["SWAP",6,7],["SWAP",5,6],["SWAP",4,5],["SWAP",3,4],["SWAP",2,3],["SWAP",1,2],["ADD",8,0,"-2"],["ADD",7,0,"-2"],["ADD",6,0,"-2"],["ADD",5,0,"-2"],["ADD",4,0,"-2"],["ADD",3,0,"-2"],["ADD",2,0,"-2"],["SWAP",0,1],["LAMBDA",0,-1],["LOCAL",8,1,0],["LAMBDA",0,1],["ADD",0,1,"-1"],["IDLE_ONE",8,[8,9]],["SWAP",7,8],["SWAP",6,8],["SWAP",5,8],["SWAP",4,8],["SWAP",3,8],["SWAP",2,8],["ADD",0,1,"1"],["SCALE",1,"-1"],["SWAP",1,8],["ADD",8,0,"1"],["ADD",7,0,"2"],["ADD",6,0,"2"],["ADD",5,0,"2"],["ADD",4,0,"2"],["ADD",3,0,"2"],["ADD",2,0,"2"],["ADD",1,0,"2"],["ADD",8,9,"-2"],["ADD",7,9,"-2"],["ADD",6,9,"-2"],["ADD",5,9,"-2"],["ADD",4,9,"-2"],["ADD",3,9,"-2"],["ADD",2,9,"-2"],["ADD",1,9,"-2"],["ADD",0,9,"-1"],["SWAP",8,9],["SWAP",7,8],["SWAP",6,7],["SWAP",5,6],["SWAP",4,5],["SWAP",3,4],["SWAP",2,3],["SWAP",1,2],["ADD",9,0,"-2"],["ADD",8,0,"-2"],["ADD",7,0,"-2"],["ADD",6,0,"-2"],["ADD",5,0,"-2"],["ADD",4,0,"-2"],["ADD",3,0,"-2"],["ADD",2,0,"-2"],["SWAP",0,1],["LAMBDA",0,-1],["LOCAL",9,1,0],["LAMBDA",0,1],["ADD",0,1,"-1"],["IDLE_ONE",9,[9]],["SWAP",8,9],["SWAP",7,9],["SWAP",6,9],["SWAP",5,9],["SWAP",4,9],["SWAP",3,9],["SWAP",2,9],["ADD",0,1,"1"],["SCALE",1,"-1"],["SWAP",1,9],["ADD",9,0,"1"],["ADD",8,0,"2"],["ADD",7,0,"2"],["ADD",6,0,"2"],["ADD",5,0,"2"],["ADD",4,0,"2"],["ADD",3,0,"2"],["ADD",2,0,"2"],["ADD",1,0,"2"],["ADD",19,1,"-1"],["ADD",18,1,"-1"],["ADD",17,1,"-1"],["ADD",16,1,"-1"],["ADD",15,1,"-1"],["ADD",14,1,"-1"],["ADD",13,1,"-1"],["ADD",12,1,"-1"],["ADD",11,1,"-1"],["ADD",10,1,"-1"],["ADD",9,1,"-1"],["ADD",8,1,"-1"],["ADD",7,1,"-1"],["ADD",6,1,"-1"],["ADD",5,1,"-1"],["ADD",4,1,"-1"],["ADD",3,1,"-1"],["ADD",2,1,"-1"],["SWAP",0,1],["LAMBDA",0,-1],["QUERY",0,1,-1],["LAMBDA",0,1],["ADD",0,1,"-1"],["ADD",19,0,"1"],["ADD",18,0,"1"],["ADD",17,0,"1"],["ADD",16,0,"1"],["ADD",15,0,"1"],["ADD",14,0,"1"],["ADD",13,0,"1"],["ADD",12,0,"1"],["ADD",11,0,"1"],["ADD",10,0,"1"],["ADD",9,0,"1"],["ADD",8,0,"1"],["ADD",7,0,"1"],["ADD",6,0,"1"],["ADD",5,0,"1"],["ADD",4,0,"1"],["ADD",3,0,"1"],["ADD",2,0,"1"],["SWAP",0,1],["ADD",1,19,"-1"],["ADD",1,18,"-1"],["ADD",1,17,"1"],["ADD",1,16,"-1"],["ADD",1,15,"1"],["ADD",1,14,"-1"],["ADD",1,13,"1"],["ADD",1,12,"-1"],["ADD",1,11,"1"],["ADD",1,10,"-1"],["ADD",1,9,"1"],["ADD",1,8,"-1"],["ADD",1,7,"1"],["ADD",1,6,"-1"],["ADD",1,5,"1"],["ADD",1,4,"-1"],["ADD",1,3,"1"],["ADD",1,2,"-1"],["SCALE",1,"-1"],["SCALE",0,"-1"],["ADD",18,0,"-2"],["ADD",17,0,"-2"],["ADD",16,0,"-2"],["ADD",15,0,"-2"],["ADD",14,0,"-2"],["ADD",13,0,"-2"],["ADD",12,0,"-2"],["ADD",11,0,"-2"],["ADD",10,0,"-2"],["ADD",1,0,"-2"],["LAMBDA",0,-1],["QUERY",0,1,-1],["LAMBDA",0,1],["ADD",0,1,"-1"],["ADD",1,19,"-1"],["ADD",1,18,"-1"],["ADD",1,17,"1"],["ADD",1,16,"-1"],["ADD",1,15,"1"],["ADD",1,14,"-1"],["ADD",1,13,"1"],["ADD",1,12,"-1"],["ADD",1,11,"1"],["ADD",1,10,"-1"],["ADD",1,9,"1"],["ADD",1,8,"-1"],["ADD",1,7,"1"],["ADD",1,6,"-1"],["ADD",1,5,"1"],["ADD",1,4,"-1"],["ADD",1,3,"1"],["ADD",1,2,"-1"],["SCALE",1,"-1"],["SCALE",0,"-1"],["ADD",18,0,"-2"],["ADD",17,0,"-2"],["ADD",16,0,"-2"],["ADD",15,0,"-2"],["ADD",14,0,"-2"],["ADD",13,0,"-2"],["ADD",12,0,"-2"],["ADD",11,0,"-2"],["ADD",10,0,"-2"],["ADD",18,19,"1"],["ADD",17,19,"1"],["ADD",16,19,"1"],["ADD",15,19,"1"],["ADD",14,19,"1"],["ADD",13,19,"1"],["ADD",12,19,"1"],["ADD",11,19,"1"],["ADD",10,19,"1"],["ADD",9,19,"1"],["ADD",8,19,"1"],["ADD",7,19,"1"],["ADD",6,19,"1"],["ADD",5,19,"1"],["ADD",4,19,"1"],["ADD",3,19,"1"],["ADD",2,19,"1"],["ADD",1,19,"1"],["ADD",17,18,"-2"],["ADD",16,18,"-2"],["ADD",15,18,"-2"],["ADD",14,18,"-2"],["ADD",13,18,"-2"],["ADD",12,18,"-2"],["ADD",11,18,"-2"],["ADD",10,18,"-2"],["ADD",9,18,"-2"],["ADD",8,18,"-2"],["ADD",7,18,"-2"],["ADD",6,18,"-2"],["ADD",5,18,"-2"],["ADD",4,18,"-2"],["ADD",3,18,"-2"],["ADD",2,18,"-2"],["ADD",1,18,"-2"],["SCALE",18,"-1"],["ADD",19,18,"2"],["SWAP",18,19],["ADD",19,18,"-1"],["ADD",16,17,"-2"],["ADD",15,17,"-2"],["ADD",14,17,"-2"],["ADD",13,17,"-2"],["ADD",12,17,"-2"],["ADD",11,17,"-2"],["ADD",10,17,"-2"],["ADD",9,17,"-2"],["ADD",8,17,"-2"],["ADD",7,17,"-2"],["ADD",6,17,"-2"],["ADD",5,17,"-2"],["ADD",4,17,"-2"],["ADD",3,17,"-2"],["ADD",2,17,"-2"],["ADD",1,17,"-2"],["SCALE",17,"-1"],["ADD",18,17,"2"],["SWAP",17,18],["ADD",18,17,"-1"],["ADD",15,16,"-2"],["ADD",14,16,"-2"],["ADD",13,16,"-2"],["ADD",12,16,"-2"],["ADD",11,16,"-2"],["ADD",10,16,"-2"],["ADD",9,16,"-2"],["ADD",8,16,"-2"],["ADD",7,16,"-2"],["ADD",6,16,"-2"],["ADD",5,16,"-2"],["ADD",4,16,"-2"],["ADD",3,16,"-2"],["ADD",2,16,"-2"],["ADD",1,16,"-2"],["SCALE",16,"-1"],["ADD",17,16,"2"],["SWAP",16,17],["ADD",17,16,"-1"],["ADD",14,15,"-2"],["ADD",13,15,"-2"],["ADD",12,15,"-2"],["ADD",11,15,"-2"],["ADD",10,15,"-2"],["ADD",9,15,"-2"],["ADD",8,15,"-2"],["ADD",7,15,"-2"],["ADD",6,15,"-2"],["ADD",5,15,"-2"],["ADD",4,15,"-2"],["ADD",3,15,"-2"],["ADD",2,15,"-2"],["ADD",1,15,"-2"],["SCALE",15,"-1"],["ADD",16,15,"2"],["SWAP",15,16],["ADD",16,15,"-1"],["ADD",13,14,"-2"],["ADD",12,14,"-2"],["ADD",11,14,"-2"],["ADD",10,14,"-2"],["ADD",9,14,"-2"],["ADD",8,14,"-2"],["ADD",7,14,"-2"],["ADD",6,14,"-2"],["ADD",5,14,"-2"],["ADD",4,14,"-2"],["ADD",3,14,"-2"],["ADD",2,14,"-2"],["ADD",1,14,"-2"],["SCALE",14,"-1"],["ADD",15,14,"2"],["SWAP",14,15],["ADD",15,14,"-1"],["ADD",12,13,"-2"],["ADD",11,13,"-2"],["ADD",10,13,"-2"],["ADD",9,13,"-2"],["ADD",8,13,"-2"],["ADD",7,13,"-2"],["ADD",6,13,"-2"],["ADD",5,13,"-2"],["ADD",4,13,"-2"],["ADD",3,13,"-2"],["ADD",2,13,"-2"],["ADD",1,13,"-2"],["SCALE",13,"-1"],["ADD",14,13,"2"],["SWAP",13,14],["ADD",14,13,"-1"],["ADD",11,12,"-2"],["ADD",10,12,"-2"],["ADD",9,12,"-2"],["ADD",8,12,"-2"],["ADD",7,12,"-2"],["ADD",6,12,"-2"],["ADD",5,12,"-2"],["ADD",4,12,"-2"],["ADD",3,12,"-2"],["ADD",2,12,"-2"],["ADD",1,12,"-2"],["SCALE",12,"-1"],["ADD",13,12,"2"],["SWAP",12,13],["ADD",13,12,"-1"],["ADD",10,11,"-2"],["ADD",9,11,"-2"],["ADD",8,11,"-2"],["ADD",7,11,"-2"],["ADD",6,11,"-2"],["ADD",5,11,"-2"],["ADD",4,11,"-2"],["ADD",3,11,"-2"],["ADD",2,11,"-2"],["ADD",1,11,"-2"],["SCALE",11,"-1"],["ADD",12,11,"2"],["SWAP",11,12],["ADD",12,11,"-1"],["ADD",9,10,"-2"],["ADD",8,10,"-2"],["ADD",7,10,"-2"],["ADD",6,10,"-2"],["ADD",5,10,"-2"],["ADD",4,10,"-2"],["ADD",3,10,"-2"],["ADD",2,10,"-2"],["ADD",1,10,"-2"],["SCALE",10,"-1"],["ADD",11,10,"2"],["SWAP",10,11],["ADD",11,10,"-1"],["ADD",8,9,"-2"],["ADD",7,9,"-2"],["ADD",6,9,"-2"],["ADD",5,9,"-2"],["ADD",4,9,"-2"],["ADD",3,9,"-2"],["ADD",2,9,"-2"],["ADD",1,9,"-2"],["SCALE",9,"-1"],["ADD",10,9,"2"],["SWAP",9,10],["ADD",10,9,"-1"],["ADD",7,8,"-2"],["ADD",6,8,"-2"],["ADD",5,8,"-2"],["ADD",4,8,"-2"],["ADD",3,8,"-2"],["ADD",2,8,"-2"],["ADD",1,8,"-2"],["SCALE",8,"-1"],["ADD",9,8,"2"],["SWAP",8,9],["ADD",9,8,"-1"],["ADD",6,7,"-2"],["ADD",5,7,"-2"],["ADD",4,7,"-2"],["ADD",3,7,"-2"],["ADD",2,7,"-2"],["ADD",1,7,"-2"],["SCALE",7,"-1"],["ADD",8,7,"2"],["SWAP",7,8],["ADD",8,7,"-1"],["ADD",5,6,"-2"],["ADD",4,6,"-2"],["ADD",3,6,"-2"],["ADD",2,6,"-2"],["ADD",1,6,"-2"],["SCALE",6,"-1"],["ADD",7,6,"2"],["SWAP",6,7],["ADD",7,6,"-1"],["ADD",4,5,"-2"],["ADD",3,5,"-2"],["ADD",2,5,"-2"],["ADD",1,5,"-2"],["SCALE",5,"-1"],["ADD",6,5,"2"],["SWAP",5,6],["ADD",6,5,"-1"],["ADD",3,4,"-2"],["ADD",2,4,"-2"],["ADD",1,4,"-2"],["SCALE",4,"-1"],["ADD",5,4,"2"],["SWAP",4,5],["ADD",5,4,"-1"],["ADD",2,3,"-2"],["ADD",1,3,"-2"],["SCALE",3,"-1"],["ADD",4,3,"2"],["SWAP",3,4],["ADD",4,3,"-1"],["ADD",1,2,"-2"],["SCALE",2,"-1"],["ADD",3,2,"2"],["SWAP",2,3],["ADD",3,2,"-1"],["SCALE",1,"-1"],["ADD",2,1,"2"],["SWAP",1,2],["ADD",2,1,"-1"],["SCALE",0,"-1"],["ADD",19,0,"-2"],["ADD",18,0,"-2"],["ADD",17,0,"-2"],["ADD",16,0,"-2"],["ADD",15,0,"-2"],["ADD",14,0,"-2"],["ADD",13,0,"-2"],["ADD",12,0,"-2"],["ADD",11,0,"-2"],["ADD",1,0,"-3"],["LAMBDA",0,-1],["QUERY",0,1,-1],["LAMBDA",0,1],["ADD",0,1,"-1"],["ADD",1,19,"-2"],["ADD",1,18,"2"],["SWAP",18,19],["ADD",1,17,"-2"],["SWAP",17,19],["ADD",1,16,"2"],["SWAP",16,19],["ADD",1,15,"-2"],["SWAP",15,19],["ADD",1,14,"2"],["SWAP",14,19],["ADD",1,13,"-2"],["SWAP",13,19],["ADD",1,12,"2"],["SWAP",12,19],["ADD",1,11,"-2"],["SWAP",11,19],["ADD",1,10,"2"],["SWAP",10,19],["ADD",1,9,"-2"],["SWAP",9,19],["ADD",1,8,"2"],["SWAP",8,19],["ADD",1,7,"-2"],["SWAP",7,19],["ADD",1,6,"2"],["SWAP",6,19],["ADD",1,5,"-2"],["SWAP",5,19],["ADD",1,4,"2"],["SWAP",4,19],["ADD",1,3,"-2"],["SWAP",3,19],["ADD",1,2,"2"],["SWAP",2,19],["SWAP",1,19],["SCALE",0,"-1"],["ADD",19,0,"1"],["ADD",18,0,"-2"],["ADD",17,0,"-2"],["ADD",16,0,"-2"],["ADD",15,0,"-2"],["ADD",14,0,"-2"],["ADD",13,0,"-2"],["ADD",12,0,"-2"],["ADD",11,0,"-2"],["ADD",10,0,"-2"],["ADD",0,10,"1"],["ADD",18,10,"-2"],["ADD",17,10,"-2"],["ADD",16,10,"-2"],["ADD",15,10,"-2"],["ADD",14,10,"-2"],["ADD",13,10,"-2"],["ADD",12,10,"-2"],["ADD",11,10,"-2"],["SWAP",9,18],["SWAP",8,17],["SWAP",7,16],["SWAP",6,15],["SWAP",5,14],["SWAP",4,13],["SWAP",3,12],["SWAP",2,11],["SWAP",1,10],["ADD",9,0,"2"],["ADD",8,0,"2"],["ADD",7,0,"2"],["ADD",6,0,"2"],["ADD",5,0,"2"],["ADD",4,0,"2"],["ADD",3,0,"2"],["ADD",2,0,"2"],["SWAP",0,1],["LAMBDA",0,-1],["LOCAL",10,1,0],["LAMBDA",0,1],["ADD",0,1,"-1"],["IDLE_ONE",2,[10]],["IDLE_ONE",3,[10,11]],["IDLE_ONE",4,[10,11,12]],["IDLE_ONE",5,[10,11,12,13]],["IDLE_ONE",6,[10,11,12,13,14]],["IDLE_ONE",7,[10,11,12,13,14,15]],["IDLE_ONE",8,[10,11,12,13,14,15,16]],["IDLE_ONE",9,[10,11,12,13,14,15,16,17]],["SWAP",9,18],["SWAP",8,17],["SWAP",7,16],["SWAP",6,15],["SWAP",5,14],["SWAP",4,13],["SWAP",3,12],["SWAP",2,11],["ADD",0,1,"-1"],["SWAP",1,10],["SCALE",0,"-1"],["ADD",18,0,"-2"],["ADD",17,0,"-2"],["ADD",16,0,"-2"],["ADD",15,0,"-2"],["ADD",14,0,"-2"],["ADD",13,0,"-2"],["ADD",12,0,"-2"],["ADD",11,0,"-2"],["ADD",10,0,"-1"],["ADD",16,17,"-1"],["ADD",15,17,"-1"],["ADD",14,17,"-1"],["ADD",13,17,"-1"],["ADD",12,17,"-2"],["ADD",11,17,"-1"],["ADD",0,17,"1"],["SCALE",17,"-1"],["ADD",18,17,"1"],["SWAP",16,18],["ADD",14,15,"-1"],["ADD",13,15,"-1"],["ADD",12,15,"-2"],["ADD",11,15,"-1"],["ADD",0,15,"1"],["SCALE",15,"-1"],["ADD",18,15,"1"],["ADD",17,15,"1"],["ADD",16,15,"1"],["SWAP",14,18],["ADD",12,13,"-2"],["ADD",11,13,"-1"],["ADD",0,13,"1"],["SCALE",13,"-1"],["ADD",18,13,"1"],["ADD",17,13,"1"],["ADD",16,13,"1"],["ADD",15,13,"1"],["ADD",14,13,"1"],["SWAP",12,18],["ADD",0,11,"1"],["SCALE",11,"-1"],["ADD",18,11,"2"],["ADD",17,11,"2"],["SWAP",11,17],["ADD",17,11,"-1"],["ADD",16,11,"1"],["ADD",15,11,"1"],["ADD",14,11,"1"],["ADD",13,11,"1"],["ADD",12,11,"1"],["SWAP",10,18],["SWAP",9,17],["SWAP",8,16],["SWAP",7,15],["SWAP",6,14],["SWAP",5,13],["SWAP",4,12],["SWAP",3,11],["SWAP",2,10],["SWAP",1,9],["ADD",8,0,"2"],["ADD",7,0,"2"],["ADD",6,0,"2"],["ADD",5,0,"2"],["ADD",4,0,"2"],["ADD",3,0,"2"],["ADD",2,0,"2"],["SWAP",0,1],["LAMBDA",0,-1],["LOCAL",11,1,0],["LAMBDA",0,1],["ADD",0,1,"-1"],["SWAP",16,18],["SWAP",15,17],["SWAP",14,16],["SWAP",13,15],["SWAP",12,14],["SWAP",11,13],["SWAP",10,12],["SWAP",9,11],["SWAP",8,18],["SWAP",7,17],["SWAP",6,16],["SWAP",5,15],["SWAP",4,14],["SWAP",3,13],["SWAP",2,12],["ADD",0,1,"-1"],["SWAP",1,11],["SCALE",0,"-1"],["ADD",18,0,"-2"],["ADD",17,0,"-2"],["ADD",16,0,"-2"],["ADD",15,0,"-2"],["ADD",14,0,"-2"],["ADD",13,0,"-2"],["ADD",12,0,"-2"],["ADD",11,0,"-1"],["ADD",17,18,"-1"],["ADD",16,18,"-1"],["ADD",15,18,"-2"],["ADD",14,18,"-2"],["ADD",13,18,"-2"],["ADD",12,18,"-1"],["ADD",0,18,"1"],["SCALE",18,"-1"],["ADD",16,17,"-1"],["ADD",15,17,"-2"],["ADD",14,17,"-2"],["ADD",13,17,"-2"],["ADD",12,17,"-1"],["ADD",0,17,"1"],["SCALE",17,"-1"],["ADD",18,17,"1"],["ADD",15,16,"-2"],["ADD",14,16,"-2"],["ADD",13,16,"-2"],["ADD",12,16,"-1"],["ADD",0,16,"1"],["SCALE",16,"-1"],["ADD",18,16,"1"],["ADD",17,16,"1"],["SWAP",15,18],["SWAP",14,17],["SWAP",13,16],["ADD",0,12,"1"],["SCALE",12,"-1"],["ADD",18,12,"2"],["ADD",17,12,"2"],["ADD",16,12,"2"],["ADD",15,12,"2"],["SWAP",12,15],["ADD",15,12,"-1"],["ADD",14,12,"1"],["ADD",13,12,"1"],["SWAP",11,18],["SWAP",10,17],["SWAP",9,16],["SWAP",8,15],["SWAP",7,14],["SWAP",6,13],["SWAP",5,12],["SWAP",4,11],["SWAP",3,10],["SWAP",2,9],["SWAP",1,8],["ADD",7,0,"2"],["ADD",6,0,"2"],["ADD",5,0,"2"],["ADD",4,0,"2"],["ADD",3,0,"2"],["ADD",2,0,"2"],["SWAP",0,1],["LAMBDA",0,-1],["LOCAL",12,1,0],["LAMBDA",0,1],["ADD",0,1,"-1"],["SWAP",17,18],["SWAP",16,17],["SWAP",15,16],["SWAP",14,18],["SWAP",13,17],["SWAP",12,16],["SWAP",11,15],["SWAP",10,14],["SWAP",9,13],["SWAP",8,12],["SWAP",7,18],["SWAP",6,17],["SWAP",5,16],["SWAP",4,15],["SWAP",3,14],["SWAP",2,13],["ADD",0,1,"-1"],["SWAP",1,12],["SCALE",0,"-1"],["ADD",18,0,"-2"],["ADD",17,0,"-2"],["ADD",16,0,"-2"],["ADD",15,0,"-2"],["ADD",14,0,"-2"],["ADD",13,0,"-2"],["ADD",12,0,"-1"],["ADD",0,13,"1"],["ADD",18,13,"-2"],["ADD",17,13,"-2"],["ADD",16,13,"-2"],["ADD",15,13,"-2"],["ADD",14,13,"-2"],["SWAP",12,18],["SWAP",11,17],["SWAP",10,16],["SWAP",9,15],["SWAP",8,14],["SWAP",7,13],["SWAP",6,12],["SWAP",5,11],["SWAP",4,10],["SWAP",3,9],["SWAP",2,8],["SWAP",1,7],["ADD",6,0,"2"],["ADD",5,0,"2"],["ADD",4,0,"2"],["ADD",3,0,"2"],["ADD",2,0,"2"],["SWAP",0,1],["LAMBDA",0,-1],["LOCAL",13,1,0],["LAMBDA",0,1],["ADD",0,1,"-1"],["SWAP",12,18],["SWAP",11,17],["SWAP",10,16],["SWAP",9,15],["SWAP",8,14],["SWAP",7,13],["SWAP",6,18],["SWAP",5,17],["SWAP",4,16],["SWAP",3,15],["SWAP",2,14],["ADD",0,1,"-1"],["SWAP",1,13],["SCALE",0,"-1"],["ADD",18,0,"-2"],["ADD",17,0,"-2"],["ADD",16,0,"-2"],["ADD",15,0,"-2"],["ADD",14,0,"-2"],["ADD",13,0,"-1"],["ADD",17,18,"-1"],["ADD",16,18,"-2"],["ADD",15,18,"-2"],["ADD",14,18,"-1"],["ADD",0,18,"1"],["SCALE",18,"-1"],["ADD",16,17,"-2"],["ADD",15,17,"-2"],["ADD",14,17,"-1"],["ADD",0,17,"1"],["SCALE",17,"-1"],["ADD",18,17,"1"],["SWAP",16,18],["SWAP",15,17],["ADD",0,14,"1"],["SCALE",14,"-1"],["ADD",18,14,"2"],["ADD",17,14,"2"],["ADD",16,14,"2"],["SWAP",14,16],["ADD",16,14,"-1"],["ADD",15,14,"1"],["SWAP",13,18],["SWAP",12,17],["SWAP",11,16],["SWAP",10,15],["SWAP",9,14],["SWAP",8,13],["SWAP",7,12],["SWAP",6,11],["SWAP",5,10],["SWAP",4,9],["SWAP",3,8],["SWAP",2,7],["SWAP",1,6],["ADD",5,0,"2"],["ADD",4,0,"2"],["ADD",3,0,"2"],["ADD",2,0,"2"],["SWAP",0,1],["LAMBDA",0,-1],["LOCAL",14,1,0],["LAMBDA",0,1],["ADD",0,1,"-1"],["SWAP",17,18],["SWAP",16,17],["SWAP",15,18],["SWAP",14,17],["SWAP",13,16],["SWAP",12,15],["SWAP",11,14],["SWAP",10,18],["SWAP",9,17],["SWAP",8,16],["SWAP",7,15],["SWAP",6,14],["SWAP",5,18],["SWAP",4,17],["SWAP",3,16],["SWAP",2,15],["ADD",0,1,"-1"],["SWAP",1,14],["SCALE",0,"-1"],["ADD",18,0,"-2"],["ADD",17,0,"-2"],["ADD",16,0,"-2"],["ADD",15,0,"-2"],["ADD",14,0,"-1"],["ADD",16,17,"-2"],["ADD",15,17,"-1"],["ADD",0,17,"1"],["SCALE",17,"-1"],["ADD",18,17,"1"],["SWAP",16,18],["ADD",0,15,"1"],["SCALE",15,"-1"],["ADD",18,15,"2"],["ADD",17,15,"2"],["SWAP",15,17],["ADD",17,15,"-1"],["ADD",16,15,"1"],["SWAP",14,18],["SWAP",13,17],["SWAP",12,16],["SWAP",11,15],["SWAP",10,14],["SWAP",9,13],["SWAP",8,12],["SWAP",7,11],["SWAP",6,10],["SWAP",5,9],["SWAP",4,8],["SWAP",3,7],["SWAP",2,6],["SWAP",1,5],["ADD",4,0,"2"],["ADD",3,0,"2"],["ADD",2,0,"2"],["SWAP",0,1],["LAMBDA",0,-1],["LOCAL",15,1,0],["LAMBDA",0,1],["ADD",0,1,"-1"],["SWAP",16,18],["SWAP",15,17],["SWAP",14,16],["SWAP",13,15],["SWAP",12,18],["SWAP",11,17],["SWAP",10,16],["SWAP",9,15],["SWAP",8,18],["SWAP",7,17],["SWAP",6,16],["SWAP",5,15],["SWAP",4,18],["SWAP",3,17],["SWAP",2,16],["ADD",0,1,"-1"],["SWAP",1,15],["SCALE",0,"-1"],["ADD",18,0,"-2"],["ADD",17,0,"-2"],["ADD",16,0,"-2"],["ADD",15,0,"-1"],["ADD",0,16,"1"],["ADD",18,16,"-2"],["ADD",17,16,"-2"],["SWAP",15,18],["SWAP",14,17],["SWAP",13,16],["SWAP",12,15],["SWAP",11,14],["SWAP",10,13],["SWAP",9,12],["SWAP",8,11],["SWAP",7,10],["SWAP",6,9],["SWAP",5,8],["SWAP",4,7],["SWAP",3,6],["SWAP",2,5],["SWAP",1,4],["ADD",3,0,"2"],["ADD",2,0,"2"],["SWAP",0,1],["LAMBDA",0,-1],["LOCAL",16,1,0],["LAMBDA",0,1],["ADD",0,1,"-1"],["SWAP",15,18],["SWAP",14,17],["SWAP",13,16],["SWAP",12,18],["SWAP",11,17],["SWAP",10,16],["SWAP",9,18],["SWAP",8,17],["SWAP",7,16],["SWAP",6,18],["SWAP",5,17],["SWAP",4,16],["SWAP",3,18],["SWAP",2,17],["ADD",0,1,"-1"],["SWAP",1,16],["SCALE",0,"-1"],["ADD",18,0,"-2"],["ADD",17,0,"-2"],["ADD",16,0,"-1"],["ADD",0,17,"1"],["ADD",18,17,"-2"],["SWAP",16,18],["SWAP",15,17],["SWAP",14,16],["SWAP",13,15],["SWAP",12,14],["SWAP",11,13],["SWAP",10,12],["SWAP",9,11],["SWAP",8,10],["SWAP",7,9],["SWAP",6,8],["SWAP",5,7],["SWAP",4,6],["SWAP",3,5],["SWAP",2,4],["SWAP",1,3],["ADD",2,0,"2"],["SWAP",0,1],["LAMBDA",0,-1],["LOCAL",17,1,0],["LAMBDA",0,1],["ADD",0,1,"-1"],["SWAP",16,18],["SWAP",15,17],["SWAP",14,18],["SWAP",13,17],["SWAP",12,18],["SWAP",11,17],["SWAP",10,18],["SWAP",9,17],["SWAP",8,18],["SWAP",7,17],["SWAP",6,18],["SWAP",5,17],["SWAP",4,18],["SWAP",3,17],["SWAP",2,18],["ADD",0,1,"-1"],["SWAP",1,17],["SCALE",0,"-1"],["ADD",18,0,"-2"],["ADD",17,0,"-1"],["ADD",0,18,"1"],["SWAP",17,18],["SWAP",16,17],["SWAP",15,16],["SWAP",14,15],["SWAP",13,14],["SWAP",12,13],["SWAP",11,12],["SWAP",10,11],["SWAP",9,10],["SWAP",8,9],["SWAP",7,8],["SWAP",6,7],["SWAP",5,6],["SWAP",4,5],["SWAP",3,4],["SWAP",2,3],["SWAP",1,2],["SWAP",0,1],["LAMBDA",0,-1],["LOCAL",18,1,0],["LAMBDA",0,1],["ADD",0,1,"-1"],["SWAP",17,18],["SWAP",16,18],["SWAP",15,18],["SWAP",14,18],["SWAP",13,18],["SWAP",12,18],["SWAP",11,18],["SWAP",10,18],["SWAP",9,18],["SWAP",8,18],["SWAP",7,18],["SWAP",6,18],["SWAP",5,18],["SWAP",4,18],["SWAP",3,18],["SWAP",2,18],["ADD",0,1,"-1"],["SWAP",1,18],["SCALE",0,"-1"],["ADD",18,0,"-1"],["LAMBDA",0,-1],["LAMBDA",1,-1],["LAMBDA",2,-1],["LAMBDA",3,-1],["LAMBDA",4,-1],["LAMBDA",5,-1],["LAMBDA",6,-1],["LAMBDA",7,-1],["LAMBDA",8,-1],["LAMBDA",9,-1],["LAMBDA",10,-1],["LAMBDA",11,-1],["LAMBDA",12,-1],["LAMBDA",13,-1],["LAMBDA",14,-1],["LAMBDA",15,-1],["LAMBDA",16,-1],["LAMBDA",17,-1],["LAMBDA",18,-1],["LAMBDA",19,-1]],"n":20,"nodes":[],"roles":20,"sL":[1,1,1,1,1,1,1,1,1],"sR":[1,1,1,1,1,1,1,1,1],"schema":"chain-nested-root/1","stages":18} diff --git a/research/chain-root-global-ceiling/retained/NOTICE b/research/chain-root-global-ceiling/retained/NOTICE new file mode 100644 index 0000000000..d03cab1fcb --- /dev/null +++ b/research/chain-root-global-ceiling/retained/NOTICE @@ -0,0 +1,5 @@ +Native main-retiming/helper retirement extension by Jerry Chen / @CubeJerry, with substantial OpenAI Codex assistance and separate source-bound review. Apache-2.0. + +Original retained headers, licenses and notices remain unchanged. See retained/caller/NOTICE for the full native/caller/compiler/interval lineage; Ali Romman supplies the helper-basis mechanism, DreamingOfClouds the #6702 native source, and zxv the #6726 caller. + +The chain-nested root caller (chain_root.py, CALLER.json) is by DreamingOfClouds with Claude Opus 5.5 (Anthropic), via Claude Code; it follows thu-nmrc's common idle fusion (#6716) and zxv's two-pair root (#6726), and uses the native word of #6824. diff --git a/research/chain-root-global-ceiling/retained/PROOF.md b/research/chain-root-global-ceiling/retained/PROOF.md new file mode 100644 index 0000000000..d0bfd74266 --- /dev/null +++ b/research/chain-root-global-ceiling/retained/PROOF.md @@ -0,0 +1,182 @@ +# Chain-nested root: identity, chain merge, invoice + +Tags: **[P]** proved below by hand, **[C]** checked by exact replay on the literal +data, **[A]** inherited assumption. `chain_root.py` and `independent/check_root.py` +do the exact checks. The native word is #6824's, and its proof is `PROOF-6824.md` +and `PROOF-6805.md`. + +## 1. The family + +Take child sizes `sL`, `sR`, with `gL`, `gR` entries. The fields are `A, f_0..f_{gL-1}, +h_0..h_{gR-1}`, plus one empty field `E` when the count would be odd, so `n` is even. +The priced shape is `(9|9)`, with `n = 20`. + +Each query is `T_k = I + (S-1) R_k`, `R_k = x_k y_k^T`, `y_k x_k = 0`. Here +`S = λ Q^-1` with `λ = (1+i)/2 + ((1-i)/2) Q^2`, so `S^2 = 1` on `Q^4 = 1`: `S = 1` at +`Q = 1, i` and `S = -1` at `Q = -1, -i`. The time order is L sites, thin queries, R sites. + +| Site | `x` | `y` | Support `M` | +|---|---|---|---| +| L, `i` | `A + f_i + 2Σ_{jm} h_l` | `A* + h_m*` | `{A, h_l : l >= m}` | + +For `gL, gR` odd the three thin queries have parameters +`(a,u,p,q) = (0,1,0,1), (-1,2,1,0), (-1,3,1,-1)`: + +```text +x = aA + (a+1)Σ f_i + (1-a)Σ h_l + qE +y = uA* + (1-u)Σ (-1)^i f_i* + (u-1)Σ (-1)^(gR-1-l) h_l* + pE* +``` + +Other parities have their own closed forms in `chain_root.thin_vectors`. They are not +priced here and this proof does not cover them. + +## 2. The root endpoint [P] + +**Lemma 1 (sign Gram).** Let `(x_k, y_k)`, `k = 0..n`, with `n` even, satisfy +`y_i x_j = sgn(i-j)`, let the `x_k` span the `n`-dimensional space, and let +`Σ (-1)^k x_k = 0`. Then `(I-2R_n)...(I-2R_0) = -I`. + +*Proof.* With `L` the strictly lower part of `G = Y^T X`, the product expands to +`I - 2X(I+2L)^{-1}Y^T`. All entries of `L` below the diagonal are 1, so +`I + 2L = G + J`, where `J` is the all-ones matrix. Let `c_k = (-1)^k`. Then `Gc = 0`, +because an odd alternating sum of signs vanishes, and `Jc = e` because `n+1` is odd. +So `(G+J)^{-1} e = c`. Put `B = X(G+J)^{-1}Y^T`. Then +`BX = X(G+J)^{-1}(G+J-J) = X - X(G+J)^{-1}e e^T = X - (Xc)e^T = X`. +The `x_k` span, so `B = I`, and the product is `I - 2I = -I`. QED. + +**The family satisfies it for `gL, gR` odd.** + +- Within L, `y_i x_l = 1 - [l=i] - 2[l>i]`, which is `sgn(i-l)`. Within R the same + computation gives the same sign. Across, `y_R x_L = 1`, `y_L x_R = -1`. +- For thin `(u,p)` against `(a',q')`, `y x = a'(2-u) + pq'`, because both alternating sums + equal 1. The three parameter rows give exactly the sign pattern. +- `y_{L,i} x_thin = a' - (a'+1) = -1`. `y_thin x_{L,i} = u + (1-u)[(-1)^i + 2Σ_{j all D`, +`f_i -> D` over L sites `>= i`, `h_m -> D` over R sites `<= m`, `E -> 1`. + +## 4. Chain-merge lemma [P] + +**Lemma 3 (chain merge).** Fix one group (L or R) with sites in time order, and for each +site a decomposition `P_k = Π_k + Σ_{ℓ ∋ k} E_ℓ`, where `E_ℓ = φ_ℓ γ_ℓ^T` and `C(ℓ)` is a +set of consecutive sites. Assume: + +1. `γ_ℓ φ_ℓ = 1`, and `γ_ℓ φ_ℓ' = 0` for `ℓ != ℓ'`; +2. `φ_ℓ, γ_ℓ` are supported in `M_k`, and `y_k φ_ℓ = 0`, `γ_ℓ x_k = 0`, for all `k` in `C(ℓ)`; +3. `Π_k` is idempotent with `Π_k x_k = x_k` and `y_k^T Π_k = y_k^T`. + +Set `G_k = (I + (D_k-1)Π_k) T_k` and `W_ℓ = Π_{k in C(ℓ)} D_k`. Then the ordered product of +`Δ_k T_k` equals the ordered product of `G_k` with one factor `I + (W_ℓ-1)E_ℓ` inserted +anywhere within or right after `C(ℓ)` such that only sites of `C(ℓ)` are crossed. + +*Proof.* The `E_ℓ` are orthogonal idempotents inside `P_k` by (1) and (2), so +`E_ℓ Π_k = Π_k E_ℓ = 0`, and +`Δ_k = (I + (D_k-1)Π_k) Π_{ℓ∋k}(I + (D_k-1)E_ℓ)`. By (2), `E_ℓ T_k = E_ℓ = T_k E_ℓ`, so +`E_ℓ` commutes with `G_k` for each `k` in `C(ℓ)`. Factors for different lines commute by (1). +So each factor `I + (D_k-1)E_ℓ` slides to the chosen time, and they multiply to +`I + (W_ℓ-1)E_ℓ`, since `E_ℓ^2 = E_ℓ`. QED. + +**Instance.** L line `j >= 1`: `φ = f_{j-1}`, `γ = f*_{j-1} - 2A*`, `C = {sites j..gL-1}`, +paid at site `j`. R line `j <= gR-2`: `φ = h_{j+1}`, `γ = h*_{j+1} + 2A*`, `C = {sites 0..j}`, +paid at site 0. Then `γ x_i = 2 - 2 = 0` and `y_i φ = 0` for `i` in `C`. +The lines fill each support outside a rank-two plane, because `|M_k| - 2` lines cover site `k`. +`verify_root` checks each hypothesis exactly, including that `Π_k` has rank two [C]. + +**Scope.** The lemma needs nothing about the fields beyond these hypotheses, and no statement +is made about other merge structures. + +## 5. The literal caller [C, with P for the gadget] + +At a full site, the gates `LAMBDA(x,-1); LOCAL(s,y,x); LAMBDA(x,1); ADD(x,y,-1)` act on +registers `(x,y)` as `D_s (x + (S-1) y, y)`. That is `G_k` in the site's basis, whose first +two columns are `x_k` and a vector `w_k` with `y_k w_k = 1` [P]. A thin query is the same +without `D`. A final `LAMBDA(r,-1)` turns `S·Π Δ` into the target `Q^-1 · Π D`. + +**Theorem.** For the priced word and all 20 arbitrary caller inputs, the output of role `r` +is `Q^-1 Π_{s in W_r} D_s` times input `r`, exactly, with no other coefficient. + +Sections 2 to 4 prove this for the root at `(9|9)`. These literal checks bind the word to it: + +- `caller.replay` (forward) and `rows.transpose` (reverse), all 400 coefficients over + `Q(i)[q, D_s]`; +- `independent/check_invoice.caller_columns`, a separately written adjoint; +- `independent/check_root.family`: the symbolic matrix product from the formula; the + literal word at `Q = ±1`, `D = 1`, giving `±I`; and at each of the 16 `IDLE_ONE` events, + the register's line and dual read from the word itself, compared with the formula, with + each covered native call shown to miss that line. + +Tree children in the gate use the retained binary supplier, whose proof is in the retained +caller lineage; there the identity is checked by replay and is not re-proved here. + +## 6. Whole-job contract, and what is not proved here + +Every credited target is a whole transform of one independent arbitrary input, and every +paid idle is one whole transform of one field per port. The word has 2,080 main fields and +10,152 native helper fields, all distinct, with no copied input. + +A whole idle on stage set `W` has rank `8|W|`, on disjoint fresh axes. The physical replay +checks its phase, and the two-coordinate exchanges on both boundaries are charged. + +**Caveat.** Ranks 48 to 64 and spans of up to 8 sites extend the rule that #6726 used at +rank 40; this package gives no new compiler proof. Also, the merged line crosses sites with +different ordinary bases, while #6716's coordinates sit in one shared basis: see +`ADAPTERS.md`. The job is applied once, to one register, so the accepted identity is +the theorem of section 5. Reviewers should confirm that the `compiler` assumption covers it. + +## 7. Invoice and gate + +Per port, the outer histogram at `(9|9)` is `T = {1:1, 9:2, 17:2, ..., 73:2, 145:1}` and +`P = {1:3, 8s:2 for s = 1..8}`, for an outer rank margin of 305. Over 18 native calls the +total is `T - P` rank mass 760, unchanged from #6824. `pricing.py` compares this formula with +the literal histogram and the physical checks. + +**Gate [C].** The same constructor at `(4,4,1|1,4,4)` gives a word with 32 roles and 518 +events that passes both replays. On the same native word, its target and paid histograms +equal those of the retained #6726 caller minus one cancelling pair `T_32 = P_32 = 208`. +Both interval engines then place its crossing in `(0.00330823456614, 0.00330823456615)`, +which is #6824's interval. So the family reproduces #6824 exactly at that shape. + +**Crossing [C].** Both interval engines place the crossing of the priced word in +`(0.0033718004754, 0.0033718004755)`. The Decimal value `.00337180047549672` is a diagnostic +in the independent audit, not a certificate. The retained derivative bound through `.0034` +gives uniqueness. + +## 8. Theorem context + +This is a finite construction plus a complete invoice. The conditional statement is the +retained chain's: given `native_all_columns`, `owned_erasure`, `compiler`, `precision_tape`, +`analytic_recovery` [A], the outer theorem admits `κ = 0.00337180`. The claim is below the +retained BIT saving `.0034`, so #6805's pin is unchanged. The selected `κ` is unchanged. + +| Item | Status | +|---|---| +| Root endpoint and sign Gram, odd/odd | P, and C at both shapes | +| Stage factors and chain merge | P, hypotheses C at both shapes | +| Whole-word identity at `(9|9)` | P + C | +| Whole-word identity at the gate | C (binary supplier retained) | +| Native word | C here; proof in `PROOF-6824.md`, `PROOF-6805.md` | +| Physical contacts, adapters, allocation, invoice | C, two implementations | +| Crossing, strictification, compiler arithmetic, 54+4 outer inequalities | C | +| Five framework assumptions | A, not discharged | +| Compiler acceptance of whole idles at ranks 48 to 64 across several sites | Not proved here | diff --git a/research/chain-root-global-ceiling/retained/README.md b/research/chain-root-global-ceiling/retained/README.md new file mode 100644 index 0000000000..a2c71f0e6c --- /dev/null +++ b/research/chain-root-global-ceiling/retained/README.md @@ -0,0 +1,114 @@ +# Conditional κ = 0.00337180 from a chain-nested root on the #6824 native word + +The supplier tree of the #6726 caller is replaced by one root with a full site for +every native call and a chain of whole idles. The native word is unchanged. The +complete 18-call construction supports **κ = 0.00337180**, up from the pending +**0.00330823** in [#6824](https://github.com/CrocSwap/integer-mult-bounds/pull/6824), +a gain of **+6.36e-5** (**+1.92%**). + +The raw crossing lies strictly in **(0.0033718004754, 0.0033718004755)**; the tested +saving is 0.00337180035. Selected κ = 0.003125804 is unchanged. + +All five framework assumptions remain: `native_all_columns`, `owned_erasure`, +`compiler`, `precision_tape`, and `analytic_recovery`. External review is open. +This is a conditional, author-side construction result. + +## The construction + +Fields are `A, f_0..f_8, h_0..h_8` and one empty field `E`, so `n = 20`. + +- L site `i`: `x = A + f_i + 2Σ_{jm} h_l`, `y = A* + h_m*`, support `{A, h_l : l >= m}`. +- Three thin queries between the groups complete the shortest root `Π(I - 2R_k) = -I`. + +Each inner field has one idle line, `φ = f_{j-1}`, `γ = f*_{j-1} - 2A*` (mirrored on the +right). The line and its dual are killed by `y_i` and `x_i` on every later site of the +group, so it commutes across them, and its stage factors combine into **one whole idle of +rank `8·(sites covered)`**, ranks 8 to 64. Each inner field has a target of rank `8q+1` +against a paid rank `8q`, and no binary supplier nodes are left. + +`PROOF.md` proves the arbitrary-input identity and states the chain-merge lemma. + +The same constructor at shape `(4,4,1|1,4,4)` is built in every replay as a gate: its +invoice equals #6726's minus one cancelling pair `T_32 = P_32`, and both interval engines +place its crossing in #6824's interval (0.00330823456614, 0.00330823456615). + +| Complete census | #6824 | This construction | +|---|---:|---:| +| Native calls / native word | 18 / same | 18 / same payload | +| Caller roles | 34 | 20 | +| Caller events | 606 | 1,237 | +| Thin queries | 15 | 3 | +| Whole idle jobs (`IDLE` / `IDLE_ONE` events) | 3,120 (12 / 6) | 1,664 (0 / 16) | +| Largest paid rank | 40 | 64 | +| Largest stage support (coordinates) | 4 | 10 | +| Productive fields | 13,688 | 12,232 | +| Paid Gaussian requests | 66,888 | 64,184 | +| Paid rank mass | 178,044 | 166,812 | +| Rank-mass surplus | 760 | 760 | +| Ordinary caller upper bound | 535,415,008 | 488,177,792 (recomputed) | +| Physical contacts | 7,488 | 7,488 (recomputed) | + +Caller scalars are integers: `ADD` by ±1, ±2, −3 and `SCALE` by −1. + +## Reproduce + +Python 3.12, standard library only. From the repository root: + +```sh +python3.12 -B scripts/research_package.py --package research/p104-chain-nested-root +``` + +The self-contained scientific replay also works without Git or network: + +```sh +python3 -B research/p104-chain-nested-root/verify.py +``` + +Expected: `PASS_CHAIN_NESTED_ROOT`, with conditional κ = 16859/5000000, and +`PASS_REGISTERED_RESEARCH_PACKAGE` from the registered command (normal and optimized +interpreters). The literal caller is `CALLER.json`, rebuilt by `chain_root.py`; the pins are +in `EXPECTED.json`. To write the native word, use +`python3 -B research/p104-chain-nested-root/construct.py --output lifted-native.json.gz`. + +## Sources and review boundary + +Base: `7c49fe32c55de02c2c873655c804b16e4c3fef0a`. The native word is rebuilt from the #6702 +word through #6805 and #6824 (`2a7ca44fbda3abaa4df355b183ed7d7478eef7c1`), and +`native_payload_sha256` is unchanged from #6824. The #6726 caller at +`435bbe91fb28cb1d7a569ca70c6c4e9eb302d486` is retained and rebuilt as the comparison +baseline. All required bytes are committed, with Git blob and SHA256 pins in +`retained/SOURCE-PINS.json`; nothing needs fetching for replay. The canonical-job adapter +charges follow [#6763](https://github.com/CrocSwap/integer-mult-bounds/pull/6763). +`ADAPTERS.md` lists each adapted driver and each recount. + +**Whole idles at ranks 48 to 64 extend the rule #6726 used at rank 40. This package gives no +new compiler proof for them.** The merged lines also cross sites with different ordinary +bases, unlike #6716's shared-basis coordinates; `ADAPTERS.md` and `PROOF.md` section 6 quote +the rule and state the reading for reviewers to check. + +The retained BIT saving is 17/5000, the claim is below it, and no BIT improvement is claimed. +The selected full multiplier cold replay, hosted CI, proof-kernel verification, historical +pending-commit ancestry and human review are not claimed. No exhaustive novelty search is +claimed. Reviews under `retained/predecessor-reviews/` concern earlier words. + +## Open next questions + +1. Does the compiler contract accept whole idles of rank 48 to 64 across several sites with + no further argument? This is the first point to review. +2. Do roots with more than one coupling field admit a longer chain? Each needs its own exact + root, identity and complete bill; none is claimed here. + +Structured first steps and blockers are in `TASK.json`. + +## Credit + +DreamingOfClouds with Claude Opus 5.5 (Anthropic), via Claude Code, for the chain-nested root. +thu-nmrc for common idle fusion (#6716); zxv for the two-pair root and paid fragments (#6726); +[@CubeJerry](https://github.com/CubeJerry) for #6805 (substantial OpenAI Codex assistance) and +the BIT pin it keeps; Ali Romman for the independent-helper basis mechanism, the exact caller +replay engines and native input lifting (#6349, with #6353 and #6372); DreamingOfClouds for +#6702, #6375 and #6824; the canonical-job adapters follow #6763. Cinna Davis, David Arias and +Gareth Davidson for native/caller predecessors; Jacob Alan Sussman for productive +recursion/compiler work; Cao Yifan, ywz65, Nick Petalas and all retained source authors for +interval and analytic work. Original notices, headers and the Apache-2.0 license are preserved. diff --git a/research/chain-root-global-ceiling/retained/RESEARCH-NOTES.md b/research/chain-root-global-ceiling/retained/RESEARCH-NOTES.md new file mode 100644 index 0000000000..933152d3fd --- /dev/null +++ b/research/chain-root-global-ceiling/retained/RESEARCH-NOTES.md @@ -0,0 +1,17 @@ +# Scope and boundaries of the chain-nested root + +The object is one exact caller for the unchanged #6824 native word. The frozen +heads and scope are in `TASK.json`. Notes of earlier steps stay as +`RESEARCH-NOTES-6824.md` and `RESEARCH-NOTES-6805.md`. + +The selected shape is `(9|9)`: every child has size one, so there are no binary +supplier nodes. `chain_root.py` is parametric in shape. `(4,4,1|1,4,4)` is built +in every replay as the gate. Only those two shapes are priced in this package; +the formula is not asserted for a shape it does not replay. + +The ordinary bases use pivots of absolute value one only, so all caller scalars +are integers (`ADD` coefficients in {±1, ±2, −3}, `SCALE` by −1). This raises the +gate count compared with a dyadic-pivot form and changes neither the invoice nor +the crossing. + +No exhaustive novelty search or optimality claim is made. diff --git a/research/chain-root-global-ceiling/retained/RESULT.json b/research/chain-root-global-ceiling/retained/RESULT.json new file mode 100644 index 0000000000..2e9c2183e8 --- /dev/null +++ b/research/chain-root-global-ceiling/retained/RESULT.json @@ -0,0 +1,2031 @@ +{ + "allocation": { + "allocation_sha256": "66baadfc8b2e6c4c268222add327335d4991c3f644893cded35a16800f89bea4", + "caller_main_fields": 2080, + "helper_boundary_normalizers": 20304, + "helpers_per_native_call": 564, + "native_helper_fields": 10152, + "native_owned_labels_per_call": 29, + "peak_owned_per_call": 14, + "sequential_thin_query_scratch": 1, + "total_independent_fields": 12232 + }, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "caller": { + "coefficients": 400, + "event_sha256": "03ecddfd75d0dbe325fcc489a50ae7657364482f0d887d81fa131ff6bf41fe70", + "events": 1237, + "inputs": 20, + "native_stages": 18 + }, + "caller_controls": { + "aliased_caller_inputs": "Distinct caller source and destination roles", + "aliased_native_inputs": "distinct valid native caller fields", + "deleted_add": "Every arbitrary-input forward coefficient", + "deleted_idle_one": "Every arbitrary-input forward coefficient", + "deleted_lambda": "Every arbitrary-input forward coefficient", + "deleted_local": "Every distinct native stage once", + "deleted_query": "Every arbitrary-input forward coefficient", + "grown_merged_idle": "Every arbitrary-input forward coefficient", + "independent_root_audit_wrong_line": "literal idle line phi", + "merged_idle_on_wrong_line": "Every arbitrary-input forward coefficient", + "shrunk_merged_idle": "Every arbitrary-input forward coefficient", + "unpaid_idle_in_invoice": "Formula and every emitted Gaussian request agree", + "wrong_phase_lambda": "Every arbitrary-input forward coefficient", + "wrong_phase_output_target": "Every arbitrary-input forward coefficient", + "wrong_phase_thin_query": "Every arbitrary-input forward coefficient", + "wrong_root_coefficient": "Sign Gram matrix" + }, + "caller_reverse": { + "coefficients": 400, + "rows": 20 + }, + "caller_scalars": { + "coefficient_height_units": 4304, + "event_census": { + "ADD": 690, + "IDLE_ONE": 16, + "LAMBDA": 62, + "LOCAL": 18, + "QUERY": 3, + "SCALE": 55, + "SWAP": 393 + }, + "max_scalar": "3", + "ordinary_lambdas": 62, + "per_instruction_envelope": 32, + "real_scalar_units_per_port": 7466, + "uncharged_gaussian_jobs": 0 + }, + "canonical_adapter_audit": { + "adapters": { + "idle_jobs": 1664, + "idle_two_axis_exchanges": 100464, + "main_jobs": 2080, + "main_nine_axis_basis_maps": 4160, + "main_phase_translations": 2080, + "main_two_axis_exchanges": 118144, + "payload_sha256": "71f54ad0ea7ee03a4cb52b7740c61cc1a83230ec84dc0794b011d6740ce19970", + "query_jobs": 312, + "query_nine_axis_basis_maps": 624, + "query_phase_translations": 312 + }, + "central_normalization": { + "central_characters": 4, + "rule": "Physical Gaussian maps tensor factorwise; ordinary scalar coefficients and lambda polynomials act on the total Q outside tensor powers.", + "two_factor_lambda_disagreement": true + }, + "controls": { + "aliased_native_helpers": "fresh native helper cannot alias an earlier public input", + "omitted_contact_phase": "full forward absolute phase", + "omitted_idle_adapter": "two adapters for every whole paid idle job", + "omitted_main_adapter": "adapter for every main input/output job", + "omitted_query_adapter": "adapters for every thin query" + }, + "ordinary": { + "caller_envelope": 82334720, + "caller_height_per_port": 5049, + "caller_scalar_upper_per_port": 17864, + "complete_scalar_budget": 1000000000, + "complete_scalar_upper": 488177792, + "growth_bound": "2^(10^9 + 166812*f), subject to retained physical precision/tape implementation rates", + "helper_normalizers_per_call": 1128, + "main_adapters_per_call": 208, + "main_input_output_adapter_and_normalizer_upper": 124438080, + "native_per_call_budget": 10000000, + "native_per_call_upper": 5680380, + "native_route_upper": 5396000, + "native_scalar_upper": 284380, + "ordinary_lambda_calls_per_port": 62, + "paid_rank_mass": 166812, + "route_rate_per_fixed_map": 1000, + "route_rate_status": "Retained rate applies to each native whole-job fixed map or each <=17-axis elementary map separately. Full153-axis main/idle permutations are decomposed and charged exchange by exchange; no blanket1000 charge for an arbitrary ambient map.", + "thin_query_adapter_upper": 936000, + "thin_query_scalar_upper": 4992, + "whole_idle_adapter_upper": 100464000 + }, + "physical": { + "contact_digest": "79930ec6c09a8e4930556c925c354bb5431203eaf069d9373f056049c061289b", + "contacts": 7488, + "dimension": 153, + "idle": { + "8": 208, + "16": 208, + "24": 208, + "32": 208, + "40": 208, + "48": 208, + "56": 208, + "64": 208 + }, + "main": { + "1": 104, + "9": 208, + "17": 208, + "25": 208, + "33": 208, + "41": 208, + "49": 208, + "57": 208, + "65": 208, + "73": 208, + "145": 104 + }, + "nonzero_contact_translations": 7488, + "output_translations": 2080 + } + }, + "changed_columns": { + "chart_pairs": [ + [ + 3, + 105 + ], + [ + 3, + 243 + ], + [ + 3, + 1051 + ], + [ + 105, + 127 + ], + [ + 105, + 246 + ], + [ + 105, + 430 + ], + [ + 105, + 755 + ], + [ + 105, + 1051 + ], + [ + 243, + 127 + ], + [ + 749, + 243 + ] + ], + "exact_columns": 5120, + "phase_controls": 10 + }, + "gate": { + "cancelling_pair": { + "per_side": 208, + "rank": 32 + }, + "events": 518, + "forward": { + "coefficients": 1024, + "event_sha256": "89130f542cd6e6212b950eab0c7e6c2cd937277da09695cf9901d04df9b56d2b", + "events": 518, + "inputs": 32, + "native_stages": 18 + }, + "max_merged_idle_stages": 5, + "reverse": { + "coefficients": 1024, + "rows": 32 + }, + "roles": 32, + "root": { + "fields": 8, + "full_sites": 6, + "idle_lines": 4, + "queries": 9, + "sign_gram_entries": 81, + "stage_supports": [ + 2, + 3, + 4, + 4, + 3, + 2 + ], + "thin_queries": 3 + } + }, + "independent_invoice": { + "caller_all_columns": { + "coefficients": 400, + "direction": "reverse adjoint", + "inputs": 20, + "ring": "Q(i)[q,C1,...,C18]/(q^4-1)" + }, + "controls": [ + { + "mutation": "price the retained #6726 caller under the new census", + "rejected": "complete final caller dimensions" + }, + { + "mutation": "omit one full native call", + "rejected": "all eighteen distinct forward native calls" + }, + { + "mutation": "reverse one thin-query orientation", + "rejected": "complete arbitrary-input caller column 0" + }, + { + "mutation": "alias one native source and destination", + "rejected": "injective full native public allocation" + }, + { + "mutation": "retain the old 563-helper allocation", + "rejected": "all independent helper roles" + } + ], + "correct_final_literal": "CALLER.json", + "counts": { + "ADD": 690, + "IDLE_ONE": 16, + "LAMBDA": 62, + "LOCAL": 18, + "QUERY": 3, + "SCALE": 55, + "SWAP": 393 + }, + "family": { + "fields": 20, + "idle_lines_read_from_word": 16, + "scope": "All-ones odd/odd shape; symbolic in every stage variable at the -1 central character; the +1 character is the diagonal product.", + "shadows": [ + "Q=1:+I", + "Q=-1:-I" + ], + "symbolic_entries": 400 + }, + "fields": { + "additional_helpers": 18, + "helper_fields": 10152, + "helpers_per_call": 564, + "invocations": [ + { + "dst": 0, + "extra_helper": 2643, + "helper_first": 2080, + "helper_last": 2643, + "src": 1, + "stage": 1 + }, + { + "dst": 0, + "extra_helper": 3207, + "helper_first": 2644, + "helper_last": 3207, + "src": 1, + "stage": 2 + }, + { + "dst": 0, + "extra_helper": 3771, + "helper_first": 3208, + "helper_last": 3771, + "src": 1, + "stage": 3 + }, + { + "dst": 0, + "extra_helper": 4335, + "helper_first": 3772, + "helper_last": 4335, + "src": 1, + "stage": 4 + }, + { + "dst": 0, + "extra_helper": 4899, + "helper_first": 4336, + "helper_last": 4899, + "src": 1, + "stage": 5 + }, + { + "dst": 0, + "extra_helper": 5463, + "helper_first": 4900, + "helper_last": 5463, + "src": 1, + "stage": 6 + }, + { + "dst": 0, + "extra_helper": 6027, + "helper_first": 5464, + "helper_last": 6027, + "src": 1, + "stage": 7 + }, + { + "dst": 0, + "extra_helper": 6591, + "helper_first": 6028, + "helper_last": 6591, + "src": 1, + "stage": 8 + }, + { + "dst": 0, + "extra_helper": 7155, + "helper_first": 6592, + "helper_last": 7155, + "src": 1, + "stage": 9 + }, + { + "dst": 0, + "extra_helper": 7719, + "helper_first": 7156, + "helper_last": 7719, + "src": 1, + "stage": 10 + }, + { + "dst": 0, + "extra_helper": 8283, + "helper_first": 7720, + "helper_last": 8283, + "src": 1, + "stage": 11 + }, + { + "dst": 0, + "extra_helper": 8847, + "helper_first": 8284, + "helper_last": 8847, + "src": 1, + "stage": 12 + }, + { + "dst": 0, + "extra_helper": 9411, + "helper_first": 8848, + "helper_last": 9411, + "src": 1, + "stage": 13 + }, + { + "dst": 0, + "extra_helper": 9975, + "helper_first": 9412, + "helper_last": 9975, + "src": 1, + "stage": 14 + }, + { + "dst": 0, + "extra_helper": 10539, + "helper_first": 9976, + "helper_last": 10539, + "src": 1, + "stage": 15 + }, + { + "dst": 0, + "extra_helper": 11103, + "helper_first": 10540, + "helper_last": 11103, + "src": 1, + "stage": 16 + }, + { + "dst": 0, + "extra_helper": 11667, + "helper_first": 11104, + "helper_last": 11667, + "src": 1, + "stage": 17 + }, + { + "dst": 0, + "extra_helper": 12231, + "helper_first": 11668, + "helper_last": 12231, + "src": 1, + "stage": 18 + } + ], + "main_fields": 2080, + "owned_first": 12232, + "owned_labels": 29, + "owned_last": 12260, + "public_fields": 12232, + "reserved_field_slots": 12262, + "thin_query_scratch": 12261 + }, + "final_claim_arithmetic": { + "alpha": "0.99999999983055693891274152410206657932682660110799240851912431527563737654014705838358829398612164968571876798", + "certification": "Parameter inequalities are exact rationals; moments are Decimal diagnostics. The raw lower endpoint is supplied by the primary exact interval certificate.", + "certified_lower": "16859002377/5000000000000", + "claim": "16859/5000000", + "compiler_gap": "1/20000000000", + "decay": "0.96875", + "delta": "0.87815513007455063064524638484272901890756430432451076687907790513226829454454869419229010392292784764748072748", + "eta": "1.0142534869934493480580729112892648840094471930355436232636140086693118656853925144518143091292715368119970391E-14", + "exact_finite_strictification": true, + "exact_rank_rounding": true, + "gamma": "0.94044252708617276892746622793738457409721204934678414386603075699315314118915405512105425161937987199584999870", + "lower_minus_tested": "627/5000000000000", + "one_minus_alpha": "1.6944306108725847589793342067317339889200759148087568472436262345985294161641170601387835031428123202E-10", + "reserve_slack_factor": "169443061087258475.89793342067317339889200759148087568472436262345985294161641170601387835031428123202", + "strictification_power": 1920, + "strictification_reserve": "1/1000000000000000000000000000", + "tested": "67436007/20000000000", + "theta_power": "4.3371903853167193168739585777461573256796887604736254848253642940568612912413458446482894901339356806016540945E-15" + }, + "inputs": { + "CALLER.json": "9a46d79125ea0bfab7112b46c4f907b00364c3ff3c47d2b3d078ea490e7ef4f6", + "CONTROLLER.json": "543b8728e659561b95e127dad7bd7534645996d7d2c61602bb5d89c89a73944c", + "DATA-PHASES.json": "c5916ff312678f12aba403847643fbbc29f643acec60bdf836fa56cd3e8251fa" + }, + "limitations": [ + "Native absolute phases and physical routes require the primary native verifier.", + "1000-unit route rate, owned erasure and other inherited framework assumptions remain.", + "No completion/compiler/outer admission is inferred from the Decimal root diagnostic." + ], + "main_targets": { + "1": 104, + "9": 208, + "17": 208, + "25": 208, + "33": 208, + "41": 208, + "49": 208, + "57": 208, + "65": 208, + "73": 208, + "145": 104 + }, + "new_diagnostic": { + "bracket": [ + "0.0033718004754967205688313924074708071440668997635641236687097987770406812879186207836266932720527930395036704282", + "0.0033718004754967205688313924074708071440668997635641236687097987770406812879186207836267447476286877197928518177" + ], + "certification": "High-precision Decimal diagnostic only; not an exact interval certificate.", + "claim": ".00337180", + "derivative_at_root": "-223865.68009239422643952422057577696181598422363997021534667902399381879862077023822025509179828110102858774669", + "margin_claim": "0.0001064473968341793098386675518173273186157739955670370482645042628495929692301107062019544576123885256432", + "margin_tested": "0.0000280944087066350103051058818284196502727210867245679195648473345593828583523730593823219899776619359763", + "precision": 110, + "raw_root": "0.0033718004754967205688313924074708071440668997635641236687097987770406812879186207836267190098407403796482611230", + "tested": ".00337180035" + }, + "old_diagnostic": { + "bracket": [ + "0.0033082345661431850190534925110834467550854556797096595186285914498853706706802458275221273722452506874234902037", + "0.0033082345661431850190534925110834467550854556797096595186285914498853706706802458275221788478211453677126715932" + ], + "certification": "High-precision Decimal diagnostic only; not an exact interval certificate.", + "claim": ".00337180", + "derivative_at_root": "-228204.01915141014377169241423399403253993974255982741887672953728700226230941514961935064272618454756366745714", + "margin_claim": "-14.5040325052022970876368588280944912858528051635689782203236481726179165729664868696828057940414091294774983", + "margin_tested": "-14.5041123561822772688846102863047522317913005179661518362723277866462304958622759215443186574649630609094019", + "precision": 110, + "raw_root": "0.0033082345661431850190534925110834467550854556797096595186285914498853706706802458275221531100331980275680808984", + "tested": ".00337180035" + }, + "ordinary": { + "budget": 1000000000, + "caller_actual_height_per_port": 4304, + "caller_actual_work_per_port": 7466, + "caller_envelope": 82334720, + "caller_maximum_scalar": "3", + "canonical_adapter_units": 225784000, + "canonical_adapters": { + "ambient_axes": 153, + "components": { + "idle_axis_swaps": 100464, + "idle_jobs": 1664, + "idle_phase_maps": 0, + "idle_q_basis_maps": 0, + "main_axis_swaps": 118144, + "main_jobs": 2080, + "main_phase_maps": 2080, + "main_q_basis_maps": 4160, + "query_axis_swaps": 0, + "query_jobs": 312, + "query_phase_maps": 312, + "query_q_basis_maps": 624 + }, + "elementary_maps": 225784, + "profiles": [ + { + "central": 0, + "kind": "idle", + "multiplicity": 208, + "negative": 0, + "rank": 8, + "swaps_per_side": 8 + }, + { + "central": 0, + "kind": "idle", + "multiplicity": 208, + "negative": 0, + "rank": 16, + "swaps_per_side": 16 + }, + { + "central": 0, + "kind": "idle", + "multiplicity": 208, + "negative": 0, + "rank": 24, + "swaps_per_side": 24 + }, + { + "central": 0, + "kind": "idle", + "multiplicity": 208, + "negative": 0, + "rank": 32, + "swaps_per_side": 32 + }, + { + "central": 0, + "kind": "idle", + "multiplicity": 208, + "negative": 0, + "rank": 40, + "swaps_per_side": 40 + }, + { + "central": 0, + "kind": "idle", + "multiplicity": 104, + "negative": 0, + "rank": 48, + "swaps_per_side": 33 + }, + { + "central": 0, + "kind": "idle", + "multiplicity": 104, + "negative": 0, + "rank": 48, + "swaps_per_side": 48 + }, + { + "central": 0, + "kind": "idle", + "multiplicity": 104, + "negative": 0, + "rank": 56, + "swaps_per_side": 25 + }, + { + "central": 0, + "kind": "idle", + "multiplicity": 104, + "negative": 0, + "rank": 56, + "swaps_per_side": 56 + }, + { + "central": 0, + "kind": "idle", + "multiplicity": 104, + "negative": 0, + "rank": 64, + "swaps_per_side": 17 + }, + { + "central": 0, + "kind": "idle", + "multiplicity": 104, + "negative": 0, + "rank": 64, + "swaps_per_side": 64 + }, + { + "central": 1, + "kind": "main", + "multiplicity": 104, + "negative": 1, + "rank": 1, + "swaps_per_side": 0 + }, + { + "central": 1, + "kind": "main", + "multiplicity": 208, + "negative": 1, + "rank": 9, + "swaps_per_side": 8 + }, + { + "central": 1, + "kind": "main", + "multiplicity": 208, + "negative": 1, + "rank": 17, + "swaps_per_side": 16 + }, + { + "central": 1, + "kind": "main", + "multiplicity": 208, + "negative": 1, + "rank": 25, + "swaps_per_side": 24 + }, + { + "central": 1, + "kind": "main", + "multiplicity": 208, + "negative": 1, + "rank": 33, + "swaps_per_side": 32 + }, + { + "central": 1, + "kind": "main", + "multiplicity": 208, + "negative": 1, + "rank": 41, + "swaps_per_side": 40 + }, + { + "central": 1, + "kind": "main", + "multiplicity": 104, + "negative": 1, + "rank": 49, + "swaps_per_side": 32 + }, + { + "central": 1, + "kind": "main", + "multiplicity": 104, + "negative": 1, + "rank": 49, + "swaps_per_side": 48 + }, + { + "central": 1, + "kind": "main", + "multiplicity": 104, + "negative": 1, + "rank": 57, + "swaps_per_side": 24 + }, + { + "central": 1, + "kind": "main", + "multiplicity": 104, + "negative": 1, + "rank": 57, + "swaps_per_side": 56 + }, + { + "central": 1, + "kind": "main", + "multiplicity": 104, + "negative": 1, + "rank": 65, + "swaps_per_side": 16 + }, + { + "central": 1, + "kind": "main", + "multiplicity": 104, + "negative": 1, + "rank": 65, + "swaps_per_side": 64 + }, + { + "central": 1, + "kind": "main", + "multiplicity": 104, + "negative": 1, + "rank": 73, + "swaps_per_side": 8 + }, + { + "central": 1, + "kind": "main", + "multiplicity": 104, + "negative": 1, + "rank": 73, + "swaps_per_side": 72 + }, + { + "central": 1, + "kind": "main", + "multiplicity": 104, + "negative": 1, + "rank": 145, + "swaps_per_side": 8 + }, + { + "central": 1, + "kind": "query", + "multiplicity": 312, + "negative": 1, + "rank": 1, + "swaps_per_side": 0 + } + ], + "q_bases_checked": 104, + "q_basis_address_checks": 53248, + "scope": "Exact coordinate permutations, q-basis inverses and multiplicity count. The 1000-unit rate is retained for each fixed native whole-job map or each elementary map supported on at most 17 specified axes; it is not a rate for an arbitrary 153-axis map." + }, + "contact_routes_per_call": 416, + "former_partial_raw_upper": 264473792, + "full_adapter_correction": 223704000, + "helper_normalizers_all_calls": 20304, + "helper_normalizers_per_call": 1128, + "lifetime_routes_per_call": 188, + "local_per_call": 5534352, + "local_routes": 5396000, + "local_scalar": 138352, + "local_upper_per_call": 10000000, + "main_adapters_per_call": 208, + "main_output_scalar_units": 54080, + "raw_counted": 407796128, + "raw_upper": 488177792, + "route_rate_status": "Retained physical/tape contract: 1000 per fixed native whole-job map or per <=17-axis elementary map; full 153-axis adapters are explicitly decomposed and charged.", + "superseded_flat_main_output_routes": 2080000, + "thin_query_work": 4992 + }, + "paid": { + "1": 40524, + "2": 8172, + "3": 8802, + "4": 1980, + "5": 2736, + "6": 126, + "7": 162, + "8": 226, + "16": 208, + "24": 208, + "32": 208, + "40": 208, + "48": 208, + "56": 208, + "64": 208 + }, + "paid_count": 64184, + "paid_delta": { + "1": 54, + "3": -18, + "4": 18, + "6": -18 + }, + "paid_rank_mass": 166812, + "raw_root_gain": "0.00006356590935353554977789989638736038898144408385446415008120732715531061723837495610456589980754235208", + "source_sha256": "e8c7a9d54d98a4cfa27e15593016b3908afed303e0f480076ed3f596192e5a4d", + "status": "PASS_INDEPENDENT_COMPLETE_CALLER_INVOICE", + "surplus": 760, + "target_count": 12232, + "target_delta": { + "4": 18, + "5": 18, + "7": 18, + "9": -36 + }, + "target_rank_mass": 167572, + "targets": { + "1": 356, + "2": 144, + "3": 72, + "4": 1962, + "5": 306, + "6": 54, + "7": 180, + "8": 720, + "9": 6670, + "17": 208, + "25": 208, + "33": 208, + "41": 208, + "49": 208, + "57": 208, + "65": 208, + "73": 208, + "145": 104 + }, + "whole_idle_paid": { + "8": 208, + "16": 208, + "24": 208, + "32": 208, + "40": 208, + "48": 208, + "56": 208, + "64": 208 + } + }, + "independent_native": { + "base": { + "all_coefficients": 640000, + "clear_nonzero": 45, + "copy_zero_checks": 1, + "events": 18577, + "helpers": { + "1": 14, + "2": 8, + "3": 4, + "4": 108, + "5": 16, + "6": 3, + "7": 9, + "8": 40, + "9": 361 + }, + "lifetimes": 47, + "opcodes": { + "ADD": 14153, + "CLEAR": 47, + "COPY": 1, + "INIT": 47, + "MOVE": 3454, + "SCALE": 875 + }, + "owned": 29, + "paid": { + "1": 2231, + "2": 454, + "3": 490, + "4": 109, + "5": 152, + "6": 8, + "7": 9, + "8": 1 + }, + "peak": 14, + "public": 771, + "scalar": 137990, + "total": 800 + }, + "candidate": { + "all_coefficients": 641601, + "clear_nonzero": 45, + "copy_zero_checks": 1, + "events": 18622, + "helpers": { + "1": 14, + "2": 8, + "3": 4, + "4": 109, + "5": 17, + "6": 3, + "7": 10, + "8": 40, + "9": 359 + }, + "lifetimes": 47, + "opcodes": { + "ADD": 14190, + "CLEAR": 47, + "COPY": 1, + "INIT": 47, + "MOVE": 3456, + "SCALE": 881 + }, + "owned": 29, + "paid": { + "1": 2234, + "2": 454, + "3": 489, + "4": 110, + "5": 152, + "6": 7, + "7": 9, + "8": 1 + }, + "peak": 14, + "public": 772, + "scalar": 138352, + "total": 801 + }, + "intermediate_sha256": "292b3ab3afb74e87deffd7770e5627e94debd610459221686c05ca04b8885d3f", + "lift": { + "added_events": 9, + "candidate": { + "all_coefficients": 641601, + "clear_nonzero": 45, + "copy_zero_checks": 1, + "events": 18622, + "helpers": { + "1": 14, + "2": 8, + "3": 4, + "4": 109, + "5": 17, + "6": 3, + "7": 10, + "8": 40, + "9": 359 + }, + "lifetimes": 47, + "opcodes": { + "ADD": 14190, + "CLEAR": 47, + "COPY": 1, + "INIT": 47, + "MOVE": 3456, + "SCALE": 881 + }, + "owned": 29, + "paid": { + "1": 2234, + "2": 454, + "3": 489, + "4": 110, + "5": 152, + "6": 7, + "7": 9, + "8": 1 + }, + "peak": 14, + "public": 772, + "scalar": 138352, + "total": 801 + }, + "controls": [ + { + "index": 9335, + "kind": "wrong coefficient", + "rejected": "complete endpoint column 556" + }, + { + "index": 9336, + "kind": "wrong coefficient", + "rejected": "complete endpoint column 664" + }, + { + "index": 9339, + "kind": "wrong coefficient", + "rejected": "complete endpoint column 664" + }, + { + "index": 9342, + "kind": "wrong coefficient", + "rejected": "complete endpoint column 664" + }, + { + "index": 18621, + "kind": "wrong coefficient", + "rejected": "complete endpoint column 664" + }, + { + "index": 18621, + "kind": "omission", + "rejected": "complete endpoint column 664" + }, + { + "index": 9335, + "kind": "omission", + "rejected": "complete endpoint column 556" + }, + { + "index": 9339, + "kind": "omission", + "rejected": "complete endpoint column 664" + }, + { + "kind": "birth frame restored without the edit", + "rejected": "scalar common chart" + }, + { + "kind": "aliased lifted helpers", + "rejected": "scalar common chart" + } + ], + "defects_before_delivery": { + "120": { + "556": "-1/2", + "664": "1" + }, + "179": { + "664": "1" + }, + "665": { + "664": "-1" + } + }, + "erased_values_unchanged": 47, + "intermediate_sha256": "292b3ab3afb74e87deffd7770e5627e94debd610459221686c05ca04b8885d3f", + "paid_delta": { + "1": 2, + "3": -1, + "4": 1, + "5": -1 + }, + "removed_events": 9, + "status": "PASS_INDEPENDENT_SHARED_CARRIER_LIFT", + "target_delta": { + "7": 1, + "9": -1 + } + }, + "limitations": [ + "Native phase/all-column replay not performed here.", + "Complete caller/outer invoice and uniform admission not performed here.", + "Exact rational normalized word and chronological interface audited." + ], + "paid_delta": { + "1": 3, + "3": -1, + "4": 1, + "6": -1 + }, + "source_sha256": "e8c7a9d54d98a4cfa27e15593016b3908afed303e0f480076ed3f596192e5a4d", + "split": { + "base": { + "all_coefficients": 640000, + "clear_nonzero": 45, + "copy_zero_checks": 1, + "events": 18577, + "helpers": { + "1": 14, + "2": 8, + "3": 4, + "4": 108, + "5": 16, + "6": 3, + "7": 9, + "8": 40, + "9": 361 + }, + "lifetimes": 47, + "opcodes": { + "ADD": 14153, + "CLEAR": 47, + "COPY": 1, + "INIT": 47, + "MOVE": 3454, + "SCALE": 875 + }, + "owned": 29, + "paid": { + "1": 2231, + "2": 454, + "3": 490, + "4": 109, + "5": 152, + "6": 8, + "7": 9, + "8": 1 + }, + "peak": 14, + "public": 771, + "scalar": 137990, + "total": 800 + }, + "candidate": { + "all_coefficients": 641601, + "clear_nonzero": 45, + "copy_zero_checks": 1, + "events": 18622, + "helpers": { + "1": 14, + "2": 8, + "3": 4, + "4": 109, + "5": 17, + "6": 3, + "7": 9, + "8": 40, + "9": 360 + }, + "lifetimes": 47, + "opcodes": { + "ADD": 14191, + "CLEAR": 47, + "COPY": 1, + "INIT": 47, + "MOVE": 3455, + "SCALE": 881 + }, + "owned": 29, + "paid": { + "1": 2232, + "2": 454, + "3": 490, + "4": 109, + "5": 153, + "6": 7, + "7": 9, + "8": 1 + }, + "peak": 14, + "public": 772, + "scalar": 138374, + "total": 801 + }, + "controls": [ + { + "index": 0, + "kind": "omission", + "rejected": "complete endpoint column 383" + }, + { + "index": 12, + "kind": "omission", + "rejected": "complete endpoint column 3" + }, + { + "index": 12385, + "kind": "omission", + "rejected": "scalar common chart" + }, + { + "index": 12386, + "kind": "omission", + "rejected": "complete endpoint column 3" + }, + { + "index": 12394, + "kind": "omission", + "rejected": "complete endpoint column 66" + }, + { + "index": 12395, + "kind": "omission", + "rejected": "complete endpoint column 66" + }, + { + "index": 12404, + "kind": "omission", + "rejected": "scalar common chart" + }, + { + "index": 18609, + "kind": "omission", + "rejected": "complete endpoint column 3" + }, + { + "index": 18621, + "kind": "omission", + "rejected": "complete endpoint column 383" + }, + { + "kind": "unearned old target", + "rejected": "complete exits" + } + ], + "copy_zero_guard_checked": true, + "exact_pairings": true, + "limitations": [ + "Native phase/all-column replay not performed here.", + "Complete caller/outer invoice and uniform admission not performed here.", + "Exact rational normalized word and chronological interface audited." + ], + "new_native_chart_pairs": [ + [ + 749, + 243 + ] + ], + "paid_delta": { + "1": 1, + "5": 1, + "6": -1 + }, + "source_sha256": "e8c7a9d54d98a4cfa27e15593016b3908afed303e0f480076ed3f596192e5a4d", + "status": "PASS_INDEPENDENT_PAID_HELPER368_SPLIT", + "target_delta": { + "4": 1, + "5": 1, + "9": -1 + }, + "zero_clear_pattern_preserved": true + }, + "status": "PASS_INDEPENDENT_SHARED_CARRIER_INPUT_LIFT", + "target_delta": { + "4": 1, + "5": 1, + "7": 1, + "9": -2 + } + }, + "independent_root": { + "fields": 20, + "idle_lines_read_from_word": 16, + "scope": "All-ones odd/odd shape; symbolic in every stage variable at the -1 central character; the +1 character is the diagonal product.", + "shadows": [ + "Q=1:+I", + "Q=-1:-I" + ], + "symbolic_entries": 400 + }, + "lift_controls": [ + { + "mutation": "wrong coefficient at edit 5 event 1", + "rejected": "('endpoint', 120, {120: Fraction(1, 1), 556: Fraction(1, 2), 8: Fraction(1, 1)}," + }, + { + "mutation": "wrong coefficient at edit 5 event 2", + "rejected": "('endpoint', 120, {120: Fraction(1, 1), 664: Fraction(-1, 1), 8: Fraction(1, 1)}" + }, + { + "mutation": "wrong coefficient at edit 6 event 0", + "rejected": "('endpoint', 179, {179: Fraction(1, 1), 664: Fraction(-2, 1), 67: Fraction(1, 1)" + }, + { + "mutation": "wrong coefficient at edit 6 event 3", + "rejected": "('endpoint', 138, {138: Fraction(1, 1), 664: Fraction(1, 1), 26: Fraction(1, 1)}" + }, + { + "mutation": "wrong coefficient at edit 11 event 0", + "rejected": "('endpoint', 665, {665: Fraction(1, 1), 664: Fraction(-1, 1)}, {665: Fraction(1," + }, + { + "mutation": "missing final repair", + "rejected": "('endpoint', 665, {665: Fraction(1, 1), 664: Fraction(1, 1)}, {665: Fraction(1, " + }, + { + "mutation": "aliased lifted helpers", + "rejected": "('move current', 9341, ['MOVE', 664, 3, 1051, False], 1051)" + }, + { + "mutation": "stale bound source event", + "rejected": "('Bound deleted source events', 768)" + }, + { + "mutation": "missing carrier delivery", + "rejected": "('endpoint', 120, {120: Fraction(1, 1), 556: Fraction(-1, 2), 8: Fraction(1, 1)}" + } + ], + "local": { + "COPY": 1, + "endpoint_coefficients": 641601, + "erased": [ + { + "event": 8393, + "frame": 1091, + "role": 800 + }, + { + "event": 8552, + "frame": 529, + "role": 797 + }, + { + "event": 8672, + "frame": 541, + "role": 799 + }, + { + "event": 8803, + "frame": 549, + "role": 798 + }, + { + "event": 9036, + "frame": 737, + "role": 772 + }, + { + "event": 9055, + "frame": 1031, + "role": 794 + }, + { + "event": 9061, + "frame": 597, + "role": 775 + }, + { + "event": 9083, + "frame": 598, + "role": 788 + }, + { + "event": 9084, + "frame": 394, + "role": 776 + }, + { + "event": 9110, + "frame": 599, + "role": 786 + }, + { + "event": 9111, + "frame": 260, + "role": 777 + }, + { + "event": 9138, + "frame": 600, + "role": 790 + }, + { + "event": 9139, + "frame": 431, + "role": 778 + }, + { + "event": 9161, + "frame": 595, + "role": 774 + }, + { + "event": 9174, + "frame": 601, + "role": 792 + }, + { + "event": 9183, + "frame": 470, + "role": 779 + }, + { + "event": 9213, + "frame": 115, + "role": 796 + }, + { + "event": 9218, + "frame": 3, + "role": 780 + }, + { + "event": 9236, + "frame": 595, + "role": 780 + }, + { + "event": 10919, + "frame": 593, + "role": 772 + }, + { + "event": 10920, + "frame": 594, + "role": 773 + }, + { + "event": 11099, + "frame": 549, + "role": 793 + }, + { + "event": 11561, + "frame": 117, + "role": 795 + }, + { + "event": 12296, + "frame": 245, + "role": 796 + }, + { + "event": 12321, + "frame": 470, + "role": 791 + }, + { + "event": 12331, + "frame": 260, + "role": 785 + }, + { + "event": 12334, + "frame": 1091, + "role": 782 + }, + { + "event": 12340, + "frame": 431, + "role": 789 + }, + { + "event": 12356, + "frame": 394, + "role": 787 + }, + { + "event": 12357, + "frame": 240, + "role": 783 + }, + { + "event": 12366, + "frame": 1090, + "role": 781 + }, + { + "event": 12376, + "frame": 243, + "role": 784 + }, + { + "event": 17840, + "frame": 127, + "role": 780 + }, + { + "event": 17841, + "frame": 127, + "role": 779 + }, + { + "event": 17842, + "frame": 127, + "role": 778 + }, + { + "event": 17843, + "frame": 127, + "role": 777 + }, + { + "event": 17844, + "frame": 127, + "role": 776 + }, + { + "event": 17845, + "frame": 127, + "role": 775 + }, + { + "event": 17846, + "frame": 127, + "role": 774 + }, + { + "event": 17847, + "frame": 127, + "role": 773 + }, + { + "event": 17848, + "frame": 127, + "role": 772 + }, + { + "event": 17920, + "frame": 127, + "role": 783 + }, + { + "event": 17921, + "frame": 127, + "role": 782 + }, + { + "event": 17922, + "frame": 127, + "role": 781 + }, + { + "event": 18579, + "frame": 127, + "role": 785 + } + ], + "events": 18622, + "helpers": { + "1": 14, + "2": 8, + "3": 4, + "4": 109, + "5": 17, + "6": 3, + "7": 10, + "8": 40, + "9": 359 + }, + "lifetimes": 47, + "owned_fields": 29, + "owned_lifetimes": 47, + "paid": { + "1": 2234, + "2": 454, + "3": 489, + "4": 110, + "5": 152, + "6": 7, + "7": 9, + "8": 1 + }, + "peak": 14, + "peak_owned_fields": 14, + "public": 772, + "public_inputs": 772, + "real_scalar_allowance": 138352, + "scalar": 138352 + }, + "merged_idle_stage_sizes": [ + 1, + 1, + 2, + 2, + 3, + 3, + 4, + 4, + 5, + 5, + 6, + 6, + 7, + 7, + 8, + 8 + ], + "native": { + "distinct_maps": 2940, + "helper_normalizers": 1128, + "helpers": { + "1": 14, + "2": 8, + "3": 4, + "4": 109, + "5": 17, + "6": 3, + "7": 10, + "8": 40, + "9": 359 + }, + "main_adapters": 208, + "proof": "Every signed Pauli image and exact global phase; frame induction at every positive tensor width", + "recipe_payload_sha256": "36402baafb22367dc3eab075ee099e85a53d3b691c68fa37238784993cb9ee57", + "wrong_phase_rejected": true + }, + "native_payload_sha256": "d3ccfce7bdbca3b79771844e6c9fee48f1a8066444a19218995648df96982821", + "physical": { + "central_square_columns": 53248, + "central_translations": 0, + "full_calls": 18, + "main_targets": { + "1": 104, + "9": 208, + "17": 208, + "25": 208, + "33": 208, + "41": 208, + "49": 208, + "57": 208, + "65": 208, + "73": 208, + "145": 104 + }, + "new_paid_jobs": 0, + "ordinary_normalizations": 62, + "physical_contacts": 7488, + "ports": 104, + "route_payload_sha256": "79930ec6c09a8e4930556c925c354bb5431203eaf069d9373f056049c061289b", + "tensor_rule": "Factorwise native maps; scalar signs stay outside the tensor power.", + "whole_idle_jobs": { + "8": 208, + "16": 208, + "24": 208, + "32": 208, + "40": 208, + "48": 208, + "56": 208, + "64": 208 + } + }, + "price": { + "compiler": { + "H": 2138900000000000, + "N": "2^2138900000000000", + "eta": { + "lower": "0.000000000000010142534869934493", + "upper": "0.000000000000010142534869934494" + }, + "gap": "1/20000000000", + "integer_test_exponent": 106945, + "logarithm_power": 2100, + "theta": "63/64", + "uniform_saving": "33718003/10000000000", + "word_materialized": false + }, + "counts": { + "ADD": 690, + "IDLE_ONE": 16, + "LAMBDA": 62, + "LOCAL": 18, + "QUERY": 3, + "SCALE": 55, + "SWAP": 393 + }, + "derivative_upper": "-692881893214203006943552510187332683389021327395539132093675795/3138550867693340381917894711603833208051177722232017256448", + "full_calls": 18, + "gate_margins": { + "lower": { + "first": { + "lower": "0.000000000726834149080815866013", + "upper": "0.000000000726834149080815866014" + }, + "second": { + "lower": "0.000000000726834149080815866013", + "upper": "0.000000000726834149080815866014" + } + }, + "upper": { + "first": { + "lower": "-0.000000001555206042433268905496", + "upper": "-0.000000001555206042433268905495" + }, + "second": { + "lower": "-0.000000001555206042433268905496", + "upper": "-0.000000001555206042433268905495" + } + } + }, + "kappa": "16859/5000000", + "local_lift_gain": { + "claim": { + "derivative_lower_bound": 0.0006641197235243467, + "interval": { + "lower": "0.001154067469144513540027774281", + "upper": "0.001154067469144513540027774282" + } + }, + "g_prime_at_1": { + "lower": "-0.355801168943512837525269655271", + "upper": "-0.355801168943512837525269655270" + }, + "second_derivative_majorant": 94.2156738216584, + "tested": { + "derivative_lower_bound": 0.000664119736868007, + "interval": { + "lower": "0.001154067584223029650505201420", + "upper": "0.001154067584223029650505201421" + } + } + }, + "nonrecursive": { + "actual_scalar_height_per_port": 4304, + "actual_scalar_work_per_port": 7466, + "all_main_input_output_adapters_and_normalizers": 124438080, + "caller_gate_passes": 82334720, + "canonical_adapter_rate": 1000, + "elementary_canonical_maps": 225784, + "local_per_call_counted": 5534352, + "local_per_call_upper": 10000000, + "local_routes": 5396000, + "local_scalar": 138352, + "maximum_literal_scalar": "3", + "native_invocations": 18, + "native_owned_labels": 29, + "native_owned_lifetimes": 47, + "native_public_inputs": 772, + "paid_rank_mass": 166812, + "peak_owned_fields": 14, + "query_adapter_work": 936000, + "raw_budget": 1000000000, + "raw_scalar_upper": 488177792, + "scalar_denominator_bits": 7, + "scalar_growth_bound": "At most 2^(10^9+R*f), R the recounted complete paid rank mass; inherited physical precision/tape rates remain assumptions.", + "scalar_numerator_bits": 8, + "thin_owned_contract": "One uncredited copied-query stream reused sequentially, cleared on return; no new helper credit.", + "thin_query_work": 4992, + "whole_idle_adapter_work": 100464000 + }, + "ordinary_BIT": { + "admitted": "17/5000", + "after_cover": "69/20000", + "atom": "1/250", + "before_cover": "3459/1000000", + "ordinary_saving": "8590884599/2500000000000", + "prime_rule": "odd q > 2^26*N^5 avoiding all fixed denominators and rank witnesses" + }, + "outer": { + "functional_checks": { + "actual_new_BIT_stock_sublinear": "4979999999253/5000000000000", + "fixed_halo_explicit_metadata_branch": "385000000001/5000000000", + "new_BIT_row_stock_sublinear_in_active_group": "19939999997009/20000000000000", + "new_semantic_group_guard": "3/20000000000" + }, + "margins": { + "boundary_algebraic_matrix": "1348720079932563997/400000000000000000000", + "fused_gaussian": "1348720079797691991/400000000000000000000", + "global_coordinate_router": "16859001/5000000000", + "group_bit_router": "337180024949422997/100000000000000000000", + "group_scans": "9999999999/10000000000", + "main_transform": "1348720059932563997/400000000000000000000", + "microbox_face_corrections": "385000000001/5000000000", + "polynomial_products": "19999999999/20000000000", + "sparse_union_movement": "163848720079932563997/400000000000000000000" + }, + "parameters": { + "a": "16859001/5000000000", + "b": "13487201/4000000000", + "beta": "19999999997/20000000000", + "bit_saving": "17/5000", + "cap_xi": "363848720059932563997/400000000000000000000", + "complex_uniform_saving": "33718003/10000000000", + "d": "1/20000000000", + "epsilon": "19999999999/20000000000", + "kappa": "16859/5000000", + "lambda_": "39865127993/40000000000", + "lambda_prime": "19932563997/20000000000", + "layout": "1/20000000000", + "q": "67436003/20000000000", + "r0": "1/200000000000", + "stop": "1/20000000000", + "tested_saving": "67436007/20000000000" + }, + "strict_checks": { + "actual_bit_above_effective": "140999/5000000000", + "actual_logarithmic_gamma_guard": "1/20000000000", + "actual_logarithmic_group_guard": "36151279970067436003/200000000000000000000", + "alpha_logarithm_absorption": "1/200000000000", + "boundary_algebraic_matrix_above_kappa": "79932563997/400000000000000000000", + "cap_above_band": "163848720059932563997/400000000000000000000", + "cap_below_cell": "36151279920067436003/400000000000000000000", + "cap_below_phase_cell_power": "436151279940067436003/400000000000000000000", + "complex_above_effective": "1/20000000000", + "complex_below_one_over_32": "111512799/4000000000", + "complex_endpoint": "1/10000000000", + "epsilon_below_one": "1/20000000000", + "epsilon_positive": "19999999999/20000000000", + "fine_prime_halo_umbrella": "7/2", + "fused_gaussian_above_kappa": "79797691991/400000000000000000000", + "gaussian_above_main": "9932563997/200000000000000000000", + "global_coordinate_router_above_kappa": "1/5000000000", + "global_gamma_power_slack": "9/200000000000", + "group_below_dimension": "1/10000000000", + "group_bit_router_above_kappa": "24949422997/100000000000000000000", + "group_gauge_power_slack": "36151279969067436003/200000000000000000000", + "group_key_fits_record": "1/10000000000", + "group_positive": "19999999997/20000000000", + "group_scans_above_kappa": "9966281999/10000000000", + "halo_covers_generic_inverse_radius": "5", + "improvement_over_user_baseline": "820414790400418148631/500000000000000000000000", + "lambda_above_internal": "1/40000000000", + "lambda_above_sigma": "3/40000000000", + "lambda_above_tau": "1/40000000000", + "lambda_prime_above_lambda": "1/40000000000", + "lambda_prime_above_leaf": "7986512799/80000000000000000000", + "leaf_saving_above_effective": "3986512799/80000000000000000000", + "main_transform_above_kappa": "59932563997/400000000000000000000", + "membership_arithmetic_fits_record": "1/20000000000", + "microbox_face_corrections_above_kappa": "384983141001/5000000000", + "microbox_halo_volume": "1580000000003/20000000000", + "new_complex_uniform_saving_above_b": "1/20000000000", + "new_semantic_guard_with_C1_one": "1/20000000000", + "polynomial_products_above_kappa": "19932563999/20000000000", + "positive_layout_slack": "1/20000000000", + "q_below_effective": "1/20000000000", + "q_below_internal": "1/20000000000", + "q_below_leaf": "7986512799/80000000000000000000", + "q_positive": "67436003/20000000000", + "short_record_fallback": "3986512799/4000000000", + "source_axis_superpolynomial": "1/20000000000", + "sparse_union_movement_above_kappa": "162500000079932563997/400000000000000000000", + "stop_below_one": "19999999999/20000000000", + "stop_positive": "1/20000000000", + "strassen_integer_power_gap": "1951441519231", + "support_router_span": "3/20000000000", + "theta_positive_polynomial_power": "2", + "union_header_fits_record": "3/20000000000", + "union_tag_work_per_visit_fits_record": "3/20000000000" + } + }, + "paid": { + "1": 40524, + "16": 208, + "2": 8172, + "24": 208, + "3": 8802, + "32": 208, + "4": 1980, + "40": 208, + "48": 208, + "5": 2736, + "56": 208, + "6": 126, + "64": 208, + "7": 162, + "8": 226 + }, + "paid_calls": 64184, + "productive_fields": 12232, + "rank_mass_surplus": 760, + "raw_endpoint_margins": { + "lower": { + "first": { + "lower": "0.000000021652415920367122927871", + "upper": "0.000000021652415920367122927872" + }, + "second": { + "lower": "0.000000021652415920367122927871", + "upper": "0.000000021652415920367122927872" + } + }, + "tested": { + "first": { + "lower": "0.000028094408706635010305105881", + "upper": "0.000028094408706635010305105882" + }, + "second": { + "lower": "0.000028094408706635010305105881", + "upper": "0.000028094408706635010305105882" + } + }, + "upper": { + "first": { + "lower": "-0.000000000734152088876528992982", + "upper": "-0.000000000734152088876528992981" + }, + "second": { + "lower": "-0.000000000734152088876528992982", + "upper": "-0.000000000734152088876528992981" + } + } + }, + "raw_root_interval": [ + "16859002377/5000000000000", + "6743600951/2000000000000" + ], + "scope": "Complete conditional price, requiring the supplied caller/native/physical inputs to be independently verified by the package. Does not itself verify those scientific inputs, discharge inherited assumptions, establish scientific admission, or change selected kappa.", + "source_assumptions": [ + "native_all_columns", + "owned_erasure", + "compiler", + "precision_tape", + "analytic_recovery" + ], + "status": "PASS_CHAIN_ROOT_COMPLETE_PRICE", + "strictification": { + "alpha": { + "lower": "0.999999999830556938912741524102", + "upper": "0.999999999830556938912741524103" + }, + "alternative_12_13_delta": { + "lower": "0.951055657856496842455443014224", + "upper": "0.951055657856496842455443014225" + }, + "cutoff": 11, + "decay": "31/32", + "delta": { + "lower": "0.878155130074550630645246384842", + "upper": "0.878155130074550630645246384843" + }, + "floor": 12, + "gamma": { + "lower": "0.940442527086172768927466227937", + "upper": "0.940442527086172768927466227938" + }, + "normalized_upper": "3017994256268166165656485281090535833916725756249835826793168925266538363332959118393649803728007713071868113265307008106165392759140166602231276176491193525838475223532850199880731698633371358238213826956369837083963326200431097200800059212002041494173164580120900614899652164774721219753022318014007470888704725853928034427162119973960367601209478471989008174546718847765864454317363747477784577139342980703179986004309023923501151623437162530359093275767500999488838821346878653618781517869929465644907239975200419119984961970595462459526672982124367238370081601117105862824672041626753878830761254937716087757500154780588952387888909545290321227690737337524636932986557487436400373746205087976939900823213412721260929246663645454333225533573417873878270966410674662217721400378580963662781229070699131856088606565064212802338219990676288305134052916065084223147113356681924295487922738831215975490003477881714792514602632531440142922321624246055420491548898870125266739034093403593861141750778390494324332020450631341177712407686809708639299932057929638453229385512844824477732475692497750505444293920505764644542985604027374525776713590758593290162240025857956398750701666193022661852817667334597363657250589474692558349187489784467784534308731452271464397192747555883724086986777180899255693019165197216450482165724399715348781376527863867611187937883511375183145576545939665590528177825191075315987382691696850289161949978761392853761291967438188096278517378245173041891296537114442099549460376841596189745440833356287809630492771955137857634049834843653214091059292899519993358715592551812122459678957257644252935128182771018674930860159078110203035231337278094843484497916736350269707423093669550405734836572742921142951535393569858677867578133947031681172583200575479732465576021412092436521998625141581486036597822439583555666166745205320062026011722745440952026157246983262052059609825801393194410107883674103170530206478790180680714175502948412787907330283634638118487371874649400893019006973397690500854473558401410620066158504863840613720936860712364614948768923065861574183333307699013929391851014406823186488763212430120437839480440610837443358734496436725017143197692415864041146359723246618363560963819742888006979937806707306886174644458636649893987953661905408261128055990516804739016024589981864256774788678522533600952517642689837813239015716470408358110154664695932620834322254734702246799101912684700303071151259570508727219713769405640694001219420631583405431371328147136055604276355342139039717035227877070657992677340778068793172328267591969261818125572871429869776365422773264912163077459311734702664754097848257207856647246563827576845151038301927915239078395646743310244244155118166302363634508949033003228555802638863720922802000624281277831431518083189590917186076428068361094207669086175823390707236441303930595597471590743181212100815143003489643346003177743777109770019130060803/3017994256268166165656491035063231693978398198787662079292383856990261666407268875266242316574304537824977438191233479479458365031897378910971682146847445831720529072444214239168813318361621021406537946333680719615698024395371618102654358301049375281526841923857353573281673124064137091623117665711938327458485803660406333782965399496384383273095619410140572062880895086412530676628570584973212341168338281143028843950725406810633018143519244412367157868500306391027430062953886066530011236452104054839696367657745585918153885105780436048055657351661582204778498269871018672509355754914642085687953169998781802659556167514409844216442138601869761940829666175939688866382484459348199377852059421048193136784272717556196313275587819271746647782752170997852125936391824736948646408133578263515625097682264701444334863759885223671808566007730417996869975879739069454556143502120678264337509191926420012606685608884721586159182735130329668235415015963539054143635378351553686650970085356070224050653205542765090703090192316158855819021850534846977519598595533227830830246675689299329067321128120764882495087257572668033863484660711961342702904922213132750672072529152647888921228554709611752116990888073427706144475582044612115354682916594199797791656758577997812612859332705485501315354164119374880954187452894641323180493161306005328627998639574009593540018002942935225879243521624482714761491136882238301907421656901587458169137534644297058714160255428538828222202270811680920184952032574111855818083323277337278951405159580396757098165528221317354723301942624608396313954059588718689633657419267824337962870655097477792938701413070284409091728049161298086123657787538745786057964843136234985017216030339846107466138423974925847895769642910846794142281362603017916752544796963565984849849769996708882692849515677511148222363661619367929957200111877107796960360666023556235009225611283531158403466647070581796672289974955924592777874597248446634937752574338785626877802036415577528724311421788748071123754637157691654232143301862938534179856363952063049872889542807412729837987869412746960678402767893645902016662880136171621266241700457558973760850667075103664334887633217911261504764438100508653101640059777972182615479323091990380294461729182853447358074876266516119635874601565061925989878395715844229089983460650371889224631036383672785343069536106257115040353041502759057432703560960094331869105852264578209033293234613213545309635230759049012769406664208577367799088589327982198040102650366683636258605290168036200739803674673414801290054883467223756247682810755116873536560345525083453513230497496834726668274182638946137769521096245230638941858893368170523070080321656837850831035321029960872976160298639386627768204700263664703090321168443994619637219281963172814020726543678137155435815999103603309013053863875221052240416961763005709684412496621711854336662627914279975977381641466926443784930454019244032", + "offset": "1/7", + "power": 1920, + "reserve": "1/1000000000000000000000000000" + }, + "targets": { + "1": 356, + "145": 104, + "17": 208, + "2": 144, + "25": 208, + "3": 72, + "33": 208, + "4": 1962, + "41": 208, + "49": 208, + "5": 306, + "57": 208, + "6": 54, + "65": 208, + "7": 180, + "73": 208, + "8": 720, + "9": 6670 + }, + "tested": "67436007/20000000000", + "thin_queries": 3, + "whole_idle_jobs": 1664 + }, + "retained_caller": { + "independent": { + "inputs_sha256": { + "CALLER-ONE-RETIRED.json": "8d7889e817faf1bbf81bb4ed681db039df6e26ecdab5555dff60c3d0e4309030", + "CALLER-UNRETIRED.json": "8693f74b4559c27dd670f788c6e8c7be8bc7cf9cd6a6abb80455fee86d20bc99", + "CONTROLLER.json": "543b8728e659561b95e127dad7bd7534645996d7d2c61602bb5d89c89a73944c", + "RETIREMENT-WITNESSES.json": "272534848a8fe8a9fd523f4daf2747b24a6b26eb9a848d27cafcb22a2e718136" + }, + "negative_controls": { + "final_return": "Independent forward column 5", + "first_handoff": "Independent forward column 4", + "first_input": "Independent reverse row 6", + "omitted_ADD": "Independent forward column 4", + "omitted_IDLE": "Independent forward column 0", + "omitted_IDLE_ONE": "Independent forward column 0", + "omitted_LAMBDA": "Independent forward column 0", + "omitted_LOCAL": "All distinct stages exactly once", + "omitted_QUERY": "Independent forward column 0", + "second_handoff": "Independent forward column 4", + "unearned_head_32": "Independent forward column 32", + "unearned_head_33": "Independent forward column 33", + "unearned_head_6": "Independent forward column 6", + "wrong_cut_normalizer": "Independent forward column 4" + }, + "pairs": [ + { + "all_coefficients": "exact Laurent/Gaussian", + "cut_after": 158, + "dual_pairings": "1", + "head": 0, + "odd_denominators": false, + "pivot": 6, + "prefix_stages": [ + 5, + 6, + 7, + 8 + ] + }, + { + "all_coefficients": "exact Laurent/Gaussian", + "cut_after": 394, + "dual_pairings": "1", + "head": 1, + "odd_denominators": false, + "pivot": 4, + "prefix_stages": [ + 10 + ] + } + ], + "scope": "Exact all-input caller algebra and dyadic witnesses. Physical/native/finite/outer assumptions are separate.", + "status": "PASS_INDEPENDENT_TWO_PAID_FRAGMENTS", + "word": { + "events": 606, + "forward_coefficients": 1156, + "independent_body_variables": 18, + "inputs": 34, + "reverse_coefficients": 1156 + } + }, + "largest_merged_idle_stages": 5, + "replay": { + "coefficients": 1156, + "event_sha256": "ba02566c7111830d358831871301af8d1d3cd6bfe8b9155bbde4db29f3c5265a", + "events": 606, + "inputs": 34, + "native_stages": 18 + }, + "root": { + "common_idle_pairs": 2, + "fields": 8, + "full_sites": [ + 0, + 1, + 2, + 6, + 7, + 8 + ], + "multilinear_stage_and_character_checks": 128, + "stage_ranks": [ + 2, + 4, + 4, + 4, + 4, + 2 + ] + } + }, + "root": { + "fields": 20, + "full_sites": 18, + "idle_lines": 16, + "queries": 21, + "sign_gram_entries": 441, + "stage_supports": [ + 2, + 3, + 4, + 5, + 6, + 7, + 8, + 9, + 10, + 10, + 9, + 8, + 7, + 6, + 5, + 4, + 3, + 2 + ], + "thin_queries": 3 + }, + "selected_frontier_changed": false, + "status": "PASS_CHAIN_NESTED_ROOT" +} diff --git a/research/chain-root-global-ceiling/retained/chain_root.py b/research/chain-root-global-ceiling/retained/chain_root.py new file mode 100644 index 0000000000..ca1e0244f1 --- /dev/null +++ b/research/chain-root-global-ceiling/retained/chain_root.py @@ -0,0 +1,239 @@ +"""Chain-nested shortest root and its literal caller; deterministic, no search at replay. + +DreamingOfClouds with Claude Opus 5.5 (Anthropic), via Claude Code. Apache-2.0. +The binary query supplier and the ordinary-basis elimination follow the retained +caller by Cinna Davis, Ali Romman, thu-nmrc and zxv (retained/caller/caller.py); +whole common idles follow thu-nmrc (#6716). + +Shape: child sizes sL (outer to centre) and sR (centre to outer). Fields are A, +f_0..f_{gL-1}, h_0..h_{gR-1} and, when the count is odd, one empty field E. +""" +from collections import Counter +from copy import deepcopy +from fractions import Fraction as Q +from algebra import add,eye,inverse,multiply,need + +SHAPE=([1]*9,[1]*9) +GATE=([4,4,1],[1,4,4]) + +def unit(q): + # Integral form: pivots are +-1 only, so the ordinary caller has integer scalars. + return Q(q) in (1,-1) + +def fields(sL,sR): + gL,gR=len(sL),len(sR) + nf=1+gL+gR;e=nf%2 + return {'n':nf+e,'A':0,'f':list(range(1,1+gL)),'h':list(range(1+gL,1+gL+gR)),'E':nf if e else None} + +def vector(n,*pairs): + v=[Q(0)]*n + for i,c in pairs:v[i]+=Q(c) + return v + +def thin_vectors(sL,sR): + """Closed-form thin queries, ordered; see PROOF.md section 2.""" + F=fields(sL,sR);n,A,f,h,E=F['n'],F['A'],F['f'],F['h'],F['E'] + def vec(a,u,p=0,q=0): + x=[Q(0)]*n;y=[Q(0)]*n + x[A]=Q(a);y[A]=Q(u) + for i,j in enumerate(f):x[j]=Q(a+1);y[j]=Q((1-u)*(-1)**i) + for r,j in enumerate(reversed(h)):x[j]=Q(1-a);y[j]=Q((u-1)*(-1)**r) + if E is not None:x[E]=Q(q);y[E]=Q(p) + return x,y + a,b=len(f)%2,len(h)%2 + if a and b:return [vec(0,1,0,1),vec(-1,2,1,0),vec(-1,3,1,-1)] + if not a and not b:return [vec(0,1,0,1),vec(-1,0,1,0),vec(-1,-1,1,-1)] + if a:return [vec(0,1),vec(-1,0)] + return [vec(0,1),vec(1,2)] + +def sites(sL,sR): + """Ordered root: (x,y,mask or None,kind,index).""" + F=fields(sL,sR);n,A,f,h=F['n'],F['A'],F['f'],F['h'] + out=[] + for i in range(len(f)): + x=vector(n,(A,1),(f[i],1),*[(f[j],2) for j in range(i)]) + y=vector(n,(A,1),(f[i],-1)) + out.append((x,y,{A,*f[:i+1]},'L',i)) + for j,(x,y) in enumerate(thin_vectors(sL,sR)):out.append((x,y,None,'Q',j)) + for m in range(len(h)): + x=vector(n,(A,-1),(h[m],1),*[(h[l],2) for l in range(m+1,len(h))]) + y=vector(n,(A,1),(h[m],1)) + out.append((x,y,{A,*h[m:]},'R',m)) + return out + +def lines(sL,sR): + """Idle lines: (phi,gamma,sites-of-group covered,side).""" + F=fields(sL,sR);n,A,f,h=F['n'],F['A'],F['f'],F['h'] + out=[] + for j in range(1,len(f)): + out.append((vector(n,(f[j-1],1)),vector(n,(f[j-1],1),(A,-2)),list(range(j,len(f))),'L')) + for j in range(len(h)-1): + out.append((vector(n,(h[j+1],1)),vector(n,(h[j+1],1),(A,2)),list(range(0,j+1)),'R')) + return out + +def dot(a,b):return sum(u*v for u,v in zip(a,b)) + +def verify_root(sL,sR): + """Exact algebra of the root: sign Gram, alternating sum, endpoint, commutants, chain merge.""" + F=fields(sL,sR);n=F['n'];S=sites(sL,sR);I=eye(n) + need(n%2==0 and len(S)==n+1,'Shortest root: n even and n+1 queries') + for i,(xi,yi,*_) in enumerate(S): + for j,(xj,*_) in enumerate(S): + need(dot(yi,xj)==(i>j)-(i=1: + emit('IDLE_ONE',2+i-1,[t for tr in treesL[i:] for t in tr['stages']]) + mix(c) + for x,y in thin_vectors(sL,sR): + c=complete(x,y,n);mix(inverse(c));query(0,1);emit('ADD',0,1,'-1');mix(c) + for m in range(gR): + x=vector(n,(A,-1),(fR[m],1),*[(fR[l],2) for l in range(m+1,gR)]) + w=vector(n,(A,1),*[(fR[l],-2) for l in range(m+1,gR)]) + used={A,fR[m]}|set(fR[m+1:]) + c=basis(x,w,[ev(fR[l]) for l in range(m+1,gR)],[ev(f) for f in range(n) if f not in used]);mix(inverse(c)) + supplier(treesR[m],0,1);emit('ADD',0,1,'-1') + if m==0: + for j in range(gR-1): + emit('IDLE_ONE',2+j,[t for tr in treesR[:j+1] for t in tr['stages']]) + mix(c) + targets[A]=[-1,[t for tr in treesL+treesR for t in tr['stages']]] + for i,f in enumerate(fL):targets[f]=[-1,[t for tr in treesL[i:] for t in tr['stages']]] + for m,h in enumerate(fR):targets[h]=[-1,[t for tr in treesR[:m+1] for t in tr['stages']]] + if E is not None:targets[E]=[-1,[]] + for r in range(next_role):emit('LAMBDA',r,-1) + diagonal=[[targets[r][0],0]+[int(j in targets[r][1]) for j in range(1,stage+1)] for r in range(next_role)] + return {'schema':'chain-nested-root/1','roles':next_role,'stages':stage,'ambient_rank':9+8*stage, + 'events':events,'diagonal':diagonal,'nodes':nodes,'n':n,'sL':list(sL),'sR':list(sR)} + +def outer_formula(sL,sR): + """Per-port outer histograms from the shape alone; compared with the literal word by pricing.py.""" + T,P=Counter(),Counter() + def nodes(m): + if m==1:return + T[8*m+1]+=2;P[8*m]+=2 + nodes(m//2);nodes(m-m//2) + for m in list(sL)+list(sR):nodes(m) + N=sum(sL)+sum(sR) + T[8*N+1]+=1 + for i in range(len(sL)): + T[8*sum(sL[i:])+1]+=1 + if i>=1:P[8*sum(sL[i:])]+=1 + for m in range(len(sR)): + T[8*sum(sR[:m+1])+1]+=1 + if m 0, "canonical positive rank") + need(type(value) is int and value > 0, "positive integer count") + result[rank] = value + return result + + +def difference(targets, paid): + return {r:targets.get(r,0)-paid.get(r,0) + for r in sorted(set(targets)|set(paid))} + + +def authenticate(root=PACKAGE): + origins = json.loads((PACKAGE/"ORIGINS.json").read_text()) + need(len(origins["files"]) == 7, "seven retained source files") + for item in origins["files"]: + need(item["head"] == HEAD, "frozen predecessor head") + data = (root/item["local_path"]).read_bytes() + need(hashlib.sha256(data).hexdigest() == item["sha256"], "source SHA256") + git_header = ("blob "+str(len(data))+"\0").encode() + need(hashlib.sha1(git_header+data).hexdigest() == item["git_blob"], "source Git blob") + + +def family(left, right): + need(type(left) is int and type(right) is int and min(left,right)>=1, + "positive integer chain lengths") + total = left+right + targets = Counter({r:total*n for r,n in HELPERS.items()}) + paid = Counter({r:total*n for r,n in PAID.items()}) + targets[8*total+1] += PORTS + for length in (left,right): + for j in range(1,length+1): + targets[8*j+1] += PORTS + for j in range(1,length): + paid[8*j] += PORTS + # This all-parity invoice relaxation contains the pinned odd/odd caller. + # Realizability of other parities is not used for its upper bound. + if total%2 == 0: + targets[1] += PORTS + paid[1] += 3*PORTS + else: + paid[1] += 2*PORTS + return dict(targets), dict(paid) + + +def source_recount(source, caller): + need(profile(source["local"]["helpers"]) == HELPERS, "pinned native helpers") + need(profile(source["local"]["paid"]) == PAID, "pinned native paid profile") + events = caller["events"] + locals_ = [event for event in events if event[0] == "LOCAL"] + need(sorted(event[1] for event in locals_) == list(range(1,19)), "18 native sites") + need(not any(event[0] == "IDLE" for event in events), "merged idle alphabet") + targets = Counter({r:18*n for r,n in HELPERS.items()}) + paid = Counter({r:18*n for r,n in PAID.items()}) + need(len(caller["diagonal"]) == 20, "20 caller output rows") + for row in caller["diagonal"]: + need(len(row) == 20 and row[:2] == [-1,0], "target q and phase exponents") + need(all(type(x) is int and x in (0,1) for x in row[2:]), "stage exponents") + targets[1+8*sum(row[2:])] += PORTS + for event in events: + if event[0] == "QUERY": + paid[1] += PORTS + elif event[0] == "IDLE_ONE": + stages = event[2] + need(len(stages)>0 and len(set(stages)) == len(stages), "idle stage set") + need(all(type(j) is int and 1<=j<=18 for j in stages), "idle stage range") + paid[8*len(stages)] += PORTS + target_dict, paid_dict = dict(targets), dict(paid) + for key, value in (("targets",target_dict),("paid",paid_dict)): + need(value == profile(source["price"][key]), "emitted/source "+key) + need(value == profile(source["independent_invoice"][key]), "independent/source "+key) + need((target_dict,paid_dict) == family(9,9), "formula/source complete bill") + return target_dict, paid_dict + + +def grouped_family(left, right): + """Source node bill for arbitrary full binary trees; no operator claim.""" + need(left and right, "nonempty lists of binary children") + nodes = [] + def count(tree): + if type(tree) is int and tree == 1: + return 1 + need(isinstance(tree,(tuple,list)) and len(tree) == 2, "full binary tree") + mass = count(tree[0])+count(tree[1]) + nodes.append(mass) + return mass + a, b = [count(x) for x in left], [count(x) for x in right] + total = sum(a)+sum(b) + need(len(nodes) == total-len(a)-len(b), "binary nodes equal omitted boundaries") + targets = Counter({r:total*n for r,n in HELPERS.items()}) + paid = Counter({r:total*n for r,n in PAID.items()}) + targets[8*total+1] += PORTS + for sizes in (a,b): + partial = 0 + for size in sizes: + partial += size + targets[8*partial+1] += PORTS + if partial0, "binary-node envelope agrees with all-one optimum") + return gap + + +def balanced_increment(total, low, high=None): + if high is None: + high = low + m = total//2 + native = moment_range(difference(HELPERS,PAID),low,high) + root = power_range(8*total+9,low,high)-power_range(8*total+1,low,high) + side = power_range(8*m+9,low,high)-power_range(8*m,low,high) + return native+(root+side).times(PORTS) + + +def ceiling_certificate(saving=UPPER, optimum=18): + before = balanced_increment(optimum-1,saving) + after = balanced_increment(optimum,saving) + margin = signed_moment(difference(*family(optimum//2,(optimum+1)//2)),saving) + need(before.lo>0, "left balanced increment positive") + need(after.hi<0, "right balanced increment negative") + need(margin.hi<0, "global maximum negative at upper endpoint") + return {"before":before.decimal(),"after":after.decimal(),"maximum":margin.decimal()} + + +def expect_failure(action, label): + try: + action() + except (ValueError,KeyError,TypeError): + return label + raise ValueError("negative control accepted: "+label) + + +def run(): + authenticate() + source = json.loads((PACKAGE/"retained/RESULT.json").read_text()) + caller = json.loads((PACKAGE/"retained/CALLER.json").read_text()) + targets, paid = source_recount(source,caller) + coefficients = difference(targets,paid) + low_margin = signed_moment(coefficients,LOWER) + high_margin = signed_moment(coefficients,UPPER) + need(low_margin.lo>0 and high_margin.hi<0, "root bracket signs") + ceiling = ceiling_certificate() + left_sign = balanced_increment(17,LOWER,UPPER) + right_sign = balanced_increment(18,LOWER,UPPER) + need(left_sign.lo>0 and right_sign.hi<0, "unique maximizer throughout root bracket") + binary_envelope_gap = binary_gap() + native = difference(HELPERS,PAID) + need(sum(native.values()) == -2892, "native count difference") + need(sum(r*n for r,n in native.items()) == -1720, "native rank-mass difference") + need(all(native[r]<0 for r in range(1,7)), "native low-rank signs") + need(native[7] == 1 and native[8] == 39 and native[9] == 359, "native high-rank signs") + derivative_lower = Fraction(-native[1]*8,81)-Fraction(2*native[7],7)-Fraction(native[8],8) + need(derivative_lower>0, "normalized native derivative lower bound") + checked_pairs = 0 + best = high_margin + for left in range(1,32): + for right in range(1,32): + signed = difference(*family(left,right)) + need(sum(r*n for r,n in signed.items()) == 48*(left+right)-104, + "family rank-mass identity") + margin = signed_moment(signed,UPPER) + need(margin.hi<0, "finite upper-endpoint corroboration") + if (left,right)!=(9,9): + need(margin.hi0 and gate_high.hi<0, + "retained (4,4,1|1,4,4) gate crossing") + exact_power_controls = [] + for rank in (1,2,3,4,8,9,16,17,64,73,81,137,145,153): + integer_power = power(rank,Fraction(0)) + need(integer_power.lo == integer_power.hi == rank*SCALE, "integer power identity") + square_root = power(rank,Fraction(1,2)) + need(square_root.lo**2 <= rank*SCALE*SCALE <= square_root.hi**2, + "square-root algebraic enclosure") + exact_power_controls.append(rank) + controls = [] + controls.append(expect_failure(lambda:binary_gap(thin_charge=0),"omit binary internal thin-query charge")) + controls.append(expect_failure(lambda:ceiling_certificate(LOWER),"favorable lower endpoint cannot certify ceiling")) + for false_optimum in (17,19): + controls.append(expect_failure(lambda n=false_optimum:ceiling_certificate(UPPER,n), + "wrong maximizing total "+str(false_optimum))) + for label,kind in (("omit thin query","QUERY"),("omit merged idle job","IDLE_ONE")): + changed = deepcopy(caller) + position = next(i for i,e in enumerate(changed["events"]) if e[0] == kind) + del changed["events"][position] + controls.append(expect_failure(lambda c=changed:source_recount(source,c),label)) + changed = deepcopy(caller) + idle = next(e for e in changed["events"] if e[0] == "IDLE_ONE" and len(e[2])>1) + idle[2].pop() + controls.append(expect_failure(lambda:source_recount(source,changed),"undercharge merged rank")) + changed = deepcopy(caller) + row = next(row for row in changed["diagonal"] if 1 in row[2:]) + row[2+row[2:].index(1)] = 0 + controls.append(expect_failure(lambda:source_recount(source,changed),"omit productive target axis")) + changed = deepcopy(caller) + changed["diagonal"][0][0] = 1 + controls.append(expect_failure(lambda:source_recount(source,changed),"wrong target q exponent")) + changed_source = deepcopy(source) + changed_source["local"]["paid"]["1"] -= 1 + controls.append(expect_failure(lambda:source_recount(changed_source,caller),"undercharge native job")) + for bad_length in (0,True,1.5): + controls.append(expect_failure(lambda n=bad_length:family(n,9),"invalid chain length "+repr(bad_length))) + with tempfile.TemporaryDirectory() as directory: + temp = Path(directory) + (temp/"retained").mkdir() + origins = json.loads((PACKAGE/"ORIGINS.json").read_text()) + for item in origins["files"]: + (temp/item["local_path"]).write_bytes((PACKAGE/item["local_path"]).read_bytes()) + authenticate(temp) + for item in origins["files"]: + path = temp/item["local_path"] + original = path.read_bytes() + path.write_bytes(original+b"\n") + controls.append(expect_failure(lambda:authenticate(temp),"source mutation "+item["local_path"])) + path.write_bytes(original) + return { + "status":"PASS_CHAIN_ROOT_GLOBAL_CEILING", + "base_commit":"7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "source_head":HEAD, + "source_pr":"CrocSwap/integer-mult-bounds#6833", + "saving_bracket":[str(LOWER),str(UPPER)], + "root_margin_lower":low_margin.decimal(), + "root_margin_upper":high_margin.decimal(), + "ceiling_certificate":ceiling, + "root_bracket_increment_signs":{"17_to_18":left_sign.decimal(),"18_to_19":right_sign.decimal()}, + "binary_child_envelope":{"delta9_minus_node_upper":binary_envelope_gap.decimal(), + "arbitrary_tree_corroboration_cases":forest_cases, + "total_leaves":[2,7],"stop_rule":"all ordered pairs of full binary forests in domain", + "gate_crossing_bracket":["0.00330823456614","0.00330823456615"], + "gate_margin_lower":gate_low.decimal(),"gate_margin_upper":gate_high.decimal()}, + "unique_maximizing_lengths":[9,9], + "normalized_native_derivative_rational_lower_bound":str(derivative_lower), + "source_counts":{"target_fields":sum(targets.values()),"paid_jobs":sum(paid.values()), + "paid_rank_mass":sum(r*n for r,n in paid.items()), + "surplus":sum(r*n for r,n in coefficients.items())}, + "finite_corroboration":{"left":[1,31],"right":[1,31],"pairs":checked_pairs, + "seed":None,"stop_rule":"exhaust all declared pairs"}, + "exact_power_control_ranks":exact_power_controls, + "negative_controls":controls, + "scope":"Declared two-chain invoice family only; analytical proof extends beyond finite corroboration. No new kappa; no supplier admission." + } + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--write",action="store_true",help="regenerate this package's deterministic result") + args = parser.parse_args() + result = run() + destination = PACKAGE/"RESULT.json" + if args.write: + destination.write_text(json.dumps(result,indent=2,sort_keys=True)+"\n") + else: + need(json.loads(destination.read_text()) == result,"committed deterministic result") + print(result["status"]) + print(json.dumps({"root_bracket":result["saving_bracket"],"maximizer":[9,9], + "negative_controls":len(result["negative_controls"]), + "corroborating_pairs":result["finite_corroboration"]["pairs"]},sort_keys=True)) + + +if __name__ == "__main__": + main()