Prove sharp N-1 parity threshold for sum-assisted coefficient recovery (no κ)

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.

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.

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"
+    }
+  ]
+}