Model.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

abbrev OAI.ArtinCAT0.Letters line 9
Also declared: ComparatorChallenges/ArtinCAT0.lean:9 (same declaration text).
abbrev OAI.ArtinCAT0.Label line 10
Also declared: ComparatorChallenges/ArtinCAT0.lean:10 (same declaration text).
def OAI.ArtinCAT0.blockLetter line 12
Also declared: ComparatorChallenges/ArtinCAT0.lean:12 (same declaration text).
def OAI.ArtinCAT0.Adjacent line 17
Also declared: ComparatorChallenges/ArtinCAT0.lean:17 (same declaration text).
def OAI.ArtinCAT0.Distant line 21
Also declared: ComparatorChallenges/ArtinCAT0.lean:21 (same declaration text).
def OAI.ArtinCAT0.Sentinel line 25
Also declared: ComparatorChallenges/ArtinCAT0.lean:25 (same declaration text).
def OAI.ArtinCAT0.explicitMatrix line 29
Also declared: ComparatorChallenges/ArtinCAT0.lean:29 (same declaration text).

def OAI.ArtinCAT0.alternating line 35

Source documentation

Alternating word of length n, starting with s.

Also declared: ComparatorChallenges/ArtinCAT0.lean:34 (same declaration text).

def alternating {S : Type uS} (s t : S) : ℕ → FreeGroup S
  | 0 => 1
  | n + 1 => FreeGroup.of s * alternating t s n

/-- Infinity imposes no relation. Diagonal entries impose only trivial relations. -/

def OAI.ArtinCAT0.artinRelators line 40
Source documentation
Infinity imposes no relation. Diagonal entries impose only trivial relations.
Also declared: ComparatorChallenges/ArtinCAT0.lean:38 (same declaration text).
```
def artinRelators {S : Type uS} (M : S → S → Label) : Set (FreeGroup S) :=
…
```
Mentions: OAI.ArtinCAT0.Label
abbrev OAI.ArtinCAT0.ArtinGroup line 44
Also declared: ComparatorChallenges/ArtinCAT0.lean:42 (same declaration text).
def OAI.ArtinCAT0.Segment line 48
Source documentation
A geodesic parametrized proportionally to length on the closed unit interval. Values outside [0,1] are irrelevant.
Also declared: ComparatorChallenges/ArtinCAT0.lean:44 (same declaration text).
```
def Segment {X : Type uX} [MetricSpace X] (x y : X) (γ : ℝ → X) : Prop :=
…
```
def OAI.ArtinCAT0.CAT0 line 58
Source documentation
Geodesic Euclidean triangle comparison. For points of parameters t and u on the sides xy and xz, the right hand side is the squared Euclidean comparison distance, expanded by the law of cosines. All geodesic sides, also degenerate ones, are quantified. Any pair of triangle sides has a common vertex, so this is the full triangle-comparison convention, not a midpoint-only condition.
Also declared: ComparatorChallenges/ArtinCAT0.lean:49 (same declaration text).
```
def CAT0 (X : Type uX) [MetricSpace X] : Prop :=
…
```
def OAI.ArtinCAT0.GeometricAction line 68
Source documentation
Proper and cocompact isometric action. Properness of the metric space and nonemptiness are separate standing hypotheses in the theorem below.
Distinct definitions of this name: ComparatorChallenges/ArtinCAT0.lean:57 (same statement text; different proof or body). Qualify references as OAI.ArtinCAT0.GeometricAction@path.
```
def GeometricAction (G : Type uG) (X : Type uX) [Group G] [MetricSpace X] [MulAction G X] : Prop :=
…
```