diff --git a/research/dyadic-query-pair/CERTIFICATE.json b/research/dyadic-query-pair/CERTIFICATE.json new file mode 100644 index 0000000000..d201254cdd --- /dev/null +++ b/research/dyadic-query-pair/CERTIFICATE.json @@ -0,0 +1,258 @@ +{ + "assignment_seed": 54, + "base_commit": "7ee02b7c96d85f22b38d28bd7ed49bb8c1aeb261", + "finite_arrays": { + "endpoint_stream_encoding": "canonical-json-lines-v1", + "endpoint_stream_sha256": "3aba23a40a8d2ec3035a8f3b08dd7b57f32946329d4d1a1973c1b6f66d29b7e8", + "full_address_query_cases": 154160, + "full_dirty_basis_columns_per_program": 154160, + "full_domains": [ + { + "fixed_addresses": 243, + "j_sign_parameters": [ + [ + 0, + -1 + ], + [ + 0, + 1 + ], + [ + 1, + -1 + ], + [ + 1, + 1 + ], + [ + 2, + -1 + ], + [ + 2, + 1 + ], + [ + 5, + -1 + ], + [ + 5, + 1 + ], + [ + 54, + -1 + ], + [ + 54, + 1 + ] + ], + "modulus": 3, + "six_field_addresses": 729, + "two_spectator_values": [ + 1, + 2 + ] + }, + { + "fixed_addresses": 3125, + "j_sign_parameters": [ + [ + 0, + 1 + ], + [ + 54, + 1 + ] + ], + "modulus": 5, + "six_field_addresses": 15625, + "two_spectator_values": [ + 1, + 2 + ] + } + ], + "full_inverse_and_involution_columns": 308320, + "full_parameter_cases": 12, + "orbit_address_query_cases": 7552, + "orbit_dirty_basis_columns_per_program": 7552, + "orbit_inverse_and_involution_columns": 15104, + "orbit_modulus_scale_lengths": [ + [ + 5, + 1, + 5 + ], + [ + 25, + 1, + 25 + ], + [ + 25, + 5, + 5 + ], + [ + 49, + 1, + 49 + ], + [ + 49, + 7, + 7 + ], + [ + 121, + 1, + 121 + ], + [ + 121, + 11, + 11 + ], + [ + 27, + 3, + 9 + ], + [ + 9, + 3, + 3 + ], + [ + 11, + 0, + 1 + ] + ], + "orbit_parameter_cases": 80, + "simultaneously_dirty_cases": 92 + }, + "fixture": { + "a": 18014398509481984, + "baseline_invoice": { + "aligned_xor_scans": 4, + "child_volume_fraction_each": "1/3", + "child_width_fraction_each": "1/3", + "ordered_affine_events": 24, + "ordinary_children": 4, + "persistent_private_rows": 0, + "query_powers": [ + -18014398509481984, + 18014398509481984, + 18014398509481984, + -18014398509481984 + ] + }, + "claimed_scope": "three-query minimum in the specified power-query/XOR model", + "fused_invoice": { + "aligned_xor_scans": 2, + "child_volume_fraction_each": "1/3", + "child_width_fraction_each": "1/3", + "ordered_affine_events": 18, + "ordinary_children": 3, + "persistent_private_rows": 0, + "query_powers": [ + -18014398509481984, + 36028797018963968, + -18014398509481984 + ] + }, + "j": 54, + "private_rows_added": 0 + }, + "format": "dyadic-native-query-pair-certificate-v1", + "implementation_and_proof_sha256": { + "PROOF.md": "9a5ce93b866371189c797fbe8837c6a0bd22c5cf71ed84d60b9ae1c22a5ec83a", + "full_domain.py": "bba8b5548ee44bbb95f56a0e27f3a05083bd24d9eceba7058a17660e4667a8c8", + "program.py": "9398e9f0f1cfe53e8e586f2f63920c0342df54bc47f7f1156cc977f54ba0e11c", + "verify.py": "d0439e64073248c2cb37f176409456053199ee252d1b39f89f7ed588aaf8f427" + }, + "laurent": { + "balanced_exponent_domain": [ + -4, + -2, + -1, + 1, + 2, + 4 + ], + "centered_survivors": 0, + "complete_binary_projector_catalogues": [ + [ + 2, + 6 + ], + [ + 3, + 28 + ], + [ + 4, + 120 + ] + ], + "scope": "finite corroboration; all-d and all-exponent exclusion is the written proof", + "signed_symbolic_program_pairs": 110, + "two_query_products_checked": 91320 + }, + "lowerings": { + "dyadic_indices": [ + 0, + 55 + ], + "modular_columns_including_inverses": 16128, + "odd_moduli": [ + 3, + 9, + 27, + 5, + 25, + 7, + 49, + 11, + 121 + ], + "rational_columns_including_inverses_and_spectators": 1792, + "signed_query_words": 112 + }, + "negative_controls": [ + "omit_fused_event_0", + "omit_fused_event_1", + "omit_fused_event_2", + "omit_fused_event_3", + "omit_fused_event_4", + "central_power_not_doubled", + "first_query_wrong_sign", + "query_mutates_DATA_source", + "wrong_XOR_source_role", + "omit_ADDRESS_event_0", + "omit_ADDRESS_event_1", + "omit_ADDRESS_event_2", + "omit_ADDRESS_event_3", + "omit_ADDRESS_event_4", + "omit_ADDRESS_event_5", + "omit_ADDRESS_event_6", + "query_push_direction_reversed", + "first_difference_has_two_queries", + "even_orbit_centered_endpoint_vanishes", + "non_dyadic_universal_lowering_rejected", + "even_residue_modulus_rejected", + "aliased_source_and_target_rejected", + "discarded_dirty_spectator_fails_restoration", + "boolean_parameter_rejected_23", + "boolean_parameter_rejected_24" + ], + "new_kappa_claimed": false, + "source_manifest_canonical_sha256": "da98d871ca8e9c5cf1c90afa63b9d4551bb50e982a22f7ce8328195405d28343" +} diff --git a/research/dyadic-query-pair/CLAIM.md b/research/dyadic-query-pair/CLAIM.md new file mode 100644 index 0000000000..9a9cc44faa --- /dev/null +++ b/research/dyadic-query-pair/CLAIM.md @@ -0,0 +1,108 @@ +# Seed 54: fuse two completed native BIT shears + +Claim recorded 2026-10-13 at 06:20 UTC (01:20 America/Chicago). +OS randomness (`secrets.randbelow(100)`) returned **54**: recursive interfaces. +Exact fresh `origin/main` base: `7ee02b7c96d85f22b38d28bd7ed49bb8c1aeb261`. +Primary checkout observed at PR756 head `4fad623a1e4ca06959f4326e221c2f8d9125c269`; +it and PR805's branch/worktree are reserved for their existing workers. +This work uses the isolated managed `seed54-boundary-interface` worktree. + +## Selection and hypothesis + +Three narrow candidates were considered: a shared-output dirty echo, a new +Gaussian boundary batch interface, and fusion of two completed native BIT +address shears. PR714/730/744/758/784/788 already cover many echo/checkpoint +classes; PR481 already prices the Gaussian batching mechanism. The third +candidate has a different object and permission contract and is selected. + +PR521 supplies a one-child native unipotent query `h`. PR677 completes the +DATA shear `S_h: x ^= (h+I)y` with two queries on the target and no private +row. Investigate the completed pair `S_(h^a) S_(h^-a)` for `a=2^j`, using +the explicit six-affine/one-child lowering of `h^k` at dyadic `k`. Hypothesis: +`h^-a; XOR_y; h^(2a); XOR_y; h^-a` replaces four children by three and four +XOR scans by two, restoring every input except the prescribed target. + +Method: derive the literal lowering over the rationals and every odd residue +ring; prove the endpoint over F2-valued full arrays; check full small ADDRESS +domains by a separate coordinate/permutation implementation; prove a +three-query lower bound in an explicitly scoped query/XOR model. Seed 54 +selects the large fixed coefficient fixture `a=2^54`. Coverage includes +`j=0..54`, both signs, full-order/shorter/fixed orbits and dyadic modular +specializations. No randomized search or stronger-bound search is planned. + +Price the optimistic complete typed recurrence before implementation: +three ordinary ADDRESS children, each on full BIT volume `V/3` and width +`N/3`, eighteen ordered affine scans, two aligned XOR scans, coefficient +preparation, primitive work, source access, routing and all head returns. +Compare against the completed four-child pair, including its twenty-four +affine scans and four XORs. No clean/disposable/borrowed full private row. +Primitive and child workspace remain paid. Growing `j` is not free. + +Expected deliverable: scoped recursive-interface construction and written +query bound, standalone exact checker/certificate, full cost/storage limits, +source pins, negative controls and one focused PR; **no new kappa**. +Expected finish: by 07:15 UTC (02:15 America/Chicago). Reserve at least the +final quarter for verification, overlap refresh and handoff. + +## Coordination and concrete non-overlap + +No pinned issue exists (GitHub GraphQL `pinnedIssues` returned empty). +Immediately before this claim, live metadata covered 627 open PRs through +#814. No centered native query-pair fusion was found. The review ledger +marks PR521 and PR481 unreviewed; citation does not imply maintainer approval. +The selected record is PR741, conditional kappa `0.001661202643272239`; +its review, actual SW4 construction and source manifest were inspected. + +PR756 is a performance change to a historical balanced-Fano enumeration. +This package touches no such checker, searches or performance receipts. +PR805 changes real rational cyclic leaves and restoration of one dirty +array plus a scalar. This package instead concerns exact odd-ring ADDRESS +permutations acting on F2 VALUE arrays, with queries on the genuine DATA +target and no full private row; it imports none of PR805's leaf construction, +restoration interface, code or verification. Both live PR descriptions and +relevant diffs were read. Neither existing PR will be changed. + +Prepared for **Wentao Li** (GitHub `VictorLiwentao`) with substantial OpenAI +Codex assistance. Predecessor names and notices will be retained. Apache-2.0. + +## Completed result (single final claim update) + +Submitted [PR840](https://github.com/CrocSwap/integer-mult-bounds/pull/840). +The mathematical package commit is +`9623aa12bc4c3c3828f6a804c94c42f90e511041`; the exact base remains +`7ee02b7c96d85f22b38d28bd7ed49bb8c1aeb261`. This result update changes +only the claim record. The final PR head is reported in the chat handoff. + +The hypothesis succeeds as a scoped construction: three ordinary ADDRESS +children, eighteen affine events and two XORs replace four children, +twenty-four affine events and four XORs for the specified completed pair. +All dirty source/spectator inputs are preserved and no full private row is +added. The proof establishes the sharp three-query minimum in the stated +power-query/XOR model; it does not assert a minimum over all tape programs. +Fixed-j coefficient costs and all typed primitive/child charges remain paid. +**No new kappa or physical runtime improvement is claimed.** + +Reproduce: `python3 -I -O -B research/dyadic-query-pair/verify.py`. +Expected: `PASS_DYADIC_QUERY_PAIR`. Completed coverage: 112 signed lowerings, +1,792 rational columns, 16,128 modular columns, 91,320 two-query products, +154,160 full-domain dirty basis columns per program, 7,552 orbit columns, +25 mathematical/admission controls and six package faults. Final evidence +agrees on CPython 3.9.6, 3.12.14 and 3.13.2, including isolated optimized +and relocated offline runs. Exact fetched Git inputs, selected-record and +staged whitespace checks pass. One untouched-base `make verify` passes its +seven initial historical groups, then stops on missing SymPy at gen4 +(exit 2); no full-suite or selected-supplier cold replay is claimed. + +Final overlap refresh covered 636 open PRs through #839. The two consumed +PR heads remain unchanged. Later PR800/822/829/836/838 have different +Clifford, storage or evidence-admission objects; no code is consumed. +Upstream advanced to `f567884aeb8851b6e794af1184119a3bfbe1e631`, selecting +PR799 at conditional kappa `0.001661634653669567`; its actual X4 construction +and review were read and recorded as context. No frontier record is edited. + +Concrete non-overlap is unchanged: PR756's Fano checker/performance package +and PR805's rational cyclic leaf/dirty-array-plus-scalar restoration are +excluded. Neither existing PR, branch or worktree was changed. The result +uses exact odd-ring ADDRESS maps and F2 VALUE arrays on the genuine DATA +target, with no full private row. Complete supplier/physical/compiler and +analytic transfer remain open, as detailed in PROOF.md and VALIDATION.md. diff --git a/research/dyadic-query-pair/LICENSE b/research/dyadic-query-pair/LICENSE new file mode 100644 index 0000000000..261eeb9e9f --- /dev/null +++ b/research/dyadic-query-pair/LICENSE @@ -0,0 +1,201 @@ + Apache License + Version 2.0, January 2004 + http://www.apache.org/licenses/ + + TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION + + 1. Definitions. + + "License" shall mean the terms and conditions for use, reproduction, + and distribution as defined by Sections 1 through 9 of this document. + + "Licensor" shall mean the copyright owner or entity authorized by + the copyright owner that is granting the License. + + "Legal Entity" shall mean the union of the acting entity and all + other entities that control, are controlled by, or are under common + control with that entity. For the purposes of this definition, + "control" means (i) the power, direct or indirect, to cause the + direction or management of such entity, whether by contract or + otherwise, or (ii) ownership of fifty percent (50%) or more of the + outstanding shares, or (iii) beneficial ownership of such entity. + + "You" (or "Your") shall mean an individual or Legal Entity + exercising permissions granted by this License. + + "Source" form shall mean the preferred form for making modifications, + including but not limited to software source code, documentation + source, and configuration files. + + "Object" form shall mean any form resulting from mechanical + transformation or translation of a Source form, including but + not limited to compiled object code, generated documentation, + and conversions to other media types. + + "Work" shall mean the work of authorship, whether in Source or + Object form, made available under the License, as indicated by a + copyright notice that is included in or attached to the work + (an example is provided in the Appendix below). + + "Derivative Works" shall mean any work, whether in Source or Object + form, that is based on (or derived from) the Work and for which the + editorial revisions, annotations, elaborations, or other modifications + represent, as a whole, an original work of authorship. For the purposes + of this License, Derivative Works shall not include works that remain + separable from, or merely link (or bind by name) to the interfaces of, + the Work and Derivative Works thereof. + + "Contribution" shall mean any work of authorship, including + the original version of the Work and any modifications or additions + to that Work or Derivative Works thereof, that is intentionally + submitted to Licensor for inclusion in the Work by the copyright owner + or by an individual or Legal Entity authorized to submit on behalf of + the copyright owner. For the purposes of this definition, "submitted" + means any form of electronic, verbal, or written communication sent + to the Licensor or its representatives, including but not limited to + communication on electronic mailing lists, source code control systems, + and issue tracking systems that are managed by, or on behalf of, the + Licensor for the purpose of discussing and improving the Work, but + excluding communication that is conspicuously marked or otherwise + designated in writing by the copyright owner as "Not a Contribution." + + "Contributor" shall mean Licensor and any individual or Legal Entity + on behalf of whom a Contribution has been received by Licensor and + subsequently incorporated within the Work. + + 2. Grant of Copyright License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + copyright license to reproduce, prepare Derivative Works of, + publicly display, publicly perform, sublicense, and distribute the + Work and such Derivative Works in Source or Object form. + + 3. Grant of Patent License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + (except as stated in this section) patent license to make, have made, + use, offer to sell, sell, import, and otherwise transfer the Work, + where such license applies only to those patent claims licensable + by such Contributor that are necessarily infringed by their + Contribution(s) alone or by combination of their Contribution(s) + with the Work to which such Contribution(s) was submitted. If You + institute patent litigation against any entity (including a + cross-claim or counterclaim in a lawsuit) alleging that the Work + or a Contribution incorporated within the Work constitutes direct + or contributory patent infringement, then any patent licenses + granted to You under this License for that Work shall terminate + as of the date such litigation is filed. + + 4. Redistribution. You may reproduce and distribute copies of the + Work or Derivative Works thereof in any medium, with or without + modifications, and in Source or Object form, provided that You + meet the following conditions: + + (a) You must give any other recipients of the Work or + Derivative Works a copy of this License; and + + (b) You must cause any modified files to carry prominent notices + stating that You changed the files; and + + (c) You must retain, in the Source form of any Derivative Works + that You distribute, all copyright, patent, trademark, and + attribution notices from the Source form of the Work, + excluding those notices that do not pertain to any part of + the Derivative Works; and + + (d) If the Work includes a "NOTICE" text file as part of its + distribution, then any Derivative Works that You distribute must + include a readable copy of the attribution notices contained + within such NOTICE file, excluding those notices that do not + pertain to any part of the Derivative Works, in at least one + of the following places: within a NOTICE text file distributed + as part of the Derivative Works; within the Source form or + documentation, if provided along with the Derivative Works; or, + within a display generated by the Derivative Works, if and + wherever such third-party notices normally appear. The contents + of the NOTICE file are for informational purposes only and + do not modify the License. You may add Your own attribution + notices within Derivative Works that You distribute, alongside + or as an addendum to the NOTICE text from the Work, provided + that such additional attribution notices cannot be construed + as modifying the License. + + You may add Your own copyright statement to Your modifications and + may provide additional or different license terms and conditions + for use, reproduction, or distribution of Your modifications, or + for any such Derivative Works as a whole, provided Your use, + reproduction, and distribution of the Work otherwise complies with + the conditions stated in this License. + + 5. Submission of Contributions. Unless You explicitly state otherwise, + any Contribution intentionally submitted for inclusion in the Work + by You to the Licensor shall be under the terms and conditions of + this License, without any additional terms or conditions. + Notwithstanding the above, nothing herein shall supersede or modify + the terms of any separate license agreement you may have executed + with Licensor regarding such Contributions. + + 6. Trademarks. This License does not grant permission to use the trade + names, trademarks, service marks, or product names of the Licensor, + except as required for reasonable and customary use in describing the + origin of the Work and reproducing the content of the NOTICE file. + + 7. Disclaimer of Warranty. Unless required by applicable law or + agreed to in writing, Licensor provides the Work (and each + Contributor provides its Contributions) on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or + implied, including, without limitation, any warranties or conditions + of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A + PARTICULAR PURPOSE. You are solely responsible for determining the + appropriateness of using or redistributing the Work and assume any + risks associated with Your exercise of permissions under this License. + + 8. Limitation of Liability. In no event and under no legal theory, + whether in tort (including negligence), contract, or otherwise, + unless required by applicable law (such as deliberate and grossly + negligent acts) or agreed to in writing, shall any Contributor be + liable to You for damages, including any direct, indirect, special, + incidental, or consequential damages of any character arising as a + result of this License or out of the use or inability to use the + Work (including but not limited to damages for loss of goodwill, + work stoppage, computer failure or malfunction, or any and all + other commercial damages or losses), even if such Contributor + has been advised of the possibility of such damages. + + 9. Accepting Warranty or Additional Liability. While redistributing + the Work or Derivative Works thereof, You may choose to offer, + and charge a fee for, acceptance of support, warranty, indemnity, + or other liability obligations and/or rights consistent with this + License. However, in accepting such obligations, You may act only + on Your own behalf and on Your sole responsibility, not on behalf + of any other Contributor, and only if You agree to indemnify, + defend, and hold each Contributor harmless for any liability + incurred by, or claims asserted against, such Contributor by reason + of your accepting any such warranty or additional liability. + + END OF TERMS AND CONDITIONS + + APPENDIX: How to apply the Apache License to your work. + + To apply the Apache License to your work, attach the following + boilerplate notice, with the fields enclosed by brackets "[]" + replaced with your own identifying information. (Don't include + the brackets!) The text should be enclosed in the appropriate + comment syntax for the file format. We also recommend that a + file or class name and description of purpose be included on the + same "printed page" as the copyright notice for easier + identification within third-party archives. + + Copyright [yyyy] [name of copyright owner] + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. diff --git a/research/dyadic-query-pair/NOTICE.md b/research/dyadic-query-pair/NOTICE.md new file mode 100644 index 0000000000..d58769de46 --- /dev/null +++ b/research/dyadic-query-pair/NOTICE.md @@ -0,0 +1,52 @@ +# Attribution, license and scope + +New compiler, checker, proof, certificate and documentation prepared for +**Wentao Li**, with substantial **OpenAI Codex (GPT-6.1 Sol) assistance** in +analysis, derivation, implementation, testing and writing. Contributor profiles: +[GitHub: VictorLiwentao](https://github.com/VictorLiwentao) and +[X: @Is__Victor](https://x.com/Is__Victor). Apache-2.0; the repository license +is copied unchanged to LICENSE. No sub-agents, independent human peer review, +proof-assistant verification or literature-priority claim. + +- **Karl Appel / applecrusher, PR521**, exact head + `a190fdb39f31647fc6f651625353710624627348`: native rank-one unipotent ADDRESS + map, one-child ordered lowering at k=1, shared-chart comparison and stated + tape premises. His proof and source-pin record are retained unchanged. +- **commdata2338, PR677**, exact head + `613c02b8b4411f991f108dcc1481b3f9100b996f`: completed first-difference DATA + shear, DATA-target querying permission, two-query model/classification, + private-storage distinctions and typed costs. The original proof and full + notice remain unchanged in vendor/. That notice retains the disclosed + OpenAI Codex / Claude Code assistance and predecessor attribution. Its + two-query first-difference theorem is preserved. +- **OpenAI, Integer multiplication below n log n, September 23, 2026**: + ordered affine streams, ordinary equal-width ADDRESS interchange, + complete spectators, tape/stack and head-return contracts. The two full + source sections and their Apache-2.0 license are copied byte for byte from + CrocSwap/integer-mult-bounds revision + `5996e33ecad6a0ccd578aec58831457829d75575`. Their source identity and the + imported framework maintained by **Douglas Colkitt** remain credited. +- The binary projector / group-algebra lineage is credited through PR677's + retained notice to **eumemic (PR288)** and **Ali Romman (PR468)**. No code + or nine-call search from those packages is imported here. +- Concurrent dirty/clean echo work by **FanPUYen, Sagar Thakrar, Ali Romman, + Koroffstrogov, Alexander Schwartzman and nightangelflowerwin-ops** was + inspected to avoid overlap. It is context, not a dependency. PR481's + Gaussian boundary batching by **Chafik Boukhalfa / chafreaky** was also + inspected and supplies no code or analytic claim here. +- Later context checks read **Jeremy Diviney / PR800** (formal Clifford + path valuations), **shhxera / PR822** (dirty connector reuse) and + **Paul Chan / PR829** (two clean checkpoints). Those objects and query/ + storage alphabets differ from this centered native ADDRESS shear. No + code, certificate or theorem from these three PRs is consumed. +- PR741 at the task base and the refreshed PR799 construction retain + their existing repository attribution. Their certificates, suppliers and + inherited conditions are not changed or re-certified by this local result. + +This package adds the dyadic lowering extension, fusion of the completed +centered shear pair, precise three-query bound and new finite evidence relative +to the pinned repository context. Elementary compute/uncompute, determinant +and Laurent methods are not claimed as new literature discoveries. PR756 and +PR805 are explicitly excluded from the consumed construction and verification. +This is not an official OpenAI release or endorsement. Exact source hashes and +inspected context heads are in SOURCES.json. diff --git a/research/dyadic-query-pair/PROGRAM.json b/research/dyadic-query-pair/PROGRAM.json new file mode 100644 index 0000000000..e7082859ad --- /dev/null +++ b/research/dyadic-query-pair/PROGRAM.json @@ -0,0 +1,258 @@ +{ + "a": 18014398509481984, + "baseline_chronological_events": [ + [ + "query", + 0, + -18014398509481984 + ], + [ + "xor", + 0, + 1 + ], + [ + "query", + 0, + 18014398509481984 + ], + [ + "xor", + 0, + 1 + ], + [ + "query", + 0, + 18014398509481984 + ], + [ + "xor", + 0, + 1 + ], + [ + "query", + 0, + -18014398509481984 + ], + [ + "xor", + 0, + 1 + ] + ], + "format": "native-dyadic-pair-program-v1", + "fused_chronological_events": [ + [ + "query", + 0, + -18014398509481984 + ], + [ + "xor", + 0, + 1 + ], + [ + "query", + 0, + 36028797018963968 + ], + [ + "xor", + 0, + 1 + ], + [ + "query", + 0, + -18014398509481984 + ] + ], + "j": 54, + "query_lowerings": { + "-18014398509481984": [ + { + "controls": [ + [ + 0, + "-1" + ] + ], + "diagonal": "1", + "op": "ordered_affine", + "target": 2 + }, + { + "controls": [ + [ + 0, + "1" + ] + ], + "diagonal": "1", + "op": "ordered_affine", + "target": 3 + }, + { + "controls": [ + [ + 0, + "-4503599627370495" + ], + [ + 2, + "4503599627370496" + ], + [ + 3, + "4503599627370496" + ] + ], + "diagonal": "-4503599627370496", + "op": "ordered_affine", + "target": 5 + }, + { + "fields": [ + 0, + 5 + ], + "op": "ordinary_child" + }, + { + "controls": [ + [ + 0, + "1" + ] + ], + "diagonal": "1", + "op": "ordered_affine", + "target": 2 + }, + { + "controls": [ + [ + 0, + "-1" + ] + ], + "diagonal": "1", + "op": "ordered_affine", + "target": 3 + }, + { + "controls": [ + [ + 0, + "-4503599627370497/4503599627370496" + ], + [ + 2, + "1" + ], + [ + 3, + "1" + ] + ], + "diagonal": "1/4503599627370496", + "op": "ordered_affine", + "target": 5 + } + ], + "36028797018963968": [ + { + "controls": [ + [ + 0, + "-1" + ] + ], + "diagonal": "1", + "op": "ordered_affine", + "target": 2 + }, + { + "controls": [ + [ + 0, + "1" + ] + ], + "diagonal": "1", + "op": "ordered_affine", + "target": 3 + }, + { + "controls": [ + [ + 0, + "9007199254740993" + ], + [ + 2, + "-9007199254740992" + ], + [ + 3, + "-9007199254740992" + ] + ], + "diagonal": "9007199254740992", + "op": "ordered_affine", + "target": 5 + }, + { + "fields": [ + 0, + 5 + ], + "op": "ordinary_child" + }, + { + "controls": [ + [ + 0, + "1" + ] + ], + "diagonal": "1", + "op": "ordered_affine", + "target": 2 + }, + { + "controls": [ + [ + 0, + "-1" + ] + ], + "diagonal": "1", + "op": "ordered_affine", + "target": 3 + }, + { + "controls": [ + [ + 0, + "-9007199254740991/9007199254740992" + ], + [ + 2, + "1" + ], + [ + 3, + "1" + ] + ], + "diagonal": "-1/9007199254740992", + "op": "ordered_affine", + "target": 5 + } + ] + } +} diff --git a/research/dyadic-query-pair/PROOF.md b/research/dyadic-query-pair/PROOF.md new file mode 100644 index 0000000000..aaba3e501d --- /dev/null +++ b/research/dyadic-query-pair/PROOF.md @@ -0,0 +1,204 @@ +# Three queries for a centered dyadic native BIT shear + +This is a local recursive-interface construction and a scoped query lower +bound. Ordinary ADDRESS interchange and ordered affine tape streams remain +premises. There is no new supplier, kappa, or formal multiplication proof. + +## Object and predecessor contracts + +Karl Appel / applecrusher's PR521 gives the native unipotent query below and +its one-child lowering at `k=1`. PR677 by commdata2338 completes the shear +`S_h(x,y,z)=(x+(h+I)y,y,z)` using two queries on the DATA target. Its source +remains untouched, and no full private row is required. VALUE addition is +over F2; ADDRESS arithmetic is rational arithmetic specialized to an odd +residue ring. The contribution here combines **two completed shears**, +extends the literal lowering to signed dyadic powers, and changes the +intermediate query to `h^(2a)`. It is not PR521's unfinished dirty chart. + +Use six physically ordered equal-width ADDRESS fields +`(H0,H1,H2,D0,D1,D2)`, each ranging over `Z/(ell^b)`, `b>=1`, `ell` odd. +Arbitrary intervening/exterior spectator fields and suffix VALUE records +are retained. Define column vectors + + s=(1,0,1,-1,0,-1)^T, r=(1,0,-1,-1,0,1)^T, + M(k)=I6+(k/4)s r^T. + +Since `r^T s=0`, `M(k)M(l)=M(k+l)` and `M(k)^-1=M(-k)`. +Let `h` be the array permutation induced by the ADDRESS **push** map `M(1)`. +Thus a VALUE moves from address `z` to `M(1)z`, and the value at a new address +is read from its inverse image. The full-array operator for `M(k)` is `h^k`. + +For each fixed integer `j>=0`, let `a=+/-2^j`. The desired completed endpoint is + + F_a(x,y,z)=(x+(h^a+h^-a)y,y,z). (1) + +Every additional arbitrary dirty row is unchanged. Source `y` is never +modified. The target requires exclusive access until the completed boundary; +the caller may not read its temporarily permuted representation mid-program. +This is the same target permission needed by PR677's DATA-target program. + +## One-child lowering of every signed dyadic power + +Put `c=k/4`, for `k=+/-2^j`. Apply, chronologically, + + z2 <- z2-z0 + z3 <- z3+z0 + z5 <- c*z5+(1+c)*z0-c*z2-c*z3 + CHILD_C(0,5) + z2 <- z2+z0 + z3 <- z3-z0 + z5 <- -(1/c)*z5+(1/c-1)*z0+z2+z3. (2) + +Every control precedes its target. The child swaps exactly two `b`-digit +fields on the complete queried BIT row, preserving every spectator. All six +affine events are charged, including their preparation, temporary tapes, +source access, counter work and head returns. The child uses its own restored +workspace; it is not an uncharged VALUE swap. + +To check (2), write incoming coordinates as `A,B,C,D,E,F` and +`d=A-C-D+F`. Just before the child, the later field is `A+c*d`, and the +middle fields are `C-A,D+A`. After the child and the next two events, +the first field is `A+c*d`, and the middle fields are `C+c*d,D-c*d`. +The final line gives `F-c*d`. Coordinates 1 and 4 stay fixed. This is +exactly `z+(k/4)s(r^T z)=M(k)z`. The literal reverse of (2), inverting +each affine event and using the same involutive child, implements `M(-k)`. + +The only diagonal units are `1,c,-1/c`. All numerator and denominator +factors of these units are powers of two, up to sign. Every control +denominator is also a power of two. Therefore (2) and its inverse +specialize to **every odd modulus**, including every odd prime-power +width. A control numerator may vanish modulo ell without invalidating a +diagonal. An arbitrary non-dyadic k would introduce prime exclusions into +this particular lowering; no such all-odd-radix claim is made. + +At k=1 this is exactly PR521's attributed word. The extension changes its +coefficients, not its tape/child contracts. For a fixed j, the finite +coefficient table is compiled into the machine description. Its size and +streaming constants depend on j. A growing j is separately priced below. + +## Completed pair fusion + +Two successive applications of PR677's completed DATA-target program, +for `h^a` and `h^-a`, produce (1): the two identity contributions cancel +over F2. This literal baseline has four queries and four XOR scans. + +Instead apply, chronologically, + + x <- h^-a x + x += y + x <- h^(2a) x + x += y + x <- h^-a x. (3) + +Following x gives `h^-a x+y`, then `h^a x+h^(2a)y`, then +`h^a x+h^(2a)y+y`, finally `x+h^a y+h^-a y`. The three target +permutations multiply to the identity. The unchanged source and spectators +can be arbitrarily dirty. No private row is initialized, borrowed, copied +or cleared. Because (1) is a VALUE shear, `F_a^2=I` despite `h^a` being +noninvolutive. Reversing and inverting the literal events restores all data. + +Lowering all queries by (2) gives **three separately paid ordinary children, +eighteen affine events and two XOR scans**, versus four children, +twenty-four affine events and four XOR scans for the completed pair. +This is a count comparison for this baseline; physical speed is not measured. + +## Three queries are necessary in the stated model + +Allow d>=2 arbitrary dirty F2-valued rows, invertible address-independent +linear XOR maps between row roles, and queries `h^e` on one row for any +integer e. All other ADDRESS maps, clean/disposable storage, erasure, +nonlinear VALUE gates and intermediate observations lie outside this model. +The lower bound counts queries, even when a non-dyadic power would need a +different physical lowering. It is not a lower bound on all tape programs. + +Restrict the complete ADDRESS domain to the orbit of `e_H0` under h. +Its addresses are `e_H0+k*s/4`, indexed by `Z/m`, `m=ell^b`. They are +distinct because a component of s and 1/4 are units. Hence h is multiplication +by t on the regular module of `R=F2[t,t^-1]/(t^m-1)`. Basis monomials +`1,t,...,t^(m-1)` are independent; zero divisors in R do not affect the +following determinant and coefficient arguments. The same proof works +over the Laurent ring for a uniform symbolic identity. +The determinants are those of d-by-d row matrices over R, not of the +expanded F2 matrix of all individual BIT positions. + +Move all constant row maps to the left, conjugating queries. At t=1, +the target `I+(t^a+t^-a)N`, `N=e_x e_y^T`, is I, so the remaining +constant map is I. A normalized query has the form + + D_P(t^e)=I+(t^e+1)P, P=u v^T, v^T u=1, + det D_P(t^e)=t^e. (4) + +The determinant of the target is one. Zero queries cannot produce its +nonzero off-diagonal entry: a is a unit modulo odd m and `t^a!=t^-a`. +One query either is the identity (e=0 modulo m) or has the wrong determinant. +For two queries, the determinant forces opposite exponents modulo m, +and their product is + + I+P+Q+t^e(P+PQ)+t^-e(Q+PQ). (5) + +If e=0 modulo m, both are identity. Otherwise, as m is odd, `1,t^e,t^-e` +are distinct basis monomials. The target's constant coefficient is I. +Comparing constant coefficients in (5) therefore forces P=Q. Then +`P^2=P` cancels both other coefficients and (5) is I, a contradiction. +Thus no two-query program implements (1), even with arbitrary dirty +spectator rows and arbitrary integer-power queries. Program (3) attains +three. This is a written algebraic proof, not an inference from finite tests. + +PR677's different first-difference target has constant coefficient `I+N` +and attains two queries. Its theorem is preserved. Allowing `h^(2a)` here +changes the physical query alphabet: substituting two `h^a` calls would +restore the four-child bill. At an even orbit a centered target can vanish; +the odd full-order hypothesis is necessary for this formulation. + +## Complete typed costs and workspace + +Let each genuine DATA row have full logical BIT volume U, including every +spectator range; V=3U and N=3b. Let C(U,b) pay one ordinary ADDRESS +interchange with restored child workspace. Let L_k(U,b) be the sum of the +six actual ordered-affine charges in (2), **including** finite coefficient +preparation, source access, counter work, temporary tapes and their returns. +Let X(U) pay one aligned XOR scan. Let R_f,R_b pay row split/merge, evaluator +routing, descriptors, parking and all additional head returns. Then + + B_a(V,3b) <= 4 C(U,b)+2 L_a(U,b)+2 L_-a(U,b)+4 X(U)+R_b, + F_a(V,3b) <= 3 C(U,b)+2 L_-a(U,b)+L_2a(U,b)+2 X(U)+R_f. (6) + +The new middle lowering has a different coefficient table. Equation (6) +does not assume equal costs for it. Relative to these literal invoices, +the saving is `C+2 L_a-L_2a+2 X+R_b-R_f`; this is not asserted positive +for every finite implementation. Under the retained tape contracts and +**fixed j**, L_k, X and R are O_j(V), giving normalized recursive-child +coefficients 4/3 and 1 respectively. The three children are sequential, +each on actual volume V/3 and width N/3. Persistent genuine-role storage is +V in both programs, with no additional full private role. A safe peak bound is + + W_f(V,3b) <= V+B_f(V,b,j)+W_C(U,b), + +where B_f pays streaming, counter/coefficient and evaluator parking workspace. +No exact physical tape count or scratch-cell saving is claimed. + +For growing j, table entries have O(j+1) numerator/denominator bits and +modular preparations and all primitive costs must retain their j dependence. +In particular the original direct multiplication stream can have a number +of pieces depending on a fixed large integer. No polynomial-in-j runtime +or uniform O(V) constant is inferred from (2). The `j=54` fixture is exact +coefficient evidence, not a practical performance demonstration. + +The left sides of (6) are a centered DATA shear; C is ordinary ADDRESS +interchange. Replacing C by F_a and solving a self-recursion would require +a separate compiler and would be circular here. Arbitrary-width padding, +common-label construction, scalar/frame/owner schedules, both supplier +invoices, precision/tape/hosting and analytic transfer remain obligations. +No supplier or assembly constraint is changed, so no new kappa follows. + +## Evidence boundary + +The checker compares (2) to an independently derived rational matrix and +modular formula, checks the VALUE endpoint over exact Laurent matrices, +and uses a separate sparse-set full-domain replay. Negative controls remove +children, change powers/directions, omit scans, destroy a dirty spectator, +and demonstrate the first-difference/even-orbit scope boundaries. +The recorded finite domains, fixed seed-selected coefficient and source pins +are in CERTIFICATE.json and SOURCES.json. No search outside those domains, +proof-assistant verification, complete supplier replay or runtime benchmark +is claimed. The universal argument above remains open to mathematical review. diff --git a/research/dyadic-query-pair/PUBLICATION-CONTEXT.json b/research/dyadic-query-pair/PUBLICATION-CONTEXT.json new file mode 100644 index 0000000000..6eef3c68f7 --- /dev/null +++ b/research/dyadic-query-pair/PUBLICATION-CONTEXT.json @@ -0,0 +1,101 @@ +{ + "changed_main_package_overlap": [], + "consumed_tape_sections_unchanged": true, + "date": "2026-10-13", + "format": "dyadic-query-pair-publication-context-v1", + "inspected": [ + { + "author": "applecrusher", + "head": "a190fdb39f31647fc6f651625353710624627348", + "number": 521, + "present_in_final_open_snapshot": true, + "title": "Native BIT ADDRESS fusion: two recursive queries to one" + }, + { + "author": "commdata2338", + "head": "613c02b8b4411f991f108dcc1481b3f9100b996f", + "number": 677, + "present_in_final_open_snapshot": true, + "title": "Research note: restored DATA-shear boundaries for PR #521's native BIT query (exact query costs, no new \u03ba)" + }, + { + "author": "VictorLiwentao", + "head": "4fad623a1e4ca06959f4326e221c2f8d9125c269", + "number": 756, + "present_in_final_open_snapshot": true, + "title": "Tooling: replay balanced Fano 2.91\u00d7 faster with identical exhaustive streams" + }, + { + "author": "VictorLiwentao", + "head": "ef34bd5b32fcf2d5640dae90b5b8f28488738d5a", + "number": 805, + "present_in_final_open_snapshot": true, + "title": "Research: determinant-balanced cyclic leaves with exact dirty restoration (no new kappa)" + }, + { + "author": "jeremydiviney", + "head": "d7d83e0a9b98f95a4443d1060336be267ac3fd80", + "number": 800, + "present_in_final_open_snapshot": true, + "title": "Research: weighted path valuations exclude a remaining eight-call Clifford word (no kappa)" + }, + { + "author": "shhxera", + "head": "8c5e1b557f59bca29139c4c2dcc65edfb808372b", + "number": 822, + "present_in_final_open_snapshot": true, + "title": "Research: reuse dirty echo connectors (no new kappa)" + }, + { + "author": "Better-Call-Paul", + "head": "64a29f934e06e4ec4563aef7fc0193eb9dfa816b", + "number": 829, + "present_in_final_open_snapshot": false, + "title": "Research: two clean checkpoints reduce the 50-factor leaf bill 1728 to 1248 (no new kappa)" + }, + { + "author": "jeremydiviney", + "head": "7ae9124f59694bb1e5acf2ae99c65e63c115b2f4", + "number": 836, + "present_in_final_open_snapshot": true, + "title": "Research: signed rank transport excludes unitary register mixers (no new kappa)" + }, + { + "author": "ljste", + "head": "2a50020bb9564229874cbfbdc112e17b235bacfc", + "number": 838, + "present_in_final_open_snapshot": true, + "title": "Research audit: PR741 binding accepts omitted replay evidence (no new kappa)" + } + ], + "latest_open_pr": 839, + "open_pr_count": 636, + "overlap_finding": "Only PR521 and PR677 directly name the native unipotent component. No centered dyadic query-pair contribution found. Other inspected later work has different Clifford, dirty-echo, clean-storage or provenance objects. No PR756/PR805 code or verification is consumed.", + "pinned_coordination_issue": null, + "refreshed_main": "f567884aeb8851b6e794af1184119a3bfbe1e631", + "scope": "Metadata/context review only; no PR799 cold replay or new frontier certificate.", + "selected_at_refreshed_main": { + "decimal": "0.001661634653669567", + "kappa": "1661634653669567/1000000000000000000", + "pr": 799, + "reproduce": "make frontier799-verify" + }, + "selected_context_read": [ + { + "commit": "f567884aeb8851b6e794af1184119a3bfbe1e631", + "path": "docs/research/community-frontier799-review.md", + "sha256": "bd91c10c67f2a873fd456b95cbb43f715a43dac0e0a66938737d591c6b754052" + }, + { + "commit": "f567884aeb8851b6e794af1184119a3bfbe1e631", + "path": "research/gauge44-frames-x/PROOF-NOTE-FRAMES-X4.md", + "sha256": "39c50420ebb6e8813706a49b2cf759f277c4afac9f6780fc0a7ac6a5fb86e036" + }, + { + "commit": "f567884aeb8851b6e794af1184119a3bfbe1e631", + "path": "research/gauge44-frames-x/CONSTRUCTION.md", + "sha256": "7d96eb958a6b4274ea4c4c539b585f8ae2e89363b76aef930f90d2d513e164ea" + } + ], + "task_base": "7ee02b7c96d85f22b38d28bd7ed49bb8c1aeb261" +} diff --git a/research/dyadic-query-pair/README.md b/research/dyadic-query-pair/README.md new file mode 100644 index 0000000000..3988b2cb22 --- /dev/null +++ b/research/dyadic-query-pair/README.md @@ -0,0 +1,98 @@ +# Fuse a completed native BIT shear pair with three children + +**Research construction / recursive interface; no new kappa.** For the native +unipotent ADDRESS query h from Karl Appel's PR521, two completed DATA shears +from commdata2338's PR677 have endpoint `x ^= (h^a+h^-a)y`, `a=+/-2^j`. +The literal program below implements that endpoint with arbitrary dirty DATA +and spectators, no full private row, and a three-query minimum in the +specified power-query/XOR model: + +```text +x <- h^-a x +x ^= y +x <- h^(2a) x +x ^= y +x <- h^-a x +``` + +Each signed dyadic query is lowered to six physically ordered affine events +and one ordinary recursive ADDRESS interchange on the entire target row. +The completed pair changes from **4 to 3 children, 24 to 18 affine events, +and 4 to 2 XOR scans**. These are explicit interface counts, not measured +runtime or a selected-supplier optimization. Coefficient costs differ: +the middle query uses 2a, and the tape constants depend on fixed j. + +From the repository root, with standard-library Python 3.9+: + +```sh +python3 -I -O -B research/dyadic-query-pair/verify.py +``` + +Expected: + +```text +PASS_DYADIC_QUERY_PAIR: children 4->3; affine 24->18; XOR 4->2; no new kappa +rational columns 1792 ; modular columns 16128 ; two-query census 91320 ; negative controls 25 +full-domain dirty basis columns 154160 ; orbit columns 7552 +``` + +The package also runs offline after relocation. `python3 -I -B +research/dyadic-query-pair/check_package.py` checks relocation and deliberate +source/certificate/program faults. `verify.py --emit /absolute/new/directory` +regenerates both JSON artifacts without overwriting an existing directory. + +The exact base is `7ee02b7c96d85f22b38d28bd7ed49bb8c1aeb261`. The freshly +selected record there is PR741, conditional kappa `0.001661202643272239`. +This contribution adds only this directory. Its OS assignment seed is 54, +which selects the retained large coefficient fixture `a=2^54`; no random +search is performed. The literal fixture is in `PROGRAM.json`, all completed +coverage and stream digests in `CERTIFICATE.json`, and immutable Git/SHA-256 +source pins in `SOURCES.json`. + +During the publication refresh, upstream advanced to +`f567884aeb8851b6e794af1184119a3bfbe1e631`, selecting PR799 at conditional +kappa `0.001661634653669567`. Its review and actual X4 construction were +read; both consumed PR heads and the two upstream tape sections remain +unchanged. The new selection supplies context, not a dependency or an +additional result of this package. The exact task base remains the one above. + +- `PROOF.md` gives the all-j lowering, full-array endpoint, sharp three-query + argument, complete typed cost/storage recurrence and limitations. +- `program.py` is a literal compiler/reference evaluator. Its child event is + an ordinary full-row ADDRESS-interchange contract; the tape supplier is not + implemented here. +- `verify.py` derives a separate rational matrix, modular specializations and + exact Laurent VALUE operators. Its two-query census checks all binary + rank-one projectors in dimensions 2, 3, 4 with balanced powers +/-1,+/-2,+/-4. + The arbitrary-dimension/power theorem is the written proof. +- `full_domain.py` uses a separately written modular coordinate interpreter + and direct push formula. It checks every six-field ADDRESS over Z/3 and + Z/5, all four-role dirty BIT basis inputs for the declared parameters, + literal inverses, fixed/shorter/full-order orbits in larger prime powers, + and simultaneous nonzero dirt. Simulator storage is not a tape measurement. +- The 25 controls omit every fused event and every individual ADDRESS event, + change query powers/signs/roles and XOR sources, and test the dirty-storage, + dyadic/odd-ring and first-difference scope boundaries. Package fault tests + also distinguish JSON integers from Boolean substitutions. + +The genuine DATA target must be exclusively writable until completion. Source +and caller-owned dirty storage remain intact. Primitive temporary streams, +child workspace, source access, routing, preparation and head returns are +paid in the recurrence; “no private row” does not mean no primitive workspace. +For growing j the j-dependent table and primitive expenses remain explicit. +This centered DATA shear cannot replace ordinary interchange without a separate +compiler. No arbitrary-width padding, complete scalar/frame/owner schedule, +new supplier invoice, assembly, precision/analytic transfer or full theorem +verification is provided. + +Concrete non-overlap: PR756 optimizes a historical balanced-Fano checker; +PR805 builds real rational cyclic leaves with one dirty array and one scalar. +This exact odd-ring ADDRESS / F2 VALUE interface consumes neither package, +changes neither PR, and uses neither restoration contract. Nearby PR714/730/ +744/758/784/788 optimize different dirty/clean echo classes. Their review heads +were inspected and retained as context in `SOURCES.json`. + +Prepared for **Wentao Li** with substantial OpenAI Codex assistance under +Apache-2.0. Predecessor credit and original immutable notices are retained in +`NOTICE.md` and `vendor/`. Validation and remaining limitations are recorded in +`VALIDATION.md`; the local claim and one result update are in `CLAIM.md`. diff --git a/research/dyadic-query-pair/SOURCES.json b/research/dyadic-query-pair/SOURCES.json new file mode 100644 index 0000000000..d535b797d1 --- /dev/null +++ b/research/dyadic-query-pair/SOURCES.json @@ -0,0 +1,171 @@ +{ + "assignment_seed": 54, + "base_commit": "7ee02b7c96d85f22b38d28bd7ed49bb8c1aeb261", + "claim_overlap": { + "inspected": [ + { + "author": "chafreaky", + "head": "5f3db6a11198bab07d8effe8f0c9f5df9c3f2eb7", + "number": 481, + "title": "Batch Gaussian boundary right-hand sides to reduce their cost" + }, + { + "author": "applecrusher", + "head": "a190fdb39f31647fc6f651625353710624627348", + "number": 521, + "title": "Native BIT ADDRESS fusion: two recursive queries to one" + }, + { + "author": "commdata2338", + "head": "613c02b8b4411f991f108dcc1481b3f9100b996f", + "number": 677, + "title": "Research note: restored DATA-shear boundaries for PR #521's native BIT query (exact query costs, no new \u03ba)" + }, + { + "author": "FanPUYen", + "head": "efad8a40094ab453c0525efef0b0eff2a5d8b850", + "number": 714, + "title": "Research: optimal clean root checkpoint saves 25\u201340% of binary product-shear calls" + }, + { + "author": "thakrarsagar", + "head": "d222e348179cc02a54d6d26dbd2838944f62c6e5", + "number": 730, + "title": "Research: optimize ordered dirty echoes at fixed scratch (no new kappa)" + }, + { + "author": "aliromman", + "head": "302383e0c1ec71c50860362d3f394f85664c2445", + "number": 744, + "title": "Independent verification: fixed-space ternary echo minima and rounded leaves" + }, + { + "author": "Koroffstrogov", + "head": "a164f06263e438ead570b169e5b7103aa45bf228", + "number": 758, + "title": "Research: higher-arity dirty echoes use 152 calls at five-array cap (no new kappa)" + }, + { + "author": "AlexS-scale", + "head": "548e42022b37a300f8bf745e848c38baccbce056", + "number": 784, + "title": "Research theorem: sharp scratch-dependent call bound for dirty echoes" + }, + { + "author": "nightangelflowerwin-ops", + "head": "ff8251519e009a01ede6b27e3f5af703eaa70132", + "number": 788, + "title": "Research: reusable clean checkpoint lowers weighted binary leaf bill 20 to 16 (no new kappa)" + }, + { + "author": "VictorLiwentao", + "head": "4fad623a1e4ca06959f4326e221c2f8d9125c269", + "number": 756, + "title": "Tooling: replay balanced Fano 2.91\u00d7 faster with identical exhaustive streams" + }, + { + "author": "VictorLiwentao", + "head": "ef34bd5b32fcf2d5640dae90b5b8f28488738d5a", + "number": 805, + "title": "Research: determinant-balanced cyclic leaves with exact dirty restoration (no new kappa)" + }, + { + "author": "shiftybitshiftr", + "head": "d91c5152b314391406b0ec792b6765a5cf0af2f1", + "number": 814, + "title": "Research: Eisenstein nonlinear message copy floor 22b under explicit width pricing" + } + ], + "max_pr": 814, + "open_count": 627, + "pinned_issue": null + }, + "format": "dyadic-native-query-pair-sources-v1", + "immutable_inputs": [ + { + "commit": "5996e33ecad6a0ccd578aec58831457829d75575", + "git_blob": "088fceea1867abc76271d7efe7532b779fee9039", + "local": "vendor/upstream-02-streams.tex", + "path": "upstream/build/sections/02-streams.tex", + "repository": "CrocSwap/integer-mult-bounds", + "sha256": "606c80db61cad13aa0c3b6060dc4b88dbbe7ac60cdd831aa93f28d908fd09dab", + "url": "https://github.com/CrocSwap/integer-mult-bounds/blob/5996e33ecad6a0ccd578aec58831457829d75575/upstream/build/sections/02-streams.tex" + }, + { + "commit": "5996e33ecad6a0ccd578aec58831457829d75575", + "git_blob": "951e792b1768e6509561380b8bbfb1d1ccb64c08", + "local": "vendor/upstream-04-swap.tex", + "path": "upstream/build/sections/04-swap.tex", + "repository": "CrocSwap/integer-mult-bounds", + "sha256": "412b170ccaab38dba96e95e3cbfae09f4876a9818f8d278776a746b0f8044906", + "url": "https://github.com/CrocSwap/integer-mult-bounds/blob/5996e33ecad6a0ccd578aec58831457829d75575/upstream/build/sections/04-swap.tex" + }, + { + "commit": "5996e33ecad6a0ccd578aec58831457829d75575", + "git_blob": "261eeb9e9f8b2b4b0d119366dda99c6fd7d35c64", + "local": "vendor/upstream-LICENSE", + "path": "upstream/LICENSE", + "repository": "CrocSwap/integer-mult-bounds", + "sha256": "c71d239df91726fc519c6eb72d318ec65820627232b2f796219e87dcf35d0ab4", + "url": "https://github.com/CrocSwap/integer-mult-bounds/blob/5996e33ecad6a0ccd578aec58831457829d75575/upstream/LICENSE" + }, + { + "commit": "a190fdb39f31647fc6f651625353710624627348", + "git_blob": "c3f67fc807aa3bf32ba559d51ea0b7e7a424229d", + "local": "vendor/pr521-PROOF.md", + "path": "research/native-unipotent-fusion/PROOF.md", + "repository": "CrocSwap/integer-mult-bounds", + "sha256": "320ce5529c1543f9e6fceb9e7f8b563ed332f13923229e38d4e7edac98f30283", + "url": "https://github.com/CrocSwap/integer-mult-bounds/blob/a190fdb39f31647fc6f651625353710624627348/research/native-unipotent-fusion/PROOF.md" + }, + { + "commit": "a190fdb39f31647fc6f651625353710624627348", + "git_blob": "549b87c2d57eb00296301c90e090d2f49d475a57", + "local": "vendor/pr521-SOURCE-PINS.json", + "path": "research/native-unipotent-fusion/SOURCE-PINS.json", + "repository": "CrocSwap/integer-mult-bounds", + "sha256": "34f97e7a31deed0dd85474ece3709a55de495f9473a3619f84e991fdbd3bf732", + "url": "https://github.com/CrocSwap/integer-mult-bounds/blob/a190fdb39f31647fc6f651625353710624627348/research/native-unipotent-fusion/SOURCE-PINS.json" + }, + { + "commit": "613c02b8b4411f991f108dcc1481b3f9100b996f", + "git_blob": "47d9bf59a3e0d85bcc4930cd76a3d21a1e43c2fc", + "local": "vendor/pr677-PROOF.md", + "path": "research/native-fusion-restored-shear/PROOF.md", + "repository": "CrocSwap/integer-mult-bounds", + "sha256": "4f281eb48b9662c03269717b3919b45b27f7c2655abb185249a1eea2a03af186", + "url": "https://github.com/CrocSwap/integer-mult-bounds/blob/613c02b8b4411f991f108dcc1481b3f9100b996f/research/native-fusion-restored-shear/PROOF.md" + }, + { + "commit": "613c02b8b4411f991f108dcc1481b3f9100b996f", + "git_blob": "bbd90a76bb1f3c55393367e24afd9970b796dba2", + "local": "vendor/pr677-NOTICE.md", + "path": "research/native-fusion-restored-shear/NOTICE.md", + "repository": "CrocSwap/integer-mult-bounds", + "sha256": "d79071e9dda5edc60305f80910572c1a61daf0b4601f5673b5ff874a6d487742", + "url": "https://github.com/CrocSwap/integer-mult-bounds/blob/613c02b8b4411f991f108dcc1481b3f9100b996f/research/native-fusion-restored-shear/NOTICE.md" + } + ], + "selected_context": [ + { + "commit": "7ee02b7c96d85f22b38d28bd7ed49bb8c1aeb261", + "path": "certificates/selected-result.json", + "sha256": "8f2bfbf11609194654d4da145866223d4c546c5418727cae056bfb9968cabcac" + }, + { + "commit": "7ee02b7c96d85f22b38d28bd7ed49bb8c1aeb261", + "path": "docs/research/community-frontier741-review.md", + "sha256": "4634694fa75ea9e749ecf19d3db3e4d82effe3b61a2efdf08ac5a97275fb676a" + }, + { + "commit": "7ee02b7c96d85f22b38d28bd7ed49bb8c1aeb261", + "path": "research/complex-sw4-frame8/PROOF.md", + "sha256": "21d8ef267f9ee4c837bcbab0f659e5a8bbf16e0ee1e79e7775342d39c8c8dd7b" + }, + { + "commit": "7ee02b7c96d85f22b38d28bd7ed49bb8c1aeb261", + "path": "docs/research/pr-ledger.json", + "sha256": "b7bf4514786dbd591a5579851871da12a5c235f925ddb465b4b93930493eb52b" + } + ] +} diff --git a/research/dyadic-query-pair/VALIDATION.md b/research/dyadic-query-pair/VALIDATION.md new file mode 100644 index 0000000000..ed7e5dac46 --- /dev/null +++ b/research/dyadic-query-pair/VALIDATION.md @@ -0,0 +1,98 @@ +# Executed validation and limits + +Executed 2026-10-13 on macOS 27.0.1 arm64. Exact base: +`7ee02b7c96d85f22b38d28bd7ed49bb8c1aeb261`. All changes are confined to +`research/dyadic-query-pair/`. The existing PR756/PR805 branches and their +worktrees were not modified. The primary checkout was rechecked at +`4fad623a1e4ca06959f4326e221c2f8d9125c269` on its PR756 branch. + +## Scoped package + +Final `verify.py` replays passed with identical complete committed evidence: + +- CPython **3.13.2**, isolated ordinary replay `python3 -I -B .../verify.py`. +- CPython **3.13.2**, isolated optimized replay and exact regeneration + `python3 -I -O -B .../verify.py --emit /absolute/new/directory`. +- CPython **3.12.14**, `python3.12 -I -O -B .../verify.py`. +- CPython **3.9.6**, `/usr/bin/python3 -I -O -B .../verify.py`. + +All use the standard library only. The committed certificate is compared +as canonical JSON, including every count, stream digest and source binding; +integer/Boolean substitutions are distinct. + +Completed finite coverage: + +- **112** signed dyadic ADDRESS words, indices 0 through 55, with literal + inverses and eight independent rational basis columns: **1,792** columns. + The index-55 check explicitly covers the doubled query of the seed-selected + index-54 pair. Nine odd moduli give **16,128** modular columns. +- **110** signed symbolic pair programs (indices 0 through 54), each with + complete baseline/fused/inverse Laurent VALUE matrices. +- Independent outer-product and literal-matrix catalogues at dimensions 2, + 3, 4 have 6, 28, 120 rank-one projectors. All **91,320** ordered products + with opposite exponents +/-1,+/-2,+/-4 reject the centered target. The + all-dimension/all-power result is the written proof, not this census. +- Full six-field domains have **729 addresses over Z/3** (243 fixed) and + **15,625 over Z/5** (3,125 fixed). The declared parameters in CERTIFICATE + give **154,160 dirty four-role basis columns per program**, with baseline + and fused endpoints checked against a direct coordinate formula, and + **308,320** literal inverse/completed-involution column checks. Two + ADDRESS spectators are fixed at values 1 and 2; their arbitrary-coordinate + identity is separately covered by the rational/modular columns and proof. +- Ten full/shorter/fixed prime-power orbit domains give **7,552** further + basis columns per program and **15,104** inverse/involution checks. + **92** simultaneous nonzero dirty-row cases also pass. +- All **25** declared mathematical/admission controls pass, including + each single ADDRESS/fused event omission, query direction/power/source + errors, source/target aliasing and dirty-spectator destruction. + +`check_package.py` passes on the final certificate under CPython 3.13.2. +Its copied directory contains spaces and has no repository/Git context. +An isolated optimized offline replay passes. All **six** deliberate faults +fail at their declared predicate: immutable source drift, missing source +inventory, integer-zero-to-Boolean substitution, an unpaid child receipt, +central query-power corruption, and implementation/source-binding drift. +Original workspace bytes are not changed by these controls. + +Every one of the **seven** vendored immutable inputs was additionally compared +byte for byte to its fetched pinned Git object. Both Git blob SHA-1 and SHA-256 +checks are performed in every standalone replay. Licenses and notices remain +unchanged. `make selected-record-check` passes for exact conditional kappa +`1661202643272239/1000000000000000000`. Staged whitespace checks pass, and +the diff contains no changes to upstream, certificates, scripts, tests or docs. + +One root `PYTHONDONTWRITEBYTECODE=1 make verify` was run on an **untouched +Git-archive export of the exact base**, so unrelated generated artifacts +did not enter this worktree. Its seven initial historical groups passed: +`verify-community`, `verify-producers`, `verify-partial-gauge`, +`verify-three-stage-cover`, `verify-paired-cube`, `verify-recycled-bit`, +and `verify-entrance-banks`. It then stopped at `gen4-bank-verify`: + +```text +ModuleNotFoundError: No module named 'sympy' +make[1]: *** [gen4-bank-verify] Error 1 +make: *** [verify] Error 2 +``` + +Exit status was 2. No full repository-suite pass is claimed. The selected +PR741 cold replay and subsequent root groups were not reached. The refreshed +PR799 construction was read as publication context; its cold replay was +not run. No dependency installation or source workaround was attempted for +this isolated standard-library contribution. + +## Review boundary + +The executable child denotes the inherited ordinary full-row ADDRESS +interchange contract. The finite evaluator swaps address coordinates to +check its specified permutation; it is not a new recursive supplier or +fixed-tape implementation. The two independently written coordinate/matrix +references are computationally separate methods prepared with the same +substantial AI assistance, not independent human reviews. + +Three queries are sharp only in the stated power-query/XOR model. The work +recurrence is typed: a centered DATA shear invokes ordinary ADDRESS +interchange. It cannot be turned into a self-recursion without an additional +compiler. j-dependent coefficient costs, physical routing/hosting, all-size +padding, actual supplier/assembly invoices and inherited tape/analytic +assumptions remain. No new kappa, runtime benchmark, Linux/remote CI result, +proof-assistant pass or full multiplication theorem is claimed. diff --git a/research/dyadic-query-pair/check_package.py b/research/dyadic-query-pair/check_package.py new file mode 100644 index 0000000000..1b3f2d99d6 --- /dev/null +++ b/research/dyadic-query-pair/check_package.py @@ -0,0 +1,82 @@ +"""Offline relocation and evidence/source corruption checks in temporary copies.""" +import json +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile + +ROOT = Path(__file__).resolve().parent + + +def run(root, success, marker): + completed = subprocess.run([sys.executable, "-I", "-O", "-B", str(root / "verify.py")], + cwd=root.parent, text=True, capture_output=True) + combined = completed.stdout + completed.stderr + if success: + if completed.returncode != 0 or marker not in combined: + raise RuntimeError("relocated replay failed: " + combined[-2000:]) + elif completed.returncode == 0 or marker not in combined: + raise RuntimeError("fault was not rejected at the required predicate: " + combined[-2000:]) + + +def change_json(root, name, mutate): + path = root / name + value = json.loads(path.read_text()) + mutate(value) + path.write_text(json.dumps(value, sort_keys=True) + "\n") + + +def main(): + with tempfile.TemporaryDirectory(prefix="dyadic query pair offline ") as scratch: + root = Path(scratch) / "standalone package with spaces" + shutil.copytree(ROOT, root) + run(root, True, "PASS_DYADIC_QUERY_PAIR") + cases = [] + + def mutate_source(root): + path = root / "vendor/pr521-PROOF.md" + path.write_bytes(path.read_bytes() + b"\nsource drift\n") + + cases.append(("immutable source drift", mutate_source, "source SHA256")) + + def missing_inventory(root): + change_json(root, "SOURCES.json", lambda v: v["immutable_inputs"].pop()) + + cases.append(("source inventory omission", missing_inventory, "complete immutable source inventory")) + + def boolean_count(root): + change_json(root, "CERTIFICATE.json", + lambda v: v["fixture"].__setitem__("private_rows_added", False)) + + cases.append(("integer zero changed to Boolean", boolean_count, "complete CERTIFICATE mismatch")) + + def invoice_count(root): + change_json(root, "CERTIFICATE.json", lambda v: v["fixture"]["fused_invoice"].__setitem__( + "ordinary_children", 2)) + + cases.append(("unpaid child in receipt", invoice_count, "complete CERTIFICATE mismatch")) + + def query_power(root): + change_json(root, "PROGRAM.json", lambda v: v["fused_chronological_events"][2].__setitem__( + 2, 1 << 54)) + + cases.append(("literal central-power corruption", query_power, "literal PROGRAM mismatch")) + + def code_drift(root): + path = root / "program.py" + path.write_bytes(path.read_bytes() + b"\n# implementation drift\n") + + cases.append(("implementation/source binding drift", code_drift, "complete CERTIFICATE mismatch")) + for name, mutate, marker in cases: + pristine = {p.relative_to(root): p.read_bytes() for p in root.rglob("*") if p.is_file()} + mutate(root) + run(root, False, marker) + for path, data in pristine.items(): + (root / path).write_bytes(data) + print("rejected:", name) + print("PASS_DYADIC_PACKAGE_CONTROLS: relocated offline replay and 6 deliberate faults") + + +if __name__ == "__main__": + main() diff --git a/research/dyadic-query-pair/full_domain.py b/research/dyadic-query-pair/full_domain.py new file mode 100644 index 0000000000..fc9c312b11 --- /dev/null +++ b/research/dyadic-query-pair/full_domain.py @@ -0,0 +1,160 @@ +"""Separate finite coordinate/permutation replay of the compiler's words. + +This module does not use the compiler's ADDRESS evaluator or Laurent code. +The expected endpoint comes from the direct s*r^T coordinate formula. +Full-domain coverage is finite evidence, not an implementation on tape. +""" +import hashlib +import itertools +import json +from fractions import Fraction + + +def check(condition, message): + if not condition: + raise RuntimeError(message) + + +def direct_push(address, exponent, modulus): + d = address[0] - address[2] - address[3] + address[5] + step = exponent * pow(4, -1, modulus) * d + result = list(address) + for i, sign in ((0, 1), (2, 1), (3, -1), (5, -1)): + result[i] = (address[i] + sign * step) % modulus + return tuple(result) + + +def literal_push(address, word, modulus): + state = list(address) + for event in word: + if event[0] == "child": + state[event[1]], state[event[2]] = state[event[2]], state[event[1]] + else: + _, target, diagonal, controls = event + check(all(source < target for source, _ in controls), "physical control order") + + def scalar(c): + c = Fraction(c) + return c.numerator * pow(c.denominator, -1, modulus) % modulus + + check(scalar(diagonal) != 0, "nonzero dyadic diagonal") + value = scalar(diagonal) * state[target] + for source, coefficient in controls: + value += scalar(coefficient) * state[source] + state[target] = value % modulus + return tuple(state) + + +def receipt_update(digest, value): + digest.update((json.dumps(value, separators=(",", ":")) + "\n").encode()) + + +def case(compiler, domain, modulus, j, sign, digest): + index = {address: i for i, address in enumerate(domain)} + baseline = compiler.baseline_program(j, sign) + fused = compiler.fused_program(j, sign) + inverse = compiler.inverse_program(fused) + exponents = sorted({event[2] for word in (baseline, fused, inverse) + for event in word if event[0] == "query"}) + permutations = {} + address_cases = 0 + for k in exponents: + word = compiler.address_word(k) + images = [] + for address in domain: + actual = literal_push(address, word, modulus) + expected = direct_push(address, k, modulus) + check(actual == expected, "full-domain literal ADDRESS lowering") + check(actual in index, "domain closure") + images.append(index[actual]) + address_cases += 1 + check(sorted(images) == list(range(len(domain))), "complete ADDRESS bijection") + permutations[k] = tuple(images) + a = sign * (1 << j) + expected_plus = [index[direct_push(z, a, modulus)] for z in domain] + expected_minus = [index[direct_push(z, -a, modulus)] for z in domain] + columns = 0 + for role in range(4): + for position in range(len(domain)): + initial = [set() for _ in range(4)] + initial[role].add(position) + expected = [row.copy() for row in initial] + if role == 1: + expected[0].symmetric_difference_update({expected_plus[position]}) + expected[0].symmetric_difference_update({expected_minus[position]}) + actual = [row.copy() for row in initial] + old = [row.copy() for row in initial] + compiler.run_bits(actual, fused, permutations) + compiler.run_bits(old, baseline, permutations) + check(actual == expected and old == expected, "complete dirty BIT column") + receipt_update(digest, [modulus, j, sign, role, position, + [sorted(row) for row in actual]]) + compiler.run_bits(actual, inverse, permutations) + check(actual == initial, "literal inverse restores dirty BIT column") + compiler.run_bits(old, fused, permutations) + check(old == initial, "completed DATA involution") + columns += 1 + # Simultaneous nonzero dirt in all four roles, with no clean private promise. + initial = [{i for i in range(len(domain)) if (53 * i + 17 * role + 54) % 7 < 3} + for role in range(4)] + expected = [row.copy() for row in initial] + for position in initial[1]: + expected[0].symmetric_difference_update({expected_plus[position]}) + expected[0].symmetric_difference_update({expected_minus[position]}) + actual = [row.copy() for row in initial] + compiler.run_bits(actual, fused, permutations) + check(actual == expected, "simultaneously dirty full rows") + compiler.run_bits(actual, inverse, permutations) + check(actual == initial, "simultaneously dirty restoration") + return address_cases, columns + + +def evidence(compiler): + digest = hashlib.sha256() + full_address = full_columns = full_cases = 0 + full_domains = [] + for modulus, parameters in ((3, [(j, sign) for j in (0, 1, 2, 5, 54) + for sign in (-1, 1)]), + (5, [(0, 1), (54, 1)])): + domain = [tuple(z) + (1, 2) for z in itertools.product(range(modulus), repeat=6)] + fixed = sum(direct_push(z, 1, modulus) == z for z in domain) + full_domains.append({"modulus": modulus, "six_field_addresses": len(domain), + "fixed_addresses": fixed, "two_spectator_values": [1, 2], + "j_sign_parameters": parameters}) + for j, sign in parameters: + address, columns = case(compiler, domain, modulus, j, sign, digest) + full_address += address + full_columns += columns + full_cases += 1 + orbit_address = orbit_columns = orbit_cases = 0 + lengths = [] + # Include full-order, nonunit shorter, and fixed orbits in odd prime powers. + for modulus, scale in ((5, 1), (25, 1), (25, 5), (49, 1), (49, 7), + (121, 1), (121, 11), (27, 3), (9, 3), (11, 0)): + start = (scale, 0, 0, 0, 0, 0, 7 % modulus, 8 % modulus) + orbit = [start] + image = direct_push(start, 1, modulus) + while image != start: + check(image not in orbit and len(orbit) < modulus, "orbit stopping rule") + orbit.append(image) + image = direct_push(image, 1, modulus) + lengths.append([modulus, scale, len(orbit)]) + for j in (0, 1, 5, 54): + for sign in (-1, 1): + address, columns = case(compiler, orbit, modulus, j, sign, digest) + orbit_address += address + orbit_columns += columns + orbit_cases += 1 + return {"full_domains": full_domains, + "full_parameter_cases": full_cases, + "full_address_query_cases": full_address, + "full_dirty_basis_columns_per_program": full_columns, + "full_inverse_and_involution_columns": 2 * full_columns, + "orbit_modulus_scale_lengths": lengths, + "orbit_parameter_cases": orbit_cases, + "orbit_address_query_cases": orbit_address, + "orbit_dirty_basis_columns_per_program": orbit_columns, + "orbit_inverse_and_involution_columns": 2 * orbit_columns, + "simultaneously_dirty_cases": full_cases + orbit_cases, + "endpoint_stream_encoding": "canonical-json-lines-v1", + "endpoint_stream_sha256": digest.hexdigest()} diff --git a/research/dyadic-query-pair/program.py b/research/dyadic-query-pair/program.py new file mode 100644 index 0000000000..7db5972e26 --- /dev/null +++ b/research/dyadic-query-pair/program.py @@ -0,0 +1,131 @@ +"""Literal native BIT query-pair compiler; all VALUE additions are XOR. + +ADDRESS scalings use exact rationals, specialized only to odd residue rings. +The child event denotes one full-row ordinary ADDRESS interchange. This +reference compiler does not implement or time the inherited tape primitive. +""" +from fractions import Fraction + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def power(j, sign=1): + require(type(j) is int and j >= 0, "nonnegative integer dyadic index") + require(type(sign) is int and sign in (-1, 1), "integer sign") + return sign * (1 << j) + + +def address_word(k): + """Seven events for M(k)=I+(k/4)s r^T; k is a signed power of two.""" + require(type(k) is int and k != 0 and abs(k) & (abs(k) - 1) == 0, + "nonzero signed dyadic power") + a = Fraction(k, 4) + return ( + ("affine", 2, Fraction(1), ((0, Fraction(-1)),)), + ("affine", 3, Fraction(1), ((0, Fraction(1)),)), + ("affine", 5, a, ((0, 1 + a), (2, -a), (3, -a))), + ("child", 0, 5), + ("affine", 2, Fraction(1), ((0, Fraction(1)),)), + ("affine", 3, Fraction(1), ((0, Fraction(-1)),)), + ("affine", 5, -1 / a, ((0, 1 / a - 1), (2, Fraction(1)), + (3, Fraction(1)))), + ) + + +def inverse_word(word): + result = [] + for event in reversed(word): + if event[0] == "child": + result.append(event) + else: + _, target, diagonal, controls = event + result.append(("affine", target, 1 / diagonal, + tuple((i, -c / diagonal) for i, c in controls))) + return tuple(result) + + +def run_address(address, word, modulus=None): + """Execute the literal events, with optional full spectator coordinates.""" + require(len(address) >= 6, "six ADDRESS fields") + if modulus is None: + reduce = Fraction + state = list(map(Fraction, address)) + else: + require(type(modulus) is int and modulus >= 3 and modulus % 2 == 1, + "odd residue modulus at least three") + require(all(type(x) is int for x in address), "integer residue coordinates") + + def reduce(value): + value = Fraction(value) + return value.numerator * pow(value.denominator, -1, modulus) % modulus + + state = [x % modulus for x in address] + for event in word: + if event[0] == "child": + _, first, last = event + state[first], state[last] = state[last], state[first] + else: + _, target, diagonal, controls = event + state[target] = reduce(diagonal) * state[target] + sum( + reduce(c) * state[i] for i, c in controls) + if modulus is not None: + state[target] %= modulus + return tuple(state) + + +def fused_program(j, sign=1): + a = power(j, sign) + return (("query", 0, -a), ("xor", 0, 1), ("query", 0, 2 * a), + ("xor", 0, 1), ("query", 0, -a)) + + +def baseline_program(j, sign=1): + a = power(j, sign) + return (("query", 0, -a), ("xor", 0, 1), ("query", 0, a), + ("xor", 0, 1), ("query", 0, a), ("xor", 0, 1), + ("query", 0, -a), ("xor", 0, 1)) + + +def inverse_program(program): + return tuple(("query", event[1], -event[2]) if event[0] == "query" + else event for event in reversed(program)) + + +def invoice(program): + queries = [event[2] for event in program if event[0] == "query"] + words = [address_word(k) for k in queries] + return {"ordinary_children": len(queries), + "ordered_affine_events": sum(sum(e[0] == "affine" for e in w) + for w in words), + "aligned_xor_scans": sum(e[0] == "xor" for e in program), + "persistent_private_rows": 0, + "query_powers": queries, + "child_volume_fraction_each": "1/3", + "child_width_fraction_each": "1/3"} + + +def run_bits(rows, program, permutations): + """Sparse exact finite-array evaluator, mutating distinct dirty row sets. + + permutations[k][i] is the literal ADDRESS push map for the entire finite + domain. No copying, erasure, or clean-row initialization is a program event. + Python's simulator storage is not a physical tape/workspace measurement. + """ + require(type(rows) is list and len(rows) >= 3, "three DATA rows") + require(all(type(row) is set for row in rows), "mutable BIT position sets") + require(len({id(row) for row in rows}) == len(rows), "distinct physical rows") + for event in program: + if event[0] == "query": + _, row, k = event + permutation = permutations[k] + replacement = {permutation[i] for i in rows[row]} + rows[row].clear() + rows[row].update(replacement) + else: + _, target, source = event + require(target != source, "distinct XOR source and target") + rows[target].symmetric_difference_update(rows[source]) + return rows diff --git a/research/dyadic-query-pair/vendor/pr521-PROOF.md b/research/dyadic-query-pair/vendor/pr521-PROOF.md new file mode 100644 index 0000000000..c3f67fc807 --- /dev/null +++ b/research/dyadic-query-pair/vendor/pr521-PROOF.md @@ -0,0 +1,183 @@ +# Exact local fusion and paid implementation + +The tape-operation premises come from the original +[ordered affine streams lemma](https://github.com/CrocSwap/integer-mult-bounds/blob/5996e33ecad6a0ccd578aec58831457829d75575/upstream/build/sections/02-streams.tex) +and [address interchange construction](https://github.com/CrocSwap/integer-mult-bounds/blob/5996e33ecad6a0ccd578aec58831457829d75575/upstream/build/sections/04-swap.tex) +of CrocSwap/integer-mult-bounds, pinned at the displayed revision. +The general rank-one lowering, selected unipotent operator and dirty +shared-chart fusion in this packet are a separate contribution. +Source pins distinguish that contribution from the borrowed tape contracts. + +## ADDRESS operator + +Use six physically ordered fields `(H0,H1,H2,D0,D1,D2)`, each of width +`b=N/3`. Each coordinate lies in the true residue ring `Z/(ell^b)`, where +ell is any odd prime. Unnamed ADDRESS fields may occur between or outside +these fields and remain spectators. Set + +``` +u = (1,0,1), t = (1,0,-1), t^T u = 0, +g = I3 + (1/2) u t^T, +g^-1 = I3 - (1/2) u t^T, +s = (u,-u), r = (t,-t), +Phi(g) = I6 + (1/4) s r^T. +``` + +The lift preserves H+D and applies g to H-D; H1 and D1 are fixed. +Since `(u t^T)^2=0`, the displayed inverse is exact. The map is not an +involution over the rationals or any odd residue ring. These are rational +ADDRESS operations specializing to residue rings, not signed arithmetic +on stored VALUE bits. + +The following chronological seven-event word equals Phi(g): + +``` +z2 <- z2-z0 +z3 <- z3+z0 +z5 <- (z5+5*z0-z2-z3)/4 +CHILD_C(0,5) +z2 <- z2+z0 +z3 <- z3-z0 +z5 <- -4*z5+3*z0+z2+z3 +``` + +Every affine control precedes its target. `CHILD_C(0,5)` is one ordinary +recursive interchange of the selected equal-width fields on the COMPLETE +private BIT stream; it preserves all other ADDRESS fields. It is a +contract invocation, not an implementation of the recursive supplier in +this packet. The affine operations use the original ordered-stream +contract, including its work tapes and head returns. Subject to those +contracts and their row/stack hypotheses, this is a fixed all-b local +implementation with six affine scans, one child and O(V) additional work. +There is no exponential array enumeration in the implementation. + +For completeness, the lowering formula is independently checked. For +`M=I+s v^T`, let `D=1+v^T s` and `a=s0*vlast`, both nonzero. Subtract +`(si/s0)z0` from each middle coordinate. Then set + +``` +zlast <- a*zlast+(D-slast*vlast)*z0+sum_middle s0*vi*zi, +swap(z0,zlast), +zi <- zi+(si/s0)*z0 for each middle coordinate, +zlast <- (-D/a)*zlast+((D-s0*v0)/a)*z0 + -sum_middle (vi/vlast)*zi. +``` + +Substitution gives M on every input coordinate. Here `v=r/4`, D=1 and +a=1/4, and only middle indices 2 and 3 need updates. Thus the formula +emits exactly the word above. The checker derives it afresh and verifies +its rational matrix. The literal reverse inverts each affine unit and +uses the same involutive child; its matrix is Phi(g^-1), not Phi(g). + +The denominators and affine diagonal numerators exclude only prime 2. +For example, a control coefficient vanishing modulo 5 does not make a +diagonal singular. This proves specialization for every odd ell and b, +including composite rings such as Z/25 and Z/49. Removing only the child +while retaining the affine wrappers changes the operator. + +## Exact comparison and native dirty chart + +Let `P=u*(1/2,0,1/2)` and `Q=u*(3/4,0,1/4)` denote outer products. +Both row pairings with u are 1, so P and Q are idempotents; Q need not be +orthogonal. Write `R_P=I-2P` and `R_Q=I-2Q`. Since PQ=Q, + +``` +R_P R_Q = I+2(Q-P) = g. +``` + +Chronologically apply Q first, then P. `PROGRAM.json` gives a separate +six-affine/one-child word for each lifted reflection. Their full matrix +product, including spectator coordinates, equals the fused word. + +For three genuine BIT DATA rows `(x1,x2,x3)` and retained private row q, +all with the same full ADDRESS domain, use this fixed chart: + +``` +q XOR= x2 +x1 XOR= q +h(q) # array permutation induced by Phi(h) +x1 XOR= q +q XOR= x2 +``` + +Write its complete linear BIT operator as H(h). Its endpoint on arbitrary +dirty inputs is + +``` +x1' = x1 XOR q XOR x2 XOR h(q) XOR h(x2), +q' = h(q) XOR x2 XOR h(x2), +x2' = x2, x3' = x3. +``` + +Equivalently, with `E=(e1+eq)(e2^T+eq^T)` over F2, E^2=E and +`H(h)=I+E tensor(h-I)`. Hence H(h2)H(h1)=H(h2 h1) for arbitrary arrays, +and in particular `H(R_P)H(R_Q)=H(g)`, including arbitrary initial q. +This proof does not assume a clean private row. There is no F9 codec, +padding promise or signed integer VALUE lift. + +The adjacent decoder and encoder in the specified two-reflection baseline +cancel exactly. That baseline already has FOUR XOR scans around its two +ADDRESS queries. The fused word also has four. The verified improvement +is two specified recursive children reduced to one; there is no separate +XOR saving. Twelve baseline affine events is its literal serialized +count before possible affine simplification. Neither affine nor child +optimality is claimed against other possible implementations. + +## Orientation, spectators and recovery controls + +For modulus m=ell^b and seed e_H0, the orbit is +`z_k=e_H0+(k/4)s`, indexed by Z/m. It has exactly m points because 1/4 +and a component of s are units. Phi(g) pushes address index k to k+1; +its array permutation reads old VALUE index k-1. The inverse reads k+1. +The reflection address maps are Q: `k -> -3-k` and P: `k -> -2-k`. +Their chronological composition pushes k to k+1, as required. + +The checker applies the actual words to these actual addresses at m=5, +25,7,49. It verifies all six ADDRESS basis columns and unchanged exterior +spectators, as well as H1/D1. On these orbits it checks all 4m dirty BIT +basis columns, 344 total, plus m VALUE spectator columns, 86 total. Each +dirty column agrees with the formula, the full two-stage word and the +chart-cancelled baseline; the literal inverse restores its input. +BIT linearity gives all assignments on each tested orbit, while the +algebraic operator identity above covers arbitrary arrays on the full +ADDRESS domain. Fixed points and their 16 four-role BIT assignments are +also checked. Replacing the WHOLE query by identity gives H(I)=I; +this differs from removing only the recursive child. + +At m=5 start with x2 a delta at index 0 and x1=x3=q=0. The forward module +gives `x1=q=[1,1,0,0,0]`. Its proper retained-q inverse restores all rows. +If q is wiped first, that inverse instead gives +`x1=[0,1,0,0,1]`, `q=[1,0,0,0,1]`: DATA is lost. Using g again as the +inverse also fails. These are explicit negative controls, not a claim +that private state can be reset between uses. + +## Paid state and limits + +Take V as the productive volume of the three genuine DATA streams. +Private q has full volume V/3, including all spectator ADDRESS ranges. +Persistent stock is 4V/3 before evaluator routing, parking, work-tape or +recursion scratch. Initially zeroing fresh q costs V/3. Each fused module +pays one separate child of actual volume V/3 and width N/3, six ordered +ADDRESS affine events, four native XOR scans, setup and head-return work. +The specified cancelled baseline pays two such children and the same +four XOR scans. Each actual separate child call must remain separately +charged in a future supplier recurrence. + +The component identity is valid with dirty q, but an enclosing DATA +construction starting from clean q must allocate and initialize it. +Its state is retained through every future use and recovery. A once-only +final wipe costs V/3 and is eligible only after a separately verified +completed DATA endpoint and the last read of q. This unfinished module +boundary does not license that wipe. No DATA row is cleared for free. + +The half-integral g is outside an odd-denominator mod-4 generator grammar; +the old rho4 construction is undefined on it. This does not invalidate +that construction on its own alphabet and cannot be priced by extending +it without a new proof. + +The packet supplies one exact local query fusion. It does not produce a +complete three-DATA cyclic-interchange c word, a complex C supplier, a +common cover/owner schedule or an all-size weighted-row compiler. Those +missing endpoints and schedules, both suppliers, all separate calls, +movement, dirty recovery and paid stock must be verified before deriving +an integer-multiplication exponent. No kappa improvement is asserted. diff --git a/research/dyadic-query-pair/vendor/pr521-SOURCE-PINS.json b/research/dyadic-query-pair/vendor/pr521-SOURCE-PINS.json new file mode 100644 index 0000000000..549b87c2d5 --- /dev/null +++ b/research/dyadic-query-pair/vendor/pr521-SOURCE-PINS.json @@ -0,0 +1,31 @@ +{ + "public_contract_sources": [ + { + "repository": "CrocSwap/integer-mult-bounds", + "revision": "5996e33ecad6a0ccd578aec58831457829d75575", + "path": "upstream/build/sections/02-streams.tex", + "git_blob": "088fceea1867abc76271d7efe7532b779fee9039", + "sha256": "606c80db61cad13aa0c3b6060dc4b88dbbe7ac60cdd831aa93f28d908fd09dab", + "url": "https://github.com/CrocSwap/integer-mult-bounds/blob/5996e33ecad6a0ccd578aec58831457829d75575/upstream/build/sections/02-streams.tex", + "used_contract": "Ordered affine streams with earlier controls, rational units, spectator fields and paid tape preparation/head returns." + }, + { + "repository": "CrocSwap/integer-mult-bounds", + "revision": "5996e33ecad6a0ccd578aec58831457829d75575", + "path": "upstream/build/sections/04-swap.tex", + "git_blob": "951e792b1768e6509561380b8bbfb1d1ccb64c08", + "sha256": "412b170ccaab38dba96e95e3cbfae09f4876a9818f8d278776a746b0f8044906", + "url": "https://github.com/CrocSwap/integer-mult-bounds/blob/5996e33ecad6a0ccd578aec58831457829d75575/upstream/build/sections/04-swap.tex", + "used_contract": "One ordinary equal-width recursive ADDRESS interchange preserves spectators; each actual invocation is separately paid under its row/stack hypotheses." + } + ], + "source_readback": "Public source excerpts and exact Git blob identities read through the GitHub connector at the pinned revision; full SHA256 values independently match the local pinned source copies.", + "contribution": "Selected rational rank-one unipotent lowering and full-dirty native shared-chart fusion of the specified reflection pair; no complete supplier or exponent claim.", + "prior_exact_verification_provenance": { + "description": "Before this standalone extraction, separate exact algebra, physical-program and paid-cost checks agreed. The opaque hashes below identify that prior verification, but its internal files are neither distributed nor dependencies. This packet checks all admitted claims from its own public files.", + "independent_algebra_checkpoint_sha256": "4fa63459e3fc7b48daf1b6cbdbccbe5d09951da39e6805ce697a95455594e1b8", + "independent_fusion_gate_sha256": "2c47e97c62e169161b126e1faf4757759cf2b159f0d88e0e654ba9a6814c6d5e", + "physical_program_checkpoint_sha256": "408f22a6669ebad10f433c448cc01dcdac281177d35a4f7f82c7450c1066bd9d", + "paid_cost_checkpoint_sha256": "5532473f8094d6c0ddda273a865387c5b64582429e279face9ccf1e2ce27c628" + } +} diff --git a/research/dyadic-query-pair/vendor/pr677-NOTICE.md b/research/dyadic-query-pair/vendor/pr677-NOTICE.md new file mode 100644 index 0000000000..bbd90a76bb --- /dev/null +++ b/research/dyadic-query-pair/vendor/pr677-NOTICE.md @@ -0,0 +1,39 @@ +# Attribution, license, and scope + +New prose and checker code in this packet are contributed under the +repository's Apache-2.0 license. The repository's LICENSE and NOTICE remain +unchanged. Submitted by @commdata2338. Prepared with substantial AI assistance: +OpenAI Codex (GPT-6-Astra) wrote the analysis, proof and checker, and +Claude Code (Claude Opus 5.5) packaged the submission. No independent +human peer review is claimed. + +- **Karl Appel / applecrusher, PR #521**, head + `a190fdb39f31647fc6f651625353710624627348`: the rank-one unipotent ADDRESS + map, its seven-event lowering, the reflected-query comparison, and the + dirty shared-chart operator. The ADDRESS word in PROGRAM.json is an + attributed transcription. The completed shear contracts, two-query + classification, cost comparison and fresh checker are this contribution. +- **OpenAI #109 / the imported upstream framework**: ordered-affine streams, + complete-range ordinary ADDRESS interchange, tape/stack and head-return + contracts. The two original sources at revision + `5996e33ecad6a0ccd578aec58831457829d75575` match the files in this base; + exact URLs and SHA-256 values are recorded in SOURCES.json. Their licenses + and repository notices are retained, and their interfaces remain premises. +- **eumemic, PR #288**, head + `475a088b5862f75f0b10596cfd6842d19531a5ec`, and **Ali Romman, PR #468**, + the in-tree `research/bit-three-register-lower-bound` package: the binary + scalar-projector/group-algebra model used for other interchange targets. + This packet credits that model and does not repeat the nine-call search. +- **Joseph Demarest, PR #83**, head + `183077b7b3ae12e96eb3a87c1dc08023e6494dca`: the scoped fixed-menu adaptive + recursion barrier, inspected when selecting this task. We do not claim + that rescheduling complete supplier profiles changes their best exponent. +- The selected #626/#622/#623 construction, #543 bit supplier, and cumulative + community authors retain their attribution. Their selected artifacts are + neither changed nor re-certified by this local note. + +No priority claim is made for the elementary compute/uncompute identities, +matrix determinant lemma, or Laurent-polynomial methods. The useful output +is the pinned component's explicit restored-boundary alternatives, their +precise model restrictions and paid recurrence, and exact reproducible +evidence for review. diff --git a/research/dyadic-query-pair/vendor/pr677-PROOF.md b/research/dyadic-query-pair/vendor/pr677-PROOF.md new file mode 100644 index 0000000000..47d9bf59a3 --- /dev/null +++ b/research/dyadic-query-pair/vendor/pr677-PROOF.md @@ -0,0 +1,383 @@ +# Restored boundaries for one native unipotent BIT query + +This is a local interface result, conditional on the cited ordinary ADDRESS +interchange and ordered-stream primitives. It supplies no complete interchange +supplier and no multiplication exponent. The algebra below proves the stated +identities and scoped query bounds; the finite checker is corroboration, not a +formal proof of a full multiplication theorem. + +## 1. Object, predecessor, and boundary contracts + +Karl Appel / applecrusher's [PR #521](https://github.com/CrocSwap/integer-mult-bounds/pull/521), +pinned at `a190fdb39f31647fc6f651625353710624627348`, replaces two particular +reflected queries by one unipotent query. Its complete dirty operator retains +a private BIT row. It explicitly does not complete a DATA interchange or +authorize erasure of that row at an unfinished boundary. Its result is not +contradicted here. + +We choose a different, modest completed endpoint. For three genuine DATA rows +`(x,y,z)` and one fixed ADDRESS permutation `h`, let + + S_h(x,y,z) = (x + (h+I)y, y, z). (1) + +All VALUE additions in this note are XOR, over F2. ADDRESS arithmetic below +is rational arithmetic specialized to odd prime-power residue rings; these +two coefficient systems must not be conflated. Equation (1) is a shear, +not the three-DATA interchange. It satisfies `S_h^2 = I`, even though +`h^2 != I`. + +The contribution is an explicit comparison of three ways to complete (1): + +| Contract | Queries `h` or `h^-1` | Additional full row | Endpoint for that row | +|---|---:|---:|---| +| Query the DATA target | 2 | none | All other dirty rows untouched | +| Queries remain on one private row, with triangular source/target XORs | 4 | one | Arbitrary initial private contents restored | +| Caller owns disposable private storage | 1 | one | Explicit copy initialization and final zeroing | + +The first count is optimal in the fixed-`h` query/XOR model of section 4. +The second is optimal in the narrower private-row model of section 5 for +a uniform all-width program. These are **not** lower bounds for arbitrary +ordinary-interchange programs with different free ADDRESS operations. +The third changes the workspace contract: discarding someone else's dirty +row is not allowed. Its successful DATA endpoint makes its *own* final clear +legitimate. It is not evidence that clearing PR #521's private row is safe +inside an arbitrary surrounding construction. + +## 2. The retained query, with its actual recursive child + +Fix an odd prime `ell`, `b >= 1`, and `m = ell^b`. Use six ordered ADDRESS +fields `(H0,H1,H2,D0,D1,D2)`, all of width `b`, and all complete spectator +ranges. Define + + s = (1,0,1,-1,0,-1)^T, + r = (1,0,-1,-1,0,1)^T, + M = I6 + s r^T / 4, M^-1 = I6 - s r^T / 4. + +Here `r^T s = 0`. The permutation `h` moves the BIT at ADDRESS `a` to `M a`; +its action on values reads the inverse ADDRESS image. PR #521's literal +lowering, transcribed in `PROGRAM.json`, is + + a2 -= a0 + a3 += a0 + a5 = (a5 + 5*a0 - a2 - a3)/4 + CHILD_C(a0,a5) + a2 += a0 + a3 -= a0 + a5 = -4*a5 + 3*a0 + a2 + a3. (2) + +Substitution gives `M`. Reversing (2) and inverting each scalar event gives +`M^-1`. The child is an ordinary interchange of two `b`-digit ADDRESS fields +on the **entire selected BIT row**, including all other ADDRESS fields. +It is not a pointwise VALUE swap or an uncharged oracle. + +All six affine events read only earlier fields. Their diagonal numerators +and denominators are powers of two up to sign; denominators of controls are +also powers of two. Thus every event is well defined for every odd `ell`. +The cited ordered-stream lemma pays the finite coefficient preparation, +counter work, complete spectator scans, temporary work and head returns. +It does not assume unit-cost arithmetic on growing integers. + +The same implementation works on a DATA row or a private row: the ADDRESS +primitive's contract is for arbitrary BIT contents and is insensitive to +the role's name. Calls must be sequential and have exclusive access to the +queried row until its completed boundary. No source chart or current supplier +schedule is asserted to provide that permission automatically. + +For `a0 = e_H0`, the addresses `a_k = e_H0 + k*s/4`, `k in Z/m`, are distinct +and satisfy `M a_k = a_(k+1)`. Hence on their VALUE array, `(h y)_k = y_(k-1)`. +This supplies a nontrivial orbit of order `m`, as well as a direct finite +check on push/read orientation. There are also fixed points and shorter +orbits at nonunit initial scales; these are included in the replay. + +## 3. Three complete programs + +### 3.1 No full private row + +Apply, chronologically, + + x <- h^-1 x + x += y + x <- h x + x += y. (3) + +The output is `x + h y + y`; `y,z` and every unrelated row are untouched. +No row is assumed zero, copied, or erased. A pre-existing private row is +an untouched spectator. Source `y` is never modified, even temporarily. +The queried target may be permuted temporarily, so callers may not inspect +it between events. This is a restored boundary, not a concurrently readable +intermediate representation. + +### 3.2 Queries only on a restored dirty private row + +For arbitrary initial `q=q0`, use + + q += y + q <- h q + x += q + q <- h^-1 q + q += y + q <- h q + x += q + q <- h^-1 q + x += y. (4) + +The two contributions read into `x` are `h(q0+y)` and `h q0`. Their sum is +`h y`. The last XOR supplies `y`; both query/inverse pairs restore their +own input, and the two source XORs restore `q0`. Thus (4) implements (1) +on DATA and the identity on arbitrary private input. It has four queries +and five XORs, not four queries plus an implicit cleanup. + +### 3.3 An owned, disposable private row + +Allocate or reserve one owned full row `q`, whose incoming contents may be +discarded, and use + + q <- copy(y) + x += y + q <- h q + x += q + q <- 0. (5) + +The copy overwrites every private cell and pays source access and +initialization in one scan. Just before the last line, DATA already equals +(1), and `q=h y` is redundant with retained `y`. No later step reads `q`. +The final full-row clear therefore returns owned work storage to zero. +All five events are charged. There is no assumption that unknown dirty +caller state can be thrown away. + +Reapplying the *completed* program (5) implements `S_h^2=I` on DATA. This is +different from applying the inverse of PR #521's unfinished dirty module +after clearing its private row; that inverse generally fails. Both facts +are checked, including arbitrary DATA inputs and explicit private-input +rejection when (5) is falsely labeled a dirty-restoring program. + +The normal form of PR #521's dirty module is +`H(h)=I+E(h-I)`, `E=(e_x+e_q)(e_y+e_q)^T`. It directly explains the +tradeoff: for initial `q=0`, its DATA output is already (1), but its private +output is `(h+I)y`. Once (1) is declared and verified as the desired complete +endpoint, terminal operations needed solely for later dirty-module recovery +can be removed. Program (5) is the simpler paid copy implementation of that +completed endpoint. It changes neither the predecessor's two-reflection +identity nor its warning about other unfinished endpoints. + +## 4. Sharp two-query classification with arbitrary dirty spectators + +The model permits any number `d >= 2` of arbitrary dirty rows. Free algebraic +operations are invertible, address-independent XOR maps of the row roles; +actual implementations still pay for these scans. A query applies `h` or +`h^-1` to one row. No other nontrivial ADDRESS map, copying into clean storage, +or erasure is free in this lower-bound model. + +Represent `h` by `t`. Work over `F2[t,t^-1]`, or over +`F2[t,t^-1]/(t^m-1)` for an odd orbit length `m >= 3`. In the latter ring, +zero divisors cause no problem: the proof uses determinants and comparison +of distinct basis coefficients, not division or a fraction field. + +On an `m`-cycle, identify a BIT row with `sum_k value_k t^k`. The query is +multiplication by `t` on the regular module of the cyclic ring. Thus equality +of these row operators is equivalent to entrywise equality of their matrices +over that ring. The determinant below is taken **in this ring**, not the +ordinary F2 determinant of the expanded bit matrix. Restricting a complete +array to the full-order orbit in section 2 gives a necessary condition for +any claimed full-array identity. + +After conjugation by an invertible binary row map, one query is + + D_P(t^e) = I + (t^e-1) P, e in {+1,-1}, + P = u v^T, v^T u = 1. (6) + +These are precisely binary rank-one idempotents. Any arbitrary interleaving +of free XOR maps normalizes to a product of such factors: commute the +constant maps to the left, conjugating each projector as they pass. +At `t=1`, the desired endpoint is `I`, so the remaining constant factor +must be `I`. Thus allowing arbitrary endpoint XOR maps does not omit a +one-query or two-query solution from this model. + +Let `N=a b^T` be a nonzero rank-one nilpotent, `b^T a=0`; the desired shear is + + T_N(t) = I + (t-1) N. (7) + +The determinant lemma, valid over each stated commutative ring, gives +`det D_P(t^e)=t^e` and `det T_N(t)=1`. Zero queries cannot give the nonconstant +(7). One query has the wrong determinant. Two queries of the same sign also +have the wrong determinant, since `t^2 != 1` on an odd orbit of length at +least three. Therefore any two-query solution has opposite signs. + +For left sign `+1`, expand the product *in operator order*: + + D_P(t) D_Q(t^-1) + = I+P+Q + t(P+PQ) + t^-1(Q+PQ). (8) + +The coefficients of `1,t,t^-1` are independent in either ring, so (8) +equals (7) **if and only if** + + PQ=Q, P+Q=N. (9) + +For the other sign order the exact conditions are + + PQ=P, P+Q=N. (10) + +This is an exhaustive classification, not just a necessary filter. In (9), +the two rank-one images coincide and equal the image of `N`. Consequently + + P=a c^T, Q=a(c+b)^T, c^T a=1. (11) + +In (10), the two row spaces coincide and equal the row space of `N`, giving + + P=(c+a)b^T, Q=c b^T, b^T c=1. (12) + +Conversely, (11) or (12) directly verifies the corresponding conditions. +Over F2 there is no nontrivial scalar rescaling of a rank-one decomposition. +Each family has `2^(d-1)` choices, so every nonzero rank-one nilpotent target +has exactly `2^d` ordered, signed two-query factorizations. Program (3) +realizes one of them for `N=e_x e_y^T`, proving the two-query minimum. + +For any private index `q` distinct from `x,y`, all these factorizations have +`P_qq=Q_qq=0`: in (11) the image is `e_x`, and in (12) the row space is +`e_y^T`. This observation separates the unrestricted dirty-row model from +the private-only contract below. + +The scalar-projector/group-algebra method is established predecessor work: +eumemic's PR #288 and Ali Romman's in-tree `bit-three-register-lower-bound` +package (PR #468) use it for different diagonal interchange targets. We do +not claim that method as new. The present two-query classification targets +one off-diagonal restored shear and includes finite cyclic rings explicitly. + +## 5. Why the private-only dirty boundary costs four queries + +Here queries are restricted to `q`; the allowed pointwise gates are +`q += y`, `x += q`, and `x += y`. Source `y` and spectator rows remain +unchanged. A free-gate prefix has the triangular form + + K(x,y,q) = (x + a q + b y, y, q + c y). + +Both `K` and `K^-1` have `qq` entry one. A normalized query projector +`K^-1 e_q e_q^T K` therefore has `P_qq=1`. Section 4 shows that no +two-query factorization of (1) can have that property. A one-query program +is already excluded. A three-query program has determinant `t^j` for +`j in {-3,-1,1,3}`, so cannot have determinant one in the Laurent model, +or on an odd orbit of length at least five. Thus a uniform all-width +program needs at least four queries. Program (4) attains four. + +This proof does not assert a separate three-query exclusion for one isolated +order-three quotient from the determinant alone. The formal finite-word +check below is over Laurent coefficients, not modulo three. The uniform +claim has no gap: for example the actual order-eleven orbit already gives +the stated lower bound, and the program must work at that width too. + +Arbitrary XOR maps that swap a DATA role with `q`, arbitrary alternate +ADDRESS maps, non-restored private state, and clean/disposable storage are +outside this private-only restriction. Removing any of those restrictions +requires a new analysis; program (3) deliberately changes the first one. + +## 6. Complete typed costs and workspace + +Let each genuine DATA row have logical BIT volume `U`, including the full +ADDRESS domain and all spectators. Productive volume is `V=3U`, and nominal +chunk width is `N=3b`. Let: + +- `C(U,b)` be the cost of one ordinary interchange of the selected two + `b`-digit fields on a complete row of volume `U`, with restored child work; +- `A(U,b)` bound each fixed ordered-affine event of (2), including coefficient + preparation, its source access, temporary work, and head returns; +- `X(U)`, `P(U)`, and `Z(U)` bound one aligned XOR, full copy, and full clear; +- `R_j(V,b)` include row split/merge, routing to the fixed evaluator tapes, + descriptor setup, parking and recovery, allocation if needed, and head + returns not already charged in a primitive. Each `R_j=O(V)` under the + inherited complete-range, fixed-number-of-rows, and stack contract. + +The complete local recurrences/charges are + + S_data(V,3b) <= 2 C(U,b) + 12 A(U,b) + 2 X(U) + R_data(V,b), + S_dirty(V,3b) <= 4 C(U,b) + 24 A(U,b) + 5 X(U) + R_dirty(V,b), + S_owned(V,3b) <= C(U,b) + 6 A(U,b) + 2 X(U) + + P(U) + Z(U) + R_owned(V,b). (13) + +Every query is lowered using (2), so there are exactly 2, 4, and 1 ordinary +recursive children respectively, all of actual volume `V/3` and width `N/3`. +There is no dropped recovery child, additional live query, or implicit +source-copy oracle. All children run sequentially and reuse restored child +workspace. Primitive affine work may itself use temporary streams; those +are covered by `A`, not claimed absent by the phrase "no private row." + +Under the cited streaming contracts, the non-child terms of (13) are `O(V)`. +If `c(b)` uniformly bounds `C(U,b)/U`, then + + s_data(3b) <= (2/3)c(b) + O(1), + s_dirty(3b) <= (4/3)c(b) + O(1), + s_owned(3b) <= (1/3)c(b) + O(1). (14) + +The constants are independent of `b,U`, for a fixed permitted radix and +the fixed literal program. Fractions count the **actual child stream +volumes**, not the persistent stock. Persistent role storage is `V` for +(3), and `4V/3` for (4) and (5), before primitive/evaluator/recursive scratch. +For peak workspace, let `B_j(V,b)` include the fixed streaming and parking +workspace and `W_C(U,b)` child workspace. A safe bound is + + W_j(V,3b) <= persistent_j(V) + B_j(V,b) + W_C(U,b), + persistent_data=V, persistent_dirty=persistent_owned=4V/3. + +`B_j=O(V)` under the same tape primitives; the bound pays their temporary +streams and does not claim an exact number of physical tapes or total cells. +Private-row allocation is not normalized away. In the owned case the initial +copy and final clear are charged on every invocation, even if a later caller +could establish safe reuse. + +These are **typed** recurrences: the left side is a DATA shear and `C` is +ordinary ADDRESS interchange. Substituting `S_data` for `C` and solving a +self-recursion would be circular without a separate compiler. No such +compiler, arbitrary-width padding, common-frame schedule, or assembled +supplier is provided. For `N` not divisible by three this packet specifies +no reduction. The old all-size, row/stack, precision and analytic assumptions +are not discharged. In particular none of (13) or (14) is a new κ certificate. + +## 7. Reproducible evidence and exact limits + +`check.py --check` uses only Python's standard library and this directory. +It does not import the predecessor's checker or any supplier implementation. + +1. Enumerate all binary matrices at dimensions 2, 3 and 4; select rank-one + idempotents by independent rank and square tests; compare against the + outer-product catalogue. The sizes are 6, 28 and 120. +2. Multiply all **60,880 ordered signed pairs** as matrix Laurent polynomials. + Check (9)/(10) against the literal polynomial result for every pair and + every nonzero rank-one nilpotent target encountered. Every target has + `2^d` factorizations; none for a DATA coordinate shear has both private + diagonals one. +3. Exhaust all four native triangular charts + `(e_q+a e_x)(e_q+b e_y)^T`, `a,b in F2`, with both query signs, through + length four. The full **4,681-word** domain is completed: counts of + successes by length are `0,0,0,0,24`. This is a finite corroboration of + the specified model, not a search over arbitrary circuits or frames. +4. Verify (2) and its inverse on all rational ADDRESS basis columns and + modulo `3,9,27,11,121`, including two additional ADDRESS spectators. + Check full and shorter orbits from nonunit initial scales, plus fixed + points. These rings differ from PR #521's `5,25,7,49` replay. +5. Propagate all independent BIT basis columns simultaneously as distinct + integer bits, so every XOR-column cancellation is exact. Check all three + literal programs, their completed DATA involution, and the separate + owned-versus-dirty workspace contracts. No VALUE assignment is sampled. +6. Reject omissions of every recursive query, a wrong inverse, missing XORs, + missing owned initialization or clear, unpaid ADDRESS children, and the + false inference that owned clearing restores arbitrary dirty state. + A concrete order-two, same-sign factorization rejects extending the + opposite-sign classification to a domain where `t=t^-1`. + +The separate `full_domain_check.py` imports no main-checker code. It applies +the literal ADDRESS program to all **729 addresses in `(Z/3)^6`**, including +all 243 fixed addresses, and compares a separately written coordinate +formula. It then tracks individual sparse sets of nonzero BIT positions, +rather than packed symbolic columns, for **2,916 independent inputs per +program**. This covers every row and every address, not just a selected +orbit. Endpoints and completed inverses give **17,496 cases** across the +three programs. The private input is discarded only in the explicitly +owned-storage contract. This second finite method is included in the +single reproduction command. + +Assignment seed 57 selects candidate `57 mod 3 = 0` in `CLAIM.md`. The +algebraic domains and stopping rule above were fixed before implementing +the verifier; there is no random search whose losing trials are omitted. +The source pins and original attribution are in `SOURCES.json` and +`NOTICE.md`. `EXPECTED.json` records deterministic finite evidence. The +universal proof in sections 3–5 is a written argument open to review; +neither the exhaustive small-dimensional checks nor a PASS string replace it. diff --git a/research/dyadic-query-pair/vendor/upstream-02-streams.tex b/research/dyadic-query-pair/vendor/upstream-02-streams.tex new file mode 100644 index 0000000000..088fceea18 --- /dev/null +++ b/research/dyadic-query-pair/vendor/upstream-02-streams.tex @@ -0,0 +1,208 @@ +\section{The machine model and elementary streams} +\label{sec:streams} + +A machine has one fixed finite alphabet and one fixed finite number of +one-dimensional tapes. A step reads and writes at most one cell on each +tape and moves each head by at most one cell. Fixed tracks and finitely +many work tapes change time by a fixed factor. We distinguish moving one +digit in a fixed radix, which needs a bounded number of scans, from +interchanging fields whose numbers of digits grow. The latter permutation +will be realized in Section~\ref{sec:tape-interchange} by computing XOR +combinations of intermediate data streams. The present section supplies +the elementary scans it uses. Every scan includes its counters and the +return of its tape heads. + +\subsection{Array order and elementary scans} + +For a positive integer $a$ write $[a]=\{0,\ldots,a-1\}$. +An array with address set $[a_1]\times\cdots\times[a_t]$ is stored in +lexicographic order, with the first coordinate most significant. Its +entries are bits unless a record width is specified. A trailing record +of $B$ bits can equivalently be regarded as a final address field $[B]$. +An address is implicit in an entry's position in this ordered stream; it +is not stored beside every data bit. +The \emph{logical volume} $V$ is the number of stored data bits. Work +tapes and duplicate streams are charged in time but do not increase $V$ +in recurrences. All the fields discussed below are nonempty. A call +with an empty array is handled directly. + +An address permutation $f$ moves the entry at $x$ to $f(x)$. Thus its +action on an array $A$ is $(fA)(f(x))=A(x)$. Adjacent fields which are +irrelevant to an operation may be replaced by a single field whose length +is their product. In particular, the elementary procedures below have a +fixed number of formal address fields even when a surrounding algorithm +has a growing list of coordinates. Lengths and positions are supplied in +canonical binary on descriptor tapes; no additional tape head is attached to an +address coordinate. Each elementary call receives a fixed number of +collapsed canonical lengths. Constructing them from a longer surrounding +list is work of the caller; recursive calls below construct their own +collapsed descriptors within their stated bounds. + +When one address field is designated as a row field, collapse the fields +before it to a prefix $[P]$ and those after it to a suffix $[B]$. If the +row field has range $[R]$, a \emph{row} at prefix $p$ and row index $r$ +is the complete consecutive block $\{p\}\times\{r\}\times[B]$. +Every row therefore contains $B$ bits in the same suffix order. + +For headers that concatenate a list of positive integer parameters, we use +the self-delimiting code +\begin{equation} + b_v=\lfloor\log_2v\rfloor+1,\qquad + \Gamma(v)=0^{b_v-1}\operatorname{bin}_{b_v}(v),\qquad + |\Gamma(v)|=2b_v-1\quad(v\ge1). + \label{eq:integer-descriptor-code} +\end{equation} +The initial zeroes specify how many further bits follow the first one, +so concatenated codes can be read in order. We use this code when an +interface specifies a header; elementary calls still receive the fixed +number of canonical binary lengths described above. + +\begin{lemma}[Elementary stream operations] +\label{lem:elementary-streams} +Fix a radix $q\ge2$. Each of the following operations on an array of +volume $V$ takes $O(V)$ steps on a fixed number of one-dimensional tapes: +\begin{enumerate} +\item any fixed permutation of the pair of digit values at two specified +radix-$q$ positions, whether or not the positions are adjacent; +\item moving one specified radix-$q$ digit to another position, preserving +the order of the intervening positions; +\item splitting on a specified radix-$q$ digit, applying a fixed +pointwise map to aligned streams, and merging them back; +\item for positive integers $P,R,B$, within each prefix of an array on +$[P]\times[R]\times[B]$, splitting +whole rows cyclically into a fixed number $W$ of streams, and, when $W$ +divides $R$, merging those streams in any fixed order of the row classes. +\end{enumerate} +The bounds include shape preparation, counter initialization and resets, +and returning or clearing the visited portions of work tapes. Their +constants may depend on the fixed radix, the fixed pointwise map, and the +fixed number of row classes. +\end{lemma} + +\begin{proof} +For the first operation split into $q^2$ streams according to the two +specified digits. With these digits fixed, the order of all remaining +digits is unchanged by the permutation. Enumerate output addresses in +their required order and read the stream prescribed by the two preimage +digits. For a digit move use $q$ streams instead. The same observation +shows that splitting on one digit gives streams with the same remaining +address set in the same order. Scan their aligned entries, apply the +fixed pointwise map, and merge according to the output digit; this proves +the third operation. For the fourth, write $r=Wg+w$, where +$0\le w0$, write each chunk as $m$ +consecutive $b=e/m$ digit fields, giving vectors $H,D$ over +$\mathbb Z/q^b\mathbb Z$. We first construct the shear $H\leftarrow H+D$. + +Split whole rows cyclically into $W$ role streams within each prefix +preceding the row field. Write the original row number as +$r=Wg+(w-1)$ with $1\le w\le W$; stream $w$ has row number $g$. +These streams have exactly the same remaining shape, including the +full ranges of $H$ and $D$. Each has +logical volume $V/W$, and its row count is divisible by $W^{k-1}$. + +For a rational matrix $M$, let $\Phi_M$ act on an array by moving its +entry at address $(H,D)$ to $(H+MD,D)$, with every spectator unchanged. +Thus $\Phi_M$ is the array permutation induced by that address map. +Its inverse is $\Phi_{-M}$ and +$\Phi_{M'}\Phi_M=\Phi_{M'+M}$. On every circuit edge apply +$\Phi_{A_e}$ to that role stream; implement it by +Lemma~\ref{lem:matrix-shear}, recursively interchanging each pivot pair +of $b$-digit fields. Execute each circuit gate pointwise at matching +addresses of its role streams. + +The row split supplies the common address set used in the +frame identity~\eqref{eq:common-frame-identity}. Here the frame at a +vertex with matrix $M$ is the address permutation $\Phi_M$, and every +edge changes it by $\Phi_{M'-M}$. The same invariant proof applies +because a common address permutation commutes with every pointwise +bit gate. For the physical input arrays $f_w$, the logical arrays are +$g_w=\Phi_{-M_{\mathrm{in}(w)}}f_w$; this only specifies their +interpretation, with no initial tape operation. The logical circuit +routes $g_w$ to role $\rho(w)$. Thus its physical output satisfies +\[ + f'_{\rho(w)} + =\Phi_{M_{\mathrm{out}(\rho(w))}} + \Phi_{-M_{\mathrm{in}(w)}}f_w + =\Phi_{I_m}f_w, +\] +by~\eqref{eq:finite-shear-contract}. Merge by returning row $g$ of +output role $\rho(w)$ to the original row $Wg+(w-1)$ within the same +preceding prefix. This undoes $\rho$ and restores row order. The result +is $H\leftarrow H+D$ on every original row, including rows assigned +to scratch roles, whose initial values were arbitrary. + +To interchange the two full chunks, perform +\[ + D\leftarrow D-H,\qquad H\leftarrow H+D,\qquad D\leftarrow H-D, +\] +componentwise. Only the middle shear uses the circuit. The other two +updates target the later group and have linear cost. The transformation +sends $(H,D)$ to $(D,H)$. + +The number of recursive calls is the sum of the edge ranks, exactly $s$. +Each acts on one role stream of volume $V/W$, retaining all other +fields as spectators. Splitting, +merging, gates, and triangular operations have total cost $O(V)$ because +their number is fixed. Below we verify that scheduling the recursive +calls on fixed tapes also costs $O(V)$ at this node. Thus if $F_k$ is a +uniform upper bound for time divided by logical volume, then +\begin{equation} +\label{eq:swap-recurrence} + F_0=O(1),\qquad F_k\le(s/W)F_{k-1}+O(1). +\end{equation} +For $a=s/W1$, it is $O(a^k)$. +Hence $F_k=O(e^\tau)$. + +\paragraph{A fixed-tape depth-first schedule.} +Here we complete the implementation assertion used in +\eqref{eq:swap-recurrence}. Reserve $W$ role tapes, a fixed set of +I/O and elementary-operation work tapes, one parking stack tape, and a +separate descriptor stack. Although $W$ is large, it is fixed. +At a call boundary all reusable work tapes, other than the current I/O +and local descriptor, are empty and their heads are at their origins. +The parking and descriptor heads are at the tops of their stacks. + +Before a recursive call, append the $W-1$ inactive role streams to the +parking stack in a fixed order, with separators. Copy the active stream +to the child I/O area, and erase the parent role tapes while traversing +their current contents. Push the parent descriptor and its finite +program counter to the descriptor stack. The role and work tapes are +now available to the child, using the same tapes at every depth. +On return, copy the child output into the designated active role. +Pop the inactive streams in reverse order. To recover a stream in its +original direction, prepare its destination to the known length and +write the popped symbols from the destination's right end toward its +left end. Erase the popped stack cells as they are left. This uses +linear time and ends with the parking head at the previously saved top. +No scan passes through a parked ancestor. Cleanup is always limited to +the region visited by the current call; a reused tape is not swept to +the largest position ever visited by an ancestor. + +Each push, pop, copy, positioning operation, or erasure moves $O(V)$ +symbols at a parent node. There are only the fixed number $s$ of child +calls. This gives precisely the additional $O(V)$ term claimed above, +even though each child itself has volume $V/W$. Temporary storage is +therefore not substituted for logical volume in the factor $s/W$. + +For completeness, descriptor processing also fits this term when the +payload is one bit. Let $V_0$ be the volume at the root of one +power-width call with width $e_0=m^{k_0}$, and $V_j=V_0/W^j$ the volume +of any depth-$j$ child. Here $j\le k_0=\log_m e_0$. The root row +count is at least $W^{k_0}$, so at depth $j$ it is still at least one. +Both original chunk ranges remain present: digits outside the current +subchunks become spectators rather than being removed. Hence +\[ + V_j\ge q^{2e_0},\qquad + j\log W\le(\log_m e_0)\log W=O(e_0)=O(\log V_j). +\] +It follows that +$\log V_0=\log V_j+j\log W=O(\log(2V_j))$. +A local descriptor lists the row field, at most the current $m+m$ +fields, and a fixed number of intervals formed from intervening +spectator fields. Computing products of their lengths, subdividing +target fields, copying lengths, and storing the current instruction take +$(\log(2V_0))^{O(1)}=O(V_j)$ time at that child, since every fixed +power of $\log(2V_j)$ is $O(V_j)$. Before descending, +construct the child's descriptor by retaining its two target fields and +combining each consecutive group of spectator fields into one interval. +The ancestor's subdivision need not remain active in the child. Stack entries contain +finite instructions and binary integers, not new alphabet symbols. +These observations establish one finite machine for every recursion +depth and every choice of spectator lengths. + +\end{proof} + + +We use the rational value $\tau=1-2^{-50}$ established in +\eqref{eq:explicit-motif-exponents}. Its verification uses fixed integer +comparisons and the displayed exponential inequality; it needs no +real-arithmetic oracle. + + +\subsection{Removing width and row restrictions} + +We have proved the fast operation for power widths with enough rows. +Rows for a general array can be supplied by a few of its own high digits. +Their movement will cost less than the final bound. + +\begin{lemma}[Arbitrary-width interchange] +\label{lem:chunk-swap} +There exist fixed $0<\tau<1$ and one fixed finite-alphabet multitape +procedure with the following property. For positive integers $P,G,B$ +and $u\ge1$, it transforms an arbitrary bit array on +\[ + [P]\times[2^u]\times[G]\times[2^u]\times[B] +\] +by the address permutation +\[ + (p,h,g,d,z)\longmapsto(p,d,g,h,z) +\] +in $O(Vu^\tau)$ steps, where $V=PG B\,2^{2u}$. +The integers specifying the shape are part of the input. The time +includes their processing, all padding and unpadding, and fixed-tape +workspace cleanup. In particular, $B=1$ is allowed. +\end{lemma} + +\begin{proof} +First suppose the two ranges are $[q^e]$, where $q$ is the fixed prime +already chosen. Set +\[ + k=\lceil\log_m e\rceil,\qquad + \rho=\left\lceil\frac{k\log W}{2\log q}\right\rceil. +\] +For all sufficiently large $e$, $1\le\rho3; affine 24->18; XOR 4->2; no new kappa") + print("rational columns", result["lowerings"]["rational_columns_including_inverses_and_spectators"], + "; modular columns", result["lowerings"]["modular_columns_including_inverses"], + "; two-query census", result["laurent"]["two_query_products_checked"], + "; negative controls", len(result["negative_controls"])) + print("full-domain dirty basis columns", result["finite_arrays"]["full_dirty_basis_columns_per_program"], + "; orbit columns", result["finite_arrays"]["orbit_dirty_basis_columns_per_program"]) + + +if __name__ == "__main__": + main()