OAI/GroupTheory/RightAngledArtin/TraceWords.lean

GitHub source file

188 declarations, 0 contain sorry, 0 declared as axioms

Signed trace normal forms and slowly varying barycentric directions.

  1. abbrev OAI.EilenbergGanea.TraceWords.Letter line 16
  2. abbrev OAI.EilenbergGanea.TraceWords.Word line 17
  3. def OAI.EilenbergGanea.TraceWords.invLetter line 19
  4. theorem OAI.EilenbergGanea.TraceWords.invLetter_invLetter line 20
  5. def OAI.EilenbergGanea.TraceWords.Independent line 23
  6. theorem OAI.EilenbergGanea.TraceWords.independent_inv_left line 24
  7. theorem OAI.EilenbergGanea.TraceWords.independent_inv_right line 26
  8. theorem OAI.EilenbergGanea.TraceWords.independent_self line 28
  9. theorem OAI.EilenbergGanea.TraceWords.Independent.symm line 29
  10. inductive OAI.EilenbergGanea.TraceWords.Swap line 33

    Source documentation

    A single exchange of independent neighboring occurrences.

    inductive Swap : Word V → Word V → Prop
  | head {x y : Letter V} {w : Word V} (h : Independent L x y) :
      Swap (x :: y :: w) (y :: x :: w)
  | cons (x : Letter V) {w w' : Word V} (h : Swap w w') : Swap (x :: w) (x :: w')

variable {L}

    Mentions: OAI.EilenbergGanea.TraceWords.Word, OAI.EilenbergGanea.TraceWords.Letter, OAI.EilenbergGanea.TraceWords.Independent

  11. theorem OAI.EilenbergGanea.TraceWords.Swap.symm line 39
  12. theorem OAI.EilenbergGanea.TraceWords.Swap.length line 44
  13. abbrev OAI.EilenbergGanea.TraceWords.Equivalent line 48
  14. theorem OAI.EilenbergGanea.TraceWords.Equivalent.refl line 51
  15. theorem OAI.EilenbergGanea.TraceWords.Equivalent.symm line 52
  16. theorem OAI.EilenbergGanea.TraceWords.Equivalent.trans line 54
  17. theorem OAI.EilenbergGanea.TraceWords.Equivalent.cons line 57
  18. theorem OAI.EilenbergGanea.TraceWords.Equivalent.length line 65
  19. inductive OAI.EilenbergGanea.TraceWords.Extract line 75

    Source documentation

    Remove an occurrence accessible from the left through independent letters. This retains the actual other occurrences, not merely their group value.

    inductive Extract (x : Letter V) : Word V → Word V → Prop
  | head (w : Word V) : Extract x (x :: w) w
  | cons {y : Letter V} {w w' : Word V} (h : Independent L x y)
      (e : Extract x w w') : Extract x (y :: w) (y :: w')

variable {L}

    Mentions: OAI.EilenbergGanea.TraceWords.Letter, OAI.EilenbergGanea.TraceWords.Word, OAI.EilenbergGanea.TraceWords.Independent

  20. theorem OAI.EilenbergGanea.TraceWords.Extract.length line 81
  21. theorem OAI.EilenbergGanea.TraceWords.Extract.equivalent line 85
  22. theorem OAI.EilenbergGanea.TraceWords.Extract.unique line 92
  23. theorem OAI.EilenbergGanea.TraceWords.Extract.diamond line 105

    Source documentation

    Independent accessible occurrences may be removed in either order.

    theorem Extract.diamond {x y : Letter V} {w v u : Word V}
    (hxy : Independent L x y) (hx : Extract L x w v) (hy : Extract L y w u) :
    ∃ t, Extract L y v t ∧ Extract L x u t := by
…

    Mentions: OAI.EilenbergGanea.TraceWords.Letter, OAI.EilenbergGanea.TraceWords.Word, OAI.EilenbergGanea.TraceWords.Independent, OAI.EilenbergGanea.TraceWords.Extract

  24. theorem OAI.EilenbergGanea.TraceWords.Extract.swap line 121

    Source documentation

    An adjacent commutation does not destroy accessible occurrences.

    theorem Extract.swap {x : Letter V} {w w' v : Word V}
    (hs : Swap L w w') (he : Extract L x w v) :
    ∃ v', Extract L x w' v' ∧ Equivalent L v v' := by
…

    Mentions: OAI.EilenbergGanea.TraceWords.Letter, OAI.EilenbergGanea.TraceWords.Word, OAI.EilenbergGanea.TraceWords.Swap, OAI.EilenbergGanea.TraceWords.Extract, OAI.EilenbergGanea.TraceWords.Equivalent

  25. inductive OAI.EilenbergGanea.TraceWords.Step line 142

    Source documentation

    Delete an inverse pair after commuting its endpoints together.

    inductive Step : Word V → Word V → Prop
  | head {x : Letter V} {w w' : Word V} (h : Extract L (invLetter x) w w') :
      Step (x :: w) w'
  | cons (x : Letter V) {w w' : Word V} (h : Step w w') : Step (x :: w) (x :: w')

variable {L}

    Mentions: OAI.EilenbergGanea.TraceWords.Word, OAI.EilenbergGanea.TraceWords.Letter, OAI.EilenbergGanea.TraceWords.Extract, OAI.EilenbergGanea.TraceWords.invLetter

  26. theorem OAI.EilenbergGanea.TraceWords.Step.length line 148
  27. theorem OAI.EilenbergGanea.TraceWords.Step.swap line 154

    Source documentation

    Lift a cancellation across one independent exchange, tracking its output.

    theorem Step.swap {w w' v : Word V} (hs : Swap L w w') (he : Step L w v) :
    ∃ v', Step L w' v' ∧ Equivalent L v v' := by
…

    Mentions: OAI.EilenbergGanea.TraceWords.Word, OAI.EilenbergGanea.TraceWords.Swap, OAI.EilenbergGanea.TraceWords.Step, OAI.EilenbergGanea.TraceWords.Equivalent

  28. theorem OAI.EilenbergGanea.TraceWords.Extract.step line 178

    Source documentation

    The only overlapping cancellation shares the accessible occurrence. Its two outcomes differ only by exchanges; disjoint deletions commute.

    theorem Extract.step {x : Letter V} {w v u : Word V}
    (hx : Extract L x w v) (hs : Step L w u) :
    Equivalent L v (invLetter x :: u) ∨
      ∃ t, Step L v t ∧ Extract L x u t := by
…

    Mentions: OAI.EilenbergGanea.TraceWords.Letter, OAI.EilenbergGanea.TraceWords.Word, OAI.EilenbergGanea.TraceWords.Extract, OAI.EilenbergGanea.TraceWords.Step, OAI.EilenbergGanea.TraceWords.Equivalent, OAI.EilenbergGanea.TraceWords.invLetter

  29. theorem OAI.EilenbergGanea.TraceWords.Step.diamond line 198

    Source documentation

    Local confluence modulo independent exchanges.

    theorem Step.diamond {w v u : Word V} (hv : Step L w v) (hu : Step L w u) :
    Equivalent L v u ∨ ∃ t t', Step L v t ∧ Step L u t' ∧ Equivalent L t t' := by
…

    Mentions: OAI.EilenbergGanea.TraceWords.Word, OAI.EilenbergGanea.TraceWords.Step, OAI.EilenbergGanea.TraceWords.Equivalent

  30. instance OAI.EilenbergGanea.TraceWords.(instance at line 219) line 219
  31. theorem OAI.EilenbergGanea.TraceWords.Equivalent.step line 222
  32. def OAI.EilenbergGanea.TraceWords.traceSetoid line 235
  33. abbrev OAI.EilenbergGanea.TraceWords.Trace line 239
  34. def OAI.EilenbergGanea.TraceWords.ofWord line 240
  35. def OAI.EilenbergGanea.TraceWords.traceLength line 242
  36. theorem OAI.EilenbergGanea.TraceWords.traceLength_ofWord line 243
  37. theorem OAI.EilenbergGanea.TraceWords.ofWord_eq line 245
  38. def OAI.EilenbergGanea.TraceWords.ReductionStep line 249

    Source documentation

    Reduction of traces, not a choice of ordered representative.

    def ReductionStep (t t' : Trace L) : Prop :=
…

    Mentions: OAI.EilenbergGanea.TraceWords.Trace

  39. theorem OAI.EilenbergGanea.TraceWords.Step.trace line 253
  40. theorem OAI.EilenbergGanea.TraceWords.ReductionStep.representative line 256
  41. theorem OAI.EilenbergGanea.TraceWords.ReductionStep.length line 263
  42. theorem OAI.EilenbergGanea.TraceWords.ReductionStep.diamond line 268
  43. abbrev OAI.EilenbergGanea.TraceWords.Reduction line 282
  44. def OAI.EilenbergGanea.TraceWords.Reduced line 283
  45. theorem OAI.EilenbergGanea.TraceWords.Reduction.length_le line 286
  46. theorem OAI.EilenbergGanea.TraceWords.Reduction.confluence line 292
  47. theorem OAI.EilenbergGanea.TraceWords.Reduced.reduction_eq line 301
  48. theorem OAI.EilenbergGanea.TraceWords.exists_reduced line 307
  49. theorem OAI.EilenbergGanea.TraceWords.reduced_unique line 318
  50. def OAI.EilenbergGanea.TraceWords.normalTrace line 324
  51. theorem OAI.EilenbergGanea.TraceWords.normalTrace_reduction line 326
  52. theorem OAI.EilenbergGanea.TraceWords.normalTrace_reduced line 329
  53. theorem OAI.EilenbergGanea.TraceWords.Reduced.normalTrace_eq line 333
  54. theorem OAI.EilenbergGanea.TraceWords.Reduction.normalTrace_eq line 336
  55. theorem OAI.EilenbergGanea.TraceWords.normalTrace_idem line 341
  56. theorem OAI.EilenbergGanea.TraceWords.Swap.append_right line 345
  57. theorem OAI.EilenbergGanea.TraceWords.Equivalent.append_right line 351
  58. theorem OAI.EilenbergGanea.TraceWords.Equivalent.append_left line 359
  59. theorem OAI.EilenbergGanea.TraceWords.Extract.append_right line 365
  60. theorem OAI.EilenbergGanea.TraceWords.Step.append_right line 371
  61. theorem OAI.EilenbergGanea.TraceWords.Step.append_left line 377
  62. def OAI.EilenbergGanea.TraceWords.appendTrace line 384
  63. theorem OAI.EilenbergGanea.TraceWords.appendTrace_ofWord line 389
  64. theorem OAI.EilenbergGanea.TraceWords.ReductionStep.append_left line 393
  65. theorem OAI.EilenbergGanea.TraceWords.ReductionStep.append_right line 399
  66. theorem OAI.EilenbergGanea.TraceWords.Reduction.append_left line 405
  67. theorem OAI.EilenbergGanea.TraceWords.Reduction.append_right line 411
  68. theorem OAI.EilenbergGanea.TraceWords.normalTrace_append line 417
  69. def OAI.EilenbergGanea.TraceWords.normalCon line 425

    Source documentation

    Equality of reduced traces is a monoid congruence on signed words.

    def normalCon : Con (FreeMonoid (Letter V)) where
…

    Mentions: OAI.EilenbergGanea.TraceWords.Letter

  70. abbrev OAI.EilenbergGanea.TraceWords.WordGroup line 438
  71. def OAI.EilenbergGanea.TraceWords.groupWord line 440
  72. theorem OAI.EilenbergGanea.TraceWords.groupWord_nil line 442
  73. theorem OAI.EilenbergGanea.TraceWords.groupWord_append line 443
  74. theorem OAI.EilenbergGanea.TraceWords.groupWord_eq line 446
  75. theorem OAI.EilenbergGanea.TraceWords.Step.groupWord line 450
  76. theorem OAI.EilenbergGanea.TraceWords.Swap.groupWord line 453
  77. theorem OAI.EilenbergGanea.TraceWords.isUnit_groupWord_singleton line 457
  78. theorem OAI.EilenbergGanea.TraceWords.isUnit_groupWord line 464
  79. instance OAI.EilenbergGanea.TraceWords.wordGroupGroup line 472
  80. theorem OAI.EilenbergGanea.TraceWords.groupWord_inv_singleton line 477
  81. def OAI.EilenbergGanea.TraceWords.letterValue line 486
  82. theorem OAI.EilenbergGanea.TraceWords.letterValue_positive line 487
  83. theorem OAI.EilenbergGanea.TraceWords.letterValue_negative line 488
  84. theorem OAI.EilenbergGanea.TraceWords.letterValue_inverse line 489
  85. def OAI.EilenbergGanea.TraceWords.wordEval line 493
  86. theorem OAI.EilenbergGanea.TraceWords.wordEval_nil line 494
  87. theorem OAI.EilenbergGanea.TraceWords.wordEval_cons line 495
  88. theorem OAI.EilenbergGanea.TraceWords.wordEval_append line 497
  89. theorem OAI.EilenbergGanea.TraceWords.wordEval_singleton line 499
  90. theorem OAI.EilenbergGanea.TraceWords.letterValue_commute line 503
  91. theorem OAI.EilenbergGanea.TraceWords.Swap.wordEval line 513
  92. theorem OAI.EilenbergGanea.TraceWords.Equivalent.wordEval line 519
  93. theorem OAI.EilenbergGanea.TraceWords.Step.wordEval line 527
  94. def OAI.EilenbergGanea.TraceWords.traceEval line 536
  95. theorem OAI.EilenbergGanea.TraceWords.traceEval_ofWord line 539
  96. theorem OAI.EilenbergGanea.TraceWords.ReductionStep.traceEval line 543
  97. theorem OAI.EilenbergGanea.TraceWords.Reduction.traceEval line 548
  98. theorem OAI.EilenbergGanea.TraceWords.traceEval_normalTrace line 554
  99. def OAI.EilenbergGanea.TraceWords.groupEval line 559
  100. theorem OAI.EilenbergGanea.TraceWords.groupEval_word line 567
  101. def OAI.EilenbergGanea.TraceWords.toArtin line 576

    Source documentation

    The kernel presentation is compared with the signed trace group, not with an assumed normal-form model.

    def toArtin : WordGroup L →* ArtinGroup L :=
…

    Mentions: OAI.EilenbergGanea.TraceWords.WordGroup

  102. theorem OAI.EilenbergGanea.TraceWords.groupWord_commute line 579
  103. def OAI.EilenbergGanea.TraceWords.ofArtin line 584
  104. theorem OAI.EilenbergGanea.TraceWords.ofArtin_generator line 587
  105. theorem OAI.EilenbergGanea.TraceWords.toArtin_word line 590
  106. theorem OAI.EilenbergGanea.TraceWords.ofArtin_letter line 593
  107. theorem OAI.EilenbergGanea.TraceWords.ofArtin_word line 602
  108. theorem OAI.EilenbergGanea.TraceWords.ofArtin_toArtin line 610
  109. theorem OAI.EilenbergGanea.TraceWords.toArtin_ofArtin line 616
  110. def OAI.EilenbergGanea.TraceWords.artinEquiv line 626

    Source documentation

    The actual presented Artin group equals the word group constructed by confluence of individual-occurrence cancellations.

    def artinEquiv : ArtinGroup L ≃* WordGroup L where
…

    Mentions: OAI.EilenbergGanea.TraceWords.WordGroup

  111. theorem OAI.EilenbergGanea.TraceWords.artin_word_eq_iff line 635

    Source documentation

    Two words have the same value in the actual Artin group exactly when they have the same reduced trace.

    theorem artin_word_eq_iff (w v : Word V) :
    wordEval (artinGenerator L) w = wordEval (artinGenerator L) v ↔
      normalTrace L (ofWord L w) = normalTrace L (ofWord L v) := by
…

    Mentions: OAI.EilenbergGanea.TraceWords.Word, OAI.EilenbergGanea.TraceWords.wordEval, OAI.EilenbergGanea.artinGenerator, OAI.EilenbergGanea.TraceWords.normalTrace, OAI.EilenbergGanea.TraceWords.ofWord

  112. theorem OAI.EilenbergGanea.TraceWords.trace_reduced_minimal line 645
  113. theorem OAI.EilenbergGanea.TraceWords.Reduced.of_equivalent line 659
  114. theorem OAI.EilenbergGanea.TraceWords.Reduced.of_append_left line 663
  115. theorem OAI.EilenbergGanea.TraceWords.Reduced.of_append_right line 668
  116. theorem OAI.EilenbergGanea.TraceWords.Reduced.tail line 673
  117. theorem OAI.EilenbergGanea.TraceWords.Extract.append_singleton line 677
  118. theorem OAI.EilenbergGanea.TraceWords.Extract.last line 698
  119. theorem OAI.EilenbergGanea.TraceWords.Step.append_reduced line 708

    Source documentation

    A cancellation in a reduced word with one appended occurrence must cancel that new occurrence. The old inverse occurrence was maximal: it can be moved all the way to the right by independent exchanges.

    theorem Step.append_reduced {x : Letter V} {w v : Word V}
    (hw : Reduced L (ofWord L w)) (h : Step L (w ++ [x]) v) :
    Equivalent L w (v ++ [invLetter x]) := by
…

    Mentions: OAI.EilenbergGanea.TraceWords.Letter, OAI.EilenbergGanea.TraceWords.Word, OAI.EilenbergGanea.TraceWords.Reduced, OAI.EilenbergGanea.TraceWords.ofWord, OAI.EilenbergGanea.TraceWords.Step, OAI.EilenbergGanea.TraceWords.Equivalent, OAI.EilenbergGanea.TraceWords.invLetter

  120. theorem OAI.EilenbergGanea.TraceWords.reduced_append_alternative line 730

    Source documentation

    On an actual reduced trace, a generator step either adds a maximal occurrence or removes a maximal inverse occurrence, with no further reduction.

    theorem reduced_append_alternative {x : Letter V} {w : Word V}
    (hw : Reduced L (ofWord L w)) :
    Reduced L (ofWord L (w ++ [x])) ∨
      ∃ v, Reduced L (ofWord L v) ∧ Equivalent L w (v ++ [invLetter x]) ∧
        normalTrace L (ofWord L (w ++ [x])) = ofWord L v := by
…

    Mentions: OAI.EilenbergGanea.TraceWords.Letter, OAI.EilenbergGanea.TraceWords.Word, OAI.EilenbergGanea.TraceWords.Reduced, OAI.EilenbergGanea.TraceWords.ofWord, OAI.EilenbergGanea.TraceWords.Equivalent, OAI.EilenbergGanea.TraceWords.invLetter, OAI.EilenbergGanea.TraceWords.normalTrace

  121. def OAI.EilenbergGanea.TraceWords.predecessorRoots line 754

    Source documentation

    The previously encountered minimal ancestral directions of letters which are dependent on the next direction. Taking the minimum recursively computes the first minimal ancestor in the occurrence poset.

    def predecessorRoots (s : Multiset (V × V)) (v : V) : Finset V := by
…
  122. def OAI.EilenbergGanea.TraceWords.nextRoot line 758
  123. def OAI.EilenbergGanea.TraceWords.rootInsert line 761
  124. def OAI.EilenbergGanea.TraceWords.rootScan line 766

    Source documentation

    Each pair records an occurrence's direction and its assigned minimal ancestral direction. Signs do not change the occurrence dependency relation.

    def rootScan (s : Multiset (V × V)) (w : Word V) : Multiset (V × V) :=
…

    Mentions: OAI.EilenbergGanea.TraceWords.Word

  125. theorem OAI.EilenbergGanea.TraceWords.rootScan_nil line 769
  126. theorem OAI.EilenbergGanea.TraceWords.rootScan_cons line 770
  127. theorem OAI.EilenbergGanea.TraceWords.rootScan_append line 773
  128. theorem OAI.EilenbergGanea.TraceWords.mem_predecessorRoots line 778
  129. theorem OAI.EilenbergGanea.TraceWords.predecessorRoots_cons_independent line 784
  130. theorem OAI.EilenbergGanea.TraceWords.nextRoot_cons_independent line 790
  131. theorem OAI.EilenbergGanea.TraceWords.rootInsert_commute line 795
  132. theorem OAI.EilenbergGanea.TraceWords.Swap.rootScan line 801
  133. theorem OAI.EilenbergGanea.TraceWords.Equivalent.rootScan line 807
  134. def OAI.EilenbergGanea.TraceWords.RootInvariant line 818

    Source documentation

    Every assigned root occurs as a minimal occurrence, and the root directions of the whole state form a clique. These assertions simultaneously express support in a simplex and permanence of old assignments.

    def RootInvariant (L : SimpleGraph V) (s : Multiset (V × V)) : Prop :=
…
  135. theorem OAI.EilenbergGanea.TraceWords.nextRoot_mem_or_new line 822
  136. theorem OAI.EilenbergGanea.TraceWords.RootInvariant.insert line 836
  137. theorem OAI.EilenbergGanea.TraceWords.RootInvariant.scan line 867
  138. theorem OAI.EilenbergGanea.TraceWords.rootInvariant_word line 873
  139. def OAI.EilenbergGanea.TraceWords.rootCounts line 877
  140. def OAI.EilenbergGanea.TraceWords.wordCounts line 880
  141. def OAI.EilenbergGanea.TraceWords.traceCounts line 882
  142. theorem OAI.EilenbergGanea.TraceWords.traceCounts_ofWord line 885
  143. theorem OAI.EilenbergGanea.TraceWords.rootCounts_cons line 889
  144. theorem OAI.EilenbergGanea.TraceWords.rootCounts_zero line 894
  145. theorem OAI.EilenbergGanea.TraceWords.wordCounts_append_singleton line 897
  146. theorem OAI.EilenbergGanea.TraceWords.rootCounts_mem_iff line 905
  147. theorem OAI.EilenbergGanea.TraceWords.rootCounts_support_clique line 916
  148. theorem OAI.EilenbergGanea.TraceWords.wordCounts_support_clique line 924
  149. theorem OAI.EilenbergGanea.TraceWords.traceCounts_support_clique line 927
  150. theorem OAI.EilenbergGanea.TraceWords.rootCounts_sum line 932
  151. theorem OAI.EilenbergGanea.TraceWords.rootScan_card line 940
  152. theorem OAI.EilenbergGanea.TraceWords.wordCounts_sum line 946
  153. theorem OAI.EilenbergGanea.TraceWords.traceCounts_sum line 950
  154. theorem OAI.EilenbergGanea.TraceWords.traceCounts_append_singleton line 955
  155. theorem OAI.EilenbergGanea.TraceWords.support_subset_singleton_add line 961
  156. theorem OAI.EilenbergGanea.TraceWords.traceCounts_append_support line 969
  157. def OAI.EilenbergGanea.TraceWords.groupNormalTrace line 980

    Source documentation

    The normal trace of an element, obtained from the actual Artin presentation.

    def groupNormalTrace : WordGroup L → Trace L :=
…

    Mentions: OAI.EilenbergGanea.TraceWords.WordGroup, OAI.EilenbergGanea.TraceWords.Trace

  158. def OAI.EilenbergGanea.TraceWords.artinNormalTrace line 984
  159. theorem OAI.EilenbergGanea.TraceWords.artinNormalTrace_word line 986
  160. theorem OAI.EilenbergGanea.TraceWords.artinNormalTrace_reduced line 991
  161. theorem OAI.EilenbergGanea.TraceWords.artinNormalTrace_eval line 997
  162. theorem OAI.EilenbergGanea.TraceWords.exists_reduced_word line 1011
  163. theorem OAI.EilenbergGanea.TraceWords.artinNormalTrace_right_step line 1024

    Source documentation

    A right generator step in the actual presented group is addition/removal of exactly one maximal occurrence in its reduced trace.

    theorem artinNormalTrace_right_step (g : ArtinGroup L) (x : Letter V) :
    (artinNormalTrace L (g * letterValue (artinGenerator L) x) =
      appendTrace L (artinNormalTrace L g) (ofWord L [x])) ∨
    (artinNormalTrace L g = appendTrace L
      (artinNormalTrace L (g * letterValue (artinGenerator L) x)) (ofWord L [invLetter x])) := by
…

    Mentions: OAI.EilenbergGanea.TraceWords.Letter, OAI.EilenbergGanea.TraceWords.artinNormalTrace, OAI.EilenbergGanea.TraceWords.letterValue, OAI.EilenbergGanea.artinGenerator, OAI.EilenbergGanea.TraceWords.appendTrace, OAI.EilenbergGanea.TraceWords.ofWord, OAI.EilenbergGanea.TraceWords.invLetter

  164. def OAI.EilenbergGanea.TraceWords.traceDirection line 1045

    Source documentation

    Barycentric direction, with value zero at the empty trace.

    def traceDirection (t : Trace L) (v : V) : ℝ :=
…

    Mentions: OAI.EilenbergGanea.TraceWords.Trace

  165. def OAI.EilenbergGanea.TraceWords.artinDirection line 1048
  166. theorem OAI.EilenbergGanea.TraceWords.traceDirection_nonneg line 1052
  167. theorem OAI.EilenbergGanea.TraceWords.traceDirection_sum line 1055
  168. theorem OAI.EilenbergGanea.TraceWords.traceLength_append_singleton line 1061
  169. theorem OAI.EilenbergGanea.TraceWords.count_normalization_bound line 1069

    Source documentation

    The exact finite-coordinate estimate used in the manuscript's direction map.

    theorem count_normalization_bound (c : V →₀ ℕ) (r : V) {n : ℕ}
    (hn : 0 < n) (hs : ∑ v, c v = n) :
    ∑ v, |((c + Finsupp.single r 1 : V →₀ ℕ) v : ℝ) / (n + 1 : ℝ) -
      (c v : ℝ) / (n : ℝ)| ≤ 2 / (n + 1 : ℝ) := by
…
  170. theorem OAI.EilenbergGanea.TraceWords.traceDirection_append_bound line 1100
  171. theorem OAI.EilenbergGanea.TraceWords.traceCounts_step_common_simplex line 1109
  172. theorem OAI.EilenbergGanea.TraceWords.artinDirection_right_step line 1117

    Source documentation

    Full trace-direction step, for the actual generators of the Artin presentation. The shorter normal trace controls both the common simplex and the uniform l1 bound.

    theorem artinDirection_right_step (g : ArtinGroup L) (x : Letter V)
    (hg : 0 < traceLength L (artinNormalTrace L g))
    (hgx : 0 < traceLength L (artinNormalTrace L
      (g * letterValue (artinGenerator L) x))) :
    let t := artinNormalTrace L g
…

    Mentions: OAI.EilenbergGanea.TraceWords.Letter, OAI.EilenbergGanea.TraceWords.traceLength, OAI.EilenbergGanea.TraceWords.artinNormalTrace, OAI.EilenbergGanea.TraceWords.letterValue, OAI.EilenbergGanea.artinGenerator

  173. theorem OAI.EilenbergGanea.TraceWords.Extract.mem line 1153
  174. theorem OAI.EilenbergGanea.TraceWords.same_sign_reduced line 1158
  175. theorem OAI.EilenbergGanea.TraceWords.nextRoot_self line 1178
  176. theorem OAI.EilenbergGanea.TraceWords.rootScan_clique line 1189
  177. theorem OAI.EilenbergGanea.TraceWords.wordCounts_clique line 1213
  178. theorem OAI.EilenbergGanea.TraceWords.counts_negative_commuting_powers line 1219
  179. theorem OAI.EilenbergGanea.TraceWords.height_generator line 1253
  180. def OAI.EilenbergGanea.TraceWords.wordHeight line 1256
  181. theorem OAI.EilenbergGanea.TraceWords.wordHeight_nil line 1258
  182. theorem OAI.EilenbergGanea.TraceWords.wordHeight_cons line 1259
  183. theorem OAI.EilenbergGanea.TraceWords.height_wordEval line 1262
  184. theorem OAI.EilenbergGanea.TraceWords.wordHeight_abs_le line 1276
  185. theorem OAI.EilenbergGanea.TraceWords.height_abs_le_traceLength line 1286
  186. theorem OAI.EilenbergGanea.TraceWords.traceLength_pos_of_height_ne line 1292
  187. theorem OAI.EilenbergGanea.TraceWords.length_negative_commuting_powers line 1300
  188. theorem OAI.EilenbergGanea.TraceWords.direction_negative_commuting_powers line 1306