From 18cd386d47b415fcc6c6cddde9ae1ac3d1c8749e Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Wed, 11 Nov 2026 13:25:25 +0000 Subject: [PATCH] feat(research): prove sharp bounded-reserve contraction --- research/bounded-adaptive-reserves/PROOF.md | 176 ++++++++++++++++ research/bounded-adaptive-reserves/README.md | 116 +++++++++++ .../bounded-adaptive-reserves/SOURCES.json | 30 +++ research/bounded-adaptive-reserves/TASK.json | 105 ++++++++++ .../bounded-adaptive-reserves/VERIFY.json | 34 +++ research/bounded-adaptive-reserves/verify.py | 197 ++++++++++++++++++ 6 files changed, 658 insertions(+) create mode 100644 research/bounded-adaptive-reserves/PROOF.md create mode 100644 research/bounded-adaptive-reserves/README.md create mode 100644 research/bounded-adaptive-reserves/SOURCES.json create mode 100644 research/bounded-adaptive-reserves/TASK.json create mode 100644 research/bounded-adaptive-reserves/VERIFY.json create mode 100644 research/bounded-adaptive-reserves/verify.py diff --git a/research/bounded-adaptive-reserves/PROOF.md b/research/bounded-adaptive-reserves/PROOF.md new file mode 100644 index 0000000000..7fcdcfb3fb --- /dev/null +++ b/research/bounded-adaptive-reserves/PROOF.md @@ -0,0 +1,176 @@ +# Sharp contraction under a reserve-imbalance cap + +This scoped written proof was produced by Nick Petalas. Apache-2.0. + +## Contract + +Let R1 and R2 be finite nonempty menus of nonnegative real rows of length +two. Write a first-type row as (a,b) and a second-type row as (c,d). +As in Ali Romman's [PR6472](https://github.com/CrocSwap/integer-mult-bounds/pull/6472), +each row choice is independently legal, and each row must already include +the complete costs of its declared children, adapters and restoration. +That interpretation is a premise, not proved for a physical supplier here. + +For B >= 1, define + +```text +q_B = min max { a + b*w2/w1, d + c*w1/w2 : (a,b) in R1, (c,d) in R2 }, +``` + +where the minimum is over w1,w2 > 0 with +max(w1,w2)/min(w1,w2) <= B. Only their ratio matters. Setting x=w2/w1 +reduces the domain to the compact interval [1/B,B], so the minimum exists. + +## Closed form + +For one row pair put + +```text +lambda(a,b,c,d) = (a+d + sqrt((a-d)^2 + 4*b*c))/2. +``` + +Then the exact answer for all finite menus is + +```text +q_B = max { + max_(a,b) [a+b/B], + max_(c,d) [d+c/B], + max_(a,b),(c,d) lambda(a,b,c,d) +}. +``` + +In particular, different row pairs may bind at different parameters. Checking +only a designated whole matrix would omit independently legal combinations. +Zero rows, zero off-diagonal entries, ties and q_B=0 are allowed. + +### Necessity + +If x in [1/B,B] is feasible at rate q, then +q >= a+b*x >= a+b/B and q >= d+c/x >= d+c/B. +Also q-a >= b*x and q-d >= c/x. Both left sides are nonnegative, so +(q-a)(q-d) >= b*c for every pair. + +For q >= max(a,d), this last inequality is equivalent to q >= lambda. +Indeed the quadratic (q-a)(q-d)-bc is nondecreasing on that half-line, +and lambda is its larger root. Thus every feasible rate is at least the +displayed maximum. + +### Sufficiency and the complete weight interval + +Suppose q is at least every term in the displayed maximum. Define + +```text +L(q) = max { 1/B, c/(q-d) for rows (c,d) with c>0 }, +U(q) = min { B, (q-a)/b for rows (a,b) with b>0 }. +``` + +The reserve-boundary terms ensure q>d whenever c>0 and q>a whenever b>0. +Thus all displayed quotients are well-defined and positive. They also give +c/(q-d) <= B and 1/B <= (q-a)/b. Finally the row-pair term gives +c/(q-d) <= (q-a)/b whenever both quotients occur. Every lower candidate +is therefore at most every upper candidate, and L(q) <= U(q). + +For any x in [L(q),U(q)], rows with positive b or c obey the required +inequalities by construction. A row with b=0 requires only q>=a; a row +with c=0 requires only q>=d. The boundary terms already ensure both. +Conversely every feasible x must belong to this interval. Hence [L(q),U(q)] +is exactly the entire feasible ratio set. At q=q_B it is the entire +minimizer set. This proves the formula and supplies explicit weights (1,x). + +## Exact rational certificates + +Suppose the rows and B are rational. For any rational proposed q>=0, +feasibility is decidable without square roots. Check the two boundary +families and all row-pair determinant inequalities. The boundaries imply +q>=max(a,d), so no extraneous lower quadratic branch is admitted. If they +pass, the endpoints L(q),U(q) are rational and give rational witnesses. + +Positive rational weights attain q_B if and only if q_B is rational. +If q_B is rational, the interval just constructed has rational endpoints. +Conversely every row ratio evaluated at rational weights is rational; +the maximum of finitely many rational values is rational. Density and +continuity on [1/B,B] imply that the rational infimum is always q_B, even +when it is not attained. The case B=1 has the single rational ratio x=1. + +This is a certificate statement, not a polynomial bit-complexity claim for +arbitrary algebraic inputs. The verifier implements only rational thresholds. + +## A literal reserve transition + +Consider the new synthetic menu + +```text +R1 = {(0,1/2), (1/8,1/4)}, +R2 = {(1/4,0), (1/16,1/8)}. +``` + +Its four pair roots are sqrt(2)/4, (1+sqrt(17))/16, 1/4 and 1/4. +The second is smaller than the first. To see this, 4*sqrt(2)-1 is +positive, and its square exceeds 17 because 16>8*sqrt(2). +The remaining roots are smaller as well. The boundary terms other than +1/(2B) are + +```text +1/8 + 1/(4B), 1/(4B), 1/8 + 1/(16B). +``` + +For 1<=B<=sqrt(2), each is at most 1/(2B): the first comparison uses +B<=2, and the last uses B<=7/2. For B>=sqrt(2), these decreasing terms +are at most their values at sqrt(2), each below sqrt(2)/4. Therefore + +```text +q_B = max { 1/(2B), sqrt(2)/4 }. +``` + +For B=sqrt(2), the first rows of the two menus force x=1/sqrt(2). +Thus rational Bsqrt(2) does not. For instance B=7/5 gives the exact certificate +x=5/7 and q=5/14. The menus and this reserve law are introduced here; +they are not PR6472's or PR6555's synthetic menu. + +## All-depth consequence of the same cap + +Let T(v)_i be the largest allowed row product at type i. Suppose q<1 +and w is a feasible positive weight. For the adaptive unit-toll recurrence +x_0=0 and x_(k+1)=1+T(x_k), the weighted maximum norm is contracted by +q. This follows from + +```text +|T(v)_i-T(z)_i| <= max_(r in Ri) r*|v-z| <= q*w_i*||v-z||_w. +``` + +Consequently 1+T has a unique fixed point u, its finite-depth iteration +converges to u, and 0<=u-x_k componentwise. Its error obeys + +```text +||u-x_k||_infinity / ||u||_infinity <= B*q^k +``` + +for every integer k>=0. Indeed weighted contraction bounds the error by +q^k*w_i*max_j(u_j/w_j), and converting to the ordinary maximum norm +costs at most max(w)/min(w)<=B. For the literal menu above, substitution +checks the fixed point u=(12/7,10/7). This is an abstract accounting tail, +not physical retained stock or a source-bound compiler cutoff. + +## Credit, originality and limits + +Ali Romman's PR6472 supplies the independent-row accounting interface, +its unit-toll semantics and the explicit common-ratio optimization question. +Classical two-by-two Perron roots, positive diagonal scaling, weighted +norms and contraction arguments are credited as established mathematics. +Global theorem priority for these classical methods is unclaimed. + +Nick Petalas's older PR6555 treats exactly one unbounded synthetic menu, +including its rational approximation and a cutoff. Those results are cited +as background; their menu, identity, construction and cutoff are not used +as the main step here. The contribution is the explicit arbitrary-menu +reserve-cap law, complete minimizer interval and rational-attainment criterion +at the repository's adaptive-row interface, with the new transition fixture. + +No actual supplier row menu is bound. Independent physical legality, +complete native charges, compiler closure, ownership, stock, precision/tape +and analytic recovery remain separate obligations. No selected-frontier +change, new kappa or complete multiplication theorem follows. The universal +claim rests on this written proof; finite checks corroborate it. +Independent human and formal proof-kernel review are unclaimed. diff --git a/research/bounded-adaptive-reserves/README.md b/research/bounded-adaptive-reserves/README.md new file mode 100644 index 0000000000..9c4f274b97 --- /dev/null +++ b/research/bounded-adaptive-reserves/README.md @@ -0,0 +1,116 @@ +# Sharp adaptive contraction with bounded reserves + +For arbitrary finite two-type nonnegative row menus, the best common +contraction rate under a reserve-weight imbalance cap has an explicit closed +form. This is a scoped written mathematical proof with exact finite +corroboration, produced by Nick Petalas. No new kappa is claimed. + +Write first-type rows as (a,b), second-type rows as (c,d), and require +max(w1,w2)/min(w1,w2) <= B for positive weights and B>=1. Then + +```text +best rate = max { + max_(a,b) [a+b/B], + max_(c,d) [d+c/B], + max_(a,b),(c,d) [(a+d+sqrt((a-d)^2+4bc))/2] +}. +``` + +[PROOF.md](PROOF.md) also gives the complete feasible weight interval at +every rate. For rational rows and rational B, rational weights attain the +best rate exactly when that rate is rational. A new synthetic four-row +example has the sharp law max(1/(2B),sqrt(2)/4), including an irrational +plateau where rational weights approach but do not attain the optimum. +The same cap gives the all-depth abstract relative tail bound B*q^k in +the ordinary maximum norm whenever q<1. + +This answers the bounded-reserve version of Open next question 2 in +Ali Romman's [#6472](https://github.com/CrocSwap/integer-mult-bounds/pull/6472). +Its independent adaptive row contract is a cited premise. No predecessor +executable, receipt or scientific census is imported or replayed. +Nick Petalas's older [#6555](https://github.com/CrocSwap/integer-mult-bounds/pull/6555) +solves one uncapped synthetic menu; its menu, identity and cutoff are +background, not the main step here. Classical two-by-two Perron roots, +positive diagonal scaling and weighted contraction retain their credit. +Global mathematical priority for these classical methods is unclaimed. + +## Evidence and reproduction + +The [verifier](verify.py) uses exact fractions. It decides a rational proposed +rate using the formula's boundary charges and determinant inequalities, then +constructs the entire feasible ratio interval. A separate oracle normalizes +w1+w2=1, enumerates all boundary vertices and tests the original row +inequalities directly. It uses no row-pair determinant. + +The complete finite domain contains every singleton or two-distinct-row menu +drawn from {0,1/2,1} squared for each type, budgets 1,3/2,3, and rates +0,1/2,1,3/2,2. All 30,375 decisions agree: 11,831 feasible and 18,544 +infeasible. Every delivered interval endpoint and midpoint is checked +against the original inequalities. Additional checks cover 455 exact phase +thresholds, 387 finite-depth tails, eleven malformed contracts and three +false certificates that expose the pair or reserve-boundary charges. + +From the repository root, with standard-library CPython 3.12: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/bounded-adaptive-reserves/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/bounded-adaptive-reserves/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/bounded-adaptive-reserves +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/bounded-adaptive-reserves --check-source-history +``` + +Another CPython 3.12 executable may replace the host-specific path. Each +direct replay prints a generated JSON receipt bound to all six package +files, followed by PASS_BOUNDED_ADAPTIVE_RESERVES. It writes no files. +Both registered commands have identical coverage and a 120-second deadline. +Exact provenance pins, including the cited predecessor proof, are in +[SOURCES.json](SOURCES.json). There are no live external proof inputs. + +## Scope and implementation limits + +The theorem covers all finite real nonnegative menus and all real B>=1. +The executable decides rational thresholds for at most sixteen rows per +type, with rational input numerators and denominators of at most 64 bits. +These executable bounds do not narrow the written theorem. + +There is no recursion, subprocess or network call. A decision has at most +256 row pairs, and the independent oracle has at most 34 vertex candidates. +The replay domain is fixed. Every function is below sixty physical lines, +and explicit invariant failures remain enabled under optimized Python. +Managed allocation is a power-of-ten deviation: fractions and collections +allocate during execution, but the input sizes, menu counts, source-file +sizes and every iteration domain are bounded. The only source I/O reads +the fixed six-file receipt inventory. Warning-strict normal and optimized +execution and AST inspection are the available diagnostics; no separate +static type checker or repository-wide analysis is claimed. + +No actual complete supplier menu, physical reserve, native delivery, +restoration, compiler, ownership, precision/tape or analytic recovery is +established. The five selected framework assumptions remain. There is no +selected-frontier change, complete multiplication theorem, selected cold +replay, Lean or Docker run. The universal result rests on the written proof, +not finite extrapolation. Independent human and formal proof-kernel review +are unclaimed. + +## Open next questions + +1. Bind one complete current two-type menu and its real reserve consumer. + Start with every child, adapter and restoration charge and the permitted + B. The missing source-to-row mapping blocks any physical improvement. +2. Retain an explicit reserve cap for three or more types. Start with a + rational threshold, one normalized weight and all pairwise reserve + inequalities. A useful higher-type formula and consumer remain open. + +The structured first steps and blockers are in [TASK.json](TASK.json). +The [advance CLAIM](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19542404) +records the scope. Source/author reservations, live PRs and Discussions, +recent account work, main README text and merged PRs were searched for +overlap. Sparse omitted notes, arbitrary historical diffs and unpublished +work remain limits; the search is not a novelty certificate. + +## Credit + +This contribution was produced by Nick Petalas. Ali Romman supplies PR6472's +row contract and optimization question, with its credited M-matrix, +Bellman, independent-row-uncertainty and typed-recursion lineage. The +predecessor's full attribution remains unchanged. New work is Apache-2.0. diff --git a/research/bounded-adaptive-reserves/SOURCES.json b/research/bounded-adaptive-reserves/SOURCES.json new file mode 100644 index 0000000000..4dc234b986 --- /dev/null +++ b/research/bounded-adaptive-reserves/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "75d77b328ea02ded535e7f23aee5b1e55d0bb1a8", + "sha256": "154c3d30455d778fd3343b6b4851f0fa4665f0f7625b0adb3675e2bafbbf6bf1" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/adaptive-row-bill/PROOF.md", + "usage": "provenance", + "git_blob": "607bdf91c6afce0868f7590b8793f1c2179d56fc", + "sha256": "a82bfb07994a1c0d45fdddf999859c534a78c7dbd37c64f554330175116bf0f9" + }, + { + "path": "research/adaptive-row-bill/README.md", + "usage": "provenance", + "git_blob": "7cbff7f56584e7246c34285761a935e5308fc793", + "sha256": "53a7b1a4c4df08594aed63d791ae01cae0f7f7f339db1ae2b2060fa6c9c86012" + } + ] +} diff --git a/research/bounded-adaptive-reserves/TASK.json b/research/bounded-adaptive-reserves/TASK.json new file mode 100644 index 0000000000..dc97d356a1 --- /dev/null +++ b/research/bounded-adaptive-reserves/TASK.json @@ -0,0 +1,105 @@ +{ + "schema_version": 1, + "task_id": "independent-moment", + "priority_revision": 8, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "original_card": { + "id": "independent-moment", + "question": "Does a changed construction's serialized target/paid invoice independently support its claimed improvement?", + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "docs/research/recursive-invoice-preflight.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "acceptance_gate": "Demonstrate independence, source binding, positive cases and semantic failure controls. Name the existing checks and the missing coverage. More digits or another equivalent evaluation of an unchanged root is not by itself new verification coverage.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "Independently recount one changed emitted word and its complete caller, importing no constructor or pricing engine. Include target losses, owned lifetimes, native orientation and extra charges. Check existing #5633/#5708/#5717/#5719 coverage to avoid duplicate audits and preserve its exact head. Stop after the chosen missing implication; a correct root alone is not supplier admission.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "overlap_terms": [ + "invoice", + "signed moment", + "productive target", + "independent recount" + ], + "existing_checks": [ + { + "scope": "PR #4088: mixed local/owner/phase ledger and moment reported.", + "evidence": "research/staged544-mixed-fourth-entry/README.md", + "remaining": "Independent binding of changed construction to paid histogram, distinct from full admission.", + "status": "author-checked", + "source_commit": "72d7efc181edb21806a878f174847c96dd410ab0", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4091: sharp pooled ceiling proposed for fixed THREE/FOUR words and inventory.", + "evidence": "research/staged-fourth-mixture-ceiling/README.md", + "remaining": "Validate dual, exhaustive pattern scope and exact source equivalence before applying to newer fills.", + "status": "author-checked", + "source_commit": "a29bdd8f56cd18b805917775cdec09ff935eddc4", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4067: paid (2,2) to (1,3) exchange and fixed OQ4 host reported.", + "evidence": "research/r437-two-window-carrier/README.md", + "remaining": "Independent full cost delta; remaining caller/precision/stock obligations are separate.", + "status": "author-checked", + "source_commit": "a95f11c52e3ca1e4c5171b3c20d8f4b0815aee2e", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Sharp common contraction and complete feasible weight ratios for finite two-type nonnegative row menus under a rational reserve-imbalance cap.", + "scope_change_reason": "Replace a predecessor recount by the open common-ratio optimization question of Ali Romman PR6472, adding an explicit reserve cap. This is a scoped abstract accounting result.", + "bottleneck_link": "A contraction rate alone omits the imbalance of reserve weights. The closed form exposes the exact tradeoff before a compiler claims a reserve or tail bound; no actual physical menu is supplied.", + "budget_minutes": 60, + "stop_rule": "Ship the first verified sharp reserve law; leave actual supplier binding and higher-type work open.", + "outcome": "completed", + "evidence": "PROOF.md; verify.py: 30375 exact rational decisions against normalized vertex enumeration, 455 transition thresholds, 387 tail prefixes and 14 rejecting controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Which complete current two-type supplier menu can use the bounded-reserve law?", + "why_it_matters": "Only source-bound rows and a real reserve consumer can turn this accounting result into a physical improvement.", + "first_step": "Serialize every legal alternative with all child, adapter and restoration charges and identify the permitted reserve ratio B.", + "blocked_by": "No physical two-type menu, complete source mapping or reserve consumer is supplied." + }, + { + "question": "Can a useful closed form or compact certificate retain an explicit reserve cap for three or more types?", + "why_it_matters": "The two-type interval argument does not extend to independent ratios without compatibility constraints.", + "first_step": "Fix three types and a rational threshold, normalize one weight, and retain all pairwise reserve inequalities in the resulting linear feasibility problem.", + "blocked_by": "A higher-type elimination formula and an actual complete consumer remain open." + } + ] +} diff --git a/research/bounded-adaptive-reserves/VERIFY.json b/research/bounded-adaptive-reserves/VERIFY.json new file mode 100644 index 0000000000..e53c018114 --- /dev/null +++ b/research/bounded-adaptive-reserves/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact bounded-reserve thresholds against independent normalized polytope vertices, phase law, finite-depth tail and malformed/false-certificate controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Identical exact coverage with optimization enabled; explicit errors must remain active." + } + ] +} diff --git a/research/bounded-adaptive-reserves/verify.py b/research/bounded-adaptive-reserves/verify.py new file mode 100644 index 0000000000..e14506321a --- /dev/null +++ b/research/bounded-adaptive-reserves/verify.py @@ -0,0 +1,197 @@ +#!/usr/bin/env python3 +"""Exact bounded-reserve contraction checks, produced by Nick Petalas. + +Apache-2.0. Independent human and formal proof-kernel review are unclaimed. +""" + +from fractions import Fraction as F +from hashlib import sha256 +from itertools import combinations, product +import json +from pathlib import Path +import platform +import sys + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def validate(first, second, budget, rate): + for menu in (first, second): + require(type(menu) is tuple and 1 <= len(menu) <= 16, "menu size/type") + for row in menu: + require(type(row) is tuple and len(row) == 2, "row shape") + for entry in row: + require(type(entry) is F and entry >= 0, "nonnegative rational row") + require(max(entry.numerator.bit_length(), + entry.denominator.bit_length()) <= 64, "entry size") + for value in (budget, rate): + require(type(value) is F, "rational budget/rate") + require(max(abs(value.numerator).bit_length(), + value.denominator.bit_length()) <= 64, "scalar size") + require(budget >= 1 and rate >= 0, "budget/rate domain") + + +def bounded_weights(first, second, budget, rate): + """Return all feasible ratios w2/w1 as a closed rational interval, or None.""" + validate(first, second, budget, rate) + if any(a + b / budget > rate for a, b in first): + return None + if any(d + c / budget > rate for c, d in second): + return None + for (a, b), (c, d) in product(first, second): + if (rate - a) * (rate - d) < b * c: + return None + low, high = 1 / budget, budget + for c, d in second: + if c: + low = max(low, c / (rate - d)) + for a, b in first: + if b: + high = min(high, (rate - a) / b) + require(0 < low <= high, "nonempty interval theorem") + return low, high + + +def literal_ok(first, second, budget, rate, w1, w2): + if min(w1, w2) <= 0 or max(w1, w2) > budget * min(w1, w2): + return False + return (all(a * w1 + b * w2 <= rate * w1 for a, b in first) + and all(c * w1 + d * w2 <= rate * w2 for c, d in second)) + + +def vertex_oracle(first, second, budget, rate): + """Enumerate normalized polytope vertices; do not use pair determinants.""" + candidates = [1 / (budget + 1), budget / (budget + 1)] + for a, b in first: + slope = a - b - rate + if slope: + candidates.append(-b / slope) + for c, d in second: + slope = c - d + rate + if slope: + candidates.append((rate - d) / slope) + for w1 in candidates: + if literal_ok(first, second, budget, rate, w1, 1 - w1): + return w1, 1 - w1 + return None + + +def compare(first, second, budget, rate): + interval = bounded_weights(first, second, budget, rate) + vertex = vertex_oracle(first, second, budget, rate) + require((interval is None) == (vertex is None), "independent decision mismatch") + if interval is not None: + for ratio in (interval[0], sum(interval) / 2, interval[1]): + require(literal_ok(first, second, budget, rate, F(1), ratio), + "invalid delivered weight") + require(interval[0] <= vertex[1] / vertex[0] <= interval[1], + "oracle vertex outside complete feasible interval") + return interval is not None + + +def census(): + rows = tuple(product((F(0), F(1, 2), F(1)), repeat=2)) + menus = tuple((row,) for row in rows) + tuple(combinations(rows, 2)) + count = feasible = 0 + for first, second in product(menus, repeat=2): + for budget in (F(1), F(3, 2), F(3)): + for rate in (F(0), F(1, 2), F(1), F(3, 2), F(2)): + feasible += compare(first, second, budget, rate) + count += 1 + return {"cases": count, "feasible": feasible, "infeasible": count - feasible} + + +def phase_law(): + first = ((F(0), F(1, 2)), (F(1, 8), F(1, 4))) + second = ((F(1, 4), F(0)), (F(1, 16), F(1, 8))) + count = 0 + for budget in (F(1), F(5, 4), F(7, 5), F(3, 2), F(2), F(4), F(100)): + for numerator in range(65): + rate = F(numerator, 64) + expected = rate >= 1 / (2 * budget) and 8 * rate * rate >= 1 + require(compare(first, second, budget, rate) == expected, "phase law") + count += 1 + interval = bounded_weights(first, second, F(7, 5), F(5, 14)) + require(interval == (F(5, 7), F(5, 7)), "literal boundary interval") + require(bounded_weights(first, second, F(7, 5), F(5, 14) - F(1, 10000)) + is None, "false strict improvement") + return count + + +def tail_checks(): + first = ((F(0), F(1, 2)), (F(1, 8), F(1, 4))) + second = ((F(1, 4), F(0)), (F(1, 16), F(1, 8))) + total = (F(12, 7), F(10, 7)) + count = 0 + for budget in (F(1), F(5, 4), F(7, 5)): + rate = 1 / (2 * budget) + require(bounded_weights(first, second, budget, rate) is not None, "tail weight") + current = (F(0), F(0)) + for depth in range(129): + error = max(total[i] - current[i] for i in range(2)) + require(min(total[i] - current[i] for i in range(2)) >= 0, "prefix overshoot") + require(error <= budget * rate ** depth * max(total), "all-depth tail") + current = tuple(1 + max(a * current[0] + b * current[1] for a, b in menu) + for menu in (first, second)) + count += 1 + require(all(1 + max(a * total[0] + b * total[1] for a, b in menu) == total[i] + for i, menu in enumerate((first, second))), "fixed point") + return count + + +def rejection_controls(): + row = ((F(0), F(1)),) + cases = [ + ((), row, F(1), F(1)), + (list(row), row, F(1), F(1)), + (((F(0),),), row, F(1), F(1)), + (((F(-1), F(0)),), row, F(1), F(1)), + (((True, F(0)),), row, F(1), F(1)), + (((F(2 ** 64), F(0)),), row, F(1), F(1)), + (row, row, F(1, 2), F(1)), + (row, row, F(1), F(-1)), + (row, row, 1, F(1)), + (row, row, F(1), F(1, 2 ** 64)), + (row * 17, row, F(1), F(1)), + ] + for args in cases: + try: + bounded_weights(*args) + except ValueError: + continue + raise ValueError("malformed contract accepted") + zero, double = ((F(0), F(0)),), ((F(0), F(2)),) + fixtures = ((double, ((F(2), F(0)),), F(4)), + (double, zero, F(1)), (zero, ((F(2), F(0)),), F(1))) + for first, second, budget in fixtures: + require(vertex_oracle(first, second, budget, F(1)) is None, "false certificate") + require(bounded_weights(first, second, budget, F(1)) is None, "missing charge") + return len(cases) + len(fixtures) + + +def receipt(result): + package = Path(__file__).resolve().parent + names = ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", "VERIFY.json", "verify.py") + hashes = {} + for name in names: + require((package / name).stat().st_size <= 262144, "package source bound") + payload = (package / name).read_bytes() + require(len(payload) <= 262144, "package source bound") + hashes[name] = sha256(payload).hexdigest() + return {"schema": "bounded-adaptive-reserves/v1", "result": result, + "sources_sha256": hashes, "python": platform.python_version()} + + +def main(): + require(sys.version_info[:2] == (3, 12), "requires CPython 3.12") + result = {"census": census(), "phase_thresholds": phase_law(), + "tail_prefixes": tail_checks(), "rejections": rejection_controls()} + print(json.dumps(receipt(result), sort_keys=True)) + print("PASS_BOUNDED_ADAPTIVE_RESERVES") + + +if __name__ == "__main__": + main()