OAI/Geometry/HyperbolicGroups/MetricHexagon.lean

GitHub source file

63 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.HyperbolicObstruction.MetricHexagon.log_dist line 42

    Source documentation

    Central log comparison is equality for every pair of hexagon vertices. This proves the exact flatness used by the obstruction without assuming a flat-sector theorem or treating the tangent cone as a vector space.

    theorem log_dist (D : MetricHexagon z) (h : CATZero X) (i j : Fin 6) :
    dist (TangentCone.log h (CATZero.mid h (z 0) (z 3)) (z i))
      (TangentCone.log h (CATZero.mid h (z 0) (z 3)) (z j)) = dist (z i) (z j) := by
…

    Mentions: OAI.HyperbolicObstruction.MetricHexagon, OAI.HyperbolicObstruction.CATZero, OAI.HyperbolicObstruction.TangentCone.log, OAI.HyperbolicObstruction.CATZero.mid

  2. theorem OAI.HyperbolicObstruction.MetricHexagon.central_mid line 77

    Source documentation

    Every central midpoint comparison in the core hexagon is an equality.

    theorem central_mid (D : MetricHexagon z) (h : CATZero X) (i j : Fin 6) :
    dist (CATZero.mid h (z 0) (z 3)) (CATZero.mid h (z i) (z j)) ^ 2 =
      3 / 4 - (hexDistSq i j : ℝ) / 4 := by
…

    Mentions: OAI.HyperbolicObstruction.MetricHexagon, OAI.HyperbolicObstruction.CATZero, OAI.HyperbolicObstruction.CATZero.mid, OAI.HyperbolicObstruction.hexDistSq

  3. def OAI.HyperbolicObstruction.IncidenceTemplate.vector line 96

    Source documentation

    Points A,B,C,D followed by the three remaining nonzero vectors.

    def vector : Fin 7 → Fin 3 → ZMod 2 :=
…
  4. def OAI.HyperbolicObstruction.IncidenceTemplate.Incident line 100

    Source documentation

    Lines are the kernels of the seven nonzero linear functionals.

    def Incident (i l : Fin 7) : Prop := ∑ j, vector i j * vector l j = 0

    Mentions: OAI.HyperbolicObstruction.IncidenceTemplate.vector

  5. instance OAI.HyperbolicObstruction.IncidenceTemplate.(instance at line 102) line 102
  6. def OAI.HyperbolicObstruction.IncidenceTemplate.pointOfRepresentative line 105

    Source documentation

    X representatives occupy 0,...,6 and the four Y representatives 7,...,10.

    def pointOfRepresentative (r : Fin 11) : Fin 7 :=
…
  7. abbrev OAI.HyperbolicObstruction.CoreGeometry.Vertex line 111
  8. instance OAI.HyperbolicObstruction.CoreGeometry.(instance at line 112) line 112
  9. def OAI.HyperbolicObstruction.CoreGeometry.Adjacent line 114
  10. instance OAI.HyperbolicObstruction.CoreGeometry.(instance at line 118) line 118
  11. def OAI.HyperbolicObstruction.CoreGeometry.Opposite line 121
  12. instance OAI.HyperbolicObstruction.CoreGeometry.(instance at line 125) line 125
  13. structure OAI.HyperbolicObstruction.CoreGeometry.HexagonCode line 128
  14. def OAI.HyperbolicObstruction.CoreGeometry.HexagonCode.vertices line 136
  15. def OAI.HyperbolicObstruction.CoreGeometry.Valid line 139
  16. instance OAI.HyperbolicObstruction.CoreGeometry.(instance at line 143) line 143
  17. def OAI.HyperbolicObstruction.CoreGeometry.centerPair line 146
  18. def OAI.HyperbolicObstruction.CoreGeometry.centerParent line 149
  19. def OAI.HyperbolicObstruction.CoreGeometry.centerHex line 152
  20. def OAI.HyperbolicObstruction.CoreGeometry.pointIndex line 155
  21. def OAI.HyperbolicObstruction.CoreGeometry.lineIndex line 158
  22. def OAI.HyperbolicObstruction.CoreGeometry.lineHex line 161
  23. lemma OAI.HyperbolicObstruction.CoreGeometry.centerHex_valid line 165
  24. lemma OAI.HyperbolicObstruction.CoreGeometry.centerHex_pair line 168
  25. lemma OAI.HyperbolicObstruction.CoreGeometry.centerHex_parent line 172
  26. lemma OAI.HyperbolicObstruction.CoreGeometry.centerPair_complete line 177
  27. lemma OAI.HyperbolicObstruction.CoreGeometry.pointIndex_correct line 181
  28. lemma OAI.HyperbolicObstruction.CoreGeometry.lineIndex_correct line 182
  29. lemma OAI.HyperbolicObstruction.CoreGeometry.lineHex_valid line 184
  30. lemma OAI.HyperbolicObstruction.CoreGeometry.lineHex_coordinates line 187
  31. def OAI.HyperbolicObstruction.CoreGeometry.InFan line 202

    Source documentation

    Membership of an (unoriented) core edge in the fan over i. Adjacency is imposed separately. The exceptional loose edge belongs to no fan.

    def InFan (i : Fin 7) : Vertex → Vertex → Prop
  | .inl r, .inr l => pointOfRepresentative r = i ∧ (r,l) ≠ (3,4)
  | .inr l, .inl r => pointOfRepresentative r = i ∧ (r,l) ≠ (3,4)
  | _, _ => False

    Mentions: OAI.HyperbolicObstruction.CoreGeometry.Vertex

  32. instance OAI.HyperbolicObstruction.CoreGeometry.(instance at line 207) line 207
  33. lemma OAI.HyperbolicObstruction.CoreGeometry.Adjacent.symm line 210
  34. lemma OAI.HyperbolicObstruction.CoreGeometry.Opposite.symm line 213
  35. lemma OAI.HyperbolicObstruction.CoreGeometry.Adjacent.not_opposite line 216
  36. def OAI.HyperbolicObstruction.CoreGeometry.ThreeQuota line 221

    Source documentation

    The three-edge fan quota, expressed without choosing an orientation for its fields. With distinct successive fields this says at most two per fan.

    def ThreeQuota (a b c d : Vertex) : Prop :=
