From 2779de2ce398eba70ec195192506e6eb9548db29 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Thu, 29 Oct 2026 13:20:37 +0000 Subject: [PATCH] feat(research): prove exact five-bit coordinate parity recovery --- .../rounded-inverse-parity-tags/MATRIX.json | 918 ++++++++++++++++++ research/rounded-inverse-parity-tags/PROOF.md | 173 ++++ .../rounded-inverse-parity-tags/README.md | 134 +++ .../rounded-inverse-parity-tags/SOURCES.json | 36 + .../rounded-inverse-parity-tags/TASK.json | 96 ++ .../rounded-inverse-parity-tags/VERIFY.json | 36 + .../rounded-inverse-parity-tags/parity.py | 142 +++ .../rounded-inverse-parity-tags/verify.py | 188 ++++ 8 files changed, 1723 insertions(+) create mode 100644 research/rounded-inverse-parity-tags/MATRIX.json create mode 100644 research/rounded-inverse-parity-tags/PROOF.md create mode 100644 research/rounded-inverse-parity-tags/README.md create mode 100644 research/rounded-inverse-parity-tags/SOURCES.json create mode 100644 research/rounded-inverse-parity-tags/TASK.json create mode 100644 research/rounded-inverse-parity-tags/VERIFY.json create mode 100644 research/rounded-inverse-parity-tags/parity.py create mode 100644 research/rounded-inverse-parity-tags/verify.py diff --git a/research/rounded-inverse-parity-tags/MATRIX.json b/research/rounded-inverse-parity-tags/MATRIX.json new file mode 100644 index 0000000000..0aa9f78163 --- /dev/null +++ b/research/rounded-inverse-parity-tags/MATRIX.json @@ -0,0 +1,918 @@ +{ + "schema": "literal-eight-mode-columns-v1", + "source_path": "research/coded-native-caller/NORMALIZERS.json", + "mode_columns": [ + [ + 1, + 1, + 1, + 1, + 1, + 1, + 1, + -1, + 1, + -1, + -1, + -1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 1, + 1, + 1, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + -1, + 1, + 1, + 1, + -1, + -1, + -1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 0, + 0, + -1, + 1, + -1, + 1, + 1, + 1, + 0, + 1, + 1, + 1, + 1, + 1, + 1, + -1, + 1, + -1, + 1, + 1, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + 1, + 1, + 0, + 0, + 0, + 0, + 1, + -1, + 0, + 0, + 0, + 0, + 1, + 1, + 1, + 1, + 1, + -1, + -1, + -1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + -1, + -1, + -1, + -1, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + -1, + -1, + -1, + 1, + 1, + 1, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + -1, + -1, + -1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 1, + 1, + -1, + 1, + 0, + 0, + -1, + 1, + 1, + 1, + 0, + -1, + -1, + 0, + 0, + 0, + 0, + 1, + -1, + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 1, + 1, + -1, + 1, + 1, + 1, + 0, + 0, + 0, + 0, + 0 + ], + [ + 1, + 0, + 1, + 0, + 0, + 0, + 0, + 1, + 0, + 1, + 1, + 1, + 1, + 0, + 0, + 0, + 0, + 1, + 1, + 1, + 0, + 0, + 1, + 1, + 1, + 1, + 0, + 1, + 0, + 0, + 0, + 1, + 1, + 1, + 1, + 1, + 0, + 0, + 1, + 1, + 1, + 0, + 0, + 0, + 0, + 1, + 0, + 0, + 1, + 1, + 1, + 0, + 0, + 0, + 1, + 1, + 1, + 1, + 0, + 0, + 0, + 1, + 1, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 1, + 0, + 0, + 0, + 1, + 1, + 0, + 1, + 0, + 1, + 0, + 0, + 0, + 1, + 0, + 1, + 0, + 1, + 1, + 1, + 1, + 0, + 1, + 0, + 0, + 0, + 1, + 0, + 1, + 1, + 1, + 1, + 0, + 0, + 0, + 1, + 1, + 1, + 0, + 0 + ], + [ + 1, + 0, + 0, + 1, + 1, + 1, + 0, + 1, + -1, + 0, + 0, + 0, + 0, + 1, + 1, + 1, + -1, + 0, + 0, + 0, + 0, + 0, + -1, + -1, + -1, + 0, + -1, + -1, + 0, + 0, + 0, + 0, + 1, + 1, + 1, + -1, + 0, + 0, + 0, + 0, + 0, + -1, + -1, + -1, + -1, + -1, + 0, + 0, + 1, + 1, + 1, + 1, + 1, + 1, + 0, + 0, + 0, + -1, + 0, + 0, + 0, + 0, + 0, + 0, + -1, + -1, + -1, + 1, + 1, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + -1, + 0, + 1, + 0, + 1, + -1, + 0, + 0, + 0, + 1, + 0, + 1, + 1, + 0, + 0, + 0, + 1, + 0, + 0, + -1, + -1, + -1, + 1, + 1, + 0, + 0, + 0, + 0, + -1, + -1, + -1, + -1, + -1, + -1, + 0, + 0 + ], + [ + 0, + 1, + 1, + 0, + 1, + 1, + -1, + 0, + 0, + 1, + 0, + 0, + 0, + -1, + 0, + 0, + 1, + 0, + -1, + -1, + 1, + 1, + 0, + 0, + -1, + -1, + 0, + 0, + -1, + 0, + 0, + 0, + -1, + 0, + 0, + 1, + -1, + -1, + 0, + 1, + 1, + 0, + 0, + -1, + -1, + -1, + -1, + -1, + 1, + 0, + 0, + 1, + 0, + 0, + 1, + 1, + 0, + 0, + 1, + 0, + 0, + -1, + 0, + 0, + 1, + 1, + 0, + 0, + -1, + -1, + 0, + 0, + -1, + 0, + 0, + -1, + 0, + 0, + 1, + -1, + 0, + 0, + 1, + 0, + 0, + 1, + 1, + 0, + 0, + 1, + 0, + 0, + 0, + -1, + 1, + 0, + -1, + -1, + -1, + -1, + 0, + -1, + -1, + 0, + 1, + 0, + 0, + 1, + 0, + 0, + 1, + 1 + ], + [ + 0, + 1, + 0, + 1, + 0, + 0, + -1, + 0, + -1, + 0, + 1, + 1, + -1, + 0, + -1, + -1, + 0, + -1, + 0, + 0, + -1, + -1, + 0, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 0, + 1, + 1, + 0, + 0, + 1, + -1, + -1, + 1, + 0, + 0, + -1, + -1, + 0, + 0, + -1, + -1, + -1, + -1, + 0, + 0, + 0, + 1, + 1, + 0, + 0, + 1, + 0, + -1, + 0, + 0, + 0, + -1, + -1, + 0, + 0, + 1, + -1, + 0, + 0, + -1, + -1, + 0, + 0, + 0, + 1, + 0, + 1, + 0, + 0, + -1, + 0, + -1, + 0, + 0, + 1, + 1, + 0, + 1, + 0, + 1, + 1, + 0, + -1, + 0, + -1, + 0, + 0, + -1, + 0, + -1, + 0, + 0, + -1, + 0, + 1, + 1, + -1, + 0, + 0, + -1, + -1 + ], + [ + 0, + 0, + 1, + 1, + 0, + 0, + 0, + 0, + 1, + -1, + 0, + 0, + 1, + 1, + 0, + 0, + 1, + -1, + 0, + 0, + 1, + 1, + -1, + -1, + 0, + -1, + -1, + 0, + 0, + -1, + -1, + -1, + 0, + -1, + -1, + 0, + 1, + 1, + 1, + 0, + 0, + 0, + 0, + 1, + -1, + 0, + -1, + -1, + 0, + 1, + 1, + -1, + 0, + 0, + 0, + 0, + 1, + 0, + 0, + 1, + 1, + 1, + 0, + 0, + 0, + 0, + 1, + -1, + 0, + 0, + 0, + 0, + 1, + -1, + -1, + 0, + 0, + -1, + 1, + -1, + 1, + 0, + 0, + 1, + 1, + 0, + 0, + 0, + -1, + -1, + 0, + 0, + 0, + 0, + 1, + -1, + 0, + 0, + 0, + -1, + -1, + 0, + 0, + 1, + -1, + 0, + 0, + 0, + 1, + 1, + -1, + -1 + ], + [ + 0, + 0, + 0, + 0, + 1, + -1, + 0, + 0, + 0, + 0, + -1, + 1, + 0, + 0, + 1, + -1, + 0, + 0, + -1, + 1, + 1, + -1, + -1, + 1, + 0, + 0, + 0, + 0, + 0, + 1, + -1, + 0, + 0, + 1, + -1, + 0, + -1, + 1, + 0, + 1, + -1, + -1, + 1, + 0, + 0, + 0, + 1, + -1, + 0, + -1, + 1, + 0, + -1, + 1, + -1, + 1, + 0, + 0, + 0, + -1, + 1, + 0, + 1, + -1, + -1, + 1, + 0, + 0, + -1, + 1, + -1, + 1, + 0, + -1, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + -1, + 1, + 0, + 0, + 0, + 0, + 0, + -1, + 1, + 0, + 0, + 0, + 0, + -1, + 1, + 0, + 0, + 0, + -1, + 1, + 0, + 0, + -1, + 1, + 0, + -1, + 1, + 1, + -1 + ] + ] +} diff --git a/research/rounded-inverse-parity-tags/PROOF.md b/research/rounded-inverse-parity-tags/PROOF.md new file mode 100644 index 0000000000..b2dd2d5fde --- /dev/null +++ b/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. diff --git a/research/rounded-inverse-parity-tags/README.md b/research/rounded-inverse-parity-tags/README.md new file mode 100644 index 0000000000..6f121e4c9e --- /dev/null +++ b/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. diff --git a/research/rounded-inverse-parity-tags/SOURCES.json b/research/rounded-inverse-parity-tags/SOURCES.json new file mode 100644 index 0000000000..98b4e4e736 --- /dev/null +++ b/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" + } + ] +} diff --git a/research/rounded-inverse-parity-tags/TASK.json b/research/rounded-inverse-parity-tags/TASK.json new file mode 100644 index 0000000000..78a2de34be --- /dev/null +++ b/research/rounded-inverse-parity-tags/TASK.json @@ -0,0 +1,96 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 8, + "base_commit": "3f0152a32eeebac0df11946dbd50cabe5a7f7839", + "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": "Exact minimum fixed original-input coordinate-parity tags for the PR5444 rounded inverse at four relative precision bits.", + "scope_change_reason": "The assigned original-contribution requirement excludes predecessor audits. PR5444 explicitly leaves recovery and unequal-lattice interfaces open; this supplies a new source-specific sparse-tag construction and matching obstruction, without claiming a selected assumption is discharged.", + "bottleneck_link": "Recovery-interface side result relevant to owned erasure and precision: it prices the information width of a restricted tag ABI, while physical acquisition, reversible cleanup and the full caller remain unpriced.", + "budget_minutes": 60, + "stop_rule": "Stop at the first verified original result: five coordinate parities suffice and every four-coordinate set fails. Package it without extending to other grids or frames.", + "outcome": "completed", + "evidence": "PROOF.md gives the all-input collision reduction. verify.py enumerates all 480 directions, all 128 signatures and all 6210820 four-coordinate sets; checks the five-coordinate witness, literal collisions and decoder controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can the five coordinate parities be physically retained and erased more cheaply than a four-bit general rank tag?", + "why_it_matters": "A simpler information interface may or may not reduce the complete physical bill.", + "first_step": "Bind the five owners to one actual inverse call and charge every read, scratch cell, decode operation and erasure.", + "blocked_by": "Actual source access, reversible cleanup and complete caller contract." + }, + { + "question": "Can a paid fixed input-coordinate change make four individual parities sufficient?", + "why_it_matters": "This would remove the one-bit coordinate-tag penalty in a changed representation.", + "first_step": "Declare one legal coordinate change and its forward/inverse invoice, then recompute collision signatures.", + "blocked_by": "A priced physical coordinate change; recoding is not free." + } + ], + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19267749", + "upstream_checkpoint": { + "commit": "3f0152a32eeebac0df11946dbd50cabe5a7f7839", + "priority_revision": 8, + "utc": "2026-10-29T13:02:07Z" + }, + "claim_type": "scoped proof with a finite exhaustive certificate and constructive codec" +} diff --git a/research/rounded-inverse-parity-tags/VERIFY.json b/research/rounded-inverse-parity-tags/VERIFY.json new file mode 100644 index 0000000000..9fe043669d --- /dev/null +++ b/research/rounded-inverse-parity-tags/VERIFY.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/precision-state-frontier/FIXTURE.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Complete collision-direction and four-coordinate-cover certificate, rational endpoint oracle, exact five-bit decoder and failure controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Same complete certificate and controls with optimization; invariants use explicit exceptions." + } + ] +} diff --git a/research/rounded-inverse-parity-tags/parity.py b/research/rounded-inverse-parity-tags/parity.py new file mode 100644 index 0000000000..cdfc843b7c --- /dev/null +++ b/research/rounded-inverse-parity-tags/parity.py @@ -0,0 +1,142 @@ +"""Coordinate-parity recovery for one fixed rounded native inverse. + +Produced by Nick Petalas. Apache-2.0. +The native matrix and rounded-map interface are credited in README.md. +""" + +import hashlib +import itertools +import json +from pathlib import Path + +OWNERS = 112 +MODES = 8 +INPUT_BITS = 4096 +SELECTED = (0, 9, 27, 76, 79) +MATRIX_HASH = "2ca4d7550fcae5b757ec500f87aee1d2ef9f64b59e4abe2bda93319521304af8" + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def matrix(): + path = Path(__file__).with_name("MATRIX.json") + need(path.stat().st_size <= 1 << 20, "matrix file size bound") + raw = path.read_bytes() + need(hashlib.sha256(raw).hexdigest() == MATRIX_HASH, "matrix source hash") + columns = json.loads(raw)["mode_columns"] + need(len(columns) == MODES, "matrix mode count") + need(all(len(c) == OWNERS for c in columns), "matrix owner count") + need(all(type(a) is int and a in (-1, 0, 1) for c in columns for a in c), + "matrix entry domain") + return tuple(zip(*columns)) + + +def vector(values, length, bits, label): + need(type(values) in (list, tuple) and len(values) == length, label + " length") + need(all(type(a) is int and a.bit_length() <= bits for a in values), + label + " integer domain") + + +def times(rows, values): + return tuple(sum(a * b for a, b in zip(row, values)) for row in rows) + + +def transpose_times(rows, values): + return tuple(sum(rows[i][j] * values[i] for i in range(OWNERS)) + for j in range(MODES)) + + +def round52(value): + magnitude = (abs(value) + 26) // 52 + return magnitude if value >= 0 else -magnitude + + +def forward(rows, values): + vector(values, OWNERS, INPUT_BITS, "input") + modes = transpose_times(rows, values) + quotient = tuple(round52(16 * a) for a in modes) + correction = times(rows, quotient) + return tuple(16 * a - b for a, b in zip(values, correction)) + + +def encode(rows, values): + output = forward(rows, values) + return output, tuple(values[i] % 2 for i in SELECTED) + + +def right_inverse(rows): + """Return sparse columns B_j with M^T B_j = 2 e_j.""" + witnesses = [] + for j in range(MODES): + target = tuple(2 * (k == j) for k in range(MODES)) + found = None + for a, b, sign in itertools.product(range(OWNERS), range(OWNERS), (-1, 1)): + if tuple(rows[a][k] + sign * rows[b][k] for k in range(MODES)) == target: + found = (a, b, sign) + break + need(found is not None, "missing two-unit row witness") + witnesses.append(found) + return tuple(witnesses) + + +def quotient_lists(rows, basis, output): + moments = transpose_times(rows, output) + choices = [] + for j, (a, b, sign) in enumerate(basis): + paired = output[a] + sign * output[b] + need(paired % 2 == 0, "output fails two-unit congruence") + residue = (-paired // 2) % 8 + low = -((26 + moments[j]) // 4) + high = (26 - moments[j]) // 4 + candidates = tuple(q for q in range(low, high + 1) if q % 8 == residue) + need(0 < len(candidates) <= 2, "quotient candidate bound") + choices.append(candidates) + return choices + + +def decode(rows, basis, output, tags): + vector(output, OWNERS, INPUT_BITS + 12, "output") + vector(tags, len(SELECTED), 1, "tags") + need(all(a in (0, 1) for a in tags), "tag bit domain") + choices = quotient_lists(rows, basis, output) + answer = None + for quotient in itertools.product(*choices): + numerator = tuple(a + b for a, b in zip(output, times(rows, quotient))) + if any(a % 16 for a in numerator): + continue + candidate = tuple(a // 16 for a in numerator) + if tuple(candidate[i] % 2 for i in SELECTED) != tuple(tags): + continue + if any(a.bit_length() > INPUT_BITS for a in candidate): + continue + if forward(rows, candidate) != tuple(output): + continue + need(answer is None, "coordinate tags are ambiguous") + answer = candidate + need(answer is not None, "no matching preimage") + return answer + + +def directions(rows): + result = [] + for v in itertools.product((-1, 0, 1), repeat=MODES): + if not any(v): + continue + image = times(rows, v) + if all(a % 2 == 0 for a in image): + result.append((v, tuple(a // 2 for a in image))) + return tuple(result) + + +def collision_pair(rows, basis, direction): + left = [0] * OWNERS + for v, (a, b, sign) in zip(direction, basis): + left[a] -= 7 * v + left[b] -= 7 * sign * v + difference = times(rows, direction) + need(all(a % 2 == 0 for a in difference), "nonintegral collision") + right = tuple(a + b // 2 for a, b in zip(left, difference)) + return tuple(left), right diff --git a/research/rounded-inverse-parity-tags/verify.py b/research/rounded-inverse-parity-tags/verify.py new file mode 100644 index 0000000000..07f8d791df --- /dev/null +++ b/research/rounded-inverse-parity-tags/verify.py @@ -0,0 +1,188 @@ +"""Finite certificate and literal recovery controls. Writes only to stdout. + +Produced by Nick Petalas. Apache-2.0. +""" + +import hashlib +import json +import math +import sys +from collections import Counter +from fractions import Fraction +from pathlib import Path + +sys.path.insert(0, str(Path(__file__).resolve().parent)) +from parity import (INPUT_BITS, MODES, OWNERS, SELECTED, collision_pair, decode, + directions, encode, forward, matrix, need, right_inverse) + +ROOT = Path(__file__).resolve().parent +PACKAGE_FILES = ("MATRIX.json", "PROOF.md", "README.md", "SOURCES.json", + "TASK.json", "VERIFY.json", "parity.py", "verify.py") + + +def reference(rows, values): + columns = tuple(zip(*rows)) + quotients = [] + for column in columns: + value = Fraction(4 * sum(a * b for a, b in zip(column, values)), 13) + rounded = math.floor(abs(value) + Fraction(1, 2)) + quotients.append(rounded if value >= 0 else -rounded) + result = [16 * a for a in values] + for j in range(MODES): + for i in range(OWNERS): + result[i] -= columns[j][i] * quotients[j] + return tuple(result) + + +def signatures_and_collisions(rows, basis): + candidates = directions(rows) + signatures = {} + for v, difference in candidates: + left, right = collision_pair(rows, basis, v) + need(left != right, "collision inputs must differ") + expected = reference(rows, left) + need(reference(rows, right) == expected, "literal collision reference") + need(forward(rows, left) == expected, "forward left reference") + need(forward(rows, right) == expected, "forward right reference") + need(tuple(b - a for a, b in zip(left, right)) == difference, + "collision difference") + need(any(difference[i] % 2 for i in SELECTED), + "literal five-coordinate separation") + mask = sum((a % 2) << i for i, a in enumerate(difference)) + need(mask != 0, "undetectable coordinate collision") + signatures.setdefault(mask, v) + need(len(candidates) == 480 and len(signatures) == 128, "collision domain") + return signatures, len(candidates) + + +def coverage(signatures): + masks = tuple(sorted(signatures)) + tests = tuple(sum(((mask >> i) & 1) << j for j, mask in enumerate(masks)) + for i in range(OWNERS)) + full = (1 << len(masks)) - 1 + selected_cover = 0 + for i in SELECTED: + selected_cover |= tests[i] + need(selected_cover == full, "five-coordinate upper bound") + return masks, tests, full + + +def four_set_certificate(tests, full): + histogram = Counter() + count = 0 + for a in range(OWNERS - 3): + for b in range(a + 1, OWNERS - 2): + pair = tests[a] | tests[b] + for c in range(b + 1, OWNERS - 1): + triple = pair | tests[c] + for d in range(c + 1, OWNERS): + uncovered = full & ~(triple | tests[d]) + need(uncovered != 0, "four coordinates unexpectedly suffice") + histogram[uncovered.bit_count()] += 1 + count += 1 + need(count == math.comb(OWNERS, 4), "complete four-set enumeration") + need(min(histogram) == 4, "sharp best four-set coverage") + return count, dict(sorted(histogram.items())) + + +def omission_controls(rows, basis, signatures, masks, tests, full): + controls = [] + for omitted in SELECTED: + retained = tuple(i for i in SELECTED if i != omitted) + cover = 0 + for i in retained: + cover |= tests[i] + missing = full & ~cover + need(missing != 0, "each selected coordinate must matter") + index = (missing & -missing).bit_length() - 1 + v = signatures[masks[index]] + left, right = collision_pair(rows, basis, v) + need(forward(rows, left) == forward(rows, right), "omission collision") + need(tuple(left[i] % 2 for i in retained) == + tuple(right[i] % 2 for i in retained), "omission parity agreement") + need(left[omitted] % 2 != right[omitted] % 2, "omitted bit separates") + for values in (left, right): + output, tags = encode(rows, values) + need(decode(rows, basis, output, tags) == values, + "omission-control decoder roundtrip") + controls.append({"omitted": omitted, "direction": list(v), + "left": list(left), "right": list(right)}) + return controls + + +def decoder_checks(rows, basis): + fixtures = [tuple(0 for _ in range(OWNERS))] + fixtures += [tuple(int(i == j) for i in range(OWNERS)) for j in range(OWNERS)] + for seed in range(16): + fixtures.append(tuple(((i * i + seed * 19 * i + 7) % 43) - 21 + for i in range(OWNERS))) + for sign in (-1, 1): + fixtures.append(tuple(sign * ((1 << (INPUT_BITS - 1)) + i) + for i in range(OWNERS))) + for values in fixtures: + output, tags = encode(rows, values) + need(output == reference(rows, values), "decoder reference fixture") + need(decode(rows, basis, output, tags) == values, "exact decoder roundtrip") + need(len(fixtures) == 131, "decoder fixture census") + return len(fixtures) + + +def invalid_inputs(rows, basis): + zero = (0,) * OWNERS + cases = (("input", zero[:-1], ()), + ("input", (True,) + zero[1:], ()), + ("input", (1 << INPUT_BITS,) + zero[1:], ()), + ("decode", zero[:-1], (0,) * 5), + ("decode", zero, (0,) * 4), + ("decode", zero, (2,) + (0,) * 4), + ("decode", zero, (1,) * 5)) + for kind, values, tags in cases: + try: + if kind == "input": + encode(rows, values) + else: + decode(rows, basis, values, tags) + except ValueError: + continue + raise ValueError("invalid input accepted: " + kind) + return len(cases) + + +def file_hashes(): + result = {} + for name in PACKAGE_FILES: + path = ROOT / name + need(path.is_file() and not path.is_symlink(), "regular package file") + need(path.stat().st_size <= 1 << 20, "package-file size bound") + result[name] = hashlib.sha256(path.read_bytes()).hexdigest() + return result + + +def main(): + rows = matrix() + basis = right_inverse(rows) + for j, (a, b, sign) in enumerate(basis): + need(tuple(rows[a][k] + sign * rows[b][k] for k in range(MODES)) == + tuple(2 * int(k == j) for k in range(MODES)), "decoder right inverse") + signatures, direction_count = signatures_and_collisions(rows, basis) + masks, tests, full = coverage(signatures) + four_sets, histogram = four_set_certificate(tests, full) + controls = omission_controls(rows, basis, signatures, masks, tests, full) + rounds = decoder_checks(rows, basis) + rejected = invalid_inputs(rows, basis) + receipt = {"status": "PASS_ROUNDED_INVERSE_PARITY_TAGS", "minimum_bits": 5, + "selected_zero_based_owners": list(SELECTED), + "signed_collision_directions": direction_count, + "distinct_parity_signatures": len(masks), + "four_coordinate_sets": four_sets, + "four_set_uncovered_histogram": histogram, + "omission_controls": controls, "decoder_roundtrips": rounds, + "omission_control_roundtrips": 2 * len(controls), + "rejected_input_classes": rejected, + "two_unit_row_witnesses": basis, + "package_sha256": file_hashes()} + print(json.dumps(receipt, sort_keys=True, indent=2)) + + +if __name__ == "__main__": + main()