OAI/GroupTheory/BooneHigman/PartialAffine.lean

GitHub source file

97 declarations, 0 contain sorry, 0 declared as axioms

Primitive recursive dyadic partial affine monoid and its six-letter presentation.

  1. abbrev OAI.FiniteAlgebraicEnvelopes.PartialAffine.Dyad line 12

    Source documentation

    An unreduced dyadic numerator difference and a power-of-two denominator. Computation never relies on Mathlib's noncomputable coding of ℚ.

    abbrev Dyad := ℕ × ℕ × ℕ
…
  2. def OAI.FiniteAlgebraicEnvelopes.PartialAffine.Dyad.val line 14
  3. def OAI.FiniteAlgebraicEnvelopes.PartialAffine.Dyad.zero line 15
  4. def OAI.FiniteAlgebraicEnvelopes.PartialAffine.Dyad.one line 16
  5. def OAI.FiniteAlgebraicEnvelopes.PartialAffine.Dyad.neg line 17
  6. def OAI.FiniteAlgebraicEnvelopes.PartialAffine.Dyad.add line 18
  7. def OAI.FiniteAlgebraicEnvelopes.PartialAffine.Dyad.mul line 20
  8. def OAI.FiniteAlgebraicEnvelopes.PartialAffine.Dyad.le line 22
  9. def OAI.FiniteAlgebraicEnvelopes.PartialAffine.Dyad.eq line 24
  10. def OAI.FiniteAlgebraicEnvelopes.PartialAffine.Dyad.max line 25
  11. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.Dyad.val_zero line 27
  12. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.Dyad.val_one line 28
  13. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.Dyad.val_neg line 29
  14. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.Dyad.val_add line 30
  15. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.Dyad.val_mul line 34
  16. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.Dyad.le_correct line 38
  17. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.Dyad.eq_correct line 44
  18. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.Dyad.val_max line 47
  19. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.Dyad.primrec_pow2 line 53
  20. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.Dyad.primrec_neg line 57
  21. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.Dyad.primrec_add line 60
  22. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.Dyad.primrec_mul line 73
  23. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.Dyad.primrec_le line 84
  24. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.Dyad.primrec_eq line 97
  25. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.Dyad.primrec_max line 101
  26. abbrev OAI.FiniteAlgebraicEnvelopes.PartialAffine.Slope line 106
  27. def OAI.FiniteAlgebraicEnvelopes.PartialAffine.Slope.dyad line 108
  28. def OAI.FiniteAlgebraicEnvelopes.PartialAffine.Slope.val line 109
  29. def OAI.FiniteAlgebraicEnvelopes.PartialAffine.Slope.mul line 110
  30. def OAI.FiniteAlgebraicEnvelopes.PartialAffine.Slope.inv line 111
  31. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.Slope.val_eq line 112
  32. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.Slope.val_pos line 113
  33. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.Slope.val_mul line 114
  34. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.Slope.val_inv line 117
  35. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.Slope.primrec_dyad line 118
  36. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.Slope.primrec_mul line 120
  37. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.Slope.primrec_inv line 123
  38. def OAI.FiniteAlgebraicEnvelopes.PartialAffine.Bound.dom line 127
  39. instance OAI.FiniteAlgebraicEnvelopes.PartialAffine.Bound.(instance at line 130) line 130
  40. def OAI.FiniteAlgebraicEnvelopes.PartialAffine.Bound.sup line 132
  41. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.Bound.dom_sup line 137
  42. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.Bound.dom_preimage line 141
  43. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.Bound.primrec_sup line 153
  44. abbrev OAI.FiniteAlgebraicEnvelopes.PartialAffine.Data line 163
  45. def OAI.FiniteAlgebraicEnvelopes.PartialAffine.Data.mul line 165
  46. def OAI.FiniteAlgebraicEnvelopes.PartialAffine.Data.one line 169
  47. def OAI.FiniteAlgebraicEnvelopes.PartialAffine.Data.act line 170
  48. def OAI.FiniteAlgebraicEnvelopes.PartialAffine.Data.represent line 173
  49. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.Data.act_mul line 175
  50. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.Data.represent_mul line 190
  51. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.Data.represent_one line 196
  52. def OAI.FiniteAlgebraicEnvelopes.PartialAffine.Data.params line 202

    Source documentation

    The three literal parameters determine exactly a partial affine map.

    def params (a : Data) : ℚ × ℚ × Option ℚ :=
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.PartialAffine.Data

  53. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.Data.represent_of_params line 205
  54. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.Data.domain_eq line 212
  55. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.Data.params_of_represent line 218
  56. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.Data.represent_eq_iff line 257
  57. def OAI.FiniteAlgebraicEnvelopes.PartialAffine.Bound.eq line 263
  58. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.Bound.eq_correct line 268
  59. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.Bound.primrec_eq line 271
  60. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.Bound.primrec_preimage line 281
  61. def OAI.FiniteAlgebraicEnvelopes.PartialAffine.Data.eq line 292
  62. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.Data.eq_correct line 296
  63. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.Data.primrec_mul line 302
  64. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.Data.primrec_eq line 313
  65. abbrev OAI.FiniteAlgebraicEnvelopes.PartialAffine.Letter line 326

    Source documentation

    The fixed six-letter alphabet in the algebra construction, in the order u,v,u⁻¹,v⁻¹,e₀,e₁.

    abbrev Letter := Fin 6
  66. def OAI.FiniteAlgebraicEnvelopes.PartialAffine.generator line 328
  67. def OAI.FiniteAlgebraicEnvelopes.PartialAffine.evaluate line 336
  68. def OAI.FiniteAlgebraicEnvelopes.PartialAffine.value line 338
  69. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.represent_evaluate line 340
  70. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.primrec_evaluate line 347
  71. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.primrec_word_equivalence line 354

    Source documentation

    Lemma partial-affine, algorithmic part: a primitive-recursive equality test for the actual partial maps, not classical decidability.

     theorem primrec_word_equivalence : PrimrecPred (fun p : List Letter × List Letter => value p.1=value p.2) := by
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.PartialAffine.Letter, OAI.FiniteAlgebraicEnvelopes.PartialAffine.value

  72. def OAI.FiniteAlgebraicEnvelopes.PartialAffine.testedClass line 362

    Source documentation

    A computable, uniquely comparable coding of the tested class for the auxiliary monoid. No rational-number coding is used as an oracle.

    noncomputable def testedClass : List Letter → List Letter :=
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.PartialAffine.Letter

  73. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.computable_testedClass line 365
  74. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.testedClass_eq_iff line 371
  75. def OAI.FiniteAlgebraicEnvelopes.PartialAffine.monoid line 377

    Source documentation

    The manuscript's auxiliary monoid is generated by the six actual partial affine maps. none is an undefined value; composition is right first.

    def monoid : Submonoid (Function.End (Option ℚ)) :=
