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..c3f983535a --- /dev/null +++ b/research/rational-circle-bound/MANIFEST.json @@ -0,0 +1,29 @@ +{ + "schema": 1, + "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", + "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" + } +} diff --git a/research/rational-circle-bound/NOTICE.md b/research/rational-circle-bound/NOTICE.md new file mode 100644 index 0000000000..75f764b802 --- /dev/null +++ b/research/rational-circle-bound/NOTICE.md @@ -0,0 +1,57 @@ +# 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, +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. 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. **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. +**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. + +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 new file mode 100644 index 0000000000..15d344789d --- /dev/null +++ b/research/rational-circle-bound/PROOF.md @@ -0,0 +1,359 @@ +# 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. + +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 +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. 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 + +\[ + \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. 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, +\] + +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. +\] + +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 +(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} +\] + +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). +\] + +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. +\] + +Integrating over 0<=phi<2pi, the integral of +|Re(e^{-i phi}v)| is 4|v| for every complex v. Hence +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, 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. +\] + +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. 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 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: + +\[ + 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 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 | +|---|---|---| +| 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, +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 new file mode 100644 index 0000000000..1a1d3068a8 --- /dev/null +++ b/research/rational-circle-bound/README.md @@ -0,0 +1,103 @@ +# 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 + +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 +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 +Ryan Pinto (@Ambassators) 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. + +## 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 new file mode 100644 index 0000000000..b0e1e27908 --- /dev/null +++ b/research/rational-circle-bound/SOURCES.json @@ -0,0 +1,121 @@ +{ + "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.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", + "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": "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": "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": [ + { + "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.", + "head": "c5b53a5e80372a1fae9830d8dcf21aaabce3f729", + "author": "Ryan Pinto (@Ambassators)" + }, + { + "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." + }, + { + "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 new file mode 100644 index 0000000000..33e131643d --- /dev/null +++ b/research/rational-circle-bound/VALIDATION.md @@ -0,0 +1,87 @@ +# 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 +`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/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}} 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()