CATZero.lean`

64 declarations, 0 contain sorry, 0 declared as axioms

def OAI.HyperbolicObstruction.CATZero.segment line 18
Source documentation
The comparison segment chosen from the CAT(0) comparison condition.
```
def segment (h : CATZero X) (x y : X) : ℝ → X := (h x y).choose
```
Mentions: OAI.HyperbolicObstruction.CATZero
theorem OAI.HyperbolicObstruction.CATZero.segment_spec line 20
theorem OAI.HyperbolicObstruction.CATZero.segment_cn line 23
theorem OAI.HyperbolicObstruction.CATZero.segment_left line 29
theorem OAI.HyperbolicObstruction.CATZero.segment_right line 36
theorem OAI.HyperbolicObstruction.CATZero.eq_segment_of_dist line 46
Source documentation
CAT(0) comparison applies to any point with the prescribed division distances, rather than just to the initially chosen segment.
```
theorem eq_segment_of_dist (h : CATZero X) {x y p : X} {t : ℝ}
    (ht : t ∈ Set.Icc (0 : ℝ) 1)
    (hx : dist x p = t * dist x y)
    (hy : dist p y = (1 - t) * dist x y) :
    p = segment h x y t := by
…
```
Mentions: OAI.HyperbolicObstruction.CATZero, OAI.HyperbolicObstruction.CATZero.segment
theorem OAI.HyperbolicObstruction.CATZero.cn_of_dist line 57
def OAI.HyperbolicObstruction.CATZero.mid line 67
Source documentation
Metric midpoint, available without completeness or properness.
```
def mid (h : CATZero X) (x y : X) : X := segment h x y (1 / 2)
```
Mentions: OAI.HyperbolicObstruction.CATZero, OAI.HyperbolicObstruction.CATZero.segment
theorem OAI.HyperbolicObstruction.CATZero.dist_left_mid line 69
theorem OAI.HyperbolicObstruction.CATZero.dist_mid_right line 73
theorem OAI.HyperbolicObstruction.CATZero.mid_cn line 79
theorem OAI.HyperbolicObstruction.CATZero.quadrilateral line 87
Source documentation
Source Lemma energy:quadrilateral, with its midpoint error retained.
```
theorem quadrilateral (h : CATZero X) (a b c d : X) :
    dist a c ^ 2 + dist b d ^ 2 + 4 * dist (mid h a c) (mid h b d) ^ 2 ≤
      dist a b ^ 2 + dist b c ^ 2 + dist c d ^ 2 + dist d a ^ 2 := by
…
```
Mentions: OAI.HyperbolicObstruction.CATZero, OAI.HyperbolicObstruction.CATZero.mid
structure OAI.HyperbolicObstruction.ConeData line 106
Source documentation
The metric description of nonnegative radial dilations in a Euclidean cone, with the angular cosine eliminated by polarization. No linear or associative addition is included.
```
structure ConeData (X : Type*) [MetricSpace X] where
…
```
def OAI.HyperbolicObstruction.ConeData.normSq line 119
def OAI.HyperbolicObstruction.ConeData.pairing line 121
theorem OAI.HyperbolicObstruction.ConeData.normSq_nonneg line 123
theorem OAI.HyperbolicObstruction.ConeData.pairing_comm line 125
theorem OAI.HyperbolicObstruction.ConeData.pairing_self line 129
theorem OAI.HyperbolicObstruction.ConeData.normSq_vertex line 132
theorem OAI.HyperbolicObstruction.ConeData.pairing_vertex line 134
theorem OAI.HyperbolicObstruction.ConeData.dist_sq line 137
theorem OAI.HyperbolicObstruction.ConeData.normSq_scale line 142
theorem OAI.HyperbolicObstruction.ConeData.pairing_scale line 147
theorem OAI.HyperbolicObstruction.ConeData.pairing_scale_left line 154
theorem OAI.HyperbolicObstruction.ConeData.pairing_scale_right line 158
theorem OAI.HyperbolicObstruction.ConeData.normSq_segment line 165
Source documentation
In a CAT(0) Euclidean cone, comparison towards the vertex is an equality. The reverse bound is obtained by comparing towards twice the division point; no flat-sector theorem is assumed.
```
theorem normSq_segment (h : CATZero X) (x y : X) {t : ℝ}
    (ht : t ∈ Set.Icc (0 : ℝ) 1) :
    T.normSq (CATZero.segment h x y t) =
      (1 - t) * T.normSq x + t * T.normSq y - t * (1 - t) * dist x y ^ 2 := by
