From c12dddd5765150fe5c37a7e9e2a83d58f6c44ccd Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Fri, 23 Oct 2026 00:13:20 +0100 Subject: [PATCH] feat(research): prove sharp Hurwitz budget-success law --- research/hurwitz-budget-success/PROOF.md | 120 +++++++++++ research/hurwitz-budget-success/README.md | 103 ++++++++++ research/hurwitz-budget-success/RESULT.json | 36 ++++ research/hurwitz-budget-success/SOURCES.json | 30 +++ research/hurwitz-budget-success/TASK.json | 90 ++++++++ research/hurwitz-budget-success/VERIFY.json | 34 ++++ research/hurwitz-budget-success/verify.py | 203 +++++++++++++++++++ 7 files changed, 616 insertions(+) create mode 100644 research/hurwitz-budget-success/PROOF.md create mode 100644 research/hurwitz-budget-success/README.md create mode 100644 research/hurwitz-budget-success/RESULT.json create mode 100644 research/hurwitz-budget-success/SOURCES.json create mode 100644 research/hurwitz-budget-success/TASK.json create mode 100644 research/hurwitz-budget-success/VERIFY.json create mode 100644 research/hurwitz-budget-success/verify.py diff --git a/research/hurwitz-budget-success/PROOF.md b/research/hurwitz-budget-success/PROOF.md new file mode 100644 index 0000000000..f88c90a039 --- /dev/null +++ b/research/hurwitz-budget-success/PROOF.md @@ -0,0 +1,120 @@ +# Exact simultaneous-success tradeoff + +## Model and statement + +Retain Alexander Templeton's [PR785](https://github.com/CrocSwap/integer-mult-bounds/pull/785) +fixed-support message model, using Douglas R. Colkitt's +[PR703](https://github.com/CrocSwap/integer-mult-bounds/pull/703) Hurwitz geometry +and pairing tariff. Those results are cited premises, not replayed results here. +The new premise permits decoding errors and measures simultaneous success. + +There are five orthogonal mate pairs of Hurwitz lines. More generally, consider +an abstract matching with m pairs. Every port t holds an independent uniform +b-bit input X_t, with b a nonnegative integer. Each message j has fixed source +support A_j, fixed reader support R_j, fixed integer width q_j, and is an +arbitrary function of X restricted to A_j. A reader receives the whole message +when it belongs to R_j. Each receiver also knows its mate's input for free. +Every other observation must be included in the messages. There are finitely +many messages. There is no input-dependent support, timing or width metadata, +interactive relay, additional side information or correlated input. + +The inherited tariff c(R,A) is zero for an empty support or orthogonal singleton +mates, one for every other case having a singleton support, and two when both +supports have at least two elements. The charge is the fixed integer +C_actual = sum_j q_j c(R_j,A_j). This is an abstract additive pricing premise. +No physical nonlinear copy-cost theorem is inferred from it. + +**Theorem.** For any nonnegative integer budget C, the largest possible +probability that all 2m receivers are correct is exactly + + P_max(m,b,C) = 2^(-max(0, mb - floor(C/2))). (1) + +The physical Hurwitz application has m=5. The arbitrary-m assertion is about +the stated matching tariff, without asserting that the same geometry exists +for other m. Independent shared or private random coins do not improve (1) +when every fixed-coin realization retains the fixed-width charge budget. + +## Upper bound by successful fibers + +A transversal T selects one endpoint of each mate pair, so there are 2^m +transversals. Let J_T contain messages whose reader and source supports both +meet T, and put Q_T = sum_(j in J_T) q_j. + +Fix every input outside T. For a fixed displayed transcript of the messages +in J_T, there is at most one X_T assignment on which every receiver succeeds. +Indeed, messages received in T but absent from J_T depend only on the fixed +outside inputs. Every receiver's free mate input is also outside T. Thus each +receiver in T has identical observations on two assignments with the same +displayed transcript. Both assignments cannot be correct at every receiver in +T unless their complete X_T tuples agree. This is the successful-subset +version of Templeton's zero-error injection; correctness outside T need not be +used for this upper bound. + +There are at most 2^Q_T transcripts. The conditional probability of simultaneous +success, under the uniform mb-bit X_T, is at most min(1,2^(Q_T-mb)). Averaging +over outside inputs leaves the same bound for the unconditional probability p. + +Colkitt's transversal accounting gives, for every support pair, + + sum_T 1[R intersects T and A intersects T] <= 2^(m-1)c(R,A). + +For completeness, a zero-tariff pair never meets one transversal on both +sides; a tariff-one pair has a singleton support, present in exactly half +the transversals; a tariff-two pair meets at most all transversals. No +geometry enumeration is needed for this elementary application. + +Consequently sum_T Q_T <= 2^(m-1) C_actual <= 2^(m-1) C. Some transversal has +integer Q_T <= floor(C/2). Applying its successful-fiber bound and p<=1 proves +the upper half of (1). In particular the odd-budget plateau follows from an +integer transcript bound, rather than a continuous entropy relaxation. + +## Attaining construction + +There are mb pair-coordinate positions. Set k=min(mb,floor(C/2)) and choose +any k of them in advance. For each chosen coordinate of mate pair {u,v}, send +the one-bit parity X_u XOR X_v from support {u,v} to readers {u,v}. This costs +two units per coordinate and at most C in total. + +For a transmitted coordinate each receiver XORs the parity with its mate's +bit and is correct. For an untransmitted coordinate each receiver guesses +its own bit equals its mate's bit. The two receivers are simultaneously +correct exactly when that pair's bits agree. This has probability 1/2, and +these equality events are independent across the mb-k omitted coordinates. +All receivers therefore succeed with probability 2^(-(mb-k)), attaining (1). +Unused odd budget does not help. No clean helper or physical implementation +is being supplied by this abstract code. + +For random codes, fix all encoder and decoder coins independently of the +inputs. Each resulting deterministic code satisfies the same upper bound. +Averaging proves the random-code statement. The deterministic parity code +already attains it. + +## Consequence and limits + +Ten one-bit ports at budgets C=0,...,10 have exact optimum success probabilities + + 1/32, 1/32, 1/16, 1/16, 1/8, 1/8, 1/4, 1/4, 1/2, 1/2, 1. + +For any b>=1, saving even one unit below the zero-error floor 10b forces +simultaneous failure probability at least 1/2. Saving 2d units forces success +probability at most 2^-d. These statements concern simultaneous correctness; +individual receiver error rates have a different optimization problem. + +An expected-charge budget with variable execution lengths is outside (1). +For example, choose independently of inputs between full parity delivery +with probability r and the zero-message strategy otherwise. Its expected +charge is 10br and its success is r+(1-r)2^(-5b), which need not obey (1) +with C replaced by that expected charge. This example does not contradict +Jerry Chen's PR912 zero-error expected-cost theorem. No adaptive-routing, +variable-length or unrestricted private-header theorem is claimed here. + +The finite checks corroborate the proof by literal decoding and independent +decoder optimization; they do not prove its unbounded parameters. No native +supplier, Dfc admission, improved kappa or complete multiplication theorem +follows from the result. Source acquisition, encoding, decoding, physical +hosting, cleanup and tape costs remain outside this abstract charge model. + +This contribution was produced by Nick Petalas. The matching geometry, +tariff, transversal method and zero-error transcript argument retain the +predecessor credit above. No literature priority is claimed for the general +counting method. Apache-2.0. diff --git a/research/hurwitz-budget-success/README.md b/research/hurwitz-budget-success/README.md new file mode 100644 index 0000000000..3c2ff2eed6 --- /dev/null +++ b/research/hurwitz-budget-success/README.md @@ -0,0 +1,103 @@ +# Sharp Hurwitz budget versus simultaneous success + +This contribution was produced by Nick Petalas. Apache-2.0. + +**Scoped proof with exact finite corroboration.** For ten independent uniform +b-bit inputs in the fixed-support Hurwitz message model, the exact maximum +probability that every receiver decodes correctly at integer charge budget C is + + P_max = 2^(-max(0, 5b - floor(C/2))). + +Each receiver knows its orthogonal mate's input. Messages may be arbitrary +nonlinear functions of their fixed source inputs, but supports and widths are +fixed, and every bit pays its inherited reader/source pairing rank. The +[proof](PROOF.md) also establishes the abstract matching-tariff formula with +5 replaced by any positive pair count m. It covers independent random coins +when every fixed-coin realization respects the same fixed-width budget. + +At b=1, budgets 0 through 10 have exact optimum probabilities + + 1/32, 1/32, 1/16, 1/16, 1/8, 1/8, 1/4, 1/4, 1/2, 1/2, 1. + +Saving one unit below the zero-error floor already forces simultaneous failure +probability at least 1/2. A partial mate-parity code attains every step. This +is a sharp decoding-error extension, not a new supplier or kappa improvement. + +## Evidence and reproduction + +From the repository root, using CPython 3.12 and the standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/hurwitz-budget-success/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/hurwitz-budget-success/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/hurwitz-budget-success +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/hurwitz-budget-success --check-source-history +``` + +The marker is `PASS_HURWITZ_BUDGET_SUCCESS`. `RESULT.json` is a generated +receipt bound to the proof, verifier and metadata hashes. Direct replay checks +the entire receipt without modifying any file. `--write NEW_EXTERNAL_PATH` +generates a new receipt after all calculations; it never overwrites a receipt. + +The first fixture exhausts every one-bit Boolean full broadcast on two mate +pairs. It constructs the receiver-observation conflict graph, computes exact +maximum independent sets for all 65,536 induced graphs, and then constructs +and literally executes optimal receiver decoders for all 65,536 encoders on +all 16 inputs. This is independent optimization of success sets, not a replay +of the theorem's formula or a predecessor's numbers. + +The attaining-code census executes all input tuples for m=1,...,5 and b=0,...,3 +with 2mb<=12, at every integer budget 0,...,2mb+2. The code sends selected +pair-coordinate parities and decodes all receivers. Controls distinguish +upward rounding of odd budgets, independent guesses instead of mate guesses, +omitted parity, conflicting successful inputs and invalid parameters. A +correlated-input boundary example succeeds with zero charge and explains why +input independence matters. Counts and the complete encoder histogram are in +the generated receipt. The written proof supplies the all-width result. + +## Scope and predecessor credit + +Alexander Templeton's merged [PR785](https://github.com/CrocSwap/integer-mult-bounds/pull/785) +supplies the fixed-support nonlinear model and zero-error transcript argument. +Douglas R. Colkitt's [PR703](https://github.com/CrocSwap/integer-mult-bounds/pull/703) +supplies the Hurwitz matching geometry, tariff and transversal accounting, +following Joel Pulikkan's [PR620](https://github.com/CrocSwap/integer-mult-bounds/pull/620). +Jerry Chen's [PR912](https://github.com/CrocSwap/integer-mult-bounds/pull/912) +treats paid adaptive headers and expected zero-error charge. It is a separate +boundary, not an input to this proof. Historical proofs are pinned as +provenance in `SOURCES.json`; no predecessor verifier or geometry is replayed. +No priority is claimed for the general successful-subset counting method. + +Only the decoding-error premise changes. Uniform independent inputs, fixed +supports and widths, mate-only free side information, and additive per-bit +pricing remain essential. Expected-charge budgets, adaptive routing, +interactive relays, correlated inputs and additional side information are +outside scope. Physical encoding, decoding, cleanup, hosting and tape costs +remain unknown; no native operation is installed. There is no selected-frontier +change or complete multiplication theorem. Independent human and formal +proof-kernel review are unclaimed. + +This is a changed-scope side result under `complex-rank-shape-decoder`. +The card's 5% supplier ceiling acceptance gate is not claimed passed. The +family expansion decision is to finish this sharp obstruction and stop; +no dependent construction campaign or selected cold replay is justified. +The base is `624de9dc66858af0945e5f8a0942488d62280d43`, priority revision 7. + +## Open next questions + +The structured questions in `TASK.json` concern individual receiver errors +and unequal paired widths. For the first, start with exact achievable error +vectors on two one-bit mate pairs. For the second, start with widths +(1,2,1,1) on two pairs. The present joint-success theorem and uniform +transversal dimensions do not settle these questions. + +## Code verification limits + +The verifier uses structured, nonrecursive loops. Its exhaustive Boolean +tables have 65,536 entries; literal witness inputs have at most 12 bits. +Managed Python allocations are an explicit Power of Ten deviation: lists, +integers and temporary tuples allocate during the scan, with live memory +bounded by those fixed domains. No callback dispatch, subprocess, network, +external source import or generated code occurs. Every function is under +60 physical lines. Checks use explicit exceptions and remain active under +optimized Python. Warning-strict normal and optimized execution are registered. diff --git a/research/hurwitz-budget-success/RESULT.json b/research/hurwitz-budget-success/RESULT.json new file mode 100644 index 0000000000..b4e8b8fc1b --- /dev/null +++ b/research/hurwitz-budget-success/RESULT.json @@ -0,0 +1,36 @@ +{ + "boolean_broadcast_census": { + "boolean_encoders": 65536, + "induced_graphs": 65536, + "literal_input_tuples": 1048576, + "optimal_success_histogram": { + "4": 1810, + "5": 17632, + "6": 28256, + "7": 15136, + "8": 2702 + } + }, + "claim_type": "scoped proof", + "controls": { + "correlated_boundary": "1", + "odd_budget": "1/2", + "rejected_invalid_cases": 5, + "zero_budget_ten_ports": "1/32" + }, + "new_kappa": false, + "schema": "hurwitz-budget-success/1", + "source_sha256": { + "PROOF.md": "7c94c46e72ae69846fd45ce5972bfdd09a5c2dae233d04575d062c3ba4b15b1f", + "README.md": "9740baebf15b4609a6a92290719ab89b8b29ed45fb21df9c2bf362a5a618e8a3", + "SOURCES.json": "414a978d97fcb65b36dd251f6b3e35db08b1e2c383cbf3c7ee8689e648688cd1", + "TASK.json": "b790f9e7eff48bf38b7cf344a43ad376f2067710158e72bcfd5d49de1b8ade93", + "VERIFY.json": "e697bbb22797e4db7c59b908540dbdf5b7735ad179e026c6ae0c4be01abaa702", + "verify.py": "3ceefa0bbb56a840020dd62e717243c666913496f9777312881679cb560126b0" + }, + "witness_census": { + "cases": 117, + "input_tuples": 143235, + "rows_sha256": "d25f68b503faff1e566e708676174a910b25b1cca159439964e64814d7157bfa" + } +} diff --git a/research/hurwitz-budget-success/SOURCES.json b/research/hurwitz-budget-success/SOURCES.json new file mode 100644 index 0000000000..10b1547bf3 --- /dev/null +++ b/research/hurwitz-budget-success/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395", + "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/hurwitz-adaptive-routing/PROOF.md", + "usage": "provenance", + "git_blob": "915a91663e8ae2eb96a2c248224a40ec052e6fda", + "sha256": "612d1723fd855503384943217b78f18a80adaca074196aa677b7124845d9e4d1" + }, + { + "path": "research/hurwitz-nonlinear-copy-floor/PROOF.md", + "usage": "provenance", + "git_blob": "9811bf631707a087086f2efb1c2eb6db24eab20c", + "sha256": "62206654c5e6928324563bd5883db7186917a4546126ae64b72eee8914d9f573" + } + ] +} diff --git a/research/hurwitz-budget-success/TASK.json b/research/hurwitz-budget-success/TASK.json new file mode 100644 index 0000000000..e5327798a7 --- /dev/null +++ b/research/hurwitz-budget-success/TASK.json @@ -0,0 +1,90 @@ +{ + "schema_version": 1, + "task_id": "complex-rank-shape-decoder", + "priority_revision": 7, + "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43", + "original_card": { + "id": "complex-rank-shape-decoder", + "question": "Can a decoder deliver the local paid mass in fewer, larger-rank children (block frame climbs instead of rank-1 to rank-3 steps)?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/complex-local-word-ceiling/README.md", + "research/complex-decoder-field-extension-seed44/README.md", + "research/complex-frame-pair-decoders/README.md", + "research/selected-k8-unrestricted-ends/README.md", + "research/eisenstein-reduction-copy-floor/README.md" + ], + "methods": [ + "Find one exact small decoding identity whose frame path climbs in blocks, and price its complete per-call profile.", + "Bound the best effective child rank achievable for one fixed support alphabet, including copies, frames and restoration." + ], + "acceptance_gate": "A per-call local profile, with all copied information, frames and restoration counted, whose ceiling exceeds the selected word's by at least 5%; masked or overcomplete supports must change an assumption of the eight-term all-pairs bound. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "research/complex-local-word-ceiling/verify.py" + ], + "expected": "PASS_COMPLEX_LOCAL_WORD_CEILING", + "inspect": "Read the selected word's per-call local profile, its packing ceiling and the lever table; run levers.py for the ideal budget of the lever you target.", + "scope": "Positive control and planning budget only; this is not a new construction or full cold replay." + }, + "first_experiment": "Before any synthesis, write the candidate per-call local profile (and centre charge / unpaid coordinates if changed) and screen it with ceiling.ceiling(); reject it if even the ideal ceiling does not beat the selected word's by your stated margin. Ideal budget: rank-16 delivery is 2.31x (levers.py).", + "bottleneck_link": "Rank-1 children are about half of recursive cost; the selected word's effective child rank is about 3.9. Larger-rank delivery lowers recursive cost per unit of paid mass.", + "allowed_variations": [ + "One masked, overcomplete or block decoder family with exact labels and supports.", + "A scoped lower bound on effective rank for one alphabet.", + "If the coverage law, template or guard changes, derive an applicable fully charged replacement bound instead of applying the incumbent ceiling outside its scope." + ], + "scope_change_triggers": [ + "Repacking idle remainders of an unchanged word (covered by the packing ceiling).", + "Repeating the eight-term all-pairs search inside its proved scope.", + "Only changing helper terminal subspaces and monotone frames within the fixed scalar word, entrances and cleanup contract already covered by #1995/#2013.", + "Searching below C=40 in the #2017 Eisenstein binary scalar-rectangle or fixed-support block-linear additive pairing model; specify a changed premise instead. This bound does not cover every complex decoder.", + "Continuing a partial cost improvement while leaving the same unpriced consumer, restoration or central-readout obligation unresolved; refresh the family expansion decision first. Local product-retiming evidence has a narrow scope and is not a ban on changed graphs or contracts." + ], + "overlap_terms": [ + "rank shape", + "block climb", + "masked decoder", + "overcomplete", + "effective rank" + ] + }, + "scope_status": "changed", + "actual_scope": "Exact maximum simultaneous decoding success under a fixed integer charge budget in the Hurwitz matching message model.", + "scope_change_reason": "Take the decoding-error exclusion in Alexander Templeton PR785 as the changed premise. This is a scoped interface side result, not a block-rank supplier or a claim to pass the card's 5% ceiling gate.", + "bottleneck_link": "Quantifies whether bounded-error nonlinear messaging can evade the inherited zero-error copy floor: saving even one unit below 10b forces at least one-half simultaneous failure.", + "budget_minutes": 60, + "stop_rule": "Stop and package the first sharp all-width success tradeoff and matching code; no downstream construction campaign.", + "outcome": "completed", + "evidence": "Written all-width proof; 117 attaining-code cases over 143235 literal input tuples; 65536 Boolean broadcasts with exact decoder optimization and 1048576 literal input tuples; five invalid-case rejections and explicit model-boundary controls. No predecessor verifier is run.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "What is the exact tradeoff for individual receiver error probabilities under this same tariff?", + "why_it_matters": "The present sharp bound concerns simultaneous correctness and does not optimize marginal errors.", + "first_step": "Enumerate two mate pairs with one broadcast bit and keep the complete achievable four-receiver error vectors.", + "blocked_by": "A joint-success maximum does not determine the Pareto frontier of receiver errors." + }, + { + "question": "What is the sharp simultaneous-success tradeoff with unequal widths on paired ports?", + "why_it_matters": "The uniform-width equality construction uses symmetric mate coordinates.", + "first_step": "Solve two mate pairs with widths (1,2,1,1), explicitly accounting for side-information alphabets.", + "blocked_by": "Transversal input dimensions now differ, so the uniform averaging bound need not be sharp." + } + ], + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19134291", + "proof_status": "Written scoped proof with exact finite corroboration; no complete multiplication theorem.", + "overlap_check": { + "canonical_main": "624de9dc66858af0945e5f8a0942488d62280d43", + "checked_at": "2026-10-22T23:11:44Z", + "open_prs": 416, + "discussion_records": 3927, + "remote_pagination_complete": true, + "local_notes_searched": 123, + "local_head_note_paths": 6319, + "local_coverage": "Sparse and incomplete. Supplemented with git grep over canonical main and merged PR searches for the object, formula and success-probability terms. No claim of exhaustive novelty." + } +} diff --git a/research/hurwitz-budget-success/VERIFY.json b/research/hurwitz-budget-success/VERIFY.json new file mode 100644 index 0000000000..a4bb95662a --- /dev/null +++ b/research/hurwitz-budget-success/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": "Literal attaining codes, independent optimal-decoder Boolean census, model-boundary and rejection controls, hash-bound generated receipt." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The same complete replay with Python assertions disabled." + } + ] +} diff --git a/research/hurwitz-budget-success/verify.py b/research/hurwitz-budget-success/verify.py new file mode 100644 index 0000000000..e89be233cc --- /dev/null +++ b/research/hurwitz-budget-success/verify.py @@ -0,0 +1,203 @@ +#!/usr/bin/env python3 +"""Exact finite corroboration of the Hurwitz budget/success theorem.""" + +import argparse +from collections import Counter +from fractions import Fraction +import hashlib +import json +from pathlib import Path + + +PACKAGE = Path(__file__).resolve().parent +BOUND_FILES = ( + "README.md", "PROOF.md", "verify.py", "TASK.json", "SOURCES.json", "VERIFY.json", +) + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def maximum_success(pairs, width, budget): + require(type(pairs) is int and pairs >= 1, "positive pair count required") + require(type(width) is int and width >= 0, "nonnegative width required") + require(type(budget) is int and budget >= 0, "nonnegative budget required") + missing = max(0, pairs * width - budget // 2) + return Fraction(1, 1 << missing) + + +def decode_partial_parities(inputs, width, kept): + pairs = len(inputs) // 2 + require(len(inputs) == 2 * pairs and pairs >= 1, "paired inputs required") + require(0 <= kept <= pairs * width, "invalid transmitted coordinate count") + payload = [] + for coordinate in range(kept): + pair, bit = divmod(coordinate, width) + payload.append(((inputs[2 * pair] ^ inputs[2 * pair + 1]) >> bit) & 1) + outputs = [] + for port in range(2 * pairs): + value = inputs[port ^ 1] + for bit in range(width): + coordinate = (port // 2) * width + bit + if coordinate < kept: + value ^= payload[coordinate] << bit + outputs.append(value) + return tuple(outputs) + + +def witness_census(): + cases = inputs_checked = 0 + rows = [] + for pairs in range(1, 6): + for width in range(4): + bits = 2 * pairs * width + if bits > 12: + continue + for budget in range(2 * pairs * width + 3): + kept = min(pairs * width, budget // 2) + successes = 0 + for word in range(1 << bits): + inputs = tuple((word >> (port * width)) & ((1 << width) - 1) + for port in range(2 * pairs)) + successes += decode_partial_parities(inputs, width, kept) == inputs + require(Fraction(successes, 1 << bits) == + maximum_success(pairs, width, budget), "attaining code failed") + require(2 * kept <= budget, "attaining code exceeds budget") + rows.append([pairs, width, budget, successes, 1 << bits]) + inputs_checked += 1 << bits + cases += 1 + return {"cases": cases, "input_tuples": inputs_checked, + "rows_sha256": hashlib.sha256(json.dumps(rows).encode()).hexdigest()} + + +def conflict_graph(): + """An edge forbids two inputs succeeding with the same broadcast bit.""" + adjacency = [] + for left in range(16): + neighbors = 0 + for right in range(16): + conflict = any(((left >> (port ^ 1)) & 1) == + ((right >> (port ^ 1)) & 1) and + ((left >> port) & 1) != ((right >> port) & 1) + for port in range(4)) + neighbors |= int(conflict) << right + adjacency.append(neighbors) + return adjacency + + +def optimal_success_sets(adjacency): + """Exhaust every induced graph by a nonrecursive independent-set DP.""" + sizes = [0] * (1 << 16) + sets = [0] * (1 << 16) + for mask in range(1, 1 << 16): + vertex_bit = mask & -mask + vertex = vertex_bit.bit_length() - 1 + rest = mask ^ vertex_bit + allowed = rest & ~adjacency[vertex] + if sizes[rest] >= 1 + sizes[allowed]: + sizes[mask], sets[mask] = sizes[rest], sets[rest] + else: + sizes[mask], sets[mask] = 1 + sizes[allowed], vertex_bit | sets[allowed] + return sizes, sets + + +def decoder_for_sets(zero_set, one_set): + lookup = [[-1] * 4 for _ in range(4)] + for broadcast, success_set in enumerate((zero_set, one_set)): + for word in range(16): + if not (success_set >> word) & 1: + continue + for port in range(4): + observation = 2 * broadcast + ((word >> (port ^ 1)) & 1) + bit = (word >> port) & 1 + old = lookup[port][observation] + require(old in (-1, bit), "successful inputs have conflicting decodes") + lookup[port][observation] = bit + return [[max(0, bit) for bit in row] for row in lookup] + + +def boolean_broadcast_census(): + adjacency = conflict_graph() + sizes, sets = optimal_success_sets(adjacency) + all_inputs = (1 << 16) - 1 + require(sizes[all_inputs] == 4, "zero-message optimal success count changed") + histogram = Counter() + for truth_table in range(1 << 16): + zero_inputs = all_inputs ^ truth_table + predicted = sizes[zero_inputs] + sizes[truth_table] + lookup = decoder_for_sets(sets[zero_inputs], sets[truth_table]) + actual = 0 + for word in range(16): + broadcast = (truth_table >> word) & 1 + actual += all(lookup[port][2 * broadcast + ((word >> (port ^ 1)) & 1)] + == ((word >> port) & 1) for port in range(4)) + require(actual == predicted, "independent decoder optimum not attained") + require(Fraction(actual, 16) <= maximum_success(2, 1, 2), + "one-bit broadcast exceeds theorem") + histogram[actual] += 1 + require(sum(histogram.values()) == 65536, "incomplete encoder census") + require(max(histogram) == 8, "sharp broadcast success count changed") + return {"boolean_encoders": 65536, "literal_input_tuples": 65536 * 16, + "induced_graphs": 65536, + "optimal_success_histogram": {str(k): v for k, v in sorted(histogram.items())}} + + +def rejection_controls(): + rejected = 0 + for arguments in ((0, 1, 1), (1, -1, 1), (1, 1, -1), (True, 1, 1)): + try: + maximum_success(*arguments) + except ValueError: + rejected += 1 + else: + raise ValueError("invalid theorem parameters accepted") + require(maximum_success(5, 1, 9) == Fraction(1, 2), "odd budget rounded upward") + require(maximum_success(5, 1, 0) == Fraction(1, 32), "mate guesses treated as independent") + require(decode_partial_parities((0, 1), 1, 0) != (0, 1), "missing bit undetected") + require(decode_partial_parities((0, 1), 1, 1) == (0, 1), "positive code rejected") + try: + decoder_for_sets((1 << 0) | (1 << 1), 0) + except ValueError: + rejected += 1 + else: + raise ValueError("conflicting successful inputs accepted") + require(all(decode_partial_parities((x, x), 1, 0) == (x, x) for x in range(2)), + "correlated-input boundary example failed") + require(Fraction(1, 1) > maximum_success(1, 1, 0), "boundary example is vacuous") + return {"rejected_invalid_cases": rejected, "odd_budget": "1/2", + "zero_budget_ten_ports": "1/32", "correlated_boundary": "1"} + + +def result(): + hashes = {} + for name in BOUND_FILES: + payload = (PACKAGE / name).read_bytes() + require(len(payload) <= 1024 * 1024, "package input exceeds byte limit") + hashes[name] = hashlib.sha256(payload).hexdigest() + return {"schema": "hurwitz-budget-success/1", "claim_type": "scoped proof", + "source_sha256": hashes, "witness_census": witness_census(), + "boolean_broadcast_census": boolean_broadcast_census(), + "controls": rejection_controls(), "new_kappa": False} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--write", type=Path, help="write generated receipt to a new external file") + args = parser.parse_args() + if args.write: + require(not args.write.resolve().is_relative_to(PACKAGE), + "generated replay output must be outside the package") + actual = result() + if args.write: + with args.write.open("x", encoding="utf-8") as output: + output.write(json.dumps(actual, indent=2, sort_keys=True) + "\n") + else: + expected = json.loads((PACKAGE / "RESULT.json").read_text(encoding="utf-8")) + require(actual == expected, "receipt mismatch") + print("PASS_HURWITZ_BUDGET_SUCCESS " + json.dumps(actual, sort_keys=True)) + + +if __name__ == "__main__": + main()