fix: require IsSimpleGroup G in m23_irrep_tensor_square_decomp#469
Merged
Conversation
The statement existentially quantified the group with only an order constraint, so it did not pin down M₂₃. Lorenzo Luccioli, using Harmonic's Aristotle, found a clever solution that never builds M₂₃: the solvable direct product SL(2,𝔽₃) × (C₂₃ ⋊ C₁₁) × C₁₆₈₀ has order 24 · 253 · 1680 = 10 200 960, and the external tensor product of a 2-, 11-, and 1-dimensional irreducible has dimension 22 and tensor-square isotypic count 2 · 2 · 1 = 4, satisfying the old existential with none of the intended M₂₃ content. Add IsSimpleGroup G. A nontrivial direct product is never simple, so all decomposable witnesses are excluded; by the classification of finite simple groups the unique simple group of order 10 200 960 is M₂₃. Update the docstring, manifest title/notes, and regenerate the workspace. Thanks to Lorenzo and Aristotle for the disproof of the earlier version. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
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.
This PR adds an
IsSimpleGroup Ghypothesis tom23_irrep_tensor_square_decompso that the statement genuinely requires the Mathieu group M₂₃ rather than admitting an unrelated witness.The previous statement existentially quantified the group with only an order constraint (
Fintype.card G = 10200960), so it did not pin down M₂₃. Lorenzo Luccioli, using Harmonic's Aristotle, found a clever solution that never builds M₂₃: the solvable direct productSL(2, 𝔽₃) × (C₂₃ ⋊ C₁₁) × C₁₆₈₀has order24 · 253 · 1680 = 10 200 960, and the external tensor product of a 2-, 11-, and 1-dimensional irreducible has dimension2 · 11 · 1 = 22with tensor-square isotypic count2 · 2 · 1 = 4, satisfying the old existential with none of the intended M₂₃ content. A nontrivial direct product is never simple, soIsSimpleGroup Gexcludes every such decomposable witness; by the classification of finite simple groups the unique simple group of order10 200 960is M₂₃. The docstring and manifest record the correction and credit Lorenzo and Aristotle for the disproof, and the generated workspace is regenerated to match.The corresponding leaderboard solve is retracted in leanprover/lean-eval-submissions#490 ("retract: remove m23_irrep_tensor_square_decomp solve").
🤖 Prepared with Claude Code