…
```
Mentions: OAI.HyperbolicObstruction.CATZero, OAI.HyperbolicObstruction.CATZero.segment
theorem OAI.HyperbolicObstruction.ConeData.normSq_eq_zero line 190
theorem OAI.HyperbolicObstruction.ConeData.scale_vertex line 193
theorem OAI.HyperbolicObstruction.ConeData.scale_mul line 198
theorem OAI.HyperbolicObstruction.ConeData.pairing_segment line 208
Source documentation
Scalar-product concavity, derived directly from CN and radial equality.
```
theorem pairing_segment (h : CATZero X) (w x y : X) {t : ℝ}
    (ht : t ∈ Set.Icc (0 : ℝ) 1) :
    (1 - t) * T.pairing w x + t * T.pairing w y ≤
      T.pairing w (CATZero.segment h x y t) := by
…
```
Mentions: OAI.HyperbolicObstruction.CATZero, OAI.HyperbolicObstruction.CATZero.segment
def OAI.HyperbolicObstruction.ConeData.add line 218
Source documentation
The manuscript's two-vector cone addition (not an associative operation).
```
def add (h : CATZero X) (x y : X) : X := T.scale 2 (CATZero.mid h x y)
```
Mentions: OAI.HyperbolicObstruction.CATZero, OAI.HyperbolicObstruction.CATZero.mid
theorem OAI.HyperbolicObstruction.ConeData.normSq_mid line 220
theorem OAI.HyperbolicObstruction.ConeData.normSq_add line 227
theorem OAI.HyperbolicObstruction.ConeData.pairing_add_left line 233
theorem OAI.HyperbolicObstruction.ConeData.pairing_add_right line 241
theorem OAI.HyperbolicObstruction.ConeData.pairing_add line 250
Source documentation
Source Equation geom:sum-concavity.
```
theorem pairing_add (h : CATZero X) (w x y : X) :
    T.pairing w x + T.pairing w y ≤ T.pairing w (T.add h x y) := by
…
```
Mentions: OAI.HyperbolicObstruction.CATZero
theorem OAI.HyperbolicObstruction.ConeData.add_antipodes line 260
Source documentation
Normalized antipodal vectors sum to the cone vertex.
```
theorem add_antipodes (h : CATZero X) {c d : X}
    (hc : T.normSq c = 1) (hd : T.normSq d = 1)
    (hcd : T.pairing c d = -1) : T.add h c d = T.vertex := by
…
```
Mentions: OAI.HyperbolicObstruction.CATZero

theorem OAI.HyperbolicObstruction.ConeData.antipodal_pairing line 268

Source documentation

The polar inequality of an isometrically embedded line.

theorem antipodal_pairing (h : CATZero X) {c d : X}
    (hc : T.normSq c = 1) (hd : T.normSq d = 1)
    (hcd : T.pairing c d = -1) (x : X) :
    T.pairing c x + T.pairing d x ≤ 0 := by
…

Mentions: OAI.HyperbolicObstruction.CATZero

theorem OAI.HyperbolicObstruction.ConeData.add_vertex line 278
def OAI.HyperbolicObstruction.ConeData.Opposite line 290
Source documentation
Equal-length opposite points of a cone. The zero pair is permitted.
```
def Opposite (c d : X) : Prop :=
…
```
theorem OAI.HyperbolicObstruction.ConeData.Opposite.symm line 293
theorem OAI.HyperbolicObstruction.ConeData.add_opposite line 297
theorem OAI.HyperbolicObstruction.ConeData.opposite_pairing line 303
def OAI.HyperbolicObstruction.ConeData.Parallel line 312
Source documentation
The zero set of the sum of the two Busemann coordinates of an axis. All splitting identities used below are proved from CN, not assumed.
```
def Parallel (c d x : X) : Prop := T.pairing c x + T.pairing d x = 0
```
theorem OAI.HyperbolicObstruction.ConeData.Parallel.symm line 314
def OAI.HyperbolicObstruction.ConeData.translate line 318
theorem OAI.HyperbolicObstruction.ConeData.normSq_translate line 321
theorem OAI.HyperbolicObstruction.ConeData.pairing_translate_base line 329
theorem OAI.HyperbolicObstruction.ConeData.pairing_translate_axis line 334
theorem OAI.HyperbolicObstruction.ConeData.pairing_translate_ge line 345
theorem OAI.HyperbolicObstruction.ConeData.parallel_translate line 351
Source documentation
Translating towards either end of an axis preserves its parallel set.
```
theorem parallel_translate (h : CATZero X) {c d x : X} (hop : T.Opposite c d)
    (hx : T.Parallel c d x) {t : ℝ} (ht : 0 ≤ t) :
    T.Parallel c d (T.translate h c t x) := by
…
```
Mentions: OAI.HyperbolicObstruction.CATZero

theorem OAI.HyperbolicObstruction.ConeData.translate_inverse line 362

Source documentation

The two cone translations are inverse on the parallel set.

theorem translate_inverse (h : CATZero X) {c d x : X} (hop : T.Opposite c d)
    (hx : T.Parallel c d x) {t : ℝ} (ht : 0 ≤ t) :
    T.translate h d t (T.translate h c t x) = x := by
…

Mentions: OAI.HyperbolicObstruction.CATZero

theorem OAI.HyperbolicObstruction.ConeData.pairing_translate line 383
Source documentation
Exact scalar-product translation formula on the parallel set. It is the needed parallel-set splitting identity, proved without a product theorem.
```
theorem pairing_translate (h : CATZero X) {c d x y : X} (hop : T.Opposite c d)
    (hx : T.Parallel c d x) (hy : T.Parallel c d y) {t : ℝ} (ht : 0 ≤ t) :
    T.pairing x (T.translate h c t y) = T.pairing x y + t * T.pairing c x := by
