diff --git a/research/fixed-budget-hidden-windows/LICENSE b/research/fixed-budget-hidden-windows/LICENSE new file mode 100644 index 0000000000..261eeb9e9f --- /dev/null +++ b/research/fixed-budget-hidden-windows/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/fixed-budget-hidden-windows/NOTICE b/research/fixed-budget-hidden-windows/NOTICE new file mode 100644 index 0000000000..c9c20c4b7e --- /dev/null +++ b/research/fixed-budget-hidden-windows/NOTICE @@ -0,0 +1,13 @@ +Prepared with substantial OpenAI Codex assistance, 2026-10-28. +Apache-2.0. No independent human or proof-assistant acceptance is claimed. + +The two inert exports under sources/ are unmodified from zxv's +research/hidden-power-windows package, PR6049 of CrocSwap/integer-mult-bounds, +commit 2646b6d67ceb74b9868e632f3a27312d8be62a0e. Its attribution is retained +in the source README. It credits Nick Petalas's PR5174 polynomial-to-invoice +precursor and Ali Romman's root-budget work. + +The repository notice is retained in UPSTREAM-NOTICE.txt. This package's +new files contain the scoped budget-width argument, exact checks and boundary +counterexamples. The separate AI review contributed the discrete strengthening. +This is not an official OpenAI release or an OpenAI endorsement. diff --git a/research/fixed-budget-hidden-windows/PROOF.md b/research/fixed-budget-hidden-windows/PROOF.md new file mode 100644 index 0000000000..f6b886f3ce --- /dev/null +++ b/research/fixed-budget-hidden-windows/PROOF.md @@ -0,0 +1,251 @@ +# A sharp call-budget bound for the hidden windows in PR6049 + +This resolves a restricted version of the fixed-budget question stated in +[PR6049](https://github.com/CrocSwap/integer-mult-bounds/pull/6049): its minimal +power-of-two rank alphabet. The proof also permits irrational interior roots. +It does not resolve the question for arbitrary rank alphabets or larger support. + +## Statement and normalization + +Fix an integer h >= 1. Let A_j and B_j be nonnegative **integers**, indexed by +j=0,...,2h+2, representing paid calls of rank 2^j. Suppose each profile contains +at most N calls, for a positive integer budget N. Put + + Q(x) = sum_j (B_j - A_j) x^j, + F(p) = Q(2^p). + +Assume F has a zero of multiplicity at least h at each of p=0 and p=1, and +two distinct interior zeros alpha < beta in (0,1), with F positive between +them (the losing window for B relative to A). Then, writing w=beta-alpha, + + w > 2 * 6^h / (N * ln(2)). (1) + +For h=1 the ranks are {1,2,4,8,16}, and the numerator is 12. The constant +2*6^h/ln(2) in a bound of the form w > constant/N is asymptotically optimal. +This is an infimum over all eligible budgets and profiles. A stronger discrete +bound below proves exact optimality at an infinite sequence of budgets, but +we do not give a closed formula for the exact optimum at every finite N. + +The budget N is **per profile**, including any common paid calls. The endpoint +condition already implies equal counts and equal rank mass, so the combined +two-profile count is T=2N_actual. With a combined-count budget T_max, (1) +becomes w > 4*6^h/(T_max*ln(2)). Using N for the sum of both profiles would +lose a factor of two. Replacing p by the saving coordinate C=1-p preserves w. + +## Integer quadratic reduction + +The substitution x=2^p is analytic with nonzero derivative, so it preserves +zero multiplicities at x=1 and x=2. Let r=2^alpha and s=2^beta. The nonzero +polynomial Q has degree at most 2h+2, and already has at least 2h+2 roots +counted with multiplicity: h each at 1 and 2, and one each at r and s. +Thus its degree is exactly 2h+2, its endpoint multiplicities are exactly h, +and its two interior roots are simple. Division by the monic integer factors +(x-1)^h and (x-2)^h leaves an integer quadratic. Choose its orientation as + + Q(x) = epsilon * (x-1)^h * (x-2)^h * R(x), + R(x) = a*x^2 + b*x + c = a*(x-r)*(x-s), a > 0, + epsilon = (-1)^(h+1), 1 < r < s < 2. + +The stated epsilon follows from positivity of Q on (r,s). All other signs +are then forced: Q is negative on (1,r) and (s,2). The discriminant + + Delta = b^2 - 4*a*c = a^2*(s-r)^2 + +is a positive integer, hence Delta >= 1. Rational roots are not required. + +## Recovering the count from the coefficients + +Every root of Q is positive. Expanding its product of real linear factors +therefore yields alternating, strictly nonzero coefficients. In particular, +all 2h+3 ranks occur in the difference, even though the premise only restricted +the allowed alphabet. It follows that + + sum_j |q_j| = |Q(-1)| + = 6^h * a*(1+r)*(1+s) + = 6^h * (a-b+c), q_j = B_j-A_j. + +Because Q(1)=0, its positive and negative coefficient sums agree. Write their +common value as W. This is the number of calls on either side after cancelling +calls shared by the profiles: + + W = (6^h/2) * a*(1+r)*(1+s) = (6^h/2)*(a-b+c), + sum A_j = sum B_j = W + sum_j min(A_j,B_j) <= N. (2) + +This cancellation identity is why common padding cannot evade the bound. +No rank mass, productive target or compiler charge is substituted for W. + +## Width inequality + +For every x>1, + + 1/x - 4/(1+x)^2 = (x-1)^2 / [x*(1+x)^2] > 0. + +Integrating from r to s gives the strict inequality + + ln(s/r) > 4*(s-r) / [(1+r)*(1+s)]. (3) + +Multiplying (3) by (2) proves the stronger discriminant-sensitive statement + + W * ln(s/r) > 2*6^h * a*(s-r) + = 2*6^h * sqrt(Delta). + +Consequently + + w > 2*6^h*sqrt(Delta) / [W*ln(2)] + >= 2*6^h / [N*ln(2)], + +as claimed. The proof is uniform in h and N. The finite checker does not +supply or replace the integration, degree-counting or limiting arguments. + +## Sharpness of the universal constant + +For any integer n>=3 take + + r_n = (n+1)/n, s_n = n/(n-1), + R_n(x) = (n*x-(n+1))*((n-1)*x-n) + = n*(n-1)*x^2 - (2*n^2-1)*x + n*(n+1). + +These roots lie strictly between 1 and 2, and Delta=1. Form Q with the +endpoint factors and orientation above, and use its positive and negative +coefficients as the disjoint integer profiles. They satisfy every premise, +with + + N = W_h(n) = (6^h/2)*(4*n^2-1), + w_n = log_2(n^2/(n^2-1)). + +For x>0, ln(1+x)=1, + z <= Z = floor((floor(N/S)-1)/2). + +The positive roots imply z>sqrt(Delta)>=1, so Z>1 for every eligible input. +The root ratio is + + s/r = (z+sqrt(Delta))/(z-sqrt(Delta)). + +For positive denominators this ratio increases with sqrt(Delta) and decreases +with z. Hence + + w >= log_2((Z+1)/(Z-1)). (4) + +Equivalently, the ratio comparison follows by positive cross multiplication +from Z*sqrt(Delta)>=z, whose square is the exact integer comparison +Z^2*Delta>=z^2. No numerical logarithm is needed to certify that comparison. + +For the family above, k=1, Delta=1, N=S*(4*n^2-1), and Z=z=2*n^2-1. +Equality holds in (4). Therefore that family **exactly minimizes width among +all eligible profiles with at most S*(4*n^2-1) calls per side**, including +those with irrational roots or common padding. This establishes exact +finite-budget optima at those budgets, not just asymptotic sharpness. + +The family need not remain optimal between those budgets. At h=1,N=120, +R=6*x^2-19*x+15 has roots 3/2 and 5/3, W=120, and width log_2(10/9), +less than the n=3 family's log_2(9/8). It also attains (4), with Z=19. +For other budgets the discrete bound need not be attained; this handoff makes +no general attainability claim. + +The identity ln(s/r)=2*atanh(sqrt(Delta)/z)>2*sqrt(Delta)/z also proves +the strictly stronger continuous estimate + + w > 2*6^h / [(W-S)*ln(2)] + >= 2*6^h / [(N-S)*ln(2)]. (5) + +All denominators here are positive for eligible profiles. The elementary +integral proof of (1) remains a separate cross-check of the normalization. + +## Exact bounded search at N=1000 + +For h=1, write b=-z. Every eligible quadratic obeys + + 1 <= a < N/12, 2*a < z < 4*a, + max(z-a+1,2*z-4*a+1) <= c + <= min(floor((z^2-1)/(4*a)), floor(N/3)-a-z). + +These inequalities are both necessary and sufficient: they respectively +place the vertex inside (1,2), make the endpoint values positive, make the +minimum negative, and impose W=3*(a+z+c)<=N. They give a finite, exhaustive +enumeration, not a random search. Since + + w = log_2((1+sqrt(Delta/z^2))/(1-sqrt(Delta/z^2))), + +minimizing width is exactly equivalent to minimizing the rational Delta/z^2. +The checker enumerates all 8,158 quadratics with N=1000, including 899 rational +and 7,259 irrational root pairs. Its exact minimum is 1/25921=1/161^2, giving +width log_2(81/80). There are two minimizing oriented quadratics: + + 60*x^2 - 161*x + 108, W=987, + 72*x^2 - 161*x + 90, W=969. + +Both have Delta=1. Common padding is not counted as a new quadratic. This is +a finite computation corroborated by a separate coefficient-simplex census; +it does not furnish a closed formula for every N. + +## A rational mesh consequence, with its exact scope + +The strict convexity of 1/x gives the composite trapezoidal upper bound + + ln(2) < (1/4)*(1/2 + 4/5 + 2/3 + 4/7 + 1/4) + = 1171/1680 < 7/10. + +Therefore every window covered by the theorem has + + w > 20*6^h/(7*N). + +A uniform grid {k/m: 0<=k<=m} with + + m = ceil(7*N/(20*6^h)) + +has maximum gap at most this lower bound and must contain a grid point +strictly inside any such window. This explains how a known integer call +budget changes the fixed-grid obstruction in this specific class. It does +not certify arbitrary exponential sums, a larger rank alphabet, a different +zero pattern, or any physical supplier. The underlying quadratic can also +be analyzed directly; this is a consequence for sampling, not a claim that +sampling is the best algorithm. + +## Dependencies, credit, and uncertainty + +The project-specific starting point is zxv's PR6049 at commit +2646b6d67ceb74b9868e632f3a27312d8be62a0e, including its explicit open +fixed-budget question. That work credits Nick Petalas's PR5174 threshold +construction and Ali Romman's root-budget work. The polynomial-to-profile +construction, endpoint multiplicity framework and minimal-support result +belong to those predecessors. Integer discriminants, alternating +coefficients of positive-root polynomials, the logarithmic integral and +adjacent rational fractions are classical tools. + +The contribution here is the stated sharp budget-width inequality for this +alphabet, its integer-quadratic extension and explicit sharpness family. +No global novelty claim is made. This is a focused follow-up to PR6049's +explicit fixed-budget question. The exact optimum at general finite N, beyond +the attained cases and bounded census above, and the arbitrary-rank problem +remain open here. The independent AI review contributed the stronger discrete +argument (4) and shifted continuous argument (5). This proof and its checks +were produced with substantial OpenAI Codex assistance, including GPT-6 Astra +and separate AI review. Neither independent human review nor proof-assistant +verification is claimed. The included scope counterexamples delimit, rather +than enlarge, the hypotheses of the main theorem. diff --git a/research/fixed-budget-hidden-windows/README.md b/research/fixed-budget-hidden-windows/README.md new file mode 100644 index 0000000000..111531111d --- /dev/null +++ b/research/fixed-budget-hidden-windows/README.md @@ -0,0 +1,126 @@ +# Fixed call budgets limit PR6049's hidden power windows + +This is a scoped follow-up to [PR6049](https://github.com/CrocSwap/integer-mult-bounds/pull/6049) +and its [canonical investigation](https://github.com/CrocSwap/integer-mult-bounds/discussions/6052). +It addresses the fixed-budget question for the minimal power-of-two alphabet. +It supplies arithmetic profiles, not a native supplier or a new kappa. + +## Claim + +Let h>=1 and N>=1 be integers. Let A_j,B_j be nonnegative integer call counts +on ranks 2^j, 0<=j<=2h+2, with at most N calls **per profile**. Put +F(p)=sum_j(B_j-A_j)2^(jp). Assume zeros of multiplicity at least h at p=0,1, +and two distinct interior zeros alpha0 on (alpha,beta). +The endpoint conditions include equal call count and rank mass. Then + + beta-alpha > 2*6^h / (N*ln(2)). + +The constant is asymptotically sharp. Irrational quadratic interior roots and +common paid padding are included. Define S=6^h/2 and +Z=floor((floor(N/S)-1)/2). Every eligible pair also satisfies + + beta-alpha >= log_2((Z+1)/(Z-1)), + beta-alpha > 2*6^h / ((N-S)*ln(2)). + +Eligible inputs have Z>=2 and N>S. The discrete bound is attained at every +N=S*(4*n^2-1), n>=3, by residual +(n*x-n-1)*((n-1)*x-n). This proves exact finite-budget optima on that infinite +sequence, not attainment at every budget. + +[PROOF.md](PROOF.md) gives the degree reduction, integer discriminant, +half-L1 normalization, trace bound, equality cases and rational mesh consequence. +For h=1,N=1000, all 8,158 eligible integer quadratics are enumerated exactly. +The minimum width is log_2(81/80), attained by 60x^2-161x+108 (987 calls) +and 72x^2-161x+90 (969 calls). The independent shifted-coordinate census agrees. + +## Scope boundaries + +[SCOPE-COUNTEREXAMPLES.md](SCOPE-COUNTEREXAMPLES.md) and the independent checker +give exact controls against extending the result without its hypotheses: + +- Seven ranks with simple endpoint zeros (h=1, larger support) admit a + two-crossing family of width Theta(N^(-3/2)); no positive universal + constant/N lower bound holds there. This is not a counterexample to the + h=2 seven-rank theorem, which requires double endpoint zeros. +- One interior crossing can produce an edge loss missed by the stated mesh. +- The same numerical constant does not transfer unchanged to a different + five-rank alphabet. + +The theorem is specific to integer multiplicities, the specified power-of-two +alphabet and endpoint/interior-zero pattern. It does not resolve arbitrary +rank alphabets, legal supplier realizability, the selected compiler, or any +of the five retained framework assumptions. It does not alter the selected +conditional kappa 781451/250000000. Finite checks corroborate the written +proof and are not a formal verification of its uniform mathematical statements. + +## Reproduce + +From the repository root, using Python 3.10+ standard-library features: + +```sh +python3 -I -B research/fixed-budget-hidden-windows/replay.py +``` + +The replay runs the main and independent verifiers and unit tests in normal +and optimized modes, serially, with a 30-second timeout per command. It checks +both JSON outputs against the saved receipts and writes no package files. +Individual entry points are: + +```sh +python3 -I -B research/fixed-budget-hidden-windows/verify.py +python3 -I -B research/fixed-budget-hidden-windows/independent_check.py +``` + +The main verifier uses exact integer/Fraction arithmetic, directed square-root +enclosures and a positive logarithm series with a rigorous tail bound. The +independent verifier uses shifted coefficients and exact Sturm root counting. +Acceptance does not depend on floating-point arithmetic. The interval helper +is conservatively incomplete at extreme inputs: a valid n=10^20 profile passes +the integer certificate but its tiny strict margin is lost at the fixed printed +precision. The built-in fixtures, through n=10^9, pass. The proof is uniform. + +Runs used CPython 3.14.7. Python 3.10 syntax/API compatibility was inspected, +not tested on a 3.10 runtime. No dependencies, network, Git, upstream Python +execution or selected-supplier replay are needed by these direct commands. +No shared CI or selected-record files are changed. This standalone package +does not opt into the repository's generic research-package metadata workflow. + +## Sources, credit and review + +Base main: 721c03822c421b7f7fcbb2598993b947c4d88419. +PR6049 head: 2646b6d67ceb74b9868e632f3a27312d8be62a0e. +[SOURCES.json](SOURCES.json) records the exact paths, commit, Git blob IDs, +SHA256 hashes and public URLs for two unmodified inert source exports. +The verifier pins that manifest and checks the exported byte hashes and Git +blob hashes. Commit/path attribution is recorded; the full offline commit-tree +chain is not included in this compact package. No publication ancestry claim +is inferred from a matching blob hash. + +zxv's PR6049 supplies the hidden-window construction, endpoint-multiplicity +framework and minimal support result. Its credited predecessors include +[Nick Petalas's PR5174](https://github.com/CrocSwap/integer-mult-bounds/pull/5174) +and Ali Romman's root-budget work. The new scope is the budget-width bounds, +attained cases, finite census and explicit boundary counterexamples. The proof +uses classical polynomial/discriminant and logarithmic inequalities; no global +novelty claim is made. Repository license and upstream notices are retained. + +Prepared with substantial OpenAI Codex assistance, including GPT-6 Astra, +and separate AI proof/implementation review. AI reviewers contributed the +stronger discrete argument and scope counterexamples. No independent human +review, proof-assistant acceptance or maintainer approval is claimed. + +Human review is requested for the degree and endpoint hypotheses, per-profile +normalization, discrete inequality and equality case, census completeness, +and seven-rank counterexample family. An archival merge alone would not +establish scientific acceptance. + +## Open next questions + +1. Characterize the budgets at which the discrete lower bound is attainable. + This would distinguish a general lower bound from an exact optimum. A first + step is to classify integer quadratics with Delta=1, -b=Z and both roots in + (1,2). The unresolved part is the arithmetic feasibility classification. +2. Determine sharp budget-width bounds for the seven-rank class. The included + family rules out constant/N but does not identify the optimal rate. A first + step is a coefficient-height separation bound for the quartic residual. + A matching lower bound is not established in this package. diff --git a/research/fixed-budget-hidden-windows/RESULT.json b/research/fixed-budget-hidden-windows/RESULT.json new file mode 100644 index 0000000000..5dc242c73d --- /dev/null +++ b/research/fixed-budget-hidden-windows/RESULT.json @@ -0,0 +1,755 @@ +{ + "census": { + "all_minimizing_quadratics": [ + { + "actual_calls_per_profile": 987, + "bound_numerator": 12, + "budget_per_profile": 1000, + "budget_trace_cap": 166, + "common_calls": 0, + "count_scale": 3, + "discrete_bound_attained": false, + "discrete_width_ratio_lower": "167/165", + "discriminant": 1, + "endpoint_residual_value": 7, + "h": 1, + "quadratic": [ + 108, + -161, + 60 + ], + "rank_mass_per_profile": 4020, + "rational_roots": true, + "stronger_continuous_bound_denominator": 997, + "support_size": 5, + "trace": 161, + "uncancelled_calls_per_profile": 987 + }, + { + "actual_calls_per_profile": 969, + "bound_numerator": 12, + "budget_per_profile": 1000, + "budget_trace_cap": 166, + "common_calls": 0, + "count_scale": 3, + "discrete_bound_attained": false, + "discrete_width_ratio_lower": "167/165", + "discriminant": 1, + "endpoint_residual_value": 1, + "h": 1, + "quadratic": [ + 90, + -161, + 72 + ], + "rank_mass_per_profile": 4200, + "rational_roots": true, + "stronger_continuous_bound_denominator": 997, + "support_size": 5, + "trace": 161, + "uncancelled_calls_per_profile": 969 + } + ], + "budget_per_profile": 1000, + "h": 1, + "irrational_root_pairs": 7259, + "minimum_Delta_over_trace_squared": "1/25921", + "objective": "minimize Delta/trace^2; width is strictly increasing in this quantity", + "ordered_certificate_sha256": "a52aec041bff97d68f527ee7b23810ceac3eb0ccfc8c48e74af7b8f0969c7f05", + "quadratics": 8158, + "rational_root_pairs": 899 + }, + "claim_type": "scoped theorem with finite exact corroboration", + "irrational_examples": [ + { + "actual_calls_per_profile": 93, + "bound_numerator": 12, + "budget_per_profile": 1000, + "budget_trace_cap": 166, + "common_calls": 0, + "count_scale": 3, + "discrete_bound_attained": false, + "discrete_width_ratio_lower": "167/165", + "discriminant": 5, + "endpoint_residual_value": 1, + "h": 1, + "interval_check": { + "normalized_ratio_lower": "792160694280153706079168764842827228347/340282366920938463463374607431768211456", + "normalized_ratio_upper": "198040173570038426519792191210706807087/85070591730234615865843651857942052864", + "strict_bound_certified": true + }, + "quadratic": [ + 11, + -15, + 5 + ], + "rank_mass_per_profile": 366, + "rational_roots": false, + "stronger_continuous_bound_denominator": 997, + "support_size": 5, + "trace": 15, + "uncancelled_calls_per_profile": 93 + }, + { + "actual_calls_per_profile": 111, + "bound_numerator": 12, + "budget_per_profile": 1000, + "budget_trace_cap": 166, + "common_calls": 0, + "count_scale": 3, + "discrete_bound_attained": false, + "discrete_width_ratio_lower": "167/165", + "discriminant": 12, + "endpoint_residual_value": 1, + "h": 1, + "interval_check": { + "normalized_ratio_lower": "76675925446733846540062368671882147411/21267647932558653966460912964485513216", + "normalized_ratio_upper": "1226814807147741544640997898750114358577/340282366920938463463374607431768211456", + "strict_bound_certified": true + }, + "quadratic": [ + 13, + -18, + 6 + ], + "rank_mass_per_profile": 438, + "rational_roots": false, + "stronger_continuous_bound_denominator": 997, + "support_size": 5, + "trace": 18, + "uncancelled_calls_per_profile": 111 + }, + { + "actual_calls_per_profile": 123, + "bound_numerator": 12, + "budget_per_profile": 1000, + "budget_trace_cap": 166, + "common_calls": 0, + "count_scale": 3, + "discrete_bound_attained": false, + "discrete_width_ratio_lower": "167/165", + "discriminant": 8, + "endpoint_residual_value": 1, + "h": 1, + "interval_check": { + "normalized_ratio_lower": "993182377405144134861919344585967356001/340282366920938463463374607431768211456", + "normalized_ratio_upper": "496591188702572067430959672292983678001/170141183460469231731687303715884105728", + "strict_bound_certified": true + }, + "quadratic": [ + 14, + -20, + 7 + ], + "rank_mass_per_profile": 492, + "rational_roots": false, + "stronger_continuous_bound_denominator": 997, + "support_size": 5, + "trace": 20, + "uncancelled_calls_per_profile": 123 + }, + { + "actual_calls_per_profile": 129, + "bound_numerator": 12, + "budget_per_profile": 1000, + "budget_trace_cap": 166, + "common_calls": 0, + "count_scale": 3, + "discrete_bound_attained": false, + "discrete_width_ratio_lower": "167/165", + "discriminant": 21, + "endpoint_residual_value": 1, + "h": 1, + "interval_check": { + "normalized_ratio_lower": "1622588396551426337533870035460953514939/340282366920938463463374607431768211456", + "normalized_ratio_upper": "405647099137856584383467508865238378735/85070591730234615865843651857942052864", + "strict_bound_certified": true + }, + "quadratic": [ + 15, + -21, + 7 + ], + "rank_mass_per_profile": 510, + "rational_roots": false, + "stronger_continuous_bound_denominator": 997, + "support_size": 5, + "trace": 21, + "uncancelled_calls_per_profile": 129 + }, + { + "actual_calls_per_profile": 138, + "bound_numerator": 12, + "budget_per_profile": 1000, + "budget_trace_cap": 166, + "common_calls": 0, + "count_scale": 3, + "discrete_bound_attained": false, + "discrete_width_ratio_lower": "167/165", + "discriminant": 8, + "endpoint_residual_value": 2, + "h": 1, + "interval_check": { + "normalized_ratio_lower": "505905870932002558760533799759333865415/170141183460469231731687303715884105728", + "normalized_ratio_upper": "1011811741864005117521067599518667730831/340282366920938463463374607431768211456", + "strict_bound_certified": true + }, + "quadratic": [ + 17, + -22, + 7 + ], + "rank_mass_per_profile": 534, + "rational_roots": false, + "stronger_continuous_bound_denominator": 997, + "support_size": 5, + "trace": 22, + "uncancelled_calls_per_profile": 138 + }, + { + "actual_calls_per_profile": 141, + "bound_numerator": 12, + "budget_per_profile": 1000, + "budget_trace_cap": 166, + "common_calls": 0, + "count_scale": 3, + "discrete_bound_attained": false, + "discrete_width_ratio_lower": "167/165", + "discriminant": 17, + "endpoint_residual_value": 1, + "h": 1, + "interval_check": { + "normalized_ratio_lower": "724589780474302675846846030784109470481/170141183460469231731687303715884105728", + "normalized_ratio_upper": "1449179560948605351693692061568218940963/340282366920938463463374607431768211456", + "strict_bound_certified": true + }, + "quadratic": [ + 16, + -23, + 8 + ], + "rank_mass_per_profile": 564, + "rational_roots": false, + "stronger_continuous_bound_denominator": 997, + "support_size": 5, + "trace": 23, + "uncancelled_calls_per_profile": 141 + }, + { + "actual_calls_per_profile": 147, + "bound_numerator": 12, + "budget_per_profile": 1000, + "budget_trace_cap": 166, + "common_calls": 0, + "count_scale": 3, + "discrete_bound_attained": false, + "discrete_width_ratio_lower": "167/165", + "discriminant": 32, + "endpoint_residual_value": 1, + "h": 1, + "interval_check": { + "normalized_ratio_lower": "2002683162014327244442633293182898407709/340282366920938463463374607431768211456", + "normalized_ratio_upper": "1001341581007163622221316646591449203855/170141183460469231731687303715884105728", + "strict_bound_certified": true + }, + "quadratic": [ + 17, + -24, + 8 + ], + "rank_mass_per_profile": 582, + "rational_roots": false, + "stronger_continuous_bound_denominator": 997, + "support_size": 5, + "trace": 24, + "uncancelled_calls_per_profile": 147 + }, + { + "actual_calls_per_profile": 156, + "bound_numerator": 12, + "budget_per_profile": 1000, + "budget_trace_cap": 166, + "common_calls": 0, + "count_scale": 3, + "discrete_bound_attained": false, + "discrete_width_ratio_lower": "167/165", + "discriminant": 17, + "endpoint_residual_value": 2, + "h": 1, + "interval_check": { + "normalized_ratio_lower": "1472590683270143020114750239705409512511/340282366920938463463374607431768211456", + "normalized_ratio_upper": "23009229426095984689292972495397023633/5316911983139663491615228241121378304", + "strict_bound_certified": true + }, + "quadratic": [ + 19, + -25, + 8 + ], + "rank_mass_per_profile": 606, + "rational_roots": false, + "stronger_continuous_bound_denominator": 997, + "support_size": 5, + "trace": 25, + "uncancelled_calls_per_profile": 156 + }, + { + "actual_calls_per_profile": 153, + "bound_numerator": 12, + "budget_per_profile": 1000, + "budget_trace_cap": 166, + "common_calls": 0, + "count_scale": 3, + "discrete_bound_attained": false, + "discrete_width_ratio_lower": "167/165", + "discriminant": 13, + "endpoint_residual_value": 1, + "h": 1, + "interval_check": { + "normalized_ratio_lower": "1260230228559995297385396774930954130919/340282366920938463463374607431768211456", + "normalized_ratio_upper": "157528778569999412173174596866369266365/42535295865117307932921825928971026432", + "strict_bound_certified": true + }, + "quadratic": [ + 17, + -25, + 9 + ], + "rank_mass_per_profile": 618, + "rational_roots": false, + "stronger_continuous_bound_denominator": 997, + "support_size": 5, + "trace": 25, + "uncancelled_calls_per_profile": 153 + }, + { + "actual_calls_per_profile": 159, + "bound_numerator": 12, + "budget_per_profile": 1000, + "budget_trace_cap": 166, + "common_calls": 0, + "count_scale": 3, + "discrete_bound_attained": false, + "discrete_width_ratio_lower": "167/165", + "discriminant": 28, + "endpoint_residual_value": 1, + "h": 1, + "interval_check": { + "normalized_ratio_lower": "930609766373781584890625109610658660489/170141183460469231731687303715884105728", + "normalized_ratio_upper": "1861219532747563169781250219221317320979/340282366920938463463374607431768211456", + "strict_bound_certified": true + }, + "quadratic": [ + 18, + -26, + 9 + ], + "rank_mass_per_profile": 636, + "rational_roots": false, + "stronger_continuous_bound_denominator": 997, + "support_size": 5, + "trace": 26, + "uncancelled_calls_per_profile": 159 + }, + { + "actual_calls_per_profile": 165, + "bound_numerator": 12, + "budget_per_profile": 1000, + "budget_trace_cap": 166, + "common_calls": 0, + "count_scale": 3, + "discrete_bound_attained": false, + "discrete_width_ratio_lower": "167/165", + "discriminant": 45, + "endpoint_residual_value": 1, + "h": 1, + "interval_check": { + "normalized_ratio_lower": "2374647889748929448307141601087925176949/340282366920938463463374607431768211456", + "normalized_ratio_upper": "1187323944874464724153570800543962588475/170141183460469231731687303715884105728", + "strict_bound_certified": true + }, + "quadratic": [ + 19, + -27, + 9 + ], + "rank_mass_per_profile": 654, + "rational_roots": false, + "stronger_continuous_bound_denominator": 997, + "support_size": 5, + "trace": 27, + "uncancelled_calls_per_profile": 165 + }, + { + "actual_calls_per_profile": 174, + "bound_numerator": 12, + "budget_per_profile": 1000, + "budget_trace_cap": 166, + "common_calls": 0, + "count_scale": 3, + "discrete_bound_attained": false, + "discrete_width_ratio_lower": "167/165", + "discriminant": 28, + "endpoint_residual_value": 2, + "h": 1, + "interval_check": { + "normalized_ratio_lower": "1887601923710325597716015530419620216909/340282366920938463463374607431768211456", + "normalized_ratio_upper": "943800961855162798858007765209810108455/170141183460469231731687303715884105728", + "strict_bound_certified": true + }, + "quadratic": [ + 21, + -28, + 9 + ], + "rank_mass_per_profile": 678, + "rational_roots": false, + "stronger_continuous_bound_denominator": 997, + "support_size": 5, + "trace": 28, + "uncancelled_calls_per_profile": 174 + } + ], + "limitations": [ + "minimal power-of-two alphabet only", + "integer multiplicities", + "not an exact optimum for each finite budget", + "no legal supplier construction or new kappa", + "finite checks do not replace the written uniform proof" + ], + "log2_upper_rational": "1171/1680", + "sharpness_fixtures": [ + { + "calls_per_profile": 105, + "discrete_bound_attained": true, + "discriminant": 1, + "exact_width": "log2(9/8)", + "h": 1, + "n": 3, + "normalized_ratio_upper_squeeze": "35/32", + "strict_bound_certified": true + }, + { + "calls_per_profile": 189, + "discrete_bound_attained": true, + "discriminant": 1, + "exact_width": "log2(16/15)", + "h": 1, + "n": 4, + "normalized_ratio_upper_squeeze": "21/20", + "strict_bound_certified": true + }, + { + "calls_per_profile": 1197, + "discrete_bound_attained": true, + "discriminant": 1, + "exact_width": "log2(100/99)", + "h": 1, + "n": 10, + "normalized_ratio_upper_squeeze": "133/132", + "strict_bound_certified": true + }, + { + "calls_per_profile": 119997, + "discrete_bound_attained": true, + "discriminant": 1, + "exact_width": "log2(10000/9999)", + "h": 1, + "n": 100, + "normalized_ratio_upper_squeeze": "13333/13332", + "strict_bound_certified": true + }, + { + "calls_per_profile": 1199999997, + "discrete_bound_attained": true, + "discriminant": 1, + "exact_width": "log2(100000000/99999999)", + "h": 1, + "n": 10000, + "normalized_ratio_upper_squeeze": "133333333/133333332", + "strict_bound_certified": true + }, + { + "calls_per_profile": 11999999999999999997, + "discrete_bound_attained": true, + "discriminant": 1, + "exact_width": "log2(1000000000000000000/999999999999999999)", + "h": 1, + "n": 1000000000, + "normalized_ratio_upper_squeeze": "1333333333333333333/1333333333333333332", + "strict_bound_certified": true + }, + { + "calls_per_profile": 630, + "discrete_bound_attained": true, + "discriminant": 1, + "exact_width": "log2(9/8)", + "h": 2, + "n": 3, + "normalized_ratio_upper_squeeze": "35/32", + "strict_bound_certified": true + }, + { + "calls_per_profile": 1134, + "discrete_bound_attained": true, + "discriminant": 1, + "exact_width": "log2(16/15)", + "h": 2, + "n": 4, + "normalized_ratio_upper_squeeze": "21/20", + "strict_bound_certified": true + }, + { + "calls_per_profile": 7182, + "discrete_bound_attained": true, + "discriminant": 1, + "exact_width": "log2(100/99)", + "h": 2, + "n": 10, + "normalized_ratio_upper_squeeze": "133/132", + "strict_bound_certified": true + }, + { + "calls_per_profile": 719982, + "discrete_bound_attained": true, + "discriminant": 1, + "exact_width": "log2(10000/9999)", + "h": 2, + "n": 100, + "normalized_ratio_upper_squeeze": "13333/13332", + "strict_bound_certified": true + }, + { + "calls_per_profile": 7199999982, + "discrete_bound_attained": true, + "discriminant": 1, + "exact_width": "log2(100000000/99999999)", + "h": 2, + "n": 10000, + "normalized_ratio_upper_squeeze": "133333333/133333332", + "strict_bound_certified": true + }, + { + "calls_per_profile": 71999999999999999982, + "discrete_bound_attained": true, + "discriminant": 1, + "exact_width": "log2(1000000000000000000/999999999999999999)", + "h": 2, + "n": 1000000000, + "normalized_ratio_upper_squeeze": "1333333333333333333/1333333333333333332", + "strict_bound_certified": true + }, + { + "calls_per_profile": 3780, + "discrete_bound_attained": true, + "discriminant": 1, + "exact_width": "log2(9/8)", + "h": 3, + "n": 3, + "normalized_ratio_upper_squeeze": "35/32", + "strict_bound_certified": true + }, + { + "calls_per_profile": 6804, + "discrete_bound_attained": true, + "discriminant": 1, + "exact_width": "log2(16/15)", + "h": 3, + "n": 4, + "normalized_ratio_upper_squeeze": "21/20", + "strict_bound_certified": true + }, + { + "calls_per_profile": 43092, + "discrete_bound_attained": true, + "discriminant": 1, + "exact_width": "log2(100/99)", + "h": 3, + "n": 10, + "normalized_ratio_upper_squeeze": "133/132", + "strict_bound_certified": true + }, + { + "calls_per_profile": 4319892, + "discrete_bound_attained": true, + "discriminant": 1, + "exact_width": "log2(10000/9999)", + "h": 3, + "n": 100, + "normalized_ratio_upper_squeeze": "13333/13332", + "strict_bound_certified": true + }, + { + "calls_per_profile": 43199999892, + "discrete_bound_attained": true, + "discriminant": 1, + "exact_width": "log2(100000000/99999999)", + "h": 3, + "n": 10000, + "normalized_ratio_upper_squeeze": "133333333/133333332", + "strict_bound_certified": true + }, + { + "calls_per_profile": 431999999999999999892, + "discrete_bound_attained": true, + "discriminant": 1, + "exact_width": "log2(1000000000000000000/999999999999999999)", + "h": 3, + "n": 1000000000, + "normalized_ratio_upper_squeeze": "1333333333333333333/1333333333333333332", + "strict_bound_certified": true + }, + { + "calls_per_profile": 29393280, + "discrete_bound_attained": true, + "discriminant": 1, + "exact_width": "log2(9/8)", + "h": 8, + "n": 3, + "normalized_ratio_upper_squeeze": "35/32", + "strict_bound_certified": true + }, + { + "calls_per_profile": 52907904, + "discrete_bound_attained": true, + "discriminant": 1, + "exact_width": "log2(16/15)", + "h": 8, + "n": 4, + "normalized_ratio_upper_squeeze": "21/20", + "strict_bound_certified": true + }, + { + "calls_per_profile": 335083392, + "discrete_bound_attained": true, + "discriminant": 1, + "exact_width": "log2(100/99)", + "h": 8, + "n": 10, + "normalized_ratio_upper_squeeze": "133/132", + "strict_bound_certified": true + }, + { + "calls_per_profile": 33591480192, + "discrete_bound_attained": true, + "discriminant": 1, + "exact_width": "log2(10000/9999)", + "h": 8, + "n": 100, + "normalized_ratio_upper_squeeze": "13333/13332", + "strict_bound_certified": true + }, + { + "calls_per_profile": 335923199160192, + "discrete_bound_attained": true, + "discriminant": 1, + "exact_width": "log2(100000000/99999999)", + "h": 8, + "n": 10000, + "normalized_ratio_upper_squeeze": "133333333/133333332", + "strict_bound_certified": true + }, + { + "calls_per_profile": 3359231999999999999160192, + "discrete_bound_attained": true, + "discriminant": 1, + "exact_width": "log2(1000000000000000000/999999999999999999)", + "h": 8, + "n": 1000000000, + "normalized_ratio_upper_squeeze": "1333333333333333333/1333333333333333332", + "strict_bound_certified": true + }, + { + "calls_per_profile": 49369423380480, + "discrete_bound_attained": true, + "discriminant": 1, + "exact_width": "log2(9/8)", + "h": 16, + "n": 3, + "normalized_ratio_upper_squeeze": "35/32", + "strict_bound_certified": true + }, + { + "calls_per_profile": 88864962084864, + "discrete_bound_attained": true, + "discriminant": 1, + "exact_width": "log2(16/15)", + "h": 16, + "n": 4, + "normalized_ratio_upper_squeeze": "21/20", + "strict_bound_certified": true + }, + { + "calls_per_profile": 562811426537472, + "discrete_bound_attained": true, + "discriminant": 1, + "exact_width": "log2(100/99)", + "h": 16, + "n": 10, + "normalized_ratio_upper_squeeze": "133/132", + "strict_bound_certified": true + }, + { + "calls_per_profile": 56420787594166272, + "discrete_bound_attained": true, + "discriminant": 1, + "exact_width": "log2(10000/9999)", + "h": 16, + "n": 100, + "normalized_ratio_upper_squeeze": "13333/13332", + "strict_bound_certified": true + }, + { + "calls_per_profile": 564221980080645046272, + "discrete_bound_attained": true, + "discriminant": 1, + "exact_width": "log2(100000000/99999999)", + "h": 16, + "n": 10000, + "normalized_ratio_upper_squeeze": "133333333/133333332", + "strict_bound_certified": true + }, + { + "calls_per_profile": 5642219814911999998589445046272, + "discrete_bound_attained": true, + "discriminant": 1, + "exact_width": "log2(1000000000000000000/999999999999999999)", + "h": 16, + "n": 1000000000, + "normalized_ratio_upper_squeeze": "1333333333333333333/1333333333333333332", + "strict_bound_certified": true + } + ], + "source_authentication": "SHA256 and Git blob checks; commit/path provenance recorded in SOURCES.json", + "source_example": { + "actual_calls_per_profile": 135, + "bound_numerator": 12, + "budget_per_profile": 135, + "budget_trace_cap": 22, + "common_calls": 0, + "count_scale": 3, + "discrete_bound_attained": false, + "discrete_width_ratio_lower": "23/21", + "discriminant": 4, + "endpoint_residual_value": 1, + "h": 1, + "interval_check": { + "normalized_ratio_lower": "697959122473768377082994859209989759027/340282366920938463463374607431768211456", + "normalized_ratio_upper": "174489780618442094270748714802497439757/85070591730234615865843651857942052864", + "strict_bound_certified": true + }, + "quadratic": [ + 15, + -22, + 8 + ], + "rank_mass_per_profile": 546, + "rational_roots": true, + "stronger_continuous_bound_denominator": 132, + "support_size": 5, + "trace": 22, + "uncancelled_calls_per_profile": 135 + }, + "source_files_verified": 2, + "status": "pass" +} diff --git a/research/fixed-budget-hidden-windows/SCOPE-COUNTEREXAMPLES.md b/research/fixed-budget-hidden-windows/SCOPE-COUNTEREXAMPLES.md new file mode 100644 index 0000000000..7171f4dbf0 --- /dev/null +++ b/research/fixed-budget-hidden-windows/SCOPE-COUNTEREXAMPLES.md @@ -0,0 +1,150 @@ +# Exact counterexamples to broader versions of the budget claim + +These examples do **not** contradict the narrow theorem. They show why its +degree, two-crossing, and rank-alphabet restrictions must remain explicit. +All coefficients and call counts below are integers. The profiles are +obtained from the positive and negative coefficients of `Q`; both sides have +equal call count and equal rank mass. They are arithmetic profiles, with no +claim of physical supplier realizability. + +Run the independent standard-library checker with: + +``` +python3 -I -B research/fixed-budget-hidden-windows/independent_check.py +``` + +It uses exact rational arithmetic and a separate Sturm-sequence root counter. +The saved result is [independent-check.json](independent-check.json). + +## Seven ranks defeat even the order `constant/N` + +On ranks `1,2,4,8,16,32,64`, take + +``` +Q_n(x) = -(x-1)(x-2)*[(x-1)^4-2*(n*(x-1)-1)^2]. +``` + +For `n=10`, its coefficients in ascending order are + +``` +[482, -1595, 1937, -1010, 180, 7, -1]. +``` + +Thus + +``` +A = 1595 H_2 + 1010 H_8 + H_64, +B = 482 H_1 + 1937 H_4 + 180 H_16 + 7 H_32. +``` + +Each has `N=W=2606` calls and rank mass `11334`. The endpoint zeros are +simple. There are exactly two interior zeros, and the difference is positive +between them and negative elsewhere in `(0,1)`. + +For a root-count proof, set `y=x-1`. The quartic factors over the reals as + +``` +[y^2-sqrt(2)*(ny-1)] * [y^2+sqrt(2)*(ny-1)]. +``` + +For `n>=3`, the first factor decreases strictly on `(0,1)` and changes from +positive to negative; the second increases strictly and changes from negative +to positive. Each has exactly one root there. The second factor's root is +below `1/n`, and the first factor's root is above it. This also proves the +stated sign pattern. Multiplication by `-(x-1)(x-2)>0` preserves that pattern. + +At `n=10`, exact evaluation of the quartic gives + +``` +R(1099/1000) = -103940399/10^12 < 0, +R(11/10) = 1/10000 > 0, +R(1101/1000)= -95939599/10^12 < 0. +``` + +Consequently its roots satisfy + +``` +1099/1000 < r < 11/10 < s < 1101/1000. +``` + +The elementary inequality `ln(1+t)0`, proves + +``` +W*ln(s/r) < 2606*(2/1099) = 5212/1099 < 12. +``` + +This strictly contradicts extending the claimed `12/(N*ln2)` lower bound to +this seven-rank alphabet. No decimal approximation is used. + +More strongly, for all `n>=4` the count is `W_n=24n^2+24n-34`. If `u,v` are +the two roots in the `y` coordinate, then + +``` +nu = 1-u^2/sqrt(2), nv = 1+v^2/sqrt(2), +v-u = (u^2+v^2)/(sqrt(2)*n). +``` + +The first quadratic factor is negative at `y=2/n`, since +`4/n^2-sqrt(2)<0`. Its strict decrease, together with the already established +root order, gives `0=4`. The two displayed identities +therefore imply `nu->1` and `nv->1`. Hence `u,v ~ 1/n`, and the width is +asymptotic to `sqrt(2)/(n^3*ln2)`. + +An order bound alone suffices for the obstruction: + +``` +v-u < 5/(sqrt(2)*n^3), +ln((1+v)/(1+u)) < (v-u)/(1+u) < v-u. +``` + +Since `W_n=24n^2+24n-34`, this proves `W_n*w_n -> 0` directly. No positive +universal bound of the form `constant/N` holds for this larger alphabet, +even with exactly two interior crossings and both endpoint equalities. + +## An edge loss defeats an overbroad mesh claim + +On the original five ranks, take + +``` +Q(x) = (x-1)(x-2)(10x-11)(x+1), +q = [-22, 31, 12, -31, 10]. +``` + +Both profiles have `53` calls and rank mass `270`. The positive loss is the +edge interval `0 11^4, k=1,2,3, +2 * 10^8 < 11^8, so p=1/8 is a positive-loss witness. +``` + +The maximum grid gap is `1/4`, which is smaller than even the theorem's +conservative rational threshold `120/(7*53)=120/371`. Hence this mesh would +hit every eligible two-crossing interior window, yet misses this edge loss. +The mesh corollary is valid only while retaining the theorem's zero pattern. + +## A different five-rank alphabet defeats the same constant + +On ranks `1,3,9,27,81`, use `F(p)=Q(3^p)` with + +``` +Q(x) = (x-1)(x-3)(3x-4)(2x-3), +q = [36, -99, 98, -41, 6]. +``` + +Both profiles have `140` calls and rank mass `1404`. They satisfy the same +two-crossing sign pattern and endpoint equalities, but the width is +`w=ln(9/8)/ln3`. The old power-of-two constant would require +`140*ln(9/8)*ln2 > 12*ln3`. In fact, + +``` +140*ln(9/8)*ln2 < 140*(1/8)*(7/10) = 49/4 < 13 < 12*ln3. +``` + +Here `ln2<7/10` and `ln3>13/12` follow directly from the positive series +`ln((1+t)/(1-t))=2*(t+t^3/3+...)`: at `t=1/3`, the tail after the first term +is less than `1/36`, giving `ln2<25/36<7/10`; at `t=1/2`, the first two +terms give `ln3>13/12`. Thus the precise `12/ln2` constant is specific to +the stated power-of-two alphabet. diff --git a/research/fixed-budget-hidden-windows/SOURCES.json b/research/fixed-budget-hidden-windows/SOURCES.json new file mode 100644 index 0000000000..09660c5356 --- /dev/null +++ b/research/fixed-budget-hidden-windows/SOURCES.json @@ -0,0 +1,26 @@ +{ + "repository": "CrocSwap/integer-mult-bounds", + "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419", + "source_pr": 6049, + "source_commit": "2646b6d67ceb74b9868e632f3a27312d8be62a0e", + "files": [ + { + "file": "sources/pr6049-README.md.txt", + "upstream_path": "research/hidden-power-windows/README.md", + "commit": "2646b6d67ceb74b9868e632f3a27312d8be62a0e", + "git_blob_sha1": "71bebc3aacc14bce229f56b3c3315bc704985877", + "url": "https://github.com/CrocSwap/integer-mult-bounds/blob/2646b6d67ceb74b9868e632f3a27312d8be62a0e/research/hidden-power-windows/README.md", + "sha256": "391b0a995b1d6ea08a634c16d71a285da94db5efb5d42fb5c1b3d9ffd973ca2b", + "bytes": 8197 + }, + { + "file": "sources/pr6049-verify.py.txt", + "upstream_path": "research/hidden-power-windows/verify.py", + "commit": "2646b6d67ceb74b9868e632f3a27312d8be62a0e", + "git_blob_sha1": "fe4adcc950f44e53a304d42dd7bf139b7b53a71e", + "url": "https://github.com/CrocSwap/integer-mult-bounds/blob/2646b6d67ceb74b9868e632f3a27312d8be62a0e/research/hidden-power-windows/verify.py", + "sha256": "506292b29d269c32981227836e546010f0d97c5b3b0f4be6c54ec45da3967bcc", + "bytes": 4800 + } + ] +} diff --git a/research/fixed-budget-hidden-windows/UPSTREAM-NOTICE.txt b/research/fixed-budget-hidden-windows/UPSTREAM-NOTICE.txt new file mode 100644 index 0000000000..59d8e0cf31 --- /dev/null +++ b/research/fixed-budget-hidden-windows/UPSTREAM-NOTICE.txt @@ -0,0 +1,415 @@ +A sharper exponent for integer multiplication +Copyright 2026 Douglas Colkitt + +This project includes unmodified source files from OpenAI's manuscript +"Integer multiplication below n log n" and its accompanying repository: +https://github.com/openai/math +Commit: adc7f1241b42e322a6451854ab7e4b4c146bf78a + +The original manuscript identifies OpenAI as its author. Its Apache-2.0 +license is retained at upstream/LICENSE. The exact source URLs and hashes +are recorded in upstream/manifest.json. Proposed modifications are supplied +as separate files under patches/; upstream source files remain unchanged. + +The original local research note, scripts, certificates, patches, and +documentation were prepared by Douglas Colkitt with assistance from OpenAI +Codex. The community release incorporates work by the contributors identified +in the notices below; it is not solely Douglas Colkitt's work. +This project is not an official OpenAI release or an OpenAI endorsement. + +Related contributions (not imported in this checkpoint): +Zhihao Chen (jacklightChen), PR #7, supplied an earlier ternary five-subset +motif, finite-alphabet transfer and a different compressed producer: +https://github.com/CrocSwap/integer-mult-bounds/pull/7 +The present checkpoint claims no priority for that motif. Related compressed +complex-network work was submitted by eumemic in PR #3: +https://github.com/CrocSwap/integer-mult-bounds/pull/3 +The pending contributions and their stronger bounds require their own review; +this notice does not represent adoption or verification of their claims. + +Additional community work, including parallel and superseded submissions, is +acknowledged in CONTRIBUTORS.md, with pinned submission metadata in +docs/research/contribution-snapshot.json. These acknowledgements do not imply +joint authorship of the checkpoint, incorporation of pending code, or verification +of submitted mathematical claims. Original source-specific notices remain in force. + +Community release (accepted by conditional maintainer audit): +The following original contributor notices apply to the imported PR #39 chain. +The preceding non-import statements describe the preserved 2^-30 checkpoint. + +Ternary five-subset construction and common-four-point resynthesis +Copyright 2026 Zhihao Chen (jacklightChen) + +This is Zhihao Chen's first submission of this specific construction to this +repository. Research, proof development, code and verification were prepared +with substantial assistance from GPT-6 Astra (OpenAI Codex), as identified by +the contributor. This is not independent review or an OpenAI endorsement. +Future research building on this contribution should explicitly acknowledge +Zhihao Chen (jacklightChen), cite the accompanying note and pull request, and +retain the preceding contributors' attribution. This notice records research +provenance; the repository's Apache-2.0 license remains unchanged. + +Dependencies retained from eumemic's Claude-assisted PRs #3 and #5: +https://github.com/CrocSwap/integer-mult-bounds/pull/3 +https://github.com/CrocSwap/integer-mult-bounds/pull/5 +PR #5 commit: d3d370c34937503bd3fa63c83d505a05e8e50893 +These include complex_circuit.py, complex_network.py, fast_gaussian.py, +their generators, construction notes and certificates. The Gaussian input +scaling proof is corrected in this derivative; see the modification notice below. +Aligned pairing also appears in Bortlesboat's PR #2. Retained totals and bank +sharing appear in dleen's PR #4 and cheaper retained centers in eumemic's PR #6. +Their results and ideas are credited separately from this new construction. + +Bulk recursion and controlled tensor basis, 8 October 2026 +Copyright 2026 icekylinx + +The new projector batching, controlled simultaneous basis, mixed-width tape +recursions, whole-residual complex recursion, and dependency-path precision +guard in the batched-23 proof package are contributed by icekylinx, developed +with substantial OpenAI GPT-6 Astra assistance. Review corrections and +repository integration were prepared with OpenAI Codex assistance. They build on the retained +PR #7 finite producers and the preceding contributions credited above. +The new package retains the repository's Apache-2.0 license and the original +authors' attribution. It is not an official OpenAI release or endorsement. + +Modification notice, 8 October 2026 (icekylinx): the retained fast Gaussian +proof now bounds shifted approximation error by F=2^ceil(1.14 alpha^2). +The P=34p precision budget and asymptotic exponent are unchanged. New batching +checks are integrated into make verify. Existing attribution and licenses +are retained. + +Partial-swap extension, 8 October 2026 +Copyright 2026 icekylinx + +The partial-swap framing, binary retained-total triple construction, +dependency-preserving positive labels and carrier reuse, unequal (25,23,57) +common basis, improved complex batching, and exact assembly are contributed +by icekylinx with substantial OpenAI GPT-6 Astra and Codex assistance. +This extension directly inherits PR #10, commit +62691e395a0458ce089a1c7b5d89e74291e95e29. The portable producer adapters +modify the retained paired-exclusion and shared-point implementations credited +above. The original licenses, attribution, and Gaussian correction are retained. + +Endpoint-gauge extension, 8 October 2026 +Copyright 2026 icekylinx + +The complementary auxiliary endpoint gauges, (32,30,40) controlled basis, +general nondegenerate binary phase residuals, retained-center complex producer, +updated path guard and exact assembly are contributed by icekylinx with +substantial OpenAI GPT-6 Astra and Codex assistance. This extension inherits +f2ab41aebad47861caf6316282c1793e5513845e and its PR #10 ancestry. New portable +adapters retain the paired-exclusion and shared-point contributions credited +above. Original licenses, notices and the Gaussian correction are retained. + +Structured-basis and semantic-bulk extension, 8 October 2026 +Copyright 2026 icekylinx + +The selected (32,30,36) bit construction, A1/A5 block refinements, fixed +middle-axis I+J profiles with bounded-minor CRT certificates, mixed dyadic +complex centers, complete data-front batching and circuit-specific assembly +are contributed by icekylinx with substantial OpenAI GPT-6 Astra and Codex +assistance. The immediate parent is ed90fd940279c336ebc45968631bdebfb087b505. + +The semantic/bulk compatibility argument, literal scalar charge, product row +stock and parameterization adapt Zhihao Chen (jacklightChen)'s PR #23, +commit 661ebabc1076c9f525d7ce4967c876b203fa9827. Translated complex endpoints +are adopted from the same contributor's PR #21, +commit 5ba6cf0bfb68f2be8d15610e7972207c50254d6a, following eumemic's source-frame +work and the earlier nested-basis contributions. + +Completed-child semantic precision, arbitrary-coordinate routing, phase-cell +Gaussian inversion and bulk tape transfer are credited to the RaD project +(hipotures), commit 45d9b60355872041f9275f77c057514def0d45bc, exposed through +PR #20 at 4f8d6c8272b5ff307a0da51df545ec3cd96a8b6e. Their selected proof +sources retain their separate CC0 license and original NOTICE under +references/semantic-bulk/rad20. The PR #23 source retains its recorded OpenAI +Codex assistance; RaD retains its recorded Codex and GPT-6.1-Sol Ultra +assistance. These are source attributions, not claims about this session's +runtime model. Related contributions by Rohan Arun and Aurel Prosz remain +acknowledged in the imported notices. No exclusive priority or additional +license condition is asserted. + +Copied retained-center extension, 8 October 2026 +Copyright 2026 icekylinx + +The copied retained-center schedule in both orientations, its complex-phase +transfer, the Wm-N+L rank budget, and the selected (25,23)/(28,28) composition +are contributed by icekylinx with substantial OpenAI GPT-6 Astra and Codex +assistance. This extension inherits PR #32 at +0ef3aeb61f55cc0b321ce6a0ef00acee25cefe52 and the preceding PR #10/#18/#24 work. + +The two-stage topology and paid copied-stream endpoint correction are due +to Aurel Prosz (Paureel), c82d09eb4781b68435e3fa3eb6beea72fa900fab, +through Zhihao Chen (jacklightChen)'s PR #29 unequal-axis composition, +9d963275075fa98f1da821e27757b238dafd6b3c. That source also credits Swapnil +Jain's two-stage development at ae405eb474d1486b2d8aef90139869f927f4836a. + +The contiguous corner method, incidence factorization and exact partition +certificates are due to Rohan Arun (PR #31), method commit +02f68f95369c39955c5ffcfddbd75cd83e26b305. The selected (25,23) certificate +specializes Dominik Scholz's parameterization (PR #33), +a499a345c040aa15b68e984a0904eadc485c7a7e. Their source notices and proof +snapshots are preserved in references/copied-centers. Historical OpenAI +Codex, GPT-6 Astra and Anthropic Claude Opus 5.5 assistance is credited to +the respective imported sources. Existing PR #21/#23 and RaD attribution, +licenses and the Gaussian correction remain in force. + +Copied centers with reversed (23,25) data corners, 2026-10-08 +Rohan Arun with substantial OpenAI Codex assistance supplies the composition, +exact dimension23 controls and cost/assembly integration. James Chang's PR34 +supplies the reversed boundary family; icekylinx's PR36 supplies copied retained +centers and the selected complex graph. The balanced assembly remains attributed +to RaD/hipotures and its PR34 specialization. Retain Dominik Scholz PR33, Rohan +Arun PR31, Zhihao Chen PR29/21/23, Paureel/Aurel Prosz, Swapnil Jain, icekylinx, +eumemic, Douglas Colkitt, OpenAI and all earlier notices and hypotheses. +This is not a claim of formal verification, new foundational rank identities, +global optimality or measured runtime speedup. + +Fixed middle basis with copied reversed corners (2026-10-08): +Rohan Arun, with substantial OpenAI Codex assistance. Composition and +simultaneous-basis proof retain icekylinx PR32/36, James Chang PR34, +Dominik Scholz PR35/38, Zhihao Chen, Paureel, Swapnil Jain, RaD/hipotures, +eumemic and all preceding attribution and licenses. See research/copied-fixed-reversed. + +Changed-graph composition with copied centers and fixed bases, 8 October 2026 +Prepared with OpenAI Codex assistance. +The new composition uses icekylinx PR36 copied centers and PR32 fixed-I+J +projectors/profiler, Dominik Scholz PR35 two fixed factors and CRT argument, +Zhihao Chen (jacklightChen) PR29/23 interfaces, Aurel Prosz (Paureel) and +Swapnil Jain's two-stage development, Rohan Arun PR25/31 corner methods, +Dominik Scholz PR33/38 dimension/composition work; James Chang (jamesyc) +PR34 reversed geometry and balanced transfer; Rohan Arun PR37/39/40 +reversed integration, modular data tests and both-fixed baseline; +RaD (hipotures) PR41 changed scalar DAGs, alternating point order and +independent role compiler; RaD balanced routing/bulk interfaces, and all +retained predecessors. +Complete attribution and the conditional proof boundary are recorded in +research/copied-fixed/PROOF.md; imported originals and source pins are retained. +Original Apache-2.0 and CC0 notices remain applicable. + +Community follow-up integration (PRs #49, #45 and #26), 8 October 2026: +Rohan Arun contributes weighted carrier matching and climbed summand/leave-one-out +orders (PRs #44/#47/#49), with Anthropic Claude assistance. The final construction +composes Chafik Boukhalfa's changed-graph checks, exact rational data recovery and +reordered exclusion sums (PRs #43/#46/#48, OpenAI Codex assistance) with RaD / +hipotures's alternating pair order and independent physical role compiler (#41). +All predecessor attribution and conditional proof interfaces remain in force. + +Alejandro Zarzuelo Urdiales contributes Gaussian parity and canonical arithmetic +proofs, finite tensor execution, profile precision accounting and mixed-center +reference checks (#45), with substantial OpenAI Codex assistance. See +research/gaussian-parity-synthesis/PROVENANCE.md for his full attribution. +Ryan S / princezuda contributes historical Lean certificate arithmetic, algebraic +frame/movement/guard lemmas and independent paired-circuit checks (#26). Original +source notices and historical snapshots are preserved. Neither formal package +claims a full formal proof of the multiplication algorithm or a new kappa. + +Joint frame compilation of skip-prefix strips + +The local compiler and exact finite witnesses were prepared by eumemic with +substantial OpenAI Codex assistance. Avi Eisenberg / ikeboy with Anthropic +Claude assistance supplied the unmodified PR #53 skip-prefix producer. +The pinned PR #48 pipeline is Chafik Boukhalfa's contribution, incorporating +Rohan Arun, RaD / hipotures, icekylinx, Dominik Scholz, James Chang, +Zhihao Chen, Aurel Prosz / Paureel, Swapnil Jain, eumemic, Douglas Colkitt, +OpenAI, David Harvey, Joris van der Hoeven and the earlier contributors +credited in the retained sources. See references/frame-compiler/pr48/NOTICE +and references/frame-compiler/pr53/NOTICE for their original attribution. +No authorship or review by those predecessors is claimed for this compiler. + +Joint dual-skip/frame-compiler composition (2026-10-08) +--------------------------------------------------- +Rohan Gupta / gupt1156 with Anthropic Claude assistance: PR55 dual-skip +scalar graph; original LICENSE and NOTICE are retained under +references/frame-compiler/pr55. eumemic with substantial OpenAI Codex +assistance: PR57 joint reversible frame compiler, serialized physical-word +replay and profile reconstruction. Chafik Boukhalfa with OpenAI Codex +assistance: this composition, independent integration and exact certificate. +Avi Eisenberg / ikeboy, Rohan Arun, RaD / hipotures, icekylinx, and all +predecessor authors retain the notices above and in pinned source files. +No original copyright or Apache-2.0 notice is removed. + +Ranked reclamation after the PR58 joint-dual composition (2026-10-08) +---------------------------------------------------------------- +Chafik Boukhalfa with OpenAI Codex assistance: prioritize retired physical +slots by descending current frame rank, retaining slot ID as the tie-breaker; +complete replay, exact profiles, comparison and adversarial controls. +The dedicated joint_dual_reclaim_compiler.py is derived from eumemic's PR57 +compiler. Its original shared compiler remains byte-identical. The PR55 +producer and all preceding attribution remain unchanged. The complete PR58 +comparison certificate and its original source/proof provenance are retained +under references/frame-compiler/pr58. + +Skip-prefix strip producer, 8 October 2026 +By Avi Eisenberg (ikeboy), with Anthropic Claude (Claude Opus 5.5) +assistance. The skip-prefix leave-one-out strip layout in +research/skip-strips/skip_graph.py is new. Everything else reuses Chafik +Boukhalfa's PR #43/#46/#48 research/copied-fixed pipeline, its verification +code, exact data recovery and support-order sorting, together with: +- Rohan Arun's PR #44 weighted carrier matching optimizer; +- RaD (hipotures) PR #41 alternating point order; +- every predecessor credited above. +Complete attribution and the conditional proof boundary are recorded in +research/skip-strips/PROOF.md. Original Apache-2.0 and CC0 notices remain +applicable. + +Local split-pair skip-prefix research continuation (2026-10-08) +Prepared with substantial OpenAI Codex assistance at the user's request. +New contribution: singleton/pair recursive partition refinement, finite summand +order and moment search, and verified composition with inherited paid clones. +Avi Eisenberg/ikeboy with Anthropic Claude assistance: PR53 skip-prefix strips. +Chafik Boukhalfa with OpenAI Codex assistance: PR54 original-envelope clone +specialization and PR43/46/48 checking interfaces. RaD/hipotures: PR51 +whole-chain/source-partition cloning and earlier producer/interfaces. +Rohan Arun: PR44 weighted matching and earlier fixed/reversed work, with all +stated historical AI assistance. All predecessor notices remain applicable. + +Original-envelope whole-chain clones on skip-prefix strips (research/skip-clones): +Chafik Boukhalfa, prepared with OpenAI Codex assistance. The complete-chain +source-partition clone operation is adapted from RaD / hipotures, PR #51, +with original envelopes retained here. The scalar base is Avi Eisenberg's +PR #53 skip-prefix layout, prepared with Anthropic Claude assistance. +All credited PR #43/#46/#48, PR #44 and earlier code/proof notices remain +in force. This extension is provided under the repository's Apache-2.0 terms. + +Community review checkpoint #50–#61, 8 October 2026 +Maintainer integration and independent arithmetic: Douglas Colkitt, with OpenAI Codex. +Avi Eisenberg / ikeboy: skip-prefix strip framework (#53), with Anthropic Claude. +Rohan Gupta / gupt1156: parallel order search (#50, stated Antigravity assistance) +and dual-suffix strips (#55, Anthropic Claude assistance). +Eumemic: equal-frame joint compilation and paid signal reclamation (#57), with Codex. +Chafik Boukhalfa: original-envelope paid clones (#54), composition (#58) and ranked +reclamation (#60), with Codex. Rohan Arun: order search (#52) and positive-frame +composition (#56), with Anthropic Claude and stated Codex validation assistance. +RaD / hipotures: enlarged frames, source partitions and paid whole-chain clones +(#51), with Codex. Rohan Garg / rohangar1: singleton/pair recursion and paid-clone +composition (#59), with Codex. Alejandro Zarzuelo Urdiales: exact parameter +refinement, scoped Lean arithmetic, matrix/parity and search tools (#61), with +his disclosed multi-tool and Codex assistance. +Parallel #50/#52 records are reviewed and credited without replacing the earlier +climbed-48 implementation; their exact commit history is retained. The separate +#51 witness is retained as research; its source-graph/negative-basis data proof +has not received the same full replay as #56's consumed compiler machinery. +See docs/research/community-round2-review.md for precise validation boundaries. +All earlier licenses, contributions and notices remain applicable. + +Interval strips and core-aware pair assembly + +The interval leave-one-out strips and the core-aware group-pair assembly in +research/pair-assembly were prepared by Avi Eisenberg / ikeboy with Anthropic +Claude assistance. They build on PR #53's skip-prefix pipeline and its +inherited PR #48 sources. The stacked witness in research/pair-assembly/frame +uses eumemic's PR #57 joint frame compiler unchanged; its driver and verifier +are adaptations of PR #57's skip_frame_compiler.py, skip_frame_compose.py and +verify_skip_frame.py. Original notices are retained. + +Stopped product-ring extension, 9 October 2026 +Copyright 2026 icekylinx + +The opposite-bank generic projector factorization, componentwise atom-ring +adapters, stopped recurrence and outer ordinary-interchange conversion, +aligned pair-star producer with rational centers, exact denominator-21 +grid and selected (23,23)/(24,24) composition are contributed by icekylinx +with substantial OpenAI GPT-6 Astra and Codex assistance. This extension +builds on merged PR #36, 11817ccacb564bb7f98789c20dc11d3fece207e3, and is +integrated on upstream main 56b66d58297deca1d7dd130247d720e960f77a37. + +The retained ordinary leaf uses the preceding projector, corner and +copied-center proofs. The selected two-stage topology retains Aurel Prosz +(Paureel), Swapnil Jain and Zhihao Chen's credits; the semantic assembly +retains PR #21/#23 and RaD's attribution. Paired producers, carrier matching, +original source notices and each imported license remain unchanged. + +Partial-gauge extension, 9 October 2026 +Copyright 2026 icekylinx + +The pair-first cube assembly, compatible backward frame enlargement, +partial source-gauge schedule and stopped whole-projector composition are +contributed by icekylinx with substantial OpenAI GPT-6 Astra and Codex +assistance, extending PR #104 at 948ce1510df750f4c18b96bdaef436a86f8bf834. + +The physical deferred bit word, reflected event accounting, fan-order +clarification and signed two-stage endpoint are adopted from Zhihao Chen +(jacklightChen), PR #97, e15350b66e4bf796153a68c240a6cc1b788abe3e, with +Codex assistance. Its deferred readouts, V leaves, lifted frames and frozen +witness originate in Swapnil Jain's 741e7aa078392553815df7926ee17ac5e25a8c38, +with the original Claude disclosure retained. Cyclic interval and core-aware +pair primitives build on Avi Eisenberg (ikeboy), PR #62, +ad0f25ff7b23cff7f08ad237c2254e6ecf74257e, with Anthropic Claude assistance. +Prior two-stage, copied-center, ordinary-leaf, semantic/bulk, routing and +precision credits remain in force. Imported source notices and licenses +are preserved under references/partial-gauge/; see SOURCES.json. + +Three-stage cover extension, 9 October 2026 +Copyright 2026 icekylinx + +The arbitrary-subspace Clifford frame theorem, three-stage Cayley geometry, +weighted q-adic GL cover, unit-lower weighted compiler, charged local-ring +fallback, uniform batching, internal row borrowing and exact composition +are contributed by icekylinx with substantial OpenAI GPT-6 Astra assistance. This +repository integration uses Codex assistance and extends +PR #115, cf60442983c153a3a0f5272ea4713f99eba13c86. + +The selected local complex DAG and support/label replay are adopted from +Copyright 2026 eumemic, PR #117, cbb05ce504d571546d9b7794c186a613c659c3bf, +with its original Apache-2.0 terms and Claude assistance disclosure. +The unchanged bit physical word retains Zhihao Chen (jacklightChen), +PR #97, and Swapnil Jain's underlying witness and assistance notices. +The prior opposite-bank, stopped ordinary-leaf, copied-center, topology, +semantic/bulk, precision and analytic credits remain applicable. +Original source notices and license bytes are preserved in +references/three-stage-cover/pr117/ and references/partial-gauge/. + +Paired-cube and shared-core extension, 9 October 2026 +Copyright 2026 icekylinx + +The paired-coordinate triple-cube identity, signed overlap channels, +original-source involution, coordinate-star centers, concrete frame/carrier +compiler, chronological source gauges, PR97 gauge-subset selection, +orthogonal cross-stage routing and exact supplier/assembly integration +are contributed by icekylinx with substantial OpenAI GPT-6 Astra assistance. +Repository integration uses Codex assistance and extends PR #130 at +6a9970a530119174507904e23592fd59ede19a5d. + +The substantial completed-core workspace-sharing principle is credited to +an664, PR #128, 530588a019b4a74f09180680c9e3961bf649ec89, with its reported +OpenAI Codex assistance. No source code, partition or serialized witness +from that PR is imported. The new routing and paired-motif integration +are described separately and claim no exclusive priority for broad sharing, +paired-coordinate, Fourier or carrier-matching ideas. + +Selected coarse queries restrict the retained eumemic PR #117 positive DAG; +its original Apache-2.0 and Claude assistance notices remain unchanged. +The bit word and original frames retain Zhihao Chen's PR #97 and Swapnil +Jain's frozen witness, notices and historical assistance disclosures. +Earlier generalized Clifford, three-stage, uniform weighted recursion, +ordinary-leaf, semantic/bulk, precision and analytic credits remain in force. +Source-specific license bytes are preserved under references/. + +October 9 recycled-bit integration: +DaysSky (#150), William Porter/hpst3r (#147), Thomas Marchand/Th0rgal (#146), +Rohan Gupta/gupt1156 (#148), James Chang/jamesyc (#124), SovereignSteak (#122). +The original notices and assistance disclosures are retained under research/, +including research/recycled-bit-integration/NOTICE. Andrew Barnes/Bortlesboat +(#101) repairs shared verifiers using rfu08's #64 counterexample. rfu08's +scoped finite and formal-transfer packages are included separately; they do +not establish the full multiplication theorem. Earlier and parallel credits +remain applicable. Douglas Colkitt integrated these with OpenAI Codex assistance. + +SovereignSteak PR151 independently supplies the matching gauge/recycling +composition and the selected 473/10^6 atom refinement; its original package +and assistance disclosure are retained under research/gauge-recycling/. + +October 9 coordinated-frame and completed-entrance-bank integration: +Dugongue PR186, 166a34d75e853e933855f0f7e940fe77c4bb6b8d, builds on +Chafik Boukhalfa/chafreaky's PR181, 7fb2194801e3a10f54772c7f0d5505035a4fc0ad, +and eumemic's PR168 v4, 4a3c769e5c5430e7114c4d3e099ff34664677f17. +The frozen package and prerequisite archive preserve all author, source-license +and assistance notices, including PR175's compiler optimization. DaysSky's +carrier closure, James Chang's terminal substitution and balanced assembly, +geckods' stopping refinements and all preceding framework credits remain. +Rohan Arun's PR185 bootstrap and chafreaky's PR182 bit refinement are reviewed +parallel contributions; their gains are not added to the selected witness. +Douglas Colkitt integrated the package and supplied the bank scheduling +supplement with OpenAI Codex assistance, under Apache-2.0. The all-size +interfaces remain conditional; finite verification is not full formalization. diff --git a/research/fixed-budget-hidden-windows/VALIDATION.json b/research/fixed-budget-hidden-windows/VALIDATION.json new file mode 100644 index 0000000000..b5e29be3b9 --- /dev/null +++ b/research/fixed-budget-hidden-windows/VALIDATION.json @@ -0,0 +1,45 @@ +{ + "python": "3.14.7", + "runs": [ + { + "check": "main", + "optimized": false, + "receipt_sha256": "8da19f212d4d5ee56258eead0524f206c1fbd75ddc18d4f20299dab0553c4fdf", + "status": "pass" + }, + { + "check": "independent", + "optimized": false, + "receipt_sha256": "32359c9408441f2df846529479e255cce00dc3a0d66a4f6d18f012a5f8af5e15", + "status": "pass" + }, + { + "check": "tests", + "optimized": false, + "status": "pass", + "tests": 26 + }, + { + "check": "main", + "optimized": true, + "receipt_sha256": "8da19f212d4d5ee56258eead0524f206c1fbd75ddc18d4f20299dab0553c4fdf", + "status": "pass" + }, + { + "check": "independent", + "optimized": true, + "receipt_sha256": "32359c9408441f2df846529479e255cce00dc3a0d66a4f6d18f012a5f8af5e15", + "status": "pass" + }, + { + "check": "tests", + "optimized": true, + "status": "pass", + "tests": 26 + } + ], + "serial": true, + "status": "pass", + "timeout_seconds_per_command": 30, + "writes_package_files": false +} diff --git a/research/fixed-budget-hidden-windows/independent-check.json b/research/fixed-budget-hidden-windows/independent-check.json new file mode 100644 index 0000000000..2fc34a6fd2 --- /dev/null +++ b/research/fixed-budget-hidden-windows/independent-check.json @@ -0,0 +1,418 @@ +{ + "arithmetic": "integer and Fraction only", + "discrete_bound_attainment": [ + { + "Z": 17, + "budget": 105, + "exact_minimum_width": "log2(9/8)", + "h": 1, + "n": 3 + }, + { + "Z": 31, + "budget": 189, + "exact_minimum_width": "log2(16/15)", + "h": 1, + "n": 4 + }, + { + "Z": 199, + "budget": 1197, + "exact_minimum_width": "log2(100/99)", + "h": 1, + "n": 10 + }, + { + "Z": 19999, + "budget": 119997, + "exact_minimum_width": "log2(10000/9999)", + "h": 1, + "n": 100 + }, + { + "Z": 199999999, + "budget": 1199999997, + "exact_minimum_width": "log2(100000000/99999999)", + "h": 1, + "n": 10000 + }, + { + "Z": 1999999999999999999, + "budget": 11999999999999999997, + "exact_minimum_width": "log2(1000000000000000000/999999999999999999)", + "h": 1, + "n": 1000000000 + }, + { + "Z": 17, + "budget": 630, + "exact_minimum_width": "log2(9/8)", + "h": 2, + "n": 3 + }, + { + "Z": 31, + "budget": 1134, + "exact_minimum_width": "log2(16/15)", + "h": 2, + "n": 4 + }, + { + "Z": 199, + "budget": 7182, + "exact_minimum_width": "log2(100/99)", + "h": 2, + "n": 10 + }, + { + "Z": 19999, + "budget": 719982, + "exact_minimum_width": "log2(10000/9999)", + "h": 2, + "n": 100 + }, + { + "Z": 199999999, + "budget": 7199999982, + "exact_minimum_width": "log2(100000000/99999999)", + "h": 2, + "n": 10000 + }, + { + "Z": 1999999999999999999, + "budget": 71999999999999999982, + "exact_minimum_width": "log2(1000000000000000000/999999999999999999)", + "h": 2, + "n": 1000000000 + }, + { + "Z": 17, + "budget": 3780, + "exact_minimum_width": "log2(9/8)", + "h": 3, + "n": 3 + }, + { + "Z": 31, + "budget": 6804, + "exact_minimum_width": "log2(16/15)", + "h": 3, + "n": 4 + }, + { + "Z": 199, + "budget": 43092, + "exact_minimum_width": "log2(100/99)", + "h": 3, + "n": 10 + }, + { + "Z": 19999, + "budget": 4319892, + "exact_minimum_width": "log2(10000/9999)", + "h": 3, + "n": 100 + }, + { + "Z": 199999999, + "budget": 43199999892, + "exact_minimum_width": "log2(100000000/99999999)", + "h": 3, + "n": 10000 + }, + { + "Z": 1999999999999999999, + "budget": 431999999999999999892, + "exact_minimum_width": "log2(1000000000000000000/999999999999999999)", + "h": 3, + "n": 1000000000 + }, + { + "Z": 17, + "budget": 29393280, + "exact_minimum_width": "log2(9/8)", + "h": 8, + "n": 3 + }, + { + "Z": 31, + "budget": 52907904, + "exact_minimum_width": "log2(16/15)", + "h": 8, + "n": 4 + }, + { + "Z": 199, + "budget": 335083392, + "exact_minimum_width": "log2(100/99)", + "h": 8, + "n": 10 + }, + { + "Z": 19999, + "budget": 33591480192, + "exact_minimum_width": "log2(10000/9999)", + "h": 8, + "n": 100 + }, + { + "Z": 199999999, + "budget": 335923199160192, + "exact_minimum_width": "log2(100000000/99999999)", + "h": 8, + "n": 10000 + }, + { + "Z": 1999999999999999999, + "budget": 3359231999999999999160192, + "exact_minimum_width": "log2(1000000000000000000/999999999999999999)", + "h": 8, + "n": 1000000000 + }, + { + "Z": 17, + "budget": 49369423380480, + "exact_minimum_width": "log2(9/8)", + "h": 16, + "n": 3 + }, + { + "Z": 31, + "budget": 88864962084864, + "exact_minimum_width": "log2(16/15)", + "h": 16, + "n": 4 + }, + { + "Z": 199, + "budget": 562811426537472, + "exact_minimum_width": "log2(100/99)", + "h": 16, + "n": 10 + }, + { + "Z": 19999, + "budget": 56420787594166272, + "exact_minimum_width": "log2(10000/9999)", + "h": 16, + "n": 100 + }, + { + "Z": 199999999, + "budget": 564221980080645046272, + "exact_minimum_width": "log2(100000000/99999999)", + "h": 16, + "n": 10000 + }, + { + "Z": 1999999999999999999, + "budget": 5642219814911999998589445046272, + "exact_minimum_width": "log2(1000000000000000000/999999999999999999)", + "h": 16, + "n": 1000000000 + }, + { + "Z": 17, + "budget": 139276569424062015476858880, + "exact_minimum_width": "log2(9/8)", + "h": 32, + "n": 3 + }, + { + "Z": 31, + "budget": 250697824963311627858345984, + "exact_minimum_width": "log2(16/15)", + "h": 32, + "n": 4 + }, + { + "Z": 199, + "budget": 1587752891434306976436191232, + "exact_minimum_width": "log2(100/99)", + "h": 32, + "n": 10 + }, + { + "Z": 19999, + "budget": 159169242868373044487396524032, + "exact_minimum_width": "log2(10000/9999)", + "h": 32, + "n": 100 + }, + { + "Z": 199999999, + "budget": 1591732218009949621905186757804032, + "exact_minimum_width": "log2(100000000/99999999)", + "h": 32, + "n": 10000 + }, + { + "Z": 1999999999999999999, + "budget": 15917322219892801764804541445026799557804032, + "exact_minimum_width": "log2(1000000000000000000/999999999999999999)", + "h": 32, + "n": 1000000000 + } + ], + "independent_census": { + "all_minimizing_quadratics": [ + { + "a": 60, + "b": -161, + "c": 108, + "calls_per_profile": 987 + }, + { + "a": 72, + "b": -161, + "c": 90, + "calls_per_profile": 969 + } + ], + "budget_per_profile": 1000, + "discrete_and_shifted_continuous_bounds_checked": true, + "irrational_root_pairs": 7259, + "minimum_Delta_over_trace_squared": "1/25921", + "minimum_calls_seen": 93, + "quadratics": 8158, + "rational_root_pairs": 899, + "shifted_enumeration_order_sha256": "879854cfe9e888753cd65cff2696d9197393151c9949354d3228c1eb680b03e0" + }, + "limits": [ + "finite corroboration, not proof assistant verification", + "independent implementation by another AI worker", + "does not establish physical supplier realizability" + ], + "scope_counterexamples": { + "edge_window": { + "calls_per_profile": 53, + "coefficients_low_to_high": [ + -22, + 31, + 12, + -31, + 10 + ], + "interior_roots": 1, + "maximum_grid_gap": "1/4", + "new": [ + 0, + 31, + 12, + 0, + 10 + ], + "old": [ + 22, + 0, + 0, + 31, + 0 + ], + "positive_witness": "p=1/8", + "rank_base": 2, + "rank_mass_per_profile": 270, + "safe_mesh_threshold_for_the_two_crossing_class": "120/371", + "sample_signs": [ + { + "p": "1/4", + "sign": -1 + }, + { + "p": "1/2", + "sign": -1 + }, + { + "p": "3/4", + "sign": -1 + } + ], + "violated_extension": "applying the mesh corollary to edge losses" + }, + "higher_degree": { + "calls_per_profile": 2606, + "coefficients_low_to_high": [ + 482, + -1595, + 1937, + -1010, + 180, + 7, + -1 + ], + "interior_roots": 2, + "new": [ + 482, + 0, + 1937, + 0, + 180, + 7, + 0 + ], + "old": [ + 0, + 1595, + 0, + 1010, + 0, + 0, + 1 + ], + "rank_base": 2, + "rank_mass_per_profile": 11334, + "residual_at_bracket_points": [ + "-103940399/1000000000000", + "1/10000", + "-95939599/1000000000000" + ], + "root_brackets": [ + [ + "1099/1000", + "11/10" + ], + [ + "11/10", + "1101/1000" + ] + ], + "strict_upper_for_W_times_ln_root_ratio": "5212/1099", + "violated_extension": "allowing rank support through 2^6 while retaining the 12 constant" + }, + "other_alphabet": { + "calls_per_profile": 140, + "coefficients_low_to_high": [ + 36, + -99, + 98, + -41, + 6 + ], + "new": [ + 36, + 0, + 98, + 0, + 6 + ], + "old": [ + 0, + 99, + 0, + 41, + 0 + ], + "rank_base": 3, + "rank_mass_per_profile": 1404, + "roots": [ + "4/3", + "3/2" + ], + "strict_lower_for_12_ln3": "13", + "strict_upper_for_W_ln_root_ratio_ln2": "49/4", + "violated_extension": "transferring 12/ln2 to arbitrary five-rank alphabets", + "width": "ln(9/8)/ln(3)" + } + }, + "status": "pass" +} diff --git a/research/fixed-budget-hidden-windows/independent_check.py b/research/fixed-budget-hidden-windows/independent_check.py new file mode 100644 index 0000000000..8affda61b3 --- /dev/null +++ b/research/fixed-budget-hidden-windows/independent_check.py @@ -0,0 +1,251 @@ +#!/usr/bin/env python3 +"""Independent exact checks for the budget proof and its scope boundaries. + +Standard library only. No imports from the proposed verifier, no subprocesses, +networking, or writes. Polynomials are listed in ascending degree order. +The written proof supplies the uniform analytic inequalities. +""" + +from fractions import Fraction as F +from math import comb, isqrt +import hashlib +import json + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def polynomial_product(left, right): + terms = {} + for i, a in enumerate(left): + for j, b in enumerate(right): + terms[i + j] = terms.get(i + j, 0) + a * b + return [terms.get(i, 0) for i in range(len(left) + len(right) - 1)] + + +def value(coefficients, point): + return sum(c * point ** i for i, c in enumerate(coefficients)) + + +def derivative(coefficients): + return [i * coefficients[i] for i in range(1, len(coefficients))] or [0] + + +def trimmed(coefficients): + answer = list(coefficients) + while len(answer) > 1 and answer[-1] == 0: + answer.pop() + return answer + + +def remainder(numerator, denominator): + work = trimmed([F(c) for c in numerator]) + denominator = trimmed([F(c) for c in denominator]) + need(denominator != [0], 'division by zero polynomial') + while work != [0] and len(work) >= len(denominator): + offset = len(work) - len(denominator) + coefficient = work[-1] / denominator[-1] + for j, c in enumerate(denominator): + work[offset + j] -= coefficient * c + work = trimmed(work) + return work + + +def sturm_count(coefficients, lower, upper): + """Count distinct roots in an interval with non-root endpoints.""" + need(lower < upper, 'reversed interval') + need(value(coefficients, lower) and value(coefficients, upper), 'root at endpoint') + sequence = [trimmed([F(c) for c in coefficients])] + sequence.append(derivative(sequence[0])) + while sequence[-1] != [0]: + next_polynomial = [-c for c in remainder(sequence[-2], sequence[-1])] + if next_polynomial == [0]: + break + sequence.append(next_polynomial) + + def variations(point): + signs = [] + for polynomial in sequence: + v = value(polynomial, point) + if v: + signs.append(1 if v > 0 else -1) + return sum(a != b for a, b in zip(signs, signs[1:])) + + return variations(lower) - variations(upper) + + +def endpoint_polynomial(h, endpoint=2): + # Binomial expansions independently construct each endpoint factor. + first = [comb(h, j) * (-1) ** (h - j) for j in range(h + 1)] + second = [comb(h, j) * (-endpoint) ** (h - j) for j in range(h + 1)] + return polynomial_product(first, second) + + +def profiles(coefficients, rank_base=2): + old = [max(0, -c) for c in coefficients] + new = [max(0, c) for c in coefficients] + old_count, new_count = sum(old), sum(new) + old_mass = sum(c * rank_base ** j for j, c in enumerate(old)) + new_mass = sum(c * rank_base ** j for j, c in enumerate(new)) + need(old_count == new_count, 'counts differ') + need(old_mass == new_mass, 'rank masses differ') + return { + 'coefficients_low_to_high': coefficients, + 'old': old, + 'new': new, + 'calls_per_profile': old_count, + 'rank_mass_per_profile': old_mass, + 'rank_base': rank_base, + } + + +def exact_scope_examples(): + # Seven ranks, two interior roots, integer counts, endpoint order one. + n = 10 + residual = [1 - 2 * (n + 1) ** 2, 4 * n * (n + 1) - 4, + 6 - 2 * n * n, -4, 1] + q = [-c for c in polynomial_product(endpoint_polynomial(1), residual)] + high_degree = profiles(q) + need(q == [482, -1595, 1937, -1010, 180, 7, -1], 'quartic coefficients') + need(high_degree['calls_per_profile'] == 2606, 'quartic call count') + need(high_degree['rank_mass_per_profile'] == 11334, 'quartic rank mass') + need(sturm_count(residual, F(1), F(2)) == 2, 'quartic interior root count') + left, middle, right = F(1099, 1000), F(11, 10), F(1101, 1000) + need(value(residual, left) < 0 < value(residual, middle), 'left bracket signs') + need(value(residual, right) < 0, 'right bracket sign') + need(sturm_count(residual, left, middle) == 1, 'left bracket root count') + need(sturm_count(residual, middle, right) == 1, 'right bracket root count') + need(value(derivative(q), 1) and value(derivative(q), 2), 'endpoint roots not simple') + # ln(s/r) < s/r-1 < right/left-1 = 2/1099. + product_upper = high_degree['calls_per_profile'] * (right / left - 1) + need(product_upper == F(5212, 1099) < 12, 'strict extended-bound violation') + high_degree.update({ + 'interior_roots': 2, + 'root_brackets': [[str(left), str(middle)], [str(middle), str(right)]], + 'residual_at_bracket_points': [str(value(residual, x)) for x in (left, middle, right)], + 'strict_upper_for_W_times_ln_root_ratio': str(product_upper), + 'violated_extension': 'allowing rank support through 2^6 while retaining the 12 constant', + }) + + # The original five ranks, but an edge loss rather than two interior roots. + residual = polynomial_product([-11, 10], [1, 1]) + edge = profiles(polynomial_product(endpoint_polynomial(1), residual)) + need(edge['coefficients_low_to_high'] == [-22, 31, 12, -31, 10], 'edge coefficients') + need(edge['calls_per_profile'] == 53 and edge['rank_mass_per_profile'] == 270, + 'edge count or mass') + need(sturm_count(residual, F(1), F(2)) == 1, 'edge root count') + sample_checks = [] + for k in (1, 2, 3): + # 2^(k/4)>11/10, so every factor's sign is fixed without decimals. + need(2 ** k * 10 ** 4 > 11 ** 4, 'sample is not beyond edge loss') + sample_checks.append({'p': str(F(k, 4)), 'sign': -1}) + need(2 * 10 ** 8 < 11 ** 8, 'p=1/8 is not inside edge loss') + need(F(1, 4) < F(120, 7 * 53), 'grid fails rational mesh criterion') + edge.update({'interior_roots': 1, 'sample_signs': sample_checks, + 'positive_witness': 'p=1/8', + 'maximum_grid_gap': '1/4', + 'safe_mesh_threshold_for_the_two_crossing_class': str(F(120, 7 * 53)), + 'violated_extension': 'applying the mesh corollary to edge losses'}) + + # Five different integer ranks: the power-of-two constant does not transfer. + q = polynomial_product(endpoint_polynomial(1, endpoint=3), [12, -17, 6]) + other_alphabet = profiles(q, rank_base=3) + need(q == [36, -99, 98, -41, 6], 'base-three coefficients') + need(other_alphabet['calls_per_profile'] == 140, 'base-three call count') + need(other_alphabet['rank_mass_per_profile'] == 1404, 'base-three rank mass') + # ln(9/8)<1/8; ln2<7/10; ln3>2*(1/2+(1/2)^3/3)=13/12. + lhs_upper = F(140, 8) * F(7, 10) + rhs_lower = 12 * F(13, 12) + need(lhs_upper == F(49, 4) < rhs_lower == 13, 'base-three bound violation') + other_alphabet.update({'roots': ['4/3', '3/2'], + 'width': 'ln(9/8)/ln(3)', + 'strict_upper_for_W_ln_root_ratio_ln2': str(lhs_upper), + 'strict_lower_for_12_ln3': str(rhs_lower), + 'violated_extension': 'transferring 12/ln2 to arbitrary five-rank alphabets'}) + return {'higher_degree': high_degree, 'edge_window': edge, 'other_alphabet': other_alphabet} + + +def independent_census(budget=1000): + """Use shifted-root parameters a*y^2-t*y+k, y=x-1. + + This is a different enumeration from the proposed verifier's (a,-b,c) + loops. Endpoint positivity and the interior vertex isolate both roots. + """ + ceiling = budget // 3 + count = rational = 0 + digest = hashlib.sha256() + minimum_calls = None + best_objective, minimizers = None, [] + for a in range(1, (ceiling - 1) // 4 + 1): + for t in range(1, 2 * a): + kmin = max(1, t - a + 1) + kmax = min((t * t - 1) // (4 * a), ceiling - 4 * a - 2 * t) + for k in range(kmin, kmax + 1): + b, c = -(2 * a + t), a + t + k + delta = t * t - 4 * a * k + need(delta > 0 and k > 0 and a - t + k > 0, 'shifted root conditions') + q = polynomial_product(endpoint_polynomial(1), [c, b, a]) + cert = profiles(q) + D, z = 4 * a + 2 * t + k, -b + W, Z = 3 * D, (budget // 3 - 1) // 2 + need(cert['calls_per_profile'] == W <= budget, 'half-L1 normalization') + need(all(q[j] * q[j + 1] < 0 for j in range(4)), 'coefficient alternation') + need(D == 2 * z + k and k >= 1 and z > isqrt(delta), 'discrete identities') + need(Z >= z > 1 and delta * Z * Z >= z * z, 'discrete root-ratio bound') + need(F(2, z) >= F(12, budget - 3), 'continuous shifted-budget bound') + count += 1 + rational += isqrt(delta) ** 2 == delta + minimum_calls = W if minimum_calls is None else min(W, minimum_calls) + objective = F(delta, z * z) + item = {'a': a, 'b': b, 'c': c, 'calls_per_profile': W} + if best_objective is None or objective < best_objective: + best_objective, minimizers = objective, [item] + elif objective == best_objective: + minimizers.append(item) + digest.update(f'{a},{b},{c}\n'.encode()) + return {'budget_per_profile': budget, 'quadratics': count, + 'rational_root_pairs': rational, 'irrational_root_pairs': count - rational, + 'minimum_calls_seen': minimum_calls, + 'minimum_Delta_over_trace_squared': str(best_objective), + 'all_minimizing_quadratics': minimizers, + 'shifted_enumeration_order_sha256': digest.hexdigest(), + 'discrete_and_shifted_continuous_bounds_checked': True} + + +def exact_attainment(): + results = [] + for h in (1, 2, 3, 8, 16, 32): + S = 6 ** h // 2 + for n in (3, 4, 10, 100, 10 ** 4, 10 ** 9): + a, b, c = n * (n - 1), -(2 * n * n - 1), n * (n + 1) + q = polynomial_product(endpoint_polynomial(h), [c, b, a]) + q = [(-1) ** (h + 1) * x for x in q] + cert = profiles(q) + N = S * (4 * n * n - 1) + Z = (N // S - 1) // 2 + need(cert['calls_per_profile'] == N, 'attainment call count') + need(a + b + c == 1 and b * b - 4 * a * c == 1, 'attainment k or discriminant') + need(Z == -b and Z > 1, 'attainment Z') + ratio = F(n * n, n * n - 1) + need(ratio == F(Z + 1, Z - 1), 'exact lower-bound attainment') + need(F(1) < F(n + 1, n) < F(n, n - 1) < F(2), 'strict interior roots') + results.append({'h': h, 'n': n, 'budget': N, 'Z': Z, + 'exact_minimum_width': f'log2({ratio})'}) + return results + + +def main(): + receipt = {'status': 'pass', 'arithmetic': 'integer and Fraction only', + 'scope_counterexamples': exact_scope_examples(), + 'independent_census': independent_census(), + 'discrete_bound_attainment': exact_attainment(), + 'limits': ['finite corroboration, not proof assistant verification', + 'independent implementation by another AI worker', + 'does not establish physical supplier realizability']} + print(json.dumps(receipt, indent=2, sort_keys=True)) + + +if __name__ == '__main__': + main() diff --git a/research/fixed-budget-hidden-windows/replay.py b/research/fixed-budget-hidden-windows/replay.py new file mode 100644 index 0000000000..39b4c1bd25 --- /dev/null +++ b/research/fixed-budget-hidden-windows/replay.py @@ -0,0 +1,49 @@ +#!/usr/bin/env python3 +"""Bounded, serial offline replay. Writes no package files. Python 3.10+.""" +from pathlib import Path +from hashlib import sha256 +import json +import os +import platform +import re +import subprocess +import sys + + +def main(): + root = Path(__file__).resolve().parent + environment = {**os.environ, 'PYTHONDONTWRITEBYTECODE': '1'} + environment.pop('PYTHONOPTIMIZE', None) + expected = {'main': (root/'RESULT.json').read_bytes(), + 'independent': (root/'independent-check.json').read_bytes()} + test_code = ('import sys,unittest;sys.path.insert(0,sys.argv[1]);' + 'suite=unittest.defaultTestLoader.loadTestsFromName("test_verify");' + 'result=unittest.TextTestRunner(verbosity=1).run(suite);' + 'sys.exit(not result.wasSuccessful())') + records = [] + for optimized in (False, True): + prefix = [sys.executable, '-I', '-B'] + (['-O'] if optimized else []) + for name, script in (('main','verify.py'), ('independent','independent_check.py'), ('tests',None)): + arguments = ([str(root/script)] if script else ['-c', test_code, str(root)]) + child = subprocess.run(prefix+arguments, cwd=root, env=environment, + capture_output=True, timeout=30, check=False) + if child.returncode: + raise RuntimeError(name+' replay failed: '+child.stderr.decode(errors='replace')) + record = {'check': name, 'optimized': optimized, 'status': 'pass'} + if name in expected: + if child.stdout != expected[name]: + raise RuntimeError(name+' output differs from saved exact receipt') + record['receipt_sha256'] = sha256(child.stdout).hexdigest() + else: + count = re.search(rb'Ran (\d+) tests',child.stderr) + if count is None or int(count.group(1)) != 26: + raise RuntimeError('test suite count changed or was empty') + record['tests'] = 26 + records.append(record) + print(json.dumps({'status':'pass','python':platform.python_version(), + 'writes_package_files':False,'timeout_seconds_per_command':30, + 'serial':True,'runs':records},indent=2,sort_keys=True)) + + +if __name__ == '__main__': + main() diff --git a/research/fixed-budget-hidden-windows/sources/pr6049-README.md.txt b/research/fixed-budget-hidden-windows/sources/pr6049-README.md.txt new file mode 100644 index 0000000000..71bebc3aac --- /dev/null +++ b/research/fixed-budget-hidden-windows/sources/pr6049-README.md.txt @@ -0,0 +1,155 @@ +# Five ranks can hide a losing power window from any fixed finite grid + +Equal call count and rank mass, a fixed five-rank support, and favorable signs +at every member of an arbitrarily large finite sample do not certify a favorable +power-moment comparison. There is a losing open interval between samples. +Five is the smallest possible support for a difference with this two-crossing +sign pattern and the two equalities. This is a scoped algebraic theorem, +with exact finite checks, not a supplier or new kappa. + +The theorem extends [Nick Petalas](https://github.com/petalas)'s one-threshold +[PR #5174](https://github.com/CrocSwap/integer-mult-bounds/pull/5174) rank-exchange construction (pinned in SOURCES.json). The existing exact +[root-budget tool](../../docs/research/recursive-power-variation.md) already +handles multiple crossings; no defect in that tool is alleged. The new result +is the sharp fixed-support impossibility of replacing a complete certificate +by any fixed finite grid. The construction also matches any prescribed finite +number of endpoint derivatives, with a sharp larger support bound. + +## Theorem and construction + +Let S be any finite subset of (0,1). Let J be any nonempty open subinterval +of (0,1) avoiding S, and let h>=1 be an integer. There are two nonnegative +integer paid profiles A,B, whose combined support consists of exactly the ranks + +``` +1, 2, 4, ..., 2^(2h+2), +``` + +whose difference F(p)=sum_r (B_r-A_r) r^p has these properties: + +1. F and its first h-1 derivatives vanish at both p=0 and p=1. +2. There are alpha0 on (alpha,beta) and F<0 everywhere + else in (0,1), except for its two zeros alpha,beta. +3. Their count and rank mass agree. Each has paid ranks below a common + productive target, so subtracting that same target changes none of the signs. +4. The 2h+3 nonzero ranks in the difference are minimal for this sign pattern + and these endpoint multiplicities, among arbitrary distinct positive ranks. + +Choose positive rationals u=a/b and v=c/d with +`1 2^p is continuous and strictly increasing and the rationals are dense. +Expand the integer polynomial + +``` +Q(x) = (-1)^(h+1) (x-1)^h (x-2)^h (b*x-a) (d*x-c) + = sum_(j=0)^(2h+2) q_j x^j. +``` + +At rank 2^j put max(-q_j,0) calls in A and max(q_j,0) calls in B. Then +`F(p)=Q(2^p)` exactly. For 1= 2h+2`, or **s>=2h+3**. The construction attains equality. For h=1, +the fixed support is {1,2,4,8,16}, independently of sample count or gap width. +Large or narrowly placed samples can require large **multiplicities**; this +result does not hold under a separately fixed coefficient budget. + +## Small explicit failed sampling construction + +Take h=1,u=5/4,v=3/2. Then + +``` +Q(x) = 8*x^4 - 46*x^3 + 97*x^2 - 89*x + 30, +A = 89 H_2 + 46 H_8, +B = 30 H_1 + 97 H_4 + 8 H_16. +``` + +Both profiles have 135 calls and rank mass 546. Their difference is negative +at p=1/4 and 3/4 but positive at p=1/2. Exactly, +`F(1/2)=256-181*sqrt(2)>0`, since `256^2 > 2*181^2`. +Thus the sampled cheaper candidate is dearer inside the missed interval. +A multiplier saving C uses p=1-C, which just reverses interval order. + +No finite sample set alone certifies a comparison on the entire interval; +a proved root budget, a sign enclosure on every cell, or a structural order +can do so. The selected source's exact interval checks are not replaced by +this example. No sampled native search is declared invalid merely because +it uses samples for discovery. + +## Evidence and reproduction + +``` +python3.12 -B scripts/research_package.py --package research/hidden-power-windows +python3.12 -B scripts/check_research_commit.py --package research/hidden-power-windows +``` + +The standard-library verifier builds gap witnesses for every interior gap in +uniform grids with denominator 2..24, and narrow root brackets around p=319/320 (saving .003125). +It checks every grid sample using exact integer comparisons of factored +rational roots, reconstructs all integer coefficients, count/mass and endpoint +multiplicity, and verifies the hidden sign at an intervening rational exponent. +Exponent denominators are capped at 2,048 before integer powering; the first +authoring run exceeded its intended memory bound with a large denominator and +was terminated, then replaced by these bounded fixtures. Higher multiplicity +h=1..8 and independent expanded-polynomial interval checks +on the small explicit example are included. Reversed signs, wrong roots, missing +coefficients and false multiplicities are rejected. Normal and optimized modes +are registered and write no package files. The written proof is uniform in S,J,h; +the finite checks corroborate its implementation. + +Base: canonical main 721c03822c421b7f7fcbb2598993b947c4d88419, revision 8, +refreshed on 2026-10-28 UTC. Full selected-supplier replay was not run. The +optional full-source-history check refuses this shallow repository; every pin +is at the immediate main-branch base. No full-history pass is claimed. + +## Significance for researchers + +Even a small rank alphabet with conservation laws can require an interval-wide +power certificate. This gives a sharp adversarial fixture for proposed search +screens and makes the missing hypothesis explicit: sample density alone is +insufficient when integer multiplicities are unbounded. It explains when the +power reduction in [PR #6047](https://github.com/CrocSwap/integer-mult-bounds/pull/6047) needs its ordered-spread premise. + +## Open next questions + +With a fixed maximum coefficient or total-call budget, how narrow can the hidden +window be? First bound the separation of two rational roots of this quadratic +interior factor at that budget, then compare general exponential sums. The +unbounded-multiplicity theorem provides no finite-budget lower bound. + +Can a legal supplier realize a two-crossing exchange? Extract a source-bound +five-rank change with a complete common boundary and all fees. These synthetic +profiles supply no physical construction, restoration, compiler or outer admission. + +## Credit + +Prepared by [zxv](https://github.com/zxv) with substantial OpenAI Codex assistance. +[Nick Petalas](https://github.com/petalas)'s rational-threshold construction +supplies the polynomial-to-invoice precursor. [Ali Romman](https://github.com/aliromman) +supplies the root-budget tool and its retained predecessors; the exponential +zero bound, Rolle argument and polynomial factorization are classical. The +sharp hidden-window formulation and endpoint-matching extension are the scoped +contribution. No independent human or proof-assistant review is claimed. Apache-2.0. diff --git a/research/fixed-budget-hidden-windows/sources/pr6049-verify.py.txt b/research/fixed-budget-hidden-windows/sources/pr6049-verify.py.txt new file mode 100644 index 0000000000..fe4adcc950 --- /dev/null +++ b/research/fixed-budget-hidden-windows/sources/pr6049-verify.py.txt @@ -0,0 +1,158 @@ +"""Sharp hidden-window family: exact algebra and sign checks. Apache-2.0.""" +from fractions import Fraction as F +from pathlib import Path +import hashlib +import json + +HERE=Path(__file__).resolve().parent + + +def need(ok,msg): + if not ok: + raise ValueError(msg) + + +def mul(a,b): + out=[0]*(len(a)+len(b)-1) + for i,x in enumerate(a): + for j,y in enumerate(b): + out[i+j]+=x*y + return out + + +def poly(h,u,v): + need(isinstance(h,int) and 1<=h<=8,'h domain') + need(F(1)0} + need(sum(old.values())==sum(new.values()),'count') + mass=sum(r*n for r,n in old.items()) + need(mass==sum(r*n for r,n in new.items()),'mass') + need(mass>max(old.keys()|new.keys()),'target larger than paid') + return old,new,mass + + +def pow_bounds(p,bits=40): + need(F(0)0)-(delta<0) + + +def sign_factored(p,u,v): + return -sign_power_minus(p,u)*sign_power_minus(p,v) + + +def gap(a,b): + need(F(0)<=a0,'roots inside gap') + return u,v,(a+b)/2 + + +def rejected(fn): + try:fn() + except ValueError:return + raise ValueError('control accepted') + + +def expanded_sign(q,p): + lo,hi=pow_bounds(p,100) + lower=upper=F(0) + for i,c in enumerate(q): + aa,bb=lo**i,hi**i + lower+=c*(aa if c>0 else bb) + upper+=c*(bb if c>0 else aa) + need(lower>0 or upper<0,'expanded sign unresolved') + return 1 if lower>0 else -1 + + +def main(): + root=HERE.parents[1] + pins=json.loads((HERE/'SOURCES.json').read_text()) + for row in pins['files']: + if row['usage']=='input': + need(hashlib.sha256((root/row['path']).read_bytes()).hexdigest()==row['sha256'],'source bytes') + witnesses=samples=0 + for n in range(2,25): + for k in range(n): + a,b=F(k,n),F(k+1,n) + u,v,mid=gap(a,b) + q=poly(1,u,v);validate(q,1) + need(sign_factored(mid,u,v)==1,'hidden loss') + for j in range(1,n): + need(sign_factored(F(j,n),u,v)==-1,'sample win') + samples+=1 + witnesses+=1 + center=F(319,320) + for bits in (24,32,40): + u,v=pow_bounds(center,bits) + for h in range(1,9): + q=poly(h,u,v);validate(q,h) + need(sign_factored(center,u,v)==1,'narrow hidden loss') + need(sign_factored(F(9,10),u,v)==-1,'narrow left sample') + need(sign_factored(F(999,1000),u,v)==-1,'narrow right sample') + witnesses+=1 + q=poly(1,F(5,4),F(3,2)) + need(q==[30,-89,97,-46,8],'literal polynomial') + old,new,mass=validate(q,1) + need((sum(old.values()),mass)==(135,546),'literal count/mass') + for p,want in ((F(1,4),-1),(F(1,2),1),(F(3,4),-1)): + need(expanded_sign(q,p)==want==sign_factored(p,F(5,4),F(3,2)),'expanded oracle') + need(256**2>2*181**2,'exact square-root loss') + rejected(lambda:validate(q,2)) + bad=q.copy();bad[0]+=1 + rejected(lambda:validate(bad,1)) + rejected(lambda:poly(1,F(3,2),F(5,4))) + rejected(lambda:poly(0,F(5,4),F(3,2))) + rejected(lambda:need(sign_factored(F(1,2),F(5,4),F(3,2))==-1,'reversed sign')) + print(json.dumps(dict(status='PASS_HIDDEN_POWER_WINDOWS',witnesses=witnesses, + sampled_wins=samples,minimal_support_h1=5, + scope='sharp scoped proof; synthetic invoices; no new kappa'),sort_keys=True)) + + +if __name__=='__main__':main() diff --git a/research/fixed-budget-hidden-windows/test_verify.py b/research/fixed-budget-hidden-windows/test_verify.py new file mode 100644 index 0000000000..785be3f19b --- /dev/null +++ b/research/fixed-budget-hidden-windows/test_verify.py @@ -0,0 +1,229 @@ +"""Mathematical regression and rejection tests; Python 3.10+ stdlib.""" +from fractions import Fraction as F +from math import isqrt +from pathlib import Path +import copy +import json +import unittest +from unittest.mock import patch + +import verify as v + + +class BudgetWidthTests(unittest.TestCase): + def setUp(self): + self.pa, self.pb = v.build(1, 6, -17, 12) # n=3, roots 4/3 and 3/2 + + def test_source_example(self): + pa, pb = v.build(1, 8, -22, 15) + self.assertEqual(pa, [0, 89, 0, 46, 0]) + self.assertEqual(pb, [30, 0, 97, 0, 8]) + cert = v.certify(1, pa, pb, 135) + self.assertEqual(cert['discriminant'], 4) + self.assertEqual(cert['rank_mass_per_profile'], 546) + + def test_common_paid_padding_is_counted(self): + pa = [x + 7 for x in self.pa] + pb = [x + 7 for x in self.pb] + cert = v.certify(1, pa, pb, 140) + self.assertEqual(cert['common_calls'], 35) + self.assertEqual(cert['uncancelled_calls_per_profile'], 105) + self.assertEqual(cert['actual_calls_per_profile'], 140) + with self.assertRaises(v.Rejected): + v.certify(1, pa, pb, 139) + + def test_budget_is_per_profile(self): + cert = v.certify(1, self.pa, self.pb, 105) + self.assertEqual(cert['actual_calls_per_profile'], 105) + self.assertEqual(sum(self.pa) + sum(self.pb), 210) + with self.assertRaises(v.Rejected): + v.certify(1, self.pa, self.pb, 104) + + def test_reversed_losing_orientation_rejected(self): + with self.assertRaises(v.Rejected): + v.certify(1, self.pb, self.pa, 105) + + def test_noninteger_and_negative_counts_rejected(self): + for bad in (True, False, 0.0, F(0), -1): + with self.subTest(bad=bad): + pa = self.pa[:] + pa[0] = bad + with self.assertRaises(v.Rejected): + v.certify(1, pa, self.pb, 1000) + + def test_noninteger_h_and_budget_rejected(self): + for bad in (True, 1.0, F(1)): + with self.assertRaises(v.Rejected): + v.certify(bad, self.pa, self.pb, 105) + with self.assertRaises(v.Rejected): + v.certify(1, self.pa, self.pb, bad) + + def test_missing_count_conservation_rejected(self): + pa = self.pa[:] + pa[0] += 1 + with self.assertRaisesRegex(v.Rejected, 'count'): + v.certify(1, pa, self.pb, 1000) + + def test_missing_rank_mass_conservation_rejected(self): + pa = self.pa[:] + pa[1] -= 1 + pa[0] += 1 + with self.assertRaisesRegex(v.Rejected, 'mass'): + v.certify(1, pa, self.pb, 1000) + + def test_extra_rank_even_common_padding_rejected(self): + with self.assertRaisesRegex(v.Rejected, 'alphabet'): + v.certify(1, self.pa + [1], self.pb + [1], 106) + + def test_repeated_root_rejected(self): + pa, pb = v.build(1, 4, -12, 9) + with self.assertRaisesRegex(v.Rejected, 'distinct'): + v.certify(1, pa, pb, 1000) + + def test_complex_roots_rejected(self): + pa, pb = v.build(1, 1, -3, 3) + with self.assertRaisesRegex(v.Rejected, 'distinct'): + v.certify(1, pa, pb, 1000) + + def test_endpoint_and_exterior_roots_rejected(self): + # (1,3/2), (3/2,2), (1/2,3/2), and (2,3). + for a, b, c in ((2, -5, 3), (2, -7, 6), (4, -8, 3), (1, -5, 6)): + pa, pb = v.build(1, a, b, c) + with self.subTest(quadratic=(a, b, c)): + with self.assertRaises(v.Rejected): + v.certify(1, pa, pb, 1000) + + def test_false_endpoint_multiplicity_rejected(self): + # Add a pair of roots elsewhere, retaining degree but not h=2 endpoints. + q = [b - a for a, b in zip(self.pa, self.pb)] + q = v.multiply(q, [12, -7, 1]) + pa, pb = [max(-x, 0) for x in q], [max(x, 0) for x in q] + with self.assertRaisesRegex(v.Rejected, 'multiplicity'): + v.certify(2, pa, pb, 100000) + + def test_zero_difference_rejected(self): + with self.assertRaisesRegex(v.Rejected, 'saturated'): + v.certify(1, self.pa, self.pa, 105) + + def test_irrational_pair_accepted_and_enclosed(self): + pa, pb = v.build(1, 5, -15, 11) + cert = v.certify(1, pa, pb, 93) + self.assertFalse(cert['rational_roots']) + self.assertEqual(cert['discriminant'], 5) + out = v.interval_check(cert) + lo, hi = F(out['normalized_ratio_lower']), F(out['normalized_ratio_upper']) + self.assertGreater(lo * lo, 5) + self.assertGreater(hi, lo) + + def test_integer_scaling_and_common_padding(self): + pa, pb = [7*x + 3 for x in self.pa], [7*x + 3 for x in self.pb] + cert = v.certify(1, pa, pb, 750) + self.assertEqual(cert['discriminant'], 49) + self.assertEqual(cert['uncancelled_calls_per_profile'], 735) + self.assertEqual(cert['common_calls'], 15) + v.interval_check(cert) + + def test_finite_budget_sharpness_is_not_claimed(self): + pa, pb = v.build(1, 6, -19, 15) + better = v.certify(1, pa, pb, 120) + family = v.certify(1, self.pa, self.pb, 120) + better_ratio = v.ratio_bounds(better) + family_ratio = v.ratio_bounds(family) + self.assertEqual(better_ratio, (F(10, 9), F(10, 9))) + self.assertEqual(family_ratio, (F(9, 8), F(9, 8))) + self.assertLess(better_ratio[1], family_ratio[0]) + + def test_discrete_budget_bound_exact_attainment(self): + for h in (1, 2, 8, 32): + for n in (3, 10, 10000): + pa, pb = v.build(h, n*(n-1), 1-2*n*n, n*(n+1)) + budget = 6**h*(4*n*n-1)//2 + cert = v.certify(h, pa, pb, budget) + self.assertTrue(cert['discrete_bound_attained']) + self.assertEqual(cert['endpoint_residual_value'], 1) + self.assertEqual(F(cert['discrete_width_ratio_lower']), F(n*n, n*n-1)) + + def test_discrete_bound_not_always_attained(self): + pa, pb = v.build(1, 72, -161, 90) + cert = v.certify(1, pa, pb, 1000) + self.assertFalse(cert['discrete_bound_attained']) + self.assertEqual(cert['budget_trace_cap'], 166) + self.assertEqual(v.ratio_bounds(cert), (F(81, 80), F(81, 80))) + self.assertLess(F(cert['discrete_width_ratio_lower']), F(81, 80)) + + def test_census_against_independent_coefficient_simplex(self): + # Enumerate the whole positive (a,-b,c) simplex allowed by W=3*(a-b+c), + # not the optimized root-derived a and c ranges in enumerate_quadratics. + for budget in (90, 135, 180): + total = budget // 3 + brute = set() + for a in range(1, total): + for z in range(1, total - a): + for c in range(1, total - a - z + 1): + delta = z*z - 4*a*c + # Compare the radical with distance from vertex to each + # boundary; equivalent inequalities, independently arranged. + left, right = z - 2*a, 4*a - z + if delta > 0 and left > 0 and right > 0 and left*left > delta and right*right > delta: + brute.add((a, -z, c)) + self.assertEqual(brute, set(v.enumerate_quadratics(budget))) + + def test_sqrt_bounds_exact_square_and_nonsquare(self): + for n in range(200): + lo, hi = v.sqrt_bounds(n, bits=12) + self.assertLessEqual(lo*lo, n) + self.assertGreaterEqual(hi*hi, n) + self.assertLessEqual(hi-lo, F(1, 4096)) + self.assertEqual(lo == hi, isqrt(n)**2 == n) + + def test_log_positive_series_nested_bounds(self): + for x in (F(1), F(11, 10), F(3, 2), F(2)): + prev = v.log_bounds(x, 1) + for terms in (2, 4, 8, 16): + now = v.log_bounds(x, terms) + self.assertGreaterEqual(now[0], prev[0]) + self.assertLessEqual(now[1], prev[1]) + prev = now + self.assertEqual(v.log_bounds(F(1)), (0, 0)) + + def test_log_outside_domain_rejected(self): + for x in (0, F(1, 2), 3, 1.0, True): + with self.assertRaises(v.Rejected): + v.log_bounds(x) + + def test_endpoint_window_outside_class_rejected(self): + # Reviewer's counterexample to dropping the two-interior-crossing premise. + q = [-22, 31, 12, -31, 10] + pa, pb = [max(-x, 0) for x in q], [max(x, 0) for x in q] + with self.assertRaises(v.Rejected): + v.certify(1, pa, pb, 53) + + def test_source_manifest_metadata_mutations_rejected(self): + root = Path(v.__file__).resolve().parent + original = json.loads((root / 'SOURCES.json').read_text()) + read = Path.read_bytes + for where, key, bad in ((None, 'source_pr', 1), (None, 'source_commit', '0'*40), + (0, 'commit', '0'*40), (0, 'upstream_path', 'wrong/path'), + (0, 'url', 'https://example.invalid/')): + changed = copy.deepcopy(original) + (changed if where is None else changed['files'][where])[key] = bad + replacement = (json.dumps(changed, indent=2)+'\n').encode() + def read_mutation(path): + return replacement if path.name == 'SOURCES.json' else read(path) + with patch.object(Path, 'read_bytes', new=read_mutation): + with self.assertRaisesRegex(v.Rejected, 'provenance manifest'): + v.source_check() + + def test_source_export_mutation_rejected(self): + read = Path.read_bytes + for filename in ('pr6049-README.md.txt', 'pr6049-verify.py.txt'): + def read_mutation(path): + data = read(path) + return data + b'changed\n' if path.name == filename else data + with patch.object(Path, 'read_bytes', new=read_mutation): + with self.assertRaisesRegex(v.Rejected, 'source SHA256'): + v.source_check() + + +if __name__ == '__main__': + unittest.main() diff --git a/research/fixed-budget-hidden-windows/verify.py b/research/fixed-budget-hidden-windows/verify.py new file mode 100644 index 0000000000..f931a0960d --- /dev/null +++ b/research/fixed-budget-hidden-windows/verify.py @@ -0,0 +1,286 @@ +#!/usr/bin/env python3 +"""Exact, bounded corroboration of the theorem in PROOF.md. Python 3.10+ stdlib. + +No networking, subprocesses, imports from upstream, or writes. The uniform +theorem is a written proof; this program checks arithmetic certificates and +finite examples, including every interior quadratic in a declared call budget. +""" +from __future__ import annotations + +from fractions import Fraction as F +from math import isqrt +from pathlib import Path +import hashlib +import json + + +class Rejected(ValueError): + pass + + +def require(condition, message): + if not condition: + raise Rejected(message) + + +def integer(value, name, minimum=None): + require(type(value) is int, name + ' must be an integer, not bool/float') + require(minimum is None or value >= minimum, name + ' is below its minimum') + return value + + +def multiply(a, b): + out = [0] * (len(a) + len(b) - 1) + for i, ai in enumerate(a): + for j, bj in enumerate(b): + out[i + j] += ai * bj + return out + + +def divide_root(coefficients, root): + """Exact division by monic x-root; low-degree coefficient order.""" + require(len(coefficients) >= 2, 'insufficient degree') + quotient = [0] * (len(coefficients) - 1) + quotient[-1] = coefficients[-1] + for j in range(len(quotient) - 2, -1, -1): + quotient[j] = coefficients[j + 1] + root * quotient[j + 1] + require(coefficients[0] + root * quotient[0] == 0, 'endpoint multiplicity fails') + return quotient + + +def build(h, a, b, c): + """Orient the residual a*x^2+b*x+c to be positive in its inner window.""" + integer(h, 'h', 1) + require(h <= 32, 'bounded checker supports h <= 32') + q = [c, b, a] + for _ in range(h): + q = multiply(multiply(q, [-1, 1]), [-2, 1]) + q = [(-1) ** (h + 1) * x for x in q] + return [max(-x, 0) for x in q], [max(x, 0) for x in q] + + +def certify(h, profile_a, profile_b, budget): + """Certify the theorem's domain using integer arithmetic only. + + This certifies neither a legal supplier nor arbitrary rank alphabets. + The two arrays index exactly ranks 2^j; the budget is PER PROFILE. + """ + integer(h, 'h', 1) + require(h <= 32, 'bounded checker supports h <= 32') + integer(budget, 'budget', 1) + require(type(profile_a) in (list, tuple) and type(profile_b) in (list, tuple), 'profiles must be sequences') + degree = 2 * h + 2 + require(len(profile_a) == degree + 1 and len(profile_b) == degree + 1, 'rank alphabet/degree mismatch') + for x in (*profile_a, *profile_b): + integer(x, 'call multiplicity', 0) + na, nb = sum(profile_a), sum(profile_b) + require(na == nb and na <= budget, 'equal per-profile count/budget fails') + ma = sum(x * (1 << j) for j, x in enumerate(profile_a)) + mb = sum(x * (1 << j) for j, x in enumerate(profile_b)) + require(ma == mb, 'rank mass differs') + q = [b - a for a, b in zip(profile_a, profile_b)] + require(q[-1] != 0, 'degree is not saturated') + residual = q[:] + for _ in range(h): + residual = divide_root(residual, 1) + residual = divide_root(residual, 2) + sign = (-1) ** (h + 1) + c, b, a = [sign * x for x in residual] + require(a > 0, 'orientation is not a positive losing inner window') + delta = b * b - 4 * a * c + require(delta > 0, 'interior roots are not distinct') + # Positive endpoint values, negative minimum and interior vertex place + # both roots strictly inside (1,2), without floating-point square roots. + require(2 * a < -b < 4 * a, 'vertex is outside (1,2)') + require(a + b + c > 0 and 4 * a + 2 * b + c > 0, 'roots are not strictly inside (1,2)') + require(all(q[j] * q[j + 1] < 0 for j in range(degree)), 'coefficient alternation fails') + positive, negative = sum(max(x, 0) for x in q), sum(max(-x, 0) for x in q) + w = positive + require(w == negative, 'uncancelled counts differ') + require(2 * w == 6 ** h * (a - b + c), 'half-L1 formula fails') + common = sum(min(x, y) for x, y in zip(profile_a, profile_b)) + require(na == w + common and w <= budget, 'common-padding identity fails') + # All roots positive gives |Q(-1)|=sum|q_j|. Check independently. + require(abs(sum(x * (-1) ** j for j, x in enumerate(q))) == 2 * w, 'evaluation at -1 fails') + count_scale, trace, endpoint_value = 6 ** h // 2, -b, a + b + c + require(w % count_scale == 0 and w // count_scale == 2 * trace + endpoint_value, + 'discrete trace/count identity fails') + trace_cap = (budget // count_scale - 1) // 2 + require(trace_cap >= trace > 1 and endpoint_value >= 1, 'trace budget bound fails') + # (z+sqrt(Delta))/(z-sqrt(Delta)) >= (Z+1)/(Z-1) + # is equivalent, after positive cross multiplication, to Z*sqrt(Delta)>=z. + require(trace_cap * trace_cap * delta >= trace * trace, 'exact discrete width bound fails') + return {'h': h, 'quadratic': [c, b, a], 'discriminant': delta, + 'uncancelled_calls_per_profile': w, 'actual_calls_per_profile': na, + 'common_calls': common, 'budget_per_profile': budget, + 'rank_mass_per_profile': ma, 'support_size': degree + 1, + 'bound_numerator': 2 * 6 ** h, + 'count_scale': count_scale, 'endpoint_residual_value': endpoint_value, + 'trace': trace, 'budget_trace_cap': trace_cap, + 'discrete_width_ratio_lower': str(F(trace_cap + 1, trace_cap - 1)), + 'discrete_bound_attained': delta == 1 and trace == trace_cap, + 'stronger_continuous_bound_denominator': budget - count_scale, + 'rational_roots': isqrt(delta) ** 2 == delta} + + +def sqrt_bounds(n, bits=160): + integer(n, 'radicand', 0) + integer(bits, 'bits', 1) + scale = 1 << bits + floor = isqrt(n << (2 * bits)) + lo = F(floor, scale) + return lo, lo if floor * floor == n * scale * scale else F(floor + 1, scale) + + +def log_bounds(x, terms=48): + """For 1<=x<=2, use 2*atanh(z) and an explicit positive tail bound.""" + require(type(x) in (int, F), 'log argument must be exact') + x = F(x) + require(1 <= x <= 2, 'log interval outside bounded domain') + integer(terms, 'terms', 1) + z = (x - 1) / (x + 1) + z2 = z * z + power, total = z, F(0) + for j in range(terms): + total += 2 * power / (2 * j + 1) + power *= z2 + tail = 2 * power / ((2 * terms + 1) * (1 - z2)) + return total, total + tail + + +def ratio_bounds(certificate): + c, b, a = certificate['quadratic'] + slo, shi = sqrt_bounds(certificate['discriminant']) + rlo, rhi = F(-b - shi, 2 * a), F(-b - slo, 2 * a) + slo_root, shi_root = F(-b + slo, 2 * a), F(-b + shi, 2 * a) + require(1 < rlo <= rhi < slo_root <= shi_root < 2, 'root enclosure unresolved') + return slo_root / rhi, shi_root / rlo + + +def interval_check(certificate): + """Independently enclose W*ln(s/r)/(2*6^h), which must exceed 1.""" + lo, hi = ratio_bounds(certificate) + lower = log_bounds(lo)[0] + upper = log_bounds(hi)[1] + scale = F(certificate['uncancelled_calls_per_profile'], certificate['bound_numerator']) + lower, upper = scale * lower, scale * upper + require(lower > 1, 'numerical enclosure does not certify strict universal bound') + delta_hi = sqrt_bounds(certificate['discriminant'])[1] + require(lower > delta_hi, 'numerical enclosure does not certify discriminant bound') + # Outward rounding keeps the public receipt small; it never determines + # whether the unrounded proof interval passed. Recheck the rounded bounds. + scale_out = 1 << 128 + lower = F((lower * scale_out).__floor__(), scale_out) + upper = F((upper * scale_out).__ceil__(), scale_out) + require(lower > delta_hi, 'rounded receipt does not retain the strict bound') + return {'normalized_ratio_lower': str(lower), 'normalized_ratio_upper': str(upper), + 'strict_bound_certified': True} + + +def enumerate_quadratics(budget): + """Exhaust every oriented integer quadratic with roots in (1,2), h=1. + + W=3*(a+z+c) and W>12*a imply a