[petalas]

Summary

Scoped proof with an exhaustive finite certificate and a constructive decoder. For PR5444's fixed 112-owner rounded inverse at four uniform relative precision bits, the exact minimum number of fixed original-input coordinate parities needed for recovery is five. Every four-coordinate set fails. An attaining zero-based set is {0,9,27,76,79}.

encode(x): return F(x), (x_i mod 2 for i in {0,9,27,76,79})
decode(y,tags): test at most 256 quotient tuples; return the unique matching x
F(x) = 16x - M round_away(16 M^T x / 52)

PR5444 already supplies a sixteen-state maximum fiber and an optimal general four-bit tag. This result gives the exact one-bit penalty for the restricted coordinate-parity interface. It does not improve the unrestricted tag optimum or claim a new kappa.

The contribution was produced by Nick Petalas. Credit zxv's PR5444 for the precision/recovery interface and open question, Ali Romman's PR5323 recovery theorem, JoyboyBrian's PR5035 kernel, Dillon Amburgey's PR4933 and David Ganz's PR4929 native geometry, and their retained lineage. The source matrix and Gram identity are cited premises; no predecessor scientific suite is audited or replayed.

Evidence

The new all-input reduction proves that every collision difference is Mv/2, where nonzero v lies in {-1,0,1}^8 and Mv is even. Every retained direction has an explicit attaining collision.

• The verifier enumerates 480 signed directions and 128 distinct parity signatures, then all 6,210,820 four-coordinate sets. The best four-set still misses four signatures; the five-coordinate witness covers all 128.
• A separate Fraction-based interpreter checks both endpoints of every new collision. Five omission controls each retain a real collision; both inputs decode with all five tags.
• All 131 additional decoder fixtures pass, including every coordinate basis input and two 4,096-bit fixtures. Seven invalid-input classes reject. Three private optimized implementation mutations reject for their named reasons.
• Direct warning-strict normal and optimized checks pass in 1.625s and 1.480s on macOS arm64, CPython 3.12.15. The complete registered command passes in 3.149s. These durations establish the local replay budget, not a speedup claim. Normal and optimized generated receipts agree exactly and bind all eight package files.
• Committed bytes/modes, declared source history, source pins, syntax/AST and whitespace checks pass at 2779de2ce398eba70ec195192506e6eb9548db29. Official export integrity and declared-input coverage pass. The read-only, empty-PATH, Git-free optimized export replay passes with all nine payload files and the export manifest unchanged.

From the repository root:

/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 --check-modes

Any 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.

Limitations and unrun obligations

The theorem covers all integer inputs for this fixed matrix and fixed individual-coordinate parity tags. Its last lower-bound step is finite exhaustive computation. The codec implementation caps input integers at 4,096 bits; the mathematical reduction has no magnitude cutoff. Coordinate changes, adaptive tags and arbitrary tag functions are different contracts.

No physical parity acquisition, reversible computation/erasure, actual caller, complete scratch/movement/precision invoice, native/compiler admission, selected cold replay, Lean, Docker or outer multiplication proof is supplied. The five selected framework assumptions remain. Independent human and formal proof-kernel review are unclaimed. The selected frontier is unchanged.

Open next questions

• At one actual inverse call, can retaining and erasing the five source parities cost less than the general four-bit rank tag? Begin with the explicit owners and charge every read, decoder operation, scratch cell and final erasure. Physical access and restoration are blockers.
• Can a permitted, fully priced input-coordinate change make four individual parities sufficient? First declare the change and its forward/inverse invoice, then apply the collision-signature criterion.

Related open work

No open PR studying this exact rounded map's coordinate-parity recovery minimum was identified in the refreshed 322-PR open corpus and targeted live searches. PR5444 and PR5323 are merged cited predecessors. PR5530's exact two-FULL numerator-width tariff has a distinct interface. Coverage includes titles/bodies and targeted canonical-main README searches, not unpublished work or every diff. No extra predecessor computation was run for numerical comparison.

Finish-line refresh read the titles and result scopes of all thirteen other account open PRs created since the CLAIM: #6172 through #6181 and #6183 through #6185. None studies this fixed 112-owner rounded map or its coordinate-parity recovery minimum. The P104 support and Gram-channel results in #6173, #6181 and #6183 concern different operators and quantities. No same-quantity disagreement was identified, and no additional scientific computations were run to compare them.

The advance CLAIM matches the delivered scope. Canonical main was refreshed before committing and remained 3f0152a32eeebac0df11946dbd50cabe5a7f7839, priority revision 8. The current selected conditional kappa is 0.003125804.

CI notes

Both hosted checks passed at 2779de2ce398eba70ec195192506e6eb9548db29: plan and replay (research/rounded-inverse-parity-tags), in run 40881338427. The checks were read once at completion. Hosted replay certifies the registered finite checks; independent scientific acceptance and the unrun physical/theorem obligations above remain unclaimed.

Merge danger

Door: two-way. Blast radius: isolated research package. No shared code, selected-frontier or frozen-predecessor changes.