…
```
Mentions: OAI.HyperbolicObstruction.CATZero
theorem OAI.HyperbolicObstruction.ConeData.add_comm line 394
theorem OAI.HyperbolicObstruction.ConeData.pairing_translates_same line 404
theorem OAI.HyperbolicObstruction.ConeData.pairing_translates_opposite line 415

theorem OAI.HyperbolicObstruction.ConeData.opposite_add_of_orthogonal line 431

Source documentation

Opposite orthogonal pairs have opposite cone sums. This is a small flat-square rigidity statement, using the proved translation identity.

theorem opposite_add_of_orthogonal (h : CATZero X) {u u' v v' : X}
    (hu : T.Opposite u u') (hv : T.Opposite v v')
    (huv : T.pairing u v = 0) (huv' : T.pairing u v' = 0)
    (hu'v : T.pairing u' v = 0) (hu'v' : T.pairing u' v' = 0) :
    T.Opposite (T.add h u v) (T.add h u' v') := by
…

Mentions: OAI.HyperbolicObstruction.CATZero

theorem OAI.HyperbolicObstruction.ConeData.pairing_unit_lower line 449
Source documentation
Unit vectors satisfy the lower Cauchy bound without any ambient linear structure. This is just the triangle inequality of the cone.
```
theorem pairing_unit_lower {x y : X} (hx : T.normSq x = 1) (hy : T.normSq y = 1) :
    -1 ≤ T.pairing x y := by
…
```
theorem OAI.HyperbolicObstruction.ConeData.exceptional_antipodes line 465
Source documentation
Source Lemma geom:antipodal, in an algebraic form that avoids a local-to-global theorem in the completed space of directions.
```
theorem exceptional_antipodes (h : CATZero X) {c d x y z : X}
    (hc : T.normSq c = 1) (hd : T.normSq d = 1)
    (hdy : T.pairing d y = 1 / 2) (hdx : T.pairing d x = 1 / 2)
    (hyz : T.Opposite y z) (hz : z = T.add h c x) : T.Opposite c d := by
…
```
Mentions: OAI.HyperbolicObstruction.CATZero
theorem OAI.HyperbolicObstruction.ConeData.eq_of_normSq_pairing line 480
theorem OAI.HyperbolicObstruction.ConeData.pairing_add_add line 487
theorem OAI.HyperbolicObstruction.ConeData.add_eq_of_pairings line 497

theorem OAI.HyperbolicObstruction.ConeData.opposite_cross_sums line 506

Source documentation

The transverse-square conclusion used in the final obstruction. The four original vectors are not assumed to lie in a plane or a vector space.

theorem opposite_cross_sums (h : CATZero X) {p q r s : X}
    (hnp : T.normSq p = 3 / 4) (hnq : T.normSq q = 3 / 4)
    (hnr : T.normSq r = 3 / 4) (hns : T.normSq s = 3 / 4)
    (hpq : T.pairing p q = -1 / 4) (hpr : T.pairing p r = -1 / 4)
    (hps : T.pairing p s = -1 / 4) (hqr : T.pairing q r = -1 / 4)
    (hqs : T.pairing q s = -1 / 4) (hrs : T.pairing r s = -1 / 4)
    (hop : T.Opposite (T.add h p q) (T.add h r s)) :
    T.Opposite (T.add h p r) (T.add h q s) := by
…

Mentions: OAI.HyperbolicObstruction.CATZero

theorem OAI.HyperbolicObstruction.ConeData.five_line_fans_contradiction line 646

Source documentation

Final algebraic contradiction in Proposition prop:no-configuration. The five line indices are AB, AC, AD, BC, BD, respectively. All geometric input here is explicit; no Hilbert-space or associativity assumption is used.

theorem five_line_fans_contradiction (h : CATZero X) (ℓ : Fin 5 → X)
    (hn : ∀ i, T.normSq (ℓ i) = 3 / 4)
    (hp : ∀ i j, i ≠ j → T.pairing (ℓ i) (ℓ j) = -1 / 4)
    (hA : T.add h (ℓ 0) (ℓ 1) = T.add h (ℓ 1) (ℓ 2))
    (hB : T.add h (ℓ 0) (ℓ 3) = T.add h (ℓ 3) (ℓ 4))
    (hop : T.Opposite (T.add h (ℓ 1) (ℓ 3)) (T.add h (ℓ 2) (ℓ 4))) : False := by
…

Mentions: OAI.HyperbolicObstruction.CATZero