WordDiagram.lean`

138 declarations, 0 contain sorry, 0 declared as axioms

abbrev OAI.ArtinCAT0.WordDiagram.Letter line 7
abbrev OAI.ArtinCAT0.WordDiagram.Word line 8
def OAI.ArtinCAT0.WordDiagram.positive line 10
def OAI.ArtinCAT0.WordDiagram.signed line 11
inductive OAI.ArtinCAT0.WordDiagram.Rel line 13
abbrev OAI.ArtinCAT0.WordDiagram.P line 18
def OAI.ArtinCAT0.WordDiagram.eval line 20
lemma OAI.ArtinCAT0.WordDiagram.rel_sound line 22
lemma OAI.ArtinCAT0.WordDiagram.isUnit_of line 27
lemma OAI.ArtinCAT0.WordDiagram.all_isUnit line 38
instance OAI.ArtinCAT0.WordDiagram.(instance at line 45) line 45
lemma OAI.ArtinCAT0.WordDiagram.negative_of line 47
def OAI.ArtinCAT0.WordDiagram.fromTriangle line 53
lemma OAI.ArtinCAT0.WordDiagram.fromTriangle_eval line 59
theorem OAI.ArtinCAT0.WordDiagram.null_derivation line 68
Source documentation
Null words have actual finite derivations from cancellation and braid moves; this is not an assumed van Kampen theorem.
```
theorem null_derivation (w : Word) (h : eval w = 1) : conGen Rel w 1 := by
…
```
Mentions: OAI.ArtinCAT0.WordDiagram.Word, OAI.ArtinCAT0.WordDiagram.eval, OAI.ArtinCAT0.WordDiagram.Rel
inductive OAI.ArtinCAT0.WordDiagram.Step line 79
Source documentation
A single local cancellation or braid replacement, with fixed contexts.
```
inductive Step : Word → Word → Prop
  | context (l r : Word) {u v : Word} (h : Rel u v) : Step (l*u*r) (l*v*r)
```
Mentions: OAI.ArtinCAT0.WordDiagram.Word, OAI.ArtinCAT0.WordDiagram.Rel
lemma OAI.ArtinCAT0.WordDiagram.step_context line 82
lemma OAI.ArtinCAT0.WordDiagram.homotopy_context line 86
lemma OAI.ArtinCAT0.WordDiagram.derivation_homotopy line 94
theorem OAI.ArtinCAT0.WordDiagram.null_local_moves line 105
def OAI.ArtinCAT0.positiveValue line 114
def OAI.ArtinCAT0.positivePerm line 119
def OAI.ArtinCAT0.positiveDegree line 128
def OAI.ArtinCAT0.directionValue line 130
def OAI.ArtinCAT0.directionPerm line 134
def OAI.ArtinCAT0.directionDegree line 138
lemma OAI.ArtinCAT0.positiveValue_xLetter line 142
lemma OAI.ArtinCAT0.positiveValue_hLetter line 145
lemma OAI.ArtinCAT0.directionValue_positive line 148
lemma OAI.ArtinCAT0.directionValue_negative line 151
lemma OAI.ArtinCAT0.positiveValue_linear line 154
lemma OAI.ArtinCAT0.positiveValue_degree line 157
lemma OAI.ArtinCAT0.directionValue_linear line 161
lemma OAI.ArtinCAT0.directionValue_degree line 169
def OAI.ArtinCAT0.directionSignature line 176
lemma OAI.ArtinCAT0.directionSignature_injective line 179
lemma OAI.ArtinCAT0.directionValue_injective line 181
lemma OAI.ArtinCAT0.TargetTriangle.difference line 191
def OAI.ArtinCAT0.TriangleMesh.SimplicialLabeling.ofVertices line 208
Source documentation
Group-vertex labels determine the labelled directions: the nine positive letters and their inverses are distinct in the actual triangle Artin group.
```
noncomputable def SimplicialLabeling.ofVertices (v : V → TriangleGroup)
    (h : ∀ f : F, ∃ c : TargetTriangle, ∀ i : Fin 3, ∃ j, c.vertex j = v (M.tail (f,i))) :
    M.SimplicialLabeling := by
