Repository navigation
Prove the sharp common-five P112 deletion bound - #3253
Merged
Mister-Meeseeks merged 1 commit intoOct 17, 2026
Merged
Mister-Meeseeks merged 1 commit into
Mister-Meeseeks merged 1 commit into
Conversation
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.
Summary
Prove the sharp common-five deletion lemma over every characteristic-zero field, for directions whose residual binary label rank is at most seven. This resolves PR3230's named handoff; its separate-five counterexample has a different contract.
Adds only
research/p112-common-five-deletion/, with the proof, literal witness, two finite implementations, complete receipts and replay instructions. Exact commitf27442f87cf1fd86a50b8ba15615d8d655d06a85, base463113d675af7410ac91d53a4fed51ec6494eb9a. Canonical investigation. TASK.json records the scope change from generic helper synthesis to this explicit handoff.Credit DreamingOfClouds/PR3154 for Lemma N and the decoder-floor reduction, Nick Petalas/PR3230 for the separate-five boundary and question, and the retained PR3161/3162/3169 E8/P112 geometry lineage, including joaqcoo. Development and verification used substantial automated assistance; no independent human review is claimed.
Evidence
The written classification uses the standard real Weyl-chamber theorem and a rational-nullspace field transfer. No new historical profile exclusion, full C5, decoder floor, supplier or kappa is claimed. Hosted planning and the complete package replay both passed at exact head
f27442f87cf1fd86a50b8ba15615d8d655d06a85. Two unsuppressed Ruff S603 trust-boundary reports are documented in README.md and CHECKS.json.Open next question: bind a still-open caller's literal single common support and retained code dimension before applying this lemma. Separately affordable cuts do not supply that hypothesis.
Merge Danger
Door: two-way
Blast Radius: research
One new opt-in package and one declared unchanged geometry input. Frozen predecessors and the selected result are unchanged. Retaining this package does not admit a supplier or certify a multiplication theorem.