Basic.lean`

23 declarations, 0 contain sorry, 0 declared as axioms

Finite complexes are standard barycentric realizations of finite abstract simplicial complexes. Area-counted elementary edge homotopies encode the usual triangular disk diagrams, allowing spurs and collapsed edges. Null edge loops (equivalently closed lifts to the universal cover) are those admitting such a disk, without any area bound. Asphericity is vanishing of all higher homotopy groups of this finite polyhedron. The CAT conditions use the standard squared-distance / hyperbolic-cosh comparison formulations.

structure OAI.HyperbolicObstruction.FiniteComplex line 26
Also declared: ComparatorChallenges/HyperbolicObstruction.lean:26 (same declaration text).
abbrev OAI.HyperbolicObstruction.FiniteComplex.Vertex line 32
Also declared: ComparatorChallenges/HyperbolicObstruction.lean:32 (same declaration text).
def OAI.HyperbolicObstruction.FiniteComplex.Carrier line 34
Also declared: ComparatorChallenges/HyperbolicObstruction.lean:34 (same declaration text).
instance OAI.HyperbolicObstruction.FiniteComplex.(instance at line 38) line 38
def OAI.HyperbolicObstruction.FiniteComplex.Edge line 41
Also declared: ComparatorChallenges/HyperbolicObstruction.lean:41 (same declaration text).
def OAI.HyperbolicObstruction.FiniteComplex.EdgePath line 44
Also declared: ComparatorChallenges/HyperbolicObstruction.lean:44 (same declaration text).
def OAI.HyperbolicObstruction.FiniteComplex.Closed line 49
Also declared: ComparatorChallenges/HyperbolicObstruction.lean:49 (same declaration text).

inductive OAI.HyperbolicObstruction.FiniteComplex.DiskMove line 54

Source documentation

An elementary disk move. A noncollapsed triangular face costs one; a spur or a collapsed edge costs zero. Contexts are unchanged.

Also declared: ComparatorChallenges/HyperbolicObstruction.lean:54 (same declaration text).

inductive DiskMove (K : FiniteComplex) : List K.Vertex → List K.Vertex → ℕ → Prop
  | stutter (l r) (a) :
      DiskMove K (l ++ [a, a] ++ r) (l ++ [a] ++ r) 0
  | spur (l r) (a b) (h : K.Edge a b) :
      DiskMove K (l ++ [a, b, a] ++ r) (l ++ [a] ++ r) 0
  | triangle (l r) (a b c) (h : {a, b, c} ∈ K.complex.faces)
      (hne : ({a, b, c} : Finset K.Vertex).card = 3) :
      DiskMove K (l ++ [a, b, c] ++ r) (l ++ [a, c] ++ r) 1

/-- A disk certificate obtained by elementary triangle attachments/removals,
    with spurs/collapses allowed. The index is the number of triangular faces. -/

Mentions: OAI.HyperbolicObstruction.FiniteComplex

inductive OAI.HyperbolicObstruction.FiniteComplex.DiskHomotopy line 65
Source documentation
A disk certificate obtained by elementary triangle attachments/removals, with spurs/collapses allowed. The index is the number of triangular faces.
Also declared: ComparatorChallenges/HyperbolicObstruction.lean:65 (same declaration text).
```
inductive DiskHomotopy (K : FiniteComplex) : List K.Vertex → List K.Vertex → ℕ → Prop
  | refl (p) : DiskHomotopy K p p 0
  | move {p q n} : DiskMove K p q n → DiskHomotopy K p q n
  | symm {p q n} : DiskHomotopy K p q n → DiskHomotopy K q p n
  | trans {p q r m n} : DiskHomotopy K p q m → DiskHomotopy K q r n →
      DiskHomotopy K p r (m + n)
```
Mentions: OAI.HyperbolicObstruction.FiniteComplex, OAI.HyperbolicObstruction.FiniteComplex.DiskMove
def OAI.HyperbolicObstruction.FiniteComplex.Disk line 72
Also declared: ComparatorChallenges/HyperbolicObstruction.lean:72 (same declaration text).
def OAI.HyperbolicObstruction.FiniteComplex.LinearDiskFilling line 75
Also declared: ComparatorChallenges/HyperbolicObstruction.lean:75 (same declaration text).
def OAI.HyperbolicObstruction.FiniteComplex.Aspherical line 79
Also declared: ComparatorChallenges/HyperbolicObstruction.lean:79 (same declaration text).
def OAI.HyperbolicObstruction.IsSegment line 85
Source documentation
A constant-speed metric segment, parametrized on [0,1].
Also declared: ComparatorChallenges/HyperbolicObstruction.lean:85 (same declaration text).
```
def IsSegment {X : Type*} [MetricSpace X] (γ : ℝ → X) (x y : X) : Prop :=
…
```
def OAI.HyperbolicObstruction.IsGeodesic line 90
Also declared: ComparatorChallenges/HyperbolicObstruction.lean:90 (same declaration text).
def OAI.HyperbolicObstruction.CATZero line 94
Source documentation
The CN characterization of CAT(0), with whole metric segments.
Also declared: ComparatorChallenges/HyperbolicObstruction.lean:94 (same declaration text).
```
def CATZero (X : Type*) [MetricSpace X] : Prop :=
…
```
def OAI.HyperbolicObstruction.CATNegOne line 101
Source documentation
The hyperbolic-cosh midpoint characterization of CAT(-1).
Also declared: ComparatorChallenges/HyperbolicObstruction.lean:101 (same declaration text).
```
def CATNegOne (X : Type*) [MetricSpace X] : Prop :=
…
```
structure OAI.HyperbolicObstruction.GeometricAction line 108
Source documentation
A proper, cocompact isometric action of a discrete group.
Also declared: ComparatorChallenges/HyperbolicObstruction.lean:108 (same declaration text).
```
structure GeometricAction (G X : Type*) [Group G] [MetricSpace X] where
…
```
def OAI.HyperbolicObstruction.NoGeometricCATZeroAction line 116
Also declared: ComparatorChallenges/HyperbolicObstruction.lean:116 (same declaration text).
def OAI.HyperbolicObstruction.WordLength line 120
Also declared: ComparatorChallenges/HyperbolicObstruction.lean:120 (same declaration text).
def OAI.HyperbolicObstruction.WordDistance line 124
Also declared: ComparatorChallenges/HyperbolicObstruction.lean:124 (same declaration text).
def OAI.HyperbolicObstruction.WordHyperbolic line 128
Source documentation
Four-point word hyperbolicity, for some finite generating set.
Also declared: ComparatorChallenges/HyperbolicObstruction.lean:128 (same declaration text).
```
def WordHyperbolic (G : Type*) [Group G] : Prop :=
…
```
def OAI.HyperbolicObstruction.CompatibleLocallyCATNegOne line 136
Source documentation
A metric on the given finite polyhedron, not on a different topology.
Also declared: ComparatorChallenges/HyperbolicObstruction.lean:136 (same declaration text).
```
def CompatibleLocallyCATNegOne (K : FiniteComplex) : Prop :=
…
```
Mentions: OAI.HyperbolicObstruction.FiniteComplex
def OAI.HyperbolicObstruction.MainStatement line 145
Source documentation
A finite aspherical complex with hyperbolic fundamental group, no geometric CAT(0) action, and no homotopy equivalent finite complex admitting a locally CAT(-1) metric.
Also declared: ComparatorChallenges/HyperbolicObstruction.lean:145 (same declaration text).
```
def MainStatement : Prop :=
…
```