Prove exact five-bit coordinate-parity recovery (no new κ)

research/rounded-inverse-parity-tags/PROOF.md

@@ -0,0 +1,173 @@
+# Five coordinate parities are necessary and sufficient
+
+This is a scoped proof using an exhaustive finite certificate for its final
+coordinate-covering step. It concerns one fixed rounded map and one restricted
+side-information interface. It is not a complete multiplication theorem.
+
+## Map and credited premises
+
+Use zxv's PR5444 matrix M, with 112 rows and eight columns, as copied without
+change into MATRIX.json. The Gram identity M^T M = 56 I and the rounded native
+inverse interface are predecessor premises, not new results here. PR5444
+builds on Ali Romman's PR5323 recovery theorem, JoyboyBrian's PR5035 finite
+kernel, and Dillon Amburgey's PR4933 and David Ganz's PR4929 native geometry.
+Their source notices and claims remain unchanged.
+
+For x in Z^112 define
+
+    q(x) = R(16 M^T x / 52),
+    F(x) = 16 x - M q(x),
+
+where R rounds each coordinate to the nearest integer, with half ties away
+from zero. A tag is the tuple of x_i modulo two for a fixed known set S of
+owner indices. The set is independent of x and the output. No additional
+input read or observation is available to the decoder.
+
+**Theorem.** The smallest cardinality of S making
+
+    x -> (F(x), (x_i mod 2) for i in S)
+
+injective on all of Z^112 is five. One attaining zero-based set is
+
+    S = {0, 9, 27, 76, 79}.
+
+The lower bound is certified by all 6,210,820 four-element subsets of the
+112 indices. Each misses at least four of the 128 distinct collision-parity
+signatures defined below. These signatures are not preimages of a single
+output; they collect all possible collision differences over all outputs.
+
+## Reduction to a fixed finite domain
+
+Choose an integer 112-by-eight matrix B satisfying M^T B = 2 I. The verifier
+finds each column B_j as a signed sum of two coordinate unit vectors and
+checks all eight identities. This also gives the decoder's quotient
+congruences. The source row-lattice description in PR5444 already implies
+the existence of such witnesses.
+
+Suppose F(x) = F(x') = y. Write q = q(x), q' = q(x'), and s = M^T y. Then
+
+    16 (x' - x) = M (q' - q),
+    M^T (16 x) = s + 56 q.
+
+The rounding equation for a single quotient coordinate is
+
+    R((s_j + 56 q_j) / 52) = q_j.
+
+It implies -26 <= s_j + 4 q_j <= 26. The admissible integers are consecutive
+after possibly deleting the boundary endpoints. There can be fourteen
+integers in the closed interval only if both endpoints occur. At residual
+-26 the lower quotient would need q_j >= 1 for half-away rounding. At
+residual +26 the upper quotient would need q_j <= -1. Both conditions cannot
+hold because the lower quotient is smaller. Thus at most thirteen
+consecutive integers survive, and |q'_j - q_j| <= 12. This scalar interval
+argument is also present in PR5444; it is recalled to delimit the new finite
+reduction rather than claimed as a new precision frontier.
+
+Multiplying the first equation by B^T gives
+
+    16 B^T (x' - x) = 2 (q' - q).
+
+Consequently q' - q = 8 v for v in {-1,0,1}^8. For a nontrivial collision
+v is nonzero, and
+
+    x' - x = M v / 2 in Z^112.
+
+Define
+
+    V = {v in {-1,0,1}^8 \ {0} : M v is even in every coordinate}.
+
+Every nontrivial collision therefore has a difference Mv/2 with v in V.
+The full domain is only 3^8 = 6,561 vectors before filtering. No cutoff on
+the magnitude of x is used in this implication.
+
+## Every retained direction is an actual collision
+
+The finite reduction above is exact, rather than just a necessary condition.
+For any v in V, set
+
+    x = -7 B v,
+    x' = x + M v / 2.
+
+These are integer vectors. The predecessor Gram identity gives
+
+    M^T x = -14 v,
+    M^T x' = 14 v.
+
+Since R(56/13) = 4, their quotients are -4v and 4v. Hence
+
+    F(x)  = 16 x + 4 M v,
+    F(x') = 16 x + 8 M v - 4 M v = F(x).
+
+They are distinct because M has full column rank and v is nonzero. The
+literal verifier also checks both endpoints of every one of these new
+collision witnesses using a separate Fraction-based implementation of F.
+
+For v in V, define the 112-bit signature
+
+    sigma(v)_i = (M v / 2)_i mod 2.
+
+It follows that a fixed coordinate set S suffices exactly when every
+signature is nonzero on S. If a signature vanishes on S, the explicit pair
+above defeats those tags. If none vanishes, the necessary collision
+reduction proves injectivity for every integer input.
+
+## Finite certificate and exact minimum
+
+The verifier enumerates all of V directly from the literal matrix. It
+obtains 480 signed directions and 128 distinct signatures, with no zero
+signature. For each owner index i it constructs a bitset recording the
+signatures nonzero at i.
+
+The union of the five bitsets for {0,9,27,76,79} contains all 128 signatures.
+For the lower bound, the verifier visits every a < b < c < d in {0,...,111}.
+It computes the uncovered-signature bitset and rejects if that bitset is
+empty. The number of visited sets must equal binomial(112,4) = 6,210,820.
+Its smallest uncovered count is four. The complete histogram is generated
+in the stdout receipt, together with package-file hashes and five literal
+collisions obtained by omitting one member of the attaining set.
+
+This is the finite computational step of the proof. The all-input
+conclusion follows from the preceding exact reduction. A set of fewer than
+four coordinates extends to a four-element set and therefore also fails.
+The five-element witness supplies the matching upper bound.
+
+## Constructive decoding
+
+Given y and the five tags, enumerate possible quotients as follows. For
+each sparse B_j, the equality y + Mq = 16x implies
+
+    B_j^T y + 2 q_j = 0 mod 16.
+
+Thus B_j^T y must be even, and q_j is fixed modulo eight. Intersect this
+residue class with the closed interval
+
+    ceil((-26-s_j)/4) <= q_j <= floor((26-s_j)/4).
+
+There are at most two choices per coordinate, hence at most 256 quotient
+tuples. For each tuple, require y + Mq to be divisible by sixteen, form x,
+check the five parities, and check the defining map F(x) = y. Valid encoded
+input has one matching candidate. The injectivity theorem rules out a
+second. Checking the defining map handles the half-tie endpoint rules
+without granting them incorrectly.
+
+The supplied Python codec limits input integers to 4,096 magnitude bits.
+Its output parser allows twelve additional bits. That covers the forward
+map, whose row supports have size four and column supports have size 56:
+|F(x)_i| <= (16 + 896/13) ||x||_infinity + 2.
+The mathematical theorem is unrestricted in integer magnitude. The code
+rejects excessive requests rather than claiming an all-size machine bill.
+
+## Scope and remaining obligations
+
+PR5444 already supplies a maximum fiber of sixteen and an optimal general
+four-bit tag at this precision. Five is the new optimum only for fixed
+individual-coordinate parity tags. It does not improve that unrestricted
+information optimum. The gap is one bit, and it avoids requiring the tag to
+be an arbitrary function of all inputs. No claim about the physical price
+of acquiring those parities or computing either decoder follows.
+
+Reversible tag acquisition and cleanup, numerical access, rounding-error
+propagation, scratch, fixed-tape travel, native hosting, the complete caller,
+recursive pricing and the outer theorem remain unproved here. No selected
+frontier change or new kappa is claimed. Independent human and formal
+proof-kernel review are unclaimed.

research/rounded-inverse-parity-tags/README.md

@@ -0,0 +1,134 @@
+# Exact five-bit coordinate-parity recovery
+
+**Scoped proof with a finite exhaustive certificate; no new kappa.** For
+the fixed 112-owner rounded inverse in zxv's
+[PR5444](https://github.com/CrocSwap/integer-mult-bounds/pull/5444), after
+four uniform relative precision bits, exactly five fixed original-input
+coordinate parities suffice to recover every integer input. Every choice
+of four coordinates fails. One attaining zero-based set is
+
+    {0, 9, 27, 76, 79}.
+
+The explicit map is
+
+    F(x) = 16 x - M round_away(16 M^T x / 52),   x in Z^112.
+
+Each tag is x_i modulo two, retained before overwriting x. The decoder sees
+only F(x), those five bits, and the fixed matrix. This is a new restricted
+recovery interface answering part of PR5444's recovery question. Its
+unrestricted four-bit recovery tag remains better in bit count. The new
+result determines the exact one-bit penalty for using individual source
+parities instead of an arbitrary tag function.
+
+[PROOF.md](PROOF.md) reduces every collision to an explicitly attainable
+direction v in {-1,0,1}^8 with Mv even. There are 480 such nonzero directions
+and 128 distinct parity signatures. The five selected coordinates cover
+all signatures. All 6,210,820 four-coordinate sets leave at least four
+signatures uncovered. These signatures range over all outputs, rather
+than belonging to one fiber. [parity.py](parity.py) supplies a decoder with
+at most 256 candidate quotient tuples.
+
+## Reproduce
+
+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/rounded-inverse-parity-tags/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/rounded-inverse-parity-tags/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/rounded-inverse-parity-tags
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/rounded-inverse-parity-tags --check-source-history
+```
+
+Another CPython 3.12 executable can replace the local path. Expected markers
+are `PASS_ROUNDED_INVERSE_PARITY_TAGS`, `PASS_REGISTERED_RESEARCH_PACKAGE`
+and `PASS_RESEARCH_COMMIT_BYTES`.
+
+The verifier generates a JSON receipt on stdout, binding all eight package
+files by SHA256. It checks the complete four-set lower bound, every signed
+direction's explicit collision with a separate rational interpreter, 131
+decoder round trips including every coordinate basis input and two
+4,096-bit fixtures, five omission controls and seven invalid-input classes.
+It uses no predecessor executable and writes no checkout files. The
+receipt is generated, not supplied as handwritten evidence.
+
+For direct codec use from Python, load the package directory on the module
+path, then call `matrix()`, `right_inverse(rows)`, `encode(rows, x)` and
+`decode(rows, basis, output, tags)`. The matrix and basis are trusted fixed
+configuration. Input values and packets pass explicit length, integer,
+bit-width, congruence and final-map checks. The operational input limit is
+4,096 bits per integer; the written injectivity theorem has no magnitude
+limit. This is an exact integer codec, not a reversible physical circuit.
+
+## Limits and verification status
+
+The contribution is the collision reduction, sparse coordinate-tag optimum
+and decoder. The source Gram identity, native matrix, uniform precision
+frontier and unrestricted tag optimum are cited predecessor premises. No
+predecessor scientific suite is replayed or audited. The final lower bound
+is finite exhaustive computation, joined to a written all-input reduction.
+Independent human and formal proof-kernel review are unclaimed.
+
+There is no new supplier, paid-call reduction, current P104 word, rounding
+budget, complete caller, physical tag-acquisition/erasure tariff, tape
+compiler, selected cold replay or outer theorem. All five selected
+framework assumptions remain. No Lean or Docker run is supplied. No
+kappa gain follows.
+
+The verifier uses bounded Python allocations. The collision domain has at
+most 6,560 nonzero candidates of eight entries and 112-entry images;
+the fixed matrix leaves 480. The lower-bound loop visits exactly
+binomial(112,4) sets while retaining only a bounded histogram. Decoder work
+has at most 256 candidates, each with 112 bounded integers. These are the
+managed-runtime deviations from preallocated steady-state memory in
+Power of Ten. All functions are below sixty lines; no recursion, dynamic
+code generation, subprocess or callback dispatch is used. Exceptions keep
+invariants active under optimization. Warning-strict execution and
+in-memory syntax/AST inspection supply the interpreted-code diagnostics.
+Follow-up for a physical implementation is a fixed-capacity bit/tape
+layout and charged reversible arithmetic, rather than assuming Python's
+allocation and arithmetic are free.
+
+## Open next questions
+
+Can these five source parities be retained and erased more cheaply than
+the predecessor's four-bit rank tag? Start with the five explicit owners
+and one actual inverse call, then price every source read, scratch cell,
+decoder operation and eventual erasure. Physical access and the caller's
+restoration contract are blockers; no execution advantage follows from
+the bit count alone.
+
+Can a permitted fixed change of input coordinates make four individual
+parities sufficient? Start by declaring its complete forward/inverse
+cost and applying the finite collision-signature criterion in that
+coordinate system. An arbitrary recoding cannot be assumed free.
+
+## Credit and provenance
+
+This contribution was produced by Nick Petalas. Credit zxv's PR5444 for
+the rounded-map precision/recovery interface and explicit open questions;
+Ali Romman's PR5323 for the underlying recovery-state theorem;
+JoyboyBrian's PR5035 for the finite kernel; Dillon Amburgey's PR4933 and
+David Ganz's PR4929 for the native matrix/geometry; and their retained
+native, controller, precision, compiler and recovery lineage. Integer
+rounding, congruence and finite set cover are standard background. No
+general priority claim is made for those methods.
+
+MATRIX.json is an exact copy of PR5444's FIXTURE.json. Its original source
+notices are retained in the unchanged predecessor package. No predecessor
+credit line is edited. Apache-2.0.
+
+Scientific base: canonical main `3f0152a32eeebac0df11946dbd50cabe5a7f7839`,
+priority revision 8. The source package's last changing commit is
+`9004eb1b185803ba2f3101b8955e6e8d0dc12ed4`. [SOURCES.json](SOURCES.json)
+pins all source bytes and the original card. The current selected record
+is conditional kappa 0.003125804 and is unchanged. The scope change from
+the uniform-transfer card to this recovery side result is explicit in
+[TASK.json](TASK.json).
+
+The [advance CLAIM](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19267749)
+names the delivered question. Live main, merged/open PRs, recent account
+contributions and coordination claims were checked before research.
+The overlap helper reported complete remote pagination and sparse local
+notes; targeted searches read canonical-main README matches directly.
+These checks do not cover unpublished work or every diff and do not
+establish novelty by themselves.

research/rounded-inverse-parity-tags/SOURCES.json

@@ -0,0 +1,36 @@
+{
+  "schema_version": 1,
+  "base_commit": "3f0152a32eeebac0df11946dbd50cabe5a7f7839",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a",
+      "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "research/precision-state-frontier/FIXTURE.json",
+      "usage": "input",
+      "git_blob": "0aa9f7816378c3eb11ec2e3d63ed9e85cfaa893c",
+      "sha256": "2ca4d7550fcae5b757ec500f87aee1d2ef9f64b59e4abe2bda93319521304af8"
+    },
+    {
+      "path": "research/precision-state-frontier/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "79090050d47de95750b7321d89848143cc945abe",
+      "sha256": "f7e4d410cc108bc8b148ed8641c09be20c4c864fbc3908c533fa889b59dae341"
+    },
+    {
+      "path": "research/precision-state-frontier/README.md",
+      "usage": "provenance",
+      "git_blob": "9c21dc65e529bc234ddafc8683f311185b644c01",
+      "sha256": "0a62a71cea7e8ec40cf1a175b84b2d42cd81a3d94c7ab106ea7d6c765d75d8d2"
+    }
+  ]
+}