diff --git a/research/midpoint-rank-credit/README.md b/research/midpoint-rank-credit/README.md new file mode 100644 index 0000000000..a8c3de887b --- /dev/null +++ b/research/midpoint-rank-credit/README.md @@ -0,0 +1,236 @@ +# Stronger rational credit for paid rank exchanges + +This contribution was produced by Nick Petalas. Apache-2.0. + +Claim type: scoped mathematical proof with exact finite corroboration. +For every integer rank k>=2, a midpoint convexity argument strengthens +the rational curvature allowance in Dugongue's +[PR3863](https://github.com/CrocSwap/integer-mult-bounds/pull/3863). +It answers that package's second Open next question. On its stated interval, +1,181 proposed `2+2 -> 1+3` exchanges suffice to fund one extra rank-one +child, reducing the cited sufficient target of 1,775 by 594 exchanges. +This is a stronger accounting certificate, not a constructed rewrite, +a minimum count for the true power moment, or a new kappa. + +The predecessor's capped-mass identity and paid-overhead transfer are +cited ingredients. No predecessor program, supplier or theorem is audited. +The new step is the larger uniform rational coefficient below and its +strict paid consequence. Jensen's inequality is classical; no general +convexity or literature-wide priority claim is made. + +## Uniform coefficient and proof + +For any real `0 < ell <= a <= u < 1`, let + +```text +f_a(x) = x^(1-a), f_a(0)=0, +theta_k(a) = 2 f_a(k) - f_a(k-1) - f_a(k+1). +``` + +For every integer k>=2, the new bound is + +```text +theta_k(a) >= ell(1-u) / [ k (1+u(k-1)) ]. (1) +``` + +The endpoints can be rational, making the right side rational without +evaluating a logarithm or a nonintegral power. The earlier sufficient +coefficient was `ell(1-u)/[(k+1)(1+uk)]`. The new coefficient is strictly +larger for every k>=2 and every permitted interval. + +Two integrations give the credited triangular-kernel identity + +```text +theta_k(a) = a(1-a) integral_-1^1 + (1-|t|) (k+t)^(-1-a) dt. +``` + +The triangular density has mass one and mean zero. The function +`x -> x^(-1-a)` is strictly convex on positive x, since its second derivative +is `(1+a)(2+a)x^(-3-a)>0`. Jensen's inequality therefore gives + +```text +theta_k(a) > a(1-a) k^(-1-a). +``` + +All arguments of the integrand are positive because k>=2. The tangent +inequality for the concave function `x^a` at x=1 gives + +```text +k^a <= 1+a(k-1) <= 1+u(k-1), +a(1-a) >= ell(1-u). +``` + +Taking the reciprocal of the first positive inequality and multiplying +proves (1), in fact strictly. For the coefficient comparison, both factors +in `(k+1)(1+uk)` exceed their positive counterparts in +`k(1+u(k-1))`. The numerators agree and are positive. + +At k=1 retain the predecessor bound + +```text +theta_1(a) >= 4 ell/(3+2 ell). +``` + +For completeness, `theta_1=2(1-exp(-a log 2))`, +`log 2>=2/3`, and `1-exp(-x)>=x/(1+x)` for x>=0 prove this bound. +No midpoint integral through zero is asserted. + +## Complete finite profiles and paid charges + +Let old and new counts `o_r,n_r` be nonnegative integers on ranks 1,...,T, +with T>=2, and define + +```text +d_r = n_r-o_r, +C_k = sum_r d_r min(r,k). +``` + +Assume `C_T=0` and every `C_k<=0`. The retained finite identity gives + +```text +sum_r (o_r-n_r) r^(1-a) = sum_(k=1)^(T-1) (-C_k) theta_k(a). +``` + +Thus a sufficient uniform raw credit is + +```text +L_mid = (-C_1) 4 ell/(3+2 ell) + + sum_(k=2)^(T-1) (-C_k) ell(1-u)/[k(1+u(k-1))]. +``` + +It never weakens the earlier credit. It strictly strengthens that credit +whenever any `C_k<0` for k>=2. This comparison concerns sufficient lower +bounds, not exact moment optima. If the only nonzero deficit is at k=1, +the two certificates coincide. + +For any actual additional nonnegative integer-rank histogram `e_r`, put +`Q=sum_r r e_r`. Since `r^(1-a)<=r` for r>=1, the complete paid raw moment +strictly improves whenever `Q 1+3` exchange, only `C_2=-1` is nonzero. At +`ell=17/10000` and `u=18/10000`, + +```text +L_mid = 84847/100180000, +1180 L_mid <= 1 < 1181 L_mid, +1181 L_mid - 1 = 24307/100180000 > 0. +``` + +Therefore 1,181 exchanges, followed by one additional rank-one child, +strictly lower the complete raw moment throughout that closed interval. +The proposed exchanges need 2,362 available rank-two children. This package +does not assert that any particular current source can realize them. +The preceding rational coefficient is `84847/150540000`; its sufficient +threshold is 1,775. At 1,181 exchanges it does not certify the paid charge. + +The count 1,181 is minimal for the displayed sufficient inequality. No +claim is made that 1,180 actual exchanges cannot pay the charge. The bound +deliberately discards curvature information. Research stops at this first +strict improvement rather than optimizing that true threshold. + +## Exact replay + +From the repository root, with CPython 3.12 and only its standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/midpoint-rank-credit/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/midpoint-rank-credit/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/midpoint-rank-credit +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/midpoint-rank-credit --check-source-history +``` + +Any CPython 3.12 executable may replace the local path. The final command +checks exact publication bytes and source ancestry after committing. +Expected direct marker is `PASS_MIDPOINT_RANK_CREDIT`. JSON stdout is a +generated receipt bound to all five package files. No receipt is handwritten +or committed; replay writes no files and imports no predecessor executable. + +The checker independently encloses powers with rational positive atanh +series and Taylor series, each with an explicit geometric remainder. It +reduces r to `2^b t` with `1<=t<2`, evaluates 24 logarithm terms, and +encloses `exp(-x)` by reciprocating and raising an enclosure of `exp(x/8)` +to the eighth power. Its 24th-degree positive exponential sum has first +omitted term `v_25`, with tail at most `v_25/(1-y/26)` for `y=x/8<=5/8`. +Monotonicity determines the endpoint directions. No floating-point +acceptance or sampled claim about an entire interval is used. + +The direct replay reports 288 curvature comparisons at ranks 1,...,32, +using both endpoints and midpoints of three intervals: the paid example, +`[1/8,1/4]` and `[1/3,2/3]`. Ninety-nine integer square/cube comparisons +separately corroborate the power enclosures at a=1/3,1/2,2/3. +All 81 count profiles on ranks 1,...,4 with counts 0,1,2 are paired. +There are 155 unequal eligible pairs, giving 465 profile/interval pairs +and 1,395 complete power-moment comparisons at the nine points. +These finite checks support the implementation. The written proof supplies +the all-rank and all-real-interval result. + +Twelve invalid profile/interval cases must reject. Separate controls cover +zero gain, exact rank-one powers and the unsound favorable-endpoint bound +`theta_2(1/2)>=1/4`. Explicit exceptions keep all fifteen controls active +under `-O`. + +## Scope, provenance and limits + +Canonical base is `7c49fe32c55de02c2c873655c804b16e4c3fef0a`, priority +revision 8. The selected source-binding positive control passed and resolves +PR6030 as selected. It is metadata orientation, not a supplier replay. +TASK.json changes the scalar-to-moment card to this accounting side result; +it does not claim a chronological construction satisfying the original gate. +SOURCES.json pins the card, selected record and conceptual predecessor +README/proof as provenance. There are no live external proof inputs. + +The verifier accepts no CLI search-size parameters. Its profile evaluator +allows at most 65 entries, each count at most one million, and rational +endpoint denominators at most one million. The fixed enumeration examines +three sets of 6,561 profile pairs. Curvature checks use at most 33 positive +power values per point; every analytic series has exactly 24 iterations. +All functions fit within sixty physical lines. There is no recursion, +subprocess, network request, dynamic evaluation or persistent resource. +CPython managed allocation is a bounded deviation from fixed steady-state +allocation. Standard-library internal allocation is not audited. +Warning-strict normal and optimized execution and AST inspection provide +available diagnostics; no standalone linter is installed. + +No physical/native circuit, supplier admission, dirty restoration, compiler, +stock, precision/tape proof, selected-frontier change or complete +multiplication theorem is supplied. No selected cold replay, Lean or Docker +suite was run. Independent human and formal proof-kernel review are unclaimed. + +Credit Dugongue / PR3863 for the explicit opening, the triangular integral, +the earlier quantitative allowance and paid-overhead framework. Credit the +ranked-pair verification and Avi Eisenberg / ikeboy, eumemic, Chafik Boukhalfa, +Dominik Scholz and their retained lineage for the capped-mass identity and +all-exponent sign theorem. MathProof supplies the earlier reserve framework. +The classical tools retain their credit. Predecessor files and credit lines +are unchanged. + +Live open and account PRs, active Discussions, recent handoffs, local +reservations, main README formula/object searches and merged general-form +searches were checked before the +[advance CLAIM](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19362857). +The cached card search covered 406 open PRs and 6,350 Discussion records, +with only 114 of 8,917 local HEAD notes in the sparse checkout. Separate +main-tree searches supplement that limit. No search establishes novelty +against unpublished work, arbitrary historical diffs or all literature. + +## Open next questions + +1. Can a legal chronological exchange attain this stronger paid target? + First freeze one compatible source pair, construct its arbitrary-dirty + endpoint identity and list every added fee. Native compatibility, + ownership, chronology, restoration and compiler/precision/stock remain + blockers. The accounting certificate alone does not fund unknown work. +2. What is the least actual exchange count on the stated interval? + First bound the derivative of `2*2^(1-a)-1-3^(1-a)` and certify its + minimum with rational enclosures. Global monotonicity and true-threshold + optimality are unproved here. No follow-on search is reserved. + +Structured questions and blockers are in [TASK.json](TASK.json). diff --git a/research/midpoint-rank-credit/SOURCES.json b/research/midpoint-rank-credit/SOURCES.json new file mode 100644 index 0000000000..5880eb39c9 --- /dev/null +++ b/research/midpoint-rank-credit/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/charged-rank-dominance/PROOF.md", + "usage": "provenance", + "git_blob": "f91c3e5439861c2ad48d42c752beb8f926b52722", + "sha256": "85bdbcb669e347cf3d0ead47d5d2af818a40a5e4fb6a47224b3b8bd96bb42e55" + }, + { + "path": "research/charged-rank-dominance/README.md", + "usage": "provenance", + "git_blob": "037ed3f6c530872ca303c325fdf31d8b48a5d125", + "sha256": "789bbbcb443454e839d1a955517827dff20f95cdb95d5aff57a3d5ebd8b85b17" + } + ] +} diff --git a/research/midpoint-rank-credit/TASK.json b/research/midpoint-rank-credit/TASK.json new file mode 100644 index 0000000000..a5ed9d71b0 --- /dev/null +++ b/research/midpoint-rank-credit/TASK.json @@ -0,0 +1,113 @@ +{ + "schema_version": 1, + "task_id": "scalar-to-moment", + "priority_revision": 8, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "original_card": { + "id": "scalar-to-moment", + "question": "Can a scalar/frame rewrite improve the complete signed moment through paid jobs, productive targets, or both?", + "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": "Require a legal chronological rewrite and favorable complete signed target-minus-paid moment with all extra charges. Unchanged ADD counts or unchanged paid-call counts alone decide neither success nor failure. Compiler, native and outer admission remain separate obligations.", + "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": "Construct one legal source-bound rewrite and compare complete before/after P and T. Charge restoration, source windows and owned helpers. A paid call need not disappear: a legal target split or rank redistribution may win. Stop if the signed moment is unchanged or the consumer repays the gain. Do not extend a scalar-only census on ADD counts.", + "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": [ + "signed moment", + "target split", + "rank exchange", + "scalar rewrite" + ], + "existing_checks": [ + { + "scope": "PR #3998: consecutive A2 scalar contraction", + "evidence": "research/staged544-a2-graph-rewrite/README.md", + "remaining": "A genuinely changed paid itinerary or a distinct independent audit; no default scalar-only expansion.", + "status": "author-checked", + "source_commit": "389268a6b5e0373a3125d5c6fcd6995f4ea324f5", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4019: separated A2 sites with unchanged recursive histogram", + "evidence": "research/staged544-separated-a2/README.md", + "remaining": "A genuinely changed paid itinerary or a distinct independent audit; no default scalar-only expansion.", + "status": "author-checked", + "source_commit": "f408e09df300b575235f7f77f81948071397e16d", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4112: composition audit", + "evidence": "research/staged544-a2-composition-audit/README.md", + "remaining": "A genuinely changed paid itinerary or a distinct independent audit; no default scalar-only expansion.", + "status": "author-checked", + "source_commit": "205b7380656ba4b6316a8a493b1a3c679b8f7a0e", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4152: A1858 contraction audit", + "evidence": "research/staged544-a1858-contraction-audit/README.md", + "remaining": "A genuinely changed paid itinerary or a distinct independent audit; no default scalar-only expansion.", + "status": "author-checked", + "source_commit": "caaa14cde5962adc372fdca71f63d0f29e73c8b2", + "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": "Stronger uniform rational curvature credits for capped-mass paid rank exchanges, answering PR3863 Open next question 2.", + "scope_change_reason": "An original accounting lemma and sufficient paid target, rather than a chronological scalar/frame rewrite. Physical construction remains open.", + "bottleneck_link": "A complete added route or restoration bill must fit below the power-moment gain. The stronger sufficient credit reduces the exchange inventory required before such a construction can be funded.", + "budget_minutes": 60, + "stop_rule": "Stop at the first strictly stronger verified credit and package it; do not search for a smaller true exchange minimum or a physical word.", + "outcome": "completed", + "evidence": "README.md supplies the all-rank proof. verify.py emits exact rational comparisons, power enclosures, rejection controls and package hashes.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can a legal chronological 2+2 to 1+3 rewrite attain the stronger paid target with all extra costs charged?", + "why_it_matters": "The accounting allowance becomes a supplier improvement only after physical delivery and restoration are constructed.", + "first_step": "Choose one source-bound compatible rank-two pair, construct its dirty endpoint identity, and record every added fee before aggregating.", + "blocked_by": "Native compatibility, ownership, chronology, restoration and compiler/precision/stock obligations are not supplied." + }, + { + "question": "What is the least actual exchange count funding one rank-one child on the stated saving interval?", + "why_it_matters": "1181 is the least count certified by this lower bound, not the optimum of the true power moment.", + "first_step": "Bound the derivative of the literal 2*2^(1-a)-1-3^(1-a) expression uniformly, then certify its endpoint minimum with rational power enclosures.", + "blocked_by": "No global monotonicity or true-threshold optimality proof is supplied here." + } + ] +} diff --git a/research/midpoint-rank-credit/VERIFY.json b/research/midpoint-rank-credit/VERIFY.json new file mode 100644 index 0000000000..33a0f945bc --- /dev/null +++ b/research/midpoint-rank-credit/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": 240, + "checks": "Exact midpoint-credit consequences, independent rational power enclosures, exhaustive small profiles and semantic/domain controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 240, + "checks": "Repeat all mathematical and rejection checks with assertions disabled." + } + ] +} diff --git a/research/midpoint-rank-credit/verify.py b/research/midpoint-rank-credit/verify.py new file mode 100644 index 0000000000..01cf9e1e45 --- /dev/null +++ b/research/midpoint-rank-credit/verify.py @@ -0,0 +1,209 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Stronger sufficient power-moment credits. Produced by Nick Petalas.""" + +from fractions import Fraction as F +from hashlib import sha256 +from itertools import product +import json +from pathlib import Path + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def interval(lower, upper): + need(type(lower) is F and type(upper) is F, "rational endpoints") + need(0 < lower <= upper < 1, "saving interval inside (0,1)") + need(max(lower.denominator, upper.denominator) <= 10**6, "precision limit") + + +def curvature(k, lower, upper): + interval(lower, upper) + need(type(k) is int and 1 <= k <= 64, "rank limit") + if k == 1: + return 4 * lower / (3 + 2 * lower) + return lower * (1 - upper) / (k * (1 + upper * (k - 1))) + + +def credit(old, new, lower, upper): + interval(lower, upper) + need(type(old) is tuple and type(new) is tuple, "tuple profiles") + need(3 <= len(old) == len(new) <= 65, "profile dimension") + need(all(type(x) is int and 0 <= x <= 10**6 for x in old + new), + "bounded nonnegative counts") + need(old[0] == new[0] == 0, "rank zero excluded") + delta = tuple(n - o for o, n in zip(old, new)) + caps = tuple(sum(min(r, k) * d for r, d in enumerate(delta)) + for k in range(len(old))) + need(caps[-1] == 0, "equal rank mass required") + need(all(c <= 0 for c in caps), "capped-mass order required") + value = sum((-caps[k] * curvature(k, lower, upper) + for k in range(1, len(old) - 1)), F(0)) + return value, caps + + +def log_series(x): + """24 positive atanh terms and a geometric tail, for 1<=x<=2.""" + need(F(1) <= x <= F(2), "log reduction") + z = (x - 1) / (x + 1) + total = sum((2 * z ** (2 * j + 1) / (2 * j + 1) + for j in range(24)), F(0)) + tail = 2 * z**49 / (49 * (1 - z * z)) + return total, total + tail + + +def exp_negative(x): + """Enclose exp(-x) by a positive Taylor series for exp(x/8).""" + need(F(0) <= x <= F(5), "exp range") + y = x / 8 + term = total = F(1) + for j in range(1, 25): + term *= y / j + total += term + first_omitted = term * y / 25 + upper = total + first_omitted / (1 - y / 26) + return 1 / upper**8, 1 / total**8 + + +def power_bounds(rank, saving): + need(type(rank) is int and 1 <= rank <= 65, "oracle rank limit") + interval(saving, saving) + b = rank.bit_length() - 1 + l2, u2 = log_series(F(2)) + lt, ut = log_series(F(rank, 2**b)) + low_log, high_log = b * l2 + lt, b * u2 + ut + low, _ = exp_negative(saving * high_log) + _, high = exp_negative(saving * low_log) + return rank * low, rank * high + + +def lower_bill(profile, powers): + return sum((count * powers[r][0] for r, count in enumerate(profile) + if r), F(0)) + + +def upper_bill(profile, powers): + return sum((count * powers[r][1] for r, count in enumerate(profile) + if r), F(0)) + + +def check_curvatures(intervals): + checked = roots = 0 + for lower, upper in intervals: + for a in (lower, (lower + upper) / 2, upper): + powers = {0: (F(0), F(0))} + powers.update({r: power_bounds(r, a) for r in range(1, 34)}) + for k in range(1, 33): + theta_low = 2 * powers[k][0] - powers[k-1][1] - powers[k+1][1] + need(theta_low >= curvature(k, lower, upper), "curvature bound") + if k >= 2: + old = lower * (1 - upper) / ((k + 1) * (1 + upper * k)) + need(curvature(k, lower, upper) > old, "strict improvement") + checked += 1 + if a in (F(1, 2), F(1, 3), F(2, 3)): + p, q = a.numerator, a.denominator + for r in range(1, 34): + lo, hi = powers[r] + need(lo**q <= r**(q-p) <= hi**q, "independent root check") + roots += 1 + return checked, roots + + +def check_profiles(intervals): + profiles = tuple((0,) + x for x in product(range(3), repeat=4)) + comparisons = pairs = 0 + for lower, upper in intervals: + oracles = tuple({r: power_bounds(r, a) for r in range(1, 5)} + for a in (lower, (lower + upper) / 2, upper)) + for old in profiles: + for new in profiles: + if old == new: + continue + delta = tuple(n-o for o, n in zip(old, new)) + caps = tuple(sum(min(r, k)*d for r, d in enumerate(delta)) + for k in range(5)) + if caps[-1] or any(c > 0 for c in caps): + continue + value, _ = credit(old, new, lower, upper) + for powers in oracles: + need(lower_bill(old, powers) - upper_bill(new, powers) >= value, + "complete profile credit") + comparisons += 1 + pairs += 1 + return pairs, comparisons + + +def check_exchange(): + lower, upper = F(17, 10000), F(18, 10000) + value, caps = credit((0, 0, 2, 0), (0, 1, 0, 1), lower, upper) + need(caps == (0, 0, -1, 0), "exchange capped profile") + need(value == F(84847, 100180000), "exact new credit") + count = value.denominator // value.numerator + 1 + need(count == 1181 and (count - 1)*value <= 1 < count*value, + "least sufficient count for this bound") + old_value = lower*(1-upper)/(3*(1+2*upper)) + old_count = old_value.denominator // old_value.numerator + 1 + need(old_count == 1775 and count*old_value < 1, "strict certificate gain") + return {"credit": str(value), "exchanges": count, + "rank_two_children_required": 2*count, + "funded_rank_one_charge": 1, + "uniform_raw_slack_lower": str(count*value-1), + "preceding_bound_exchanges": old_count, + "fewer_exchanges": old_count-count} + + +def check_controls(): + lo, hi = F(17, 10000), F(18, 10000) + old, new = (0, 0, 2, 0), (0, 1, 0, 1) + fixtures = ( + (new, old, lo, hi), (old, (0, 1, 0, 0), lo, hi), + ((1, 0, 2, 0), new, lo, hi), ((0, -1, 2, 0), new, lo, hi), + ((0, True, 2, 0), new, lo, hi), (old, new, F(0), hi), + (old, new, hi, lo), (old, new, lo, F(1)), + (list(old), new, lo, hi), (old, new, F(1, 1000001), hi), + ((0,)*66, (0,)*66, lo, hi), ((0, 1000001, 0), (0, 1000001, 0), lo, hi), + ) + for args in fixtures: + rejected = False + try: + credit(*args) + except ValueError: + rejected = True + need(rejected, "invalid credit accepted") + powers = {r: power_bounds(r, F(1, 2)) for r in (1, 2, 3)} + theta_high = 2*powers[2][1] - powers[1][0] - powers[3][0] + need(theta_high < F(1, 4), "favorable-endpoint false bound not rejected") + need(credit(old, old, lo, hi)[0] == 0, "zero gain control") + need(power_bounds(1, lo) == (F(1), F(1)), "rank-one exactness") + return len(fixtures) + 3 + + +def main(): + intervals = ((F(17, 10000), F(18, 10000)), + (F(1, 8), F(1, 4)), (F(1, 3), F(2, 3))) + curvature_cases, root_cases = check_curvatures(intervals) + pairs, comparisons = check_profiles(intervals) + result = {"status": "PASS_MIDPOINT_RANK_CREDIT", + "claim_type": "scoped proof with exact finite corroboration", + "curvature_cases": curvature_cases, + "independent_root_cases": root_cases, + "profile_interval_pairs": pairs, + "profile_point_comparisons": comparisons, + "controls": check_controls(), "exchange": check_exchange()} + package = Path(__file__).resolve().parent + names = ("README.md", "TASK.json", "SOURCES.json", "VERIFY.json", "verify.py") + hashes = {} + for name in names: + with (package / name).open("rb") as handle: + raw = handle.read(131073) + need(len(raw) <= 131072, "package file limit") + hashes[name] = sha256(raw).hexdigest() + result["package_sha256"] = hashes + print(json.dumps(result, sort_keys=True, indent=2)) + + +if __name__ == "__main__": + main()