From d213ac12d4a1ab8f717d942e844df318ceb395fb Mon Sep 17 00:00:00 2001 From: alephnan <206279168+alephnan@users.noreply.github.com> Date: Mon, 12 Oct 2026 23:53:00 -0600 Subject: [PATCH 1/2] Research: degree-controlled cyclic inverse bound by root reflection Apply classical root reflection, rational arc length, and Hardy coefficient control to the pinned PR621 circle certificate. Add the written proof, exact finite verifier, fault controls, source pins, and attribution. No new kappa claim. Prepared for Rafael Guevara with substantial OpenAI Codex assistance. --- research/rational-circle-bound/.gitattributes | 2 + research/rational-circle-bound/CLAIM.json | 73 +++ research/rational-circle-bound/EXPECTED.json | 233 +++++++++ research/rational-circle-bound/LICENSE | 201 ++++++++ research/rational-circle-bound/MANIFEST.json | 24 + research/rational-circle-bound/NOTICE.md | 46 ++ research/rational-circle-bound/PROOF.md | 257 ++++++++++ research/rational-circle-bound/README.md | 91 ++++ research/rational-circle-bound/SOURCES.json | 109 ++++ research/rational-circle-bound/VALIDATION.md | 81 +++ .../evidence/environment.json | 16 + .../evidence/package-tests.txt | 9 + .../rational-circle-bound/evidence/verify.txt | 2 + .../rational-circle-bound/test_package.py | 106 ++++ .../vendor/previous-fourier-NOTICE.md | 34 ++ .../vendor/previous-fourier-PROOF.md | 172 +++++++ .../vendor/prime-power-NOTICE.md | 21 + .../vendor/prime-power-proof.md | 212 ++++++++ .../vendor/selected-result.json | 123 +++++ research/rational-circle-bound/verify.py | 474 ++++++++++++++++++ 20 files changed, 2286 insertions(+) create mode 100644 research/rational-circle-bound/.gitattributes create mode 100644 research/rational-circle-bound/CLAIM.json create mode 100644 research/rational-circle-bound/EXPECTED.json create mode 100644 research/rational-circle-bound/LICENSE create mode 100644 research/rational-circle-bound/MANIFEST.json create mode 100644 research/rational-circle-bound/NOTICE.md create mode 100644 research/rational-circle-bound/PROOF.md create mode 100644 research/rational-circle-bound/README.md create mode 100644 research/rational-circle-bound/SOURCES.json create mode 100644 research/rational-circle-bound/VALIDATION.md create mode 100644 research/rational-circle-bound/evidence/environment.json create mode 100644 research/rational-circle-bound/evidence/package-tests.txt create mode 100644 research/rational-circle-bound/evidence/verify.txt create mode 100644 research/rational-circle-bound/test_package.py create mode 100644 research/rational-circle-bound/vendor/previous-fourier-NOTICE.md create mode 100644 research/rational-circle-bound/vendor/previous-fourier-PROOF.md create mode 100644 research/rational-circle-bound/vendor/prime-power-NOTICE.md create mode 100644 research/rational-circle-bound/vendor/prime-power-proof.md create mode 100644 research/rational-circle-bound/vendor/selected-result.json create mode 100644 research/rational-circle-bound/verify.py diff --git a/research/rational-circle-bound/.gitattributes b/research/rational-circle-bound/.gitattributes new file mode 100644 index 0000000000..5107610dd5 --- /dev/null +++ b/research/rational-circle-bound/.gitattributes @@ -0,0 +1,2 @@ +# Source and receipt hashes refer to exact committed bytes on every platform. +* -text diff --git a/research/rational-circle-bound/CLAIM.json b/research/rational-circle-bound/CLAIM.json new file mode 100644 index 0000000000..81549e5dbf --- /dev/null +++ b/research/rational-circle-bound/CLAIM.json @@ -0,0 +1,73 @@ +{ + "status": "prepared_for_pull_request", + "started_utc": "2026-10-13T05:18:28Z", + "claim_utc": "2026-10-13T05:27:00Z", + "expected_finish_utc": "2026-10-13T06:15:00Z", + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "assignment": "Continuation of OS-seed-71 mathematical audit, at the user's request to try a distinct approach using the previous findings. No new random track draw.", + "coordination": "Only open issue #650 found; it requests Discussions and is not a coordination issue. Local claim; no reservation issue.", + "candidates": [ + { + "idea": "Sharpen scan rounding by shared closure factors", + "decision": "Rejected: new PR764 already supplies a sharp inverse-square bound." + }, + { + "idea": "Use the q-difference identity P(uz)=(1-z)P(z)+z^r/r for composite nonvanishing", + "decision": "Deferred: no complete quantitative consequence established in the orientation budget; PR666 already covers modular composite lifting." + }, + { + "idea": "Reflect interior roots and use rational arc length plus Hardy coefficient control", + "decision": "Selected: replace a derivative-dependent inverse-gap power by a polynomial degree factor." + } + ], + "hypothesis": "For a degree-n polynomial P with |P|>=delta on the circle, the Laurent coefficient norm of 1/P is at most (1+4n)^2/delta; hence the same bound for P(U)^-1 when all integer powers of U have norm at most one.", + "bounded_experiment": "Written proof of all analytic steps; 14 exact budget comparisons; fixed rational polynomial/reflection and cyclic inverse families; finite Hilbert-matrix checks; near-circle one-pole family; explicit invalid-shortcut controls.", + "novelty_scope": "New application relative to the inspected repository work, not a priority claim for reflection, Blaschke products, Hardy's inequality or the Dolzhenko-Spijker inequality.", + "related_prs": [ + 621, + 628, + 666, + 668, + 692, + 736, + 764 + ], + "latest_pr_seen_at_claim": 767, + "verification_reserve": "Reserve the final quarter for proof audit, clean and optimized replays, source/overlap refresh, and patch packaging.", + "finished_utc": "2026-10-13T05:38:45.011622+00:00", + "final_main_unchanged": true, + "latest_pr_seen_final": 783, + "final_overlap_queries": [ + "Blaschke", + "Hardy", + "Spijker", + "Fourier", + "cyclic inverse", + "circle bound" + ], + "final_related_head_unchanged": { + "764": "983d66f0f2e48ee500ec7eee2da9244c001c5064" + }, + "result": "Degree-controlled inverse bound (1+4n)^2/delta; necessary inverse-gap exponent one; no kappa claim.", + "checks": { + "radix_budgets": 14, + "reflection_families": 126, + "boundary_identities": 756, + "cyclic_matrices": 546, + "cyclic_inverse_entries": 9516, + "hilbert_comparisons": 6565, + "near_circle_instances": 128, + "mathematical_controls": 21, + "package_tests": 8 + }, + "checkout": "Isolated Git worktree at local partial-snapshot commit 042d24c, with upstream identity recorded separately. Network clone unavailable; exact pinned inputs were obtained in the preceding audit.", + "initial_submission": "Focused patch fallback. Fresh API lookup of alephnan/integer-mult-bounds returned NOT_FOUND; no available fork-creation capability, and the session browser was unavailable. No PR created.", + "publication_preflight_utc": "2026-10-13T05:51:45.482843+00:00", + "submission": "User created the fork and authorized submission. Publication targets CrocSwap/integer-mult-bounds:main from alephnan:research/rational-circle-bound. GitHub API commit uses the complete upstream base tree and commit as parent.", + "latest_pr_seen_before_publication": 799, + "additional_overlap": { + "pr": 796, + "head": "22902155c7875139e43e4fdf15723142d6709bdd", + "distinction": "Nonarchimedean root valuations; explicitly not complex root moduli or a conditioning bound." + } +} diff --git a/research/rational-circle-bound/EXPECTED.json b/research/rational-circle-bound/EXPECTED.json new file mode 100644 index 0000000000..a86016f8dc --- /dev/null +++ b/research/rational-circle-bound/EXPECTED.json @@ -0,0 +1,233 @@ +{ + "schema": 1, + "status": "PASS_RATIONAL_CIRCLE_BOUND", + "base": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "source_files": 6, + "budgets": [ + { + "r": 3, + "prime": 3, + "prime_exponent": 1, + "n": 2, + "D": 2, + "old_bits": 28, + "previous_bits": 21, + "new_bits": 19, + "saved_vs_previous": 2, + "saved_vs_original": 9 + }, + { + "r": 4, + "prime": 2, + "prime_exponent": 2, + "n": 3, + "D": 2, + "old_bits": 53, + "previous_bits": 40, + "new_bits": 32, + "saved_vs_previous": 8, + "saved_vs_original": 21 + }, + { + "r": 5, + "prime": 5, + "prime_exponent": 1, + "n": 4, + "D": 4, + "old_bits": 165, + "previous_bits": 124, + "new_bits": 88, + "saved_vs_previous": 36, + "saved_vs_original": 77 + }, + { + "r": 7, + "prime": 7, + "prime_exponent": 1, + "n": 6, + "D": 6, + "old_bits": 510, + "previous_bits": 382, + "new_bits": 261, + "saved_vs_previous": 121, + "saved_vs_original": 249 + }, + { + "r": 8, + "prime": 2, + "prime_exponent": 3, + "n": 7, + "D": 4, + "old_bits": 455, + "previous_bits": 340, + "new_bits": 233, + "saved_vs_previous": 107, + "saved_vs_original": 222 + }, + { + "r": 9, + "prime": 3, + "prime_exponent": 2, + "n": 8, + "D": 6, + "old_bits": 870, + "previous_bits": 651, + "new_bits": 441, + "saved_vs_previous": 210, + "saved_vs_original": 429 + }, + { + "r": 11, + "prime": 11, + "prime_exponent": 1, + "n": 10, + "D": 10, + "old_bits": 2206, + "previous_bits": 1652, + "new_bits": 1108, + "saved_vs_previous": 544, + "saved_vs_original": 1098 + }, + { + "r": 16, + "prime": 2, + "prime_exponent": 4, + "n": 15, + "D": 8, + "old_bits": 3843, + "previous_bits": 2879, + "new_bits": 1925, + "saved_vs_previous": 954, + "saved_vs_original": 1918 + }, + { + "r": 25, + "prime": 5, + "prime_exponent": 2, + "n": 24, + "D": 20, + "old_bits": 23997, + "previous_bits": 17992, + "new_bits": 11999, + "saved_vs_previous": 5993, + "saved_vs_original": 11998 + }, + { + "r": 27, + "prime": 3, + "prime_exponent": 3, + "n": 26, + "D": 18, + "old_bits": 25267, + "previous_bits": 18945, + "new_bits": 12633, + "saved_vs_previous": 6312, + "saved_vs_original": 12634 + }, + { + "r": 32, + "prime": 2, + "prime_exponent": 5, + "n": 31, + "D": 16, + "old_bits": 31735, + "previous_bits": 23794, + "new_bits": 15865, + "saved_vs_previous": 7929, + "saved_vs_original": 15870 + }, + { + "r": 49, + "prime": 7, + "prime_exponent": 2, + "n": 48, + "D": 42, + "old_bits": 197545, + "previous_bits": 148147, + "new_bits": 98763, + "saved_vs_previous": 49384, + "saved_vs_original": 98782 + }, + { + "r": 64, + "prime": 2, + "prime_exponent": 6, + "n": 63, + "D": 32, + "old_bits": 258011, + "previous_bits": 193493, + "new_bits": 128989, + "saved_vs_previous": 64504, + "saved_vs_original": 129022 + }, + { + "r": 71, + "prime": 71, + "prime_exponent": 1, + "n": 70, + "D": 70, + "old_bits": 695757, + "previous_bits": 521801, + "new_bits": 347859, + "saved_vs_previous": 173942, + "saved_vs_original": 347898 + } + ], + "reflection": { + "families": 126, + "boundary_points": 756, + "all_inner": 33, + "all_outer": 18, + "contains_zero": 32, + "contains_repetition": 37 + }, + "cyclic_inverses": { + "cases": 546, + "inverse_entries": 9516, + "zero_stride_cases": 195, + "nonzero_noncoprime_cases": 78 + }, + "hilbert": { + "comparisons": 6565, + "exhaustive_vectors_each_side": 81, + "exhaustive_length": 4, + "long_lengths": [ + 8, + 16, + 32, + 64 + ] + }, + "near_circle": { + "families": 128, + "epsilon": "2^-k, 1<=k<=128", + "one_pole_W_norm": "1", + "pointwise_derivative_at_1": "2^k-1", + "necessary_gap_power": "P=z-(1+epsilon), gap=epsilon, inverse at U=I has norm 2^k" + }, + "controls": [ + "inadmissible inherited radix 0", + "inadmissible inherited radix 1", + "inadmissible inherited radix 2", + "inadmissible inherited radix 6", + "inadmissible inherited radix 10", + "inadmissible inherited radix 12", + "inadmissible inherited radix 15", + "inadmissible inherited radix 18", + "inadmissible inherited radix True", + "inadmissible inherited radix 3", + "unit-circle root C(re=Fraction(1, 1), im=Fraction(0, 1))", + "unit-circle root C(re=Fraction(0, 1), im=Fraction(1, 1))", + "unit-circle root C(re=Fraction(3, 5), im=Fraction(4, 5))", + "zero polynomial", + "nonunit phase", + "zero cycle length", + "reflection without conjugation", + "omit Blaschke factor", + "Taylor expansion across an interior pole", + "replace Hilbert constant four by one", + "equate scalar maximum with induced infinity norm" + ], + "new_kappa_claim": false, + "scope": "Exact finite checks; analytic all-length proof is PROOF.md, not formalized." +} diff --git a/research/rational-circle-bound/LICENSE b/research/rational-circle-bound/LICENSE new file mode 100644 index 0000000000..261eeb9e9f --- /dev/null +++ b/research/rational-circle-bound/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-circle-bound/MANIFEST.json b/research/rational-circle-bound/MANIFEST.json new file mode 100644 index 0000000000..9bc8bcd12b --- /dev/null +++ b/research/rational-circle-bound/MANIFEST.json @@ -0,0 +1,24 @@ +{ + "schema": 1, + "sha256": { + ".gitattributes": "8d3eea09c326d8636669849bb00208a26ec4a709dfdaa505c9fdec253798dfa3", + "CLAIM.json": "26eeeaa2027af5e90e7edb40be533a549b7197211599ab2c21f9087e354dbc76", + "evidence/environment.json": "7a7fe94aaf9af7d585426260c51505685397ec836b44094d78fe353a92e2bdfd", + "evidence/package-tests.txt": "32e8de78ad3ff79dcdd0f162cfbd5f01dc031a39f346f76c57ecba288befaf91", + "evidence/verify.txt": "953432aa42f96318eb5cfe65e1d0f17a3dc0f75ca60e5e57a04fc00d4136dd9a", + "EXPECTED.json": "9e019e77443a9fc1c4938d9d03d809d813de0558581fecf2fb72efef48f4bdcc", + "LICENSE": "c71d239df91726fc519c6eb72d318ec65820627232b2f796219e87dcf35d0ab4", + "NOTICE.md": "032c8a86591624e69dd306f93a66cbc2edf5ef108a5eacd7b893a0c48f6bab08", + "PROOF.md": "ffcad151a6fda894d16d7c227c219caa79a0fc0d446d2b7f7c903ebf1a06438e", + "README.md": "af582bea08442fea7e690202c5ee23d5f79f12b2305b1dd49a3e24444813d1eb", + "SOURCES.json": "68fca3bf9cdc9a69375d692514f2bd402ed59e0540bdb87b3d96d276ce7f9c01", + "test_package.py": "287632c4632bd0de696cad3d5170eae1c15b739802a194143941abf7c41fa03d", + "VALIDATION.md": "92a7a586a9ae4fc2e0b2b168cf62f6d5fa9f31b3e42680ab8c70c96ca2a3cd4f", + "vendor/previous-fourier-NOTICE.md": "05e6e660b74d34a8ed298f41889b9bb8b7fe365137bf2179f9828cdd2bb9a8b7", + "vendor/previous-fourier-PROOF.md": "0dd5ff1a4377f4eeb92b3af7b75254bb343c64675b09201db132b394b0ebaaad", + "vendor/prime-power-NOTICE.md": "96111c95cfec3c03a6f69c8e02c5d0bceff957d187e638d0534c676d6e3ffd77", + "vendor/prime-power-proof.md": "2b8056c88e66f692f407450fff0414d41bcd09db8597be22e274a6c3dc20eb9e", + "vendor/selected-result.json": "b3bf402f31a69bde0629936a9b569bed48281568d7b16d5fba120b5311ea1f53", + "verify.py": "b40f04343586a17a8a6debb22408c30e7ed8265cbce9b079bcdddce4f0c9da6d" + } +} diff --git a/research/rational-circle-bound/NOTICE.md b/research/rational-circle-bound/NOTICE.md new file mode 100644 index 0000000000..77ff23ba18 --- /dev/null +++ b/research/rational-circle-bound/NOTICE.md @@ -0,0 +1,46 @@ +# Attribution + +Prepared for **Rafael Guevara (@alephnan)** with substantial **OpenAI Codex +assistance** in choosing the approach, mathematical derivation, source +research, implementation, verification, and writing. No sub-agents were +used. No independent human review or proof-assistant formalization is claimed. + +**Ali Romman**, incorporated PR621, supplies the prime-power polynomial, +all-embedding nonvanishing argument, quantitative resultant/cofactor circle +bound, and cyclic-operator setting. Its proof and original attribution +notice are preserved byte for byte under `vendor/`. This package relies +on that circle theorem rather than reproducing its foundation arithmetic. + +Our prior unpublished weighted-Fourier audit (local commit +`4c0004759b0ac8e2db1a1afd9fff690270786dfe`) is a comparison baseline. Its +proof and notice are retained unchanged. Its analytic bound is superseded +here for the admitted prime-power family; the prior result remains valid. + +Root reflection using finite Blaschke products and Hardy's coefficient +inequality are classical. The rational arc-length inequality is credited +to **E. P. Dolzhenko** and **M. N. Spijker**, following the historical +discussion in **Anton Baranov and Rachid Zarouf**, arXiv:1310.1182v1, +Section 1.2.2. That paper was inspected for the normalized statement and +attribution. **Yuichi Kanjin and Kunio Sato**, "Hardy's inequality for +Jacobi expansions" (2004), opening page, also records the classical Hardy +coefficient inequality. Neither paper is redistributed. The elementary +proofs and nonoptimal constant four are written out for review here. +No novelty claim is made for those classical tools or their general +combination in rational function theory. + +The finite-geometric inverse is standard. **Joshua Snider / jsnider3**, +PR692, already uses it for weighted-stride closure and bilinear-dual +verification. Our small Gaussian-rational implementation is newly written; +no PR692 code is consumed. **Chafik Boukhalfa / chafreaky**, PR628, and +**Charles Bethin / cbethin**, PR764, supply distinct rounded-scan results. +**Jason Willems / at1as**, PR666, supplies composite lifting and finite +certificates. Their results do not become discharged implementation +obligations of this analytic note. PR736's elimination optimization is +also distinct. + +The underlying kernel and OpenAI exact-DFT preprint provenance remain +as recorded in the preserved PR621 notice. The selected-result snapshot +retains the #626/#543 contributor lineage. It is historical context, not +evidence of a new exponent. + +New text and code are Apache-2.0. The unchanged upstream license is included. diff --git a/research/rational-circle-bound/PROOF.md b/research/rational-circle-bound/PROOF.md new file mode 100644 index 0000000000..0813082ee8 --- /dev/null +++ b/research/rational-circle-bound/PROOF.md @@ -0,0 +1,257 @@ +# A degree-controlled inverse bound by root reflection + +## Result + +Let P be a nonzero complex polynomial of degree n, and suppose +|P(z)| >= delta > 0 for |z|=1. Let m count its roots strictly inside +the disk, with multiplicity. The absolutely convergent Laurent series +of 1/P on the circle has coefficient norm + +\[ + \boxed{\quad \|1/P\|_W + \le { (1+4m)(1+4n)\over\delta} + \le { (1+4n)^2\over\delta}.\quad} \tag{1} +\] + +Here W denotes the sum of absolute values of all Fourier coefficients, +including negative indices. No separation between roots, nor a lower +bound on each root's distance to the circle, enters the multiplier. +Repeated roots and roots at zero are allowed. A constant polynomial +has m=n=0 and satisfies the same statement. + +If an invertible bounded operator U on a complex Banach space satisfies +||U^k|| <= 1 for every integer k, then + +\[ + \|P(U)^{-1}\|\le (1+4n)^2/\delta. \tag{2} +\] + +This applies to U=tau Z_L^w for every L>=1, integer w (including zero +and noncoprime strides), and |tau|=1, in induced infinity norm. It also +applies to a permutation with independently varying unit phases. + +The ingredients below are classical. The contribution is their explicit, +self-contained application to the circle certificate retained from Ali +Romman's PR621 and its comparison with our previous Fourier audit. It +is not a literature-priority claim, a paid inversion algorithm, a formal +proof-assistant result, or a new multiplication exponent. + +## 1. A coefficient inequality with an elementary constant + +For an analytic function h in a neighborhood of the closed disk, write +h(z)=sum_{j>=0} h_j z^j. With normalized circle measure, we will use + +\[ + \sum_{j\ge0}{|h_j|\over j+1}\le4\|h\|_{L^1}. \tag{3} +\] + +Here is a proof of this nonoptimal version of Hardy's inequality. +First the matrix K_{jk}=1/(j+k+1), j,k>=0, has l2 operator norm at most +4. Set w_j=(j+1/2)^(-1/2) and a=j+1/2. The positive function +x^(-1/2)/(a+x) is convex on x>0: in the second derivative of the +product, both second-derivative terms and the cross term are positive. +The midpoint inequality on each [k,k+1] therefore gives + +\[ + \sum_{k\ge0}{w_k\over j+k+1} + \le\int_0^\infty{dx\over(a+x)\sqrt{x}} + \le {4\over\sqrt a}=4w_j. +\] + +For the last bound, split the integral at a. Use 1/a for 1/(a+x) +on (0,a), and 1/x on (a,infinity); each piece is at most 2/sqrt(a). +Weighted Cauchy-Schwarz applied to finite nonnegative sequences s,t +now yields + +\[ + \sum_{j,k}{s_jt_k\over j+k+1} + \le \left(\sum_{j,k}K_{jk}{w_k\over w_j}s_j^2\right)^{1/2} + \left(\sum_{j,k}K_{jk}{w_j\over w_k}t_k^2\right)^{1/2} + \le4\|s\|_2\|t\|_2. \tag{4} +\] + +Suppose initially that h has no zero on the circle and is not identically +zero. Remove its finitely many disk zeros, with multiplicity, by a finite +Blaschke product J. Then h/J is analytic and zero-free on the closed +disk and has an analytic square root v in a neighborhood of that disk. +Put a=Jv, b=v. These functions satisfy h=ab and + +\[ + \|a\|_2^2=\|b\|_2^2=\|h\|_1, +\] + +since |J|=1 on the circle. The coefficient convolution, the triangle +inequality, (4), and Parseval give + +\[ + \sum_{l\ge0}{|h_l|\over l+1} + \le\sum_{j,k\ge0}{|a_j||b_k|\over j+k+1} + \le4\|a\|_2\|b\|_2=4\|h\|_1. +\] + +Use finite sums followed by monotone limits, so absolute summability is +not assumed in advance. The zero function is immediate. For possible +circle zeros, apply the result to h(rho z) along rho increasing to 1 +and avoiding the finitely many zero radii, then use monotone convergence +on the coefficients and uniform convergence on the circle. This proves +(3), including its normalization and endpoint case. + +## 2. Rational degree controls arc length + +For R=A/B of rational degree d=max(deg A,deg B), without poles on the +circle, put M=max_{|z|=1}|R(z)|. The classical Dolzhenko-Spijker estimate is + +\[ + \|R'\|_{L^1(\mathbb T)}\le dM. \tag{5} +\] + +A projection proof records why no pole distance is needed. Cancel any +common factors first, so B has no zeros on the circle. Set +gamma(t)=R(e^{it}) and x_phi(t)=Re(e^{-i phi} gamma(t)). For any fixed +phi and real level s, clearing |B(z)|^2 in x_phi(t)=s and multiplying +by z^d yields a polynomial of degree at most 2d. Conjugated polynomials +on the circle are evaluated at 1/z. Unless the polynomial is identically +zero, the level has at most 2d preimages in 0<=t<2pi. + +For each phi an identically zero level equation can occur for at most +one s, which has measure zero. Equivalently, if the projection is +constant its variation is zero. Split the nonconstant real analytic +projection into its finitely many monotone intervals. Its total variation +is the integral of the number of level crossings. Since |x_phi|<=M, + +\[ + \int_0^{2\pi}|x_\phi'(t)|\,dt\le 4dM. +\] + +Integrating over 0<=phi<2pi, the integral of +|Re(e^{-i phi}v)| is 4|v| for every complex v. Hence +4 int |gamma'| <= 8pi dM. On the circle |gamma'|=|R'|; divide by 2pi +to obtain (5). The case of a constant R is immediate. This is an +elementary proof of a classical result, not a new arc-length theorem. + +## 3. An analytic rational function has a degree-only Wiener penalty + +If R is rational of degree at most d and analytic in a neighborhood of +the closed disk, apply (3) to h=R'. For R(z)=sum r_j z^j, + +\[ + \sum_{j\ge1}|r_j|\le4\|R'\|_1\le4d\|R\|_\infty. +\] + +Also |r_0|<=||R||_infinity by the maximum principle. Therefore + +\[ + \|R\|_W\le(1+4d)\|R\|_\infty. \tag{6} +\] + +The analyticity requirement matters: 1/P can have disk poles. Applying +(6) to it before addressing those poles would be an invalid argument. + +## 4. Reflect interior roots without changing circle magnitude + +Factor P(z)=c product_{j=1}^n(z-alpha_j). All |alpha_j| differ from 1. +Define + +\[ + Q(z)=c\prod_{|\alpha_j|<1}(1-\overline{\alpha_j}z) + \prod_{|\alpha_j|>1}(z-\alpha_j), + \qquad + J(z)=\prod_{|\alpha_j|<1}{z-\alpha_j\over1-\overline{\alpha_j}z}. +\] + +Then P=JQ exactly. Every nonconstant reflected factor of Q has its +root outside the disk, and a zero root contributes the constant factor +1 to Q and a factor z to J. Thus Q has no zeros in the closed disk, +deg Q<=n, J has rational degree m, and |J|=1 on the circle. In +particular |Q|=|P|>=delta there. + +Both 1/Q and J are analytic in a neighborhood of the closed disk. +By (6), + +\[ + \|1/Q\|_W\le(1+4n)/\delta,\qquad \|J\|_W\le1+4m. +\] + +On the circle, 1/P=overline(J)/Q. Conjugating the values reverses the +Fourier indices and conjugates the coefficients, preserving their l1 +norm. The convolution inequality for absolutely summable coefficients +now gives (1). No roots need be computed to use the worst-case m<=n. + +## 5. Operator substitution and the prime-power comparison + +Write 1/P(z)=sum_{k in Z} c_k z^k on the circle. Absolute convergence +and ||U^k||<=1 make sum c_k U^k converge in operator norm. The finite +polynomial times this series has the coefficients of 1. Substitute U +to obtain P(U) sum c_k U^k = I in both orders, proving (2). + +Retain PR621's certified inputs, without changing its nonvanishing proof: + +\[ + r=\ell^a\ge3,\quad n=r-1,\quad D=\varphi(r),\quad H=2^r-1, + \quad A=\delta^{-1}=2rnH^{nD-1},\quad X=nH^{nD/2}. +\] + +The three explicit norm overestimates are + +| Estimate | Constant | Leading power of H | +|---|---|---| +| Incorporated PR621 | A(1+4X^2) | 2nD-1 | +| Previous local weighted-Fourier audit | A(1+4X) | 3nD/2-1 | +| This degree-controlled application | A(1+4n)^2 | nD-1 | + +The new constant is strictly smaller than both predecessors for every +admitted r. Indeed n>=2, D>=2, H>=2n+1, and +H^{nD/2}>=H^2>4n+2. Thus +1+4nH^{nD/2}>(1+4n)^2. The previous audit already proved its own +strict improvement over PR621; alternatively X>1 makes it immediate. + +The dominant logarithmic term is reduced by one third relative to our +previous audit and one half relative to PR621 as r grows. The order is +still O(r^2 phi(r)), not a better asymptotic order. Binary ceilings in +EXPECTED.json concern these sufficient norm constants, not measured +condition numbers, execution speed, or full working precision. + +Radix two keeps its sharper geometric bound 2. The general theorem +applies to composite radices if a separate circle lower bound is proved; +it does not prove that missing nonvanishing premise. For products of +operators one may multiply the displayed constants. Independently +varying unit phases and unit diagonal conjugation preserve the required +power-norm property. No new weighted-stride solver is claimed. + +## 6. The inverse-gap power cannot be reduced in general + +The factor delta^{-1} is necessary even at fixed degree. For 0=1. +This establishes the necessary gap exponent, not optimality of the +quadratic degree factor in (1). + +## 7. Limits and relation to other work + +The reflection factorization is used for a proof, not an instruction to +find roots during execution. This package therefore supplies no new +factor-preparation, arithmetic, traffic, routing, scratch, or bit-cost +bound. PR628 and the concurrent PR764 concern rounded implementations; +this estimate has not been integrated into their error recurrences. It +does not imply their per-factor margins, dirty-restoration precision, +or their operation counts automatically improve. + +In particular the finite verifier cannot prove the analytic lemmas. It +checks exact polynomial/reflection identities, independent cyclic inverse +formulas, finite Hilbert inequalities, budget arithmetic, and specified +failure modes. The written argument supplies the all-frequency and +all-length reasoning. Independent human or proof-assistant review remains +open, as do the repository's full multiplication obligations. + +Classical references and repository pins are recorded in SOURCES.json +and NOTICE.md. The normalized arc-length inequality is explicitly +stated in Baranov-Zarouf, arXiv:1310.1182v1, Section 1.2.2, equation +(1.3), with attribution to Dolzhenko and Spijker. Hardy's coefficient +inequality and finite Blaschke reflection are standard; complete +nonoptimal arguments are included here to make constants reviewable. + +Prepared for Rafael Guevara (@alephnan) with substantial OpenAI Codex +assistance. Apache-2.0. diff --git a/research/rational-circle-bound/README.md b/research/rational-circle-bound/README.md new file mode 100644 index 0000000000..1703d4a2c4 --- /dev/null +++ b/research/rational-circle-bound/README.md @@ -0,0 +1,91 @@ +# Reflecting roots removes the extra inverse-gap power + +For a polynomial P of degree n with a certified unit-circle lower bound +delta>0, this note proves + +\[ +\|P(\tau Z_L^w)^{-1}\|_\infty\le(1+4n)^2/\delta +\] + +uniformly over length, stride, and unit phase. Interior roots are permitted. +Root reflection, the classical Dolzhenko-Spijker arc-length inequality, +and a self-contained Hardy coefficient estimate replace the derivative +bound used in our previous audit. The linear inverse-gap dependence is +necessary even at degree one; optimality of the degree factor is not claimed. + +Applied to Ali Romman's incorporated PR621, the dominant logarithmic term +in the sufficient norm bound is half the original and two thirds of our +previous bound. This remains O(r^2 phi(r)). It is not a faster algorithm, +a complete working-precision guarantee, or a new kappa. + +Exact ceilings of log2 of the sufficient norm constants illustrate the +change. These are bound sizes, not working precision or measured norms. + +| Radix | PR621 | Previous audit | This application | +|---:|---:|---:|---:| +| 3 | 28 | 21 | 19 | +| 9 | 870 | 651 | 441 | +| 25 | 23,997 | 17,992 | 11,999 | +| 71 | 695,757 | 521,801 | 347,859 | + +## Review and reproduce + +Read `PROOF.md`, then run from the repository root: + +```sh +python -B research/rational-circle-bound/verify.py +python -B research/rational-circle-bound/test_package.py +``` + +Python 3.10+ and only the standard library are required. Expected verifier +marker: `PASS_RATIONAL_CIRCLE_BOUND`. The default run checks immutable +source hashes, package hashes, and exact equality with `EXPECTED.json`. +An explicit `--emit NEW_PATH` writes a new receipt, refusing overwrites; +this mode checks source identity but skips package/expected comparison. + +The finite coverage is declared, not a proof of the analytic inequalities: + +- 126 exact rational root families, including mixed roots, multiplicity, + zero roots, and near-circle roots; 756 exact boundary identities. +- 546 independent dense versus finite-geometric cyclic inverse comparisons, + including zero and noncoprime strides; 9,516 inverse entries agree. +- 6,565 finite Hilbert-matrix inequalities, including all pairs of the + 81 length-four vectors in {0,1,2}^4. +- 128 exact near-circle parameter instances, with geometric-tail identities + and witnesses showing the inverse-gap power one is necessary. +- 14 exact prime-power budget comparisons and 21 admission/shortcut controls. + +See `VALIDATION.md` for the actual platform, package fault tests, and limits. +The cyclic oracle is the standard finite-geometric identity, also used by +Joshua Snider in PR692; it is not a new solver. + +## Scope and provenance + +This adds only `research/rational-circle-bound/`. The selected result, +upstream sources, and original algorithms are unchanged. Base: +`66849e1475c930fd7732b1a0067ffee7e1e95f60`. The local worktree starts from +an explicitly partial snapshot of pinned text inputs because a network +clone was unavailable. The final patch contains only new paths and can +be applied to a full checkout at that upstream base. +The publication commit uses the complete upstream tree and that upstream +commit as its parent. + +The package's `.gitattributes` preserves exact bytes across Git checkouts. +When applying the standalone patch on Windows, use +`git -c core.autocrlf=false apply /path/to/integer-mult-rational-circle-bound.patch` +to prevent conversion before those new attributes are installed. + +`SOURCES.json` pins six byte-exact source/context files and cites the +classical literature. The previous unpublished audit is included for +comparison; the new proof does not depend on that audit. `CLAIM.json` +records the alternative candidates and overlap review. + +This is a new application relative to the inspected repository work, not +a claim of mathematical priority. In particular PR628 and PR764 address +rounded scans. Their per-factor margins, precision recurrences, and paid +costs have not been improved merely by proving this operator bound. +Concurrent PR796 computes nonarchimedean root valuations; it does not +supply a complex conditioning bound and is distinct from this application. + +Prepared for Rafael Guevara (@alephnan) with substantial OpenAI Codex +assistance. Apache-2.0. See `NOTICE.md`. diff --git a/research/rational-circle-bound/SOURCES.json b/research/rational-circle-bound/SOURCES.json new file mode 100644 index 0000000000..5f5d339325 --- /dev/null +++ b/research/rational-circle-bound/SOURCES.json @@ -0,0 +1,109 @@ +{ + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "predecessor_pr": 621, + "predecessor_head": "520774462b19b29af41554b74def31f9d01e997e", + "files": [ + { + "local_path": "vendor/prime-power-proof.md", + "upstream_path": "research/prime-power-cyclic-inverse/PROOF.md", + "git_blob": "0c757c37c70fdeb261d73f111ceedd3b233287bf", + "sha256": "2b8056c88e66f692f407450fff0414d41bcd09db8597be22e274a6c3dc20eb9e", + "repository": "CrocSwap/integer-mult-bounds", + "commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60" + }, + { + "local_path": "vendor/prime-power-NOTICE.md", + "upstream_path": "research/prime-power-cyclic-inverse/NOTICE.md", + "git_blob": "a78e84066711e2f4776152d69d480e9629c26961", + "sha256": "96111c95cfec3c03a6f69c8e02c5d0bceff957d187e638d0534c676d6e3ffd77", + "repository": "CrocSwap/integer-mult-bounds", + "commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60" + }, + { + "local_path": "vendor/selected-result.json", + "upstream_path": "certificates/selected-result.json", + "git_blob": "92a10096dee76479af88a897714b3818d8263141", + "sha256": "b3bf402f31a69bde0629936a9b569bed48281568d7b16d5fba120b5311ea1f53", + "repository": "CrocSwap/integer-mult-bounds", + "commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60" + }, + { + "local_path": "LICENSE", + "upstream_path": "LICENSE", + "git_blob": "261eeb9e9f8b2b4b0d119366dda99c6fd7d35c64", + "sha256": "c71d239df91726fc519c6eb72d318ec65820627232b2f796219e87dcf35d0ab4", + "repository": "CrocSwap/integer-mult-bounds", + "commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60" + }, + { + "local_path": "vendor/previous-fourier-PROOF.md", + "upstream_path": "research/prime-power-fourier-bound/PROOF.md", + "repository": "local partial snapshot; unpublished patch", + "commit": "4c0004759b0ac8e2db1a1afd9fff690270786dfe", + "sha256": "0dd5ff1a4377f4eeb92b3af7b75254bb343c64675b09201db132b394b0ebaaad", + "git_blob": "4c189a7311d1be3851c32240809d39c8376ca0c5" + }, + { + "local_path": "vendor/previous-fourier-NOTICE.md", + "upstream_path": "research/prime-power-fourier-bound/NOTICE.md", + "repository": "local partial snapshot; unpublished patch", + "commit": "4c0004759b0ac8e2db1a1afd9fff690270786dfe", + "sha256": "05e6e660b74d34a8ed298f41889b9bb8b7fe365137bf2179f9828cdd2bb9a8b7", + "git_blob": "523638fa2c5eedfae3d92dff0633638adb673a8f" + } + ], + "scope": "Six byte-exact source texts and context/license inputs; no upstream implementation copied. Classical papers are cited, not distributed. Previous local audit is a comparison, not a needed premise.", + "classical_references": [ + { + "authors": "Anton Baranov and Rachid Zarouf", + "title": "A model space approach to some classical inequalities for rational functions", + "url": "https://arxiv.org/abs/1310.1182v1", + "locator": "Section 1.2.2, equation (1.3), and bibliography [D], [S]", + "use": "Confirms the normalized Dolzhenko-Spijker inequality and classical attribution. Not vendored. The note supplies its own projection proof." + }, + { + "authors": "Yuichi Kanjin and Kunio Sato", + "title": "Hardy\u2019s inequality for Jacobi expansions", + "year": 2004, + "url": "https://files.ele-math.com/articles/mia-07-56.pdf", + "locator": "Opening statement on page 551", + "use": "Confirms the classical Hardy coefficient inequality. Not vendored. The constant four is proved here by factorization and a Schur estimate." + }, + { + "authors": "M. N. Spijker", + "title": "On a conjecture by LeVeque and Trefethen related to the Kreiss matrix theorem", + "publication": "BIT 31 (1991), 551-555", + "use": "Historical attribution as cited by Baranov-Zarouf; original article not independently retrieved." + } + ], + "related_work": [ + { + "pr": 621, + "head": "520774462b19b29af41554b74def31f9d01e997e", + "relation": "Inherited polynomial, nonvanishing, and delta certificate; incorporated." + }, + { + "pr": 628, + "head": "0768f97d06c623b8211e651543c66135796b62bf", + "relation": "Rounded factor scans; no implementation or budget integration claimed." + }, + { + "pr": 764, + "head": "983d66f0f2e48ee500ec7eee2da9244c001c5064", + "relation": "Concurrent inverse-square scan-rounding bound; distinct mechanism." + }, + { + "pr": 692, + "relation": "Prior finite-geometric weighted-stride resolvent; that standard oracle formula is not new here." + }, + { + "pr": 666, + "relation": "Composite lifting; the present general theorem requires a separately proved circle gap." + }, + { + "pr": 736, + "head": "eccc3b74767848eb6746f39412d57df6c9544b5d", + "relation": "Finite elimination optimization, not an analytic norm bound." + } + ] +} diff --git a/research/rational-circle-bound/VALIDATION.md b/research/rational-circle-bound/VALIDATION.md new file mode 100644 index 0000000000..dae4717f68 --- /dev/null +++ b/research/rational-circle-bound/VALIDATION.md @@ -0,0 +1,81 @@ +# Validation and limits + +Executed on Windows 11 (10.0.26300), CPython 3.12.2, 2026-10-13 UTC. +The detailed interpreter/platform strings and command receipts are in +`evidence/environment.json`, `evidence/verify.txt`, and +`evidence/package-tests.txt`. Captured text logs are normalized to LF; +vendored source files are copied byte for byte and separately hashed. + +## Executed checks + +The normal verifier passed in 2.859 seconds on this session's machine. +This timing describes one evidence replay; it is not a benchmark of an +inversion algorithm or a claimed speedup. Its deterministic receipt is +`EXPECTED.json`. Counts there refer to one run, not sums across reruns. + +It checks 14 integer budget comparisons, 126 root/reflection families, +756 exact circle identities, 546 cyclic inverse matrices (9,516 inverse +entries), 6,565 finite Hilbert comparisons, 128 near-circle instances, +and 21 rejection/counterexample controls. All arithmetic is integer or +rational, including Gaussian-rational complex arithmetic. No numerical +root finder, floating-point quadrature, solver, or sampled circle minimum +is used as evidence of nonvanishing. +The cyclic matrices in these finite tests use the explicitly supplied +rational root families; they are not new exact inverses of PR621's +cyclotomic kernels. + +Eight package tests passed in 11.312 seconds including subprocess launch. +Each runs with `python -I -B -O` from an unrelated temporary directory: + +1. An intact offline copy under a path containing spaces passes. +2. Changed vendored proof bytes fail their pinned SHA-256, even after + updating that file's package checksum. +3. A changed pinned Git blob fails, even after updating the package checksum. +4. An unrecorded proof edit fails the package manifest. +5. A changed expected radix budget fails the recomputed evidence comparison, + even after updating the expected file's package checksum. +6. Removing conjugation from the reflection code fails a circle-modulus check. +7. Changing the closure denominator sign fails dense/geometric inverse agreement. +8. An attempt to overwrite existing evidence is rejected before any write. + +The code fault tests update the modified verifier's package checksum so +they reach the mathematical checks; hash rejection alone is not counted +as catching those mathematical faults. All checks use explicit exceptions +and remain active when Python assertions are optimized away. + +## Proof audit + +The written proof was reviewed locally for measure normalization, +both Fourier directions, degree versus number of distinct roots, boundary +zeros in the Hardy factorization, roots at zero, repeated and mixed roots, +the exceptional constant projection in the arc-length argument, and the +operator-series convergence hypothesis. This is author/AI review, not an +independent human assessment or proof-assistant certificate. + +Two analytic statements remain distinct from finite evidence: the +all-frequency coefficient inequalities proved in `PROOF.md`, and PR621's +inherited nonvanishing/circle estimate. The latter's unchanged expensive +foundation replay was not repeated. PR621's original notice and proof are +included with immutable pins. + +## Unexecuted and unclaimed + +No Linux/macOS or second-Python-version replay, remote CI, Lean proof, +full repository `make verify`, or selected-supplier cold replay is claimed. +The contribution changes no selected construction or existing implementation. +Source preparation, rounded execution, error propagation, scratch restoration, +traffic/routing, tape/compiler/hosting, and the all-size multiplication +transfer remain outside this result. No new kappa is reported. + +The local preparation branch is based on an explicitly partial snapshot +of exact upstream text inputs. The initial handoff was a focused patch +because clone/browser access was unavailable and no writable fork was +accessible. The user subsequently created `alephnan/integer-mult-bounds`. +Publication uses the GitHub API with the complete pinned upstream tree and +upstream commit as parent. GitHub main and the fork's main both matched +that base before publication. The handoff records clean patch application +and byte checks. +The initial fresh-repository application detected Windows CRLF conversion. +The package now supplies `.gitattributes` to preserve exact bytes; the handoff +also disables conversion for that one apply command. The final applied +artifact is compared byte for byte and replayed under optimized Python. diff --git a/research/rational-circle-bound/evidence/environment.json b/research/rational-circle-bound/evidence/environment.json new file mode 100644 index 0000000000..aa719def80 --- /dev/null +++ b/research/rational-circle-bound/evidence/environment.json @@ -0,0 +1,16 @@ +{ + "python": "3.12.2 (tags/v3.12.2:6abddd9, Feb 6 2024, 21:26:36) [MSC v.1937 64 bit (AMD64)]", + "platform": "Windows-11-10.0.26300-SP0", + "checks": [ + { + "script": "verify.py", + "exit_code": 0, + "seconds": 2.859 + }, + { + "script": "test_package.py", + "exit_code": 0, + "seconds": 11.312 + } + ] +} diff --git a/research/rational-circle-bound/evidence/package-tests.txt b/research/rational-circle-bound/evidence/package-tests.txt new file mode 100644 index 0000000000..91d21417c8 --- /dev/null +++ b/research/rational-circle-bound/evidence/package-tests.txt @@ -0,0 +1,9 @@ +PASS pristine relocated optimized +PASS source bytes drift +PASS wrong source Git blob +PASS unrecorded proof drift +PASS changed expected budget +PASS lost reflection conjugation +PASS wrong closure denominator sign +PASS refuse expected overwrite +{"count": 8, "seconds": 11.187, "status": "PASS_PACKAGE_CONTROLS", "tests": ["pristine relocated optimized", "source bytes drift", "wrong source Git blob", "unrecorded proof drift", "changed expected budget", "lost reflection conjugation", "wrong closure denominator sign", "refuse expected overwrite"]} diff --git a/research/rational-circle-bound/evidence/verify.txt b/research/rational-circle-bound/evidence/verify.txt new file mode 100644 index 0000000000..122f0785fa --- /dev/null +++ b/research/rational-circle-bound/evidence/verify.txt @@ -0,0 +1,2 @@ +PASS_RATIONAL_CIRCLE_BOUND +{"controls": 21, "cyclic_inverses": {"cases": 546, "inverse_entries": 9516, "nonzero_noncoprime_cases": 78, "zero_stride_cases": 195}, "hilbert": {"comparisons": 6565, "exhaustive_length": 4, "exhaustive_vectors_each_side": 81, "long_lengths": [8, 16, 32, 64]}, "near_circle_families": 128, "radix_budgets": 14, "reflection": {"all_inner": 33, "all_outer": 18, "boundary_points": 756, "contains_repetition": 37, "contains_zero": 32, "families": 126}} diff --git a/research/rational-circle-bound/test_package.py b/research/rational-circle-bound/test_package.py new file mode 100644 index 0000000000..6c5b8e4504 --- /dev/null +++ b/research/rational-circle-bound/test_package.py @@ -0,0 +1,106 @@ +#!/usr/bin/env python3 +"""Behavioral controls for a relocated offline research package.""" +from hashlib import sha256 +from pathlib import Path +import json +import subprocess +import sys +import tempfile +import time + +ROOT = Path(__file__).resolve().parent + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def rehash(root, name): + manifest = json.loads((root/'MANIFEST.json').read_text(encoding='utf-8')) + manifest['sha256'][name] = sha256((root/name).read_bytes()).hexdigest() + (root/'MANIFEST.json').write_text(json.dumps(manifest, indent=2)+'\n', encoding='utf-8') + + +def main(): + started = time.monotonic() + data = {str(p.relative_to(ROOT)): p.read_bytes() for p in ROOT.rglob('*') + if p.is_file() and '__pycache__' not in p.parts} + results = [] + # TemporaryDirectory owns its one verified absolute temporary root. + with tempfile.TemporaryDirectory(prefix='rational audit with spaces ') as td: + top = Path(td).resolve() + + def run(name, mutate=None, expected=None, extra=()): + root = (top/name).resolve() + need(top in root.parents, 'Test target escaped temporary root') + for path, value in data.items(): + target = root/path + target.parent.mkdir(parents=True, exist_ok=True) + target.write_bytes(value) + if mutate: + mutate(root) + result = subprocess.run([sys.executable, '-I', '-B', '-O', str(root/'verify.py'), *extra], + cwd=top, stdout=subprocess.PIPE, stderr=subprocess.STDOUT, + text=True, timeout=120) + if expected is None: + need(result.returncode == 0 and 'PASS_RATIONAL_CIRCLE_BOUND' in result.stdout, + name+' failed: '+result.stdout) + else: + need(result.returncode != 0 and expected in result.stdout, + name+' did not reject expected fault: '+result.stdout) + results.append(name) + print('PASS '+name, flush=True) + + run('pristine relocated optimized') + + def source_drift(root): + p = root/'vendor/prime-power-proof.md' + p.write_bytes(p.read_bytes()+b'\nChanged source\n') + rehash(root, 'vendor/prime-power-proof.md') + run('source bytes drift', source_drift, 'Source SHA-256 mismatch') + + def git_drift(root): + p = root/'SOURCES.json' + obj = json.loads(p.read_text(encoding='utf-8')) + obj['files'][0]['git_blob'] = '0'*40 + p.write_text(json.dumps(obj), encoding='utf-8') + rehash(root, 'SOURCES.json') + run('wrong source Git blob', git_drift, 'Source Git-blob mismatch') + + def proof_drift(root): + p = root/'PROOF.md' + p.write_bytes(p.read_bytes()+b'\nChanged proof\n') + run('unrecorded proof drift', proof_drift, 'Package hash mismatch: PROOF.md') + + def receipt_drift(root): + p = root/'EXPECTED.json' + obj = json.loads(p.read_text(encoding='utf-8')) + obj['budgets'][-1]['new_bits'] -= 1 + p.write_text(json.dumps(obj), encoding='utf-8') + rehash(root, 'EXPECTED.json') + run('changed expected budget', receipt_drift, 'Expected evidence mismatch') + + def mutate_code(old, new): + def mutate(root): + p = root/'verify.py' + code = p.read_text(encoding='utf-8') + need(code.count(old) == 1, 'Mutation anchor is not unique') + p.write_text(code.replace(old, new), encoding='utf-8') + rehash(root, 'verify.py') + return mutate + + run('lost reflection conjugation', + mutate_code('mirror = [ONE, -a.conj()]', 'mirror = [ONE, -a]'), + 'Circle modulus preservation') + run('wrong closure denominator sign', + mutate_code('denom = phase**length-root**length', 'denom = phase**length+root**length'), + 'Dense / geometric inverse disagreement') + run('refuse expected overwrite', expected='Refusing to overwrite evidence', + extra=('--emit', str(ROOT/'EXPECTED.json'))) + print(json.dumps({'status': 'PASS_PACKAGE_CONTROLS', 'tests': results, + 'count': len(results), 'seconds': round(time.monotonic()-started, 3)}, sort_keys=True)) + + +if __name__ == '__main__': + main() diff --git a/research/rational-circle-bound/vendor/previous-fourier-NOTICE.md b/research/rational-circle-bound/vendor/previous-fourier-NOTICE.md new file mode 100644 index 0000000000..523638fa2c --- /dev/null +++ b/research/rational-circle-bound/vendor/previous-fourier-NOTICE.md @@ -0,0 +1,34 @@ +# Attribution and scope of reuse + +Prepared for **Rafael Guevara (@alephnan)** with substantial **OpenAI Codex +assistance** in research selection, mathematical derivation, source review, +coding, finite verification, and writing. No independent human review or +proof-assistant formalization is claimed. No sub-agents were used. + +The direct mathematical predecessor is **Ali Romman's PR #621**, +"Prove uniform prime-power cyclic inverse bounds", incorporated into +CrocSwap/integer-mult-bounds. Its nonvanishing argument, resultant/cofactor +circle estimate, derivative estimate, cyclic-operator context, and original +Fourier transfer are retained. The original proof and attribution notice +are copied byte for byte under `vendor/`, with source and hash pins in +SOURCES.json. Their substantial OpenAI Codex assistance remains disclosed +in the original notice. The weighted Cauchy-Schwarz method is standard; +this contribution applies it to the predecessor's explicit constants. + +The underlying kernel comes from the OpenAI exact-DFT preprint at commit +`adc7f1241b42e322a6451854ab7e4b4c146bf78a`, source anchors `loc:newton` +and `loc:fourier-factorization`. The Newton/q-Pochhammer factorization is +classical; the predecessor credits Alexey Kuznetsov's "Using q-calculus +to study LDLT factorization of a certain Vandermonde matrix". We do not +claim to have independently reviewed those external sources or to have +proved a new kernel definition. + +The selected-result snapshot retains the reviewed #626/#543 source and +full contributor lineage. No new supplier or selected exponent is claimed. +Nearby contributions #628, #663, #666, #668, and #692 are acknowledged +for their distinct rounded-inverse, restoration, composite, resultant, +and stride investigations. Their code is not a dependency of this package. + +All new code and text are contributed under the repository's Apache-2.0 +license. The unchanged upstream LICENSE is included. No literature-priority +claim is made. diff --git a/research/rational-circle-bound/vendor/previous-fourier-PROOF.md b/research/rational-circle-bound/vendor/previous-fourier-PROOF.md new file mode 100644 index 0000000000..4c189a7311 --- /dev/null +++ b/research/rational-circle-bound/vendor/previous-fourier-PROOF.md @@ -0,0 +1,172 @@ +# A smaller Fourier-to-operator bound for the prime-power kernels + +## Statement and inherited premises + +This note audits the quantitative Fourier step in Ali Romman's incorporated +PR #621. The old estimate is valid. A standard weighted Cauchy-Schwarz +argument makes it substantially smaller without changing the polynomial, +the nonvanishing theorem, or the circle lower bound. No literature-priority +claim, paid algorithm, or new multiplication exponent is made. + +Retain the notation and proved circle bound of the pinned predecessor: + +\[ +r=\ell^a\ge3,\quad n=r-1,\quad D=\varphi(r),\quad H=2^r-1, +\qquad \delta=(2rnH^{nD-1})^{-1}. +\] + +Here \(\ell\) is prime, the kernel uses any primitive \(r\)-th root, and +\(P(z)=\sum_{j=0}^{r-1}z^j/\prod_{s=1}^j(1-u^s)\). +The predecessor establishes \(|P(z)|\ge\delta\) on \(|z|=1\) and +\(|P'(z)|\le M=nH/r\) there. These are inherited inputs, not conclusions +of the finite checks in this package. Put + +\[ +A=\delta^{-1},\qquad X=nH^{nD/2}. +\] + +For every cyclic length \(L\ge1\), integer stride \(w\), and scalar +\(|\tau|=1\), the following exact integer is an upper bound: + +\[ +\boxed{\ \|P(\tau Z_L^w)^{-1}\|_\infty + \le C_{\rm new}=A(1+4X).\ } +\] + +The old bound is exactly \(C_{\rm old}=A(1+4X^2)\). Thus this is a strict +improvement for every admitted \(r\ge3\). Both bounds remain uniform in +length, stride, and scalar phase. This is an analytic norm estimate, not +a count of arithmetic operations or a guarantee of rounded execution. + +## Weighted Fourier lemma + +Use normalized Lebesgue measure on \([0,2\pi]\). Let \(g\) be continuously +differentiable and periodic, with Fourier coefficients \(c_k\). Suppose +\(\|g\|_2\le A\) and \(\|g'\|_2\le B\), where \(A>0\), \(B>0\). +For every real \(t>0\), + +\[ +\sum_{k\in\mathbb Z}|c_k| + \le\sqrt{(1+4t)(A^2+B^2/t^2)}. +\tag{1} +\] + +To prove this without assuming absolute convergence in advance, first +apply Cauchy-Schwarz to the finite sum over \(-N\le k\le N\), with +weights \(1+k^2/t^2\). Parseval for \(g\) and \(g'\) bounds its first +factor squared by \(A^2+B^2/t^2\). For the second factor, the function +\(f(x)=(1+x^2/t^2)^{-1}\) decreases on the nonnegative half-line, so + +\[ +\sum_{k\in\mathbb Z}(1+k^2/t^2)^{-1} +\le1+2\int_0^\infty f(x)\,dx\le1+4t. +\] + +The last inequality follows by bounding the integral on \([0,t]\) by +\(t\), and on \([t,\infty)\) by +\(t^2\int_t^\infty x^{-2}\,dx=t\). Both signs of the frequency are +charged. Letting \(N\) increase proves (1), including absolute convergence. +This is a standard Fourier/Sobolev estimate, proved here for completeness. + +Choosing \(t=B/A\) gives + +\[ +\sum_k|c_k|\le A\sqrt{2+8B/A}. +\tag{2} +\] + +If \(B=0\), Parseval makes every nonzero-frequency coefficient zero and +the bound is simply \(\sum|c_k|\le A\). Equation (2) is only used with +positive \(B\). It is not claimed to improve the old bound for every +possible ratio \(B/A\); the prime-power specialization below does. + +## Specialization and exact comparison + +Set \(g(\theta)=1/P(e^{i\theta})\). Nonvanishing makes \(g\) smooth, and +the pointwise estimates give the normalized \(L^2\) bounds + +\[ +\|g\|_2\le A=\delta^{-1},\qquad +\|g'\|_2\le B=M\delta^{-2}. +\] + +Then + +\[ +t=B/A=M/\delta=2n^2H^{nD}=2X^2. +\] + +For every integer \(r>2\), \(\varphi(r)\) is even: pair each unit modulo +\(r\) with its distinct negative. Hence \(nD/2\) is an integer and +\(X\) is an integer, at least two in the present domain. Equation (2) +and the exact identity + +\[ +(1+4X)^2-(2+16X^2)=8X-1>0 +\] + +give \(\sum|c_k|\le A(1+4X)\). The old expression rewrites as + +\[ +\delta^{-1}+2M\delta^{-2}=A(1+2t)=A(1+4X^2). +\] + +Thus \(C_{\rm old}-C_{\rm new}=4AX(X-1)>0\). All quantities in this +comparison are exact integers. No logarithm or floating-point rounding +is needed to certify the comparison or the reported binary ceilings. + +## Transfer to an operator + +Write \(U=\tau Z_L^w\). Every integer power of \(U\), including negative +powers and non-coprime or zero strides, has induced infinity norm one. +Consequently \(\sum_k c_kU^k\) converges absolutely in that matrix norm. +The absolutely convergent Fourier series equals \(g\): it has the same +Fourier coefficients and both functions are continuous. Multiplying the +series by the finite polynomial \(P\) gives the constant one. Substitution +of \(U\), justified by absolute convergence and the finite product, yields + +\[ +P(U)\sum_kc_kU^k=\sum_kc_kU^kP(U)=I. +\] + +The series is therefore the inverse and its norm is at most \(\sum|c_k|\). +This proves the statement for all \(L,w,\tau\); there is no assumption +that the eigenvalues of \(U\) are distinct. Finite products are bounded +by the product of these constants. Unit diagonal conjugation preserves +the induced infinity norm, as in #621. The radix-two special bound of +two remains separate and unchanged. + +The spectral bound \(\sup_{|z|=1}|P(z)^{-1}|\) alone is insufficient +for the induced infinity norm. An exact counterexample is + +\[ +P(z)=1+z/2+z^2/2,\qquad +|P(e^{i\theta})|^2=2(\cos\theta+3/8)^2+7/32. +\] + +The valid rational lower bound \(\delta=7/15\) would give +\(\delta^{-1}=15/7\). But for the three-cycle, +\(P(Z_3)^{-1}=(3I-Z_3-Z_3^2)/2\), with row sum \(5/2>15/7\). +This rejects a deliberately invalid shortcut; it is not a counterexample +to #621 or to the weighted estimate. + +## What improves, and what does not + +The leading powers of \(H\) in the explicit bounds change from +\(2nD-1\) to \(3nD/2-1\). The dominant term in the logarithm of this +particular norm overestimate is therefore reduced by one quarter as +\(r\) grows. Both estimates still have logarithm \(O(r^2\varphi(r))\). +The integer bit ceilings in EXPECTED.json describe these constants only; +they are not sufficient working precisions for a complete algorithm. + +The finite verification checks exact budget arithmetic, the implementation +of (1) on a declared finite family, and the counterexample. It is not a +formal proof of the Fourier lemma or the multiplication theorem. The +written argument above supplies the all-frequency/all-length reasoning. +Kernel nonvanishing and its circle lower bound remain inherited from +#621. Preparation, rounding, error propagation, dirty restoration, +routing, compiler, tape, hosting, and multiplication transfer are not +discharged, and no new kappa, complex saving, or BIT saving follows. + +Prepared for Rafael Guevara (@alephnan) with substantial OpenAI Codex +assistance. Apache-2.0. See NOTICE.md for predecessor attribution. diff --git a/research/rational-circle-bound/vendor/prime-power-NOTICE.md b/research/rational-circle-bound/vendor/prime-power-NOTICE.md new file mode 100644 index 0000000000..a78e840667 --- /dev/null +++ b/research/rational-circle-bound/vendor/prime-power-NOTICE.md @@ -0,0 +1,21 @@ +# Attribution and assistance + +The kernel definition comes from the OpenAI exact-DFT preprint at +`adc7f1241b42e322a6451854ab7e4b4c146bf78a`, at `loc:newton` and +`loc:fourier-factorization`. Its source has the Apache-2.0 license. +The Newton and q-Pochhammer Fourier factorization is classical; see +Alexey Kuznetsov, [Using q-calculus to study LDLT factorization of a +certain Vandermonde matrix](https://arxiv.org/abs/1507.02959v2). +This source is not presented as a proof of the cyclic conditioning result. + +The proof extends prior unpublished local cyclic inverse and stability +notes from research directed by Ali Romman. The rational field routines +use that work's exact-arithmetic scaffold. The full proof is included +here; no private file is needed for replay. No literature priority is claimed. + +The proof, verifier, and package were prepared with substantial OpenAI +Codex assistance. Separate Codex agents reviewed the proof and checked +it with independent SymPy arithmetic. These are AI-assisted reviews, +not maintainer acceptance or a full Lean multiplication proof. + +This contribution uses the repository's Apache-2.0 license. diff --git a/research/rational-circle-bound/vendor/prime-power-proof.md b/research/rational-circle-bound/vendor/prime-power-proof.md new file mode 100644 index 0000000000..0c757c37c7 --- /dev/null +++ b/research/rational-circle-bound/vendor/prime-power-proof.md @@ -0,0 +1,212 @@ +# Uniform bounds for the prime-power cyclic inverse + +## Result and scope + +Let r=ell^a>=3, where ell is prime and a>=1. Let u be a primitive +r-th root of unity, and put n=r-1 and D=phi(r). Define + + h_j = 1 / product_(s=1)^j (1-u^s), + P(z) = sum_(j=0)^n h_j z^j, + f(z) = r P(z). + +For every such r and u, P has no zero on the complex unit circle. +Put H=2^r-1 and delta_r=1/(2rn H^(nD-1)). For every complex +z with |z|=1, + + |P(z)| >= delta_r. + +This bound does not depend on the order of z. In particular, it holds +at all eigenvalues of a cyclic shift of any length. The old bound from +the algebraic norm of P at a root of unity depends on that root's order. +The new bound removes that dependence. + +There is also an operator bound that does not require root +classification. For any complex scalar tau with |tau|=1, +any cyclic shift Z_L with L>=1, and any integer w, put U=tau Z_L^w. Then + + ||P(U)^-1||_infinity <= delta_r^-1 + 2nH/(r delta_r^2). + +The bound has logarithm O(r^2 phi(r)), hence O(r^3). It is uniform +in L, w, and tau. The induced infinity norm is the maximum absolute +row sum. This bound does not supply a complete O(p polylog p) guard +for growing radix families. Efficient coefficient preparation, rounded +execution, scratch restoration, and a fast fixed-tape circuit remain open. No integer +kappa, complex b, or BIT c changes in this result. + +For an odd prime q, D=n=q-1, so the circle bound becomes + + delta_q = 1/(2q(q-1) (2^q-1)^((q-1)^2-1)). + +The result includes dyadic r>=4. For r=2, P(z)=1+z/2; the geometric +series gives ||P(U)^-1||_infinity<=2. No result for other composite +radices is claimed. The ideal argument below requires a prime power. + +## Integral polynomial and unit roots + +The identity product_(s=1)^(r-1)(1-u^s)=r gives + + f(z) = sum_(j=0)^n a_j z^j, + a_j = product_(s=j+1)^n (1-u^s). + +All a_j are algebraic integers in K=Q(u), and a_n=1. Thus f is +monic. Every root of f is an algebraic integer. + +Take any root alpha and a number field E that contains K and alpha. +The algebraic integer 1-u is not a unit in E, since + + |Norm_(E/Q)(1-u)| = ell^[E:K] > 1. + +Here Norm_(K/Q)(1-u)=Phi_r(1)=ell. The prime-power cyclotomic +polynomial is Phi_r(x)=sum_(j=0)^(ell-1) x^(j r/ell). + +There is a maximal ideal m in the ring of integers of E that contains +1-u. Modulo m, all a_j with j=3, the two embeddings are distinct. Bound the other +D-2 factors by H^(2n). This gives + + 1 <= |Norm_(K/Q)(R)| <= |R|^2 H^(2n(D-2)), + |R| >= H^(-n(D-2)). + +The equation S adj(S) e_0 = R e_0 gives polynomials A and C of +degree below n with + + A(z) f(z) + C(z) f*(z) = R. + +Each coefficient of A and C is a cofactor of S. A cofactor is a +determinant of size 2n-1. Deleting a row and a column cannot +increase the Euclidean norm of any retained column. Therefore each +cofactor has modulus at most H^(2n-1). For |z|=1, + + |A(z)| + |C(z)| <= 2n H^(2n-1), + |f*(z)| = |f(z)|. + +The Bezout identity gives + + |f(z)| >= H^(-n(D-2)) / (2n H^(2n-1)) + = 1 / (2n H^(nD-1)). + +Divide by r to obtain the stated bound for P. Neither this proof +nor its constants use the degree of a root of unity at which P is +evaluated. + +## An inverse bound from Fourier coefficients + +Let g(t)=1/P(exp(it)). The circle bound gives |g(t)|<=delta_r^-1. +The coefficient bound gives + + |P'(exp(it))| <= nH/r, + |g'(t)| <= nH/(r delta_r^2). + +Let c_k be the Fourier coefficients of g, with the average integral +on [0,2 pi] as the normalization. Parseval's identity for g' gives + + sum_k k^2 |c_k|^2 <= (nH/(r delta_r^2))^2. + +The estimate sum_(k!=0) k^-2 <= 4 follows from comparison of the +positive tail with the integral of x^-2 on [1,infinity). By the +Cauchy-Schwarz inequality and |c_0|<=delta_r^-1, + + sum_k |c_k| <= delta_r^-1 + 2nH/(r delta_r^2). + +Thus the Fourier series is absolutely convergent. Its product with +the finite polynomial P(exp(it)) has Fourier coefficients equal to +those of the constant one. For U=tau Z_L^w, every integer power U^k +has infinity norm one. The absolutely convergent matrix series + + sum_(k in Z) c_k U^k + +therefore has norm at most sum_k |c_k|. Multiplication by P(U) gives +the identity matrix, by the same coefficient identities. This proves +the stated inverse bound for all L, w, and unit tau. + +This is a bound for the exact operator. It is not a paid +coefficient-preparation or rounded-program theorem. The infinite +series is used to prove the norm bound, not as a declared algorithm. + +## Products and unit gauges + +For a finite family of such kernels with r_i>=3 on the same cyclic array, put + + C = product_i P_i(tau_i Z_L^(w_i)). + +Each factor is invertible. Submultiplicativity gives + + ||C^-1||_infinity <= product_i [delta_i^-1 + 2n_i H_i/(r_i delta_i^2)]. + +A diagonal conjugation with entries of modulus one preserves this +norm. Thus this bound also applies to a unit-gauged product. Its +logarithm is O(sum_i r_i^2 phi(r_i)). The bound concerns arbitrary +input vectors. It does not give operation counts or a tape schedule. + +## Value, sources, and remaining work + +This result permits inner roots and proves a uniform circle bound for +every primitive root choice. It supplies an explicit all-length inverse +bound for each growing prime-power radix. For an odd prime q and a root of unity xi, a direct algebraic norm +argument in E=Q(u,xi) gives + + |P_q(xi)| >= q^-1 (2^q-1)^(-([E:Q]-1)). + +The degree of E can grow with the order of xi. The new bound uses +Q(u) only and controls every point on the unit circle. The logarithm +of its inverse upper bound still grows polynomially with r. It does +not establish the required combined precision guard or change the +full-array traffic of the literal filter chain. A sharper lower bound +and a paid implementation remain useful next questions. + +The polynomial is from the pinned OpenAI exact-DFT preprint: + +https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/An-explicit-power-saving-for-the-exact-discrete-Fourier-transform-September-25-2026/build/sections/local.tex + +The unit-ideal argument extends the prior unpublished local note +"Cyclic polynomial stability, norm growth, and rescaling". The prior +local note "Full-output cyclic quotient: exact structure and cost" +supplies the cyclic inverse context. The field arithmetic in the +finite verifier uses the prior local exact-arithmetic scaffold. +The resultant and cofactor estimates use standard algebraic and +linear-algebra facts. Repository and literature novelty checks are +separate from this proof. No priority claim is made here. + +Prepared with OpenAI Codex assistance. Apache-2.0. diff --git a/research/rational-circle-bound/vendor/selected-result.json b/research/rational-circle-bound/vendor/selected-result.json new file mode 100644 index 0000000000..92a10096de --- /dev/null +++ b/research/rational-circle-bound/vendor/selected-result.json @@ -0,0 +1,123 @@ +{ + "status": "Maintainer-reviewed conditional finite construction; see the integration receipt for publication and PR resolution status", + "kappa": "51110230636731/31250000000000000", + "decimal": "0.001635527380375392", + "source_prs": [ + 626, + 623, + 622, + 620, + 617, + 615, + 604, + 601, + 596, + 592, + 591, + 593, + 599, + 588, + 543, + 584, + 586, + 583, + 582, + 579, + 576, + 575, + 574, + 571, + 569, + 568, + 567, + 564, + 562, + 561, + 559, + 558, + 552, + 550, + 548, + 541, + 535, + 510, + 503, + 531, + 523, + 493, + 514, + 507, + 484, + 496, + 505, + 522, + 520, + 472, + 458, + 445, + 442, + 425, + 433, + 370, + 361, + 315 + ], + "source_manifest": "research/community-k492-audit/SELECTED-SOURCE.json", + "certificate": "research/community-k492-audit/pr626/replay/ASSEMBLY.json", + "certificate_sha256": "6127732e2fcdd470dab349c1c51d03cd9f0787ad0309b1b4a7c811a908028f4e", + "proof": "docs/research/community-k492-review.md", + "proof_supplements": { + "research/e8-bit-r420/README.md": "9807be57c6adf26b30e4f54e2f8160075bbc05091f1a6d157e43d2a4620c1c9f", + "research/complex-571-free4fc8/NOTICE.md": "a4c084abdc1c7a9ac683eeb11124335d51cff8a6deba6ee92ba5a12bceaa2c97", + "research/complex-multicold/proof/CONSTRUCTION.md": "27ece5e1c11b90d97a808b56eff897b998c10e61016db95867f84e6e6aef132f", + "research/complex-multicold/vendor/pr559/PROOF.md": "d5d498edc56fdef8c5798af7f5ec66948bd2f66c553b9efe366cdaab01bd3453", + "research/structural-gain/frontier-composition/README.md": "70f0f791cbe3b2603f85d85bb9055aa0ee1df6dc06ba82fc1921356948312887", + "research/complex-joint-prefix/proof/CONSTRUCTION.md": "a92e610e7a598d99c612d1b63d1a03a49c0cd1e15ddd29fa55c465ddd8c18105", + "research/kernel-frame-coalescing/PROOF.md": "fa8b2f36b9590ee80ff45d3f7724f8c7de8ad29a29f366d5133010c77e41fe1b", + "research/complex-571-hpeq5/README.md": "4000b37f6c07c09d971dc4010ceb137c13340f3a8809d3272046ccaf746c3e2b", + "research/hyperplane-end-lean/PROOF.md": "1cbce5cf0ff0152f71e8ae7bef25841d1ce13010af248ff7209182d2328c21c9", + "docs/research/community-hyperplane599-review.md": "3298cd0d451541508af232cac72efbd7c10580e6c6ad493a855ab0faa01ade8c", + "research/complex-571-cold14-b3/README.md": "1945785785c153c7d0e8d4c071adabe626c1091b71721ff85d2d67191b376b96", + "research/complex-571-cold14-b3/PROOF-NOTE.md": "1cf592cbc8ab8e21d2dd8c1e945a5c64c6d5cde1216fb06e05a36c1c6ec6613d", + "scripts/verify_cold617_interface.py": "95d7a9094c05ad975fb72f5ab7605593003245a503c8456764987e512028fa6a", + "docs/research/community-cold617-review.md": "b3f2bcbae1249f1f651032022ce1e6e2bfb3f563ce580bf53671f50a074d7046", + "research/complex-k492-owner-repair/README.md": "ee5a1ace4828f7a073be97e95c2d931988774dd3a29a877e65abdf429aeec902", + "research/complex-k492-owner-repair/PROOF-NOTE.md": "337d70fe7abd9afca1d90954c23bde87f4dc27888cc1a6b4bb80506fd6fbf8c5", + "research/complex-k492-owner-repair/PROOF-NOTE-R.md": "22312bb347bdf159e6a01a45c47675e6170d33b258e2fd9ed52aee88fb92c0ed", + "docs/research/community-k492-review.md": "3b731d30e80010b15408a289b0b32192700885474c8b36d48ee3320a7a8c5c47", + "scripts/verify_frontier626.py": "2207bd0ef04a19ef276869085afdedad80a0938fa75db5e1aa7ab73fd3429444", + "scripts/verify_frontier626_bindings.py": "cda63ff41c6d6e2e352c7bf75b84e690c0ce57e4ec6c0355573bb5d9b1f98280", + "scripts/verify_frontier588_bindings.py": "6d1932eea7b1936598118ea8e607b09c29b6e31b749ec41bbe0744ea4f0b606d", + "scripts/verify_hpe_lean_binding.py": "52aa1d23641e4c716b43c98f6b883ad042087dd03a9d01369e8e6a735b07aa03", + "research/hyperplane-end-lean/HyperplaneEnd/Exact.lean": "eebf3a3982af7ab9be45777b272a6aaa523206fa7667ceb6df63ad6589fd8183" + }, + "review": "docs/research/community-k492-review.md", + "validation": "docs/research/community-k492-integration.json", + "reproduce": "make frontier626-verify", + "scope": "Finite scalar, frame, phase, whole-owner, invoice and exact assembly checks. All-size/compiler/common-label/mutable-basis/pooled-cell hosting/residual/precision/tape/analytic assumptions remain. This is not a full Lean multiplication theorem. See review for replay reuse and Linux CI status.", + "previous_kappa": "817591864627889/500000000000000000", + "previous_record": "certificates/checkpoints/cold617.json", + "audited_source_head": "660de893d27bb7abd1d5b01b1640207528a5c851", + "reviewed_dependency_heads": { + "588": "6d0e53b66c29abd17981881a09eaff41ac862d85", + "543": "2065fe4f72a914d907f1046603f5a36f17018535", + "568": "71c99ac935a33bb7b59a1b4a7af8725a939b0b90", + "569": "1424da81263a5305b35e4cf74ef686c275f03f3f", + "571": "b7bdc5a8de18fcf418cfb9c7d83a2b1097a5e4a3", + "575": "eac6f7e378ab622dac50a2fd4b7ef6eab014de44", + "583": "89be768f0157f5a3d8e4db69cf1748768605eac9", + "586": "4846fee5b06af770e9b3a10c36200f673d656725", + "591": "f622547244bf6d895a571a7b035142ba66279806", + "592": "1f471c445c06a45a32e2c47e8d74c8264b68356b", + "593": "fdb6dcc6d7bc29764c5b6b4d32b7fa050acf74a4", + "596": "7732dd5e46863ff294b5e443661cb9d99abf4e01", + "599": "bc13c8a3e000442606bd2dbe8583a17649ba6c32", + "601": "529ab7dcb59d5ea7a5798e9e06cf5b3aee8a1550", + "604": "1b795c5d7dea746ba310572585c0ef067574b4a6", + "615": "bf8a49a34350599763cced8592db81dc62c2c1c0", + "617": "904d62855723c00f8acef9a287a10768598fdeb2", + "622": "f69477f4f6d3c7eb1f740b166881bffed4ffa9f6", + "623": "e39a615ca601ce5d62abeb24f3fcdb8644ca1005", + "626": "660de893d27bb7abd1d5b01b1640207528a5c851" + } +} diff --git a/research/rational-circle-bound/verify.py b/research/rational-circle-bound/verify.py new file mode 100644 index 0000000000..be291eb113 --- /dev/null +++ b/research/rational-circle-bound/verify.py @@ -0,0 +1,474 @@ +#!/usr/bin/env python3 +"""Exact finite evidence for the rational-circle-bound note. + +Python 3.10+ standard library. The analytic proof is in PROOF.md. +All checks use explicit exceptions and remain enabled under python -O. +""" +from dataclasses import dataclass +from fractions import Fraction as F +from hashlib import sha1, sha256 +from itertools import product +from pathlib import Path +import argparse +import json + +ROOT = Path(__file__).resolve().parent +BASE = "66849e1475c930fd7732b1a0067ffee7e1e95f60" +RADICES = (3, 4, 5, 7, 8, 9, 11, 16, 25, 27, 32, 49, 64, 71) + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +@dataclass(frozen=True) +class C: + """Gaussian rational; no floating-point conversions.""" + re: F = F(0) + im: F = F(0) + + def __post_init__(self): + object.__setattr__(self, "re", F(self.re)) + object.__setattr__(self, "im", F(self.im)) + + @staticmethod + def of(x): + return x if isinstance(x, C) else C(x) + + def __add__(self, x): + x = C.of(x) + return C(self.re + x.re, self.im + x.im) + + __radd__ = __add__ + + def __neg__(self): + return C(-self.re, -self.im) + + def __sub__(self, x): + return self + (-C.of(x)) + + def __rsub__(self, x): + return C.of(x) - self + + def __mul__(self, x): + x = C.of(x) + return C(self.re*x.re - self.im*x.im, + self.re*x.im + self.im*x.re) + + __rmul__ = __mul__ + + def __truediv__(self, x): + x = C.of(x) + need(x.abs2() != 0, "Division by zero") + return self * C(x.re/x.abs2(), -x.im/x.abs2()) + + def __rtruediv__(self, x): + return C.of(x) / self + + def __pow__(self, n): + need(type(n) is int, "Integer power required") + if n < 0: + return (1/self)**(-n) + out, a = C(1), self + while n: + if n & 1: + out = out*a + a, n = a*a, n//2 + return out + + def conj(self): + return C(self.re, -self.im) + + def abs2(self): + return self.re**2 + self.im**2 + + def upper_abs(self): + return abs(self.re) + abs(self.im) + + +ZERO, ONE = C(), C(1) + + +def trim(p): + p = list(map(C.of, p)) + while len(p) > 1 and p[-1] == ZERO: + p.pop() + return p + + +def pmul(p, q): + a = [ZERO]*(len(p)+len(q)-1) + for j, x in enumerate(p): + for k, y in enumerate(q): + a[j+k] = a[j+k] + x*y + return trim(a) + + +def peval(p, z): + a = ZERO + for x in reversed(p): + a = a*z + x + return a + + +def reflected(roots, leading=ONE): + """Return P,Q,N,D,m with P=(N/D)*Q, using exact supplied roots.""" + leading = C.of(leading) + need(leading != ZERO, "Zero polynomial has no positive circle gap") + p, q, numer, denom, m = [leading], [leading], [ONE], [ONE], 0 + for a in roots: + need(a.abs2() != 1, "Root on unit circle") + factor = [-a, ONE] + p = pmul(p, factor) + if a.abs2() < 1: + mirror = [ONE, -a.conj()] + q, numer, denom = pmul(q, mirror), pmul(numer, factor), pmul(denom, mirror) + m += 1 + else: + q = pmul(q, factor) + return p, q, numer, denom, m + + +def ident(n): + return [[C(int(i == j)) for j in range(n)] for i in range(n)] + + +def madd(a, b): + return [[x+y for x, y in zip(ar, br)] for ar, br in zip(a, b)] + + +def mscale(a, c): + return [[x*c for x in row] for row in a] + + +def mmul(a, b): + n = len(a) + out = [[ZERO]*n for _ in range(n)] + for i in range(n): + for k in range(n): + if a[i][k] != ZERO: + for j in range(n): + if b[k][j] != ZERO: + out[i][j] = out[i][j] + a[i][k]*b[k][j] + return out + + +def inverse(a): + """Gauss-Jordan oracle, separate from the geometric inverse formula.""" + n = len(a) + aug = [row[:] + unit for row, unit in zip(a, ident(n))] + for j in range(n): + pivot = next((i for i in range(j, n) if aug[i][j] != ZERO), None) + need(pivot is not None, "Singular matrix") + aug[j], aug[pivot] = aug[pivot], aug[j] + v = aug[j][j] + aug[j] = [x/v for x in aug[j]] + for i in range(n): + if i != j and aug[i][j] != ZERO: + c = aug[i][j] + aug[i] = [x-c*y for x, y in zip(aug[i], aug[j])] + need([row[:n] for row in aug] == ident(n), "Elimination residual") + return [row[n:] for row in aug] + + +def cyclic(n, stride, phase): + need(type(n) is int and n >= 1, "Positive cyclic length required") + need(phase.abs2() == 1, "Unit phase required") + a = [[ZERO]*n for _ in range(n)] + for i in range(n): + a[i][(i-stride) % n] = phase + return a + + +def mpowers(a, count): + p = [ident(len(a))] + for _ in range(count): + p.append(mmul(p[-1], a)) + return p + + +def polynomial_matrix(p, powers): + out = [[ZERO]*len(powers[0]) for _ in powers[0]] + for c, a in zip(p, powers): + out = madd(out, mscale(a, c)) + return out + + +def geometric_inverse(root, phase, powers): + """(U-aI)^-1 using U^L=phase^L I, valid also for noncoprime strides.""" + length = len(powers[0]) + denom = phase**length-root**length + need(denom != ZERO, "Singular geometric closure") + out = [[ZERO]*length for _ in range(length)] + for j in range(length): + out = madd(out, mscale(powers[j], root**(length-1-j)/denom)) + return out + + +def prime_power(r): + need(type(r) is int and r >= 3, "Inherited budget requires integer r>=3") + p = next(d for d in range(2, r+1) if r % d == 0) + rest, exponent = r, 0 + while rest % p == 0: + rest //= p + exponent += 1 + need(rest == 1, "Inherited circle budget only admits prime powers") + return p, exponent + + +def ceil_log2(x): + need(type(x) is int and x > 0, "Positive integer budget required") + return (x-1).bit_length() + + +def budget(r): + p, exponent = prime_power(r) + n, d, h = r-1, r-r//p, 2**r-1 + need(d % 2 == 0, "Totient parity") + a = 2*r*n*h**(n*d-1) + x = n*h**(n*d//2) + old = a + 2*F(n*h, r)*a*a + need(old.denominator == 1, "Old bound integrality") + old, previous, new = int(old), a*(1+4*x), a*(1+4*n)**2 + need(old == a*(1+4*x*x), "Original formula mismatch") + need(h >= 2*n+1 and h**(n*d//2) > 4*n+2, "Universal comparison witness") + need(new < previous < old, "Strict bound comparison") + bits = [ceil_log2(v) for v in (old, previous, new)] + for value, b in zip((old, previous, new), bits): + need(2**(b-1) < value <= 2**b, "Binary ceiling enclosure") + return {"r": r, "prime": p, "prime_exponent": exponent, + "n": n, "D": d, "old_bits": bits[0], "previous_bits": bits[1], + "new_bits": bits[2], "saved_vs_previous": bits[1]-bits[2], + "saved_vs_original": bits[0]-bits[2]} + + +PHASES = (ONE, C(0, 1), C(F(3, 5), F(4, 5))) +POINTS = PHASES + (-ONE, C(0, -1), C(F(5, 13), F(12, 13))) +ATOMS = (ZERO, C(F(1, 2)), C(F(-1, 2)), C(2), C(-2), + C(F(3, 10), F(2, 5)), C(F(6, 5), F(8, 5)), + C(F(31, 32)), C(F(33, 32))) + + +def families(): + out = [(), (ZERO,), (ZERO, ZERO), (C(F(1, 2)),), (C(2),), + (C(F(1, 2)), C(2)), (C(F(1, 2)),)*3, (C(2),)*3, + (C(F(31, 32)), C(F(33, 32))), + (C(F(3, 10), F(2, 5)), C(F(6, 5), F(8, 5))), + (ZERO, C(-2), C(F(1, 2))), + (C(F(-1, 2)), C(2), C(F(3, 10), F(2, 5))), + (ZERO, ZERO, C(F(1, 2)), C(2))] + out.extend(tuple(a) for a in product(ATOMS, repeat=2)) + # A declared deterministic family, not an open-ended randomized search. + for i in range(32): + out.append(tuple(ATOMS[(i*7+j*j+3*j) % len(ATOMS)] for j in range(3+i % 4))) + return out + + +def reflection_checks(): + cases, point_checks, inner, outer, zero, repeated = 0, 0, 0, 0, 0, 0 + for roots in families(): + p, q, num, den, m = reflected(roots) + need(len(p)-1 == len(roots), "Multiplicity/degree mismatch") + need(pmul(p, den) == pmul(num, q), "Reflection identity P*D=N*Q") + need(len(q)-1 <= len(roots), "Reflected degree bound") + need(m == sum(a.abs2() < 1 for a in roots), "Inner multiplicity count") + for a in roots: + if 0 < a.abs2() < 1: + need((1/a.conj()).abs2() > 1, "Reflected pole outside disk") + for z in POINTS: + pv, qv, nv, dv = (peval(f, z) for f in (p, q, num, den)) + need(dv != ZERO and qv != ZERO, "Unexpected boundary zero") + need(pv.abs2() == qv.abs2(), "Circle modulus preservation") + need(nv.abs2() == dv.abs2(), "Blaschke modulus one") + need(1/pv == (nv/dv).conj()/qv, "Conjugate reciprocal identity") + point_checks += 1 + cases += 1 + inner += int(m == len(roots) and bool(roots)) + outer += int(m == 0 and bool(roots)) + zero += int(ZERO in roots) + repeated += int(len(set(roots)) < len(roots)) + return {"families": cases, "boundary_points": point_checks, + "all_inner": inner, "all_outer": outer, "contains_zero": zero, + "contains_repetition": repeated} + + +def cycle_checks(): + cases, entry_comparisons, zero_stride, noncoprime = 0, 0, 0, 0 + chosen = families()[:13] + for roots in chosen: + p, q, num, den, m = reflected(roots) + for length in (1, 2, 3, 4, 6): + for stride in sorted({-1 % length, 0, 1 % length, 2 % length}): + for phase in PHASES: + u = cyclic(length, stride, phase) + powers = mpowers(u, max(length, len(p))) + need(powers[length] == mscale(ident(length), phase**length), "Cyclic closure") + matrix = polynomial_matrix(p, powers) + exact = inverse(matrix) + factored = ident(length) + for a in roots: + factored = mmul(factored, geometric_inverse(a, phase, powers)) + need(exact == factored, "Dense / geometric inverse disagreement") + need(mmul(matrix, factored) == ident(length), "Left inverse residual") + need(mmul(factored, matrix) == ident(length), "Right inverse residual") + # Direct coefficient evaluation using the entry map, independent of matrix powers. + direct = [[ZERO]*length for _ in range(length)] + for j, c in enumerate(p): + for row in range(length): + col = (row-j*stride) % length + direct[row][col] = direct[row][col] + c*phase**j + need(direct == matrix, "Polynomial matrix / entry-map disagreement") + cases += 1 + entry_comparisons += length*length + zero_stride += int(stride == 0) + from math import gcd + noncoprime += int(stride != 0 and gcd(stride, length) > 1) + return {"cases": cases, "inverse_entries": entry_comparisons, + "zero_stride_cases": zero_stride, "nonzero_noncoprime_cases": noncoprime} + + +def hilbert_checks(): + vectors = tuple(product((0, 1, 2), repeat=4)) + norms = {v: sum(x*x for x in v) for v in vectors} + kernel = [[F(1, j+k+1) for k in range(4)] for j in range(4)] + count = 0 + for a in vectors: + weighted = [sum((a[j]*kernel[j][k] for j in range(4)), F(0)) for k in range(4)] + for b in vectors: + lhs = sum((weighted[k]*b[k] for k in range(4)), F(0)) + need(lhs*lhs <= 16*norms[a]*norms[b], "Finite Hilbert inequality") + count += 1 + # More frequencies with exact rational coefficients; use squared comparisons. + for length in (8, 16, 32, 64): + a = [F(1, j+1) for j in range(length)] + b = [F(1, 2*j+1) for j in range(length)] + lhs = sum((a[j]*b[k]/(j+k+1) for j in range(length) for k in range(length)), F(0)) + need(lhs*lhs <= 16*sum(x*x for x in a)*sum(x*x for x in b), "Long Hilbert inequality") + count += 1 + return {"comparisons": count, "exhaustive_vectors_each_side": len(vectors), + "exhaustive_length": 4, "long_lengths": [8, 16, 32, 64]} + + +def near_circle_checks(): + for k in range(1, 129): + eps = F(1, 2**k) + a = 1-eps + # R=eps/(1-a*z): positive coefficients and exact infinite geometric tail. + partial = sum((eps*a**j for j in range(17)), F(0)) + tail = a**17 + need(partial+tail == 1, "Exact one-pole Wiener norm") + need(eps/(1-a) == 1, "One-pole circle maximum") + need(eps*a/(1-a)**2 == 2**k-1, "Diverging pointwise derivative") + # Elementary Blaschke factor b_a=(z-a)/(1-a*z). + first = a + sum(((1-a*a)*a**(j-1) for j in range(1, 18)), F(0)) + rest = (1+a)*a**17 + need(first+rest == 1+2*a <= 5, "Exact Blaschke norm and degree-one bound") + # P_eps=z-(1+eps) has exact circle gap eps and inverse at U=I of size 1/eps. + outer = 1+eps + need(abs(1-outer) == eps and abs(1/(1-outer)) == 2**k, + "Necessary inverse-gap exponent witness") + return {"families": 128, "epsilon": "2^-k, 1<=k<=128", + "one_pole_W_norm": "1", "pointwise_derivative_at_1": "2^k-1", + "necessary_gap_power": "P=z-(1+epsilon), gap=epsilon, inverse at U=I has norm 2^k"} + + +def expect_failure(fn, label): + try: + fn() + except (ValueError, ZeroDivisionError): + return label + raise ValueError("Control did not fail: "+label) + + +def controls(): + rejected = [] + for r in (0, 1, 2, 6, 10, 12, 15, 18, True, F(3)): + rejected.append(expect_failure(lambda r=r: budget(r), "inadmissible inherited radix "+str(r))) + for root in (ONE, C(0, 1), PHASES[2]): + rejected.append(expect_failure(lambda root=root: reflected((root,)), "unit-circle root "+str(root))) + rejected.append(expect_failure(lambda: reflected((), ZERO), "zero polynomial")) + rejected.append(expect_failure(lambda: cyclic(2, 1, C(2)), "nonunit phase")) + rejected.append(expect_failure(lambda: cyclic(0, 1, ONE), "zero cycle length")) + # A missing conjugation breaks modulus preservation for a nonreal root. + root, z = C(0, F(1, 2)), C(0, 1) + need((z-root).abs2() != (1-root*z).abs2(), "Wrong-conjugation control failed") + rejected.append("reflection without conjugation") + # Omitting the inner factor loses a sign already at z=-1. + p, q, num, den, m = reflected((C(F(1, 2)),)) + need(1/peval(p, -ONE) != 1/peval(q, -ONE), "Missing inner factor control failed") + rejected.append("omit Blaschke factor") + # Taylor coefficients of 1/(z-1/2) about zero diverge at z=1. + taylor_at_1 = -sum((F(2)**(j+1) for j in range(17)), F(0)) + residual = F(1, 2)*taylor_at_1-1 + need(abs(residual) == 2**17, "Interior-pole Taylor control failed") + rejected.append("Taylor expansion across an interior pole") + # Hilbert norm constant one is false: vector (1,1) on both sides. + need(F(7, 3)**2 > 4, "Hilbert constant-one control failed") + rejected.append("replace Hilbert constant four by one") + # Scalar circle information alone is not an induced infinity-norm bound. + p = [ONE, C(F(1, 2)), C(F(1, 2))] + mat = polynomial_matrix(p, mpowers(cyclic(3, 1, ONE), 3)) + inv = inverse(mat) + expected = [[C(F(3, 2) if i == j else F(-1, 2)) for j in range(3)] for i in range(3)] + need(inv == expected, "Spectral-shortcut witness inverse") + need(F(7, 32) > F(7, 15)**2, "Spectral-shortcut circle lower bound") + need(sum(abs(x.re) for x in inv[0]) == F(5, 2) > F(15, 7), "Spectral-shortcut strict witness") + rejected.append("equate scalar maximum with induced infinity norm") + return rejected + + +def blob(data): + return sha1(b"blob "+str(len(data)).encode("ascii")+b"\0"+data).hexdigest() + + +def check_sources(): + obj = json.loads((ROOT/"SOURCES.json").read_text(encoding="utf-8")) + need(obj["base_commit"] == BASE, "Base pin mismatch") + for entry in obj["files"]: + data = (ROOT/entry["local_path"]).read_bytes() + need(sha256(data).hexdigest() == entry["sha256"], "Source SHA-256 mismatch: "+entry["local_path"]) + need(blob(data) == entry["git_blob"], "Source Git-blob mismatch: "+entry["local_path"]) + selected = json.loads((ROOT/"vendor/selected-result.json").read_text(encoding="utf-8")) + need(selected["kappa"] == "51110230636731/31250000000000000", "Selected context mismatch") + return len(obj["files"]) + + +def evidence(): + return {"schema": 1, "status": "PASS_RATIONAL_CIRCLE_BOUND", "base": BASE, + "source_files": check_sources(), "budgets": [budget(r) for r in RADICES], + "reflection": reflection_checks(), "cyclic_inverses": cycle_checks(), + "hilbert": hilbert_checks(), "near_circle": near_circle_checks(), + "controls": controls(), "new_kappa_claim": False, + "scope": "Exact finite checks; analytic all-length proof is PROOF.md, not formalized."} + + +def check_manifest(): + obj = json.loads((ROOT/"MANIFEST.json").read_text(encoding="utf-8")) + for path, digest in obj["sha256"].items(): + need(sha256((ROOT/path).read_bytes()).hexdigest() == digest, "Package hash mismatch: "+path) + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--emit", type=Path, help="Write evidence to a new file; refuse any overwrite") + args = parser.parse_args() + if args.emit: + need(not args.emit.exists(), "Refusing to overwrite evidence") + else: + check_manifest() + obj = evidence() + if args.emit: + with args.emit.open("x", encoding="utf-8", newline="\n") as f: + f.write(json.dumps(obj, indent=2)+"\n") + else: + want = json.loads((ROOT/"EXPECTED.json").read_text(encoding="utf-8")) + need(obj == want, "Expected evidence mismatch") + print(obj["status"]) + print(json.dumps({"reflection": obj["reflection"], "cyclic_inverses": obj["cyclic_inverses"], + "hilbert": obj["hilbert"], "near_circle_families": obj["near_circle"]["families"], + "controls": len(obj["controls"]), "radix_budgets": len(obj["budgets"])}, sort_keys=True)) + + +if __name__ == "__main__": + main() From a0f15ce84f0951f69b39795f229cb854307ca52b Mon Sep 17 00:00:00 2001 From: AlephNaN <206279168+alephnan@users.noreply.github.com> Date: Tue, 13 Oct 2026 23:10:35 -0600 Subject: [PATCH 2/2] Clarify PR803 analytic proof and source audit --- research/rational-circle-bound/MANIFEST.json | 19 +- research/rational-circle-bound/NOTICE.md | 21 ++- research/rational-circle-bound/PROOF.md | 176 ++++++++++++++---- research/rational-circle-bound/README.md | 16 +- research/rational-circle-bound/SOURCES.json | 22 ++- research/rational-circle-bound/VALIDATION.md | 6 + .../rational-circle-bound/audit/README.md | 101 ++++++++++ .../rational-circle-bound/audit/TASK.json | 84 +++++++++ .../audit/VALIDATION.json | 85 +++++++++ .../audit/package-tests.txt | 9 + .../rational-circle-bound/audit/verify.txt | 2 + 11 files changed, 485 insertions(+), 56 deletions(-) create mode 100644 research/rational-circle-bound/audit/README.md create mode 100644 research/rational-circle-bound/audit/TASK.json create mode 100644 research/rational-circle-bound/audit/VALIDATION.json create mode 100644 research/rational-circle-bound/audit/package-tests.txt create mode 100644 research/rational-circle-bound/audit/verify.txt diff --git a/research/rational-circle-bound/MANIFEST.json b/research/rational-circle-bound/MANIFEST.json index 9bc8bcd12b..c3f983535a 100644 --- a/research/rational-circle-bound/MANIFEST.json +++ b/research/rational-circle-bound/MANIFEST.json @@ -3,17 +3,22 @@ "sha256": { ".gitattributes": "8d3eea09c326d8636669849bb00208a26ec4a709dfdaa505c9fdec253798dfa3", "CLAIM.json": "26eeeaa2027af5e90e7edb40be533a549b7197211599ab2c21f9087e354dbc76", + "EXPECTED.json": "9e019e77443a9fc1c4938d9d03d809d813de0558581fecf2fb72efef48f4bdcc", + "LICENSE": "c71d239df91726fc519c6eb72d318ec65820627232b2f796219e87dcf35d0ab4", + "NOTICE.md": "6e211502bc80038dcf2551dc914b77bc9603c8fb3c0c865268ba494102e73355", + "PROOF.md": "6c28d93d9d1d37da0bbc3876070ef8c6f0f5dad8e186b31b31330028e5420c0e", + "README.md": "77dcfe10cf69b66e092c4bf9501353cd82e61d899fca0b983f60dec25e012c4f", + "SOURCES.json": "d7f49b44d77321ac7da6b0b0652763518131474e28f23e1053706d7db3aa4e3e", + "VALIDATION.md": "23fa4a9731257ffdc1eb1f6b8614e43768c110c0d41d94315d45c030da2d5f47", + "audit/README.md": "8bfb503f127187d77697b8fca3e81bb93c5ef962a560898a6d737a0d5d0dd717", + "audit/TASK.json": "16339fdf45fa099d6d6e3f7371c73e98f6fcea2e4978844327f221a99fe96f0d", + "audit/VALIDATION.json": "c27fd0dd262620190f0c56dbe37f8467ecde4b2c2cc5bfbc9d56f2a4975e43fd", + "audit/package-tests.txt": "13f36996702c7cfbdeb015254dd2e6a7495e5d46a50e74bd93f1350b59a2546a", + "audit/verify.txt": "953432aa42f96318eb5cfe65e1d0f17a3dc0f75ca60e5e57a04fc00d4136dd9a", "evidence/environment.json": "7a7fe94aaf9af7d585426260c51505685397ec836b44094d78fe353a92e2bdfd", "evidence/package-tests.txt": "32e8de78ad3ff79dcdd0f162cfbd5f01dc031a39f346f76c57ecba288befaf91", "evidence/verify.txt": "953432aa42f96318eb5cfe65e1d0f17a3dc0f75ca60e5e57a04fc00d4136dd9a", - "EXPECTED.json": "9e019e77443a9fc1c4938d9d03d809d813de0558581fecf2fb72efef48f4bdcc", - "LICENSE": "c71d239df91726fc519c6eb72d318ec65820627232b2f796219e87dcf35d0ab4", - "NOTICE.md": "032c8a86591624e69dd306f93a66cbc2edf5ef108a5eacd7b893a0c48f6bab08", - "PROOF.md": "ffcad151a6fda894d16d7c227c219caa79a0fc0d446d2b7f7c903ebf1a06438e", - "README.md": "af582bea08442fea7e690202c5ee23d5f79f12b2305b1dd49a3e24444813d1eb", - "SOURCES.json": "68fca3bf9cdc9a69375d692514f2bd402ed59e0540bdb87b3d96d276ce7f9c01", "test_package.py": "287632c4632bd0de696cad3d5170eae1c15b739802a194143941abf7c41fa03d", - "VALIDATION.md": "92a7a586a9ae4fc2e0b2b168cf62f6d5fa9f31b3e42680ab8c70c96ca2a3cd4f", "vendor/previous-fourier-NOTICE.md": "05e6e660b74d34a8ed298f41889b9bb8b7fe365137bf2179f9828cdd2bb9a8b7", "vendor/previous-fourier-PROOF.md": "0dd5ff1a4377f4eeb92b3af7b75254bb343c64675b09201db132b394b0ebaaad", "vendor/prime-power-NOTICE.md": "96111c95cfec3c03a6f69c8e02c5d0bceff957d187e638d0534c676d6e3ffd77", diff --git a/research/rational-circle-bound/NOTICE.md b/research/rational-circle-bound/NOTICE.md index 77ff23ba18..75f764b802 100644 --- a/research/rational-circle-bound/NOTICE.md +++ b/research/rational-circle-bound/NOTICE.md @@ -20,16 +20,22 @@ Root reflection using finite Blaschke products and Hardy's coefficient inequality are classical. The rational arc-length inequality is credited to **E. P. Dolzhenko** and **M. N. Spijker**, following the historical discussion in **Anton Baranov and Rachid Zarouf**, arXiv:1310.1182v1, -Section 1.2.2. That paper was inspected for the normalized statement and -attribution. **Yuichi Kanjin and Kunio Sato**, "Hardy's inequality for +Sections 1.1 and 1.2.2. That paper was inspected for the normalized +statement and attribution. For the PR803 review continuation, Spijker's +original BIT 31 (1991), pp. 552-554, equation (4) and Lemma 2, was also +inspected in the author-uploaded full text linked in SOURCES.json. +Our projection derivation follows that classical proof, with its level +polynomial and limit justifications expanded; it is not a new method. +**Yuichi Kanjin and Kunio Sato**, "Hardy's inequality for Jacobi expansions" (2004), opening page, also records the classical Hardy -coefficient inequality. Neither paper is redistributed. The elementary +coefficient inequality. None of these papers is redistributed. The elementary proofs and nonoptimal constant four are written out for review here. No novelty claim is made for those classical tools or their general combination in rational function theory. -The finite-geometric inverse is standard. **Joshua Snider / jsnider3**, -PR692, already uses it for weighted-stride closure and bilinear-dual +The finite-geometric inverse is standard. **Ryan Pinto / Ambassators**, +PR692 at `c5b53a5e80372a1fae9830d8dcf21aaabce3f729`, already uses it +for weighted-stride closure and bilinear-dual verification. Our small Gaussian-rational implementation is newly written; no PR692 code is consumed. **Chafik Boukhalfa / chafreaky**, PR628, and **Charles Bethin / cbethin**, PR764, supply distinct rounded-scan results. @@ -43,4 +49,9 @@ as recorded in the preserved PR621 notice. The selected-result snapshot retains the #626/#543 contributor lineage. It is historical context, not evidence of a new exponent. +The review continuation corrects the earlier misattribution of PR692 to +Joshua Snider / jsnider3. Ryan Pinto's authorship is stated in PR692's +own description. The earlier source-head evidence remains available in +Git; no vendored source or historical test receipt is altered. + New text and code are Apache-2.0. The unchanged upstream license is included. diff --git a/research/rational-circle-bound/PROOF.md b/research/rational-circle-bound/PROOF.md index 0813082ee8..15d344789d 100644 --- a/research/rational-circle-bound/PROOF.md +++ b/research/rational-circle-bound/PROOF.md @@ -36,6 +36,18 @@ Romman's PR621 and its comparison with our previous Fourier audit. It is not a literature-priority claim, a paid inversion algorithm, a formal proof-assistant result, or a new multiplication exponent. +The source and analytic audit responding to the review of commit +`d213ac12d4a1ab8f717d942e844df318ceb395fb` is in +[audit/README.md](audit/README.md). It maps each implication to its proof +and records the limits of that audit separately from finite evidence. +Throughout, circle integrals use `dt/(2 pi)` unless explicitly unnormalized, +and the Fourier convention is + +\[ + \widehat f(k)={1\over2\pi}\int_0^{2\pi}f(e^{it})e^{-ikt}\,dt, + \qquad \|f\|_W=\sum_{k\in\mathbb Z}|\widehat f(k)|. +\] + ## 1. A coefficient inequality with an elementary constant For an analytic function h in a neighborhood of the closed disk, write @@ -47,9 +59,17 @@ h(z)=sum_{j>=0} h_j z^j. With normalized circle measure, we will use Here is a proof of this nonoptimal version of Hardy's inequality. First the matrix K_{jk}=1/(j+k+1), j,k>=0, has l2 operator norm at most -4. Set w_j=(j+1/2)^(-1/2) and a=j+1/2. The positive function -x^(-1/2)/(a+x) is convex on x>0: in the second derivative of the -product, both second-derivative terms and the cross term are positive. +4. Set w_j=(j+1/2)^(-1/2) and a=j+1/2. For +f_a(x)=x^(-1/2)/(a+x), direct differentiation gives + +\[ + f_a''(x)={3\over4x^{5/2}(a+x)} + +{1\over x^{3/2}(a+x)^2} + +{2\over x^{1/2}(a+x)^3}>0. +\] + +The integral at zero is improper but finite. Jensen's midpoint inequality +also applies on [0,1] (or by a limit of interior integrals). The midpoint inequality on each [k,k+1] therefore gives \[ @@ -72,9 +92,14 @@ now yields Suppose initially that h has no zero on the circle and is not identically zero. Remove its finitely many disk zeros, with multiplicity, by a finite -Blaschke product J. Then h/J is analytic and zero-free on the closed -disk and has an analytic square root v in a neighborhood of that disk. -Put a=Jv, b=v. These functions satisfy h=ab and +Blaschke product J. The apparent singularities of h/J at these zeros +are removable, with +nonzero limiting values because the multiplicities match. The quotient +is therefore analytic and zero-free on the closed disk. By compactness, +it is analytic and zero-free on some disk |z|<1+eta, eta>0; shrink eta +also to avoid the finitely many poles of J. On that simply connected +disk it has an analytic logarithm, so v=exp(log(h/J)/2) is an analytic +square root. Put a=Jv, b=v. These functions satisfy h=ab and \[ \|a\|_2^2=\|b\|_2^2=\|h\|_1, @@ -89,8 +114,12 @@ inequality, (4), and Parseval give \le4\|a\|_2\|b\|_2=4\|h\|_1. \] -Use finite sums followed by monotone limits, so absolute summability is -not assumed in advance. The zero function is immediate. For possible +More explicitly, for each N bound sum_{l=0}^N |h_l|/(l+1) by the +nonnegative convolution sum over j+k<=N, then by the square truncation +0<=j,k<=N of (4). Parseval bounds both truncated l2 norms uniformly. +Let N tend to infinity. This proves the infinite inequality without +assuming the desired weighted absolute summability in advance. +The zero function is immediate. For possible circle zeros, apply the result to h(rho z) along rho increasing to 1 and avoiding the finitely many zero radii, then use monotone convergence on the coefficients and uniform convergence on the circle. This proves @@ -105,19 +134,48 @@ circle, put M=max_{|z|=1}|R(z)|. The classical Dolzhenko-Spijker estimate is \|R'\|_{L^1(\mathbb T)}\le dM. \tag{5} \] -A projection proof records why no pole distance is needed. Cancel any -common factors first, so B has no zeros on the circle. Set -gamma(t)=R(e^{it}) and x_phi(t)=Re(e^{-i phi} gamma(t)). For any fixed -phi and real level s, clearing |B(z)|^2 in x_phi(t)=s and multiplying -by z^d yields a polynomial of degree at most 2d. Conjugated polynomials -on the circle are evaluated at 1/z. Unless the polynomial is identically -zero, the level has at most 2d preimages in 0<=t<2pi. +The following is the projection argument of Spijker's original Lemma 2, +with the polynomial and normalization made explicit; it is not a new +proof method. See BIT 31 (1991), pp. 552-554, equation (4) and Lemma 2; +the original author-uploaded text is linked in SOURCES.json. The same +normalized statement is Baranov-Zarouf, Section 1.2.2, equation (1.3). + +Cancel any common factors first. Use the reduced degree d, or any larger +integer degree bound; B has no zero on the circle. For a polynomial A of +degree at most d define its padded conjugate reciprocal by + +\[ + A^{\#}_d(z)=\sum_{j=0}^d\overline{a_j}z^{d-j}, + \qquad A^{\#}_d(z)=z^d\overline{A(z)}\quad(|z|=1). +\] -For each phi an identically zero level equation can occur for at most -one s, which has measure zero. Equivalently, if the projection is -constant its variation is zero. Split the nonconstant real analytic -projection into its finitely many monotone intervals. Its total variation -is the integral of the number of level crossings. Since |x_phi|<=M, +Define B^{#}_d likewise. Put gamma(t)=R(e^{it}) and +x_phi(t)=Re(e^{-i phi} gamma(t)). For z=e^{it}, the level equation +x_phi(t)=s is equivalent to + +\[ + F_{\phi,s}(z)=e^{-i\phi}A(z)B^{\#}_d(z) + +e^{i\phi}A^{\#}_d(z)B(z)-2sB(z)B^{\#}_d(z)=0. \tag{5a} +\] + +Indeed, this is obtained by multiplying the level equation by +2 z^d |B(z)|^2, which is nonzero on the circle. Every term in (5a) +has degree at most 2d, also when A or B has degree less than d. + +If x_phi is constant its variation is zero. Otherwise F_{phi,s} is a +nonzero polynomial for every s: an identically zero F would make the +projection constantly s. It therefore has at most 2d distinct unit-circle +zeros, hence at most 2d preimages in 0<=t<2pi for every level s. + +The projection is real analytic on a neighborhood of the parameter +circle. Its derivative either vanishes identically (the constant case) +or has finitely many zeros on a period, by the identity theorem and +compactness. Split at these zeros and at the period endpoint. On each +open piece x_phi is strictly monotone, so its variation is the integral +of the indicator of its image interval. Summing the finitely many +pieces gives the integral of the number of preimages for almost every +s; the finitely many endpoint and critical values have measure zero. +Since |x_phi|<=M, \[ \int_0^{2\pi}|x_\phi'(t)|\,dt\le 4dM. @@ -125,14 +183,18 @@ is the integral of the number of level crossings. Since |x_phi|<=M, Integrating over 0<=phi<2pi, the integral of |Re(e^{-i phi}v)| is 4|v| for every complex v. Hence -4 int |gamma'| <= 8pi dM. On the circle |gamma'|=|R'|; divide by 2pi -to obtain (5). The case of a constant R is immediate. This is an +4 int_0^{2pi} |gamma'| dt <= 8pi dM. Interchanging these +nonnegative continuous integrands is valid. The chain rule gives +gamma'(t)=i e^{it} R'(e^{it}), so dividing the last bound by 8pi +proves ||R'||_1 <= dM with normalized circle measure, as in (5). The +case of a constant R is immediate. This is an elementary proof of a classical result, not a new arc-length theorem. ## 3. An analytic rational function has a degree-only Wiener penalty If R is rational of degree at most d and analytic in a neighborhood of -the closed disk, apply (3) to h=R'. For R(z)=sum r_j z^j, +the closed disk, then so is h=R'. For R(z)=sum r_j z^j, its derivative +has coefficients h_j=(j+1)r_{j+1}. Applying (3) therefore gives exactly \[ \sum_{j\ge1}|r_j|\le4\|R'\|_1\le4d\|R\|_\infty. @@ -172,17 +234,52 @@ By (6), \|1/Q\|_W\le(1+4n)/\delta,\qquad \|J\|_W\le1+4m. \] -On the circle, 1/P=overline(J)/Q. Conjugating the values reverses the -Fourier indices and conjugates the coefficients, preserving their l1 -norm. The convolution inequality for absolutely summable coefficients -now gives (1). No roots need be computed to use the worst-case m<=n. +On the circle, 1/P=overline(J)/Q. Write J(z)=sum_{j>=0} b_j z^j +and 1/Q(z)=sum_{l>=0} a_l z^l. Both coefficient sequences are in l1 +by (6), and their series converge uniformly on the circle. Thus + +\[ + {1\over P(z)}=\sum_{j,l\ge0}\overline{b_j}a_l z^{l-j}, + \qquad c_k=\sum_{l-j=k}\overline{b_j}a_l, + \qquad \sum_{k\in\mathbb Z}|c_k| + \le\left(\sum_j|b_j|\right)\left(\sum_l|a_l|\right). \tag{7} +\] + +The double absolute sum is finite, which justifies regrouping and +termwise integration to identify c_k as the Fourier coefficients of +1/P. This establishes (1), including negative indices; no Fourier +sampling or limit in the cyclic length is involved. It also agrees +with the Laurent series on a root-free annulus containing the circle. +No roots need be computed to use the worst-case m<=n. ## 5. Operator substitution and the prime-power comparison -Write 1/P(z)=sum_{k in Z} c_k z^k on the circle. Absolute convergence -and ||U^k||<=1 make sum c_k U^k converge in operator norm. The finite -polynomial times this series has the coefficients of 1. Substitute U -to obtain P(U) sum c_k U^k = I in both orders, proving (2). +Write P(z)=sum_{j=0}^n p_j z^j and use c_k from (7). In the Banach +algebra of bounded operators, ||U^k||<=1 for every integer k makes +S=sum_{k in Z} c_k U^k converge absolutely in operator norm, with +||S||<=sum_k |c_k|. Invertibility of U makes all negative powers defined. + +The uniformly convergent circle identity P(z) sum_k c_k z^k=1 gives, +by termwise Fourier integration, + +\[ + \sum_{j=0}^n p_jc_{q-j}=\begin{cases}1,&q=0,\\0,&q\ne0.\end{cases} +\] + +Moreover sum_{j,k}|p_j c_k| ||U^{j+k}|| is finite. Regrouping the +operator series by q=j+k is therefore valid and gives P(U)S=I. +All integer powers of U commute, giving SP(U)=I by the same calculation. +Thus S is the inverse, proving (2) without assuming invertibility of +P(U) or diagonalizing it in advance. + +A fixed permutation matrix multiplied by a diagonal of unit-modulus +entries, and its inverse, are infinity-norm isometries. Their integer +powers have norm one, including zero/noncoprime strides and arbitrary +coordinate-dependent unit phases. Unit-circle spectrum alone would +not suffice: U=[[1,25],[0,1]] and P(z)=z-2 have delta=1 and +||P(U)^{-1}||_infinity=26>25=(1+4)^2. That U violates the power-norm +hypothesis. The separate weighted-cycle audit PR852 likewise treats +this hypothesis as essential, not as a consequence of spectral location. Retain PR621's certified inputs, without changing its nonvanishing proof: @@ -191,6 +288,8 @@ Retain PR621's certified inputs, without changing its nonvanishing proof: \quad A=\delta^{-1}=2rnH^{nD-1},\quad X=nH^{nD/2}. \] +The inherited PR621 expression is A+(2nH/r)A^2. Since +(2nH/r)A=4n^2 H^{nD}=4X^2, it equals A(1+4X^2) exactly. The three explicit norm overestimates are | Estimate | Constant | Leading power of H | @@ -246,12 +345,15 @@ failure modes. The written argument supplies the all-frequency and all-length reasoning. Independent human or proof-assistant review remains open, as do the repository's full multiplication obligations. -Classical references and repository pins are recorded in SOURCES.json -and NOTICE.md. The normalized arc-length inequality is explicitly -stated in Baranov-Zarouf, arXiv:1310.1182v1, Section 1.2.2, equation -(1.3), with attribution to Dolzhenko and Spijker. Hardy's coefficient -inequality and finite Blaschke reflection are standard; complete -nonoptimal arguments are included here to make constants reviewable. +Classical references and repository pins are recorded in SOURCES.json, +NOTICE.md, and audit/README.md. Spijker's original equation (4) and +Lemma 2 use unnormalized arc length; dividing by 2 pi gives (5). +Baranov-Zarouf, arXiv:1310.1182v1, Section 1.1 and Section 1.2.2, +equation (1.3), confirm the normalized form and Dolzhenko attribution. +The opening of Kanjin-Sato records Hardy's coefficient inequality with +an unspecified constant and unnormalized H1 measure. It is background +attribution, not a source for our normalized constant four; Section 1 +proves that constant directly. Finite Blaschke reflection is classical. Prepared for Rafael Guevara (@alephnan) with substantial OpenAI Codex assistance. Apache-2.0. diff --git a/research/rational-circle-bound/README.md b/research/rational-circle-bound/README.md index 1703d4a2c4..1a1d3068a8 100644 --- a/research/rational-circle-bound/README.md +++ b/research/rational-circle-bound/README.md @@ -30,7 +30,11 @@ change. These are bound sizes, not working precision or measured norms. ## Review and reproduce -Read `PROOF.md`, then run from the repository root: +Start with [the source and analytic audit](audit/README.md), which responds +to the PR803 review at `d213ac12d4a1ab8f717d942e844df318ceb395fb`. +It records the classical source locators, normalization, all-frequency +proof steps, and outstanding independent-review obligations. Read +[PROOF.md](PROOF.md) for the expanded argument, then run from the repository root: ```sh python -B research/rational-circle-bound/verify.py @@ -57,7 +61,7 @@ The finite coverage is declared, not a proof of the analytic inequalities: See `VALIDATION.md` for the actual platform, package fault tests, and limits. The cyclic oracle is the standard finite-geometric identity, also used by -Joshua Snider in PR692; it is not a new solver. +Ryan Pinto (@Ambassators) in PR692; it is not a new solver. ## Scope and provenance @@ -87,5 +91,13 @@ costs have not been improved merely by proving this operator bound. Concurrent PR796 computes nonarchimedean root valuations; it does not supply a complex conditioning bound and is distinct from this application. +## Open next questions + +- Independent analytic review: check the implication map and source normalization + in `audit/README.md` against `PROOF.md`; finite tests cannot settle this. +- Rounded implementation: determine whether the norm estimate improves a specific + precision recurrence, with all preparation, restoration and routing charges. + The analytic theorem alone does not provide that implementation. + Prepared for Rafael Guevara (@alephnan) with substantial OpenAI Codex assistance. Apache-2.0. See `NOTICE.md`. diff --git a/research/rational-circle-bound/SOURCES.json b/research/rational-circle-bound/SOURCES.json index 5f5d339325..b0e1e27908 100644 --- a/research/rational-circle-bound/SOURCES.json +++ b/research/rational-circle-bound/SOURCES.json @@ -58,8 +58,8 @@ "authors": "Anton Baranov and Rachid Zarouf", "title": "A model space approach to some classical inequalities for rational functions", "url": "https://arxiv.org/abs/1310.1182v1", - "locator": "Section 1.2.2, equation (1.3), and bibliography [D], [S]", - "use": "Confirms the normalized Dolzhenko-Spijker inequality and classical attribution. Not vendored. The note supplies its own projection proof." + "locator": "Section 1.1, p. 1 (degree and normalized measure); Section 1.2.2, p. 3, equation (1.3); bibliography [D], [S]", + "use": "Confirms the normalized Dolzhenko-Spijker inequality and classical attribution. Not vendored. The note expands the classical projection derivation, with the original Spijker source identified below." }, { "authors": "Yuichi Kanjin and Kunio Sato", @@ -67,13 +67,17 @@ "year": 2004, "url": "https://files.ele-math.com/articles/mia-07-56.pdf", "locator": "Opening statement on page 551", - "use": "Confirms the classical Hardy coefficient inequality. Not vendored. The constant four is proved here by factorization and a Schur estimate." + "use": "Background attribution only: the opening states the classical Hardy coefficient inequality with an unspecified constant and unnormalized H1 measure. The normalized constant four is proved locally, not imported from this reference." }, { "authors": "M. N. Spijker", "title": "On a conjecture by LeVeque and Trefethen related to the Kreiss matrix theorem", "publication": "BIT 31 (1991), 551-555", - "use": "Historical attribution as cited by Baranov-Zarouf; original article not independently retrieved." + "use": "Original author-uploaded full text inspected during the PR803 review continuation. Its unnormalized arc-length bound with gamma=1 becomes the local normalized inequality after division by 2 pi. The projection argument follows this proof. Not redistributed.", + "doi": "10.1007/BF01933268", + "url": "https://www.researchgate.net/publication/227228151_On_a_conjecture_by_LeVeque_and_Trefethen_related_to_the_Kreiss_matrix_theorem", + "locator": "p. 552, definition of the rational class and equation (4); pp. 552-554, Lemma 2 and its projection/level-count proof", + "accessed_utc": "2026-10-14" } ], "related_work": [ @@ -94,7 +98,9 @@ }, { "pr": 692, - "relation": "Prior finite-geometric weighted-stride resolvent; that standard oracle formula is not new here." + "relation": "Prior finite-geometric weighted-stride resolvent; that standard oracle formula is not new here.", + "head": "c5b53a5e80372a1fae9830d8dcf21aaabce3f729", + "author": "Ryan Pinto (@Ambassators)" }, { "pr": 666, @@ -104,6 +110,12 @@ "pr": 736, "head": "eccc3b74767848eb6746f39412d57df6c9544b5d", "relation": "Finite elimination optimization, not an analytic norm bound." + }, + { + "pr": 852, + "head": "aa26b2ad761aa3bac76670e4749f53d2dafb3fea", + "author": "William Lawyer (@WilliamLawyer)", + "relation": "Downstream weighted-cycle power audit. It inherits PR803 as an explicit analytic premise, so it does not independently certify this Wiener theorem. No PR852 source is imported." } ] } diff --git a/research/rational-circle-bound/VALIDATION.md b/research/rational-circle-bound/VALIDATION.md index dae4717f68..33e131643d 100644 --- a/research/rational-circle-bound/VALIDATION.md +++ b/research/rational-circle-bound/VALIDATION.md @@ -1,5 +1,11 @@ # Validation and limits +The sections below retain the original 2026-10-13 execution record. +The later PR803 source/analytic review continuation is documented in +[audit/README.md](audit/README.md), with separate revision checks in +[audit/VALIDATION.json](audit/VALIDATION.json). The historical receipts +are unchanged and are not promoted to an analytic-proof certificate. + Executed on Windows 11 (10.0.26300), CPython 3.12.2, 2026-10-13 UTC. The detailed interpreter/platform strings and command receipts are in `evidence/environment.json`, `evidence/verify.txt`, and diff --git a/research/rational-circle-bound/audit/README.md b/research/rational-circle-bound/audit/README.md new file mode 100644 index 0000000000..4d590ad3fd --- /dev/null +++ b/research/rational-circle-bound/audit/README.md @@ -0,0 +1,101 @@ +# PR803 source and analytic proof audit + +This continues the [review comment](https://github.com/CrocSwap/integer-mult-bounds/pull/803#issuecomment-6160966501) +on source head `d213ac12d4a1ab8f717d942e844df318ceb395fb`. +It addresses the analytic proof of + +\[ + \|1/P\|_W\le (1+4m)(1+4n)/\delta\le(1+4n)^2/\delta, +\] + +for every nonzero degree-n complex polynomial with |P|>=delta>0 on +the entire unit circle; m counts interior roots with multiplicity. +The conclusion of this author/AI audit is that the stated proof chain +supports the bound. The revision makes the source normalization and +previously compressed implications explicit. It changes neither the +bound nor the admissible operators, and does not claim independent +human review, formal verification, or maintainer acceptance. + +## Sources actually checked + +| Source and locator | What was checked | Role and limit | +| --- | --- | --- | +| [Baranov-Zarouf, arXiv:1310.1182v1](https://arxiv.org/pdf/1310.1182v1), Section 1.1, p. 1; Section 1.2.2, p. 3, (1.3) | Rational degree is the maximum of numerator and denominator degrees; poles on the circle are excluded; Lebesgue measure is normalized. Their derivative L1 bound is degree times the circle supremum. | Matches `PROOF.md` (5), including poles inside the disk. Also supplies historical attribution to Dolzhenko. Dolzhenko's original article was not independently inspected. | +| [Spijker, BIT 31 (1991), 551-555](https://www.researchgate.net/publication/227228151_On_a_conjecture_by_LeVeque_and_Trefethen_related_to_the_Kreiss_matrix_theorem), author-uploaded original full text, p. 552 (4), pp. 552-554 Lemma 2 | The original inequality uses unnormalized arc length with factor 2 pi times degree. Lemma 2 establishes constant gamma=1 by projection and a degree-2n level polynomial. | Dividing by 2 pi gives (5). The local projection derivation follows this classical proof; it is not a new proof method. DOI: [10.1007/BF01933268](https://doi.org/10.1007/BF01933268). | +| [Kanjin-Sato, Mathematical Inequalities & Applications 7 (2004), 551-555](https://files.ele-math.com/articles/mia-07-56.pdf), opening of p. 551 | The classical Hardy coefficient inequality is stated with an unspecified constant and an unnormalized H1 integral. | Background attribution only. It does not supply the normalized constant four used here. That constant is derived in `PROOF.md` Section 1. | +| [Ali Romman's PR621](https://github.com/CrocSwap/integer-mult-bounds/pull/621), head `520774462b19b29af41554b74def31f9d01e997e`; local `vendor/prime-power-proof.md` | The declared kernel, n=r-1, D=phi(r), H=2^r-1, delta=(2rn H^(nD-1))^-1, and original norm expression agree with the application. | Only source identity and the specialization interface are covered here. Its nonvanishing/resultant theorem remains the inherited foundation; no new foundation replay or full re-audit is claimed. | + +These readings were made on 2026-10-14 UTC (2026-10-13 in the contributor's +America/Mexico_City timezone). Papers are cited, not redistributed. The +Leiden-hosted Spijker PDF returned HTTP 404; the inspected original text +is the author-uploaded version linked above. Exact local source SHA-256 +and Git-blob pins remain in `SOURCES.json`; none of its six immutable +source/context files changed. + +## Analytic implication audit + +Read the revised [PROOF.md](../PROOF.md) in the following order. Each row +is a mathematical argument, not an inference from a finite verifier. + +| Step | Analytic obligation and resolution | +| --- | --- | +| Section 1, (3)-(4) | The explicit positive second derivative proves the midpoint bound, including its integrable endpoint at zero. The weighted Cauchy-Schwarz argument is first applied to finite truncations, with a uniform bound four. Multiplicity-matched Blaschke removal gives a zero-free analytic quotient on a slightly larger disk, where an analytic logarithm supplies its square root. Parseval then bounds the coefficient convolution. The proof takes finite truncations before the monotone limit; boundary zeros are handled by radial dilation avoiding the finitely many zero radii and uniform convergence. | +| Section 2, (5)-(5a) | The padded reciprocal polynomials give the exact level equation of degree at most 2d without losing conjugation or requiring equal numerator/denominator degrees. A constant projection contributes zero variation. Otherwise the level polynomial cannot be identically zero, and a real analytic projection has finitely many critical points per period. The monotone-interval count holds off finitely many critical/endpoint levels. Integration over projection angles and division by 8 pi yield the normalized derivative bound. | +| Section 3, (6) | The coefficient identity for R' cancels the weight in (3). The degree used in (5) is that of R, not R'. Cauchy's constant-coefficient estimate supplies the remaining term. Both R and R' are analytic on a neighborhood of the closed disk; this lemma is not applied directly to 1/P with interior poles. | +| Section 4, (7) | Reflection gives the rational identity P=JQ. The roots of J's numerator are inside and its denominator roots outside, so no cancellation invalidates degree m. Zero roots contribute z to J and 1 to Q. Repetition changes multiplicity but not the argument. The two analytic factors have l1 coefficients; their absolutely convergent double series identifies both Fourier directions of 1/P and bounds their sum by the product of the two norms. No root-distance estimate is introduced. | +| Section 5 | Completeness of the bounded-operator algebra and the bound on every signed power give an absolutely convergent series S. The finite polynomial identity yields coefficient-wise convolution with the unit sequence. Absolute convergence permits regrouping the operator series, producing both P(U)S=I and SP(U)=I. Thus invertibility of P(U) is proved, not assumed from its spectrum. | +| Section 5, application | A unit-modulus monomial matrix and its inverse are infinity-norm isometries; length, stride and repeated eigenvalues introduce no extra factor. Merely having unit-circle spectrum is insufficient, as the displayed 2-by-2 Jordan example shows. The inherited norm constant rewrites exactly as A(1+4X^2). The strict comparison uses n,D>=2 and H^(nD/2)>=H^2>4n+2. | +| Section 6 | P_epsilon(z)=z-(1+epsilon) has circle minimum epsilon and inverse norm epsilon^-1 at U=I. Multiplying by z^(n-1) preserves both facts for any fixed n>=1. This proves necessity of the inverse-gap exponent, not optimality of the degree factor. | + +The remaining basic tools are the fundamental theorem of algebra, +removable singularities, analytic logarithms on simply connected zero-free +domains, Parseval/Cauchy coefficient formulas, polynomial root counting, +and absolute/monotone convergence. No root separation, finite sample +coverage, diagonalization, or unproved numerical limit is a premise. + +## Attribution correction and overlap + +[PR692](https://github.com/CrocSwap/integer-mult-bounds/pull/692), head +`c5b53a5e80372a1fae9830d8dcf21aaabce3f729`, identifies **Ryan Pinto +(@Ambassators)** as its contributor. The previous PR803 prose incorrectly +credited Joshua Snider / jsnider3 for that PR. `README.md`, `NOTICE.md` and +`SOURCES.json` now carry the verified credit. No PR692 code is consumed. + +[William Lawyer's PR852](https://github.com/CrocSwap/integer-mult-bounds/pull/852), +head `aa26b2ad761aa3bac76670e4749f53d2dafb3fea`, treats PR803's analytic +bound as an explicit inherited premise. Its weighted-cycle power results +therefore do not independently certify this proof. Its scope differs +from this assigned continuation. The overlap helper's cached PR and +discussion coverage, freshness limits, and the live head checks are +recorded in `TASK.json`; no novelty claim follows from that search. + +## Retained evidence and revision checks + +The [batch disposition](https://github.com/CrocSwap/integer-mult-bounds/blob/main/research/community-efficient100-audit/DISPOSITIONS.json) +marks PR803 partially reviewed. Its [source packet](https://github.com/CrocSwap/integer-mult-bounds/blob/main/research/community-efficient100-audit/packets/803.json) +records 20 added paths and an empty `checks` list; it does not claim an +independent maintainer replay of this package. The contributor's earlier +finite evidence remains in `../evidence/` and `../EXPECTED.json` unchanged. + +The new evidence is the source comparison and expanded analytic reasoning. +The existing verifier and eight package controls are rerun only to check +the revised package and regenerated manifest, with results in +[VALIDATION.json](VALIDATION.json). No new finite domains or tests are added, +and these regression checks do not certify an analytic theorem. The +original `CLAIM.json`, all vendored files, both executable scripts, and +the earlier test receipts are preserved byte for byte at the reviewed head. + +## Open next questions + +1. **Independent acceptance of this proof.** A reviewer can start with the + implication table above and verify (3)-(7) in the revised proof, especially + the padded level polynomial and the two absolute-convergence arguments. + No independent human review or proof-assistant certificate is supplied. +2. **A paid rounded implementation.** Pick a specific precision recurrence + and prove its preparation, propagation, restoration and routing obligations + using the new bound. The all-length exact-operator estimate alone does not + pay for that implementation or change the selected multiplication exponent. + +Prepared for Rafael Guevara (@alephnan) with substantial OpenAI Codex +assistance in source checking, mathematical review and writing. No sub-agents +were used. This is a contribution-side audit, not a maintainer disposition. diff --git a/research/rational-circle-bound/audit/TASK.json b/research/rational-circle-bound/audit/TASK.json new file mode 100644 index 0000000000..4e8ffe07e3 --- /dev/null +++ b/research/rational-circle-bound/audit/TASK.json @@ -0,0 +1,84 @@ +{ + "task_id": "pr803-source-analytic-audit", + "assignment": "Explicit user continuation of the analytic proof/source review comment on PR803; no random task draw.", + "reviewed_head": "d213ac12d4a1ab8f717d942e844df318ceb395fb", + "upstream_base": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "review_comment": "https://github.com/CrocSwap/integer-mult-bounds/pull/803#issuecomment-6160966501", + "scope_status": "unchanged", + "scope_reason": "Make the existing all-frequency/all-length proof and source attribution reviewable; preserve the theorem, finite domains and inherited premises.", + "question": "Does the written proof justify (1+4m)(1+4n)/delta for all stated polynomials and all-integer-power contractions, with matching source normalizations?", + "method": "Source comparison and direct analytic audit of each implication; explicit limiting arguments and an operator-hypothesis counterexample.", + "domain": "Every nonzero complex polynomial of finite degree with positive whole-circle gap; all bounded invertible complex Banach-space operators with norm at most one for every signed power.", + "success_evidence": "Source locators and normalization map; explicit proof of the analytic implications. Existing finite tests serve only as package regressions.", + "falsification_checks": [ + "Boundary zeros in Hardy factorization", + "Constant projections", + "Missing complex conjugation", + "Degree loss at zero roots", + "Unjustified rearrangement of infinite series", + "Replacing two-sided power control by unit-circle spectrum" + ], + "budget_minutes": 60, + "predecessor_authors": [ + "Ali Romman / aliromman (PR621)", + "Ryan Pinto / Ambassators (PR692)", + "E. P. Dolzhenko", + "M. N. Spijker", + "G. H. Hardy", + "Anton Baranov and Rachid Zarouf", + "Yuichi Kanjin and Kunio Sato" + ], + "original_files": { + "PROOF.md": { + "sha256": "ffcad151a6fda894d16d7c227c219caa79a0fc0d446d2b7f7c903ebf1a06438e" + }, + "SOURCES.json": { + "sha256": "68fca3bf9cdc9a69375d692514f2bd402ed59e0540bdb87b3d96d276ce7f9c01" + }, + "MANIFEST.json": { + "sha256": "c5357e926179dc5b760f60fcaff857fcea82f7b1221c8b4071d62e4b0afcbd31" + }, + "EXPECTED.json": { + "sha256": "9e019e77443a9fc1c4938d9d03d809d813de0558581fecf2fb72efef48f4bdcc" + }, + "verify.py": { + "sha256": "b40f04343586a17a8a6debb22408c30e7ed8265cbce9b079bcdddce4f0c9da6d" + }, + "test_package.py": { + "sha256": "287632c4632bd0de696cad3d5170eae1c15b739802a194143941abf7c41fa03d" + } + }, + "overlap": { + "command": "python scripts/find_overlap.py Wiener rational-circle-bound --offline --json", + "command_context": "Original checkout at ef5f3940, not the historical PR803 checkout where this helper was not yet present.", + "searched_at_utc": "2026-10-14T04:59:01.643651+00:00", + "cached_open_prs": { + "fetched_at_utc": "2026-10-14T04:14:01.119665+00:00", + "records": 733, + "complete_pagination": true + }, + "cached_discussions": { + "fetched_at_utc": "2026-10-14T04:15:18.188464+00:00", + "records": 259, + "complete_pagination": true + }, + "local_records": 327, + "matches": [ + "PR803", + "PR852", + "research/additive-cyclic-no-connector/README.md", + "research/grouped-dirty-cyclic/README.md" + ], + "live_read": [ + "Discussion1163 start-here", + "Active discussion listing", + "PR803 metadata/comments/review threads", + "PR852 metadata and explicit PR803 premise", + "PR621 and PR692 metadata and credit" + ], + "limitations": "Offline helper cache may miss current changes; local checkout predates the batch review. Live direct source/head reads supplement it. No novelty certificate or general reservation is claimed.", + "coordination": "Local continuation record only; no new Discussion post or claim." + }, + "new_kappa_claim": false, + "assistance": "Substantial OpenAI Codex assistance; author/AI review only; no sub-agents." +} diff --git a/research/rational-circle-bound/audit/VALIDATION.json b/research/rational-circle-bound/audit/VALIDATION.json new file mode 100644 index 0000000000..c37eb8b8c4 --- /dev/null +++ b/research/rational-circle-bound/audit/VALIDATION.json @@ -0,0 +1,85 @@ +{ + "schema": 1, + "status": "PASS_SCOPED_PACKAGE_REGRESSION", + "reviewed_predecessor": "d213ac12d4a1ab8f717d942e844df318ceb395fb", + "python": "3.12.2 (tags/v3.12.2:6abddd9, Feb 6 2024, 21:26:36) [MSC v.1937 64 bit (AMD64)]", + "platform": "Windows-11-10.0.26300-SP0", + "recorded_utc": "2026-10-14T05:06:32.073056+00:00", + "coverage": "Existing exact verifier and all eight existing package controls after proof/source documentation revision; no new finite test domains.", + "commands": [ + { + "command": "python -I -O -B research/rational-circle-bound/verify.py", + "argv": [ + "C:\\Users\\rafag\\AppData\\Local\\Programs\\Python\\Python312\\python.exe", + "-I", + "-O", + "-B", + "research/rational-circle-bound/verify.py" + ], + "started_utc": "2026-10-14T05:06:04.807316+00:00", + "seconds": 7.672, + "exit_code": 0, + "expected_marker": "PASS_RATIONAL_CIRCLE_BOUND", + "marker_present": true, + "output": "audit/verify.txt", + "output_sha256": "953432aa42f96318eb5cfe65e1d0f17a3dc0f75ca60e5e57a04fc00d4136dd9a" + }, + { + "command": "python -I -O -B research/rational-circle-bound/test_package.py", + "argv": [ + "C:\\Users\\rafag\\AppData\\Local\\Programs\\Python\\Python312\\python.exe", + "-I", + "-O", + "-B", + "research/rational-circle-bound/test_package.py" + ], + "started_utc": "2026-10-14T05:06:12.485322+00:00", + "seconds": 19.063, + "exit_code": 0, + "expected_marker": "PASS_PACKAGE_CONTROLS", + "marker_present": true, + "output": "audit/package-tests.txt", + "output_sha256": "13f36996702c7cfbdeb015254dd2e6a7495e5d46a50e74bd93f1350b59a2546a" + } + ], + "retained_files_byte_identical": { + ".gitattributes": "8d3eea09c326d8636669849bb00208a26ec4a709dfdaa505c9fdec253798dfa3", + "CLAIM.json": "26eeeaa2027af5e90e7edb40be533a549b7197211599ab2c21f9087e354dbc76", + "evidence/environment.json": "7a7fe94aaf9af7d585426260c51505685397ec836b44094d78fe353a92e2bdfd", + "evidence/package-tests.txt": "32e8de78ad3ff79dcdd0f162cfbd5f01dc031a39f346f76c57ecba288befaf91", + "evidence/verify.txt": "953432aa42f96318eb5cfe65e1d0f17a3dc0f75ca60e5e57a04fc00d4136dd9a", + "EXPECTED.json": "9e019e77443a9fc1c4938d9d03d809d813de0558581fecf2fb72efef48f4bdcc", + "LICENSE": "c71d239df91726fc519c6eb72d318ec65820627232b2f796219e87dcf35d0ab4", + "test_package.py": "287632c4632bd0de696cad3d5170eae1c15b739802a194143941abf7c41fa03d", + "vendor/previous-fourier-NOTICE.md": "05e6e660b74d34a8ed298f41889b9bb8b7fe365137bf2179f9828cdd2bb9a8b7", + "vendor/previous-fourier-PROOF.md": "0dd5ff1a4377f4eeb92b3af7b75254bb343c64675b09201db132b394b0ebaaad", + "vendor/prime-power-NOTICE.md": "96111c95cfec3c03a6f69c8e02c5d0bceff957d187e638d0534c676d6e3ffd77", + "vendor/prime-power-proof.md": "2b8056c88e66f692f407450fff0414d41bcd09db8597be22e274a6c3dc20eb9e", + "vendor/selected-result.json": "b3bf402f31a69bde0629936a9b569bed48281568d7b16d5fba120b5311ea1f53", + "verify.py": "b40f04343586a17a8a6debb22408c30e7ed8265cbce9b079bcdddce4f0c9da6d" + }, + "immutable_source_entries_unchanged": true, + "revised_analytic_texts": { + "NOTICE.md": "6e211502bc80038dcf2551dc914b77bc9603c8fb3c0c865268ba494102e73355", + "PROOF.md": "6c28d93d9d1d37da0bbc3876070ef8c6f0f5dad8e186b31b31330028e5420c0e", + "README.md": "77dcfe10cf69b66e092c4bf9501353cd82e61d899fca0b983f60dec25e012c4f", + "SOURCES.json": "d7f49b44d77321ac7da6b0b0652763518131474e28f23e1053706d7db3aa4e3e", + "VALIDATION.md": "23fa4a9731257ffdc1eb1f6b8614e43768c110c0d41d94315d45c030da2d5f47", + "audit/README.md": "8bfb503f127187d77697b8fca3e81bb93c5ef962a560898a6d737a0d5d0dd717", + "audit/TASK.json": "16339fdf45fa099d6d6e3f7371c73e98f6fcea2e4978844327f221a99fe96f0d" + }, + "analytic_status": "Written author/AI source and proof audit in audit/README.md. The PASS markers are finite/package checks, not certification of the theorem.", + "not_run": [ + "PR621 foundation replay", + "Full repository make verify", + "Selected-supplier cold replay", + "Second-platform replay", + "Proof-assistant formalization" + ], + "not_claimed": [ + "Independent human analytic review", + "Maintainer acceptance", + "Complete multiplication theorem", + "New kappa" + ] +} diff --git a/research/rational-circle-bound/audit/package-tests.txt b/research/rational-circle-bound/audit/package-tests.txt new file mode 100644 index 0000000000..02ca4a0917 --- /dev/null +++ b/research/rational-circle-bound/audit/package-tests.txt @@ -0,0 +1,9 @@ +PASS pristine relocated optimized +PASS source bytes drift +PASS wrong source Git blob +PASS unrecorded proof drift +PASS changed expected budget +PASS lost reflection conjugation +PASS wrong closure denominator sign +PASS refuse expected overwrite +{"count": 8, "seconds": 18.563, "status": "PASS_PACKAGE_CONTROLS", "tests": ["pristine relocated optimized", "source bytes drift", "wrong source Git blob", "unrecorded proof drift", "changed expected budget", "lost reflection conjugation", "wrong closure denominator sign", "refuse expected overwrite"]} diff --git a/research/rational-circle-bound/audit/verify.txt b/research/rational-circle-bound/audit/verify.txt new file mode 100644 index 0000000000..122f0785fa --- /dev/null +++ b/research/rational-circle-bound/audit/verify.txt @@ -0,0 +1,2 @@ +PASS_RATIONAL_CIRCLE_BOUND +{"controls": 21, "cyclic_inverses": {"cases": 546, "inverse_entries": 9516, "nonzero_noncoprime_cases": 78, "zero_stride_cases": 195}, "hilbert": {"comparisons": 6565, "exhaustive_length": 4, "exhaustive_vectors_each_side": 81, "long_lengths": [8, 16, 32, 64]}, "near_circle_families": 128, "radix_budgets": 14, "reflection": {"all_inner": 33, "all_outer": 18, "boundary_points": 756, "contains_repetition": 37, "contains_zero": 32, "families": 126}}