Repository navigation
Prove the sharp formal orbit query bound with returned spectators - #4267
Merged
Mister-Meeseeks merged 1 commit intoOct 21, 2026
Conversation
3 of 4 tasks
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Change and mathematical scope
Proves a sharp
3B-call theorem for the fixed two-bank, three-port orbit grammar. First variation or two evaluations supply the lower bound, even with arbitrary restored dirty scalar spectators and invertible parameter-independent bridges. Three cyclic port-conjugates per bank pair attain it. BIT, complex C4 and the C3 regular-cover models have separate explicit hypotheses.Only
research/orbit-closed-call-bound/changes. The pinned E8 census supplies 54 eligible root lines in 18 orthogonal triples. It is geometric motivation, not a reduction of arbitrary native callers to the formal query alphabet. No native cost, complete supplier, new kappa or selected-result change is claimed.Task and overlap
Base
12fa8c5c844be21bfefb38a19503fbd867a11244, priority 7. The explicit user request to finish preserved C09 work changes the currentjoint-query-controllerscope; the installed QQ16 caller's complete bill remains outside this result.PR4023 proves a different one-bank order-four/quartic query theorem. The present contribution completes the two-bank orbit bound to sharpness and permits arbitrary restored scalar spectators. The separate cubic scalar-caller theorem is excluded from this PR. Live PR/Discussion and current manifest searches were reconciled; their bounded text coverage is not a novelty certificate.
Validation
Exact reviewed head:
647de55efebbffd34375d5019b3a92259b54a546. Local and official export checks passed with unchanged read-only inventory. Wrapper integrity controls also pass in normal/optimized Python 3.12: 58 intended rejections and 14 check deletions per mode.Run
python3.12 -B scripts/research_package.py --package research/orbit-closed-call-bound. Finite cases use B=1,2,4 and h=0,1,3, retaining full formal coefficients and 1,104 BIT / 8,832 C4 regular-action columns. Thirty deliberate defects and thirty named-guard deletion controls exercise the mathematical components. The all-B/h/f result is a written proof under the specified formal models, not an exhaustive finite search or formal-kernel proof. The larger retained R865 circuit and unrelated frontier packages are not replayed.Credit
Scientific data are pinned to
20ecf2891d80b5acf18d980b2164fb44ea7faa90. The E8 chart retains Dylan Crow / utcorvusvolat-dotcom's PR370 ancestry through eumemic's carrier-skeleton package, with original notices. Earlier group-algebra rank/specialization methods, including eumemic's retained PR288 and Ali Romman's PR468, are credited. Historical C09 bytes remain unchanged. Ross Richardson with substantial OpenAI Codex assistance, including separate mathematical review contexts. Apache-2.0; no independent human acceptance is implied.Open next questions
Bind one literal paid native caller to the local-generator and parameter-independent bridge contracts before applying this formal floor.
README.mdandTASK.jsonstate the smallest useful follow-up and the missing native reduction and complete physical-cost obligations.