diff --git a/research/joint-cross-merge-threshold/README.md b/research/joint-cross-merge-threshold/README.md new file mode 100644 index 0000000000..7cd7809f08 --- /dev/null +++ b/research/joint-cross-merge-threshold/README.md @@ -0,0 +1,171 @@ +# Exactly 406 cross-side merges for the frozen joint invoice + +This contribution is produced by Nick Petalas. It is a scoped mathematical +proof with a finite exact accounting certificate, under Apache-2.0. + +For the complete frozen role ledger of Mark / Matarener's +[PR #5298](https://github.com/CrocSwap/integer-mult-bounds/pull/5298), the minimum +number of disjoint cross-side paid-job merges that passes the signed moment at +`C = 7/2000` is **406**. Each merge replaces one complex rank `a` and one BIT +rank `b` by the paid rank `a+b`. Every productive target and every unmerged paid +job stays in the bill. All roles are optimistically eligible. No job can be +used twice, and merged jobs cannot merge again. + +The constructive witness is 222 pairs of ranks `(72,63)`, two pairs `(72,56)`, +and 182 pairs `(64,56)`. Write `M = sum targets^(1-C) - sum paid^(1-C)`. +The exact verifier encloses the optimal margins in these rational intervals: + +```text +405 merges: -0.197285824316 <= M <= -0.197285824315 +406 merges: 0.088428560458 <= M <= 0.088428560459 +``` + +The general pairing theorem below makes 405 an exclusion for every allowed +matching, rather than a failed heuristic search. The application and exact threshold are the new result. +The predecessor's ledger and mathematical conclusions are cited premises and +are not re-audited here. This changes the `joint-query-controller` card to a +precise accounting question at the predecessor's explicit whole-job boundary. + +## Optimal pairing theorem + +Let `0 < alpha < 1` and let both sides be finite lists of positive ranks. +For exactly `k` disjoint cross-side merges, the smallest paid alpha-moment +comes from selecting the largest `k` ranks on each side and pairing them in +that same descending order. This holds for arbitrary positive real ranks. + +To prove it, define the saving from one merge by + +```text +Delta(a,b) = a^alpha + b^alpha - (a+b)^alpha. +``` + +It is positive by strict concavity. Its derivative in `a` is +`alpha [a^(alpha-1) - (a+b)^(alpha-1)] > 0`, and the derivative in `b` is +positive too. Thus replacing a selected rank by a larger unselected rank +cannot reduce the saving. Repeating the exchange selects the largest `k` +ranks on both sides, including ties in any order. + +The mixed derivative is +`Delta_ab = alpha(1-alpha)(a+b)^(alpha-2) > 0`. +For `a >= a'` and `b >= b'`, integrate this derivative over the rectangle to +obtain + +```text +Delta(a,b) + Delta(a',b') >= Delta(a,b') + Delta(a',b). +``` + +Exchanging inverted pairs therefore increases or preserves the total saving. +A finite sequence of exchanges produces the descending pairing. Since the +unmerged original bill is fixed, maximizing this saving minimizes the complete +paid moment. Further disjoint merges strictly improve the margin, so failure +at the optimal 405-pair matching excludes every matching with at most 405 +pairs. The explicit 406-pair witness proves sharpness. + +This is a specialization of the classical supermodular rearrangement argument. +The contribution claims the exact source-bound threshold and its application, +not discovery of rearrangement or of concave merge gains. + +## Exact arithmetic and evidence + +The stdlib-only verifier reads the full predecessor `RESULT.json` as a frozen +input, with SHA256 +`e712e5373ecbfea0c1b7c115b52eea4fb533c6c7c2ebae3aa98a2dd1f058721c`. +It computes the new complete moments from that ledger, without replaying the +predecessor's roots, six models, native words or other conclusions. + +The exponent is the exact rational `alpha=1993/2000`. Powers use rational +outward bounds, without floating point, Decimal, logarithm library calls or a +root grid. Write `r=2^s u` with `1<=u<2`. For `z=(u-1)/(u+1)`, sum the first +64 terms of `log u = 2 sum z^(2j+1)/(2j+1)` on a `2^-120` grid, rounding each +term outward. The remaining positive tail is bounded by +`2 z^129/[129(1-z^2)]`. Apply the same bound to `log 2`. + +For `x=C log r`, the verifier sums `exp(x)` through degree 24 and bounds its +tail by the degree-25 term times `26/25`, valid for `0<=x<=1`. Monotonicity and +reciprocal interval arithmetic then bound `r exp(-C log r)`. +All later additions, subtractions and comparisons use exact rational numbers. + +An independent certificate rounds every needed power interval outward to a +`2^-36` grid and checks the defining integer-power inequalities for all 145 +ranks from 1 through 145. If its endpoints are `l/2^36` and `u/2^36`, it checks +`l^2000 <= r^1993 * 2^72000 <= u^2000`. The coarser, integer-certified bounds +separately prove both moment signs. Thus the sharp 406 threshold has a finite +certificate that does not require trusting the logarithm/exponential enclosure +implementation. The general matching theorem remains a written proof. + +Finite corroboration enumerates all 1,200 choices of two three-job multisets +over ranks 1 through 4 and a merge count 1 through 3. All 13,200 labeled partial +matchings agree with the optimal pairing theorem. Seven invalid input controls +reject, and a strict crossed-pair example detects reversing the pairing rule. +The source hash, mass preservation, job-count reduction and explicit pair +multiplicities are executable invariants. Every run prints a generated receipt +binding the package files by SHA256. + +## Reproduce + +From the repository root, use CPython 3.12, standard library only: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/joint-cross-merge-threshold/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/joint-cross-merge-threshold/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/joint-cross-merge-threshold +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/joint-cross-merge-threshold --check-source-history +``` + +Use an available CPython 3.12 path on another machine. The expected marker is +`PASS_JOINT_CROSS_MERGE_THRESHOLD` with `minimum_merges: 406`. +Verification writes no files. See `VERIFY.json` for both registered commands. + +## Scope and limitations + +This is an exact threshold in an optimistic, finite accounting model of two +historical invoices. It supplies no physical merge, joint native word, compiler, +controller, dirty-state restoration, tape bill or new kappa. The target `7/2000` +is an explicit benchmark above the frozen side roots, not a selected admission +threshold. The current selected record remains unchanged. + +Additional fees can consume the positive margin. Restrictions on eligible roles +can raise the minimum. Repeated merges, splitting, altered targets, extra credits +or a different invoice are outside the theorem's threshold application. Native +and all-size multiplication obligations were not run. Independent human and +formal proof-kernel review are unclaimed. + +The runtime is managed Python. The verifier's largest supplied side has fewer +than 100,000 jobs and its exhaustive oracle has fixed finite loops. Dynamic +integer, rational and collection allocations are bounded by this fixture; +Python cannot enforce allocation-free execution. Memoization is limited to 512 +power bounds. Functions remain below 60 physical lines. These are the applicable +Power of Ten deviations, not changes to shared repository checks. The bounded +cache decorator and seven-entry control dispatch are standard-Python deviations +from the restrictions on metaprogramming and indirect calls. + +## Sources and credit + +The exact source is PR #5298 head +`e63b0a32ed2c021a8f4344e5aeb7e9123ff2eaef`, +`research/joint-supplier-average-ceiling/RESULT.json`. +`inputs/PR5298-RESULT.json` retains its bytes verbatim because this pending +source is not available from the package base history. The verifier authenticates +that retained file locally; no remote Git object or network access is required. +`SOURCES.json` binds the original card and selected record at the package base. +`TASK.json` records the external source URL, head and digest explicitly. + +Mark / Matarener supplied the joint invoice, whole-job boundary and merge +examples. James Reed / jwr404 identified the scope correction. zxv and the +retained #4470 lineage supplied the complex invoice; ai-nanachi and #4814 on +#4760 supplied the BIT invoice. Ali Romman's #5341 supplies separate crossing +results, which are not required or replayed here. The retained Zhihao Chen, +RaD/hipotures, icekylinx and eumemic controller and moment lineage keeps its +credit. This package adds the optimal disjoint-pair rule and exact 406 threshold. + +## Open next questions + +Can a native child legally realize any of the threshold witness's three rank +pairs while retaining both arbitrary payloads and their returned state? This +decides whether the relaxed accounting witness has a physical interpretation. +Start with one `(72,63)` pair and write its complete producer/consumer and fee +contract. No such joint native contract is supplied here. + +Can an explicit role-eligibility graph still admit 406 effective merges? First +derive its legal edges from one actual joint word, then solve the finite weighted +matching problem with all fees. The missing physical edge relation is the blocker. diff --git a/research/joint-cross-merge-threshold/SOURCES.json b/research/joint-cross-merge-threshold/SOURCES.json new file mode 100644 index 0000000000..d596e2e530 --- /dev/null +++ b/research/joint-cross-merge-threshold/SOURCES.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8", + "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + } + ] +} diff --git a/research/joint-cross-merge-threshold/TASK.json b/research/joint-cross-merge-threshold/TASK.json new file mode 100644 index 0000000000..771a871e5e --- /dev/null +++ b/research/joint-cross-merge-threshold/TASK.json @@ -0,0 +1,107 @@ +{ + "schema_version": 1, + "task_id": "joint-query-controller", + "priority_revision": 8, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "original_card": { + "id": "joint-query-controller", + "question": "Can a changed query demand or caller remove real work while satisfying native chronology and restoration?", + "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" + ], + "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": "A source-bound arbitrary-input identity and legal producer/consumer boundary with the complete paid and productive target invoice, including restoration, ownership, native alignment and extra charges. Price under the actual current model; historical ceiling.py assumptions must be established before use. A favorable optimistic relaxation keeps a route open but is not a completed supplier. A scoped local result remains useful; expansion requires the family-level budget gate.", + "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": "Choose an exact caller and a new demand/interface hypothesis. Read the scoped #5617/#5631/#5649/#5747 and #5720/#5745 objections before rebuilding an excluded schedule. Compare the complete matched source/consumer protocols including all retained helper outputs. For an active-mode injection, first check #5745: its canonical delivery claim repays the eight removed centre jobs. Audit that exact claim or change its channel/feedback hypothesis; do not repeat the same free-injection search. Stop if the full favorable budget fails or the required restored output is unobservable.", + "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": [ + "query demand", + "active mode", + "5720", + "5745", + "5747", + "caller" + ], + "existing_checks": [ + { + "scope": "PR #4166: author-checked installed producer/service/return/bridge connection; native-component comparison loses.", + "evidence": "research/qq16-caller-install/README.md", + "remaining": "Complete matched physical protocol bill, or changed source-compatible demand/circuit; no affordable supplier yet.", + "status": "author-checked", + "source_commit": "0b082d22a0e9a442d264ab0633e35ef26c790630", + "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 minimum number of disjoint cross-side paid-job merges at C=7/2000 in the exact PR5298 frozen joint invoice.", + "scope_change_reason": "The current card asks for a physically completed changed caller. This side result resolves a necessary finite accounting threshold at PR5298's explicit whole-job-premise boundary, without claiming a native realization.", + "bottleneck_link": "Quantifies the optimistic cross-side merge budget needed to escape the frozen whole-job bound; physical eligibility and all fees remain open.", + "budget_minutes": 60, + "stop_rule": "Stop at the first exact threshold certificate, or report a bounded failure. No larger saving or additional construction search.", + "outcome": "completed", + "evidence": "Optimal-pairing proof; exact rational signed-moment signs at 405 and 406, independently certified by 145 integer-power comparisons; exhaustive 13200 partial matchings; eight controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can a joint native child realize a witness rank pair?", + "why_it_matters": "The accounting relaxation has no physical construction.", + "first_step": "Specify one (72,63) pair with both arbitrary inputs and exact returned states, including all fees.", + "blocked_by": "No joint native producer/consumer contract." + }, + { + "question": "Can a physically derived eligibility graph support an effective 406-pair matching?", + "why_it_matters": "Restricted roles or extra fees may invalidate the relaxed witness.", + "first_step": "Derive legal cross-side edges from one actual joint word and solve its weighted matching.", + "blocked_by": "No physical edge relation or complete fee bill." + } + ], + "external_sources": [ + { + "pull_request": 5298, + "author": "Matarener", + "head": "e63b0a32ed2c021a8f4344e5aeb7e9123ff2eaef", + "original_path": "research/joint-supplier-average-ceiling/RESULT.json", + "url": "https://github.com/CrocSwap/integer-mult-bounds/blob/e63b0a32ed2c021a8f4344e5aeb7e9123ff2eaef/research/joint-supplier-average-ceiling/RESULT.json", + "retained_path": "research/joint-cross-merge-threshold/inputs/PR5298-RESULT.json", + "sha256": "e712e5373ecbfea0c1b7c115b52eea4fb533c6c7c2ebae3aa98a2dd1f058721c" + } + ], + "environment": { + "python_implementation": "CPython", + "python_version": "3.12.15", + "platform": "macOS-27.0.1-arm64-arm-64bit", + "dependencies": "Python standard library only" + } +} diff --git a/research/joint-cross-merge-threshold/VERIFY.json b/research/joint-cross-merge-threshold/VERIFY.json new file mode 100644 index 0000000000..ebd7a3e5bc --- /dev/null +++ b/research/joint-cross-merge-threshold/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 405/406 moment signs, optimal-pairing oracle, source bytes, mass/job invariants and rejection controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Identical full verification under optimized Python." + } + ] +} diff --git a/research/joint-cross-merge-threshold/inputs/PR5298-RESULT.json b/research/joint-cross-merge-threshold/inputs/PR5298-RESULT.json new file mode 100644 index 0000000000..9452ad12bb --- /dev/null +++ b/research/joint-cross-merge-threshold/inputs/PR5298-RESULT.json @@ -0,0 +1,207 @@ +{ + "schema_version": 1, + "status": "negative-result", + "summary": { + "claim": "On the p16 controller, under the whole-job premise (each side's paid jobs keep their individual ranks; no cross-job merge), any one-word-for-both-sides supplier whose joint ledger respects the rank-mass identity has saving at most the mass-weighted average of the #4470 complex root and the #4814 BIT root: C_joint <= 0.003232 (+7.0% over the selected 0.00302015), below the 0.003475458 BIT gate (+15.1%) that an ordinary complex-side improvement reaches. The mass identity alone does not cap the joint saving: merging paid jobs keeps mass and raises the root (models E/F, and the same merge inside the complex side alone), so whether the premise binds a joint native word is open. Idle ranks 8(j+1) and 7(j+1) never coincide; the literal 'identical (rank, role) paid once' rule drops 74,499 paid mass with unchanged targets and is not a ceiling; aligned-max twins have negative surplus. Each equation has one root in (0, 1/5] by the weighted-tail lemma of #5341 (minimum tails 32480 / 26160 / 32480).", + "selected_kappa_unchanged": "0.00302015", + "bit_admitted_unchanged": "0.003475458" + }, + "receipt": { + "baseline": { + "min_weighted_tail": { + "complex": 32480, + "bit": 26160, + "A_sum": 32480 + }, + "complex_root": "0.003020165977015620489716149158188481802050", + "bit_root": "0.003475458064076428997514139772259187321850", + "S_complex": 752, + "S_bit": 753, + "G_complex": "250637", + "G_bit": "218265", + "S_over_G_complex": "0.003000", + "S_over_G_bit": "0.003450" + }, + "models": { + "A_side_by_side": { + "C_joint": "0.003232027079", + "S": 1505, + "G": "468902", + "ratio_to_complex": "1.0701", + "ratio_to_bit": "0.9300", + "mass_identity": true, + "target_mass": 456672, + "paid_mass": 455167 + }, + "B_literal_paid_once": { + "C_joint": "0.182226946239", + "S": 76004, + "G": "592405", + "ratio_to_complex": "60.3367", + "ratio_to_bit": "52.4325", + "mass_identity": false, + "target_mass": 456672, + "paid_mass": 380668 + }, + "C_aligned_max": { + "C_joint": "0E-12", + "S": -5314, + "G": "244590", + "ratio_to_complex": "0.0000", + "ratio_to_bit": "0.0000", + "mass_identity": true, + "target_mass": 245772, + "paid_mass": 251086 + }, + "D_stacked_sum": { + "C_joint": "0.003198535119", + "S": 1505, + "G": "474776", + "ratio_to_complex": "1.0591", + "ratio_to_bit": "0.9203", + "mass_identity": true, + "target_mass": 456672, + "paid_mass": 455167 + }, + "E_paid_merged_targets_separate": { + "C_joint": "0.009324901846", + "S": 1505, + "G": "162702", + "ratio_to_complex": "3.0875", + "ratio_to_bit": "2.6831", + "mass_identity": true, + "target_mass": 456672, + "paid_mass": 455167 + }, + "F_paid_merged_reverse_pairing": { + "C_joint": "0.007541218084", + "S": 1505, + "G": "201811", + "ratio_to_complex": "2.4970", + "ratio_to_bit": "2.1698", + "mass_identity": true, + "target_mass": 456672, + "paid_mass": 455167 + } + }, + "conclusion": { + "best_mass_consistent_joint": "0.003232027", + "gain_over_selected": "0.0701", + "bit_gate_gain": "0.1508" + } + }, + "ledger": { + "identical_rank_role_paid_jobs": 35589, + "identical_rank_role_paid_mass": 74499, + "paid_mass": { + "complex": 239134, + "bit": 216033 + }, + "paid_by_role": { + "complex": { + "centre": { + "8": 144 + }, + "local": { + "1": 40266, + "2": 6984, + "3": 8892, + "4": 2646, + "5": 648 + }, + "shear": { + "1": 1680 + }, + "idle": { + "16": 448, + "24": 448, + "32": 448, + "40": 448, + "48": 448, + "56": 448, + "64": 448, + "72": 224 + } + }, + "bit": { + "centre": {}, + "local": { + "1": 23742, + "2": 24156, + "3": 1404, + "4": 702, + "5": 1836, + "6": 180, + "7": 324 + }, + "shear": { + "1": 1665 + }, + "idle": { + "14": 444, + "21": 444, + "28": 444, + "35": 444, + "42": 444, + "49": 444, + "56": 444, + "63": 222 + } + } + }, + "targets_by_role": { + "complex": { + "main": { + "145": 224 + }, + "idle": { + "17": 448, + "25": 448, + "33": 448, + "41": 448, + "49": 448, + "57": 448, + "65": 448, + "73": 224 + }, + "helper": { + "4": 504, + "7": 126, + "8": 846, + "9": 5868 + } + }, + "bit": { + "main": { + "127": 222 + }, + "idle": { + "15": 444, + "22": 444, + "29": 444, + "36": 444, + "43": 444, + "50": 444, + "57": 444, + "64": 222 + }, + "helper": { + "4": 72, + "8": 7776 + } + } + } + }, + "within_side_merge_control": { + "complex_local_jobs_paired": "0.004109298", + "ratio_to_complex": "1.3606" + }, + "rejected_controls": [ + "surplus identity", + "recorded BIT surplus", + "idle rank grid", + "decreasing equation", + "literal model as ceiling", + "source pin" + ] +} diff --git a/research/joint-cross-merge-threshold/verify.py b/research/joint-cross-merge-threshold/verify.py new file mode 100644 index 0000000000..b657b223b6 --- /dev/null +++ b/research/joint-cross-merge-threshold/verify.py @@ -0,0 +1,227 @@ +#!/usr/bin/env python3 +"""Exact disjoint cross-side merge threshold. Apache-2.0, Nick Petalas.""" + +from collections import Counter +from fractions import Fraction as F +from functools import lru_cache +import hashlib +from itertools import combinations, combinations_with_replacement, permutations +import json +from pathlib import Path + + +PACKAGE = Path(__file__).resolve().parent +SAVING = F(7, 2000) +SCALE = 1 << 120 +SOURCE_HASH = "e712e5373ecbfea0c1b7c115b52eea4fb533c6c7c2ebae3aa98a2dd1f058721c" + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def ceil_div(numerator, denominator): + return -(-numerator // denominator) + + +def log_unit_bounds(numerator, denominator): + """Bounds on log(numerator/denominator), with ratio in [1, 2].""" + require(denominator <= numerator <= 2 * denominator, "log ratio") + a, b = numerator - denominator, numerator + denominator + lower = upper = 0 + for j in range(64): + top = 2 * SCALE * a ** (2 * j + 1) + bottom = (2 * j + 1) * b ** (2 * j + 1) + lower += top // bottom + upper += ceil_div(top, bottom) + # The positive atanh tail is at most 2*z^129/(129*(1-z^2)). + tail_top = 2 * SCALE * a**129 * b**2 + tail_bottom = 129 * b**129 * (b**2 - a**2) + upper += ceil_div(tail_top, tail_bottom) + return F(lower, SCALE), F(upper, SCALE) + + +def exp_bounds(x): + """Positive Taylor series plus a geometric bound for its tail.""" + require(0 <= x <= 1, "exponential range") + term = total = F(1) + for j in range(1, 25): + term *= x / j + total += term + # All subsequent term ratios are at most 1/26. + tail = term * x / 25 * F(26, 25) + return total, total + tail + + +@lru_cache(maxsize=512) +def power_bounds(rank, saving=SAVING): + require(isinstance(rank, int) and 1 <= rank <= 1024, "rank range") + require(0 < saving <= F(1, 8), "saving range") + shift = rank.bit_length() - 1 + l2, u2 = log_unit_bounds(2, 1) + low, high = log_unit_bounds(rank, 1 << shift) + low += shift * l2 + high += shift * u2 + exp_low, _ = exp_bounds(saving * low) + _, exp_high = exp_bounds(saving * high) + return rank / exp_high, rank / exp_low + + +def moment_bounds(histogram, saving=SAVING): + low = high = F(0) + require(len(histogram) <= 1024, "histogram size") + for rank, count in histogram.items(): + require(isinstance(count, int) and count >= 0, "job count") + left, right = power_bounds(rank, saving) + low += count * left + high += count * right + return low, high + + +def load_ledger(raw=None): + if raw is None: + raw = (PACKAGE / "inputs/PR5298-RESULT.json").read_bytes() + require(hashlib.sha256(raw).hexdigest() == SOURCE_HASH, "source hash") + ledger = json.loads(raw)["ledger"] + paid, targets = {}, Counter() + for side in ("complex", "bit"): + jobs = Counter() + for role in ledger["paid_by_role"][side].values(): + jobs.update({int(r): n for r, n in role.items()}) + require(sum(jobs.values()) <= 100000, "side capacity") + require(all(1 <= r <= 1024 and n > 0 for r, n in jobs.items()), "jobs") + paid[side] = jobs + for role in ledger["targets_by_role"][side].values(): + targets.update({int(r): n for r, n in role.items()}) + return paid, targets + + +def descending_jobs(histogram): + return sorted(histogram.elements(), reverse=True) + + +def merge(paid, left, right, count): + require(0 <= count <= min(len(left), len(right)), "merge count") + result = paid.copy() + for j in range(count): + a, b = left[j], right[j] + result[a] -= 1 + result[b] -= 1 + result[a + b] += 1 + require(all(n >= 0 for n in result.values()), "disjointness") + return +result + + +def threshold_certificate(paid, targets): + left, right = (descending_jobs(paid[s]) for s in ("complex", "bit")) + original = paid["complex"] + paid["bit"] + t_low, t_high = moment_bounds(targets) + before = merge(original, left, right, 405) + after = merge(original, left, right, 406) + b_low, b_high = moment_bounds(before) + a_low, a_high = moment_bounds(after) + require(t_high < b_low, "405 must fail even under optimal pairing") + require(t_low > a_high, "406 must pass") + require(sum(r*n for r, n in before.items()) == sum(r*n for r, n in after.items()), + "merge must preserve paid rank mass") + require(sum(original.values()) - sum(after.values()) == 406, "job reduction") + pairs = Counter(zip(left[:406], right[:406])) + require(pairs == {(72, 63): 222, (72, 56): 2, (64, 56): 182}, "pair witness") + scale = 10**12 + margins = [[(t_low-p_high)*scale//1, ceil_div((t_high-p_low).numerator*scale, + (t_high-p_low).denominator)] for p_low, p_high in + ((b_low, b_high), (a_low, a_high))] + return {"minimum_merges": 406, "saving": str(SAVING), + "margin_scale": scale, "margin_integer_intervals": margins, + "pairs": [[a, b, n] for (a, b), n in sorted(pairs.items(), reverse=True)]} + + +def integer_power_certificate(paid, targets): + """Certify coarse power bounds independently, by integer exponentiation.""" + scale, bounds = 1 << 36, {} + for rank in range(1, 146): + low, high = power_bounds(rank) + lower = low * scale // 1 + upper = ceil_div(high.numerator * scale, high.denominator) + exact = rank**1993 * scale**2000 + require(lower**2000 <= exact <= upper**2000, "integer power certificate") + bounds[rank] = (F(lower, scale), F(upper, scale)) + original = paid["complex"] + paid["bit"] + left, right = (descending_jobs(paid[s]) for s in ("complex", "bit")) + target_low = sum(n * bounds[r][0] for r, n in targets.items()) + target_high = sum(n * bounds[r][1] for r, n in targets.items()) + before = merge(original, left, right, 405) + after = merge(original, left, right, 406) + require(target_high < sum(n * bounds[r][0] for r, n in before.items()), + "independent 405 exclusion") + require(target_low > sum(n * bounds[r][1] for r, n in after.items()), + "independent 406 witness") + return len(bounds) + + +def finite_matching_oracle(): + """Enumerate every partial matching of two labeled three-job lists.""" + cases = matchings = 0 + lists = tuple(combinations_with_replacement(range(1, 5), 3)) + for left in lists: + for right in lists: + original = Counter(left + right) + for count in range(1, 4): + optimum = merge(original, sorted(left, reverse=True), + sorted(right, reverse=True), count) + _, best_high = moment_bounds(optimum) + for a_ids in combinations(range(3), count): + for b_ids in permutations(range(3), count): + candidate = original.copy() + for i, j in zip(a_ids, b_ids): + a, b = left[i], right[j] + candidate[a] -= 1 + candidate[b] -= 1 + candidate[a+b] += 1 + candidate = +candidate + if candidate != optimum: + low, _ = moment_bounds(candidate) + require(best_high < low, "matching oracle") + matchings += 1 + cases += 1 + return cases, matchings + + +def controls(): + rejected = 0 + for function, arguments in ((power_bounds, (0,)), (power_bounds, (1025,)), + (power_bounds, (2, F(0))), (exp_bounds, (F(2),)), + (log_unit_bounds, (3, 1)), + (merge, (Counter({1: 2}), [1], [1], 2)), + (load_ledger, (b"{}",))): + try: + function(*arguments) + except ValueError: + rejected += 1 + else: + raise ValueError("invalid argument was accepted") + good = Counter({2: 1, 8: 1}) + crossed = Counter({5: 2}) + # Largest-with-largest gives merged ranks 8 and 2, versus 5 and 5. + _, high = moment_bounds(good) + low, _ = moment_bounds(crossed) + require(high < low, "reverse-pairing control") + return rejected + 1 + + +def main(): + paid, targets = load_ledger() + result = threshold_certificate(paid, targets) + cases, matchings = finite_matching_oracle() + result.update({"matching_cases": cases, "enumerated_matchings": matchings, + "integer_power_bounds": integer_power_certificate(paid, targets), + "controls": controls()}) + hashes = {str(p.relative_to(PACKAGE)): hashlib.sha256(p.read_bytes()).hexdigest() + for p in sorted(PACKAGE.rglob("*")) if p.is_file()} + print("PASS_JOINT_CROSS_MERGE_THRESHOLD " + json.dumps(result, sort_keys=True)) + print(json.dumps({"receipt_schema": 1, "package_sha256": hashes}, sort_keys=True)) + + +if __name__ == "__main__": + main()