CATZeroFurther.lean`

15 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.HyperbolicObstruction.CATZero.square_mid line 28

Source documentation

The midpoint part of square rigidity, retaining just the metric data needed later.

theorem square_mid (h : CATZero X) {p q r s : X}
    (hpq : dist p q ^ 2 = 1) (hqr : dist q r ^ 2 = 1)
    (hrs : dist r s ^ 2 = 1) (hsp : dist s p ^ 2 = 1)
    (hpr : dist p r ^ 2 = 2) (hqs : dist q s ^ 2 = 2) :
    mid h p r = mid h q s := by
…

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

theorem OAI.HyperbolicObstruction.TangentCone.cn_eq_of_log_dist line 44
Source documentation
A log-isometric base gives every radial CN equality, directly from the constructed cone metric law and uniqueness of segments.
```
theorem cn_eq_of_log_dist (o x y : X)
    (he : dist (log h o x) (log h o y) = dist x y) {t : ℝ}
    (ht : t ∈ Set.Icc (0 : ℝ) 1) :
    dist o (CATZero.segment h x y t) ^ 2 =
      (1 - t) * dist o x ^ 2 + t * dist o y ^ 2 - t * (1 - t) * dist x y ^ 2 := by
…
```
Mentions: OAI.HyperbolicObstruction.TangentCone.log, OAI.HyperbolicObstruction.CATZero.segment

theorem OAI.HyperbolicObstruction.TangentCone.fan_identity line 57

Source documentation

The fan midpoint identity, derived from a metric square and the central flatness of its line diagonal.

theorem fan_identity (c x y a b : X)
    (hcx : dist c x ^ 2 = 3 / 4) (hcy : dist c y ^ 2 = 3 / 4)
    (hca : dist c a ^ 2 = 3 / 4) (hcb : dist c b ^ 2 = 3 / 4)
    (hxa : dist x a ^ 2 = 1) (hay : dist a y ^ 2 = 1)
    (hyb : dist y b ^ 2 = 1) (hbx : dist b x ^ 2 = 1)
    (hxy : dist x y ^ 2 = 2) (hab : dist a b ^ 2 = 2)
    (hflat : dist c (CATZero.mid h a b) ^ 2 = 1 / 4) :
    (coneData h c).pairing (log h c x) (log h c y) = -1 / 4 ∧
    (coneData h c).add (catZero h c) (log h c x) (log h c y) =
      (coneData h c).add (catZero h c) (log h c a) (log h c b) := by
…

Mentions: OAI.HyperbolicObstruction.CATZero.mid, OAI.HyperbolicObstruction.TangentCone.coneData, OAI.HyperbolicObstruction.TangentCone.log, OAI.HyperbolicObstruction.TangentCone.catZero

theorem OAI.HyperbolicObstruction.TangentCone.exceptional_identity line 86

Source documentation

Source exceptional-incidence identity. Its hypotheses are entirely metric, including the fixed-fraction test; no flat triangle or cone identity is assumed.

theorem exceptional_identity (c p q z k : X)
    (hcp : dist c p ^ 2 = 3 / 4) (hcq : dist c q ^ 2 = 3 / 4)
    (hcz : dist c z ^ 2 = 3 / 4) (hck : dist c k ^ 2 = 3 / 4)
    (hpq : dist p q ^ 2 = 2) (hpz : dist p z ^ 2 = 2) (hqz : dist q z ^ 2 = 2)
    (hcj : dist c (CATZero.mid h p q) ^ 2 = 1 / 4)
    (hkj : dist k (CATZero.mid h p q) ^ 2 = 1 / 2) (hkz : dist k z ^ 2 = 1)
    (hfrac : ∀ t ∈ Set.Ioc (0 : ℝ) 1,
      t ^ 2 * (1 / 2 + 1) ≤ dist (CATZero.segment h k (CATZero.mid h p q) t)
        (CATZero.segment h k z t) ^ 2) :
    log h c k = (coneData h c).add (catZero h c)
      ((coneData h c).add (catZero h c) (log h c p) (log h c q)) (log h c z) := by
…

Mentions: OAI.HyperbolicObstruction.CATZero.mid, OAI.HyperbolicObstruction.CATZero.segment, OAI.HyperbolicObstruction.TangentCone.log, OAI.HyperbolicObstruction.TangentCone.coneData, OAI.HyperbolicObstruction.TangentCone.catZero

structure OAI.HyperbolicObstruction.MetricSquare line 168
Source documentation
Squared metric data for the unit square, in cyclic order.
```
structure MetricSquare {X : Type*} [MetricSpace X] (p q r s : X) : Prop where
…
```
theorem OAI.HyperbolicObstruction.MetricSquare.mid_eq line 176
def OAI.HyperbolicObstruction.fullLines line 182
Source documentation
Full incidences among the six lines AB, AC, AD, BC, BD, CD at A,B,C,D. These are exactly the doubled fans of the source.
```
def fullLines : Fin 4 → Finset (Fin 6) :=
…
```
structure OAI.HyperbolicObstruction.FiniteObstructionData line 189
Source documentation
The specific subconfiguration used by the source obstruction. This is metric input to a contradiction, not an assumed existence assertion. All its conditions are consequences asserted by source Proposition configuration; the existence-from-actions direction remains a separate obligation.
```
structure FiniteObstructionData {X : Type*} [MetricSpace X] (h : CATZero X) where
…
```
Mentions: OAI.HyperbolicObstruction.CATZero
theorem OAI.HyperbolicObstruction.no_finite_obstruction line 212
Source documentation
The complete finite CAT(0) metric obstruction from Section 6. The proof constructs the completed tangent cone and all rigidity identities internally.
```
theorem no_finite_obstruction {X : Type*} [MetricSpace X] (h : CATZero X)
    (D : FiniteObstructionData h) : False := by