…
```
Mentions: OAI.ArtinCAT0.TriangleGroup, OAI.ArtinCAT0.TargetTriangle
def OAI.ArtinCAT0.WordDiagram.Legal line 245
lemma OAI.ArtinCAT0.WordDiagram.Legal.of_corners line 248
lemma OAI.ArtinCAT0.WordDiagram.Legal.constant line 251
lemma OAI.ArtinCAT0.WordDiagram.Legal.swap line 254
lemma OAI.ArtinCAT0.WordDiagram.legal_signed line 258
inductive OAI.ArtinCAT0.WordDiagram.PathStep line 266
abbrev OAI.ArtinCAT0.WordDiagram.PathHomotopy line 272
lemma OAI.ArtinCAT0.WordDiagram.pathStep_context line 274
lemma OAI.ArtinCAT0.WordDiagram.path_context line 280
def OAI.ArtinCAT0.WordDiagram.walk line 288
lemma OAI.ArtinCAT0.WordDiagram.walk_ne_nil line 292
lemma OAI.ArtinCAT0.WordDiagram.walk_head line 293
lemma OAI.ArtinCAT0.WordDiagram.eval_cons line 296
lemma OAI.ArtinCAT0.WordDiagram.walk_append line 300
lemma OAI.ArtinCAT0.WordDiagram.walk_concat line 308
lemma OAI.ArtinCAT0.WordDiagram.braid_path line 319
lemma OAI.ArtinCAT0.WordDiagram.rel_path line 345
lemma OAI.ArtinCAT0.WordDiagram.step_sound line 357
lemma OAI.ArtinCAT0.WordDiagram.walk_context line 361
lemma OAI.ArtinCAT0.WordDiagram.step_path line 375
lemma OAI.ArtinCAT0.WordDiagram.homotopy_path line 380
theorem OAI.ArtinCAT0.WordDiagram.null_path line 390
Source documentation
Every null word admits an explicit finite homotopy using only actual triangles of the Cayley complex and repeated vertices.
```
theorem null_path (w : Word) (hw : eval w = 1) (g : TriangleGroup) :
    PathHomotopy (walk g w.toList) [g] :=
…
```
Mentions: OAI.ArtinCAT0.WordDiagram.Word, OAI.ArtinCAT0.WordDiagram.eval, OAI.ArtinCAT0.TriangleGroup, OAI.ArtinCAT0.WordDiagram.PathHomotopy, OAI.ArtinCAT0.WordDiagram.walk
lemma OAI.ArtinCAT0.WordDiagram.Legal.permute line 399
abbrev OAI.ArtinCAT0.WordDiagram.Edge line 405
lemma OAI.ArtinCAT0.WordDiagram.edge_refl line 406
lemma OAI.ArtinCAT0.WordDiagram.edge_symm line 407
lemma OAI.ArtinCAT0.WordDiagram.edge_dup line 410
abbrev OAI.ArtinCAT0.WordDiagram.Row line 415
def OAI.ArtinCAT0.WordDiagram.RowGood line 417
def OAI.ArtinCAT0.WordDiagram.Strip line 418
lemma OAI.ArtinCAT0.WordDiagram.strip_good line 421
lemma OAI.ArtinCAT0.WordDiagram.strip_refl line 426
lemma OAI.ArtinCAT0.WordDiagram.strip_rotate line 430
lemma OAI.ArtinCAT0.WordDiagram.strip_swap_rotate line 434
lemma OAI.ArtinCAT0.WordDiagram.good_shift line 438
lemma OAI.ArtinCAT0.WordDiagram.reachable_rotate line 442
lemma OAI.ArtinCAT0.WordDiagram.strip_symmetric line 451
lemma OAI.ArtinCAT0.WordDiagram.strip_reach_reverse line 465
lemma OAI.ArtinCAT0.WordDiagram.strip_homotopy line 470
lemma OAI.ArtinCAT0.WordDiagram.getD_append_formula line 482
lemma OAI.ArtinCAT0.WordDiagram.getD_delete line 487
lemma OAI.ArtinCAT0.WordDiagram.getD_stutter line 498
def OAI.ArtinCAT0.WordDiagram.GoodPath line 509
lemma OAI.ArtinCAT0.WordDiagram.step_good line 512
lemma OAI.ArtinCAT0.WordDiagram.goodPath_padded line 531
def OAI.ArtinCAT0.WordDiagram.padded line 548
lemma OAI.ArtinCAT0.WordDiagram.padded_good line 550
lemma OAI.ArtinCAT0.WordDiagram.triangle_strip_nat line 566
lemma OAI.ArtinCAT0.WordDiagram.stutter_strip_nat line 583
lemma OAI.ArtinCAT0.WordDiagram.strip_padded_of_nat line 597
lemma OAI.ArtinCAT0.WordDiagram.step_strip line 613
lemma OAI.ArtinCAT0.WordDiagram.homotopy_good line 623
theorem OAI.ArtinCAT0.WordDiagram.path_grid line 633
Source documentation
A legal path homotopy is realizable on every sufficiently wide cyclic grid. All extra columns are repeated base vertices.
```
theorem path_grid {p q : List TriangleGroup} (h : PathHomotopy p q) (g : TriangleGroup) :
    ∃ B : ℕ, ∀ N : ℕ, B ≤ N → GoodPath g p →
      ReflTransGen Strip (padded g p : Row (N+1)) (padded g q) := by
