Main.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Intermediate simple overgroups, finite-presentation transport, and Boone–Higman equivalence.

theorem OAI.FiniteAlgebraicEnvelopes.input_countable_simple_extension line 17

Source documentation

A countable simple overgroup supplied by the action envelope.

theorem input_countable_simple_extension (G : Type u) [Group G] [Group.FG G]
    (hG : HasDecidableWordProblem G) :
    ∃ (H : Type u) (_ : Group H), Countable H ∧ IsSimpleGroup H ∧
      ∃ f : G →* H, Function.Injective f := by
…

theorem OAI.FiniteAlgebraicEnvelopes.input_finitely_generated_simple_extension line 35

Source documentation

A finitely generated countable simple overgroup.

theorem input_finitely_generated_simple_extension (G : Type u) [Group G] [Group.FG G]
    (hG : HasDecidableWordProblem G) :
    ∃ (H : Type u) (_ : Group H), Group.FG H ∧ Countable H ∧ IsSimpleGroup H ∧
      ∃ f : G →* H, Function.Injective f := by
…

theorem OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.finitelyPresented line 70

Source documentation

Finite presentation of the actual twisted finite-chart group for a faithful 2-transitive action with finitely generated point stabilizers.

theorem finitelyPresented [Group.IsFinitelyPresented Γ] [Infinite X]
    [FaithfulSMul Γ X]
    (htwo : ∀ x₁ x₂ y₁ y₂ : X, x₁ ≠ x₂ → y₁ ≠ y₂ →
      ∃ g : Γ, g • x₁ = y₁ ∧ g • x₂ = y₂)
    (hstab : ∀ x : X, Group.FG (MulAction.stabilizer Γ x)) :
    Group.IsFinitelyPresented (group (Γ:=Γ) (X:=X)) := by
…

Mentions: OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.group

theorem OAI.FiniteAlgebraicEnvelopes.main_forward line 101
Source documentation
Forward direction of the Boone–Higman equivalence, using the proved action envelope and the complete finite presentation of its concrete simple endpoint.
```
theorem main_forward (G : Type u) [Group G] [Group.FG G]
    (hG : HasDecidableWordProblem G) : EmbedsInFinitelyPresentedSimpleGroup G := by
…
```
theorem OAI.FiniteAlgebraicEnvelopes.main line 115
Source documentation
Manuscript Theorem 1.1, with arbitrary finitely generated input, including finite and trivial input groups, and genuine algorithmic word-problem decidability.
Distinct definitions of this name: ComparatorChallenges/BooneHigman.lean:26 (different declaration text). Qualify references as OAI.FiniteAlgebraicEnvelopes.main@path.
```
theorem main (G : Type u) [Group G] [Group.FG G] :
    HasDecidableWordProblem G ↔ EmbedsInFinitelyPresentedSimpleGroup G :=
…
```