OAI/NumberTheory/DukePrimeDegree/Geometry/HorosphereAtomicSupport.lean

The atomic horospherical support theorem

This proves the support conclusion used in EKL (2006), Lemma 4.4(1). For each peripheral root, an explicit diagonal flow isolates its matrix entry. Atomicity and compact recurrence force that entry to vanish. Thus only the distinguished root remains. This argument establishes the needed consequence directly, without assuming the general product formula of Einsiedler–Katok (2003), Proposition 8.3.