…
  76. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.value_mem line 380
  77. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.exists_word line 386
  78. def OAI.FiniteAlgebraicEnvelopes.PartialAffine.wordValue line 397
  79. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.wordValue_surjective line 399
  80. instance OAI.FiniteAlgebraicEnvelopes.PartialAffine.(instance at line 404) line 404
  81. instance OAI.FiniteAlgebraicEnvelopes.PartialAffine.(instance at line 408) line 408
  82. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.primrec_wordValue_equivalence line 410
  83. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.representation line 417

    Source documentation

    Every element has the exact nonempty-tail form stated in Lemma partial-affine, including a full domain as none.

     theorem representation (a : monoid) : ∃ (d : Data),Data.represent d=a := by
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.PartialAffine.monoid, OAI.FiniteAlgebraicEnvelopes.PartialAffine.Data, OAI.FiniteAlgebraicEnvelopes.PartialAffine.Data.represent

  84. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.nonempty_domain line 421
  85. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.slope_integer_power line 430
  86. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.dyadic_value line 434
  87. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.strictMono_on_domain line 438
  88. def OAI.FiniteAlgebraicEnvelopes.PartialAffine.tail line 453

    Source documentation

    Partial identities on rational tails, in the ambient partial-map monoid.

    def tail (r : ℚ) : Function.End (Option ℚ) :=
…
  89. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.tail_mul line 456
  90. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.tail_injective line 465
  91. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.tail_ne_one line 474
  92. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.generator_tail0 line 481
  93. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.generator_tail1 line 485
  94. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.generator_u line 489
  95. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.generator_v line 493
  96. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.generator_ui line 497
  97. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.generator_vi line 500