Skip to content

Prove a nine-call returned-register minimum and restrict clean-helper words - #4961

Merged
Mister-Meeseeks merged 1 commit into
CrocSwap:mainfrom
aliromman:codex/publish-four-register-query-limits
Oct 23, 2026
Merged

Mister-Meeseeks merged 1 commit into
CrocSwap:mainfrom
aliromman:codex/publish-four-register-query-limits

Conversation

@aliromman

Copy link
Copy Markdown
Contributor

This adds two scoped lower-bound results for three active targets and one extra register in the formal abelian bit model. With an arbitrary fourth input that must return unchanged, nine paid calls are necessary and sufficient, even when the three targets differ. With a zero fourth input whose output is discarded, the second result excludes two complete scalar classes and narrows the remaining eight-call question. Neither result changes the complete kappa calculation.

The returned-register proof, clean-register proof guide, and the two source manifests (returned, clean) state the hypotheses and retained inputs.

Each paid factor is I + ([A]-1)N over F_2[M_3(Q)], with additive rational address frames. Each A is nonzero and has rational rank one; each N is a binary rank-one idempotent on four scalar registers. The three targets are invertible lower-triangular rational 3 by 3 matrices. No numerator or denominator bound is imposed on the rational frames.

  • The returned-register theorem requires the full endpoint diag([C_1],[C_2],[C_3],1). It rules out every eight-call word in this four-register model. The direct nine-call word attains the bound and preserves the arbitrary fourth input.
  • The clean-register result constrains only the active 3 by 3 block. Span at most four needs at least nine calls; span eight is impossible; span seven forces zero active off-diagonal projector entries. A complete check excludes all 24 projectors with that pattern. A second complete check excludes every eight-call word over the coordinate-basis projectors plus one arbitrary binary-basis set.

These give concrete rejection criteria for proposed short circuits. The clean problem remains open at frame spans five and six outside those two scalar classes. Fixing one basis to the coordinate basis is a restriction, not a normalization of every pair of bases. The clean endpoint is the product of the listed paid factors; no additional final free scalar map is included. These results give no physical supplier, implementation speedup, or complete clean-helper lower bound.

The base is cef4b52f2a59009865bf8eabde1be3f159063703. PR #468, at its consumed source pin, supplies the three-register theorem, span-four method and exact relation-search framework. Its lineage credits @eumemic through PR #288, at 475a088b5862f75f0b10596cfd6842d19531a5ec, for the register model and projection/flag bound. It also credits @huxint through PR #203, at d2873e20750d0949d2ad75cbc4cd82b5b1a74e84, for the related common triangular-frame obstruction. Original source bytes and notices are retained. No literature-priority claim is made.

From the repository root, use Python 3.10 or later, a C++17 compiler, and new build paths. Only the Python standard library is required. CXX selects the main compiler; the unchanged historical returned-register control script also requires clang++ on PATH.

python3 -B research/bit-three-active-one-returned/verify.py --build /tmp/three-active-one-returned-replay
python3 -B research/bit-three-active-one-returned/verify_independent.py --primary-build /tmp/three-active-one-returned-replay --build /tmp/three-active-one-returned-independent
python3 -E -B research/bit-three-active-one-returned/verify_fraction_terminals.py research/bit-three-active-one-returned /tmp/three-active-one-returned-replay /tmp/three-active-one-returned-fraction.json
python3 -B research/bit-clean-extra-register/verify.py --build /tmp/clean-extra-register-replay

The returned primary replay reports:

Exact checks: 2 27156 0 0
Exact checks: 3 1901600 538 0

The clean replay ends with:

PASS_CLEAN_RESTRICTED_CLASSES 314666 7406643

Fresh independent agent checks passed. For the returned endpoint, both exact engines agree on all 27,156 rank-two and 1,901,600 rank-three words. A separate front end covers 831,600 and 41,706,000 raw orders and reproduces both binary streams. All 538 terminal words also pass the Fraction replay, with zero candidates. Seven formal-polynomial controls and 19 bounded controls passed, including a full nine-call endpoint check, every deleted-call mutation, and a changed returned endpoint. The returned review and review receipt record the exact scope.

For the clean endpoint, both exact engines agree on all 314,666 zero-pattern words; a separate generator covers all 3,674,160 raw orders. The full 166-alphabet census covers 7,406,643 words and 181,099,930 relation states, with zero survivors. The separate Fraction engine agrees on 48 selected words and 54 terminals. Independent projector/completion checks, five polynomial acceptance/rejection controls, source-corruption checks and Python-environment controls also passed. The clean review and review receipt distinguish the full census from selected-case corroboration. The full basis census was not repeated with a second arithmetic engine. Polynomial fixtures are not paid-call circuit constructions.

The reviews record the final wrapper environment fixes and receipt additions, which received targeted checks after the full runs on unchanged mathematical sources. The inherited PR #468 finite search was not repeated. No selected-supplier cold replay, complete kappa computation, proof-assistant verification or hosted CI result is claimed. Substantial OpenAI Codex assistance was used for the proofs, implementations and packaging. Separate agent review is not independent human review. The package guides state the remaining returned-role and clean-helper questions and their first proof obligations.

@Mister-Meeseeks
Mister-Meeseeks merged commit 9f789e8 into CrocSwap:main Oct 23, 2026
2 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants