From 64a58e7bce47a1745aa74918485afd657bc5f871 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Thu, 29 Oct 2026 16:24:03 +0000 Subject: [PATCH] feat(research): prove sharp sum-parity recovery threshold --- research/sum-parity-recovery/PROOF.md | 110 +++++++++++++ research/sum-parity-recovery/README.md | 95 +++++++++++ research/sum-parity-recovery/SOURCES.json | 30 ++++ research/sum-parity-recovery/TASK.json | 120 ++++++++++++++ research/sum-parity-recovery/VERIFY.json | 34 ++++ research/sum-parity-recovery/recovery.py | 90 ++++++++++ research/sum-parity-recovery/verify.py | 192 ++++++++++++++++++++++ 7 files changed, 671 insertions(+) create mode 100644 research/sum-parity-recovery/PROOF.md create mode 100644 research/sum-parity-recovery/README.md create mode 100644 research/sum-parity-recovery/SOURCES.json create mode 100644 research/sum-parity-recovery/TASK.json create mode 100644 research/sum-parity-recovery/VERIFY.json create mode 100644 research/sum-parity-recovery/recovery.py create mode 100644 research/sum-parity-recovery/verify.py diff --git a/research/sum-parity-recovery/PROOF.md b/research/sum-parity-recovery/PROOF.md new file mode 100644 index 0000000000..28bf06c6fc --- /dev/null +++ b/research/sum-parity-recovery/PROOF.md @@ -0,0 +1,110 @@ +# Exact sum and fixed parity checks under uniform coefficient error + +This contribution was produced by Nick Petalas. Apache-2.0. + +## Contract and result + +Fix N >= 2, a binary m by N matrix H, and a real R >= 0. The unknown +coefficient vector is c in Z^N. A decoder receives a real vector y with +|y_i-c_i| <= R, the exact integer S=sum_i c_i, and H(c mod 2). +It must recover c for every such input. The rows of H are fixed before c +and y are known. The decoder itself can be nonlinear and computationally +unbounded. Giving it S for free strengthens the interface being tested. + +The exact classification is: + +1. For 0 <= R < 1/2, recovery needs no parity checks. +2. For 1/2 <= R < 1, recovery is possible if and only if the binary matrix + obtained by appending the all-ones row to H has column rank N. + Consequently the minimum is exactly N-1 parity checks. +3. For R >= 1, recovery is impossible for every H, including the matrix + revealing all N coordinate parities. + +The endpoints concern a closed error promise. At R=1/2 the first obstruction +already applies, and at R=1 the second applies. When N=1 the exact sum is +the unknown coefficient, so the classification is intentionally restricted +to N >= 2. + +## Below half a unit + +Distinct integer vectors have coordinate distance at least one. Their closed +radius-R boxes are disjoint when 2R<1. Rounding each y_i to its nearest +integer therefore recovers c, without using S or H. + +## Necessity in the middle interval + +Suppose the augmented matrix has rank less than N. It has a nonzero binary +kernel vector v. The all-ones row implies that v has even weight 2k, with +k>=1. Partition its support into disjoint sets A and B of size k. +Let c and d be the zero/one indicator vectors of A and B, respectively. + +Then c and d are distinct, have the same exact sum k, and have the same +syndrome because c-d reduces to v modulo two. For y=(c+d)/2, both errors +are at most 1/2. Thus the same complete observation admits two answers for +every R>=1/2. The ambiguity uses nonnegative coefficients and a known sum; +it does not depend on cancellation between large signed inputs. + +No choice of decoding algorithm can distinguish that pair. This is a +worst-case information obstruction, rather than failure of the implemented +decoder or a numerical search. + +## Sufficiency in the middle interval + +Suppose the augmented matrix has rank N. The supplied syndrome, together +with S mod 2, determines the full coordinate parity vector r=c mod 2 by +binary linear algebra. For a fixed parity r_i, consecutive possible integers +are two apart. Since R<1, at most one of them is within R of y_i. +The promise supplies existence. Recover every coordinate this way. + +Equivalently, if c and d were two candidates, their difference would be +even in each coordinate and have absolute value at most 2R<2. It must be +zero. This argument covers arbitrary real observations and all integer +magnitudes, not merely the rational bounded domain of the implementation. + +The augmented matrix has at most m+1 independent rows, so m>=N-1. +Taking the first N-1 coordinate parities attains equality: the last parity +is S minus their sum, modulo two. Dense linear checks cannot use fewer +bits than these coordinate checks in this fixed-sketch model. + +## The unit-radius obstruction + +Take c=(0,2,0,...,0), d=(2,0,0,...,0), and y=(1,1,0,...,0). +Both coefficients have sum two, every coordinate parity agrees, and the +maximum error is exactly one. Every binary-linear syndrome therefore +agrees as well. Recovery fails for every R>=1. + +## Consequence for a precision-saving proposal + +The selected construction retains an analytic integer-recovery obligation. +Its selected review and zxv's PR6062 discuss strict half-unit recovery. +The proposed changed contract here grants an exact sum and seeks to relax +the uniform absolute-error tolerance using a small fixed parity sketch. +The theorem rules out a sublinear number of checks for that unrestricted +coefficient interface as soon as the allowed error reaches 1/2. It does +not bound the cost of computing N-1 checks or prove that they are affordable. +The result fixes the target for such a proposal before implementation work. + +This is not a lower bound for integer multiplication. Actual convolution +coefficients can satisfy additional restrictions, and a caller may provide +other information. Sparse or probabilistic errors, adaptive checks, nonlinear +checks, odd moduli, relative-error contracts, and stronger exact measurements +are different interfaces. None is excluded. No selected assumption is +discharged and no new kappa is claimed. + +## Evidence and background + +The proof uses standard binary linear algebra and lattice separation. Those +methods and coding-theoretic ideas are not claimed as new. The contribution +is this sharp changed recovery contract and its explicit coefficient +ambiguities, with an attaining decoder, in the present research programme. +The selected source and PR6062 supply context rather than mathematical +premises. PR6182 studies a deterministic rounded native inverse and selected +coordinate tags; its rounded map and collision families are not used here. + +The checker enumerates every binary row space through N=6 and independently +tests equal-weight zero/one coefficient pairs. Unique reduced row forms and +the Gaussian-binomial count establish the finite inventory. A separate +bounded decoder uses elimination. Closed-boundary fixtures, omitted-check +ambiguities, unit-radius ambiguities and invalid inputs are tested under +ordinary and optimized Python. These finite checks corroborate the written +all-input proof; they do not establish its infinite quantifiers. diff --git a/research/sum-parity-recovery/README.md b/research/sum-parity-recovery/README.md new file mode 100644 index 0000000000..d886053cdf --- /dev/null +++ b/research/sum-parity-recovery/README.md @@ -0,0 +1,95 @@ +# A sharp parity-check barrier to relaxing integer recovery precision + +This contribution was produced by Nick Petalas. Apache-2.0. + +For N>=2 arbitrary integer coefficients, grant their exact sum and approximate +values with uniform absolute error at most R. A fixed binary-linear sketch +permits exact recovery for every input precisely as follows: + +| Closed error radius | Necessary and sufficient condition | +| --- | --- | +| 0 <= R < 1/2 | No sketch needed | +| 1/2 <= R < 1 | Append the all-ones row to the sketch matrix: binary rank must be N | +| R >= 1 | Impossible even with every coordinate parity | + +The middle regime needs exactly **N-1 parity checks**, attained by revealing +the first N-1 coordinate parities. Dense fixed checks cannot improve that +count. Every sketch excluded in the middle regime has an explicit pair of nonnegative zero/one +coefficient vectors with the same sum and sketch, both within 1/2 of the +same observation. [PROOF.md](PROOF.md) proves the all-input classification. + +This is a **scoped obstruction and construction proof with finite exact +corroboration**, not a search failure or a complete multiplication theorem. +It rejects a sublinear fixed-parity replacement for the strict half-unit +error requirement in the unrestricted coefficient interface. It gives no new kappa, +supplier admission or lower bound for actual convolution coefficient sets. + +## Reproduction + +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/sum-parity-recovery/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/sum-parity-recovery/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/sum-parity-recovery +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/sum-parity-recovery --check-source-history +``` + +Any CPython 3.12 executable can replace the local path. The verifier writes +nothing. It prints a generated JSON receipt bound to every package file, +then `PASS_SUM_PARITY_RECOVERY`. The registered replay runs both modes. +The finite oracle enumerates all binary sketch row spaces for N=2..6 and +tests their actual equal-weight binary coefficient observations. It also +checks the constructive decoder, closed endpoints and rejected contracts. + +On CPython 3.12.15, normal and optimized direct runs passed in about 0.25 +seconds each; the complete registered replay passed in 0.75 seconds. These +are replay-budget observations. The exact finite result is 3,287 row spaces, +67 admitting sketches, 3,220 explicit ambiguities, 5,704 boundary decodes, +1,089 sub-half-unit decodes, 66 omitted-check controls, 63 unit-radius +ambiguities, 20 invalid-contract rejections and one 4,001-bit integer fixture. + +## Scope, sources and credit + +The new question changes `uniform-transfer-audit` to an analytic-recovery +contract obstruction; it does not audit or discharge a selected assumption. +Base is canonical main `a5bff3bf133e482541c09eba4e773884bdb2b1b7`, priority +revision 8. The selected conditional kappa is .003125804. + +The selected review and zxv's [PR6062](https://github.com/CrocSwap/integer-mult-bounds/pull/6062) +supply recovery context. The original fixed-syndrome question is not taken +from that package. Standard binary linear algebra, coding and integer-lattice +separation retain their background credit; no literature-priority claim is +made. No predecessor numerical result, matrix or scientific checker is used. +The P104/native/helper/compiler/outer lineage retains its original credit. +[PR6182](https://github.com/CrocSwap/integer-mult-bounds/pull/6182) has a different +deterministic rounded inverse and coordinate-tag model, absent here. + +The mathematical result permits all N and all integer magnitudes. The exact +decoder executable accepts N=2..64, at most 64 sketch rows, and at most 4096 +bits in each input integer or rational numerator/denominator. Python requires +dynamic allocation; these bounds constrain its live arithmetic and equation +storage. Exhaustive checks stop at N=6. No recursive code, external dependency +or generated code is used. Test rejection callbacks have fixed local targets. + +The exact sum and sketch acquisition, restoration, tape movement and complete +physical bill are unpriced. Sparse/probabilistic errors, adaptive or nonlinear +checks, odd moduli, and additional coefficient restrictions are not covered. +No selected cold replay, numerical supplier, formal kernel or full outer +proof ran. Independent human and formal proof-kernel review are unclaimed. +The two Python files pass warning-strict execution, syntax/AST checks and +the 60-line function ceiling. There is no project Python linter configuration +in this checkout; no separate linter or static type-checker pass is claimed. + +## Open next questions + +- Can one actual convolution caller restrict the possible coefficient-error + supports enough to use fewer exact checks? First prove a support restriction + from its completed numerical error, then price acquisition and decoding. + A uniform norm bound alone supplies no such restriction. +- Can a fully charged odd-modulus recovery interface improve the precision + budget? First specify its exact coefficient domain, modulus acquisition, + returned error and storage. This binary theorem gives no odd-modulus bound. + +The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19272169) +records the predicted scope. Only this package is changed. diff --git a/research/sum-parity-recovery/SOURCES.json b/research/sum-parity-recovery/SOURCES.json new file mode 100644 index 0000000000..e696a0d4e9 --- /dev/null +++ b/research/sum-parity-recovery/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "a5bff3bf133e482541c09eba4e773884bdb2b1b7", + "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": "docs/research/pr-intake-evidence/pr6030-audit/PROOF-REVIEW.md", + "usage": "provenance", + "git_blob": "26f2f6324bce57e69e861d2aae5a27c9de325a8e", + "sha256": "8bd158b8ef68202000f167b9b78db0b31531b5b067b5cbd91b5bf35f3ddd1ab6" + }, + { + "path": "research/outer-representation-budget/PROOF.md", + "usage": "provenance", + "git_blob": "d1856c6d4b20753b62da3716ac3da3fbe04ddfb7", + "sha256": "2585aed04130b2c202a50a6f70b68fbfcea8506b4ae56ad53430627ad6a84c1f" + } + ] +} diff --git a/research/sum-parity-recovery/TASK.json b/research/sum-parity-recovery/TASK.json new file mode 100644 index 0000000000..bf68636b33 --- /dev/null +++ b/research/sum-parity-recovery/TASK.json @@ -0,0 +1,120 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 8, + "base_commit": "a5bff3bf133e482541c09eba4e773884bdb2b1b7", + "original_card": { + "id": "uniform-transfer-audit", + "question": "Can one of the selected record's five inherited assumptions be proved at its actual caller?", + "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": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.", + "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 one assumption ID (native_all_columns, owned_erasure, compiler, precision_tape, analytic_recovery), one quantified implication and exact dependency closure. Check current handoffs, including #5625 row reentry and #5707 root-prefix lowering, without treating their partial scope as the whole theorem. Prove or falsify that implication with a caller-bound argument; stop at the chosen obligation. Finite tests or root digits do not discharge an all-size statement.", + "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": [ + "native_all_columns", + "owned_erasure", + "compiler", + "precision_tape", + "analytic_recovery" + ], + "existing_checks": [ + { + "scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "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": "Classify exact recovery of arbitrary integer coefficients from a uniform closed error box, their exact sum, and fixed binary-linear checks; construct an attaining decoder and explicit ambiguities.", + "scope_change_reason": "The user requires original work, not an audit. This tests an original changed analytic_recovery interface rather than discharging a retained assumption or extending a predecessor rounded map.", + "bottleneck_link": "Tests whether a sublinear fixed parity sketch could relax the uniform half-unit coefficient precision requirement. A sharp negative result stops that unrestricted recovery route before physical implementation.", + "budget_minutes": 60, + "stop_rule": "Stop at the first verified exact classification and constructive decoder; package the result without extending the model.", + "outcome": "completed", + "evidence": "PROOF.md gives the all-input proof. verify.py enumerates every binary row space through dimension six, compares a direct coefficient observation oracle, tests the decoder and boundary/rejection controls, and generates file-bound output.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can an actual convolution caller guarantee sparse coefficient-error supports?", + "why_it_matters": "A support restriction could escape the unrestricted uniform-error obstruction.", + "first_step": "Prove an error-support restriction from a completed numerical supplier, then price exact checks and decoding.", + "blocked_by": "A uniform absolute-error estimate does not establish support sparsity." + }, + { + "question": "Can a fully paid odd-modulus recovery interface lower required precision?", + "why_it_matters": "The binary obstruction does not cover larger residue alphabets.", + "first_step": "Specify a coefficient domain, exact residue acquisition, returned error and full storage/restoration bill.", + "blocked_by": "No odd-modulus caller or cost contract is supplied." + } + ], + "coordination": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19272169", + "playbook": "autonomous local run", + "freshness": { + "canonical_main": "a5bff3bf133e482541c09eba4e773884bdb2b1b7", + "priority_revision": 8, + "overlap_open_prs_utc": "2026-10-29T16:12:13Z", + "overlap_discussions_utc": "2026-10-29T16:13:26Z", + "limits": "Cached helper: 310 open PRs and 5898 discussion records with complete reported remote pagination; local sparse notes incomplete. Separate current-main README and merged-title/body searches were also performed. Unpublished work and arbitrary diffs remain outside coverage.", + "final_fetch_utc": "2026-10-29T16:23:00Z", + "final_canonical_main": "a5bff3bf133e482541c09eba4e773884bdb2b1b7", + "final_overlap": "Live open PRs, exact-sum/parity/sketch main README terms, merged PR body searches and all current local locks checked before committing; no same-question work identified. Searches are bounded and do not establish novelty." + }, + "validation": { + "environment": "CPython 3.12.15; macOS 27.0.1 arm64; standard library only", + "registered_normal_and_optimized": "PASS; all 3287 row spaces through N=6, 67 admitting/3220 excluding, 5704 boundary decodes, 1089 sub-half decodes, 66 omitted-check controls, 63 unit ambiguities, 20 invalid contracts, one large-integer fixture", + "direct_replay_seconds": [ + "0.25", + "0.25" + ], + "registered_seconds": "0.75", + "syntax_and_function_lengths": "PASS; both Python files, maximum 60 lines per function", + "unrun": [ + "selected scientific cold replay", + "physical acquisition and restoration", + "actual convolution caller", + "numerical supplier", + "Lean", + "Docker", + "independent human or formal proof-kernel review" + ] + } +} diff --git a/research/sum-parity-recovery/VERIFY.json b/research/sum-parity-recovery/VERIFY.json new file mode 100644 index 0000000000..67bc5b1515 --- /dev/null +++ b/research/sum-parity-recovery/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 row-space census, direct equal-sum coefficient collision oracle, constructive decoder, closed-boundary and invalid-input controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The same complete finite checks with Python assertions disabled." + } + ] +} diff --git a/research/sum-parity-recovery/recovery.py b/research/sum-parity-recovery/recovery.py new file mode 100644 index 0000000000..c52f417678 --- /dev/null +++ b/research/sum-parity-recovery/recovery.py @@ -0,0 +1,90 @@ +"""Exact integer recovery with a fixed binary sketch and an exact sum. + +Produced by Nick Petalas. Apache-2.0. +The executable domain is bounded; PROOF.md has no dimension/magnitude bound. +""" + +from fractions import Fraction + +MAX_DIMENSION = 64 +MAX_BITS = 4096 + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def checked_integer(value, name): + require(type(value) is int, name + " must be an integer") + require(value.bit_length() <= MAX_BITS, name + " exceeds bit limit") + return value + + +def checked_fraction(value, name): + require(type(value) in (int, Fraction), name + " must be exact") + value = Fraction(value) + checked_integer(value.numerator, name + " numerator") + checked_integer(value.denominator, name + " denominator") + return value + + +def sketch(values, rows): + """Internal exact parity evaluation after boundary validation.""" + bits = sum((value & 1) << i for i, value in enumerate(values)) + return tuple((bits & row).bit_count() & 1 for row in rows) + + +def unique_binary_solution(rows, right, dimension): + """Eliminate at most 65 equations in at most 64 binary unknowns.""" + equations = list(zip(rows, right)) + pivot_rows = [] + for column in range(dimension): + candidates = [i for i in range(len(pivot_rows), len(equations)) + if equations[i][0] & (1 << column)] + require(bool(candidates), "Parity and sum do not determine all parities") + pivot = len(pivot_rows) + other = candidates[0] + equations[pivot], equations[other] = equations[other], equations[pivot] + mask, value = equations[pivot] + for i, (old_mask, old_value) in enumerate(equations): + if i != pivot and old_mask & (1 << column): + equations[i] = (old_mask ^ mask, old_value ^ value) + pivot_rows.append(pivot) + require(all(mask or not value for mask, value in equations), + "Inconsistent parity equations") + assert all(equations[i][0] == 1 << i for i in range(dimension)) + return tuple(equations[i][1] for i in range(dimension)) + + +def decode(observations, rows, tags, total, radius): + """Return the unique promised vector, or reject an invalid contract. + + Fixed rows are N-bit masks. The promise is |y_i-c_i| <= radius < 1. + For radius >= 1/2, the augmented parity matrix must have full rank. + """ + dimension = len(observations) + require(2 <= dimension <= MAX_DIMENSION, "Dimension outside 2..64") + require(len(rows) <= MAX_DIMENSION and len(rows) == len(tags), + "Sketch size outside contract") + total = checked_integer(total, "Sum") + radius = checked_fraction(radius, "Radius") + require(0 <= radius < 1, "Radius outside [0,1)") + exact = tuple(checked_fraction(y, "Observation") for y in observations) + for row in rows: + checked_integer(row, "Row") + require(0 <= row < 1 << dimension, "Row outside dimension") + require(all(type(tag) is int and tag in (0, 1) for tag in tags), + "Tags must be binary integers") + if radius < Fraction(1, 2): + result = tuple((y + Fraction(1, 2)).__floor__() for y in exact) + else: + parity = unique_binary_solution( + [*rows, (1 << dimension) - 1], [*tags, total & 1], dimension) + result = tuple(2 * ((y - bit + 1) / 2).__floor__() + bit + for y, bit in zip(exact, parity)) + require(all(abs(y - value) <= radius for y, value in zip(exact, result)), + "No vector meets the radius promise") + require(sum(result) == total, "Recovered sum disagrees") + require(sketch(result, rows) == tuple(tags), "Recovered sketch disagrees") + return result diff --git a/research/sum-parity-recovery/verify.py b/research/sum-parity-recovery/verify.py new file mode 100644 index 0000000000..c3801eca13 --- /dev/null +++ b/research/sum-parity-recovery/verify.py @@ -0,0 +1,192 @@ +"""Bounded exact corroboration of PROOF.md; writes nothing. + +Produced by Nick Petalas. Apache-2.0. Standard library only. +""" + +from fractions import Fraction as F +from hashlib import sha256 +from itertools import combinations, product +from pathlib import Path +import json +import sys + +sys.path.insert(0, str(Path(__file__).resolve().parent)) +from recovery import decode, require, sketch + +HERE = Path(__file__).resolve().parent +PACKAGE_FILES = ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", + "VERIFY.json", "recovery.py", "verify.py") + + +def row_spaces(dimension): + """Every reduced binary row space once; used only for 2 <= N <= 6.""" + require(2 <= dimension <= 6, "Exhaustive dimension outside 2..6") + for rank in range(dimension + 1): + for pivots in combinations(range(dimension), rank): + free = [(i, j) for i, pivot in enumerate(pivots) + for j in range(pivot + 1, dimension) if j not in pivots] + for assignment in range(1 << len(free)): + rows = [1 << pivot for pivot in pivots] + for bit, (i, j) in enumerate(free): + rows[i] |= ((assignment >> bit) & 1) << j + yield tuple(rows) + + +def subspace_count(dimension): + answer = 0 + for rank in range(dimension + 1): + numerator = denominator = 1 + for i in range(rank): + numerator *= (1 << dimension) - (1 << i) + denominator *= (1 << rank) - (1 << i) + require(numerator % denominator == 0, "Gaussian binomial integrality") + answer += numerator // denominator + return answer + + +def span_is_full(rows, dimension): + """Independent bounded span enumeration, without decoder elimination.""" + span = {0} + for row in [*rows, (1 << dimension) - 1]: + span |= {x ^ row for x in tuple(span)} + return len(span) == 1 << dimension + + +def boolean_collision(rows, dimension): + """Direct observation oracle on every binary vector and its exact sum.""" + seen = {} + for mask in range(1 << dimension): + values = tuple((mask >> i) & 1 for i in range(dimension)) + key = (sum(values), sketch(values, rows)) + if key in seen: + return seen[key], values + seen[key] = values + return None + + +def exhaustive_sketches(): + census = [] + failed = admitted = collision_checks = decoder_checks = 0 + for dimension in range(2, 7): + spaces = list(row_spaces(dimension)) + require(len(set(spaces)) == len(spaces) == subspace_count(dimension), + "Complete distinct row-space inventory") + census.append([dimension, len(spaces)]) + for rows in spaces: + full = span_is_full(rows, dimension) + collision = boolean_collision(rows, dimension) + require(full == (collision is None), "Rank criterion versus direct oracle") + if collision is not None: + left, right = collision + midpoint = tuple(F(a + b, 2) for a, b in zip(left, right)) + require(left != right and sum(left) == sum(right), "Distinct equal sums") + require(sketch(left, rows) == sketch(right, rows), "Equal sketches") + require(all(abs(y - a) <= F(1, 2) and abs(y - b) <= F(1, 2) + for y, a, b in zip(midpoint, left, right)), + "Actual half-unit ambiguity") + failed += 1 + collision_checks += 1 + continue + admitted += 1 + for mask in range(1 << dimension): + values = tuple(((mask >> i) & 1) * 7 - 3 for i in range(dimension)) + for radius in (F(1, 2), F(999, 1000)): + noise = tuple(radius * (-1 if (mask >> i) & 1 else 1) + for i in range(dimension)) + observed = tuple(a + e for a, e in zip(values, noise)) + require(decode(observed, rows, sketch(values, rows), + sum(values), radius) == values, + "Constructive decoder at closed error boundary") + decoder_checks += 1 + return dict(row_spaces=census, admitted_sketches=admitted, + excluded_sketches=failed, explicit_ambiguities=collision_checks, + boundary_decodes=decoder_checks) + + +def expect_rejection(call, phrase): + try: + call() + except ValueError as error: + require(phrase in str(error), "Rejection had an unexpected cause") + else: + raise ValueError("Invalid contract accepted: " + phrase) + + +def boundary_controls(): + low_noise = 0 + for dimension in range(2, 7): + for values in product((-1, 0, 1), repeat=dimension): + observed = tuple(F(x) + F(499, 1000) * (-1 if i & 1 else 1) + for i, x in enumerate(values)) + require(decode(observed, (), (), sum(values), F(499, 1000)) == values, + "Sub-half-unit recovery with no sketch") + low_noise += 1 + omissions = 0 + for dimension in range(2, 13): + optimal = tuple(1 << i for i in range(dimension - 1)) + require(span_is_full(optimal, dimension), "N-1 attaining construction") + for removed in range(dimension - 1): + rows = optimal[:removed] + optimal[removed + 1:] + left = tuple(int(i == removed) for i in range(dimension)) + right = tuple(int(i == dimension - 1) for i in range(dimension)) + require(sketch(left, rows) == sketch(right, rows), "Omitted check ambiguity") + observed = tuple(F(a + b, 2) for a, b in zip(left, right)) + expect_rejection(lambda: decode(observed, rows, sketch(left, rows), + 1, F(1, 2)), "determine all parities") + omissions += 1 + unit_ambiguities = 0 + for dimension in range(2, 65): + left = (0, 2) + (0,) * (dimension - 2) + right = (2, 0) + (0,) * (dimension - 2) + rows = tuple(1 << i for i in range(dimension)) + require(sum(left) == sum(right) and sketch(left, rows) == sketch(right, rows), + "Radius-one ambiguity") + require(max(abs(F(a + b, 2) - a) for a, b in zip(left, right)) == 1, + "Exact unit error") + unit_ambiguities += 1 + return dict(sub_half_decodes=low_noise, indispensable_check_controls=omissions, + unit_radius_ambiguities=unit_ambiguities) + + +def invalid_controls(): + valid = dict(observations=(F(1, 2), F(1, 2)), rows=(1,), tags=(0,), total=1, radius=F(1, 2)) + controls = [ + ({"observations": (F(0),)}, "Dimension"), + ({"observations": (F(0),) * 65}, "Dimension"), + ({"rows": (1,) * 65, "tags": (0,) * 65}, "Sketch size"), + ({"tags": ()}, "Sketch size"), ({"tags": (True,)}, "Tags"), + ({"tags": (2,)}, "Tags"), ({"rows": (-1,)}, "Row outside"), + ({"rows": (4,)}, "Row outside"), ({"rows": (True,)}, "must be an integer"), + ({"radius": 1}, "Radius outside"), ({"radius": F(-1)}, "Radius outside"), + ({"radius": 0.5}, "must be exact"), ({"total": True}, "must be an integer"), + ({"total": 1 << 4096}, "bit limit"), + ({"observations": (0.5, F(1, 2))}, "must be exact"), + ({"observations": (F(1, 1 << 4096), F(0))}, "bit limit"), + ({"observations": (F(0), F(0)), "total": 2, "radius": F(0)}, "sum disagrees"), + ({"observations": (F(0), F(0)), "total": 0, "tags": (1,), "radius": F(0)}, "sketch disagrees"), + ({"observations": (F(1, 2), F(1, 2)), "radius": F(0)}, "radius promise"), + ({"rows": (1, 1), "tags": (0, 1)}, "Inconsistent parity"), + ] + for changes, phrase in controls: + arguments = dict(valid, **changes) + expect_rejection(lambda: decode(**arguments), phrase) + huge = (1 << 4000, -(1 << 4000) + 1) + require(decode(tuple(F(x) + F(3, 4) for x in huge), (1,), (0,), 1, F(3, 4)) == huge, + "Large signed integer fixture") + return dict(invalid_contract_rejections=len(controls), large_integer_decodes=1) + + +def main(): + require(len(sys.argv) == 1, "No command-line options are supported") + result = dict(schema="sum-parity-recovery/1", claim_type="scoped proof with finite corroboration") + result.update(exhaustive_sketches()) + result.update(boundary_controls()) + result.update(invalid_controls()) + result["package_sha256"] = {name: sha256((HERE / name).read_bytes()).hexdigest() + for name in PACKAGE_FILES} + print(json.dumps(result, indent=2, sort_keys=True)) + print("PASS_SUM_PARITY_RECOVERY") + + +if __name__ == "__main__": + main()