Angle rigidity holds for any chart-compatible direction assignment
DisprovedEuclideanBuildingDirections.angleRigidity_of_chart_dirRetired 2026-09-07 — disproved, false as formalized. Do not use as a dependency.
EuclideanBuildingData (Def_frame_2026_harmonic_building_interfaces) carries only Kleiner--Leeb EB3 (pair_mem_apartment, ray_mem_apartment, line_mem_apartment), EB4 (overlap_compatible), atlas maximality and the Hadamard condition. It has no direction map and neither EB1 (directions) nor EB2 (angle rigidity) -- the two axioms Kleiner--Leeb call the key geometric ingredient (Publ. Math. IHES 86 (1997), §4.1.2). Those axioms do not follow from apartment coverage and chart compatibility, so a structure satisfying the posted axioms need not be a Euclidean building and need not admit a direction assignment at all.
The corrected structure is BuildingWithDirections in Def_euclidean_building_directions, which carries all four axioms; EuclideanBuildingDirections.exists_euclideanBuildingData (Proved) gives the converse passage. No corrected replacement for this statement exists yet.
import Definitions.Def_euclidean_building_directions
namespace EuclideanBuildingDirections
open HarmonicBuilding MetricGeometry
theorem angleRigidity_of_chart_dir {N : ℕ} (C : EuclideanCoxeterData N)
{X : Type*} [MetricSpace X] [CompleteSpace X]
(E : EuclideanBuildingData N C X)
(dir : X → X → ModelEuclideanSpace N)
(hunit : ∀ x y : X, x ≠ y → ‖dir x y‖ = 1)
(hchart : ∀ c ∈ E.atlas, ∀ p q : ModelEuclideanSpace N, p ≠ q →
∃ w : C.weyl,
dir (c p) (c q) = (w : OrthogonalGroup N) (segmentDirection p q)) :
∀ x y z : X, ∀ g₁ g₂ : ℝ → X, x ≠ y → x ≠ z →
IsGeodesicSegment g₁ x y → IsGeodesicSegment g₂ x z →
∃ w : C.weyl,
alexandrovAngle x g₁ g₂
= InnerProductGeometry.angle (dir x y)
((w : OrthogonalGroup N) (dir x z)) := by sorry
end EuclideanBuildingDirections