OAI/GroupTheory/BooneHigman/GroupInput.lean

GitHub source file

55 declarations, 0 contain sorry, 0 declared as axioms

Wreath-product reduction to countably infinite finitely generated decidable input groups.

  1. def OAI.FiniteAlgebraicEnvelopes.GroupInput.shift line 16
  2. def OAI.FiniteAlgebraicEnvelopes.GroupInput.shifts line 23
  3. abbrev OAI.FiniteAlgebraicEnvelopes.GroupInput.Ambient line 28
  4. def OAI.FiniteAlgebraicEnvelopes.GroupInput.base line 30
  5. def OAI.FiniteAlgebraicEnvelopes.GroupInput.embed line 35
  6. def OAI.FiniteAlgebraicEnvelopes.GroupInput.stable line 36
  7. theorem OAI.FiniteAlgebraicEnvelopes.GroupInput.embed_injective line 38
  8. theorem OAI.FiniteAlgebraicEnvelopes.GroupInput.stable_conj line 45
  9. theorem OAI.FiniteAlgebraicEnvelopes.GroupInput.commutator line 54
  10. abbrev OAI.FiniteAlgebraicEnvelopes.GroupInput.Letters line 60
  11. abbrev OAI.FiniteAlgebraicEnvelopes.GroupInput.InputWord line 61
  12. def OAI.FiniteAlgebraicEnvelopes.GroupInput.generators line 63
  13. def OAI.FiniteAlgebraicEnvelopes.GroupInput.heightLetter line 68
  14. def OAI.FiniteAlgebraicEnvelopes.GroupInput.atLetter line 73
  15. def OAI.FiniteAlgebraicEnvelopes.GroupInput.height line 78
  16. def OAI.FiniteAlgebraicEnvelopes.GroupInput.sectionWord line 80
  17. def OAI.FiniteAlgebraicEnvelopes.GroupInput.value line 84
  18. theorem OAI.FiniteAlgebraicEnvelopes.GroupInput.height_nil line 87
  19. theorem OAI.FiniteAlgebraicEnvelopes.GroupInput.height_cons line 88
  20. theorem OAI.FiniteAlgebraicEnvelopes.GroupInput.heightLetter_bounds line 91
  21. theorem OAI.FiniteAlgebraicEnvelopes.GroupInput.value_nil line 95
  22. theorem OAI.FiniteAlgebraicEnvelopes.GroupInput.value_cons line 96
  23. theorem OAI.FiniteAlgebraicEnvelopes.GroupInput.value_right line 100
  24. theorem OAI.FiniteAlgebraicEnvelopes.GroupInput.signed_right line 114
  25. theorem OAI.FiniteAlgebraicEnvelopes.GroupInput.signed_left line 121
  26. theorem OAI.FiniteAlgebraicEnvelopes.GroupInput.value_cons_left line 136
  27. theorem OAI.FiniteAlgebraicEnvelopes.GroupInput.value_left line 147
  28. theorem OAI.FiniteAlgebraicEnvelopes.GroupInput.at_low line 155
  29. theorem OAI.FiniteAlgebraicEnvelopes.GroupInput.at_high line 168
  30. theorem OAI.FiniteAlgebraicEnvelopes.GroupInput.value_eq_one_iff line 183
  31. def OAI.FiniteAlgebraicEnvelopes.GroupInput.countsLetter line 215

    Source documentation

    Unsimplified positive/negative counters avoid assuming a computation model on G.

    def countsLetter {n} : Letters n × Bool → ℕ × ℕ
  | (none, true) => (1,0)
  | (none, false) => (0,1)
  | (some _, _) => (0,0)

    Mentions: OAI.FiniteAlgebraicEnvelopes.GroupInput.Letters

  32. def OAI.FiniteAlgebraicEnvelopes.GroupInput.counts line 220
  33. def OAI.FiniteAlgebraicEnvelopes.GroupInput.natAtLetter line 223
  34. def OAI.FiniteAlgebraicEnvelopes.GroupInput.natStep line 229
  35. def OAI.FiniteAlgebraicEnvelopes.GroupInput.natAt line 233
  36. theorem OAI.FiniteAlgebraicEnvelopes.GroupInput.heightLetter_eq line 236
  37. theorem OAI.FiniteAlgebraicEnvelopes.GroupInput.counts_fold line 240
  38. theorem OAI.FiniteAlgebraicEnvelopes.GroupInput.counts_eq_height line 251
  39. theorem OAI.FiniteAlgebraicEnvelopes.GroupInput.natAtLetter_eq line 255
  40. theorem OAI.FiniteAlgebraicEnvelopes.GroupInput.natStep_fold line 261
  41. theorem OAI.FiniteAlgebraicEnvelopes.GroupInput.natAt_eq line 275
  42. theorem OAI.FiniteAlgebraicEnvelopes.GroupInput.countsLetter_primrec line 281
  43. theorem OAI.FiniteAlgebraicEnvelopes.GroupInput.counts_primrec line 283
  44. theorem OAI.FiniteAlgebraicEnvelopes.GroupInput.natAtLetter_primrec line 295
  45. theorem OAI.FiniteAlgebraicEnvelopes.GroupInput.natStep_primrec line 315
  46. theorem OAI.FiniteAlgebraicEnvelopes.GroupInput.natAt_primrec line 326
  47. theorem OAI.FiniteAlgebraicEnvelopes.GroupInput.computable_forall_lt line 334

    Source documentation

    Closure of genuine computability under a variable finite universal test.

    theorem computable_forall_lt {α : Type*} [Primcodable α] {p : α × ℕ → Prop}
    (hp : ComputablePred p) : ComputablePred (fun a : α × ℕ => ∀ k < a.2, p (a.1,k)) := by
