diff --git a/research/p104-joint-restriction-gate/CERTIFICATE.json.gz b/research/p104-joint-restriction-gate/CERTIFICATE.json.gz new file mode 100644 index 0000000000..ffcf64a5a3 Binary files /dev/null and b/research/p104-joint-restriction-gate/CERTIFICATE.json.gz differ diff --git a/research/p104-joint-restriction-gate/INPUTS.json b/research/p104-joint-restriction-gate/INPUTS.json new file mode 100644 index 0000000000..567cb4c563 --- /dev/null +++ b/research/p104-joint-restriction-gate/INPUTS.json @@ -0,0 +1,29 @@ +{ + "source_head": "05cd36e5af06d7a3790e30ce3f449fa89b853768", + "files": { + "WORD.json.gz": { + "commit": "05cd36e5af06d7a3790e30ce3f449fa89b853768", + "path": "research/p104-unread-path-resynthesis/WORD.json.gz", + "git_blob": "6341a49f717bd64ef2a5b7c440bd86d5513425dc", + "sha256": "5d50e5654910c9535e9025de0f644bb2dece2396e799b4a766110363448fd0b0" + }, + "PR5827-NOTICE": { + "commit": "05cd36e5af06d7a3790e30ce3f449fa89b853768", + "path": "research/p104-unread-path-resynthesis/NOTICE", + "git_blob": "8fc3f76cc0d66f19c9abd7c7111ec69c73c0434d", + "sha256": "fe02063ca48bf070303ac05f613ab1e6e4dd9ee62141f7e7012d855faf7b0c78" + }, + "PR5827-PROOF.md": { + "commit": "05cd36e5af06d7a3790e30ce3f449fa89b853768", + "path": "research/p104-unread-path-resynthesis/PROOF.md", + "git_blob": "eae2e1b895284155a1485f240a0ad43a4b52c0aa", + "sha256": "16b1ba9b9468b097796d900ac04f9a278e09cba5ec9e08436b6e06ee066b385b" + }, + "PR5827-RESULT.json": { + "commit": "05cd36e5af06d7a3790e30ce3f449fa89b853768", + "path": "research/p104-unread-path-resynthesis/RESULT.json", + "git_blob": "e2e078df445d6c1b988cf926fed3bc7570a88237", + "sha256": "e437dd9fc7368de705cef8a9d27c6161f1b246f36e320e5c155dde89f88e16e2" + } + } +} diff --git a/research/p104-joint-restriction-gate/LICENSE b/research/p104-joint-restriction-gate/LICENSE new file mode 100644 index 0000000000..261eeb9e9f --- /dev/null +++ b/research/p104-joint-restriction-gate/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/p104-joint-restriction-gate/NOTICE b/research/p104-joint-restriction-gate/NOTICE new file mode 100644 index 0000000000..e5c107cf8f --- /dev/null +++ b/research/p104-joint-restriction-gate/NOTICE @@ -0,0 +1,10 @@ +P104 joint restriction gate +Copyright 2026 Ali Romman. Apache-2.0. + +New proof, discovery and checks by Ali Romman with substantial OpenAI Codex +assistance; no subagents. All checks are author-side. + +The exact PR5827 notice is retained at inputs/PR5827-NOTICE. The source word, +proof and receipt remain unchanged. Credit Mason Hale, Joel Pulikkan, Dugongue, +flyingviper, Cinna Davis and all retained P104, native, caller, compiler and BIT +authors. The earlier single-input and forty-helper screens retain their authors. diff --git a/research/p104-joint-restriction-gate/ONE-PERCENT.json.gz b/research/p104-joint-restriction-gate/ONE-PERCENT.json.gz new file mode 100644 index 0000000000..5957810a5d Binary files /dev/null and b/research/p104-joint-restriction-gate/ONE-PERCENT.json.gz differ diff --git a/research/p104-joint-restriction-gate/PROOF.md b/research/p104-joint-restriction-gate/PROOF.md new file mode 100644 index 0000000000..d0b731883a --- /dev/null +++ b/research/p104-joint-restriction-gate/PROOF.md @@ -0,0 +1,168 @@ +# Exact joint-restriction gate + +## 1. Fixed source and quantified model + +Let T be the decoded scalar map of the pinned PR5827 word. Its 770 public +coordinates are independent. Its 29 owned coordinates start arbitrary; INIT +must erase their input columns, and all owned outputs are zero. On public +coordinates, T is the identity plus the 104 prescribed X-to-Y shears. +The exact forward and transpose checks establish these statements for this +finite scalar word. Native realization is a retained source premise. + +Partition the public coordinates into 666 groups: one pair `{r,r+112}` for +each live main port r, and one singleton for each of the 562 helpers. Choose +any set D of groups to remove. Retain at least one main pair. Set removed +inputs to zero and omit removed outputs. Paired main removal ensures that +T has no coupling between a removed pair and a retained pair. + +At every original paid query e, compute the exact decoded prefix row and +suffix column on the original word. Let A_e and B_e be their group supports. +The discovery model permits removal of e if + +``` +A_e is contained in D, or B_e is contained in D. +``` + +The first condition makes the original argument zero. The second condition +makes a change in the original queried field invisible to retained outputs. +Grant both conditions independently, at every query. Their simultaneous +physical implementation is not assumed. This is a relaxation: a candidate +that uses only these original support discounts cannot receive a larger +discount. A candidate that changes the arguments or creates new cancellations +is outside this model. + +The replay uses exact rational coefficients. No modular rank or sampled +column is used in the certificate. The source query count is 3455. The scalar +map and its transpose are checked on all 799 input labels; owned input columns +are erased. The current query ranks and helper target ranks are read from the +source frames. Their complete histograms equal the published source receipt. +No new native phase assertion follows from this scalar check. + +## 2. Complete price and rational bounds + +Put H_r = r^(1-kappa). For a helper group g, let w_g be H_r at its original +productive target rank r. For a main-port pair, define + +``` +w_main = [2 H_145 - 15 H_1 + + 2 sum_(l in {7,8}) sum_(j=1..l) + (H_(1+8(j+1)) - H_(8(j+1)))] / 18. +``` + +There are 18 full calls, 15 thin shears and two main lanes per port on the +length-seven and length-eight paths. Thus the complete moment margin divided +by 18, for a candidate in the relaxation, is + +``` +Phi(D) = sum_(g not in D) w_g + - sum_(e not granted removal) H_rank(e). +``` + +The implementation reconstructs the original full invoice from these terms. +It matches 66870 paid calls and 13444 productive fields, including every whole +idle and thin query. New nonnegative costs are omitted favorably. + +The tests use the exact rational values `.003124767` and `.003156014468`. +The latter equals `101/100` times the declared source `.00312476680`. +No interval monotonicity statement is used. + +For an integer r, write r = 2^m u with 1 <= u < 2. For +z = (u-1)/(u+1), use + +``` +log u = 2 sum_(j>=0) z^(2j+1)/(2j+1). +``` + +After 32 terms, the remaining positive tail is at most +`2 z^65 / [65(1-z^2)]`. Apply the same bound to log 2 with z=1/3. +This gives rational L <= log r <= U. Here `0 <= kappa U < 1`. +The alternating exponential series of degrees 13 and 14 gives + +``` +r sum_(j=0..13) (-kappa U)^j/j! <= H_r +H_r <= r sum_(j=0..14) (-kappa L)^j/j!. +``` + +All terms are rational. Use upper bounds for retained target terms and lower bounds for retained +paid terms. In w_main, use lower bounds on its subtracted idle terms. +At scale S=10^12, round target weights upward to integers c_g and query +weights downward to integers p_e. Then + +``` +S Phi(D) <= sum_(g not in D) c_g - sum_(e retained) p_e. +``` + +Rounding is done on retained terms. Thus removing a term removes the same +integer from the total; no inconsistent debit is introduced. + +## 3. Branch coverage and flow dual + +A branch fixes a set Y of removed groups and a disjoint set N of retained +groups. If A_e meets N, the input condition is impossible on this branch. +If B_e meets N, the output condition is impossible. If both are impossible, +the query is not granted a discount. If exactly one remains possible, use +its complete support as a necessary removed set. If both remain possible, +use A_e intersect B_e as a necessary removed set. Remove Y from this set. +Call the resulting free-group set K_e. + +Merge equal K_e and add their integer query prices. This produces terms +(K_i, p_i). Set C = sum_g c_g - sum_e p_e. The branch margin is at most + +``` +C - sum_(g in Y) c_g + + sum_i p_i v_i - sum_(free g) c_g z_g, +``` + +where z_g is the removal indicator and v_i <= z_g for every g in K_i. +This implication is only a necessary condition. Replacing the true query +predicate by it can only increase the upper bound. + +The certificate supplies nonnegative integer allocations f_ig only on +edges g in K_i. It satisfies + +``` +sum_g f_ig <= p_i, sum_i f_ig <= c_g. +``` + +Since v_i <= z_g, subtracting the allocated parts and using these two +capacity inequalities gives + +``` +sum_i p_i v_i - sum_g c_g z_g <= sum_i p_i - sum_ig f_ig. +``` + +The checker validates every edge and both capacities. It does not solve a +flow problem. Every priced leaf has the strict integer bound + +``` +C - sum_(g in Y) c_g + sum_i p_i - sum_ig f_ig < 0. +``` + +Every internal node splits one previously free group into its retained and +removed cases. The checker visits both children and rejects reuse, an absent +child or an unused node. A leaf may instead exclude a branch where all 104 +main groups are removed. Induction on this finite tree covers every subset +with at least one retained main group. There are 233 nodes at the near gate +and 221 nodes at the one-percent gate. + +The least negative certified local upper bounds are respectively +`-2481461/10^12` and `-46854465615/10^12`. Therefore every admissible subset +in this relaxed model has a negative complete moment margin at each tested +saving. The conclusion is pointwise and source-bound. + +## 4. Controls and remaining obligations + +The original source has a strictly positive rational lower margin at its +published `.00312476680` claim. It is a positive price control. The certificate +checker rejects a changed saving, repeated branch, false empty-main leaf, +nonnegative leaf bound, negative flow, excessive flow and a Boolean flow value. +All decisions use explicit checks and remain active under Python optimization. + +The optional search uses a flow solver to find allocations and floating-point +scores only to choose branches. Neither the scores nor solver status is trusted +by replay. The exact integer allocation and complete tree are the proof data. + +This proof does not create a new native word, confirm a compiler assumption, +prove a bound for changed input relations, or establish a universal exponent +ceiling. It does not count the absence of a search hit as proof. The two exact +certificates are the evidence for the stated finite restriction model. diff --git a/research/p104-joint-restriction-gate/README.md b/research/p104-joint-restriction-gate/README.md new file mode 100644 index 0000000000..87cf5b7327 --- /dev/null +++ b/research/p104-joint-restriction-gate/README.md @@ -0,0 +1,97 @@ +# Fixed P104 source restrictions fail two exact moment gates + +**Scoped finite obstruction; no new kappa.** For the exact PR5827 word, +no simultaneous coordinate restriction of its main ports and productive +helpers passes either tested moment gate: + +- `kappa = 0.003124767`, just above the source claim `0.00312476680`; +- `kappa = 0.003156014468`, exactly one percent above that source claim. + +This statement permits every subset of 666 groups: 104 main-port pairs and +562 individual helpers, with at least one main port retained. It gives an +optimistic query discount whenever the complete original input support or +output support of that query is removed. The test debits all removed targets +and rebuilds the complete p16/a7 main contribution. It omits new ordinary, +route and precision costs in favor of the candidate. + +The two certificates have 233 and 221 branch nodes. Their integer flow +allocations prove strict negative upper bounds without a solver at replay. +The primary checker recomputes all 3455 query supports with rational arithmetic +from the 25984-event word and checks its forward and transpose endpoints. +It also reconstructs the entire published paid and target invoice. + +| Tested kappa | Priced leaves | Largest local upper bound | +|---|---:|---:| +| 0.003124767 | 116 | -2481461 / 10^12 | +| 0.003156014468 | 110 | -46854465615 / 10^12 | + +The full caller margin is 18 times the local margin in this table. +These are bounds from the certificates, not exact maximizing values. +The original word passes its own lower gate as a positive control. + +## Reproduce + +```sh +python3.12 -B scripts/research_package.py --package research/p104-joint-restriction-gate +``` + +Expected: `PASS_P104_JOINT_RESTRICTION_GATE` in normal and optimized modes. +Only the Python standard library is required. The scientific replay reads +package files only. It needs no Git, network, flow solver or predecessor import. +[PROOF.md](PROOF.md) states the exact model, tariff and dual inequality. +[RESULT.json](RESULT.json) contains the complete expected receipt. + +`discover.py` is optional. It needs PyMaxflow and NetworkX and writes a new +certificate. It is not a proof dependency. The checker only validates positive +integer allocations against source and group capacities and checks coverage +of both children at each branch. Seven semantic corruptions must fail at each +tested saving. Source bytes have independent SHA256 and Git-blob pins. + +## Scope and attribution + +Source: [PR5827](https://github.com/CrocSwap/integer-mult-bounds/pull/5827), +head `05cd36e5af06d7a3790e30ce3f449fa89b853768`. +Canonical main: `de5ec2e7a6074068452f45b1a191b5c72832df4a`, priority 8. +The selected `.00310045` record is unchanged. + +This result closes a fixed-source restriction screen. It does not exclude +changed scalar words, native paths, arbitrary linear quotient inputs, new +helpers or a new caller. The two pointwise moment tests do not prove monotonicity +on an interval or a universal kappa ceiling. Individual zero/dead conditions +need not compose into a legal physical word; the model grants every such +discount at once, so its failure is a favorable necessary-condition test. +No new physical supplier, full native replay, uniform compiler, rounded +multiplier or proof-assistant acceptance is claimed. The five inherited +framework assumptions remain. + +The earlier single-input tests in Discussion #5125 and forty-helper experiment +in Discussion #5645 are prior work. This package adds complete subset coverage +for the declared support model and exact prices. Its source includes Mason +Hale's PR5811 composition, Ali Romman's helper and accumulation work, Joel +Pulikkan's R22, Dugongue's composition proof, flyingviper and all retained +native/controller/compiler/BIT authors. The full PR5827 notice is preserved +in `inputs/PR5827-NOTICE`. New work: Ali Romman with substantial OpenAI Codex +assistance; no subagents. Apache-2.0. All new checks are author-side. + +The later [PR5835 audit](https://github.com/CrocSwap/integer-mult-bounds/pull/5835) +by unpaidmoon corrects the order of two frame ranks in the source proof. +It leaves the paid multiset unchanged. This checker uses the actual word and +frame basis lengths. The vendored source proof is preserved without edits. + +[Canonical coordination](https://github.com/CrocSwap/integer-mult-bounds/discussions/5600#discussioncomment-19209322) +records the scope and earlier local searches. Current open PRs and adjacent +live claims were checked. The complete cached Discussion index was searched. Sparse notes, +arbitrary diffs and unpublished work remain coverage limits. Hosted CI and +independent scientific acceptance are separate from local checks. + +## Open next questions + +- Can a changed query argument permit a paid saving that is absent from the + original zero/dead supports? This changes the model. Check the live #5645 + historical-value claim before choosing a disjoint source and edit. +- Can an independent reviewer check the complete main-port debit and the flow + coverage proof? Start with Sections 2 and 3 of PROOF.md and the solver-free + replay. No physical native replay is needed to check the stated finite model. + +The donor's requested large kappa improvement remains unmet. This negative +result is a research handoff, not completion of that goal. diff --git a/research/p104-joint-restriction-gate/RESULT.json b/research/p104-joint-restriction-gate/RESULT.json new file mode 100644 index 0000000000..ddb3d59e1c --- /dev/null +++ b/research/p104-joint-restriction-gate/RESULT.json @@ -0,0 +1,40 @@ +{ + "groups": 666, + "queries": 3455, + "program_events": 25984, + "source_margin_lower_numerator": 202400, + "tests": [ + { + "nodes": 233, + "priced_leaves": 116, + "largest_upper_numerator": -2481461, + "scale": 1000000000000, + "kappa": "3124767/1000000000", + "controls": [ + "wrong-saving", + "missing-branch", + "wrong-upper", + "negative-flow", + "over-capacity", + "boolean-flow", + "false-empty-main" + ] + }, + { + "nodes": 221, + "priced_leaves": 110, + "largest_upper_numerator": -46854465615, + "scale": 1000000000000, + "kappa": "789003617/250000000000", + "controls": [ + "wrong-saving", + "missing-branch", + "wrong-upper", + "negative-flow", + "over-capacity", + "boolean-flow", + "false-empty-main" + ] + } + ] +} diff --git a/research/p104-joint-restriction-gate/SOURCES.json b/research/p104-joint-restriction-gate/SOURCES.json new file mode 100644 index 0000000000..b7b56c1325 --- /dev/null +++ b/research/p104-joint-restriction-gate/SOURCES.json @@ -0,0 +1,47 @@ +{ + "schema_version": 1, + "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8", + "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/p104-unread-path-resynthesis/WORD.json.gz", + "usage": "provenance", + "pin": "head:05cd36e5af06d7a3790e30ce3f449fa89b853768:research/p104-unread-path-resynthesis/WORD.json.gz", + "git_blob": "6341a49f717bd64ef2a5b7c440bd86d5513425dc", + "sha256": "5d50e5654910c9535e9025de0f644bb2dece2396e799b4a766110363448fd0b0" + }, + { + "path": "research/p104-unread-path-resynthesis/NOTICE", + "usage": "provenance", + "pin": "head:05cd36e5af06d7a3790e30ce3f449fa89b853768:research/p104-unread-path-resynthesis/NOTICE", + "git_blob": "8fc3f76cc0d66f19c9abd7c7111ec69c73c0434d", + "sha256": "fe02063ca48bf070303ac05f613ab1e6e4dd9ee62141f7e7012d855faf7b0c78" + }, + { + "path": "research/p104-unread-path-resynthesis/PROOF.md", + "usage": "provenance", + "pin": "head:05cd36e5af06d7a3790e30ce3f449fa89b853768:research/p104-unread-path-resynthesis/PROOF.md", + "git_blob": "eae2e1b895284155a1485f240a0ad43a4b52c0aa", + "sha256": "16b1ba9b9468b097796d900ac04f9a278e09cba5ec9e08436b6e06ee066b385b" + }, + { + "path": "research/p104-unread-path-resynthesis/RESULT.json", + "usage": "provenance", + "pin": "head:05cd36e5af06d7a3790e30ce3f449fa89b853768:research/p104-unread-path-resynthesis/RESULT.json", + "git_blob": "e2e078df445d6c1b988cf926fed3bc7570a88237", + "sha256": "e437dd9fc7368de705cef8a9d27c6161f1b246f36e320e5c155dde89f88e16e2" + } + ], + "runtime_source_policy": "The scientific replay reads authenticated package inputs only. The exact source head is provenance. No network, Git or predecessor executable is used." +} diff --git a/research/p104-joint-restriction-gate/TASK.json b/research/p104-joint-restriction-gate/TASK.json new file mode 100644 index 0000000000..8408fae159 --- /dev/null +++ b/research/p104-joint-restriction-gate/TASK.json @@ -0,0 +1,101 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 8, + "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a", + "original_card": { + "id": "formal-interface-lemma", + "question": "Can one uncovered interface implication be formalized with exact caller and certificate bindings?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/gate-operand-parity-lean/README.md", + "research/staged544-certified-endpoint/README.md", + "research/unconditional-batched-crt/README.md" + ], + "methods": [ + "Formalize a missing boundary lemma identified by the selected review.", + "Audit a formal theorem-to-certificate binding independently." + ], + "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.", + "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse." + }, + "first_experiment": "Write one missing statement with quantified hypotheses, actual caller and existing coverage. A compact-switch lemma is a candidate only after its mathematical contract is reviewed. Establish a bounded proof plan before a separately budgeted proof-assistant build; do not rerun large Lean jobs as orientation.", + "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.", + "allowed_variations": [ + "Narrow to one formal lemma or one theorem-to-certificate binding." + ], + "scope_change_triggers": [ + "Formalizing already-covered arithmetic and claiming the full multiplication theorem." + ], + "overlap_terms": [ + "hyperplane end", + "formal interface", + "Lean binding", + "3807", + "3857", + "4100", + "gate-operand-parity-lean", + "staged544-certified-endpoint", + "unconditional-batched-crt" + ], + "existing_checks": [ + { + "scope": "PR #3807: scoped gate-operand parity formalization.", + "evidence": "research/gate-operand-parity-lean/README.md", + "remaining": "Exact theorem-to-caller binding and genuinely uncovered interface lemmas.", + "status": "author-checked", + "source_commit": "4c3530f42a6abcc48e7a6bcffd6c901911dc8269", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #3857: certified real-power moment/endpoint arithmetic.", + "evidence": "research/staged544-certified-endpoint/README.md", + "remaining": "Uniform algorithmic implications, not another endpoint digit.", + "status": "author-checked", + "source_commit": "ef4315b8caa605e47a2515004845eb2d2ed71a86", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4100: compact-switch formalization proposed as future validation.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Audit the statement and assumptions before a formal proof campaign.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Prove a source-bound implication from arbitrary coordinate restrictions to two failed complete moment gates on PR5827.", + "scope_change_reason": "The explicit donor task seeks a larger kappa. A complete joint-restriction search gave a compact negative certificate. This package records that side result; the donor goal remains active.", + "bottleneck_link": "It excludes every subset of the declared source groups in a favorable zero/dead-query relaxation, so a new candidate needs a changed argument, word or relation.", + "budget_minutes": 60, + "stop_rule": "Publish the exact finite certificate after source, tariff, dual coverage, control and portable replay checks. Do not count it as a kappa improvement.", + "outcome": "completed", + "evidence": "PROOF.md, CERTIFICATE.json.gz, ONE-PERCENT.json.gz and RESULT.json.", + "author": "Ali Romman with substantial OpenAI Codex assistance", + "ai_assistance": "Substantial OpenAI Codex assistance for discovery, proof, code and author-side verification; no subagents.", + "open_questions": [ + { + "question": "Can a changed query argument permit a paid saving outside the original support model?", + "why_it_matters": "The source restriction model fails both tested gates.", + "first_step": "Check the live Discussion #5645 claim and select a disjoint source edit.", + "blocked_by": "A complete legal word and favorable full invoice are not supplied here." + }, + { + "question": "Can an independent reviewer confirm the main-port debit and complete flow coverage?", + "why_it_matters": "The result is an author-checked finite obstruction.", + "first_step": "Read PROOF.md Sections 2 and 3 and run the solver-free registered replay.", + "blocked_by": "Independent scientific acceptance remains pending." + } + ] +} diff --git a/research/p104-joint-restriction-gate/VALIDATION.md b/research/p104-joint-restriction-gate/VALIDATION.md new file mode 100644 index 0000000000..a958f2ce11 --- /dev/null +++ b/research/p104-joint-restriction-gate/VALIDATION.md @@ -0,0 +1,25 @@ +# Validation scope + +The metadata and source pins passed with Python 3.12.13. Both registered modes +passed the complete rational source replay, reconstructed invoice, exact power +bounds, both dual trees, original-source positive control and seven corrupted +certificate controls per gate. + +``` +/tmp/kappa-step-venv/bin/python -B scripts/research_package.py --package research/p104-joint-restriction-gate --check-only +/tmp/kappa-step-venv/bin/python -B scripts/research_package.py --package research/p104-joint-restriction-gate +``` + +The exact source supports also matched the earlier modulo 65521 discovery +supports at all 3455 queries. The certificate uses the rational supports only. +PyMaxflow supplied discovery allocations. The standard-library checker checked +their capacities directly; no solver result is accepted as proof. + +Committed-byte, official export and sealed replay results are recorded in the +publication body. Hosted CI and independent scientific acceptance are separate. +The source native and physical caller suites, full-history preflight, Lean and +Docker were not run for this fixed scalar-support and price result. The source +head is an explicit provenance pin, not an ancestor of this new-main branch. + +No conditional kappa increase is claimed. The large-improvement donor goal +remains active outside this scoped package. diff --git a/research/p104-joint-restriction-gate/VERIFY.json b/research/p104-joint-restriction-gate/VERIFY.json new file mode 100644 index 0000000000..2f79c65986 --- /dev/null +++ b/research/p104-joint-restriction-gate/VERIFY.json @@ -0,0 +1,28 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact source supports, rational tariffs, both complete dual trees and semantic controls." + }, + { + "argv": [ + "{python}", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The same complete replay with Python assertions disabled." + } + ] +} diff --git a/research/p104-joint-restriction-gate/discover.py b/research/p104-joint-restriction-gate/discover.py new file mode 100644 index 0000000000..1168a711ec --- /dev/null +++ b/research/p104-joint-restriction-gate/discover.py @@ -0,0 +1,87 @@ +"""Build a flow certificate. This search is not a replay dependency. + +Use PyMaxflow and NetworkX. Ali Romman with Codex assistance. Apache-2.0. +""" +from collections import defaultdict +import gzip +import json +import maxflow +import model as M + + +def main(): + import argparse + parser = argparse.ArgumentParser() + parser.add_argument("--one-percent", action="store_true") + args = parser.parse_args() + kappa = M.LARGE_TARGET if args.one_percent else M.KAPPA + word = M.source() + groups, queries = M.supports(word) + costs, rewards, constant = M.invoice(word, groups, queries, kappa) + size, main_mask = len(groups), (1 << 104)-1 + nodes = [] + + def visit(yes, no): + index = len(nodes) + nodes.append(None) + if yes & main_mask == main_mask: + nodes[index] = {"empty_main": True} + return index + terms = M.relaxation(queries, rewards, yes, no) + graph = maxflow.Graph[int](size+len(terms), sum(k.bit_count() for k, _ in terms)) + graph.add_nodes(size+len(terms)) + for j, cost in enumerate(costs): + if not (yes | no) >> j & 1: + graph.add_tedge(j, 0, cost) + for i, (key, reward) in enumerate(terms, size): + graph.add_tedge(i, reward, 0) + for j in M.bits(key): + graph.add_edge(i, j, 10**17, 0) + flow = graph.maxflow() + upper = constant + sum(v for _, v in terms) - flow - sum(costs[j] for j in M.bits(yes)) + if upper < 0: + residual = graph.get_nx_graph() + allocations = [] + for i, (key, _) in enumerate(terms): + for j in M.bits(key): + amount = residual.get_edge_data(j, size+i, {}).get("weight", 0) + if amount: + allocations.append([i, j, int(amount)]) + M.need(sum(a for _, _, a in allocations) == flow, "Exported dual flow") + nodes[index] = {"allocations": allocations, "upper": upper} + return index + selected = yes | sum(1 << j for j in range(size) + if not (yes | no) >> j & 1 and graph.get_segment(j) == 0) + bad = defaultdict(float) + for q, reward in zip(queries, rewards): + a, b = q["input"], q["output"] + if a & no or b & no: + continue + common = (a & b) & ~yes + if common & selected != common or a & selected == a or b & selected == b: + continue + missing = (a | b) & ~selected + for j in M.bits(missing): + bad[j] += reward / missing.bit_count() * (2 if j < 104 else 1) + if bad: + split = max(bad, key=lambda j: (bad[j], costs[j], -j)) + else: + free = main_mask & ~(yes | no) + M.need(bool(free) and not no & main_mask, "Remaining main branch") + split = next(M.bits(free)) + kept = visit(yes, no | (1 << split)) + removed = visit(yes | (1 << split), no) + nodes[index] = {"split": split, "kept": kept, "removed": removed} + return index + + root = visit(0, 0) + certificate = {"schema": 1, "kappa": str(kappa), "scale": M.SCALE, + "groups": len(groups), "queries": len(queries), "root": root, "nodes": nodes} + data = json.dumps(certificate, sort_keys=True, separators=(",", ":")).encode() + filename = "ONE-PERCENT.json.gz" if args.one_percent else "CERTIFICATE.json.gz" + (M.HERE / filename).write_bytes(gzip.compress(data, mtime=0)) + print("CERTIFICATE", len(nodes), "nodes", len(data), "plain bytes") + + +if __name__ == "__main__": + main() diff --git a/research/p104-joint-restriction-gate/inputs/PR5827-NOTICE b/research/p104-joint-restriction-gate/inputs/PR5827-NOTICE new file mode 100644 index 0000000000..8fc3f76cc0 --- /dev/null +++ b/research/p104-joint-restriction-gate/inputs/PR5827-NOTICE @@ -0,0 +1,113 @@ +Unread-register path resynthesis +Copyright 2026 Ali Romman. Apache-2.0. + +New construction, code, calculations and prose: Ali Romman with substantial +OpenAI Codex assistance. No subagents. All new checks are author-side. + +Mason Hale supplied PR5811, the complete two-block composition and the exact +role92 remapping and fourth accumulation. The earlier elementary accumulation, +retained-copy and second-block work is by Ali Romman. Joel Pulikkan supplied +R22. Dugongue supplied the concurrent baseline composition proof. Their source +notice and proof are retained byte for byte under inputs/pr5811-*. + +The source closure retains flyingviper, Cinna Davis, David Arias, Gareth +Davidson, Jacob Alan Sussman, zxv, Cao Yifan, Pierre-Loic Doulcet, thu-nmrc, +Scratch-net and all native/helper/controller/compiler/geometry/analytic +predecessors. The exact PR5786 source archive and its nested notices remain. +This package does not claim any predecessor construction as new. + +Exact PR5811 vendor/accumulated/NOTICE follows. Source head: +33d7760d0a6fea6394aefd014eea68f0af02a92e + +Accumulated native updates +New work: Ali Romman with substantial OpenAI Codex assistance. Apache-2.0. +No subagents. The same assistant made the construction and the author checks. + +Concurrent scope: Discussion5125 now tests retained copies in the transposed +supplier. That route uses the same source/destination duality. This package +claims the three fixed forward-supplier groups and their complete result, +not the elementary accumulation identity or the broader transposed search. + +Exact source: PR5786 at 6b936acd68a7e0f9062037900f0fe9bc4b6fdd25. +The complete predecessor notice follows unchanged. + +Asynchronous helper hubs +New work: Ali Romman with substantial OpenAI Codex assistance. Apache-2.0. + +Retained native copies from PR5774 at 7d6ec0cdef31d0c37b7d2563e709979caa0d5eae. +All prior credit follows unchanged. + +Paid intermediate meetings and collective helper splits. +Ali Romman, with substantial OpenAI Codex assistance. Apache-2.0. +No subagents. All checks are author-side calculations. + +The complete PR5718 notice follows unchanged. + +Four paid interior public-basis changes. +Ali Romman, with substantial OpenAI Codex assistance. Apache-2.0. +No subagents. + +The following exact notice is retained from PR5660. + +New helper-subspace construction, proof and replay: +Ali Romman with substantial OpenAI Codex assistance. Apache-2.0. +The same assistant performed the construction and author-side checks. + +Retained contributions: +flyingviper: PR5605 shared relay, PR5612 delayed relay, and the PR5608/PR5613 +relay/split compositions. +Scratch-net: PR5606 prepared-helper identities and target debit. +Pierre-Loic Doulcet (hexapode): PR5565 commuting-contact construction, used as the exact source. +Ali Romman: PR5602 fixed boundary relations, PR5601 three-contact frame +change, PR5580 contact step, +and PR5544/5545 complete P104 caller. +Joel Pulikkan (GamingPuzzled): PR5569 priced helper handoff. +DreamingOfClouds: PR5561 free helper endpoints and PR5568 search tools. +thu-nmrc: PR5551 contact improvements. +Gareth Davidson (bitplane): PR2305 source composition. +David Arias: PR2152 coalesced P104 word. +Cinna Davis: PR2219 private reuse and the controller lineage. +Jacob Alan Sussman: productive mixed-target recursion. +zxv and Cao Yifan: exact intervals, compiler and native/pricing lineage. +GamingPuzzled: PR5472 successor handoff, a predecessor to the split concept. +The retained source notices preserve earlier geometry, BIT and analytic credit. + +The elementary rank-one basis identity is not claimed as a new general +linear-algebra theorem. The contribution is its explicit independent-target +use on this P104 word and the complete conditional kappa improvement. + +New contribution: Ali Romman, with substantial OpenAI Codex assistance. +The four-gate source-version rewrite composes zxv PR5643 and Ali Romman PR5644. +The A2 method retains Chris R/Clear1nsight PR3998 and ToikY PR4019 credit. +The compensated triangle method retains Cinna Davis PR4692 credit. +No subagents were used for this contribution. Apache-2.0. + +Concurrent PR5650 by zxv publishes the PR5643/PR5644 composition. PR5651 by +Ali Romman corroborates it. This package credits that released composition +and contributes the further four-gate placement. + +New work: distributed scalar updates on an unobserved public field interval, the exact witness and complete conditional price. Prepared for Ali Romman with substantial OpenAI Codex assistance. No subagents. Apache-2.0. The source archive retains all predecessor notices. + +Two-boundary main-assisted helper split and early cleanup: flyingviper with substantial +OpenAI Codex assistance, including independent AI review agents. Apache-2.0. + +Retained native-copy construction +Prepared by Ali Romman with substantial OpenAI Codex assistance. No subagents. +The paid-meeting source is PR5751 by Ali Romman with OpenAI Codex assistance. +The dimension-four span [265,194,164,75] is from Joel Pulikkan / GamingPuzzled +PR5739, with Claude Opus 5.5 assistance. The R22 block edits are not included. +The retained-copy mechanism, exact constructor, source-specific verification, +new price and proof are the contribution of this package. Apache-2.0. + +Exact PR5811 vendor/blocks/NOTICE follows. Source head: +33d7760d0a6fea6394aefd014eea68f0af02a92e + +The second block is PR5796 at4b30391e633ba0c7c674f03586ae97d443e9bc9c, by Ali Romman with substantial OpenAI Codex assistance, following Joel Pulikkan/GamingPuzzled R22. Exact notice, plan, proof and source words are retained in source/SECOND-* unchanged. + +The final immediate source is PR5786 asynchronous helper hubs by Ali Romman with substantial OpenAI Codex assistance. Its three temporal helper splits and complete completion parameters are retained and credited. The earlier PR5774-only composition is a superseded checkpoint, not a separate contribution. + +New complete retained-copy and R22 composition: Ali Romman with substantial OpenAI Codex assistance. No subagents. Apache-2.0. + +The thirteen retained native conversions and changed helper targets are by Ali Romman with OpenAI Codex assistance in PR5774. The R22 block and rank-four basis are by Joel Pulikkan (GamingPuzzled), with Claude Opus5.5 assistance, in PR5739/5756. The complete source archive and R22 notice remain unchanged. + +The construction retains Ali Romman PR5751 paid intermediate meetings, flyingviper PR5718 boundary splits, Cinna Davis's productive controller, Jacob Alan Sussman's productive recursion, zxv and Cao Yifan's interval/compiler line, and every P104/native/BIT predecessor in the source notices. The source engines are reused under exact byte bindings, not claimed as new implementations. diff --git a/research/p104-joint-restriction-gate/inputs/PR5827-PROOF.md b/research/p104-joint-restriction-gate/inputs/PR5827-PROOF.md new file mode 100644 index 0000000000..eae2e1b895 --- /dev/null +++ b/research/p104-joint-restriction-gate/inputs/PR5827-PROOF.md @@ -0,0 +1,152 @@ +# One direct query for an unread register + +The exact source is PR5811 at +`33d7760d0a6fea6394aefd014eea68f0af02a92e`. This package changes one +seven-event interval. It retains every public input, target and boundary, +and every owned event. The complete conditional claim is kappa 0.00312476680. +The five inherited assumptions remain. + +## Four-field identity and physical frames + +Let a, b, c and d be the entry values of roles 695, 733, 773 and 709. +These four values are arbitrary, including c in the owned field. Let A be +frame 3, C be frame 597, and B be frame 1031. The exact source has +A strictly inside C strictly inside B, at dimensions 0, 4 and 5. + +The source interval starts at event 13815. It performs: + +```text +MOVE c: B -> C +ADD d += c in C +MOVE b: A -> C +ADD b += c in C +MOVE a: A -> C +ADD a += b in C +MOVE a: C -> B +``` + +The replacement performs: + +```text +ADD a += b in A +MOVE a: A -> B +ADD a += c in B +MOVE c: B -> C +ADD d += c in C +MOVE b: A -> C +ADD b += c in C +``` + +Both words leave the decoded values +`a'=a+b+c`, `b'=b+c`, `c'=c` and `d'=d+c` in the same exit frames. +The first new ADD reads b before its update. The second reads c before +its reverse native query. No outside event occurs inside this interval. +Thus the replacement preserves every later source observation, including +all 23 COPY payloads. The constructor also compares the entire owned-event +subsequence byte for byte. + +The constructor checks the exact interval and its unique location. A +separate four-by-four rational transfer calculation compares all entry +coefficients. The full forward replay checks all 799 input coordinates, +including owned input columns. A dense integer transpose interpreter checks +the same endpoint in reverse order with binary denominators. Each interpreter +checks 638401 coefficients. All arbitrary public helper inputs are retained. + +## Native and ordinary costs + +The two public queries A to C and C to B have ranks 4 and 1. Their +replacement A to B has rank 5. Every native map must implement the actual +frame change, including its absolute phase. Exact Clifford lowering and a +separate native interpreter check all 2918 distinct maps. The checks also +cover 208 main adapters and 1124 helper normalizers. + +Write H_r(t)=r^t. The exact local changes are + +```text +Delta paid = -H1-H4+H5 +Delta targets = 0 +``` + +The signed gain is H1+H4-H5. It is positive for every 0 2^26*N^5 avoiding all fixed denominators and rank witnesses" + }, + "outer": { + "functional_checks": { + "actual_new_BIT_stock_sublinear": "348599999999253/350000000000000", + "fixed_halo_explicit_metadata_branch": "26950000000001/350000000000", + "new_BIT_row_stock_sublinear_in_active_group": "1395799999997009/1400000000000000", + "new_semantic_group_guard": "3/1400000000000" + }, + "margins": { + "boundary_algebraic_matrix": "6124542933595625326477/1960000000000000000000000", + "fused_gaussian": "6124542933586875979431/1960000000000000000000000", + "global_coordinate_router": "1093668381/350000000000", + "group_bit_router": "1531135733746718994857/490000000000000000000000", + "group_scans": "699999999999/700000000000", + "main_transform": "6124542932195625326477/1960000000000000000000000", + "microbox_face_corrections": "26950000000001/350000000000", + "polynomial_products": "1399999999999/1400000000000", + "sparse_union_movement": "802374542933595625326477/1960000000000000000000000" + }, + "parameters": { + "a": "1093668381/350000000000", + "b": "174986941/56000000000", + "beta": "1399999999997/1400000000000", + "bit_saving": "17/5000", + "cap_xi": "1782374542932195625326477/1960000000000000000000000", + "complex_uniform_saving": "2187336763/700000000000", + "d": "1/1400000000000", + "epsilon": "1399999999999/1400000000000", + "kappa": "7811917/2500000000", + "lambda_": "398750093279/400000000000", + "lambda_prime": "1395625326477/1400000000000", + "layout": "1/1400000000000", + "q": "4374673523/1400000000000", + "r0": "1/14000000000000", + "stop": "1/1400000000000", + "tested_saving": "624953361/200000000000" + }, + "strict_checks": { + "actual_bit_above_effective": "96331619/350000000000", + "actual_logarithmic_gamma_guard": "1/1400000000000", + "actual_logarithmic_group_guard": "177625457069904374673523/980000000000000000000000", + "alpha_logarithm_absorption": "1/14000000000000", + "boundary_algebraic_matrix_above_kappa": "5595625326477/1960000000000000000000000", + "cap_above_band": "802374542932195625326477/1960000000000000000000000", + "cap_below_cell": "177625457066404374673523/1960000000000000000000000", + "cap_below_phase_cell_power": "2137625457067804374673523/1960000000000000000000000", + "complex_above_effective": "1/1400000000000", + "complex_below_one_over_32": "1575013059/56000000000", + "complex_endpoint": "1/700000000000", + "epsilon_below_one": "1/1400000000000", + "epsilon_positive": "1399999999999/1400000000000", + "fine_prime_halo_umbrella": "7/2", + "fused_gaussian_above_kappa": "5586875979431/1960000000000000000000000", + "gaussian_above_main": "695625326477/980000000000000000000000", + "global_coordinate_router_above_kappa": "1/350000000000", + "global_gamma_power_slack": "9/14000000000000", + "group_below_dimension": "1/700000000000", + "group_bit_router_above_kappa": "1746718994857/490000000000000000000000", + "group_gauge_power_slack": "177625457069834374673523/980000000000000000000000", + "group_key_fits_record": "1/700000000000", + "group_positive": "1399999999997/1400000000000", + "group_scans_above_kappa": "697812663239/700000000000", + "halo_covers_generic_inverse_radius": "5", + "improvement_over_user_baseline": "696898190400418148631/500000000000000000000000", + "lambda_above_internal": "1/2800000000000", + "lambda_above_sigma": "3/2800000000000", + "lambda_above_tau": "1/2800000000000", + "lambda_prime_above_lambda": "1/2800000000000", + "lambda_prime_above_leaf": "111825013059/78400000000000000000000", + "leaf_saving_above_effective": "55825013059/78400000000000000000000", + "main_transform_above_kappa": "4195625326477/1960000000000000000000000", + "membership_arithmetic_fits_record": "1/1400000000000", + "microbox_face_corrections_above_kappa": "26948906331621/350000000000", + "microbox_halo_volume": "110600000000003/1400000000000", + "new_complex_uniform_saving_above_b": "1/1400000000000", + "new_semantic_guard_with_C1_one": "1/1400000000000", + "polynomial_products_above_kappa": "1395625326479/1400000000000", + "positive_layout_slack": "1/1400000000000", + "q_below_effective": "1/1400000000000", + "q_below_internal": "1/1400000000000", + "q_below_leaf": "111825013059/78400000000000000000000", + "q_positive": "4374673523/1400000000000", + "short_record_fallback": "55825013059/56000000000", + "source_axis_superpolynomial": "1/1400000000000", + "sparse_union_movement_above_kappa": "796250000005595625326477/1960000000000000000000000", + "stop_below_one": "1399999999999/1400000000000", + "stop_positive": "1/1400000000000", + "strassen_integer_power_gap": "1951441519231", + "support_router_span": "3/1400000000000", + "theta_positive_polynomial_power": "2", + "union_header_fits_record": "3/1400000000000", + "union_tag_work_per_visit_fits_record": "3/1400000000000" + } + }, + "paid": { + "1": 41610, + "16": 416, + "2": 8208, + "24": 416, + "3": 8964, + "32": 416, + "4": 1764, + "40": 416, + "48": 416, + "5": 2934, + "56": 416, + "6": 162, + "64": 416, + "7": 108, + "72": 208 + }, + "paid_calls": 66870, + "previous_pr5811": "39052329133/12500000000000", + "productive_fields": 13444, + "query_shears": 15, + "rank_mass_surplus": 760, + "raw_ceiling": { + "derivative_upper": "-367933136390632154472669927947898325700600889223675898395208059/1569275433846670190958947355801916604025588861116008628224", + "interval": [ + "0", + "17/5000" + ] + }, + "raw_headroom": [ + "1507/100000000000000", + "377/25000000000000" + ], + "raw_root_interval": [ + "312476681507/100000000000000", + "78119170377/25000000000000" + ], + "relative_gain_percent": "725586700/39052329133", + "strictification": { + "alpha": { + "lower": "0.999999999989768874284444177647", + "upper": "0.999999999989768874284444177648" + }, + "cutoff": 16, + "delta": { + "lower": "0.951913152001029451974474596213", + "upper": "0.951913152001029451974474596214" + }, + "floor": 17, + "gamma": { + "lower": "0.975606802226899703414382904960", + "upper": "0.975606802226899703414382904961" + }, + "normalized_paid_upper": "1048576000976562501/1048576001073741824", + "power": 1024, + "reserve": "1/1000000000000", + "tail_block": 128, + "tail_decay": "125/128", + "tail_offset": "1/7", + "tested": "624953361/200000000000" + }, + "targets": { + "1": 324, + "145": 208, + "17": 416, + "2": 126, + "25": 416, + "3": 72, + "33": 416, + "4": 1926, + "41": 416, + "49": 416, + "5": 252, + "57": 416, + "65": 416, + "7": 162, + "73": 208, + "8": 324, + "9": 6930 + }, + "whole_idle_jobs": 3120 + }, + "controls": { + "changed_source_interval": "One exact source interval", + "damaged_source_NOTICE": "Exact source SHA256: research/p104-accumulated-block-composition/NOTICE", + "damaged_source_PROOF.md": "Exact source SHA256: research/p104-accumulated-block-composition/PROOF.md", + "damaged_source_RESULT.json": "Exact source SHA256: research/p104-accumulated-block-composition/RESULT.json", + "damaged_source_WORD.json.gz": "Exact source SHA256: research/p104-accumulated-block-composition/WORD.json.gz", + "extra_target_credit": "Every productive helper has a native target", + "late_use_of_old_value": "Scalar destination and coefficient", + "missing_central_translation": "Rejected by the complete Laurent endpoint", + "missing_direct_query": "Scalar destination and coefficient", + "missing_early_observation": "All public and owned rows", + "unpaid_query": "Complete field and call counts", + "wrong_late_sign": "All public and owned rows" + }, + "limits": [ + "All five inherited framework assumptions remain.", + "This is a small gain and does not meet the donor large-improvement target.", + "The large uniform word and rounded multiplier are not materialized.", + "Author checks do not establish independent acceptance.", + "The selected frontier is unchanged." + ], + "local": { + "endpoint_coefficients": 638401, + "helpers": { + "1": 18, + "2": 7, + "3": 4, + "4": 107, + "5": 14, + "7": 9, + "8": 18, + "9": 385 + }, + "owned_fields": 29, + "owned_lifetimes": 31, + "paid": { + "1": 2225, + "2": 456, + "3": 498, + "4": 98, + "5": 163, + "6": 9, + "7": 6 + }, + "paid_rank_mass": 5934, + "peak_owned_fields": 13, + "public_inputs": 770, + "real_scalar_allowance": 225046 + }, + "native": { + "distinct_maps": 2918, + "helper_normalizers": 1124, + "helpers": { + "1": 18, + "2": 7, + "3": 4, + "4": 107, + "5": 14, + "7": 9, + "8": 18, + "9": 385 + }, + "main_adapters": 208, + "proof": "Every signed Pauli image and exact global phase; frame induction at every positive tensor width", + "recipe_payload_sha256": "fdaf779e9bf6affff9a356b0182f7971b2bddb41b2dc8f40cdbfbccb7735e803", + "wrong_phase_rejected": true + }, + "paid_delta": { + "1": -1, + "4": -1, + "5": 1 + }, + "physical_caller": { + "central_square_columns": 53248, + "full_calls": 18, + "main_targets": { + "145": 208, + "17": 416, + "25": 416, + "33": 416, + "41": 416, + "49": 416, + "57": 416, + "65": 416, + "73": 208 + }, + "new_paid_jobs": 0, + "physical_contacts": 7488, + "ports": 104, + "route_payload_sha256": "7f4f0ca768ffbc4f93dcff575592c4c67411f46b4289e45b73f715a2ad47b142", + "tensor_rule": "Factorwise native maps; scalar signs stay outside the tensor power.", + "whole_idle_jobs": { + "16": 416, + "24": 416, + "32": 416, + "40": 416, + "48": 416, + "56": 416, + "64": 416, + "72": 208 + }, + "wrapper_sites": [ + 1, + 3, + 5, + 7, + 9, + 11, + 13, + 15, + 17, + 19, + 21, + 23, + 25, + 27, + 29, + 31 + ] + }, + "separate_columns": { + "arithmetic": "Dense integer rows with binary denominators; reverse chronology", + "coefficients": 638401, + "columns": 799 + }, + "source_commit": "33d7760d0a6fea6394aefd014eea68f0af02a92e", + "source_local": { + "endpoint_coefficients": 638401, + "helpers": { + "1": 18, + "2": 7, + "3": 4, + "4": 107, + "5": 14, + "7": 9, + "8": 18, + "9": 385 + }, + "owned_fields": 29, + "owned_lifetimes": 31, + "paid": { + "1": 2226, + "2": 456, + "3": 498, + "4": 99, + "5": 162, + "6": 9, + "7": 6 + }, + "paid_rank_mass": 5934, + "peak_owned_fields": 13, + "public_inputs": 770, + "real_scalar_allowance": 225038 + }, + "source_margin_upper_at_new_claim": "-440220558061576121529811506669002615477042299180450565263/3138550867693340381917894711603833208051177722232017256448", + "status": "PASS_P104_UNREAD_PATH_KAPPA_00312476680", + "target_delta": {} +} diff --git a/research/p104-joint-restriction-gate/inputs/WORD.json.gz b/research/p104-joint-restriction-gate/inputs/WORD.json.gz new file mode 100644 index 0000000000..6341a49f71 Binary files /dev/null and b/research/p104-joint-restriction-gate/inputs/WORD.json.gz differ diff --git a/research/p104-joint-restriction-gate/model.py b/research/p104-joint-restriction-gate/model.py new file mode 100644 index 0000000000..a93b0f90fc --- /dev/null +++ b/research/p104-joint-restriction-gate/model.py @@ -0,0 +1,197 @@ +"""Exact source supports and a fixed restriction price. + +Source: PR5827 and its retained P104 authors. +New work: Ali Romman with substantial OpenAI Codex assistance. Apache-2.0. +""" +from collections import Counter +from fractions import Fraction as Q +from hashlib import sha1, sha256 +from pathlib import Path +import gzip +import json + +HERE = Path(__file__).resolve().parent +KAPPA = Q(".003124767") +LARGE_TARGET = Q(".00312476680") * Q(101, 100) +SCALE = 10**12 + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def bits(mask): + while mask: + low = mask & -mask + yield low.bit_length() - 1 + mask ^= low + + +def source(): + pins = json.loads((HERE / "INPUTS.json").read_text()) + for name, pin in pins["files"].items(): + data = (HERE / "inputs" / name).read_bytes() + need(sha256(data).hexdigest() == pin["sha256"], "Source digest") + blob = b"blob " + str(len(data)).encode() + b"\0" + data + need(sha1(blob).hexdigest() == pin["git_blob"], "Source Git blob") + return json.loads(gzip.decompress((HERE / "inputs/WORD.json.gz").read_bytes())) + + +def supports(word): + public = word["public"] + size = public + word["owned_fields"] + ports = set(word["live"]) + main = ports | {r + 112 for r in ports} + groups = [[r, r + 112] for r in sorted(ports)] + groups += [[r] for r in range(public) if r not in main] + owner = {r: i for i, group in enumerate(groups) for r in group} + dims = list(map(len, word["frames"])) + coefficients = {e[-2]: Q(e[-2]) for e in word["program"] + if e[0] in ("ADD", "COPY", "SCALE")} + + def add(dst, src, scale): + for j, value in src.items(): + value = dst.get(j, Q(0)) + scale * value + if value: + dst[j] = value + else: + dst.pop(j, None) + + def apply(rows, event, reverse): + op, r = event[:2] + if op == "MOVE": + return + if op in ("INIT", "CLEAR"): + rows[r] = {} + elif op == "SCALE": + rows[r] = {j: coefficients[event[-2]] * v + for j, v in rows[r].items()} + elif reverse: + need(op in ("ADD", "COPY"), "Scalar opcode") + add(rows[event[2]], rows[r], coefficients[event[-2]]) + if op == "COPY": + rows[r] = {} + else: + need(op in ("ADD", "COPY"), "Scalar opcode") + if op == "COPY": + rows[r] = {} + add(rows[r], rows[event[2]], coefficients[event[-2]]) + + def mask(row): + return sum(1 << j for j in {owner[r] for r in row}) + + rows = [{r: Q(1)} for r in range(size)] + queries = {} + for i, e in enumerate(word["program"]): + if e[0] == "MOVE": + queries[i] = {"event": i, "role": e[1], + "rank": abs(dims[e[3]] - dims[e[2]]), + "input": mask(rows[e[1]])} + apply(rows, e, False) + for r, row in enumerate(rows): + expected = {r: Q(1)} if r < public else {} + if r - 112 in ports: + expected[r - 112] = Q(1) + need(row == expected, "Complete forward endpoint") + rows = [{r: Q(1)} if r < public else {} for r in range(size)] + for i in range(len(word["program"]) - 1, -1, -1): + e = word["program"][i] + if e[0] == "MOVE": + queries[i]["output"] = mask(rows[e[1]]) + apply(rows, e, True) + for r, row in enumerate(rows): + expected = {r: Q(1)} if r < public else {} + if r in ports: + expected[r + 112] = Q(1) + need(row == expected, "Complete transpose endpoint") + need(len(groups) == 666 and len(ports) == 104, "Source group census") + need(len(queries) == 3455, "Source query census") + return groups, list(queries.values()) + + +def log_bounds(value): + exponent = value.bit_length() - 1 + + def series(z): + power, total = z, Q(0) + for j in range(32): + total += 2 * power / (2*j + 1) + power *= z*z + return total, total + 2*power / (65*(1-z*z)) + + a, b = series(Q(1, 3)) + u = Q(value, 2**exponent) + c, d = series((u-1)/(u+1)) + return exponent*a+c, exponent*b+d + + +def power_bounds(rank, kappa=KAPPA): + if rank == 1: + return Q(1), Q(1) + lower, upper = log_bounds(rank) + + def partial(x, degree): + need(0 <= x < 1, "Alternating exponential domain") + term = total = Q(1) + for j in range(1, degree+1): + term *= -x/j + total += term + return total + + return rank*partial(kappa*upper, 13), rank*partial(kappa*lower, 14) + + +def invoice(word, groups, queries, kappa=KAPPA): + dims = list(map(len, word["frames"])) + local_paid = Counter(q["rank"] for q in queries) + local_targets = Counter(dims[word["final"][g[0]]] - dims[word["initial"][g[0]]] + for g in groups if len(g) == 1) + source_result = json.loads((HERE / "inputs/PR5827-RESULT.json").read_text()) + need(local_paid == Counter({int(k): v for k, v in source_result["local"]["paid"].items()}), + "Source local paid invoice") + need(local_targets == Counter({int(k): v for k, v in source_result["local"]["helpers"].items()}), + "Source local target invoice") + paid = Counter({r: 18*n for r, n in local_paid.items()}) + targets = Counter({r: 18*n for r, n in local_targets.items()}) + paid[1] += 15*104 + targets[145] += 2*104 + for length in (7, 8): + for j in range(1, length+1): + paid[8*(j+1)] += 2*104 + targets[1+8*(j+1)] += 2*104 + for key, actual in (("paid", paid), ("targets", targets)): + expected = Counter({int(k): v for k, v in source_result["complete_cost"][key].items()}) + need(actual == expected, "Complete source " + key) + ranks = set(range(1, 10)) | {145} + ranks |= {8*(j+1)+s for length in (7, 8) + for j in range(1, length+1) for s in (0, 1)} + powers = {r: power_bounds(r, kappa) for r in ranks} + main = (2*powers[145][1] + 2*sum( + powers[1+8*(j+1)][1] - powers[8*(j+1)][0] + for length in (7, 8) for j in range(1, length+1)) - 15) / 18 + + def ceil(q): + return -((-q.numerator)//q.denominator) + + costs = [] + for group in groups: + rank = dims[word["final"][group[0]]] - dims[word["initial"][group[0]]] + value = main if len(group) == 2 else powers[rank][1] + costs.append(ceil(SCALE*value)) + rewards = [(SCALE*powers[q["rank"]][0]).numerator // + (SCALE*powers[q["rank"]][0]).denominator for q in queries] + need(all(x > 0 for x in costs + rewards), "Positive tariff") + return costs, rewards, sum(costs)-sum(rewards) + + +def relaxation(queries, rewards, yes, no): + terms = Counter() + for q, reward in zip(queries, rewards): + a, b = q["input"], q["output"] + left, right = not a & no, not b & no + if not left and not right: + continue + required = (a & b) if left and right else (a if left else b) + terms[required & ~yes] += reward + return [(key, terms[key]) for key in sorted(terms)] diff --git a/research/p104-joint-restriction-gate/verify.py b/research/p104-joint-restriction-gate/verify.py new file mode 100644 index 0000000000..82166d2ae7 --- /dev/null +++ b/research/p104-joint-restriction-gate/verify.py @@ -0,0 +1,123 @@ +"""Check the exact source, rational tariff and integer dual certificate. + +This checker does not import a flow solver. Apache-2.0. +Ali Romman with substantial OpenAI Codex assistance. +""" +from collections import Counter +from copy import deepcopy +import gzip +import json +import model as M + + +def integer(value): + M.need(type(value) is int, "Strict integer") + return value + + +def check(certificate, groups, queries, costs, rewards, constant, kappa=M.KAPPA): + M.need(integer(certificate["schema"]) == 1, "Certificate schema") + M.need(certificate["kappa"] == str(kappa), "Exact tested saving") + M.need(integer(certificate["scale"]) == M.SCALE, "Tariff scale") + M.need(integer(certificate["groups"]) == len(groups), "Group count") + M.need(integer(certificate["queries"]) == len(queries), "Query count") + nodes, seen, uppers = certificate["nodes"], set(), [] + main_mask = (1 << 104)-1 + + def visit(index, yes, no): + index = integer(index) + M.need(0 <= index < len(nodes) and index not in seen, "Complete tree") + seen.add(index) + node = nodes[index] + if "split" in node: + M.need(set(node) == {"split", "kept", "removed"}, "Branch fields") + split = integer(node["split"]) + M.need(0 <= split < len(groups) and not (yes | no) >> split & 1, + "Fresh branch variable") + visit(node["kept"], yes, no | (1 << split)) + visit(node["removed"], yes | (1 << split), no) + return + if "empty_main" in node: + M.need(node == {"empty_main": True} and yes & main_mask == main_mask, + "Empty-main exclusion") + return + M.need(set(node) == {"allocations", "upper"}, "Leaf fields") + terms = M.relaxation(queries, rewards, yes, no) + sent, received, edges = Counter(), Counter(), set() + for row in node["allocations"]: + M.need(type(row) is list and len(row) == 3, "Flow row") + i, j, amount = map(integer, row) + M.need(0 <= i < len(terms) and 0 <= j < len(groups), "Flow index") + M.need(amount > 0 and (i, j) not in edges, "Unique positive allocation") + edges.add((i, j)) + M.need(terms[i][0] >> j & 1 and not (yes | no) >> j & 1, + "Required free group") + sent[i] += amount + received[j] += amount + M.need(all(amount <= terms[i][1] for i, amount in sent.items()), "Source capacity") + M.need(all(amount <= costs[j] for j, amount in received.items()), "Group capacity") + upper = constant + sum(v for _, v in terms) - sum(sent.values()) + upper -= sum(costs[j] for j in M.bits(yes)) + M.need(upper == integer(node["upper"]) and upper < 0, "Strict negative upper bound") + uppers.append(upper) + + visit(certificate["root"], 0, 0) + M.need(seen == set(range(len(nodes))), "No unused proof nodes") + return {"nodes": len(nodes), "priced_leaves": len(uppers), + "largest_upper_numerator": max(uppers), "scale": M.SCALE} + + +def controls(certificate, data): + cases = [] + def edit(label, change): + mutant = deepcopy(certificate) + change(mutant) + cases.append((label, mutant)) + leaf = next(i for i, node in enumerate(certificate["nodes"]) if "allocations" in node) + edit("wrong-saving", lambda c: c.update(kappa=".0034")) + edit("missing-branch", lambda c: c["nodes"][0].update(removed=c["nodes"][0]["kept"])) + edit("wrong-upper", lambda c: c["nodes"][leaf].update(upper=0)) + edit("negative-flow", lambda c: c["nodes"][leaf]["allocations"][0].__setitem__(2, -1)) + edit("over-capacity", lambda c: c["nodes"][leaf]["allocations"][0].__setitem__(2, 10**30)) + edit("boolean-flow", lambda c: c["nodes"][leaf]["allocations"][0].__setitem__(2, True)) + edit("false-empty-main", lambda c: c["nodes"].__setitem__(leaf, {"empty_main": True})) + for label, mutant in cases: + try: + check(mutant, *data) + except ValueError: + continue + raise ValueError("Control accepted: " + label) + return [label for label, _ in cases] + + +def main(): + word = M.source() + groups, queries = M.supports(word) + source_cost = json.loads((M.HERE / "inputs/PR5827-RESULT.json").read_text())["complete_cost"] + signed = Counter({int(k): v for k, v in source_cost["targets"].items()}) + signed.subtract({int(k): v for k, v in source_cost["paid"].items()}) + from fractions import Fraction + lower = sum(n*M.power_bounds(r, Fraction(".00312476680"))[0 if n > 0 else 1] + for r, n in signed.items() if n) / 18 + M.need(lower > 0, "Published source passes its own moment gate") + tests = [] + for filename, kappa in (("CERTIFICATE.json.gz", M.KAPPA), + ("ONE-PERCENT.json.gz", M.LARGE_TARGET)): + costs, rewards, constant = M.invoice(word, groups, queries, kappa) + certificate = json.loads(gzip.decompress((M.HERE / filename).read_bytes())) + data = (groups, queries, costs, rewards, constant, kappa) + test = check(certificate, *data) + test.update(kappa=str(kappa), controls=controls(certificate, data)) + tests.append(test) + result = {"groups": len(groups), "queries": len(queries), + "program_events": len(word["program"]), + "source_margin_lower_numerator": (M.SCALE*lower).numerator // (M.SCALE*lower).denominator, + "tests": tests} + expected = json.loads((M.HERE / "RESULT.json").read_text()) + M.need(result == expected, "Complete expected receipt") + print(json.dumps(result, sort_keys=True)) + print("PASS_P104_JOINT_RESTRICTION_GATE") + + +if __name__ == "__main__": + main()