Repository navigation
Prove the width-two F2 six-call floor with genuine group-word collisions - #6097
Open
JoyboyBrian wants to merge 11 commits into
Open
JoyboyBrian wants to merge 11 commits into
JoyboyBrian wants to merge 11 commits into
Conversation
Corner sandwiches with the first and last projectors replace the group-specific support filter of CrocSwap#4089 and CrocSwap#4093, so the floor holds for every noncommuting pair, coefficient field and width.
…al pair targets (no new κ) Independent line-by-line audit of PR6038's conjugate-pair proof (no error), Theorem S: any label set avoiding the two target entries needs four calls, with a two-case proof, and a stdlib group-free finite certificate. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
This was referenced Oct 28, 2026
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 support-only relaxation in #6048 leaves the five-call
diag([xyx],[yxy])question open because independently assigned subset classes need not respect group cancellation. This package proves a computer-assisted six-call floor for arbitrary groups and label sets, restricted to width two over F2, when the two distinct targets each require at least three labels. Forxyx/yxysatisfying those hypotheses the direct six-call construction meets the bound.The proof explains why common-prefix/suffix cancellation and joint coefficient parity preserve every actual group realization. A small exact refutation enumerates all 9,331 rank-one-projector tuples of lengths zero through five, with zero survivors; it does not enumerate groups or infer a theorem from finite-group examples. A written five-call example exposes the shared relation that a support-only relaxation misses.
Validation: registered Python 3.12 normal and optimized checks; independent authentication of every generated cancellation rule; exact six-call endpoint; collision-solver acceptance of known four- and six-call constructions; reopened four-call control without cancellation and reopened two-call control without the short-target restriction; committed-byte, source-history and mode checks; official export/input check; Git-free normal and optimized replay. Exact source heads #6048
518cd2a7880f94b80c9c93aad304a7f041def647and #60380cee0e104b68ce6f06bf84af03f46ac30680e64care pinned and retained in ancestry without changing frozen files.Scope: the result depends on the small Python refutation and its written soundness argument. Other fields, larger widths, proof-kernel verification, native tariffs, restoration, complete suppliers and the selected frontier remain outside this result. Open next questions are included.
Credit: Josie Elliston (#6048), Nick Petalas (#6038), Wentao Li (#4089/#4093), and Cinna Davis (#2246). Prepared by JoyboyBrian with substantial OpenAI Codex assistance. Canonical investigation: #6093.