structure AffineBuilding.GeodesicSegment {V : Type u_1} [DecidableEq V] (b : Building V) (md : ApartmentMetricData b) (x y : V) : Type u_1

A geodesic segment in a building from $x$ to $y$: a set of points characterised by satisfying the parametrised distance equations $d(p, x) = (1-t) d(x, y)$ and $d(p, y) = t d(x, y)$ for some $t \in [0, 1]$, together with completeness (every such point is included).

• points : Set V
• endpoints : x ∈ self.points ∧ y ∈ self.points
• dist_characterization (p : V) : p ∈ self.points → ∃ (t : ℝ), 0 ≤ t ∧ t ≤ 1 ∧ buildingDist b md p x = (1 - t) * buildingDist b md x y ∧ buildingDist b md p y = t * buildingDist b md x y
• complete (p : V) : (∃ (t : ℝ), 0 ≤ t ∧ t ≤ 1 ∧ buildingDist b md p x = (1 - t) * buildingDist b md x y ∧ buildingDist b md p y = t * buildingDist b md x y) → p ∈ self.points

theorem AffineBuilding.buildingDist_nonneg {V : Type u_1} [DecidableEq V] (b : Building V) (md : ApartmentMetricData b) (x y : V) : 0 ≤ buildingDist b md x y

The building distance is non-negative.