…
```
Mentions: OAI.HyperbolicObstruction.CATZero, OAI.HyperbolicObstruction.FiniteObstructionData
theorem OAI.HyperbolicObstruction.CATZero.radialPairing_endpoint_gap line 310
Source documentation
The elementary endpoint estimate behind first variation: fixing one radial endpoint changes a comparison product by at most a first-order error. It follows from the triangle inequality and convexity of the real square.
```
theorem radialPairing_endpoint_gap (h : CATZero X) (o x y : X) {a b : ℝ}
    (ha : a ∈ Set.Ioc (0 : ℝ) 1) (hb : b ∈ Set.Ioc (0 : ℝ) 1) :
    2 * b * (radialPairing h o x y a b - radialPairing h o x y a 1) ≤
      a * dist o x ^ 2 := by
…
```
Mentions: OAI.HyperbolicObstruction.CATZero, OAI.HyperbolicObstruction.CATZero.radialPairing
theorem OAI.HyperbolicObstruction.CATZero.radialPairing_endpoint_tendsto line 342
Source documentation
First-variation comparison product along a quadratic radial parameter. This suffices for the minimizer argument and avoids any assumed angle theorem.
```
theorem radialPairing_endpoint_tendsto (h : CATZero X) (o x y : X) :
    Tendsto (fun t : ℝ => radialPairing h o x y (t ^ 2) 1) (𝓝[>] 0)
      (𝓝 (tangentPairing h o x y)) := by
…
```
Mentions: OAI.HyperbolicObstruction.CATZero, OAI.HyperbolicObstruction.CATZero.radialPairing, OAI.HyperbolicObstruction.CATZero.tangentPairing
theorem OAI.HyperbolicObstruction.CATZero.tangentPairing_sum_nonpos_of_minimum line 376
Source documentation
A finite squared-distance minimizer has nonpositive directional product sum. The proof uses the actual comparison-product limit, not first variation as an imported hypothesis.
```
theorem tangentPairing_sum_nonpos_of_minimum (h : CATZero X) (o : X) (y : ι → X)
    (hmin : ∀ x : X, (∑ i, dist o (y i) ^ 2) ≤ ∑ i, dist x (y i) ^ 2) (z : X) :
    (∑ i, tangentPairing h o z (y i)) ≤ 0 := by
…
```
Mentions: OAI.HyperbolicObstruction.CATZero, OAI.HyperbolicObstruction.CATZero.tangentPairing
theorem OAI.HyperbolicObstruction.TangentCone.pairing_ray_log line 418
theorem OAI.HyperbolicObstruction.TangentCone.pairing_sum_nonpos_of_minimum line 431
Source documentation
The tangent barycenter inequality at an actual finite squared-distance minimizer, extended to the completed cone by density.
```
theorem pairing_sum_nonpos_of_minimum {ι : Type*} [Fintype ι] (y : ι → X)
    (hmin : ∀ x : X, (∑ i, dist o (y i) ^ 2) ≤ ∑ i, dist x (y i) ^ 2)
    (v : TangentCone h o) : (∑ i, (coneData h o).pairing v (log h o (y i))) ≤ 0 := by
…
```
Mentions: OAI.HyperbolicObstruction.TangentCone, OAI.HyperbolicObstruction.TangentCone.coneData, OAI.HyperbolicObstruction.TangentCone.log

theorem OAI.HyperbolicObstruction.TangentCone.variance_of_minimum line 446

Source documentation

Variance form of the zero tangent barycenter.

theorem variance_of_minimum {ι : Type*} [Fintype ι] (y : ι → X)
    (hmin : ∀ x : X, (∑ i, dist o (y i) ^ 2) ≤ ∑ i, dist x (y i) ^ 2)
    (v : TangentCone h o) :
    (Fintype.card ι : ℝ) * (coneData h o).normSq v + (∑ i, dist o (y i) ^ 2) ≤
      ∑ i, dist v (log h o (y i)) ^ 2 := by
…

Mentions: OAI.HyperbolicObstruction.TangentCone, OAI.HyperbolicObstruction.TangentCone.coneData, OAI.HyperbolicObstruction.TangentCone.log