feat: add Kuznetsov/Boone–Higman word-problem-solvable eval problem#382
Merged
Hidden character warning
The head ref may contain hidden characters: "knill-\u00a7122-boone-higman-simple"
Conversation
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
…imple Codex review of PR #382 confirmed the formal encoding is faithful (ComputablePred is the right level of algorithmic decidability; List (Fin n × Bool) signed-letter words match FreeGroup.mk; IsNormalClosureFG + Surjective matches Group.IsFinitelyPresented; IsSimpleGroup extends Nontrivial, so the trivial-group case is excluded automatically) and caught a real mathematical error in informal_solution. My prior text claimed "adjoining any nontrivial relator collapses G" with no mechanism — adding `w' just makes `w = 1' immediate, which proves nothing about non-membership of `w'. Rewrote with the correct Kuznetsov argument: in a nontrivial simple group, a nontrivial `w' has normal closure = G, so adding `w = 1' collapses the presented group to trivial; semi-decide `w ≠ 1' by enumerating consequences of `rels ∪ {w}' until each generator is forced to 1. Also tightened the attribution: this is Kuznetsov's theorem 1958; Boone–Higman 1974 is the later iff characterisation that situates it. Retitled and softened the docstring + manifest accordingly. Co-Authored-By: Claude Opus 4.7 <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 the Kuznetsov / Boone–Higman theorem (A.V. Kuznetsov 1958, W.W. Boone–G. Higman 1974) as an eval problem: a finitely presented simple group has a solvable word problem.
The encoding is computability-genuine: a word in the generators
g₁, …, gₙand their inverses isList (Fin n × Bool)(which isPrimcodable), and the word problem is decidable iff the predicatew ↦ φ (FreeGroup.mk w) = 1isComputablePred— i.e. there's a Turing machine deciding it, not just a bundledProp. The hypotheseshsurj+hkerunpackGroup.IsFinitelyPresented Gfor this presentation; since solvability of the word problem is independent of the chosen finite presentation, quantifying over an arbitrary one is the standard reading.Mathlib has
Group.IsFinitelyPresented,Subgroup.IsNormalClosureFG,FreeGroup,PresentedGroup,IsSimpleGroup, and the fullComputablePred/Computable/Partrecstack withPrimcodableinstances forFin n × BoolandList _, but no notion of the word problem of a group, no Kuznetsov / Boone–Higman / Novikov result, and no r.e./co-r.e. machinery wired to group presentations. The proof (consequences r.e., negation r.e. via collapse from simplicity, both r.e. ⇒ decidable) is absent.§122 of Knill's Some Fundamental Theorems in Mathematics (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf).
🤖 Prepared with Claude+Codex+Aristotle