From 5ed1ce17a9df4c853a93f9758ba903d2620c3443 Mon Sep 17 00:00:00 2001 From: Hanson Sun Date: Tue, 13 Oct 2026 17:03:44 -0400 Subject: [PATCH] Research: price nonzero reader-defect repair --- .../CERTIFICATE.json | 491 ++++++++++++++++++ research/paid-reader-defect-seed58/CLAIM.json | 36 ++ research/paid-reader-defect-seed58/LICENSE | 201 +++++++ .../paid-reader-defect-seed58/OVERLAP.json | 58 +++ research/paid-reader-defect-seed58/README.md | 288 ++++++++++ .../SOURCE-PINS.json | 51 ++ .../paid-reader-defect-seed58/VALIDATION.json | 49 ++ .../context/pr1199-README.md | 198 +++++++ .../context/pr1205-README.md | 263 ++++++++++ .../context/pr1227-README.md | 240 +++++++++ research/paid-reader-defect-seed58/model.py | 201 +++++++ .../paid-reader-defect-seed58/test_package.py | 77 +++ research/paid-reader-defect-seed58/verify.py | 405 +++++++++++++++ 13 files changed, 2558 insertions(+) create mode 100644 research/paid-reader-defect-seed58/CERTIFICATE.json create mode 100644 research/paid-reader-defect-seed58/CLAIM.json create mode 100644 research/paid-reader-defect-seed58/LICENSE create mode 100644 research/paid-reader-defect-seed58/OVERLAP.json create mode 100644 research/paid-reader-defect-seed58/README.md create mode 100644 research/paid-reader-defect-seed58/SOURCE-PINS.json create mode 100644 research/paid-reader-defect-seed58/VALIDATION.json create mode 100644 research/paid-reader-defect-seed58/context/pr1199-README.md create mode 100644 research/paid-reader-defect-seed58/context/pr1205-README.md create mode 100644 research/paid-reader-defect-seed58/context/pr1227-README.md create mode 100644 research/paid-reader-defect-seed58/model.py create mode 100644 research/paid-reader-defect-seed58/test_package.py create mode 100644 research/paid-reader-defect-seed58/verify.py diff --git a/research/paid-reader-defect-seed58/CERTIFICATE.json b/research/paid-reader-defect-seed58/CERTIFICATE.json new file mode 100644 index 0000000000..fb1c23e964 --- /dev/null +++ b/research/paid-reader-defect-seed58/CERTIFICATE.json @@ -0,0 +1,491 @@ +{ + "assignment_seed": 58, + "controls": { + "invalid_inputs_rejected": 8, + "mathematical_controls": [ + { + "actual": [ + -3, + 1, + 0, + 0, + 0, + 0 + ], + "control": "omit_nonzero_defect_correction", + "expected": [ + 1, + 1, + 0, + 0, + 0, + 0 + ], + "input_basis_column": 1 + }, + { + "actual": [ + -7, + 1, + 0, + 0, + 0, + 0 + ], + "control": "reverse_correction_sign", + "expected": [ + 1, + 1, + 0, + 0, + 0, + 0 + ], + "input_basis_column": 1 + }, + { + "actual": [ + 2, + 1, + 0, + 0 + ], + "control": "repair_before_restoring_entry_coordinates", + "expected": [ + 1, + 1, + 0, + 0 + ], + "input_basis_column": 1 + }, + { + "actual": [ + 2, + 0, + 0, + 1 + ], + "control": "omit_workspace_restoration", + "expected": [ + 1, + 1, + 0, + 0 + ], + "input_basis_column": 1 + }, + { + "actual": [ + 3, + 0, + 1, + 0 + ], + "control": "wrong_noncommuting_inverse_order", + "expected": [ + 1, + 1, + 0, + 0 + ], + "input_basis_column": 1 + }, + { + "actual": [ + 0, + 1, + 0, + 0, + 0, + 0, + 1, + 0, + 0, + 0, + 0 + ], + "control": "omit_source_uncopy", + "expected": [ + 1, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "input_basis_column": 1 + }, + { + "actual": [ + 1, + 0, + 0, + 0, + 0, + 0, + 1, + 0, + 0, + 0, + 0 + ], + "control": "omit_second_batch", + "expected": [ + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 0, + 0, + 0, + 0 + ], + "input_basis_column": 6 + }, + { + "actual_row": [ + 1, + 0, + -2, + 0, + 2, + 0 + ], + "control": "premature_output_observer", + "expected_row": [ + 1, + 0, + 0, + 0, + 0, + 0 + ], + "forced_boundary_cost": 80 + }, + { + "control": "nonunit_coefficients_are_not_free", + "nonzero_entries": 4, + "paid_ADD": 12 + } + ] + }, + "finite_census": { + "exhaustive_batches": 5256, + "exhaustive_partitions_per_policy": 10440, + "exhaustive_strict_improvements": 1116, + "results_sha256": "79863cfa31bc6d19d6102c612c97617dcfd0ef6d5a3940ce6b5076ad1e3aad8f", + "seeded_batches": 160, + "seeded_noncommuting": 160, + "seeded_strict_improvements": 152, + "seeded_with_required_cuts": 54 + }, + "format": "paid-reader-defect-v1", + "provenance": { + "base_commit": "49b3157d1d89adcef16df8be98445451672be5ba", + "model_sha256": "06aa3037392ae024ce3ae30345352886096b3e1a067027da30da7a87cc20a1c2", + "source_manifest_sha256": "de116db31760fc4713cfef44f15bf560dfdab727adb25ec5230cfad92e5af817", + "source_notes": 3, + "verifier_sha256": "93040ad283488b3091fbe58924ed11a07756f70cb3e3a3ea743bc47154545db8" + }, + "recursive_census": { + "generic_basis_columns": 1044, + "generic_cases": 120, + "results_sha256": "3981f34dcff44ce13c91575f8147b6d9a7216c46515156d3215a0bff01c9eaec", + "selected_echoes": [ + { + "ADD": 300, + "NEG": 80, + "data_reads": 680, + "data_writes": 380, + "depth": 1, + "descriptor_fields": 1360, + "instructions": 380, + "integer_row_l1_peak": 11, + "mode": "eager", + "registers": 11 + }, + { + "ADD": 300, + "NEG": 80, + "data_reads": 680, + "data_writes": 380, + "depth": 1, + "descriptor_fields": 1360, + "instructions": 380, + "integer_row_l1_peak": 11, + "mode": "zero", + "registers": 11 + }, + { + "ADD": 204, + "NEG": 40, + "data_reads": 448, + "data_writes": 244, + "depth": 1, + "descriptor_fields": 896, + "instructions": 244, + "integer_row_l1_peak": 27, + "mode": "repair", + "registers": 11 + }, + { + "ADD": 3250, + "NEG": 880, + "data_reads": 7380, + "data_writes": 4130, + "depth": 2, + "descriptor_fields": 14760, + "instructions": 4130, + "integer_row_l1_peak": 26, + "mode": "eager", + "registers": 16 + }, + { + "ADD": 3250, + "NEG": 880, + "data_reads": 7380, + "data_writes": 4130, + "depth": 2, + "descriptor_fields": 14760, + "instructions": 4130, + "integer_row_l1_peak": 26, + "mode": "zero", + "registers": 16 + }, + { + "ADD": 2194, + "NEG": 440, + "data_reads": 4828, + "data_writes": 2634, + "depth": 2, + "descriptor_fields": 9656, + "instructions": 2634, + "integer_row_l1_peak": 52, + "mode": "repair", + "registers": 16 + }, + { + "ADD": 32750, + "NEG": 8880, + "data_reads": 74380, + "data_writes": 41630, + "depth": 3, + "descriptor_fields": 148760, + "instructions": 41630, + "integer_row_l1_peak": 46, + "mode": "eager", + "registers": 21 + }, + { + "ADD": 32750, + "NEG": 8880, + "data_reads": 74380, + "data_writes": 41630, + "depth": 3, + "descriptor_fields": 148760, + "instructions": 41630, + "integer_row_l1_peak": 46, + "mode": "zero", + "registers": 21 + }, + { + "ADD": 22094, + "NEG": 4440, + "data_reads": 48628, + "data_writes": 26534, + "depth": 3, + "descriptor_fields": 97256, + "instructions": 26534, + "integer_row_l1_peak": 71, + "mode": "repair", + "registers": 21 + } + ] + }, + "selected": { + "all_partitions": [ + { + "cuts": [ + 5 + ], + "instructions": 117 + }, + { + "cuts": [ + 1, + 5 + ], + "instructions": 149 + }, + { + "cuts": [ + 2, + 5 + ], + "instructions": 153 + }, + { + "cuts": [ + 1, + 2, + 5 + ], + "instructions": 165 + }, + { + "cuts": [ + 3, + 5 + ], + "instructions": 153 + }, + { + "cuts": [ + 1, + 3, + 5 + ], + "instructions": 161 + }, + { + "cuts": [ + 2, + 3, + 5 + ], + "instructions": 161 + }, + { + "cuts": [ + 1, + 2, + 3, + 5 + ], + "instructions": 173 + }, + { + "cuts": [ + 4, + 5 + ], + "instructions": 145 + }, + { + "cuts": [ + 1, + 4, + 5 + ], + "instructions": 157 + }, + { + "cuts": [ + 2, + 4, + 5 + ], + "instructions": 161 + }, + { + "cuts": [ + 1, + 2, + 4, + 5 + ], + "instructions": 173 + }, + { + "cuts": [ + 3, + 4, + 5 + ], + "instructions": 165 + }, + { + "cuts": [ + 1, + 3, + 4, + 5 + ], + "instructions": 173 + }, + { + "cuts": [ + 2, + 3, + 4, + 5 + ], + "instructions": 173 + }, + { + "cuts": [ + 1, + 2, + 3, + 4, + 5 + ], + "instructions": 185 + } + ], + "defect": [ + -4, + -2, + 2, + 4, + 0 + ], + "drift": [ + 2, + 3, + 4, + 5, + 1 + ], + "repair_plan": [ + 12, + [ + 5 + ] + ], + "row": [ + 1, + -1, + -1, + 1, + 1 + ], + "signs": [ + 1, + -1, + -1, + 1, + 1 + ], + "zero_defect_plan": [ + 80, + [ + 1, + 2, + 3, + 4, + 5 + ] + ] + }, + "status": "scoped exact recursive-interface construction; no new kappa" +} diff --git a/research/paid-reader-defect-seed58/CLAIM.json b/research/paid-reader-defect-seed58/CLAIM.json new file mode 100644 index 0000000000..4821dd7654 --- /dev/null +++ b/research/paid-reader-defect-seed58/CLAIM.json @@ -0,0 +1,36 @@ +{ + "track": "recursive interfaces", + "assignment_seed": 58, + "seed_source": "secrets.randbelow(100), OS-backed; work/sprint-meta.json", + "base_commit": "49b3157d1d89adcef16df8be98445451672be5ba", + "claimed_at_utc": "2026-10-13T20:46:43.817718+00:00", + "expected_finish_utc": "2026-10-13T21:31:29Z", + "scope_key": "persistent-boundary/signed-permutation-readers/nonzero-defect-correction", + "candidates": [ + { + "scope": "T37 hosted restoration deferral", + "decision": "covered by PR1012/974; no changed hosted premise identified" + }, + { + "scope": "compatible readers and output sign restoration", + "decision": "covered by PR1199/1203/1205/1227" + }, + { + "scope": "paid nonzero reader-defect correction and partition planner", + "decision": "chosen; admit nonzero defects by explicitly charging canonical output ADD repair" + } + ], + "method": "Exact integer block algebra plus independently emitted ADD/NEG programs; dynamic programming compared with all partitions. Signed-permutation drifts; no data-to-workspace feedback or intermediate observation within a block.", + "domain": "seed-selected width 5, five children; all one/two-child width-2 signed permutations and readers in {-1,0,1}^2; seeded noncommuting and longer checks; recursive depths 0..3", + "deliverable": "Scoped construction/proof, complete recursive scalar/access invoice, exact certificate, standalone verifier with negative controls. No supplier or kappa claim.", + "stopping_rule": "Complete fixed domains; stop if exact repair bill cannot beat eager restoration. At most one pivot. Reserve final 25 percent for verification.", + "coordination": "GitHub GraphQL returned no pinned issues. Claim is local per donor instructions. Inspected six current discussions including 1163/1166/1167; captured 838 open PR titles/bodies. No separate reservation issue.", + "dependencies": { + "1205": "e2008d7ffcad464da7ec21c69e8d8a8c91de4930", + "1199": "85ac2880ea5bda44f28632b71ffa2b4e35ec6b7d", + "1227": "fea44a4d0d78570021d854881d15d9efe62e1713" + }, + "status": "claimed", + "scope_status": "refined", + "scope_reason": "The user-assigned recursive-interface track is refined to nonzero defect repair for fixed signed-permutation readers; it changes the zero-defect-only boundary, not the supplier." +} diff --git a/research/paid-reader-defect-seed58/LICENSE b/research/paid-reader-defect-seed58/LICENSE new file mode 100644 index 0000000000..261eeb9e9f --- /dev/null +++ b/research/paid-reader-defect-seed58/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/paid-reader-defect-seed58/OVERLAP.json b/research/paid-reader-defect-seed58/OVERLAP.json new file mode 100644 index 0000000000..c4c70206c1 --- /dev/null +++ b/research/paid-reader-defect-seed58/OVERLAP.json @@ -0,0 +1,58 @@ +{ + "checked_at_utc": "2026-10-13T20:58:15Z", + "open_prs": 843, + "highest_open_pr": 1240, + "discussions": 9, + "pinned_issues": 0, + "main_head": "dd6403f774a0891093a006ae9716c02e371b1fdb", + "selected_record_and_context_inputs_unchanged": true, + "nearest": [ + { + "number": 1235, + "title": "research: reduce calibrated endpoint gauges to exact source tours", + "head": "3941a3c63651d379feceb411019c30310e9e12d0" + }, + { + "number": 1227, + "title": "Research construction: sharp restoration cost for fixed readers", + "head": "fea44a4d0d78570021d854881d15d9efe62e1713" + }, + { + "number": 1205, + "title": "Research: observer-safe restoration with nonzero readers (no new kappa)", + "head": "e2008d7ffcad464da7ec21c69e8d8a8c91de4930" + }, + { + "number": 1203, + "title": "Research: noncommuting reader restoration with a paid dirty-state wrapper", + "head": "38459854fd5bb93099871a84324413bd0e338d8e" + }, + { + "number": 1199, + "title": "Recursive interface: coalesce restoration with cancelling readers", + "head": "85ac2880ea5bda44f28632b71ffa2b4e35ec6b7d" + }, + { + "number": 1155, + "title": "Research note: restoration coalescing across a recursion batch (read-free + composable-family boundary; no new kappa)", + "head": "9821c6e9388f3fc097e94b72be9fa7b41a849527" + }, + { + "number": 1012, + "title": "Research note: restoration deferral is mass-neutral in the hosted T37 recurrence (no new kappa)", + "head": "4ceaf380ed41b28dadcc41d2f974f025ac4d8c03" + }, + { + "number": 974, + "title": "Research: T21/T37 interface budget and bit-binding headroom (no new kappa)", + "head": "f40cd20a8c257bcfee17508c7de68fee24df0568" + }, + { + "number": 889, + "title": "Research: batch common-factor product shears with dirty restoration", + "head": "e2021d1c9e06948528cbc0a8fd7079b671da981d" + } + ], + "coverage": "All open PR titles/bodies including drafts; current discussion bodies/comments/replies with complete reported pagination; cached local package notes and ledger. Not all code diffs or closed PRs.", + "additional_value": "Paid nonzero output-defect repair and a minimum over canonically repaired partitions. Predecessor cancelling-reader identities, cut planners, sign frames, and dirty echo are credited. PR1235 concerns individually calibrated phase tours without role mixing, not these reader corrections." +} diff --git a/research/paid-reader-defect-seed58/README.md b/research/paid-reader-defect-seed58/README.md new file mode 100644 index 0000000000..e9263fffce --- /dev/null +++ b/research/paid-reader-defect-seed58/README.md @@ -0,0 +1,288 @@ +# Pay for nonzero reader defects instead of restoring every child + +**Recursive-interface construction and partition planner; no new kappa.** +For the fixed five-child example below, a complete dirty-workspace echo costs +**244 scalar instructions instead of 380**. Readers do not cancel their drift +errors. The parent restores the workspace and pays for an explicit output +correction. Both source-copy passes, both directions of every child, all +private scratch and the correction are included. + +The contribution extends the zero-defect cut rule in Sagar Thakrar's +[PR1199](https://github.com/CrocSwap/integer-mult-bounds/pull/1199) and the +observer criterion independently developed by mightyOil in +[PR1203](https://github.com/CrocSwap/integer-mult-bounds/pull/1203) and Adam Gall in +[PR1205](https://github.com/CrocSwap/integer-mult-bounds/pull/1205). Their defect +identity is reused and credited, not claimed as new. The added operation is a +**paid output shear with a nonzero defect**, together with a minimum-cost +partition over a specified implementation of that operation. The selected +example uses a noncentral cyclic workspace permutation, outside the fixed +workspace-negation alphabet of Thakrar's +[PR1227](https://github.com/CrocSwap/integer-mult-bounds/pull/1227). + +This is an interface result with indivisible children. If a compiler may open +these particular leaves, their final map is just a five-ADD signed dot product; +direct evaluation is much cheaper than either echo. No supported supplier +requiring this indivisible boundary has been identified. The result supplies +a checked option for such a boundary, not an optimized matrix algorithm, +physical supplier, runtime speedup or change to the selected exponent. + +## Exact terminal repair + +Let `D` be data and `W` arbitrary dirty workspace. Fixed linear children satisfy + +``` +C_i(D,W) = (D + B_i W, G_i W), G_i invertible. +``` + +Each child's private scratch is arbitrary and restored. The matrices do not +depend on intermediate data, and there is no data-to-workspace feedback. +Eager execution follows every child by its workspace inverse. Its desired +return map is `(D + sum_i B_i W, W)`. + +Write `P_0=I`, `P_i=G_i ... G_1` and + +``` +E = sum_i B_i (P_(i-1) - I). +``` + +The cited predecessor criterion admits uncorrected deferral exactly when +`E=0`. For arbitrary `E`, the following enlarged boundary is exact: + +1. Execute each unchanged child once in its fixed order. +2. Apply `P_k^-1` to workspace. +3. Apply `D <- D - E W`, now using restored entry-coordinate workspace. + +**Proof.** Before child `i`, deferred workspace is `P_(i-1) W_entry`. The raw +data return is therefore `D_entry + (sum_i B_i + E) W_entry`. Step 2 returns +`W_entry`; step 3 subtracts exactly the unwanted term. Every private scratch +port has its original value. This proves the identity for arbitrary dirty +inputs and dimensions over any field with these exact operations. It does +not infer a universal theorem from finite samples. + +Restoration must precede the stated correction. Correcting against `P_k W` +instead would require a different matrix, `E P_k^-1`. A noncommuting example +in the controls detects this order error. An intermediate observer or adaptive +child cannot use the uncorrected output as if it were canonical. Such a point +must be a required cut, with its entire restoration and correction paid first. + +## Declared operation alphabet and partition optimum + +The executable specialization has one output coordinate, an integer row +`B_i`, and a signed permutation `G_i` on `N` workspace coordinates. There are +only two scalar instructions: `target += sign * source` for distinct ports, +where `sign` is `+1` or `-1`, and unary `NEG`. Registers are addressed exactly; +no clean scratch or implicit source copy is available. + +Canonical signed-permutation synthesis first permutes absolute indices using +`N-cycles` swaps, then negates negative coordinates. A swap uses three ADDs +and one NEG, with no temporary. Inversion has the same number of cycles and +negative coordinates. The correction repeats a unit signed ADD `|E_j|` times +for each coefficient. A coefficient of magnitude four costs four ADDs, not +one. These are implementations with a known price, not globally shortest +linear circuits. + +For a segment `[a,b)`, its boundary cost is thus + +``` +b(a,b) = 4 (N - cycles(abs(P))) + negative_signs(P) + sum_j |E_j|. +``` + +The child words are common to every partition. With `F(0)=0`, the planner uses + +``` +F(t) = min_{0 <= s < t} { F(s) + b(s,t) }, +``` + +excluding intervals that cross a required observation cut. Each chosen segment +returns the same data and workspace as eager execution, so legal segments +compose. Conversely, every partition in this alphabet has a last segment; +removing it gives the displayed recurrence. Induction proves the minimum over +these partitions. This is not an optimum over arbitrary repairs, edits inside +children, interleaved adapters, or a different operation alphabet. The +`zero_defect_only` comparison additionally requires `E=0` on every segment. + +## Seed-selected example and actual eliminated work + +OS assignment seed **58** selected recursive interfaces. It also selects +`N=3+(58 mod 4)=5`, then the following row and signs using the documented +`random.Random(58)` calls in `selected()`: + +``` +R = (1,-1,-1,1,1) +s = (1,-1,-1,1,1), sum s_i = 1 +B_i = s_i R +G(W_0,W_1,W_2,W_3,W_4) = (W_1,W_2,W_3,W_4,W_0). +``` + +Each child reader costs five ADDs. Its workspace cycle costs twelve ADDs and +four NEGs. On the full five-child batch, `P=I` and + +``` +E = (-4,-2,2,4,0). +``` + +The raw batch is wrong: on `W=e_0` it adds `-3` instead of `1`. The completed +one-block repair costs twelve ADDs. The best zero-defect partition is all five +singletons, costing **80 boundary instructions**. The repaired optimum is +the full batch at **12**, as checked against all sixteen partitions. It removes +five workspace inverses, pays twelve correction ADDs, and preserves the child +word. If every interior child boundary must be observed, the optimum returns +to 80; the observation restriction is material. + +The transparent source echo uses a separate arbitrary dirty `W` and preserved +source `X`: + +``` +W += X; B(D,W); W -= X; B^-1(D,W). +``` + +Since the completed batch is `B(D,W)=(D+R W,W)`, the two passes add +`R(W_initial+X)-R W_initial = R X`. The inverse is the literal reversed +instruction word, not a free inverse query. At depth one the complete echo is: + +| Schedule | ADD | NEG | Total | Reads | Writes | Descriptor fields | +|---|---:|---:|---:|---:|---:|---:| +| Eager / zero-defect cuts | 300 | 80 | 380 | 680 | 380 | 1,360 | +| Paid defect repair | 204 | 40 | 244 | 448 | 244 | 896 | + +## Complete recursion, storage and arithmetic scope + +`recursive_word` realizes an actual tree. A leaf adds its signed row to `D` +and applies `G` to its source. An interior reader executes the above echo using +five depth-`h-1` readers with rows `s_i R`, then applies `G` to its own source. +Because the signs sum to one, the reader at every depth returns +`(D+R X,G X)`. Negative rows use the same construction with all reader +coefficients negated. Children restore their private scratch, so siblings and +both echo passes reuse one dirty block per active level. An induction on depth +proves the stated map for all incoming values. + +Let `A_h,Q_h` count ADD and NEG instructions of an interior **reader**, including +all descendants and inverses. For this selected family the complete recurrences +are: + +``` +A_0 = 17, Q_0 = 4 +eager: A_h = 10 A_(h-1) + 142; Q_h = 10 Q_(h-1) + 44 +repair: A_h = 10 A_(h-1) + 46; Q_h = 10 Q_(h-1) + 4. +``` + +The factor ten pays both directions of all five children. The additive terms +include ten source-copy ADDs, both boundary bills, and the final source cycle. +A root echo omits that last cycle: subtract twelve ADDs and four NEGs. Thus +the depth-`h` saving is `136*(10^h-1)/9` instructions. This is tree depth at +fixed port width, not an input-size recurrence or a primitive exponent. + +| Echo depth | Eager total | Repaired total | Data registers | Eager peak | Repaired peak | +|---|---:|---:|---:|---:|---:| +| 1 | 380 | 244 | 11 | 11 | 27 | +| 2 | 4,130 | 2,634 | 16 | 26 | 52 | +| 3 | 41,630 | 26,534 | 21 | 46 | 71 | + +The data allocation is `1+(h+1)N` scalars: output, source and dirty blocks. +For `A` ADDs and `Q` NEGs, every emitted instruction incurs one dispatch, +`2A+Q` data reads, `A+Q` writes and `4A+2Q` instruction-field reads, including +signs and addresses. On the declared addressed machine, arbitrary prices for +arithmetic, these accesses and dispatch can be substituted into those counts. +All recursive calls are expanded into this instruction word; there is no +omitted runtime call dispatcher or coefficient multiplication. No frame change +is a free relabeling: each signed permutation is physically emitted. + +Program preparation is separate work. For fixed `N`, arity and bounded row, +the supplied compiler conservatively takes `O((h+1)P_h)` list work and storage, +where `P_h=A_h+Q_h`, including its repeated planning and word reversal/copying. +The materialized program contains exactly the tabulated descriptor fields. +An end-to-end bill must add this preparation to execution; the counts do not +claim faster compilation or an amortization schedule. No streaming compiler, +tape routing, address-bit cost or physical hosting theorem is supplied. + +The peaks in the table are exact maximum row one-norms over **every instruction +prefix**, on the complete original-input basis, including private dirt. If +initial integers have magnitude at most `M`, every intermediate magnitude is +at most `peak*M`. The repaired schedule therefore needs a larger magnitude +bound in these examples. The verifier uses unbounded integers and rationals; +unit instruction counts alone do not price arbitrary-precision bit arithmetic. +For general emitted words, the elementary bound `2^A M` also suffices. Neither +these bounds nor finite replay establishes a rounded or fixed-tape interface. + +## Reproduce and inspect the evidence + +Python 3.10+; standard library only. From the repository root: + +```sh +python3 -I -O -B research/paid-reader-defect-seed58/test_package.py +``` + +Expected markers: + +``` +PASS_PAID_READER_DEFECT batches=5256 seeded=160 echo=380->244 controls=9 kappa=unchanged +PASS_PAID_READER_PACKAGE relocation=1 corruptions=5 +``` + +`verify.py` checks the retained source-note SHA256 and Git blob identities, +recomputes every field of `CERTIFICATE.json`, and compares the result exactly. +`--emit` prints the recomputed certificate without changing files. Checks use +explicit exceptions and remain active with Python's `-O` flag. + +The independent oracle composes complete state matrices and exhausts all cut +sets. It does not call the production defect routine or planner to derive +its costs. The bounded domain is all 72 single children and 5,184 ordered pairs +at width two: eight signed permutations and nine rows in `{-1,0,1}^2` per +child. This covers **5,256 batches and 10,440 partitions per policy**; 1,116 +batches strictly improve over zero-defect cuts. An additional 160 deterministic +seed-58 cases have widths 3..6, arities 3..7 and row entries -2..2. All contain +noncommuting adjacent drifts; 54 impose interior observation cuts. Their 152 +improvements are finite evidence, not an impossibility or optimality theorem +outside the stated domain. The stopping rule is completion of these domains. + +The recursive census checks 120 generic reader/echo cases on all 1,044 original +basis columns, literal inverses and rational dirty probes, plus nine selected +depth/schedule cases. Every selected partition is also replayed. Nine controls +cover omitted/wrong-sign correction, wrong repair coordinates, missing cleanup, +noncommuting inverse order, omitted source uncopy, a missing second pass, +premature output observation, and nonunit coefficient cost. Eight invalid +inputs are rejected. The package test runs from outside the repository and +rejects five real file corruptions: retained source bytes, source-commit label, +certificate price, omitted correction, and treating a nonunit coefficient as a +single ADD. Source labels are recorded fetch pins; this is not a cryptographic +proof of GitHub publication or a fresh replay of predecessor packages. + +## Provenance, scope and open next questions + +Investigation base: `49b3157d1d89adcef16df8be98445451672be5ba`. The selected +certificate at that base is PR1094, conditional +`kappa=836330098538459/500000000000000000`. Its actual construction, source +manifest and review were followed; `SOURCE-PINS.json` records their hashes as +context. The source-binding baseline check passed. The selected cold replay, +native supplier admission, Linux CI, independent human review and a formal +multiplication proof were not run. Selected compiler/all-size, realization, +hosting, precision/tape, analytic and bit-interface obligations remain open. + +`CLAIM.json` records the three considered tasks, scope, seed and bounded +domain. No pinned sprint issue was present, so the donor's local-claim fallback +was used. Open PR bodies and current discussions were checked; overlap evidence +is bounded and is not proof of novelty. This package changes no predecessor, +selected record, review ledger or upstream source. + +**Open next questions.** Does a supported supplier expose indivisible drifting +readers whose defect is cheap to apply? Trace one concrete child return map and +price its composed inverse and correction before implementing this wrapper. +The blockers are a real child contract, routing and precision; transparent +leaves that can simply be rewritten do not qualify. Within the declared model, +a correction circuit with sharing could reduce the twelve-ADD bill further, +but it would need a different cost function and a newly checked partition +comparison. No global shortest-circuit claim is made here. + +Credit Aaron Wang / Navinor's PR1155 for restoration coalescing; Sagar Thakrar's +PR1199 and PR1227 for the cut and output-sign interfaces; mightyOil's PR1203 and +Adam Gall's PR1205 for independent observer/dirty-reader treatments; and Ross +Richardson / CubeJerry's PR889 for prior common-factor dirty echo work. PR1012 +and PR974 address hosted restoration mass, a different cost model. The selected +Rohan Arun / Jeremy Kothe construction and its contributor lineage are unchanged. +Three predecessor notes are retained byte-for-byte with their notices and exact +heads in `SOURCE-PINS.json`; no predecessor executable is imported. + +Prepared by **Hanson Sun (@bbMisk)** with substantial **OpenAI Codex assistance** +in algebra, implementation, verification and writing. New material is Apache-2.0 +under the retained repository license. This is a written scoped proof with exact +finite implementation evidence, not independent human or proof-assistant review. diff --git a/research/paid-reader-defect-seed58/SOURCE-PINS.json b/research/paid-reader-defect-seed58/SOURCE-PINS.json new file mode 100644 index 0000000000..7103c1aa4f --- /dev/null +++ b/research/paid-reader-defect-seed58/SOURCE-PINS.json @@ -0,0 +1,51 @@ +{ + "base_commit": "49b3157d1d89adcef16df8be98445451672be5ba", + "sources": [ + { + "pr": 1205, + "commit": "e2008d7ffcad464da7ec21c69e8d8a8c91de4930", + "source_path": "research/observer-safe-restoration/README.md", + "local_path": "context/pr1205-README.md", + "sha256": "fc672e69f4b3363fa7736efa4b4103c755fcb72f6f5d45e5d268c10e133a914d", + "git_blob": "7ed4d89d17c5cdeba0e5e5eb160919e0e9c5a076" + }, + { + "pr": 1199, + "commit": "85ac2880ea5bda44f28632b71ffa2b4e35ec6b7d", + "source_path": "research/reader-restoration-cuts-seed53/README.md", + "local_path": "context/pr1199-README.md", + "sha256": "a073617e65be95d8fe7ceba41387d85171950d19f5e03f2ad1d9d1c8a6f4dae7", + "git_blob": "f58d1581de51da4aa369a354bd19a9962144eac9" + }, + { + "pr": 1227, + "commit": "fea44a4d0d78570021d854881d15d9efe62e1713", + "source_path": "research/output-sign-restoration-seed51/README.md", + "local_path": "context/pr1227-README.md", + "sha256": "1a038312c647b33cb697cd78bd5b2f74f5fbb8d87ec39894176c0f6ce90f5026", + "git_blob": "ade3f00abbc5e4c8f933b81bd9c07d38180781d5" + } + ], + "selected_context": [ + { + "path": "certificates/selected-result.json", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "research/community-frontier1094-audit/ASSEMBLY.json", + "sha256": "1122cb3a575f8c788345fc1bf4c108ac7c3250fb81a5988671f5eb04b3ab3045" + }, + { + "path": "research/community-frontier1094-audit/SELECTED-SOURCE.json", + "sha256": "79b3de5db3dbcb9829789ba58e9e45758926031e2a7d80667a08429d369be53b" + }, + { + "path": "docs/research/community-batch1099-review.md", + "sha256": "7e76d2c38e5fce30587835b7251df1430488ae4dd372611ef69a3f03f476b6cb" + }, + { + "path": "research/complex-t16-rare-pattern-exchanges/README.md", + "sha256": "da542711a6a3eb01ce1ebdf8f28a748e6195512687f61d003b95ac5ff281a7b2" + } + ] +} diff --git a/research/paid-reader-defect-seed58/VALIDATION.json b/research/paid-reader-defect-seed58/VALIDATION.json new file mode 100644 index 0000000000..5a59cf14eb --- /dev/null +++ b/research/paid-reader-defect-seed58/VALIDATION.json @@ -0,0 +1,49 @@ +{ + "validated_at_utc": "2026-10-13T21:02:04Z", + "base_commit": "49b3157d1d89adcef16df8be98445451672be5ba", + "refreshed_main": "dd6403f774a0891093a006ae9716c02e371b1fdb", + "platform": "macOS-27.0.1-arm64-arm-64bit-Mach-O", + "certificate_sha256": "f76eed4fb427dae905d0b03c1391b5d2fb79f836f523d2a3451e881818df18c8", + "checked_implementations": { + "base_commit": "49b3157d1d89adcef16df8be98445451672be5ba", + "model_sha256": "06aa3037392ae024ce3ae30345352886096b3e1a067027da30da7a87cc20a1c2", + "source_manifest_sha256": "de116db31760fc4713cfef44f15bf560dfdab727adb25ec5230cfad92e5af817", + "source_notes": 3, + "verifier_sha256": "93040ad283488b3091fbe58924ed11a07756f70cb3e3a3ea743bc47154545db8" + }, + "commands": [ + { + "command": "python3 -I -O -B research/paid-reader-defect-seed58/test_package.py", + "python": "3.14.6", + "exit_code": 0, + "markers": [ + "PASS_PAID_READER_DEFECT batches=5256 seeded=160 echo=380->244 controls=9 kappa=unchanged", + "PASS_PAID_READER_PACKAGE relocation=1 corruptions=5" + ] + }, + { + "command": "python3.11 -I -O -B research/paid-reader-defect-seed58/verify.py", + "python": "3.11.5", + "exit_code": 0, + "marker": "PASS_PAID_READER_DEFECT batches=5256 seeded=160 echo=380->244 controls=9 kappa=unchanged" + }, + { + "command": "python3 -B scripts/research_baseline.py", + "exit_code": 0, + "scope": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY; source bindings and arithmetic, not a selected cold replay" + } + ], + "additional_checks": [ + "All five selected-context SHA256 pins agree at both investigation base and refreshed main.", + "New package path is absent on refreshed main.", + "Independent dense state/cycle-count oracle agrees with canonical repair planner and recursive scalar recurrence." + ], + "not_run": [ + "selected frontier cold replay", + "repository-wide historical suites", + "Linux or hosted CI", + "formal proof assistant", + "independent human review" + ], + "interpretation": "Exact finite checks support the written scoped interface proof. They do not admit a physical supplier or establish a stronger exponent." +} diff --git a/research/paid-reader-defect-seed58/context/pr1199-README.md b/research/paid-reader-defect-seed58/context/pr1199-README.md new file mode 100644 index 0000000000..f58d1581de --- /dev/null +++ b/research/paid-reader-defect-seed58/context/pr1199-README.md @@ -0,0 +1,198 @@ +# Restoration cuts that allow workspace readers + +This recursive-interface construction removes four of five restorations in a +batch where every child reads the dirty workspace. It also provides an exact +planner for the cheapest checkpoint-correct partition of a fixed diagonal +batch. No supplier, paid moment, runtime improvement or new kappa is claimed. + +The counterexample corrects the stated necessity of read-free children in +[PR1155](https://github.com/CrocSwap/integer-mult-bounds/pull/1155). Its retained +verifier reproduces both its original certificate and this new example. The +original failing-reader example remains valid; it does not establish necessity. +The added value is a checked applicability correction and a usable cut planner, +not a claim that linear cancellation or dynamic programming is new. + +## Five readers, one restoration + +Use scalar state D,W with arbitrary initial values. Each child first performs +`D += b_i W`, then `W = -W`, with reader coefficients + +``` +b = [1, 1, 1, -1, 1]. +``` + +Eager execution restores W after every child. Deferred execution lets it drift +until the batch ends. In both cases D ends at `D_initial + 3 W_initial`, and +one final negation restores deferred W. All five readers are nonzero, including +readers of the changed workspace. The restoration bill is five negations versus +one. With `D_initial=11,W_initial=7`, both end at `(32,7)`. + +After child two, eager D is 25 and deferred D is 11. Requiring an observation +and restoration there makes the optimal bill five again. Output timing is part +of the contract. This is not safe substitution under arbitrary prefix observers. + +## Reproduce and use + +Python 3.11 or newer, standard library only, from the repository root: + +```sh +rtk proxy python3 -I -O -B research/reader-restoration-cuts-seed53/verify.py +rtk proxy python3 -I -O -B research/reader-restoration-cuts-seed53/test_package.py +rtk proxy python3 -I -B research/reader-restoration-cuts-seed53/planner.py research/reader-restoration-cuts-seed53/fixture.json +``` + +The verifier prints +`PASS_READER_RESTORATION_CUTS restoration=5->1 forced_cut=5 exhaustive=2851 seeded=160`. +The package test reports relocation, canonical regeneration and four rejected +corruptions. The planner emits cost 1, cuts `[5]` and a final negation of coordinate +zero. Adding `"required": [2]` to a copy of the fixture yields cost 5 and all five +cuts. Coordinates are zero based; cuts count completed children, from one to r. + +Planner input contains `children`, each with equally sized integer `reader` and +`signs` arrays, and positive integer `prices` for complete coordinate negations. +Signs must be -1 or 1. Optional `overhead` is a nonnegative complete per-nonempty- +restoration dispatch charge. `required` lists mandatory cuts. An empty batch is +valid. Zero reader coefficients represent workspace-independent data work; +such independent increments can be added unchanged outside this model. + +## Exact criterion and proof + +Let D,W have N coordinates over a characteristic-zero field. Child i applies + +``` +D <- D + diag(b_i) W +W <- diag(g_i) W, g_ij in {-1,1}. +``` + +The child restores its private work and preserves all other data. Source and +target do not alias. There are no intermediate observers except declared cuts, +no hidden state, no rounding and no other dependence on W or old D. The eager +comparator restores W after each child. The planner accepts integer readers; +the proof itself also holds for rational or complex readers. + +For an interval [a,b), define `p_a=1` componentwise and +`p_(i+1)=g_i p_i`. Just before child i the deferred workspace is `p_i W_entry`. +The deferred-minus-eager data increment is therefore + +``` +diag(E_ab) W_entry, E_ab = sum_(i=a)^(b-1) b_i (p_i - 1). +``` + +The interval is correct for every input exactly when every coordinate of E_ab +is zero. Sufficiency follows by substitution. For necessity, a nonzero entry +is detected by its workspace basis vector. Applying the final diagonal sign +`p_b` restores W since each sign is its own inverse. Read-free intervals set +every b_i to zero, but they are only one sufficient case. The example above +has two nonzero residual terms that cancel. + +For general linear readers B_i and invertible workspace maps G_i the same +calculation gives `sum B_i(P_i-I)=0`, with ordered prefixes P_i. This is context +for the correction, not an implemented general-matrix optimizer. Unlike earlier +dirty-response transport, this tool changes no reader and moves no supplier gate. + +## Restricted optimum + +Every selected cut must reproduce eager D and W. This requirement applies even +to additional cuts introduced by the planner. A legal interval cannot cross a +mandatory cut. Its price is the sum of the supplied prices of the coordinates +with final sign -1, plus overhead if that set is nonempty. Identity restoration +emits no command and costs zero under this explicit model. + +Set `F(0)=0`. For b from one through r, minimize + +``` +F(b) = min_(legal [a,b)) F(a) + restore_price(a,b). +``` + +Every legal partition has a final interval and its preceding prefix is a legal +partition. Conversely, adjoining a legal interval to a correct prefix gives a +correct partition. Induction proves the recurrence gives the minimum in this +class. Ties use fewer segments, then lexicographic cuts. Single-child intervals +are always correct, so an input satisfying the schema always has a plan. + +This does not optimize schedules whose errors persist across an inserted cut +and cancel later, reordering, changed child implementations, non-diagonal +restorations, or arbitrary reversible programs. The literal-column checker +enumerates partitions independently and tests equality at every proposed cut. + +The implementation computes residuals and prefixes with O(r^2 N) integer +arithmetic operations, plus O(r^3) worst-case required-cut tests and tuple +copying/tie comparisons. Storage is O(r^2 N + r^2), including candidate masks +and saved cut tuples. Integer bit costs are additional. No precomputed plan or +descriptor is assumed free. + +## Complete node bill and precision + +Let C_i be the complete cost of child i under the deferred interface, including +its recursive descendants, source/coefficient accesses, private work and its +restoration, data readout, workspace sign change, routing and frame adapters. +The same fixed upper price and common precision must be valid for every allowed +incoming state and for both eager and deferred schedules. Children cannot have +unpriced dependence on the current workspace value. + +For node v, the complete conditional recurrence is + +``` +T_v = admission_v + preparation_v + planning_v + program_storage_and_reads_v + + sum_i T_child_i + sum_i local_child_work_i + + sum_(emitted restorations h) Restore_v(h) + + batch_control_v + routing_or_frame_work_not_in_children_v. +``` + +Here `T_child_i + local_child_work_i = C_i`. Restore_v must include reads, +negations, writes, mask/descriptor access, dispatch, head return and any private +work. If a backend realizes Restore_v as the supplied additive prices plus the +supplied overhead, the planner is optimal for that restoration term. Otherwise +this price model must not be used for that backend. Eager replaces the emitted +restorations by each child's inverse sign. All other terms stay explicitly +charged; different preparation/program/control costs must be compared too. +Repeated nodes use the displayed recurrence, paying planning where it occurs. +There is no claimed improvement to the selected unequal-rank child moment. + +For exact integer input bounds `|W_j|<=U`, `|D_j|<=V`, both schedules satisfy +`|W_j|<=U` and `|D_j|<=V+U sum_i |b_ij|` at all prefixes. Products obey the +same majorant. A sufficient common signed width is one plus the bit length of +the maximum of U, `V+U max_j sum_i |b_ij|`, and all coefficient magnitudes. +The fixture takes U=7,V=11 and seven signed bits. This is an exact integer +headroom bound, not a numerical rounding theorem. + +For the fixture, the specified scalar interpreter reads W,D and b,g per child, +multiplies bW, adds to D, writes D, and negates/writes W for g=-1. A restoration +reads W, negates it and writes W. Both programs execute five multiplies and five +adds, and read ten coefficients. Eager/deferred data reads are 15/11, data writes +15/11, negations 10/6 and program records 10/6. Each record's bit decoding and +travel cost, storage, initial admission, preparation and planner work are the +separate terms above. The interpreter also reverses the literal program. +These are counted operations, not a runtime benchmark or fixed-tape compiler. + +## Evidence, sources and remaining work + +[CERTIFICATE.json](CERTIFICATE.json) records 1,555 exhaustive scalar batches of +length zero through four, 1,296 exhaustive two-coordinate two-child batches, +and 160 deterministic seed-53 longer batches of length five through eight. +All binary cut masks are exhausted within each declared batch, after enforcing +mandatory cuts. The independent interpreter retains every D and W basis column. +The certificate records the exact partition counts. Finite tests support the +written proof; they are not a formal proof of the multiplication theorem. + +Controls change the cancelling reader, add an intermediate observation, reorder +a read around a workspace change, corrupt an emitted cost and mutate source or +certificate bytes. Nine input errors and one unknown CLI field are rejected. +The unchanged PR1155 certificate still passes. Its exact Batch implementation +also confirms the new construction on real and imaginary basis inputs and a +nontrivial dirty Gaussian input. No claim is made against its valid negative +example or its finite recorded counts. Its heterogeneous-cost discussion is +outside this contribution's scope. + +Base `1b59b624d21924f8e3537cdc1ac52d3be6eda2fe` selected PR1094 at conditional +kappa `836330098538459/500000000000000000`. [SOURCES.json](SOURCES.json) binds +the runtime predecessor files and records separate context-only selected pins. +The package replays offline from its own directory. It does not depend on a +future moving selected record. [CLAIM.md](CLAIM.md) records assignment, rejected +covered candidates, exact heads and overlap. [NOTICE.md](NOTICE.md) preserves +credit and license. [VALIDATION.md](VALIDATION.md) records environments and checks. + +Supplier realization, common labels and frames, whole-call hosting, fixed-tape +routing, precision/recovery beyond the exact integer model, and analytic transfer +remain unproved here. No selected source, frozen upstream file or other PR is +modified. No full cold replay or proof-assistant verification is claimed. diff --git a/research/paid-reader-defect-seed58/context/pr1205-README.md b/research/paid-reader-defect-seed58/context/pr1205-README.md new file mode 100644 index 0000000000..7ed4d89d17 --- /dev/null +++ b/research/paid-reader-defect-seed58/context/pr1205-README.md @@ -0,0 +1,263 @@ +# Observer-safe deferred dirty restoration + +**Recursive-interface research construction and correction; no new kappa.** +Adam Gall (@adamgall), with substantial OpenAI Codex assistance in the research, +proof, implementation, verification and writing. New material is Apache-2.0. + +## Result and provenance + +[PR1155](https://github.com/CrocSwap/integer-mult-bounds/pull/1155), Aaron Wang +(@navinor), proposes replacing per-child workspace restoration by one final +composed restoration. Its frozen README says this preserves final observables +“if and only if no child reads the workspace's intermediate value” and that +“one reader child breaks it”. Its exhibited bad reader is a valid counterexample +to *unrestricted* deferral, but cannot establish that necessity statement. + +This package gives the exact replacement criterion, a strictly larger constructive +class with nonzero readers, and the distinction between terminal and prefix +observations. It does not dispute PR1155's read-free examples or claim priority +for restoration coalescing. Its finite census is new evidence, not a finite +replay presented as an all-size proof. The proof below supplies the all-size +statement in the specified linear model. + +Base: `1b59b624d21924f8e3537cdc1ac52d3be6eda2fe`. PR1155 source head: +`9821c6e9388f3fc097e94b72be9fa7b41a849527`. The complete source README is +preserved byte-for-byte under `context/`, with attribution intact; `SOURCES.json` +pins it, the license and the base selected record. No predecessor verifier is +imported. The actual selected base result is PR1094, conditional +`kappa = 836330098538459/500000000000000000`, not an open PR headline. Its +[review](../../docs/research/community-batch1099-review.md) and actual +`research/complex-t16-rare-pattern-exchanges/README.md` were followed from the +selected certificate. This package does not modify that construction. + +Seed **52**, derived from fresh OS uint32 `3718171852` modulo 100. The seed picks +the recursive-interface track and the concrete odd arity `2 + (52 mod 7) = 5`. +`CLAIM.json` records the three candidates and overlap decisions. No pinned sprint +issue exists; the only open issues at claiming were #913 and #650, neither a +coordination issue. Scope was claimed locally before implementation and reserved +with the parent of the five independent rounds. Prior PRs #1114 and #1098 are +not reused as these rounds' deliverables. + +## Exact criterion + +Work over any field. Let data be `D in F^d`, borrowed workspace `W in F^w`, and +fixed child `i` perform + +``` +D <- D + B_i W (reads the pre-child workspace) +W <- G_i W (G_i invertible) +``` + +Read-only external-source increments may be added to both versions and cancel. +The children do not choose later matrices from intermediate data. Eager execution +applies `G_i^{-1}` after every child. Deferred execution applies only +`P_r^{-1}` at the end, where `P_0=I` and `P_i=G_i ... G_1`. + +**Terminal theorem.** The two programs agree on final `(D,W)` for every arbitrary +dirty input exactly when + +``` +Delta_r = sum_{i=1}^r B_i (P_{i-1} - I) = 0. +``` + +**Proof.** Before child `i`, eager workspace is `W_0`, and deferred workspace is +`P_{i-1} W_0`. Summing the respective data increments gives difference +`Delta_r W_0`. Both restore workspace to `W_0`. Equality on every `W_0` is +equivalent to the displayed matrix vanishing (test the basis columns). This is +an all-size algebraic proof, not an inference from the census. + +**Prefix theorem.** If data may be observed after every child, agreement requires +and is equivalent to `Delta_j=0` for every `j`. Subtracting consecutive equations +makes this equivalent to `B_i(P_{i-1}-I)=0` for each `i`. It does *not* require +`B_i=0`. These observations exclude the intentionally drifting workspace itself. +If that workspace must be observed in its entry coordinates, it must be restored +at that observation boundary. If a later control depends on data, use the prefix +criterion; terminal cancellation alone is not an admissible adaptive rewrite. + +### Two strict counterexamples to read-free necessity + +Let `G_i = [[1,1],[0,1]]` for three children and write workspace `(a,b)`. + +1. `B_i=(0,1)` for every child. Each child reads nonzero dirty data `b`, yet + drift changes only `a`. Every data prefix agrees; both final programs return + `(D+3b,a,b)`. Final restoration is `a <- a-3b`. +2. `B_1=(0,0), B_2=(2,0), B_3=(-1,0)`. Child 2 genuinely reads the changed + value `a+b`; child 3 reads `a+2b`. Deferred data increment is + `2(a+b)-(a+2b)=a`, equal to eager `2a-a=a`. The intermediate data difference + after child 2 is `2b`, so this batch is terminal-safe but not prefix-safe. + +The second example directly addresses observable reads of the changing component, +not just a reader that happens to avoid it. + +## Constructive family and fully paid local invoice + +For a square-zero drift `U=uv^T` with `v^T u=0`, take `G_i=I+alpha_i U`. +Then `P_i=I+(sum_{k<=i}alpha_k)U`, and its inverse subtracts that coefficient. +Every `B_i` with `B_i u=0` is prefix-safe, even if nonzero. This supplies a family +at arbitrary dimension and arity. Its cheap implementation below uses coordinate +`u=e_a,v=e_b`, rather than pretending a dense outer product costs one primitive. + +There are three length-`N` streams `D,a,b`. The concrete child shell is +`D += b; a += alpha_i b`, with each `alpha_i` equal to `+1` or `-1`. +Every source access is retained; no clean copy of `a` or `b` is required. +Eager additionally executes `a -= alpha_i b` after each shell. Deferred executes +`a -= S b` once, where `S=sum alpha_i`, skipping it only when `S=0`. + +Count a signed ADD as one scalar primitive and a nonunit constant multiplication +as one additional primitive; this is an exact-arithmetic accounting convention, +not the selected complex real-primitive backend. Let `h=[S!=0]` and +`m=[abs(S)>1]`. At one node the complete shell invoice is: + +| Work | Eager | Deferred | +|---|---:|---:| +| nonzero-reader ADDs | rN | rN | +| forward workspace ADDs | rN | rN | +| restoration ADDs | rN | hN | +| nonunit constant MULs | 0 | mN | +| total scalar primitives | 3rN | (2r+h+m)N | + +Each ADD reads two data scalars and writes one; each extra multiplication reads +one scalar and writes one reusable scalar temporary. Thus reads are +`2*ADD+MUL`, writes `ADD+MUL`, and peak allocated data is `3N+m` scalars (the +extra scalar may be reused across all nodes). Constants and event descriptors are +read-only program data. For the frozen family they are compile-time constants; +constructing a general coefficient sum costs `r-1` descriptor additions once per +node specification, not an uncharged data pass. Forward shears, output updates, +final restoration, accesses and any temporary are all included. There are no +frame changes, initialized auxiliary streams, source copies, or omitted inverse +recursive calls in this explicitly specified program. + +All-positive coefficients give `S=r`, so the priced saving is `(r-2)N`, not +`(r-1)N`: the multiplication by `r` is paid. The seed-selected odd-five family +`(1,-1,1,-1,1)` gives `S=1`, so every command is an ADD: **15N -> 11N**, a saving +of **4N**. Scratch really drifts at children 2 and 4, while each reader still +sees the invariant stream. This is not merely omitting an identity restoration. + +## Complete recursion and precision boundary + +To make the child term explicit, `emit` constructs an actual recursive program. +At depth `d>0`, split each stream into `r` disjoint equal partitions. For each +child `i`, first invoke the depth-`d-1` source-restoring program on partition `i` +with its arbitrary current dirty `a`, then execute that child's full-`N` shell +above. Eager restores after each shell, deferred only at node exit. A leaf is +the identity and has zero cost. Children can run with drifted `a` because every +data read depends only on invariant `b`; by induction all children restore their +entry workspace. Each position receives `r*d` additions of its own `b`. + +For `N=r^d`, the full recurrences, including all recursive work, are + +``` +E_0(N)=F_0(N)=0 +E_d(N)=r E_{d-1}(N/r) + 3rN +F_d(N)=r F_{d-1}(N/r) + (2r+h+m)N +E_d(N)=3rNd; F_d(N)=(2r+h+m)Nd. +``` + +These equations count scalar arithmetic, not free machine dispatch. There are +`J=(r^d-1)/(r-1)` internal nodes, `rJ` recursive child invocations, and respectively +`3rJ` or `(2r+h)J` stream events. Charging `C_call` per recursive invocation, +`C_event` per event and `C_step` per scalar loop iteration adds exactly +`rJ*C_call + events*C_event + ADD*C_step` in this abstract controller model, +plus the separately tabulated data reads/writes. An event's five immutable +descriptor fields can be charged five descriptor reads within `C_event`. +Routing is an ordered contiguous scan of the named partition, not a free +permutation. A streaming recursive realization keeps an `O(d)` index stack +and the fixed `r` coefficients besides the stated data; it need not materialize +the word. The verifier deliberately materializes the complete event list +(`5*events` descriptor scalars) for independent reversal and replay. Neither +its Python memory use nor its runtime is claimed to attain the streaming +resource bound. All extra controller terms and the reader/scratch work remain; +only the displayed restoration events disappear. + +The inverse program reverses all events and negates coefficients, without new +storage; its scalar invoice is identical. `verify.py` replays both directions +on every basis column of all three dirty streams for depths 0..3 and arities 3 +and 5. The zero-cost identity leaf is part of this completely implemented +restoration experiment, not a placeholder for a promised supplier. A real leaf +backend of cost `L` would add `r^d L` to *both* recurrences and must independently +satisfy this reader/restoration contract. + +For integer inputs of magnitude at most `M`, unit shells along a depth-`d` path +keep both data and scratch magnitudes at most `(1+rd)M`; the temporary for a +nonunit restoration is at most `rM`. Consequently adding +`ceil(log2(1+rd))` magnitude bits (plus a sign bit under an unsigned-magnitude +convention) suffices in this integer model. The code uses unbounded exact Python +integers and Fractions. No fixed-tape implementation, rounded complex arithmetic +contract, native compiler, or supplier precision admission is claimed. This +boundary is distinct from the rounded-leaf obstruction in PR1135 and modular +borrowing in PR1159; it does not evade those results. + +## Reproduction, domain and controls + +From the repository root, Python 3.10+, standard library only: + +```sh +python3 -I -O -B research/observer-safe-restoration/verify.py +``` + +The command authenticates the pinned source/context bytes, recomputes every +certificate field and compares `EXPECTED.json`. It never writes by default. +`--write NEW_PATH` creates a fresh certificate and refuses to overwrite one. +No randomized search or tolerance acceptance is used. + +For one complete relocated replay followed by an actual source-corruption +subprocess rejection (without repeating the expensive census for the corrupt +source), run: + +```sh +python3 -I -O -B research/observer-safe-restoration/test_package.py +``` + +Its final marker is +`PASS_OBSERVER_RESTORATION_PACKAGE relocation=1 source_corruption=1`. + +The bounded census is all **46,656** three-child tuples: each `G_i` is one of +four integral shears `I +/- E_12`, `I +/- E_21`; each row reader is one of the nine +vectors in `{-1,0,1}^2`. Full 3-by-3 state-operator composition is compared with +the separately computed two-dimensional defect. The signed coefficient domain, +three-child stopping rule and complete coverage are fixed before execution. +This census is not an impossibility theorem outside its domain. A noncommuting +rational fixture additionally checks the formula with genuine denominators. + +The completed census finds **7,776 terminal-safe** tuples, of which **6,048** +are prefix-safe and **1,728** are terminal-only. **7,712** terminal-safe tuples +contain a nonzero reader. Recursive forward/inverse replay covers **588** +dirty-state basis columns across eight `(arity,depth)` instances. At arity five, +depth three and `N=125`, the complete emitted scalar invoice is **5,625 -> 4,125 +ADDs** (zero constant multiplications), saving 1,500 ADDs with the same 375 dirty +data scalars. These are emitted-program counts, not a runtime measurement. + +Six meaningful controls require failure: a reader outside the drift annihilator, +observing an unsafe prefix of a terminal-cancelling batch, wrong inverse order +for noncommuting shears, omitted final restoration, changing a shear direction, +and a defect hidden by testing only zero-initialized dirty helpers. These are +mathematical counterexamples, not failed searches. The exact receipt records +classification counts, all recursive invoices and the explicit rational defect. + +Only this isolated package's checks are relevant. No selected cold replay, +repository-wide `make verify`, remote CI or proof-assistant build is claimed. +The universal theorem is the written argument above; finite tests check the +implementations and exhibited failures. Selected all-size/compiler, +common-label/mutable-source, hosting, precision/tape, analytic and bit H1-H5 +assumptions remain untouched. No new multiplication exponent or admitted paid +supplier profile follows from saving these boundary primitives. + +## Related work and credit + +Aaron Wang / Navinor's PR1155 is the direct predecessor and supplies the model, +coalescing direction and source text corrected here. Its own credits to Chafik +Boukhalfa's dirty-connector work, Gareth Davidson, Ross Richardson, Douglas +Colkitt and the retained complex batching recurrence are preserved in the frozen +README. PR1012 and PR974 price restoration at hosted-assembly level; this package +changes the operator admissibility class, not their rank-mass conclusion. +PR1057/1164 concern borrowed-port echo allocation, and PR1135/1159 concern exact +versus rounded/modular contracts; none is a dependency of this implementation. +PR889 (`e2021d1c9e06948528cbc0a8fd7079b671da981d`) batches common-factor +product shears with a query-minimal one-connector word. It does not supply this +observer defect criterion. PR1105 (`20a960b545f4b0ade4f26922ef686bd5eaf275f4`) +audits projected cleanup with target feedback in PR543; our children have no +data-to-workspace feedback and use full inverse workspace restoration. These +nearby algebraic interfaces are distinct and their negative conclusions are +not reopened. +Substantial OpenAI Codex assistance is disclosed above; no independent human or +formal review is asserted. The repository Apache-2.0 license is retained locally. diff --git a/research/paid-reader-defect-seed58/context/pr1227-README.md b/research/paid-reader-defect-seed58/context/pr1227-README.md new file mode 100644 index 0000000000..ade3f00abb --- /dev/null +++ b/research/paid-reader-defect-seed58/context/pr1227-README.md @@ -0,0 +1,240 @@ +# Output sign frames replace large workspace restorations + +This is a recursive-interface research construction with a sharp boundary +cost in a restricted model. It does not improve the selected multiplication +exponent. With five fixed children, an eight-coordinate dirty workspace and +one output coordinate, a complete source-dependent echo uses **96 ADD + 104 +NEG**, versus **96 ADD + 160 NEG** with eager restoration. Both restore every +scratch coordinate on every input. The saving is 56 scalar negations. + +The restriction matters: child calls are indivisible. The parent may negate +either the whole output register or the whole workspace between calls. A +compiler that can remove a child's internal drift can beat both words. For +example, the explicit matrix leaves below expose their final negations; direct +evaluation of their sum is cheaper than the echo. This is an exact interface +result, not an optimized matrix algorithm or a runtime benchmark. + +## Interface and exact boundary cost + +Work over the integers, rationals or complex numbers with exact arithmetic. +Let `D` have width `d`, `W` have width `N`, and let fixed children satisfy + +``` +C_i(D,W) = (D + R_i W, -W), i = 1,...,k. +``` + +Each `R_i` is a linear map. A child's private scratch is arbitrary and restored; +its cost includes its reader, source access, source negation and private work. +The caller has both execution directions at the same declared scalar cost. +These children are involutions, but the implementation still emits the literal +reverse word for inverse calls. No sign-controllable reader is assumed. + +The desired batch is `B(D,W)=(D + (sum_i R_i)W,W)`. Eager execution restores +`W` after every child, for `kN` additional scalar NEG instructions. The parent +can instead execute these operations: + +1. Call the first child directly. +2. Before each subsequent child, negate all `d` output coordinates. +3. At exit, negate `W` if `k` is odd, or negate `D` if `k` is even. + +Before child `i`, both registers are in sign `(-1)^(i-1)` relative to the +canonical eager state. Linearity makes the child's increment have that same +sign. It then flips `W`, and the next output negation aligns the two signs +again. The final operation restores both canonical registers. This proves the +batch identity for every dimension and every tuple of linear maps, including +nonzero readers of every changing workspace coordinate. + +The additional cost of this schedule is `2 floor(k/2)d + (k mod 2)N`. +Choosing it when `d=k`. Restoration also +requires `a = k mod 2` and `b = 0 mod 2`. Minimizing `aN+bd` under these +constraints gives the displayed formula, and the two schedules attain it. +Operations in the entrance gap cannot improve this lower bound. + +Thus `d>=N` yields no saving in this model. For `d