…
```
Mentions: OAI.ArtinCAT0.TriangleGroup, OAI.ArtinCAT0.WordDiagram.PathHomotopy, OAI.ArtinCAT0.WordDiagram.GoodPath, OAI.ArtinCAT0.WordDiagram.Strip, OAI.ArtinCAT0.WordDiagram.padded, OAI.ArtinCAT0.WordDiagram.Row
lemma OAI.ArtinCAT0.WordDiagram.walk_append_chain line 654
lemma OAI.ArtinCAT0.WordDiagram.walk_good line 670
lemma OAI.ArtinCAT0.WordDiagram.reachable_sequence line 677
lemma OAI.ArtinCAT0.WordDiagram.Legal.target line 696
def OAI.ArtinCAT0.WordDiagram.gridLabels line 707
lemma OAI.ArtinCAT0.WordDiagram.gridLabels_legal line 711
theorem OAI.ArtinCAT0.WordDiagram.null_grid line 727
Source documentation
Every null original-generator loop has legal grid fillings of all sufficiently large widths. The entire disk is actual labelled triangles.
```
theorem null_grid (g : TriangleGroup) (w : Word) (hw : eval w = 1) :
    ∃ B : ℕ, ∀ N : ℕ, B ≤ N → ∃ H : ℕ, ∃ v : GridDisk.Vertex H (N+1) → TriangleGroup,
      (∀ i, v (Sum.inl (Fin.last (H+1),i)) = (walk g w.toList).getD i.val g) ∧
      (∀ a : GridDisk.Face H (N+1), ∃ t : TargetTriangle, ∀ k, ∃ j,
        t.vertex j = v ((GridDisk.patch H (N+1)).tail (a,k))) := by
…
```
Mentions: OAI.ArtinCAT0.TriangleGroup, OAI.ArtinCAT0.WordDiagram.Word, OAI.ArtinCAT0.WordDiagram.eval, OAI.ArtinCAT0.GridDisk.Vertex, OAI.ArtinCAT0.WordDiagram.walk, OAI.ArtinCAT0.GridDisk.Face, OAI.ArtinCAT0.TargetTriangle, OAI.ArtinCAT0.GridDisk.patch
lemma OAI.ArtinCAT0.commuting_minimizer line 758
Source documentation
A common minimizing point for two commuting elements, obtained by applying semisimplicity inside the first minimum set. No flat-torus theorem is assumed.
```
lemma commuting_minimizer (hG : GeometricAction G X) (y : X) {g h : G}
    (hc : Commute g h) : ∃ x : X,
      dist x (g • x) = stableLengthAt y g ∧ dist x (h • x) = stableLengthAt y h := by