…
  48. theorem OAI.FiniteAlgebraicEnvelopes.GroupInput.value_wordProblem line 360

    Source documentation

    The decision procedure for this finitely generated wreath subgroup.

    theorem value_wordProblem {n} (s : Fin n → G)
    (hs : ComputablePred (fun w : Word n => evalWord s w = 1)) :
    ComputablePred (fun w : InputWord n => value G s w = 1) := by
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.GroupInput.InputWord, OAI.FiniteAlgebraicEnvelopes.GroupInput.value

  49. def OAI.FiniteAlgebraicEnvelopes.GroupInput.generated line 401

    Source documentation

    The finitely generated subgroup, rather than the whole unrestricted wreath product.

    def generated {n} (s : Fin n → G) : Subgroup (Ambient G) :=
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.GroupInput.Ambient

  50. theorem OAI.FiniteAlgebraicEnvelopes.GroupInput.embed_mem_generated line 404
  51. def OAI.FiniteAlgebraicEnvelopes.GroupInput.subgroupGenerators line 426
  52. theorem OAI.FiniteAlgebraicEnvelopes.GroupInput.subgroupGenerators_generate line 429
  53. theorem OAI.FiniteAlgebraicEnvelopes.GroupInput.generated_fg line 446
  54. theorem OAI.FiniteAlgebraicEnvelopes.GroupInput.generated_wordProblem line 450
  55. theorem OAI.FiniteAlgebraicEnvelopes.group_input line 483

    Source documentation

    Wreath-product reduction using an explicit step-function witness. The construction includes finite and trivial input groups.

    theorem group_input (G : Type u) [Group G] (hG : HasDecidableWordProblem G) :
    ∃ (H : Type u) (_ : Group H), Group.FG H ∧ HasDecidableWordProblem H ∧
      ∃ (f : G × G →* H) (s : H), Function.Injective f ∧
        ∀ g : G, f (g,g) * s * (f (g,g))⁻¹ * s⁻¹ = f (g,1) := by
…