Liu: state Theorem 2.1 directly, drop statement scaffolding (part 1) - #1096
Merged
Merged
Conversation
Restate the proved Liu results with plain hypotheses and replace the predicate/relation-parameterized factor-return route by a direct proof: the three degree cases of a left deletion branch give the translated right-pencil splitting, which restores compatibility; the right branch follows by symmetry. The common-interleaver hypothesis of the old factor-return statements was never used and is gone. Delete the theorem-shaped statement defs of Interfaces, Theorem21Assembly, Corollary22, DeletionBranches, the FactorReturn* layers and the positive-split x-subtraction leaves, all wrappers taking them as hypotheses (including every theorem conditional on the refuted branch-only forward direction), and the superseded low-degree packagings. Only the refuted published forward statement stays, beside its negation. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
PerAlexandersson
force-pushed
the
chore/wrappers-liu
branch
from
October 2, 2026 16:08
e6314a6 to
83f7133
Compare
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
1 participant
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.
Part 1 of the Liu cluster wrapper cleanup (Theorem 2.1 top layers and the factor-return route). Low-level
xSub…Splits, quartic boundary, cubic root-order andpositiveSplit…RootCountAboveNonRootstatements follow in a second PR.Deleted (415 declarations, ~4.4k lines)
…Statementdefs: every theorem-shaped target inInterfaces,Theorem21Assembly,Corollary22,DeletionBranches,FactorReturnStatements,FactorReturnAssembly/*, and the positive-split x-subtraction relation/predicate leaves (XSub/SameDegree,XSub/LeftSucc).theorem21CompatibleToRootCountBranchesStatement,theorem21CompatibleRootCount[Nonconstant]Statement,…DeletionPair…, the two vacuous_of_forwardlemmas inTheorem.lean).…Predicate_of_right_natDegree_…,…_of_xSub, low-degreeNatDegreeLeTwopackages) and 49 plain low-degree/predicate plumbing lemmas, all special cases of the proved general reverse direction.Theorem21Assembly,Corollary22,FactorReturnStatements,FactorReturnAssembly/{Left,Right,Predicate}DegreeCases,FactorReturnAssembly/DegreeCaseAssembly.Restated / new
positiveSplit{SameDegree,RightSuccDegree,LeftSuccDegree}TranslatedXSubRightFamily: explicit binders (same argument order as before).theorem21LeftFactorReturn{SameDegree,SuccDegree,TwoDegree}TranslatedRightFamily: the genuine reductions, formerly…_of_xSub_rightPredicate, now unconditional. Their unused common-interleaver and predicate arguments are gone.LeftRootCountBranch.compatible,RightRootCountBranch.compatible, andcompatible_of_theorem21RootCountBranches(the reverse direction, for all degrees). These replace the six-case factor-return package.theorem21CompatibleToRootCountBranchesNoCommonNonconstant,theorem21CompatibleRootCountNoCommonNonconstant: explicit binders.corollary22DegreeDiff_proofis renamed tocorollary22DegreeDiffwith explicit binders. The old projection of that name is removed.Kept
theorem21CompatibleToRootCountBranchesNonconstantStatement, besidenot_theorem21CompatibleToRootCountBranchesNonconstantStatement. This is the refuted interface listed inPROOF_STATUS.mdand is used by the catalog'spublished_forward_direction_fails.theorem21DeletionPairCommonInterleaverBranches…,theorem21PositiveDeletionCompatibleBranches…, the low-degree x-subtraction lemmas).🤖 Generated with Claude Code