…
```
Mentions: OAI.ArtinCAT0.stableLengthAt
lemma OAI.ArtinCAT0.minimizer_of_length_eq line 785
lemma OAI.ArtinCAT0.minimizer_zpow line 793
lemma OAI.ArtinCAT0.commuting_minimizer_product line 807
theorem OAI.ArtinCAT0.commuting_orbit_uniform line 822
lemma OAI.ArtinCAT0.WordDiagram.step_length line 843
lemma OAI.ArtinCAT0.WordDiagram.deletions_length line 846
lemma OAI.ArtinCAT0.WordDiagram.deletions_homotopy line 851
lemma OAI.ArtinCAT0.WordDiagram.deletions_context line 856
lemma OAI.ArtinCAT0.WordDiagram.deletions_grid line 863
lemma OAI.ArtinCAT0.WordDiagram.fill_row line 872
lemma OAI.ArtinCAT0.WordDiagram.pad_singleton line 886

theorem OAI.ArtinCAT0.WordDiagram.refined_grid line 894

Source documentation

Padding a boundary by repeated vertices does not demand additional uncontrolled width: the deletions themselves realize its prescribed boundary.

theorem refined_grid (g : TriangleGroup) (w : Word) (hw : eval w = 1) :
    ∃ B : ℕ, ∀ N : ℕ, B ≤ N → ∀ p : List TriangleGroup,
      ReflTransGen PathStep p (walk g w.toList) → p.length ≤ N+1 →
      ∃ H : ℕ, ∃ v : GridDisk.Vertex H (N+1) → TriangleGroup,
      (∀ i, v (Sum.inl (Fin.last (H+1),i)) = p.getD i.val g) ∧
      (∀ a : GridDisk.Face H (N+1), ∃ t : TargetTriangle, ∀ k, ∃ j,
        t.vertex j = v ((GridDisk.patch H (N+1)).tail (a,k))) := by
…

Mentions: OAI.ArtinCAT0.TriangleGroup, OAI.ArtinCAT0.WordDiagram.Word, OAI.ArtinCAT0.WordDiagram.eval, OAI.ArtinCAT0.WordDiagram.PathStep, OAI.ArtinCAT0.WordDiagram.walk, OAI.ArtinCAT0.GridDisk.Vertex, OAI.ArtinCAT0.GridDisk.Face, OAI.ArtinCAT0.TargetTriangle, OAI.ArtinCAT0.GridDisk.patch

lemma OAI.ArtinCAT0.WordDiagram.walk_join line 909
lemma OAI.ArtinCAT0.WordDiagram.repeat_contract line 920
lemma OAI.ArtinCAT0.WordDiagram.walk_pad_contract line 929
def OAI.ArtinCAT0.WordDiagram.sidePath line 936
lemma OAI.ArtinCAT0.WordDiagram.sidePath_contract line 939
lemma OAI.ArtinCAT0.WordDiagram.walk_length line 943
lemma OAI.ArtinCAT0.WordDiagram.sidePath_length line 948
def OAI.ArtinCAT0.WordDiagram.triangleBoundary line 953
lemma OAI.ArtinCAT0.WordDiagram.triangleBoundary_contract line 956
lemma OAI.ArtinCAT0.WordDiagram.triangleBoundary_length line 972
lemma OAI.ArtinCAT0.WordDiagram.fill_row_tall line 979
lemma OAI.ArtinCAT0.WordDiagram.PathStep.reverse line 992
lemma OAI.ArtinCAT0.WordDiagram.deletions_reverse line 1002
def OAI.ArtinCAT0.WordDiagram.inverseLetter line 1008
def OAI.ArtinCAT0.WordDiagram.inverseLetters line 1009
lemma OAI.ArtinCAT0.WordDiagram.signed_inverseLetter line 1011
lemma OAI.ArtinCAT0.WordDiagram.inverseLetters_cons line 1015
lemma OAI.ArtinCAT0.WordDiagram.eval_inverseLetters line 1019
lemma OAI.ArtinCAT0.WordDiagram.walk_last_append line 1027
lemma OAI.ArtinCAT0.WordDiagram.walk_append_one line 1031
lemma OAI.ArtinCAT0.WordDiagram.walk_reverse line 1038
lemma OAI.ArtinCAT0.WordDiagram.repeat_pre_contract line 1050
def OAI.ArtinCAT0.WordDiagram.fullSide line 1060
Source documentation
Extra endpoint stutters allow either orientation to be trimmed while retaining both endpoints. This ensures exact shared-edge parametrizations.
```
def fullSide (g : TriangleGroup) (w : Word) (K : ℕ) : List TriangleGroup :=
…
```
Mentions: OAI.ArtinCAT0.TriangleGroup, OAI.ArtinCAT0.WordDiagram.Word
lemma OAI.ArtinCAT0.WordDiagram.fullSide_length line 1063
lemma OAI.ArtinCAT0.WordDiagram.fullSide_trim_forward line 1068
lemma OAI.ArtinCAT0.WordDiagram.fullSide_trim_reverse line 1078