diff --git a/research/rank7-chronological-face/.gitattributes b/research/rank7-chronological-face/.gitattributes new file mode 100644 index 0000000000..61eccae983 --- /dev/null +++ b/research/rank7-chronological-face/.gitattributes @@ -0,0 +1,2 @@ +# Frozen scientific evidence is authenticated byte for byte. +sources/** -text -whitespace diff --git a/research/rank7-chronological-face/FACE-PROOF.md b/research/rank7-chronological-face/FACE-PROOF.md new file mode 100644 index 0000000000..9d9b200fee --- /dev/null +++ b/research/rank7-chronological-face/FACE-PROOF.md @@ -0,0 +1,161 @@ +# The saturated rank-7 pattern direction preserves every rank tariff + +This independent check concerns PR #2979 at commit +`be191346391661f4d35fc0d1508d0a6029572576`, specifically its frozen +`construction/allocation/T37-FACE-MIX.json`, `certificates/RELAX-CAP.json` +and `allocation/PROFILE.json`. It proves finite bin-pattern arithmetic and +a written identity for arbitrary rank tariffs. It does not certify the +source supplier, cap root, all-size recurrence or a new exponent saving. + +The construction and pattern direction are due to Marius-Paul Dumitrean's +PR #2979, building on the source's credited PR2917 chronology, PR2930 flow +fill, PR2857 model, and themilkman216's cap/integrality observation. This +independent derivation was prepared by Ross's Codex automation with +OpenAI GPT-6.1 Sol assistance. Source credit and Apache-2.0 notices remain +in `sources/CREDITS.md` and `sources/NOTICE`. + +## Contract and exact identity + +A bin has capacity c in {8,16,32,48}; its pattern is a multiset of helper +widths in {4,5,6,7,8,9}, with sum at most c. Under the source model a bin +pays one residual child of rank c minus its used width, with rank zero +omitted. Helpers are whole roles in one bin. The local supplier profile +and inventory per call are held fixed. Scheduling windows, same-call +physical-family collisions, routing, native operators, arbitrary dirty +inputs and exact restoration remain separate source obligations. + +Write A=[7,8,8,9]@32, B=[7,9]@16, C=[8,8]@16 and D=[7,7,9,9]@32. +The move is A+B -> C+D. Both sides have one capacity-16 and one +capacity-32 bin, and inventory {7:2,8:2,9:2}. All four bins are saturated. +Consequently both sides have exactly one zero residual at each capacity, +with no positive residual. This proves equality of the *complete* +residual histogram separately at every capacity, even if zero residuals +are retained. + +For any function H on the ranks, the sum of residual tariffs H(r) is +therefore identical before and after the move. The usual source tariff +H_b(r)=r(73/r)^b for r>0, H_b(0)=0 is one example; the statement does not +rely on a root, a parameter interval, concavity or equality of rank mass. +Adding the same fully paid local profile preserves the whole moment at +every b. This is a cost identity for a legal pattern replacement; it +does not supply the chronological replacement or price any new routing. + +The source's ten-column fractional basis contains A, B and C. Its +constraint columns satisfy a_D=a_A+a_B-a_C, with the same identity for +their zero residual costs. Every dual which is tight on those basis +columns is also tight on D. Thus D is a zero reduced-cost direction +whenever that basis is optimal. The independent checker also inverts +the rational basis and obtains identically zero reduced cost as a +formal linear combination of tariff values, without invoking an LP, +certifying signs of other reduced costs, or recomputing a root. + +## The exact integral family + +Reversing 1,063 moves from the shipped T37 mix defines k=0. Applying k +forward moves gives the following counts; omitted zero counts are allowed. + +| capacity | helper widths | count | +| --- | --- | ---: | +| 8 | [8] | 24864 | +| 16 | [7,9] | 16253-k | +| 16 | [8,8] | 323+k | +| 32 | [7,8,8,9] | 1063-k | +| 32 | [7,7,9,9] | k | +| 32 | [9,9,9] | 864 | +| 32 | [6,8,9,9] | 5328 | +| 32 | [5,9,9,9] | 666 | +| 32 | [4,9,9,9] | 8655 | +| 48 | [] | 14095 | +| 48 | [9,9,9,9,9] | 2478 | +| 48 | [4,8,9,9,9,9] | 3 | + +All pattern multiplicities are nonnegative integers exactly when +0<=k<=1063. Necessity follows from D having multiplicity k and A having +multiplicity 1063-k; sufficiency follows directly from the table. +The source is exactly k=1063. This is the maximal interval for this +particular one-dimensional affine family, not the full feasible set of +integral packings. + +The width-7 slots outside capacity 16 number (1063-k)+2k=1063+k. +This family has at most one width-7 slot in each capacity-16 bin; the +unrestricted catalogue also permits [7,7]@16. Any Hall obstruction using +that at-most-one premise is restricted to this family (or another +explicitly restricted support), not every capacity-16 allocation. +No claim is made here that all 1,064 family members can be scheduled, +or that a necessary interval Hall condition is sufficient. + +## Complete finite invoice and T74 scaling + +Each point has bin counts {8:24864,16:16576,32:16576,48:16576}. There +are 333 calls. The per-call inventory is +{4:26,5:2,6:16,7:52,8:99,9:213}, summing to 408 helpers, so the complete +inventory is {4:8658,5:666,6:5328,7:17316,8:32967,9:70929}, with +135,864 helper roles. + +The residual histograms, including zero, are: + +| capacity | residual-rank histogram | +| --- | --- | +| 8 | {0:24864} | +| 16 | {0:16576} | +| 32 | {0:7057,1:8655,5:864} | +| 48 | {0:3,3:2478,48:14095} | + +Hence there are 48,500 saturated bins and positive idle histogram +{1:8655,3:2478,5:864,48:14095}. The fully paid local per-call profile is +{1:2445,2:706,3:232,4:108,5:18,8:8}. Adding 333 copies gives exactly +{1:822840,2:235098,3:79734,4:35964,5:6858,8:2664,48:14095}, with rank +mass 2,408,256 = 65088*37. Thus the complete source-style moment at T37 is + + [822840 H(1) + 235098 H(2) + 79734 H(3) + 35964 H(4) + + 6858 H(5) + 2664 H(8) + 14095 H(48)] / [73*896*37]. + +Doubling the finite counts gives T74, 666 calls, 271,728 roles, and +{1:1645680,2:470196,3:159468,4:71928,5:13716,8:5328,48:28190}, exactly +the frozen `allocation/PROFILE.json`. The source-style moment is +unchanged because its numerator and denominator double. This arithmetic +does not independently prove that the literal interleaving preserves +windows or physical families; the owner's chronological check has that +separate obligation. + +## Fractional cap and integral mixture are distinct + +The source README's phrase "cap-level integer mixes" must not identify +the preceding integral family with the fractional cap profile. The +fractional basis has residual counts per replica +{1:234,3:1341/20,5:93/4,48:7619/20}. At T37, subtracting this profile +from the integral family's profile yields the exact nonzero difference + + Delta = -3 e1 - (57/20) e3 + (15/4) e5 - (3/20) e48. + +Its rank mass is zero, but its histogram is different. Therefore the +identity among the integral family preserves its existing near-cap +moment; it does not close its gap to the fractional cap. The source +reports a near-cap root, and this check neither recomputes its digits +nor proves the basis optimal. Fractionality of one basis alone would +also not rule out another integral optimum on a larger face. An exact +cap-attainment claim would require its own complete optimal-face and +chronological argument. + +## Verification and defect sensitivity + +Run `python3 -B research/rank7-chronological-face/independent_face.py`, +also with `python3 -O -B`. Explicit exceptions, not assertions, enforce +the checks. The program independently reconstructs all finite counts, +enumerates the 1,064 family points, checks per-capacity residuals and +the T74 profile, and checks the symbolic target reduced cost. + +Negative controls reject both out-of-range endpoints, a changed source +count, a capacity-preserving count transfer which changes width +inventory, and a claimed-profile change which preserves child count +and rank mass. A saturated wrong swap A+B -> A+C preserves capacities +and residuals but changes inventory. A stronger rank-mass control uses +[4,5]@16+[6,7]@16 versus [4,6]@16+[5,7]@16: both preserve inventory, +two residual children and residual rank mass 10, but their histograms +are {3:1,7:1} and {4:1,6:1}; tariff H(r)=r^2 gives 58 versus 52. +These controls show why rank mass alone does not establish the claim. + +The written swap identity holds for arbitrary tariffs and all legal +applications. The exhaustive finite computation covers the stipulated +T37 family only. Neither is a formal-kernel proof or a new supplier or +recursive-complexity admission. diff --git a/research/rank7-chronological-face/HALL-PROOF.md b/research/rank7-chronological-face/HALL-PROOF.md new file mode 100644 index 0000000000..602064c899 --- /dev/null +++ b/research/rank7-chronological-face/HALL-PROOF.md @@ -0,0 +1,208 @@ +# The chronological width-7 cut on the fixed packing face + +This checks the allocation mechanism in Marius-Paul Dumitrean's PR [2979](https://github.com/CrocSwap/integer-mult-bounds/pull/2979), frozen at +`be191346391661f4d35fc0d1508d0a6029572576`. The integer mix, chronology and literal +fill are predecessor artifacts, not new constructions here. The new result is +an independent derivation of the cut, its exact consequence for the one-parameter +face, and a check of the literal two-copy realization. It does not claim a new +exponent saving. + +The precise conclusion is that **every feasible member of the stated face family +must have `k >= 473`**. Member `k=472` fails the cut by one role. Member `k=473` +passes this necessary cut; no realization of that member is provided. The source +literal realization is member `k=1063`. + +## Premises and source chronology + +The fixed domain has 37 replicas, nine calls per replica, 408 ordered helpers per +call, and 112 indivisible ports per `(owner replica, child)` bin. Both declared +provider inventories are +`{4:26, 5:2, 6:16, 7:52, 8:99, 9:213}`. The ordered width of each actual helper is +read through the literal provider dispatch; equal inventory counts do not replace +that binding. Derivation of those widths from native entering and exiting frames +is an inherited premise. + +Use zero-based time `t` in the literal `PLAN.order`, denoted `O37`, and let +`tau_s(r)` be the position of `(stage s, replica r)` in that order. Each replica's +stage order is increasing. The checker does not reconstruct the order from an +assumed priority: in this source, sorting by `(4*s+r,s,r)` first disagrees at time +14, where that priority puts `(2,0)` and the literal source puts `(0,9)`. + +The source recipe identifies the pair touched by each local call. Scan the +`TEMPLATE.execution_schedule` in its written order. A local event updates that +pair's most recent source stage; a bridge updates both its source and destination +pairs. An idle-cover event ends the pending window at its current stage and starts +it strictly after the pair's most recent source event, or at initial time `-1`. +Only children retained in `TEMPLATE.idle_children` are owner bins. Bank and padding +children mentioned by other idle-cover events are excluded. This gives the +following stage endpoints without running the predecessor owner engine: + +| Children | Capacity | Legal call times for owner `r` | +|---|---:|---| +| 0, 2 | 16 | `-1 < t <= tau_1(r)` | +| 1, 3 | 8 | `tau_1(r) < t <= tau_2(r)` | +| 4, 6 | 32 | `-1 < t <= tau_3(r)` | +| 5, 7 | 8 | `tau_3(r) < t <= tau_4(r)` | +| 8, 10 | 48 | `-1 < t <= tau_5(r)` | +| 9, 11 | 8 | `tau_5(r) < t <= tau_6(r)` | +| 12, 13 | 48 | `tau_2(r) < t <= tau_8(r)` | +| 14, 15 | 32 | `tau_4(r) < t <= tau_8(r)` | +| 16, 17 | 16 | `tau_6(r) < t <= tau_8(r)` | + +All 666 instantiated windows agree exactly with `PLAN.windows`, including every +integer time in each window. Lower endpoints are excluded and upper endpoints +are included. Physical family identity remains +`(owner replica, PLAN.pairs[child], PLAN.sides[child], port)`; changing child IDs +does not necessarily change the physical family. + +## The interval cut + +For an inclusive interval `I=[a,b]`, a window `(L,U]` meets `I` exactly when +`U >= a` and `L < b`. The pattern restriction used here is that **at most one +width-7 role occupies any capacity-16 bin over that bin's entire pending window**. +This holds for every member of the fixed face below. It is not a general +capacity bound: a different pattern `[7,7]@16` could hold two such roles and lies +outside this argument's domain. + +There are `52 |I|` width-7 roles requested in `I`. Every one assigned to capacity +16 needs a different bin whose window meets `I`. Therefore, if `B16(I)` counts +those bins and `R` counts all width-7 slots outside capacity 16 globally, + +```text +R >= number of width-7 roles in I outside capacity 16 + >= 52 |I| - B16(I). +``` + +For `I=[45,332]`, there are 288 calls. For children 0 and 2, the eligible replicas +are exactly `14..36`, giving 23 owner windows for each child; in particular +`tau_1(13)=44` excludes replica 13. For children 16 and 17, all 37 owner windows +meet `I`. Consequently, + +```text +B16(I) = 112 (23 + 23 + 37 + 37) = 13,440, +demand = 52 * 288 = 14,976, +R >= 14,976 - 13,440 = 1,536. +``` + +The checker also exhausts all `333*334/2 = 55,611` nonempty contiguous call +intervals, using these exact source windows. The maximum of +`52 |I| - B16(I)` is 1,536, attained uniquely by `[45,332]`. Thus the bound above is +the strongest global-reserve bound obtained from a single contiguous interval +with this counting rule. This is neither a check of all subsets of calls nor a +sufficient Hall criterion for the full scheduling problem. The count also +relaxes active-family and coordinate restrictions; those cannot invalidate this +necessary lower bound. + +## The exact one-parameter family + +Undo the source's 1,063 swaps to define member `k=0`. The four changing pattern +counts at member `k` are: + +| Capacity | Pattern | Multiplicity | +|---:|---|---:| +| 16 | `[8,8]` | `323+k` | +| 16 | `[7,9]` | `16253-k` | +| 32 | `[7,8,8,9]` | `1063-k` | +| 32 | `[7,7,9,9]` | `k` | + +All other pattern counts are exactly the source `T37-FACE-MIX.json` counts. The +covered domain is every integer `0 <= k <= 1063`. All multiplicities remain +nonnegative. Each step implements the source's swap + +```text +[7,8,8,9]@32 + [7,9]@16 -> [8,8]@16 + [7,7,9,9]@32. +``` + +The capacity-16 patterns have at most one width-7 slot, and no unchanged pattern +contains a width-7 slot. Hence the exact total outside capacity 16 is + +```text +R(k) = (1063-k) + 2k = 1063+k. +``` + +The interval cut implies `1063+k >= 1536`, equivalently `k >= 473`. The initial +global-reserve deficit is exactly 473 roles. At `k=472`, the global reserve is +1,535, which is one short. At `k=473`, the global reserve is 1,536. Nothing in +this calculation ensures that all those slots can serve the interval, that the +other widths can be assigned, or that family and mask constraints can be met. + +Every changed bin is full both before and after a swap. Thus each step preserves +the counts of each width, each capacity, every idle rank, and the inherited native +calls, bridges, centres and cleanup interface. Its complete paid-profile change +is zero, conditional on that unchanged interface. This is a possible allocation +repair, not a scalar-operation saving promoted to a recursive improvement. + +## The literal T74 witness + +The literal `ORDER` is exactly the interleaving + +```text +O74[2t+b] = (s, r+37b), where O37[t]=(s,r) and b in {0,1}. +``` + +The provider IDs also project identically in the two copies. For any same-copy +source endpoint with `L >= 0`, its image is `2L+b`; the initial endpoint remains +`-1`. The equivalence +`L < t <= U` iff `2L+b < 2t+b <= 2U+b`, with the initial case checked separately, +proves that the embedding preserves each copy's legal source times. + +The checker visits all 271,728 literal rows, checking complete `(call,helper)` +coverage, source windows, at most one helper per physical family per call, +capacity bounds, disjoint integral coordinate masks, and compact pending prefixes. +All owners are in the requesting call's copy. Projecting `time -> time//2` and +`owner -> owner mod 37` gives two identical sets of 135,864 literal rows. The +actual bin patterns equal twice the source `k=1063` mix, including empty bins. + +Each copy has 17,316 width-7 roles, with 2,126 outside capacity 16. Within the cut, +12,853 use capacity 16 and 2,123 use other capacities. These are checks of the +existing final witness; they do not construct `k=473`. + +From the literal idle ranks and the **declared** provider-local paid profiles, +the checker independently sums the complete source child profile + +```text +T74: {1:1645680, 2:470196, 3:159468, 4:71928, + 5:13716, 8:5328, 48:28190}. +``` + +Equivalently, its conditional charged child cost is +`1645680 H_1 + 470196 H_2 + 159468 H_3 + 71928 H_4 + 13716 H_5 + 5328 H_8 + 28190 H_48`, +for the inherited recursive tariff `H`. Source native arithmetic, arbitrary dirty +input restoration, the derivation of paid local profiles, physical stock, source +access, precision, and outer transfer remain predecessor obligations rather than +newly admitted consequences of this finite check. + +## Reproduction and proof level + +```sh +python3 research/rank7-chronological-face/independent_hall.py +python3 -O research/rank7-chronological-face/independent_hall.py +``` + +The importable interface is `verify_hall(package_root=None)`, returning a +JSON-serializable receipt. It uses only the Python standard library and does not +execute or import any predecessor producer, searcher or owner engine. It verifies +the hashes of its eight frozen JSON inputs against `SOURCES.json` and rechecks +them at exit. All checks raise explicit exceptions, so `python3 -O` retains them. +Six controls reject a real width-7 role at its excluded lower endpoint, an +expanded source window, a duplicated same-call physical family, a missing width-7 +role, a demand undercount by one, and a changed two-copy interleaving. + +The counting inequality and implication `k>=473` are written mathematical proofs +for the stated fixed model. The source extraction, complete interval maximum and +literal geometry are finite exhaustive computations over the pinned artifacts. +There is no formal-kernel proof, no all-parameter allocation theorem, and no claim +that the new boundary member is schedulable. + +## Attribution + +The source package credits Marius-Paul Dumitrean for its new words and allocation +(with substantial AI assistance from Anthropic Claude), Mason Hale/PR2917 for the +T74 chronology, Jeremy Kothe/PR2833 for the source materializer and inherited +supplier, Yiyang Lu/PR2857 for chronological flow and realization, Dugongue for +the owner-engine lineage, Tekalign for the earlier independent owner checker, +and themilkman216 for the cap-integrality observation. The face swap and source +cut are retained from PR2979; their origin is not reassigned by this independent +check. See the frozen `sources/CREDITS.md` and `sources/NOTICE` for the complete +predecessor credits and license notice. This independent proof and checker were +prepared with GPT-6.1 Sol assistance. diff --git a/research/rank7-chronological-face/LICENSE b/research/rank7-chronological-face/LICENSE new file mode 100644 index 0000000000..261eeb9e9f --- /dev/null +++ b/research/rank7-chronological-face/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/rank7-chronological-face/NOTICE b/research/rank7-chronological-face/NOTICE new file mode 100644 index 0000000000..6078040bd2 --- /dev/null +++ b/research/rank7-chronological-face/NOTICE @@ -0,0 +1,4 @@ +Rank-seven chronological face check +Copyright 2026 Ross Richardson, with substantial OpenAI Codex assistance. +Apache-2.0. Source evidence from Marius-Paul Dumitrean PR2979; original CREDITS and NOTICE are retained under sources/. +Chronology/owner lineage includes Mason Hale, Jeremy Diviney, Jeremy Kothe, Yiyang Lu, Dugongue, themilkman216, Tekalign, icekylinx and the original credited authors. diff --git a/research/rank7-chronological-face/README.md b/research/rank7-chronological-face/README.md new file mode 100644 index 0000000000..c87a0b11f4 --- /dev/null +++ b/research/rank7-chronological-face/README.md @@ -0,0 +1,112 @@ +# Rank-seven helper packing: an exact chronological cut and a cost-neutral repair + +An independent check of Marius-Paul Dumitrean's [PR2979](https://github.com/CrocSwap/integer-mult-bounds/pull/2979) +at `be191346391661f4d35fc0d1508d0a6029572576` confirms a concrete bridge +needed by its changed helper boundaries: a pattern replacement can remove a +chronological width-seven deficit while preserving every recursive rank tariff. +This package makes no new kappa or complete supplier claim. + +## Result and covered model + +The source's six-width inventory is +`{4:26,5:2,6:16,7:52,8:99,9:213}` per call. Its T37 chronology has 333 calls. +On calls 45 through 332 inclusive, 14,976 width-seven roles can reach at most +13,440 capacity-16 bins. In the stipulated pattern family each such bin has +at most one width-seven slot. Therefore at least 1,536 of those roles must +use another capacity. This is a restricted pattern obstruction: an arbitrary +capacity-16 bin can instead contain two width-seven helpers. + +Reverse the source's 1,063 declared swaps to obtain the naive integer mix. +After k swaps its four changing pattern counts are: + +| capacity | helper widths | count | +| --- | --- | ---: | +| 16 | 7,9 | 16,253-k | +| 16 | 8,8 | 323+k | +| 32 | 7,8,8,9 | 1,063-k | +| 32 | 7,7,9,9 | k | + +The nonnegative integer range is exactly `0 <= k <= 1063`. Width-seven slots +outside capacity 16 total `1063+k`; hence the displayed interval requires +`k >= 473`. In particular k=472 fails by one role. Passing this necessary +cut at k=473 does not construct a schedule. The shipped k=1063 fill is checked +separately against the actual chronology and provider-indexed widths. +The interval is the unique strongest one among all 55,611 contiguous intervals +under this global-reserve inequality. Arbitrary subsets and other constraints +can give different necessary conditions. + +The swap + +```text +[7,8,8,9]@32 + [7,9]@16 -> [8,8]@16 + [7,7,9,9]@32 +``` + +preserves helper inventory, bin counts separately by capacity, and the complete +residual-rank histogram. All four bins are saturated. Thus it preserves the +whole rank moment for *every* tariff H, including the recursive power tariffs, +when the local word and all other charges remain fixed. It is stronger than +a rank-mass equality and does not claim that rearrangement is operationally free. + +Every member has the T37 complete source-profile +`{1:822840,2:235098,3:79734,4:35964,5:6858,8:2664,48:14095}`; +doubling gives the frozen T74 profile. The integer family retains its existing +gap to the fractional cap. Its idle histogram minus 37 times the recorded +fractional-cap histogram is exactly +`-3 e1 -(57/20)e3 +(15/4)e5 -(3/20)e48`, which has zero rank mass and is nonzero. +No cap optimality, root digits or integral optimum are recertified here. + +## Evidence and independence + +[HALL-PROOF.md](HALL-PROOF.md) derives windows from the source event template, +literal order and replica cuts, then checks the relevant literal placement. +[FACE-PROOF.md](FACE-PROOF.md) proves the all-tariff identity and derives the +finite family and complete profiles. The two new standard-library implementations +do not import or execute predecessor owner, producer, LP or root routines. +All 1,064 integer family points and defect controls are checked explicitly. +`RESULT.json` records the exact finite coverage and controls. +The placement check covers all 271,728 roles, their integral masks and compact +prefixes, source windows, helper identities and same-call physical-family +exclusions. Both T74 copies project onto identical T37 rows. Each copy places +12,853 of the cut's width-seven roles in capacity 16 and 2,123 outside it. + +`SOURCES.json` binds 19 frozen evidence files by SHA256 and Git blob identity. +The registered metadata check additionally checks their original Git provenance +and the pinned catalogue/selected record. The portable verifier authenticates +the frozen exports without requiring Git history. The width registry and event +template are conditional inputs: this check does not independently derive native +widths or prove arbitrary-dirty-input native restoration, phase adapters, +precision, physical tape costs, outer admission or all-size/compiler implications. +This is a written scoped argument with finite exact computation, not a +formal-kernel or independent human proof. + +## Reproduction + +```sh +python3.12 scripts/research_package.py --package research/rank7-chronological-face +python3.12 -I -B -O research/rank7-chronological-face/verify.py --check-result +``` + +The package directory alone, including its frozen sources, supports the second +command from any working directory with the script path adjusted. No solver, +network, native compiler or dependency installation is needed. + +## Open next questions + +What is the least k in this family admitting a complete chronological fill? +The necessary cut gives a lower bound and the shipped k=1063 witness supplies +an upper bound. Test remaining k with exact role, source-window, compact-mask +and physical-family constraints; a feasible cut alone is insufficient. +Changed words, pattern supports or chronologies require a new model. +The structured handoff is in `TASK.json`. + +## Credit and scientific pins + +Scientific base main `30f016dd79ee6a23c40d7dab44a9466c148c42dd`, priority revision 5; +selected-record SHA256 `bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129`. +PR2979 supplies the construction and swap. Credit its author Marius-Paul Dumitrean, +Jeremy Kothe/PR2957/2966, Dugongue/2969, Mason Hale/2917, Jeremy Diviney/2908, +Yiyang Lu/2857, themilkman216, Tekalign, icekylinx and the retained owner/native +lineage. Original notices and detailed credit remain in `sources/`. +Ross Richardson, with substantial OpenAI Codex assistance and separate AI +mathematical checks; Apache-2.0. Earlier PR2974 checks a different frozen word +and does not establish this new inventory's placement. diff --git a/research/rank7-chronological-face/RESULT.json b/research/rank7-chronological-face/RESULT.json new file mode 100644 index 0000000000..0ed75530cc --- /dev/null +++ b/research/rank7-chronological-face/RESULT.json @@ -0,0 +1,314 @@ +{ + "face": { + "T37": { + "bins": { + "16": 16576, + "32": 16576, + "48": 16576, + "8": 24864 + }, + "calls": 333, + "helper_roles": 135864, + "idle": { + "1": 8655, + "3": 2478, + "48": 14095, + "5": 864 + }, + "inventory": { + "4": 8658, + "5": 666, + "6": 5328, + "7": 17316, + "8": 32967, + "9": 70929 + }, + "profile": { + "1": 822840, + "2": 235098, + "3": 79734, + "4": 35964, + "48": 14095, + "5": 6858, + "8": 2664 + }, + "rank_mass": 2408256, + "replicas": 37, + "zero_residual_bins": 48500 + }, + "T74_profile": { + "1": 1645680, + "2": 470196, + "3": 159468, + "4": 71928, + "48": 28190, + "5": 13716, + "8": 5328 + }, + "controls": [ + { + "name": "negative_family_endpoint", + "reason": "family parameter outside 0..1063" + }, + { + "name": "upper_family_endpoint", + "reason": "family parameter outside 0..1063" + }, + { + "name": "source_count_increment", + "reason": "bins by capacity" + }, + { + "name": "capacity_preserving_source_count_change", + "reason": "width inventory" + }, + { + "name": "rank_mass_preserving_claimed_profile", + "reason": "claimed profile" + }, + { + "name": "saturated_wrong_swap_inventory", + "reason": "width inventory changed" + }, + { + "name": "inventory_and_mass_tie_wrong_histogram", + "reason": "residual histogram changed" + } + ], + "integer_family": { + "first": 0, + "last": 1063, + "source_parameter": 1063, + "verified_points": 1064, + "width7_outside_cap16": "1063+k" + }, + "integral_minus_fractional_cap_idle": { + "1": "-3", + "3": "-57/20", + "48": "-3/20", + "5": "15/4" + }, + "scope": "finite bin-pattern arithmetic and written all-tariff identity; no chronology for all k, cap optimality/root replay, supplier admission or new kappa", + "source_commit": "be191346391661f4d35fc0d1508d0a6029572576", + "status": "PASS_INDEPENDENT_RANK7_FACE_ARITHMETIC", + "target_symbolic_reduced_cost": {} + }, + "hall": { + "PLAN_matches_priority_4s_plus_r": false, + "T37_windows_checked": 666, + "T74_exact_call_and_role_projection": true, + "all_contiguous_intervals": { + "attaining_intervals_inclusive": [ + [ + 45, + 332 + ] + ], + "intervals_checked": 55611, + "maximum_required_outside_cap16": 1536 + }, + "controls": [ + { + "name": "role_at_excluded_lower_endpoint", + "reason": "literal source window" + }, + { + "name": "expanded_source_window", + "reason": "PLAN window equality" + }, + { + "name": "duplicate_same_call_physical_family", + "reason": "same-call physical family collision" + }, + { + "name": "missing_width7_role", + "reason": "complete literal role count" + }, + { + "name": "undercounted_width7_demand", + "reason": "cut demand" + }, + { + "name": "changed_interleaving_endpoint", + "reason": "exact T74 call projection" + } + ], + "cut": { + "calls": 288, + "cap16_abstract_windows_by_child": { + "0": 23, + "16": 37, + "17": 37, + "2": 23 + }, + "cap16_bins_touching": 13440, + "interval_inclusive": [ + 45, + 332 + ], + "required_outside_cap16": 1536, + "width7_demand": 14976 + }, + "face_family": { + "integer_k_inclusive": [ + 0, + 1063 + ], + "k472": "REJECTED_BY_CUT", + "k473": "PASSES_THIS_NECESSARY_CUT_ONLY", + "necessary_k_lower_bound": 473, + "outside_width7_formula": "1063+k" + }, + "literal_witness": { + "conditional_complete_profile": { + "1": 1645680, + "2": 470196, + "3": 159468, + "4": 71928, + "48": 28190, + "5": 13716, + "8": 5328 + }, + "cut_width7_cap16_per_copy": [ + 12853, + 12853 + ], + "cut_width7_outside_cap16_per_copy": [ + 2123, + 2123 + ], + "idle_profile": { + "1": 17310, + "3": 4956, + "48": 28190, + "5": 1728 + }, + "projected_roles_per_copy": 135864, + "roles_checked": 271728, + "width7_outside_cap16_per_copy": [ + 2126, + 2126 + ], + "width7_roles_per_copy": [ + 17316, + 17316 + ] + }, + "scope": "Finite literal owner geometry conditional on source ordered provider widths; written necessary inequality for this fixed pattern face. No sufficiency, native circuit admission, formal kernel proof, or new kappa claim.", + "source_commit": "be191346391661f4d35fc0d1508d0a6029572576", + "source_sha256": { + "sources/allocation/DISPATCH.json": "65e435bd68e97243c003677271b88485a29d4d0fae2dff1354100404a145e74c", + "sources/allocation/FILL.json.gz": "c2136be9434cda511a1a8a44d98f9f72ea5376830a8426674253b4ee351c4c39", + "sources/allocation/ORDER.json": "519d1d5dbb997a219fcfcad34c0b03e7838bef24199784d7e964fa10090f66e1", + "sources/allocation/PROVIDERS.json": "f2edb7922f3029a5d607437e737775ff3371bca49ebab62e5e2495d16d3bf573", + "sources/allocation/vendor/PLAN.json.gz": "d566cfb87b71639d4138e1f89b543e2dd6a7772070226a2a14c799a6835bf21e", + "sources/allocation/vendor/TEMPLATE.json.gz": "21297b20f1f2dc76eb9dd8124416068c3cb096bab9df17fa4da19bc68dfe082e", + "sources/construction/allocation/T37-FACE-MIX.json": "10598b7ea2e26fbd49db2b4d2f08122415fd6673b87fb7b458019d503ae60744", + "sources/construction/allocation/T37-PATTERNS.json": "df09e4581d7ed73fa22253909197ceb26ced59333f50c008c822894a4082f0e4" + }, + "status": "PASS_INDEPENDENT_CHRONOLOGICAL_FACE_CUT", + "symbolic_stage_windows": { + "0": [ + 16, + -1, + 1 + ], + "1": [ + 8, + 1, + 2 + ], + "10": [ + 48, + -1, + 5 + ], + "11": [ + 8, + 5, + 6 + ], + "12": [ + 48, + 2, + 8 + ], + "13": [ + 48, + 2, + 8 + ], + "14": [ + 32, + 4, + 8 + ], + "15": [ + 32, + 4, + 8 + ], + "16": [ + 16, + 6, + 8 + ], + "17": [ + 16, + 6, + 8 + ], + "2": [ + 16, + -1, + 1 + ], + "3": [ + 8, + 1, + 2 + ], + "4": [ + 32, + -1, + 3 + ], + "5": [ + 8, + 3, + 4 + ], + "6": [ + 32, + -1, + 3 + ], + "7": [ + 8, + 3, + 4 + ], + "8": [ + 48, + -1, + 5 + ], + "9": [ + 8, + 5, + 6 + ] + } + }, + "scope": "Finite source-bound interval obstruction, pattern-family identity and literal owner geometry conditional on the supplied native width registry; no native residual, precision, outer, all-size or new-kappa admission.", + "sources": { + "bytes": 2643054, + "controls": [ + "changed frozen byte rejected before mathematical checks" + ], + "files": 19, + "manifest_sha256": "a8ba6f0e44313c718111a011631351a1eb740d1fb3d6f1879ae3b13d840b3d06", + "source_commit": "be191346391661f4d35fc0d1508d0a6029572576" + }, + "status": "PASS_RANK7_CHRONOLOGICAL_FACE_NO_NEW_KAPPA" +} diff --git a/research/rank7-chronological-face/SOURCES.json b/research/rank7-chronological-face/SOURCES.json new file mode 100644 index 0000000000..c60197e642 --- /dev/null +++ b/research/rank7-chronological-face/SOURCES.json @@ -0,0 +1,191 @@ +{ + "source_pr": 2979, + "source_commit": "be191346391661f4d35fc0d1508d0a6029572576", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "889b95d936746df124872133ae1e7cc339adcb92", + "sha256": "7d185cd8c2af35988d638d969748ad7b670f902606444dbfc748e4402c340df6" + }, + { + "path": "research/rank7-joint-endframes/README.md", + "usage": "provenance", + "pin": "head:be191346391661f4d35fc0d1508d0a6029572576:research/rank7-joint-endframes/README.md", + "git_blob": "ad4fde698389d02543df632d46b54dcd93e53a97", + "sha256": "d00d123fc6cb7da627a8db1b8ae95b732ef7c55f802a784059de982159548634", + "export_path": "sources/README.md", + "bytes": 24923 + }, + { + "path": "research/rank7-joint-endframes/CREDITS.md", + "usage": "provenance", + "pin": "head:be191346391661f4d35fc0d1508d0a6029572576:research/rank7-joint-endframes/CREDITS.md", + "git_blob": "5f4197842052437f5fb6dc41cfd8d4dc9349cc22", + "sha256": "bf85777bd2d9b8e537dae2e70614759ba1a265101dd903a72fbd2cfc2869c406", + "export_path": "sources/CREDITS.md", + "bytes": 3587 + }, + { + "path": "research/rank7-joint-endframes/NOTICE", + "usage": "provenance", + "pin": "head:be191346391661f4d35fc0d1508d0a6029572576:research/rank7-joint-endframes/NOTICE", + "git_blob": "9df951052ae186bce02a6258219dae58f7cf2e80", + "sha256": "b767e40e8c7e16058d1ebb8c08eef9b9bffae31cfa30512b843ae1fcbfc6f5cd", + "export_path": "sources/NOTICE", + "bytes": 2613 + }, + { + "path": "research/rank7-joint-endframes/PINS.json", + "usage": "provenance", + "pin": "head:be191346391661f4d35fc0d1508d0a6029572576:research/rank7-joint-endframes/PINS.json", + "git_blob": "d71aaccbae9232322721638cb0857a25bab4b91c", + "sha256": "978b20708cabb86cc379e42ca04f45b9251d60a5241c3d70092288f42051cc68", + "export_path": "sources/PINS.json", + "bytes": 2789 + }, + { + "path": "research/rank7-joint-endframes/allocation/ORDER.json", + "usage": "provenance", + "pin": "head:be191346391661f4d35fc0d1508d0a6029572576:research/rank7-joint-endframes/allocation/ORDER.json", + "git_blob": "7409c4df1092241729739596c7648bda504e6aad", + "sha256": "519d1d5dbb997a219fcfcad34c0b03e7838bef24199784d7e964fa10090f66e1", + "export_path": "sources/allocation/ORDER.json", + "bytes": 4573 + }, + { + "path": "research/rank7-joint-endframes/allocation/DISPATCH.json", + "usage": "provenance", + "pin": "head:be191346391661f4d35fc0d1508d0a6029572576:research/rank7-joint-endframes/allocation/DISPATCH.json", + "git_blob": "9544fee4e6ee1f202cee22bfaeaf229ee3b2515e", + "sha256": "65e435bd68e97243c003677271b88485a29d4d0fae2dff1354100404a145e74c", + "export_path": "sources/allocation/DISPATCH.json", + "bytes": 10401 + }, + { + "path": "research/rank7-joint-endframes/allocation/FILL.json.gz", + "usage": "provenance", + "pin": "head:be191346391661f4d35fc0d1508d0a6029572576:research/rank7-joint-endframes/allocation/FILL.json.gz", + "git_blob": "8d4fd644d60ba2c98106dc770803b647afdf0963", + "sha256": "c2136be9434cda511a1a8a44d98f9f72ea5376830a8426674253b4ee351c4c39", + "export_path": "sources/allocation/FILL.json.gz", + "bytes": 1347458 + }, + { + "path": "research/rank7-joint-endframes/allocation/PROVIDERS.json", + "usage": "provenance", + "pin": "head:be191346391661f4d35fc0d1508d0a6029572576:research/rank7-joint-endframes/allocation/PROVIDERS.json", + "git_blob": "e1d99e12cfa3ac8375984d85c0b040dc36ea1312", + "sha256": "f2edb7922f3029a5d607437e737775ff3371bca49ebab62e5e2495d16d3bf573", + "export_path": "sources/allocation/PROVIDERS.json", + "bytes": 7684 + }, + { + "path": "research/rank7-joint-endframes/allocation/PROFILE.json", + "usage": "provenance", + "pin": "head:be191346391661f4d35fc0d1508d0a6029572576:research/rank7-joint-endframes/allocation/PROFILE.json", + "git_blob": "46a83eeda67ab67cccbffe8b7ad8e44368b40ea7", + "sha256": "94a819747f3ced41f1544ada0036c983fc0c92847b9644380f877a06cd7931cf", + "export_path": "sources/allocation/PROFILE.json", + "bytes": 104 + }, + { + "path": "research/rank7-joint-endframes/allocation/SEARCH.json", + "usage": "provenance", + "pin": "head:be191346391661f4d35fc0d1508d0a6029572576:research/rank7-joint-endframes/allocation/SEARCH.json", + "git_blob": "cf0a2e7ca4bb431ab32b2515050ff81c7b5faae2", + "sha256": "2ceb1f825cb68e44d17d4251f74c3975ae5122c845391c1ca8de2e564ac4246a", + "export_path": "sources/allocation/SEARCH.json", + "bytes": 1831 + }, + { + "path": "research/rank7-joint-endframes/allocation/vendor/PLAN.json.gz", + "usage": "provenance", + "pin": "head:be191346391661f4d35fc0d1508d0a6029572576:research/rank7-joint-endframes/allocation/vendor/PLAN.json.gz", + "git_blob": "7a1db55a4d53ee99280be4f3ab7d29f7b2033adf", + "sha256": "d566cfb87b71639d4138e1f89b543e2dd6a7772070226a2a14c799a6835bf21e", + "export_path": "sources/allocation/vendor/PLAN.json.gz", + "bytes": 29933 + }, + { + "path": "research/rank7-joint-endframes/allocation/vendor/TEMPLATE.json.gz", + "usage": "provenance", + "pin": "head:be191346391661f4d35fc0d1508d0a6029572576:research/rank7-joint-endframes/allocation/vendor/TEMPLATE.json.gz", + "git_blob": "114808c32b1799da53524bdc25cea67efb60009e", + "sha256": "21297b20f1f2dc76eb9dd8124416068c3cb096bab9df17fa4da19bc68dfe082e", + "export_path": "sources/allocation/vendor/TEMPLATE.json.gz", + "bytes": 1124331 + }, + { + "path": "research/rank7-joint-endframes/construction/allocation/T37-FACE-MIX.json", + "usage": "provenance", + "pin": "head:be191346391661f4d35fc0d1508d0a6029572576:research/rank7-joint-endframes/construction/allocation/T37-FACE-MIX.json", + "git_blob": "6e6c97d6bdcc4f81051968ae0be99a2299f72157", + "sha256": "10598b7ea2e26fbd49db2b4d2f08122415fd6673b87fb7b458019d503ae60744", + "export_path": "sources/construction/allocation/T37-FACE-MIX.json", + "bytes": 1987 + }, + { + "path": "research/rank7-joint-endframes/construction/allocation/T37-PATTERNS.json", + "usage": "provenance", + "pin": "head:be191346391661f4d35fc0d1508d0a6029572576:research/rank7-joint-endframes/construction/allocation/T37-PATTERNS.json", + "git_blob": "7fbf9e238f3509c4603534c14e4ab931e2f4ccac", + "sha256": "df09e4581d7ed73fa22253909197ceb26ced59333f50c008c822894a4082f0e4", + "export_path": "sources/construction/allocation/T37-PATTERNS.json", + "bytes": 1775 + }, + { + "path": "research/rank7-joint-endframes/construction/allocation/T37-FLOW.json.gz", + "usage": "provenance", + "pin": "head:be191346391661f4d35fc0d1508d0a6029572576:research/rank7-joint-endframes/construction/allocation/T37-FLOW.json.gz", + "git_blob": "592ca15f4390d83d694c15a5b7a5d1d6302ae674", + "sha256": "765c6b774ca207f715dd5f579995700f4787c1f4eb92a7855bfc1424f683eca4", + "export_path": "sources/construction/allocation/T37-FLOW.json.gz", + "bytes": 15002 + }, + { + "path": "research/rank7-joint-endframes/construction/allocation/fill17.py", + "usage": "provenance", + "pin": "head:be191346391661f4d35fc0d1508d0a6029572576:research/rank7-joint-endframes/construction/allocation/fill17.py", + "git_blob": "d2a51867833f7ee69997977693d278624f6deb0f", + "sha256": "933be460381d65ea04a6e7f288f977ba22a7e4068b69494d65c38ccd7e5f4dbf", + "export_path": "sources/construction/allocation/fill17.py", + "bytes": 34531 + }, + { + "path": "research/rank7-joint-endframes/allocation/vendor/independent_owners.py", + "usage": "provenance", + "pin": "head:be191346391661f4d35fc0d1508d0a6029572576:research/rank7-joint-endframes/allocation/vendor/independent_owners.py", + "git_blob": "16013201b19054f7e45398ecf10af74c9c6a9114", + "sha256": "77a848729159e271ba64f403dfd59dddb13044b17b2950fa56700f442e2fe461", + "export_path": "sources/allocation/vendor/independent_owners.py", + "bytes": 10057 + }, + { + "path": "research/rank7-joint-endframes/tools/relax.py", + "usage": "provenance", + "pin": "head:be191346391661f4d35fc0d1508d0a6029572576:research/rank7-joint-endframes/tools/relax.py", + "git_blob": "97dfe35c434283ca6e83818e61aed65740522f50", + "sha256": "0fed1c56b50a2e6d44deeeb6db0f1c7e1f71b86d1747130e1a9202216249a728", + "export_path": "sources/tools/relax.py", + "bytes": 17680 + }, + { + "path": "research/rank7-joint-endframes/certificates/RELAX-CAP.json", + "usage": "provenance", + "pin": "head:be191346391661f4d35fc0d1508d0a6029572576:research/rank7-joint-endframes/certificates/RELAX-CAP.json", + "git_blob": "14de38f85eedf4a96500173576184a439348328c", + "sha256": "b272680de5842f7fd5f442cd0aeadfd317fe6af266ddee1a1e0738a919ba856e", + "export_path": "sources/certificates/RELAX-CAP.json", + "bytes": 1795 + } + ], + "schema_version": 1, + "base_commit": "30f016dd79ee6a23c40d7dab44a9466c148c42dd" +} diff --git a/research/rank7-chronological-face/TASK.json b/research/rank7-chronological-face/TASK.json new file mode 100644 index 0000000000..6877672ebd --- /dev/null +++ b/research/rank7-chronological-face/TASK.json @@ -0,0 +1,77 @@ +{ + "schema_version": 1, + "task_id": "independent-moment", + "priority_revision": 5, + "base_commit": "30f016dd79ee6a23c40d7dab44a9466c148c42dd", + "original_card": { + "id": "independent-moment", + "question": "Does one changed supplier or assembly claim lack a source-bound independent check of a specific new implication?", + "starting_points": [ + "certificates/selected-result.json" + ], + "methods": [ + "Reconstruct the rank ledger from original operations rather than trusting its aggregate.", + "Implement certified moment inequalities through a different exact enclosure method." + ], + "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_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Record the selected certificate and complex_profile rather than taking a PR headline as input.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "List the existing independent checks for the exact selected or candidate sources. Pick a new changed input, missing binding or distinct failure mode; stop with a handoff if the proposed arithmetic check is already covered.", + "bottleneck_link": "Independent pricing prevents unsupported frontier claims and can reveal genuine accounting slack.", + "allowed_variations": [ + "Reconstruct either a source ledger or a numeric enclosure with a different method." + ], + "scope_change_triggers": [ + "Importing the primary function and calling its output independent verification." + ], + "overlap_terms": [ + "independent moment", + "rank histogram", + "exact enclosure" + ] + }, + "scope_status": "refined", + "actual_scope": "Independently prove the interval Hall obstruction and exact moment-preserving pattern repair needed by PR2979 rank-seven end-frame helper inventory, with source-bound final width-seven placement checks.", + "scope_change_reason": "The user limits work to mechanisms changing fully charged recursive cost. PR2979 changes helper boundaries and inventory. The new obligation is its chronology-to-pattern bridge, not another root evaluation or the already checked PR2942 invoice.", + "bottleneck_link": "A cost-preserving change of optimal-face pattern multiplicities can remove a chronological width-seven deficit without repaying the local end-frame saving. Exact Hall counts test that mechanism directly.", + "budget_minutes": 60, + "stop_rule": "Stop after the finite obstruction/repair implication and independent verification, or decisive defect. No new solver search, full supplier admission or new kappa.", + "outcome": "completed", + "evidence": "RESULT.json: all55,611 contiguous intervals, exact473 necessary threshold, all1,064 family points,271,728 literal helper placements, exact duplicatedT74/T37 geometry and all-tariff swap identity with13 mathematical rejection controls; no new kappa.", + "author": "Ross Richardson, with substantial OpenAI Codex assistance", + "ai_assistance": "Parent and separate GPT-6.1 Sol Max owner-allocation and asymptotic-bounds mathematical specialists; no independent human or formal-kernel review claimed.", + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/2612#discussioncomment-18977418", + "overlap": { + "open_prs": { + "fetched_at": "2026-10-16T16:03:07.881442+00:00", + "complete_pagination": true, + "records": 229 + }, + "discussions": { + "fetched_at": "2026-10-16T16:03:55.113269+00:00", + "complete_pagination": true, + "records": 1681 + }, + "closed_prs": { + "fetched_at": "2026-10-16T16:04:28.547941+00:00", + "complete_pagination": true, + "records": 2438 + } + }, + "open_questions": [ + { + "question": "What is the least cost-neutral swap count admitting a complete chronological fill within this one-parameter integer family?", + "why_it_matters": "A necessary interval cut may understate the swaps or other constraints needed for a literal allocation.", + "first_step": "Pin the interval473<=k<=1063 within this exact family and test complete chronological feasibility with exact role, source-window, compact-mask and physical-family constraints.", + "blocked_by": "One Hall cut and moment equality alone are not sufficient for full chronological feasibility; native/precision/outer/all-size obligations are separate." + } + ] +} diff --git a/research/rank7-chronological-face/VALIDATION.md b/research/rank7-chronological-face/VALIDATION.md new file mode 100644 index 0000000000..8a0ca73966 --- /dev/null +++ b/research/rank7-chronological-face/VALIDATION.md @@ -0,0 +1,34 @@ +# Verification scope and local evidence + +The registered CPython 3.12 replay passes with marker +`PASS_RANK7_CHRONOLOGICAL_FACE_NO_NEW_KAPPA`. The package uses the standard +library only, no solver, no source producer/owner imports and no network. + +The exact result covers 19 frozen exports (SHA256 and Git blob identity), +all 55,611 contiguous intervals, all 1,064 points of the stipulated integral +pattern family, and every one of the 271,728 final literal helper roles. +Two separately written mathematical implementations join at the exact +conditional paid and idle histograms. Thirteen mathematical corruption controls +and one frozen-byte corruption control reject; all checks use explicit +exceptions and remain active under `-O`. + +Commands: + +```sh +python3.12 scripts/research_package.py --package research/rank7-chronological-face +python3.12 -I -B -O research/rank7-chronological-face/verify.py --check-result +python3.14 -I -B -O research/rank7-chronological-face/verify.py --check-result +``` + +The last command is also run on a read-only Git-free export; its receipt must +equal the registered result, and every exported file is hashed before and after. +Exact publication and any hosted checks are reported separately from these +local checks. No GitHub workflow dispatch or rerun is requested. + +The mathematical scope is conditional on the source event template and ordered +native width registry. A valid literal mask/window allocation does not prove +native arbitrary-dirty-input arithmetic, phase/restoration interfaces, physical +stock or tape costs, prefix/precision, outer release or all-size transfer. +The all-tariff swap identity is a written argument; the interval maximum and +literal geometry are finite computations. Neither is formal-kernel or independent +human proof, and no new kappa or cap-attainment claim is made. diff --git a/research/rank7-chronological-face/VERIFY.json b/research/rank7-chronological-face/VERIFY.json new file mode 100644 index 0000000000..cded04d617 --- /dev/null +++ b/research/rank7-chronological-face/VERIFY.json @@ -0,0 +1,20 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py", + "--check-result" + ], + "timeout_seconds": 180, + "checks": "Independent source-window Hall counts, finite pattern family and all-tariff cost identity, shipped width-seven placement/projection, source pins and defect-sensitive controls." + } + ] +} diff --git a/research/rank7-chronological-face/independent_face.py b/research/rank7-chronological-face/independent_face.py new file mode 100644 index 0000000000..43627f4ec5 --- /dev/null +++ b/research/rank7-chronological-face/independent_face.py @@ -0,0 +1,223 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Independent exact arithmetic for PR2979's saturated pattern direction. + +No allocation producer, owner checker, LP solver or root routine is imported. +This checks finite bin-pattern arithmetic, not chronological realizability. +All gates remain active with Python -O. +""" + +from collections import Counter +from copy import deepcopy +from fractions import Fraction +import json +from pathlib import Path + + +CAPS = (8, 16, 32, 48) +WIDTHS = (4, 5, 6, 7, 8, 9) +T = 37 +LOCAL = {1: 2445, 2: 706, 3: 232, 4: 108, 5: 18, 8: 8} +INVENTORY = {4: 26, 5: 2, 6: 16, 7: 52, 8: 99, 9: 213} +BINS = {8: 24864, 16: 16576, 32: 16576, 48: 16576} +IDLE = {1: 8655, 3: 2478, 5: 864, 48: 14095} +PROFILE = {1: 822840, 2: 235098, 3: 79734, 4: 35964, + 5: 6858, 8: 2664, 48: 14095} +A = (32, (7, 8, 8, 9)) +B = (16, (7, 9)) +C = (16, (8, 8)) +D = (32, (7, 7, 9, 9)) +SWAP_LEFT = Counter({A: 1, B: 1}) +SWAP_RIGHT = Counter({C: 1, D: 1}) + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def plain(counter): + return {k: v for k, v in sorted(counter.items()) if v} + + +def load_json(path): + return json.loads(path.read_text()) + + +def decode(target, widths): + need(tuple(widths) == WIDTHS, "source width order") + result = Counter() + for row in target: + need(type(row) is list and len(row) == 3, "source pattern row") + cap, counts, multiplicity = row + need(type(cap) is int and cap in CAPS, "source capacity") + need(type(counts) is list and len(counts) == len(widths), "source count vector") + need(all(type(n) is int and n >= 0 for n in counts), "source width counts") + need(type(multiplicity) is int and multiplicity > 0, "source multiplicity") + pattern = tuple(w for w, n in zip(widths, counts) for _ in range(n)) + key = (cap, pattern) + need(key not in result, "duplicate source pattern") + result[key] = multiplicity + return result + + +def measure(patterns): + bins, inventory, residual, by_cap = Counter(), Counter(), Counter(), Counter() + for (cap, widths), count in patterns.items(): + need(type(count) is int and count >= 0, "nonnegative integral pattern counts") + need(cap in CAPS and all(w in WIDTHS for w in widths), "allowed pattern") + remainder = cap - sum(widths) + need(remainder >= 0, "pattern over capacity") + bins[cap] += count + for width in widths: + inventory[width] += count + residual[remainder] += count + by_cap[cap, remainder] += count + return tuple(plain(c) for c in (bins, inventory, residual, by_cap)) + + +def family(k): + need(type(k) is int and 0 <= k <= 1063, "family parameter outside 0..1063") + return Counter({ + (8, (8,)): 24864, + B: 16253 - k, C: 323 + k, + (32, (9, 9, 9)): 864, + A: 1063 - k, D: k, + (32, (6, 8, 9, 9)): 5328, + (32, (5, 9, 9, 9)): 666, + (32, (4, 9, 9, 9)): 8655, + (48, ()): 14095, + (48, (9, 9, 9, 9, 9)): 2478, + (48, (4, 8, 9, 9, 9, 9)): 3, + }) + + +def validate_mix(mix): + need(mix["T"] == T, "source T37") + patterns = decode(mix["target"], mix["widths"]) + bins, inventory, residual, by_cap = measure(patterns) + need(bins == BINS, "bins by capacity") + need(inventory == {w: 9 * T * n for w, n in INVENTORY.items()}, "width inventory") + idle = {r: n for r, n in residual.items() if r} + need(idle == IDLE, "residual histogram") + profile = Counter({r: 9 * T * n for r, n in LOCAL.items()}) + profile.update(idle) + need(plain(profile) == PROFILE, "complete paid profile") + need({int(r): n for r, n in mix["profile"].items()} == PROFILE, "claimed profile") + need({int(r): n for r, n in mix["idle"].items()} == IDLE, "claimed idle histogram") + need(plain(patterns) == plain(family(1063)), "source family endpoint") + return bins, inventory, residual, by_cap + + +def symbolic_target_reduced_cost(cap_receipt): + """Compute the basis dual symbolically in independent formal tariff values. + + H(0)=0 is the source convention here. No positivity or optimality is inferred. + The target's zero result also follows directly from the column relation. + """ + basis = cap_receipt["basis_patterns"] + columns = [[Fraction(cap == p["capacity"]) for cap in CAPS] + + [Fraction(p["widths"].count(w)) for w in WIDTHS] for p in basis] + size = len(CAPS) + len(WIDTHS) + need(len(columns) == size, "ten-column relaxation basis") + matrix = [[columns[j][i] for j in range(size)] + + [Fraction(i == j) for j in range(size)] for i in range(size)] + for col in range(size): + pivot = next((i for i in range(col, size) if matrix[i][col]), None) + need(pivot is not None, "nonsingular source basis") + matrix[col], matrix[pivot] = matrix[pivot], matrix[col] + value = matrix[col][col] + matrix[col] = [v / value for v in matrix[col]] + for row in range(size): + if row != col: + value = matrix[row][col] + matrix[row] = [v - value * p for v, p in zip(matrix[row], matrix[col])] + inverse = [row[size:] for row in matrix] + target = [Fraction(cap == D[0]) for cap in CAPS] + [Fraction(D[1].count(w)) for w in WIDTHS] + coefficients = Counter() + for i, p in enumerate(basis): + remainder = p["capacity"] - sum(p["widths"]) + if remainder: + coefficients[remainder] -= sum(inverse[i][j] * target[j] for j in range(size)) + need(not plain(coefficients), "symbolic target reduced cost") + return {} + + +def verify_face(package_root=None): + root = Path(package_root) if package_root is not None else Path(__file__).resolve().parent + source = root / "sources" + mix = load_json(source / "construction/allocation/T37-FACE-MIX.json") + receipt = load_json(source / "certificates/RELAX-CAP.json") + measured = validate_mix(mix) + need(measure(SWAP_LEFT) == measure(SWAP_RIGHT), "all-tariff swap identity") + need(all(sum(widths) == cap for cap, widths in SWAP_LEFT | SWAP_RIGHT), "saturated swap bins") + for k in range(1064): + patterns = family(k) + need(measure(patterns) == measured, "complete family invariants") + outside = sum(count * widths.count(7) for (cap, widths), count in patterns.items() if cap != 16) + need(outside == 1063 + k, "width-7 outside count") + need({int(r): n for r, n in receipt["local_per_call"].items()} == LOCAL, "source local profile") + need({int(w): n for w, n in receipt["inventory_per_call"].items()} == INVENTORY, "source per-call inventory") + cap_idle = {int(r): Fraction(n) * T for r, n in receipt["idle_per_replica"].items()} + delta = plain({r: Fraction(IDLE.get(r, 0)) - cap_idle.get(r, 0) for r in set(IDLE) | set(cap_idle)}) + need(delta == {1: Fraction(-3), 3: Fraction(-57, 20), 5: Fraction(15, 4), 48: Fraction(-3, 20)}, "integral versus cap histogram") + need(sum(r * n for r, n in delta.items()) == 0 and delta, "equal mass is not equal tariff") + need(symbolic_target_reduced_cost(receipt) == {}, "zero symbolic reduced cost") + t74 = {int(r): n for r, n in load_json(source / "allocation/PROFILE.json").items()} + need(t74 == {r: 2 * n for r, n in PROFILE.items()}, "T74 doubled profile") + need(sum(INVENTORY.values()) == 408, "408 helpers per call") + need(sum(r * n for r, n in PROFILE.items()) == 65088 * T, "complete rank mass") + rejected = [] + + def reject(name, operation, reason): + try: + operation() + except ValueError as error: + need(str(error) == reason, "wrong rejection reason: " + name) + rejected.append({"name": name, "reason": reason}) + else: + raise ValueError("accepted corruption: " + name) + + reject("negative_family_endpoint", lambda: family(-1), "family parameter outside 0..1063") + reject("upper_family_endpoint", lambda: family(1064), "family parameter outside 0..1063") + bad = deepcopy(mix) + bad["target"][0][2] += 1 + reject("source_count_increment", lambda: validate_mix(bad), "bins by capacity") + bad_inventory = deepcopy(mix) + bad_inventory["target"][1][2] -= 1 + bad_inventory["target"][2][2] += 1 + reject("capacity_preserving_source_count_change", lambda: validate_mix(bad_inventory), "width inventory") + bad_profile = deepcopy(mix) + bad_profile["profile"]["1"] += 1 + bad_profile["profile"]["2"] -= 2 + bad_profile["profile"]["3"] += 1 + reject("rank_mass_preserving_claimed_profile", lambda: validate_mix(bad_profile), "claimed profile") + wrong = Counter({C: 1, A: 1}) + need(measure(wrong)[0] == measure(SWAP_LEFT)[0] and measure(wrong)[2] == measure(SWAP_LEFT)[2], "wrong swap preserves capacities and residuals") + reject("saturated_wrong_swap_inventory", lambda: need(measure(wrong)[1] == measure(SWAP_LEFT)[1], "width inventory changed"), "width inventory changed") + tie_left = Counter({(16, (4, 5)): 1, (16, (6, 7)): 1}) + tie_right = Counter({(16, (4, 6)): 1, (16, (5, 7)): 1}) + left, right = measure(tie_left), measure(tie_right) + need(left[:2] == right[:2] and sum(r*n for r,n in left[2].items()) == sum(r*n for r,n in right[2].items()), "rank-mass tie control premises") + need(sum(n for r,n in left[2].items() if r) == sum(n for r,n in right[2].items() if r) == 2, "rank-mass tie child count") + need(sum(r*r*n for r,n in left[2].items()) == 58 and sum(r*r*n for r,n in right[2].items()) == 52, "explicit tariff distinction") + reject("inventory_and_mass_tie_wrong_histogram", lambda: need(left[2] == right[2], "residual histogram changed"), "residual histogram changed") + return { + "status": "PASS_INDEPENDENT_RANK7_FACE_ARITHMETIC", + "source_commit": "be191346391661f4d35fc0d1508d0a6029572576", + "integer_family": {"first": 0, "last": 1063, "verified_points": 1064, + "source_parameter": 1063, "width7_outside_cap16": "1063+k"}, + "T37": {"replicas": T, "calls": 9*T, "helper_roles": 9*T*408, + "bins": BINS, "inventory": measured[1], "idle": IDLE, + "zero_residual_bins": measured[2][0], "profile": PROFILE, + "rank_mass": 65088*T}, + "T74_profile": t74, + "integral_minus_fractional_cap_idle": {str(r): str(v) for r, v in delta.items()}, + "target_symbolic_reduced_cost": {}, + "controls": rejected, + "scope": "finite bin-pattern arithmetic and written all-tariff identity; no chronology for all k, cap optimality/root replay, supplier admission or new kappa", + } + + +if __name__ == "__main__": + print(json.dumps(verify_face(), sort_keys=True, indent=2)) diff --git a/research/rank7-chronological-face/independent_hall.py b/research/rank7-chronological-face/independent_hall.py new file mode 100644 index 0000000000..cc5ec7dd3f --- /dev/null +++ b/research/rank7-chronological-face/independent_hall.py @@ -0,0 +1,375 @@ +# SPDX-License-Identifier: Apache-2.0 +"""Independent finite chronological cut and literal owner-geometry check. + +Only standard-library modules are imported. In particular, neither source owner +engine nor any producer/search code is executed or imported. The source JSON +widths and paid local profiles are premises; native circuit correctness is not +proved here. Run normally or with python3 -O; all checks use explicit exceptions. +""" + +import argparse +from collections import Counter, defaultdict +from copy import deepcopy +import gzip +import hashlib +import json +from pathlib import Path + + +SOURCE_COMMIT = "be191346391661f4d35fc0d1508d0a6029572576" +PORTS = 112 +T = 37 +HELPERS = 408 +INTERVAL = (45, 332) +SWAPS = 1063 + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def read_json(path): + data = path.read_bytes() + return json.loads(gzip.decompress(data) if path.suffix == ".gz" else data) + + +def symbolic_windows(template, plan): + """Resolve source-event endpoints once in stage labels, before any retiming.""" + child_ports = defaultdict(dict) + for row in template["idle_children"]: + c, p, rank = row["child"], row["port"], row["rank"] + require(p not in child_ports[c], "duplicate source child/port") + child_ports[c][p] = rank + require(set(child_ports) == set(range(18)), "retained source child coverage") + ranks = {} + for c, ports in child_ports.items(): + require(set(ports) == set(range(PORTS)), "source port coverage") + require(len(set(ports.values())) == 1, "source port rank consistency") + ranks[c] = ports[0] + local_pairs = {e["stage"]: e["pair"] for e in template["recipe"] + if e["kind"] == "local"} + require(set(local_pairs) == set(range(9)), "local stage coverage") + last_stage, endpoints = {}, {} + stage = None + seen_stages = [] + for event in template["execution_schedule"]: + kind = event["kind"] + if kind == "local_cover_sweep": + stage = event["stage"] + seen_stages.append(stage) + last_stage[local_pairs[stage]] = stage + elif kind == "bridge": + require(stage is not None, "bridge before source stage") + for pair in (event["src"], event["dst"]): + last_stage[pair] = stage + elif kind == "idle_cover_sweep": + require(stage is not None, "idle event before source stage") + pair = event["pair"] + for child in event["child_indices"]: + # Bank/padding children are not retained owner windows. + if child not in ranks: + continue + require(child not in endpoints, "duplicate retained idle endpoint") + require(plan["pairs"][str(child)] == pair, "source pair binding") + lo = last_stage.get(pair, -1) + require(lo < stage, "nonempty source stage window") + endpoints[child] = (ranks[child], lo, stage) + else: + require(kind in {"terminal_Y_translations", "terminal", + "bank_padding_cover_sweep", "translate_every_live_family"}, + "unrecognized source event") + require(seen_stages == list(range(9)), "source stage progression") + require(set(endpoints) == set(ranks), "complete retained endpoints") + return endpoints + + +def timed_windows(order, replicas, endpoints): + require(len(order) == 9 * replicas, "literal call count") + positions = {tuple(call): t for t, call in enumerate(order)} + require(set(positions) == {(s, r) for s in range(9) for r in range(replicas)}, + "literal call coverage") + for r in range(replicas): + require(all(positions[s, r] < positions[s + 1, r] for s in range(8)), + "replica source chronology") + return {(r, c): (cap, -1 if lo == -1 else positions[lo, r], positions[hi, r]) + for r in range(replicas) for c, (cap, lo, hi) in endpoints.items()} + + +def check_plan_windows(plan, windows): + expected = {f"{r},{c}": [cap, list(range(lo + 1, hi + 1))] + for (r, c), (cap, lo, hi) in windows.items()} + require(plan["windows"] == expected, "PLAN window equality") + + +def check_projection(order37, order74): + expected = [[s, r + T * b] for s, r in order37 for b in range(2)] + require(order74 == expected, "exact T74 call projection") + + +def interval_cut(windows, widths_by_call, first, last): + require(0 <= first <= last < len(widths_by_call), "cut interval bounds") + demand = sum(widths_by_call[t].count(7) for t in range(first, last + 1)) + counts = Counter(c for (r, c), (cap, lo, hi) in windows.items() + if cap == 16 and hi >= first and lo < last) + bins = PORTS * sum(counts.values()) + return {"interval_inclusive": [first, last], "calls": last - first + 1, + "width7_demand": demand, "cap16_abstract_windows_by_child": dict(counts), + "cap16_bins_touching": bins, "required_outside_cap16": max(0, demand - bins)} + + +def strongest_contiguous_cut(windows, widths_by_call): + """All 55,611 intervals, not arbitrary subsets or full scheduling feasibility.""" + n = len(widths_by_call) + prefix = [0] + for widths in widths_by_call: + prefix.append(prefix[-1] + widths.count(7)) + cap16 = [(lo + 1, hi) for cap, lo, hi in windows.values() if cap == 16] + best, attaining, checked = 0, [], 0 + for first in range(n): + arrivals = Counter(max(first, lo) for lo, hi in cap16 if hi >= first) + bins = 0 + for last in range(first, n): + bins += PORTS * arrivals[last] + bound = prefix[last + 1] - prefix[first] - bins + checked += 1 + if bound > best: + best, attaining = bound, [[first, last]] + elif bound == best: + attaining.append([first, last]) + return {"intervals_checked": checked, "maximum_required_outside_cap16": best, + "attaining_intervals_inclusive": attaining} + + +def geometry(rows, order, windows, dispatch, providers, plan): + """All literal roles; no native arithmetic or entering-frame proof.""" + require(len(rows) == len(order) * HELPERS, "complete literal role count") + helper_masks = [0] * len(order) + families = [set() for _ in order] + occupied, bin_widths = {}, defaultdict(list) + width7 = [0, 0] + outside = [0, 0] + cut_cap16, cut_other = [0, 0], [0, 0] + projected = [set(), set()] + for row in rows: + require(len(row) == 6 and all(type(x) is int for x in row), "integer role shape") + time, helper, owner, child, port, offset = row + require(0 <= time < len(order) and 0 <= helper < HELPERS and + 0 <= port < PORTS and (owner, child) in windows, "role bounds") + cap, lo, hi = windows[owner, child] + require(lo < time <= hi, "literal source window") + require(not helper_masks[time] & (1 << helper), "duplicate helper role") + helper_masks[time] |= 1 << helper + family = (owner, plan["pairs"][str(child)], plan["sides"][str(child)], port) + require(family not in families[time], "same-call physical family collision") + families[time].add(family) + width = providers[dispatch[tuple(order[time])]]["widths"][helper] + require(0 <= offset and offset + width <= cap, "literal bin capacity") + key = (owner, child, port) + mask = ((1 << width) - 1) << offset + require(not occupied.get(key, 0) & mask, "literal coordinate overlap") + occupied[key] = occupied.get(key, 0) | mask + bin_widths[key].append(width) + copy = order[time][1] // T + require(owner // T == copy, "source witness copy separation") + projected[copy].add((time // 2, helper, owner % T, child, port, offset)) + if width == 7: + width7[copy] += 1 + outside[copy] += cap != 16 + if INTERVAL[0] <= time // 2 <= INTERVAL[1]: + (cut_cap16 if cap == 16 else cut_other)[copy] += 1 + require(all(m == (1 << HELPERS) - 1 for m in helper_masks), "complete helper identities") + require(projected[0] == projected[1] and len(projected[0]) == 9 * T * HELPERS, + "exact T74 role projection") + idle, patterns = Counter(), Counter() + for (owner, child), (cap, lo, hi) in windows.items(): + for port in range(PORTS): + key = (owner, child, port) + mask = occupied.get(key, 0) + used = mask.bit_count() + require(mask == (1 << used) - 1, "literal compact prefix") + ws = bin_widths.get(key, []) + if cap == 16: + require(ws.count(7) <= 1, "cap16 one-width7 pattern restriction") + patterns[cap, tuple(sorted(ws))] += 1 + if used < cap: + idle[cap - used] += 1 + profile = Counter(idle) + for call in order: + profile.update({int(r): n for r, n in + providers[dispatch[tuple(call)]]["actual_paid_profile"].items()}) + return {"roles_checked": len(rows), "width7_roles_per_copy": width7, + "width7_outside_cap16_per_copy": outside, + "cut_width7_cap16_per_copy": cut_cap16, + "cut_width7_outside_cap16_per_copy": cut_other, + "projected_roles_per_copy": len(projected[0]), + "idle_profile": dict(sorted(idle.items())), + "conditional_complete_profile": dict(sorted(profile.items()))}, patterns + + +def verify_hall(package_root=None): + root = Path(package_root) if package_root is not None else Path(__file__).resolve().parent + manifest = read_json(root / "SOURCES.json") + require(manifest["source_commit"] == SOURCE_COMMIT, "frozen source commit") + exports = {row.get("export_path", row["path"]): row for row in manifest["files"]} + hashes = {} + + def source(name): + rel = "sources/" + name + path = root / rel + digest = hashlib.sha256(path.read_bytes()).hexdigest() + require(rel in exports and digest == exports[rel]["sha256"], "source hash: " + rel) + hashes[rel] = digest + return read_json(path) + + template = source("allocation/vendor/TEMPLATE.json.gz") + plan = source("allocation/vendor/PLAN.json.gz") + order74 = source("allocation/ORDER.json") + dispatch_rows = source("allocation/DISPATCH.json") + providers = source("allocation/PROVIDERS.json") + fill = source("allocation/FILL.json.gz") + face = source("construction/allocation/T37-FACE-MIX.json") + patterns_record = source("construction/allocation/T37-PATTERNS.json") + order37 = plan["order"] + endpoints = symbolic_windows(template, plan) + windows37 = timed_windows(order37, T, endpoints) + check_plan_windows(plan, windows37) + check_projection(order37, order74) + windows74 = timed_windows(order74, 2 * T, endpoints) + dispatch = {(s, r): provider for s, r, provider in dispatch_rows} + require(len(dispatch_rows) == len(dispatch) == len(order74) and + set(dispatch) == set(map(tuple, order74)) and + set(dispatch.values()) <= set(providers), "literal dispatch coverage") + require(all(dispatch[s, r] == dispatch[s, r + T] for s, r in order37), + "T74 provider projection") + expected_inventory = Counter({4: 26, 5: 2, 6: 16, 7: 52, 8: 99, 9: 213}) + require(all(Counter(p["widths"]) == expected_inventory for p in providers.values()), + "source provider width inventory") + widths37 = [providers[dispatch[s, r]]["widths"] for s, r in order37] + cut = interval_cut(windows37, widths37, *INTERVAL) + require(cut["width7_demand"] == 14976, "cut demand") + require(cut["cap16_bins_touching"] == 13440, "cut accessible bins") + require(cut["required_outside_cap16"] == 1536, "cut outside requirement") + strongest = strongest_contiguous_cut(windows37, widths37) + require(strongest == {"intervals_checked": 55611, + "maximum_required_outside_cap16": 1536, + "attaining_intervals_inclusive": [[45, 332]]}, + "complete contiguous-interval maximum") + require(face["target"] == patterns_record["target"], "final source pattern agreement") + require(face["widths"] == [4, 5, 6, 7, 8, 9], "pattern width ordering") + final = Counter({(cap, tuple(counts)): n for cap, counts, n in face["target"]}) + swap = Counter({(16, (0, 0, 0, 0, 2, 0)): 1, + (32, (0, 0, 0, 2, 0, 2)): 1, + (16, (0, 0, 0, 1, 0, 1)): -1, + (32, (0, 0, 0, 1, 2, 1)): -1}) + keys = set(final) | set(swap) + base = {key: final[key] - SWAPS * swap[key] for key in keys} + width7_index = face["widths"].index(7) + reserves = [] + for k in range(SWAPS + 1): + mix = {key: base[key] + k * swap[key] for key in keys} + require(min(mix.values()) >= 0, "nonnegative face-family multiplicities") + require(all(counts[width7_index] <= 1 for (cap, counts), n in mix.items() + if cap == 16 and n), "face-family one-width7 restriction") + outside = sum(n * counts[width7_index] for (cap, counts), n in mix.items() + if cap != 16) + require(outside == SWAPS + k, "exact face-family outside reserve") + reserves.append(outside) + first_pass = next(k for k, n in enumerate(reserves) if n >= 1536) + require(first_pass == 473 and reserves[472] == 1535 and reserves[473] == 1536, + "sharp necessary face-family threshold") + require(fill["columns"] == ["time", "helper", "owner_replica", "child", "port", "offset"], + "literal FILL columns") + require(fill["dispatch_overrides"] == [], "no unhandled fill dispatch overrides") + witness, actual_patterns = geometry(fill["rows"], order74, windows74, + dispatch, providers, plan) + expected_patterns = Counter() + for (cap, counts), n in final.items(): + ws = tuple(w for w, count in zip(face["widths"], counts) for _ in range(count)) + expected_patterns[cap, ws] += 2 * n + require(actual_patterns == expected_patterns, "literal final face pattern coverage") + require(witness["width7_roles_per_copy"] == [17316, 17316] and + witness["width7_outside_cap16_per_copy"] == [2126, 2126], + "literal width7 counts") + controls = [] + + def reject(name, fn, message): + try: + fn() + except ValueError as error: + require(str(error) == message, "incorrect control rejection: " + name) + controls.append({"name": name, "reason": message}) + else: + raise ValueError("accepted defect: " + name) + + # A real role moved to its excluded source endpoint, preserving all widths. + row_index = next(i for i, row in enumerate(fill["rows"]) + if windows74[row[2], row[3]][1] >= 0 and + providers[dispatch[tuple(order74[row[0]])]]["widths"][row[1]] == 7) + rows = list(fill["rows"]) + changed = list(rows[row_index]) + changed[0] = windows74[changed[2], changed[3]][1] + rows[row_index] = changed + reject("role_at_excluded_lower_endpoint", + lambda: geometry(rows, order74, windows74, dispatch, providers, plan), + "literal source window") + bad_plan = {**plan, "windows": deepcopy(plan["windows"])} + key = next(key for key, value in bad_plan["windows"].items() if value[1][0] > 0) + bad_plan["windows"][key][1].insert(0, bad_plan["windows"][key][1][0] - 1) + reject("expanded_source_window", lambda: check_plan_windows(bad_plan, windows37), + "PLAN window equality") + rows = list(fill["rows"]) + first, second = rows[0], list(rows[1]) + require(first[0] == second[0], "family control same call") + second[2:5] = first[2:5] + rows[1] = second + reject("duplicate_same_call_physical_family", + lambda: geometry(rows, order74, windows74, dispatch, providers, plan), + "same-call physical family collision") + reject("missing_width7_role", + lambda: geometry(fill["rows"][:row_index] + fill["rows"][row_index + 1:], + order74, windows74, dispatch, providers, plan), + "complete literal role count") + def false_demand(): + require(cut["width7_demand"] - 1 == sum(widths37[t].count(7) + for t in range(INTERVAL[0], INTERVAL[1] + 1)), "cut demand") + reject("undercounted_width7_demand", false_demand, "cut demand") + bad_order = deepcopy(order74) + bad_order[0], bad_order[1] = bad_order[1], bad_order[0] + reject("changed_interleaving_endpoint", lambda: check_projection(order37, bad_order), + "exact T74 call projection") + naive_priority = [list(call) for call in sorted(map(tuple, order37), + key=lambda call: (4 * call[0] + call[1], call[0], call[1]))] + require(naive_priority != order37, "source chronology differs from naive priority") + require(all(hashlib.sha256((root / p).read_bytes()).hexdigest() == h + for p, h in hashes.items()), "source input drift") + return {"status": "PASS_INDEPENDENT_CHRONOLOGICAL_FACE_CUT", + "source_commit": SOURCE_COMMIT, "source_sha256": hashes, + "symbolic_stage_windows": {str(k): list(v) for k, v in endpoints.items()}, + "PLAN_matches_priority_4s_plus_r": False, "T37_windows_checked": len(windows37), + "T74_exact_call_and_role_projection": True, "cut": cut, + "all_contiguous_intervals": strongest, + "face_family": {"integer_k_inclusive": [0, 1063], + "outside_width7_formula": "1063+k", + "necessary_k_lower_bound": first_pass, + "k472": "REJECTED_BY_CUT", + "k473": "PASSES_THIS_NECESSARY_CUT_ONLY"}, + "literal_witness": witness, "controls": controls, + "scope": "Finite literal owner geometry conditional on source ordered provider widths; " + "written necessary inequality for this fixed pattern face. No sufficiency, " + "native circuit admission, formal kernel proof, or new kappa claim."} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--out", type=Path) + args = parser.parse_args() + result = verify_hall() + text = json.dumps(result, indent=2, sort_keys=True) + "\n" + if args.out: + args.out.write_text(text, encoding="utf8") + print(text, end="") + + +if __name__ == "__main__": + main() diff --git a/research/rank7-chronological-face/sources/CREDITS.md b/research/rank7-chronological-face/sources/CREDITS.md new file mode 100644 index 0000000000..5f41978420 --- /dev/null +++ b/research/rank7-chronological-face/sources/CREDITS.md @@ -0,0 +1,16 @@ +# Credits + +- **PR #2908, Jeremy Diviney**: the paired input/output extraction, its compensation rule `C*S`, the exact two-sided certificate (`structure.py`, vendored unchanged) and the closed-adapter admission chain. +- **PR #2917, Mason Hale**: the nine paired extractions and 82-endpoint words under PR2942, the refit/compose producer model that stage 2 follows, the T74 chronology (ORDER/DISPATCH), the allocation checker, moment auditor, extension stage and adapter derivation reused here. +- **PR #2957 / #2948 / #2966, Jeremy Kothe (jeremykothe2)**: the fourteen declared exactness-preserving gate rewrites in five classes (R-retime, A3779-cut-start-read, PM-carrier-lender-entry, B-carrier-retime, A-commuting-swap) and their pure applier (`vendor/declared_rewrites.py`, vendored unchanged); stage 3 composes exactly these rewrites onto this package's stage-2 word (`data/REWRITES-2957.json`, re-addressed with exact preimages). PR2966 composed the same rewrites onto our PR2942 words. +- **PR #2969, Dugongue**: the PR2942 + PR2957 composition at T370 and its cap-level headline nomination, this package's comparator and moment baseline (`allocation/baseline/`). Our stage 3 composes the same fourteen rewrites, here onto the stage-2 word. +- **PR #2918 (research/helper408-rank7-pairing), RossRichardson**: the fixed-cut rank-seven obstruction for helper408; this package's census of fresh rank-7 extractions reproduces it exactly and is consistent with it. +- **PR #2894 / #2833, Jeremy Kothe**: the preload re-synthesis supplier, the frame accounting and inverse-reverse cleanup (`vendor/preload_move.py`), the source materializer and the inherited supplier lineage. +- **PR #2857 / #2848, Yiyang Lu (Lyy-iiis)**: the shared-kernel words, the staged native/overlay tooling and the chronological flow model and realization (edge colouring) used to construct the allocation; PR2843 (Marius-Paul Dumitrean) is that flow model's starting point. +- **PR #2863 / #2839, Dugongue**: the packing lineage and the PR2839 owner engine. +- **Tekalign**: the independent owner/chronology checker (`allocation/vendor/independent_owners.py`) and admission tooling. +- **icekylinx**: the exact free-operator auditor retained as `vendor/audit_local.py` (PR2833). +- **themilkman216**: the observation that a cap-level allocation of these inventories needs a T whose basic counts are integral, which the allocation's degenerate-face step builds on. +- **Gareth Davidson (bitplane), PR #1995 / #2013**: the fixed-word terminal-subspace bounds that frame stage 1's scope; earlier rank-seven helper ends on other words are in `research/complex-rank7-end-pair`, `research/k8-rank7-composition` and the PR1090/PR1104 lineage (credited there). +- **PR #2930 / #2942, Marius-Paul Dumitrean**: the cap allocation of PR2917's words, the four normal-45 extractions under these words, the relaxation tools and the overlay/producer conventions reused here. +- **New here (Marius-Paul Dumitrean, with substantial AI assistance from Anthropic Claude via Claude Code)**: the codimension-2 census on paired-extraction words, the joint end-frame lowering of 22 restored helpers in five groups (stage 1), the five further extractions it makes profitable (stage 2), the exact composition with PR2957's rewrites (stage 3), the producer and local verification for all three stages, the overlay stage `rank7-joint-endframes` with its rebuild guards, the adapter generalization to six width classes, the literal T74 allocation of the changed inventory, its relaxation certificates and recorded gap, and the complete fresh replay. diff --git a/research/rank7-chronological-face/sources/NOTICE b/research/rank7-chronological-face/sources/NOTICE new file mode 100644 index 0000000000..9df951052a --- /dev/null +++ b/research/rank7-chronological-face/sources/NOTICE @@ -0,0 +1,26 @@ +research/rank7-joint-endframes +Copyright 2026 Marius-Paul Dumitrean. Licensed under the Apache License, Version 2.0. +Prepared with substantial AI assistance (Anthropic Claude, via Claude Code). + +This package retains, byte-identical, Apache-2.0 files from: PR #2942 (Marius-Paul Dumitrean, head +a027b0f6fdb0ab2b42ba10fc31b53960166bf2bf, research/paired-extension-normal45): data/PARENT-base.json.gz and +data/PARENT-extra.json.gz (its data/WORD-*.json.gz), comparators/PR2942-CLAIM.json and tools/wordedit.py; PR #2917 +(Mason Hale, head 224bd5e56041c40078ff6b5fa7393733a215de5c, research/paired-helper-extension): structure.py (Jeremy +Diviney's PR2908 two-sided certificate checker), vendor/audit_local.py (PR2833's independent exact auditor, icekylinx +attribution), vendor/preload_move.py (Jeremy Kothe's PR2894 frame accounting and cleanup), allocation/ORDER.json, +allocation/DISPATCH.json and allocation/vendor/ (independent_owners.py: Tekalign's independent owner checker as vendored +by PR2839/PR2917; PLAN.json.gz, TEMPLATE.json.gz); PR #2957 (Jeremy Kothe, head b74b25f3ccc84c16e1a801d73b2f47e5ea764c78, +research/paired-extension-cap-fill-swaps): vendor/declared_rewrites.py (the pure applier of the fourteen declared +rewrites) and comparators/PR2957-CLAIM.json; PR #2966 (Jeremy Kothe, head e62d3eb9005117d82a9babcfa937ecc53237c490, +research/paired-extension-normal45-rewrites): comparators/PR2966-CLAIM.json; PR #2969 (Dugongue, head +e2ca469b08385d3d5e29a918d66dbefaf889e9f3, research/paired-swap-normal45): allocation/baseline/ (its CLAIM.json and its +allocation ORDER.json and PROFILE.json); and PR #2930 (head 81f3b5d12977eba09e06fbff729167d59faabe90): tools/relax.py, +tools/root.py, tools/relax_exact.py. +data/REWRITES-2957.json is Jeremy Kothe's PR2957 rewrite list, re-addressed to this package's stage-2 word with exact +preimages (every entry keeps a credit field). producer.py follows PR2917's producer.py (Mason Hale) for its paired steps; +verify.py, check_allocation.py, check_cap.py, run_registered.py and reproduce.py adapt our PR2942 versions of PR2917's and +PR2930's; tools/audit_allocation_moment.py is PR2917's exact moment auditor with only its authenticated baseline changed (to +the PR2969 headline); tools/derive_adapters.py generalizes PR2917's adapter derivation (PR2908, Jeremy Diviney); +tools/build_overlay.py follows the overlay conventions of PR2908's and PR2917's builders. construction/allocation/ retains +the flow model of PR2857/PR2843 (Yiyang Lu, Marius-Paul Dumitrean) as adapted for this allocation. All original notices of +the exported predecessor packages remain in force. diff --git a/research/rank7-chronological-face/sources/PINS.json b/research/rank7-chronological-face/sources/PINS.json new file mode 100644 index 0000000000..d71aaccbae --- /dev/null +++ b/research/rank7-chronological-face/sources/PINS.json @@ -0,0 +1,31 @@ +{ + "certificates/RELAX-CAP.json": "b272680de5842f7fd5f442cd0aeadfd317fe6af266ddee1a1e0738a919ba856e", + "certificates/RELAX-STAGES.json": "0e5ec700a191b668ba3d4b6d675f5c047d264b9a5109fc55fa92961b3fcb7d68", + "comparators/PR2942-CLAIM.json": "011aaac80ad79f7f29dc429a672441bb6b3c21a68bbcb34c7a0d5f943c3c3c2e", + "comparators/PR2957-CLAIM.json": "a93e6c9e94bc9bf5664b5e23506dda9647fad1930e1eede66d5ba9f3718b598a", + "comparators/PR2966-CLAIM.json": "4d4c4800bf3bcb36d09021313b2712aebd4aa0830c74dda30991daf6851c220a", + "construction/STAGE-PRICES.json": "dfb7d06724bf95367f3fdb398f4828fc70f803d23030bc0eee0b00541457f546", + "data/PARENT-base.json.gz": "54ca34c749e3228d7e2df3d8dbf7aa1568c2872490166997c5962f12fd03da35", + "data/PARENT-extra.json.gz": "eded756dfe8f411c3d1f80a3ac16516f0ea5dd6f9866728b2179b157630fa7b6", + "data/REWRITES-2957.json": "a37ade675876e4f5b00b33066c84f495fccd264863b7eb5d813837b1d01c3e7d", + "data/STAGE1-FRAME-EDITS.json": "5fbfce004330ebc1fbac8de264614fe295f1a074811b478db4892c3bc3852cd3", + "data/TRANSFORM-226.json": "1732a39728c068f9d663111c7876b4e0b96088f3dd3b8e6ff824551b5a711338", + "data/TRANSFORM-228.json": "82346e6a5173c4822e16b2dad06ca232111b6795a340079f9aceabe0098797c0", + "data/TRANSFORM-230.json": "8ad70d545695b5d2246fb9e09d46abcc1e42926c1161884f69b77f978a28f46d", + "data/TRANSFORM-363.json": "84d2a609739eb30d4d9356fb6f04b2ff32c8823a978d7a51db1ace1d6d2352cc", + "data/TRANSFORM-395.json": "065aa5d7713683942bc2156b543681857e33c6e2f30f32cba47e2cbb9d1bef69", + "data/WORD-base.json.gz": "abaf67bfcb257528658c906b612f57025617592bd7889828f92b97a5f4f4300d", + "data/WORD-extra.json.gz": "e0eaf64c4d5d324693d43889bce1b9e53e8da00402105c8c978fd102f208bed7", + "producer.py": "d4577cee26314b36b59723cc68df9b8895b22449cc15807c95f325f555c4da3a", + "structure.py": "83f63b6d9a1a543ecfa2c98d479dbe4e7a1c3caf6fd1c3566123308efbc32e96", + "tools/audit_allocation_moment.py": "c632527ecf092f013862660dbd7f52b599a50b321a8aa88ddc45af0547e79cb5", + "tools/build_overlay.py": "9d98ace9bffb37aeebd05b93ed386f73e6eee169d960e4956cf14a66e6852140", + "tools/derive_adapters.py": "5c06828151cd230add3e328b42dda72c4a2ed1075bd2902f38ee28727870bc84", + "tools/relax.py": "0fed1c56b50a2e6d44deeeb6db0f1c7e1f71b86d1747130e1a9202216249a728", + "tools/relax_exact.py": "baf1855d6095c951a90d19a0d8094bd33290519940b732e2b758c5647830f044", + "tools/root.py": "55f5aca39b5ee2fe4687ac8863e6c24569010f27a332883c069b8e14b8fe09e3", + "tools/wordedit.py": "cae8ae0f5d7fb3387ec6922fe966068aae05e3a6d3586830d4361b650cfb3617", + "vendor/audit_local.py": "a38940094f7d19cd6376aafdd4734fa68eabc9aff4c98c3c4a3e9540328b1c90", + "vendor/declared_rewrites.py": "2509f1335e47543f8814b42d6bf83032b30c5899b4f7cc62a6adc03f5138ae13", + "vendor/preload_move.py": "c8fda4674644fcd5cbf39b6645ce148a21daa90a998b678cbe51f970b78b0044" +} diff --git a/research/rank7-chronological-face/sources/README.md b/research/rank7-chronological-face/sources/README.md new file mode 100644 index 0000000000..ad4fde6983 --- /dev/null +++ b/research/rank7-chronological-face/sources/README.md @@ -0,0 +1,273 @@ +# Joint rank-7 end frames, five more paired extractions and PR #2957's rewrites on PR #2942's words: conditional κ = 0.001729033982646513517717 − 10⁻⁴⁶ − 10⁻⁷⁰ + +```text +Status / UTC update / priority revision: DONE (conditional candidate) · 2026-10-16 · priority revision 5 · base main 484a8ade +Concrete question and changed premise: the fill layer of PR2942's words with PR2957's rewrites is exhausted (PR2969 attains + their packing cap), so a gain must change the words. Paired extraction restores helpers at rank-8 hyperplanes, and every + further extraction on PR2942's words is below break-even. Can restored helpers end one dimension lower (at shared rank-7 + subspaces), and does that make further extractions profitable? +Established result and evidence status: yes. Lowering the end frames of 22 restored helpers jointly, in five groups that + each share one rank-7 subspace (frame-only), pays where every single lowering loses; it makes five further paired + extractions profitable (normal 42: 226, 228, 230; normal 7: 363, 395); Jeremy Kothe's fourteen PR2957 rewrites compose + exactly on top. With a new literal T74 allocation, the complete fresh-native admission and modern outer release pass: + κ = 0.001729033982646513517717 − 10⁻⁴⁶ − 10⁻⁷⁰, exactly 4998757898408639167/10²⁴ ≈ 4.9988e-6 above PR2969 + (Dugongue, head e2ca469b) and ≈ 4.9997e-6 above PR2966. Author-checked (AI-assisted); not maintainer-reviewed. +Public artifact URL + exact commit: this package (see the PR). +Next useful task: census of one-dimension lowerings of the five new pivots and their partners; normals 25/52 with other pivots. +Active claim / expiry: released. +``` + +## Result + +| | κ (headline; each − 10⁻⁴⁶ − 10⁻⁷⁰) | local profile per call | width inventory | private buffers | +|---|---|---|---|---:| +| PR #2942 (our four normal-45 extractions) | 0.001722816319863214327996 | {1:2434, 2:632, 3:286, 4:104, 5:26, 8:8} | {4:26, 5:2, 7:62, 8:100, 9:218} | 86 | +| PR #2957 (Jeremy Kothe; PR2917 words + 14 rewrites) | 0.001723717415070738170971 | {1:2412, 2:636, 3:276, 4:116, 5:26, 8:8} | {4:26, 5:2, 7:62, 8:96, 9:222} | 82 | +| PR #2966 (Jeremy Kothe; PR2942 words + 14 rewrites) | 0.001724034272523452177412 | {1:2430, 2:628, 3:282, 4:110, 5:26, 8:8} | {4:26, 5:2, 7:62, 8:100, 9:218} | 86 | +| PR #2969 (Dugongue; same words at T370, outer release pending) | 0.00172403522474810487855 | same as PR2966 | same | 86 | +| **this package** | **0.001729033982646513517717** | **{1:2445, 2:706, 3:232, 4:108, 5:18, 8:8}** | **{4:26, 5:2, 6:16, 7:52, 8:99, 9:213}** | **91** | + +Exact gains of the headline: over PR2969 `4998757898408639167/10²⁴` ≈ **4.9988e-6** (0.290%); over PR2966 +`999942024612268061/(2·10²³)` ≈ 4.9997e-6; over PR2957 `2658283787887673373/(5·10²³)` ≈ 5.3166e-6; over PR2942 +`6217662783299189721/10²⁴` ≈ 6.2177e-6 (`check_cap.py` recomputes all four from the pinned CLAIM.json files). The complete +paid profile (T74, PR2917's chronology, ORDER/DISPATCH byte-identical) is {1:1645680, 2:470196, 3:159468, 4:71928, +5:13716, 8:5328, 48:28190}. Physical stock 66,304 + 408 + 8 + 91 + 2 = **66,813**; 632 independent inputs, 408 live helpers, +271,728 helper roles. PR2969's kappa is a moment nomination whose outer release is pending; this package's admission uses +it as the pinned comparator and its T370 ORDER/PROFILE as the moment baseline, and passes the complete release itself. + +## The three stages + +| stage | change (both providers, one declared record each) | local profile after | inventory after | buffers | literal price (units) | freed width units | margin | fixed-capacity cap | +|---|---|---|---|---:|---:|---:|---:|---| +| parent | PR2942's words | {1:2434, 2:632, 3:286, 4:104, 5:26, 8:8} | {7:62, 8:100, 9:218} | 86 | | | | 0.0017228172707 | +| 1 | 22 end frames lowered to five shared rank-7 subspaces; 139 gate frames (B 60, restore 79), each one dimension lower | {1:2430, 2:722, 3:236, 4:102, 5:18, 8:8} | {6:16, 7:52, 8:94, 9:218} | 86 | −46,150,994 | 22 | +142,394 | 0.0017262265796 | +| 2 | five paired extractions (normal 42: 226, 228, 230; normal 7: 363, 395), one declared frame change | {1:2449, 2:710, 3:236, 4:102, 5:18, 8:8} | {6:16, 7:52, 8:99, 9:213} | 91 | −10,523,403 | 5 | +66,903 | 0.0017278107473 | +| 3 | Jeremy Kothe's fourteen PR2957 rewrites, re-addressed with exact preimages | {1:2445, 2:706, 3:232, 4:108, 5:18, 8:8} | unchanged | 91 | −52,350 | 0 | +52,350 | 0.0017290357649 | + +(`4:26, 5:2` are unchanged throughout.) Prices are the certified frame solver's integer local costs in units of 2⁻⁴⁰ at the +base saving b ≈ 0.0017037 (c1 = 2,116,671, c2 = 4,228,346, c3 = 6,338,140, c4 = 8,446,713, c5 = 10,554,378); `verify.py` +recomputes every literal stage price from the frame-report profiles. Each lowered or extracted helper saves c1 locally (one +rank less in its end climb) and frees one width unit, which costs about 2,091,300 units of idle rank in the packing at +fixed capacity (the break-even); margins are −price − k × 2,091,300, so each helper may spend at most about **25,371 +units** on its partners. The caps are exact (`check_cap.py`, fixed-capacity +fractional relaxation, Fractions-only certificates for the parent and every stage). + +### Stage 1: why single rank-7 lowerings lose and joint lowering pays + +A restored helper `h` (one whose end frame is a declared `helper_final`, with its own private cleanup buffer) can end at +a smaller subspace W if every gate touching `h` has its frame inside W. Lowering `h` by one dimension saves one rank of its +end climb, but the gates touching `h` are mostly restore gates that it shares with other registers (its *partners*); their +frames must drop into W too, and the partners pay to climb back. A necessary condition is that W contain `L_h`, the solver's +lower bound at `h`'s last vertex; over all 86 restored helpers exactly 20 (end dimension 8, `L_h` of dimension 7, so +W = `L_h`) plus PR2942's four normal-45 pivots qualify, and no helper has room for two dimensions. + +Priced alone, every one of the 24 candidates is below break-even. But helpers whose `L_h` coincide share their partners, +and the partners drop into W **once** for the whole group: the overhead is paid once and the saving k times. Five groups +pay (helpers 586 and 588, each alone at its own W, stay at −3,345 and are not used): + +| group | shared rank-7 subspace W | helpers (width change) | single lowerings, margin each | joint price | joint margin | +|---|---|---|---|---:|---:| +| V45 | ⟨256, 128, 64, 35, 16, 11, 5⟩ = E_7 ∩ E_42 ∩ E_45 | 249, 251, 265, 267 (PR2942's pivots, 8 → 7) | −53,141 each | −8,388,172 | **+22,972** | +| A | ⟨256, 128, 64, 38, 20, 10, 1⟩ ⊂ E_30 | 331 (PR2917's step 4, 8 → 7); 450, 451, 508, 509 (entering, 7 → 6) | 331: −58,943; 450: −19,901; 451: −14,905; 508, 509: −21,782 | −10,499,041 | **+42,541** | +| B | ⟨256, 128, 64, 34, 17, 11, 4⟩ ⊂ E_51 | 299 (PR2917's step 5, 8 → 7); 448, 449, 484, 485 (7 → 6) | 299: −58,943; 448, 449: −14,905; 484, 485: −21,782 | −10,499,041 | **+42,541** | +| C | ⟨256, 128, 64, 32, 19, 11, 6⟩ | 452, 453, 532, 533 (entering, 7 → 6) | 453: −14,905; 452, 532, 533: −16,786 | −8,382,370 | **+17,170** | +| D | ⟨256, 128, 64, 37, 21, 8, 3⟩ | 454, 455, 556, 557 (entering, 7 → 6) | 454: −14,905; 455, 556, 557: −16,786 | −8,382,370 | **+17,170** | + +The groups are independent (every pairwise union prices exactly as the sum), the four V45 subsets climb monotonically +(−53,141 / −27,770 / −2,399 / +22,972 for one to four helpers), and leaving any one helper out of its group costs +23,490 to 25,371 units, so every member contributes. The stage changes no gate, scalar, operator, entrance or cleanup: +only 22 `helper_final` entries (each new end frame a hyperplane of the old one, all equal to their group's W) and 139 gate +frames (each a hyperplane of the old frame). These prices are search-time evidence (`construction/STAGE-PRICES.json`); +`verify.py` checks them against the literal words: the five joint prices sum exactly to the literal stage-1 price +−46,150,994, and one control per group keeps a single helper lowered on top of the group's partner frames, which is a valid +word but fails the joint claim (margins −53,141 for V45 and −58,943 for A–D against the joint +22,972 … +42,541). + +### Stage 2: how the lowered partners make five more extractions profitable + +On PR2942's words no rank-8 paired extraction clears break-even (best −29,645 at normals 486/504; normals 7 and 42 at +−68,935 and −86,879). Stage 1 moves the U12 partners of normal 45 into V45 ⊂ E_7 ∩ E_42 and the group partners into the +W's, so they become cheap or free partners for new rank-8 directions: on the stage-1 word the exact composition pricing +gives normal 7 +30,758 (k = 2, pivots 363, 395), normal 42 +26,153 (k = 3; realized +36,145), and normals 25 and 52 ++20,766 each (25 reuses pivot 363 and 52 pivot 395). The shipped composition is normal 42 three times, then normal 7 twice, each step a +PR2908/PR2917 paired extraction (input gates at frame zero after the prelude, output gates at E_n appended to restore, +compensation C·S, one more private zero buffer) with PR2908's exact two-sided certificate: + +| step | normal | pivot | inputs / outputs | frame changes | price | margin vs break-even | +|---:|---:|---:|---|---:|---:|---:| +| 1 | 42 | 226 | 20 / 6 | 0 | −2,101,683 | +10,383 | +| 2 | 42 | 228 | 16 / 7 | 1 (its first output gate drops from E_42 into group A's W) | −2,106,679 | +15,379 | +| 3 | 42 | 230 | 54 / 15 | 0 | −2,101,683 | +10,383 | +| 4 | 7 | 363 | 28 / 6 | 0 | −2,106,679 | +15,379 | +| 5 | 7 | 395 | 21 / 7 | 0 | −2,106,679 | +15,379 | + +After stage 2, normals 7, 42 and 52 have pairing rank 0 and normal 25's best is −34,529: the lever is exhausted for these +normals on the final word. + +### Stage 3: PR2957's rewrites, composed exactly + +Jeremy Kothe's fourteen declared rewrites (R-retime ×4, A3779-cut-start-read, PM-carrier-lender-entry ×2, +B-carrier-retime ×2, A-commuting-swap ×5) all apply to the stage-2 word with exact preimages after re-addressing A indices +by +261 versus PR2917 (our 122-gate and 139-gate input blocks; the A84 insertion lands after both); stage 1's B and +restore frame refits touch none of their preimages. `data/REWRITES-2957.json` is that re-addressed list (each entry keeps +its credit), applied by PR2957's own pure applier, vendored byte-identical (`vendor/declared_rewrites.py`, called with +`check_declared=False` because its declared profile is PR2917's). The certified delta is −52,350 = the sum of the singles, +exactly as on PR2917's and PR2942's words: no interaction with stages 1 and 2. PR2966 and PR2969 composed the same +fourteen rewrites with PR2942's words; here they are composed with the stage-2 word. + +### The fresh 9 → 7 route is an exact negative + +A 7-dimensional V ⊂ F₂⁹ lies in exactly three hyperplanes E_n1, E_n2, E_n1⊕n2 (its annihilator is {0, n1, n2, n1⊕n2}), and +the admissible pairing at V restricts the pairing at each of them, so a fresh helper can pair at V only if all three +normals pair. Over all 43,435 rank-7 subspaces: on PR2942's words (and on the stage-1 word) no pairing triple closes under +xor, so no fresh rank-7 extraction exists; on PR2917's words the single live V is V45 itself, with prank 4, which is +exactly normal 45's structure (realized here as PR2942 plus the V45 group: −8,378,128 − 8,388,172 = −16,766,300, the 9 → 7 +identity's prediction). On the PR2894 parent the census reproduces RossRichardson's PR2918 obstruction exactly +(at E7 = ⟨256, 128, 66, 36, 22, 8, 1⟩: R = {105, 307, 309, 314, 369, 371, 373, 378, 408, 572, 573}, |H| = 226, +dimA = dimB = 0). Rank-7 ends are therefore reachable only by lowering already restored helpers, which is stage 1. + +## Packing the changed inventory + +The fixed-capacity fractional relaxation of {4:26, 5:2, 6:16, 7:52, 8:99, 9:213} with local profile {1:2445, 2:706, 3:232, +4:108, 5:18, 8:8} has a 10-pattern optimal basis over all 2,551 patterns: per replica [8]×672, [7,9]×1757/4, +[7,8,8,9]×115/4, [8,8]×35/4, [6,8,9,9]×144, [4,9,9,9]×234, [9⁵]×1341/20, [9,9,9]×93/4, [5,9,9,9]×18 and []×7619/20; +cap ∈ [0.001729035764875516181444, 0.0017290357648755161814441]. The basis is fractional at T74, and the cap-level integer +mixes are not schedulable on the chronology: over calls 45..332 of the T37 chronology that PR2917's T74 order interleaves +twice, the width-7 roles (52 × 288 = 14,976) need distinct cap-16 bins in those mixes but only 13,440 cap-16 bins are open +(an interval Hall condition), so at least 1,536 width-7 roles must sit in cap-32 bins. A moment-preserving swap on a +degenerate face of the optimum, [7,8,8,9]@32 + [7,9]@16 → [8,8]@16 + [7,7,9,9]@32, applied 1,063 times to the T37 +all-pattern integer mix, satisfies that condition at no moment cost (building on themilkman216's observation about the T +at which these caps become integral and on PR2930's flow fill). PR2857's chronological flow model (CP-SAT, one worker, seed +1, optimal in 153 s; `construction/allocation/`) realizes the mix on the T37 chronology, and PR2917's exact interleaving +doubles it onto its T74 order. The literal root is **1.782e-9 below the cap** (integrality only); `check_cap.py` records +the exact gap. No optimality of the literal fill among integral allocations is claimed. + +Provenance (not entry points): `construction/STAGE-PRICES.json` holds the search-time prices quoted above; +`construction/search/` the census and realization scripts as executed (they import the round's certified frame-solver +harness, which is not shipped); `construction/records/` the derivation of `data/` from the realized words (per-step frame +changes, re-addressed rewrites); `construction/allocation/` the flow model run and the face-move mix. Scratch paths are +replaced by placeholders. + +## Verification + +**Registered, bounded** (`run_registered.py`, standard library, about one minute): +- complete package pins; +- `verify.py`: `producer.py` rebuilds both WORD files and every intermediate stage word from PARENT (PR2942's words, + byte-identical) and the declared records; stage 1: every lowered end frame is a hyperplane of the old one and equals its + group's W, every gate touching a lowered helper lies in W (326 gates), no gate or scalar changes, the cleanup is + unchanged; stage 2: PR2908/PR2917's unchanged `structure.py` checks the seven two-sided identities over the exact free + operator algebra at every step and for both providers; stage 3: PR2957's vendored applier with report and cleanup + re-derived and compared; PR2833's unchanged auditor replays every stage word and both final words forward and dual over + all 632 inputs (`PASS_INDEPENDENT_EXACT_BORROWING_WORD`, 91 restored endpoints and buffers at the end); `frame_report` + equals each word's report; **86 semantic controls** are rejected (stage 1, per provider: one helper of each group lowered + alone (fails the joint claim, priced below break-even), a wrong rank-7 subspace, an omitted gate frame edit, an omitted + partner frame edit, a stale report, a widened end frame; stage 2, per step and provider: drop an input gate and flip an + output coefficient (rejected by the auditor and by the certificate), the output change on a wrong hyperplane, a stale + cleanup, a stale compensation, and the omitted frame change of step 2; stage 3, per provider: a rewrite's deletion + removed, its insertion dropped, a transported coefficient flipped, a stale preimage (rejected by the applier), unshifted + warp positions, a stale cleanup, an unresolved swap frame); the overlay producer `tools/wordedit.py` round-trips + PARENT → WORD; +- `check_allocation.py`: the vendored PR2839 owner engine on the new allocation (271,728 roles, six width classes, windows, + same-call families, capacities, complete profile, physical 66,813) with five rejection controls, and PR2917's exact dyadic + moment auditor with its authenticated baseline re-pinned to the PR2969 headline (strict gain); +- `check_cap.py`: Fractions-only cap certificates of the parent and of every stage (each stage raises the cap), the literal + profile's completeness and its exact gap to the final cap, four controls, and exact gains over PR2969, PR2966, PR2957 + and PR2942; +- binding of the stored overlay, native, admission and release receipts in `evidence/` to the exact words, allocation and claim. + +**Complete replay** (`reproduce.py`): exact Git exports of PR2908 (51309592), PR2917 (224bd5e5), PR2942 (a027b0f6), PR2957 +(b74b25f3), PR2966 (e62d3eb9) and PR2969 (e2ca469b), and through them PR2894 (18d03c44) and PR2833 (e9307b48); fresh retained +bootstrap; PR2857's four-kernel stage, PR2894's preload stage, PR2908's paired stage and PR2917's extension stage, giving +PR2917's derived source (manifest 98d57c82, 632 files); then `tools/build_overlay.py` appends the stage +`rank7-joint-endframes`: the exact edit spec PR2917 word → this word (`tools/wordedit.py`, cleanup re-derived) is replayed +by the source's own `rebuild_borrow.py`, whose patched block now accepts inherited endpoints lowered to a subspace and warps +whose B positions move (both are new here), so every previous state stays in the audit chain (manifest 751b4636, 637 +files); closed adapters for 91 buffers whose admission control count is derived from the providers' width classes (139 +for six classes instead of PR2917's pinned 119 for five), with the PR2917, PR2966 and PR2969 headlines as pinned +comparators; fresh five-stage native chains for both providers; complete admission (owners, parent lift, rebind, +discovery, block norm, physical/prefix invoice, independent outer checks, and the release, which reruns the admitted +source's own verify.py and its 17-stage rebuild chain for both providers, ending with `rank7-joint-endframes`). + +The recorded run (`evidence/`) is a single invocation of this package's `reproduce.py --jobs 2` on macOS arm64, CPython +3.12.13 (numpy 2.4.5, scipy 1.16.1, sympy 1.14.0, mpmath 1.3.0, gmpy2 2.3.2, psutil 7.2.1): fresh retained bootstrap 311 s, +source stages including the overlay 3 s, fresh native chains for both providers 32 s, complete admission 287 s (release 221 +s), 635 s wall, ending `PASS_RANK7_JOINT_ENDFRAMES_COMPLETE_REPLAY`. The native receipt's "reused retained" fields refer to +the retained cache that the same run had just bootstrapped (`evidence/FULL-REPLAY-RESULT.json`: `fresh_retained_bootstrap: +true`). Hash-bound receipts are stored verbatim (they contain the run's absolute paths); logs under `evidence/logs/` have +paths replaced by placeholders. The run used a frozen copy of the package that is byte-identical to this one on every file +the replay executes or binds; only documentation was refined afterwards. + +```sh +# exact predecessor commits must be present locally (no network access during the replay) +git fetch https://github.com/CrocSwap/integer-mult-bounds.git \ + e2ca469b08385d3d5e29a918d66dbefaf889e9f3 e62d3eb9005117d82a9babcfa937ecc53237c490 \ + b74b25f3ccc84c16e1a801d73b2f47e5ea764c78 a027b0f6fdb0ab2b42ba10fc31b53960166bf2bf \ + 224bd5e56041c40078ff6b5fa7393733a215de5c 51309592971e3b5be935599eed2a95404dc7781e \ + 18d03c447886895ef9abf888398178e0428533ca e9307b48d7d1b690939935ecef0f8e524e6d92f4 +python3.12 scripts/research_package.py --package research/rank7-joint-endframes +OPENBLAS_NUM_THREADS=1 OMP_NUM_THREADS=1 \ + python3.12 -B research/rank7-joint-endframes/reproduce.py --repo . --work /tmp/rank7-complete --jobs 2 +``` + +The complete replay needs Python 3.12 with numpy, scipy, sympy, mpmath, gmpy2 and psutil (versions of the recorded run in +`evidence/ENVIRONMENT.json`). `--retained DIR` reuses an authenticated retained cache instead of the fresh bootstrap. +For the local checks alone: `python3.12 -B research/rank7-joint-endframes/verify.py --work /tmp/rank7-local`. + +## Scope + +Conditional finite supplier and modern outer certificate, exactly as inherited by PR2917/PR2942; all inherited all-size, +compiler, hosting, precision and analytic hypotheses remain. No selected-frontier change, no unconditional multiplication +theorem and no independent human review is claimed. Stage 1 alone is a fixed-word change of helper terminal subspaces and +monotone frames, the class whose relaxation Gareth Davidson's #1995/#2013 bound on the selected k8 word; here it is applied +to restored paired-extraction helpers of a different word and composed with a changed scalar word (stages 2 and 3), and +the whole is admitted with its changed inventory, buffers and cleanup contract. Lowering helper ends to rank seven is not +new as such (`research/complex-rank7-end-pair`, `research/k8-rank7-composition` and the PR1090/PR1104 lineage do it on +other words); what is new here is the joint, shared-subspace lowering of restored paired-extraction helpers and its +effect on further extractions. The search and optimality statements are relative to the stated cost model and census +(lower-bound candidates for one-dimension lowerings; all 43,435 rank-7 subspaces for fresh extractions; the exact +composition pricing per normal), not impossibility results beyond it. No optimality of the literal fill among integral +allocations is claimed. + +## Open next questions + +Checked after packaging on the final word (local exact runs with the certified frame solver and #2833's auditor on both +providers; not part of this package's gates): + +- **The lowering/extraction iteration is at a fixed point.** A one-dimension lowering census over all 91 restored endpoints + (the five new pivots and every changed partner included) leaves slack only at 586 and 588, with different target + subspaces at -3,345 units each; no endpoint has two dimensions of slack. Normals 7, 42, 45 and 52 now have pairing rank 0; + the best rank-8 block at 25, 76, 82, 97, 127, 486 or 504 is -29,645 units against break-even; no rank-7 subspace has all + three normals paired. +- **Other stage-2 orders tie at best.** On the stage-1 word, the orders 42 then 7, 7 then 42, and 42 then 25 then 52 each + realize five extractions at +66,903; orders that start with normal 25 give +61,907 or +46,919. +- **Earlier levers re-checked on this word.** No hidden compensation quartet narrows (the 502-517 family is certified + infeasible at #2917's restore outputs and at the new normal-7 output `96 -= 4*395`); entering helpers can enter v but + not u or the pivot (best direction 2,137 units short); renaming the output carriers bounds at 16,196 units, but every + pivot's output support is unique and every transfer placement is infeasible or non-negative. A census of #2957's rewrite + classes (retimes, commuting moves, cut-start reads, restore-to-B and cross-cut moves, read merges and splits) on the new + input block, the new output gates, the stage-1 refits and every gate touching a lowered helper prices 5,893 candidates + per provider with no negative delta. + +Still open: + +1. **Re-pairing the B phase** around the normal-7 pivots (363 with 73, 395 with 5) so the output map can use free carriers. +2. **Input changes placed later in A** instead of right after the prelude (identities as in #2908, new compensation). +3. **Integral packing at the cap.** The cap basis is fractional at T74 (denominators 4 and 20); a direct T74 solve of the + 1.552e-9 mix ended UNKNOWN at 900 s twice, so a T at which the basic counts are integral (keeping the interval Hall + condition for width-7 roles) may close part of the remaining 1.8e-9. + +Details are in `TASK.json`. + +## Credit + +Jeremy Diviney (PR #2908) for the paired input/output extraction method, its compensation rule and `structure.py` +(vendored unchanged); Mason Hale (PR #2917) for the words under PR2942, the producer model stage 2 follows, the T74 +chronology, owner/moment checks, extension stage and adapter derivation; **Jeremy Kothe (PR #2957/#2948/#2966) for the +fourteen declared rewrites of stage 3 and their applier (`vendor/declared_rewrites.py`, vendored unchanged), composed here +exactly, as PR2966 did with our PR2942 words**, and for the supplier, frame accounting and inverse cleanup +(`vendor/preload_move.py`, PR #2894/#2833); Dugongue (PR #2969) for the PR2942 + PR2957 composition at T370 that is this +package's comparator and moment baseline, and for the PR2863/PR2839 owner-engine lineage; RossRichardson (PR #2918) for the +rank-seven isolation boundary our census reproduces; Yiyang Lu (PR #2857/#2848) for the flow model and realization used to +build the allocation; Tekalign for the independent owner checker; icekylinx for the exact auditor +(`vendor/audit_local.py`); themilkman216 for the cap/T observation the allocation builds on. See `CREDITS.md` and +`NOTICE`. New work by Marius-Paul Dumitrean, prepared with substantial AI assistance (Anthropic Claude, via Claude Code). +Apache-2.0. diff --git a/research/rank7-chronological-face/sources/allocation/DISPATCH.json b/research/rank7-chronological-face/sources/allocation/DISPATCH.json new file mode 100644 index 0000000000..9544fee4e6 --- /dev/null +++ b/research/rank7-chronological-face/sources/allocation/DISPATCH.json @@ -0,0 +1 @@ +[[0,0,"extra"],[0,37,"extra"],[0,1,"extra"],[0,38,"extra"],[0,2,"extra"],[0,39,"extra"],[0,3,"extra"],[0,40,"extra"],[0,4,"extra"],[0,41,"extra"],[1,0,"extra"],[1,37,"extra"],[0,5,"extra"],[0,42,"extra"],[1,1,"extra"],[1,38,"extra"],[0,6,"extra"],[0,43,"extra"],[1,2,"extra"],[1,39,"extra"],[0,7,"extra"],[0,44,"extra"],[1,3,"extra"],[1,40,"extra"],[0,8,"extra"],[0,45,"extra"],[1,4,"extra"],[1,41,"extra"],[0,9,"extra"],[0,46,"extra"],[2,0,"extra"],[2,37,"extra"],[1,5,"extra"],[1,42,"extra"],[0,10,"extra"],[0,47,"extra"],[2,1,"extra"],[2,38,"extra"],[1,6,"extra"],[1,43,"extra"],[0,11,"extra"],[0,48,"extra"],[2,2,"extra"],[2,39,"extra"],[1,7,"extra"],[1,44,"extra"],[0,12,"extra"],[0,49,"extra"],[2,3,"extra"],[2,40,"extra"],[1,8,"extra"],[1,45,"extra"],[0,13,"extra"],[0,50,"extra"],[2,4,"extra"],[2,41,"extra"],[1,9,"extra"],[1,46,"extra"],[3,0,"extra"],[3,37,"extra"],[0,14,"extra"],[0,51,"extra"],[2,5,"extra"],[2,42,"extra"],[1,10,"extra"],[1,47,"extra"],[3,1,"extra"],[3,38,"extra"],[0,15,"extra"],[0,52,"extra"],[2,6,"extra"],[2,43,"extra"],[1,11,"extra"],[1,48,"extra"],[3,2,"extra"],[3,39,"extra"],[0,16,"extra"],[0,53,"extra"],[2,7,"extra"],[2,44,"extra"],[1,12,"extra"],[1,49,"extra"],[3,3,"extra"],[3,40,"extra"],[0,17,"extra"],[0,54,"extra"],[2,8,"extra"],[2,45,"extra"],[1,13,"extra"],[1,50,"extra"],[3,4,"extra"],[3,41,"extra"],[0,18,"extra"],[0,55,"extra"],[2,9,"extra"],[2,46,"extra"],[4,0,"extra"],[4,37,"extra"],[1,14,"extra"],[1,51,"extra"],[3,5,"extra"],[3,42,"extra"],[0,19,"extra"],[0,56,"extra"],[2,10,"extra"],[2,47,"extra"],[4,1,"extra"],[4,38,"extra"],[1,15,"extra"],[1,52,"extra"],[3,6,"extra"],[3,43,"extra"],[0,20,"extra"],[0,57,"extra"],[2,11,"extra"],[2,48,"extra"],[4,2,"extra"],[4,39,"extra"],[1,16,"extra"],[1,53,"extra"],[3,7,"extra"],[3,44,"extra"],[0,21,"extra"],[0,58,"extra"],[2,12,"extra"],[2,49,"extra"],[4,3,"extra"],[4,40,"extra"],[1,17,"extra"],[1,54,"extra"],[3,8,"extra"],[3,45,"extra"],[0,22,"extra"],[0,59,"extra"],[2,13,"extra"],[2,50,"extra"],[4,4,"extra"],[4,41,"extra"],[1,18,"extra"],[1,55,"extra"],[3,9,"extra"],[3,46,"extra"],[0,23,"extra"],[0,60,"extra"],[5,0,"extra"],[5,37,"extra"],[2,14,"extra"],[2,51,"extra"],[4,5,"extra"],[4,42,"extra"],[1,19,"extra"],[1,56,"extra"],[3,10,"extra"],[3,47,"extra"],[0,24,"extra"],[0,61,"extra"],[5,1,"extra"],[5,38,"extra"],[2,15,"extra"],[2,52,"extra"],[4,6,"extra"],[4,43,"extra"],[1,20,"extra"],[1,57,"extra"],[3,11,"extra"],[3,48,"extra"],[0,25,"extra"],[0,62,"extra"],[5,2,"extra"],[5,39,"extra"],[2,16,"extra"],[2,53,"extra"],[4,7,"extra"],[4,44,"extra"],[1,21,"extra"],[1,58,"extra"],[3,12,"extra"],[3,49,"extra"],[0,26,"extra"],[0,63,"extra"],[5,3,"extra"],[5,40,"extra"],[2,17,"extra"],[2,54,"extra"],[4,8,"extra"],[4,45,"extra"],[1,22,"extra"],[1,59,"extra"],[3,13,"extra"],[3,50,"extra"],[0,27,"extra"],[0,64,"extra"],[5,4,"extra"],[5,41,"extra"],[2,18,"extra"],[2,55,"extra"],[4,9,"extra"],[4,46,"extra"],[1,23,"extra"],[1,60,"extra"],[6,0,"extra"],[6,37,"extra"],[3,14,"extra"],[3,51,"extra"],[0,28,"extra"],[0,65,"extra"],[5,5,"extra"],[5,42,"extra"],[2,19,"extra"],[2,56,"extra"],[4,10,"extra"],[4,47,"extra"],[1,24,"extra"],[1,61,"extra"],[6,1,"extra"],[6,38,"extra"],[3,15,"extra"],[3,52,"extra"],[0,29,"extra"],[0,66,"extra"],[5,6,"extra"],[5,43,"extra"],[2,20,"extra"],[2,57,"extra"],[4,11,"extra"],[4,48,"extra"],[1,25,"extra"],[1,62,"extra"],[6,2,"extra"],[6,39,"extra"],[3,16,"extra"],[3,53,"extra"],[0,30,"extra"],[0,67,"extra"],[5,7,"extra"],[5,44,"extra"],[2,21,"extra"],[2,58,"extra"],[4,12,"extra"],[4,49,"extra"],[1,26,"extra"],[1,63,"extra"],[6,3,"extra"],[6,40,"extra"],[3,17,"extra"],[3,54,"extra"],[0,31,"extra"],[0,68,"extra"],[5,8,"extra"],[5,45,"extra"],[2,22,"extra"],[2,59,"extra"],[4,13,"extra"],[4,50,"extra"],[1,27,"extra"],[1,64,"extra"],[6,4,"extra"],[6,41,"extra"],[3,18,"extra"],[3,55,"extra"],[0,32,"extra"],[0,69,"extra"],[5,9,"extra"],[5,46,"extra"],[2,23,"extra"],[2,60,"extra"],[7,0,"extra"],[7,37,"extra"],[4,14,"extra"],[4,51,"extra"],[1,28,"extra"],[1,65,"extra"],[6,5,"extra"],[6,42,"extra"],[3,19,"extra"],[3,56,"extra"],[0,33,"extra"],[0,70,"extra"],[5,10,"extra"],[5,47,"extra"],[2,24,"extra"],[2,61,"extra"],[7,1,"extra"],[7,38,"extra"],[4,15,"extra"],[4,52,"extra"],[1,29,"extra"],[1,66,"extra"],[6,6,"extra"],[6,43,"extra"],[3,20,"extra"],[3,57,"extra"],[0,34,"extra"],[0,71,"extra"],[5,11,"extra"],[5,48,"extra"],[2,25,"extra"],[2,62,"extra"],[7,2,"extra"],[7,39,"extra"],[4,16,"extra"],[4,53,"extra"],[1,30,"extra"],[1,67,"extra"],[6,7,"extra"],[6,44,"extra"],[3,21,"extra"],[3,58,"extra"],[0,35,"extra"],[0,72,"extra"],[5,12,"extra"],[5,49,"extra"],[2,26,"extra"],[2,63,"extra"],[7,3,"extra"],[7,40,"extra"],[4,17,"extra"],[4,54,"extra"],[1,31,"extra"],[1,68,"extra"],[6,8,"extra"],[6,45,"extra"],[3,22,"extra"],[3,59,"extra"],[0,36,"extra"],[0,73,"extra"],[5,13,"extra"],[5,50,"extra"],[2,27,"extra"],[2,64,"extra"],[7,4,"extra"],[7,41,"extra"],[4,18,"extra"],[4,55,"extra"],[1,32,"extra"],[1,69,"extra"],[6,9,"extra"],[6,46,"extra"],[3,23,"extra"],[3,60,"extra"],[8,0,"extra"],[8,37,"extra"],[5,14,"extra"],[5,51,"extra"],[2,28,"extra"],[2,65,"extra"],[7,5,"extra"],[7,42,"extra"],[4,19,"extra"],[4,56,"extra"],[1,33,"extra"],[1,70,"extra"],[6,10,"extra"],[6,47,"extra"],[3,24,"extra"],[3,61,"extra"],[8,1,"extra"],[8,38,"extra"],[5,15,"extra"],[5,52,"extra"],[2,29,"extra"],[2,66,"extra"],[7,6,"extra"],[7,43,"extra"],[4,20,"extra"],[4,57,"extra"],[1,34,"extra"],[1,71,"extra"],[6,11,"extra"],[6,48,"extra"],[3,25,"extra"],[3,62,"extra"],[8,2,"extra"],[8,39,"extra"],[5,16,"extra"],[5,53,"extra"],[2,30,"extra"],[2,67,"extra"],[7,7,"extra"],[7,44,"extra"],[4,21,"extra"],[4,58,"extra"],[1,35,"extra"],[1,72,"extra"],[6,12,"extra"],[6,49,"extra"],[3,26,"extra"],[3,63,"extra"],[8,3,"extra"],[8,40,"extra"],[5,17,"extra"],[5,54,"extra"],[2,31,"extra"],[2,68,"extra"],[7,8,"extra"],[7,45,"extra"],[4,22,"extra"],[4,59,"extra"],[1,36,"extra"],[1,73,"extra"],[6,13,"extra"],[6,50,"extra"],[3,27,"extra"],[3,64,"extra"],[8,4,"extra"],[8,41,"extra"],[5,18,"extra"],[5,55,"extra"],[2,32,"extra"],[2,69,"extra"],[7,9,"extra"],[7,46,"extra"],[4,23,"extra"],[4,60,"extra"],[6,14,"extra"],[6,51,"extra"],[3,28,"gauge44"],[3,65,"gauge44"],[8,5,"gauge44"],[8,42,"gauge44"],[5,19,"gauge44"],[5,56,"gauge44"],[2,33,"gauge44"],[2,70,"gauge44"],[7,10,"gauge44"],[7,47,"gauge44"],[4,24,"gauge44"],[4,61,"gauge44"],[6,15,"gauge44"],[6,52,"gauge44"],[3,29,"gauge44"],[3,66,"gauge44"],[8,6,"gauge44"],[8,43,"gauge44"],[5,20,"gauge44"],[5,57,"gauge44"],[2,34,"gauge44"],[2,71,"gauge44"],[7,11,"gauge44"],[7,48,"gauge44"],[4,25,"gauge44"],[4,62,"gauge44"],[6,16,"gauge44"],[6,53,"gauge44"],[3,30,"gauge44"],[3,67,"gauge44"],[8,7,"gauge44"],[8,44,"gauge44"],[5,21,"gauge44"],[5,58,"gauge44"],[2,35,"gauge44"],[2,72,"gauge44"],[7,12,"gauge44"],[7,49,"gauge44"],[4,26,"gauge44"],[4,63,"gauge44"],[6,17,"gauge44"],[6,54,"gauge44"],[3,31,"gauge44"],[3,68,"gauge44"],[8,8,"gauge44"],[8,45,"gauge44"],[5,22,"gauge44"],[5,59,"gauge44"],[2,36,"gauge44"],[2,73,"gauge44"],[7,13,"gauge44"],[7,50,"gauge44"],[4,27,"gauge44"],[4,64,"gauge44"],[6,18,"gauge44"],[6,55,"gauge44"],[3,32,"gauge44"],[3,69,"gauge44"],[8,9,"gauge44"],[8,46,"gauge44"],[5,23,"gauge44"],[5,60,"gauge44"],[7,14,"gauge44"],[7,51,"gauge44"],[4,28,"gauge44"],[4,65,"gauge44"],[6,19,"gauge44"],[6,56,"gauge44"],[3,33,"gauge44"],[3,70,"gauge44"],[8,10,"gauge44"],[8,47,"gauge44"],[5,24,"gauge44"],[5,61,"gauge44"],[7,15,"gauge44"],[7,52,"gauge44"],[4,29,"gauge44"],[4,66,"gauge44"],[6,20,"gauge44"],[6,57,"gauge44"],[3,34,"gauge44"],[3,71,"gauge44"],[8,11,"gauge44"],[8,48,"gauge44"],[5,25,"gauge44"],[5,62,"gauge44"],[7,16,"gauge44"],[7,53,"gauge44"],[4,30,"gauge44"],[4,67,"gauge44"],[6,21,"gauge44"],[6,58,"gauge44"],[3,35,"gauge44"],[3,72,"gauge44"],[8,12,"gauge44"],[8,49,"gauge44"],[5,26,"gauge44"],[5,63,"gauge44"],[7,17,"gauge44"],[7,54,"gauge44"],[4,31,"gauge44"],[4,68,"gauge44"],[6,22,"gauge44"],[6,59,"gauge44"],[3,36,"gauge44"],[3,73,"gauge44"],[8,13,"gauge44"],[8,50,"gauge44"],[5,27,"gauge44"],[5,64,"gauge44"],[7,18,"gauge44"],[7,55,"gauge44"],[4,32,"gauge44"],[4,69,"gauge44"],[6,23,"gauge44"],[6,60,"gauge44"],[8,14,"gauge44"],[8,51,"gauge44"],[5,28,"gauge44"],[5,65,"gauge44"],[7,19,"gauge44"],[7,56,"gauge44"],[4,33,"gauge44"],[4,70,"gauge44"],[6,24,"gauge44"],[6,61,"gauge44"],[8,15,"gauge44"],[8,52,"gauge44"],[5,29,"gauge44"],[5,66,"gauge44"],[7,20,"gauge44"],[7,57,"gauge44"],[4,34,"gauge44"],[4,71,"gauge44"],[6,25,"gauge44"],[6,62,"gauge44"],[8,16,"gauge44"],[8,53,"gauge44"],[5,30,"gauge44"],[5,67,"gauge44"],[7,21,"gauge44"],[7,58,"gauge44"],[4,35,"gauge44"],[4,72,"gauge44"],[6,26,"gauge44"],[6,63,"gauge44"],[8,17,"gauge44"],[8,54,"gauge44"],[5,31,"gauge44"],[5,68,"gauge44"],[7,22,"gauge44"],[7,59,"gauge44"],[4,36,"gauge44"],[4,73,"gauge44"],[6,27,"gauge44"],[6,64,"gauge44"],[8,18,"gauge44"],[8,55,"gauge44"],[5,32,"gauge44"],[5,69,"gauge44"],[7,23,"gauge44"],[7,60,"gauge44"],[6,28,"gauge44"],[6,65,"gauge44"],[8,19,"gauge44"],[8,56,"gauge44"],[5,33,"gauge44"],[5,70,"gauge44"],[7,24,"gauge44"],[7,61,"gauge44"],[6,29,"gauge44"],[6,66,"gauge44"],[8,20,"gauge44"],[8,57,"gauge44"],[5,34,"gauge44"],[5,71,"gauge44"],[7,25,"gauge44"],[7,62,"gauge44"],[6,30,"gauge44"],[6,67,"gauge44"],[8,21,"gauge44"],[8,58,"gauge44"],[5,35,"gauge44"],[5,72,"gauge44"],[7,26,"gauge44"],[7,63,"gauge44"],[6,31,"gauge44"],[6,68,"gauge44"],[8,22,"gauge44"],[8,59,"gauge44"],[5,36,"gauge44"],[5,73,"gauge44"],[7,27,"gauge44"],[7,64,"gauge44"],[6,32,"gauge44"],[6,69,"gauge44"],[8,23,"gauge44"],[8,60,"gauge44"],[7,28,"gauge44"],[7,65,"gauge44"],[6,33,"gauge44"],[6,70,"gauge44"],[8,24,"gauge44"],[8,61,"gauge44"],[7,29,"gauge44"],[7,66,"gauge44"],[6,34,"gauge44"],[6,71,"gauge44"],[8,25,"gauge44"],[8,62,"gauge44"],[7,30,"gauge44"],[7,67,"gauge44"],[6,35,"gauge44"],[6,72,"gauge44"],[8,26,"gauge44"],[8,63,"gauge44"],[7,31,"gauge44"],[7,68,"gauge44"],[6,36,"gauge44"],[6,73,"gauge44"],[8,27,"gauge44"],[8,64,"gauge44"],[7,32,"gauge44"],[7,69,"gauge44"],[8,28,"gauge44"],[8,65,"gauge44"],[7,33,"gauge44"],[7,70,"gauge44"],[8,29,"gauge44"],[8,66,"gauge44"],[7,34,"gauge44"],[7,71,"gauge44"],[8,30,"gauge44"],[8,67,"gauge44"],[7,35,"gauge44"],[7,72,"gauge44"],[8,31,"gauge44"],[8,68,"gauge44"],[7,36,"gauge44"],[7,73,"gauge44"],[8,32,"gauge44"],[8,69,"gauge44"],[8,33,"gauge44"],[8,70,"gauge44"],[8,34,"gauge44"],[8,71,"gauge44"],[8,35,"gauge44"],[8,72,"gauge44"],[8,36,"gauge44"],[8,73,"gauge44"]] \ No newline at end of file diff --git a/research/rank7-chronological-face/sources/allocation/FILL.json.gz b/research/rank7-chronological-face/sources/allocation/FILL.json.gz new file mode 100644 index 0000000000..8d4fd644d6 Binary files /dev/null and b/research/rank7-chronological-face/sources/allocation/FILL.json.gz differ diff --git a/research/rank7-chronological-face/sources/allocation/ORDER.json b/research/rank7-chronological-face/sources/allocation/ORDER.json new file mode 100644 index 0000000000..7409c4df10 --- /dev/null +++ b/research/rank7-chronological-face/sources/allocation/ORDER.json @@ -0,0 +1 @@ +[[0,0],[0,37],[0,1],[0,38],[0,2],[0,39],[0,3],[0,40],[0,4],[0,41],[1,0],[1,37],[0,5],[0,42],[1,1],[1,38],[0,6],[0,43],[1,2],[1,39],[0,7],[0,44],[1,3],[1,40],[0,8],[0,45],[1,4],[1,41],[0,9],[0,46],[2,0],[2,37],[1,5],[1,42],[0,10],[0,47],[2,1],[2,38],[1,6],[1,43],[0,11],[0,48],[2,2],[2,39],[1,7],[1,44],[0,12],[0,49],[2,3],[2,40],[1,8],[1,45],[0,13],[0,50],[2,4],[2,41],[1,9],[1,46],[3,0],[3,37],[0,14],[0,51],[2,5],[2,42],[1,10],[1,47],[3,1],[3,38],[0,15],[0,52],[2,6],[2,43],[1,11],[1,48],[3,2],[3,39],[0,16],[0,53],[2,7],[2,44],[1,12],[1,49],[3,3],[3,40],[0,17],[0,54],[2,8],[2,45],[1,13],[1,50],[3,4],[3,41],[0,18],[0,55],[2,9],[2,46],[4,0],[4,37],[1,14],[1,51],[3,5],[3,42],[0,19],[0,56],[2,10],[2,47],[4,1],[4,38],[1,15],[1,52],[3,6],[3,43],[0,20],[0,57],[2,11],[2,48],[4,2],[4,39],[1,16],[1,53],[3,7],[3,44],[0,21],[0,58],[2,12],[2,49],[4,3],[4,40],[1,17],[1,54],[3,8],[3,45],[0,22],[0,59],[2,13],[2,50],[4,4],[4,41],[1,18],[1,55],[3,9],[3,46],[0,23],[0,60],[5,0],[5,37],[2,14],[2,51],[4,5],[4,42],[1,19],[1,56],[3,10],[3,47],[0,24],[0,61],[5,1],[5,38],[2,15],[2,52],[4,6],[4,43],[1,20],[1,57],[3,11],[3,48],[0,25],[0,62],[5,2],[5,39],[2,16],[2,53],[4,7],[4,44],[1,21],[1,58],[3,12],[3,49],[0,26],[0,63],[5,3],[5,40],[2,17],[2,54],[4,8],[4,45],[1,22],[1,59],[3,13],[3,50],[0,27],[0,64],[5,4],[5,41],[2,18],[2,55],[4,9],[4,46],[1,23],[1,60],[6,0],[6,37],[3,14],[3,51],[0,28],[0,65],[5,5],[5,42],[2,19],[2,56],[4,10],[4,47],[1,24],[1,61],[6,1],[6,38],[3,15],[3,52],[0,29],[0,66],[5,6],[5,43],[2,20],[2,57],[4,11],[4,48],[1,25],[1,62],[6,2],[6,39],[3,16],[3,53],[0,30],[0,67],[5,7],[5,44],[2,21],[2,58],[4,12],[4,49],[1,26],[1,63],[6,3],[6,40],[3,17],[3,54],[0,31],[0,68],[5,8],[5,45],[2,22],[2,59],[4,13],[4,50],[1,27],[1,64],[6,4],[6,41],[3,18],[3,55],[0,32],[0,69],[5,9],[5,46],[2,23],[2,60],[7,0],[7,37],[4,14],[4,51],[1,28],[1,65],[6,5],[6,42],[3,19],[3,56],[0,33],[0,70],[5,10],[5,47],[2,24],[2,61],[7,1],[7,38],[4,15],[4,52],[1,29],[1,66],[6,6],[6,43],[3,20],[3,57],[0,34],[0,71],[5,11],[5,48],[2,25],[2,62],[7,2],[7,39],[4,16],[4,53],[1,30],[1,67],[6,7],[6,44],[3,21],[3,58],[0,35],[0,72],[5,12],[5,49],[2,26],[2,63],[7,3],[7,40],[4,17],[4,54],[1,31],[1,68],[6,8],[6,45],[3,22],[3,59],[0,36],[0,73],[5,13],[5,50],[2,27],[2,64],[7,4],[7,41],[4,18],[4,55],[1,32],[1,69],[6,9],[6,46],[3,23],[3,60],[8,0],[8,37],[5,14],[5,51],[2,28],[2,65],[7,5],[7,42],[4,19],[4,56],[1,33],[1,70],[6,10],[6,47],[3,24],[3,61],[8,1],[8,38],[5,15],[5,52],[2,29],[2,66],[7,6],[7,43],[4,20],[4,57],[1,34],[1,71],[6,11],[6,48],[3,25],[3,62],[8,2],[8,39],[5,16],[5,53],[2,30],[2,67],[7,7],[7,44],[4,21],[4,58],[1,35],[1,72],[6,12],[6,49],[3,26],[3,63],[8,3],[8,40],[5,17],[5,54],[2,31],[2,68],[7,8],[7,45],[4,22],[4,59],[1,36],[1,73],[6,13],[6,50],[3,27],[3,64],[8,4],[8,41],[5,18],[5,55],[2,32],[2,69],[7,9],[7,46],[4,23],[4,60],[6,14],[6,51],[3,28],[3,65],[8,5],[8,42],[5,19],[5,56],[2,33],[2,70],[7,10],[7,47],[4,24],[4,61],[6,15],[6,52],[3,29],[3,66],[8,6],[8,43],[5,20],[5,57],[2,34],[2,71],[7,11],[7,48],[4,25],[4,62],[6,16],[6,53],[3,30],[3,67],[8,7],[8,44],[5,21],[5,58],[2,35],[2,72],[7,12],[7,49],[4,26],[4,63],[6,17],[6,54],[3,31],[3,68],[8,8],[8,45],[5,22],[5,59],[2,36],[2,73],[7,13],[7,50],[4,27],[4,64],[6,18],[6,55],[3,32],[3,69],[8,9],[8,46],[5,23],[5,60],[7,14],[7,51],[4,28],[4,65],[6,19],[6,56],[3,33],[3,70],[8,10],[8,47],[5,24],[5,61],[7,15],[7,52],[4,29],[4,66],[6,20],[6,57],[3,34],[3,71],[8,11],[8,48],[5,25],[5,62],[7,16],[7,53],[4,30],[4,67],[6,21],[6,58],[3,35],[3,72],[8,12],[8,49],[5,26],[5,63],[7,17],[7,54],[4,31],[4,68],[6,22],[6,59],[3,36],[3,73],[8,13],[8,50],[5,27],[5,64],[7,18],[7,55],[4,32],[4,69],[6,23],[6,60],[8,14],[8,51],[5,28],[5,65],[7,19],[7,56],[4,33],[4,70],[6,24],[6,61],[8,15],[8,52],[5,29],[5,66],[7,20],[7,57],[4,34],[4,71],[6,25],[6,62],[8,16],[8,53],[5,30],[5,67],[7,21],[7,58],[4,35],[4,72],[6,26],[6,63],[8,17],[8,54],[5,31],[5,68],[7,22],[7,59],[4,36],[4,73],[6,27],[6,64],[8,18],[8,55],[5,32],[5,69],[7,23],[7,60],[6,28],[6,65],[8,19],[8,56],[5,33],[5,70],[7,24],[7,61],[6,29],[6,66],[8,20],[8,57],[5,34],[5,71],[7,25],[7,62],[6,30],[6,67],[8,21],[8,58],[5,35],[5,72],[7,26],[7,63],[6,31],[6,68],[8,22],[8,59],[5,36],[5,73],[7,27],[7,64],[6,32],[6,69],[8,23],[8,60],[7,28],[7,65],[6,33],[6,70],[8,24],[8,61],[7,29],[7,66],[6,34],[6,71],[8,25],[8,62],[7,30],[7,67],[6,35],[6,72],[8,26],[8,63],[7,31],[7,68],[6,36],[6,73],[8,27],[8,64],[7,32],[7,69],[8,28],[8,65],[7,33],[7,70],[8,29],[8,66],[7,34],[7,71],[8,30],[8,67],[7,35],[7,72],[8,31],[8,68],[7,36],[7,73],[8,32],[8,69],[8,33],[8,70],[8,34],[8,71],[8,35],[8,72],[8,36],[8,73]] \ No newline at end of file diff --git a/research/rank7-chronological-face/sources/allocation/PROFILE.json b/research/rank7-chronological-face/sources/allocation/PROFILE.json new file mode 100644 index 0000000000..46a83eeda6 --- /dev/null +++ b/research/rank7-chronological-face/sources/allocation/PROFILE.json @@ -0,0 +1,9 @@ +{ + "1": 1645680, + "2": 470196, + "3": 159468, + "4": 71928, + "5": 13716, + "8": 5328, + "48": 28190 +} \ No newline at end of file diff --git a/research/rank7-chronological-face/sources/allocation/PROVIDERS.json b/research/rank7-chronological-face/sources/allocation/PROVIDERS.json new file mode 100644 index 0000000000..e1d99e12cf --- /dev/null +++ b/research/rank7-chronological-face/sources/allocation/PROVIDERS.json @@ -0,0 +1,842 @@ +{ + "extra": { + "actual_paid_profile": { + "1": 2445, + "2": 706, + "3": 232, + "4": 108, + "5": 18, + "8": 8 + }, + "widths": [ + 9, + 9, + 8, + 9, + 8, + 9, + 8, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 7, + 9, + 7, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 7, + 9, + 7, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 4, + 9, + 9, + 9, + 9, + 4, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 4, + 9, + 9, + 9, + 9, + 4, + 7, + 9, + 9, + 9, + 9, + 8, + 9, + 9, + 4, + 9, + 4, + 9, + 8, + 9, + 9, + 4, + 9, + 9, + 9, + 9, + 9, + 8, + 9, + 9, + 4, + 9, + 4, + 9, + 8, + 9, + 9, + 4, + 7, + 9, + 9, + 9, + 9, + 9, + 4, + 9, + 4, + 9, + 4, + 9, + 9, + 9, + 9, + 4, + 9, + 9, + 9, + 9, + 9, + 9, + 4, + 9, + 4, + 9, + 4, + 9, + 9, + 9, + 9, + 4, + 8, + 9, + 9, + 9, + 9, + 9, + 4, + 9, + 4, + 9, + 4, + 9, + 9, + 9, + 9, + 4, + 9, + 9, + 9, + 9, + 9, + 9, + 4, + 9, + 4, + 9, + 4, + 9, + 9, + 9, + 9, + 4, + 8, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 8, + 9, + 9, + 9, + 8, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 8, + 9, + 9, + 9, + 8, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 6, + 6, + 6, + 6, + 6, + 6, + 6, + 6, + 9, + 8, + 8, + 9, + 8, + 9, + 8, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 8, + 8, + 7, + 7, + 7, + 7, + 8, + 9, + 8, + 9, + 6, + 6, + 7, + 7, + 7, + 7, + 9, + 9, + 9, + 9, + 8, + 8, + 8, + 8, + 8, + 8, + 9, + 9, + 9, + 9, + 8, + 6, + 6, + 8, + 8, + 8, + 8, + 9, + 9, + 9, + 9, + 8, + 8, + 8, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 8, + 7, + 6, + 6, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 8, + 7, + 8, + 8, + 9, + 9, + 9, + 9, + 8, + 8, + 8, + 8, + 7, + 7, + 6, + 6, + 9, + 8, + 9, + 8, + 8, + 8, + 8, + 8, + 7, + 7, + 9, + 8, + 9, + 8, + 7, + 7, + 7, + 7, + 8, + 8, + 8, + 8, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 5, + 5, + 8, + 8, + 8, + 8 + ] + }, + "gauge44": { + "actual_paid_profile": { + "1": 2445, + "2": 706, + "3": 232, + "4": 108, + "5": 18, + "8": 8 + }, + "widths": [ + 9, + 9, + 8, + 9, + 8, + 9, + 8, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 7, + 9, + 7, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 7, + 9, + 7, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 4, + 9, + 9, + 9, + 9, + 4, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 4, + 9, + 9, + 9, + 9, + 4, + 7, + 9, + 9, + 9, + 9, + 8, + 9, + 9, + 4, + 9, + 4, + 9, + 8, + 9, + 9, + 4, + 9, + 9, + 9, + 9, + 9, + 8, + 9, + 9, + 4, + 9, + 4, + 9, + 8, + 9, + 9, + 4, + 7, + 9, + 9, + 9, + 9, + 9, + 4, + 9, + 4, + 9, + 4, + 9, + 9, + 9, + 9, + 4, + 9, + 9, + 9, + 9, + 9, + 9, + 4, + 9, + 4, + 9, + 4, + 9, + 9, + 9, + 9, + 4, + 8, + 9, + 9, + 9, + 9, + 9, + 4, + 9, + 4, + 9, + 4, + 9, + 9, + 9, + 9, + 4, + 9, + 9, + 9, + 9, + 9, + 9, + 4, + 9, + 4, + 9, + 4, + 9, + 9, + 9, + 9, + 4, + 8, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 8, + 9, + 9, + 9, + 8, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 8, + 9, + 9, + 9, + 8, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 6, + 6, + 6, + 6, + 6, + 6, + 6, + 6, + 9, + 8, + 8, + 9, + 8, + 9, + 8, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 8, + 8, + 7, + 7, + 7, + 7, + 8, + 9, + 8, + 9, + 6, + 6, + 7, + 7, + 7, + 7, + 9, + 9, + 9, + 9, + 8, + 8, + 8, + 8, + 8, + 8, + 9, + 9, + 9, + 9, + 8, + 6, + 6, + 8, + 8, + 8, + 8, + 9, + 9, + 9, + 9, + 8, + 8, + 8, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 8, + 7, + 6, + 6, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 8, + 7, + 8, + 8, + 9, + 9, + 9, + 9, + 8, + 8, + 8, + 8, + 7, + 7, + 6, + 6, + 9, + 8, + 9, + 8, + 8, + 8, + 8, + 8, + 7, + 7, + 9, + 8, + 9, + 8, + 7, + 7, + 7, + 7, + 8, + 8, + 8, + 8, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 5, + 5, + 8, + 8, + 8, + 8 + ] + } +} \ No newline at end of file diff --git a/research/rank7-chronological-face/sources/allocation/SEARCH.json b/research/rank7-chronological-face/sources/allocation/SEARCH.json new file mode 100644 index 0000000000..cf0a2e7ca4 --- /dev/null +++ b/research/rank7-chronological-face/sources/allocation/SEARCH.json @@ -0,0 +1,46 @@ +{ + "calls": 666, + "catalogue": null, + "chronology": "pr2917-t74", + "gap_to_relaxation_cap_float": 1.7822290026637266e-09, + "headline": "0.0017290339826465135177169999999999999999999998999999999999999999999999", + "idle_histogram": { + "1": 17310, + "3": 4956, + "48": 28190, + "5": 1728 + }, + "kappa_root_bracket": [ + "691613593058605407087/400000000000000000000000", + "2161292478308141897147/1250000000000000000000000" + ], + "kappa_root_lower_decimal": "0.0017290339826465135177175", + "lineage": "PR2917 (mason-hale) chronology/engine; PR2930/PR2942 fills; r14 lane A words; PR2857 flow model and realization; PR2839 owner engine; lane C r12 relax/root/fill tools; r13/r14 lane C1.", + "moment_auditor": "PASS_SEPARATE_EXACT_RATIONAL_FRONTIER_MOMENT", + "note": "L27R words; T37 fixed-target CP-SAT flow on an OPTIMAL-FACE integer mix of the relaxation (T37 all-pattern milp mix moved by 1063 cost-free face moves [7,8,8,9]@32+[7,9]@16 -> [8,8]@16+[7,7,9,9]@32 so that >= 1536 width-7 roles sit in cap-32 bins, the interval Hall condition of the chronology), seed 1, first flow 152.6 s, doubled onto PR2917 T74 order.", + "order_and_dispatch_unchanged_vs_PR2917": true, + "pattern_mix": null, + "physical": 66813, + "profile": { + "1": 1645680, + "2": 470196, + "3": 159468, + "4": 71928, + "48": 28190, + "5": 13716, + "8": 5328 + }, + "relaxation_cap_bracket": [ + "432258941218879045361/250000000000000000000000", + "17290357648755161814441/10000000000000000000000000" + ], + "replicas": 74, + "roles": 271728, + "seed": null, + "solver": "DOUBLED_FROM_T37_FILL S/r13/agents/C1-fill-flow/out/L27R/t37-faceB-s1", + "status": "C1_FLOW_ROUTE_LITERAL_FILL_L27R_V2", + "words_sha256": { + "base": "abaf67bfcb257528658c906b612f57025617592bd7889828f92b97a5f4f4300d", + "extra": "e0eaf64c4d5d324693d43889bce1b9e53e8da00402105c8c978fd102f208bed7" + } +} diff --git a/research/rank7-chronological-face/sources/allocation/vendor/PLAN.json.gz b/research/rank7-chronological-face/sources/allocation/vendor/PLAN.json.gz new file mode 100644 index 0000000000..7a1db55a4d Binary files /dev/null and b/research/rank7-chronological-face/sources/allocation/vendor/PLAN.json.gz differ diff --git a/research/rank7-chronological-face/sources/allocation/vendor/TEMPLATE.json.gz b/research/rank7-chronological-face/sources/allocation/vendor/TEMPLATE.json.gz new file mode 100644 index 0000000000..114808c32b Binary files /dev/null and b/research/rank7-chronological-face/sources/allocation/vendor/TEMPLATE.json.gz differ diff --git a/research/rank7-chronological-face/sources/allocation/vendor/independent_owners.py b/research/rank7-chronological-face/sources/allocation/vendor/independent_owners.py new file mode 100644 index 0000000000..16013201b1 --- /dev/null +++ b/research/rank7-chronological-face/sources/allocation/vendor/independent_owners.py @@ -0,0 +1,111 @@ +# SPDX-License-Identifier: Apache-2.0 +"""Independent integer-time and mask check of the actual parameterized-replica owner allocation with PR2802 retired7 providers. + +Chronology/mask method derives from Tekalign's PR2751 independent_owners.py; +Marius-Paul Dumitrean's PR2802 retired7 native construction and the retained +provider frame checker keep their +upstream attribution. No solver, producer, emitter or floating arithmetic is +imported. This checks finite geometry, not global native/outer admission. +""" +from pathlib import Path +from collections import Counter,defaultdict +import argparse,hashlib,gzip,json,sys,types +sys.dont_write_bytecode=True +def need(v,msg): + if not v:raise ValueError(msg) +def sha(p):return hashlib.sha256(p.read_bytes()).hexdigest() +def read(p): + b=Path(p).read_bytes();return json.loads(gzip.decompress(b)if str(p).endswith('.gz')else b) +def inputs(PROVIDER): + provider_pins={'inputs/PLAN.json.gz':'afb3c5c8134fc2cfce0b50a21758490c225574994b2c3c5161e53e2355acc6fa','inputs/GLOBAL-TEMPLATE.json.gz':'21297b20f1f2dc76eb9dd8124416068c3cb096bab9df17fa4da19bc68dfe082e','independent_local.py':'ee1faab70095fa312fc61d375ddf015b76104cb1a542ae7876a149e7999faa20','inputs/PROVIDERS.json':'391075b1411a3976850c633f92f58c35ed3f046f09d55bd435d7545124543fd4','inputs/WORD-base.json.gz':'dca8becca633ffc5e998985631bcbcab1123b27ca7f10ac6a96b1ec21ce69a66','inputs/WORD-extra.json.gz':'6bcb3c2c73eaf7558ddc6ef6b484334f8d96b9d2b227e265483b657de00f4bb7'} + hashes={} + for n,pin in provider_pins.items(): + p=PROVIDER/n;need(sha(p)==pin,'pinned PR2802 provider source '+n);hashes[str(p)]=pin + L=types.ModuleType('retained_independent_frames');exec(compile((PROVIDER/'independent_local.py').read_bytes(),'pinned_PR2802_independent_local.py','exec'),L.__dict__);providers=read(PROVIDER/'inputs/PROVIDERS.json') + for tag,pid in [('base','gauge44'),('extra','extra')]: + word=read(PROVIDER/f'inputs/WORD-{tag}.json.gz');report,start,ends=L.check_frames(word);L.check_cleanup(word);L.algebra(word) + widths=[L.dm(ends[k])-L.dm(start[k])for k in sorted(start)if k>=224] + need(widths==providers[pid]['widths']and len(widths)==408,'actual ordered provider frame widths');need(len(word['centers'])==8,'eight centres');providers[pid]['actual_paid_profile']={int(k):v for k,v in report['profile'].items()} + return read(PROVIDER/'inputs/PLAN.json.gz'),read(PROVIDER/'inputs/GLOBAL-TEMPLATE.json.gz'),providers,hashes + +def windows(template,order,T): + ranks={c['child']:c['rank']for c in template['idle_children']};pairs={e['stage']:e['pair']for e in template['recipe']if e['kind']=='local'} + blocks={};stage=None + for event in template['execution_schedule']: + if event['kind']in('bank_padding_cover_sweep','translate_every_live_family'):continue + if event['kind']=='local_cover_sweep':stage=event['stage'];blocks[stage]=[] + need(stage is not None,'source event before local call');blocks[stage].append(event) + need(set(blocks)==set(range(9)),'nine source stages') + progress=[0]*T;last={};result={} + for t,(stage,replica)in enumerate(order): + need(0<=replica0,'idle source position');start=last.get((replica,event['pair']),-1) + for child in event['child_indices']: + if child in ranks:result[replica,child]=(ranks[child],start,t) + elif kind in ('terminal_Y_translations','terminal'):pass # inherited terminal phase; no pending-window endpoints + else:raise ValueError('unknown source event kind') + need(progress==[9]*T,'complete replica source progression');return result + +def check(T,order,fill,dispatch,claimed,plan,template,providers): + need(type(T)is int and T>0,'positive T');N=9*T + need(len(order)==N and set(map(tuple,order))=={(s,r)for s in range(9)for r in range(T)},'complete T call coverage') + win=windows(template,order,T) + need(set(dispatch)==set(map(tuple,order))and all(p in providers for p in dispatch.values()),'provider dispatch coverage') + for s,r,pid in fill.get('dispatch_overrides',[]):need(dispatch.get((s,r))==pid,'final dispatch override binding') + need(fill['columns']==['time','helper','owner_replica','child','port','offset'],'literal role columns') + need(len(fill['rows'])==N*408,'complete role count');helpers=[0]*N;families=[0]*N;occupied={};lastrow={} + for idx,row in enumerate(fill['rows']): + need(len(row)==6 and all(type(x)is int for x in row),'integer role shape');t,h,o,c,p,z=row + need(0<=tlastrow[key][0]:lastrow[key]=(z,idx,w) + need(helpers==[(1<<408)-1]*N,'all helper identities');idle=Counter() + for(o,c),(cap,_,_)in win.items(): + for p in range(112): + key=(o,c,p);mask=occupied.get(key,0);used=mask.bit_count();need(mask==(1<= len(slots) + ti = {t: j for j, t in enumerate(times)} + A = np.zeros((K, K), dtype=np.int64) + slot_by_w = collections.defaultdict(list) + for j, w in enumerate(slots): + slot_by_w[w].append(j) + for w, js in slot_by_w.items(): + atslot = 0 + remaining = n + for t in times: + needed = counts.get((t, w), 0) + while needed: + take = min(needed, remaining) + A[ti[t], js[atslot]] += take + needed -= take + remaining -= take + if remaining == 0: + atslot += 1 + remaining = n + assert atslot == len(js) + assert all(v <= n for v in A.sum(axis=1)) + j = len(slots) + remaining = n + for r in range(K): + needed = n - int(A[r].sum()) + while needed: + assert j < K + take = min(needed, remaining) + A[r, j] += take + needed -= take + remaining -= take + if remaining == 0: + j += 1 + remaining = n + assert np.all(A.sum(axis=0) == n) and np.all(A.sum(axis=1) == n) + output = [] + for color in range(n): + matching = maximum_bipartite_matching(csr_matrix(A > 0), perm_type='column') + assert len(matching) == K and min(matching) >= 0 and len(set(map(int, matching))) == K + output.append([(times[r], slots[int(c)]) for r, c in enumerate(matching) if c < len(slots)]) + A[np.arange(K), matching] -= 1 + assert not A.any() + return output + + +def pattern_name(WID, counts): + return '+'.join(str(w) for w, k in zip(WID, counts) for _ in range(k)) or 'empty' + + +def fill_to_bins(fill, order, disp, providers): + """literal fill rows -> {bin: [(t, w)]} using the provider widths (helper column = 0-based index, as the engine reads it).""" + bybin = collections.defaultdict(list) + for t, h, o, c, p, z in fill['rows']: + w = providers[disp[tuple(order[t])]]['widths'][h] + bybin[o, c, p].append((t, w)) + return bybin + + +def price(profile, T, rel): + k_lo, k_hi = R.kappa_from_profile(profile, T) + cap_hi = Q(rel['cap_upper']) + return k_lo, k_hi, dict(kappa_lower=str(k_lo), kappa_upper=str(k_hi), kappa_lower_decimal=R.mpmath_str(k_lo, 25), kappa_upper_decimal=R.mpmath_str(k_hi, 25), + headline_floor24_minus=str(Q(int(k_lo * 10 ** 24), 10 ** 24) - Q(1, 10 ** 46) - Q(1, 10 ** 70)), + relaxation_cap_lower=rel['cap_lower'], relaxation_cap_upper=rel['cap_upper'], relaxation_cap_upper_decimal=rel['cap_upper_decimal'], + gap_to_relaxation_cap=float(cap_hi - k_lo), gain_vs_PR2917_claim_float=float(k_lo - PR2917_KAPPA), gain_vs_PR2917_root_lower_float=float(k_lo - PR2917_ROOT_LOWER), + gain_vs_PR2917_claim_exact_lower=str(k_lo - PR2917_KAPPA), + gain_vs_PR2930_claim_float=float(k_lo - PR2930_KAPPA), gain_vs_PR2930_claim_exact_lower=str(k_lo - PR2930_KAPPA), + gain_vs_PR2966_headline24=str(Q(int(k_lo * 10 ** 24), 10 ** 24) - PR2966_HEAD24), gain_vs_PR2966_float=float(Q(int(k_lo * 10 ** 24), 10 ** 24) - PR2966_HEAD24)) + + +def main(): + ap = argparse.ArgumentParser(description=__doc__, formatter_class=argparse.RawDescriptionHelpFormatter) + ap.add_argument('--work', type=pathlib.Path, required=True) + ap.add_argument('--chronology', choices=['pr2833-t37', 'pr2833-t74', 'pr2917-t74'], default='pr2833-t37') + ap.add_argument('--providers', type=pathlib.Path, default=PKG17 / 'allocation/PROVIDERS.json') + ap.add_argument('--local', help='JSON per-call local profile overriding PROVIDERS (both providers)') + ap.add_argument('--catalogue', default='tight', help="all | tight | tightonly | rc: (free-mix: patterns with reduced cost <= x at the cap root)") + ap.add_argument('--mix-file', type=pathlib.Path, help='PATTERNS.json-style target list [[cap, counts, n], ...] to use instead of the milp') + ap.add_argument('--mix-only', action='store_true') + ap.add_argument('--seconds', type=int, default=600) + ap.add_argument('--workers', type=int, default=1) + ap.add_argument('--seed', type=int, default=124) + ap.add_argument('--hint-flow', type=pathlib.Path, help='FLOW.json.gz of the same chronology/T (e.g. PR2857 allocation/construction/FLOW.json.gz for pr2833-t37)') + ap.add_argument('--hint-fill', type=pathlib.Path, help='literal FILL.json.gz of the same chronology (e.g. #2917 allocation/FILL.json.gz for pr2917-t74); converted to X/Z hints') + ap.add_argument('--hint-zeros', action='store_true') + ap.add_argument('--reuse-flow', type=pathlib.Path) + ap.add_argument('--solver', choices=['cp', 'highs-lp', 'highs-mip'], default='cp', help='cp = CP-SAT; highs-lp = LP relaxation feasibility only (fractional flow); highs-mip = scipy milp') + ap.add_argument('--check-fill', type=pathlib.Path, help='replay: owner-check and price this literal fill under the chronology (no solve)') + ap.add_argument('--free-mix', action='store_true', help='no global pattern targets: CP-SAT minimizes the linearized moment sum_bins H_idle(b*) over the catalogue (tight = relaxation-tight + single residues + empties; all = every pattern; rc:x = reduced cost <= x)') + ap.add_argument('--objective-scale', type=int, default=10 ** 6) + ap.add_argument('--buffers', type=int, default=PRIVATE_BUFFERS, help='private zero buffers for the physical display (PR2917 82, n45x4 86)') + ap.add_argument('--method', default='r13 lane C1: relax.py integer pattern mix + CP-SAT chronological flow + edge-colouring realization (fill17.py)') + a = ap.parse_args() + assert a.workers == 1, 'num_search_workers must be 1 on this machine (3 deadlocks)' + out = a.work.resolve() + out.mkdir(parents=True, exist_ok=False) + t0 = time.time() + assert hashlib.sha256(ENGINE.read_bytes()).hexdigest() == ENGINE_SHA, 'owner engine pin' + owner = types.ModuleType('frozen_owner') + exec(compile(ENGINE.read_bytes(), 'frozen_owner', 'exec'), owner.__dict__) + template, plan, order, dispatch, T = load_chronology(a.chronology) + local_override = {int(k): int(v) for k, v in json.loads(a.local).items()} if a.local else None + providers = load_providers(a.providers, local_override) + disp = {(s, r): p for s, r, p in dispatch} + inv_by_call = [collections.Counter(providers[disp[tuple(sr)]]['widths']) for sr in order] + calls_by_pid = collections.Counter(disp[tuple(sr)] for sr in order) + locals_ = {pid: providers[pid]['actual_paid_profile'] for pid in providers} + # relaxation cap (call-weighted average inventory; the local profile is the same for both providers here) + avg_inv = collections.Counter() + for inv in inv_by_call: + for w, n in inv.items(): + avg_inv[w] += Q(n, len(order)) + loc0 = next(iter(locals_.values())) + assert all(l == loc0 for l in locals_.values()), 'providers differ in local profile; relax.py needs one profile' + rel = X.relax(loc0, avg_inv) + cap_lo, cap_hi = Q(rel['cap_lower']), Q(rel['cap_upper']) + log('CHRONOLOGY', a.chronology, 'T', T, 'calls', len(order), 'calls per provider', dict(calls_by_pid)) + log('INVENTORY', {pid: dict(sorted(collections.Counter(providers[pid]['widths']).items())) for pid in providers}, 'LOCAL', loc0) + log('RELAX cap', rel['cap_lower_decimal'], rel['cap_upper_decimal'], 'tight', rel['tight_patterns'], 'idle/replica', rel['idle_per_replica']) + live = 896 * T + physical = live + HELPERS + CENTRES + a.buffers + GUARDS + + if a.check_fill: + fill = read(a.check_fill) + result, _, _ = owner.check(T, order, fill, disp, None, plan, template, providers) + profile = {int(k): v for k, v in result['profile'].items()} + k_lo, k_hi, pr = price(profile, T, rel) + bybin = fill_to_bins(fill, order, disp, providers) + pat_hist = collections.Counter() + win = owner.windows(template, order, T) + for (o, c), (cap, lo, hi) in win.items(): + for port in range(112): + rs = bybin.get((o, c, port), []) + pat_hist['%d:%s' % (cap, '+'.join(str(w) for w in sorted(w for t, w in rs)) or 'empty')] += 1 + assert result['live'] == live + check = dict(result, status='PASS_VENDORED_PR2839_OWNER_ENGINE_CHECK', mode='check-fill', fill=str(a.check_fill), chronology=a.chronology, T=T, + physical=result['live'] + HELPERS + CENTRES + a.buffers + GUARDS, physical_expected=physical, pattern_histogram=dict(sorted(pat_hist.items())), **pr) + save(out / 'OWNER-CHECK.json', check) + save(out / 'PROFILE.json', dict(sorted(profile.items()))) + log('CHECK-FILL PASS roles', result['roles'], 'idle', result['idle'], 'physical', check['physical']) + log('PATTERNS', dict(sorted(pat_hist.items()))) + log('KAPPA', pr['kappa_lower_decimal'], '..', pr['kappa_upper_decimal'], 'cap', rel['cap_upper_decimal'], 'gap %.3e' % pr['gap_to_relaxation_cap'], 'gain vs PR2917 claim %.4e' % pr['gain_vs_PR2917_claim_float'], 'gain vs PR2930 claim %.4e' % pr['gain_vs_PR2930_claim_float'], 'gain vs PR2966 %.6e' % pr['gain_vs_PR2966_float']) + return + + bins_per_replica = X.BINS + if a.free_mix: + WIDf = sorted({w for inv in inv_by_call for w in inv}) + allp = X.patterns(bins_per_replica, WIDf) + bstar = float((cap_lo + cap_hi) / 2) + if a.catalogue.startswith('rc:'): + thr = float(a.catalogue.split(':')[1]) + Y = rel['dual_Y'] + yv = lambda row: sum(float(Q(v)) * X.Hfloat(int(k), bstar) for k, v in Y[row].items()) + keep = {(cap, counts) for cap, counts, r in allp if X.Hfloat(r, bstar) - yv('cap%d' % cap) - sum(n * yv('w%d' % w) for w, n in zip(WIDf, counts)) <= thr} + elif a.catalogue == 'all': + keep = {(cap, counts) for cap, counts, r in allp} + else: + keep = {(t['capacity'], tuple(t['widths'].count(w) for w in WIDf)) for t in rel['tight_pattern_list']} + for cap in bins_per_replica: + for i, w in enumerate(WIDf): + if w <= cap: + keep.add((cap, tuple(int(j == i) for j in range(len(WIDf))))) + keep.add((cap, tuple(0 for _ in WIDf))) + target = {k: None for k in sorted(keep)} + WID = WIDf + log('FREE MIX catalogue', {cap: sum(1 for c, q in keep if c == cap) for cap in sorted(bins_per_replica)}) + elif a.mix_file: + mf = read(a.mix_file) + WID = [int(w) for w in mf['widths']] + target = {(int(cap), tuple(int(k) for k in counts)): int(n) for cap, counts, n in mf['target']} + else: + target, WID = integer_pattern_mix(inv_by_call, T, bins_per_replica, (cap_lo + cap_hi) / 2, a.catalogue, rel['tight_pattern_list']) + idle_mix = collections.Counter() + for (cap, counts), n in target.items(): + r = cap - sum(w * k for w, k in zip(WID, counts)) + assert r >= 0 + if r and n: + idle_mix[r] += n + profile_mix = collections.Counter(idle_mix) + for pid, ncalls in calls_by_pid.items(): + for r, n in locals_[pid].items(): + profile_mix[r] += n * ncalls + if a.free_mix: + mix_lo = mix_hi = None + mix_pr = dict(kappa_lower_decimal='(free mix)', kappa_upper_decimal='', gap_to_relaxation_cap=float('nan'), gain_vs_PR2917_claim_float=float('nan'), gain_vs_PR2930_claim_float=float('nan')) + else: + mix_lo, mix_hi, mix_pr = price(dict(profile_mix), T, rel) + if not a.free_mix: + log('PATTERN MIX', {('%d:%s' % (cap, pattern_name(WID, counts))): n for (cap, counts), n in sorted(target.items())}) + log('MIX kappa bracket', mix_pr['kappa_lower_decimal'], mix_pr['kappa_upper_decimal'], 'idle', dict(sorted(idle_mix.items())), 'gap to cap %.3e' % mix_pr['gap_to_relaxation_cap'], 'gain vs PR2917 %.4e' % mix_pr['gain_vs_PR2917_claim_float'], 'gain vs PR2930 %.4e' % mix_pr['gain_vs_PR2930_claim_float']) + if not a.free_mix: + save(out / 'PATTERNS.json', dict(mode='milp' if not a.mix_file else 'file', catalogue=a.catalogue, T=T, chronology=a.chronology, widths=WID, + target=[[cap, list(counts), n] for (cap, counts), n in sorted(target.items())], idle=dict(sorted(idle_mix.items())), + profile=dict(sorted(profile_mix.items())), **mix_pr)) + if a.mix_only: + return + + # ---- chronology windows and the flow model (PR2857 discover_original.py, all bins active) + win = owner.windows(template, order, T) + family = lambda b: b[0] * 896 + (2 * plan['pairs'][str(b[1])] + plan['sides'][str(b[1])]) * 112 + b[2] + fw = collections.defaultdict(list) + for (o, c), (cap, lo, hi) in win.items(): + fw[family((o, c, 0))].append((lo, hi, c)) + for ww in fw.values(): + for i, (lo, hi, c) in enumerate(ww): + assert all(max(lo, l) >= min(hi, h) for l, h, d in ww[i + 1:]), 'overlapping same-family windows' + need = {t: collections.Counter(inv_by_call[t]) for t in range(len(order))} + pats = collections.defaultdict(list) + for (cap, counts) in target: + pats[cap].append(counts) + groups = collections.defaultdict(list) + for (o, c), (cap, lo, hi) in win.items(): + for port in range(112): + groups[cap, tuple(range(max(0, lo + 1), min(len(order), hi + 1)))].append((o, c, port)) + G = sorted(groups) + groupof = {b: gi for gi, g in enumerate(G) for b in groups[g]} + edge, lb, ub, rl, ru = [], [], [], [], [] + Xv, Zv = {}, {} + + def cr(l, u=None): + j = len(rl) + rl.append(l) + ru.append(l if u is None else u) + return j + + def cv(u): + j = len(lb) + lb.append(0) + ub.append(u) + return j + + def put(r, v, n): + if n: + edge.append((r, v, n)) + callrow = {(t, w): cr(n) for t, cnt in need.items() for w, n in cnt.items() if n} + globalrow = {} if a.free_mix else {key: cr(n) for key, n in target.items()} + for gi, (cap, ts) in enumerate(G): + nb = len(groups[G[gi]]) + br = cr(nb) + for q in pats[cap]: + xv = cv(nb) + Xv[gi, q] = xv + put(br, xv, 1) + if not a.free_mix: + put(globalrow[cap, q], xv, 1) + residual = {w: q[j] for j, w in enumerate(WID) if q[j]} + wr = {w: cr(0) for w in residual} + for w, n in residual.items(): + put(wr[w], xv, -n) + for t in ts: + tr = cr(-nb, 0) + put(tr, xv, -1) + for w in residual: + if (t, w) not in callrow: + continue + zv = cv(min(nb, need[t][w])) + Zv[gi, q, t, w] = zv + put(tr, zv, 1) + put(wr[w], zv, 1) + put(callrow[t, w], zv, 1) + modelinfo = dict(T=T, chronology=a.chronology, groups=len(G), variables=len(lb), pattern_variables=len(Xv), flow_variables=len(Zv), constraints=len(rl), nonzeros=len(edge), workers=a.workers, + catalogue=a.catalogue, patterns_per_cap={str(cap): len(ps) for cap, ps in pats.items()}) + save(out / 'MODEL.json', modelinfo) + log('MODEL', modelinfo) + rr = np.fromiter((e[0] for e in edge), np.int32) + cc = np.fromiter((e[1] for e in edge), np.int32) + vv = np.fromiter((e[2] for e in edge), np.float64) + mat = coo_matrix((vv, (rr, cc)), shape=(len(rl), len(lb))).tocsr() + del edge + t1 = time.time() + if a.reuse_flow: + saved = read(a.reuse_flow) + value = np.zeros(len(lb), dtype=np.int64) + for gi, q, n in saved['x']: + value[Xv[gi, tuple(q)]] = n + for gi, q, t, w, n in saved['z']: + value[Zv[gi, tuple(q), t, w]] = n + status = 'EXACT_FLOW_REPLAY' + elif a.solver == 'highs-lp': + from scipy.optimize import milp, Bounds, LinearConstraint + r = milp(np.zeros(len(lb)), integrality=np.zeros(len(lb)), bounds=Bounds(np.array(lb, dtype=float), np.array(ub, dtype=float)), constraints=LinearConstraint(mat, np.array(rl, dtype=float), np.array(ru, dtype=float)), options={'time_limit': a.seconds, 'disp': True}) + status = 'LP_RELAXATION_' + ('FEASIBLE' if r.x is not None else 'INFEASIBLE_OR_FAILED') + ': ' + str(r.message) + log('LP RELAXATION', status, '%.1f s' % (time.time() - t1)) + save(out / 'SOLVER.json', dict(status=status, solver='highs-lp', seconds=time.time() - t1, chronology=a.chronology, T=T, catalogue=a.catalogue, mix_file=str(a.mix_file) if a.mix_file else None)) + return + elif a.solver == 'highs-mip': + from scipy.optimize import milp, Bounds, LinearConstraint + r = milp(np.zeros(len(lb)), integrality=np.ones(len(lb)), bounds=Bounds(np.array(lb, dtype=float), np.array(ub, dtype=float)), constraints=LinearConstraint(mat, np.array(rl, dtype=float), np.array(ru, dtype=float)), options={'time_limit': a.seconds, 'mip_rel_gap': 0, 'disp': True}) + status = str(r.message) + value = None if r.x is None else np.rint(r.x).astype(np.int64) + else: + from ortools.sat.python import cp_model + model = cp_model.CpModel() + vs = [model.NewIntVar(int(l), int(u), '') for l, u in zip(lb, ub)] + for j, (l, u) in enumerate(zip(rl, ru)): + b, e = mat.indptr[j:j + 2] + ind = mat.indices[b:e] + co = mat.data[b:e] + model.AddLinearConstraint(cp_model.LinearExpr.WeightedSum([vs[int(k)] for k in ind], [int(k) for k in co]), int(l), int(u)) + if a.free_mix: + bstar = float((cap_lo + cap_hi) / 2) + obj = [] + for (gi, q), j in Xv.items(): + r = G[gi][0] - sum(w * k for w, k in zip(WID, q)) + c = 0 if r == 0 else int(round(a.objective_scale * X.Hfloat(r, bstar))) + if c: + obj.append((vs[j], c)) + model.Minimize(cp_model.LinearExpr.WeightedSum([v for v, c in obj], [c for v, c in obj])) + hinted = {} + if a.hint_flow: + saved = read(a.hint_flow) + for gi, q, n in saved['x']: + if (gi, tuple(q)) in Xv: + hinted[Xv[gi, tuple(q)]] = min(int(n), int(ub[Xv[gi, tuple(q)]])) + for gi, q, t, w, n in saved['z']: + if (gi, tuple(q), t, w) in Zv: + hinted[Zv[gi, tuple(q), t, w]] = min(int(n), int(ub[Zv[gi, tuple(q), t, w]])) + log('HINT from flow', a.hint_flow, 'variables', len(hinted), 'of', len(vs)) + if a.hint_fill: + hf = read(a.hint_fill) + bybin = fill_to_bins(hf, order, disp, providers) + hx = collections.Counter() + hz = collections.Counter() + missing = collections.Counter() + for gi_, g_ in enumerate(G): + for b in groups[g_]: + rs = bybin.get(b, []) + q = tuple(sum(1 for t, w in rs if w == ww) for ww in WID) + if (gi_, q) not in Xv: + missing['%d:%s' % (G[gi_][0], pattern_name(WID, q))] += 1 + continue + hx[gi_, q] += 1 + for t, w in rs: + hz[gi_, q, t, w] += 1 + for k, n in hx.items(): + hinted[Xv[k]] = min(n, int(ub[Xv[k]])) + for k, n in hz.items(): + if k in Zv: + hinted[Zv[k]] = min(n, int(ub[Zv[k]])) + log('HINT from fill', a.hint_fill, 'bins hinted', sum(hx.values()), 'bins with non-catalogue patterns (unhinted)', sum(missing.values()), dict(missing.most_common(12)), 'variables', len(hinted)) + if hinted: + for j, v in hinted.items(): + model.AddHint(vs[j], v) + if a.hint_zeros: + for j in range(len(vs)): + if j not in hinted: + model.AddHint(vs[j], 0) + log('HINT total', len(hinted), '(+ zeros for the rest)' if a.hint_zeros else '') + solver = cp_model.CpSolver() + solver.parameters.num_search_workers = a.workers + solver.parameters.max_time_in_seconds = a.seconds + solver.parameters.random_seed = a.seed + solver.parameters.log_search_progress = True + result = solver.Solve(model) + status = solver.StatusName(result) + value = np.array([solver.Value(v) for v in vs], dtype=np.int64) if result in (cp_model.OPTIMAL, cp_model.FEASIBLE) else None + log(solver.ResponseStats()) + solve_seconds = time.time() - t1 + log('SOLVER', status, '%.1f s' % solve_seconds) + save(out / 'SOLVER.json', dict(status=status, seconds=solve_seconds, workers=a.workers, seed=a.seed, max_time_seconds=a.seconds, candidate=value is not None, chronology=a.chronology, T=T, catalogue=a.catalogue, + hint_flow=str(a.hint_flow) if a.hint_flow else None, hint_fill=str(a.hint_fill) if a.hint_fill else None, hint_zeros=a.hint_zeros)) + if value is None: + log('NO FEASIBLE FLOW (status %s)' % status) + raise SystemExit(2) + assert not (np.any(value < lb) or np.any(value > ub) or np.any(mat @ value < rl) or np.any(mat @ value > ru)) + xc = collections.defaultdict(collections.Counter) + zc = collections.defaultdict(collections.Counter) + for (gi, q), v in Xv.items(): + if value[v]: + xc[gi][q] = int(value[v]) + for (gi, q, t, w), v in Zv.items(): + if value[v]: + zc[gi, q][t, w] = int(value[v]) + save(out / 'FLOW.json.gz', {'x': [[gi, list(q), n] for gi, c in xc.items() for q, n in c.items()], 'z': [[gi, list(q), t, w, n] for (gi, q), c in zc.items() for (t, w), n in c.items()]}) + gc = collections.Counter() + for gi, c in xc.items(): + for q, n in c.items(): + gc[G[gi][0], q] += n + if a.free_mix: + target = dict(gc) + idle_mix = collections.Counter() + for (cap, counts), n in target.items(): + r = cap - sum(w * k for w, k in zip(WID, counts)) + if r: + idle_mix[r] += n + profile_mix = collections.Counter(idle_mix) + for pid, ncalls in calls_by_pid.items(): + for r, n in locals_[pid].items(): + profile_mix[r] += n * ncalls + log('FREE MIX realized', {('%d:%s' % (cap, pattern_name(WID, counts))): n for (cap, counts), n in sorted(target.items())}) + assert dict(gc) == target, 'global integer pattern counts differ' + for gi in range(len(G)): + assert sum(xc[gi].values()) == len(groups[G[gi]]), 'window class bin count' + call_count = collections.defaultdict(collections.Counter) + for (gi, q), c in zc.items(): + by_w = collections.Counter() + by_t = collections.Counter() + for (t, w), n in c.items(): + assert t in G[gi][1] and q[WID.index(w)] > 0, 'ineligible time/width flow' + by_w[w] += n + by_t[t] += n + call_count[t][w] += n + assert all(by_w[w] == q[j] * xc[gi][q] for j, w in enumerate(WID)), 'pattern-width supply' + assert all(n <= xc[gi][q] for n in by_t.values()), 'more than one role per bin/time' + assert all(call_count[t] == need[t] for t in range(len(order))), 'flow call width demand' + slots = [] + for gi, (cap, ts) in enumerate(G): + bins = groups[G[gi]] + offset = 0 + for q, n in sorted(xc[gi].items()): + res = color_pattern(n, q, zc[gi, q], WID) + assert len(res) == n + for b, it in zip(bins[offset:offset + n], res): + z = 0 + for t, w in sorted(it): + slots.append((t, w, *b, z)) + z += w + assert z <= cap + offset += n + assert offset == len(bins) + available = {t: collections.defaultdict(list) for t in range(len(order))} + for t in available: + for h, w in enumerate(providers[disp[tuple(order[t])]]['widths']): + available[t][w].append(h) + final = [] + for t, w, o, c, p, z in sorted(slots): + final.append([t, available[t][w].pop(), o, c, p, z]) + assert not any(v for d in available.values() for v in d.values()) + fill = {'columns': ['time', 'helper', 'owner_replica', 'child', 'port', 'offset'], 'dispatch_overrides': [], 'method': a.method, 'rows': sorted(final)} + result, _, _ = owner.check(T, order, fill, disp, None, plan, template, providers) + profile = {int(k): v for k, v in result['profile'].items()} + assert collections.Counter(profile) == profile_mix, 'realized profile differs from the pattern-mix profile' + assert result['live'] == live + k_lo, k_hi, pr = price(profile, T, rel) + payload_sha = {} + prov_out = {pid: {'actual_paid_profile': {str(r): n for r, n in providers[pid]['actual_paid_profile'].items()}, 'widths': providers[pid]['widths']} for pid in providers} + for n, obj in [('ORDER.json', order), ('FILL.json.gz', fill), ('DISPATCH.json', dispatch), ('PROFILE.json', {str(k): v for k, v in sorted(profile.items())}), ('PROVIDERS.json', prov_out)]: + save(out / n, obj) + payload_sha[n] = hashlib.sha256(json.dumps(obj, sort_keys=True, separators=(',', ':')).encode()).hexdigest() + check = dict(result, status='PASS_VENDORED_PR2839_OWNER_ENGINE_CHECK', solver=status, solve_seconds=solve_seconds, total_seconds=time.time() - t0, chronology=a.chronology, T=T, calls=len(order), + physical=result['live'] + HELPERS + CENTRES + a.buffers + GUARDS, physical_formula='live + 408 helpers + 8 centres + %d private buffers + 2 guards' % a.buffers, + inventory={pid: dict(sorted(collections.Counter(providers[pid]['widths']).items())) for pid in providers}, local=loc0, engine_sha256=ENGINE_SHA, catalogue=a.catalogue, + pattern_mix={('%d:%s' % (cap, pattern_name(WID, counts))): n for (cap, counts), n in sorted(target.items())}, payload_sha256=payload_sha, seed=a.seed, **pr) + save(out / 'OWNER-CHECK.json', check) + log('OWNER_CHECK_PASS', out, 'roles', result['roles'], 'idle', result['idle'], 'physical', check['physical']) + log('KAPPA', pr['kappa_lower_decimal'], '..', pr['kappa_upper_decimal'], 'cap', rel['cap_upper_decimal'], 'gap %.3e' % pr['gap_to_relaxation_cap'], 'gain vs PR2917 claim %.4e' % pr['gain_vs_PR2917_claim_float'], 'gain vs PR2930 claim %.4e' % pr['gain_vs_PR2930_claim_float'], 'gain vs PR2966 %.6e' % pr['gain_vs_PR2966_float']) + + +if __name__ == '__main__': + main() diff --git a/research/rank7-chronological-face/sources/tools/relax.py b/research/rank7-chronological-face/sources/tools/relax.py new file mode 100644 index 0000000000..97dfe35c43 --- /dev/null +++ b/research/rank7-chronological-face/sources/tools/relax.py @@ -0,0 +1,329 @@ +#!/usr/bin/env python3 +"""relax.py -- changed-inventory, fixed-capacity fractional relaxation (upper bound on the complex endpoint) +for an ARBITRARY per-call local profile and per-call helper-width inventory, with exact rational verification. + +Model (everything per replica; the fractional cap is independent of T): + * bins: every replica has 112 ports x 18 idle children; the child capacities (ranks) come from the + T37 template: 6 children of capacity 8, 4 of 16, 4 of 32, 4 of 48 -> bins {8:672, 16:448, 32:448, 48:448}. + * roles: every call hosts all its helpers; a helper of width w occupies w consecutive units of ONE bin; + the 9 calls of a replica supply 9*inventory[w] roles of width w per replica (the inventory is per call; + with two providers of different widths pass the call-weighted average, a Fraction is fine). + * pattern catalogue: every multiset of widths with sum <= capacity ("bounded count-vector enumeration"); + the bin then pays ONE idle child of rank cap - used (rank 0 = nothing). + * CHRONOLOGY IS IGNORED: no source windows, no per-call family collisions, no "one role per bin per call", + no integrality. A bin pattern count may be fractional. Hence this is an UPPER bound on what any + actual fill of the same inventory can reach, and the bound is NOT a chronological witness. + * local profile is fixed and fully paid: 9 * local[r] children of rank r per replica. + Moment: M_x(b) = (9*sum_r local_r H_r(b) + sum_p x_p H_{r_p}(b)) / (73*896), H_r(b) = r*(73/r)^b, + LP(b): min_x sum_p x_p H_{r_p}(b) s.t. sum_{p in cap c} x_p = bins[c], sum_p n_w(p) x_p = 9*inv[w], x>=0. + cap = the root b of min_x M_x(b) = 1 (g(b) = min_x M_x(b) is increasing). + +Exact verification (same technique as PR2857's audit_relaxation.py, re-implemented): + 1. float bisection with scipy/HiGHS locates b*; the optimal basis B (9 columns) is read off; + 2. x_B = B^-1 rhs exactly (Fractions) -> the primal profile; root bracketed at 10^-25 with the package's + rational interval arithmetic (root.py): M(lo) < 1 < M(hi) -> cap >= lo (x_B is feasible); + 3. dual y(b) = B^-T c_B(b) is an exact rational combination of the H_k(b): the Y matrix of the receipt; + every pattern's reduced cost at b = hi is bracketed with the H enclosures and must be > 0 (or identically 0 + for the tight patterns) -> by weak duality every feasible x has M_x(hi) >= M_{x_B}(hi) > 1 -> cap <= hi. + Reproduces PR2857: cap in [0.001720100805416885927944, 0.001720100805416885927945], 1163 patterns, 11 tight. + +Usage: + python -B relax.py --calibrate + python -B relax.py --inventory '{"4":26,"5":2,"7":62,"8":85,"9":233}' --local '{"1":2397,"2":640,"3":266,"4":128,"5":26,"8":8}' + python -B relax.py --delta-inventory '{"8":1,"9":-1}' --delta-local '{"1":3,"2":-2}' # relative to PR2857 + python -B relax.py --scenarios # the hypothetical table of ROUND.md (one/two 9->8, 8->7, removal) +API: relax(local, inventory, bins=BINS) -> dict (cap_lower, cap_upper, active patterns, idle histogram, dual check, ...) +""" +from fractions import Fraction as Q +from itertools import product +import argparse, json, sys, os +sys.path.insert(0, os.path.dirname(os.path.abspath(__file__))) +import root as R + +BINS = {8: 672, 16: 448, 32: 448, 48: 448} # bins per replica (112 ports x children per capacity) +LIVE = R.LIVE_PER_REPLICA # 896 +CALLS = R.CALLS_PER_REPLICA # 9 +PR2857_LOCAL = {1: 2394, 2: 642, 3: 266, 4: 128, 5: 26, 8: 8} +PR2857_INV = {4: 26, 5: 2, 7: 62, 8: 84, 9: 234} +PR2857_REALIZED_LOWER = Q('17200966286848326009728/10000000000000000000000000') +PR2857_REALIZED_UPPER = Q('17200966286848326009729/10000000000000000000000000') +PR2857_CAP_UPPER = Q('344020161083377185589/200000000000000000000000') # 0.001720100805416885927945 +PR2848_KAPPA = Q('17186585083049300/10000000000000000000') # 0.0017186585083049300 (incumbent of PR2857's gain) + + +def need(c, m): + if not c: + raise ValueError(m) + + +def patterns(bins, widths): + out = [] + for cap in sorted(bins): + for counts in product(*(range(cap // w + 1) for w in widths)): + used = sum(w * n for w, n in zip(widths, counts)) + if used <= cap: + out.append((cap, counts, cap - used)) + return out + + +def Hfloat(r, b): + import math + return 0.0 if r == 0 else r * (73.0 / r) ** b + + +def lp_min(pats, caps, widths, rhs, b): + """float LP at saving b: returns (optimal value, x, duals y).""" + import numpy as np + from scipy.optimize import linprog + c = np.array([Hfloat(r, b) for cap, counts, r in pats]) + A = np.zeros((len(caps) + len(widths), len(pats))) + for j, (cap, counts, r) in enumerate(pats): + A[caps.index(cap), j] = 1.0 + for i, n in enumerate(counts): + if n: + A[len(caps) + i, j] = n + res = linprog(c, A_eq=A, b_eq=np.array([float(v) for v in rhs]), bounds=(0, None), method='highs') + need(res.status == 0, 'LP infeasible or failed: ' + res.message) + return res.fun, res.x, res.eqlin.marginals, A + + +def rat_inverse(Bm): + n = len(Bm) + M = [row[:] + [Q(int(i == j)) for j in range(n)] for i, row in enumerate(Bm)] + for col in range(n): + piv = next((r for r in range(col, n) if M[r][col] != 0), None) + need(piv is not None, 'singular basis') + M[col], M[piv] = M[piv], M[col] + f = M[col][col] + M[col] = [v / f for v in M[col]] + for r in range(n): + if r != col and M[r][col] != 0: + g = M[r][col] + M[r] = [a - g * bb for a, bb in zip(M[r], M[col])] + return [row[n:] for row in M] + + +def rat_rank(cols): + """rank of a list of rational column vectors""" + rows = [list(c) for c in cols] + rank = 0 + ncol = len(rows[0]) if rows else 0 + for col in range(ncol): + piv = next((r for r in range(rank, len(rows)) if rows[r][col] != 0), None) + if piv is None: + continue + rows[rank], rows[piv] = rows[piv], rows[rank] + for r in range(len(rows)): + if r != rank and rows[r][col] != 0: + g = rows[r][col] / rows[rank][col] + rows[r] = [a - g * bb for a, bb in zip(rows[r], rows[rank])] + rank += 1 + return rank + + +def column(pat, caps, widths): + cap, counts, r = pat + return [Q(int(cap == c)) for c in caps] + [Q(n) for n in counts] + + +def relax(local, inventory, bins=BINS, digits=25, verbose=False): + local = {int(r): Q(n) for r, n in local.items() if Q(n) != 0} + inventory = {int(w): Q(n) for w, n in inventory.items() if Q(n) != 0} + need(all(n > 0 for n in local.values()) and all(n > 0 for n in inventory.values()), 'positive local/inventory') + widths = sorted(inventory) + caps = sorted(bins) + pats = patterns(bins, widths) + rhs = [Q(bins[c]) for c in caps] + [CALLS * inventory[w] for w in widths] + local_rep = {r: CALLS * n for r, n in local.items()} + total_cap = sum(c * bins[c] for c in caps) + inv_mass = sum(w * inventory[w] for w in widths) * CALLS + local_mass = sum(r * n for r, n in local_rep.items()) + idle_mass = total_cap - inv_mass + need(idle_mass >= 0, 'inventory exceeds bin capacity') + mass_ok = (local_mass + idle_mass == R.MASS_PER_REPLICA) + + # --- 1. float bisection on b + import numpy as np + def gfloat(b): + val, x, y, A = lp_min(pats, caps, widths, rhs, b) + loc = sum(float(n) * Hfloat(r, b) for r, n in local_rep.items()) + return (loc + val) / (73 * LIVE) - 1.0, x, y + lo, hi = 0.0, 0.01 + g_lo, _, _ = gfloat(lo) + g_hi, _, _ = gfloat(hi) + need(g_lo < 0 < g_hi, 'root window [0, 0.01] does not bracket the cap') + for _ in range(64): + mid = (lo + hi) / 2 + g, x, y = gfloat(mid) + if g < 0: + lo = mid + else: + hi = mid + b_star = (lo + hi) / 2 + g, x, y, = gfloat(b_star) + val, x, y, A = lp_min(pats, caps, widths, rhs, b_star) + + # --- 2. basis: support of x, completed by tight (zero reduced cost) columns to full rank + c = np.array([Hfloat(r, b_star) for cap, counts, r in pats]) + rc = c - A.T @ y + order = sorted(range(len(pats)), key=lambda j: (0 if x[j] > 1e-9 else 1, abs(float(rc[j])), -float(x[j]))) + basis = [] + cols = [] + for j in order: + if len(basis) == len(rhs): + break + if x[j] <= 1e-9 and abs(rc[j]) > 1e-7: + continue + col = column(pats[j], caps, widths) + if rat_rank(cols + [col]) > len(cols): + basis.append(j) + cols.append(col) + need(len(basis) == len(rhs), 'could not complete an optimal basis (degenerate LP); %d of %d' % (len(basis), len(rhs))) + Bm = [[cols[k][i] for k in range(len(basis))] for i in range(len(rhs))] # rows = constraints + Binv = rat_inverse(Bm) + xB = [sum(Binv[k][i] * rhs[i] for i in range(len(rhs))) for k in range(len(basis))] + need(all(v >= 0 for v in xB), 'basis not primal feasible') + active = [(pats[j], xB[k]) for k, j in enumerate(basis) if xB[k] > 0] + idle = {} + for (cap, counts, r), n in active: + if r: + idle[r] = idle.get(r, 0) + n + full = dict(local_rep) + for r, n in idle.items(): + full[r] = full.get(r, 0) + n + cap_lo, cap_hi = R.root_bracket(full, LIVE, digits, check_mass_T=1 if mass_ok else None) + + # --- 3. exact dual in the H basis: y_j(b) = sum_k (B^-T)_{j,k} H_{r_k}(b) + ranks = sorted({r for cap, counts, r in pats if r}) + # (B^-T)_{j,k} = Binv[k][j] + Y = {j: {} for j in range(len(rhs))} + for j in range(len(rhs)): + for k, pj in enumerate(basis): + r = pats[pj][2] + if r == 0 or Binv[k][j] == 0: + continue + Y[j][r] = Y[j].get(r, 0) + Binv[k][j] + Hhi = {r: R.H(r, cap_hi) for r in ranks} + tight = [] + strict = 0 + min_slack = None + for p in pats: + cap, counts, r = p + a = column(p, caps, widths) + coeff = {} + if r: + coeff[r] = Q(1) + for j in range(len(rhs)): + if a[j] == 0: + continue + for k, v in Y[j].items(): + coeff[k] = coeff.get(k, 0) - a[j] * v + coeff = {k: v for k, v in coeff.items() if v != 0} + if not coeff: + tight.append(p) + continue + lower = sum(v * (Hhi[k][0] if v > 0 else Hhi[k][1]) for k, v in coeff.items()) + need(lower > 0, 'dual sign failure for pattern %s (reduced-cost lower bound %s)' % (str(p), str(lower))) + strict += 1 + min_slack = lower if min_slack is None else min(min_slack, lower) + dual_obj = sum(rhs[j] * sum(v * Hhi[k][0] for k, v in Y[j].items()) for j in range(len(rhs))) # not needed for the proof, informational + dual_rows = ['cap%d' % c for c in caps] + ['w%d' % w for w in widths] + return dict( + status='PASS_EXACT_RELAXATION_CAP' if mass_ok else 'PASS_EXACT_RELAXATION_CAP_MASS_NOT_65088', + cap_lower=str(cap_lo), cap_upper=str(cap_hi), cap_lower_decimal=R.mpmath_str(cap_lo, digits), cap_upper_decimal=R.mpmath_str(cap_hi, digits), + patterns=len(pats), tight_patterns=len(tight), strict_patterns=strict, minimum_slack_lower=str(min_slack), + basis_patterns=[dict(capacity=pats[j][0], widths=[w for w, n in zip(widths, pats[j][1]) for _ in range(n)], count_per_replica=str(xB[k])) for k, j in enumerate(basis)], + tight_pattern_list=[dict(capacity=p[0], widths=[w for w, n in zip(widths, p[1]) for _ in range(n)]) for p in tight], + idle_per_replica={str(r): str(n) for r, n in sorted(idle.items())}, + idle_mass_per_replica=str(idle_mass), local_mass_per_replica=str(local_mass), rank_mass_per_replica=str(local_mass + idle_mass), rank_mass_identity=mass_ok, + dual_Y={dual_rows[j]: {str(k): str(v) for k, v in sorted(Y[j].items())} for j in range(len(rhs))}, + inventory_per_call={str(w): str(inventory[w]) for w in widths}, local_per_call={str(r): str(n) for r, n in sorted(local.items())}, bins_per_replica=bins, + delta_vs_PR2857_realized=dict(lower=str(cap_lo - PR2857_REALIZED_UPPER), upper=str(cap_hi - PR2857_REALIZED_LOWER), float=float(cap_lo - PR2857_REALIZED_LOWER)), + delta_vs_PR2857_cap=dict(float=float(cap_lo - PR2857_CAP_UPPER)), + assumptions='fixed capacities 8/16/32/48 (112 ports x 6/4/4/4 children per replica), all count-vector patterns with sum<=cap, one idle child of rank cap-used per bin, chronology/windows/collisions/integrality ignored, local profile fully paid; upper bound on any actual fill of this inventory, not a witness', + ) + + +def scenarios(): + base_local, base_inv = PR2857_LOCAL, PR2857_INV + def mod(dl, di): + l = {r: base_local.get(r, 0) + dl.get(r, 0) for r in set(base_local) | set(dl)} + i = {w: base_inv.get(w, 0) + di.get(w, 0) for w in set(base_inv) | set(di)} + return {r: n for r, n in l.items() if n}, {w: n for w, n in i.items() if n} + table = [ + ('PR2857 actual (calibration)', {}, {}), + ('one more 9->8 at PR2857 cost {1:+3,2:-2}', {1: 3, 2: -2}, {8: 1, 9: -1}), + ('one more 9->8 at PR2853 cost {1:+5,2:-3}', {1: 5, 2: -3}, {8: 1, 9: -1}), + ('one more 9->8 at minimal cost {1:+1,2:-1}', {1: 1, 2: -1}, {8: 1, 9: -1}), + ('two more 9->8 at PR2857 cost {1:+6,2:-4}', {1: 6, 2: -4}, {8: 2, 9: -2}), + ('four more 9->8 at PR2857 cost {1:+12,2:-8}', {1: 12, 2: -8}, {8: 4, 9: -4}), + ('one 8->7 at PR2857-like cost {1:+3,2:-2}', {1: 3, 2: -2}, {7: 1, 8: -1}), + ('one 8->7 at minimal cost {1:+1,2:-1}', {1: 1, 2: -1}, {7: 1, 8: -1}), + ('one 9->7 (two units) at cost {1:+6,2:-4}', {1: 6, 2: -4}, {7: 1, 9: -1}), + ('remove one width-9 helper, its 9 one-dim climbs vanish {1:-9}', {1: -9}, {9: -1}), + ('remove one width-9 helper paying {1:-7,2:-1}', {1: -7, 2: -1}, {9: -1}), + ('remove one width-8 helper {1:-8}', {1: -8}, {8: -1}), + ('remove one width-4 helper {1:-4}', {1: -4}, {4: -1}), + ('local only: +1 H1 -1 H2 per call (mass -1, inventory unchanged: NOT a legal word, derivative probe)', {1: 1, 2: -1}, {}), + ('local only: -1 H1 per call (mass -1, derivative probe)', {1: -1}, {}), + ('local only: 2 H1 -> 1 H2 per call (mass neutral)', {1: -2, 2: 1}, {}), + ('local only: 1 H3 -> 1 H1 + 1 H2 per call (mass neutral)', {3: -1, 1: 1, 2: 1}, {}), + ] + out = [] + for name, dl, di in table: + l, i = mod(dl, di) + try: + r = relax(l, i) + row = dict(scenario=name, delta_local=dl, delta_inventory=di, cap_lower=r['cap_lower_decimal'], cap_upper=r['cap_upper_decimal'], + gain_vs_PR2857_realized_float=r['delta_vs_PR2857_realized']['float'], gain_vs_PR2857_cap_float=r['delta_vs_PR2857_cap']['float'], + tight=r['tight_patterns'], patterns=r['patterns'], idle_per_replica=r['idle_per_replica'], basis=r['basis_patterns'], rank_mass_identity=r['rank_mass_identity'], status=r['status']) + except Exception as e: # noqa + row = dict(scenario=name, delta_local=dl, delta_inventory=di, error=str(e)) + out.append(row) + print('%-95s cap<= %s gain vs realized %+.4e vs cap %+.4e %s' % (name, row.get('cap_upper', '?'), row.get('gain_vs_PR2857_realized_float', float('nan')), row.get('gain_vs_PR2857_cap_float', float('nan')), row.get('error', '')), file=sys.stderr, flush=True) + return out + + +def main(): + ap = argparse.ArgumentParser(description=__doc__, formatter_class=argparse.RawDescriptionHelpFormatter) + ap.add_argument('--calibrate', action='store_true') + ap.add_argument('--scenarios', action='store_true') + ap.add_argument('--inventory', help='JSON per-call {width: count}') + ap.add_argument('--local', help='JSON per-call {rank: count}') + ap.add_argument('--delta-inventory', help='JSON {width: +-count} relative to PR2857') + ap.add_argument('--delta-local', help='JSON {rank: +-count} relative to PR2857') + ap.add_argument('--digits', type=int, default=25) + ap.add_argument('--out') + a = ap.parse_args() + if a.calibrate: + r = relax(PR2857_LOCAL, PR2857_INV, digits=a.digits) + r['reproduces_PR2857_cap_lower'] = (Q(r['cap_lower']) == Q('215012600677110740993/125000000000000000000000')) + r['bracket_inside_PR2857_bracket'] = (Q(r['cap_lower']) >= Q('215012600677110740993/125000000000000000000000') and Q(r['cap_upper']) <= PR2857_CAP_UPPER) + r['reproduces_PR2857_cap_upper_at_24_digits'] = (relax(PR2857_LOCAL, PR2857_INV, digits=24)['cap_upper'] == str(PR2857_CAP_UPPER)) + r['reproduces_PR2857_pattern_count_1163'] = (r['patterns'] == 1163) + r['reproduces_PR2857_11_tight_1152_strict'] = (r['tight_patterns'] == 11 and r['strict_patterns'] == 1152) + res = r + elif a.scenarios: + res = scenarios() + else: + local = dict(PR2857_LOCAL) + inv = dict(PR2857_INV) + if a.local: + local = {int(k): Q(v) for k, v in json.loads(a.local).items()} + if a.inventory: + inv = {int(k): Q(v) for k, v in json.loads(a.inventory).items()} + if a.delta_local: + for k, v in json.loads(a.delta_local).items(): + local[int(k)] = local.get(int(k), 0) + Q(v) + if a.delta_inventory: + for k, v in json.loads(a.delta_inventory).items(): + inv[int(k)] = inv.get(int(k), 0) + Q(v) + res = relax({k: v for k, v in local.items() if v}, {k: v for k, v in inv.items() if v}, digits=a.digits) + s = json.dumps(res, indent=1, sort_keys=True, default=str) + if a.out: + open(a.out, 'w').write(s) + print(s) + + +if __name__ == '__main__': + main() diff --git a/research/rank7-chronological-face/verify.py b/research/rank7-chronological-face/verify.py new file mode 100644 index 0000000000..a98c18882f --- /dev/null +++ b/research/rank7-chronological-face/verify.py @@ -0,0 +1,110 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Independent finite Hall/face check; no solver or predecessor code imports. + +Ross Richardson, with substantial OpenAI Codex assistance. Separate AI +mathematical checks are not independent human review or a formal-kernel proof. +""" +import argparse +import hashlib +import json +from pathlib import Path + +ROOT = Path(__file__).resolve().parent +SOURCE = "be191346391661f4d35fc0d1508d0a6029572576" +BASE = "30f016dd79ee6a23c40d7dab44a9466c148c42dd" + + +def require(value, reason): + if not value: + raise ValueError(reason) + + +def check_payload(row, raw): + require(hashlib.sha256(raw).hexdigest() == row["sha256"], + "frozen source SHA256: " + row["export_path"]) + blob = hashlib.sha1(b"blob " + str(len(raw)).encode() + b"\0" + raw).hexdigest() + require(blob == row["git_blob"], "frozen source Git blob: " + row["export_path"]) + require(len(raw) == row["bytes"], "frozen source byte count") + + +def check_sources(root): + manifest = json.loads((root / "SOURCES.json").read_text()) + require(manifest["source_commit"] == SOURCE and manifest["base_commit"] == BASE, + "exact scientific pins") + rows = [row for row in manifest["files"] if "export_path" in row] + require(len(rows) == 19, "complete frozen evidence subset") + names = set() + for row in rows: + name = row["export_path"] + path = root / name + require(name.startswith("sources/") and name not in names and + path.resolve().is_relative_to((root / "sources").resolve()) and + path.is_file() and not path.is_symlink(), "unique local frozen source") + require(row["pin"] == "head:" + SOURCE + ":" + row["path"], "source commit binding") + names.add(name) + check_payload(row, path.read_bytes()) + actual = {p.relative_to(root).as_posix() for p in (root / "sources").rglob("*") if p.is_file()} + require(actual == names, "no unpinned frozen files") + row = rows[0] + raw = (root / row["export_path"]).read_bytes() + bad = bytes([raw[0] ^ 1]) + raw[1:] + try: + check_payload(row, bad) + except ValueError as exc: + require(str(exc).startswith("frozen source SHA256:"), "source drift rejection reason") + else: + raise ValueError("accepted frozen source corruption") + return {"files": len(rows), "bytes": sum(row["bytes"] for row in rows), + "source_commit": SOURCE, "manifest_sha256": hashlib.sha256( + (root / "SOURCES.json").read_bytes()).hexdigest(), + "controls": ["changed frozen byte rejected before mathematical checks"]} + + +def source_module(root, name): + """Load the two new implementations directly from source, without a pyc.""" + path = root / name + namespace = {"__name__": name[:-3], "__file__": str(path)} + exec(compile(path.read_bytes(), str(path), "exec"), namespace) + return namespace + + +def verify(root=ROOT): + root = Path(root) + sources = check_sources(root) + hall = source_module(root, "independent_hall.py")["verify_hall"](root) + face = source_module(root, "independent_face.py")["verify_face"](root) + require(hall["literal_witness"]["conditional_complete_profile"] == face["T74_profile"], + "literal provider invoice equals independent pattern invoice") + require(hall["literal_witness"]["idle_profile"] == + {rank: 2 * count for rank, count in face["T37"]["idle"].items()}, + "literal idle ranks equal doubled independent pattern ranks") + require(hall["face_family"]["integer_k_inclusive"] == + [face["integer_family"]["first"], face["integer_family"]["last"]], + "identical mathematical family in both independent checks") + require(check_sources(root) == sources, "frozen evidence unchanged during replay") + result = {"status": "PASS_RANK7_CHRONOLOGICAL_FACE_NO_NEW_KAPPA", + "sources": sources, "hall": hall, "face": face, + "scope": "Finite source-bound interval obstruction, pattern-family identity and " + "literal owner geometry conditional on the supplied native width registry; " + "no native residual, precision, outer, all-size or new-kappa admission."} + # The independent counters use integer keys; the receipt has JSON keys. + return json.loads(json.dumps(result, sort_keys=True)) + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--check-result", action="store_true") + parser.add_argument("--write-result", action="store_true") + args = parser.parse_args() + require(not (args.check_result and args.write_result), "choose one result mode") + result = verify() + if args.check_result: + require(result == json.loads((ROOT / "RESULT.json").read_text()), "recorded result matches replay") + if args.write_result: + (ROOT / "RESULT.json").write_text(json.dumps(result, sort_keys=True, indent=2) + "\n") + print(json.dumps(result, sort_keys=True, indent=2)) + + +if __name__ == "__main__": + main()