theorem AffineBuilding.buildingDist_eq_dist_fn {V : Type u_1} [DecidableEq V] (b : Building V) (md : ApartmentMetricData b) (A : { A : SimplicialComplex V // A ∈ b.apartmentSystem.apartments }) (u v : V) (huA : ∃ s ∈ (↑A).faces, u ∈ s) (hvA : ∃ s ∈ (↑A).faces, v ∈ s) : buildingDist b md u v = md.dist_fn A u v

The building distance between two vertices that lie in a common apartment $A$ equals the apartment distance computed in $A$.

def AffineBuilding.NegCurvatureIneq {V : Type u_1} [DecidableEq V] (b : Building V) (md : ApartmentMetricData b) : Prop

The CAT(0) negative-curvature inequality: for any point $z$ and any geodesic parametrisation $z_t = (1-t) x + t y$ (in terms of the building distance), $d(z, z_t)^2 \le t\, d(z, x)^2 + (1-t)\, d(z, y)^2 - t(1-t)\, d(x, y)^2$.

theorem AffineBuilding.euclidean_identity_ips {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (x y : E) (t : ℝ) : ‖t • x + (1 - t) • y‖ ^ 2 = t * ‖x‖ ^ 2 + (1 - t) * ‖y‖ ^ 2 - t * (1 - t) * ‖x - y‖ ^ 2

Parallelogram-style identity in a real inner product space: for $x, y \in E$ and $t \in \mathbb{R}$, $\|t x + (1-t) y\|^2 = t \|x\|^2 + (1-t) \|y\|^2 - t(1-t) \|x-y\|^2$.

theorem AffineBuilding.euclidean_identity_origin_shifted {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (q x y z_t : E) (t : ℝ) (h_zt : z_t = t • x + (1 - t) • y) : ‖q - z_t‖ ^ 2 = t * ‖q - x‖ ^ 2 + (1 - t) * ‖q - y‖ ^ 2 - t * (1 - t) * ‖x - y‖ ^ 2

Origin-shifted Euclidean identity: for $z_t = t x + (1-t) y$ and any base point $q$, $\|q - z_t\|^2 = t \|q - x\|^2 + (1-t) \|q - y\|^2 - t(1-t)\|x-y\|^2$.

theorem AffineBuilding.euclidean_identity_in_apartment {V : Type u_1} [DecidableEq V] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (b : Building V) (md : ApartmentMetricData b) (coord : { A : SimplicialComplex V // A ∈ b.apartmentSystem.apartments } → V → E) (dist_eq_norm : ∀ (A : { A : SimplicialComplex V // A ∈ b.apartmentSystem.apartments }) (u v : V), md.dist_fn A u v = ‖coord A u - coord A v‖) (coord_geodesic : ∀ (A : { A : SimplicialComplex V // A ∈ b.apartmentSystem.apartments }) (x y z_t : V) (t : ℝ), (∃ s ∈ (↑A).faces, x ∈ s) → (∃ s ∈ (↑A).faces, y ∈ s) → (∃ s ∈ (↑A).faces, z_t ∈ s) → md.dist_fn A z_t x = (1 - t) * md.dist_fn A x y → md.dist_fn A z_t y = t * md.dist_fn A x y → coord A z_t = t • coord A x + (1 - t) • coord A y) (x y q z_t : V) (t : ℝ) (_ht0 : 0 ≤ t) (_ht1 : t ≤ 1) (hzt_x : buildingDist b md z_t x = (1 - t) * buildingDist b md x y) (hzt_y : buildingDist b md z_t y = t * buildingDist b md x y) (A : { A : SimplicialComplex V // A ∈ b.apartmentSystem.apartments }) (hqA : ∃ s ∈ (↑A).faces, q ∈ s) (hxA : ∃ s ∈ (↑A).faces, x ∈ s) (hyA : ∃ s ∈ (↑A).faces, y ∈ s) (hztA : ∃ s ∈ (↑A).faces, z_t ∈ s) : buildingDist b md q z_t ^ 2 = t * buildingDist b md q x ^ 2 + (1 - t) * buildingDist b md q y ^ 2 - t * (1 - t) * buildingDist b md x y ^ 2

Within a single apartment $A$ realised as Euclidean space $E$, the CAT(0) identity becomes an equality (not just inequality): the geodesic point $z_t = t x + (1-t) y$ satisfies the parallelogram identity with the building distance.

theorem AffineBuilding.negCurvatureIneq {V : Type u_1} [DecidableEq V] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (b : Building V) (md : ApartmentMetricData b) (coord : { A : SimplicialComplex V // A ∈ b.apartmentSystem.apartments } → V → E) (dist_eq_norm : ∀ (A : { A : SimplicialComplex V // A ∈ b.apartmentSystem.apartments }) (u v : V), md.dist_fn A u v = ‖coord A u - coord A v‖) (coord_geodesic : ∀ (A : { A : SimplicialComplex V // A ∈ b.apartmentSystem.apartments }) (x y z_t : V) (t : ℝ), (∃ s ∈ (↑A).faces, x ∈ s) → (∃ s ∈ (↑A).faces, y ∈ s) → (∃ s ∈ (↑A).faces, z_t ∈ s) → md.dist_fn A z_t x = (1 - t) * md.dist_fn A x y → md.dist_fn A z_t y = t * md.dist_fn A x y → coord A z_t = t • coord A x + (1 - t) • coord A y) (retract_exists : ∀ (x y z z_t : V), ∃ (ρ : V → V) (A : { A : SimplicialComplex V // A ∈ b.apartmentSystem.apartments }), (∃ s ∈ (↑A).faces, x ∈ s) ∧ (∃ s ∈ (↑A).faces, y ∈ s) ∧ (∃ s ∈ (↑A).faces, ρ z ∈ s) ∧ ρ x = x ∧ ρ y = y ∧ (∀ (u v : V), buildingDist b md (ρ u) (ρ v) ≤ buildingDist b md u v) ∧ buildingDist b md z z_t = buildingDist b md (ρ z) z_t) (zt_in_apt : ∀ (x y z_t : V) (t : ℝ), 0 ≤ t → t ≤ 1 → buildingDist b md z_t x = (1 - t) * buildingDist b md x y → buildingDist b md z_t y = t * buildingDist b md x y → ∀ (A : { A : SimplicialComplex V // A ∈ b.apartmentSystem.apartments }), (∃ s ∈ (↑A).faces, x ∈ s) → (∃ s ∈ (↑A).faces, y ∈ s) → ∃ s ∈ (↑A).faces, z_t ∈ s) : NegCurvatureIneq b md

An affine building with a distance-non-increasing retraction onto each apartment and a Euclidean realisation of every apartment satisfies the CAT(0) negative-curvature inequality. This reduces the inequality to the Euclidean parallelogram identity inside one apartment after retracting.

structure AffineBuilding.IsCAT0 {V : Type u_1} [DecidableEq V] (b : Building V) (md : ApartmentMetricData b) : Prop

A building $(\mathcal{B}, d)$ is CAT(0) if it is a complete geodesic metric space satisfying the negative-curvature (CAT(0)) inequality on every geodesic triangle. This is the geometric form of "non-positive curvature".

• metric : IsMetricSpace b md
• geodesic : IsGeodesic b md
• neg_curvature : NegCurvatureIneq b md

structure AffineBuilding.EuclideanRealizationData {V : Type u_1} [DecidableEq V] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (b : Building V) (md : ApartmentMetricData b) : Type (max u_1 u_2)

Data realising each apartment of a building as an isometric copy of a Euclidean (inner product) space $E$: coordinates, the distance-as-norm identity, and the fact that the geodesic point in the apartment maps to the Euclidean barycentric combination.

• coord : { A : SimplicialComplex V // A ∈ b.apartmentSystem.apartments } → V → E
• dist_eq_norm (A : { A : SimplicialComplex V // A ∈ b.apartmentSystem.apartments }) (u v : V) : md.dist_fn A u v = ‖self.coord A u - self.coord A v‖
• coord_geodesic (A : { A : SimplicialComplex V // A ∈ b.apartmentSystem.apartments }) (x y z_t : V) (t : ℝ) : (∃ s ∈ (↑A).faces, x ∈ s) → (∃ s ∈ (↑A).faces, y ∈ s) → (∃ s ∈ (↑A).faces, z_t ∈ s) → md.dist_fn A z_t x = (1 - t) * md.dist_fn A x y → md.dist_fn A z_t y = t * md.dist_fn A x y → self.coord A z_t = t • self.coord A x + (1 - t) • self.coord A y

structure AffineBuilding.BuildingRetractionData {V : Type u_1} [DecidableEq V] (b : Building V) (md : ApartmentMetricData b) : Prop

Data witnessing that a building admits suitable retractions: for any four vertices $x, y, z, z_t$ there is a distance-non-increasing retraction $\rho$ to an apartment $A$ containing $x$, $y$, $\rho z$ and fixing $x$ and $y$, together with the assertion that a geodesic point $z_t$ remains in any apartment containing both endpoints.

• retract_exists (x y z z_t : V) : ∃ (ρ : V → V) (A : { A : SimplicialComplex V // A ∈ b.apartmentSystem.apartments }), (∃ s ∈ (↑A).faces, x ∈ s) ∧ (∃ s ∈ (↑A).faces, y ∈ s) ∧ (∃ s ∈ (↑A).faces, ρ z ∈ s) ∧ ρ x = x ∧ ρ y = y ∧ (∀ (u v : V), buildingDist b md (ρ u) (ρ v) ≤ buildingDist b md u v) ∧ buildingDist b md z z_t = buildingDist b md (ρ z) z_t
• zt_in_apt (x y z_t : V) (t : ℝ) : 0 ≤ t → t ≤ 1 → buildingDist b md z_t x = (1 - t) * buildingDist b md x y → buildingDist b md z_t y = t * buildingDist b md x y → ∀ (A : { A : SimplicialComplex V // A ∈ b.apartmentSystem.apartments }), (∃ s ∈ (↑A).faces, x ∈ s) → (∃ s ∈ (↑A).faces, y ∈ s) → ∃ s ∈ (↑A).faces, z_t ∈ s

def AffineBuilding.IsContractible {V : Type u_1} [DecidableEq V] (b : Building V) (md : ApartmentMetricData b) : Prop

The building is contractible: there is a base point $y_0$ and a homotopy $f : [0,1] \times \mathcal{B} \to \mathcal{B}$ with $f(1, \cdot) = \mathrm{id}$, $f(0, \cdot) = y_0$, geodesic-distance constraints, and joint continuity in $(t, x)$.

def AffineBuilding.IsComplete {V : Type u_1} [DecidableEq V] (b : Building V) (md : ApartmentMetricData b) : Prop

The building is complete: every Cauchy sequence of vertices converges to a limit in $V$.