diff --git a/research/lean-nonlinear-commutator/CLAIM.json b/research/lean-nonlinear-commutator/CLAIM.json new file mode 100644 index 0000000000..e0563551aa --- /dev/null +++ b/research/lean-nonlinear-commutator/CLAIM.json @@ -0,0 +1,178 @@ +{ + "pass": 8, + "assignment_seed": 83, + "drawn_at_utc": "2026-10-13T10:18:13.485465+00:00", + "track": "independent verification or formalization", + "base": "f567884aeb8851b6e794af1184119a3bfbe1e631", + "status": "submitted", + "branch": "research/pass08-verification-seed83", + "claimed_at_utc": "2026-10-13T10:26:20.672476+00:00", + "candidate_selection": "83 modulo 3 = 2; fresh draw coincidentally equals the preceding seed, but the proof obligation is different", + "candidates": [ + { + "object": "Formal fractional-grid admission criterion for dyadic scalar prefixes", + "chosen": false, + "reason": "A complete rational/program bridge would require a larger arithmetic-library setup; the existing exact finite audit already isolates the immediate guard change" + }, + { + "object": "Formal exact balanced-tree leaf-count formula from PR663", + "chosen": false, + "reason": "Useful arithmetic, but it leaves the more consequential nonlinear restoration interface untouched" + }, + { + "object": "All-tree nonlinear dirty commutator semantics and ordered additive-map product", + "chosen": true, + "method": "Lean 4 core/Std, finite integer-array values of arbitrary width, indexed disjoint scratch pools; pin the original dispatcher and PR663 argument" + } + ], + "statement": "Prove by structural induction that every binary dirty commutator restores arbitrary borrowed arrays, has a target-independent increment and an exact reverse-word inverse for arbitrary fixed deterministic nonlinear leaves. Under leaf additivity, prove the ordered composite independent of initial dirt. Bind the abstract semantics to the pinned PR628 dispatcher by bounded trace and execution checks.", + "domain": "Binary reserved-scratch trees; fixed-point arrays represented as integer vectors of arbitrary finite width; leaves assumed to restore their source and add a fixed function of that source to a distinct target. Fixed, nonaliased external data.", + "stopping_rule": "One scoped semantics formalization plus explicit bounded source correspondence; no rounded leaf accuracy proof, alias-guard repair, multiway/connector reuse, resource optimum, physical supplier or new kappa.", + "expected_finish": "Approximately 120 minutes from claim; reserve final quarter for validation and handoff", + "coordination": "Only open issue #650 asks for Discussions; no coordination claim channel exists. Claim recorded locally.", + "initial_open_pr_count": 679, + "latest_pr_at_claim": 887, + "related_prs": { + "628": "Subject binary dispatcher and inherited leaf contract", + "663": "Written all-n nonlinear induction and free-term finite audit; this adds a kernel proof", + "673": "Multiway extension and phase-alias repair, outside scope", + "784": "Reserved-scratch resource theorem", + "887": "Previous pass formalizes resource counts, not execution semantics", + "878": "Selected XOR boundary semantics, different circuit and model", + "877": "Precision bound retaining the nonlinear restoration hypothesis", + "889": "Concurrent common-factor multi-output batch; different recursive interface, no imported dependency" + }, + "bounded_correspondence": { + "all_binary_trees_by_leaves_1_to_7": [ + 1, + 1, + 2, + 5, + 14, + 42, + 132 + ], + "all_binary_trees_total": 197, + "generated_lean_sha256": "35d6a7bed4b0b0350e539c71a5f58a5a9f54ad4abc02bd436c7c0985b34455bc", + "lean_trace_equalities": 34, + "source_execution_cases": 1170, + "source_execution_leaf_calls_including_inverse": 3722940, + "source_factor_counts": [ + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 8, + 9, + 10, + 11, + 12, + 13, + 14, + 15, + 16, + 17, + 18, + 19, + 20, + 21, + 22, + 23, + 24, + 25, + 26, + 27, + 28, + 29, + 30, + 31, + 32, + 33, + 34, + 35, + 36, + 37, + 38, + 39, + 40, + 41, + 42, + 43, + 44, + 45, + 46, + 47, + 48, + 49, + 50, + 51, + 52, + 53, + 54, + 55, + 56, + 57, + 58, + 59, + 60, + 61, + 62, + 63, + 64, + 83 + ], + "source_trace_instructions": 206830, + "source_words": 130, + "tree_execution_cases": 2364, + "array_widths": [ + 1, + 2, + 3 + ], + "leaf_families": [ + "integer floor with nonzero offset", + "bounded square modulo 97", + "noncommuting integer shears" + ], + "formal_trace_factor_counts": [ + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 8, + 9, + 10, + 11, + 12, + 13, + 14, + 15, + 16, + 83 + ], + "controls": 13 + }, + "overlap_refresh": { + "open_prs": 686, + "through_pr": 894, + "upstream_head": "f567884aeb8851b6e794af1184119a3bfbe1e631", + "subject_and_audit_heads_unchanged": true, + "related_new_work": "PR889 batches multiple outputs sharing a common factor and gives different query-count evidence. It does not formalize this binary-tree nonlinear contract. PR893 audits historical Lean evidence rather than this mathematical obligation." + }, + "completed_at_utc": "2026-10-13T10:57:03.649998+00:00", + "pr": 896, + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/896", + "mathematical_commit": "238f0bbca6271441e365d3dca4af00a39382dfd4", + "result": "Lean 4.21.0 proves the typed binary evaluator restores arbitrary dirt, has target-independent nonlinear increments and exact inverses; additive leaves give the ordered product. Twelve formal statements, 34 source trace equalities, 1170 source and 2364 tree executions, and 13 controls pass. Leaf correctness and all-size address/Python correspondence remain separate. No new kappa.", + "validation": "Complete ordinary Python 3.14.4 and isolated optimized read-only Python 3.12.3 replays agree. Source/receipt/overwrite controls, selected-record integrity and staged scope/whitespace pass; hosted CI tracked separately.", + "immediate_pre_submission_check": { + "through_pr": 895, + "new_arrival": "PR895 screens BW16 as a decoder unit; no overlap with nonlinear restoration semantics" + } +} diff --git a/research/lean-nonlinear-commutator/EXPECTED.json b/research/lean-nonlinear-commutator/EXPECTED.json new file mode 100644 index 0000000000..562b9da03f --- /dev/null +++ b/research/lean-nonlinear-commutator/EXPECTED.json @@ -0,0 +1,264 @@ +{ + "audit_head": "e0e546fd01b396478c68b6b6c5a16d87515983ba", + "base_commit": "f567884aeb8851b6e794af1184119a3bfbe1e631", + "finite": { + "all_binary_trees_by_leaves_1_to_7": [ + 1, + 1, + 2, + 5, + 14, + 42, + 132 + ], + "all_binary_trees_total": 197, + "generated_lean_sha256": "35d6a7bed4b0b0350e539c71a5f58a5a9f54ad4abc02bd436c7c0985b34455bc", + "inverse_order_witness": { + "correct": [ + [ + 1 + ], + [ + 6 + ], + [ + 1 + ] + ], + "wrong": [ + [ + 1 + ], + [ + 10 + ], + [ + 1 + ] + ] + }, + "lean_trace_equalities": 34, + "noncommuting_product": [ + [ + 2, + -1 + ], + [ + 1, + 0 + ] + ], + "nonlinear_dirt_witness": [ + [ + [ + 1 + ], + [ + 10 + ], + [ + 0 + ] + ], + [ + [ + 1 + ], + [ + 12 + ], + [ + 1 + ] + ] + ], + "source_compose_sha256": "7b9651bbed8bc2faa0cbdbfa896d75175564b01bca612dc8971c51e8ca9a5361", + "source_execution_cases": 1170, + "source_execution_leaf_calls_including_inverse": 3722940, + "source_factor_counts": [ + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 8, + 9, + 10, + 11, + 12, + 13, + 14, + 15, + 16, + 17, + 18, + 19, + 20, + 21, + 22, + 23, + 24, + 25, + 26, + 27, + 28, + 29, + 30, + 31, + 32, + 33, + 34, + 35, + 36, + 37, + 38, + 39, + 40, + 41, + 42, + 43, + 44, + 45, + 46, + 47, + 48, + 49, + 50, + 51, + 52, + 53, + 54, + 55, + 56, + 57, + 58, + 59, + 60, + 61, + 62, + 63, + 64, + 83 + ], + "source_trace_instructions": 206830, + "source_words": 130, + "source_words_sha256": "6ce40e47309ec96a621e694e893b2636a8fa1d1e9782a2bc3653efdf118d0125", + "state_cases_sha256": "7f53d9ea44f25b43e3d5ef918e10afe65cce79d05a474c65b8fe80ddfa58f337", + "tree_execution_cases": 2364 + }, + "formal_axioms": { + "NonlinearEcho.delta_eq_product": [ + "Quot.sound", + "propext" + ], + "NonlinearEcho.exact_inverse": [ + "Quot.sound", + "propext" + ], + "NonlinearEcho.full_execution": [ + "Quot.sound", + "propext" + ], + "NonlinearEcho.ideal_execution": [ + "Quot.sound", + "propext" + ], + "NonlinearEcho.inverse_involutive": [ + "Quot.sound", + "propext" + ], + "NonlinearEcho.inverse_then_forward": [ + "Quot.sound", + "propext" + ], + "NonlinearEcho.negative_node_order": [ + "Quot.sound", + "propext" + ], + "NonlinearEcho.nonlinear_dirt_counterexample": [ + "Quot.sound", + "propext" + ], + "NonlinearEcho.positive_increment": [ + "Quot.sound", + "propext" + ], + "NonlinearEcho.product_additive": [ + "propext" + ], + "NonlinearEcho.run_eq": [ + "Quot.sound", + "propext" + ], + "NonlinearEcho.scratch_restored": [ + "Quot.sound", + "propext" + ] + }, + "formal_source_sha256": "c08de49fe02781d69eddc7bb9b4f3c8d311cc1bbe21e6ccb1db86eeafb97dceb", + "lean_commit": "6741444a63ee", + "lean_version": "4.21.0", + "negative_controls": [ + "omit_scratch_restore", + "wrong_final_target_sign", + "target_dependent_leaf", + "reverse_factor_order", + "omit_inverse_reversal", + "wrong_source_trace_literal", + "reject_axiom_sorryAx", + "reject_axiom_Lean.ofReduceBool", + "reject_axiom_user_assumption", + "source_target_alias", + "scratch_source_alias", + "scratch_target_alias", + "insufficient_depth" + ], + "schema": "lean-nonlinear-commutator-v1", + "source_sha256": { + "vendor/pr628/DIRTY-PROOF.md": "bb7c2fdc1c4673d56531fd56fb8790c81a16813ac152c10f1afabc9efdd70d61", + "vendor/pr628/NOTICE.md": "abeacf1ad1491d5797cfcf1f3832799bbf3b24b99597229d7bc884059a51ec68", + "vendor/pr628/dirty.py": "09e7f41141594e6540828330d27be27c083ee6569660ae42c0cd519b09fc8d21", + "vendor/pr663/NOTICE.md": "39c6f175693297f1e0b24264747aec8dbee09833cb52c585142a7920d80e9d52", + "vendor/pr663/README.md": "0fed6e3a82c7c158614c696504d25b5693a0e8b6fe24a2140ced4e8cae2f7582", + "vendor/pr663/SOURCE.json": "723b1412d7bef4b13dcd9be35bc5983c876215c2998ed3897ee54291f8982654" + }, + "subject_head": "0768f97d06c623b8211e651543c66135796b62bf", + "trace_axioms": { + "trace_10_false": [], + "trace_10_true": [], + "trace_11_false": [], + "trace_11_true": [], + "trace_12_false": [], + "trace_12_true": [], + "trace_13_false": [], + "trace_13_true": [], + "trace_14_false": [], + "trace_14_true": [], + "trace_15_false": [], + "trace_15_true": [], + "trace_16_false": [], + "trace_16_true": [], + "trace_1_false": [], + "trace_1_true": [], + "trace_2_false": [], + "trace_2_true": [], + "trace_3_false": [], + "trace_3_true": [], + "trace_4_false": [], + "trace_4_true": [], + "trace_5_false": [], + "trace_5_true": [], + "trace_6_false": [], + "trace_6_true": [], + "trace_7_false": [], + "trace_7_true": [], + "trace_83_false": [], + "trace_83_true": [], + "trace_8_false": [], + "trace_8_true": [], + "trace_9_false": [], + "trace_9_true": [] + } +} diff --git a/research/lean-nonlinear-commutator/LICENSE b/research/lean-nonlinear-commutator/LICENSE new file mode 100644 index 0000000000..261eeb9e9f --- /dev/null +++ b/research/lean-nonlinear-commutator/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/lean-nonlinear-commutator/MODEL.md b/research/lean-nonlinear-commutator/MODEL.md new file mode 100644 index 0000000000..bffbebde14 --- /dev/null +++ b/research/lean-nonlinear-commutator/MODEL.md @@ -0,0 +1,117 @@ +# Formal semantics and source boundary + +This package formalizes the nonlinear binary-commutator induction written in +PR628 and independently audited in PR663. The resource optimum from PR784/887 +is a different statement. Here the question is what a completed recursive +call does to arbitrary initial source, target, and borrowed data. + +## Values, leaves, and disjoint storage + +`Value width` is `Fin width → Int`: an integer array of arbitrary finite width. +A common fixed-point grid is represented by an external common scale; complex +arrays can be represented by their integer real and imaginary coordinates. +Addition and subtraction are componentwise. The proof uses their exact group +identities, not any analytic estimate or floating-point arithmetic. + +`f : Nat → Value width → Value width` assigns an arbitrary deterministic map +to each leaf label. It can be nonlinear, non-zero-preserving, discontinuous, +and can mix coordinates. Fixed coefficient, phase, orientation, and precision +parameters may be captured in this function. They must remain fixed across +paired calls. A positive completed leaf adds `f label source` to its target; +a negative leaf subtracts the same value. + +The completed-leaf interface assumes that each leaf restores its source and +does not consult its target while computing the increment. This proof does +not establish that property for PR628's numerical `lift` implementation. +The source is accordingly an immutable argument of the formal evaluator. +`full_execution` includes that source in the returned state, but its source +part is an interface assumption encoded by the model, not a new proof about +the leaf's temporary source writes. + +`Tree depth` contains a leaf label or two children at the next smaller depth. +Leaves may leave capacity unused. `Dirt width depth` contains a separate array +at each reserved level. The parent connector is the head, and both children +reuse the disjoint tail. Source, target, and scratch are distinct typed +components; equal *contents* are allowed. Aliased mutable locations and +stateful callbacks are outside this model. + +## Literal recursive execution + +The positive `run` evaluator performs four completed child calls: + +```text +(z1, t1) = left +(x, z0, t0) +(y1, t2) = right +(z1, y0, t1) +(z2, t3) = left -(x, z1, t2) +(y2, t4) = right -(z2, y1, t3) +return (y2, z2::t4) +``` + +Its negative branch uses the complete reversed word with inverted signs: +`right +; left +; right -; left -`. The intermediate scratch states are +passed explicitly. They are not silently reset before the next child. + +For arbitrary nonlinear leaves, the increment is defined recursively by + +```text +delta_leaf(x,t) = f_label(x) +delta_node(x,z,t) = delta_right(z + delta_left(x,t), t) + - delta_right(z, t). +``` + +`run_eq` proves by structural induction that the positive result is +`(y+delta,scratch)` and the negative result `(y-delta,scratch)`. It quantifies +over all finite trees, widths, arrays, and maps, with no linearity premise. +The cancellation is valid because the induction hypothesis restores the +deeper pool at each intermediate call. Consequences include exact restoration +of all scratch, target independence, and cancellation in both execution orders. + +Under the separate premise that every leaf map is additive, `delta_eq_product` +proves that the increment is the ordered composite of all leaves. At a node +the right composite is applied after the left composite. The proof uses +additivity and cancellation; it never interchanges factors. This covers +noncommuting additive maps on multi-coordinate arrays. Initial dirt disappears +from the ideal formula, whereas it need not disappear for nonlinear maps. + +`nonlinear_dirt_counterexample` kernel-checks the latter distinction. With +`f0(x)=x`, `f1(x)=x²`, and `x=1`, the two increments are 1 and 3 at initial +connector values 0 and 1. Both calls still restore the connector exactly. + +## What the executable binding proves + +`positiveWord` lowers the same recursive four-call grammar to explicit +factor/source/target/sign records. `inverseWord` reverses the whole list and +flips signs. The universal `negative_node_order` theorem checks that this +negative lowering has the same child order as the negative evaluator. + +The pinned Python `compose` function is extracted unchanged from its AST; +its top-level imports, arithmetic leaf, and preparation code are not executed. +A completed-leaf stub records actual source and target list identities and +performs the specified integer-array shear. The six vendored files are checked +against SHA256 and Git-blob identities before extraction. + +For factor counts 1..64 and 83, both actual dispatcher traces agree with the +independent lowering. Lean additionally checks the complete source-derived +instruction lists for counts 1..16 and 83 by definitional equality: 34 trace +theorems, with no axiom dependencies. These include all 7,744 instructions of +each 83-factor sign. The generated literals come from the actual dispatcher, +not from the reference emitter. + +Execution checks compare the mutable source dispatcher with a functional +transcription of `run` and the independent `delta` recurrence. A separate +instruction-list interpreter checks all 197 ordered binary trees through +seven leaves, including strongly unbalanced trees. Floor maps, bounded square +maps, and noncommuting integer shears exercise widths 1..3 with nonzero signed +initial dirt and targets. Both signs and full inverse cancellation are checked. + +This is a universal proof of the typed recursive evaluator and bounded +evidence connecting it to the address-level lowering and Python dispatcher. +An all-size denotational correctness proof for the address compiler and a +formal semantics of Python remain separate obligations. Literal trace equality +alone is not a proof of the numerical leaf's correctness. In particular, the +known phase-alias admission gap in the unmodified PR628 source is not repaired +here; callers must satisfy the fixed, nonaliased external-data contract. + +Rounding accuracy, coefficient preparation, physical bit/tape execution, +multiway echoes, connector reuse, cost optimization, and the multiplication +reduction are outside this result. The selected conditional κ is unchanged. diff --git a/research/lean-nonlinear-commutator/NOTICE.md b/research/lean-nonlinear-commutator/NOTICE.md new file mode 100644 index 0000000000..f42c134314 --- /dev/null +++ b/research/lean-nonlinear-commutator/NOTICE.md @@ -0,0 +1,26 @@ +# Attribution and license + +Prepared for Gareth Davidson (@bitplane), with substantial OpenAI Codex +assistance in scope selection, Lean proof development, implementation, +verification, and documentation. One AI agent performed this work; no +independent human peer review is claimed. New files are Apache-2.0. + +- Chafik Boukhalfa (@chafreaky), PR628: source-restoring rounded leaves, binary + dirty composition, and its inherited numerical/implementation contract. +- @0xkilgore, PR663: the written all-size nonlinear restoration induction, + independent free-term and noncommutative finite audit, and the exact balanced + call count. This package adds a kernel-checked semantics proof, not a new + commutator identity or a new call-count improvement. +- @androolloyd, PR673: multiway extension and the phase-alias repair, credited + context rather than an imported implementation. +- Ali Romman (@aliromman), PR621: the underlying cyclic-kernel work, with + further source attribution retained by the original notices. + +The exact consumed PR628 and PR663 files are vendored unchanged, with their +original notices and complete source pins. Their historical selected-frontier +and precision statements retain their original scope. The separate PR784/887 +resource theorem and PR877 precision audit are not dependencies of this proof. +No literature-priority claim is made for the commutator or its algebra. + +The official Lean compiler and bundled libraries are external prerequisites; +no toolchain binary is redistributed. diff --git a/research/lean-nonlinear-commutator/NonlinearEcho.lean b/research/lean-nonlinear-commutator/NonlinearEcho.lean new file mode 100644 index 0000000000..2157b8157d --- /dev/null +++ b/research/lean-nonlinear-commutator/NonlinearEcho.lean @@ -0,0 +1,251 @@ +import Std + +/- +Copyright (c) 2026 Gareth Davidson (@bitplane). Apache-2.0. +Prepared with substantial OpenAI Codex assistance. +Formalizes the binary nonlinear restoration argument of PR628 / PR663. +Leaves are completed source-restoring shears with fixed external data. +-/ + +set_option autoImplicit false + +namespace NonlinearEcho + +abbrev Value (width : Nat) := Fin width → Int +abbrev Dirt (width depth : Nat) := Fin depth → Value width + +def add {w : Nat} (a b : Value w) : Value w := fun i => a i + b i +def sub {w : Nat} (a b : Value w) : Value w := fun i => a i - b i + +theorem add_sub_cancel {w : Nat} (a b : Value w) : sub (add a b) b = a := by + funext i + simp [add, sub] + +theorem sub_add_cancel {w : Nat} (a b : Value w) : add (sub a b) b = a := by + funext i + simp [add, sub] + +theorem target_forward {w : Nat} (y a b : Value w) : + sub (add y a) b = add y (sub a b) := by + funext i + simp only [add, sub] + omega + +theorem target_inverse {w : Nat} (y a b : Value w) : + sub (add y b) a = sub y (sub a b) := by + funext i + simp only [add, sub] + omega + +theorem add_sub_left {w : Nat} (a b : Value w) : sub (add a b) a = b := by + funext i + simp only [add, sub] + omega + +def head {w d : Nat} (s : Dirt w (d+1)) : Value w := s 0 +def tail {w d : Nat} (s : Dirt w (d+1)) : Dirt w d := fun i => s i.succ +def join {w d : Nat} (z : Value w) (s : Dirt w d) : Dirt w (d+1) := Fin.cases z s + +theorem join_head_tail {w d : Nat} (s : Dirt w (d+1)) : join (head s) (tail s) = s := by + funext i + refine Fin.cases ?_ (fun j => ?_) i + · rfl + · rfl + +/-- Binary factor trees, indexed by available disjoint deeper scratch. +Leaves may leave capacity unused; both children reuse the same deeper pool. -/ +inductive Tree : Nat → Type where + | leaf (depth label : Nat) : Tree depth + | node {depth : Nat} (left right : Tree depth) : Tree (depth+1) + +/-- The literal four-call sequence, including the true reverse word. +The source is an immutable argument of the completed-leaf interface. +Scratch arrays and target are separate typed components. -/ +def run {w d : Nat} (f : Nat → Value w → Value w) (t : Tree d) + (positive : Bool) (x y : Value w) (s : Dirt w d) : Value w × Dirt w d := + match t with + | .leaf _ label => (if positive then add y (f label x) else sub y (f label x), s) + | .node left right => + let z := head s + let rest := tail s + if positive then + let (z1, s1) := run f left true x z rest + let (y1, s2) := run f right true z1 y s1 + let (z2, s3) := run f left false x z1 s2 + let (y2, s4) := run f right false z2 y1 s3 + (y2, join z2 s4) + else + let (y1, s1) := run f right true z y rest + let (z1, s2) := run f left true x z s1 + let (y2, s3) := run f right false z1 y1 s2 + let (z2, s4) := run f left false x z1 s3 + (y2, join z2 s4) + +/-- A recursively composed nonlinear increment can depend on initial dirt. -/ +def delta {w d : Nat} (f : Nat → Value w → Value w) (t : Tree d) + (x : Value w) (s : Dirt w d) : Value w := + match t with + | .leaf _ label => f label x + | .node left right => + sub (delta f right (add (head s) (delta f left x (tail s))) (tail s)) + (delta f right (head s) (tail s)) + +/-- All finite trees, widths, integer arrays, and deterministic nonlinear leaves. -/ +theorem run_eq {w d : Nat} (f : Nat → Value w → Value w) (t : Tree d) + (positive : Bool) (x y : Value w) (s : Dirt w d) : + run f t positive x y s = + (if positive then add y (delta f t x s) else sub y (delta f t x s), s) := by + induction t generalizing positive x y with + | leaf depth label => rfl + | node left right ihl ihr => + cases positive <;> + simp only [run, Bool.false_eq_true, ↓reduceIte, ihl, ihr, + add_sub_cancel, join_head_tail, delta] + · rw [target_inverse] + · rw [target_forward] + +theorem scratch_restored {w d : Nat} (f : Nat → Value w → Value w) (t : Tree d) + (positive : Bool) (x y : Value w) (s : Dirt w d) : + (run f t positive x y s).2 = s := by + rw [run_eq] + +theorem positive_increment {w d : Nat} (f : Nat → Value w → Value w) (t : Tree d) + (x y : Value w) (s : Dirt w d) : + sub (run f t true x y s).1 y = delta f t x s := by + rw [run_eq] + exact add_sub_left y _ + +theorem exact_inverse {w d : Nat} (f : Nat → Value w → Value w) (t : Tree d) + (x y : Value w) (s : Dirt w d) : + let forward := run f t true x y s + run f t false x forward.1 forward.2 = (y,s) := by + simp only [run_eq, Bool.false_eq_true, ↓reduceIte, add_sub_cancel] + +theorem inverse_then_forward {w d : Nat} (f : Nat → Value w → Value w) (t : Tree d) + (x y : Value w) (s : Dirt w d) : + let backward := run f t false x y s + run f t true x backward.1 backward.2 = (y,s) := by + simp only [run_eq, Bool.false_eq_true, ↓reduceIte, sub_add_cancel] + +def IsAdditive {w : Nat} (f : Value w → Value w) : Prop := + ∀ a b, f (add a b) = add (f a) (f b) + +/-- Factors apply in left-to-right leaf order: right after left. +No interchange of factor maps is used. -/ +def product {w d : Nat} (f : Nat → Value w → Value w) (t : Tree d) + (x : Value w) : Value w := + match t with + | .leaf _ label => f label x + | .node left right => product f right (product f left x) + +theorem product_additive {w d : Nat} (f : Nat → Value w → Value w) + (hf : ∀ label, IsAdditive (f label)) (t : Tree d) : IsAdditive (product f t) := by + induction t with + | leaf depth label => exact hf label + | node left right ihl ihr => + intro a b + simp only [product, ihl a b, ihr (product f left a) (product f left b)] + +/-- Ideal additive maps give the ordered product, independently of all dirt. -/ +theorem delta_eq_product {w d : Nat} (f : Nat → Value w → Value w) + (hf : ∀ label, IsAdditive (f label)) (t : Tree d) (x : Value w) (s : Dirt w d) : + delta f t x s = product f t x := by + induction t generalizing x with + | leaf depth label => rfl + | node left right ihl ihr => + simp only [delta, ihl, ihr, product] + have hadd := product_additive f hf right (head s) (product f left x) + rw [hadd, add_sub_left] + +theorem ideal_execution {w d : Nat} (f : Nat → Value w → Value w) + (hf : ∀ label, IsAdditive (f label)) (t : Tree d) + (positive : Bool) (x y : Value w) (s : Dirt w d) : + run f t positive x y s = + (if positive then add y (product f t x) else sub y (product f t x), s) := by + rw [run_eq, delta_eq_product f hf] + +structure State (width depth : Nat) where + source : Value width + target : Value width + dirty : Dirt width depth + +def execute {w d : Nat} (f : Nat → Value w → Value w) (t : Tree d) + (positive : Bool) (state : State w d) : State w d := + let result := run f t positive state.source state.target state.dirty + ⟨state.source, result.1, result.2⟩ + +/-- Source restoration is the assumed completed-leaf interface; the scratch +restoration and target formula follow from the recursive semantics proof. -/ +theorem full_execution {w d : Nat} (f : Nat → Value w → Value w) (t : Tree d) + (positive : Bool) (state : State w d) : + execute f t positive state = + ⟨state.source, + if positive then add state.target (delta f t state.source state.dirty) + else sub state.target (delta f t state.source state.dirty), + state.dirty⟩ := by + simp only [execute, run_eq] + +def twoLeaf : Tree 1 := .node (.leaf 0 0) (.leaf 0 1) +def nonlinearLeaves (label : Nat) (x : Value 1) : Value 1 := + if label = 0 then x else fun i => x i * x i + +/-- Exact restoration alone does not imply independence from initial dirt. -/ +theorem nonlinear_dirt_counterexample : + delta nonlinearLeaves twoLeaf (fun _ => 1) (fun _ _ => 0) ≠ + delta nonlinearLeaves twoLeaf (fun _ => 1) (fun _ _ => 1) := by + intro h + have hi := congrFun h 0 + change (1 : Int) = 3 at hi + omega + +structure Instruction where + factor : Nat + source : Nat + target : Nat + positive : Bool + deriving DecidableEq, Repr + +def flip (i : Instruction) : Instruction := { i with positive := !i.positive } +def inverseWord (xs : List Instruction) : List Instruction := xs.reverse.map flip + +theorem inverse_append (xs ys : List Instruction) : + inverseWord (xs ++ ys) = inverseWord ys ++ inverseWord xs := by + simp [inverseWord, List.reverse_append] + +theorem inverse_involutive (xs : List Instruction) : inverseWord (inverseWord xs) = xs := by + simp [inverseWord, List.map_reverse, List.map_map, Function.comp_def, flip] + +/-- Address-level lowering of the same four-call macro grammar. +The caller assigns source/target below `fresh`; deeper scratch starts above it. -/ +def positiveWord {d : Nat} (t : Tree d) (source target fresh : Nat) : List Instruction := + match t with + | .leaf _ label => [⟨label, source, target, true⟩] + | .node left right => + let a := positiveWord left source fresh (fresh+1) + let b := positiveWord right fresh target (fresh+1) + a ++ b ++ inverseWord a ++ inverseWord b + +def word {d : Nat} (t : Tree d) (positive : Bool) (source target fresh : Nat) : List Instruction := + if positive then positiveWord t source target fresh + else inverseWord (positiveWord t source target fresh) + +theorem negative_node_order {d : Nat} (left right : Tree d) (source target fresh : Nat) : + word (.node left right) false source target fresh = + word right true fresh target (fresh+1) ++ word left true source fresh (fresh+1) ++ + word right false fresh target (fresh+1) ++ word left false source fresh (fresh+1) := by + simp [word, positiveWord, inverse_append, inverse_involutive, List.append_assoc] + +#print axioms run_eq +#print axioms scratch_restored +#print axioms positive_increment +#print axioms exact_inverse +#print axioms inverse_then_forward +#print axioms product_additive +#print axioms delta_eq_product +#print axioms ideal_execution +#print axioms full_execution +#print axioms nonlinear_dirt_counterexample +#print axioms inverse_involutive +#print axioms negative_node_order + +end NonlinearEcho diff --git a/research/lean-nonlinear-commutator/README.md b/research/lean-nonlinear-commutator/README.md new file mode 100644 index 0000000000..f1bd49fb37 --- /dev/null +++ b/research/lean-nonlinear-commutator/README.md @@ -0,0 +1,115 @@ +# Lean semantics of nonlinear dirty commutators + +**Scoped formalization / independent verification; no new κ.** +Lean 4.21.0 proves the nonlinear restoration induction from +[PR628](https://github.com/CrocSwap/integer-mult-bounds/pull/628) and +[PR663](https://github.com/CrocSwap/integer-mult-bounds/pull/663) for an explicit +typed recursive evaluator. Every finite binary tree restores its arbitrary +borrowed arrays, has an increment independent of its initial target, and has +an exact reverse-word inverse. Leaves may be arbitrary deterministic nonlinear +maps on integer arrays of any finite width. + +With additive leaves, a separate theorem proves the ordered factor product, +independent of initial dirt, without assuming that factors commute. This adds +a kernel-checked proof of the existing argument, not a new commutator, +call-count improvement, precision estimate, or multiplication exponent. + +The key identity is + +```text +delta_node(x,z,t) = delta_right(z + delta_left(x,t), t) + - delta_right(z,t) +run_positive(x,y,s) = (y + delta(x,s), s) +run_negative(x,y,s) = (y - delta(x,s), s). +``` + +The evaluator passes the actual intermediate deeper-scratch states between +children. Their restoration is proved by induction. The source-restoring, +target-independent leaf interface and fixed external parameters are premises +of the model. [MODEL.md](MODEL.md) states the exact trust boundary; the source +proof is [NonlinearEcho.lean](NonlinearEcho.lean). + +## Reproduce + +Use Python 3.12+ and the official +[Lean 4.21.0 toolchain](https://github.com/leanprover/lean4/releases/tag/v4.21.0), +with core and bundled Std only: + +```sh +python3 -B -I research/lean-nonlinear-commutator/verify.py --lean /path/to/lean-4.21.0/bin/lean +``` + +Expected final line: + +```text +PASS_NONLINEAR_ECHO: 12 formal statements; 34 kernel trace equalities; 1170 source cases; 2364 tree cases; 13 controls; kappa unchanged +``` + +The generic proof alone, from this directory: + +```sh +lean -DwarningAsError=true NonlinearEcho.lean +``` + +The verifier compiles fresh temporary objects, authenticates every consumed +source before AST extraction, and compares the complete deterministic receipt +with [EXPECTED.json](EXPECTED.json). It needs neither Git nor network access +and writes nothing inside the package by default. `--write /new/receipt.json` +reconstructs a receipt; `--emit-cases /new/TraceCases.lean` saves all source +trace equalities for inspection. Both refuse to overwrite existing outputs. +The expanded 83-factor proofs use an explicit 64 MiB Lean thread stack. + +## Completed evidence + +- **12 audited formal statements**, using only standard `propext` and + `Quot.sound`. The universal semantics, exact inverse in both orders, + additive-map product, and a nonlinear dirt-dependence counterexample are + kernel-checked. No proof placeholder, custom axiom, or native evaluation + oracle is used. +- **130 actual dispatcher traces / 206,830 instructions** cover factor + counts 1..64 and 83, both signs. **34 Lean equalities** bind the complete + literal source traces for counts 1..16 and 83 to the address compiler. + These equalities have no axiom dependencies. The 83-factor word has 7,744 + instructions in each direction. +- **1,170 source execution cases** use widths 1,2,3 and three leaf families: + offset floor maps, bounded square maps, and noncommuting integer shears. + Functional evaluation and the independent increment recurrence agree with + the mutable dispatcher. Both signs and full inverses execute **3,722,940** + complete leaf calls. All source and borrowed data return exactly. +- **2,364 additional execution cases** cover all **197 ordered binary trees + through seven leaves**, including unbalanced trees, with a separate literal + instruction interpreter. Ideal products retain factor order. +- **13 controls:** six compiler mutations, three disallowed-axiom inputs, + and four source alias/depth rejections. Concrete nonlinear witnesses also + distinguish scratch restoration from dirt-independent output, and full + inversion from merely negating signs in forward order. + +[VALIDATION.md](VALIDATION.md) records the executed portability and failure +checks. The bounded domain and stopping rule are in [CLAIM.json](CLAIM.json). +The fresh OS draw was **83**, coincidentally the same as the preceding pass; +this pass addresses execution semantics, whereas PR887 addresses resources. + +## Scope, pins, and credit + +Base: `f567884aeb8851b6e794af1184119a3bfbe1e631`. The dispatcher is pinned at +PR628 `0768f97d06c623b8211e651543c66135796b62bf`; the independent written audit +is PR663 `e0e546fd01b396478c68b6b6c5a16d87515983ba`. Six verbatim files and +their notices are retained with SHA256/Git-blob pins in +[SOURCES.json](SOURCES.json). The selected #799 κ remains +`1661634653669567/10^18`. + +The universal theorem concerns the typed recursive evaluator. Connection to +the raw-address compiler and Python is the stated bounded evidence. All-size +compiler correctness, Python semantics, rounded leaf accuracy/restoration, +phase preparation, physical bit/tape execution, and the multiplication theorem +remain separate obligations. The known phase-alias gap in unmodified PR628 +is not repaired here: external phase/coefficient data must be fixed and +nonaliased. Multiway echoes, connector reuse, and clean checkpoints have +different scopes. + +Credit **Chafik Boukhalfa (@chafreaky)** for PR628, **0xkilgore** for PR663's +written induction and symbolic audit, **androolloyd** for related PR673, and +**Ali Romman** for the PR621 kernel lineage. Original notices preserve further +credit. Prepared for **Gareth Davidson (@bitplane), with substantial OpenAI +Codex assistance**. One AI agent performed the work; no independent human +review is claimed. Apache-2.0; see [NOTICE.md](NOTICE.md). diff --git a/research/lean-nonlinear-commutator/SOURCES.json b/research/lean-nonlinear-commutator/SOURCES.json new file mode 100644 index 0000000000..e061294839 --- /dev/null +++ b/research/lean-nonlinear-commutator/SOURCES.json @@ -0,0 +1,60 @@ +{ + "base_commit": "f567884aeb8851b6e794af1184119a3bfbe1e631", + "subject_pr": 628, + "subject_head": "0768f97d06c623b8211e651543c66135796b62bf", + "audit_pr": 663, + "audit_head": "e0e546fd01b396478c68b6b6c5a16d87515983ba", + "files": [ + { + "commit": "0768f97d06c623b8211e651543c66135796b62bf", + "source_path": "research/prime-power-cyclic-scan/dirty.py", + "vendored_path": "vendor/pr628/dirty.py", + "sha256": "09e7f41141594e6540828330d27be27c083ee6569660ae42c0cd519b09fc8d21", + "git_blob": "2b9471083706a37519a1af7598e012f5fecf2636" + }, + { + "commit": "0768f97d06c623b8211e651543c66135796b62bf", + "source_path": "research/prime-power-cyclic-scan/DIRTY-PROOF.md", + "vendored_path": "vendor/pr628/DIRTY-PROOF.md", + "sha256": "bb7c2fdc1c4673d56531fd56fb8790c81a16813ac152c10f1afabc9efdd70d61", + "git_blob": "caf4aafc784a630d61ca7874a0bd19cbcb34e585" + }, + { + "commit": "0768f97d06c623b8211e651543c66135796b62bf", + "source_path": "research/prime-power-cyclic-scan/NOTICE.md", + "vendored_path": "vendor/pr628/NOTICE.md", + "sha256": "abeacf1ad1491d5797cfcf1f3832799bbf3b24b99597229d7bc884059a51ec68", + "git_blob": "22fbeb8ef0a28dd6b3feea718492091319ceb96e" + }, + { + "commit": "e0e546fd01b396478c68b6b6c5a16d87515983ba", + "source_path": "research/dirty-commutator-audit/README.md", + "vendored_path": "vendor/pr663/README.md", + "sha256": "0fed6e3a82c7c158614c696504d25b5693a0e8b6fe24a2140ced4e8cae2f7582", + "git_blob": "aeed8aeb2667d684786b72617df359f3e7941e96" + }, + { + "commit": "e0e546fd01b396478c68b6b6c5a16d87515983ba", + "source_path": "research/dirty-commutator-audit/NOTICE.md", + "vendored_path": "vendor/pr663/NOTICE.md", + "sha256": "39c6f175693297f1e0b24264747aec8dbee09833cb52c585142a7920d80e9d52", + "git_blob": "f70d7122899b217709597a655443b05ef3c5a338" + }, + { + "commit": "e0e546fd01b396478c68b6b6c5a16d87515983ba", + "source_path": "research/dirty-commutator-audit/SOURCE.json", + "vendored_path": "vendor/pr663/SOURCE.json", + "sha256": "723b1412d7bef4b13dcd9be35bc5983c876215c2998ed3897ee54291f8982654", + "git_blob": "24ff2299506a653c5478418b891bcae3a329e2bd" + } + ], + "compiler": "leanprover/lean4:v4.21.0", + "libraries": "core and bundled Std only", + "selected_kappa_at_base": "1661634653669567/1000000000000000000", + "compiler_release": { + "url": "https://github.com/leanprover/lean4/releases/tag/v4.21.0", + "commit": "6741444a63ee", + "tested_asset": "lean-4.21.0-linux.tar.zst", + "tested_asset_sha256": "455c6df09d5bd54d2a51b137939c47e2dda816d512ac789c4b3642c9bf98bde8" + } +} diff --git a/research/lean-nonlinear-commutator/VALIDATION.md b/research/lean-nonlinear-commutator/VALIDATION.md new file mode 100644 index 0000000000..2d68fc2540 --- /dev/null +++ b/research/lean-nonlinear-commutator/VALIDATION.md @@ -0,0 +1,104 @@ +# Executed validation + +Checked on Linux x86-64, 2026-10-13, with Python 3.14.4 and 3.12.3 and the +official Lean 4.21.0 Release compiler, commit `6741444a63ee`. Only core and +bundled Std are required. The toolchain archive SHA256 is recorded in +`SOURCES.json`; no compiler or library binary is redistributed. + +## Formal proof and source traces + +The following passes from the repository root: + +```sh +python3 -B -I research/lean-nonlinear-commutator/verify.py --lean /path/to/lean-4.21.0/bin/lean +``` + +The verifier compiles both the generic proof and the generated trace statements +from source in a fresh temporary directory. It uses one Lean worker, a 64 MiB +thread stack, warnings as errors, recursion bound 100,000, heartbeat bound +4,000,000, and a 300-second timeout per invocation. The larger explicit stack +is needed for the expanded 83-factor equality; the ordinary default stack +overflowed in the initial attempt. The complete planned domain passes with +the explicit settings. + +All 12 generic statement probes use only `propext` and/or `Quot.sound`. +All **34 literal source-trace equalities have no axiom dependencies**. No +placeholder, custom assumption, or native evaluation oracle is admitted. +The `IsAdditive` premise and completed-leaf interface remain explicit model +hypotheses, as detailed in `MODEL.md`. + +| Completed check | Coverage | +|---|---:| +| Actual source traces, both signs, n=1..64 and n=83 | 130 | +| Instructions in those traces | 206,830 | +| Kernel-checked literal traces, both signs, n=1..16 and n=83 | 34 | +| Mutable source execution cases | 1,170 | +| Source leaf calls including whole-word inverse checks | 3,722,940 | +| All ordered binary trees through seven leaves | 197 | +| Additional functional/word/delta execution cases on those trees | 2,364 | +| Compiler rejection controls | 6 | +| Disallowed-axiom audit controls | 3 | +| Source alias/depth admission controls | 4 | + +The source cases cover widths 1,2,3; the complete tree census covers widths +2,3. Both use the fixed floor, bounded-square, and integer-shear families. +Nonzero signed dirt and initial targets are deterministic. The finite domain +is not an adaptive search, and no finite replay is extrapolated into the +universal theorem. + +The generated `TraceCases.lean` SHA256 is +`35d6a7bed4b0b0350e539c71a5f58a5a9f54ad4abc02bd436c7c0985b34455bc`. +Use `--emit-cases /new/TraceCases.lean` to export it. The generic proof's +SHA256 is `c08de49fe02781d69eddc7bb9b4f3c8d311cc1bbe21e6ccb1db86eeafb97dceb`. + +## Reproducibility and failure checks + +The complete ordinary isolated Python 3.14.4 replay matches `EXPECTED.json`. +A standalone copy outside Git, in a path containing spaces, passes under +isolated **optimized** Python 3.12.3. Every copied package file and directory +is read-only during that run, and all bytes remain unchanged afterward. It +took about 41 seconds on this host, including all controls; no performance +improvement is claimed. + +An early portability check found that `ast.dump` serializes empty fields +differently between these Python versions. The final receipt instead binds +the exact extracted `compose` source segment, SHA256 +`7b9651bbed8bc2faa0cbdbfa896d75175564b01bca612dc8971c51e8ca9a5361`. +The entire immutable source is separately pinned by SHA256 and Git blob. +All proof-relevant receipt fields compare by canonical JSON, without elapsed +times, host paths, or interpreter debug serialization. + +Additional package checks reject a changed pinned `dirty.py`, a missing +`dirty.py`, and a receipt replacing the first integer factor count `1` with +JSON `true`. The last case tests strict receipt comparison despite Python's +ordinary `1 == True`. Existing receipt and generated-case output destinations +are rejected before work, preserving their original contents. These controls +also run with Python optimization enabled. + +The compiler controls independently alter scratch restoration, a final target +sign, the target-independent leaf contract, ideal factor order, whole-word +reversal, and a source-derived literal sign. Each produces a Lean error. +Audit inputs containing `sorryAx`, `Lean.ofReduceBool`, or a custom assumption +are rejected. Source admission rejects source/target aliasing, each ancestor +alias as scratch, and insufficient depth before invoking a leaf. + +## Repository and publication scope + +`make selected-record-check` passes with the selected exact +κ=`1661634653669567/10^18`. Package whitespace and scope checks pass. No selected +artifact, producer, or `upstream/` source changes. Full regenerating suites, +cold supplier reconstruction, and hosted CI success are outside the local +validation claim. + +The final full queue refresh covered **686 open PRs through #894**. Main +remained `f567884aeb8851b6e794af1184119a3bfbe1e631`, and consumed PR628/663 +heads were unchanged. New PR889 batches distinct output shears with a common +factor and has a different interface; PR893 audits historical Lean source +and recorded evidence. Neither supplies this binary-tree semantics proof. +There is no pinned coordination issue; the local claim records the result +and final PR link. + +The all-size typed semantics and the bounded Python/address connection are +distinct evidence. Numerical leaf correctness, all-size address-compiler +correctness, Python semantics, external-data nonaliasing, physical execution, +and the full multiplication reduction remain as stated in `MODEL.md`. diff --git a/research/lean-nonlinear-commutator/lean-toolchain b/research/lean-nonlinear-commutator/lean-toolchain new file mode 100644 index 0000000000..980709bbba --- /dev/null +++ b/research/lean-nonlinear-commutator/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:v4.21.0 diff --git a/research/lean-nonlinear-commutator/vendor/pr628/DIRTY-PROOF.md b/research/lean-nonlinear-commutator/vendor/pr628/DIRTY-PROOF.md new file mode 100644 index 0000000000..caf4aafc78 --- /dev/null +++ b/research/lean-nonlinear-commutator/vendor/pr628/DIRTY-PROOF.md @@ -0,0 +1,128 @@ +# Cyclic inverse shears with dirty array restoration + +This extends the classical rounded cyclic-inverse primitive of PR628. It removes +its need for a clean length-L intermediate array. It does not supply a common-label +Clifford realization, reversible bit arithmetic, transform layout, or the complete +integer-multiplication reduction. No new kappa follows from this lemma. + +## Contract + +Input x, target y and h borrowed arrays are complex dyadic grids of spacing u=2^-w. +Every array has length L>=1 and may initially contain arbitrary data. The arrays +are distinct. Their initial infinity norms are at most D. Read-only phases tau_i +have modulus one. Phase generation/storage and coefficient preparation are paid; +there is no free phase table. The primitive adds an approximation to Q(W)^-1 x +to y, restores x and every borrowed array exactly, and needs only a constant number +of clean scalar arithmetic registers besides loop counters and factor descriptors. +Here (Wx)_i=tau_i*x_(i-d), initially for d=+/-1 in a cyclic layout, and +Q(z)=r^-1 product_(j=1)^n(z-rho_j), n=r-1, with stable reciprocal/inner factors +of norm at most 1-beta. The final increment can depend on the initial dirt within +the stated approximation error. Exact independence of the increment from dirt is +not claimed for rounded arithmetic. + +## One factor + +First consider T x = y defined by y_i=x_i+b_i*y_(i-d), |b_i|<=1-beta. +Choose the cyclic order in direction d. Let z be the zero-boundary causal solution +and p_i the product of b from the first position through i. Let c be the complete +product. Then y_i=z_i+p_i*s, s=z_last/(1-c). The stable cyclic equation itself +implies ||y||<=B/beta when ||x||<=B, so |s|<=B/beta. + +On the dyadic grid, perform the causal pass directly in x, skipping the first +position: x_i += round(b_i*x_previous). These are integer lifts. Reversing their +order and subtracting the same rounded source products restores x exactly, +including arbitrary nonzero initial values. During the first pass also accumulate +the rounded scalar product c_hat. Compute s_hat=round(z_hat_last/(1-c_hat)). +In a second pass accumulate rounded prefix products p_hat_i and add +round(m_i*(z_hat_i+round(p_hat_i*s_hat))) to the appropriate target position. +Finally undo the causal lifts. Each target position is written exactly once; +its existing value never enters the computed increment. Scalar arithmetic and +coefficient scratch can be cleared classically; no reversible arithmetic gate +claim is made. Three passes suffice, excluding validation scans and paid +coefficient access. O(1) clean scalar words and O(log L) indexing bits suffice. + +Nearest complex rounding has norm error at most u. Assuming u<=beta^2/2, +|z_hat-z|<=u/beta, |p_hat-p|<=u/beta, |c_hat-c|<=u/beta, and +|1-c_hat|>=beta/2. Using s=z_last/(1-c), rather than separately bounding the +numerator and denominator, gives + + |s_hat-s| <= u + (2/beta)*(u/beta + (B/beta)*(u/beta)) + <= 5*(B+1)*u/beta^3. + +Also |p_hat|<=1+u/beta<=3/2. Hence the corrected output before m multiplication +has error at most 12*(B+1)*u/beta^3. If |m_i|<=r, the final rounded multiplication +has error at most a*(B+1)*u, a=13*(r+1)/beta^3. None of these constants depends +on L. + +For an outer root, b_i=rho^-1*tau_i, m_i=-rho^-1. For an inner root, scan in +direction -d with b_i=rho*conjugate(tau_(i+d)); the value at position i is +multiplied by conjugate(tau_i) and added at i-d. This is +(W-rho I)^-1=(I-rho W^-1)^-1 W^-1. The scalar r is included in one leaf's +multiplier. Each exact factor has operator norm at most K=r/beta. No permutation +of the mutable source array is required for the inner factor. + +## Product of factors + +For exact linear maps A,B and a dirty scratch array z, the sequence + + z += B*x; y += A*z; z -= B*x; y -= A*z + +adds AB*x to y and restores z. Split the factor list in halves recursively; +use one distinct borrowed array per recursion depth. A negative call executes +the exact inverse instruction word (reverse operation order and invert signs). +It is not obtained by negating signs in the original order. + +The rounded construction still restores every borrowed array and x exactly. +Inductively each call preserves its input and all deeper scratch, and its increment +is independent of its target. The paired calls computing B therefore see the same +input and deeper initial dirt. Never use an ancestor input or target as deeper +scratch: the ancestor target may have changed between the paired calls. This is +an explicit alias exclusion in the executable contract. + +There are h=ceil(log2 n) borrowed arrays and at most N=4*n^2 leaf calls. Pad to the +next power of two for this count if desired (identity leaves require no rounded +inverse). The implementation splits without padding and checks the actual count. + +For the ideal elementary shears, the joint max norm grows by at most C=1+K per +leaf. With a*u<=1 the computed trajectory satisfies + + M_j+1 <= G^j*(D+1), G=C+1. + +Comparing the complete rounded word with the ideal word on the same initial +arrays, and summing the propagated leaf errors, gives + + E_N <= N*a*(D+1)*u*G^(N-1). + +The ideal word cancels all borrowed initial data exactly. This proves the target +error bound for every length and every initial dirt bounded by D, while actual +restoration is exact without an error allowance. Choosing + + w >= p+1+ceil(log2(N*a*(D+1)))+(N-1)*ceil(log2 G) + +and enforcing a*u<=1 and u<=beta^2/2 gives execution error <=2^(-p-1). +PR628's coefficient/phase perturbation bound, budgeted to <=2^(-p-1) for the +original x, then gives total <=2^-p. That perturbation bound scales with ||x||; +for general input bound X use p+ceil(log2(max(1,X))) in its preparation budget. +The initial borrowed dirt does not enter the ideal operator perturbation bound. + +PR628 has log2(beta^-1)=O(r^3). Therefore these deliberately loose budgets need +w=O(p+log(D+1)+r^5) bits, and O(r^2) passes. Inside a leaf, the causal state and closure scalars add at most another +O(log(beta^-1)+log r) magnitude bits. Maximum transient magnitudes thus add +O(log(D+1)+r^5) integer bits, already covered by this word-size bound. Standard +fast fixed-precision arithmetic yields soft-O((L*r^2+r^3)*(p+log(D+1)+r^5)) +bit work plus charged phase-oracle and routing costs. Factor preparation and +coefficient enclosures are inherited from PR628. Borrowed storage is +O(L log r) words; clean arithmetic storage is O(w+log L) bits up to the chosen +multiplication implementation's workspace, plus O(r) read-only factor descriptors. +A machine with only a fixed number of dirty data arrays is not covered by this +contract. Arbitrary stride still incurs PR628's explicitly charged routing. + +## Executable evidence + +`dirty.py` uses exact rational arithmetic and explicit nearest dyadic rounding. +It checks generic variable-coefficient leaves, dense independently assembled +factor inverses, both orientations, nonzero targets, several initial dirty arrays, +exact source/scratch restoration, exact whole-word inversion, and the leaf count. +Finite checks support the implementation; the inequalities above are the all-L +argument. The exact-rational prototype does not itself implement the claimed +fast fixed-precision arithmetic cost. diff --git a/research/lean-nonlinear-commutator/vendor/pr628/NOTICE.md b/research/lean-nonlinear-commutator/vendor/pr628/NOTICE.md new file mode 100644 index 0000000000..22fbeb8ef0 --- /dev/null +++ b/research/lean-nonlinear-commutator/vendor/pr628/NOTICE.md @@ -0,0 +1,24 @@ +# Attribution and scope + +Ali Romman's PR621, exact head 520774462b19b29af41554b74def31f9d01e997e, +supplies the prime-power kernel circle bound. Its kernel attribution is +OpenAI's exact-DFT preprint at adc7f1241b42e322a6451854ab7e4b4c146bf78a +(`loc:newton`, `loc:fourier-factorization`) and classical q-Pochhammer/Newton +factorization, including Alexey Kuznetsov's cited q-calculus work. This +package does not claim to originate those constructions. + +Pan's approximate-factorization theorem is used in the form stated by +Mehlhorn, Sagraloff and Wang; Brent's work supplies fast elementary-function +evaluation. Causal/anticausal recursive filtering is standard, as illustrated +by the Briand-Davy source listed in SOURCE.json. Sources are cited for these +specific tools, not as proofs of this package's complete claim. + +The scan rounding analysis, explicit budget composition, interval and +factor certificates, routed reference execution, and packaging were +prepared with substantial OpenAI Codex assistance for chafreaky. The dense +matrix solver and algebraic coefficient crosschecks provide independent +computational paths, not human peer review or formal Lean verification. + +No new multiplication exponent, literature priority, maintainer acceptance, +physical tape execution, or production performance result is claimed. +The code and documents use the repository's Apache-2.0 license. diff --git a/research/lean-nonlinear-commutator/vendor/pr628/dirty.py b/research/lean-nonlinear-commutator/vendor/pr628/dirty.py new file mode 100644 index 0000000000..2b94710837 --- /dev/null +++ b/research/lean-nonlinear-commutator/vendor/pr628/dirty.py @@ -0,0 +1,133 @@ +"""Integer lifting for cyclic inverse shears using borrowed dirty arrays. +Exact rational prototype. Arithmetic workspace and phase access are charged in the proof; +this is not a common-label Clifford word or a bit-reversible arithmetic compiler. +""" +from pathlib import Path +from fractions import Fraction as F +import importlib.util,json,argparse,itertools +P=Path(__file__).resolve().parent +s=importlib.util.spec_from_file_location('weighted',P/'weighted.py');w=importlib.util.module_from_spec(s);s.loader.exec_module(w);c=w.c + +def scaled(z,q):return(z[0]*q,z[1]*q) +def conj(z):return(z[0],-z[1]) +def ordered(n,d):return range(n)if d==1 else range(n-1,-1,-1) + +def lift(x,y,coefficient,beta,bits,d,sign=1,destination=None,multiplier=None,stats=None): + """y += sign*F(x), restoring x exactly; no length-dependent clean data array.""" + n=len(x);c.need(x is not y and n==len(y)>0,'distinct equally sized arrays') + c.need(d in(-1,1)and sign in(-1,1),'orientation and sign') + c.need(0=(beta/2)**2,'closure denominator') + seed=c.rounded(c.div(x[previous],denominator),bits) + power=c.ONE + for i in ordered(n,d): + power=c.rounded(c.mul(coefficient(i),power),bits) + value=c.add(x[i],c.rounded(c.mul(power,seed),bits)) + value=c.rounded(c.mul(multiplier(i),value),bits) + j=destination(i);y[j]=c.add(y[j],scaled(value,sign)) + # The scalar seed and coefficient scratch may be cleared by ordinary classical + # arithmetic. The dirty data itself is restored by exact inverse integer lifts. + first=0 if d==1 else n-1 + for i in ordered(n,-d): + if i!=first:x[i]=c.sub(x[i],c.rounded(c.mul(coefficient(i),x[i-d]),bits)) + if stats is not None:stats['leaves']+=1;stats['scalar_steps']+=3*n + +def leaf(x,y,factor,phases,beta,bits,d,sign,stats): + inside,b,scale=factor;n=len(x) + if inside: + lift(x,y,lambda i:c.mul(b,conj(phases[(i+d)%n])),beta,bits,-d,sign, + lambda i:(i-d)%n,lambda i:scaled(conj(phases[i]),scale),stats) + else: + lift(x,y,lambda i:c.mul(b,phases[i]),beta,bits,d,sign, + multiplier=lambda i:scaled(c.neg(b),scale),stats=stats) + +def compose(x,y,factors,scratch,phases,beta,bits,d,sign=1,stats=None): + """Balanced commutator; negative call is the exact inverse instruction word.""" + c.need(sign in(-1,1)and d in(-1,1),'orientation and sign') + c.need(factors and len(scratch)>=(len(factors)-1).bit_length(),'dirty depth') + arrays=[x,y]+scratch;c.need(len({id(v)for v in arrays})==len(arrays),'all ancestor arrays distinct') + c.need(len(x)>0 and all(len(v)==len(x)for v in arrays)and len(phases)==len(x),'array lengths') + c.need(all(c.norm2(t)==1 for t in phases),'unit phases') + if len(factors)==1:return leaf(x,y,factors[0],phases,beta,bits,d,sign,stats) + mid=len(factors)//2;B,A=factors[:mid],factors[mid:];z=scratch[0];rest=scratch[1:] + operations=[(x,z,B,1),(z,y,A,1),(x,z,B,-1),(z,y,A,-1)] + if sign==-1:operations=[(src,dst,fs,-sgn)for src,dst,fs,sgn in reversed(operations)] + for src,dst,fs,sgn in operations:compose(src,dst,fs,rest,phases,beta,bits,d,sgn,stats) + +def exact_operator(x,factors,phases,d): + # Dense rational oracle constructed independently from the lifting recurrence. + n=len(x);out=x[:] + for inside,b,scale in factors: + a=[[c.ZERO for _ in range(n)]for _ in range(n)] + if inside: + for i in range(n):a[i][i]=c.neg(b);a[i][(i-d)%n]=c.add(a[i][(i-d)%n],phases[i]) + else: + rho=c.div(c.ONE,b) + for i in range(n):a[i][i]=c.neg(rho);a[i][(i-d)%n]=c.add(a[i][(i-d)%n],phases[i]) + out=[scaled(z,scale)for z in w.solve(a,out)] + return out + +def certificate(n,beta,r,D,bits): + N=4*n*n;a=13*(r+1)/beta**3;G=2+F(r)/beta;u=F(1,1<