A Euclidean building given by a maximal atlas is one in the sense of Kleiner--Leeb

Every Euclidean building given by a maximal atlas of apartments is a Euclidean building in the sense of Kleiner and Leeb: if $X$ is a complete CAT(0) space with a maximal atlas $\mathcal A$ of apartments modelled on the Euclidean Coxeter data $C$, in which every segment, ray and line is contained and whose overlaps are governed by the affine Weyl group, then $X$ carries a $\Delta_{\mathrm{mod}}$-direction structure satisfying EB1 and EB2 whose atlas is exactly $\mathcal A$.

Role. Together with EuclideanBuildingDirections.exists_euclideanBuildingData, which goes the other way, this makes the two descriptions of a Euclidean building used here interchangeable. Its purpose in this development is to remove a duplication: several statements are formulated twice, once over an atlas and once over a direction structure, and the analytic content — the tangent-map reduction, the order of a harmonic map, the closed billiards path — has to be proved only once if the two settings can be translated into each other.

Two of the fields of the direction structure are elementary consequences of maximality of the atlas rather than new content. Closure under precomposition with the affine Weyl group is one: if $c$ is compatible with every chart of the atlas by an element $w$, then $c\circ g$ is compatible with the same chart by $g^{-1}w$, so $c\circ g$ is again in the atlas. The coverage axioms and the CAT(0) condition are carried over unchanged. What is genuinely new is the direction assignment itself, which is supplied by EuclideanBuildingDirections.exists_directionAssignment.

Formalization note. The conclusion records that the resulting structure has the same atlas, so that a chart used on one side is available on the other.