Repository navigation
Verify changed-owner and recursive-query phase gates (no new κ) - #4712
Merged
Mister-Meeseeks merged 1 commit intoOct 22, 2026
Merged
Conversation
This was referenced Oct 22, 2026
Merged
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.
The phase-adapter research now changes the owner/query protocol beyond the retained fixed phase graph. This adds exact arbitrary-input constructions, explicit failed admission gates, and two fresh Lean modules with eight standard-axiom reports. No improvement beyond PR4610's conditional κ = 0.0030217758 is established.
The changed-owner package emits a 128-owner dyadic adapter satisfying A³ = I, with 2,356 scalar operations and tariff 26,632. Its implementation uses no Gaussian oracle, so finite order earns no productive Gaussian credit; the proposed shared-owner split fails. A separate dirty-helper construction returns
(x,y+Fx,Fh)exactly, but three paid calls minus its one independent helper reward costs twice the replaced center bill.The recursive-query package proves an all-input four-shear producer and both row/column split identities. Its honest direct invoice remains 120 heads per row or column query, not eight: the four-shear implementation costs 480 heads versus 240 for the shared pre/post implementation. Actual transported-projector counterexamples also reject the proposed scalar Temperley–Lieb closure. These are scoped negative gates, not a universal lower bound.
A separate evaluator audits Dugongue's PR4703 complementary B/C suppliers: both 632-row arbitrary-input endpoints, independent helpers, scalar frames, actual paid widths and shared maps. The exact upstream optimized replay also completed, including 2,088 B and 2,048 C paid/helper phase pairs in both orientations and corruption controls. Its local improvement still lacks a profitable complete gauged consumer and compiler admission.
Validation and replay:
propext,Classical.choiceandQuot.sound. Source/log/object/runtime pins and clean-checkout replay instructions are included. The registered Python hook does not compile Lean.The entry point is
research/kappa-recursive-phase-checkpoint-20261023/README.md. The earlier 29-report round-seven checkpoint is already published in PR4610 and is linked as predecessor evidence, not counted as fresh work here. This PR starts from canonical mainb58ad9ef4d4e861b0eaa5dba41742bdc072dca51, priority revision 7, and leaves the selected record unchanged.Credit PR4610 and the retained Gaussian/helper/query/compiler lineage; Cinna Davis's PR4696, PR4700 and PR4698; and Dugongue's PR4654 and PR4703. Retained source attribution and notices are preserved. Substantial OpenAI Codex assistance; new work is Apache-2.0.
The remaining task is an affordable physical producer/consumer with complete arbitrary-owner restoration and a strict paid recurrence, followed by native, finite-compiler and outer-transfer admission. These scoped Lean identities and finite checks do not prove the full integer-multiplication theorem.