diff --git a/research/rational-residue-scope/CASE.json.gz b/research/rational-residue-scope/CASE.json.gz new file mode 100644 index 0000000000..b0f0fefb5e Binary files /dev/null and b/research/rational-residue-scope/CASE.json.gz differ diff --git a/research/rational-residue-scope/CLAIM.json b/research/rational-residue-scope/CLAIM.json new file mode 100644 index 0000000000..b8c1436822 --- /dev/null +++ b/research/rational-residue-scope/CLAIM.json @@ -0,0 +1,47 @@ +{ + "task_id": "pass22-consolidation99-exact-rational-residue-scope", + "seed": 99, + "track": "research consolidation", + "catalogue_card": "scope-navigation", + "base_commit": "1b59b624d21924f8e3537cdc1ac52d3be6eda2fe", + "claimed_at_utc": "2026-10-13T20:01:17.007812+00:00", + "expires_at_utc": "2026-10-13T22:01:17.007812+00:00", + "instruction_revision": "6d8cffe3dcb0680b68ae8a9d79b98e6e719f1f34", + "selection_note": "The legacy seed99 draw preceded detection of the updated gist. Keep the already assigned consolidation task; use current repository coordination and scope guidance.", + "candidates": [ + { + "question": "Reconcile PR1135 rational numerator width with PR1159 binary residue backend", + "decision": "chosen: explicit unit-denominator/integral-output boundary, with a source-bound application and failure witnesses" + }, + { + "question": "Retained PR1015 B-block attribution", + "decision": "defer: PR1181 already supplies the retention receipt" + }, + { + "question": "PR279 parent-source inventory", + "decision": "defer: PR1190 already supplies the complete Git-tree reconstruction" + } + ], + "predecessors": { + "PR1057": "78a062df1dcab2bffea5ff4d8243f3da6e465414", + "PR1135": "4c35687d7c0da8e6cf33f17e418ecf31c95ff3ad", + "PR1159": "f38bfe5da0bed21f42ce5251d23491a56519d7c4" + }, + "scope": "Compare three exact contracts: arbitrary additive rational echo, common-denominator numerator storage, and quotient-register storage. Extend only the algebraic interpretation of PR1159 to reduced odd-denominator rational matrices whose completed output is integral and has a strict signed bound. Rounded leaves and nonintegral output decoding are explicitly excluded; even reduced denominators are not units modulo 2^w.", + "method": "Prove the localization homomorphism and source-bound applicability table; run a centrally rescaled rational version of the frozen 52-factor PR1159 program with alternating 1/3 and3 factors, unchanged integral full product, and all literal modular primitives. Independent Fraction-prefix and dirty-basis replay; exact residue inverses and full additional coefficient-preparation invoice. Bounded small odd-denominator/matrix cases, failures for nonunit denominator, false integrality, wrapping, rounded substitution and bad inverses.", + "budget": "About 70 minutes from19:54 UTC; at least final25% validation/packaging; no broad rational reconstruction or rounded repair search. Stop on a failed homomorphism or unpaid interface; at most one bounded pivot.", + "optimistic_complete_cost": "Inherited1376 calls, five length-two data arrays and four private work registers. If all coefficient denominators are units, the kernel stays52292 commands and56-bit data for the same integer endpoint bound. Price inverse preparation, every coefficient conversion, checks, input/output conversion, control, routing and all original descriptor storage separately. No q^D initialization for residue data; no claim it removes PR1135 cost for its different exact numerator representation.", + "coordination": "Read Discussions1163/1166/1167 and all active threads; no overlapping claim. Open PRs through1190, including1159/1135/1164 and1181/1190. Public scoped claim authorized by updated user gist.", + "status": "completed; submitted", + "attribution": "Gareth Davidson with substantial OpenAI Codex assistance; Ali Romman PR1135, Davidson PR1057/1159 and their credited source lineage; modular localization is classical, no priority claim.", + "completed_at_utc": "2026-10-13T20:38:24.272420+00:00", + "submission_base": "49b3157d1d89adcef16df8be98445451672be5ba", + "mathematical_head": "7961d6ab49181a0cfd5813daccdae89ea904ece6", + "pr": "https://github.com/CrocSwap/integer-mult-bounds/pull/1229", + "discussion": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1202", + "scope_status": "changed; executable comparison broader than original navigation card", + "result": "52 rational factors,1376 unchanged calls; exact least prefix denominator9;94-bit sufficient common-numerator data versus56-bit residue data, neither numerator minimum nor runtime comparison;2406 paid preparation commands plus52292 kernel commands; rounded and nonintegral output boundaries excluded; no kappa.", + "validation": "Complete Python3.14 and read-only isolated optimized3.12 replay receipts agree. Registered metadata/replay pass;8 package tests and25 selected/source-binding tests pass;12 mathematical/admission/price controls.", + "receipt_sha256": "2c63ba9c68e4537a49815af076b9097ae49c3f5a7ca66229710455b9d3aed6e2", + "final_overlap": "20:35 UTC;836 open PRs through1228,6 Discussion threads and comments,324 local records; complete pagination,no warnings. Relevant predecessor heads unchanged; declared search coverage is not a novelty certificate." +} diff --git a/research/rational-residue-scope/EXPECTED.json b/research/rational-residue-scope/EXPECTED.json new file mode 100644 index 0000000000..397273c975 --- /dev/null +++ b/research/rational-residue-scope/EXPECTED.json @@ -0,0 +1,618 @@ +{ + "admission_rational_product_ops": { + "adds": 416, + "multiplies": 416, + "scope": "Additional arbitrary-precision product check; operand sizes, normalization, descriptors, norm guard and routing are separate paid terms" + }, + "basis": [ + { + "columns": 10, + "common_numerator_bound": "7793009394993530082268099074", + "common_numerator_sufficient_bits": 94, + "denominator_witness": { + "column": 0, + "leaf": 80, + "row": 8, + "value": [ + -2584, + 9 + ] + }, + "endpoint_direction": 1, + "leaf_prefixes": 1376, + "least_common_prefix_denominator": 9, + "rational_absolute_prefix_bound": [ + 865889932777058898029788786, + 1 + ] + }, + { + "columns": 10, + "common_numerator_bound": "7793009394991748258988883689", + "common_numerator_sufficient_bits": 94, + "denominator_witness": { + "column": 0, + "leaf": 592, + "row": 8, + "value": [ + -2584, + 9 + ] + }, + "endpoint_direction": -1, + "leaf_prefixes": 1376, + "least_common_prefix_denominator": 9, + "rational_absolute_prefix_bound": [ + 865889932776860917665431521, + 1 + ] + } + ], + "bounds": { + "endpoint_radius": [ + 31525197391593479, + 1 + ], + "product_norm_bound": [ + 4503599627370496, + 1 + ], + "width": 56 + }, + "case_sha256": "043fdf6821548ed74e94b8635cd4ec3f0ae278efd66321bc2ba9c1ff9b46446c", + "comparison": { + "conservative_denominator": "10301051460877537453973547267843", + "conservative_denominator_bits": 104, + "conservative_numerator_sufficient_bits": 194, + "formal_prefix_degree": 65, + "least_common_prefix_denominator": 9, + "numerator_sufficient_bits": 94 + }, + "controls": { + "counterexamples": { + "nested_rounded_helper": { + "final": [ + -2, + -5, + 0, + -1, + -2 + ], + "initial": [ + -2, + -2, + 0, + -2, + -2 + ] + }, + "nonintegral_residue": 11, + "nonintegral_signed_decode": -5, + "rounded_integral_product": { + "final": [ + 1, + 0, + 2, + -1, + 3 + ], + "initial": [ + 1, + 0, + 2, + -1, + 3 + ] + } + }, + "positive_controls": [ + "2/6 normalizes to unit denominator 3" + ], + "rejected": [ + "even reduced denominator", + "odd denominator but nonintegral completed map", + "integral endpoint beyond signed range", + "equality at signed cap", + "zero map cannot hide nonrepresentable source", + "bad prepared inverse/coefficient", + "omitted inverse update move", + "unpaid inverse table", + "unpaid preparation head travel", + "boolean width", + "raw denominator exceeds priced preparation workspace", + "common numerator denominator three is insufficient" + ] + }, + "format": "rational-residue-scope-receipt/1", + "initial_sets": [ + [ + [ + 7, + -7 + ], + [ + -3, + 5 + ], + [ + 36028797018963967, + -18014398509481984 + ], + [ + -36028797018963968, + 123 + ], + [ + 17, + -91 + ] + ], + [ + [ + 7, + -7 + ], + [ + -3, + 5 + ], + [ + 2, + -4 + ], + [ + -7, + 6 + ], + [ + 5, + -1 + ] + ] + ], + "kernel": { + "accesses": 16512, + "address_bits": 8, + "address_events": 16512, + "coefficient_bits": 11648, + "commands": 52292, + "counts": { + "add": 8256, + "add_a": 5504, + "add_v": 2752, + "coeff": 5504, + "low": 13760, + "low_a": 5504, + "low_p": 5504, + "low_v": 2752, + "mul": 5504, + "read": 8256, + "write": 2752, + "zero": 8260, + "zero_a": 4129, + "zero_c": 1377, + "zero_p": 1377, + "zero_v": 1377 + }, + "data_bit_actions": 924672, + "data_bits": 560, + "decoded_target_cells": 2, + "head_bit_moves": 76431616, + "intercell_steps": 1332416, + "leaves": 1376, + "preparation_reductions": 212, + "program_bits": 17888, + "program_forward_and_rewind_bits": 35776, + "program_read_bits": 17888, + "program_record_bits": 13, + "work_bits": 283 + }, + "kernel_plus_priced_preparation_commands": 54698, + "new_kappa_claim": false, + "preparation": { + "commands": 2406, + "counts": { + "check_odd": 2, + "check_one": 2, + "low": 454, + "move": 12, + "mul": 234, + "read_denominator": 210, + "read_inverse": 208, + "read_numerator": 208, + "set_one": 2, + "subtract": 12, + "write_coefficient": 208, + "write_inverse": 2, + "zero": 852 + }, + "descriptor_layout": { + "coefficient_start": 560, + "denominator_bits": 2, + "descriptor_start": 12320, + "inverse_start": 12208, + "numerator_bits": 3 + }, + "external_memory": { + "accesses": 836, + "bit_actions": 24452, + "data_coefficient_inverse_descriptor_bits": 13360, + "head_bit_moves": 5438192, + "interfield_bit_travel": 5390960, + "trace_sha256": "bf8c73783982890055356730e2eaf8e0896ecb8674a064ee8f56ccf9efde7508" + }, + "inverse_commands": 114, + "inverse_counts": { + "check_odd": 2, + "check_one": 2, + "low": 38, + "move": 12, + "mul": 26, + "read_denominator": 2, + "set_one": 2, + "subtract": 12, + "write_inverse": 2, + "zero": 16 + }, + "inverse_table": [ + [ + 1, + 1 + ], + [ + 3, + 48038396025285291 + ] + ], + "inverse_table_bits": 112, + "iterations": { + "1": 6, + "3": 6 + }, + "original_descriptor_bits": 728, + "original_descriptor_fixed_bits": 1040, + "work_bits": 283, + "work_peaks": { + "a": 72057594037927935, + "c": 48038396025285291, + "p": 3461531239023218395001132873504085, + "v": 72057594037927935 + } + }, + "replays": [ + { + "denominator_peak": 9, + "final_residues": [ + [ + 7, + 72057594037927929 + ], + [ + 88103883172, + 142555077523 + ], + [ + 36028797018963967, + 54043195528445952 + ], + [ + 36028797018963968, + 123 + ], + [ + 17, + 72057594037927845 + ] + ], + "leaf_prefixes": 1376, + "numerator_peak_signed_bits": 90, + "primitive": { + "accesses": 16512, + "commands": 52292, + "counts": { + "add": 8256, + "add_a": 5504, + "add_v": 2752, + "coeff": 5504, + "low": 13760, + "low_a": 5504, + "low_p": 5504, + "low_v": 2752, + "mul": 5504, + "read": 8256, + "write": 2752, + "zero": 8260, + "zero_a": 4129, + "zero_c": 1377, + "zero_p": 1377, + "zero_v": 1377 + }, + "data_bit_actions": 924672, + "head_bit_moves": 76431616, + "intercell_steps": 1332416, + "leaves": 1376, + "nontrivial_reductions": { + "a": 679, + "p": 3696, + "v": 1303 + }, + "work_bits": 283, + "work_peaks": { + "a": 144115188075853261, + "c": 72057594037927933, + "p": 5192296858534810046477551074804435, + "v": 144115188075855740 + }, + "work_widths": { + "a": 57, + "c": 56, + "p": 112, + "v": 58 + } + }, + "target": [ + 88103883172, + 142555077523 + ] + }, + { + "denominator_peak": 9, + "final_residues": [ + [ + 7, + 72057594037927929 + ], + [ + 72057505934044758, + 72057451482850423 + ], + [ + 36028797018963967, + 54043195528445952 + ], + [ + 36028797018963968, + 123 + ], + [ + 17, + 72057594037927845 + ] + ], + "leaf_prefixes": 1376, + "numerator_peak_signed_bits": 90, + "primitive": { + "accesses": 16512, + "commands": 52292, + "counts": { + "add": 8256, + "add_a": 5504, + "add_v": 2752, + "coeff": 5504, + "low": 13760, + "low_a": 5504, + "low_p": 5504, + "low_v": 2752, + "mul": 5504, + "read": 8256, + "write": 2752, + "zero": 8260, + "zero_a": 4129, + "zero_c": 1377, + "zero_p": 1377, + "zero_v": 1377 + }, + "data_bit_actions": 924672, + "head_bit_moves": 76431616, + "intercell_steps": 1332416, + "leaves": 1376, + "nontrivial_reductions": { + "a": 648, + "p": 3643, + "v": 1423 + }, + "work_bits": 283, + "work_peaks": { + "a": 144115188075853261, + "c": 72057594037927933, + "p": 5192296855275867221704489597031874, + "v": 144115188075855752 + }, + "work_widths": { + "a": 57, + "c": 56, + "p": 112, + "v": 58 + } + }, + "target": [ + -88103883178, + -142555077513 + ] + }, + { + "denominator_peak": 9, + "final_residues": [ + [ + 7, + 72057594037927929 + ], + [ + 88103883172, + 142555077523 + ], + [ + 2, + 72057594037927932 + ], + [ + 72057594037927929, + 6 + ], + [ + 5, + 72057594037927935 + ] + ], + "leaf_prefixes": 1376, + "numerator_peak_signed_bits": 48, + "primitive": { + "accesses": 16512, + "commands": 52292, + "counts": { + "add": 8256, + "add_a": 5504, + "add_v": 2752, + "coeff": 5504, + "low": 13760, + "low_a": 5504, + "low_p": 5504, + "low_v": 2752, + "mul": 5504, + "read": 8256, + "write": 2752, + "zero": 8260, + "zero_a": 4129, + "zero_c": 1377, + "zero_p": 1377, + "zero_v": 1377 + }, + "data_bit_actions": 924672, + "head_bit_moves": 76431616, + "intercell_steps": 1332416, + "leaves": 1376, + "nontrivial_reductions": { + "a": 678, + "p": 3635, + "v": 1268 + }, + "work_bits": 283, + "work_peaks": { + "a": 144115188075855853, + "c": 72057594037927933, + "p": 5192296858534827124127338063724556, + "v": 144115188075855869 + }, + "work_widths": { + "a": 57, + "c": 56, + "p": 112, + "v": 58 + } + }, + "target": [ + 88103883172, + 142555077523 + ] + }, + { + "denominator_peak": 9, + "final_residues": [ + [ + 7, + 72057594037927929 + ], + [ + 72057505934044758, + 72057451482850423 + ], + [ + 2, + 72057594037927932 + ], + [ + 72057594037927929, + 6 + ], + [ + 5, + 72057594037927935 + ] + ], + "leaf_prefixes": 1376, + "numerator_peak_signed_bits": 48, + "primitive": { + "accesses": 16512, + "commands": 52292, + "counts": { + "add": 8256, + "add_a": 5504, + "add_v": 2752, + "coeff": 5504, + "low": 13760, + "low_a": 5504, + "low_p": 5504, + "low_v": 2752, + "mul": 5504, + "read": 8256, + "write": 2752, + "zero": 8260, + "zero_a": 4129, + "zero_c": 1377, + "zero_p": 1377, + "zero_v": 1377 + }, + "data_bit_actions": 924672, + "head_bit_moves": 76431616, + "intercell_steps": 1332416, + "leaves": 1376, + "nontrivial_reductions": { + "a": 662, + "p": 3635, + "v": 1495 + }, + "work_bits": 283, + "work_peaks": { + "a": 144115188075855853, + "c": 72057594037927933, + "p": 5192296858534827124127338063724556, + "v": 144115188075855869 + }, + "work_widths": { + "a": 57, + "c": 56, + "p": 112, + "v": 58 + } + }, + "target": [ + -88103883178, + -142555077513 + ] + } + ], + "small_cases": { + "cases": 144, + "commands": 120780, + "denominators": [ + 3, + 5, + 7 + ], + "dimensions": [ + 1, + 2, + 3 + ], + "directions": 2, + "factor_counts": [ + 1, + 8 + ], + "leaf_prefixes": 2862 + }, + "source_manifest_sha256": "4f00d12b750879c6697d61f8be93baeb32e9a89d4512d2395fdaaf3021fc70a6", + "unit_census": { + "nonunit_exclusions": 120, + "quotient_addition_cases": 65520, + "unit_inverse_cases": 128, + "widths_addition": [ + 1, + 6 + ], + "widths_units": [ + 1, + 8 + ] + } +} diff --git a/research/rational-residue-scope/LICENSE b/research/rational-residue-scope/LICENSE new file mode 100644 index 0000000000..261eeb9e9f --- /dev/null +++ b/research/rational-residue-scope/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/rational-residue-scope/NOTICE.md b/research/rational-residue-scope/NOTICE.md new file mode 100644 index 0000000000..7624c6019f --- /dev/null +++ b/research/rational-residue-scope/NOTICE.md @@ -0,0 +1,31 @@ +# Attribution and license + +Consolidation, rational/residue comparison, preparation interpreter and checks: +**Gareth Davidson (@bitplane)**, with substantial **OpenAI Codex assistance**. +Apache-2.0. No subagents, independent human review, or proof-assistant review. + +- **Ali Romman, PR1135**, supplies the rounded-borrowing contract, precise + translation and summary hypotheses, exact common-denominator comparison, + formal prefix-degree routine and nearest-rounding convention. Its proof + already excludes cancelled kernels from its endpoint denominator lower bound. + The original package proof, README, contracts, license and notice are preserved. +- **Gareth Davidson PR1057 and PR1159** supply the additive borrowing word, + three-dirty-array allocator, fixed 52-factor fixture, literal bounded-register + modular backend, endpoint guard and paid invoice. Their source programs and + notices are unchanged. Credit retained by those notices includes **shhxera + PR822**, **androolloyd PR673**, **Sagar Thakrar PR730**, **Chafik Boukhalfa + PR628**, and the Ben-Or–Cleve register principle. +- Modular localization, unit inversion by Newton doubling, and signed residue + recovery are classical. No priority is claimed for these algebraic facts. + The source-bound applicability comparison and its explicit charges are the + contribution. The localization property is recorded in the + [Stacks Project, Proposition 10.9.3](https://stacks.math.columbia.edu/tag/00CP); + no external source code or proof text is copied from that reference. +- **woklerx PR1164** extends arity; **Navinor PR1155** changes batch restoration. + Those are separate mechanisms and are not imported as savings here. +- Source-container versus decoded-artifact handling follows the repository's + guidance credited to **Maxime Fleury** and **Antoine Olivier**. + +The recorded selected context is **Rohan Arun PR1094**, with its credited +complex/owner chain and **DreamingOfClouds PR589** on **eumemic PR555/543** for +bits. No selected source, frontier or predecessor disposition is changed. diff --git a/research/rational-residue-scope/PROOF.md b/research/rational-residue-scope/PROOF.md new file mode 100644 index 0000000000..881c7e6941 --- /dev/null +++ b/research/rational-residue-scope/PROOF.md @@ -0,0 +1,184 @@ +# Representation and restoration boundaries + +## 1. The exact algebraic interface + +Let `S` be the rational numbers whose reduced denominator is odd, and let +`M=2^w`, `w>=1`. Define + +```text +phi(a/b) = a * b^(-1) mod M, gcd(b,2)=1. +``` + +Every such b is a unit modulo M. If `a/b=c/d`, then `ad=bc`; multiplying that +identity by the two unit inverses proves that phi is independent of the +representation. Common denominators directly prove preservation of addition, +subtraction and multiplication. Thus phi is a ring homomorphism from S to +`Z/MZ`. This is the standard localization property, also stated in the +[Stacks Project, Proposition 10.9.3](https://stacks.math.columbia.edu/tag/00CP). +No new algebraic result is claimed for it. + +An L-by-L matrix over S induces an additive map on `(Z/MZ)^L` by entrywise phi. +Its matrix need not be invertible: a leaf is the shear +`target += sign * A source`, whose inverse negates the sign. The credited +PR1057 borrowing induction therefore applies unchanged to every ordered +binary/ternary tree and arbitrary dirty residue arrays. No commutation of +matrix factors is required. The resulting map is the reduction of the exact +rational product; all other data rows restore, including borrowed ancestor +ports. Equality of residues gives equality of their stored w-bit patterns. + +This general additive-group scope already belongs to PR1057. PR1159 implements +the integer-factor special case. Here only coefficient preparation and the +source-bound interpretation are extended; its actual dense backend is unchanged. + +## 2. Integer recovery and its limits + +Suppose the external source x and initial output y are integer vectors with +norm bounds X,Y. Let `P=A_(n-1)...A_0`, and require that `P x` is integral on +the admitted source domain. A sufficient stronger admission is that every +entry of P is an integer; that is what this package's generic checker tests. +Let `K_i=||A_i||_infinity` and `R=Y+X product(K_i)`. If + +```text +2^(w-1) > max(X,R), +``` + +then both source and completed output have unique signed representatives. +The residue endpoint decodes to exactly `y + sign*P x`. Dirty helpers require +no small norm or coarse-lattice promise; they start as arbitrary w-bit patterns +and return unchanged. Internal boundaries are residues, with no signed decoding. +The actual supplied x,y must meet the declared X,Y bounds; the code checks them. + +Three missing hypotheses have different failure modes. + +- A reduced even denominator cannot be inverted modulo `2^w`: for instance + `2z=1` has no solution. There is no unital ring map sending 1/2 into this ring. + Restricted source lattices or a different modulus need another contract and + implementation. A raw denominator may cancel: `2/6=1/3` is a valid unit case. +- Small absolute rational magnitude does not imply integer recoverability. + `1/3 mod16=11`, which signed-decodes to `-5`. Integrality or another proved + reconstruction interface is indispensable. +- Omitting the signed guard can wrap an integral endpoint. Its X term is also + necessary for unchanged-input representation when a zero factor makes the + output small. Equality at the stated strict cap is rejected. + +The tested family has `A_i = 3^(e_i) U_i`, where the U_i are PR1159's integer +matrices and `e_i=-1,+1` alternately for 52 factors. Since their sum is zero, +P is exactly the original integer product. All norms are `2*3^(e_i)`, so +their product is `2^52`. The same endpoint radius as PR1159 admits w=56. + +## 3. What the numerator comparison establishes + +PR1135 Section 7 uses a common denominator `q^D`, where D is the largest formal +factor degree at any prefix of the literal word. Its source routine gives +D=65 here, larger than the root's 52 factors. That construction is sufficient; +it does not claim `q^D` is the minimum for concrete cancelling coefficients. +Its endpoint lower bound for repeated coprime scalar p/q factors explicitly +excludes denominator-cancelling kernels. + +An independent Fraction matrix interpreter computes every actual prefix on +all ten integer input columns. The lcm of all entry denominators is nine in +each direction. It is sufficient for common integer numerators at every +prefix. It is necessary because the reduced coefficient `-2584/9` occurs. +In particular denominator three fails on that literal basis input. This is +a finite statement about this program and these matrices, not a family-wide +bound or an arbitrary representation lower bound. + +For each prefix row with coefficients c_j and initial magnitude bounds B_j, +the triangle inequality gives `|row| <= sum_j |c_j| B_j`. Use B_j=7 for source +and output coordinates and `2^55` for dirty coordinates. Initial rows are also +included. The largest forward bound is +`865889932777058898029788786`; multiplying by nine yields +`7793009394993530082268099074`, which fits 94 signed bits under the conservative +`1+bit_length` rule. The reverse bound also fits 94. Multiplying the same +bounds by `3^65` gives 194 sufficient bits. Neither result is a width minimum. + +These count numerator data only. A numerator implementation additionally pays +for embedding the original data, products, sums, exact divisions, private +work and any precision extensions. Exact division can be performed after a +complete matrix dot product when needed; per-term divisibility is not assumed. +The residue implementation avoids scaling the data by either denominator, +but pays coefficient preparation and the modular kernel's reductions. No +total runtime or total-storage dominance is inferred from the data widths. + +## 4. Literal coefficient preparation and cost + +For the priced preparer, original signed numerator descriptors fit w+2 bits +and reduced positive denominators lie below `2^w`. Descriptors outside this +range are rejected by that implementation. The algebraic statement permits +larger heights, but would require separately paid reading/reduction and +workspace. Input normalization and validation are also separate costs. + +For each distinct denominator q, start u=1. The update +`u <- u(2-qu) mod2^w` squares the error `1-qu`. Hence its correct low-bit count +doubles from one and `ceil(log2 w)` iterations suffice. Each iteration performs +two products, three reductions, a subtraction and a move. Four startup clears, +the denominator read, oddness check, setting one, a final multiply/reduce/check, +the inverse write and four closing clears are explicit. With t iterations, +one denominator costs `15+7t` commands. An independent bit-at-a-time inverse +checks the resulting coefficients. + +For every coefficient a/b, the program reads a and b, reduces a, reads the +prepared inverse, multiplies, reduces, writes the coefficient, and clears all +four work registers. It uses 11 commands per coefficient plus four startup +clears. Thus r distinct denominators and E coefficients cost + +```text +P_setup = r*(15+7 ceil(log2 w)) + 4 + 11E. +``` + +Here r=2, E=208 and w=56, giving 2,406 commands. The private capacities are +`a:w+1 unsigned`, `c:w unsigned`, `v:w+2 signed`, `p:2w unsigned`, as in PR1159. +Products of two residues fit p, reduced accumulators fit a, and `2-p_reduced` +fits v. They are cleared on exit. The inverse and coefficient tables are owned +prepared storage, not promised-restored arbitrary dirty inputs. + +The external layout is: five data arrays, residue coefficients, inverse table, +then fixed-width original numerator/denominator descriptors. Each source read +and table write has an explicit bit position and field width. The head returns +to zero after each inverse and coefficient. Independent itinerary summation +checks all 836 accesses and the bit-action/head-motion bill. Private arithmetic +movement is part of each primitive's cost, not included again in that external +itinerary. Variable-width packed payload bits are reported only diagnostically; +the charged descriptor storage uses fixed three-bit numerator and two-bit +denominator fields for this instance. + +The actual full conditional cost is + +```text +C_admission_and_normalization ++ C_original_input_and_output_conversion ++ sum over every counted setup and kernel primitive of its width-aware cost ++ C_external_source_and_table_routing ++ C_program_and_preparation_control ++ C_physical_adapter. +``` + +None of these terms is set to zero. The emitted kernel has 52,292 primitive +commands; setup plus kernel has 54,698. Their explicit field-access costs are +separate from arithmetic costs and control annotations. If generic product +integrality is checked online, the 416 exact rational products, 416 additions, +height/normalization work, norm checks and temporary product matrices are +additional preprocessing. The four-private-register bound applies to setup +and the kernel, not to arbitrary rational certificate verification. The fixed +scaling family has its own symbolic integrality proof, without claiming free +certification for arbitrary input factors. + +## 5. Rounded interfaces remain different + +PR1135's no-wrap, nearest-rounded map is not phi. A binary echo with ideal +factors `1/3` then `3` has integral ideal product one. Replacing the first leaf +by nearest rounding gives target increment `3*nearest(x/3)`, which is zero +at x=1 rather than one. An integral ideal endpoint therefore does not justify +silently substituting rounded implementations. + +At the actual nested PR1057 boundary `(0,((1,2),3))`, let factor 2 be +`nearest(4z/3)` and all other factors be identity. The pinned PR1135 rounding +and literal word send `[-2,-2,0,-2,-2]` to `[-2,-5,0,-1,-2]`: a dirty helper +changes. This is an exact algebraic boundary witness, not a replay of PR985's +complete physical leaf implementation. It corroborates, rather than repairs, +PR1135's scoped translation obstruction. + +Changed moduli, nonintegral rational reconstruction, restricted source grids, +rounded or irrational leaves, and actual supplier/compiler/hosting admission +remain open interfaces. The comparison does not alter any selected bound or +establish the full multiplication theorem. diff --git a/research/rational-residue-scope/README.md b/research/rational-residue-scope/README.md new file mode 100644 index 0000000000..e01611d5f6 --- /dev/null +++ b/research/rational-residue-scope/README.md @@ -0,0 +1,172 @@ +# Exact rational borrowing: numerator and residue contracts + +**Research consolidation with an exact comparison construction; no new κ.** +This makes the representation boundary between Ali Romman's PR1135 exact-lift +comparison and Gareth Davidson's PR1159 residue backend explicit and executable. +Neither predecessor is contradicted. PR1135 already limits its numerator-width +claim to its representation and excludes denominator-cancelling kernels. + +Exact rational factors with **odd reduced denominators** act on binary residue +registers. When their completed map is integral, an endpoint bound recovers the +integer output. The unchanged PR1057 word and PR1159 backend then restore every +dirty bit pattern. Coefficient inverses, conversions, tables and source routing +are additional paid work. This does not implement rounded rational leaves or +decode arbitrary nonintegral outputs. + +| Source / representation | Required boundary | What its result does not imply | +|---|---|---| +| PR1057 additive borrowing | Exact additive child shears; restored private dirt | Arbitrary deterministic or rounded children need not satisfy it | +| PR1135 rounded restoration | No wrap; same-grid rounded maps; stated translation/summary contract | Its scoped obstructions do not exclude every changed representation | +| PR1135 common numerators | Coarse inputs embedded with denominator `q^D`; sufficient numerator and product headroom | `q^D` is not an unconditional lower bound for cancelled factors or residues | +| PR1159 integer residues | Integer factors; residue boundaries; integral bounded endpoint | Signed decoding alone does not recover a nonintegral rational | +| This comparison | Odd reduced denominators; exact rational factors; integral bounded completed map | Even denominators, rounded substitutions and general supplier admission remain outside scope | + +## Fixed source-bound example + +Take the **52 integer matrices and 1,376-call word of PR1159**. Multiply the +even-indexed factors by `1/3` and the odd-indexed factors by `3`. These central +scales cancel in the ordered product without commuting any matrices. The +complete product is exactly the original integral matrix. Intermediate factors +and data are rational. Input and initial-output bounds remain seven, giving + +```text +R = 7 + 7*2^52 = 31525197391593479 < 2^55. +``` + +Thus the residue data still use **56 bits**, with three dirty length-two arrays, +one source array, one output array and the same four private work registers. +The following comparisons distinguish bounds from minima: + +| Quantity on this fixed word, both directions | Certified value | +|---|---:| +| Formal noncommutative prefix degree D | 65 | +| Generic common denominator `3^D` | 104 bits | +| Least common denominator of all actual rational prefix coefficients | **9** | +| Sufficient common-numerator data width using denominator 9 | **94 bits** | +| Sufficient common-numerator data width using `3^65` | 194 bits | +| Residue data width from the endpoint guard | **56 bits** | + +The numerator bounds cover source/output magnitudes at most seven and dirty +integer entries of magnitude at most `2^55`. They concern data registers; +numerator products, initialization and division need their own workspace and +costs. They are not minimum bit-width claims. The least denominator **is** exact: +all formal prefix coefficients divide nine, and coefficient `-2584/9` at forward +leaf 80, row 8, column 0 forces a multiple of nine. The conservative `3^65` +comparison is not presented as necessary for this instance. + +Four explicit executions use small and arbitrary signed 56-bit dirty values, +in both directions. Every literal leaf agrees with a separate Fraction lift. +The latter reaches 90 signed numerator bits in the dirty stress fixture; all +residue data remain 56-bit patterns. The example is a representation tradeoff, +not a measured runtime improvement. + +## Paid model + +The unchanged kernel executes **52,292 commands**, including 13,760 reductions. +The added bounded-register preparation executes **2,406 commands**: 114 for +the two denominator inverses (including the trivial denominator one) and 2,292 +for 208 coefficient conversions with all private clearing. Together these +parts execute **54,698 commands**. A multiplication command has its actual +width-dependent cost; this is not a machine-time estimate. + +Both phases reuse the original **283-bit** private allocation, including the +112-bit product register. Data occupy 560 bits, residue coefficients 11,648, +the inverse table 112, and fixed-width original rational descriptors 1,040: +**13,360 model bits**, plus private work and the inherited 17,888-bit leaf-word +encoding. Preparation uses 836 explicitly routed accesses, 24,452 bit actions, +and 5,438,192 head-bit moves in the declared field layout. Including the kernel +gives 949,124 bit actions and 81,869,808 head-bit moves. These counts price the +declared external-field scans; private arithmetic and its routing are the +primitive cost terms from PR1159. + +**Additional costs remain explicit:** admission, rational descriptor validation +or normalization, source/input conversion, final signed decoding, program and +preparation-control dispatch, original input storage, and a physical tape +adapter. The verifier's generic integrality admission multiplies the complete +rational product (416 rational multiplies and 416 adds here). If used online, +its coefficient-height cost and product-matrix workspace must be paid separately. +The fixed central-scaling family also has the written integrality proof below; +an offline proof is not a claim of free runtime certification for arbitrary +inputs. [PROOF.md](PROOF.md) gives the conditional full cost expression and +the priced preparation's descriptor-size restriction. + +## Reproduce + +Python 3.10+, standard library only, from the repository root: + +```sh +python3 -I -B research/rational-residue-scope/verify.py +python3 -I -O -B research/rational-residue-scope/test_package.py +``` + +Expected marker: + +```text +PASS_RATIONAL_RESIDUE_SCOPE: 52 rational factors; 1376 calls; 56-bit data; 54698 priced kernel/preparation commands; 144 small cases; no rounded contract or new kappa +``` + +The verifier regenerates [CASE.json.gz](CASE.json.gz) and compares the complete +deterministic [EXPECTED.json](EXPECTED.json). It checks all ten formal columns +at every forward/reverse prefix, 144 smaller dimension/denominator/sign cases, +128 unit inverses, 120 nonunit exclusions and 65,520 quotient-addition cases. +Twelve mathematical/admission/price corruptions reject. Three concrete +counterexamples distinguish nonintegral signed decoding, rounded evaluation +despite an integral ideal product, and actual nested dirty-helper corruption. +Eight package tests include real subprocess mutations and recompression. + +Use `--output /absolute/new/path --receipt /absolute/new/file.json` to retain a +regenerated case and receipt. Outputs must be new; sources are never regenerated. +The complete receipt agrees between CPython 3.14.4 and a read-only relocated +3.12.3 run with `-I -O -B`; see [VALIDATION.md](VALIDATION.md). +The optional [VERIFY.json](VERIFY.json) registers these same two commands for +the repository's bounded Python 3.12 replay hook. It can be run locally with +`python3.12 scripts/research_package.py --package research/rational-residue-scope`. + +## Open next questions + +The structured questions and blockers are in [TASK.json](TASK.json). + +1. Does a useful exact segment of a selected supplier satisfy the odd-denominator + and integral-boundary contract? This determines whether the comparison helps + an actual supplier. First extract the rational coefficients of PR1094's + retained scalar A segment, record their reduced denominator valuations at + two, and check its exact boundary on formal columns. Even denominators, + rounded/irrational leaves and nonintegral boundaries need another interface; + physical admission and complete paid costs would still be required. +2. Can a structured integrality certificate cost less online than forming the + complete rational matrix product? Admission cost and workspace can offset + data-space gains. First emit and price a certificate for the central-scaling + family, including descriptor reads and normalization. No generic cheap + integrality certificate is supplied here. + +## Provenance and remaining work + +Consolidation seed **99**, drawn before detecting the revised task gist; the +already assigned task was retained. Base: +`1b59b624d21924f8e3537cdc1ac52d3be6eda2fe`. Scoped coordination is in +[Discussion 1202](https://github.com/CrocSwap/integer-mult-bounds/discussions/1202). +[CLAIM.json](CLAIM.json) records alternatives and limits; [SOURCE-PINS.json](SOURCE-PINS.json) +pins 20 files from PR1057, PR1135, PR1159 and the selected context. The sources +are preserved byte for byte, including notices and licenses. +Submission is based on `49b3157d1d89adcef16df8be98445451672be5ba`, with the +experimental inputs unchanged. [SOURCES.json](SOURCES.json) preserves the +originating card/context provenance for the optional replay hook. TASK records +the changed scope: the executable comparison is broader than a pure navigation +edit. The final overlap snapshot covered all 836 open PRs (through PR1228), all +six Discussion threads and their comments, and local package notes. No matching +borrowed-word unit-denominator comparison was identified under the declared +search terms; this is not a novelty certificate. PR1199/1203/1205 concern deferred +readers and PR1211 prices a different balanced factor tape. + +This neither replays all of PR1135's rounded-leaf experiment nor changes any +predecessor disposition. The selected PR1094 frontier and PR589 supplier stay +unchanged. PR1164 changes echo arity and remains a separate contribution; +PR1155 changes batch restoration. This uses neither mechanism. Existing +all-size/compiler, common-label, hosting, precision/tape and analytic +obligations remain. No supplier, complete multiplication algorithm, arbitrary +rational reconstruction, or rounded-interface repair is supplied. + +Prepared by **Gareth Davidson (@bitplane)** with substantial **OpenAI Codex +assistance**. Credit **Ali Romman PR1135**, the retained PR1057/1159 lineage and +the classical localization/Newton-inversion principles. No algebraic priority, +subagent review or independent human review is claimed. Apache-2.0. diff --git a/research/rational-residue-scope/SOURCE-PINS.json b/research/rational-residue-scope/SOURCE-PINS.json new file mode 100644 index 0000000000..80587abf8c --- /dev/null +++ b/research/rational-residue-scope/SOURCE-PINS.json @@ -0,0 +1,125 @@ +{ + "base_commit": "1b59b624d21924f8e3537cdc1ac52d3be6eda2fe", + "files": { + "vendor/pr1057/borrow.py": { + "commit": "78a062df1dcab2bffea5ff4d8243f3da6e465414", + "source_path": "research/linear-port-borrowing/borrow.py", + "sha256": "14f267a3a6b85b08f0d23326cdb6de8c27f70ad8d156359c01fdf93bf19682d0", + "git_blob": "b5014c9eb26adad166e4021a430eebfc2ca10d55" + }, + "vendor/pr1057/PROOF.md": { + "commit": "78a062df1dcab2bffea5ff4d8243f3da6e465414", + "source_path": "research/linear-port-borrowing/PROOF.md", + "sha256": "790fb2c67d9e59c7e80e212cb025d643a5315636f977ab9269e96cc7eef5556e", + "git_blob": "96e13812019eaf39a86b265ca96c552300bfbe15" + }, + "vendor/pr1057/README.md": { + "commit": "78a062df1dcab2bffea5ff4d8243f3da6e465414", + "source_path": "research/linear-port-borrowing/README.md", + "sha256": "a1fac70b54269a93b136da727a9db81f15f2fdd5d7ca792b102157ad575d71b7", + "git_blob": "59c4167f89533a588808262af98420e4500f55c9" + }, + "vendor/pr1057/NOTICE.md": { + "commit": "78a062df1dcab2bffea5ff4d8243f3da6e465414", + "source_path": "research/linear-port-borrowing/NOTICE.md", + "sha256": "1f8ce68b254b6c40fe6255bffd2975ef8cf7c0df1de7414cd59353eea80f1e37", + "git_blob": "e718ab189a0eb51cb1bdadf0f898598f72815600" + }, + "vendor/pr1057/LICENSE": { + "commit": "78a062df1dcab2bffea5ff4d8243f3da6e465414", + "source_path": "research/linear-port-borrowing/LICENSE", + "sha256": "c71d239df91726fc519c6eb72d318ec65820627232b2f796219e87dcf35d0ab4", + "git_blob": "261eeb9e9f8b2b4b0d119366dda99c6fd7d35c64" + }, + "vendor/pr1135/contracts.py": { + "commit": "4c35687d7c0da8e6cf33f17e418ecf31c95ff3ad", + "source_path": "research/rounded-borrowing-contract/contracts.py", + "sha256": "bef12e6cd14fdf864f2df07152e1fef619359beca042dbe2fcac2458ef33c142", + "git_blob": "db8e4767ce331a183f00aa38f43ea042b16ddef9" + }, + "vendor/pr1135/PROOF.md": { + "commit": "4c35687d7c0da8e6cf33f17e418ecf31c95ff3ad", + "source_path": "research/rounded-borrowing-contract/PROOF.md", + "sha256": "ec941e11023b79b0e4987869cbea64271f2938c4a686bfb62b65bd3b6c5a710d", + "git_blob": "dd452ddfc64e4eddc9eba5483c989fb66890a01f" + }, + "vendor/pr1135/README.md": { + "commit": "4c35687d7c0da8e6cf33f17e418ecf31c95ff3ad", + "source_path": "research/rounded-borrowing-contract/README.md", + "sha256": "4c2d8e745b9036fc769ae75cbbf7cc1dfaef34e37de39729a147e78219460c67", + "git_blob": "dd5d9a671cca4b768721dba02c674c11e74c1c8b" + }, + "vendor/pr1135/NOTICE.md": { + "commit": "4c35687d7c0da8e6cf33f17e418ecf31c95ff3ad", + "source_path": "research/rounded-borrowing-contract/NOTICE.md", + "sha256": "31963ec6a358c6f883eae97d2fdf3c552254554bddc3042b05b1441414c65c6b", + "git_blob": "f25d5272dddd4d034039b8f1282e72b2c3b68534" + }, + "vendor/pr1135/LICENSE": { + "commit": "4c35687d7c0da8e6cf33f17e418ecf31c95ff3ad", + "source_path": "research/rounded-borrowing-contract/LICENSE", + "sha256": "c71d239df91726fc519c6eb72d318ec65820627232b2f796219e87dcf35d0ab4", + "git_blob": "261eeb9e9f8b2b4b0d119366dda99c6fd7d35c64" + }, + "vendor/pr1159/dense.py": { + "commit": "f38bfe5da0bed21f42ce5251d23491a56519d7c4", + "source_path": "research/modular-port-borrowing/dense.py", + "sha256": "2087206770557d1642002a701f025d9668d44cdea3344d0d67ce3bf89d6f2283", + "git_blob": "47de0632655679f17ffac92b2bc2a64b8a7eba47" + }, + "vendor/pr1159/common.py": { + "commit": "f38bfe5da0bed21f42ce5251d23491a56519d7c4", + "source_path": "research/modular-port-borrowing/common.py", + "sha256": "54c19e208aa894176b5cb59214519b6e9274843dea5d1ae5623fae9f0cc8f950", + "git_blob": "f27258c847ef8df336dc78fd8cd0cd44436d2149" + }, + "vendor/pr1159/CASE.json.gz": { + "commit": "f38bfe5da0bed21f42ce5251d23491a56519d7c4", + "source_path": "research/modular-port-borrowing/CASE.json.gz", + "sha256": "e098deb0309c6f305af566020076a3658e903992371991911646f447ba05b4ab", + "git_blob": "70700a5b018b6698593f42fef0fdc154ac54a0f9" + }, + "vendor/pr1159/PROGRAM.json.gz": { + "commit": "f38bfe5da0bed21f42ce5251d23491a56519d7c4", + "source_path": "research/modular-port-borrowing/PROGRAM.json.gz", + "sha256": "a9ab593ffb7d3961f4e0ed54161a2cffae7a49687af03757e8bf651c96e9d2f3", + "git_blob": "32113e7fdf7cc07f5ace9465c2543e4c54aa3e9d" + }, + "vendor/pr1159/README.md": { + "commit": "f38bfe5da0bed21f42ce5251d23491a56519d7c4", + "source_path": "research/modular-port-borrowing/README.md", + "sha256": "61512ec419a9ae04b1f5321167d14515e4e25db6702704f417cdb32857243fb7", + "git_blob": "c55a507a2e844abcb0d74060cfc42c536aeb70a7" + }, + "vendor/pr1159/PROOF.md": { + "commit": "f38bfe5da0bed21f42ce5251d23491a56519d7c4", + "source_path": "research/modular-port-borrowing/PROOF.md", + "sha256": "5e72268f6652dc242212d20babcc933d211de21daed0c4b76b0304cf341717f1", + "git_blob": "76c923f5bb8b8de003fc0200e5e8a31e6207f99f" + }, + "vendor/pr1159/NOTICE.md": { + "commit": "f38bfe5da0bed21f42ce5251d23491a56519d7c4", + "source_path": "research/modular-port-borrowing/NOTICE.md", + "sha256": "b09d666a26d93a82cd89447357c05f6bb4a77686533b20be33a52f320adbb6ab", + "git_blob": "3beacc2be632a1b7f0df3030dbb3fb17231c383f" + }, + "vendor/pr1159/LICENSE": { + "commit": "f38bfe5da0bed21f42ce5251d23491a56519d7c4", + "source_path": "research/modular-port-borrowing/LICENSE", + "sha256": "c71d239df91726fc519c6eb72d318ec65820627232b2f796219e87dcf35d0ab4", + "git_blob": "261eeb9e9f8b2b4b0d119366dda99c6fd7d35c64" + }, + "context/selected-result.json": { + "commit": "1b59b624d21924f8e3537cdc1ac52d3be6eda2fe", + "source_path": "certificates/selected-result.json", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11" + }, + "context/community-batch1099-review.md": { + "commit": "1b59b624d21924f8e3537cdc1ac52d3be6eda2fe", + "source_path": "docs/research/community-batch1099-review.md", + "sha256": "7e76d2c38e5fce30587835b7251df1430488ae4dd372611ef69a3f03f476b6cb", + "git_blob": "6cb6ec061a071a06a2d18cd4dc3e9a2b05d28099" + } + } +} diff --git a/research/rational-residue-scope/SOURCES.json b/research/rational-residue-scope/SOURCES.json new file mode 100644 index 0000000000..ffef48fe1a --- /dev/null +++ b/research/rational-residue-scope/SOURCES.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "base_commit": "1b59b624d21924f8e3537cdc1ac52d3be6eda2fe", + "files": [ + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "430174a66507b77de88c5ffae2323029f90bdd82", + "sha256": "8c423c0ca0bd33166bcbc58c9b7e60d629fd04f236f11c8f4e1df713fc05028b" + }, + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + } + ] +} diff --git a/research/rational-residue-scope/TASK.json b/research/rational-residue-scope/TASK.json new file mode 100644 index 0000000000..2f2d9bc50c --- /dev/null +++ b/research/rational-residue-scope/TASK.json @@ -0,0 +1,47 @@ +{ + "schema_version": 1, + "task_id": "scope-navigation", + "original_card": { + "id": "scope-navigation", + "question": "Can one misleading historical-current claim or missing research cross-reference be corrected?", + "starting_points": [ + "docs/research/current-status.md", + "docs/research/pr-ledger.md", + "certificates/selected-result.json" + ], + "methods": [ + "Trace one confusing path from onboarding to its authoritative source.", + "Index one tightly related family of obstructions with explicit excluded and open hypotheses." + ], + "acceptance_gate": "Produce evidence-backed navigation, preserve historical records and avoid a duplicate global survey." + }, + "base_commit": "1b59b624d21924f8e3537cdc1ac52d3be6eda2fe", + "assignment_seed": 99, + "priority_revision": 1, + "scope_status": "changed", + "scope_change_reason": "PR1159 already links PR1135, so a navigation-only edit would add little. The claimed task adds an executable applicability comparison and a finite rational construction to reconcile the representation hypotheses. This is explicitly broader than the original pure navigation card.", + "actual_scope": "Consolidate PR1057/1135/1159 exact representation contracts using an odd-denominator, integral-output rational comparison, full source pins, least actual prefix denominator and a paid preparation/kernel invoice.", + "bottleneck_link": "This identifies one possible precision representation for exact additive boundaries. It does not change paid supplier profiles or supply rounded/physical interfaces, so no kappa gain follows.", + "stop_rule": "One frozen 52-factor comparison and declared small cases; no broad rational reconstruction or rounded-supplier search.", + "evidence": "README.md, PROOF.md, CASE.json.gz, EXPECTED.json and the two explicit replay commands.", + "time_budget_minutes": 60, + "outcome": "completed", + "author": "Gareth Davidson (@bitplane)", + "ai_assistance": "Substantial OpenAI Codex assistance; no subagents or independent human review.", + "open_questions": [ + { + "question": "Does a useful exact segment of a named selected supplier satisfy the odd-denominator and integral-boundary contract?", + "why_it_matters": "This decides whether the representation comparison can help an actual supplier, rather than only the dense example.", + "first_step": "Extract the rational coefficients of PR1094's retained scalar A segment, record their reduced denominator valuations at two, and check its exact boundary on formal columns before any optimization.", + "blocked_by": "Even denominators, rounded or irrational leaves, or nonintegral required intermediate boundaries need another interface; physical admission and full paid costs remain required." + }, + { + "question": "Can a structured integrality certificate be checked with less online cost and workspace than forming the complete rational matrix product?", + "why_it_matters": "Generic admission can offset data-space benefits and adds temporary matrix storage.", + "first_step": "Emit and price a certificate for the central-scaling family using integer base matrices and a unit product of scales, including descriptor reads and normalization.", + "blocked_by": "No generic cheap integrality certificate is provided; changing preprocessing assumptions cannot be counted as a free runtime improvement." + } + ], + "discussion": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1202", + "source_pin_inventory": "SOURCE-PINS.json" +} diff --git a/research/rational-residue-scope/VALIDATION.md b/research/rational-residue-scope/VALIDATION.md new file mode 100644 index 0000000000..a44fc24465 --- /dev/null +++ b/research/rational-residue-scope/VALIDATION.md @@ -0,0 +1,59 @@ +# Validation record + +2026-10-13, Linux x86-64. Complete replay passed on CPython 3.14.4 normally and +on CPython 3.12.3 under `-I -O -B` from a relocated read-only package, with +scratch output elsewhere. Standard library only. Canonical receipt: + +```text +2c63ba9c68e4537a49815af076b9097ae49c3f5a7ca66229710455b9d3aed6e2 +``` + +Complete decoded CASE hash: +`043fdf6821548ed74e94b8635cd4ec3f0ae278efd66321bc2ba9c1ff9b46446c`. +All 20 source Git blobs/SHA-256 pins are checked. Exact dependency heads are in +SOURCE-PINS.json. Source pins are checked before importing their executable code. +The two optional replay-metadata provenance pins also match their Git objects. +The final 36-file registered package was copied to a new read-only location and +replayed under Python 3.12 with the identical complete receipt; every input file +remained unchanged. + +- All ten formal input columns at 2,752 forward/reverse leaf prefixes determine + the exact common prefix denominator and rational data bound. +- Four primary executions check 5,504 literal leaf boundaries against separate + Fraction states and the inherited complete kernel/address invoice. +- 144 small parameter cases use 1–8 factors, dimensions 1–3, central denominators + 3/5/7 and both directions: 2,862 leaf prefixes and 120,780 kernel commands. +- 128 independent unit-inverse cases, 120 exhaustive nonunit exclusions and + 65,520 quotient-addition cases pass. +- Twelve semantic/admission/price controls reject, including missing recovery + and source guards, false integrality, nonunit denominators, corrupt coefficient + inverses, omitted inverse moves, unpaid inverse tables/head travel and an + insufficient common denominator. Three exact counterexamples retain the + distinct rounded/nonintegral boundaries; `2/6=1/3` is an accepted positive case. +- Eight package tests pass, including actual optimized subprocess failures for + changed executable sources, changed immutable source containers, forged cases, + understated receipts and occupied outputs. Own-artifact recompression passes; + source-container recompression correctly fails the immutable source pin. + Twenty-five selected-result/inventory/proof-binding repository tests pass. +- Optional package metadata validation and the complete registered Python 3.12 + replay hook pass, including both the verifier and all eight package tests: + `python3.12 scripts/research_package.py --package research/rational-residue-scope`. + +The final overlap helper snapshot at 20:35 UTC covered all 836 open PRs, +ten Discussion/comment records and 324 local README/TASK/ledger records, with +complete remote pagination and no refresh warnings. Its literal terms were +`rational residue`, `odd denominator`, `common denominator`, and `rational-residue`. +The historical common-denominator matches concern other constructions; no +matching borrowed-word unit-denominator comparison was identified. This is +bounded overlap evidence, not a novelty certificate. Relevant PR1057/1135/1159 +heads remain the pinned heads. + +The verifier compares complete regenerated objects, including all source-bound +prices and scopes; JSON duplicate keys and nonfinite constants reject. Normal +and optimized runs use explicit rejections rather than Python assertions for +the new checks. No files in the read-only source closure change during replay. + +The selected hosted cold replay, historical global suite, native supplier +admission, fixed-tape compiler and proof-assistant build were not run. They are +not claimed by this representation comparison. Hosted PR CI is reported +separately; local success is not a claim that those jobs passed. diff --git a/research/rational-residue-scope/VERIFY.json b/research/rational-residue-scope/VERIFY.json new file mode 100644 index 0000000000..4066753057 --- /dev/null +++ b/research/rational-residue-scope/VERIFY.json @@ -0,0 +1,31 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Complete source-bound rational/residue comparison, exact prefix bases, paid preparation and kernel, finite census and twelve failure controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/test_package.py" + ], + "timeout_seconds": 120, + "checks": "Eight package tests including real source/receipt subprocess mutations and decoded-artifact recompression." + } + ] +} diff --git a/research/rational-residue-scope/algebra.py b/research/rational-residue-scope/algebra.py new file mode 100644 index 0000000000..f8fec3af59 --- /dev/null +++ b/research/rational-residue-scope/algebra.py @@ -0,0 +1,276 @@ +"""Exact rational/residue scope comparison; Apache-2.0. + +Gareth Davidson, substantial OpenAI Codex assistance. The borrowed word and +dense residue executor are unchanged PR1057/1159 sources. Localization and +Newton inversion are standard algebra, not claimed new methods. +""" +from collections import Counter +from fractions import Fraction as F +from math import lcm +from pathlib import Path +import runpy + +C = runpy.run_path(str(Path(__file__).with_name("common.py"))) +need = C["need"] + + +def encode(value): + value = F(value) + return [value.numerator, value.denominator] + + +def residue(value, width): + value = F(value) + need(value.denominator % 2 == 1, "nonunit reduced denominator") + modulus = 1 << width + return (value.numerator * pow(value.denominator, -1, modulus)) % modulus + + +def multiply(a, b): + return [[sum((x * y for x, y in zip(row, col)), F(0)) for col in zip(*b)] for row in a] + + +def product(factors): + length = len(factors[0]) + result = [[F(i == j) for j in range(length)] for i in range(length)] + for matrix in factors: + result = multiply(matrix, result) + return result + + +def rational_bound(factors, x, y): + need(type(x) is int and type(y) is int and x >= 0 and y >= 0, "endpoint bound domain") + growth = F(1) + for matrix in factors: + growth *= max(sum(abs(a) for a in row) for row in matrix) + radius = y + x * growth + bound = max(F(x), radius) + width = 1 + while (1 << (width - 1)) <= bound: + width += 1 + return dict(product_norm_bound=encode(growth), endpoint_radius=encode(radius), width=width) + + +def validate(factors, width, x, y): + need(type(width) is int and width >= 1, "positive width") + need(type(factors) is list and len(factors) > 0, "nonempty rational factors") + length = len(factors[0]) + need(length > 0 and all(len(a) == length and all(len(row) == length for row in a) + for a in factors), "square rational matrices") + need(all(F(z).denominator % 2 for a in factors for row in a for z in row), "nonunit reduced denominator") + # This explicit admission route checks the complete rational product. + # Its arbitrary-precision arithmetic/preparation cost is separate and paid. + endpoint = product(factors) + need(all(z.denominator == 1 for row in endpoint for z in row), "completed map not integral") + info = rational_bound(factors, x, y) + need(max(F(x), F(*info["endpoint_radius"])) < 1 << (width - 1), "strict signed recovery guard") + return endpoint, info + + +def scale_fixture(factors, denominator=3): + """Central scales alternate 1/q,q; a last unpaired factor has scale one.""" + n = len(factors) + exponents = [-1 if i % 2 == 0 else 1 for i in range(n)] + if n % 2: + exponents[-1] = 0 + scales = [F(denominator) ** e for e in exponents] + return [[[F(z) * scale for z in row] for row in matrix] + for matrix, scale in zip(factors, scales)], exponents + + +def prefix_basis(word, factors, width, x_bound, y_bound): + """Independent exact rational matrices on all five arrays, no residue code.""" + length = len(factors[0]) + size = 5 * length + state = [[F(i == j) for j in range(size)] for i in range(size)] + denominators = 1 + witness = None + limits = [x_bound] * length + [y_bound] * length + [1 << (width - 1)] * (3 * length) + peak_bound = F(max(limits)) + for at, (source, target, factor, sign) in enumerate(word): + source_rows = state[source * length:(source + 1) * length] + delta = multiply(factors[factor], source_rows) + for i in range(length): + row = [a + sign * b for a, b in zip(state[target * length + i], delta[i])] + state[target * length + i] = row + for j, value in enumerate(row): + before = denominators + denominators = lcm(denominators, value.denominator) + if denominators != before: + witness = dict(leaf=at, row=target * length + i, column=j, value=encode(value)) + peak_bound = max(peak_bound, sum(abs(a) * b for a, b in zip(row, limits))) + expected = [[F(i == j) for j in range(size)] for i in range(size)] + endpoint = product(factors) + # The caller supplies either the positive word or its literal inverse. + positive = all(state[length+i][j] - expected[length+i][j] == endpoint[i][j] + for i in range(length) for j in range(length)) + negative = all(state[length+i][j] - expected[length+i][j] == -endpoint[i][j] + for i in range(length) for j in range(length)) + need(positive or negative, "basis target map") + direction = 1 if positive else -1 + for i in range(length): + for j in range(length): + expected[length+i][j] += direction * endpoint[i][j] + need(state == expected, "arbitrary dirty basis restoration") + scaled = denominators * peak_bound + need(scaled.denominator == 1, "common denominator bound integral") + return dict(columns=size, leaf_prefixes=len(word), endpoint_direction=direction, + least_common_prefix_denominator=denominators, denominator_witness=witness, + rational_absolute_prefix_bound=encode(peak_bound), + common_numerator_bound=str(scaled.numerator), + common_numerator_sufficient_bits=scaled.numerator.bit_length() + 1) + + +def prepare(factors, width): + """Literal bounded-register preparation for this declared descriptor class. + + Original signed numerators must fit w+2 bits and denominators lie in 1..M-1. + Larger descriptors need an additional streamed reduction implementation. + Four work registers have the SAME capacities as PR1159, and are reused. + Every read, inverse check, move, reduction, write and private clear is paid. + """ + modulus, mask = 1 << width, (1 << width) - 1 + flat = [F(z) for a in factors for row in a for z in row] + denominators = sorted({z.denominator for z in flat}) + need(all(q % 2 and 0 < q < modulus for q in denominators), "preparation unit descriptor range") + need(all(-(1 << (width + 1)) <= z.numerator < 1 << (width + 1) for z in flat), + "preparation numerator descriptor range") + counts = Counter() + length = len(factors[0]) + entries = len(flat) + numerator_bits = max(abs(z.numerator).bit_length()+1 for z in flat) + denominator_bits = max(z.denominator.bit_length() for z in flat) + coefficient_start = 5*length*width + inverse_start = coefficient_start + entries*width + descriptor_start = inverse_start + len(denominators)*width + descriptor_stride = numerator_bits + denominator_bits + trace, head, travel, scans = [], 0, 0, 0 + + def visit(position, bits, kind): + nonlocal head, travel, scans + travel += abs(position-head) + scans += 2*(bits-1) + head = position + trace.append([position, bits, kind]) + + def home(): + nonlocal head, travel + travel += head + head = 0 + peaks = {role: 0 for role in "acvp"} + work = {role: 1 for role in "acvp"} + bits = dict(a=width+1, c=width, v=width+2, p=2*width) + + def put(op, role, value): + counts[op] += 1 + need(-(1 << (bits[role]-1)) <= value < 1 << (bits[role]-1) if role == "v" + else 0 <= value < 1 << bits[role], "preparation work overflow") + work[role] = value + peaks[role] = max(peaks[role], abs(value)) + + def clear(): + for role in "acvp": + put("zero", role, 0) + + inverses, iterations = {}, {} + for q in denominators: + clear() + first = next(i for i, z in enumerate(flat) if z.denominator == q) + visit(descriptor_start+first*descriptor_stride+numerator_bits, denominator_bits, "read") + put("read_denominator", "c", q) + counts["check_odd"] += 1 + need(work["c"] % 2 == 1, "unit inverse") + put("set_one", "a", 1) + correct, steps = 1, 0 + while correct < width: + put("mul", "p", work["c"] * work["a"]) + put("low", "p", work["p"] & mask) + put("subtract", "v", 2 - work["p"]) + put("low", "v", work["v"] & mask) + put("mul", "p", work["a"] * work["v"]) + put("low", "p", work["p"] & mask) + put("move", "a", work["p"]) + correct *= 2 + steps += 1 + put("mul", "p", work["c"] * work["a"]) + put("low", "p", work["p"] & mask) + counts["check_one"] += 1 + need(work["p"] == 1, "prepared inverse incorrect") + counts["write_inverse"] += 1 + visit(inverse_start+denominators.index(q)*width, width, "write") + inverses[q], iterations[q] = work["a"], steps + clear() + home() + inverse_counts = dict(counts) + clear() # Explicit coefficient-program startup. + encoded = [] + for index, value in enumerate(flat): + visit(descriptor_start+index*descriptor_stride, numerator_bits, "read") + put("read_numerator", "v", value.numerator) + put("low", "v", work["v"] & mask) + visit(descriptor_start+index*descriptor_stride+numerator_bits, denominator_bits, "read") + put("read_denominator", "c", value.denominator) + visit(inverse_start+denominators.index(value.denominator)*width, width, "read") + put("read_inverse", "c", inverses[work["c"]]) + put("mul", "p", work["c"] * work["v"]) + put("low", "p", work["p"] & mask) + counts["write_coefficient"] += 1 + visit(coefficient_start+index*width, width, "write") + encoded.append(work["p"]) + clear() + home() + need(all(v == 0 for v in work.values()), "preparation private closure") + matrices = [] + at = 0 + for _ in factors: + matrices.append([encoded[at+i*length:at+(i+1)*length] for i in range(length)]) + at += length*length + return matrices, dict(counts=dict(counts), commands=sum(counts.values()), + inverse_counts=inverse_counts, inverse_commands=sum(inverse_counts.values()), + iterations={str(q): n for q, n in iterations.items()}, + inverse_table=[[q, inverses[q]] for q in denominators], + inverse_table_bits=len(denominators)*width, + work_bits=sum(bits.values()), work_peaks=peaks, + original_descriptor_fixed_bits=entries*descriptor_stride, + descriptor_layout=dict(numerator_bits=numerator_bits, denominator_bits=denominator_bits, + coefficient_start=coefficient_start, inverse_start=inverse_start, + descriptor_start=descriptor_start), + external_memory=dict(accesses=len(trace), bit_actions=sum(x[1] for x in trace), + interfield_bit_travel=travel, head_bit_moves=travel+scans, + trace_sha256=C["digest"](trace), + data_coefficient_inverse_descriptor_bits=descriptor_start+entries*descriptor_stride), + original_descriptor_bits=sum(max(1, abs(z.numerator).bit_length()+1) + + z.denominator.bit_length() for z in flat)) + + +def lifted_replay(word, factors, initial, coefficients, width, dense, x_bound, y_bound): + """Every native primitive, paired with separate exact Fraction leaf updates.""" + initial_fraction = [[F(x) for x in row] for row in initial] + need(max(abs(x) for x in initial_fraction[0]) <= x_bound, "actual input exceeds declared bound") + need(max(abs(x) for x in initial_fraction[1]) <= y_bound, "actual output entry exceeds declared bound") + rational = [row[:] for row in initial_fraction] + modulus = 1 << width + start = [[x % modulus for x in row] for row in initial] + peak_numerator, peak_denominator, prefix_count = 1, 1, 0 + + def observe(at, record, data): + nonlocal peak_numerator, peak_denominator, prefix_count + source, target, factor, sign = word[at] + need(tuple(record) == tuple(word[at]), "literal leaf order") + delta = [sum((a*b for a, b in zip(row, rational[source])), F(0)) for row in factors[factor]] + rational[target] = [a+sign*b for a, b in zip(rational[target], delta)] + need(data == [[residue(x, width) for x in row] for row in rational], "rational/residue prefix") + for row in rational: + for x in row: + peak_numerator = max(peak_numerator, abs(x.numerator)) + peak_denominator = max(peak_denominator, x.denominator) + prefix_count += 1 + + final, report = dense.execute(dense.primitive_word(word, len(factors[0])), coefficients, start, width, observe) + for i in (0, 2, 3, 4): + need(rational[i] == initial_fraction[i] and final[i] == start[i], "dirty data restoration") + need(all(x.denominator == 1 for x in rational[1]), "completed output not integral") + need([dense.signed(x, width) for x in final[1]] == rational[1], "signed endpoint recovery") + return dict(target=[int(x) for x in rational[1]], primitive=report, leaf_prefixes=prefix_count, + numerator_peak_signed_bits=peak_numerator.bit_length()+1, + denominator_peak=peak_denominator, final_residues=final) diff --git a/research/rational-residue-scope/common.py b/research/rational-residue-scope/common.py new file mode 100644 index 0000000000..daddbd06d5 --- /dev/null +++ b/research/rational-residue-scope/common.py @@ -0,0 +1,67 @@ +"""Strict source-bound artifact I/O, adapted from PR1159; Apache-2.0.""" +import gzip +import hashlib +import importlib.util +import json +from pathlib import Path + +HERE = Path(__file__).resolve().parent + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def pairs(items): + out = {} + for key, value in items: + need(key not in out, "duplicate JSON key: " + key) + out[key] = value + return out + + +def invalid(value): + raise ValueError("nonfinite JSON: " + value) + + +def canonical(value): + return json.dumps(value, sort_keys=True, separators=(",", ":"), allow_nan=False).encode() + + +def digest(value): + return hashlib.sha256(canonical(value)).hexdigest() + + +def same(a, b, message): + need(canonical(a) == canonical(b), message) + + +def load(path): + path = Path(path) + data = path.read_bytes() + if path.suffix == ".gz": + data = gzip.decompress(data) + return json.loads(data, object_pairs_hook=pairs, parse_constant=invalid) + + +def write(path, value): + path = Path(path) + with path.open("xb") as stream: + stream.write(gzip.compress(canonical(value), mtime=0) if path.suffix == ".gz" else + (json.dumps(value, indent=2, sort_keys=True, allow_nan=False) + "\n").encode()) + + +def module(name, path): + spec = importlib.util.spec_from_file_location(name, path) + result = importlib.util.module_from_spec(spec) + spec.loader.exec_module(result) + return result + + +def pins(): + manifest = load(HERE / "SOURCE-PINS.json") + for name, pin in manifest["files"].items(): + need(hashlib.sha256((HERE / name).read_bytes()).hexdigest() == pin["sha256"], + "source hash mismatch: " + name) + return manifest diff --git a/research/rational-residue-scope/context/community-batch1099-review.md b/research/rational-residue-scope/context/community-batch1099-review.md new file mode 100644 index 0000000000..6cb6ec061a --- /dev/null +++ b/research/rational-residue-scope/context/community-batch1099-review.md @@ -0,0 +1,86 @@ +# Forty-PR review: packing refinements, independent audits and finite circuits + +This round freezes forty PR heads at the main checkpoint recorded in [PLAN.json](../../research/community-batch1099-audit/PLAN.json). Review completion, publication, unresolved questions and GitHub merge states are tracked separately in the [integration receipt](community-batch1099-integration.json) and [PR ledger](pr-ledger.md). A submitted receipt or a successful arithmetic check alone is not full construction acceptance. + +The leading conditional witness is Rohan Arun's #1094, **κ = 0.001672660197076918**. It improves the selected #1042 saving by about **0.02823%**, through owner packing on the same seven-slot k8 word. Jeremy Kothe's #1050/#1053/#1055/#1061/#1065/#1068/#1074/#1087 and Rohan's #1056/#1063/#1082 are individually replayed and retained. This is cumulative packing work on Jeremy's mutable-leaver construction, Rohan's #987 slot discovery and Hao Yan's #858 controller, with the full prior geometry, ownership, native compiler and PR589/PR555 bit lineage retained. It is not a measured runtime improvement. + +## Individual contributions and boundaries + +| PR | Contributor | Accepted scope or outstanding finding | +|---|---|---| +| [#987](https://github.com/CrocSwap/integer-mult-bounds/pull/987) | rohanarun (`rohanarun`) | Rohan Arun's U10 word: two additional triangle-hybrid slots on unchanged T37 owners; full dirty-state, native, controller and conditional assembly replay. Superseded numerically, with independent mechanism credit. | +| [#1050](https://github.com/CrocSwap/integer-mult-bounds/pull/1050) | jeremykothe2 (`jeremykothe2`) | Jeremy Kothe's exact T16 owner-map refinement on the unchanged seven-slot k8 word; complete hosting, controller, invoice, moment and assembly replay. | +| [#1053](https://github.com/CrocSwap/integer-mult-bounds/pull/1053) | jeremykothe2 (`jeremykothe2`) | Jeremy Kothe's next exact T16 owner-map refinement; same word and compiler, independently replayed frozen placement. | +| [#1055](https://github.com/CrocSwap/integer-mult-bounds/pull/1055) | jeremykothe2 (`jeremykothe2`) | Jeremy Kothe's next exact T16 owner-map refinement; same word and compiler, independently replayed frozen placement. | +| [#1056](https://github.com/CrocSwap/integer-mult-bounds/pull/1056) | rohanarun (`rohanarun`) | Rohan Arun's whole-helper exchanges from PR1050: 24 changed placements, unchanged local supplier; full unchanged strict verifier. | +| [#1061](https://github.com/CrocSwap/integer-mult-bounds/pull/1061) | jeremykothe2 (`jeremykothe2`) | Jeremy Kothe's exact LNS T16 owner-map refinement; full strict replay, no global-optimality claim. | +| [#1063](https://github.com/CrocSwap/integer-mult-bounds/pull/1063) | rohanarun (`rohanarun`) | Rohan Arun's neutral reshuffles unlock whole-helper exchanges; separately retained below later frontier, full strict replay. | +| [#1065](https://github.com/CrocSwap/integer-mult-bounds/pull/1065) | jeremykothe2 (`jeremykothe2`) | Jeremy Kothe's next exact T16 packing; full strict replay with unchanged compiler and local word. | +| [#1068](https://github.com/CrocSwap/integer-mult-bounds/pull/1068) | jeremykothe2 (`jeremykothe2`) | Jeremy Kothe's next exact T16 packing; full strict replay with unchanged compiler and local word. | +| [#1074](https://github.com/CrocSwap/integer-mult-bounds/pull/1074) | jeremykothe2 (`jeremykothe2`) | Jeremy Kothe's next exact T16 packing; full strict replay with unchanged compiler and local word. | +| [#1082](https://github.com/CrocSwap/integer-mult-bounds/pull/1082) | rohanarun (`rohanarun`) | Rohan Arun's twelve-bin targeted repacking changes 30 placements; unchanged word and strict admission. | +| [#1087](https://github.com/CrocSwap/integer-mult-bounds/pull/1087) | jeremykothe2 (`jeremykothe2`) | Jeremy Kothe's next exact T16 packing; full strict replay, direct parent of PR1094. | +| [#1094](https://github.com/CrocSwap/integer-mult-bounds/pull/1094) | rohanarun (`rohanarun`) | Rohan Arun's rare-pattern sixteen-bin exchanges change 193 placements from PR1087; candidate conditional kappa 0.001672660197076918 with inherited full finite admission. | +| [#1090](https://github.com/CrocSwap/integer-mult-bounds/pull/1090) | Cinna Davis (`1337isnot1337`) | Transfer of Alexander Schwartzman's rank-seven helper ends to k8 helpers 574/575; eight B frames and two tails change, width 3730 to 3728, fresh native and complete owner admission. Distinct construction, below selected packing candidate. | +| [#1072](https://github.com/CrocSwap/integer-mult-bounds/pull/1072) | David Breslauer (`davidNbreslauer`) | David Breslauer's one-call E4 entrance-frame modification consumes four T37 gaps; four width increases and owner exchanges, full mixed-provider construction/admission. Historical parallel contribution, no automatic composition with k8. | +| [#1049](https://github.com/CrocSwap/integer-mult-bounds/pull/1049) | thakrarsagar (`thakrarsagar`) | Code-disjoint exact scalar/frame audit of eight mutable-leaver cells, 24 leavers and seven slots, 704 columns and 14 controls. Corrects the raw per-cell profile description to +6H1-12H2+3H3-3H6; final priced word is unchanged. | +| [#1051](https://github.com/CrocSwap/integer-mult-bounds/pull/1051) | thakrarsagar (`thakrarsagar`) | Independent prime-chain logarithm/Taylor interval audit of T37 and bit endpoints plus binding kappa; seven controls. Historical selection pin redirected to identical checkpoint bytes. | +| [#1052](https://github.com/CrocSwap/integer-mult-bounds/pull/1052) | steph4n (`steph4n-gh`) | Independent positive-binomial certification of six moment decisions, 42 all-T inequalities, 14 bootstrap steps and 94 outer slacks, plus exact remainder-trade identities. Historical checkpoint retained byte-identically. | +| [#1069](https://github.com/CrocSwap/integer-mult-bounds/pull/1069) | thakrarsagar (`thakrarsagar`) | Code-disjoint arithmetic repricing of sixteen pinned historical claims, including deficit identity W-64N; source blobs rebound. Does not itself verify realized words or owners. | +| [#1091](https://github.com/CrocSwap/integer-mult-bounds/pull/1091) | Josie Elliston (`JosieElliston`) | Independent event/window/owner recount of fifteen historical T16 maps and T8, including disjoint pending axes across children; eleven controls. No emitted controller, invoice or outer theorem claim. | +| [#1048](https://github.com/CrocSwap/integer-mult-bounds/pull/1048) | flemhhh (`flemhhh`) | Deferred: false general fixed-exponent root-ordering claim, floating-point search decisions presented as exact exclusions, and insufficient fail-closed endpoint bracketing. Exact counterexample and correction requirements retained; no optimality endorsement. | +| [#1096](https://github.com/CrocSwap/integer-mult-bounds/pull/1096) | woklerx (`woklerx`) | Complete PR589 nine-stage positive-majorant audit: 220905 events, 4839 columns; exact positive peak 127 bits, bank envelope 132, coarse bound 177. Production 192-bit charge unchanged; no physical 128-bit admission. | +| [#1059](https://github.com/CrocSwap/integer-mult-bounds/pull/1059) | thakrarsagar (`thakrarsagar`) | Opt-in record/evaluate/replay parallelization of unchanged layer-end controls, byte-identical receipt and failure controls. Verification acceleration only. | +| [#1092](https://github.com/CrocSwap/integer-mult-bounds/pull/1092) | ToikY (`ToikY`) | Opt-in exact Clifford input-state reuse: pinned compiler edit, independent Gaussian-rational oracle, paired phase replays and driver fault controls. No selected compiler replacement or combined speedup claim. | +| [#1099](https://github.com/CrocSwap/integer-mult-bounds/pull/1099) | woklerx (`woklerx`) | Exact mask enumeration preserves ordered PR968 D/E/H streams: 1260 frames, 7168 decoders, 57344 term ranks and controls. Local benchmark separated from mathematical receipt. | +| [#1046](https://github.com/CrocSwap/integer-mult-bounds/pull/1046) | martinxxx9 (`martinxxx9`) | Smallest five-cube affine-code factorization: exact total pairing-rank floor 32 and peak floor eight, attained by four totals. Overcomplete factors included; only the stated additive stage ledger is excluded. | +| [#1088](https://github.com/CrocSwap/integer-mult-bounds/pull/1088) | martinxxx9 (`martinxxx9`) | Signed three-by-three connector query optimum 2 sum(cF)+2 min(cF), six repairs across 288 orientations; full dirty restoration and 308-vs-332 priced fixture. Sign-symmetric fixed query prices only. | +| [#1077](https://github.com/CrocSwap/integer-mult-bounds/pull/1077) | woklerx (`woklerx`) | Complex-coefficient extension of the exact eight-term E8 all-pairs decoder floor max(72-p,56), p<=24. Handles isotropic cross-term coincidences; inherits real root-hyperplane classification and excludes masked or overcomplete decoders. | +| [#1098](https://github.com/CrocSwap/integer-mult-bounds/pull/1098) | Adam Gall (`adamgall`) | Label-free P112 Gram support spectrum certificate: 511 characters, 503 full rank, eight coordinate kernels, ten spectra and sharp restricted energy four. Corroborates PR845's finite premise only. | +| [#1097](https://github.com/CrocSwap/integer-mult-bounds/pull/1097) | Gareth Davidson (`bitplane`) | Proof-carrying reconciliation of PR620 archived P111 minimum rank nine and unique rank-nine fitting matrix: 37044 RUP additions, 1409475 hints. Exact archival root order; does not transfer to different supplier punctures or close wider PR620. | +| [#1008](https://github.com/CrocSwap/integer-mult-bounds/pull/1008) | woklerx (`woklerx`) | Exact census of 6480 elementary shears of the fixed punctured P111 two-factor product basis, unchanged pairing-cost floor 3969. No arbitrary-GL or multi-shear barrier. | +| [#1023](https://github.com/CrocSwap/integer-mult-bounds/pull/1023) | thakrarsagar (`thakrarsagar`) | No-bank width-eight slot-packing optimum for PR589, with hypothetical width-seven headroom prices. Does not construct narrower bit helpers or discharge window timing/hosting. | +| [#1016](https://github.com/CrocSwap/integer-mult-bounds/pull/1016) | ToikY (`ToikY`) | PR952 fixed-word frame reassignment exclusion: 137 components, 13730 assignments, 933 concavity certificates plus one explicitly proved exceptional profile. Fixed order, operands, COPY frames and live-line spans only. | +| [#1017](https://github.com/CrocSwap/integer-mult-bounds/pull/1017) | woklerx (`woklerx`) | Complete 5563 single-ADD omission atlas on frozen PR967 D, all 661 symbolic columns; distinct nonzero full syndromes, 221 target-invisible helper restorations. No multi-fault or full-native guarantee. | +| [#1034](https://github.com/CrocSwap/integer-mult-bounds/pull/1034) | Ali Romman (`aliromman`) | Common dual for 71 pinned provider records/25 interfaces with mixed helper inventories, whole helpers and fixed capacities; arbitrary real call counts allowed. Explicitly excludes later U10/leaver providers. | +| [#1003](https://github.com/CrocSwap/integer-mult-bounds/pull/1003) | ToikY (`ToikY`) | Historical R480 Q-node2 shortened 52 to 43 XORs, complete word 33958 to 33940; full positive envelope and native 5/9/11-stage checks. Paid profile unchanged, no kappa gain. | +| [#1027](https://github.com/CrocSwap/integer-mult-bounds/pull/1027) | bbMisk (`bbMisk`) | R480 quad12 admission of the known eleven-ADD minimum: complete 252 shortest-program census/four reverse classes, whole word 33934 and native checks. Credits PR1002's prior minimum; fixed positive transfer only. | +| [#1089](https://github.com/CrocSwap/integer-mult-bounds/pull/1089) | martinxxx9 (`martinxxx9`) | Historical R480 Q-node5 shortened 51 to 41 XORs, complete word 33938; all dirty columns and independent Python 5/9/11-stage evidence. Historical selected context redirected without changing hash; no native C++ claim. | +| [#1045](https://github.com/CrocSwap/integer-mult-bounds/pull/1045) | thakrarsagar (`thakrarsagar`) | Connected four-helper fusion crosses PR941 disjoint-pair floor: 1290240 fully priced GL(4,2) cases, word 11946, native checks. Semantic D candidate retains known syntactic H2/K mismatch; not a selected supplier. | +| [#1062](https://github.com/CrocSwap/integer-mult-bounds/pull/1062) | thakrarsagar (`thakrarsagar`) | Compose nine PR1015 blocks and PR923 frame520 with helper-star D; 11783 to 11515 then 11500 ADDs as freed precision admits extra stars. All 661 columns and full local/nine-stage envelopes; known H2/K mismatch retained, no hosted supplier admission. | + +## Construction and verification review + +Every one of the twelve same-word packing proposals passes the unchanged strict T16 admission on the freshly reconstructed seven-slot local word retained from batch1047. The eight Jeremy packages differ from the retained shared package only in six manifest/data/documentation files; these variants are stored byte-for-byte rather than overwriting selected or historical source inventories. The four Rohan packages preserve and authenticate their original compiler archive before overlaying three candidate data files. Each replay covers 69 admission controls, twelve bit controls, fifteen controller mutations, six independent owner controls, both exact moment engines and 47 strict outer inequalities. The final inventory remains 69,120 roles, 144 complete calls, prefix 397 charged at 512, and row coefficient 16,469 below 20,161. + +The new `verify_frontier1094.py` cold command rebuilds #1042 and then #1094. Its explicit reuse mode accepts only the published #1042 review receipt, checks its sources, stage logs and every artifact, and rechecks the complete retained bit/PR741/PR799 ancestry. Local execution in this review uses that recorded reuse. The previous selected package is unchanged and the old selected record is preserved as `certificates/checkpoints/frontier1042.json`. + +Josie Elliston's #1091 supplies a separately written owner/event-window checker, including disjoint pending axes on distinct idle children of a physical family. Sagar Thakrar's #1069 supplies separately written endpoint arithmetic. The maintainer composition [check_frontier1094.py](../../research/community-batch1099-audit/check_frontier1094.py) applies both unchanged auditors to #1094 as well, requiring all eleven owner mutation controls and the exact endpoint/grid decisions. This extends the tested input, not the auditors' inherited-interface scope. + +Rohan's #987 supplies a distinct two-slot U10 word on T37 owners and receives construction credit despite its lower historical number. #1090 ports Alexander Schwartzman's #1030 rank-seven-end mechanism to the k8 word, changing eight B frames and two early tails. David Breslauer's #1072 changes one T37 call's entrance frames and uses four idle gaps. These are independent finite constructions and are not added numerically to #1094. + +## Audit findings and historical context + +Sagar's #1049 independently finds the raw per-cell profile change **+6H1 −12H2 +3H3 −3H6**, rather than the unqualified **−30H1 +6H2 +6H3** sentence in the construction descriptions. The eight-cell and k5/k8 differences are additive under the recounted convention. The final κ uses the complete final word profile, which is independently reproduced; this documentation issue does not change it. Frozen source descriptions remain preserved, with this correction made explicit. + +#1091 also clarifies that the copied `evidence/local`, `evidence/global` and `evidence/audit` directories in the T16 source package are historical #645 evidence. The current T16 admission is established by fresh replay receipts archived with the reviews, not by treating those old directories as a T16 run. + +Five historical packages (#1051, #1052, #1089, #1090 and #1072) pinned the moving `certificates/selected-result.json`. The lookup path was redirected to the byte-identical #942 checkpoint; #1090’s package manifest was rehashed solely to bind that path adaptation. Expected digests, mathematical inputs and verifier predicates were retained. Original manifests, initial rejected runs and passing corrected checks are archived. Historical source Git-blob maps continue to describe the original paths at their stated base. + +The independent T37 audits use different arithmetic: prime-chain atanh/Taylor enclosures in #1051, positive generalized-binomial enclosures with exact integer calibration in #1052. They check historical arithmetic, bootstrap and stated assembly inequalities; they do not prove the physical interfaces. #1096 proves a 132-bit bank-wise positive envelope for PR589's full finite schedule and observes a 127-bit exact positive-program maximum. Neither changes the production 192-bit charge or supplies 128-bit physical admission. + +## Deferred #1048: pricing and exactness need correction + +The PR claims that, for any fixed exponent a0, the weighted count G(a0)=sum n_r r^(1-a0) orders the certified roots. This is false even for equal rank mass and equal m,W. Take m=8, W=4, A={2:15}, B={1:14,4:4}; both have mass 30 and deficit 2. At a0=1/2, G_A=15 sqrt(2)<22=G_B, but root_A<47/1000