…

    Mentions: OAI.HyperbolicObstruction.CoreGeometry.Vertex

  37. instance OAI.HyperbolicObstruction.CoreGeometry.(instance at line 224) line 224
  38. lemma OAI.HyperbolicObstruction.CoreGeometry.threeQuota_of_opposite line 227
  39. structure OAI.HyperbolicObstruction.CoreGeometry.MetricCore line 238

    Source documentation

    Exactly the core path distances in Proposition configuration (i). The third condition uses distinct fields and the actual fan quota; the exceptional loose edge is not charged to the D fan.

    structure MetricCore {X : Type*} [MetricSpace X] (z : Vertex → X) : Prop where
…

    Mentions: OAI.HyperbolicObstruction.CoreGeometry.Vertex

  40. theorem OAI.HyperbolicObstruction.CoreGeometry.MetricCore.three_of_opposite line 249
  41. theorem OAI.HyperbolicObstruction.CoreGeometry.MetricCore.hexagon line 261
  42. def OAI.HyperbolicObstruction.CoreGeometry.MetricCore.center line 276

    Source documentation

    A fixed actual opposite pair defines the common center.

    def center (h : CATZero X) : X := CATZero.mid h (z (.inl 0)) (z (.inr 0))

    Mentions: OAI.HyperbolicObstruction.CATZero, OAI.HyperbolicObstruction.CATZero.mid

  43. theorem OAI.HyperbolicObstruction.CoreGeometry.MetricCore.centerPairs line 278
  44. theorem OAI.HyperbolicObstruction.CoreGeometry.MetricCore.hexagon_center line 293
  45. theorem OAI.HyperbolicObstruction.CoreGeometry.MetricCore.radius_point line 302
  46. theorem OAI.HyperbolicObstruction.CoreGeometry.MetricCore.radius_line line 312
  47. theorem OAI.HyperbolicObstruction.CoreGeometry.MetricCore.line_dist line 322
  48. theorem OAI.HyperbolicObstruction.CoreGeometry.MetricCore.line_flat line 330
  49. def OAI.HyperbolicObstruction.CoreGeometry.xRep line 351
  50. def OAI.HyperbolicObstruction.CoreGeometry.yRep line 352
  51. def OAI.HyperbolicObstruction.CoreGeometry.sixLine line 354

    Source documentation

    AB, AC, AD, BC, BD, CD in the fixed linear-functional indexing.

    def sixLine : Fin 6 → Fin 7 := ![2,1,6,0,5,4]
  52. lemma OAI.HyperbolicObstruction.CoreGeometry.sixLine_injective line 356
  53. lemma OAI.HyperbolicObstruction.CoreGeometry.xy_distinct line 357
  54. lemma OAI.HyperbolicObstruction.CoreGeometry.fullLines_x line 358
  55. lemma OAI.HyperbolicObstruction.CoreGeometry.fullLines_y line 361
  56. def OAI.HyperbolicObstruction.CoreGeometry.ExceptionalTest line 367

    Source documentation

    The three-field, two-fractional-geodesic inequality in the source's configuration proposition, at the exceptional missing incidence.

    def ExceptionalTest {X : Type*} [MetricSpace X] (h : CATZero X) (z : Vertex → X) : Prop :=
…

    Mentions: OAI.HyperbolicObstruction.CATZero, OAI.HyperbolicObstruction.CoreGeometry.Vertex

  57. def OAI.HyperbolicObstruction.CoreGeometry.MetricCore.toObstruction line 378

    Source documentation

    Assemble the source's actual graph configuration, rather than assuming common centers or tangent-cone distances, into the proved obstruction.

    def toObstruction (h : CATZero X) (he : ExceptionalTest h z) : FiniteObstructionData h where
…

    Mentions: OAI.HyperbolicObstruction.CATZero, OAI.HyperbolicObstruction.CoreGeometry.ExceptionalTest, OAI.HyperbolicObstruction.FiniteObstructionData

  58. theorem OAI.HyperbolicObstruction.CoreGeometry.MetricCore.impossible line 409

    Source documentation

    No CAT(0) space contains the exact limiting core configuration of Proposition configuration, including its exceptional fractional test.

    theorem impossible (h : CATZero X) (he : ExceptionalTest h z) : False :=
…

    Mentions: OAI.HyperbolicObstruction.CATZero, OAI.HyperbolicObstruction.CoreGeometry.ExceptionalTest

  59. structure OAI.HyperbolicObstruction.MetricScale.Space line 422
  60. instance OAI.HyperbolicObstruction.MetricScale.(instance at line 427) line 427
  61. lemma OAI.HyperbolicObstruction.MetricScale.dist_eq line 438
  62. theorem OAI.HyperbolicObstruction.MetricScale.catZero line 443
  63. lemma OAI.HyperbolicObstruction.MetricScale.val_segment line 461